Re: [isabelle] Proof failed using rules
Just like simp, auto uses equations only in the left-to-right direction.
PS you don't need any of the !! or the [rule_format].
Stephy Wong schrieb:
> 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