new theorem int_infinite
authorpaulson
Thu Feb 01 13:41:19 2007 +0100 (2007-02-01)
changeset 22226699385e6cb45
parent 22225 30ab97554602
child 22227 7f88a6848fc2
new theorem int_infinite
src/HOL/Library/Infinite_Set.thy
     1.1 --- a/src/HOL/Library/Infinite_Set.thy	Wed Jan 31 20:07:40 2007 +0100
     1.2 +++ b/src/HOL/Library/Infinite_Set.thy	Thu Feb 01 13:41:19 2007 +0100
     1.3 @@ -215,6 +215,15 @@
     1.4    then show False by simp
     1.5  qed
     1.6  
     1.7 +lemma int_infinite [simp]:
     1.8 +  shows "infinite (UNIV::int set)"
     1.9 +proof -
    1.10 +  from inj_int have "infinite (range int)" by (rule range_inj_infinite)
    1.11 +  moreover 
    1.12 +  have "range int \<subseteq> (UNIV::int set)" by simp
    1.13 +  ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
    1.14 +qed
    1.15 +
    1.16  text {*
    1.17    The ``only if'' direction is harder because it requires the
    1.18    construction of a sequence of pairwise different elements of an