*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*: Fri, 3 Apr 2015 07:02:36 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <551DB1BE.9050308@in.tum.de>*References*: <551D646E.9060508@in.tum.de> <5AD61EC4-4357-4542-A826-081AB4BE3623@inria.fr> <551DB1BE.9050308@in.tum.de>

> 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:*Manuel Eberl

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

- Previous by Date: Re: [isabelle] An induction rule
- Next by Date: Re: [isabelle] An induction rule
- 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