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



Hi Florian,

On Mon, Nov 10, 2008 at 02:22:38PM +0100, Florian Haftmann wrote:
> 
> 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).

I see. I hadn't really bothered to look inside GCD properly, but I will now.
 
> In your particular case, what would work is to simply leave out the
> hypothesis since the conclusion alone is sufficient to prove (using "eval").

Actually, this lemma was just cut+pasted from a goal in a larger
development...
 
> P.S. Note that you can also use numeral syntax for natural numbers.

.. and I was about to say I had no idea where the 'Suc's came from, but now
I realise they just came through an import.

	Thanks,

	Duraid





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