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
