author | paulson |

Thu Feb 01 13:41:19 2007 +0100 (2007-02-01) | |

changeset 22226 | 699385e6cb45 |

parent 22225 | 30ab97554602 |

child 22227 | 7f88a6848fc2 |

new theorem int_infinite

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