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