summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 01 Feb 2007 13:41:19 +0100 | |

changeset 22226 | 699385e6cb45 |

parent 22225 | 30ab97554602 |

child 22227 | 7f88a6848fc2 |

new theorem int_infinite

--- a/src/HOL/Library/Infinite_Set.thy Wed Jan 31 20:07:40 2007 +0100 +++ b/src/HOL/Library/Infinite_Set.thy Thu Feb 01 13:41:19 2007 +0100 @@ -215,6 +215,15 @@ then show False by simp qed +lemma int_infinite [simp]: + shows "infinite (UNIV::int set)" +proof - + from inj_int 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 + text {* The ``only if'' direction is harder because it requires the construction of a sequence of pairwise different elements of an