*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Generalized elimination rule?*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Wed, 10 Mar 2010 12:44:34 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Brian Huffman <brianh at cs.pdx.edu>*In-reply-to*: <4B967FA7.80405@uni-muenster.de>*References*: <4B86BBA6.803@uni-muenster.de> <cc2478ab1002251054r16465cc0t1f7be1a9ad9a44f2@mail.gmail.com> <4B870B93.1030904@rsise.anu.edu.au> <4B967FA7.80405@uni-muenster.de>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Peter Lammich wrote:

Hi Brian, Many thanks you for your answer.I adopted your proposal for my needs. However, I ran into a problemthat should also be imminent in your proposal (?).If there are premises of the form !!x. _==>_, they are counted innhyps, however dtac keepI will not unify against them, thusval ktac = EVERY' (replicate nhyps (dtac keepI)) : int -> tactic ; produces premises that are doubly-wrapped into keep. What's the best way around? Only counting "plain" premises? (How?) Can keepI be defined to also wrap higher-order premises? Best, Peter

Dear Peter, I'm not quite sure if I understand you correctly.

(Isn't this rather unusual - could I see an example of how this arises ?) Certainly, keep, as I defined it, won't wrap around a premise of the form

Regards, Jeremy

consts meta_keep :: "bool => prop => prop" defs meta_keep_def : "meta_keep b f == f" val meta_iffD2 = prove_goal ProtoPure.thy "[| PROP P==PROP Q; PROP Q |] ==> PROP P" (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]); val meta_iffD1 = symmetric_thm RS meta_iffD2; val meta_iffDs = [meta_iffD1, meta_iffD2] ; val _ = ListPair.app bind_thm (["meta_keepD", "meta_keepI"], [meta_keep_def] RL meta_iffDs) ; val _ = bind_thm ("meta_keepTD", read_instantiate [("b", "True")] meta_keepD) ; val _ = bind_thm ("meta_keepFD", read_instantiate [("b", "False")] meta_keepD) ; val _ = bind_thm ("meta_keepF_thin", meta_keepFD RS thin_rl) ; (* meta_fetac : thm -> int -> int -> tactic like fatac n but also deletes hypotheses matched *) fun meta_fetac th n sg st = let val fth = thin_rl RS (replicate n meta_keepFD MRS th) : thm ; val subgoal = List.nth (prems_of st, sg - 1) : term ; (* turn all subgoal hypotheses H into meta_keep ?b H *) val nhyps = length (Logic.strip_assums_hyp subgoal) ; val ktac = EVERY' (replicate nhyps (dtac meta_keepI)) : int -> tactic ; (* then apply ftac fth - see later *) (* then apply atac n times, which marks the hypotheses to be deleted with meta_keep False *) val atacs = EVERY' (replicate n atac) ; (* treat other instances of meta_keep ?b as meta_keep True, and erase *) val ekttac = REPEAT o dtac meta_keepTD : int -> tactic ; (* delete hypotheses which are (meta_keep False ...) *) val ekftac = REPEAT o etac meta_keepF_thin : int -> tactic ; (* combine all the above *) val ctac = EVERY' [ktac, ftac fth, atacs] THEN_ALL_NEW (ekttac THEN' ekftac) : int -> tactic ; in ctac sg st end ;

**Follow-Ups**:**Re: [isabelle] Generalized elimination rule?***From:*Peter Lammich

**References**:**Re: [isabelle] Generalized elimination rule?***From:*Peter Lammich

- Previous by Date: Re: [isabelle] bijections to/from the natural numbers
- Next by Date: Re: [isabelle] bijections to/from the natural numbers
- Previous by Thread: Re: [isabelle] Generalized elimination rule?
- Next by Thread: Re: [isabelle] Generalized elimination rule?
- Cl-isabelle-users March 2010 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