Re: [isabelle] Proof failed using rules



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





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