*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] arith*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 03 Jun 2008 07:13:40 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <52B3F22D-9FF6-4E77-BBE1-B1A236EA5AC9@galois.com>*References*: <52B3F22D-9FF6-4E77-BBE1-B1A236EA5AC9@galois.com>*User-agent*: Thunderbird 2.0.0.9 (Macintosh/20071031)

Thank you, that should not be the case, will look into it (at some point). Tobias John Matthews schrieb:

I've come across some strange behavior with the arith proof method inIsabelle2007. It is able to prove the following lemma:lemma "[| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"(Here f is a free variable). However, if I turn x into a parameter ofthe subgoal, then arith fails:lemma "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2" On the other hand, if I replace (f x) with z, then it works again: lemma "!!x. [| 0 <= (x::int); x div 2 < z |] ==> x < z * 2" Thanks, -john

**References**:**[isabelle] arith***From:*John Matthews

- Previous by Date: [isabelle] arith
- Next by Date: Re: [isabelle] Nested Recursion inside a tuple
- Previous by Thread: [isabelle] arith
- Next by Thread: [isabelle] Isabelle problem
- Cl-isabelle-users June 2008 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