12 Completeness of reals: use supremum property of |
12 Completeness of reals: use supremum property of |
13 preal and theorems about real_preal. Theorems |
13 preal and theorems about real_preal. Theorems |
14 previously in Real.ML. |
14 previously in Real.ML. |
15 ---------------------------------------------------------*) |
15 ---------------------------------------------------------*) |
16 (*a few lemmas*) |
16 (*a few lemmas*) |
17 Goal "! x:P. 0r < x ==> \ |
17 Goal "! x:P. #0 < x ==> \ |
18 \ ((? x:P. y < x) = (? X. real_of_preal X : P & \ |
18 \ ((? x:P. y < x) = (? X. real_of_preal X : P & \ |
19 \ y < real_of_preal X))"; |
19 \ y < real_of_preal X))"; |
20 by (blast_tac (claset() addSDs [bspec, |
20 by (blast_tac (claset() addSDs [bspec,rename_numerals thy |
21 real_gt_zero_preal_Ex RS iffD1]) 1); |
21 real_gt_zero_preal_Ex RS iffD1]) 1); |
22 qed "real_sup_lemma1"; |
22 qed "real_sup_lemma1"; |
23 |
23 |
24 Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \ |
24 Goal "[| ! x:P. #0 < x; ? x. x: P; ? y. !x: P. x < y |] \ |
25 \ ==> (? X. X: {w. real_of_preal w : P}) & \ |
25 \ ==> (? X. X: {w. real_of_preal w : P}) & \ |
26 \ (? Y. !X: {w. real_of_preal w : P}. X < Y)"; |
26 \ (? Y. !X: {w. real_of_preal w : P}. X < Y)"; |
27 by (rtac conjI 1); |
27 by (rtac conjI 1); |
28 by (blast_tac (claset() addDs [bspec, real_gt_zero_preal_Ex RS iffD1]) 1); |
28 by (blast_tac (claset() addDs [bspec, rename_numerals thy |
|
29 real_gt_zero_preal_Ex RS iffD1]) 1); |
29 by Auto_tac; |
30 by Auto_tac; |
30 by (dtac bspec 1 THEN assume_tac 1); |
31 by (dtac bspec 1 THEN assume_tac 1); |
31 by (ftac bspec 1 THEN assume_tac 1); |
32 by (ftac bspec 1 THEN assume_tac 1); |
32 by (dtac real_less_trans 1 THEN assume_tac 1); |
33 by (dtac real_less_trans 1 THEN assume_tac 1); |
33 by (dtac (real_gt_zero_preal_Ex RS iffD1) 1 THEN etac exE 1); |
34 by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1 |
|
35 THEN etac exE 1); |
34 by (res_inst_tac [("x","ya")] exI 1); |
36 by (res_inst_tac [("x","ya")] exI 1); |
35 by Auto_tac; |
37 by Auto_tac; |
36 by (dres_inst_tac [("x","real_of_preal X")] bspec 1 THEN assume_tac 1); |
38 by (dres_inst_tac [("x","real_of_preal X")] bspec 1 THEN assume_tac 1); |
37 by (etac real_of_preal_lessD 1); |
39 by (etac real_of_preal_lessD 1); |
38 qed "real_sup_lemma2"; |
40 qed "real_sup_lemma2"; |
39 |
41 |
40 (*------------------------------------------------------------- |
42 (*------------------------------------------------------------- |
41 Completeness of Positive Reals |
43 Completeness of Positive Reals |
42 -------------------------------------------------------------*) |
44 -------------------------------------------------------------*) |
43 |
45 |
44 (* Supremum property for the set of positive reals *) |
46 (** |
45 (* FIXME: long proof - can be improved - need only have |
47 Supremum property for the set of positive reals |
46 one case split *) (* will do for now *) |
48 FIXME: long proof - should be improved - need |
47 Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \ |
49 only have one case split |
|
50 **) |
|
51 |
|
52 Goal "[| ! x:P. (#0::real) < x; ? x. x: P; ? y. !x: P. x < y |] \ |
48 \ ==> (? S. !y. (? x: P. y < x) = (y < S))"; |
53 \ ==> (? S. !y. (? x: P. y < x) = (y < S))"; |
49 by (res_inst_tac |
54 by (res_inst_tac |
50 [("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1); |
55 [("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1); |
51 by Auto_tac; |
56 by Auto_tac; |
52 by (ftac real_sup_lemma2 1 THEN Auto_tac); |
57 by (ftac real_sup_lemma2 1 THEN Auto_tac); |
53 by (case_tac "0r < ya" 1); |
58 by (case_tac "#0 < ya" 1); |
54 by (dtac (real_gt_zero_preal_Ex RS iffD1) 1); |
59 by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); |
55 by (dtac real_less_all_real2 2); |
60 by (dtac (full_rename_numerals thy real_less_all_real2) 2); |
56 by Auto_tac; |
61 by Auto_tac; |
57 by (rtac (preal_complete RS spec RS iffD1) 1); |
62 by (rtac (preal_complete RS spec RS iffD1) 1); |
58 by Auto_tac; |
63 by Auto_tac; |
59 by (ftac real_gt_preal_preal_Ex 1); |
64 by (ftac real_gt_preal_preal_Ex 1); |
60 by Auto_tac; |
65 by Auto_tac; |
61 (* second part *) |
66 (* second part *) |
62 by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1); |
67 by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1); |
63 by (case_tac "0r < ya" 1); |
68 by (case_tac "#0 < ya" 1); |
64 by (auto_tac (claset() addSDs [real_less_all_real2, |
69 by (auto_tac (claset() addSDs (map (full_rename_numerals |
65 real_gt_zero_preal_Ex RS iffD1],simpset())); |
70 thy) [real_less_all_real2,real_gt_zero_preal_Ex RS iffD1]), |
|
71 simpset())); |
66 by (ftac real_sup_lemma2 2 THEN Auto_tac); |
72 by (ftac real_sup_lemma2 2 THEN Auto_tac); |
67 by (ftac real_sup_lemma2 1 THEN Auto_tac); |
73 by (ftac real_sup_lemma2 1 THEN Auto_tac); |
68 by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1); |
74 by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1); |
69 by (Blast_tac 3); |
75 by (Blast_tac 3); |
70 by (Blast_tac 1); |
76 by (ALLGOALS(Blast_tac)); |
71 by (Blast_tac 1); |
|
72 by (Blast_tac 1); |
|
73 qed "posreal_complete"; |
77 qed "posreal_complete"; |
74 |
78 |
75 (*-------------------------------------------------------- |
79 (*-------------------------------------------------------- |
76 Completeness properties using isUb, isLub etc. |
80 Completeness properties using isUb, isLub etc. |
77 -------------------------------------------------------*) |
81 -------------------------------------------------------*) |
89 |
93 |
90 (*---------------------------------------------------------------- |
94 (*---------------------------------------------------------------- |
91 Completeness theorem for the positive reals(again) |
95 Completeness theorem for the positive reals(again) |
92 ----------------------------------------------------------------*) |
96 ----------------------------------------------------------------*) |
93 |
97 |
94 Goal "[| ALL x: S. 0r < x; \ |
98 Goal "[| ALL x: S. #0 < x; \ |
95 \ EX x. x: S; \ |
99 \ EX x. x: S; \ |
96 \ EX u. isUb (UNIV::real set) S u \ |
100 \ EX u. isUb (UNIV::real set) S u \ |
97 \ |] ==> EX t. isLub (UNIV::real set) S t"; |
101 \ |] ==> EX t. isLub (UNIV::real set) S t"; |
98 by (res_inst_tac [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1); |
102 by (res_inst_tac |
99 by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def])); |
103 [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1); |
|
104 by (auto_tac (claset(), simpset() addsimps |
|
105 [isLub_def,leastP_def,isUb_def])); |
100 by (auto_tac (claset() addSIs [setleI,setgeI] |
106 by (auto_tac (claset() addSIs [setleI,setgeI] |
101 addSDs [real_gt_zero_preal_Ex RS iffD1], |
107 addSDs [(rename_numerals thy real_gt_zero_preal_Ex) |
102 simpset())); |
108 RS iffD1],simpset())); |
103 by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1); |
109 by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1); |
104 by (dtac (real_gt_zero_preal_Ex RS iffD1) 1); |
110 by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); |
105 by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff])); |
111 by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff])); |
106 by (rtac preal_psup_leI2a 1); |
112 by (rtac preal_psup_leI2a 1); |
107 by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1); |
113 by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1); |
108 by (ftac real_ge_preal_preal_Ex 1); |
114 by (ftac real_ge_preal_preal_Ex 1); |
109 by (Step_tac 1); |
115 by (Step_tac 1); |
110 by (res_inst_tac [("x","y")] exI 1); |
116 by (res_inst_tac [("x","y")] exI 1); |
111 by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1); |
117 by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1); |
112 by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1); |
118 by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1); |
113 by (ftac isUbD2 1); |
119 by (ftac isUbD2 1); |
114 by (dtac (real_gt_zero_preal_Ex RS iffD1) 1); |
120 by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); |
115 by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex], |
121 by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex], |
116 simpset() addsimps [real_of_preal_le_iff])); |
122 simpset() addsimps [real_of_preal_le_iff])); |
117 by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] |
123 by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] |
118 addIs [real_of_preal_le_iff RS iffD1]) 1); |
124 addIs [real_of_preal_le_iff RS iffD1]) 1); |
119 qed "posreals_complete"; |
125 qed "posreals_complete"; |
120 |
126 |
121 |
127 |
122 (*------------------------------- |
128 (*------------------------------- |
123 Lemmas |
129 Lemmas |
124 -------------------------------*) |
130 -------------------------------*) |
125 Goal "! y : {z. ? x: P. z = x + (-xa) + 1r} Int {x. 0r < x}. 0r < y"; |
131 Goal "! y : {z. ? x: P. z = x + (-xa) + #1} Int {x. #0 < x}. #0 < y"; |
126 by Auto_tac; |
132 by Auto_tac; |
127 qed "real_sup_lemma3"; |
133 qed "real_sup_lemma3"; |
128 |
134 |
129 Goal "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))"; |
135 Goal "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))"; |
130 by (simp_tac (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ |
136 by (Auto_tac); |
131 real_add_ac) 1); |
|
132 qed "lemma_le_swap2"; |
137 qed "lemma_le_swap2"; |
133 |
138 |
134 Goal "[| 0r < x + (-X) + 1r; x < xa |] ==> 0r < xa + (-X) + 1r"; |
139 Goal "[| #0 < (x::real) + (-X) + #1; x < xa |] ==> #0 < xa + (-X) + #1"; |
135 by (dtac real_add_less_mono 1); |
140 by (Auto_tac); |
136 by (assume_tac 1); |
|
137 by (dres_inst_tac [("C","-x"),("A","0r + x")] real_add_less_mono2 1); |
|
138 by (asm_full_simp_tac |
|
139 (simpset() addsimps [real_add_zero_right, real_add_assoc RS sym, |
|
140 real_add_minus_left,real_add_zero_left]) 1); |
|
141 qed "lemma_real_complete1"; |
141 qed "lemma_real_complete1"; |
142 |
142 |
143 Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa + (-X) + 1r <= S"; |
143 Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa + (-X) + #1 <= S"; |
144 by (dtac real_less_imp_le 1); |
144 by (Auto_tac); |
145 by (dtac real_add_le_mono 1); |
|
146 by (assume_tac 1); |
|
147 by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1); |
|
148 qed "lemma_real_complete2"; |
145 qed "lemma_real_complete2"; |
149 |
146 |
150 Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa <= S + X + (-1r)"; (**) |
147 Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa <= S + X + (-#1)"; (**) |
151 by (rtac (lemma_le_swap2 RS iffD2) 1); |
148 by (Auto_tac); |
152 by (etac lemma_real_complete2 1); |
|
153 by (assume_tac 1); |
|
154 qed "lemma_real_complete2a"; |
149 qed "lemma_real_complete2a"; |
155 |
150 |
156 Goal "[| x + (-X) + 1r <= S; xa <= x |] ==> xa <= S + X + (-1r)"; |
151 Goal "[| (x::real) + (-X) + #1 <= S; xa <= x |] ==> xa <= S + X + (-#1)"; |
157 by (rotate_tac 1 1); |
152 by (Auto_tac); |
158 by (etac (real_le_imp_less_or_eq RS disjE) 1); |
|
159 by (blast_tac (claset() addIs [lemma_real_complete2a]) 1); |
|
160 by (blast_tac (claset() addIs [(lemma_le_swap2 RS iffD2)]) 1); |
|
161 qed "lemma_real_complete2b"; |
153 qed "lemma_real_complete2b"; |
162 |
154 |
163 (*------------------------------------ |
155 (*---------------------------------------------------------- |
164 reals Completeness (again!) |
156 reals Completeness (again!) |
165 ------------------------------------*) |
157 ----------------------------------------------------------*) |
166 Goal "[| EX X. X: S; EX Y. isUb (UNIV::real set) S Y |] \ |
158 Goal "[| EX X. X: S; EX Y. isUb (UNIV::real set) S Y |] \ |
167 \ ==> EX t. isLub (UNIV :: real set) S t"; |
159 \ ==> EX t. isLub (UNIV :: real set) S t"; |
168 by (Step_tac 1); |
160 by (Step_tac 1); |
169 by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + 1r} \ |
161 by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + #1} \ |
170 \ Int {x. 0r < x}" 1); |
162 \ Int {x. #0 < x}" 1); |
171 by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + 1r} \ |
163 by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + #1} \ |
172 \ Int {x. 0r < x}) (Y + (-X) + 1r)" 1); |
164 \ Int {x. #0 < x}) (Y + (-X) + #1)" 1); |
173 by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1); |
165 by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1); |
174 by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, |
166 by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, |
175 Step_tac]); |
167 Step_tac]); |
176 by (res_inst_tac [("x","t + X + (-1r)")] exI 1); |
168 by (res_inst_tac [("x","t + X + (-#1)")] exI 1); |
177 by (rtac isLubI2 1); |
169 by (rtac isLubI2 1); |
178 by (rtac setgeI 2 THEN Step_tac 2); |
170 by (rtac setgeI 2 THEN Step_tac 2); |
179 by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + 1r} \ |
171 by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + #1} \ |
180 \ Int {x. 0r < x}) (y + (-X) + 1r)" 2); |
172 \ Int {x. #0 < x}) (y + (-X) + #1)" 2); |
181 by (dres_inst_tac [("y","(y + (- X) + 1r)")] isLub_le_isUb 2 |
173 by (dres_inst_tac [("y","(y + (- X) + #1)")] isLub_le_isUb 2 |
182 THEN assume_tac 2); |
174 THEN assume_tac 2); |
183 by (full_simp_tac |
175 by (full_simp_tac |
184 (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ |
176 (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ |
185 real_add_ac) 2); |
177 real_add_ac) 2); |
186 by (rtac (setleI RS isUbI) 1); |
178 by (rtac (setleI RS isUbI) 1); |
200 by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
192 by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
201 by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] |
193 by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] |
202 addIs [real_add_le_mono1]) 1); |
194 addIs [real_add_le_mono1]) 1); |
203 by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] |
195 by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] |
204 addIs [real_add_le_mono1]) 1); |
196 addIs [real_add_le_mono1]) 1); |
205 by (auto_tac (claset(), |
197 by (Auto_tac); |
206 simpset() addsimps [real_add_assoc RS sym, |
|
207 real_zero_less_one])); |
|
208 qed "reals_complete"; |
198 qed "reals_complete"; |
209 |
199 |
210 (*---------------------------------------------------------------- |
200 (*---------------------------------------------------------------- |
211 Related: Archimedean property of reals |
201 Related: Archimedean property of reals |
212 ----------------------------------------------------------------*) |
202 ----------------------------------------------------------------*) |
213 |
203 |
214 Goal "0r < x ==> EX n. rinv(real_of_posnat n) < x"; |
204 Goal "#0 < x ==> EX n. rinv(real_of_posnat n) < x"; |
215 by (stac real_of_posnat_rinv_Ex_iff 1); |
205 by (stac real_of_posnat_rinv_Ex_iff 1); |
216 by (EVERY1[rtac ccontr, Asm_full_simp_tac]); |
206 by (EVERY1[rtac ccontr, Asm_full_simp_tac]); |
217 by (fold_tac [real_le_def]); |
207 by (fold_tac [real_le_def]); |
218 by (subgoal_tac "isUb (UNIV::real set) \ |
208 by (subgoal_tac "isUb (UNIV::real set) \ |
219 \ {z. EX n. z = x*(real_of_posnat n)} 1r" 1); |
209 \ {z. EX n. z = x*(real_of_posnat n)} #1" 1); |
220 by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1); |
210 by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1); |
221 by (dtac reals_complete 1); |
211 by (dtac reals_complete 1); |
222 by (auto_tac (claset() addIs [isUbI,setleI],simpset())); |
212 by (auto_tac (claset() addIs [isUbI,setleI],simpset())); |
223 by (subgoal_tac "ALL m. x*(real_of_posnat(Suc m)) <= t" 1); |
213 by (subgoal_tac "ALL m. x*(real_of_posnat(Suc m)) <= t" 1); |
224 by (asm_full_simp_tac (simpset() addsimps |
214 by (asm_full_simp_tac (simpset() addsimps |
235 (real_minus_zero_less_iff2 RS iffD2)], |
225 (real_minus_zero_less_iff2 RS iffD2)], |
236 simpset() addsimps [real_less_not_refl,real_add_assoc RS sym])); |
226 simpset() addsimps [real_less_not_refl,real_add_assoc RS sym])); |
237 qed "reals_Archimedean"; |
227 qed "reals_Archimedean"; |
238 |
228 |
239 Goal "EX n. (x::real) < real_of_posnat n"; |
229 Goal "EX n. (x::real) < real_of_posnat n"; |
240 by (res_inst_tac [("R1.0","x"),("R2.0","0r")] real_linear_less2 1); |
230 by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1); |
241 by (res_inst_tac [("x","0")] exI 1); |
231 by (res_inst_tac [("x","0")] exI 1); |
242 by (res_inst_tac [("x","0")] exI 2); |
232 by (res_inst_tac [("x","0")] exI 2); |
243 by (auto_tac (claset() addEs [real_less_trans], |
233 by (auto_tac (claset() addEs [real_less_trans], |
244 simpset() addsimps [real_of_posnat_one,real_zero_less_one])); |
234 simpset() addsimps [real_of_posnat_one,real_zero_less_one])); |
245 by (forward_tac [(real_rinv_gt_zero RS reals_Archimedean)] 1); |
235 by (forward_tac [((full_rename_numerals thy real_rinv_gt_zero) |
|
236 RS reals_Archimedean)] 1); |
246 by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1); |
237 by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1); |
247 by (forw_inst_tac [("y","rinv x")] real_mult_less_mono1 1); |
238 by (forw_inst_tac [("y","rinv x")] |
|
239 (full_rename_numerals thy real_mult_less_mono1) 1); |
248 by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym])); |
240 by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym])); |
249 by (dres_inst_tac [("n1","n"),("y","1r")] |
241 by (dres_inst_tac [("n1","n"),("y","#1")] |
250 (real_of_posnat_less_zero RS real_mult_less_mono2) 1); |
242 (real_of_posnat_less_zero RS real_mult_less_mono2) 1); |
251 by (auto_tac (claset(), |
243 by (auto_tac (claset(), |
252 simpset() addsimps [real_of_posnat_less_zero, |
244 simpset() addsimps [rename_numerals thy |
|
245 real_of_posnat_less_zero, |
253 real_not_refl2 RS not_sym, |
246 real_not_refl2 RS not_sym, |
254 real_mult_assoc RS sym])); |
247 real_mult_assoc RS sym])); |
255 qed "reals_Archimedean2"; |
248 qed "reals_Archimedean2"; |
256 |
249 |
257 |
250 |