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