*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Proof failed using rules*From*: Stephy Wong <s.wong.731 at googlemail.com>*Date*: Sun, 15 Mar 2009 22:53:52 +0000

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

**Follow-Ups**:**Re: [isabelle] Proof failed using rules***From:*Tobias Nipkow

- Previous by Date: [isabelle] Slow rule application in case of many parameters?
- Next by Date: Re: [isabelle] How do I find out via "find_theorems", for an existing theorem, whether it is marked as simp/intro/elim?
- Previous by Thread: Re: [isabelle] Slow rule application in case of many parameters?
- Next by Thread: Re: [isabelle] Proof failed using rules
- 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