[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"

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)
  have "range int \<subseteq> (UNIV::int set)" by simp
  ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)


This is what you are looking for as "infinite" is defined as 
"not finite".

Hope this helps,

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