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