[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))
theorem t: "!! x y. gn_inj_Int(Bar(x, Foo(y))) >' 0"
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