*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Modify theorem with equality assumption*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Thu, 02 Apr 2015 23:16:46 +0200*In-reply-to*: <5AD61EC4-4357-4542-A826-081AB4BE3623@inria.fr>*References*: <551D646E.9060508@in.tum.de> <5AD61EC4-4357-4542-A826-081AB4BE3623@inria.fr>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0

It occurred to me to simply use theorem rewriting. The following piece of code seems to do what I want to do. Am I doing anything in there that I should not do or do differently? ML {* fun generalize_master_thm ctxt thm = let val ([p'], ctxt') = Variable.variant_fixes ["p''"] ctxt val p' = Free (p', HOLogic.realT) val a = @{term "nth as"} $ Bound 0 val b = @{term "Transcendental.powr"} $ (@{term "nth bs"} $ Bound 0) $ p' val f = Abs ("i", HOLogic.natT, @{term "op * :: real => real => real"} $ a $ b) val setsum = @{term "setsum :: (nat => real) => nat set => real"} $ f $ @{term "{..<k}"} val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (setsum, @{term "1::real"})) val cprop = Thm.cterm_of ctxt' prop in thm |> Local_Defs.unfold ctxt' [Thm.assume cprop RS @{thm p_unique}] |> Thm.implies_intr cprop |> rotate_prems 1 |> singleton (Variable.export ctxt' ctxt) end val _ = Pretty.writeln (Syntax.pretty_term @{context} (Thm.prop_of @{thm master1})) val _ = Pretty.writeln (Syntax.pretty_term @{context} (Thm.prop_of (generalize_master_thm @{context} @{thm master1}))) *} Input theorem: g â O(Îx. real x powr ?p') â 1 < (âi<k. as ! i * bs ! i powr ?p') â eventually (Îx. 0 < f x) sequentially â f â Î(Îx. real x powr p) Output theorem: g â O(Îx. real x powr ?p') â 1 < (âi<k. as ! i * bs ! i powr ?p') â eventually (Îx. 0 < f x) sequentially â (âi<k. as ! i * bs ! i powr ?p''1) = 1 â f â Î(Îx. real x powr ?p''1) Cheers, Manuel On 02/04/15 18:35, Jasmin Blanchette wrote: >> I have a number of theorems that contain some constant p both in their >> assumptions and in their conclusions. >> >> I now want to derive modified theorems from them by adding an assumption >> "p = ?q" (for a schematic variable ?q) and replace all occurrences of p >> in the assumptions and the conclusion with ?q. Ideally in ML. >> >> What is the easiest way to do that? > I think youâll have to instantiate the âsubstâ theorem with the right âPâ and âsâ (using âDrule.cterm_instantiateâ or other similar functions), then you can use resolution with your original theorems (e.g. âRSâ or âOFâ in ML). This is a bit tricky, but a good opportunity to exercise forward theorem derivations in Isabelle. > > Alternative: A backward proof. You construct the statement of the theorem you want to prove and write a little tactic to solve it. Here, both forward and backward are about equally difficult, because you need to build some terms (the âPâ instance in the forward proof, the goal statement in the backward proof). > > Jasmin > >

**Follow-Ups**:**Re: [isabelle] Modify theorem with equality assumption***From:*Jasmin Blanchette

**Re: [isabelle] Modify theorem with equality assumption***From:*Makarius

**References**:**[isabelle] Modify theorem with equality assumption***From:*Manuel Eberl

**Re: [isabelle] Modify theorem with equality assumption***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Modify theorem with equality assumption
- Next by Date: [isabelle] An induction rule
- Previous by Thread: Re: [isabelle] Modify theorem with equality assumption
- Next by Thread: Re: [isabelle] Modify theorem with equality assumption
- Cl-isabelle-users April 2015 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