# [isabelle] Showing that type 'int' is infinite

John Matthews writes:
> 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?
Hi John,
I think the best way is to use the facts that there is an
injection from nats to ints and that there are infinitely
many nats. My proof would go as follows
theory Test
imports "Infinite_Set"
begin
lemma infinite_int:
shows "infinite (UNIV::int set)"
proof -
have "inj int" by (rule inj_int)
then have "infinite (range int)" by (rule range_inj_infinite)
moreover
have "range int \<subseteq> (UNIV::int set)" by simp
ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
qed
end
This is what you are looking for as "infinite" is defined as
"not finite".
Hope this helps,
Christian

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