Re: [isabelle] Showing that type 'int' is infinite



John,

this is theorem nat_infinite (or nat_not_finite) from theory Infinite_Set.

All the best,
Stephan

John Matthews wrote:
I have a subgoal of the form

  1. "~ (finite (UNIV :: int set))"

However, I can't find a corresponding theorem using find_theorems in Isabelle/HOL. Nor was find_theorems produce successful on the terms "card (UNIV :: int set)" or "setsum ?f (UNIV :: int set)".

What is the best way to prove this subgoal?

Thanks,
-john
begin:vcard
fn:Stephan Merz
n:Merz;Stephan
org:INRIA Lorraine & LORIA
adr;quoted-printable:;;615 rue du Jardin Botanique;Villers-l=C3=A8s-Nancy;;54602;France
email;internet:Stephan.Merz at loria.fr
tel;work:(+33) 354 95 84 78
tel;fax:(+33) 383 41 30 79
x-mozilla-html:FALSE
url:http://www.loria.fr/~merz/
version:2.1
end:vcard



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