*To*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Subject*: Re: [isabelle] Modify theorem with equality assumption*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 03 Apr 2015 12:20:50 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <A9D5660E-91C3-413E-925D-9AECE3D68775@inria.fr>*References*: <551D646E.9060508@in.tum.de> <5AD61EC4-4357-4542-A826-081AB4BE3623@inria.fr> <551DB1BE.9050308@in.tum.de> <A9D5660E-91C3-413E-925D-9AECE3D68775@inria.fr>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0

Yes, I do another step. I do not assume the equation directly, but something that implies it. A function that does what I actually asked is this: fun generalize_master_thm ctxt thm = let val ([p'], ctxt') = Variable.variant_fixes ["p''"] ctxt val p' = Free (p', HOLogic.realT) val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (@{term "p"}, p')) val cprop = Thm.cterm_of ctxt prop in thm |> Local_Defs.unfold ctxt' [Thm.assume cprop] |> Thm.implies_intr cprop |> rotate_prems 1 |> singleton (Variable.export ctxt' ctxt) end with 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) and output theorem g â O(Îx. real x powr ?p') â 1 < (âi<k. as ! i * bs ! i powr ?p') â eventually (Îx. 0 < f x) sequentially â p = ?p''1 â f â Î(Îx. real x powr ?p''1) What I would like to know is whether any of the things I do are considered bad style. Cheers, Manuel On 03/04/15 07:02, Jasmin Blanchette wrote: >> On 02.04.2015, at 23:16, Manuel Eberl <eberlm at in.tum.de> wrote: >> >> 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? > I donât know, but this > >> 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) > looks different from what you described abstractly in your previous email. > > 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

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

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

- Previous by Date: Re: [isabelle] An induction rule
- Next by Date: Re: [isabelle] CFP: 10th Panhellenic Logic Symposium -- deadline extension: April 12
- 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