While pattern matching is one of my favorite things about OCaml, I'm not sure this fits well in Python. A big part of Python is trying to keep the language from being all things to all people and accumulating esoteric cruft, especially in the syntax. If I ran the zoo, I would have probably chosen a slightly different subset of features for Python, but I have a lot of respect for Guido's intent.
Also, doing anything by overloading arithmetic operators for a semantically unrelated purpose tends to be pretty disharmonious with the rest of the language. The only exception I can think of is Lua's LPEG (http://www.inf.puc-rio.br/~roberto/lpeg/lpeg.html), but that's a specific sub-language that tends to be clearly isolated to grammars; in practice, it's usually as distinct as using * within regular expression strings.
I wrote some pattern matching code myself for python a few months back just for fun. It was extremely unpythonic, but a fun exercise. For comparison, here's my code:
While I don't have direct experience with either of these (I just googled for "python prolog backtracking"), you could probably do just as well in idiomatic Python using generators:
Also, doing anything by overloading arithmetic operators for a semantically unrelated purpose tends to be pretty disharmonious with the rest of the language. The only exception I can think of is Lua's LPEG (http://www.inf.puc-rio.br/~roberto/lpeg/lpeg.html), but that's a specific sub-language that tends to be clearly isolated to grammars; in practice, it's usually as distinct as using * within regular expression strings.