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