# [isabelle] can't prove "True => True"

The following lemma:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
theory bug imports Main GCD
begin
lemma test:
"gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) *
((Suc (Suc 0) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) +
2 * ((3 + Suc (Suc 0) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) -
Suc (Suc (Suc (Suc 0))) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc
0))))) mod
3)) mod
6) ~=
4
==> gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) *
((Suc (Suc 0) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc 0)))) +
2 * ((3 + Suc (Suc 0) div gcd (Suc (Suc 0), Suc (Suc (Suc (Suc
0)))) -
Suc (Suc (Suc (Suc 0))) div gcd (Suc (Suc 0), Suc (Suc (Suc
(Suc 0))))) mod
3)) mod
6) =
10"
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
is "True => True" in that if I try to apply 'value' to each side of the
==>, Isabelle immediately returns True in both cases, but I cannot figure
out how to prove the above lemma.
What sort of tactic should I be using in this case? Or is there some
bug here? Perhaps the fact that apply(eval) reports:
*** exception TERM raised: dest_Trueprop
will be helpful to someone, but I can't say I fully understand it. I am not
sure why, for example,
lemma doh:
"1+1=(3::nat) --> 1+1=(4::nat)"
apply(eval)
done
works, but
lemma doh:
"1+1=(3::nat) ==> 1+1=(4::nat)"
apply(eval)
done
fails. Is this exception the intended behaviour for the latter case? Note
that using 'auto' rather than 'eval' will prove both versions of lemma
"doh", but auto will _not_ prove lemma "test", above.
Puzzled,
Duraid

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