Hi Bill, | I'm quite mystified that the REWRITE_TAC[DIST_SYM] only rewrote the | middle dist term
Generally speaking, with constructs like REWRITE_TAC that apply rewrites repeatedly, there are special heuristics to deal with those that would obviously loop indefinitely. (This doesn't apply to more controlled strategies like ONCE_REWRITE_TAC.) Sometimes looping rewrites are just quietly ignored (there used to be a warning message but I eliminated it). With some "permutative" rewrites, HOL tries to do a bit better, applying the rewrite with ordering constraints to "normalize" a term. Typically the ordering is somewhat arbitrary (e.g. just alphabetical on variables), but it can be useful just to rewrite subterms consistently in different places. In simple cases this can even prove theorems for you, e.g. # g `(x + 1) + y + z = z + (1 + y) + x`;; Warning: Free variables in goal: x, y, z val it : goalstack = 1 subgoal (1 total) `(x + 1) + y + z = z + (1 + y) + x` # e(REWRITE_TAC[ADD_AC]);; val it : goalstack = No subgoals This idea goes back to Boyer and Moore, and you can find a more systematic treatment and many nice examples in a paper by Ursula Martin and Tobias Nipkow, "Ordered Rewriting and Confluence". http://www21.in.tum.de/~nipkow/pubs/cade90.html See p43 of the HOL Light tutorial for a bit more: http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf John. ------------------------------------------------------------------------------ Android apps run on BlackBerry 10 Introducing the new BlackBerry 10.2.1 Runtime for Android apps. Now with support for Jelly Bean, Bluetooth, Mapview and more. Get your Android app in front of a whole new audience. Start now. http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
