[isabelle] Proof failed using rules


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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.