On 19.02.2014 14:41, Bill Richter wrote: > - if you have existentials or disjunctions in the theorems you want to > use or in the goal, use MESON_TAC > > By putting this after SIMP_TAC, I infer that SIMP_TAC will not handle > existentials or disjunctions. Indeed - most of the time.
Let me give you a brief overview of the main idea of REWRITE_TAC and how you get progressively to the complex version of it as it is now in HOL Light: ******* 1 in its most basic form, REWRITE_TAC just takes a theorem th of the form "|- !xyz. t = u", looks for any occurrence of "t" in the goal, and replaces them by the corresponding instantiation of "u". 2 in practice we often need to do this several times in a row, so REWRITE_TAC actually automatically repeats this procedure. -> this is how you can end up with non-terminating calls 3 non-termination is annoying but there are - say - two sorts of non-termination: * those that occur because we (user-side) did not expect a particular combination of theorems to actually trigger a cycle: in such cases, dealing with non-termination is the matter of the user * those that occur because a u matches t (using the notations above), e.g., commutativity theorem: in such cases, it is legitimate to consider that the user is not dumb enough to give such a theorem to REWRITE_TAC and hoping it will apply indefinitely. Such situations can be detected and dealt with: one could imagine rewriting only once in such cases, or not at all. What is done in HOL Light (and probably in HOL4 - don't remember), is to rewrite only if applying the rewrite would result in a "lower" term, according to an arbitrary (well-founded, and with other good properties) order. This way the rewrite applies finitely many times. -> this is the reason why you obtained the single rewrite the other day: the right-hand side of the equation of DIST_SYM matches its left-hand side, so applying it naively would yield non-termination, so we apply only if the order is satisfied, and only your middle "dist" was satisfying this property. 4 note that "!xyz. t <=> u" is just the same as "!xyz. t = u" if t is a boolean; so REWRITE_TAC can be used for free to rewrite boolean terms. 5 at this stage, REWRITE_TAC is already quite useful, but it could actually do more: theorems of the form "|- !xyz. p", where "p" is not an equality, are equivalent to "!xyz. p <=> T", so that REWRITE_TAC could also make use of them. Therefore when REWRITE_TAC gets such theorems, it transforms them automatically - i.e., behind the scene - into "!xyz. p <=> T". 6 similarly theorems of the form "|- !xyz. ~p" are turned into "|- !xyz. p = F" 7 with these two latter improvements, you generally get "T" and "F" all over the place in your goal, but this can be generally trivially removed by using usual identity relations like "T /\ x <=> x", "T \/ x <=> T", "~F <=> T", etc. These identities are implicitly added to the list of theorems that you give to REWRITE_TAC, without you knowing it, so that all these simplifications are made for free (for free on the user side) 8 finally if the goal happens to be rewritten completely to just "T", then the goal is automatically solved: this is what happens when REWRITE_TAC concludes a goal ******* And there you obtain basically what is REWRITE_TAC. You can take any of your daily rewrites and make a comparison with the above steps to see how it makes use of them. For info, some of the involved HOL Light functions: - "term_order" implements the order mentioned in 3 - the implicit transformations of 5 and 6 (among others) are implemented in "mk_rewrites" - you can see the theorems that are implicitly added (in 7) with the function "basic_rewrites" (and extend it with "extend_basic_rewrites") - you can get REWRITE_TAC without these implicit theorems by calling PURE_REWRITE_TAC I hope that helps. This will also help you understand the implementation of REWRITE_TAC if you want to have a look at them (in the file "simp.ml"). I can then tell you what SIMP_TAC adds to it if you're interested. -- Dr Vincent Aravantinos Analysis and Design of Dependable Systems fortiss GmbH <www.fortiss.org/en> T +49 (0)89 360 35 22 33 | Fx +49 (0)89 360 35 22 50 Guerickestrasse 25 | 80805 Munich | Germany ------------------------------------------------------------------------------ Managing the Performance of Cloud-Based Applications Take advantage of what the Cloud has to offer - Avoid Common Pitfalls. Read the Whitepaper. http://pubads.g.doubleclick.net/gampad/clk?id=121054471&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
