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 [Gleason- p. 121]
7 provides some of the definitions.
10 theory PReal = Rational:
12 text{*Could be generalized and moved to @{text Ring_and_Field}*}
13 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"
14 by (rule_tac x="b-a" in exI, simp)
16 text{*As a special case, the sum of two positives is positive. One of the
17 premises could be weakened to the relation @{text "\<le>"}.*}
18 lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semidom)"
19 by (insert add_strict_mono [of 0 a b c], simp)
21 lemma interval_empty_iff:
22 "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))"
23 by (blast dest: dense intro: order_less_trans)
27 cut :: "rat set => bool"
28 "cut A == {} \<subset> A &
30 (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u)))"
34 assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}"
36 let ?A = "{r::rat. 0 < r & r < q}"
37 from q have pos: "?A < {r. 0 < r}" by force
38 have nonempty: "{} \<subset> ?A"
40 show "{} \<subseteq> ?A" by simp
42 by (force simp only: q eq_commute [of "{}"] interval_empty_iff)
45 by (simp add: cut_def pos nonempty,
46 blast dest: dense intro: order_less_trans)
50 typedef preal = "{A. cut A}"
51 by (blast intro: cut_of_rat [OF zero_less_one])
53 instance preal :: "{ord, plus, minus, times, inverse}" ..
56 preal_of_rat :: "rat => preal"
57 "preal_of_rat q == Abs_preal({x::rat. 0 < x & x < q})"
59 psup :: "preal set => preal"
60 "psup(P) == Abs_preal(\<Union>X \<in> P. Rep_preal(X))"
62 add_set :: "[rat set,rat set] => rat set"
63 "add_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
65 diff_set :: "[rat set,rat set] => rat set"
66 "diff_set A B == {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
68 mult_set :: "[rat set,rat set] => rat set"
69 "mult_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
71 inverse_set :: "rat set => rat set"
72 "inverse_set A == {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
78 "R < (S::preal) == Rep_preal R < Rep_preal S"
81 "R \<le> (S::preal) == Rep_preal R \<subseteq> Rep_preal S"
84 "R + S == Abs_preal (add_set (Rep_preal R) (Rep_preal S))"
87 "R - S == Abs_preal (diff_set (Rep_preal R) (Rep_preal S))"
90 "R * S == Abs_preal(mult_set (Rep_preal R) (Rep_preal S))"
93 "inverse R == Abs_preal(inverse_set (Rep_preal R))"
96 lemma inj_on_Abs_preal: "inj_on Abs_preal preal"
97 apply (rule inj_on_inverseI)
98 apply (erule Abs_preal_inverse)
101 declare inj_on_Abs_preal [THEN inj_on_iff, simp]
103 lemma inj_Rep_preal: "inj(Rep_preal)"
104 apply (rule inj_on_inverseI)
105 apply (rule Rep_preal_inverse)
108 lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
109 by (unfold preal_def cut_def, blast)
111 lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
112 by (force simp add: preal_def cut_def)
114 lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
115 by (drule preal_imp_psubset_positives, auto)
117 lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
118 by (unfold preal_def cut_def, blast)
120 lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X"
121 apply (insert Rep_preal [of X])
122 apply (unfold preal_def cut_def, blast)
125 declare Abs_preal_inverse [simp]
127 lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
128 by (unfold preal_def cut_def, blast)
130 text{*Relaxing the final premise*}
131 lemma preal_downwards_closed':
132 "[| A \<in> preal; y \<in> A; 0 < z; z \<le> y |] ==> z \<in> A"
133 apply (simp add: order_le_less)
134 apply (blast intro: preal_downwards_closed)
137 lemma Rep_preal_exists_bound: "\<exists>x. 0 < x & x \<notin> Rep_preal X"
138 apply (cut_tac x = X in Rep_preal)
139 apply (drule preal_imp_psubset_positives)
140 apply (auto simp add: psubset_def)
144 subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
146 lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal"
147 apply (auto simp add: preal_def cut_def intro: order_less_trans)
148 apply (force simp only: eq_commute [of "{}"] interval_empty_iff)
149 apply (blast dest: dense intro: order_less_trans)
152 lemma rat_subset_imp_le:
153 "[|{u::rat. 0 < u & u < x} \<subseteq> {u. 0 < u & u < y}; 0<x|] ==> x \<le> y"
154 apply (simp add: linorder_not_less [symmetric])
155 apply (blast dest: dense intro: order_less_trans)
158 lemma rat_set_eq_imp_eq:
159 "[|{u::rat. 0 < u & u < x} = {u. 0 < u & u < y};
160 0 < x; 0 < y|] ==> x = y"
161 by (blast intro: rat_subset_imp_le order_antisym)
165 subsection{*Theorems for Ordering*}
167 text{*A positive fraction not in a positive real is an upper bound.
168 Gleason p. 122 - Remark (1)*}
170 lemma not_in_preal_ub:
171 assumes A: "A \<in> preal"
172 and notx: "x \<notin> A"
176 proof (cases rule: linorder_cases)
178 with notx show ?thesis
179 by (simp add: preal_downwards_closed [OF A y] pos)
182 with notx and y show ?thesis by simp
185 thus ?thesis by assumption
188 lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal]
191 subsection{*The @{text "\<le>"} Ordering*}
193 lemma preal_le_refl: "w \<le> (w::preal)"
194 by (simp add: preal_le_def)
196 lemma preal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::preal)"
197 by (force simp add: preal_le_def)
199 lemma preal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::preal)"
200 apply (simp add: preal_le_def)
201 apply (rule Rep_preal_inject [THEN iffD1], blast)
204 (* Axiom 'order_less_le' of class 'order': *)
205 lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
206 by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def)
208 instance preal :: order
211 rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
213 lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
214 by (insert preal_imp_psubset_positives, blast)
216 lemma preal_le_linear: "x <= y | y <= (x::preal)"
217 apply (auto simp add: preal_le_def)
219 apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
220 elim: order_less_asym)
223 instance preal :: linorder
224 by intro_classes (rule preal_le_linear)
228 subsection{*Properties of Addition*}
230 lemma preal_add_commute: "(x::preal) + y = y + x"
231 apply (unfold preal_add_def add_set_def)
232 apply (rule_tac f = Abs_preal in arg_cong)
233 apply (force simp add: add_commute)
236 text{*Lemmas for proving that addition of two positive reals gives
239 lemma empty_psubset_nonempty: "a \<in> A ==> {} \<subset> A"
242 text{*Part 1 of Dedekind sections definition*}
243 lemma add_set_not_empty:
244 "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> add_set A B"
245 apply (insert preal_nonempty [of A] preal_nonempty [of B])
246 apply (auto simp add: add_set_def)
249 text{*Part 2 of Dedekind sections definition. A structured version of
250 this proof is @{text preal_not_mem_mult_set_Ex} below.*}
251 lemma preal_not_mem_add_set_Ex:
252 "[|A \<in> preal; B \<in> preal|] ==> \<exists>q. 0 < q & q \<notin> add_set A B"
253 apply (insert preal_exists_bound [of A] preal_exists_bound [of B], auto)
254 apply (rule_tac x = "x+xa" in exI)
255 apply (simp add: add_set_def, clarify)
256 apply (drule not_in_preal_ub, assumption+)+
257 apply (force dest: add_strict_mono)
260 lemma add_set_not_rat_set:
261 assumes A: "A \<in> preal"
262 and B: "B \<in> preal"
263 shows "add_set A B < {r. 0 < r}"
265 from preal_imp_pos [OF A] preal_imp_pos [OF B]
266 show "add_set A B \<subseteq> {r. 0 < r}" by (force simp add: add_set_def)
268 show "add_set A B \<noteq> {r. 0 < r}"
269 by (insert preal_not_mem_add_set_Ex [OF A B], blast)
272 text{*Part 3 of Dedekind sections definition*}
273 lemma add_set_lemma3:
274 "[|A \<in> preal; B \<in> preal; u \<in> add_set A B; 0 < z; z < u|]
275 ==> z \<in> add_set A B"
276 proof (unfold add_set_def, clarify)
277 fix x::rat and y::rat
278 assume A: "A \<in> preal"
279 and B: "B \<in> preal"
281 and zless: "z < x + y"
284 have xpos [simp]: "0<x" by (rule preal_imp_pos [OF A x])
285 have ypos [simp]: "0<y" by (rule preal_imp_pos [OF B y])
286 have xypos [simp]: "0 < x+y" by (simp add: pos_add_strict)
288 have fless: "?f < 1" by (simp add: zless pos_divide_less_eq)
289 show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
291 show "\<exists>y' \<in> B. z = x*?f + y'"
293 show "z = x*?f + y*?f"
294 by (simp add: left_distrib [symmetric] divide_inverse mult_ac
295 order_less_imp_not_eq2)
297 show "y * ?f \<in> B"
298 proof (rule preal_downwards_closed [OF B y])
300 by (simp add: divide_inverse zero_less_mult_iff)
303 by (insert mult_strict_left_mono [OF fless ypos], simp)
307 show "x * ?f \<in> A"
308 proof (rule preal_downwards_closed [OF A x])
310 by (simp add: divide_inverse zero_less_mult_iff)
313 by (insert mult_strict_left_mono [OF fless xpos], simp)
318 text{*Part 4 of Dedekind sections definition*}
319 lemma add_set_lemma4:
320 "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
321 apply (auto simp add: add_set_def)
322 apply (frule preal_exists_greater [of A], auto)
323 apply (rule_tac x="u + y" in exI)
324 apply (auto intro: add_strict_left_mono)
328 "[|A \<in> preal; B \<in> preal|] ==> add_set A B \<in> preal"
329 apply (simp (no_asm_simp) add: preal_def cut_def)
330 apply (blast intro!: add_set_not_empty add_set_not_rat_set
331 add_set_lemma3 add_set_lemma4)
334 lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
335 apply (simp add: preal_add_def mem_add_set Rep_preal)
336 apply (force simp add: add_set_def add_ac)
339 lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
340 apply (rule mk_left_commute [of "op +"])
341 apply (rule preal_add_assoc)
342 apply (rule preal_add_commute)
345 text{* Positive Real addition is an AC operator *}
346 lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
349 subsection{*Properties of Multiplication*}
351 text{*Proofs essentially same as for addition*}
353 lemma preal_mult_commute: "(x::preal) * y = y * x"
354 apply (unfold preal_mult_def mult_set_def)
355 apply (rule_tac f = Abs_preal in arg_cong)
356 apply (force simp add: mult_commute)
359 text{*Multiplication of two positive reals gives a positive real.}
361 text{*Lemmas for proving positive reals multiplication set in @{typ preal}*}
363 text{*Part 1 of Dedekind sections definition*}
364 lemma mult_set_not_empty:
365 "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> mult_set A B"
366 apply (insert preal_nonempty [of A] preal_nonempty [of B])
367 apply (auto simp add: mult_set_def)
370 text{*Part 2 of Dedekind sections definition*}
371 lemma preal_not_mem_mult_set_Ex:
372 assumes A: "A \<in> preal"
373 and B: "B \<in> preal"
374 shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
376 from preal_exists_bound [OF A]
377 obtain x where [simp]: "0 < x" "x \<notin> A" by blast
378 from preal_exists_bound [OF B]
379 obtain y where [simp]: "0 < y" "y \<notin> B" by blast
381 proof (intro exI conjI)
382 show "0 < x*y" by (simp add: mult_pos)
383 show "x * y \<notin> mult_set A B"
385 { fix u::rat and v::rat
386 assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
388 with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
390 with prems have "0\<le>v"
391 by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems)
394 have "u*v < x*y" by (blast intro: mult_strict_mono prems)
395 ultimately have False by force }
396 thus ?thesis by (auto simp add: mult_set_def)
401 lemma mult_set_not_rat_set:
402 assumes A: "A \<in> preal"
403 and B: "B \<in> preal"
404 shows "mult_set A B < {r. 0 < r}"
406 show "mult_set A B \<subseteq> {r. 0 < r}"
407 by (force simp add: mult_set_def
408 intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos)
410 show "mult_set A B \<noteq> {r. 0 < r}"
411 by (insert preal_not_mem_mult_set_Ex [OF A B], blast)
416 text{*Part 3 of Dedekind sections definition*}
417 lemma mult_set_lemma3:
418 "[|A \<in> preal; B \<in> preal; u \<in> mult_set A B; 0 < z; z < u|]
419 ==> z \<in> mult_set A B"
420 proof (unfold mult_set_def, clarify)
421 fix x::rat and y::rat
422 assume A: "A \<in> preal"
423 and B: "B \<in> preal"
425 and zless: "z < x * y"
428 have [simp]: "0<y" by (rule preal_imp_pos [OF B y])
429 show "\<exists>x' \<in> A. \<exists>y' \<in> B. z = x' * y'"
431 show "\<exists>y'\<in>B. z = (z/y) * y'"
434 by (simp add: divide_inverse mult_commute [of y] mult_assoc
435 order_less_imp_not_eq2)
440 proof (rule preal_downwards_closed [OF A x])
442 by (simp add: zero_less_divide_iff)
443 show "z/y < x" by (simp add: pos_divide_less_eq zless)
448 text{*Part 4 of Dedekind sections definition*}
449 lemma mult_set_lemma4:
450 "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
451 apply (auto simp add: mult_set_def)
452 apply (frule preal_exists_greater [of A], auto)
453 apply (rule_tac x="u * y" in exI)
454 apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B]
455 mult_strict_right_mono)
460 "[|A \<in> preal; B \<in> preal|] ==> mult_set A B \<in> preal"
461 apply (simp (no_asm_simp) add: preal_def cut_def)
462 apply (blast intro!: mult_set_not_empty mult_set_not_rat_set
463 mult_set_lemma3 mult_set_lemma4)
466 lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
467 apply (simp add: preal_mult_def mem_mult_set Rep_preal)
468 apply (force simp add: mult_set_def mult_ac)
471 lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
472 apply (rule mk_left_commute [of "op *"])
473 apply (rule preal_mult_assoc)
474 apply (rule preal_mult_commute)
478 text{* Positive Real multiplication is an AC operator *}
479 lemmas preal_mult_ac =
480 preal_mult_assoc preal_mult_commute preal_mult_left_commute
483 text{* Positive real 1 is the multiplicative identity element *}
485 lemma rat_mem_preal: "0 < q ==> {r::rat. 0 < r & r < q} \<in> preal"
486 by (simp add: preal_def cut_of_rat)
488 lemma preal_mult_1: "(preal_of_rat 1) * z = z"
491 assume A: "A \<in> preal"
492 have "{w. \<exists>u. 0 < u \<and> u < 1 & (\<exists>v \<in> A. w = u * v)} = A" (is "?lhs = A")
494 show "?lhs \<subseteq> A"
496 fix x::rat and u::rat and v::rat
497 assume upos: "0<u" and "u<1" and v: "v \<in> A"
498 have vpos: "0<v" by (rule preal_imp_pos [OF A v])
499 hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
501 by (force intro: preal_downwards_closed [OF A v] mult_pos upos vpos)
504 show "A \<subseteq> ?lhs"
507 assume x: "x \<in> A"
508 have xpos: "0<x" by (rule preal_imp_pos [OF A x])
509 from preal_exists_greater [OF A x]
510 obtain v where v: "v \<in> A" and xlessv: "x < v" ..
511 have vpos: "0<v" by (rule preal_imp_pos [OF A v])
512 show "\<exists>u. 0 < u \<and> u < 1 \<and> (\<exists>v\<in>A. x = u * v)"
513 proof (intro exI conjI)
515 by (simp add: zero_less_divide_iff xpos vpos)
517 by (simp add: pos_divide_less_eq vpos xlessv)
518 show "\<exists>v'\<in>A. x = (x / v) * v'"
521 by (simp add: divide_inverse mult_assoc vpos
522 order_less_imp_not_eq2)
528 thus "preal_of_rat 1 * Abs_preal A = Abs_preal A"
529 by (simp add: preal_of_rat_def preal_mult_def mult_set_def
534 lemma preal_mult_1_right: "z * (preal_of_rat 1) = z"
535 apply (rule preal_mult_commute [THEN subst])
536 apply (rule preal_mult_1)
540 subsection{*Distribution of Multiplication across Addition*}
542 lemma mem_Rep_preal_add_iff:
543 "(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x + y)"
544 apply (simp add: preal_add_def mem_add_set Rep_preal)
545 apply (simp add: add_set_def)
548 lemma mem_Rep_preal_mult_iff:
549 "(z \<in> Rep_preal(R*S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x * y)"
550 apply (simp add: preal_mult_def mem_mult_set Rep_preal)
551 apply (simp add: mult_set_def)
554 lemma distrib_subset1:
555 "Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)"
556 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
557 apply (force simp add: right_distrib)
560 lemma linorder_le_cases [case_names le ge]:
561 "((x::'a::linorder) <= y ==> P) ==> (y <= x ==> P) ==> P"
562 apply (insert linorder_linear, blast)
565 lemma preal_add_mult_distrib_mean:
566 assumes a: "a \<in> Rep_preal w"
567 and b: "b \<in> Rep_preal w"
568 and d: "d \<in> Rep_preal x"
569 and e: "e \<in> Rep_preal y"
570 shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
572 let ?c = "(a*d + b*e)/(d+e)"
573 have [simp]: "0<a" "0<b" "0<d" "0<e" "0<d+e"
574 by (blast intro: preal_imp_pos [OF Rep_preal] a b d e pos_add_strict)+
576 by (simp add: zero_less_divide_iff zero_less_mult_iff pos_add_strict)
577 show "a * d + b * e = ?c * (d + e)"
578 by (simp add: divide_inverse mult_assoc order_less_imp_not_eq2)
579 show "?c \<in> Rep_preal w"
580 proof (cases rule: linorder_le_cases)
583 by (simp add: pos_divide_le_eq right_distrib mult_right_mono
585 thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos])
589 by (simp add: pos_divide_le_eq right_distrib mult_right_mono
591 thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos])
595 lemma distrib_subset2:
596 "Rep_preal (w * x + w * y) \<subseteq> Rep_preal (w * (x + y))"
597 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
598 apply (drule_tac w=w and x=x and y=y in preal_add_mult_distrib_mean, auto)
601 lemma preal_add_mult_distrib2: "(w * ((x::preal) + y)) = (w * x) + (w * y)"
602 apply (rule inj_Rep_preal [THEN injD])
603 apply (rule equalityI [OF distrib_subset1 distrib_subset2])
606 lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)"
607 by (simp add: preal_mult_commute preal_add_mult_distrib2)
610 subsection{*Existence of Inverse, a Positive Real*}
612 lemma mem_inv_set_ex:
613 assumes A: "A \<in> preal" shows "\<exists>x y. 0 < x & x < y & inverse y \<notin> A"
615 from preal_exists_bound [OF A]
616 obtain x where [simp]: "0<x" "x \<notin> A" by blast
618 proof (intro exI conjI)
619 show "0 < inverse (x+1)"
620 by (simp add: order_less_trans [OF _ less_add_one])
621 show "inverse(x+1) < inverse x"
622 by (simp add: less_imp_inverse_less less_add_one)
623 show "inverse (inverse x) \<notin> A"
624 by (simp add: order_less_imp_not_eq2)
628 text{*Part 1 of Dedekind sections definition*}
629 lemma inverse_set_not_empty:
630 "A \<in> preal ==> {} \<subset> inverse_set A"
631 apply (insert mem_inv_set_ex [of A])
632 apply (auto simp add: inverse_set_def)
635 text{*Part 2 of Dedekind sections definition*}
637 lemma preal_not_mem_inverse_set_Ex:
638 assumes A: "A \<in> preal" shows "\<exists>q. 0 < q & q \<notin> inverse_set A"
640 from preal_nonempty [OF A]
641 obtain x where x: "x \<in> A" and xpos [simp]: "0<x" ..
643 proof (intro exI conjI)
644 show "0 < inverse x" by simp
645 show "inverse x \<notin> inverse_set A"
648 assume ygt: "inverse x < y"
649 have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
650 have iyless: "inverse y < x"
651 by (simp add: inverse_less_imp_less [of x] ygt)
652 have "inverse y \<in> A"
653 by (simp add: preal_downwards_closed [OF A x] iyless)}
654 thus ?thesis by (auto simp add: inverse_set_def)
659 lemma inverse_set_not_rat_set:
660 assumes A: "A \<in> preal" shows "inverse_set A < {r. 0 < r}"
662 show "inverse_set A \<subseteq> {r. 0 < r}" by (force simp add: inverse_set_def)
664 show "inverse_set A \<noteq> {r. 0 < r}"
665 by (insert preal_not_mem_inverse_set_Ex [OF A], blast)
668 text{*Part 3 of Dedekind sections definition*}
669 lemma inverse_set_lemma3:
670 "[|A \<in> preal; u \<in> inverse_set A; 0 < z; z < u|]
671 ==> z \<in> inverse_set A"
672 apply (auto simp add: inverse_set_def)
673 apply (auto intro: order_less_trans)
676 text{*Part 4 of Dedekind sections definition*}
677 lemma inverse_set_lemma4:
678 "[|A \<in> preal; y \<in> inverse_set A|] ==> \<exists>u \<in> inverse_set A. y < u"
679 apply (auto simp add: inverse_set_def)
680 apply (drule dense [of y])
681 apply (blast intro: order_less_trans)
685 lemma mem_inverse_set:
686 "A \<in> preal ==> inverse_set A \<in> preal"
687 apply (simp (no_asm_simp) add: preal_def cut_def)
688 apply (blast intro!: inverse_set_not_empty inverse_set_not_rat_set
689 inverse_set_lemma3 inverse_set_lemma4)
693 subsection{*Gleason's Lemma 9-3.4, page 122*}
695 lemma Gleason9_34_exists:
696 assumes A: "A \<in> preal"
697 and "\<forall>x\<in>A. x + u \<in> A"
699 shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
700 proof (cases z rule: int_cases)
703 proof (simp add: prems, induct n)
705 from preal_nonempty [OF A]
708 from this obtain b where "b \<in> A" "b + of_int (int k) * u \<in> A" ..
709 hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
710 thus ?case by (force simp add: left_distrib add_ac prems)
714 with prems show ?thesis by simp
717 lemma Gleason9_34_contra:
718 assumes A: "A \<in> preal"
719 shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
720 proof (induct u, induct y)
721 fix a::int and b::int
722 fix c::int and d::int
723 assume bpos [simp]: "0 < b"
724 and dpos [simp]: "0 < d"
725 and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
726 and upos: "0 < Fract c d"
727 and ypos: "0 < Fract a b"
728 and notin: "Fract a b \<notin> A"
729 have cpos [simp]: "0 < c"
730 by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos)
731 have apos [simp]: "0 < a"
732 by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos)
734 have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)"
736 have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
737 by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac)
739 have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
741 simp_all add: int_one_le_iff_zero_less zero_less_mult_iff
746 have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff)
747 from Gleason9_34_exists [OF A closed k]
748 obtain z where z: "z \<in> A"
749 and mem: "z + of_int ?k * Fract c d \<in> A" ..
750 have less: "z + of_int ?k * Fract c d < Fract a b"
751 by (rule not_in_preal_ub [OF A notin mem ypos])
752 have "0<z" by (rule preal_imp_pos [OF A z])
753 with frle and less show False by (simp add: Fract_of_int_eq)
758 assumes A: "A \<in> preal"
760 shows "\<exists>r \<in> A. r + u \<notin> A"
761 proof (rule ccontr, simp)
762 assume closed: "\<forall>r\<in>A. r + u \<in> A"
763 from preal_exists_bound [OF A]
764 obtain y where y: "y \<notin> A" and ypos: "0 < y" by blast
766 by (rule Gleason9_34_contra [OF A closed upos ypos y])
771 subsection{*Gleason's Lemma 9-3.6*}
773 lemma lemma_gleason9_36:
774 assumes A: "A \<in> preal"
776 shows "\<exists>r \<in> A. r*x \<notin> A"
778 from preal_nonempty [OF A]
779 obtain y where y: "y \<in> A" and ypos: "0<y" ..
781 proof (rule classical)
782 assume "~(\<exists>r\<in>A. r * x \<notin> A)"
783 with y have ymem: "y * x \<in> A" by blast
784 from ypos mult_strict_left_mono [OF x]
785 have yless: "y < y*x" by simp
787 from yless have dpos: "0 < ?d" and eq: "y + ?d = y*x" by auto
788 from Gleason9_34 [OF A dpos]
789 obtain r where r: "r\<in>A" and notin: "r + ?d \<notin> A" ..
790 have rpos: "0<r" by (rule preal_imp_pos [OF A r])
791 with dpos have rdpos: "0 < r + ?d" by arith
792 have "~ (r + ?d \<le> y + ?d)"
794 assume le: "r + ?d \<le> y + ?d"
795 from ymem have yd: "y + ?d \<in> A" by (simp add: eq)
796 have "r + ?d \<in> A" by (rule preal_downwards_closed' [OF A yd rdpos le])
797 with notin show False by simp
799 hence "y < r" by simp
800 with ypos have dless: "?d < (r * ?d)/y"
801 by (simp add: pos_less_divide_eq mult_commute [of ?d]
802 mult_strict_right_mono dpos)
805 have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
806 also with ypos have "... = (r/y) * (y + ?d)"
807 by (simp only: right_distrib divide_inverse mult_ac, simp)
808 also have "... = r*x" using ypos
810 finally show "r + ?d < r*x" .
813 show "\<exists>r\<in>A. r * x \<notin> A" by (blast dest: preal_downwards_closed [OF A])
817 subsection{*Existence of Inverse: Part 2*}
819 lemma mem_Rep_preal_inverse_iff:
820 "(z \<in> Rep_preal(inverse R)) =
821 (0 < z \<and> (\<exists>y. z < y \<and> inverse y \<notin> Rep_preal R))"
822 apply (simp add: preal_inverse_def mem_inverse_set Rep_preal)
823 apply (simp add: inverse_set_def)
826 lemma Rep_preal_of_rat:
827 "0 < q ==> Rep_preal (preal_of_rat q) = {x. 0 < x \<and> x < q}"
828 by (simp add: preal_of_rat_def rat_mem_preal)
830 lemma subset_inverse_mult_lemma:
831 assumes xpos: "0 < x" and xless: "x < 1"
832 shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R &
833 u \<in> Rep_preal R & x = r * u"
835 from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff)
836 from lemma_gleason9_36 [OF Rep_preal this]
837 obtain r where r: "r \<in> Rep_preal R"
838 and notin: "r * (inverse x) \<notin> Rep_preal R" ..
839 have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
840 from preal_exists_greater [OF Rep_preal r]
841 obtain u where u: "u \<in> Rep_preal R" and rless: "r < u" ..
842 have upos: "0<u" by (rule preal_imp_pos [OF Rep_preal u])
844 proof (intro exI conjI)
845 show "0 < x/u" using xpos upos
846 by (simp add: zero_less_divide_iff)
847 show "x/u < x/r" using xpos upos rpos
848 by (simp add: divide_inverse mult_less_cancel_left rless)
849 show "inverse (x / r) \<notin> Rep_preal R" using notin
850 by (simp add: divide_inverse mult_commute)
851 show "u \<in> Rep_preal R" by (rule u)
852 show "x = x / u * u" using upos
853 by (simp add: divide_inverse mult_commute)
857 lemma subset_inverse_mult:
858 "Rep_preal(preal_of_rat 1) \<subseteq> Rep_preal(inverse R * R)"
859 apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff
860 mem_Rep_preal_mult_iff)
861 apply (blast dest: subset_inverse_mult_lemma)
864 lemma inverse_mult_subset_lemma:
865 assumes rpos: "0 < r"
867 and notin: "inverse y \<notin> Rep_preal R"
868 and q: "q \<in> Rep_preal R"
871 have "q < inverse y" using rpos rless
872 by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
873 hence "r * q < r/y" using rpos
874 by (simp add: divide_inverse mult_less_cancel_left)
875 also have "... \<le> 1" using rpos rless
876 by (simp add: pos_divide_le_eq)
877 finally show ?thesis .
880 lemma inverse_mult_subset:
881 "Rep_preal(inverse R * R) \<subseteq> Rep_preal(preal_of_rat 1)"
882 apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff
883 mem_Rep_preal_mult_iff)
884 apply (simp add: zero_less_mult_iff preal_imp_pos [OF Rep_preal])
885 apply (blast intro: inverse_mult_subset_lemma)
888 lemma preal_mult_inverse:
889 "inverse R * R = (preal_of_rat 1)"
890 apply (rule inj_Rep_preal [THEN injD])
891 apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult])
894 lemma preal_mult_inverse_right:
895 "R * inverse R = (preal_of_rat 1)"
896 apply (rule preal_mult_commute [THEN subst])
897 apply (rule preal_mult_inverse)
901 text{*Theorems needing @{text Gleason9_34}*}
903 lemma Rep_preal_self_subset: "Rep_preal (R) \<subseteq> Rep_preal(R + S)"
906 assume r: "r \<in> Rep_preal R"
907 have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
908 from mem_Rep_preal_Ex
909 obtain y where y: "y \<in> Rep_preal S" ..
910 have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
911 have ry: "r+y \<in> Rep_preal(R + S)" using r y
912 by (auto simp add: mem_Rep_preal_add_iff)
913 show "r \<in> Rep_preal(R + S)" using r ypos rpos
914 by (simp add: preal_downwards_closed [OF Rep_preal ry])
917 lemma Rep_preal_sum_not_subset: "~ Rep_preal (R + S) \<subseteq> Rep_preal(R)"
919 from mem_Rep_preal_Ex
920 obtain y where y: "y \<in> Rep_preal S" ..
921 have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
922 from Gleason9_34 [OF Rep_preal ypos]
923 obtain r where r: "r \<in> Rep_preal R" and notin: "r + y \<notin> Rep_preal R" ..
924 have "r + y \<in> Rep_preal (R + S)" using r y
925 by (auto simp add: mem_Rep_preal_add_iff)
926 thus ?thesis using notin by blast
929 lemma Rep_preal_sum_not_eq: "Rep_preal (R + S) \<noteq> Rep_preal(R)"
930 by (insert Rep_preal_sum_not_subset, blast)
932 text{*at last, Gleason prop. 9-3.5(iii) page 123*}
933 lemma preal_self_less_add_left: "(R::preal) < R + S"
934 apply (unfold preal_less_def psubset_def)
935 apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
938 lemma preal_self_less_add_right: "(R::preal) < S + R"
939 by (simp add: preal_add_commute preal_self_less_add_left)
941 lemma preal_not_eq_self: "x \<noteq> x + (y::preal)"
942 by (insert preal_self_less_add_left [of x y], auto)
945 subsection{*Subtraction for Positive Reals*}
947 text{*Gleason prop. 9-3.5(iv), page 123: proving @{term "A < B ==> \<exists>D. A + D =
948 B"}. We define the claimed @{term D} and show that it is a positive real*}
950 text{*Part 1 of Dedekind sections definition*}
951 lemma diff_set_not_empty:
952 "R < S ==> {} \<subset> diff_set (Rep_preal S) (Rep_preal R)"
953 apply (auto simp add: preal_less_def diff_set_def elim!: equalityE)
954 apply (frule_tac x1 = S in Rep_preal [THEN preal_exists_greater])
955 apply (drule preal_imp_pos [OF Rep_preal], clarify)
956 apply (cut_tac a=x and b=u in add_eq_exists, force)
959 text{*Part 2 of Dedekind sections definition*}
960 lemma diff_set_nonempty:
961 "\<exists>q. 0 < q & q \<notin> diff_set (Rep_preal S) (Rep_preal R)"
962 apply (cut_tac X = S in Rep_preal_exists_bound)
964 apply (rule_tac x = x in exI, auto)
965 apply (simp add: diff_set_def)
966 apply (auto dest: Rep_preal [THEN preal_downwards_closed])
969 lemma diff_set_not_rat_set:
970 "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
972 show "?lhs \<subseteq> ?rhs" by (auto simp add: diff_set_def)
973 show "?lhs \<noteq> ?rhs" using diff_set_nonempty by blast
976 text{*Part 3 of Dedekind sections definition*}
977 lemma diff_set_lemma3:
978 "[|R < S; u \<in> diff_set (Rep_preal S) (Rep_preal R); 0 < z; z < u|]
979 ==> z \<in> diff_set (Rep_preal S) (Rep_preal R)"
980 apply (auto simp add: diff_set_def)
981 apply (rule_tac x=x in exI)
982 apply (drule Rep_preal [THEN preal_downwards_closed], auto)
985 text{*Part 4 of Dedekind sections definition*}
986 lemma diff_set_lemma4:
987 "[|R < S; y \<in> diff_set (Rep_preal S) (Rep_preal R)|]
988 ==> \<exists>u \<in> diff_set (Rep_preal S) (Rep_preal R). y < u"
989 apply (auto simp add: diff_set_def)
990 apply (drule Rep_preal [THEN preal_exists_greater], clarify)
991 apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify)
992 apply (rule_tac x="y+xa" in exI)
993 apply (auto simp add: add_ac)
997 "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
998 apply (unfold preal_def cut_def)
999 apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
1000 diff_set_lemma3 diff_set_lemma4)
1003 lemma mem_Rep_preal_diff_iff:
1005 (z \<in> Rep_preal(S-R)) =
1006 (\<exists>x. 0 < x & 0 < z & x \<notin> Rep_preal R & x + z \<in> Rep_preal S)"
1007 apply (simp add: preal_diff_def mem_diff_set Rep_preal)
1008 apply (force simp add: diff_set_def)
1012 text{*proving that @{term "R + D \<le> S"}*}
1014 lemma less_add_left_lemma:
1015 assumes Rless: "R < S"
1016 and a: "a \<in> Rep_preal R"
1017 and cb: "c + b \<in> Rep_preal S"
1018 and "c \<notin> Rep_preal R"
1021 shows "a + b \<in> Rep_preal S"
1023 have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
1025 have "a < c" using prems
1026 by (blast intro: not_in_Rep_preal_ub )
1027 ultimately show ?thesis using prems
1028 by (simp add: preal_downwards_closed [OF Rep_preal cb])
1031 lemma less_add_left_le1:
1032 "R < (S::preal) ==> R + (S-R) \<le> S"
1033 apply (auto simp add: Bex_def preal_le_def mem_Rep_preal_add_iff
1034 mem_Rep_preal_diff_iff)
1035 apply (blast intro: less_add_left_lemma)
1038 subsection{*proving that @{term "S \<le> R + D"} --- trickier*}
1040 lemma lemma_sum_mem_Rep_preal_ex:
1041 "x \<in> Rep_preal S ==> \<exists>e. 0 < e & x + e \<in> Rep_preal S"
1042 apply (drule Rep_preal [THEN preal_exists_greater], clarify)
1043 apply (cut_tac a=x and b=u in add_eq_exists, auto)
1046 lemma less_add_left_lemma2:
1047 assumes Rless: "R < S"
1048 and x: "x \<in> Rep_preal S"
1049 and xnot: "x \<notin> Rep_preal R"
1050 shows "\<exists>u v z. 0 < v & 0 < z & u \<in> Rep_preal R & z \<notin> Rep_preal R &
1051 z + v \<in> Rep_preal S & x = u + v"
1053 have xpos: "0<x" by (rule preal_imp_pos [OF Rep_preal x])
1054 from lemma_sum_mem_Rep_preal_ex [OF x]
1055 obtain e where epos: "0 < e" and xe: "x + e \<in> Rep_preal S" by blast
1056 from Gleason9_34 [OF Rep_preal epos]
1057 obtain r where r: "r \<in> Rep_preal R" and notin: "r + e \<notin> Rep_preal R" ..
1058 with x xnot xpos have rless: "r < x" by (blast intro: not_in_Rep_preal_ub)
1059 from add_eq_exists [of r x]
1060 obtain y where eq: "x = r+y" by auto
1062 proof (intro exI conjI)
1063 show "r \<in> Rep_preal R" by (rule r)
1064 show "r + e \<notin> Rep_preal R" by (rule notin)
1065 show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac)
1066 show "x = r + y" by (simp add: eq)
1067 show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r]
1069 show "0 < y" using rless eq by arith
1073 lemma less_add_left_le2: "R < (S::preal) ==> S \<le> R + (S-R)"
1074 apply (auto simp add: preal_le_def)
1075 apply (case_tac "x \<in> Rep_preal R")
1076 apply (cut_tac Rep_preal_self_subset [of R], force)
1077 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_diff_iff)
1078 apply (blast dest: less_add_left_lemma2)
1081 lemma less_add_left: "R < (S::preal) ==> R + (S-R) = S"
1082 by (blast intro: preal_le_anti_sym [OF less_add_left_le1 less_add_left_le2])
1084 lemma less_add_left_Ex: "R < (S::preal) ==> \<exists>D. R + D = S"
1085 by (fast dest: less_add_left)
1087 lemma preal_add_less2_mono1: "R < (S::preal) ==> R + T < S + T"
1088 apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc)
1089 apply (rule_tac y1 = D in preal_add_commute [THEN subst])
1090 apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric])
1093 lemma preal_add_less2_mono2: "R < (S::preal) ==> T + R < T + S"
1094 by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of T])
1096 lemma preal_add_right_less_cancel: "R + T < S + T ==> R < (S::preal)"
1097 apply (insert linorder_less_linear [of R S], auto)
1098 apply (drule_tac R = S and T = T in preal_add_less2_mono1)
1099 apply (blast dest: order_less_trans)
1102 lemma preal_add_left_less_cancel: "T + R < T + S ==> R < (S::preal)"
1103 by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T])
1105 lemma preal_add_less_cancel_right: "((R::preal) + T < S + T) = (R < S)"
1106 by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel)
1108 lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)"
1109 by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
1111 lemma preal_add_le_cancel_right: "((R::preal) + T \<le> S + T) = (R \<le> S)"
1112 by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_right)
1114 lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
1115 by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left)
1117 lemma preal_add_less_mono:
1118 "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)"
1119 apply (auto dest!: less_add_left_Ex simp add: preal_add_ac)
1120 apply (rule preal_add_assoc [THEN subst])
1121 apply (rule preal_self_less_add_right)
1124 lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S"
1125 apply (insert linorder_less_linear [of R S], safe)
1126 apply (drule_tac [!] T = T in preal_add_less2_mono1, auto)
1129 lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)"
1130 by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
1132 lemma preal_add_left_cancel_iff: "(C + A = C + B) = ((A::preal) = B)"
1133 by (fast intro: preal_add_left_cancel)
1135 lemma preal_add_right_cancel_iff: "(A + C = B + C) = ((A::preal) = B)"
1136 by (fast intro: preal_add_right_cancel)
1138 lemmas preal_cancels =
1139 preal_add_less_cancel_right preal_add_less_cancel_left
1140 preal_add_le_cancel_right preal_add_le_cancel_left
1141 preal_add_left_cancel_iff preal_add_right_cancel_iff
1144 subsection{*Completeness of type @{typ preal}*}
1146 text{*Prove that supremum is a cut*}
1148 text{*Part 1 of Dedekind sections definition*}
1150 lemma preal_sup_set_not_empty:
1151 "P \<noteq> {} ==> {} \<subset> (\<Union>X \<in> P. Rep_preal(X))"
1153 apply (cut_tac X = x in mem_Rep_preal_Ex, auto)
1157 text{*Part 2 of Dedekind sections definition*}
1159 lemma preal_sup_not_exists:
1160 "\<forall>X \<in> P. X \<le> Y ==> \<exists>q. 0 < q & q \<notin> (\<Union>X \<in> P. Rep_preal(X))"
1161 apply (cut_tac X = Y in Rep_preal_exists_bound)
1162 apply (auto simp add: preal_le_def)
1165 lemma preal_sup_set_not_rat_set:
1166 "\<forall>X \<in> P. X \<le> Y ==> (\<Union>X \<in> P. Rep_preal(X)) < {r. 0 < r}"
1167 apply (drule preal_sup_not_exists)
1168 apply (blast intro: preal_imp_pos [OF Rep_preal])
1171 text{*Part 3 of Dedekind sections definition*}
1172 lemma preal_sup_set_lemma3:
1173 "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; u \<in> (\<Union>X \<in> P. Rep_preal(X)); 0 < z; z < u|]
1174 ==> z \<in> (\<Union>X \<in> P. Rep_preal(X))"
1175 by (auto elim: Rep_preal [THEN preal_downwards_closed])
1177 text{*Part 4 of Dedekind sections definition*}
1178 lemma preal_sup_set_lemma4:
1179 "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; y \<in> (\<Union>X \<in> P. Rep_preal(X)) |]
1180 ==> \<exists>u \<in> (\<Union>X \<in> P. Rep_preal(X)). y < u"
1181 by (blast dest: Rep_preal [THEN preal_exists_greater])
1184 "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
1185 apply (unfold preal_def cut_def)
1186 apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
1187 preal_sup_set_lemma3 preal_sup_set_lemma4)
1190 lemma preal_psup_le:
1191 "[| \<forall>X \<in> P. X \<le> Y; x \<in> P |] ==> x \<le> psup P"
1192 apply (simp (no_asm_simp) add: preal_le_def)
1193 apply (subgoal_tac "P \<noteq> {}")
1194 apply (auto simp add: psup_def preal_sup)
1197 lemma psup_le_ub: "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> Y"
1198 apply (simp (no_asm_simp) add: preal_le_def)
1199 apply (simp add: psup_def preal_sup)
1200 apply (auto simp add: preal_le_def)
1203 text{*Supremum property*}
1204 lemma preal_complete:
1205 "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> (\<exists>X \<in> P. Z < X) = (Z < psup P)"
1206 apply (simp add: preal_less_def psup_def preal_sup)
1207 apply (auto simp add: preal_le_def)
1208 apply (rename_tac U)
1209 apply (cut_tac x = U and y = Z in linorder_less_linear)
1210 apply (auto simp add: preal_less_def)
1214 subsection{*The Embadding from @{typ rat} into @{typ preal}*}
1216 lemma preal_of_rat_add_lemma1:
1217 "[|x < y + z; 0 < x; 0 < y|] ==> x * y * inverse (y + z) < (y::rat)"
1218 apply (frule_tac c = "y * inverse (y + z) " in mult_strict_right_mono)
1219 apply (simp add: zero_less_mult_iff)
1220 apply (simp add: mult_ac)
1223 lemma preal_of_rat_add_lemma2:
1228 shows "\<exists>v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w"
1229 proof (intro exI conjI)
1230 show "u * x * inverse(x+y) < x" using prems
1231 by (simp add: preal_of_rat_add_lemma1)
1232 show "u * y * inverse(x+y) < y" using prems
1233 by (simp add: preal_of_rat_add_lemma1 add_commute [of x])
1234 show "0 < u * x * inverse (x + y)" using prems
1235 by (simp add: zero_less_mult_iff)
1236 show "0 < u * y * inverse (x + y)" using prems
1237 by (simp add: zero_less_mult_iff)
1238 show "u = u * x * inverse (x + y) + u * y * inverse (x + y)" using prems
1239 by (simp add: left_distrib [symmetric] right_distrib [symmetric] mult_ac)
1242 lemma preal_of_rat_add:
1244 ==> preal_of_rat ((x::rat) + y) = preal_of_rat x + preal_of_rat y"
1245 apply (unfold preal_of_rat_def preal_add_def)
1246 apply (simp add: rat_mem_preal)
1247 apply (rule_tac f = Abs_preal in arg_cong)
1248 apply (auto simp add: add_set_def)
1249 apply (blast dest: preal_of_rat_add_lemma2)
1252 lemma preal_of_rat_mult_lemma1:
1253 "[|x < y; 0 < x; 0 < z|] ==> x * z * inverse y < (z::rat)"
1254 apply (frule_tac c = "z * inverse y" in mult_strict_right_mono)
1255 apply (simp add: zero_less_mult_iff)
1256 apply (subgoal_tac "y * (z * inverse y) = z * (y * inverse y)")
1257 apply (simp_all add: mult_ac)
1260 lemma preal_of_rat_mult_lemma2:
1261 assumes xless: "x < y * z"
1264 shows "x * z * inverse y * inverse z < (z::rat)"
1266 have "0 < y * z" using prems by simp
1267 hence zpos: "0 < z" using prems by (simp add: zero_less_mult_iff)
1268 have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
1269 by (simp add: mult_ac)
1270 also have "... = x/y" using zpos
1271 by (simp add: divide_inverse)
1273 by (simp add: pos_divide_less_eq [OF ypos] mult_commute)
1274 finally show ?thesis .
1277 lemma preal_of_rat_mult_lemma3:
1278 assumes uless: "u < x * y"
1282 shows "\<exists>v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w"
1284 from dense [OF uless]
1285 obtain r where "u < r" "r < x * y" by blast
1287 proof (intro exI conjI)
1288 show "u * x * inverse r < x" using prems
1289 by (simp add: preal_of_rat_mult_lemma1)
1290 show "r * y * inverse x * inverse y < y" using prems
1291 by (simp add: preal_of_rat_mult_lemma2)
1292 show "0 < u * x * inverse r" using prems
1293 by (simp add: zero_less_mult_iff)
1294 show "0 < r * y * inverse x * inverse y" using prems
1295 by (simp add: zero_less_mult_iff)
1296 have "u * x * inverse r * (r * y * inverse x * inverse y) =
1297 u * (r * inverse r) * (x * inverse x) * (y * inverse y)"
1298 by (simp only: mult_ac)
1299 thus "u = u * x * inverse r * (r * y * inverse x * inverse y)" using prems
1304 lemma preal_of_rat_mult:
1306 ==> preal_of_rat ((x::rat) * y) = preal_of_rat x * preal_of_rat y"
1307 apply (unfold preal_of_rat_def preal_mult_def)
1308 apply (simp add: rat_mem_preal)
1309 apply (rule_tac f = Abs_preal in arg_cong)
1310 apply (auto simp add: zero_less_mult_iff mult_strict_mono mult_set_def)
1311 apply (blast dest: preal_of_rat_mult_lemma3)
1314 lemma preal_of_rat_less_iff:
1315 "[| 0 < x; 0 < y|] ==> (preal_of_rat x < preal_of_rat y) = (x < y)"
1316 by (force simp add: preal_of_rat_def preal_less_def rat_mem_preal)
1318 lemma preal_of_rat_le_iff:
1319 "[| 0 < x; 0 < y|] ==> (preal_of_rat x \<le> preal_of_rat y) = (x \<le> y)"
1320 by (simp add: preal_of_rat_less_iff linorder_not_less [symmetric])
1322 lemma preal_of_rat_eq_iff:
1323 "[| 0 < x; 0 < y|] ==> (preal_of_rat x = preal_of_rat y) = (x = y)"
1324 by (simp add: preal_of_rat_le_iff order_eq_iff)
1329 val inj_on_Abs_preal = thm"inj_on_Abs_preal";
1330 val inj_Rep_preal = thm"inj_Rep_preal";
1331 val mem_Rep_preal_Ex = thm"mem_Rep_preal_Ex";
1332 val preal_add_commute = thm"preal_add_commute";
1333 val preal_add_assoc = thm"preal_add_assoc";
1334 val preal_add_left_commute = thm"preal_add_left_commute";
1335 val preal_mult_commute = thm"preal_mult_commute";
1336 val preal_mult_assoc = thm"preal_mult_assoc";
1337 val preal_mult_left_commute = thm"preal_mult_left_commute";
1338 val preal_add_mult_distrib2 = thm"preal_add_mult_distrib2";
1339 val preal_add_mult_distrib = thm"preal_add_mult_distrib";
1340 val preal_self_less_add_left = thm"preal_self_less_add_left";
1341 val preal_self_less_add_right = thm"preal_self_less_add_right";
1342 val less_add_left = thm"less_add_left";
1343 val preal_add_less2_mono1 = thm"preal_add_less2_mono1";
1344 val preal_add_less2_mono2 = thm"preal_add_less2_mono2";
1345 val preal_add_right_less_cancel = thm"preal_add_right_less_cancel";
1346 val preal_add_left_less_cancel = thm"preal_add_left_less_cancel";
1347 val preal_add_right_cancel = thm"preal_add_right_cancel";
1348 val preal_add_left_cancel = thm"preal_add_left_cancel";
1349 val preal_add_left_cancel_iff = thm"preal_add_left_cancel_iff";
1350 val preal_add_right_cancel_iff = thm"preal_add_right_cancel_iff";
1351 val preal_psup_le = thm"preal_psup_le";
1352 val psup_le_ub = thm"psup_le_ub";
1353 val preal_complete = thm"preal_complete";
1354 val preal_of_rat_add = thm"preal_of_rat_add";
1355 val preal_of_rat_mult = thm"preal_of_rat_mult";
1357 val preal_add_ac = thms"preal_add_ac";
1358 val preal_mult_ac = thms"preal_mult_ac";