Re: [Hol-info] Automatic subgoal to apply a conditional rewrite

[Konrad S. <kon...@gm...>]

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 <
vin...@gm...> 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
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>