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,
	Florian

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

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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