5078
|
1 |
(* Title : PReal.ML
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 1998 University of Cambridge
|
|
4 |
Description : The positive reals as Dedekind sections of positive
|
|
5 |
rationals. Fundamentals of Abstract Analysis
|
|
6 |
[Gleason- p. 121] provides some of the definitions.
|
|
7 |
*)
|
|
8 |
|
|
9 |
open PReal;
|
|
10 |
|
|
11 |
Goal "inj_on Abs_preal preal";
|
|
12 |
by (rtac inj_on_inverseI 1);
|
|
13 |
by (etac Abs_preal_inverse 1);
|
|
14 |
qed "inj_on_Abs_preal";
|
|
15 |
|
|
16 |
Addsimps [inj_on_Abs_preal RS inj_on_iff];
|
|
17 |
|
|
18 |
Goal "inj(Rep_preal)";
|
|
19 |
by (rtac inj_inverseI 1);
|
|
20 |
by (rtac Rep_preal_inverse 1);
|
|
21 |
qed "inj_Rep_preal";
|
|
22 |
|
|
23 |
Goalw [preal_def] "{} ~: preal";
|
|
24 |
by (Fast_tac 1);
|
|
25 |
qed "empty_not_mem_preal";
|
|
26 |
|
|
27 |
(* {} : preal ==> P *)
|
|
28 |
bind_thm ("empty_not_mem_prealE", empty_not_mem_preal RS notE);
|
|
29 |
|
|
30 |
Addsimps [empty_not_mem_preal];
|
|
31 |
|
|
32 |
Goalw [preal_def] "{x::prat. x < $#Abs_pnat 1} : preal";
|
|
33 |
by (rtac preal_1 1);
|
|
34 |
qed "one_set_mem_preal";
|
|
35 |
|
|
36 |
Addsimps [one_set_mem_preal];
|
|
37 |
|
|
38 |
Goalw [preal_def] "!!x. x : preal ==> {} < x";
|
|
39 |
by (Fast_tac 1);
|
|
40 |
qed "preal_psubset_empty";
|
|
41 |
|
|
42 |
Goal "{} < Rep_preal x";
|
|
43 |
by (rtac (Rep_preal RS preal_psubset_empty) 1);
|
|
44 |
qed "Rep_preal_psubset_empty";
|
|
45 |
|
|
46 |
Goal "? x. x: Rep_preal X";
|
|
47 |
by (cut_inst_tac [("x","X")] Rep_preal_psubset_empty 1);
|
|
48 |
by (auto_tac (claset() addIs [(equals0I RS sym)],
|
|
49 |
simpset() addsimps [psubset_def]));
|
|
50 |
qed "mem_Rep_preal_Ex";
|
|
51 |
|
|
52 |
Goalw [preal_def]
|
|
53 |
"!!A. [| {} < A; A < {q::prat. True}; \
|
|
54 |
\ (!y: A. ((!z. z < y --> z: A) & \
|
|
55 |
\ (? u: A. y < u))) |] ==> A : preal";
|
|
56 |
by (Fast_tac 1);
|
|
57 |
qed "prealI1";
|
|
58 |
|
|
59 |
Goalw [preal_def]
|
|
60 |
"!!A. [| {} < A; A < {q::prat. True}; \
|
|
61 |
\ !y: A. (!z. z < y --> z: A); \
|
|
62 |
\ !y: A. (? u: A. y < u) |] ==> A : preal";
|
|
63 |
by (Best_tac 1);
|
|
64 |
qed "prealI2";
|
|
65 |
|
|
66 |
Goalw [preal_def]
|
|
67 |
"!!A. A : preal ==> {} < A & A < {q::prat. True} & \
|
|
68 |
\ (!y: A. ((!z. z < y --> z: A) & \
|
|
69 |
\ (? u: A. y < u)))";
|
|
70 |
by (Fast_tac 1);
|
|
71 |
qed "prealE_lemma";
|
|
72 |
|
|
73 |
|
|
74 |
AddSIs [prealI1,prealI2];
|
|
75 |
|
|
76 |
Addsimps [Abs_preal_inverse];
|
|
77 |
|
|
78 |
|
|
79 |
Goalw [preal_def]
|
|
80 |
"!!A. A : preal ==> {} < A";
|
|
81 |
by (Fast_tac 1);
|
|
82 |
qed "prealE_lemma1";
|
|
83 |
|
|
84 |
Goalw [preal_def]
|
|
85 |
"!!A. A : preal ==> A < {q::prat. True}";
|
|
86 |
by (Fast_tac 1);
|
|
87 |
qed "prealE_lemma2";
|
|
88 |
|
|
89 |
Goalw [preal_def]
|
|
90 |
"!!A. A : preal ==> !y: A. (!z. z < y --> z: A)";
|
|
91 |
by (Fast_tac 1);
|
|
92 |
qed "prealE_lemma3";
|
|
93 |
|
|
94 |
Goal
|
|
95 |
"!!A. [| A : preal; y: A |] ==> (!z. z < y --> z: A)";
|
|
96 |
by (fast_tac (claset() addSDs [prealE_lemma3]) 1);
|
|
97 |
qed "prealE_lemma3a";
|
|
98 |
|
|
99 |
Goal
|
|
100 |
"!!A. [| A : preal; y: A; z < y |] ==> z: A";
|
|
101 |
by (fast_tac (claset() addSDs [prealE_lemma3a]) 1);
|
|
102 |
qed "prealE_lemma3b";
|
|
103 |
|
|
104 |
Goalw [preal_def]
|
|
105 |
"!!A. A : preal ==> !y: A. (? u: A. y < u)";
|
|
106 |
by (Fast_tac 1);
|
|
107 |
qed "prealE_lemma4";
|
|
108 |
|
|
109 |
Goal
|
|
110 |
"!!A. [| A : preal; y: A |] ==> ? u: A. y < u";
|
|
111 |
by (fast_tac (claset() addSDs [prealE_lemma4]) 1);
|
|
112 |
qed "prealE_lemma4a";
|
|
113 |
|
|
114 |
Goal "? x. x~: Rep_preal X";
|
|
115 |
by (cut_inst_tac [("x","X")] Rep_preal 1);
|
|
116 |
by (dtac prealE_lemma2 1);
|
|
117 |
by (rtac ccontr 1);
|
|
118 |
by (auto_tac (claset(),simpset() addsimps [psubset_def]));
|
|
119 |
by (blast_tac (claset() addIs [set_ext] addEs [swap]) 1);
|
|
120 |
qed "not_mem_Rep_preal_Ex";
|
|
121 |
|
|
122 |
(** prat_pnat: the injection from prat to preal **)
|
|
123 |
(** A few lemmas **)
|
|
124 |
Goal "{} < {xa::prat. xa < y}";
|
|
125 |
by (cut_facts_tac [qless_Ex] 1);
|
|
126 |
by (auto_tac (claset() addEs [equalityCE],
|
|
127 |
simpset() addsimps [psubset_def]));
|
|
128 |
qed "lemma_prat_less_set_Ex";
|
|
129 |
|
|
130 |
Goal "{xa::prat. xa < y} : preal";
|
|
131 |
by (cut_facts_tac [qless_Ex] 1);
|
|
132 |
by Safe_tac;
|
|
133 |
by (rtac lemma_prat_less_set_Ex 1);
|
|
134 |
by (auto_tac (claset() addIs [prat_less_trans],
|
|
135 |
simpset() addsimps [psubset_def]));
|
|
136 |
by (eres_inst_tac [("c","y")] equalityCE 1);
|
|
137 |
by (auto_tac (claset() addDs [prat_less_irrefl],simpset()));
|
|
138 |
by (dres_inst_tac [("q1.0","ya")] prat_dense 1);
|
|
139 |
by (Fast_tac 1);
|
|
140 |
qed "lemma_prat_less_set_mem_preal";
|
|
141 |
|
|
142 |
Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y";
|
|
143 |
by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1);
|
|
144 |
by Auto_tac;
|
|
145 |
by (dtac prat_dense 1 THEN etac exE 1);
|
|
146 |
by (eres_inst_tac [("c","xa")] equalityCE 1);
|
|
147 |
by (auto_tac (claset() addDs [prat_less_asym],simpset()));
|
|
148 |
by (dtac prat_dense 1 THEN etac exE 1);
|
|
149 |
by (eres_inst_tac [("c","xa")] equalityCE 1);
|
|
150 |
by (auto_tac (claset() addDs [prat_less_asym],simpset()));
|
|
151 |
qed "lemma_prat_set_eq";
|
|
152 |
|
|
153 |
Goal "inj(preal_prat)";
|
|
154 |
by (rtac injI 1);
|
|
155 |
by (rewtac preal_prat_def);
|
|
156 |
by (dtac (inj_on_Abs_preal RS inj_onD) 1);
|
|
157 |
by (rtac lemma_prat_less_set_mem_preal 1);
|
|
158 |
by (rtac lemma_prat_less_set_mem_preal 1);
|
|
159 |
by (etac lemma_prat_set_eq 1);
|
|
160 |
qed "inj_preal_prat";
|
|
161 |
|
|
162 |
(*** theorems for ordering ***)
|
|
163 |
(* prove introduction and elimination rules for preal_less *)
|
|
164 |
|
|
165 |
Goalw [preal_less_def]
|
|
166 |
"R1 < (R2::preal) = (Rep_preal(R1) < Rep_preal(R2))";
|
|
167 |
by (Fast_tac 1);
|
|
168 |
qed "preal_less_iff";
|
|
169 |
|
|
170 |
Goalw [preal_less_def]
|
|
171 |
"!! (R1::preal). R1 < R2 ==> (Rep_preal(R1) < Rep_preal(R2))";
|
|
172 |
by (Fast_tac 1);
|
|
173 |
qed "preal_lessI";
|
|
174 |
|
|
175 |
Goalw [preal_less_def]
|
|
176 |
"R1 < (R2::preal) --> (Rep_preal(R1) < Rep_preal(R2))";
|
|
177 |
by (Fast_tac 1);
|
|
178 |
qed "preal_lessE_lemma";
|
|
179 |
|
|
180 |
Goal
|
|
181 |
"!! R1. [| R1 < (R2::preal); \
|
|
182 |
\ (Rep_preal(R1) < Rep_preal(R2)) ==> P |] \
|
|
183 |
\ ==> P";
|
|
184 |
by (dtac (preal_lessE_lemma RS mp) 1);
|
|
185 |
by Auto_tac;
|
|
186 |
qed "preal_lessE";
|
|
187 |
|
|
188 |
(* A positive fraction not in a positive real is an upper bound *)
|
|
189 |
(* Gleason p. 122 - Remark (1) *)
|
|
190 |
|
|
191 |
Goal "!!x. x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
|
|
192 |
by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
|
|
193 |
by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
|
|
194 |
qed "not_in_preal_ub";
|
|
195 |
|
|
196 |
(* preal_less is a strong order i.e nonreflexive and transitive *)
|
|
197 |
|
|
198 |
Goalw [preal_less_def] "~ (x::preal) < x";
|
|
199 |
by (simp_tac (simpset() addsimps [psubset_def]) 1);
|
|
200 |
qed "preal_less_not_refl";
|
|
201 |
|
|
202 |
(*** y < y ==> P ***)
|
|
203 |
bind_thm("preal_less_irrefl",preal_less_not_refl RS notE);
|
|
204 |
|
|
205 |
Goal "!!(x::preal). x < y ==> x ~= y";
|
|
206 |
by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
|
|
207 |
qed "preal_not_refl2";
|
|
208 |
|
|
209 |
Goalw [preal_less_def] "!!(x::preal). [| x < y; y < z |] ==> x < z";
|
|
210 |
by (auto_tac (claset() addDs [subsetD,equalityI],
|
|
211 |
simpset() addsimps [psubset_def]));
|
|
212 |
qed "preal_less_trans";
|
|
213 |
|
|
214 |
Goal "!! (q1::preal). [| q1 < q2; q2 < q1 |] ==> P";
|
|
215 |
by (dtac preal_less_trans 1 THEN assume_tac 1);
|
|
216 |
by (asm_full_simp_tac (simpset() addsimps [preal_less_not_refl]) 1);
|
|
217 |
qed "preal_less_asym";
|
|
218 |
|
|
219 |
Goalw [preal_less_def]
|
|
220 |
"(r1::preal) < r2 | r1 = r2 | r2 < r1";
|
|
221 |
by (auto_tac (claset() addSDs [inj_Rep_preal RS injD],
|
|
222 |
simpset() addsimps [psubset_def]));
|
|
223 |
by (rtac prealE_lemma3b 1 THEN rtac Rep_preal 1);
|
|
224 |
by (assume_tac 1);
|
|
225 |
by (fast_tac (claset() addDs [not_in_preal_ub]) 1);
|
|
226 |
qed "preal_linear";
|
|
227 |
|
|
228 |
Goal
|
|
229 |
"!!(r1::preal). [| r1 < r2 ==> P; r1 = r2 ==> P; \
|
|
230 |
\ r2 < r1 ==> P |] ==> P";
|
|
231 |
by (cut_inst_tac [("r1.0","r1"),("r2.0","r2")] preal_linear 1);
|
|
232 |
by Auto_tac;
|
|
233 |
qed "preal_linear_less2";
|
|
234 |
|
|
235 |
(*** Properties of addition ***)
|
|
236 |
|
|
237 |
Goalw [preal_add_def] "(x::preal) + y = y + x";
|
|
238 |
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
|
|
239 |
by (rtac set_ext 1);
|
|
240 |
by (blast_tac (claset() addIs [prat_add_commute RS subst]) 1);
|
|
241 |
qed "preal_add_commute";
|
|
242 |
|
|
243 |
(** addition of two positive reals gives a positive real **)
|
|
244 |
(** lemmas for proving positive reals addition set in preal **)
|
|
245 |
|
|
246 |
(** Part 1 of Dedekind sections def **)
|
|
247 |
Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
|
|
248 |
by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
|
|
249 |
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
|
|
250 |
qed "preal_add_set_not_empty";
|
|
251 |
|
|
252 |
(** Part 2 of Dedekind sections def **)
|
|
253 |
Goal "? q. q ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
|
|
254 |
by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
|
|
255 |
by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
|
|
256 |
by (REPEAT(etac exE 1));
|
|
257 |
by (REPEAT(dtac not_in_preal_ub 1));
|
|
258 |
by (res_inst_tac [("x","x+xa")] exI 1);
|
|
259 |
by (Auto_tac THEN (REPEAT(etac ballE 1)) THEN Auto_tac);
|
|
260 |
by (dtac prat_add_less_mono 1);
|
|
261 |
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
|
|
262 |
qed "preal_not_mem_add_set_Ex";
|
|
263 |
|
|
264 |
Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < {q. True}";
|
|
265 |
by (auto_tac (claset() addSIs [psubsetI],simpset()));
|
|
266 |
by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
|
|
267 |
by (etac exE 1);
|
|
268 |
by (eres_inst_tac [("c","q")] equalityCE 1);
|
|
269 |
by Auto_tac;
|
|
270 |
qed "preal_add_set_not_prat_set";
|
|
271 |
|
|
272 |
(** Part 3 of Dedekind sections def **)
|
|
273 |
Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
|
|
274 |
\ !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x + y}";
|
|
275 |
by Auto_tac;
|
|
276 |
by (forward_tac [prat_mult_qinv_less_1] 1);
|
|
277 |
by (forw_inst_tac [("x","x"),("q2.0","$#Abs_pnat 1")]
|
|
278 |
prat_mult_less2_mono1 1);
|
|
279 |
by (forw_inst_tac [("x","ya"),("q2.0","$#Abs_pnat 1")]
|
|
280 |
prat_mult_less2_mono1 1);
|
|
281 |
by (Asm_full_simp_tac 1);
|
|
282 |
by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1));
|
|
283 |
by (REPEAT(etac allE 1));
|
|
284 |
by Auto_tac;
|
|
285 |
by (REPEAT(rtac bexI 1));
|
|
286 |
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2
|
|
287 |
RS sym,prat_add_assoc RS sym,prat_mult_assoc]));
|
|
288 |
qed "preal_add_set_lemma3";
|
|
289 |
|
|
290 |
Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
|
|
291 |
\ ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. y < u";
|
|
292 |
by Auto_tac;
|
|
293 |
by (dtac (Rep_preal RS prealE_lemma4a) 1);
|
|
294 |
by (auto_tac (claset() addIs [prat_add_less2_mono1],simpset()));
|
|
295 |
qed "preal_add_set_lemma4";
|
|
296 |
|
|
297 |
Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y} : preal";
|
|
298 |
by (rtac prealI2 1);
|
|
299 |
by (rtac preal_add_set_not_empty 1);
|
|
300 |
by (rtac preal_add_set_not_prat_set 1);
|
|
301 |
by (rtac preal_add_set_lemma3 1);
|
|
302 |
by (rtac preal_add_set_lemma4 1);
|
|
303 |
qed "preal_mem_add_set";
|
|
304 |
|
|
305 |
Goalw [preal_add_def] "((x::preal) + y) + z = x + (y + z)";
|
|
306 |
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
|
|
307 |
by (rtac set_ext 1);
|
|
308 |
by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
|
|
309 |
by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
|
|
310 |
by (auto_tac (claset(),simpset() addsimps prat_add_ac));
|
|
311 |
by (rtac bexI 1);
|
|
312 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_add_ac));
|
|
313 |
qed "preal_add_assoc";
|
|
314 |
|
|
315 |
qed_goal "preal_add_left_commute" thy
|
|
316 |
"(z1::preal) + (z2 + z3) = z2 + (z1 + z3)"
|
|
317 |
(fn _ => [rtac (preal_add_commute RS trans) 1, rtac (preal_add_assoc RS trans) 1,
|
|
318 |
rtac (preal_add_commute RS arg_cong) 1]);
|
|
319 |
|
|
320 |
(* Positive Reals addition is an AC operator *)
|
|
321 |
val preal_add_ac = [preal_add_assoc, preal_add_commute, preal_add_left_commute];
|
|
322 |
|
|
323 |
(*** Properties of multiplication ***)
|
|
324 |
|
|
325 |
(** Proofs essentially same as for addition **)
|
|
326 |
|
|
327 |
Goalw [preal_mult_def] "(x::preal) * y = y * x";
|
|
328 |
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
|
|
329 |
by (rtac set_ext 1);
|
|
330 |
by (blast_tac (claset() addIs [prat_mult_commute RS subst]) 1);
|
|
331 |
qed "preal_mult_commute";
|
|
332 |
|
|
333 |
(** multiplication of two positive reals gives a positive real **)
|
|
334 |
(** lemmas for proving positive reals multiplication set in preal **)
|
|
335 |
|
|
336 |
(** Part 1 of Dedekind sections def **)
|
|
337 |
Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
|
|
338 |
by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
|
|
339 |
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
|
|
340 |
qed "preal_mult_set_not_empty";
|
|
341 |
|
|
342 |
(** Part 2 of Dedekind sections def **)
|
|
343 |
Goal "? q. q ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
|
|
344 |
by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
|
|
345 |
by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
|
|
346 |
by (REPEAT(etac exE 1));
|
|
347 |
by (REPEAT(dtac not_in_preal_ub 1));
|
|
348 |
by (res_inst_tac [("x","x*xa")] exI 1);
|
|
349 |
by (Auto_tac THEN (REPEAT(etac ballE 1)) THEN Auto_tac );
|
|
350 |
by (dtac prat_mult_less_mono 1);
|
|
351 |
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
|
|
352 |
qed "preal_not_mem_mult_set_Ex";
|
|
353 |
|
|
354 |
Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < {q. True}";
|
|
355 |
by (auto_tac (claset() addSIs [psubsetI],simpset()));
|
|
356 |
by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
|
|
357 |
by (etac exE 1);
|
|
358 |
by (eres_inst_tac [("c","q")] equalityCE 1);
|
|
359 |
by Auto_tac;
|
|
360 |
qed "preal_mult_set_not_prat_set";
|
|
361 |
|
|
362 |
(** Part 3 of Dedekind sections def **)
|
|
363 |
Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
|
|
364 |
\ !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x * y}";
|
|
365 |
by Auto_tac;
|
|
366 |
by (forw_inst_tac [("x","qinv(ya)"),("q1.0","z")]
|
|
367 |
prat_mult_left_less2_mono1 1);
|
|
368 |
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
|
|
369 |
by (dtac (Rep_preal RS prealE_lemma3a) 1);
|
|
370 |
by (etac allE 1);
|
|
371 |
by (REPEAT(rtac bexI 1));
|
|
372 |
by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
|
|
373 |
qed "preal_mult_set_lemma3";
|
|
374 |
|
|
375 |
Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
|
|
376 |
\ ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. y < u";
|
|
377 |
by Auto_tac;
|
|
378 |
by (dtac (Rep_preal RS prealE_lemma4a) 1);
|
|
379 |
by (auto_tac (claset() addIs [prat_mult_less2_mono1],simpset()));
|
|
380 |
qed "preal_mult_set_lemma4";
|
|
381 |
|
|
382 |
Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y} : preal";
|
|
383 |
by (rtac prealI2 1);
|
|
384 |
by (rtac preal_mult_set_not_empty 1);
|
|
385 |
by (rtac preal_mult_set_not_prat_set 1);
|
|
386 |
by (rtac preal_mult_set_lemma3 1);
|
|
387 |
by (rtac preal_mult_set_lemma4 1);
|
|
388 |
qed "preal_mem_mult_set";
|
|
389 |
|
|
390 |
Goalw [preal_mult_def] "((x::preal) * y) * z = x * (y * z)";
|
|
391 |
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
|
|
392 |
by (rtac set_ext 1);
|
|
393 |
by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
|
|
394 |
by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
|
|
395 |
by (auto_tac (claset(),simpset() addsimps prat_mult_ac));
|
|
396 |
by (rtac bexI 1);
|
|
397 |
by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_mult_ac));
|
|
398 |
qed "preal_mult_assoc";
|
|
399 |
|
|
400 |
qed_goal "preal_mult_left_commute" thy
|
|
401 |
"(z1::preal) * (z2 * z3) = z2 * (z1 * z3)"
|
|
402 |
(fn _ => [rtac (preal_mult_commute RS trans) 1,
|
|
403 |
rtac (preal_mult_assoc RS trans) 1,
|
|
404 |
rtac (preal_mult_commute RS arg_cong) 1]);
|
|
405 |
|
|
406 |
(* Positive Reals multiplication is an AC operator *)
|
|
407 |
val preal_mult_ac = [preal_mult_assoc,
|
|
408 |
preal_mult_commute,
|
|
409 |
preal_mult_left_commute];
|
|
410 |
|
|
411 |
(* Positive Real 1 is the multiplicative identity element *)
|
|
412 |
(* long *)
|
|
413 |
Goalw [preal_prat_def,preal_mult_def] "(@#($#Abs_pnat 1)) * z = z";
|
|
414 |
by (rtac (Rep_preal_inverse RS subst) 1);
|
|
415 |
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
|
|
416 |
by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1);
|
|
417 |
by (rtac set_ext 1);
|
|
418 |
by (auto_tac(claset(),simpset() addsimps [Rep_preal_inverse]));
|
|
419 |
by (EVERY1[dtac (Rep_preal RS prealE_lemma4a),etac bexE]);
|
|
420 |
by (dtac prat_mult_less_mono 1);
|
|
421 |
by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3a],simpset()));
|
|
422 |
by (EVERY1[forward_tac [Rep_preal RS prealE_lemma4a],etac bexE]);
|
|
423 |
by (forw_inst_tac [("x","qinv(u)"),("q1.0","x")]
|
|
424 |
prat_mult_less2_mono1 1);
|
|
425 |
by (rtac exI 1 THEN Auto_tac THEN res_inst_tac [("x","u")] bexI 1);
|
|
426 |
by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
|
|
427 |
qed "preal_mult_1";
|
|
428 |
|
|
429 |
Goal "z * (@#($#Abs_pnat 1)) = z";
|
|
430 |
by (rtac (preal_mult_commute RS subst) 1);
|
|
431 |
by (rtac preal_mult_1 1);
|
|
432 |
qed "preal_mult_1_right";
|
|
433 |
|
|
434 |
(** Lemmas **)
|
|
435 |
|
|
436 |
qed_goal "preal_add_assoc_cong" thy
|
|
437 |
"!!z. (z::preal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
|
|
438 |
(fn _ => [(asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1)]);
|
|
439 |
|
|
440 |
qed_goal "preal_add_assoc_swap" thy "(z::preal) + (v + w) = v + (z + w)"
|
|
441 |
(fn _ => [(REPEAT (ares_tac [preal_add_commute RS preal_add_assoc_cong] 1))]);
|
|
442 |
|
|
443 |
(** Distribution of multiplication across addition **)
|
|
444 |
(** lemmas for the proof **)
|
|
445 |
|
|
446 |
(** lemmas **)
|
|
447 |
Goalw [preal_add_def]
|
|
448 |
"!!R. z: Rep_preal(R+S) ==> \
|
|
449 |
\ ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y";
|
|
450 |
by (dtac (preal_mem_add_set RS Abs_preal_inverse RS subst) 1);
|
|
451 |
by (Fast_tac 1);
|
|
452 |
qed "mem_Rep_preal_addD";
|
|
453 |
|
|
454 |
Goalw [preal_add_def]
|
|
455 |
"!!R. ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y \
|
|
456 |
\ ==> z: Rep_preal(R+S)";
|
|
457 |
by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
|
|
458 |
by (Fast_tac 1);
|
|
459 |
qed "mem_Rep_preal_addI";
|
|
460 |
|
|
461 |
Goal " z: Rep_preal(R+S) = (? x: Rep_preal(R). \
|
|
462 |
\ ? y: Rep_preal(S). z = x + y)";
|
|
463 |
by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
|
|
464 |
qed "mem_Rep_preal_add_iff";
|
|
465 |
|
|
466 |
Goalw [preal_mult_def]
|
|
467 |
"!!R. z: Rep_preal(R*S) ==> \
|
|
468 |
\ ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y";
|
|
469 |
by (dtac (preal_mem_mult_set RS Abs_preal_inverse RS subst) 1);
|
|
470 |
by (Fast_tac 1);
|
|
471 |
qed "mem_Rep_preal_multD";
|
|
472 |
|
|
473 |
Goalw [preal_mult_def]
|
|
474 |
"!!R. ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y \
|
|
475 |
\ ==> z: Rep_preal(R*S)";
|
|
476 |
by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
|
|
477 |
by (Fast_tac 1);
|
|
478 |
qed "mem_Rep_preal_multI";
|
|
479 |
|
|
480 |
Goal " z: Rep_preal(R*S) = (? x: Rep_preal(R). \
|
|
481 |
\ ? y: Rep_preal(S). z = x * y)";
|
|
482 |
by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
|
|
483 |
qed "mem_Rep_preal_mult_iff";
|
|
484 |
|
|
485 |
(** More lemmas for preal_add_mult_distrib2 **)
|
|
486 |
goal PRat.thy "!!(a1::prat). a1 < a2 ==> a1 * b + a2 * c < a2 * (b + c)";
|
|
487 |
by (auto_tac (claset() addSIs [prat_add_less2_mono1,prat_mult_less2_mono1],
|
|
488 |
simpset() addsimps [prat_add_mult_distrib2]));
|
|
489 |
qed "lemma_prat_add_mult_mono";
|
|
490 |
|
|
491 |
Goal "!!xb. [| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
|
|
492 |
\ Rep_preal w; yb: Rep_preal w |] ==> \
|
|
493 |
\ xb * ya + xc * yb: Rep_preal (z1 * w + z2 * w)";
|
|
494 |
by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
|
|
495 |
qed "lemma_add_mult_mem_Rep_preal";
|
|
496 |
|
|
497 |
Goal "!!xb. [| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
|
|
498 |
\ Rep_preal w; yb: Rep_preal w |] ==> \
|
|
499 |
\ yb*(xb + xc): Rep_preal (w*(z1 + z2))";
|
|
500 |
by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
|
|
501 |
qed "lemma_add_mult_mem_Rep_preal1";
|
|
502 |
|
|
503 |
Goal "!!x. x: Rep_preal (w * z1 + w * z2) ==> \
|
|
504 |
\ x: Rep_preal (w * (z1 + z2))";
|
|
505 |
by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD],
|
|
506 |
simpset()));
|
|
507 |
by (forw_inst_tac [("ya","xb"),("yb","xc"),("xb","ya"),("xc","yb")]
|
|
508 |
lemma_add_mult_mem_Rep_preal1 1);
|
|
509 |
by Auto_tac;
|
|
510 |
by (res_inst_tac [("q1.0","xb"),("q2.0","xc")] prat_linear_less2 1);
|
|
511 |
by (dres_inst_tac [("b","ya"),("c","yb")] lemma_prat_add_mult_mono 1);
|
|
512 |
by (rtac (Rep_preal RS prealE_lemma3b) 1);
|
|
513 |
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2]));
|
|
514 |
by (dres_inst_tac [("ya","xc"),("yb","xb"),("xc","ya"),("xb","yb")]
|
|
515 |
lemma_add_mult_mem_Rep_preal1 1);
|
|
516 |
by Auto_tac;
|
|
517 |
by (dres_inst_tac [("b","yb"),("c","ya")] lemma_prat_add_mult_mono 1);
|
|
518 |
by (rtac (Rep_preal RS prealE_lemma3b) 1);
|
|
519 |
by (thin_tac "xc * ya + xc * yb : Rep_preal (w * (z1 + z2))" 1);
|
|
520 |
by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib,
|
|
521 |
prat_add_commute] @ preal_add_ac ));
|
|
522 |
qed "lemma_preal_add_mult_distrib";
|
|
523 |
|
|
524 |
Goal "!!x. x: Rep_preal (w * (z1 + z2)) ==> \
|
|
525 |
\ x: Rep_preal (w * z1 + w * z2)";
|
|
526 |
by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD]
|
|
527 |
addSIs [bexI,mem_Rep_preal_addI,mem_Rep_preal_multI],
|
|
528 |
simpset() addsimps [prat_add_mult_distrib2]));
|
|
529 |
qed "lemma_preal_add_mult_distrib2";
|
|
530 |
|
|
531 |
Goal "(w * ((z1::preal) + z2)) = (w * z1) + (w * z2)";
|
|
532 |
by (rtac (inj_Rep_preal RS injD) 1);
|
|
533 |
by (rtac set_ext 1);
|
|
534 |
by (fast_tac (claset() addIs [lemma_preal_add_mult_distrib,
|
|
535 |
lemma_preal_add_mult_distrib2]) 1);
|
|
536 |
qed "preal_add_mult_distrib2";
|
|
537 |
|
|
538 |
Goal "(((z1::preal) + z2) * w) = (z1 * w) + (z2 * w)";
|
|
539 |
by (simp_tac (simpset() addsimps [preal_mult_commute,
|
|
540 |
preal_add_mult_distrib2]) 1);
|
|
541 |
qed "preal_add_mult_distrib";
|
|
542 |
|
|
543 |
(*** Prove existence of inverse ***)
|
|
544 |
(*** Inverse is a positive real ***)
|
|
545 |
|
|
546 |
Goal "? y. qinv(y) ~: Rep_preal X";
|
|
547 |
by (cut_inst_tac [("X","X")] not_mem_Rep_preal_Ex 1);
|
|
548 |
by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
|
|
549 |
by Auto_tac;
|
|
550 |
qed "qinv_not_mem_Rep_preal_Ex";
|
|
551 |
|
|
552 |
Goal "? q. q: {x. ? y. x < y & qinv y ~: Rep_preal A}";
|
|
553 |
by (cut_inst_tac [("X","A")] qinv_not_mem_Rep_preal_Ex 1);
|
|
554 |
by Auto_tac;
|
|
555 |
by (cut_inst_tac [("y","y")] qless_Ex 1);
|
|
556 |
by (Fast_tac 1);
|
|
557 |
qed "lemma_preal_mem_inv_set_ex";
|
|
558 |
|
|
559 |
(** Part 1 of Dedekind sections def **)
|
|
560 |
Goal "{} < {x. ? y. x < y & qinv y ~: Rep_preal A}";
|
|
561 |
by (cut_facts_tac [lemma_preal_mem_inv_set_ex] 1);
|
|
562 |
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
|
|
563 |
qed "preal_inv_set_not_empty";
|
|
564 |
|
|
565 |
(** Part 2 of Dedekind sections def **)
|
|
566 |
Goal "? y. qinv(y) : Rep_preal X";
|
|
567 |
by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
|
|
568 |
by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
|
|
569 |
by Auto_tac;
|
|
570 |
qed "qinv_mem_Rep_preal_Ex";
|
|
571 |
|
|
572 |
Goal "? x. x ~: {x. ? y. x < y & qinv y ~: Rep_preal A}";
|
|
573 |
by (rtac ccontr 1);
|
|
574 |
by (cut_inst_tac [("X","A")] qinv_mem_Rep_preal_Ex 1);
|
|
575 |
by Auto_tac;
|
|
576 |
by (EVERY1[etac allE, etac exE, etac conjE]);
|
|
577 |
by (dtac qinv_prat_less 1 THEN dtac not_in_preal_ub 1);
|
|
578 |
by (eres_inst_tac [("x","qinv y")] ballE 1);
|
|
579 |
by (dtac prat_less_trans 1);
|
|
580 |
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
|
|
581 |
qed "preal_not_mem_inv_set_Ex";
|
|
582 |
|
|
583 |
Goal "{x. ? y. x < y & qinv y ~: Rep_preal A} < {q. True}";
|
|
584 |
by (auto_tac (claset() addSIs [psubsetI],simpset()));
|
|
585 |
by (cut_inst_tac [("A","A")] preal_not_mem_inv_set_Ex 1);
|
|
586 |
by (etac exE 1);
|
|
587 |
by (eres_inst_tac [("c","x")] equalityCE 1);
|
|
588 |
by Auto_tac;
|
|
589 |
qed "preal_inv_set_not_prat_set";
|
|
590 |
|
|
591 |
(** Part 3 of Dedekind sections def **)
|
|
592 |
Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
|
|
593 |
\ !z. z < y --> z : {x. ? y. x < y & qinv y ~: Rep_preal A}";
|
|
594 |
by Auto_tac;
|
|
595 |
by (res_inst_tac [("x","ya")] exI 1);
|
|
596 |
by (auto_tac (claset() addIs [prat_less_trans],simpset()));
|
|
597 |
qed "preal_inv_set_lemma3";
|
|
598 |
|
|
599 |
Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
|
|
600 |
\ Bex {x. ? y. x < y & qinv y ~: Rep_preal A} (op < y)";
|
|
601 |
by (blast_tac (claset() addDs [prat_dense]) 1);
|
|
602 |
qed "preal_inv_set_lemma4";
|
|
603 |
|
|
604 |
Goal "{x. ? y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
|
|
605 |
by (rtac prealI2 1);
|
|
606 |
by (rtac preal_inv_set_not_empty 1);
|
|
607 |
by (rtac preal_inv_set_not_prat_set 1);
|
|
608 |
by (rtac preal_inv_set_lemma3 1);
|
|
609 |
by (rtac preal_inv_set_lemma4 1);
|
|
610 |
qed "preal_mem_inv_set";
|
|
611 |
|
|
612 |
(*more lemmas for inverse *)
|
|
613 |
Goal "!!x. x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
|
|
614 |
by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
|
|
615 |
simpset() addsimps [pinv_def,preal_prat_def] ));
|
|
616 |
by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
|
|
617 |
by (auto_tac (claset() addSDs [not_in_preal_ub],simpset()));
|
|
618 |
by (dtac prat_mult_less_mono 1 THEN Blast_tac 1);
|
|
619 |
by (auto_tac (claset(),simpset()));
|
|
620 |
qed "preal_mem_mult_invD";
|
|
621 |
|
|
622 |
(*** Gleason's Lemma 9-3.4 p 122 ***)
|
|
623 |
Goal "!!p. ! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
|
|
624 |
\ ? xb : Rep_preal(A). xb + ($#p)*x : Rep_preal(A)";
|
|
625 |
by (cut_facts_tac [mem_Rep_preal_Ex] 1);
|
|
626 |
by (res_inst_tac [("n","p")] pnat_induct 1);
|
|
627 |
by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
|
|
628 |
pSuc_is_plus_one,prat_add_mult_distrib,prat_pnat_add,prat_add_assoc RS sym]));
|
|
629 |
qed "lemma1_gleason9_34";
|
|
630 |
|
|
631 |
Goal "Abs_prat (ratrel ^^ {(y, z)}) < xb + \
|
|
632 |
\ Abs_prat (ratrel ^^ {(x*y, Abs_pnat 1)})*Abs_prat (ratrel ^^ {(w, x)})";
|
|
633 |
by (res_inst_tac [("j","Abs_prat (ratrel ^^ {(x * y, Abs_pnat 1)}) *\
|
|
634 |
\ Abs_prat (ratrel ^^ {(w, x)})")] prat_le_less_trans 1);
|
|
635 |
by (rtac prat_self_less_add_right 2);
|
|
636 |
by (auto_tac (claset() addIs [lemma_Abs_prat_le3],
|
|
637 |
simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
|
|
638 |
qed "lemma1b_gleason9_34";
|
|
639 |
|
|
640 |
Goal "!!A. ! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
|
|
641 |
by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
|
|
642 |
by (etac exE 1);
|
|
643 |
by (dtac not_in_preal_ub 1);
|
|
644 |
by (res_inst_tac [("z","x")] eq_Abs_prat 1);
|
|
645 |
by (res_inst_tac [("z","xa")] eq_Abs_prat 1);
|
|
646 |
by (dres_inst_tac [("p","y*xb")] lemma1_gleason9_34 1);
|
|
647 |
by (etac bexE 1);
|
|
648 |
by (cut_inst_tac [("x","y"),("y","xb"),("w","xaa"),
|
|
649 |
("z","ya"),("xb","xba")] lemma1b_gleason9_34 1);
|
|
650 |
by (dres_inst_tac [("x","xba + $#(y * xb) * x")] bspec 1);
|
|
651 |
by (auto_tac (claset() addIs [prat_less_asym],
|
|
652 |
simpset() addsimps [prat_pnat_def]));
|
|
653 |
qed "lemma_gleason9_34a";
|
|
654 |
|
|
655 |
Goal "? r: Rep_preal(R). r + x ~: Rep_preal(R)";
|
|
656 |
by (rtac ccontr 1);
|
|
657 |
by (blast_tac (claset() addIs [lemma_gleason9_34a]) 1);
|
|
658 |
qed "lemma_gleason9_34";
|
|
659 |
|
|
660 |
(*** Gleason's Lemma 9-3.6 ***)
|
|
661 |
(* lemmas for Gleason 9-3.6 *)
|
|
662 |
(* *)
|
|
663 |
(******************************)
|
|
664 |
|
|
665 |
Goal "r + r*qinv(xa)*Q3 = r*qinv(xa)*(xa + Q3)";
|
|
666 |
by (full_simp_tac (simpset() addsimps [prat_add_mult_distrib2,
|
|
667 |
prat_mult_assoc]) 1);
|
|
668 |
qed "lemma1_gleason9_36";
|
|
669 |
|
|
670 |
Goal "r*qinv(xa)*(xa*x) = r*x";
|
|
671 |
by (full_simp_tac (simpset() addsimps prat_mult_ac) 1);
|
|
672 |
qed "lemma2_gleason9_36";
|
|
673 |
(******)
|
|
674 |
|
|
675 |
(*** FIXME: long! ***)
|
|
676 |
Goal "!!A. $#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
|
|
677 |
by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
|
|
678 |
by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
|
|
679 |
by (Fast_tac 1);
|
|
680 |
by (dres_inst_tac [("x","xa")] prat_self_less_mult_right 1);
|
|
681 |
by (etac prat_lessE 1);
|
|
682 |
by (cut_inst_tac [("R","A"),("x","Q3")] lemma_gleason9_34 1);
|
|
683 |
by (dtac sym 1 THEN Auto_tac );
|
|
684 |
by (forward_tac [not_in_preal_ub] 1);
|
|
685 |
by (dres_inst_tac [("x","xa + Q3")] bspec 1 THEN assume_tac 1);
|
|
686 |
by (dtac prat_add_right_less_cancel 1);
|
|
687 |
by (dres_inst_tac [("x","qinv(xa)*Q3")] prat_mult_less2_mono1 1);
|
|
688 |
by (dres_inst_tac [("x","r")] prat_add_less2_mono2 1);
|
|
689 |
by (asm_full_simp_tac (simpset() addsimps
|
|
690 |
[prat_mult_assoc RS sym,lemma1_gleason9_36]) 1);
|
|
691 |
by (dtac sym 1);
|
|
692 |
by (auto_tac (claset(),simpset() addsimps [lemma2_gleason9_36]));
|
|
693 |
by (res_inst_tac [("x","r")] bexI 1);
|
|
694 |
by (rtac notI 1);
|
|
695 |
by (dres_inst_tac [("y","r*x")] (Rep_preal RS prealE_lemma3b) 1);
|
|
696 |
by Auto_tac;
|
|
697 |
qed "lemma_gleason9_36";
|
|
698 |
|
|
699 |
Goal "!!A. $#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
|
|
700 |
by (rtac lemma_gleason9_36 1);
|
|
701 |
by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
|
|
702 |
qed "lemma_gleason9_36a";
|
|
703 |
|
|
704 |
(*** Part 2 of existence of inverse ***)
|
|
705 |
Goal "!!x. x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
|
|
706 |
by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
|
|
707 |
simpset() addsimps [pinv_def,preal_prat_def] ));
|
|
708 |
by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1);
|
|
709 |
by (dtac prat_qinv_gt_1 1);
|
|
710 |
by (dres_inst_tac [("A","A")] lemma_gleason9_36a 1);
|
|
711 |
by Auto_tac;
|
|
712 |
by (dtac (Rep_preal RS prealE_lemma4a) 1);
|
|
713 |
by (Auto_tac THEN dtac qinv_prat_less 1);
|
|
714 |
by (res_inst_tac [("x","qinv(u)*x")] exI 1);
|
|
715 |
by (rtac conjI 1);
|
|
716 |
by (res_inst_tac [("x","qinv(r)*x")] exI 1);
|
|
717 |
by (auto_tac (claset() addIs [prat_mult_less2_mono1],
|
|
718 |
simpset() addsimps [qinv_mult_eq,qinv_qinv]));
|
|
719 |
by (res_inst_tac [("x","u")] bexI 1);
|
|
720 |
by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc,
|
|
721 |
prat_mult_left_commute]));
|
|
722 |
qed "preal_mem_mult_invI";
|
|
723 |
|
|
724 |
Goal "pinv(A)*A = (@#($#Abs_pnat 1))";
|
|
725 |
by (rtac (inj_Rep_preal RS injD) 1);
|
|
726 |
by (rtac set_ext 1);
|
|
727 |
by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1);
|
|
728 |
qed "preal_mult_inv";
|
|
729 |
|
|
730 |
Goal "A*pinv(A) = (@#($#Abs_pnat 1))";
|
|
731 |
by (rtac (preal_mult_commute RS subst) 1);
|
|
732 |
by (rtac preal_mult_inv 1);
|
|
733 |
qed "preal_mult_inv_right";
|
|
734 |
|
|
735 |
val [prem] = goal thy
|
|
736 |
"(!!u. z = Abs_preal(u) ==> P) ==> P";
|
|
737 |
by (cut_inst_tac [("x1","z")]
|
|
738 |
(rewrite_rule [preal_def] (Rep_preal RS Abs_preal_inverse)) 1);
|
|
739 |
by (res_inst_tac [("u","Rep_preal z")] prem 1);
|
|
740 |
by (dtac (inj_Rep_preal RS injD) 1);
|
|
741 |
by (Asm_simp_tac 1);
|
|
742 |
qed "eq_Abs_preal";
|
|
743 |
|
|
744 |
(*** Lemmas/Theorem(s) need lemma_gleason9_34 ***)
|
|
745 |
Goal "Rep_preal (R1) <= Rep_preal(R1 + R2)";
|
|
746 |
by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1);
|
|
747 |
by (auto_tac (claset() addSIs [bexI] addIs [(Rep_preal RS prealE_lemma3b),
|
|
748 |
prat_self_less_add_left,mem_Rep_preal_addI],simpset()));
|
|
749 |
qed "Rep_preal_self_subset";
|
|
750 |
|
|
751 |
Goal "~ Rep_preal (R1 + R2) <= Rep_preal(R1)";
|
|
752 |
by (cut_inst_tac [("X","R2")] mem_Rep_preal_Ex 1);
|
|
753 |
by (etac exE 1);
|
|
754 |
by (cut_inst_tac [("R","R1")] lemma_gleason9_34 1);
|
|
755 |
by (auto_tac (claset() addIs [mem_Rep_preal_addI],simpset()));
|
|
756 |
qed "Rep_preal_sum_not_subset";
|
|
757 |
|
|
758 |
Goal "Rep_preal (R1 + R2) ~= Rep_preal(R1)";
|
|
759 |
by (rtac notI 1);
|
|
760 |
by (etac equalityE 1);
|
|
761 |
by (asm_full_simp_tac (simpset() addsimps [Rep_preal_sum_not_subset]) 1);
|
|
762 |
qed "Rep_preal_sum_not_eq";
|
|
763 |
|
|
764 |
(*** at last --- Gleason prop. 9-3.5(iii) p. 123 ***)
|
|
765 |
Goalw [preal_less_def,psubset_def] "(R1::preal) < R1 + R2";
|
|
766 |
by (simp_tac (simpset() addsimps [Rep_preal_self_subset,
|
|
767 |
Rep_preal_sum_not_eq RS not_sym]) 1);
|
|
768 |
qed "preal_self_less_add_left";
|
|
769 |
|
|
770 |
Goal "(R1::preal) < R2 + R1";
|
|
771 |
by (simp_tac (simpset() addsimps [preal_add_commute,preal_self_less_add_left]) 1);
|
|
772 |
qed "preal_self_less_add_right";
|
|
773 |
|
|
774 |
(*** Properties of <= ***)
|
|
775 |
|
|
776 |
Goalw [preal_le_def,psubset_def,preal_less_def]
|
|
777 |
"!!w. z<=w ==> ~(w<(z::preal))";
|
|
778 |
by (auto_tac (claset() addDs [equalityI],simpset()));
|
|
779 |
qed "preal_leD";
|
|
780 |
|
|
781 |
val preal_leE = make_elim preal_leD;
|
|
782 |
|
|
783 |
Goalw [preal_le_def,psubset_def,preal_less_def]
|
|
784 |
"!!z. ~ z <= w ==> w<(z::preal)";
|
|
785 |
by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
|
|
786 |
by (auto_tac (claset(),simpset() addsimps [preal_less_def,psubset_def]));
|
|
787 |
qed "not_preal_leE";
|
|
788 |
|
|
789 |
Goal "!!w. ~(w < z) ==> z <= (w::preal)";
|
|
790 |
by (fast_tac (claset() addIs [not_preal_leE]) 1);
|
|
791 |
qed "preal_leI";
|
|
792 |
|
|
793 |
Goal "!!w. (~(w < z)) = (z <= (w::preal))";
|
|
794 |
by (fast_tac (claset() addSIs [preal_leI,preal_leD]) 1);
|
|
795 |
qed "preal_less_le_iff";
|
|
796 |
|
|
797 |
Goalw [preal_le_def,preal_less_def,psubset_def]
|
|
798 |
"!!z. z < w ==> z <= (w::preal)";
|
|
799 |
by (Fast_tac 1);
|
|
800 |
qed "preal_less_imp_le";
|
|
801 |
|
|
802 |
Goalw [preal_le_def,preal_less_def,psubset_def]
|
|
803 |
"!!(x::preal). x <= y ==> x < y | x = y";
|
|
804 |
by (auto_tac (claset() addIs [inj_Rep_preal RS injD],simpset()));
|
|
805 |
qed "preal_le_imp_less_or_eq";
|
|
806 |
|
|
807 |
Goalw [preal_le_def,preal_less_def,psubset_def]
|
|
808 |
"!!(x::preal). x < y | x = y ==> x <=y";
|
|
809 |
by Auto_tac;
|
|
810 |
qed "preal_less_or_eq_imp_le";
|
|
811 |
|
|
812 |
Goal "(x <= (y::preal)) = (x < y | x=y)";
|
|
813 |
by (REPEAT(ares_tac [iffI, preal_less_or_eq_imp_le, preal_le_imp_less_or_eq] 1));
|
|
814 |
qed "preal_le_eq_less_or_eq";
|
|
815 |
|
|
816 |
Goalw [preal_le_def] "w <= (w::preal)";
|
|
817 |
by (Simp_tac 1);
|
|
818 |
qed "preal_le_refl";
|
|
819 |
|
|
820 |
val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::preal)";
|
|
821 |
by (dtac preal_le_imp_less_or_eq 1);
|
|
822 |
by (fast_tac (claset() addIs [preal_less_trans]) 1);
|
|
823 |
qed "preal_le_less_trans";
|
|
824 |
|
|
825 |
val prems = goal thy "!!i. [| i < j; j <= k |] ==> i < (k::preal)";
|
|
826 |
by (dtac preal_le_imp_less_or_eq 1);
|
|
827 |
by (fast_tac (claset() addIs [preal_less_trans]) 1);
|
|
828 |
qed "preal_less_le_trans";
|
|
829 |
|
|
830 |
Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::preal)";
|
|
831 |
by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
|
|
832 |
rtac preal_less_or_eq_imp_le, fast_tac (claset() addIs [preal_less_trans])]);
|
|
833 |
qed "preal_le_trans";
|
|
834 |
|
|
835 |
Goal "!!z. [| z <= w; w <= z |] ==> z = (w::preal)";
|
|
836 |
by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
|
|
837 |
fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]);
|
|
838 |
qed "preal_le_anti_sym";
|
|
839 |
|
|
840 |
Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::preal)";
|
|
841 |
by (rtac not_preal_leE 1);
|
|
842 |
by (fast_tac (claset() addDs [preal_le_imp_less_or_eq]) 1);
|
|
843 |
qed "not_less_not_eq_preal_less";
|
|
844 |
|
|
845 |
(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
|
|
846 |
|
|
847 |
(**** Set up all lemmas for proving A < B ==> ?D. A + D = B ****)
|
|
848 |
(**** Gleason prop. 9-3.5(iv) p. 123 ****)
|
|
849 |
(**** Define the D required and show that it is a positive real ****)
|
|
850 |
|
|
851 |
(* useful lemmas - proved elsewhere? *)
|
|
852 |
Goalw [psubset_def] "!!A. A < B ==> ? x. x ~: A & x : B";
|
|
853 |
by (etac conjE 1);
|
|
854 |
by (etac swap 1);
|
|
855 |
by (etac equalityI 1);
|
|
856 |
by Auto_tac;
|
|
857 |
qed "lemma_psubset_mem";
|
|
858 |
|
|
859 |
Goalw [psubset_def] "~ (A::'a set) < A";
|
|
860 |
by (Fast_tac 1);
|
|
861 |
qed "lemma_psubset_not_refl";
|
|
862 |
|
|
863 |
Goalw [psubset_def] "!!(A::'a set). [| A < B; B < C |] ==> A < C";
|
|
864 |
by (auto_tac (claset() addDs [subset_antisym],simpset()));
|
|
865 |
qed "psubset_trans";
|
|
866 |
|
|
867 |
Goalw [psubset_def] "!!(A::'a set). [| A <= B; B < C |] ==> A < C";
|
|
868 |
by (auto_tac (claset() addDs [subset_antisym],simpset()));
|
|
869 |
qed "subset_psubset_trans";
|
|
870 |
|
|
871 |
Goalw [psubset_def] "!!(A::'a set). [| A < B; B <= C |] ==> A < C";
|
|
872 |
by (auto_tac (claset() addDs [subset_antisym],simpset()));
|
|
873 |
qed "subset_psubset_trans2";
|
|
874 |
|
|
875 |
Goalw [psubset_def] "!!(A::'a set). [| A < B; c : A |] ==> c : B";
|
|
876 |
by (auto_tac (claset() addDs [subsetD],simpset()));
|
|
877 |
qed "psubsetD";
|
|
878 |
|
|
879 |
(** Part 1 of Dedekind sections def **)
|
|
880 |
Goalw [preal_less_def]
|
|
881 |
"!!A. A < B ==> \
|
|
882 |
\ ? q. q : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
|
|
883 |
by (EVERY1[dtac lemma_psubset_mem, etac exE, etac conjE]);
|
|
884 |
by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma4a) 1);
|
|
885 |
by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
|
|
886 |
qed "lemma_ex_mem_less_left_add1";
|
|
887 |
|
|
888 |
Goal
|
|
889 |
"!!A. A < B ==> \
|
|
890 |
\ {} < {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
|
|
891 |
by (dtac lemma_ex_mem_less_left_add1 1);
|
|
892 |
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
|
|
893 |
qed "preal_less_set_not_empty";
|
|
894 |
|
|
895 |
(** Part 2 of Dedekind sections def **)
|
|
896 |
Goal "? q. q ~: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
|
|
897 |
by (cut_inst_tac [("X","B")] not_mem_Rep_preal_Ex 1);
|
|
898 |
by (etac exE 1);
|
|
899 |
by (res_inst_tac [("x","x")] exI 1);
|
|
900 |
by Auto_tac;
|
|
901 |
by (cut_inst_tac [("x","x"),("y","n")] prat_self_less_add_right 1);
|
|
902 |
by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
|
|
903 |
qed "lemma_ex_not_mem_less_left_add1";
|
|
904 |
|
|
905 |
Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < {q. True}";
|
|
906 |
by (auto_tac (claset() addSIs [psubsetI],simpset()));
|
|
907 |
by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
|
|
908 |
by (etac exE 1);
|
|
909 |
by (eres_inst_tac [("c","q")] equalityCE 1);
|
|
910 |
by Auto_tac;
|
|
911 |
qed "preal_less_set_not_prat_set";
|
|
912 |
|
|
913 |
(** Part 3 of Dedekind sections def **)
|
|
914 |
Goal "!!A. A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
|
|
915 |
\ !z. z < y --> z : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
|
|
916 |
by Auto_tac;
|
|
917 |
by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
|
|
918 |
by (dtac (Rep_preal RS prealE_lemma3b) 1);
|
|
919 |
by Auto_tac;
|
|
920 |
qed "preal_less_set_lemma3";
|
|
921 |
|
|
922 |
Goal "!!A. A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
|
|
923 |
\ Bex {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
|
|
924 |
by Auto_tac;
|
|
925 |
by (dtac (Rep_preal RS prealE_lemma4a) 1);
|
|
926 |
by (auto_tac (claset(),simpset() addsimps [prat_less_def,prat_add_assoc]));
|
|
927 |
qed "preal_less_set_lemma4";
|
|
928 |
|
|
929 |
Goal
|
|
930 |
"!! (A::preal). A < B ==> \
|
|
931 |
\ {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
|
|
932 |
by (rtac prealI2 1);
|
|
933 |
by (rtac preal_less_set_not_empty 1);
|
|
934 |
by (rtac preal_less_set_not_prat_set 2);
|
|
935 |
by (rtac preal_less_set_lemma3 2);
|
|
936 |
by (rtac preal_less_set_lemma4 3);
|
|
937 |
by Auto_tac;
|
|
938 |
qed "preal_mem_less_set";
|
|
939 |
|
|
940 |
(** proving that A + D <= B **)
|
|
941 |
Goalw [preal_le_def]
|
|
942 |
"!! (A::preal). A < B ==> \
|
|
943 |
\ A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
|
|
944 |
by (rtac subsetI 1);
|
|
945 |
by (dtac mem_Rep_preal_addD 1);
|
|
946 |
by (auto_tac (claset(),simpset() addsimps [
|
|
947 |
preal_mem_less_set RS Abs_preal_inverse]));
|
|
948 |
by (dtac not_in_preal_ub 1);
|
|
949 |
by (dtac bspec 1 THEN assume_tac 1);
|
|
950 |
by (dres_inst_tac [("x","y")] prat_add_less2_mono1 1);
|
|
951 |
by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma3b) 1);
|
|
952 |
by Auto_tac;
|
|
953 |
qed "preal_less_add_left_subsetI";
|
|
954 |
|
|
955 |
(** proving that B <= A + D --- trickier **)
|
|
956 |
(** lemma **)
|
|
957 |
Goal "!!x. x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
|
|
958 |
by (dtac (Rep_preal RS prealE_lemma4a) 1);
|
|
959 |
by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
|
|
960 |
qed "lemma_sum_mem_Rep_preal_ex";
|
|
961 |
|
|
962 |
Goalw [preal_le_def]
|
|
963 |
"!! (A::preal). A < B ==> \
|
|
964 |
\ B <= A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
|
|
965 |
by (rtac subsetI 1);
|
|
966 |
by (res_inst_tac [("Q","x: Rep_preal(A)")] (excluded_middle RS disjE) 1);
|
|
967 |
by (rtac mem_Rep_preal_addI 1);
|
|
968 |
by (dtac lemma_sum_mem_Rep_preal_ex 1);
|
|
969 |
by (etac exE 1);
|
|
970 |
by (cut_inst_tac [("R","A"),("x","e")] lemma_gleason9_34 1 THEN etac bexE 1);
|
|
971 |
by (dtac not_in_preal_ub 1 THEN dtac bspec 1 THEN assume_tac 1);
|
|
972 |
by (etac prat_lessE 1);
|
|
973 |
by (res_inst_tac [("x","r")] bexI 1);
|
|
974 |
by (res_inst_tac [("x","Q3")] bexI 1);
|
|
975 |
by (cut_facts_tac [Rep_preal_self_subset] 4);
|
|
976 |
by (auto_tac (claset(),simpset() addsimps [
|
|
977 |
preal_mem_less_set RS Abs_preal_inverse]));
|
|
978 |
by (res_inst_tac [("x","r+e")] exI 1);
|
|
979 |
by (asm_full_simp_tac (simpset() addsimps prat_add_ac) 1);
|
|
980 |
qed "preal_less_add_left_subsetI2";
|
|
981 |
|
|
982 |
(*** required proof ***)
|
|
983 |
Goal "!! (A::preal). A < B ==> \
|
|
984 |
\ A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
|
|
985 |
by (blast_tac (claset() addIs [preal_le_anti_sym,
|
|
986 |
preal_less_add_left_subsetI,preal_less_add_left_subsetI2]) 1);
|
|
987 |
qed "preal_less_add_left";
|
|
988 |
|
|
989 |
Goal "!! (A::preal). A < B ==> ? D. A + D = B";
|
|
990 |
by (fast_tac (claset() addDs [preal_less_add_left]) 1);
|
|
991 |
qed "preal_less_add_left_Ex";
|
|
992 |
|
|
993 |
Goal "!!(A::preal). A < B ==> A + C < B + C";
|
|
994 |
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
|
|
995 |
simpset() addsimps [preal_add_assoc]));
|
|
996 |
by (res_inst_tac [("y1","D")] (preal_add_commute RS subst) 1);
|
|
997 |
by (auto_tac (claset() addIs [preal_self_less_add_left],
|
|
998 |
simpset() addsimps [preal_add_assoc RS sym]));
|
|
999 |
qed "preal_add_less2_mono1";
|
|
1000 |
|
|
1001 |
Goal "!!(A::preal). A < B ==> C + A < C + B";
|
|
1002 |
by (auto_tac (claset() addIs [preal_add_less2_mono1],
|
|
1003 |
simpset() addsimps [preal_add_commute]));
|
|
1004 |
qed "preal_add_less2_mono2";
|
|
1005 |
|
|
1006 |
Goal
|
|
1007 |
"!!(q1::preal). q1 < q2 ==> q1 * x < q2 * x";
|
|
1008 |
by (dtac preal_less_add_left_Ex 1);
|
|
1009 |
by (auto_tac (claset(),simpset() addsimps [preal_add_mult_distrib,
|
|
1010 |
preal_self_less_add_left]));
|
|
1011 |
qed "preal_mult_less_mono1";
|
|
1012 |
|
|
1013 |
Goal "!!(q1::preal). q1 < q2 ==> x * q1 < x * q2";
|
|
1014 |
by (auto_tac (claset() addDs [preal_mult_less_mono1],
|
|
1015 |
simpset() addsimps [preal_mult_commute]));
|
|
1016 |
qed "preal_mult_left_less_mono1";
|
|
1017 |
|
|
1018 |
Goal "!!(q1::preal). q1 <= q2 ==> x * q1 <= x * q2";
|
|
1019 |
by (dtac preal_le_imp_less_or_eq 1);
|
|
1020 |
by (Step_tac 1);
|
|
1021 |
by (auto_tac (claset() addSIs [preal_le_refl,
|
|
1022 |
preal_less_imp_le,preal_mult_left_less_mono1],simpset()));
|
|
1023 |
qed "preal_mult_left_le_mono1";
|
|
1024 |
|
|
1025 |
Goal "!!(q1::preal). q1 <= q2 ==> q1 * x <= q2 * x";
|
|
1026 |
by (auto_tac (claset() addDs [preal_mult_left_le_mono1],
|
|
1027 |
simpset() addsimps [preal_mult_commute]));
|
|
1028 |
qed "preal_mult_le_mono1";
|
|
1029 |
|
|
1030 |
Goal "!!(q1::preal). q1 <= q2 ==> x + q1 <= x + q2";
|
|
1031 |
by (dtac preal_le_imp_less_or_eq 1);
|
|
1032 |
by (Step_tac 1);
|
|
1033 |
by (auto_tac (claset() addSIs [preal_le_refl,
|
|
1034 |
preal_less_imp_le,preal_add_less2_mono1],
|
|
1035 |
simpset() addsimps [preal_add_commute]));
|
|
1036 |
qed "preal_add_left_le_mono1";
|
|
1037 |
|
|
1038 |
Goal "!!(q1::preal). q1 <= q2 ==> q1 + x <= q2 + x";
|
|
1039 |
by (auto_tac (claset() addDs [preal_add_left_le_mono1],
|
|
1040 |
simpset() addsimps [preal_add_commute]));
|
|
1041 |
qed "preal_add_le_mono1";
|
|
1042 |
|
|
1043 |
Goal "!!k l::preal. [|i<=j; k<=l |] ==> i + k <= j + l";
|
|
1044 |
by (etac (preal_add_le_mono1 RS preal_le_trans) 1);
|
|
1045 |
by (simp_tac (simpset() addsimps [preal_add_commute]) 1);
|
|
1046 |
(*j moves to the end because it is free while k, l are bound*)
|
|
1047 |
by (etac preal_add_le_mono1 1);
|
|
1048 |
qed "preal_add_le_mono";
|
|
1049 |
|
|
1050 |
Goal "!!(A::preal). A + C < B + C ==> A < B";
|
|
1051 |
by (cut_facts_tac [preal_linear] 1);
|
|
1052 |
by (auto_tac (claset() addEs [preal_less_irrefl],simpset()));
|
|
1053 |
by (dres_inst_tac [("A","B"),("C","C")] preal_add_less2_mono1 1);
|
|
1054 |
by (fast_tac (claset() addDs [preal_less_trans]
|
|
1055 |
addEs [preal_less_irrefl]) 1);
|
|
1056 |
qed "preal_add_right_less_cancel";
|
|
1057 |
|
|
1058 |
Goal "!!(A::preal). C + A < C + B ==> A < B";
|
|
1059 |
by (auto_tac (claset() addEs [preal_add_right_less_cancel],
|
|
1060 |
simpset() addsimps [preal_add_commute]));
|
|
1061 |
qed "preal_add_left_less_cancel";
|
|
1062 |
|
|
1063 |
Goal "((A::preal) + C < B + C) = (A < B)";
|
|
1064 |
by (REPEAT(ares_tac [iffI,preal_add_less2_mono1,
|
|
1065 |
preal_add_right_less_cancel] 1));
|
|
1066 |
qed "preal_add_less_iff1";
|
|
1067 |
|
|
1068 |
Addsimps [preal_add_less_iff1];
|
|
1069 |
|
|
1070 |
Goal "(C + (A::preal) < C + B) = (A < B)";
|
|
1071 |
by (REPEAT(ares_tac [iffI,preal_add_less2_mono2,
|
|
1072 |
preal_add_left_less_cancel] 1));
|
|
1073 |
qed "preal_add_less_iff2";
|
|
1074 |
|
|
1075 |
Addsimps [preal_add_less_iff2];
|
|
1076 |
|
|
1077 |
Goal
|
|
1078 |
"!!x1. [| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)";
|
|
1079 |
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
|
|
1080 |
simpset() addsimps preal_add_ac));
|
|
1081 |
by (rtac (preal_add_assoc RS subst) 1);
|
|
1082 |
by (rtac preal_self_less_add_right 1);
|
|
1083 |
qed "preal_add_less_mono";
|
|
1084 |
|
|
1085 |
Goal
|
|
1086 |
"!!x1. [| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)";
|
|
1087 |
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
|
|
1088 |
simpset() addsimps [preal_add_mult_distrib,
|
|
1089 |
preal_add_mult_distrib2,preal_self_less_add_left,
|
|
1090 |
preal_add_assoc] @ preal_mult_ac));
|
|
1091 |
qed "preal_mult_less_mono";
|
|
1092 |
|
|
1093 |
Goal "!!(A::preal). A + C = B + C ==> A = B";
|
|
1094 |
by (cut_facts_tac [preal_linear] 1);
|
|
1095 |
by Auto_tac;
|
|
1096 |
by (ALLGOALS(dres_inst_tac [("C","C")] preal_add_less2_mono1));
|
|
1097 |
by (auto_tac (claset() addEs [preal_less_irrefl],simpset()));
|
|
1098 |
qed "preal_add_right_cancel";
|
|
1099 |
|
|
1100 |
Goal "!!(A::preal). C + A = C + B ==> A = B";
|
|
1101 |
by (auto_tac (claset() addIs [preal_add_right_cancel],
|
|
1102 |
simpset() addsimps [preal_add_commute]));
|
|
1103 |
qed "preal_add_left_cancel";
|
|
1104 |
|
|
1105 |
Goal "(C + A = C + B) = ((A::preal) = B)";
|
|
1106 |
by (fast_tac (claset() addIs [preal_add_left_cancel]) 1);
|
|
1107 |
qed "preal_add_left_cancel_iff";
|
|
1108 |
|
|
1109 |
Goal "(A + C = B + C) = ((A::preal) = B)";
|
|
1110 |
by (fast_tac (claset() addIs [preal_add_right_cancel]) 1);
|
|
1111 |
qed "preal_add_right_cancel_iff";
|
|
1112 |
|
|
1113 |
Addsimps [preal_add_left_cancel_iff,preal_add_right_cancel_iff];
|
|
1114 |
|
|
1115 |
(*** Completeness of preal ***)
|
|
1116 |
|
|
1117 |
(*** prove that supremum is a cut ***)
|
|
1118 |
Goal "!!P. ? (X::preal). X: P ==> \
|
|
1119 |
\ ? q. q: {w. ? X. X : P & w : Rep_preal X}";
|
|
1120 |
by Safe_tac;
|
|
1121 |
by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
|
|
1122 |
by Auto_tac;
|
|
1123 |
qed "preal_sup_mem_Ex";
|
|
1124 |
|
|
1125 |
(** Part 1 of Dedekind def **)
|
|
1126 |
Goal "!!P. ? (X::preal). X: P ==> \
|
|
1127 |
\ {} < {w. ? X : P. w : Rep_preal X}";
|
|
1128 |
by (dtac preal_sup_mem_Ex 1);
|
|
1129 |
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
|
|
1130 |
qed "preal_sup_set_not_empty";
|
|
1131 |
|
|
1132 |
(** Part 2 of Dedekind sections def **)
|
|
1133 |
Goalw [preal_less_def] "!!P. ? Y. (! X: P. X < Y) \
|
|
1134 |
\ ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}"; (**)
|
|
1135 |
by (auto_tac (claset(),simpset() addsimps [psubset_def]));
|
|
1136 |
by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
|
|
1137 |
by (etac exE 1);
|
|
1138 |
by (res_inst_tac [("x","x")] exI 1);
|
|
1139 |
by (auto_tac (claset() addSDs [bspec],simpset()));
|
|
1140 |
qed "preal_sup_not_mem_Ex";
|
|
1141 |
|
|
1142 |
Goalw [preal_le_def] "!!P. ? Y. (! X: P. X <= Y) \
|
|
1143 |
\ ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}";
|
|
1144 |
by (Step_tac 1);
|
|
1145 |
by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
|
|
1146 |
by (etac exE 1);
|
|
1147 |
by (res_inst_tac [("x","x")] exI 1);
|
|
1148 |
by (auto_tac (claset() addSDs [bspec],simpset()));
|
|
1149 |
qed "preal_sup_not_mem_Ex1";
|
|
1150 |
|
|
1151 |
Goal "!!P. ? Y. (! X: P. X < Y) \
|
|
1152 |
\ ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}"; (**)
|
|
1153 |
by (dtac preal_sup_not_mem_Ex 1);
|
|
1154 |
by (auto_tac (claset() addSIs [psubsetI],simpset()));
|
|
1155 |
by (eres_inst_tac [("c","q")] equalityCE 1);
|
|
1156 |
by Auto_tac;
|
|
1157 |
qed "preal_sup_set_not_prat_set";
|
|
1158 |
|
|
1159 |
Goal "!!P. ? Y. (! X: P. X <= Y) \
|
|
1160 |
\ ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";
|
|
1161 |
by (dtac preal_sup_not_mem_Ex1 1);
|
|
1162 |
by (auto_tac (claset() addSIs [psubsetI],simpset()));
|
|
1163 |
by (eres_inst_tac [("c","q")] equalityCE 1);
|
|
1164 |
by Auto_tac;
|
|
1165 |
qed "preal_sup_set_not_prat_set1";
|
|
1166 |
|
|
1167 |
(** Part 3 of Dedekind sections def **)
|
|
1168 |
Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
|
|
1169 |
\ ==> ! y: {w. ? X: P. w: Rep_preal X}. \
|
|
1170 |
\ !z. z < y --> z: {w. ? X: P. w: Rep_preal X}"; (**)
|
|
1171 |
by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
|
|
1172 |
qed "preal_sup_set_lemma3";
|
|
1173 |
|
|
1174 |
Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
|
|
1175 |
\ ==> ! y: {w. ? X: P. w: Rep_preal X}. \
|
|
1176 |
\ !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";
|
|
1177 |
by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
|
|
1178 |
qed "preal_sup_set_lemma3_1";
|
|
1179 |
|
|
1180 |
Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
|
|
1181 |
\ ==> !y: {w. ? X: P. w: Rep_preal X}. \
|
|
1182 |
\ Bex {w. ? X: P. w: Rep_preal X} (op < y)"; (**)
|
|
1183 |
by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
|
|
1184 |
qed "preal_sup_set_lemma4";
|
|
1185 |
|
|
1186 |
Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
|
|
1187 |
\ ==> !y: {w. ? X: P. w: Rep_preal X}. \
|
|
1188 |
\ Bex {w. ? X: P. w: Rep_preal X} (op < y)";
|
|
1189 |
by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
|
|
1190 |
qed "preal_sup_set_lemma4_1";
|
|
1191 |
|
|
1192 |
Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
|
|
1193 |
\ ==> {w. ? X: P. w: Rep_preal(X)}: preal"; (**)
|
|
1194 |
by (rtac prealI2 1);
|
|
1195 |
by (rtac preal_sup_set_not_empty 1);
|
|
1196 |
by (rtac preal_sup_set_not_prat_set 2);
|
|
1197 |
by (rtac preal_sup_set_lemma3 3);
|
|
1198 |
by (rtac preal_sup_set_lemma4 5);
|
|
1199 |
by Auto_tac;
|
|
1200 |
qed "preal_sup";
|
|
1201 |
|
|
1202 |
Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
|
|
1203 |
\ ==> {w. ? X: P. w: Rep_preal(X)}: preal";
|
|
1204 |
by (rtac prealI2 1);
|
|
1205 |
by (rtac preal_sup_set_not_empty 1);
|
|
1206 |
by (rtac preal_sup_set_not_prat_set1 2);
|
|
1207 |
by (rtac preal_sup_set_lemma3_1 3);
|
|
1208 |
by (rtac preal_sup_set_lemma4_1 5);
|
|
1209 |
by Auto_tac;
|
|
1210 |
qed "preal_sup1";
|
|
1211 |
|
|
1212 |
Goalw [psup_def] "!!P. ? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P"; (**)
|
|
1213 |
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
|
|
1214 |
by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
|
|
1215 |
by Auto_tac;
|
|
1216 |
qed "preal_psup_leI";
|
|
1217 |
|
|
1218 |
Goalw [psup_def] "!!P. ? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
|
|
1219 |
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
|
|
1220 |
by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
|
|
1221 |
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
|
|
1222 |
qed "preal_psup_leI2";
|
|
1223 |
|
|
1224 |
Goal "!!P. [| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P"; (**)
|
|
1225 |
by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
|
|
1226 |
qed "preal_psup_leI2b";
|
|
1227 |
|
|
1228 |
Goal "!!P. [| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
|
|
1229 |
by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
|
|
1230 |
qed "preal_psup_leI2a";
|
|
1231 |
|
|
1232 |
Goalw [psup_def] "!!P. [| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y"; (**)
|
|
1233 |
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
|
|
1234 |
by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
|
|
1235 |
by (rotate_tac 1 2);
|
|
1236 |
by (assume_tac 2);
|
|
1237 |
by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
|
|
1238 |
qed "psup_le_ub";
|
|
1239 |
|
|
1240 |
Goalw [psup_def] "!!P. [| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
|
|
1241 |
by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
|
|
1242 |
by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
|
|
1243 |
by (rotate_tac 1 2);
|
|
1244 |
by (assume_tac 2);
|
|
1245 |
by (auto_tac (claset() addSDs [bspec],
|
|
1246 |
simpset() addsimps [preal_less_def,psubset_def,preal_le_def]));
|
|
1247 |
qed "psup_le_ub1";
|
|
1248 |
|
|
1249 |
(** supremum property **)
|
|
1250 |
Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \
|
|
1251 |
\ ==> (!Y. (? X: P. Y < X) = (Y < psup P))";
|
|
1252 |
by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
|
|
1253 |
by (Fast_tac 1);
|
|
1254 |
by (auto_tac (claset() addSIs [psubsetI],simpset() addsimps [psup_def,preal_less_def]));
|
|
1255 |
by (blast_tac (claset() addDs [psubset_def RS meta_eq_to_obj_eq RS iffD1]) 1);
|
|
1256 |
by (rotate_tac 4 1);
|
|
1257 |
by (asm_full_simp_tac (simpset() addsimps [psubset_def]) 1);
|
|
1258 |
by (dtac bspec 1 THEN assume_tac 1);
|
|
1259 |
by (REPEAT(etac conjE 1));
|
|
1260 |
by (EVERY1[rtac swap, assume_tac, rtac set_ext]);
|
|
1261 |
by (auto_tac (claset() addSDs [lemma_psubset_mem],simpset()));
|
|
1262 |
by (cut_inst_tac [("r1.0","Xa"),("r2.0","Ya")] preal_linear 1);
|
|
1263 |
by (auto_tac (claset() addDs [psubsetD],simpset() addsimps [preal_less_def]));
|
|
1264 |
qed "preal_complete";
|
|
1265 |
|
|
1266 |
(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
|
|
1267 |
(****** Embedding ******)
|
|
1268 |
(*** mapping from prat into preal ***)
|
|
1269 |
|
|
1270 |
Goal "!!z1. x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
|
|
1271 |
by (dres_inst_tac [("x","z1 * qinv (z1 + z2)")] prat_mult_less2_mono1 1);
|
|
1272 |
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
|
|
1273 |
qed "lemma_preal_rat_less";
|
|
1274 |
|
|
1275 |
Goal "!!z1. x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
|
|
1276 |
by (stac prat_add_commute 1);
|
|
1277 |
by (dtac (prat_add_commute RS subst) 1);
|
|
1278 |
by (etac lemma_preal_rat_less 1);
|
|
1279 |
qed "lemma_preal_rat_less2";
|
|
1280 |
|
|
1281 |
Goalw [preal_prat_def,preal_add_def]
|
|
1282 |
"@#((z1::prat) + z2) = @#z1 + @#z2";
|
|
1283 |
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
|
|
1284 |
by (auto_tac (claset() addIs [prat_add_less_mono] addSIs [set_ext],simpset() addsimps
|
|
1285 |
[lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
|
|
1286 |
by (res_inst_tac [("x","x*z1*qinv(z1+z2)")] exI 1 THEN rtac conjI 1);
|
|
1287 |
by (etac lemma_preal_rat_less 1);
|
|
1288 |
by (res_inst_tac [("x","x*z2*qinv(z1+z2)")] exI 1 THEN rtac conjI 1);
|
|
1289 |
by (etac lemma_preal_rat_less2 1);
|
|
1290 |
by (asm_full_simp_tac (simpset() addsimps [prat_add_mult_distrib RS sym,
|
|
1291 |
prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1);
|
|
1292 |
qed "preal_prat_add";
|
|
1293 |
|
|
1294 |
Goal "!!xa. x < xa ==> x*z1*qinv(xa) < z1";
|
|
1295 |
by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1);
|
|
1296 |
by (dtac (prat_mult_left_commute RS subst) 1);
|
|
1297 |
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
|
|
1298 |
qed "lemma_preal_rat_less3";
|
|
1299 |
|
|
1300 |
Goal "!!xa. xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
|
|
1301 |
by (dres_inst_tac [("x","z2 * qinv(z1*z2)")] prat_mult_less2_mono1 1);
|
|
1302 |
by (dtac (prat_mult_left_commute RS subst) 1);
|
|
1303 |
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
|
|
1304 |
qed "lemma_preal_rat_less4";
|
|
1305 |
|
|
1306 |
Goalw [preal_prat_def,preal_mult_def]
|
|
1307 |
"@#((z1::prat) * z2) = @#z1 * @#z2";
|
|
1308 |
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
|
|
1309 |
by (auto_tac (claset() addIs [prat_mult_less_mono] addSIs [set_ext],simpset() addsimps
|
|
1310 |
[lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
|
|
1311 |
by (dtac prat_dense 1);
|
|
1312 |
by (Step_tac 1);
|
|
1313 |
by (res_inst_tac [("x","x*z1*qinv(xa)")] exI 1 THEN rtac conjI 1);
|
|
1314 |
by (etac lemma_preal_rat_less3 1);
|
|
1315 |
by (res_inst_tac [("x"," xa*z2*qinv(z1*z2)")] exI 1 THEN rtac conjI 1);
|
|
1316 |
by (etac lemma_preal_rat_less4 1);
|
|
1317 |
by (asm_full_simp_tac (simpset()
|
|
1318 |
addsimps [qinv_mult_eq RS sym] @ prat_mult_ac) 1);
|
|
1319 |
by (asm_full_simp_tac (simpset()
|
|
1320 |
addsimps [prat_mult_assoc RS sym]) 1);
|
|
1321 |
qed "preal_prat_mult";
|
|
1322 |
|
|
1323 |
Goalw [preal_prat_def,preal_less_def]
|
|
1324 |
"(@#p < @#q) = (p < q)";
|
|
1325 |
by (auto_tac (claset() addSDs [lemma_prat_set_eq] addEs [prat_less_trans],
|
|
1326 |
simpset() addsimps [lemma_prat_less_set_mem_preal,
|
|
1327 |
psubset_def,prat_less_not_refl]));
|
|
1328 |
by (res_inst_tac [("q1.0","p"),("q2.0","q")] prat_linear_less2 1);
|
|
1329 |
by (auto_tac (claset() addIs [prat_less_irrefl],simpset()));
|
|
1330 |
qed "preal_prat_less_iff";
|
|
1331 |
|
|
1332 |
Addsimps [preal_prat_less_iff];
|