*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Modify theorem with equality assumption*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Sat, 4 Apr 2015 08:28:14 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <551E6982.6090606@in.tum.de>*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> <551E6982.6090606@in.tum.de>

Hi Manuel, > On 03.04.2015, at 12:20, Manuel Eberl <eberlm at in.tum.de <mailto:eberlm at in.tum.de>> wrote: > > 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. Normally, when allocating names, I would (following an idiom I learned from Dmitriy) still use the original context without the names and thread that one through the program, i.e. âunfold ctxtâ without prime. I think you can get into trouble if you start using âctxtâ â, e.g. if you define new types or constants. Typically, the only place where you need âctxtâ â is in an âexportâ or when allocating further names. Dmitriy usually calls these contexts âctxt_namesâ, to clarify their role. Otherwise, if youâre an eta-macho, you can kill the âthmâ argument and change all â|>ââs to â#>ââs. Itâs quite tempting in your example, actually. ;) Jasmin

**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

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

- Previous by Date: Re: [isabelle] CFP: 10th Panhellenic Logic Symposium -- deadline extension: April 12
- Next by Date: [isabelle] finally published online: GÃdelâs Incompleteness Theorems
- 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