Hi Vincent,
Peter Homeier has given a thorough treatment of just this problem some
time ago. It can be found in the structure "dep_rewrite". It seems you have
to load it before opening it. There is documentation in
src/1/dep_rewrite.sml
in the distribution.
Cheers,
Konrad.
On Thu, Nov 22, 2012 at 2:31 PM, Vincent Aravantinos <
[email protected]> 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;
>
> --
> Vincent Aravantinos
> Postdoctoral Fellow, Concordia University, Hardware Verification Group
> http://users.encs.concordia.ca/~vincent
>
>
>
> ------------------------------------------------------------------------------
> 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
>
------------------------------------------------------------------------------
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
