Note that this approach will fail if the term to be rewritten is under a variable binding.
MP_REWRITE_TAC REAL_DIV_REFL ([], ``!x. x <> 0 ==> P (x/x)``) gives back an unprovable x <> 0 as a new subgoal, and also fails to simplify the bound x/x in the “original” branch. (Put `x*x + 1` in `x` if you want a slightly more realistic instance; the simplifier can obviously discharge the side-condition on the original by itself.) Even with the quantification gone, the x <> 0 assumption also needs to be stripped as well to make MP_REWRITE_TAC do the right thing. For this reason, I think the best solution (I don’t have one right now!) to this problem would integrate with the simplifier and its ability to accumulate context as it traverses a term. Michael On 23/11/12 07:31, Vincent Aravantinos wrote: > Hi list, > I often face the following small but annoying problem: > * Situation: > - I have a theorem (say, "Th") of the form "P ==> t = u" > ex: REAL_DIV_REFL > (|- !x. ~(x = &0) ==> x / x = &1 in HOL-Light, |- !x. x <> 0 ==> (x > / x = 1) in HOL4) > - the conclusion of my goal is a (big) term containing a subterm > (say, " t' ") matching t > ex: a big expression with a subterm t / t somewhere deep inside the > term > * My aim: rewrite t' into u' using Th > * Solution: > - make a subgoal to prove P' (the instance of P corresponding to t') > ex: t / t <> &0 > (assume t is a big expression to make it annoying to type in) > - use this subgoal to rewrite the original goal > * Problem: > What annoys me in this frequent use case is that I have to explicitly > state the subgoal P' whereas it seems it can be automatized. > So, questions: > - Am I the only one to find this annoying? :-) > - If not, I imagine there might already exist a tactic that solves > this recurrent problem, but if so I did not find it ? > * Possible solution: > If not, I developed my own tactic which a couple of students here at > HVG have been using and found useful. > Please find below the implementation in HOL4 and HOL Light, the > tactic is called "MP_REWRITE_TAC". > In order to use it, e.g., for the above situation, just use: > e(MP_REWRITE_TAC REAL_DIV_REFL) > then the tactic will: > - search the goal for a subterm matching t (if several matches it > takes the first one it finds), > - introduce a subgoal for the corresponding P', > - rewrite the original goal with Th, taking P' into account. > - add P' to the set of assumptions of the original goal, so that it > can be reused later if needed. > Regards, > V. > Code: > HOL-Light: > let MP_REWRITE_TAC th (_,c as g) = > let sel = lhs o snd o strip_forall o snd o dest_imp in > let PART_MATCH = PART_MATCH sel (SPEC_ALL th) in > let th = ref TRUTH in > ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> > false) c); > (SUBGOAL_THEN (lhand (concl !th)) (fun x -> > REWRITE_TAC[MP !th x] THEN STRIP_ASSUME_TAC x)) g;; > HOL4: > fun MP_REWRITE_TAC th g = > let > val sel = lhs o snd o strip_forall o snd o dest_imp > val PART_MATCH = PART_MATCH sel (SPEC_ALL th) > val th = ref TRUTH > val _ = > find_term (fn t => (th := PART_MATCH t; true) handle _ => false) > (snd g) > in > (SUBGOAL_THEN (lhand (concl (!th))) (fn x => > REWRITE_TAC[MP (!th) x] THEN STRIP_ASSUME_TAC x)) g > end;
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
