author | paulson |
Wed, 15 Jul 1998 10:15:13 +0200 | |
changeset 5143 | b94cd208f073 |
parent 5078 | 7b5ea59c0275 |
child 5521 | 7970832271cc |
permissions | -rw-r--r-- |
5078 | 1 |
(* Title : RComplete.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
Description : Completeness theorems for positive |
|
5 |
reals and reals |
|
6 |
*) |
|
7 |
||
8 |
||
9 |
open RComplete; |
|
10 |
||
11 |
Goal "!!(x::real). [| isLub R S x; isLub R S y |] ==> x = y"; |
|
12 |
by (forward_tac [isLub_isUb] 1); |
|
13 |
by (forw_inst_tac [("x","y")] isLub_isUb 1); |
|
14 |
by (blast_tac (claset() addSIs [real_le_anti_sym] |
|
15 |
addSDs [isLub_le_isUb]) 1); |
|
16 |
qed "real_isLub_unique"; |
|
17 |
||
18 |
Goalw [setle_def,setge_def] |
|
19 |
"!!x::real. [| x <=* S'; S <= S' |] ==> x <=* S"; |
|
20 |
by (Blast_tac 1); |
|
21 |
qed "real_order_restrict"; |
|
22 |
||
23 |
(*---------------------------------------------------------------- |
|
24 |
Completeness theorem for the positive reals(again) |
|
25 |
----------------------------------------------------------------*) |
|
26 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
27 |
Goal "[| ALL x: S. 0r < x; \ |
5078 | 28 |
\ EX x. x: S; \ |
29 |
\ EX u. isUb (UNIV::real set) S u \ |
|
30 |
\ |] ==> EX t. isLub (UNIV::real set) S t"; |
|
31 |
by (res_inst_tac [("x","%#psup({w. %#w : S})")] exI 1); |
|
32 |
by (auto_tac (claset(),simpset() addsimps [isLub_def,leastP_def,isUb_def])); |
|
33 |
by (auto_tac (claset() addSIs [setleI,setgeI] |
|
34 |
addSDs [real_gt_zero_preal_Ex RS iffD1],simpset())); |
|
35 |
by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1); |
|
36 |
by (dtac (real_gt_zero_preal_Ex RS iffD1) 1); |
|
37 |
by (auto_tac (claset(),simpset() addsimps [real_preal_le_iff])); |
|
38 |
by (rtac preal_psup_leI2a 1); |
|
39 |
by (forw_inst_tac [("y","%#ya")] setleD 1 THEN assume_tac 1); |
|
40 |
by (forward_tac [real_ge_preal_preal_Ex] 1); |
|
41 |
by (Step_tac 1); |
|
42 |
by (res_inst_tac [("x","y")] exI 1); |
|
43 |
by (blast_tac (claset() addSDs [setleD] addIs [real_preal_le_iff RS iffD1]) 1); |
|
44 |
by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1); |
|
45 |
by (forward_tac [isUbD2] 1); |
|
46 |
by (dtac (real_gt_zero_preal_Ex RS iffD1) 1); |
|
47 |
by (auto_tac (claset() addSDs [isUbD, |
|
48 |
real_ge_preal_preal_Ex],simpset() addsimps [real_preal_le_iff])); |
|
49 |
by (blast_tac (claset() addSDs [setleD] addSIs |
|
50 |
[psup_le_ub1] addIs [real_preal_le_iff RS iffD1]) 1); |
|
51 |
qed "posreals_complete"; |
|
52 |
||
53 |
||
54 |
(*------------------------------- |
|
55 |
Lemmas |
|
56 |
-------------------------------*) |
|
57 |
Goal "! y : {z. ? x: P. z = x + %~xa + 1r} Int {x. 0r < x}. 0r < y"; |
|
58 |
by Auto_tac; |
|
59 |
qed "real_sup_lemma3"; |
|
60 |
||
61 |
(* lemmas re-arranging the terms *) |
|
62 |
Goal "(S <= Y + %~X + Z) = (S + X + %~Z <= Y)"; |
|
63 |
by (Step_tac 1); |
|
64 |
by (dres_inst_tac [("x","%~Z")] real_add_le_mono1 1); |
|
65 |
by (dres_inst_tac [("x","Z")] real_add_le_mono1 2); |
|
66 |
by (auto_tac (claset(),simpset() addsimps [real_add_assoc, |
|
67 |
real_add_minus,real_add_zero_right,real_add_minus_left])); |
|
68 |
by (dres_inst_tac [("x","X")] real_add_le_mono1 1); |
|
69 |
by (dres_inst_tac [("x","%~X")] real_add_le_mono1 2); |
|
70 |
by (auto_tac (claset(),simpset() addsimps [real_add_assoc, |
|
71 |
real_add_minus,real_add_zero_right,real_add_minus_left])); |
|
72 |
by (auto_tac (claset(),simpset() addsimps [real_add_commute])); |
|
73 |
qed "lemma_le_swap"; |
|
74 |
||
75 |
Goal "(xa <= S + X + %~Z) = (xa + %~X + Z <= S)"; |
|
76 |
by (Step_tac 1); |
|
77 |
by (dres_inst_tac [("x","Z")] real_add_le_mono1 1); |
|
78 |
by (dres_inst_tac [("x","%~Z")] real_add_le_mono1 2); |
|
79 |
by (auto_tac (claset(),simpset() addsimps [real_add_assoc, |
|
80 |
real_add_minus,real_add_zero_right,real_add_minus_left])); |
|
81 |
by (dres_inst_tac [("x","%~X")] real_add_le_mono1 1); |
|
82 |
by (dres_inst_tac [("x","X")] real_add_le_mono1 2); |
|
83 |
by (auto_tac (claset(),simpset() addsimps [real_add_assoc, |
|
84 |
real_add_minus,real_add_zero_right,real_add_minus_left])); |
|
85 |
by (auto_tac (claset(),simpset() addsimps [real_add_commute])); |
|
86 |
qed "lemma_le_swap2"; |
|
87 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
88 |
Goal "[| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r"; |
5078 | 89 |
by (dtac real_add_less_mono 1); |
90 |
by (assume_tac 1); |
|
91 |
by (dres_inst_tac [("C","%~x"),("A","0r + x")] real_add_less_mono2 1); |
|
92 |
by (asm_full_simp_tac (simpset() addsimps [real_add_zero_right, |
|
93 |
real_add_assoc RS sym,real_add_minus_left,real_add_zero_left]) 1); |
|
94 |
by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1); |
|
95 |
qed "lemma_real_complete1"; |
|
96 |
||
97 |
Goal "!!x. [| x + %~X + 1r <= S; xa < x |] ==> xa + %~X + 1r <= S"; |
|
98 |
by (dtac real_less_imp_le 1); |
|
99 |
by (dtac real_add_le_mono 1); |
|
100 |
by (assume_tac 1); |
|
101 |
by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1); |
|
102 |
by (dres_inst_tac [("x","%~x"),("q2.0","x + S")] real_add_left_le_mono1 1); |
|
103 |
by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym, |
|
104 |
real_add_minus_left,real_add_zero_left]) 1); |
|
105 |
qed "lemma_real_complete2"; |
|
106 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
107 |
Goal "[| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**) |
5078 | 108 |
by (rtac (lemma_le_swap2 RS iffD2) 1); |
109 |
by (etac lemma_real_complete2 1); |
|
110 |
by (assume_tac 1); |
|
111 |
qed "lemma_real_complete2a"; |
|
112 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
113 |
Goal "[| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r"; |
5078 | 114 |
by (rotate_tac 1 1); |
115 |
by (etac (real_le_imp_less_or_eq RS disjE) 1); |
|
116 |
by (blast_tac (claset() addIs [lemma_real_complete2a]) 1); |
|
117 |
by (blast_tac (claset() addIs [(lemma_le_swap2 RS iffD2)]) 1); |
|
118 |
qed "lemma_real_complete2b"; |
|
119 |
||
120 |
(*------------------------------------ |
|
121 |
reals Completeness (again!) |
|
122 |
------------------------------------*) |
|
123 |
Goal "!!(S::real set). [| EX X. X: S; \ |
|
124 |
\ EX Y. isUb (UNIV::real set) S Y \ |
|
125 |
\ |] ==> EX t. isLub (UNIV :: real set) S t"; |
|
126 |
by (Step_tac 1); |
|
127 |
by (subgoal_tac "? u. u: {z. ? x: S. z = x + %~X + 1r} \ |
|
128 |
\ Int {x. 0r < x}" 1); |
|
129 |
by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + %~X + 1r} \ |
|
130 |
\ Int {x. 0r < x}) (Y + %~X + 1r)" 1); |
|
131 |
by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1); |
|
132 |
by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, Step_tac]); |
|
133 |
by (res_inst_tac [("x","t + X + %~1r")] exI 1); |
|
134 |
by (rtac isLubI2 1); |
|
135 |
by (rtac setgeI 2 THEN Step_tac 2); |
|
136 |
by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + %~X + 1r} \ |
|
137 |
\ Int {x. 0r < x}) (y + %~X + 1r)" 2); |
|
138 |
by (dres_inst_tac [("y","(y + %~ X + 1r)")] isLub_le_isUb 2 |
|
139 |
THEN assume_tac 2); |
|
140 |
by (etac (lemma_le_swap RS subst) 2); |
|
141 |
by (rtac (setleI RS isUbI) 1); |
|
142 |
by (Step_tac 1); |
|
143 |
by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1); |
|
144 |
by (stac lemma_le_swap2 1); |
|
145 |
by (forward_tac [isLubD2] 1 THEN assume_tac 2); |
|
146 |
by (Step_tac 1); |
|
147 |
by (Blast_tac 1); |
|
148 |
by (dtac lemma_real_complete1 1 THEN REPEAT(assume_tac 1)); |
|
149 |
by (stac lemma_le_swap2 1); |
|
150 |
by (forward_tac [isLubD2] 1 THEN assume_tac 2); |
|
151 |
by (Blast_tac 1); |
|
152 |
by (rtac lemma_real_complete2b 1); |
|
153 |
by (etac real_less_imp_le 2); |
|
154 |
by (blast_tac (claset() addSIs [isLubD2]) 1 THEN Step_tac 1); |
|
155 |
by (blast_tac (claset() addDs [isUbD] addSIs [(setleI RS isUbI)] |
|
156 |
addIs [real_add_le_mono1,real_add_assoc RS ssubst]) 1); |
|
157 |
by (blast_tac (claset() addDs [isUbD] addSIs [(setleI RS isUbI)] |
|
158 |
addIs [real_add_le_mono1,real_add_assoc RS ssubst]) 1); |
|
159 |
by (auto_tac (claset(),simpset() addsimps [real_add_assoc RS sym, |
|
160 |
real_add_minus,real_add_zero_left,real_zero_less_one])); |
|
161 |
qed "reals_complete"; |
|
162 |
||
163 |
(*---------------------------------------------------------------- |
|
164 |
Related property: Archimedean property of reals |
|
165 |
----------------------------------------------------------------*) |
|
166 |
||
167 |
Goal "(ALL m. x*%%#m + x <= t) = (ALL m. x*%%#m <= t + %~x)"; |
|
168 |
by Auto_tac; |
|
169 |
by (ALLGOALS(dres_inst_tac [("x","m")] spec)); |
|
170 |
by (dres_inst_tac [("x","%~x")] real_add_le_mono1 1); |
|
171 |
by (dres_inst_tac [("x","x")] real_add_le_mono1 2); |
|
172 |
by (auto_tac (claset(),simpset() addsimps [real_add_assoc, |
|
173 |
real_add_minus,real_add_minus_left,real_add_zero_right])); |
|
174 |
qed "lemma_arch"; |
|
175 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
176 |
Goal "0r < x ==> EX n. rinv(%%#n) < x"; |
5078 | 177 |
by (stac real_nat_rinv_Ex_iff 1); |
178 |
by (EVERY1[rtac ccontr, Asm_full_simp_tac]); |
|
179 |
by (fold_tac [real_le_def]); |
|
180 |
by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} 1r" 1); |
|
181 |
by (subgoal_tac "EX X. X : {z. EX n. z = x*%%#n}" 1); |
|
182 |
by (dtac reals_complete 1); |
|
183 |
by (auto_tac (claset() addIs [isUbI,setleI],simpset())); |
|
184 |
by (subgoal_tac "ALL m. x*(%%#Suc m) <= t" 1); |
|
185 |
by (asm_full_simp_tac (simpset() addsimps |
|
186 |
[real_nat_Suc,real_add_mult_distrib2]) 1); |
|
187 |
by (blast_tac (claset() addIs [isLubD2]) 2); |
|
188 |
by (asm_full_simp_tac (simpset() addsimps [lemma_arch]) 1); |
|
189 |
by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} (t + %~x)" 1); |
|
190 |
by (blast_tac (claset() addSIs [isUbI,setleI]) 2); |
|
191 |
by (dres_inst_tac [("y","t+%~x")] isLub_le_isUb 1); |
|
192 |
by (dres_inst_tac [("x","%~t")] real_add_left_le_mono1 2); |
|
193 |
by (auto_tac (claset() addDs [real_le_less_trans, |
|
194 |
(real_minus_zero_less_iff2 RS iffD2)], simpset() |
|
195 |
addsimps [real_less_not_refl,real_add_assoc RS sym, |
|
196 |
real_add_minus_left,real_add_zero_left])); |
|
197 |
qed "reals_Archimedean"; |
|
198 |
||
199 |
Goal "EX n. (x::real) < %%#n"; |
|
200 |
by (res_inst_tac [("R1.0","x"),("R2.0","0r")] real_linear_less2 1); |
|
201 |
by (res_inst_tac [("x","0")] exI 1); |
|
202 |
by (res_inst_tac [("x","0")] exI 2); |
|
203 |
by (auto_tac (claset() addEs [real_less_trans], |
|
204 |
simpset() addsimps [real_nat_one,real_zero_less_one])); |
|
205 |
by (forward_tac [(real_rinv_gt_zero RS reals_Archimedean)] 1); |
|
206 |
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1); |
|
207 |
by (forw_inst_tac [("y","rinv x")] real_mult_less_mono1 1); |
|
208 |
by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym])); |
|
209 |
by (dres_inst_tac [("n1","n"),("y","1r")] |
|
210 |
(real_nat_less_zero RS real_mult_less_mono2) 1); |
|
211 |
by (auto_tac (claset(),simpset() addsimps [real_nat_less_zero, |
|
212 |
real_not_refl2 RS not_sym,real_mult_assoc RS sym])); |
|
213 |
qed "reals_Archimedean2"; |
|
214 |
||
215 |
||
216 |
||
217 |
||
218 |