src/HOL/Real/PReal.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15234 ec91a90c604e
permissions -rw-r--r--
import -> imports
     1 (*  Title       : PReal.thy
     2     ID          : $Id$
     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.
     8 *)
     9 
    10 theory PReal
    11 imports Rational
    12 begin
    13 
    14 text{*Could be generalized and moved to @{text Ring_and_Field}*}
    15 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"
    16 by (rule_tac x="b-a" in exI, simp)
    17 
    18 text{*As a special case, the sum of two positives is positive.  One of the
    19 premises could be weakened to the relation @{text "\<le>"}.*}
    20 lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semidom)"
    21 by (insert add_strict_mono [of 0 a b c], simp)
    22 
    23 lemma interval_empty_iff:
    24      "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))"
    25 by (blast dest: dense intro: order_less_trans)
    26 
    27 
    28 constdefs
    29   cut :: "rat set => bool"
    30     "cut A == {} \<subset> A &
    31               A < {r. 0 < r} &
    32               (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u)))"
    33 
    34 
    35 lemma cut_of_rat: 
    36   assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}"
    37 proof -
    38   let ?A = "{r::rat. 0 < r & r < q}"
    39   from q have pos: "?A < {r. 0 < r}" by force
    40   have nonempty: "{} \<subset> ?A"
    41   proof
    42     show "{} \<subseteq> ?A" by simp
    43     show "{} \<noteq> ?A"
    44       by (force simp only: q eq_commute [of "{}"] interval_empty_iff)
    45   qed
    46   show ?thesis
    47     by (simp add: cut_def pos nonempty,
    48         blast dest: dense intro: order_less_trans)
    49 qed
    50 
    51 
    52 typedef preal = "{A. cut A}"
    53   by (blast intro: cut_of_rat [OF zero_less_one])
    54 
    55 instance preal :: "{ord, plus, minus, times, inverse}" ..
    56 
    57 constdefs
    58   preal_of_rat :: "rat => preal"
    59      "preal_of_rat q == Abs_preal({x::rat. 0 < x & x < q})"
    60 
    61   psup       :: "preal set => preal"
    62     "psup(P)   == Abs_preal(\<Union>X \<in> P. Rep_preal(X))"
    63 
    64   add_set :: "[rat set,rat set] => rat set"
    65     "add_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
    66 
    67   diff_set :: "[rat set,rat set] => rat set"
    68     "diff_set A B == {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
    69 
    70   mult_set :: "[rat set,rat set] => rat set"
    71     "mult_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
    72 
    73   inverse_set :: "rat set => rat set"
    74     "inverse_set A == {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
    75 
    76 
    77 defs (overloaded)
    78 
    79   preal_less_def:
    80     "R < (S::preal) == Rep_preal R < Rep_preal S"
    81 
    82   preal_le_def:
    83     "R \<le> (S::preal) == Rep_preal R \<subseteq> Rep_preal S"
    84 
    85   preal_add_def:
    86     "R + S == Abs_preal (add_set (Rep_preal R) (Rep_preal S))"
    87 
    88   preal_diff_def:
    89     "R - S == Abs_preal (diff_set (Rep_preal R) (Rep_preal S))"
    90 
    91   preal_mult_def:
    92     "R * S == Abs_preal(mult_set (Rep_preal R) (Rep_preal S))"
    93 
    94   preal_inverse_def:
    95     "inverse R == Abs_preal(inverse_set (Rep_preal R))"
    96 
    97 
    98 lemma inj_on_Abs_preal: "inj_on Abs_preal preal"
    99 apply (rule inj_on_inverseI)
   100 apply (erule Abs_preal_inverse)
   101 done
   102 
   103 declare inj_on_Abs_preal [THEN inj_on_iff, simp]
   104 
   105 lemma inj_Rep_preal: "inj(Rep_preal)"
   106 apply (rule inj_on_inverseI)
   107 apply (rule Rep_preal_inverse)
   108 done
   109 
   110 lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
   111 by (unfold preal_def cut_def, blast)
   112 
   113 lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
   114 by (force simp add: preal_def cut_def)
   115 
   116 lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
   117 by (drule preal_imp_psubset_positives, auto)
   118 
   119 lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
   120 by (unfold preal_def cut_def, blast)
   121 
   122 lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X"
   123 apply (insert Rep_preal [of X])
   124 apply (unfold preal_def cut_def, blast)
   125 done
   126 
   127 declare Abs_preal_inverse [simp]
   128 
   129 lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
   130 by (unfold preal_def cut_def, blast)
   131 
   132 text{*Relaxing the final premise*}
   133 lemma preal_downwards_closed':
   134      "[| A \<in> preal; y \<in> A; 0 < z; z \<le> y |] ==> z \<in> A"
   135 apply (simp add: order_le_less)
   136 apply (blast intro: preal_downwards_closed)
   137 done
   138 
   139 lemma Rep_preal_exists_bound: "\<exists>x. 0 < x & x \<notin> Rep_preal X"
   140 apply (cut_tac x = X in Rep_preal)
   141 apply (drule preal_imp_psubset_positives)
   142 apply (auto simp add: psubset_def)
   143 done
   144 
   145 
   146 subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
   147 
   148 lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal"
   149 apply (auto simp add: preal_def cut_def intro: order_less_trans)
   150 apply (force simp only: eq_commute [of "{}"] interval_empty_iff)
   151 apply (blast dest: dense intro: order_less_trans)
   152 done
   153 
   154 lemma rat_subset_imp_le:
   155      "[|{u::rat. 0 < u & u < x} \<subseteq> {u. 0 < u & u < y}; 0<x|] ==> x \<le> y"
   156 apply (simp add: linorder_not_less [symmetric])
   157 apply (blast dest: dense intro: order_less_trans)
   158 done
   159 
   160 lemma rat_set_eq_imp_eq:
   161      "[|{u::rat. 0 < u & u < x} = {u. 0 < u & u < y};
   162         0 < x; 0 < y|] ==> x = y"
   163 by (blast intro: rat_subset_imp_le order_antisym)
   164 
   165 
   166 
   167 subsection{*Theorems for Ordering*}
   168 
   169 text{*A positive fraction not in a positive real is an upper bound.
   170  Gleason p. 122 - Remark (1)*}
   171 
   172 lemma not_in_preal_ub:
   173      assumes A: "A \<in> preal"
   174          and notx: "x \<notin> A"
   175          and y: "y \<in> A"
   176          and pos: "0 < x"
   177         shows "y < x"
   178 proof (cases rule: linorder_cases)
   179   assume "x<y"
   180   with notx show ?thesis
   181     by (simp add:  preal_downwards_closed [OF A y] pos)
   182 next
   183   assume "x=y"
   184   with notx and y show ?thesis by simp
   185 next
   186   assume "y<x"
   187   thus ?thesis by assumption
   188 qed
   189 
   190 lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal]
   191 
   192 
   193 subsection{*The @{text "\<le>"} Ordering*}
   194 
   195 lemma preal_le_refl: "w \<le> (w::preal)"
   196 by (simp add: preal_le_def)
   197 
   198 lemma preal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::preal)"
   199 by (force simp add: preal_le_def)
   200 
   201 lemma preal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::preal)"
   202 apply (simp add: preal_le_def)
   203 apply (rule Rep_preal_inject [THEN iffD1], blast)
   204 done
   205 
   206 (* Axiom 'order_less_le' of class 'order': *)
   207 lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
   208 by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def)
   209 
   210 instance preal :: order
   211   by intro_classes
   212     (assumption |
   213       rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
   214 
   215 lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
   216 by (insert preal_imp_psubset_positives, blast)
   217 
   218 lemma preal_le_linear: "x <= y | y <= (x::preal)"
   219 apply (auto simp add: preal_le_def)
   220 apply (rule ccontr)
   221 apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
   222              elim: order_less_asym)
   223 done
   224 
   225 instance preal :: linorder
   226   by intro_classes (rule preal_le_linear)
   227 
   228 
   229 
   230 subsection{*Properties of Addition*}
   231 
   232 lemma preal_add_commute: "(x::preal) + y = y + x"
   233 apply (unfold preal_add_def add_set_def)
   234 apply (rule_tac f = Abs_preal in arg_cong)
   235 apply (force simp add: add_commute)
   236 done
   237 
   238 text{*Lemmas for proving that addition of two positive reals gives
   239  a positive real*}
   240 
   241 lemma empty_psubset_nonempty: "a \<in> A ==> {} \<subset> A"
   242 by blast
   243 
   244 text{*Part 1 of Dedekind sections definition*}
   245 lemma add_set_not_empty:
   246      "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> add_set A B"
   247 apply (insert preal_nonempty [of A] preal_nonempty [of B]) 
   248 apply (auto simp add: add_set_def)
   249 done
   250 
   251 text{*Part 2 of Dedekind sections definition.  A structured version of
   252 this proof is @{text preal_not_mem_mult_set_Ex} below.*}
   253 lemma preal_not_mem_add_set_Ex:
   254      "[|A \<in> preal; B \<in> preal|] ==> \<exists>q. 0 < q & q \<notin> add_set A B"
   255 apply (insert preal_exists_bound [of A] preal_exists_bound [of B], auto) 
   256 apply (rule_tac x = "x+xa" in exI)
   257 apply (simp add: add_set_def, clarify)
   258 apply (drule not_in_preal_ub, assumption+)+
   259 apply (force dest: add_strict_mono)
   260 done
   261 
   262 lemma add_set_not_rat_set:
   263    assumes A: "A \<in> preal" 
   264        and B: "B \<in> preal"
   265      shows "add_set A B < {r. 0 < r}"
   266 proof
   267   from preal_imp_pos [OF A] preal_imp_pos [OF B]
   268   show "add_set A B \<subseteq> {r. 0 < r}" by (force simp add: add_set_def) 
   269 next
   270   show "add_set A B \<noteq> {r. 0 < r}"
   271     by (insert preal_not_mem_add_set_Ex [OF A B], blast) 
   272 qed
   273 
   274 text{*Part 3 of Dedekind sections definition*}
   275 lemma add_set_lemma3:
   276      "[|A \<in> preal; B \<in> preal; u \<in> add_set A B; 0 < z; z < u|] 
   277       ==> z \<in> add_set A B"
   278 proof (unfold add_set_def, clarify)
   279   fix x::rat and y::rat
   280   assume A: "A \<in> preal" 
   281      and B: "B \<in> preal"
   282      and [simp]: "0 < z"
   283      and zless: "z < x + y"
   284      and x:  "x \<in> A"
   285      and y:  "y \<in> B"
   286   have xpos [simp]: "0<x" by (rule preal_imp_pos [OF A x])
   287   have ypos [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   288   have xypos [simp]: "0 < x+y" by (simp add: pos_add_strict)
   289   let ?f = "z/(x+y)"
   290   have fless: "?f < 1" by (simp add: zless pos_divide_less_eq)
   291   show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
   292   proof
   293     show "\<exists>y' \<in> B. z = x*?f + y'"
   294     proof
   295       show "z = x*?f + y*?f"
   296 	by (simp add: left_distrib [symmetric] divide_inverse mult_ac
   297 		      order_less_imp_not_eq2)
   298     next
   299       show "y * ?f \<in> B"
   300       proof (rule preal_downwards_closed [OF B y])
   301         show "0 < y * ?f"
   302           by (simp add: divide_inverse zero_less_mult_iff)
   303       next
   304         show "y * ?f < y"
   305           by (insert mult_strict_left_mono [OF fless ypos], simp)
   306       qed
   307     qed
   308   next
   309     show "x * ?f \<in> A"
   310     proof (rule preal_downwards_closed [OF A x])
   311       show "0 < x * ?f"
   312 	by (simp add: divide_inverse zero_less_mult_iff)
   313     next
   314       show "x * ?f < x"
   315 	by (insert mult_strict_left_mono [OF fless xpos], simp)
   316     qed
   317   qed
   318 qed
   319 
   320 text{*Part 4 of Dedekind sections definition*}
   321 lemma add_set_lemma4:
   322      "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
   323 apply (auto simp add: add_set_def)
   324 apply (frule preal_exists_greater [of A], auto) 
   325 apply (rule_tac x="u + y" in exI)
   326 apply (auto intro: add_strict_left_mono)
   327 done
   328 
   329 lemma mem_add_set:
   330      "[|A \<in> preal; B \<in> preal|] ==> add_set A B \<in> preal"
   331 apply (simp (no_asm_simp) add: preal_def cut_def)
   332 apply (blast intro!: add_set_not_empty add_set_not_rat_set
   333                      add_set_lemma3 add_set_lemma4)
   334 done
   335 
   336 lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
   337 apply (simp add: preal_add_def mem_add_set Rep_preal)
   338 apply (force simp add: add_set_def add_ac)
   339 done
   340 
   341 lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
   342   apply (rule mk_left_commute [of "op +"])
   343   apply (rule preal_add_assoc)
   344   apply (rule preal_add_commute)
   345   done
   346 
   347 text{* Positive Real addition is an AC operator *}
   348 lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
   349 
   350 
   351 subsection{*Properties of Multiplication*}
   352 
   353 text{*Proofs essentially same as for addition*}
   354 
   355 lemma preal_mult_commute: "(x::preal) * y = y * x"
   356 apply (unfold preal_mult_def mult_set_def)
   357 apply (rule_tac f = Abs_preal in arg_cong)
   358 apply (force simp add: mult_commute)
   359 done
   360 
   361 text{*Multiplication of two positive reals gives a positive real.*}
   362 
   363 text{*Lemmas for proving positive reals multiplication set in @{typ preal}*}
   364 
   365 text{*Part 1 of Dedekind sections definition*}
   366 lemma mult_set_not_empty:
   367      "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> mult_set A B"
   368 apply (insert preal_nonempty [of A] preal_nonempty [of B]) 
   369 apply (auto simp add: mult_set_def)
   370 done
   371 
   372 text{*Part 2 of Dedekind sections definition*}
   373 lemma preal_not_mem_mult_set_Ex:
   374    assumes A: "A \<in> preal" 
   375        and B: "B \<in> preal"
   376      shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
   377 proof -
   378   from preal_exists_bound [OF A]
   379   obtain x where [simp]: "0 < x" "x \<notin> A" by blast
   380   from preal_exists_bound [OF B]
   381   obtain y where [simp]: "0 < y" "y \<notin> B" by blast
   382   show ?thesis
   383   proof (intro exI conjI)
   384     show "0 < x*y" by (simp add: mult_pos)
   385     show "x * y \<notin> mult_set A B"
   386     proof -
   387       { fix u::rat and v::rat
   388 	      assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
   389 	      moreover
   390 	      with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
   391 	      moreover
   392 	      with prems have "0\<le>v"
   393 	        by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
   394 	      moreover
   395         from calculation
   396 	      have "u*v < x*y" by (blast intro: mult_strict_mono prems)
   397 	      ultimately have False by force }
   398       thus ?thesis by (auto simp add: mult_set_def)
   399     qed
   400   qed
   401 qed
   402 
   403 lemma mult_set_not_rat_set:
   404    assumes A: "A \<in> preal" 
   405        and B: "B \<in> preal"
   406      shows "mult_set A B < {r. 0 < r}"
   407 proof
   408   show "mult_set A B \<subseteq> {r. 0 < r}"
   409     by (force simp add: mult_set_def
   410               intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos)
   411 next
   412   show "mult_set A B \<noteq> {r. 0 < r}"
   413     by (insert preal_not_mem_mult_set_Ex [OF A B], blast)
   414 qed
   415 
   416 
   417 
   418 text{*Part 3 of Dedekind sections definition*}
   419 lemma mult_set_lemma3:
   420      "[|A \<in> preal; B \<in> preal; u \<in> mult_set A B; 0 < z; z < u|] 
   421       ==> z \<in> mult_set A B"
   422 proof (unfold mult_set_def, clarify)
   423   fix x::rat and y::rat
   424   assume A: "A \<in> preal" 
   425      and B: "B \<in> preal"
   426      and [simp]: "0 < z"
   427      and zless: "z < x * y"
   428      and x:  "x \<in> A"
   429      and y:  "y \<in> B"
   430   have [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   431   show "\<exists>x' \<in> A. \<exists>y' \<in> B. z = x' * y'"
   432   proof
   433     show "\<exists>y'\<in>B. z = (z/y) * y'"
   434     proof
   435       show "z = (z/y)*y"
   436 	by (simp add: divide_inverse mult_commute [of y] mult_assoc
   437 		      order_less_imp_not_eq2)
   438       show "y \<in> B" .
   439     qed
   440   next
   441     show "z/y \<in> A"
   442     proof (rule preal_downwards_closed [OF A x])
   443       show "0 < z/y"
   444 	by (simp add: zero_less_divide_iff)
   445       show "z/y < x" by (simp add: pos_divide_less_eq zless)
   446     qed
   447   qed
   448 qed
   449 
   450 text{*Part 4 of Dedekind sections definition*}
   451 lemma mult_set_lemma4:
   452      "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
   453 apply (auto simp add: mult_set_def)
   454 apply (frule preal_exists_greater [of A], auto) 
   455 apply (rule_tac x="u * y" in exI)
   456 apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B] 
   457                    mult_strict_right_mono)
   458 done
   459 
   460 
   461 lemma mem_mult_set:
   462      "[|A \<in> preal; B \<in> preal|] ==> mult_set A B \<in> preal"
   463 apply (simp (no_asm_simp) add: preal_def cut_def)
   464 apply (blast intro!: mult_set_not_empty mult_set_not_rat_set
   465                      mult_set_lemma3 mult_set_lemma4)
   466 done
   467 
   468 lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
   469 apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   470 apply (force simp add: mult_set_def mult_ac)
   471 done
   472 
   473 lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
   474   apply (rule mk_left_commute [of "op *"])
   475   apply (rule preal_mult_assoc)
   476   apply (rule preal_mult_commute)
   477   done
   478 
   479 
   480 text{* Positive Real multiplication is an AC operator *}
   481 lemmas preal_mult_ac =
   482        preal_mult_assoc preal_mult_commute preal_mult_left_commute
   483 
   484 
   485 text{* Positive real 1 is the multiplicative identity element *}
   486 
   487 lemma rat_mem_preal: "0 < q ==> {r::rat. 0 < r & r < q} \<in> preal"
   488 by (simp add: preal_def cut_of_rat)
   489 
   490 lemma preal_mult_1: "(preal_of_rat 1) * z = z"
   491 proof (induct z)
   492   fix A :: "rat set"
   493   assume A: "A \<in> preal"
   494   have "{w. \<exists>u. 0 < u \<and> u < 1 & (\<exists>v \<in> A. w = u * v)} = A" (is "?lhs = A")
   495   proof
   496     show "?lhs \<subseteq> A"
   497     proof clarify
   498       fix x::rat and u::rat and v::rat
   499       assume upos: "0<u" and "u<1" and v: "v \<in> A"
   500       have vpos: "0<v" by (rule preal_imp_pos [OF A v])
   501       hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
   502       thus "u * v \<in> A"
   503         by (force intro: preal_downwards_closed [OF A v] mult_pos upos vpos)
   504     qed
   505   next
   506     show "A \<subseteq> ?lhs"
   507     proof clarify
   508       fix x::rat
   509       assume x: "x \<in> A"
   510       have xpos: "0<x" by (rule preal_imp_pos [OF A x])
   511       from preal_exists_greater [OF A x]
   512       obtain v where v: "v \<in> A" and xlessv: "x < v" ..
   513       have vpos: "0<v" by (rule preal_imp_pos [OF A v])
   514       show "\<exists>u. 0 < u \<and> u < 1 \<and> (\<exists>v\<in>A. x = u * v)"
   515       proof (intro exI conjI)
   516         show "0 < x/v"
   517           by (simp add: zero_less_divide_iff xpos vpos)
   518 	show "x / v < 1"
   519           by (simp add: pos_divide_less_eq vpos xlessv)
   520         show "\<exists>v'\<in>A. x = (x / v) * v'"
   521         proof
   522           show "x = (x/v)*v"
   523 	    by (simp add: divide_inverse mult_assoc vpos
   524                           order_less_imp_not_eq2)
   525           show "v \<in> A" .
   526         qed
   527       qed
   528     qed
   529   qed
   530   thus "preal_of_rat 1 * Abs_preal A = Abs_preal A"
   531     by (simp add: preal_of_rat_def preal_mult_def mult_set_def 
   532                   rat_mem_preal A)
   533 qed
   534 
   535 
   536 lemma preal_mult_1_right: "z * (preal_of_rat 1) = z"
   537 apply (rule preal_mult_commute [THEN subst])
   538 apply (rule preal_mult_1)
   539 done
   540 
   541 
   542 subsection{*Distribution of Multiplication across Addition*}
   543 
   544 lemma mem_Rep_preal_add_iff:
   545       "(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x + y)"
   546 apply (simp add: preal_add_def mem_add_set Rep_preal)
   547 apply (simp add: add_set_def) 
   548 done
   549 
   550 lemma mem_Rep_preal_mult_iff:
   551       "(z \<in> Rep_preal(R*S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x * y)"
   552 apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   553 apply (simp add: mult_set_def) 
   554 done
   555 
   556 lemma distrib_subset1:
   557      "Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)"
   558 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
   559 apply (force simp add: right_distrib)
   560 done
   561 
   562 lemma linorder_le_cases [case_names le ge]:
   563     "((x::'a::linorder) <= y ==> P) ==> (y <= x ==> P) ==> P"
   564   apply (insert linorder_linear, blast)
   565   done
   566 
   567 lemma preal_add_mult_distrib_mean:
   568   assumes a: "a \<in> Rep_preal w"
   569       and b: "b \<in> Rep_preal w"
   570       and d: "d \<in> Rep_preal x"
   571       and e: "e \<in> Rep_preal y"
   572      shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
   573 proof
   574   let ?c = "(a*d + b*e)/(d+e)"
   575   have [simp]: "0<a" "0<b" "0<d" "0<e" "0<d+e"
   576     by (blast intro: preal_imp_pos [OF Rep_preal] a b d e pos_add_strict)+
   577   have cpos: "0 < ?c"
   578     by (simp add: zero_less_divide_iff zero_less_mult_iff pos_add_strict)
   579   show "a * d + b * e = ?c * (d + e)"
   580     by (simp add: divide_inverse mult_assoc order_less_imp_not_eq2)
   581   show "?c \<in> Rep_preal w"
   582     proof (cases rule: linorder_le_cases)
   583       assume "a \<le> b"
   584       hence "?c \<le> b"
   585 	by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   586                       order_less_imp_le)
   587       thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos])
   588     next
   589       assume "b \<le> a"
   590       hence "?c \<le> a"
   591 	by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   592                       order_less_imp_le)
   593       thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos])
   594     qed
   595   qed
   596 
   597 lemma distrib_subset2:
   598      "Rep_preal (w * x + w * y) \<subseteq> Rep_preal (w * (x + y))"
   599 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
   600 apply (drule_tac w=w and x=x and y=y in preal_add_mult_distrib_mean, auto)
   601 done
   602 
   603 lemma preal_add_mult_distrib2: "(w * ((x::preal) + y)) = (w * x) + (w * y)"
   604 apply (rule inj_Rep_preal [THEN injD])
   605 apply (rule equalityI [OF distrib_subset1 distrib_subset2])
   606 done
   607 
   608 lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)"
   609 by (simp add: preal_mult_commute preal_add_mult_distrib2)
   610 
   611 
   612 subsection{*Existence of Inverse, a Positive Real*}
   613 
   614 lemma mem_inv_set_ex:
   615   assumes A: "A \<in> preal" shows "\<exists>x y. 0 < x & x < y & inverse y \<notin> A"
   616 proof -
   617   from preal_exists_bound [OF A]
   618   obtain x where [simp]: "0<x" "x \<notin> A" by blast
   619   show ?thesis
   620   proof (intro exI conjI)
   621     show "0 < inverse (x+1)"
   622       by (simp add: order_less_trans [OF _ less_add_one]) 
   623     show "inverse(x+1) < inverse x"
   624       by (simp add: less_imp_inverse_less less_add_one)
   625     show "inverse (inverse x) \<notin> A"
   626       by (simp add: order_less_imp_not_eq2)
   627   qed
   628 qed
   629 
   630 text{*Part 1 of Dedekind sections definition*}
   631 lemma inverse_set_not_empty:
   632      "A \<in> preal ==> {} \<subset> inverse_set A"
   633 apply (insert mem_inv_set_ex [of A])
   634 apply (auto simp add: inverse_set_def)
   635 done
   636 
   637 text{*Part 2 of Dedekind sections definition*}
   638 
   639 lemma preal_not_mem_inverse_set_Ex:
   640    assumes A: "A \<in> preal"  shows "\<exists>q. 0 < q & q \<notin> inverse_set A"
   641 proof -
   642   from preal_nonempty [OF A]
   643   obtain x where x: "x \<in> A" and  xpos [simp]: "0<x" ..
   644   show ?thesis
   645   proof (intro exI conjI)
   646     show "0 < inverse x" by simp
   647     show "inverse x \<notin> inverse_set A"
   648     proof -
   649       { fix y::rat 
   650 	assume ygt: "inverse x < y"
   651 	have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
   652 	have iyless: "inverse y < x" 
   653 	  by (simp add: inverse_less_imp_less [of x] ygt)
   654 	have "inverse y \<in> A"
   655 	  by (simp add: preal_downwards_closed [OF A x] iyless)}
   656      thus ?thesis by (auto simp add: inverse_set_def)
   657     qed
   658   qed
   659 qed
   660 
   661 lemma inverse_set_not_rat_set:
   662    assumes A: "A \<in> preal"  shows "inverse_set A < {r. 0 < r}"
   663 proof
   664   show "inverse_set A \<subseteq> {r. 0 < r}"  by (force simp add: inverse_set_def)
   665 next
   666   show "inverse_set A \<noteq> {r. 0 < r}"
   667     by (insert preal_not_mem_inverse_set_Ex [OF A], blast)
   668 qed
   669 
   670 text{*Part 3 of Dedekind sections definition*}
   671 lemma inverse_set_lemma3:
   672      "[|A \<in> preal; u \<in> inverse_set A; 0 < z; z < u|] 
   673       ==> z \<in> inverse_set A"
   674 apply (auto simp add: inverse_set_def)
   675 apply (auto intro: order_less_trans)
   676 done
   677 
   678 text{*Part 4 of Dedekind sections definition*}
   679 lemma inverse_set_lemma4:
   680      "[|A \<in> preal; y \<in> inverse_set A|] ==> \<exists>u \<in> inverse_set A. y < u"
   681 apply (auto simp add: inverse_set_def)
   682 apply (drule dense [of y]) 
   683 apply (blast intro: order_less_trans)
   684 done
   685 
   686 
   687 lemma mem_inverse_set:
   688      "A \<in> preal ==> inverse_set A \<in> preal"
   689 apply (simp (no_asm_simp) add: preal_def cut_def)
   690 apply (blast intro!: inverse_set_not_empty inverse_set_not_rat_set
   691                      inverse_set_lemma3 inverse_set_lemma4)
   692 done
   693 
   694 
   695 subsection{*Gleason's Lemma 9-3.4, page 122*}
   696 
   697 lemma Gleason9_34_exists:
   698   assumes A: "A \<in> preal"
   699       and "\<forall>x\<in>A. x + u \<in> A"
   700       and "0 \<le> z"
   701      shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
   702 proof (cases z rule: int_cases)
   703   case (nonneg n)
   704   show ?thesis
   705   proof (simp add: prems, induct n)
   706     case 0
   707       from preal_nonempty [OF A]
   708       show ?case  by force 
   709     case (Suc k)
   710       from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
   711       hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
   712       thus ?case by (force simp add: left_distrib add_ac prems) 
   713   qed
   714 next
   715   case (neg n)
   716   with prems show ?thesis by simp
   717 qed
   718 
   719 lemma Gleason9_34_contra:
   720   assumes A: "A \<in> preal"
   721     shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
   722 proof (induct u, induct y)
   723   fix a::int and b::int
   724   fix c::int and d::int
   725   assume bpos [simp]: "0 < b"
   726      and dpos [simp]: "0 < d"
   727      and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
   728      and upos: "0 < Fract c d"
   729      and ypos: "0 < Fract a b"
   730      and notin: "Fract a b \<notin> A"
   731   have cpos [simp]: "0 < c" 
   732     by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos) 
   733   have apos [simp]: "0 < a" 
   734     by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos) 
   735   let ?k = "a*d"
   736   have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
   737   proof -
   738     have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
   739       by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac) 
   740     moreover
   741     have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
   742       by (rule mult_mono, 
   743           simp_all add: int_one_le_iff_zero_less zero_less_mult_iff 
   744                         order_less_imp_le)
   745     ultimately
   746     show ?thesis by simp
   747   qed
   748   have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff)  
   749   from Gleason9_34_exists [OF A closed k]
   750   obtain z where z: "z \<in> A" 
   751              and mem: "z + of_int ?k * Fract c d \<in> A" ..
   752   have less: "z + of_int ?k * Fract c d < Fract a b"
   753     by (rule not_in_preal_ub [OF A notin mem ypos])
   754   have "0<z" by (rule preal_imp_pos [OF A z])
   755   with frle and less show False by (simp add: Fract_of_int_eq) 
   756 qed
   757 
   758 
   759 lemma Gleason9_34:
   760   assumes A: "A \<in> preal"
   761       and upos: "0 < u"
   762     shows "\<exists>r \<in> A. r + u \<notin> A"
   763 proof (rule ccontr, simp)
   764   assume closed: "\<forall>r\<in>A. r + u \<in> A"
   765   from preal_exists_bound [OF A]
   766   obtain y where y: "y \<notin> A" and ypos: "0 < y" by blast
   767   show False
   768     by (rule Gleason9_34_contra [OF A closed upos ypos y])
   769 qed
   770 
   771 
   772 
   773 subsection{*Gleason's Lemma 9-3.6*}
   774 
   775 lemma lemma_gleason9_36:
   776   assumes A: "A \<in> preal"
   777       and x: "1 < x"
   778     shows "\<exists>r \<in> A. r*x \<notin> A"
   779 proof -
   780   from preal_nonempty [OF A]
   781   obtain y where y: "y \<in> A" and  ypos: "0<y" ..
   782   show ?thesis 
   783   proof (rule classical)
   784     assume "~(\<exists>r\<in>A. r * x \<notin> A)"
   785     with y have ymem: "y * x \<in> A" by blast 
   786     from ypos mult_strict_left_mono [OF x]
   787     have yless: "y < y*x" by simp 
   788     let ?d = "y*x - y"
   789     from yless have dpos: "0 < ?d" and eq: "y + ?d = y*x" by auto
   790     from Gleason9_34 [OF A dpos]
   791     obtain r where r: "r\<in>A" and notin: "r + ?d \<notin> A" ..
   792     have rpos: "0<r" by (rule preal_imp_pos [OF A r])
   793     with dpos have rdpos: "0 < r + ?d" by arith
   794     have "~ (r + ?d \<le> y + ?d)"
   795     proof
   796       assume le: "r + ?d \<le> y + ?d" 
   797       from ymem have yd: "y + ?d \<in> A" by (simp add: eq)
   798       have "r + ?d \<in> A" by (rule preal_downwards_closed' [OF A yd rdpos le])
   799       with notin show False by simp
   800     qed
   801     hence "y < r" by simp
   802     with ypos have  dless: "?d < (r * ?d)/y"
   803       by (simp add: pos_less_divide_eq mult_commute [of ?d]
   804                     mult_strict_right_mono dpos)
   805     have "r + ?d < r*x"
   806     proof -
   807       have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
   808       also with ypos have "... = (r/y) * (y + ?d)"
   809 	by (simp only: right_distrib divide_inverse mult_ac, simp)
   810       also have "... = r*x" using ypos
   811 	by simp
   812       finally show "r + ?d < r*x" .
   813     qed
   814     with r notin rdpos
   815     show "\<exists>r\<in>A. r * x \<notin> A" by (blast dest:  preal_downwards_closed [OF A])
   816   qed  
   817 qed
   818 
   819 subsection{*Existence of Inverse: Part 2*}
   820 
   821 lemma mem_Rep_preal_inverse_iff:
   822       "(z \<in> Rep_preal(inverse R)) = 
   823        (0 < z \<and> (\<exists>y. z < y \<and> inverse y \<notin> Rep_preal R))"
   824 apply (simp add: preal_inverse_def mem_inverse_set Rep_preal)
   825 apply (simp add: inverse_set_def) 
   826 done
   827 
   828 lemma Rep_preal_of_rat:
   829      "0 < q ==> Rep_preal (preal_of_rat q) = {x. 0 < x \<and> x < q}"
   830 by (simp add: preal_of_rat_def rat_mem_preal) 
   831 
   832 lemma subset_inverse_mult_lemma:
   833       assumes xpos: "0 < x" and xless: "x < 1"
   834          shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R & 
   835                         u \<in> Rep_preal R & x = r * u"
   836 proof -
   837   from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff)
   838   from lemma_gleason9_36 [OF Rep_preal this]
   839   obtain r where r: "r \<in> Rep_preal R" 
   840              and notin: "r * (inverse x) \<notin> Rep_preal R" ..
   841   have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
   842   from preal_exists_greater [OF Rep_preal r]
   843   obtain u where u: "u \<in> Rep_preal R" and rless: "r < u" ..
   844   have upos: "0<u" by (rule preal_imp_pos [OF Rep_preal u])
   845   show ?thesis
   846   proof (intro exI conjI)
   847     show "0 < x/u" using xpos upos
   848       by (simp add: zero_less_divide_iff)  
   849     show "x/u < x/r" using xpos upos rpos
   850       by (simp add: divide_inverse mult_less_cancel_left rless) 
   851     show "inverse (x / r) \<notin> Rep_preal R" using notin
   852       by (simp add: divide_inverse mult_commute) 
   853     show "u \<in> Rep_preal R" by (rule u) 
   854     show "x = x / u * u" using upos 
   855       by (simp add: divide_inverse mult_commute) 
   856   qed
   857 qed
   858 
   859 lemma subset_inverse_mult: 
   860      "Rep_preal(preal_of_rat 1) \<subseteq> Rep_preal(inverse R * R)"
   861 apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
   862                       mem_Rep_preal_mult_iff)
   863 apply (blast dest: subset_inverse_mult_lemma) 
   864 done
   865 
   866 lemma inverse_mult_subset_lemma:
   867      assumes rpos: "0 < r" 
   868          and rless: "r < y"
   869          and notin: "inverse y \<notin> Rep_preal R"
   870          and q: "q \<in> Rep_preal R"
   871      shows "r*q < 1"
   872 proof -
   873   have "q < inverse y" using rpos rless
   874     by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
   875   hence "r * q < r/y" using rpos
   876     by (simp add: divide_inverse mult_less_cancel_left)
   877   also have "... \<le> 1" using rpos rless
   878     by (simp add: pos_divide_le_eq)
   879   finally show ?thesis .
   880 qed
   881 
   882 lemma inverse_mult_subset:
   883      "Rep_preal(inverse R * R) \<subseteq> Rep_preal(preal_of_rat 1)"
   884 apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
   885                       mem_Rep_preal_mult_iff)
   886 apply (simp add: zero_less_mult_iff preal_imp_pos [OF Rep_preal]) 
   887 apply (blast intro: inverse_mult_subset_lemma) 
   888 done
   889 
   890 lemma preal_mult_inverse:
   891      "inverse R * R = (preal_of_rat 1)"
   892 apply (rule inj_Rep_preal [THEN injD])
   893 apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) 
   894 done
   895 
   896 lemma preal_mult_inverse_right:
   897      "R * inverse R = (preal_of_rat 1)"
   898 apply (rule preal_mult_commute [THEN subst])
   899 apply (rule preal_mult_inverse)
   900 done
   901 
   902 
   903 text{*Theorems needing @{text Gleason9_34}*}
   904 
   905 lemma Rep_preal_self_subset: "Rep_preal (R) \<subseteq> Rep_preal(R + S)"
   906 proof 
   907   fix r
   908   assume r: "r \<in> Rep_preal R"
   909   have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
   910   from mem_Rep_preal_Ex 
   911   obtain y where y: "y \<in> Rep_preal S" ..
   912   have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
   913   have ry: "r+y \<in> Rep_preal(R + S)" using r y
   914     by (auto simp add: mem_Rep_preal_add_iff)
   915   show "r \<in> Rep_preal(R + S)" using r ypos rpos 
   916     by (simp add:  preal_downwards_closed [OF Rep_preal ry]) 
   917 qed
   918 
   919 lemma Rep_preal_sum_not_subset: "~ Rep_preal (R + S) \<subseteq> Rep_preal(R)"
   920 proof -
   921   from mem_Rep_preal_Ex 
   922   obtain y where y: "y \<in> Rep_preal S" ..
   923   have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
   924   from  Gleason9_34 [OF Rep_preal ypos]
   925   obtain r where r: "r \<in> Rep_preal R" and notin: "r + y \<notin> Rep_preal R" ..
   926   have "r + y \<in> Rep_preal (R + S)" using r y
   927     by (auto simp add: mem_Rep_preal_add_iff)
   928   thus ?thesis using notin by blast
   929 qed
   930 
   931 lemma Rep_preal_sum_not_eq: "Rep_preal (R + S) \<noteq> Rep_preal(R)"
   932 by (insert Rep_preal_sum_not_subset, blast)
   933 
   934 text{*at last, Gleason prop. 9-3.5(iii) page 123*}
   935 lemma preal_self_less_add_left: "(R::preal) < R + S"
   936 apply (unfold preal_less_def psubset_def)
   937 apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
   938 done
   939 
   940 lemma preal_self_less_add_right: "(R::preal) < S + R"
   941 by (simp add: preal_add_commute preal_self_less_add_left)
   942 
   943 lemma preal_not_eq_self: "x \<noteq> x + (y::preal)"
   944 by (insert preal_self_less_add_left [of x y], auto)
   945 
   946 
   947 subsection{*Subtraction for Positive Reals*}
   948 
   949 text{*Gleason prop. 9-3.5(iv), page 123: proving @{term "A < B ==> \<exists>D. A + D =
   950 B"}. We define the claimed @{term D} and show that it is a positive real*}
   951 
   952 text{*Part 1 of Dedekind sections definition*}
   953 lemma diff_set_not_empty:
   954      "R < S ==> {} \<subset> diff_set (Rep_preal S) (Rep_preal R)"
   955 apply (auto simp add: preal_less_def diff_set_def elim!: equalityE) 
   956 apply (frule_tac x1 = S in Rep_preal [THEN preal_exists_greater])
   957 apply (drule preal_imp_pos [OF Rep_preal], clarify)
   958 apply (cut_tac a=x and b=u in add_eq_exists, force) 
   959 done
   960 
   961 text{*Part 2 of Dedekind sections definition*}
   962 lemma diff_set_nonempty:
   963      "\<exists>q. 0 < q & q \<notin> diff_set (Rep_preal S) (Rep_preal R)"
   964 apply (cut_tac X = S in Rep_preal_exists_bound)
   965 apply (erule exE)
   966 apply (rule_tac x = x in exI, auto)
   967 apply (simp add: diff_set_def) 
   968 apply (auto dest: Rep_preal [THEN preal_downwards_closed])
   969 done
   970 
   971 lemma diff_set_not_rat_set:
   972      "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
   973 proof
   974   show "?lhs \<subseteq> ?rhs" by (auto simp add: diff_set_def) 
   975   show "?lhs \<noteq> ?rhs" using diff_set_nonempty by blast
   976 qed
   977 
   978 text{*Part 3 of Dedekind sections definition*}
   979 lemma diff_set_lemma3:
   980      "[|R < S; u \<in> diff_set (Rep_preal S) (Rep_preal R); 0 < z; z < u|] 
   981       ==> z \<in> diff_set (Rep_preal S) (Rep_preal R)"
   982 apply (auto simp add: diff_set_def) 
   983 apply (rule_tac x=x in exI) 
   984 apply (drule Rep_preal [THEN preal_downwards_closed], auto)
   985 done
   986 
   987 text{*Part 4 of Dedekind sections definition*}
   988 lemma diff_set_lemma4:
   989      "[|R < S; y \<in> diff_set (Rep_preal S) (Rep_preal R)|] 
   990       ==> \<exists>u \<in> diff_set (Rep_preal S) (Rep_preal R). y < u"
   991 apply (auto simp add: diff_set_def) 
   992 apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
   993 apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify)  
   994 apply (rule_tac x="y+xa" in exI) 
   995 apply (auto simp add: add_ac)
   996 done
   997 
   998 lemma mem_diff_set:
   999      "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
  1000 apply (unfold preal_def cut_def)
  1001 apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
  1002                      diff_set_lemma3 diff_set_lemma4)
  1003 done
  1004 
  1005 lemma mem_Rep_preal_diff_iff:
  1006       "R < S ==>
  1007        (z \<in> Rep_preal(S-R)) = 
  1008        (\<exists>x. 0 < x & 0 < z & x \<notin> Rep_preal R & x + z \<in> Rep_preal S)"
  1009 apply (simp add: preal_diff_def mem_diff_set Rep_preal)
  1010 apply (force simp add: diff_set_def) 
  1011 done
  1012 
  1013 
  1014 text{*proving that @{term "R + D \<le> S"}*}
  1015 
  1016 lemma less_add_left_lemma:
  1017   assumes Rless: "R < S"
  1018       and a: "a \<in> Rep_preal R"
  1019       and cb: "c + b \<in> Rep_preal S"
  1020       and "c \<notin> Rep_preal R"
  1021       and "0 < b"
  1022       and "0 < c"
  1023   shows "a + b \<in> Rep_preal S"
  1024 proof -
  1025   have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
  1026   moreover
  1027   have "a < c" using prems
  1028     by (blast intro: not_in_Rep_preal_ub ) 
  1029   ultimately show ?thesis using prems
  1030     by (simp add: preal_downwards_closed [OF Rep_preal cb]) 
  1031 qed
  1032 
  1033 lemma less_add_left_le1:
  1034        "R < (S::preal) ==> R + (S-R) \<le> S"
  1035 apply (auto simp add: Bex_def preal_le_def mem_Rep_preal_add_iff 
  1036                       mem_Rep_preal_diff_iff)
  1037 apply (blast intro: less_add_left_lemma) 
  1038 done
  1039 
  1040 subsection{*proving that @{term "S \<le> R + D"} --- trickier*}
  1041 
  1042 lemma lemma_sum_mem_Rep_preal_ex:
  1043      "x \<in> Rep_preal S ==> \<exists>e. 0 < e & x + e \<in> Rep_preal S"
  1044 apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
  1045 apply (cut_tac a=x and b=u in add_eq_exists, auto) 
  1046 done
  1047 
  1048 lemma less_add_left_lemma2:
  1049   assumes Rless: "R < S"
  1050       and x:     "x \<in> Rep_preal S"
  1051       and xnot: "x \<notin>  Rep_preal R"
  1052   shows "\<exists>u v z. 0 < v & 0 < z & u \<in> Rep_preal R & z \<notin> Rep_preal R & 
  1053                      z + v \<in> Rep_preal S & x = u + v"
  1054 proof -
  1055   have xpos: "0<x" by (rule preal_imp_pos [OF Rep_preal x])
  1056   from lemma_sum_mem_Rep_preal_ex [OF x]
  1057   obtain e where epos: "0 < e" and xe: "x + e \<in> Rep_preal S" by blast
  1058   from  Gleason9_34 [OF Rep_preal epos]
  1059   obtain r where r: "r \<in> Rep_preal R" and notin: "r + e \<notin> Rep_preal R" ..
  1060   with x xnot xpos have rless: "r < x" by (blast intro: not_in_Rep_preal_ub)
  1061   from add_eq_exists [of r x]
  1062   obtain y where eq: "x = r+y" by auto
  1063   show ?thesis 
  1064   proof (intro exI conjI)
  1065     show "r \<in> Rep_preal R" by (rule r)
  1066     show "r + e \<notin> Rep_preal R" by (rule notin)
  1067     show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac)
  1068     show "x = r + y" by (simp add: eq)
  1069     show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r]
  1070       by simp
  1071     show "0 < y" using rless eq by arith
  1072   qed
  1073 qed
  1074 
  1075 lemma less_add_left_le2: "R < (S::preal) ==> S \<le> R + (S-R)"
  1076 apply (auto simp add: preal_le_def)
  1077 apply (case_tac "x \<in> Rep_preal R")
  1078 apply (cut_tac Rep_preal_self_subset [of R], force)
  1079 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_diff_iff)
  1080 apply (blast dest: less_add_left_lemma2)
  1081 done
  1082 
  1083 lemma less_add_left: "R < (S::preal) ==> R + (S-R) = S"
  1084 by (blast intro: preal_le_anti_sym [OF less_add_left_le1 less_add_left_le2])
  1085 
  1086 lemma less_add_left_Ex: "R < (S::preal) ==> \<exists>D. R + D = S"
  1087 by (fast dest: less_add_left)
  1088 
  1089 lemma preal_add_less2_mono1: "R < (S::preal) ==> R + T < S + T"
  1090 apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc)
  1091 apply (rule_tac y1 = D in preal_add_commute [THEN subst])
  1092 apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric])
  1093 done
  1094 
  1095 lemma preal_add_less2_mono2: "R < (S::preal) ==> T + R < T + S"
  1096 by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of T])
  1097 
  1098 lemma preal_add_right_less_cancel: "R + T < S + T ==> R < (S::preal)"
  1099 apply (insert linorder_less_linear [of R S], auto)
  1100 apply (drule_tac R = S and T = T in preal_add_less2_mono1)
  1101 apply (blast dest: order_less_trans) 
  1102 done
  1103 
  1104 lemma preal_add_left_less_cancel: "T + R < T + S ==> R <  (S::preal)"
  1105 by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T])
  1106 
  1107 lemma preal_add_less_cancel_right: "((R::preal) + T < S + T) = (R < S)"
  1108 by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel)
  1109 
  1110 lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)"
  1111 by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
  1112 
  1113 lemma preal_add_le_cancel_right: "((R::preal) + T \<le> S + T) = (R \<le> S)"
  1114 by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_right) 
  1115 
  1116 lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
  1117 by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left) 
  1118 
  1119 lemma preal_add_less_mono:
  1120      "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)"
  1121 apply (auto dest!: less_add_left_Ex simp add: preal_add_ac)
  1122 apply (rule preal_add_assoc [THEN subst])
  1123 apply (rule preal_self_less_add_right)
  1124 done
  1125 
  1126 lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S"
  1127 apply (insert linorder_less_linear [of R S], safe)
  1128 apply (drule_tac [!] T = T in preal_add_less2_mono1, auto)
  1129 done
  1130 
  1131 lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)"
  1132 by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
  1133 
  1134 lemma preal_add_left_cancel_iff: "(C + A = C + B) = ((A::preal) = B)"
  1135 by (fast intro: preal_add_left_cancel)
  1136 
  1137 lemma preal_add_right_cancel_iff: "(A + C = B + C) = ((A::preal) = B)"
  1138 by (fast intro: preal_add_right_cancel)
  1139 
  1140 lemmas preal_cancels =
  1141     preal_add_less_cancel_right preal_add_less_cancel_left
  1142     preal_add_le_cancel_right preal_add_le_cancel_left
  1143     preal_add_left_cancel_iff preal_add_right_cancel_iff
  1144 
  1145 
  1146 subsection{*Completeness of type @{typ preal}*}
  1147 
  1148 text{*Prove that supremum is a cut*}
  1149 
  1150 text{*Part 1 of Dedekind sections definition*}
  1151 
  1152 lemma preal_sup_set_not_empty:
  1153      "P \<noteq> {} ==> {} \<subset> (\<Union>X \<in> P. Rep_preal(X))"
  1154 apply auto
  1155 apply (cut_tac X = x in mem_Rep_preal_Ex, auto)
  1156 done
  1157 
  1158 
  1159 text{*Part 2 of Dedekind sections definition*}
  1160 
  1161 lemma preal_sup_not_exists:
  1162      "\<forall>X \<in> P. X \<le> Y ==> \<exists>q. 0 < q & q \<notin> (\<Union>X \<in> P. Rep_preal(X))"
  1163 apply (cut_tac X = Y in Rep_preal_exists_bound)
  1164 apply (auto simp add: preal_le_def)
  1165 done
  1166 
  1167 lemma preal_sup_set_not_rat_set:
  1168      "\<forall>X \<in> P. X \<le> Y ==> (\<Union>X \<in> P. Rep_preal(X)) < {r. 0 < r}"
  1169 apply (drule preal_sup_not_exists)
  1170 apply (blast intro: preal_imp_pos [OF Rep_preal])  
  1171 done
  1172 
  1173 text{*Part 3 of Dedekind sections definition*}
  1174 lemma preal_sup_set_lemma3:
  1175      "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; u \<in> (\<Union>X \<in> P. Rep_preal(X)); 0 < z; z < u|]
  1176       ==> z \<in> (\<Union>X \<in> P. Rep_preal(X))"
  1177 by (auto elim: Rep_preal [THEN preal_downwards_closed])
  1178 
  1179 text{*Part 4 of Dedekind sections definition*}
  1180 lemma preal_sup_set_lemma4:
  1181      "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; y \<in> (\<Union>X \<in> P. Rep_preal(X)) |]
  1182           ==> \<exists>u \<in> (\<Union>X \<in> P. Rep_preal(X)). y < u"
  1183 by (blast dest: Rep_preal [THEN preal_exists_greater])
  1184 
  1185 lemma preal_sup:
  1186      "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
  1187 apply (unfold preal_def cut_def)
  1188 apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
  1189                      preal_sup_set_lemma3 preal_sup_set_lemma4)
  1190 done
  1191 
  1192 lemma preal_psup_le:
  1193      "[| \<forall>X \<in> P. X \<le> Y;  x \<in> P |] ==> x \<le> psup P"
  1194 apply (simp (no_asm_simp) add: preal_le_def) 
  1195 apply (subgoal_tac "P \<noteq> {}") 
  1196 apply (auto simp add: psup_def preal_sup) 
  1197 done
  1198 
  1199 lemma psup_le_ub: "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> Y"
  1200 apply (simp (no_asm_simp) add: preal_le_def)
  1201 apply (simp add: psup_def preal_sup) 
  1202 apply (auto simp add: preal_le_def)
  1203 done
  1204 
  1205 text{*Supremum property*}
  1206 lemma preal_complete:
  1207      "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> (\<exists>X \<in> P. Z < X) = (Z < psup P)"
  1208 apply (simp add: preal_less_def psup_def preal_sup)
  1209 apply (auto simp add: preal_le_def)
  1210 apply (rename_tac U) 
  1211 apply (cut_tac x = U and y = Z in linorder_less_linear)
  1212 apply (auto simp add: preal_less_def)
  1213 done
  1214 
  1215 
  1216 subsection{*The Embadding from @{typ rat} into @{typ preal}*}
  1217 
  1218 lemma preal_of_rat_add_lemma1:
  1219      "[|x < y + z; 0 < x; 0 < y|] ==> x * y * inverse (y + z) < (y::rat)"
  1220 apply (frule_tac c = "y * inverse (y + z) " in mult_strict_right_mono)
  1221 apply (simp add: zero_less_mult_iff) 
  1222 apply (simp add: mult_ac)
  1223 done
  1224 
  1225 lemma preal_of_rat_add_lemma2:
  1226   assumes "u < x + y"
  1227       and "0 < x"
  1228       and "0 < y"
  1229       and "0 < u"
  1230   shows "\<exists>v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w"
  1231 proof (intro exI conjI)
  1232   show "u * x * inverse(x+y) < x" using prems 
  1233     by (simp add: preal_of_rat_add_lemma1) 
  1234   show "u * y * inverse(x+y) < y" using prems 
  1235     by (simp add: preal_of_rat_add_lemma1 add_commute [of x]) 
  1236   show "0 < u * x * inverse (x + y)" using prems
  1237     by (simp add: zero_less_mult_iff) 
  1238   show "0 < u * y * inverse (x + y)" using prems
  1239     by (simp add: zero_less_mult_iff) 
  1240   show "u = u * x * inverse (x + y) + u * y * inverse (x + y)" using prems
  1241     by (simp add: left_distrib [symmetric] right_distrib [symmetric] mult_ac)
  1242 qed
  1243 
  1244 lemma preal_of_rat_add:
  1245      "[| 0 < x; 0 < y|] 
  1246       ==> preal_of_rat ((x::rat) + y) = preal_of_rat x + preal_of_rat y"
  1247 apply (unfold preal_of_rat_def preal_add_def)
  1248 apply (simp add: rat_mem_preal) 
  1249 apply (rule_tac f = Abs_preal in arg_cong)
  1250 apply (auto simp add: add_set_def) 
  1251 apply (blast dest: preal_of_rat_add_lemma2) 
  1252 done
  1253 
  1254 lemma preal_of_rat_mult_lemma1:
  1255      "[|x < y; 0 < x; 0 < z|] ==> x * z * inverse y < (z::rat)"
  1256 apply (frule_tac c = "z * inverse y" in mult_strict_right_mono)
  1257 apply (simp add: zero_less_mult_iff)
  1258 apply (subgoal_tac "y * (z * inverse y) = z * (y * inverse y)")
  1259 apply (simp_all add: mult_ac)
  1260 done
  1261 
  1262 lemma preal_of_rat_mult_lemma2: 
  1263   assumes xless: "x < y * z"
  1264       and xpos: "0 < x"
  1265       and ypos: "0 < y"
  1266   shows "x * z * inverse y * inverse z < (z::rat)"
  1267 proof -
  1268   have "0 < y * z" using prems by simp
  1269   hence zpos:  "0 < z" using prems by (simp add: zero_less_mult_iff)
  1270   have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
  1271     by (simp add: mult_ac)
  1272   also have "... = x/y" using zpos
  1273     by (simp add: divide_inverse)
  1274   also have "... < z"
  1275     by (simp add: pos_divide_less_eq [OF ypos] mult_commute) 
  1276   finally show ?thesis .
  1277 qed
  1278 
  1279 lemma preal_of_rat_mult_lemma3:
  1280   assumes uless: "u < x * y"
  1281       and "0 < x"
  1282       and "0 < y"
  1283       and "0 < u"
  1284   shows "\<exists>v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w"
  1285 proof -
  1286   from dense [OF uless] 
  1287   obtain r where "u < r" "r < x * y" by blast
  1288   thus ?thesis
  1289   proof (intro exI conjI)
  1290   show "u * x * inverse r < x" using prems 
  1291     by (simp add: preal_of_rat_mult_lemma1) 
  1292   show "r * y * inverse x * inverse y < y" using prems
  1293     by (simp add: preal_of_rat_mult_lemma2)
  1294   show "0 < u * x * inverse r" using prems
  1295     by (simp add: zero_less_mult_iff) 
  1296   show "0 < r * y * inverse x * inverse y" using prems
  1297     by (simp add: zero_less_mult_iff) 
  1298   have "u * x * inverse r * (r * y * inverse x * inverse y) =
  1299         u * (r * inverse r) * (x * inverse x) * (y * inverse y)"
  1300     by (simp only: mult_ac)
  1301   thus "u = u * x * inverse r * (r * y * inverse x * inverse y)" using prems
  1302     by simp
  1303   qed
  1304 qed
  1305 
  1306 lemma preal_of_rat_mult:
  1307      "[| 0 < x; 0 < y|] 
  1308       ==> preal_of_rat ((x::rat) * y) = preal_of_rat x * preal_of_rat y"
  1309 apply (unfold preal_of_rat_def preal_mult_def)
  1310 apply (simp add: rat_mem_preal) 
  1311 apply (rule_tac f = Abs_preal in arg_cong)
  1312 apply (auto simp add: zero_less_mult_iff mult_strict_mono mult_set_def) 
  1313 apply (blast dest: preal_of_rat_mult_lemma3) 
  1314 done
  1315 
  1316 lemma preal_of_rat_less_iff:
  1317       "[| 0 < x; 0 < y|] ==> (preal_of_rat x < preal_of_rat y) = (x < y)"
  1318 by (force simp add: preal_of_rat_def preal_less_def rat_mem_preal) 
  1319 
  1320 lemma preal_of_rat_le_iff:
  1321       "[| 0 < x; 0 < y|] ==> (preal_of_rat x \<le> preal_of_rat y) = (x \<le> y)"
  1322 by (simp add: preal_of_rat_less_iff linorder_not_less [symmetric]) 
  1323 
  1324 lemma preal_of_rat_eq_iff:
  1325       "[| 0 < x; 0 < y|] ==> (preal_of_rat x = preal_of_rat y) = (x = y)"
  1326 by (simp add: preal_of_rat_le_iff order_eq_iff) 
  1327 
  1328 
  1329 ML
  1330 {*
  1331 val inj_on_Abs_preal = thm"inj_on_Abs_preal";
  1332 val inj_Rep_preal = thm"inj_Rep_preal";
  1333 val mem_Rep_preal_Ex = thm"mem_Rep_preal_Ex";
  1334 val preal_add_commute = thm"preal_add_commute";
  1335 val preal_add_assoc = thm"preal_add_assoc";
  1336 val preal_add_left_commute = thm"preal_add_left_commute";
  1337 val preal_mult_commute = thm"preal_mult_commute";
  1338 val preal_mult_assoc = thm"preal_mult_assoc";
  1339 val preal_mult_left_commute = thm"preal_mult_left_commute";
  1340 val preal_add_mult_distrib2 = thm"preal_add_mult_distrib2";
  1341 val preal_add_mult_distrib = thm"preal_add_mult_distrib";
  1342 val preal_self_less_add_left = thm"preal_self_less_add_left";
  1343 val preal_self_less_add_right = thm"preal_self_less_add_right";
  1344 val less_add_left = thm"less_add_left";
  1345 val preal_add_less2_mono1 = thm"preal_add_less2_mono1";
  1346 val preal_add_less2_mono2 = thm"preal_add_less2_mono2";
  1347 val preal_add_right_less_cancel = thm"preal_add_right_less_cancel";
  1348 val preal_add_left_less_cancel = thm"preal_add_left_less_cancel";
  1349 val preal_add_right_cancel = thm"preal_add_right_cancel";
  1350 val preal_add_left_cancel = thm"preal_add_left_cancel";
  1351 val preal_add_left_cancel_iff = thm"preal_add_left_cancel_iff";
  1352 val preal_add_right_cancel_iff = thm"preal_add_right_cancel_iff";
  1353 val preal_psup_le = thm"preal_psup_le";
  1354 val psup_le_ub = thm"psup_le_ub";
  1355 val preal_complete = thm"preal_complete";
  1356 val preal_of_rat_add = thm"preal_of_rat_add";
  1357 val preal_of_rat_mult = thm"preal_of_rat_mult";
  1358 
  1359 val preal_add_ac = thms"preal_add_ac";
  1360 val preal_mult_ac = thms"preal_mult_ac";
  1361 *}
  1362 
  1363 end