Re: [isabelle] Modify theorem with equality assumption



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