Re: [isabelle] can't prove "True => True"

Hi Duraid,

the issue is that "eval" is a very special method which compiles the
goal to prove into an ML term of type and then evaluates it, proving the
 goal if the result is true.  This does not work with statements
involving meta-connectives like ==> (though I perfectly agree that the
error message could be more explicit).

Usually, such closed expressions would be proven using method "simp".
Alas, for gcd there are no suitable default lemmas for "simp", making a
proof involving "simp" a little bit tedious (use find_theorems to search
for suitable simplification rules).

In your particular case, what would work is to simply leave out the
hypothesis since the conclusion alone is sufficient to prove (using "eval").

Hope this helps,

P.S. Note that you can also use numeral syntax for natural numbers.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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