src/HOL/PReal.thy
changeset 28952 15a4b2cf8c34
parent 28945 da79ac67794b
child 29197 6d4cb27ed19c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/PReal.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,1343 @@
     1.4 +(*  Title       : PReal.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : The positive reals as Dedekind sections of positive
     1.8 +         rationals. Fundamentals of Abstract Analysis [Gleason- p. 121]
     1.9 +                  provides some of the definitions.
    1.10 +*)
    1.11 +
    1.12 +header {* Positive real numbers *}
    1.13 +
    1.14 +theory PReal
    1.15 +imports Rational "~~/src/HOL/Library/Dense_Linear_Order"
    1.16 +begin
    1.17 +
    1.18 +text{*Could be generalized and moved to @{text Ring_and_Field}*}
    1.19 +lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"
    1.20 +by (rule_tac x="b-a" in exI, simp)
    1.21 +
    1.22 +definition
    1.23 +  cut :: "rat set => bool" where
    1.24 +  [code del]: "cut A = ({} \<subset> A &
    1.25 +            A < {r. 0 < r} &
    1.26 +            (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
    1.27 +
    1.28 +lemma cut_of_rat: 
    1.29 +  assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A")
    1.30 +proof -
    1.31 +  from q have pos: "?A < {r. 0 < r}" by force
    1.32 +  have nonempty: "{} \<subset> ?A"
    1.33 +  proof
    1.34 +    show "{} \<subseteq> ?A" by simp
    1.35 +    show "{} \<noteq> ?A"
    1.36 +      by (force simp only: q eq_commute [of "{}"] interval_empty_iff)
    1.37 +  qed
    1.38 +  show ?thesis
    1.39 +    by (simp add: cut_def pos nonempty,
    1.40 +        blast dest: dense intro: order_less_trans)
    1.41 +qed
    1.42 +
    1.43 +
    1.44 +typedef preal = "{A. cut A}"
    1.45 +  by (blast intro: cut_of_rat [OF zero_less_one])
    1.46 +
    1.47 +definition
    1.48 +  preal_of_rat :: "rat => preal" where
    1.49 +  "preal_of_rat q = Abs_preal {x::rat. 0 < x & x < q}"
    1.50 +
    1.51 +definition
    1.52 +  psup :: "preal set => preal" where
    1.53 +  "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
    1.54 +
    1.55 +definition
    1.56 +  add_set :: "[rat set,rat set] => rat set" where
    1.57 +  "add_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
    1.58 +
    1.59 +definition
    1.60 +  diff_set :: "[rat set,rat set] => rat set" where
    1.61 +  [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
    1.62 +
    1.63 +definition
    1.64 +  mult_set :: "[rat set,rat set] => rat set" where
    1.65 +  "mult_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
    1.66 +
    1.67 +definition
    1.68 +  inverse_set :: "rat set => rat set" where
    1.69 +  [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
    1.70 +
    1.71 +instantiation preal :: "{ord, plus, minus, times, inverse, one}"
    1.72 +begin
    1.73 +
    1.74 +definition
    1.75 +  preal_less_def [code del]:
    1.76 +    "R < S == Rep_preal R < Rep_preal S"
    1.77 +
    1.78 +definition
    1.79 +  preal_le_def [code del]:
    1.80 +    "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
    1.81 +
    1.82 +definition
    1.83 +  preal_add_def:
    1.84 +    "R + S == Abs_preal (add_set (Rep_preal R) (Rep_preal S))"
    1.85 +
    1.86 +definition
    1.87 +  preal_diff_def:
    1.88 +    "R - S == Abs_preal (diff_set (Rep_preal R) (Rep_preal S))"
    1.89 +
    1.90 +definition
    1.91 +  preal_mult_def:
    1.92 +    "R * S == Abs_preal (mult_set (Rep_preal R) (Rep_preal S))"
    1.93 +
    1.94 +definition
    1.95 +  preal_inverse_def:
    1.96 +    "inverse R == Abs_preal (inverse_set (Rep_preal R))"
    1.97 +
    1.98 +definition "R / S = R * inverse (S\<Colon>preal)"
    1.99 +
   1.100 +definition
   1.101 +  preal_one_def:
   1.102 +    "1 == preal_of_rat 1"
   1.103 +
   1.104 +instance ..
   1.105 +
   1.106 +end
   1.107 +
   1.108 +
   1.109 +text{*Reduces equality on abstractions to equality on representatives*}
   1.110 +declare Abs_preal_inject [simp]
   1.111 +declare Abs_preal_inverse [simp]
   1.112 +
   1.113 +lemma rat_mem_preal: "0 < q ==> {r::rat. 0 < r & r < q} \<in> preal"
   1.114 +by (simp add: preal_def cut_of_rat)
   1.115 +
   1.116 +lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
   1.117 +by (unfold preal_def cut_def, blast)
   1.118 +
   1.119 +lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
   1.120 +by (drule preal_nonempty, fast)
   1.121 +
   1.122 +lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
   1.123 +by (force simp add: preal_def cut_def)
   1.124 +
   1.125 +lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
   1.126 +by (drule preal_imp_psubset_positives, auto)
   1.127 +
   1.128 +lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
   1.129 +by (unfold preal_def cut_def, blast)
   1.130 +
   1.131 +lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
   1.132 +by (unfold preal_def cut_def, blast)
   1.133 +
   1.134 +text{*Relaxing the final premise*}
   1.135 +lemma preal_downwards_closed':
   1.136 +     "[| A \<in> preal; y \<in> A; 0 < z; z \<le> y |] ==> z \<in> A"
   1.137 +apply (simp add: order_le_less)
   1.138 +apply (blast intro: preal_downwards_closed)
   1.139 +done
   1.140 +
   1.141 +text{*A positive fraction not in a positive real is an upper bound.
   1.142 + Gleason p. 122 - Remark (1)*}
   1.143 +
   1.144 +lemma not_in_preal_ub:
   1.145 +  assumes A: "A \<in> preal"
   1.146 +    and notx: "x \<notin> A"
   1.147 +    and y: "y \<in> A"
   1.148 +    and pos: "0 < x"
   1.149 +  shows "y < x"
   1.150 +proof (cases rule: linorder_cases)
   1.151 +  assume "x<y"
   1.152 +  with notx show ?thesis
   1.153 +    by (simp add:  preal_downwards_closed [OF A y] pos)
   1.154 +next
   1.155 +  assume "x=y"
   1.156 +  with notx and y show ?thesis by simp
   1.157 +next
   1.158 +  assume "y<x"
   1.159 +  thus ?thesis .
   1.160 +qed
   1.161 +
   1.162 +text {* preal lemmas instantiated to @{term "Rep_preal X"} *}
   1.163 +
   1.164 +lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X"
   1.165 +by (rule preal_Ex_mem [OF Rep_preal])
   1.166 +
   1.167 +lemma Rep_preal_exists_bound: "\<exists>x>0. x \<notin> Rep_preal X"
   1.168 +by (rule preal_exists_bound [OF Rep_preal])
   1.169 +
   1.170 +lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal]
   1.171 +
   1.172 +
   1.173 +
   1.174 +subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
   1.175 +
   1.176 +lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal"
   1.177 +by (simp add: preal_def cut_of_rat)
   1.178 +
   1.179 +lemma rat_subset_imp_le:
   1.180 +     "[|{u::rat. 0 < u & u < x} \<subseteq> {u. 0 < u & u < y}; 0<x|] ==> x \<le> y"
   1.181 +apply (simp add: linorder_not_less [symmetric])
   1.182 +apply (blast dest: dense intro: order_less_trans)
   1.183 +done
   1.184 +
   1.185 +lemma rat_set_eq_imp_eq:
   1.186 +     "[|{u::rat. 0 < u & u < x} = {u. 0 < u & u < y};
   1.187 +        0 < x; 0 < y|] ==> x = y"
   1.188 +by (blast intro: rat_subset_imp_le order_antisym)
   1.189 +
   1.190 +
   1.191 +
   1.192 +subsection{*Properties of Ordering*}
   1.193 +
   1.194 +instance preal :: order
   1.195 +proof
   1.196 +  fix w :: preal
   1.197 +  show "w \<le> w" by (simp add: preal_le_def)
   1.198 +next
   1.199 +  fix i j k :: preal
   1.200 +  assume "i \<le> j" and "j \<le> k"
   1.201 +  then show "i \<le> k" by (simp add: preal_le_def)
   1.202 +next
   1.203 +  fix z w :: preal
   1.204 +  assume "z \<le> w" and "w \<le> z"
   1.205 +  then show "z = w" by (simp add: preal_le_def Rep_preal_inject)
   1.206 +next
   1.207 +  fix z w :: preal
   1.208 +  show "z < w \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
   1.209 +  by (auto simp add: preal_le_def preal_less_def Rep_preal_inject)
   1.210 +qed  
   1.211 +
   1.212 +lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
   1.213 +by (insert preal_imp_psubset_positives, blast)
   1.214 +
   1.215 +instance preal :: linorder
   1.216 +proof
   1.217 +  fix x y :: preal
   1.218 +  show "x <= y | y <= x"
   1.219 +    apply (auto simp add: preal_le_def)
   1.220 +    apply (rule ccontr)
   1.221 +    apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
   1.222 +             elim: order_less_asym)
   1.223 +    done
   1.224 +qed
   1.225 +
   1.226 +instantiation preal :: distrib_lattice
   1.227 +begin
   1.228 +
   1.229 +definition
   1.230 +  "(inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = min"
   1.231 +
   1.232 +definition
   1.233 +  "(sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = max"
   1.234 +
   1.235 +instance
   1.236 +  by intro_classes
   1.237 +    (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
   1.238 +
   1.239 +end
   1.240 +
   1.241 +subsection{*Properties of Addition*}
   1.242 +
   1.243 +lemma preal_add_commute: "(x::preal) + y = y + x"
   1.244 +apply (unfold preal_add_def add_set_def)
   1.245 +apply (rule_tac f = Abs_preal in arg_cong)
   1.246 +apply (force simp add: add_commute)
   1.247 +done
   1.248 +
   1.249 +text{*Lemmas for proving that addition of two positive reals gives
   1.250 + a positive real*}
   1.251 +
   1.252 +lemma empty_psubset_nonempty: "a \<in> A ==> {} \<subset> A"
   1.253 +by blast
   1.254 +
   1.255 +text{*Part 1 of Dedekind sections definition*}
   1.256 +lemma add_set_not_empty:
   1.257 +     "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> add_set A B"
   1.258 +apply (drule preal_nonempty)+
   1.259 +apply (auto simp add: add_set_def)
   1.260 +done
   1.261 +
   1.262 +text{*Part 2 of Dedekind sections definition.  A structured version of
   1.263 +this proof is @{text preal_not_mem_mult_set_Ex} below.*}
   1.264 +lemma preal_not_mem_add_set_Ex:
   1.265 +     "[|A \<in> preal; B \<in> preal|] ==> \<exists>q>0. q \<notin> add_set A B"
   1.266 +apply (insert preal_exists_bound [of A] preal_exists_bound [of B], auto) 
   1.267 +apply (rule_tac x = "x+xa" in exI)
   1.268 +apply (simp add: add_set_def, clarify)
   1.269 +apply (drule (3) not_in_preal_ub)+
   1.270 +apply (force dest: add_strict_mono)
   1.271 +done
   1.272 +
   1.273 +lemma add_set_not_rat_set:
   1.274 +   assumes A: "A \<in> preal" 
   1.275 +       and B: "B \<in> preal"
   1.276 +     shows "add_set A B < {r. 0 < r}"
   1.277 +proof
   1.278 +  from preal_imp_pos [OF A] preal_imp_pos [OF B]
   1.279 +  show "add_set A B \<subseteq> {r. 0 < r}" by (force simp add: add_set_def) 
   1.280 +next
   1.281 +  show "add_set A B \<noteq> {r. 0 < r}"
   1.282 +    by (insert preal_not_mem_add_set_Ex [OF A B], blast) 
   1.283 +qed
   1.284 +
   1.285 +text{*Part 3 of Dedekind sections definition*}
   1.286 +lemma add_set_lemma3:
   1.287 +     "[|A \<in> preal; B \<in> preal; u \<in> add_set A B; 0 < z; z < u|] 
   1.288 +      ==> z \<in> add_set A B"
   1.289 +proof (unfold add_set_def, clarify)
   1.290 +  fix x::rat and y::rat
   1.291 +  assume A: "A \<in> preal" 
   1.292 +    and B: "B \<in> preal"
   1.293 +    and [simp]: "0 < z"
   1.294 +    and zless: "z < x + y"
   1.295 +    and x:  "x \<in> A"
   1.296 +    and y:  "y \<in> B"
   1.297 +  have xpos [simp]: "0<x" by (rule preal_imp_pos [OF A x])
   1.298 +  have ypos [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   1.299 +  have xypos [simp]: "0 < x+y" by (simp add: pos_add_strict)
   1.300 +  let ?f = "z/(x+y)"
   1.301 +  have fless: "?f < 1" by (simp add: zless pos_divide_less_eq)
   1.302 +  show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
   1.303 +  proof (intro bexI)
   1.304 +    show "z = x*?f + y*?f"
   1.305 +      by (simp add: left_distrib [symmetric] divide_inverse mult_ac
   1.306 +          order_less_imp_not_eq2)
   1.307 +  next
   1.308 +    show "y * ?f \<in> B"
   1.309 +    proof (rule preal_downwards_closed [OF B y])
   1.310 +      show "0 < y * ?f"
   1.311 +        by (simp add: divide_inverse zero_less_mult_iff)
   1.312 +    next
   1.313 +      show "y * ?f < y"
   1.314 +        by (insert mult_strict_left_mono [OF fless ypos], simp)
   1.315 +    qed
   1.316 +  next
   1.317 +    show "x * ?f \<in> A"
   1.318 +    proof (rule preal_downwards_closed [OF A x])
   1.319 +      show "0 < x * ?f"
   1.320 +	by (simp add: divide_inverse zero_less_mult_iff)
   1.321 +    next
   1.322 +      show "x * ?f < x"
   1.323 +	by (insert mult_strict_left_mono [OF fless xpos], simp)
   1.324 +    qed
   1.325 +  qed
   1.326 +qed
   1.327 +
   1.328 +text{*Part 4 of Dedekind sections definition*}
   1.329 +lemma add_set_lemma4:
   1.330 +     "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
   1.331 +apply (auto simp add: add_set_def)
   1.332 +apply (frule preal_exists_greater [of A], auto) 
   1.333 +apply (rule_tac x="u + y" in exI)
   1.334 +apply (auto intro: add_strict_left_mono)
   1.335 +done
   1.336 +
   1.337 +lemma mem_add_set:
   1.338 +     "[|A \<in> preal; B \<in> preal|] ==> add_set A B \<in> preal"
   1.339 +apply (simp (no_asm_simp) add: preal_def cut_def)
   1.340 +apply (blast intro!: add_set_not_empty add_set_not_rat_set
   1.341 +                     add_set_lemma3 add_set_lemma4)
   1.342 +done
   1.343 +
   1.344 +lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
   1.345 +apply (simp add: preal_add_def mem_add_set Rep_preal)
   1.346 +apply (force simp add: add_set_def add_ac)
   1.347 +done
   1.348 +
   1.349 +instance preal :: ab_semigroup_add
   1.350 +proof
   1.351 +  fix a b c :: preal
   1.352 +  show "(a + b) + c = a + (b + c)" by (rule preal_add_assoc)
   1.353 +  show "a + b = b + a" by (rule preal_add_commute)
   1.354 +qed
   1.355 +
   1.356 +lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
   1.357 +by (rule add_left_commute)
   1.358 +
   1.359 +text{* Positive Real addition is an AC operator *}
   1.360 +lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
   1.361 +
   1.362 +
   1.363 +subsection{*Properties of Multiplication*}
   1.364 +
   1.365 +text{*Proofs essentially same as for addition*}
   1.366 +
   1.367 +lemma preal_mult_commute: "(x::preal) * y = y * x"
   1.368 +apply (unfold preal_mult_def mult_set_def)
   1.369 +apply (rule_tac f = Abs_preal in arg_cong)
   1.370 +apply (force simp add: mult_commute)
   1.371 +done
   1.372 +
   1.373 +text{*Multiplication of two positive reals gives a positive real.*}
   1.374 +
   1.375 +text{*Lemmas for proving positive reals multiplication set in @{typ preal}*}
   1.376 +
   1.377 +text{*Part 1 of Dedekind sections definition*}
   1.378 +lemma mult_set_not_empty:
   1.379 +     "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> mult_set A B"
   1.380 +apply (insert preal_nonempty [of A] preal_nonempty [of B]) 
   1.381 +apply (auto simp add: mult_set_def)
   1.382 +done
   1.383 +
   1.384 +text{*Part 2 of Dedekind sections definition*}
   1.385 +lemma preal_not_mem_mult_set_Ex:
   1.386 +   assumes A: "A \<in> preal" 
   1.387 +       and B: "B \<in> preal"
   1.388 +     shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
   1.389 +proof -
   1.390 +  from preal_exists_bound [OF A]
   1.391 +  obtain x where [simp]: "0 < x" "x \<notin> A" by blast
   1.392 +  from preal_exists_bound [OF B]
   1.393 +  obtain y where [simp]: "0 < y" "y \<notin> B" by blast
   1.394 +  show ?thesis
   1.395 +  proof (intro exI conjI)
   1.396 +    show "0 < x*y" by (simp add: mult_pos_pos)
   1.397 +    show "x * y \<notin> mult_set A B"
   1.398 +    proof -
   1.399 +      { fix u::rat and v::rat
   1.400 +	      assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
   1.401 +	      moreover
   1.402 +	      with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
   1.403 +	      moreover
   1.404 +	      with prems have "0\<le>v"
   1.405 +	        by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
   1.406 +	      moreover
   1.407 +        from calculation
   1.408 +	      have "u*v < x*y" by (blast intro: mult_strict_mono prems)
   1.409 +	      ultimately have False by force }
   1.410 +      thus ?thesis by (auto simp add: mult_set_def)
   1.411 +    qed
   1.412 +  qed
   1.413 +qed
   1.414 +
   1.415 +lemma mult_set_not_rat_set:
   1.416 +  assumes A: "A \<in> preal" 
   1.417 +    and B: "B \<in> preal"
   1.418 +  shows "mult_set A B < {r. 0 < r}"
   1.419 +proof
   1.420 +  show "mult_set A B \<subseteq> {r. 0 < r}"
   1.421 +    by (force simp add: mult_set_def
   1.422 +      intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos)
   1.423 +  show "mult_set A B \<noteq> {r. 0 < r}"
   1.424 +    using preal_not_mem_mult_set_Ex [OF A B] by blast
   1.425 +qed
   1.426 +
   1.427 +
   1.428 +
   1.429 +text{*Part 3 of Dedekind sections definition*}
   1.430 +lemma mult_set_lemma3:
   1.431 +     "[|A \<in> preal; B \<in> preal; u \<in> mult_set A B; 0 < z; z < u|] 
   1.432 +      ==> z \<in> mult_set A B"
   1.433 +proof (unfold mult_set_def, clarify)
   1.434 +  fix x::rat and y::rat
   1.435 +  assume A: "A \<in> preal" 
   1.436 +    and B: "B \<in> preal"
   1.437 +    and [simp]: "0 < z"
   1.438 +    and zless: "z < x * y"
   1.439 +    and x:  "x \<in> A"
   1.440 +    and y:  "y \<in> B"
   1.441 +  have [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   1.442 +  show "\<exists>x' \<in> A. \<exists>y' \<in> B. z = x' * y'"
   1.443 +  proof
   1.444 +    show "\<exists>y'\<in>B. z = (z/y) * y'"
   1.445 +    proof
   1.446 +      show "z = (z/y)*y"
   1.447 +	by (simp add: divide_inverse mult_commute [of y] mult_assoc
   1.448 +		      order_less_imp_not_eq2)
   1.449 +      show "y \<in> B" by fact
   1.450 +    qed
   1.451 +  next
   1.452 +    show "z/y \<in> A"
   1.453 +    proof (rule preal_downwards_closed [OF A x])
   1.454 +      show "0 < z/y"
   1.455 +	by (simp add: zero_less_divide_iff)
   1.456 +      show "z/y < x" by (simp add: pos_divide_less_eq zless)
   1.457 +    qed
   1.458 +  qed
   1.459 +qed
   1.460 +
   1.461 +text{*Part 4 of Dedekind sections definition*}
   1.462 +lemma mult_set_lemma4:
   1.463 +     "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
   1.464 +apply (auto simp add: mult_set_def)
   1.465 +apply (frule preal_exists_greater [of A], auto) 
   1.466 +apply (rule_tac x="u * y" in exI)
   1.467 +apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B] 
   1.468 +                   mult_strict_right_mono)
   1.469 +done
   1.470 +
   1.471 +
   1.472 +lemma mem_mult_set:
   1.473 +     "[|A \<in> preal; B \<in> preal|] ==> mult_set A B \<in> preal"
   1.474 +apply (simp (no_asm_simp) add: preal_def cut_def)
   1.475 +apply (blast intro!: mult_set_not_empty mult_set_not_rat_set
   1.476 +                     mult_set_lemma3 mult_set_lemma4)
   1.477 +done
   1.478 +
   1.479 +lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
   1.480 +apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   1.481 +apply (force simp add: mult_set_def mult_ac)
   1.482 +done
   1.483 +
   1.484 +instance preal :: ab_semigroup_mult
   1.485 +proof
   1.486 +  fix a b c :: preal
   1.487 +  show "(a * b) * c = a * (b * c)" by (rule preal_mult_assoc)
   1.488 +  show "a * b = b * a" by (rule preal_mult_commute)
   1.489 +qed
   1.490 +
   1.491 +lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
   1.492 +by (rule mult_left_commute)
   1.493 +
   1.494 +
   1.495 +text{* Positive Real multiplication is an AC operator *}
   1.496 +lemmas preal_mult_ac =
   1.497 +       preal_mult_assoc preal_mult_commute preal_mult_left_commute
   1.498 +
   1.499 +
   1.500 +text{* Positive real 1 is the multiplicative identity element *}
   1.501 +
   1.502 +lemma preal_mult_1: "(1::preal) * z = z"
   1.503 +unfolding preal_one_def
   1.504 +proof (induct z)
   1.505 +  fix A :: "rat set"
   1.506 +  assume A: "A \<in> preal"
   1.507 +  have "{w. \<exists>u. 0 < u \<and> u < 1 & (\<exists>v \<in> A. w = u * v)} = A" (is "?lhs = A")
   1.508 +  proof
   1.509 +    show "?lhs \<subseteq> A"
   1.510 +    proof clarify
   1.511 +      fix x::rat and u::rat and v::rat
   1.512 +      assume upos: "0<u" and "u<1" and v: "v \<in> A"
   1.513 +      have vpos: "0<v" by (rule preal_imp_pos [OF A v])
   1.514 +      hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
   1.515 +      thus "u * v \<in> A"
   1.516 +        by (force intro: preal_downwards_closed [OF A v] mult_pos_pos 
   1.517 +          upos vpos)
   1.518 +    qed
   1.519 +  next
   1.520 +    show "A \<subseteq> ?lhs"
   1.521 +    proof clarify
   1.522 +      fix x::rat
   1.523 +      assume x: "x \<in> A"
   1.524 +      have xpos: "0<x" by (rule preal_imp_pos [OF A x])
   1.525 +      from preal_exists_greater [OF A x]
   1.526 +      obtain v where v: "v \<in> A" and xlessv: "x < v" ..
   1.527 +      have vpos: "0<v" by (rule preal_imp_pos [OF A v])
   1.528 +      show "\<exists>u. 0 < u \<and> u < 1 \<and> (\<exists>v\<in>A. x = u * v)"
   1.529 +      proof (intro exI conjI)
   1.530 +        show "0 < x/v"
   1.531 +          by (simp add: zero_less_divide_iff xpos vpos)
   1.532 +	show "x / v < 1"
   1.533 +          by (simp add: pos_divide_less_eq vpos xlessv)
   1.534 +        show "\<exists>v'\<in>A. x = (x / v) * v'"
   1.535 +        proof
   1.536 +          show "x = (x/v)*v"
   1.537 +	    by (simp add: divide_inverse mult_assoc vpos
   1.538 +                          order_less_imp_not_eq2)
   1.539 +          show "v \<in> A" by fact
   1.540 +        qed
   1.541 +      qed
   1.542 +    qed
   1.543 +  qed
   1.544 +  thus "preal_of_rat 1 * Abs_preal A = Abs_preal A"
   1.545 +    by (simp add: preal_of_rat_def preal_mult_def mult_set_def 
   1.546 +                  rat_mem_preal A)
   1.547 +qed
   1.548 +
   1.549 +instance preal :: comm_monoid_mult
   1.550 +by intro_classes (rule preal_mult_1)
   1.551 +
   1.552 +lemma preal_mult_1_right: "z * (1::preal) = z"
   1.553 +by (rule mult_1_right)
   1.554 +
   1.555 +
   1.556 +subsection{*Distribution of Multiplication across Addition*}
   1.557 +
   1.558 +lemma mem_Rep_preal_add_iff:
   1.559 +      "(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x + y)"
   1.560 +apply (simp add: preal_add_def mem_add_set Rep_preal)
   1.561 +apply (simp add: add_set_def) 
   1.562 +done
   1.563 +
   1.564 +lemma mem_Rep_preal_mult_iff:
   1.565 +      "(z \<in> Rep_preal(R*S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x * y)"
   1.566 +apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   1.567 +apply (simp add: mult_set_def) 
   1.568 +done
   1.569 +
   1.570 +lemma distrib_subset1:
   1.571 +     "Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)"
   1.572 +apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
   1.573 +apply (force simp add: right_distrib)
   1.574 +done
   1.575 +
   1.576 +lemma preal_add_mult_distrib_mean:
   1.577 +  assumes a: "a \<in> Rep_preal w"
   1.578 +    and b: "b \<in> Rep_preal w"
   1.579 +    and d: "d \<in> Rep_preal x"
   1.580 +    and e: "e \<in> Rep_preal y"
   1.581 +  shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
   1.582 +proof
   1.583 +  let ?c = "(a*d + b*e)/(d+e)"
   1.584 +  have [simp]: "0<a" "0<b" "0<d" "0<e" "0<d+e"
   1.585 +    by (blast intro: preal_imp_pos [OF Rep_preal] a b d e pos_add_strict)+
   1.586 +  have cpos: "0 < ?c"
   1.587 +    by (simp add: zero_less_divide_iff zero_less_mult_iff pos_add_strict)
   1.588 +  show "a * d + b * e = ?c * (d + e)"
   1.589 +    by (simp add: divide_inverse mult_assoc order_less_imp_not_eq2)
   1.590 +  show "?c \<in> Rep_preal w"
   1.591 +  proof (cases rule: linorder_le_cases)
   1.592 +    assume "a \<le> b"
   1.593 +    hence "?c \<le> b"
   1.594 +      by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   1.595 +                    order_less_imp_le)
   1.596 +    thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos])
   1.597 +  next
   1.598 +    assume "b \<le> a"
   1.599 +    hence "?c \<le> a"
   1.600 +      by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   1.601 +                    order_less_imp_le)
   1.602 +    thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos])
   1.603 +  qed
   1.604 +qed
   1.605 +
   1.606 +lemma distrib_subset2:
   1.607 +     "Rep_preal (w * x + w * y) \<subseteq> Rep_preal (w * (x + y))"
   1.608 +apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
   1.609 +apply (drule_tac w=w and x=x and y=y in preal_add_mult_distrib_mean, auto)
   1.610 +done
   1.611 +
   1.612 +lemma preal_add_mult_distrib2: "(w * ((x::preal) + y)) = (w * x) + (w * y)"
   1.613 +apply (rule Rep_preal_inject [THEN iffD1])
   1.614 +apply (rule equalityI [OF distrib_subset1 distrib_subset2])
   1.615 +done
   1.616 +
   1.617 +lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)"
   1.618 +by (simp add: preal_mult_commute preal_add_mult_distrib2)
   1.619 +
   1.620 +instance preal :: comm_semiring
   1.621 +by intro_classes (rule preal_add_mult_distrib)
   1.622 +
   1.623 +
   1.624 +subsection{*Existence of Inverse, a Positive Real*}
   1.625 +
   1.626 +lemma mem_inv_set_ex:
   1.627 +  assumes A: "A \<in> preal" shows "\<exists>x y. 0 < x & x < y & inverse y \<notin> A"
   1.628 +proof -
   1.629 +  from preal_exists_bound [OF A]
   1.630 +  obtain x where [simp]: "0<x" "x \<notin> A" by blast
   1.631 +  show ?thesis
   1.632 +  proof (intro exI conjI)
   1.633 +    show "0 < inverse (x+1)"
   1.634 +      by (simp add: order_less_trans [OF _ less_add_one]) 
   1.635 +    show "inverse(x+1) < inverse x"
   1.636 +      by (simp add: less_imp_inverse_less less_add_one)
   1.637 +    show "inverse (inverse x) \<notin> A"
   1.638 +      by (simp add: order_less_imp_not_eq2)
   1.639 +  qed
   1.640 +qed
   1.641 +
   1.642 +text{*Part 1 of Dedekind sections definition*}
   1.643 +lemma inverse_set_not_empty:
   1.644 +     "A \<in> preal ==> {} \<subset> inverse_set A"
   1.645 +apply (insert mem_inv_set_ex [of A])
   1.646 +apply (auto simp add: inverse_set_def)
   1.647 +done
   1.648 +
   1.649 +text{*Part 2 of Dedekind sections definition*}
   1.650 +
   1.651 +lemma preal_not_mem_inverse_set_Ex:
   1.652 +   assumes A: "A \<in> preal"  shows "\<exists>q. 0 < q & q \<notin> inverse_set A"
   1.653 +proof -
   1.654 +  from preal_nonempty [OF A]
   1.655 +  obtain x where x: "x \<in> A" and  xpos [simp]: "0<x" ..
   1.656 +  show ?thesis
   1.657 +  proof (intro exI conjI)
   1.658 +    show "0 < inverse x" by simp
   1.659 +    show "inverse x \<notin> inverse_set A"
   1.660 +    proof -
   1.661 +      { fix y::rat 
   1.662 +	assume ygt: "inverse x < y"
   1.663 +	have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
   1.664 +	have iyless: "inverse y < x" 
   1.665 +	  by (simp add: inverse_less_imp_less [of x] ygt)
   1.666 +	have "inverse y \<in> A"
   1.667 +	  by (simp add: preal_downwards_closed [OF A x] iyless)}
   1.668 +     thus ?thesis by (auto simp add: inverse_set_def)
   1.669 +    qed
   1.670 +  qed
   1.671 +qed
   1.672 +
   1.673 +lemma inverse_set_not_rat_set:
   1.674 +   assumes A: "A \<in> preal"  shows "inverse_set A < {r. 0 < r}"
   1.675 +proof
   1.676 +  show "inverse_set A \<subseteq> {r. 0 < r}"  by (force simp add: inverse_set_def)
   1.677 +next
   1.678 +  show "inverse_set A \<noteq> {r. 0 < r}"
   1.679 +    by (insert preal_not_mem_inverse_set_Ex [OF A], blast)
   1.680 +qed
   1.681 +
   1.682 +text{*Part 3 of Dedekind sections definition*}
   1.683 +lemma inverse_set_lemma3:
   1.684 +     "[|A \<in> preal; u \<in> inverse_set A; 0 < z; z < u|] 
   1.685 +      ==> z \<in> inverse_set A"
   1.686 +apply (auto simp add: inverse_set_def)
   1.687 +apply (auto intro: order_less_trans)
   1.688 +done
   1.689 +
   1.690 +text{*Part 4 of Dedekind sections definition*}
   1.691 +lemma inverse_set_lemma4:
   1.692 +     "[|A \<in> preal; y \<in> inverse_set A|] ==> \<exists>u \<in> inverse_set A. y < u"
   1.693 +apply (auto simp add: inverse_set_def)
   1.694 +apply (drule dense [of y]) 
   1.695 +apply (blast intro: order_less_trans)
   1.696 +done
   1.697 +
   1.698 +
   1.699 +lemma mem_inverse_set:
   1.700 +     "A \<in> preal ==> inverse_set A \<in> preal"
   1.701 +apply (simp (no_asm_simp) add: preal_def cut_def)
   1.702 +apply (blast intro!: inverse_set_not_empty inverse_set_not_rat_set
   1.703 +                     inverse_set_lemma3 inverse_set_lemma4)
   1.704 +done
   1.705 +
   1.706 +
   1.707 +subsection{*Gleason's Lemma 9-3.4, page 122*}
   1.708 +
   1.709 +lemma Gleason9_34_exists:
   1.710 +  assumes A: "A \<in> preal"
   1.711 +    and "\<forall>x\<in>A. x + u \<in> A"
   1.712 +    and "0 \<le> z"
   1.713 +  shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
   1.714 +proof (cases z rule: int_cases)
   1.715 +  case (nonneg n)
   1.716 +  show ?thesis
   1.717 +  proof (simp add: prems, induct n)
   1.718 +    case 0
   1.719 +      from preal_nonempty [OF A]
   1.720 +      show ?case  by force 
   1.721 +    case (Suc k)
   1.722 +      from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
   1.723 +      hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
   1.724 +      thus ?case by (force simp add: left_distrib add_ac prems) 
   1.725 +  qed
   1.726 +next
   1.727 +  case (neg n)
   1.728 +  with prems show ?thesis by simp
   1.729 +qed
   1.730 +
   1.731 +lemma Gleason9_34_contra:
   1.732 +  assumes A: "A \<in> preal"
   1.733 +    shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
   1.734 +proof (induct u, induct y)
   1.735 +  fix a::int and b::int
   1.736 +  fix c::int and d::int
   1.737 +  assume bpos [simp]: "0 < b"
   1.738 +    and dpos [simp]: "0 < d"
   1.739 +    and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
   1.740 +    and upos: "0 < Fract c d"
   1.741 +    and ypos: "0 < Fract a b"
   1.742 +    and notin: "Fract a b \<notin> A"
   1.743 +  have cpos [simp]: "0 < c" 
   1.744 +    by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos) 
   1.745 +  have apos [simp]: "0 < a" 
   1.746 +    by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos) 
   1.747 +  let ?k = "a*d"
   1.748 +  have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
   1.749 +  proof -
   1.750 +    have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
   1.751 +      by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac) 
   1.752 +    moreover
   1.753 +    have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
   1.754 +      by (rule mult_mono, 
   1.755 +          simp_all add: int_one_le_iff_zero_less zero_less_mult_iff 
   1.756 +                        order_less_imp_le)
   1.757 +    ultimately
   1.758 +    show ?thesis by simp
   1.759 +  qed
   1.760 +  have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff)  
   1.761 +  from Gleason9_34_exists [OF A closed k]
   1.762 +  obtain z where z: "z \<in> A" 
   1.763 +             and mem: "z + of_int ?k * Fract c d \<in> A" ..
   1.764 +  have less: "z + of_int ?k * Fract c d < Fract a b"
   1.765 +    by (rule not_in_preal_ub [OF A notin mem ypos])
   1.766 +  have "0<z" by (rule preal_imp_pos [OF A z])
   1.767 +  with frle and less show False by (simp add: Fract_of_int_eq) 
   1.768 +qed
   1.769 +
   1.770 +
   1.771 +lemma Gleason9_34:
   1.772 +  assumes A: "A \<in> preal"
   1.773 +    and upos: "0 < u"
   1.774 +  shows "\<exists>r \<in> A. r + u \<notin> A"
   1.775 +proof (rule ccontr, simp)
   1.776 +  assume closed: "\<forall>r\<in>A. r + u \<in> A"
   1.777 +  from preal_exists_bound [OF A]
   1.778 +  obtain y where y: "y \<notin> A" and ypos: "0 < y" by blast
   1.779 +  show False
   1.780 +    by (rule Gleason9_34_contra [OF A closed upos ypos y])
   1.781 +qed
   1.782 +
   1.783 +
   1.784 +
   1.785 +subsection{*Gleason's Lemma 9-3.6*}
   1.786 +
   1.787 +lemma lemma_gleason9_36:
   1.788 +  assumes A: "A \<in> preal"
   1.789 +    and x: "1 < x"
   1.790 +  shows "\<exists>r \<in> A. r*x \<notin> A"
   1.791 +proof -
   1.792 +  from preal_nonempty [OF A]
   1.793 +  obtain y where y: "y \<in> A" and  ypos: "0<y" ..
   1.794 +  show ?thesis 
   1.795 +  proof (rule classical)
   1.796 +    assume "~(\<exists>r\<in>A. r * x \<notin> A)"
   1.797 +    with y have ymem: "y * x \<in> A" by blast 
   1.798 +    from ypos mult_strict_left_mono [OF x]
   1.799 +    have yless: "y < y*x" by simp 
   1.800 +    let ?d = "y*x - y"
   1.801 +    from yless have dpos: "0 < ?d" and eq: "y + ?d = y*x" by auto
   1.802 +    from Gleason9_34 [OF A dpos]
   1.803 +    obtain r where r: "r\<in>A" and notin: "r + ?d \<notin> A" ..
   1.804 +    have rpos: "0<r" by (rule preal_imp_pos [OF A r])
   1.805 +    with dpos have rdpos: "0 < r + ?d" by arith
   1.806 +    have "~ (r + ?d \<le> y + ?d)"
   1.807 +    proof
   1.808 +      assume le: "r + ?d \<le> y + ?d" 
   1.809 +      from ymem have yd: "y + ?d \<in> A" by (simp add: eq)
   1.810 +      have "r + ?d \<in> A" by (rule preal_downwards_closed' [OF A yd rdpos le])
   1.811 +      with notin show False by simp
   1.812 +    qed
   1.813 +    hence "y < r" by simp
   1.814 +    with ypos have  dless: "?d < (r * ?d)/y"
   1.815 +      by (simp add: pos_less_divide_eq mult_commute [of ?d]
   1.816 +                    mult_strict_right_mono dpos)
   1.817 +    have "r + ?d < r*x"
   1.818 +    proof -
   1.819 +      have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
   1.820 +      also with ypos have "... = (r/y) * (y + ?d)"
   1.821 +	by (simp only: right_distrib divide_inverse mult_ac, simp)
   1.822 +      also have "... = r*x" using ypos
   1.823 +	by (simp add: times_divide_eq_left) 
   1.824 +      finally show "r + ?d < r*x" .
   1.825 +    qed
   1.826 +    with r notin rdpos
   1.827 +    show "\<exists>r\<in>A. r * x \<notin> A" by (blast dest:  preal_downwards_closed [OF A])
   1.828 +  qed  
   1.829 +qed
   1.830 +
   1.831 +subsection{*Existence of Inverse: Part 2*}
   1.832 +
   1.833 +lemma mem_Rep_preal_inverse_iff:
   1.834 +      "(z \<in> Rep_preal(inverse R)) = 
   1.835 +       (0 < z \<and> (\<exists>y. z < y \<and> inverse y \<notin> Rep_preal R))"
   1.836 +apply (simp add: preal_inverse_def mem_inverse_set Rep_preal)
   1.837 +apply (simp add: inverse_set_def) 
   1.838 +done
   1.839 +
   1.840 +lemma Rep_preal_of_rat:
   1.841 +     "0 < q ==> Rep_preal (preal_of_rat q) = {x. 0 < x \<and> x < q}"
   1.842 +by (simp add: preal_of_rat_def rat_mem_preal) 
   1.843 +
   1.844 +lemma subset_inverse_mult_lemma:
   1.845 +  assumes xpos: "0 < x" and xless: "x < 1"
   1.846 +  shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R & 
   1.847 +    u \<in> Rep_preal R & x = r * u"
   1.848 +proof -
   1.849 +  from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff)
   1.850 +  from lemma_gleason9_36 [OF Rep_preal this]
   1.851 +  obtain r where r: "r \<in> Rep_preal R" 
   1.852 +             and notin: "r * (inverse x) \<notin> Rep_preal R" ..
   1.853 +  have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
   1.854 +  from preal_exists_greater [OF Rep_preal r]
   1.855 +  obtain u where u: "u \<in> Rep_preal R" and rless: "r < u" ..
   1.856 +  have upos: "0<u" by (rule preal_imp_pos [OF Rep_preal u])
   1.857 +  show ?thesis
   1.858 +  proof (intro exI conjI)
   1.859 +    show "0 < x/u" using xpos upos
   1.860 +      by (simp add: zero_less_divide_iff)  
   1.861 +    show "x/u < x/r" using xpos upos rpos
   1.862 +      by (simp add: divide_inverse mult_less_cancel_left rless) 
   1.863 +    show "inverse (x / r) \<notin> Rep_preal R" using notin
   1.864 +      by (simp add: divide_inverse mult_commute) 
   1.865 +    show "u \<in> Rep_preal R" by (rule u) 
   1.866 +    show "x = x / u * u" using upos 
   1.867 +      by (simp add: divide_inverse mult_commute) 
   1.868 +  qed
   1.869 +qed
   1.870 +
   1.871 +lemma subset_inverse_mult: 
   1.872 +     "Rep_preal(preal_of_rat 1) \<subseteq> Rep_preal(inverse R * R)"
   1.873 +apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
   1.874 +                      mem_Rep_preal_mult_iff)
   1.875 +apply (blast dest: subset_inverse_mult_lemma) 
   1.876 +done
   1.877 +
   1.878 +lemma inverse_mult_subset_lemma:
   1.879 +  assumes rpos: "0 < r" 
   1.880 +    and rless: "r < y"
   1.881 +    and notin: "inverse y \<notin> Rep_preal R"
   1.882 +    and q: "q \<in> Rep_preal R"
   1.883 +  shows "r*q < 1"
   1.884 +proof -
   1.885 +  have "q < inverse y" using rpos rless
   1.886 +    by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
   1.887 +  hence "r * q < r/y" using rpos
   1.888 +    by (simp add: divide_inverse mult_less_cancel_left)
   1.889 +  also have "... \<le> 1" using rpos rless
   1.890 +    by (simp add: pos_divide_le_eq)
   1.891 +  finally show ?thesis .
   1.892 +qed
   1.893 +
   1.894 +lemma inverse_mult_subset:
   1.895 +     "Rep_preal(inverse R * R) \<subseteq> Rep_preal(preal_of_rat 1)"
   1.896 +apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
   1.897 +                      mem_Rep_preal_mult_iff)
   1.898 +apply (simp add: zero_less_mult_iff preal_imp_pos [OF Rep_preal]) 
   1.899 +apply (blast intro: inverse_mult_subset_lemma) 
   1.900 +done
   1.901 +
   1.902 +lemma preal_mult_inverse: "inverse R * R = (1::preal)"
   1.903 +unfolding preal_one_def
   1.904 +apply (rule Rep_preal_inject [THEN iffD1])
   1.905 +apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) 
   1.906 +done
   1.907 +
   1.908 +lemma preal_mult_inverse_right: "R * inverse R = (1::preal)"
   1.909 +apply (rule preal_mult_commute [THEN subst])
   1.910 +apply (rule preal_mult_inverse)
   1.911 +done
   1.912 +
   1.913 +
   1.914 +text{*Theorems needing @{text Gleason9_34}*}
   1.915 +
   1.916 +lemma Rep_preal_self_subset: "Rep_preal (R) \<subseteq> Rep_preal(R + S)"
   1.917 +proof 
   1.918 +  fix r
   1.919 +  assume r: "r \<in> Rep_preal R"
   1.920 +  have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
   1.921 +  from mem_Rep_preal_Ex 
   1.922 +  obtain y where y: "y \<in> Rep_preal S" ..
   1.923 +  have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
   1.924 +  have ry: "r+y \<in> Rep_preal(R + S)" using r y
   1.925 +    by (auto simp add: mem_Rep_preal_add_iff)
   1.926 +  show "r \<in> Rep_preal(R + S)" using r ypos rpos 
   1.927 +    by (simp add:  preal_downwards_closed [OF Rep_preal ry]) 
   1.928 +qed
   1.929 +
   1.930 +lemma Rep_preal_sum_not_subset: "~ Rep_preal (R + S) \<subseteq> Rep_preal(R)"
   1.931 +proof -
   1.932 +  from mem_Rep_preal_Ex 
   1.933 +  obtain y where y: "y \<in> Rep_preal S" ..
   1.934 +  have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
   1.935 +  from  Gleason9_34 [OF Rep_preal ypos]
   1.936 +  obtain r where r: "r \<in> Rep_preal R" and notin: "r + y \<notin> Rep_preal R" ..
   1.937 +  have "r + y \<in> Rep_preal (R + S)" using r y
   1.938 +    by (auto simp add: mem_Rep_preal_add_iff)
   1.939 +  thus ?thesis using notin by blast
   1.940 +qed
   1.941 +
   1.942 +lemma Rep_preal_sum_not_eq: "Rep_preal (R + S) \<noteq> Rep_preal(R)"
   1.943 +by (insert Rep_preal_sum_not_subset, blast)
   1.944 +
   1.945 +text{*at last, Gleason prop. 9-3.5(iii) page 123*}
   1.946 +lemma preal_self_less_add_left: "(R::preal) < R + S"
   1.947 +apply (unfold preal_less_def less_le)
   1.948 +apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
   1.949 +done
   1.950 +
   1.951 +lemma preal_self_less_add_right: "(R::preal) < S + R"
   1.952 +by (simp add: preal_add_commute preal_self_less_add_left)
   1.953 +
   1.954 +lemma preal_not_eq_self: "x \<noteq> x + (y::preal)"
   1.955 +by (insert preal_self_less_add_left [of x y], auto)
   1.956 +
   1.957 +
   1.958 +subsection{*Subtraction for Positive Reals*}
   1.959 +
   1.960 +text{*Gleason prop. 9-3.5(iv), page 123: proving @{prop "A < B ==> \<exists>D. A + D =
   1.961 +B"}. We define the claimed @{term D} and show that it is a positive real*}
   1.962 +
   1.963 +text{*Part 1 of Dedekind sections definition*}
   1.964 +lemma diff_set_not_empty:
   1.965 +     "R < S ==> {} \<subset> diff_set (Rep_preal S) (Rep_preal R)"
   1.966 +apply (auto simp add: preal_less_def diff_set_def elim!: equalityE) 
   1.967 +apply (frule_tac x1 = S in Rep_preal [THEN preal_exists_greater])
   1.968 +apply (drule preal_imp_pos [OF Rep_preal], clarify)
   1.969 +apply (cut_tac a=x and b=u in add_eq_exists, force) 
   1.970 +done
   1.971 +
   1.972 +text{*Part 2 of Dedekind sections definition*}
   1.973 +lemma diff_set_nonempty:
   1.974 +     "\<exists>q. 0 < q & q \<notin> diff_set (Rep_preal S) (Rep_preal R)"
   1.975 +apply (cut_tac X = S in Rep_preal_exists_bound)
   1.976 +apply (erule exE)
   1.977 +apply (rule_tac x = x in exI, auto)
   1.978 +apply (simp add: diff_set_def) 
   1.979 +apply (auto dest: Rep_preal [THEN preal_downwards_closed])
   1.980 +done
   1.981 +
   1.982 +lemma diff_set_not_rat_set:
   1.983 +  "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
   1.984 +proof
   1.985 +  show "?lhs \<subseteq> ?rhs" by (auto simp add: diff_set_def) 
   1.986 +  show "?lhs \<noteq> ?rhs" using diff_set_nonempty by blast
   1.987 +qed
   1.988 +
   1.989 +text{*Part 3 of Dedekind sections definition*}
   1.990 +lemma diff_set_lemma3:
   1.991 +     "[|R < S; u \<in> diff_set (Rep_preal S) (Rep_preal R); 0 < z; z < u|] 
   1.992 +      ==> z \<in> diff_set (Rep_preal S) (Rep_preal R)"
   1.993 +apply (auto simp add: diff_set_def) 
   1.994 +apply (rule_tac x=x in exI) 
   1.995 +apply (drule Rep_preal [THEN preal_downwards_closed], auto)
   1.996 +done
   1.997 +
   1.998 +text{*Part 4 of Dedekind sections definition*}
   1.999 +lemma diff_set_lemma4:
  1.1000 +     "[|R < S; y \<in> diff_set (Rep_preal S) (Rep_preal R)|] 
  1.1001 +      ==> \<exists>u \<in> diff_set (Rep_preal S) (Rep_preal R). y < u"
  1.1002 +apply (auto simp add: diff_set_def) 
  1.1003 +apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
  1.1004 +apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify)  
  1.1005 +apply (rule_tac x="y+xa" in exI) 
  1.1006 +apply (auto simp add: add_ac)
  1.1007 +done
  1.1008 +
  1.1009 +lemma mem_diff_set:
  1.1010 +     "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
  1.1011 +apply (unfold preal_def cut_def)
  1.1012 +apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
  1.1013 +                     diff_set_lemma3 diff_set_lemma4)
  1.1014 +done
  1.1015 +
  1.1016 +lemma mem_Rep_preal_diff_iff:
  1.1017 +      "R < S ==>
  1.1018 +       (z \<in> Rep_preal(S-R)) = 
  1.1019 +       (\<exists>x. 0 < x & 0 < z & x \<notin> Rep_preal R & x + z \<in> Rep_preal S)"
  1.1020 +apply (simp add: preal_diff_def mem_diff_set Rep_preal)
  1.1021 +apply (force simp add: diff_set_def) 
  1.1022 +done
  1.1023 +
  1.1024 +
  1.1025 +text{*proving that @{term "R + D \<le> S"}*}
  1.1026 +
  1.1027 +lemma less_add_left_lemma:
  1.1028 +  assumes Rless: "R < S"
  1.1029 +    and a: "a \<in> Rep_preal R"
  1.1030 +    and cb: "c + b \<in> Rep_preal S"
  1.1031 +    and "c \<notin> Rep_preal R"
  1.1032 +    and "0 < b"
  1.1033 +    and "0 < c"
  1.1034 +  shows "a + b \<in> Rep_preal S"
  1.1035 +proof -
  1.1036 +  have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
  1.1037 +  moreover
  1.1038 +  have "a < c" using prems
  1.1039 +    by (blast intro: not_in_Rep_preal_ub ) 
  1.1040 +  ultimately show ?thesis using prems
  1.1041 +    by (simp add: preal_downwards_closed [OF Rep_preal cb]) 
  1.1042 +qed
  1.1043 +
  1.1044 +lemma less_add_left_le1:
  1.1045 +       "R < (S::preal) ==> R + (S-R) \<le> S"
  1.1046 +apply (auto simp add: Bex_def preal_le_def mem_Rep_preal_add_iff 
  1.1047 +                      mem_Rep_preal_diff_iff)
  1.1048 +apply (blast intro: less_add_left_lemma) 
  1.1049 +done
  1.1050 +
  1.1051 +subsection{*proving that @{term "S \<le> R + D"} --- trickier*}
  1.1052 +
  1.1053 +lemma lemma_sum_mem_Rep_preal_ex:
  1.1054 +     "x \<in> Rep_preal S ==> \<exists>e. 0 < e & x + e \<in> Rep_preal S"
  1.1055 +apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
  1.1056 +apply (cut_tac a=x and b=u in add_eq_exists, auto) 
  1.1057 +done
  1.1058 +
  1.1059 +lemma less_add_left_lemma2:
  1.1060 +  assumes Rless: "R < S"
  1.1061 +    and x:     "x \<in> Rep_preal S"
  1.1062 +    and xnot: "x \<notin>  Rep_preal R"
  1.1063 +  shows "\<exists>u v z. 0 < v & 0 < z & u \<in> Rep_preal R & z \<notin> Rep_preal R & 
  1.1064 +                     z + v \<in> Rep_preal S & x = u + v"
  1.1065 +proof -
  1.1066 +  have xpos: "0<x" by (rule preal_imp_pos [OF Rep_preal x])
  1.1067 +  from lemma_sum_mem_Rep_preal_ex [OF x]
  1.1068 +  obtain e where epos: "0 < e" and xe: "x + e \<in> Rep_preal S" by blast
  1.1069 +  from  Gleason9_34 [OF Rep_preal epos]
  1.1070 +  obtain r where r: "r \<in> Rep_preal R" and notin: "r + e \<notin> Rep_preal R" ..
  1.1071 +  with x xnot xpos have rless: "r < x" by (blast intro: not_in_Rep_preal_ub)
  1.1072 +  from add_eq_exists [of r x]
  1.1073 +  obtain y where eq: "x = r+y" by auto
  1.1074 +  show ?thesis 
  1.1075 +  proof (intro exI conjI)
  1.1076 +    show "r \<in> Rep_preal R" by (rule r)
  1.1077 +    show "r + e \<notin> Rep_preal R" by (rule notin)
  1.1078 +    show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac)
  1.1079 +    show "x = r + y" by (simp add: eq)
  1.1080 +    show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r]
  1.1081 +      by simp
  1.1082 +    show "0 < y" using rless eq by arith
  1.1083 +  qed
  1.1084 +qed
  1.1085 +
  1.1086 +lemma less_add_left_le2: "R < (S::preal) ==> S \<le> R + (S-R)"
  1.1087 +apply (auto simp add: preal_le_def)
  1.1088 +apply (case_tac "x \<in> Rep_preal R")
  1.1089 +apply (cut_tac Rep_preal_self_subset [of R], force)
  1.1090 +apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_diff_iff)
  1.1091 +apply (blast dest: less_add_left_lemma2)
  1.1092 +done
  1.1093 +
  1.1094 +lemma less_add_left: "R < (S::preal) ==> R + (S-R) = S"
  1.1095 +by (blast intro: antisym [OF less_add_left_le1 less_add_left_le2])
  1.1096 +
  1.1097 +lemma less_add_left_Ex: "R < (S::preal) ==> \<exists>D. R + D = S"
  1.1098 +by (fast dest: less_add_left)
  1.1099 +
  1.1100 +lemma preal_add_less2_mono1: "R < (S::preal) ==> R + T < S + T"
  1.1101 +apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc)
  1.1102 +apply (rule_tac y1 = D in preal_add_commute [THEN subst])
  1.1103 +apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric])
  1.1104 +done
  1.1105 +
  1.1106 +lemma preal_add_less2_mono2: "R < (S::preal) ==> T + R < T + S"
  1.1107 +by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of T])
  1.1108 +
  1.1109 +lemma preal_add_right_less_cancel: "R + T < S + T ==> R < (S::preal)"
  1.1110 +apply (insert linorder_less_linear [of R S], auto)
  1.1111 +apply (drule_tac R = S and T = T in preal_add_less2_mono1)
  1.1112 +apply (blast dest: order_less_trans) 
  1.1113 +done
  1.1114 +
  1.1115 +lemma preal_add_left_less_cancel: "T + R < T + S ==> R <  (S::preal)"
  1.1116 +by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T])
  1.1117 +
  1.1118 +lemma preal_add_less_cancel_right: "((R::preal) + T < S + T) = (R < S)"
  1.1119 +by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel)
  1.1120 +
  1.1121 +lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)"
  1.1122 +by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
  1.1123 +
  1.1124 +lemma preal_add_le_cancel_right: "((R::preal) + T \<le> S + T) = (R \<le> S)"
  1.1125 +by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_right) 
  1.1126 +
  1.1127 +lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
  1.1128 +by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left) 
  1.1129 +
  1.1130 +lemma preal_add_less_mono:
  1.1131 +     "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)"
  1.1132 +apply (auto dest!: less_add_left_Ex simp add: preal_add_ac)
  1.1133 +apply (rule preal_add_assoc [THEN subst])
  1.1134 +apply (rule preal_self_less_add_right)
  1.1135 +done
  1.1136 +
  1.1137 +lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S"
  1.1138 +apply (insert linorder_less_linear [of R S], safe)
  1.1139 +apply (drule_tac [!] T = T in preal_add_less2_mono1, auto)
  1.1140 +done
  1.1141 +
  1.1142 +lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)"
  1.1143 +by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
  1.1144 +
  1.1145 +lemma preal_add_left_cancel_iff: "(C + A = C + B) = ((A::preal) = B)"
  1.1146 +by (fast intro: preal_add_left_cancel)
  1.1147 +
  1.1148 +lemma preal_add_right_cancel_iff: "(A + C = B + C) = ((A::preal) = B)"
  1.1149 +by (fast intro: preal_add_right_cancel)
  1.1150 +
  1.1151 +lemmas preal_cancels =
  1.1152 +    preal_add_less_cancel_right preal_add_less_cancel_left
  1.1153 +    preal_add_le_cancel_right preal_add_le_cancel_left
  1.1154 +    preal_add_left_cancel_iff preal_add_right_cancel_iff
  1.1155 +
  1.1156 +instance preal :: ordered_cancel_ab_semigroup_add
  1.1157 +proof
  1.1158 +  fix a b c :: preal
  1.1159 +  show "a + b = a + c \<Longrightarrow> b = c" by (rule preal_add_left_cancel)
  1.1160 +  show "a \<le> b \<Longrightarrow> c + a \<le> c + b" by (simp only: preal_add_le_cancel_left)
  1.1161 +qed
  1.1162 +
  1.1163 +
  1.1164 +subsection{*Completeness of type @{typ preal}*}
  1.1165 +
  1.1166 +text{*Prove that supremum is a cut*}
  1.1167 +
  1.1168 +text{*Part 1 of Dedekind sections definition*}
  1.1169 +
  1.1170 +lemma preal_sup_set_not_empty:
  1.1171 +     "P \<noteq> {} ==> {} \<subset> (\<Union>X \<in> P. Rep_preal(X))"
  1.1172 +apply auto
  1.1173 +apply (cut_tac X = x in mem_Rep_preal_Ex, auto)
  1.1174 +done
  1.1175 +
  1.1176 +
  1.1177 +text{*Part 2 of Dedekind sections definition*}
  1.1178 +
  1.1179 +lemma preal_sup_not_exists:
  1.1180 +     "\<forall>X \<in> P. X \<le> Y ==> \<exists>q. 0 < q & q \<notin> (\<Union>X \<in> P. Rep_preal(X))"
  1.1181 +apply (cut_tac X = Y in Rep_preal_exists_bound)
  1.1182 +apply (auto simp add: preal_le_def)
  1.1183 +done
  1.1184 +
  1.1185 +lemma preal_sup_set_not_rat_set:
  1.1186 +     "\<forall>X \<in> P. X \<le> Y ==> (\<Union>X \<in> P. Rep_preal(X)) < {r. 0 < r}"
  1.1187 +apply (drule preal_sup_not_exists)
  1.1188 +apply (blast intro: preal_imp_pos [OF Rep_preal])  
  1.1189 +done
  1.1190 +
  1.1191 +text{*Part 3 of Dedekind sections definition*}
  1.1192 +lemma preal_sup_set_lemma3:
  1.1193 +     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; u \<in> (\<Union>X \<in> P. Rep_preal(X)); 0 < z; z < u|]
  1.1194 +      ==> z \<in> (\<Union>X \<in> P. Rep_preal(X))"
  1.1195 +by (auto elim: Rep_preal [THEN preal_downwards_closed])
  1.1196 +
  1.1197 +text{*Part 4 of Dedekind sections definition*}
  1.1198 +lemma preal_sup_set_lemma4:
  1.1199 +     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; y \<in> (\<Union>X \<in> P. Rep_preal(X)) |]
  1.1200 +          ==> \<exists>u \<in> (\<Union>X \<in> P. Rep_preal(X)). y < u"
  1.1201 +by (blast dest: Rep_preal [THEN preal_exists_greater])
  1.1202 +
  1.1203 +lemma preal_sup:
  1.1204 +     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
  1.1205 +apply (unfold preal_def cut_def)
  1.1206 +apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
  1.1207 +                     preal_sup_set_lemma3 preal_sup_set_lemma4)
  1.1208 +done
  1.1209 +
  1.1210 +lemma preal_psup_le:
  1.1211 +     "[| \<forall>X \<in> P. X \<le> Y;  x \<in> P |] ==> x \<le> psup P"
  1.1212 +apply (simp (no_asm_simp) add: preal_le_def) 
  1.1213 +apply (subgoal_tac "P \<noteq> {}") 
  1.1214 +apply (auto simp add: psup_def preal_sup) 
  1.1215 +done
  1.1216 +
  1.1217 +lemma psup_le_ub: "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> Y"
  1.1218 +apply (simp (no_asm_simp) add: preal_le_def)
  1.1219 +apply (simp add: psup_def preal_sup) 
  1.1220 +apply (auto simp add: preal_le_def)
  1.1221 +done
  1.1222 +
  1.1223 +text{*Supremum property*}
  1.1224 +lemma preal_complete:
  1.1225 +     "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> (\<exists>X \<in> P. Z < X) = (Z < psup P)"
  1.1226 +apply (simp add: preal_less_def psup_def preal_sup)
  1.1227 +apply (auto simp add: preal_le_def)
  1.1228 +apply (rename_tac U) 
  1.1229 +apply (cut_tac x = U and y = Z in linorder_less_linear)
  1.1230 +apply (auto simp add: preal_less_def)
  1.1231 +done
  1.1232 +
  1.1233 +
  1.1234 +subsection{*The Embedding from @{typ rat} into @{typ preal}*}
  1.1235 +
  1.1236 +lemma preal_of_rat_add_lemma1:
  1.1237 +     "[|x < y + z; 0 < x; 0 < y|] ==> x * y * inverse (y + z) < (y::rat)"
  1.1238 +apply (frule_tac c = "y * inverse (y + z) " in mult_strict_right_mono)
  1.1239 +apply (simp add: zero_less_mult_iff) 
  1.1240 +apply (simp add: mult_ac)
  1.1241 +done
  1.1242 +
  1.1243 +lemma preal_of_rat_add_lemma2:
  1.1244 +  assumes "u < x + y"
  1.1245 +    and "0 < x"
  1.1246 +    and "0 < y"
  1.1247 +    and "0 < u"
  1.1248 +  shows "\<exists>v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w"
  1.1249 +proof (intro exI conjI)
  1.1250 +  show "u * x * inverse(x+y) < x" using prems 
  1.1251 +    by (simp add: preal_of_rat_add_lemma1) 
  1.1252 +  show "u * y * inverse(x+y) < y" using prems 
  1.1253 +    by (simp add: preal_of_rat_add_lemma1 add_commute [of x]) 
  1.1254 +  show "0 < u * x * inverse (x + y)" using prems
  1.1255 +    by (simp add: zero_less_mult_iff) 
  1.1256 +  show "0 < u * y * inverse (x + y)" using prems
  1.1257 +    by (simp add: zero_less_mult_iff) 
  1.1258 +  show "u = u * x * inverse (x + y) + u * y * inverse (x + y)" using prems
  1.1259 +    by (simp add: left_distrib [symmetric] right_distrib [symmetric] mult_ac)
  1.1260 +qed
  1.1261 +
  1.1262 +lemma preal_of_rat_add:
  1.1263 +     "[| 0 < x; 0 < y|] 
  1.1264 +      ==> preal_of_rat ((x::rat) + y) = preal_of_rat x + preal_of_rat y"
  1.1265 +apply (unfold preal_of_rat_def preal_add_def)
  1.1266 +apply (simp add: rat_mem_preal) 
  1.1267 +apply (rule_tac f = Abs_preal in arg_cong)
  1.1268 +apply (auto simp add: add_set_def) 
  1.1269 +apply (blast dest: preal_of_rat_add_lemma2) 
  1.1270 +done
  1.1271 +
  1.1272 +lemma preal_of_rat_mult_lemma1:
  1.1273 +     "[|x < y; 0 < x; 0 < z|] ==> x * z * inverse y < (z::rat)"
  1.1274 +apply (frule_tac c = "z * inverse y" in mult_strict_right_mono)
  1.1275 +apply (simp add: zero_less_mult_iff)
  1.1276 +apply (subgoal_tac "y * (z * inverse y) = z * (y * inverse y)")
  1.1277 +apply (simp_all add: mult_ac)
  1.1278 +done
  1.1279 +
  1.1280 +lemma preal_of_rat_mult_lemma2: 
  1.1281 +  assumes xless: "x < y * z"
  1.1282 +    and xpos: "0 < x"
  1.1283 +    and ypos: "0 < y"
  1.1284 +  shows "x * z * inverse y * inverse z < (z::rat)"
  1.1285 +proof -
  1.1286 +  have "0 < y * z" using prems by simp
  1.1287 +  hence zpos:  "0 < z" using prems by (simp add: zero_less_mult_iff)
  1.1288 +  have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
  1.1289 +    by (simp add: mult_ac)
  1.1290 +  also have "... = x/y" using zpos
  1.1291 +    by (simp add: divide_inverse)
  1.1292 +  also from xless have "... < z"
  1.1293 +    by (simp add: pos_divide_less_eq [OF ypos] mult_commute)
  1.1294 +  finally show ?thesis .
  1.1295 +qed
  1.1296 +
  1.1297 +lemma preal_of_rat_mult_lemma3:
  1.1298 +  assumes uless: "u < x * y"
  1.1299 +    and "0 < x"
  1.1300 +    and "0 < y"
  1.1301 +    and "0 < u"
  1.1302 +  shows "\<exists>v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w"
  1.1303 +proof -
  1.1304 +  from dense [OF uless] 
  1.1305 +  obtain r where "u < r" "r < x * y" by blast
  1.1306 +  thus ?thesis
  1.1307 +  proof (intro exI conjI)
  1.1308 +  show "u * x * inverse r < x" using prems 
  1.1309 +    by (simp add: preal_of_rat_mult_lemma1) 
  1.1310 +  show "r * y * inverse x * inverse y < y" using prems
  1.1311 +    by (simp add: preal_of_rat_mult_lemma2)
  1.1312 +  show "0 < u * x * inverse r" using prems
  1.1313 +    by (simp add: zero_less_mult_iff) 
  1.1314 +  show "0 < r * y * inverse x * inverse y" using prems
  1.1315 +    by (simp add: zero_less_mult_iff) 
  1.1316 +  have "u * x * inverse r * (r * y * inverse x * inverse y) =
  1.1317 +        u * (r * inverse r) * (x * inverse x) * (y * inverse y)"
  1.1318 +    by (simp only: mult_ac)
  1.1319 +  thus "u = u * x * inverse r * (r * y * inverse x * inverse y)" using prems
  1.1320 +    by simp
  1.1321 +  qed
  1.1322 +qed
  1.1323 +
  1.1324 +lemma preal_of_rat_mult:
  1.1325 +     "[| 0 < x; 0 < y|] 
  1.1326 +      ==> preal_of_rat ((x::rat) * y) = preal_of_rat x * preal_of_rat y"
  1.1327 +apply (unfold preal_of_rat_def preal_mult_def)
  1.1328 +apply (simp add: rat_mem_preal) 
  1.1329 +apply (rule_tac f = Abs_preal in arg_cong)
  1.1330 +apply (auto simp add: zero_less_mult_iff mult_strict_mono mult_set_def) 
  1.1331 +apply (blast dest: preal_of_rat_mult_lemma3) 
  1.1332 +done
  1.1333 +
  1.1334 +lemma preal_of_rat_less_iff:
  1.1335 +      "[| 0 < x; 0 < y|] ==> (preal_of_rat x < preal_of_rat y) = (x < y)"
  1.1336 +by (force simp add: preal_of_rat_def preal_less_def rat_mem_preal) 
  1.1337 +
  1.1338 +lemma preal_of_rat_le_iff:
  1.1339 +      "[| 0 < x; 0 < y|] ==> (preal_of_rat x \<le> preal_of_rat y) = (x \<le> y)"
  1.1340 +by (simp add: preal_of_rat_less_iff linorder_not_less [symmetric]) 
  1.1341 +
  1.1342 +lemma preal_of_rat_eq_iff:
  1.1343 +      "[| 0 < x; 0 < y|] ==> (preal_of_rat x = preal_of_rat y) = (x = y)"
  1.1344 +by (simp add: preal_of_rat_le_iff order_eq_iff) 
  1.1345 +
  1.1346 +end