*To*: Amine Chaieb <chaieb at in.tum.de>*Subject*: Re: [isabelle] Simple problem with variable instantiation*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Thu, 10 Apr 2008 10:50:11 +0200*Cc*: c fe <zehfee at googlemail.com>, isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <47FDD2E2.6020805@in.tum.de>*References*: <a1e5e35a0804090352y2e690edap16c01df21f126494@mail.gmail.com> <47FDD2E2.6020805@in.tum.de>*User-agent*: Thunderbird 2.0.0.12 (X11/20080226)

Amine Chaieb wrote:

Hi, The variable must be exactly the same as it appears in the theorem, i.e. ?c2.0 and not c2.0 All these theorems can be proved automatically by eg. arith. Best, Amine.

-- Peter

c fe wrote:Hallo, I stumbled upon a problem with Isabelle 2007 that didn't occur in Isabelle 2003 (IIRC). I made a small (not very meaningful) example: lemma test: "c1 + (c2::nat) < a ==> c1 < a" apply simp done lemma test': "a + (b::nat) < c ==> a < c" apply simp done lemma test2: "7 < (a::nat) ==> 5 < a" (* Now use either [1] or [2] *) [1] apply (rule_tac "c2.0"="2" in test) [2] apply (rule_tac b=2 in test') apply simp done If I want to use test to proof test2 I can't instantiate c2. That isn't a big problem as I can just make lemmas like test' but if there is a simple solution to this I'd be interested to hear about it. Thanks, Christoph Feller

**References**:**[isabelle] Simple problem with variable instantiation***From:*c fe

**Re: [isabelle] Simple problem with variable instantiation***From:*Amine Chaieb

- Previous by Date: Re: [isabelle] Simple problem with variable instantiation
- Next by Date: [isabelle] Fwd: mechanical proof of Boyer-Moore fast string searching
- Previous by Thread: Re: [isabelle] Simple problem with variable instantiation
- Next by Thread: [isabelle] CFP: Proof-Carrying Code workshop PCC 2008
- Cl-isabelle-users April 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