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