1757 qed |
1755 qed |
1758 qed |
1756 qed |
1759 qed |
1757 qed |
1760 |
1758 |
1761 text {* |
1759 text {* |
1762 \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc. |
1760 \medskip Completeness |
1763 *} |
1761 *} |
1764 |
1762 |
1765 lemma posreals_complete: |
|
1766 assumes positive_S: "\<forall>x \<in> S. 0 < x" |
|
1767 and not_empty_S: "\<exists>x. x \<in> S" |
|
1768 and upper_bound_Ex: "\<exists>u. isUb (UNIV::real set) S u" |
|
1769 shows "\<exists>t. isLub (UNIV::real set) S t" |
|
1770 proof |
|
1771 let ?pS = "{w. real_of_preal w \<in> S}" |
|
1772 |
|
1773 obtain u where "isUb UNIV S u" using upper_bound_Ex .. |
|
1774 hence sup: "\<forall>x \<in> S. x \<le> u" by (simp add: isUb_def setle_def) |
|
1775 |
|
1776 obtain x where x_in_S: "x \<in> S" using not_empty_S .. |
|
1777 hence x_gt_zero: "0 < x" using positive_S by simp |
|
1778 have "x \<le> u" using sup and x_in_S .. |
|
1779 hence "0 < u" using x_gt_zero by arith |
|
1780 |
|
1781 then obtain pu where u_is_pu: "u = real_of_preal pu" |
|
1782 by (auto simp add: real_gt_zero_preal_Ex) |
|
1783 |
|
1784 have pS_less_pu: "\<forall>pa \<in> ?pS. pa \<le> pu" |
|
1785 proof |
|
1786 fix pa |
|
1787 assume "pa \<in> ?pS" |
|
1788 then obtain a where a: "a \<in> S" "a = real_of_preal pa" |
|
1789 by simp |
|
1790 then have "a \<le> u" using sup by simp |
|
1791 with a show "pa \<le> pu" |
|
1792 using sup and u_is_pu by (simp add: real_of_preal_le_iff) |
|
1793 qed |
|
1794 |
|
1795 have "\<forall>y \<in> S. y \<le> real_of_preal (psup ?pS)" |
|
1796 proof |
|
1797 fix y |
|
1798 assume y_in_S: "y \<in> S" |
|
1799 hence "0 < y" using positive_S by simp |
|
1800 then obtain py where y_is_py: "y = real_of_preal py" |
|
1801 by (auto simp add: real_gt_zero_preal_Ex) |
|
1802 hence py_in_pS: "py \<in> ?pS" using y_in_S by simp |
|
1803 with pS_less_pu have "py \<le> psup ?pS" |
|
1804 by (rule preal_psup_le) |
|
1805 thus "y \<le> real_of_preal (psup ?pS)" |
|
1806 using y_is_py by (simp add: real_of_preal_le_iff) |
|
1807 qed |
|
1808 |
|
1809 moreover { |
|
1810 fix x |
|
1811 assume x_ub_S: "\<forall>y\<in>S. y \<le> x" |
|
1812 have "real_of_preal (psup ?pS) \<le> x" |
|
1813 proof - |
|
1814 obtain "s" where s_in_S: "s \<in> S" using not_empty_S .. |
|
1815 hence s_pos: "0 < s" using positive_S by simp |
|
1816 |
|
1817 hence "\<exists> ps. s = real_of_preal ps" by (simp add: real_gt_zero_preal_Ex) |
|
1818 then obtain "ps" where s_is_ps: "s = real_of_preal ps" .. |
|
1819 hence ps_in_pS: "ps \<in> {w. real_of_preal w \<in> S}" using s_in_S by simp |
|
1820 |
|
1821 from x_ub_S have "s \<le> x" using s_in_S .. |
|
1822 hence "0 < x" using s_pos by simp |
|
1823 hence "\<exists> px. x = real_of_preal px" by (simp add: real_gt_zero_preal_Ex) |
|
1824 then obtain "px" where x_is_px: "x = real_of_preal px" .. |
|
1825 |
|
1826 have "\<forall>pe \<in> ?pS. pe \<le> px" |
|
1827 proof |
|
1828 fix pe |
|
1829 assume "pe \<in> ?pS" |
|
1830 hence "real_of_preal pe \<in> S" by simp |
|
1831 hence "real_of_preal pe \<le> x" using x_ub_S by simp |
|
1832 thus "pe \<le> px" using x_is_px by (simp add: real_of_preal_le_iff) |
|
1833 qed |
|
1834 |
|
1835 moreover have "?pS \<noteq> {}" using ps_in_pS by auto |
|
1836 ultimately have "(psup ?pS) \<le> px" by (simp add: psup_le_ub) |
|
1837 thus "real_of_preal (psup ?pS) \<le> x" using x_is_px by (simp add: real_of_preal_le_iff) |
|
1838 qed |
|
1839 } |
|
1840 ultimately show "isLub UNIV S (real_of_preal (psup ?pS))" |
|
1841 by (simp add: isLub_def leastP_def isUb_def setle_def setge_def) |
|
1842 qed |
|
1843 |
|
1844 text {* |
|
1845 \medskip reals Completeness (again!) |
|
1846 *} |
|
1847 |
|
1848 lemma reals_complete: |
1763 lemma reals_complete: |
|
1764 fixes S :: "real set" |
1849 assumes notempty_S: "\<exists>X. X \<in> S" |
1765 assumes notempty_S: "\<exists>X. X \<in> S" |
1850 and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y" |
1766 and exists_Ub: "bdd_above S" |
1851 shows "\<exists>t. isLub (UNIV :: real set) S t" |
1767 shows "\<exists>x. (\<forall>s\<in>S. s \<le> x) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> x \<le> y)" |
1852 proof - |
1768 proof - |
1853 obtain X where X_in_S: "X \<in> S" using notempty_S .. |
1769 obtain X where X_in_S: "X \<in> S" using notempty_S .. |
1854 obtain Y where Y_isUb: "isUb (UNIV::real set) S Y" |
1770 obtain Y where Y_isUb: "\<forall>s\<in>S. s \<le> Y" |
1855 using exists_Ub .. |
1771 using exists_Ub by (auto simp: bdd_above_def) |
1856 let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (-X) + 1} \<inter> {x. 0 < x}" |
1772 let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (-X) + 1} \<inter> {x. 0 < x}" |
1857 |
1773 |
1858 { |
1774 { |
1859 fix x |
1775 fix x |
1860 assume "isUb (UNIV::real set) S x" |
1776 assume S_le_x: "\<forall>s\<in>S. s \<le> x" |
1861 hence S_le_x: "\<forall> y \<in> S. y <= x" |
|
1862 by (simp add: isUb_def setle_def) |
|
1863 { |
1777 { |
1864 fix s |
1778 fix s |
1865 assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}" |
1779 assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}" |
1866 hence "\<exists> x \<in> S. s = x + -X + 1" .. |
1780 hence "\<exists> x \<in> S. s = x + -X + 1" .. |
1867 then obtain x1 where x1: "x1 \<in> S" "s = x1 + (-X) + 1" .. |
1781 then obtain x1 where x1: "x1 \<in> S" "s = x1 + (-X) + 1" .. |
1868 then have "x1 \<le> x" using S_le_x by simp |
1782 then have "x1 \<le> x" using S_le_x by simp |
1869 with x1 have "s \<le> x + - X + 1" by arith |
1783 with x1 have "s \<le> x + - X + 1" by arith |
1870 } |
1784 } |
1871 then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)" |
1785 then have "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1" |
1872 by (auto simp add: isUb_def setle_def) |
1786 by auto |
1873 } note S_Ub_is_SHIFT_Ub = this |
1787 } note S_Ub_is_SHIFT_Ub = this |
1874 |
1788 |
1875 hence "isUb UNIV ?SHIFT (Y + (-X) + 1)" using Y_isUb by simp |
1789 have *: "\<forall>s\<in>?SHIFT. s \<le> Y + (-X) + 1" using Y_isUb by (rule S_Ub_is_SHIFT_Ub) |
1876 hence "\<exists>Z. isUb UNIV ?SHIFT Z" .. |
1790 have "\<forall>s\<in>?SHIFT. s < Y + (-X) + 2" |
|
1791 proof |
|
1792 fix s assume "s\<in>?SHIFT" |
|
1793 with * have "s \<le> Y + (-X) + 1" by simp |
|
1794 also have "\<dots> < Y + (-X) + 2" by simp |
|
1795 finally show "s < Y + (-X) + 2" . |
|
1796 qed |
1877 moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto |
1797 moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto |
1878 moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT" |
1798 moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT" |
1879 using X_in_S and Y_isUb by auto |
1799 using X_in_S and Y_isUb by auto |
1880 ultimately obtain t where t_is_Lub: "isLub UNIV ?SHIFT t" |
1800 ultimately obtain t where t_is_Lub: "\<forall>y. (\<exists>x\<in>?SHIFT. y < x) = (y < t)" |
1881 using posreals_complete [of ?SHIFT] by blast |
1801 using posreal_complete [of ?SHIFT] unfolding bdd_above_def by blast |
1882 |
1802 |
1883 show ?thesis |
1803 show ?thesis |
1884 proof |
1804 proof |
1885 show "isLub UNIV S (t + X + (-1))" |
1805 show "(\<forall>s\<in>S. s \<le> (t + X + (-1))) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> (t + X + (-1)) \<le> y)" |
1886 proof (rule isLubI2) |
1806 proof safe |
1887 { |
1807 fix x |
1888 fix x |
1808 assume "\<forall>s\<in>S. s \<le> x" |
1889 assume "isUb (UNIV::real set) S x" |
1809 hence "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1" |
1890 hence "isUb (UNIV::real set) (?SHIFT) (x + (-X) + 1)" |
1810 using S_Ub_is_SHIFT_Ub by simp |
1891 using S_Ub_is_SHIFT_Ub by simp |
1811 then have "\<not> x + (-X) + 1 < t" |
1892 hence "t \<le> (x + (-X) + 1)" |
1812 by (subst t_is_Lub[rule_format, symmetric]) (simp add: not_less) |
1893 using t_is_Lub by (simp add: isLub_le_isUb) |
1813 thus "t + X + -1 \<le> x" by arith |
1894 hence "t + X + -1 \<le> x" by arith |
|
1895 } |
|
1896 then show "(t + X + -1) <=* Collect (isUb UNIV S)" |
|
1897 by (simp add: setgeI) |
|
1898 next |
1814 next |
1899 show "isUb UNIV S (t + X + -1)" |
1815 fix y |
1900 proof - |
1816 assume y_in_S: "y \<in> S" |
1901 { |
1817 obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty .. |
1902 fix y |
1818 hence "\<exists> x \<in> S. u = x + - X + 1" by simp |
1903 assume y_in_S: "y \<in> S" |
1819 then obtain "x" where x_and_u: "u = x + - X + 1" .. |
1904 have "y \<le> t + X + -1" |
1820 have u_le_t: "u \<le> t" |
1905 proof - |
1821 proof (rule dense_le) |
1906 obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty .. |
1822 fix x assume "x < u" then have "x < t" |
1907 hence "\<exists> x \<in> S. u = x + - X + 1" by simp |
1823 using u_in_shift t_is_Lub by auto |
1908 then obtain "x" where x_and_u: "u = x + - X + 1" .. |
1824 then show "x \<le> t" by simp |
1909 have u_le_t: "u \<le> t" using u_in_shift and t_is_Lub by (simp add: isLubD2) |
1825 qed |
1910 |
1826 |
1911 show ?thesis |
1827 show "y \<le> t + X + -1" |
1912 proof cases |
1828 proof cases |
1913 assume "y \<le> x" |
1829 assume "y \<le> x" |
1914 moreover have "x = u + X + - 1" using x_and_u by arith |
1830 moreover have "x = u + X + - 1" using x_and_u by arith |
1915 moreover have "u + X + - 1 \<le> t + X + -1" using u_le_t by arith |
1831 moreover have "u + X + - 1 \<le> t + X + -1" using u_le_t by arith |
1916 ultimately show "y \<le> t + X + -1" by arith |
1832 ultimately show "y \<le> t + X + -1" by arith |
1917 next |
1833 next |
1918 assume "~(y \<le> x)" |
1834 assume "~(y \<le> x)" |
1919 hence x_less_y: "x < y" by arith |
1835 hence x_less_y: "x < y" by arith |
1920 |
1836 |
1921 have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp |
1837 have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp |
1922 hence "0 < x + (-X) + 1" by simp |
1838 hence "0 < x + (-X) + 1" by simp |
1923 hence "0 < y + (-X) + 1" using x_less_y by arith |
1839 hence "0 < y + (-X) + 1" using x_less_y by arith |
1924 hence "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp |
1840 hence *: "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp |
1925 hence "y + (-X) + 1 \<le> t" using t_is_Lub by (simp add: isLubD2) |
1841 have "y + (-X) + 1 \<le> t" |
1926 thus ?thesis by simp |
1842 proof (rule dense_le) |
1927 qed |
1843 fix x assume "x < y + (-X) + 1" then have "x < t" |
1928 qed |
1844 using * t_is_Lub by auto |
1929 } |
1845 then show "x \<le> t" by simp |
1930 then show ?thesis by (simp add: isUb_def setle_def) |
1846 qed |
|
1847 thus ?thesis by simp |
1931 qed |
1848 qed |
1932 qed |
1849 qed |
1933 qed |
1850 qed |
1934 qed |
1851 qed |
1935 |
|
1936 text{*A version of the same theorem without all those predicates!*} |
|
1937 lemma reals_complete2: |
|
1938 fixes S :: "(real set)" |
|
1939 assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x" |
|
1940 shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & |
|
1941 (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))" |
|
1942 proof - |
|
1943 have "\<exists>x. isLub UNIV S x" |
|
1944 by (rule reals_complete) |
|
1945 (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def assms) |
|
1946 thus ?thesis |
|
1947 by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI) |
|
1948 qed |
|
1949 |
|
1950 |
1852 |
1951 subsection {* The Archimedean Property of the Reals *} |
1853 subsection {* The Archimedean Property of the Reals *} |
1952 |
1854 |
1953 theorem reals_Archimedean: |
1855 theorem reals_Archimedean: |
1954 fixes x :: real |
1856 fixes x :: real |
1967 by (rule of_nat_0_le_iff) |
1869 by (rule of_nat_0_le_iff) |
1968 ultimately have "x * of_nat (Suc n) \<le> (1 / of_nat (Suc n)) * of_nat (Suc n)" |
1870 ultimately have "x * of_nat (Suc n) \<le> (1 / of_nat (Suc n)) * of_nat (Suc n)" |
1969 by (rule mult_right_mono) |
1871 by (rule mult_right_mono) |
1970 thus "x * of_nat (Suc n) \<le> 1" by (simp del: of_nat_Suc) |
1872 thus "x * of_nat (Suc n) \<le> 1" by (simp del: of_nat_Suc) |
1971 qed |
1873 qed |
1972 hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= 1" |
1874 hence 2: "bdd_above {z. \<exists>n. z = x * (of_nat (Suc n))}" |
1973 by (simp add: setle_def del: of_nat_Suc, safe, rule spec) |
1875 by (auto intro!: bdd_aboveI[of _ 1]) |
1974 hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} 1" |
1876 have 1: "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto |
1975 by (simp add: isUbI) |
1877 obtain t where |
1976 hence "\<exists>Y. isUb (UNIV::real set) {z. \<exists>n. z = x* (of_nat (Suc n))} Y" .. |
1878 upper: "\<And>z. z \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> z \<le> t" and |
1977 moreover have "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto |
1879 least: "\<And>y. (\<And>a. a \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> a \<le> y) \<Longrightarrow> t \<le> y" |
1978 ultimately have "\<exists>t. isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t" |
1880 using reals_complete[OF 1 2] by auto |
1979 by (simp add: reals_complete) |
1881 |
1980 then obtain "t" where |
1882 |
1981 t_is_Lub: "isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t" .. |
1883 have "t \<le> t + - x" |
1982 |
1884 proof (rule least) |
1983 have "\<forall>n::nat. x * of_nat n \<le> t + - x" |
1885 fix a assume a: "a \<in> {z. \<exists>n. z = x * (of_nat (Suc n))}" |
1984 proof |
1886 have "\<forall>n::nat. x * of_nat n \<le> t + - x" |
1985 fix n |
1887 proof |
1986 from t_is_Lub have "x * of_nat (Suc n) \<le> t" |
1888 fix n |
1987 by (simp add: isLubD2) |
1889 have "x * of_nat (Suc n) \<le> t" |
1988 hence "x * (of_nat n) + x \<le> t" |
1890 by (simp add: upper) |
1989 by (simp add: distrib_left) |
1891 hence "x * (of_nat n) + x \<le> t" |
1990 thus "x * (of_nat n) \<le> t + - x" by arith |
1892 by (simp add: distrib_left) |
|
1893 thus "x * (of_nat n) \<le> t + - x" by arith |
|
1894 qed hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc) |
|
1895 with a show "a \<le> t + - x" |
|
1896 by auto |
1991 qed |
1897 qed |
1992 |
|
1993 hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc) |
|
1994 hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= (t + - x)" |
|
1995 by (auto simp add: setle_def) |
|
1996 hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} (t + (-x))" |
|
1997 by (simp add: isUbI) |
|
1998 hence "t \<le> t + - x" |
|
1999 using t_is_Lub by (simp add: isLub_le_isUb) |
|
2000 thus False using x_pos by arith |
1898 thus False using x_pos by arith |
2001 qed |
1899 qed |
2002 |
1900 |
2003 text {* |
1901 text {* |
2004 There must be other proofs, e.g. @{text Suc} of the largest |
1902 There must be other proofs, e.g. @{text Suc} of the largest |