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