# [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.