1785 by simp |
1785 by simp |
1786 qed |
1786 qed |
1787 |
1787 |
1788 hide_const (open) Finite_Set.fold |
1788 hide_const (open) Finite_Set.fold |
1789 |
1789 |
|
1790 |
|
1791 subsection "Infinite Sets" |
|
1792 |
|
1793 text \<open> |
|
1794 Some elementary facts about infinite sets, mostly by Stephan Merz. |
|
1795 Beware! Because "infinite" merely abbreviates a negation, these |
|
1796 lemmas may not work well with \<open>blast\<close>. |
|
1797 \<close> |
|
1798 |
|
1799 abbreviation infinite :: "'a set \<Rightarrow> bool" |
|
1800 where "infinite S \<equiv> \<not> finite S" |
|
1801 |
|
1802 text \<open> |
|
1803 Infinite sets are non-empty, and if we remove some elements from an |
|
1804 infinite set, the result is still infinite. |
|
1805 \<close> |
|
1806 |
|
1807 lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}" |
|
1808 by auto |
|
1809 |
|
1810 lemma infinite_remove: "infinite S \<Longrightarrow> infinite (S - {a})" |
|
1811 by simp |
|
1812 |
|
1813 lemma Diff_infinite_finite: |
|
1814 assumes T: "finite T" and S: "infinite S" |
|
1815 shows "infinite (S - T)" |
|
1816 using T |
|
1817 proof induct |
|
1818 from S |
|
1819 show "infinite (S - {})" by auto |
|
1820 next |
|
1821 fix T x |
|
1822 assume ih: "infinite (S - T)" |
|
1823 have "S - (insert x T) = (S - T) - {x}" |
|
1824 by (rule Diff_insert) |
|
1825 with ih |
|
1826 show "infinite (S - (insert x T))" |
|
1827 by (simp add: infinite_remove) |
|
1828 qed |
|
1829 |
|
1830 lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)" |
|
1831 by simp |
|
1832 |
|
1833 lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
1834 by simp |
|
1835 |
|
1836 lemma infinite_super: |
|
1837 assumes T: "S \<subseteq> T" and S: "infinite S" |
|
1838 shows "infinite T" |
|
1839 proof |
|
1840 assume "finite T" |
|
1841 with T have "finite S" by (simp add: finite_subset) |
|
1842 with S show False by simp |
|
1843 qed |
|
1844 |
|
1845 proposition infinite_coinduct [consumes 1, case_names infinite]: |
|
1846 assumes "X A" |
|
1847 and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})" |
|
1848 shows "infinite A" |
|
1849 proof |
|
1850 assume "finite A" |
|
1851 then show False using \<open>X A\<close> |
|
1852 proof (induction rule: finite_psubset_induct) |
|
1853 case (psubset A) |
|
1854 then obtain x where "x \<in> A" "X (A - {x}) \<or> infinite (A - {x})" |
|
1855 using local.step psubset.prems by blast |
|
1856 then have "X (A - {x})" |
|
1857 using psubset.hyps by blast |
|
1858 show False |
|
1859 apply (rule psubset.IH [where B = "A - {x}"]) |
|
1860 using \<open>x \<in> A\<close> apply blast |
|
1861 by (simp add: \<open>X (A - {x})\<close>) |
|
1862 qed |
|
1863 qed |
|
1864 |
|
1865 text \<open> |
|
1866 For any function with infinite domain and finite range there is some |
|
1867 element that is the image of infinitely many domain elements. In |
|
1868 particular, any infinite sequence of elements from a finite set |
|
1869 contains some element that occurs infinitely often. |
|
1870 \<close> |
|
1871 |
|
1872 lemma inf_img_fin_dom': |
|
1873 assumes img: "finite (f ` A)" and dom: "infinite A" |
|
1874 shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)" |
|
1875 proof (rule ccontr) |
|
1876 have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto |
|
1877 moreover |
|
1878 assume "\<not> ?thesis" |
|
1879 with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast |
|
1880 ultimately have "finite A" by(rule finite_subset) |
|
1881 with dom show False by contradiction |
|
1882 qed |
|
1883 |
|
1884 lemma inf_img_fin_domE': |
|
1885 assumes "finite (f ` A)" and "infinite A" |
|
1886 obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)" |
|
1887 using assms by (blast dest: inf_img_fin_dom') |
|
1888 |
|
1889 lemma inf_img_fin_dom: |
|
1890 assumes img: "finite (f`A)" and dom: "infinite A" |
|
1891 shows "\<exists>y \<in> f`A. infinite (f -` {y})" |
|
1892 using inf_img_fin_dom'[OF assms] by auto |
|
1893 |
|
1894 lemma inf_img_fin_domE: |
|
1895 assumes "finite (f`A)" and "infinite A" |
|
1896 obtains y where "y \<in> f`A" and "infinite (f -` {y})" |
|
1897 using assms by (blast dest: inf_img_fin_dom) |
|
1898 |
|
1899 proposition finite_image_absD: |
|
1900 fixes S :: "'a::linordered_ring set" |
|
1901 shows "finite (abs ` S) \<Longrightarrow> finite S" |
|
1902 by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom) |
|
1903 |
1790 end |
1904 end |