*To*: Duraid Madina <duraid at kinoko.c.u-tokyo.ac.jp>*Subject*: Re: [isabelle] can't prove "True => True"*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Mon, 10 Nov 2008 14:22:38 +0100*Cc*: USR Isabelle <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <20081109155723.GA79514@kinoko.c.u-tokyo.ac.jp>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <20081109155723.GA79514@kinoko.c.u-tokyo.ac.jp>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Hi Duraid, the issue is that "eval" is a very special method which compiles the goal to prove into an ML term of type and then evaluates it, proving the goal if the result is true. This does not work with statements involving meta-connectives like ==> (though I perfectly agree that the error message could be more explicit). Usually, such closed expressions would be proven using method "simp". Alas, for gcd there are no suitable default lemmas for "simp", making a proof involving "simp" a little bit tedious (use find_theorems to search for suitable simplification rules). In your particular case, what would work is to simply leave out the hypothesis since the conclusion alone is sufficient to prove (using "eval"). Hope this helps, Florian P.S. Note that you can also use numeral syntax for natural numbers. -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] can't prove "True => True"***From:*Duraid Madina

**References**:**[isabelle] can't prove "True => True"***From:*Duraid Madina

- Previous by Date: Re: [isabelle] can't prove "True => True"
- Next by Date: Re: [isabelle] can't prove "True => True"
- Previous by Thread: Re: [isabelle] can't prove "True => True"
- Next by Thread: Re: [isabelle] can't prove "True => True"
- Cl-isabelle-users November 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