19 by auto |
19 by auto |
20 |
20 |
21 subsection {* Completeness of Positive Reals *} |
21 subsection {* Completeness of Positive Reals *} |
22 |
22 |
23 text {* |
23 text {* |
24 Supremum property for the set of positive reals |
|
25 |
|
26 Let @{text "P"} be a non-empty set of positive reals, with an upper |
|
27 bound @{text "y"}. Then @{text "P"} has a least upper bound |
|
28 (written @{text "S"}). |
|
29 |
|
30 FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}? |
|
31 *} |
|
32 |
|
33 text {* Only used in HOL/Import/HOL4Compat.thy; delete? *} |
|
34 |
|
35 lemma posreal_complete: |
|
36 fixes P :: "real set" |
|
37 assumes not_empty_P: "\<exists>x. x \<in> P" |
|
38 and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y" |
|
39 shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)" |
|
40 proof - |
|
41 from upper_bound_Ex have "\<exists>z. \<forall>x\<in>P. x \<le> z" |
|
42 by (auto intro: less_imp_le) |
|
43 from complete_real [OF not_empty_P this] obtain S |
|
44 where S1: "\<And>x. x \<in> P \<Longrightarrow> x \<le> S" and S2: "\<And>z. \<forall>x\<in>P. x \<le> z \<Longrightarrow> S \<le> z" by fast |
|
45 have "\<forall>y. (\<exists>x \<in> P. y < x) = (y < S)" |
|
46 proof |
|
47 fix y show "(\<exists>x\<in>P. y < x) = (y < S)" |
|
48 apply (cases "\<exists>x\<in>P. y < x", simp_all) |
|
49 apply (clarify, drule S1, simp) |
|
50 apply (simp add: not_less S2) |
|
51 done |
|
52 qed |
|
53 thus ?thesis .. |
|
54 qed |
|
55 |
|
56 text {* |
|
57 \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc. |
24 \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc. |
58 *} |
25 *} |
59 |
26 |
60 lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)" |
27 lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)" |
61 apply (frule isLub_isUb) |
28 apply (frule isLub_isUb) |
66 |
33 |
67 text {* |
34 text {* |
68 \medskip reals Completeness (again!) |
35 \medskip reals Completeness (again!) |
69 *} |
36 *} |
70 |
37 |
71 lemma reals_complete: |
38 lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t" |
72 assumes notempty_S: "\<exists>X. X \<in> S" |
39 by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro: cSup_upper) |
73 and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y" |
|
74 shows "\<exists>t. isLub (UNIV :: real set) S t" |
|
75 proof - |
|
76 from assms have "\<exists>X. X \<in> S" and "\<exists>Y. \<forall>x\<in>S. x \<le> Y" |
|
77 unfolding isUb_def setle_def by simp_all |
|
78 from complete_real [OF this] show ?thesis |
|
79 by (simp add: isLub_def leastP_def isUb_def setle_def setge_def) |
|
80 qed |
|
81 |
40 |
82 |
41 |
83 subsection {* The Archimedean Property of the Reals *} |
42 subsection {* The Archimedean Property of the Reals *} |
84 |
43 |
85 theorem reals_Archimedean: |
44 theorem reals_Archimedean: |