*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] substituting in hypotheses*From*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*Date*: Wed, 24 Aug 2005 16:33:21 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <abaf6a1ae63d98b78f48a5b6f2439bea@galois.com>*Organization*: Australian National University*References*: <abaf6a1ae63d98b78f48a5b6f2439bea@galois.com>*User-agent*: Mozilla Thunderbird 0.9 (X11/20041124)

John Matthews wrote:

Is there anything analogous to Isar's "subst" method that allows me toperform a one-off substitution in a selected subgoal's hypothesis? Hereis a contrived example that could be proved trivially by auto, butdemonstrates what I'm trying to do in general:lemma L1: "(x::nat)+1 = x+1+0" by auto lemma silly: "[| P(x+1::nat); R(%(x::nat). x+1) |] ==> R(%x. x+1+0)"When proving "silly" I'd like to use lemma L1 to substitute "x+1+0" for"x+1" in the second hypotheses. Note thatapply (simp only: L1) will cause Isabelle to loop, and apply (unfold L1)fails. Even if unfold didn't fail here, it would likely also loop orunfold the occurrence of x+1 in the other hypothesis and conclusion of"silly", which I don't want.Currently, the easiest way I know of to perform the substitution in thehypothesis is through these cumbersome series of methods:apply (erule_tac Q="R(%x. x+1)" in contrapos_pp) apply (subst L1) apply (erule_tac Q="R (%x. x+1+0)" in contrapos_nn) Is there a more concise way to do this? Thanks, -john

John,

Goal "(x::nat)+1 = x+1+0"; auto(); qed "L1"; Goal "[| P(x+1::nat); R(%(x::nat). x+1) |] ==> R(%x. x+1+0)" ;

val conv = eqc [mk_eq L1] ; val tac = CONV_TAC (TDSTOP_CONV conv) ; (* this changes all three spots *) val abs_tac = CONV_TAC (TDSTOP_CONV (ABS_CONV conv)) ; (* this changes only immediately under an abstraction *) val ntac = CONV_TAC (TDSTOP_CONV (NTH_CONV [2] conv)) ; (* this changes only the second occurrence *) or indeed val ptac = CONV_GOAL_TAC (PREM_CONV 2 (TDSTOP_CONV conv)) 1 ; (* this works in premise 2 of goal 1 *) val ptac' = CONV_GOALS_TAC (PREM_CONV 2 (TDSTOP_CONV conv)) ; (* this works in premise 2 of any goal *) val ptac'' = CONV_TAC (TDSTOP_CONV (PREM_CONV 2 (TDSTOP_CONV conv))) ; (* this works anywhere in any second premise anywhere in the term *) (* and so on, as complicated as you like! *) Regards, Jeremy

**References**:**[isabelle] substituting in hypotheses***From:*John Matthews

- Previous by Date: Re: [isabelle] substituting in hypotheses
- Next by Date: Re: [isabelle] substituting in hypotheses
- Previous by Thread: Re: [isabelle] substituting in hypotheses
- Next by Thread: [isabelle] Does Isabelle (on Proof general) support comments in others languages (for example Chinese)
- Cl-isabelle-users August 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list