Re: [isabelle] Modify theorem with equality assumption



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.