# Re: [isabelle] Modify theorem with equality assumption

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

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
>

```

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