*To*: Stephy Wong <s.wong.731 at googlemail.com>*Subject*: Re: [isabelle] Proof failed using rules*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 16 Mar 2009 09:42:21 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <12d162d00903151553y6cc69acdl9d8d6f6479c4a2e@mail.gmail.com>*References*: <12d162d00903151553y6cc69acdl9d8d6f6479c4a2e@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.19 (Macintosh/20081209)

Just like simp, auto uses equations only in the left-to-right direction. Tobias PS you don't need any of the !! or the [rule_format]. Stephy Wong schrieb: > Hi, > > I have a rather basic problem and hope someone could help me out. > > I have no idea why the following fails: > > axioms Ax1 [rule_format] : "!! x y z. (y = Foo(z)) = (gn_inj_Int(Bar(x, y)) >> ' 0'" > > theorem t: "!! x y. gn_inj_Int(Bar(x, Foo(y))) >' 0" > using Ax1 > by auto > > Since Ax1 says that (gn_inj_Int(Bar(x, y)) >' 0 if and only if the second > argument of Bar is Foo(z), then how come t can't be proved? > > Any help will be appreciated. > > Regards, > Steph

**References**:**[isabelle] Proof failed using rules***From:*Stephy Wong

- Previous by Date: Re: [isabelle] How do I find out via "find_theorems", for an existing theorem, whether it is marked as simp/intro/elim?
- Next by Date: [isabelle] FCS 2009 call for paper
- Previous by Thread: [isabelle] Proof failed using rules
- Next by Thread: [isabelle] FCS 2009 call for paper
- Cl-isabelle-users March 2009 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