put construction of reals using Dedekind cuts in HOL/ex
authorhuffman
Mon May 10 11:30:05 2010 -0700 (2010-05-10 ago)
changeset 3679327da0a27b76f
parent 36786 b7a62e7dec00
child 36794 f736a853864f
put construction of reals using Dedekind cuts in HOL/ex
src/HOL/IsaMakefile
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon May 10 17:37:32 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon May 10 11:30:05 2010 -0700
     1.3 @@ -962,7 +962,7 @@
     1.4    ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
     1.5    ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy		\
     1.6    ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy		\
     1.7 -  ex/Codegenerator_Test.thy ex/Coherent.thy				\
     1.8 +  ex/Codegenerator_Test.thy ex/Coherent.thy ex/Dedekind_Real.thy	\
     1.9    ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy	\
    1.10    ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy	\
    1.11    ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy		\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Mon May 10 11:30:05 2010 -0700
     2.3 @@ -0,0 +1,2044 @@
     2.4 +(*  Title:      HOL/ex/Dedekind_Real.thy
     2.5 +    Author:     Jacques D. Fleuriot, University of Cambridge
     2.6 +
     2.7 +The positive reals as Dedekind sections of positive
     2.8 +rationals. Fundamentals of Abstract Analysis [Gleason- p. 121]
     2.9 +provides some of the definitions.
    2.10 +*)
    2.11 +
    2.12 +theory Dedekind_Real
    2.13 +imports Rat Lubs
    2.14 +begin
    2.15 +
    2.16 +section {* Positive real numbers *}
    2.17 +
    2.18 +text{*Could be generalized and moved to @{text Groups}*}
    2.19 +lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"
    2.20 +by (rule_tac x="b-a" in exI, simp)
    2.21 +
    2.22 +definition
    2.23 +  cut :: "rat set => bool" where
    2.24 +  [code del]: "cut A = ({} \<subset> A &
    2.25 +            A < {r. 0 < r} &
    2.26 +            (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
    2.27 +
    2.28 +lemma interval_empty_iff:
    2.29 +  "{y. (x::'a::dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
    2.30 +  by (auto dest: dense)
    2.31 +
    2.32 +
    2.33 +lemma cut_of_rat: 
    2.34 +  assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A")
    2.35 +proof -
    2.36 +  from q have pos: "?A < {r. 0 < r}" by force
    2.37 +  have nonempty: "{} \<subset> ?A"
    2.38 +  proof
    2.39 +    show "{} \<subseteq> ?A" by simp
    2.40 +    show "{} \<noteq> ?A"
    2.41 +      by (force simp only: q eq_commute [of "{}"] interval_empty_iff)
    2.42 +  qed
    2.43 +  show ?thesis
    2.44 +    by (simp add: cut_def pos nonempty,
    2.45 +        blast dest: dense intro: order_less_trans)
    2.46 +qed
    2.47 +
    2.48 +
    2.49 +typedef preal = "{A. cut A}"
    2.50 +  by (blast intro: cut_of_rat [OF zero_less_one])
    2.51 +
    2.52 +definition
    2.53 +  psup :: "preal set => preal" where
    2.54 +  [code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
    2.55 +
    2.56 +definition
    2.57 +  add_set :: "[rat set,rat set] => rat set" where
    2.58 +  "add_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
    2.59 +
    2.60 +definition
    2.61 +  diff_set :: "[rat set,rat set] => rat set" where
    2.62 +  [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
    2.63 +
    2.64 +definition
    2.65 +  mult_set :: "[rat set,rat set] => rat set" where
    2.66 +  "mult_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
    2.67 +
    2.68 +definition
    2.69 +  inverse_set :: "rat set => rat set" where
    2.70 +  [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
    2.71 +
    2.72 +instantiation preal :: "{ord, plus, minus, times, inverse, one}"
    2.73 +begin
    2.74 +
    2.75 +definition
    2.76 +  preal_less_def [code del]:
    2.77 +    "R < S == Rep_preal R < Rep_preal S"
    2.78 +
    2.79 +definition
    2.80 +  preal_le_def [code del]:
    2.81 +    "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
    2.82 +
    2.83 +definition
    2.84 +  preal_add_def:
    2.85 +    "R + S == Abs_preal (add_set (Rep_preal R) (Rep_preal S))"
    2.86 +
    2.87 +definition
    2.88 +  preal_diff_def:
    2.89 +    "R - S == Abs_preal (diff_set (Rep_preal R) (Rep_preal S))"
    2.90 +
    2.91 +definition
    2.92 +  preal_mult_def:
    2.93 +    "R * S == Abs_preal (mult_set (Rep_preal R) (Rep_preal S))"
    2.94 +
    2.95 +definition
    2.96 +  preal_inverse_def:
    2.97 +    "inverse R == Abs_preal (inverse_set (Rep_preal R))"
    2.98 +
    2.99 +definition "R / S = R * inverse (S\<Colon>preal)"
   2.100 +
   2.101 +definition
   2.102 +  preal_one_def:
   2.103 +    "1 == Abs_preal {x. 0 < x & x < 1}"
   2.104 +
   2.105 +instance ..
   2.106 +
   2.107 +end
   2.108 +
   2.109 +
   2.110 +text{*Reduces equality on abstractions to equality on representatives*}
   2.111 +declare Abs_preal_inject [simp]
   2.112 +declare Abs_preal_inverse [simp]
   2.113 +
   2.114 +lemma rat_mem_preal: "0 < q ==> {r::rat. 0 < r & r < q} \<in> preal"
   2.115 +by (simp add: preal_def cut_of_rat)
   2.116 +
   2.117 +lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
   2.118 +by (unfold preal_def cut_def, blast)
   2.119 +
   2.120 +lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
   2.121 +by (drule preal_nonempty, fast)
   2.122 +
   2.123 +lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
   2.124 +by (force simp add: preal_def cut_def)
   2.125 +
   2.126 +lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
   2.127 +by (drule preal_imp_psubset_positives, auto)
   2.128 +
   2.129 +lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
   2.130 +by (unfold preal_def cut_def, blast)
   2.131 +
   2.132 +lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
   2.133 +by (unfold preal_def cut_def, blast)
   2.134 +
   2.135 +text{*Relaxing the final premise*}
   2.136 +lemma preal_downwards_closed':
   2.137 +     "[| A \<in> preal; y \<in> A; 0 < z; z \<le> y |] ==> z \<in> A"
   2.138 +apply (simp add: order_le_less)
   2.139 +apply (blast intro: preal_downwards_closed)
   2.140 +done
   2.141 +
   2.142 +text{*A positive fraction not in a positive real is an upper bound.
   2.143 + Gleason p. 122 - Remark (1)*}
   2.144 +
   2.145 +lemma not_in_preal_ub:
   2.146 +  assumes A: "A \<in> preal"
   2.147 +    and notx: "x \<notin> A"
   2.148 +    and y: "y \<in> A"
   2.149 +    and pos: "0 < x"
   2.150 +  shows "y < x"
   2.151 +proof (cases rule: linorder_cases)
   2.152 +  assume "x<y"
   2.153 +  with notx show ?thesis
   2.154 +    by (simp add:  preal_downwards_closed [OF A y] pos)
   2.155 +next
   2.156 +  assume "x=y"
   2.157 +  with notx and y show ?thesis by simp
   2.158 +next
   2.159 +  assume "y<x"
   2.160 +  thus ?thesis .
   2.161 +qed
   2.162 +
   2.163 +text {* preal lemmas instantiated to @{term "Rep_preal X"} *}
   2.164 +
   2.165 +lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X"
   2.166 +by (rule preal_Ex_mem [OF Rep_preal])
   2.167 +
   2.168 +lemma Rep_preal_exists_bound: "\<exists>x>0. x \<notin> Rep_preal X"
   2.169 +by (rule preal_exists_bound [OF Rep_preal])
   2.170 +
   2.171 +lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal]
   2.172 +
   2.173 +
   2.174 +subsection{*Properties of Ordering*}
   2.175 +
   2.176 +instance preal :: order
   2.177 +proof
   2.178 +  fix w :: preal
   2.179 +  show "w \<le> w" by (simp add: preal_le_def)
   2.180 +next
   2.181 +  fix i j k :: preal
   2.182 +  assume "i \<le> j" and "j \<le> k"
   2.183 +  then show "i \<le> k" by (simp add: preal_le_def)
   2.184 +next
   2.185 +  fix z w :: preal
   2.186 +  assume "z \<le> w" and "w \<le> z"
   2.187 +  then show "z = w" by (simp add: preal_le_def Rep_preal_inject)
   2.188 +next
   2.189 +  fix z w :: preal
   2.190 +  show "z < w \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
   2.191 +  by (auto simp add: preal_le_def preal_less_def Rep_preal_inject)
   2.192 +qed  
   2.193 +
   2.194 +lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
   2.195 +by (insert preal_imp_psubset_positives, blast)
   2.196 +
   2.197 +instance preal :: linorder
   2.198 +proof
   2.199 +  fix x y :: preal
   2.200 +  show "x <= y | y <= x"
   2.201 +    apply (auto simp add: preal_le_def)
   2.202 +    apply (rule ccontr)
   2.203 +    apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
   2.204 +             elim: order_less_asym)
   2.205 +    done
   2.206 +qed
   2.207 +
   2.208 +instantiation preal :: distrib_lattice
   2.209 +begin
   2.210 +
   2.211 +definition
   2.212 +  "(inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = min"
   2.213 +
   2.214 +definition
   2.215 +  "(sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = max"
   2.216 +
   2.217 +instance
   2.218 +  by intro_classes
   2.219 +    (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
   2.220 +
   2.221 +end
   2.222 +
   2.223 +subsection{*Properties of Addition*}
   2.224 +
   2.225 +lemma preal_add_commute: "(x::preal) + y = y + x"
   2.226 +apply (unfold preal_add_def add_set_def)
   2.227 +apply (rule_tac f = Abs_preal in arg_cong)
   2.228 +apply (force simp add: add_commute)
   2.229 +done
   2.230 +
   2.231 +text{*Lemmas for proving that addition of two positive reals gives
   2.232 + a positive real*}
   2.233 +
   2.234 +text{*Part 1 of Dedekind sections definition*}
   2.235 +lemma add_set_not_empty:
   2.236 +     "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> add_set A B"
   2.237 +apply (drule preal_nonempty)+
   2.238 +apply (auto simp add: add_set_def)
   2.239 +done
   2.240 +
   2.241 +text{*Part 2 of Dedekind sections definition.  A structured version of
   2.242 +this proof is @{text preal_not_mem_mult_set_Ex} below.*}
   2.243 +lemma preal_not_mem_add_set_Ex:
   2.244 +     "[|A \<in> preal; B \<in> preal|] ==> \<exists>q>0. q \<notin> add_set A B"
   2.245 +apply (insert preal_exists_bound [of A] preal_exists_bound [of B], auto) 
   2.246 +apply (rule_tac x = "x+xa" in exI)
   2.247 +apply (simp add: add_set_def, clarify)
   2.248 +apply (drule (3) not_in_preal_ub)+
   2.249 +apply (force dest: add_strict_mono)
   2.250 +done
   2.251 +
   2.252 +lemma add_set_not_rat_set:
   2.253 +   assumes A: "A \<in> preal" 
   2.254 +       and B: "B \<in> preal"
   2.255 +     shows "add_set A B < {r. 0 < r}"
   2.256 +proof
   2.257 +  from preal_imp_pos [OF A] preal_imp_pos [OF B]
   2.258 +  show "add_set A B \<subseteq> {r. 0 < r}" by (force simp add: add_set_def) 
   2.259 +next
   2.260 +  show "add_set A B \<noteq> {r. 0 < r}"
   2.261 +    by (insert preal_not_mem_add_set_Ex [OF A B], blast) 
   2.262 +qed
   2.263 +
   2.264 +text{*Part 3 of Dedekind sections definition*}
   2.265 +lemma add_set_lemma3:
   2.266 +     "[|A \<in> preal; B \<in> preal; u \<in> add_set A B; 0 < z; z < u|] 
   2.267 +      ==> z \<in> add_set A B"
   2.268 +proof (unfold add_set_def, clarify)
   2.269 +  fix x::rat and y::rat
   2.270 +  assume A: "A \<in> preal" 
   2.271 +    and B: "B \<in> preal"
   2.272 +    and [simp]: "0 < z"
   2.273 +    and zless: "z < x + y"
   2.274 +    and x:  "x \<in> A"
   2.275 +    and y:  "y \<in> B"
   2.276 +  have xpos [simp]: "0<x" by (rule preal_imp_pos [OF A x])
   2.277 +  have ypos [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   2.278 +  have xypos [simp]: "0 < x+y" by (simp add: pos_add_strict)
   2.279 +  let ?f = "z/(x+y)"
   2.280 +  have fless: "?f < 1" by (simp add: zless pos_divide_less_eq)
   2.281 +  show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
   2.282 +  proof (intro bexI)
   2.283 +    show "z = x*?f + y*?f"
   2.284 +      by (simp add: left_distrib [symmetric] divide_inverse mult_ac
   2.285 +          order_less_imp_not_eq2)
   2.286 +  next
   2.287 +    show "y * ?f \<in> B"
   2.288 +    proof (rule preal_downwards_closed [OF B y])
   2.289 +      show "0 < y * ?f"
   2.290 +        by (simp add: divide_inverse zero_less_mult_iff)
   2.291 +    next
   2.292 +      show "y * ?f < y"
   2.293 +        by (insert mult_strict_left_mono [OF fless ypos], simp)
   2.294 +    qed
   2.295 +  next
   2.296 +    show "x * ?f \<in> A"
   2.297 +    proof (rule preal_downwards_closed [OF A x])
   2.298 +      show "0 < x * ?f"
   2.299 +        by (simp add: divide_inverse zero_less_mult_iff)
   2.300 +    next
   2.301 +      show "x * ?f < x"
   2.302 +        by (insert mult_strict_left_mono [OF fless xpos], simp)
   2.303 +    qed
   2.304 +  qed
   2.305 +qed
   2.306 +
   2.307 +text{*Part 4 of Dedekind sections definition*}
   2.308 +lemma add_set_lemma4:
   2.309 +     "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
   2.310 +apply (auto simp add: add_set_def)
   2.311 +apply (frule preal_exists_greater [of A], auto) 
   2.312 +apply (rule_tac x="u + y" in exI)
   2.313 +apply (auto intro: add_strict_left_mono)
   2.314 +done
   2.315 +
   2.316 +lemma mem_add_set:
   2.317 +     "[|A \<in> preal; B \<in> preal|] ==> add_set A B \<in> preal"
   2.318 +apply (simp (no_asm_simp) add: preal_def cut_def)
   2.319 +apply (blast intro!: add_set_not_empty add_set_not_rat_set
   2.320 +                     add_set_lemma3 add_set_lemma4)
   2.321 +done
   2.322 +
   2.323 +lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
   2.324 +apply (simp add: preal_add_def mem_add_set Rep_preal)
   2.325 +apply (force simp add: add_set_def add_ac)
   2.326 +done
   2.327 +
   2.328 +instance preal :: ab_semigroup_add
   2.329 +proof
   2.330 +  fix a b c :: preal
   2.331 +  show "(a + b) + c = a + (b + c)" by (rule preal_add_assoc)
   2.332 +  show "a + b = b + a" by (rule preal_add_commute)
   2.333 +qed
   2.334 +
   2.335 +
   2.336 +subsection{*Properties of Multiplication*}
   2.337 +
   2.338 +text{*Proofs essentially same as for addition*}
   2.339 +
   2.340 +lemma preal_mult_commute: "(x::preal) * y = y * x"
   2.341 +apply (unfold preal_mult_def mult_set_def)
   2.342 +apply (rule_tac f = Abs_preal in arg_cong)
   2.343 +apply (force simp add: mult_commute)
   2.344 +done
   2.345 +
   2.346 +text{*Multiplication of two positive reals gives a positive real.*}
   2.347 +
   2.348 +text{*Lemmas for proving positive reals multiplication set in @{typ preal}*}
   2.349 +
   2.350 +text{*Part 1 of Dedekind sections definition*}
   2.351 +lemma mult_set_not_empty:
   2.352 +     "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> mult_set A B"
   2.353 +apply (insert preal_nonempty [of A] preal_nonempty [of B]) 
   2.354 +apply (auto simp add: mult_set_def)
   2.355 +done
   2.356 +
   2.357 +text{*Part 2 of Dedekind sections definition*}
   2.358 +lemma preal_not_mem_mult_set_Ex:
   2.359 +   assumes A: "A \<in> preal" 
   2.360 +       and B: "B \<in> preal"
   2.361 +     shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
   2.362 +proof -
   2.363 +  from preal_exists_bound [OF A]
   2.364 +  obtain x where [simp]: "0 < x" "x \<notin> A" by blast
   2.365 +  from preal_exists_bound [OF B]
   2.366 +  obtain y where [simp]: "0 < y" "y \<notin> B" by blast
   2.367 +  show ?thesis
   2.368 +  proof (intro exI conjI)
   2.369 +    show "0 < x*y" by (simp add: mult_pos_pos)
   2.370 +    show "x * y \<notin> mult_set A B"
   2.371 +    proof -
   2.372 +      { fix u::rat and v::rat
   2.373 +              assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
   2.374 +              moreover
   2.375 +              with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
   2.376 +              moreover
   2.377 +              with prems have "0\<le>v"
   2.378 +                by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
   2.379 +              moreover
   2.380 +        from calculation
   2.381 +              have "u*v < x*y" by (blast intro: mult_strict_mono prems)
   2.382 +              ultimately have False by force }
   2.383 +      thus ?thesis by (auto simp add: mult_set_def)
   2.384 +    qed
   2.385 +  qed
   2.386 +qed
   2.387 +
   2.388 +lemma mult_set_not_rat_set:
   2.389 +  assumes A: "A \<in> preal" 
   2.390 +    and B: "B \<in> preal"
   2.391 +  shows "mult_set A B < {r. 0 < r}"
   2.392 +proof
   2.393 +  show "mult_set A B \<subseteq> {r. 0 < r}"
   2.394 +    by (force simp add: mult_set_def
   2.395 +      intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos)
   2.396 +  show "mult_set A B \<noteq> {r. 0 < r}"
   2.397 +    using preal_not_mem_mult_set_Ex [OF A B] by blast
   2.398 +qed
   2.399 +
   2.400 +
   2.401 +
   2.402 +text{*Part 3 of Dedekind sections definition*}
   2.403 +lemma mult_set_lemma3:
   2.404 +     "[|A \<in> preal; B \<in> preal; u \<in> mult_set A B; 0 < z; z < u|] 
   2.405 +      ==> z \<in> mult_set A B"
   2.406 +proof (unfold mult_set_def, clarify)
   2.407 +  fix x::rat and y::rat
   2.408 +  assume A: "A \<in> preal" 
   2.409 +    and B: "B \<in> preal"
   2.410 +    and [simp]: "0 < z"
   2.411 +    and zless: "z < x * y"
   2.412 +    and x:  "x \<in> A"
   2.413 +    and y:  "y \<in> B"
   2.414 +  have [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   2.415 +  show "\<exists>x' \<in> A. \<exists>y' \<in> B. z = x' * y'"
   2.416 +  proof
   2.417 +    show "\<exists>y'\<in>B. z = (z/y) * y'"
   2.418 +    proof
   2.419 +      show "z = (z/y)*y"
   2.420 +        by (simp add: divide_inverse mult_commute [of y] mult_assoc
   2.421 +                      order_less_imp_not_eq2)
   2.422 +      show "y \<in> B" by fact
   2.423 +    qed
   2.424 +  next
   2.425 +    show "z/y \<in> A"
   2.426 +    proof (rule preal_downwards_closed [OF A x])
   2.427 +      show "0 < z/y"
   2.428 +        by (simp add: zero_less_divide_iff)
   2.429 +      show "z/y < x" by (simp add: pos_divide_less_eq zless)
   2.430 +    qed
   2.431 +  qed
   2.432 +qed
   2.433 +
   2.434 +text{*Part 4 of Dedekind sections definition*}
   2.435 +lemma mult_set_lemma4:
   2.436 +     "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
   2.437 +apply (auto simp add: mult_set_def)
   2.438 +apply (frule preal_exists_greater [of A], auto) 
   2.439 +apply (rule_tac x="u * y" in exI)
   2.440 +apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B] 
   2.441 +                   mult_strict_right_mono)
   2.442 +done
   2.443 +
   2.444 +
   2.445 +lemma mem_mult_set:
   2.446 +     "[|A \<in> preal; B \<in> preal|] ==> mult_set A B \<in> preal"
   2.447 +apply (simp (no_asm_simp) add: preal_def cut_def)
   2.448 +apply (blast intro!: mult_set_not_empty mult_set_not_rat_set
   2.449 +                     mult_set_lemma3 mult_set_lemma4)
   2.450 +done
   2.451 +
   2.452 +lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
   2.453 +apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   2.454 +apply (force simp add: mult_set_def mult_ac)
   2.455 +done
   2.456 +
   2.457 +instance preal :: ab_semigroup_mult
   2.458 +proof
   2.459 +  fix a b c :: preal
   2.460 +  show "(a * b) * c = a * (b * c)" by (rule preal_mult_assoc)
   2.461 +  show "a * b = b * a" by (rule preal_mult_commute)
   2.462 +qed
   2.463 +
   2.464 +
   2.465 +text{* Positive real 1 is the multiplicative identity element *}
   2.466 +
   2.467 +lemma preal_mult_1: "(1::preal) * z = z"
   2.468 +proof (induct z)
   2.469 +  fix A :: "rat set"
   2.470 +  assume A: "A \<in> preal"
   2.471 +  have "{w. \<exists>u. 0 < u \<and> u < 1 & (\<exists>v \<in> A. w = u * v)} = A" (is "?lhs = A")
   2.472 +  proof
   2.473 +    show "?lhs \<subseteq> A"
   2.474 +    proof clarify
   2.475 +      fix x::rat and u::rat and v::rat
   2.476 +      assume upos: "0<u" and "u<1" and v: "v \<in> A"
   2.477 +      have vpos: "0<v" by (rule preal_imp_pos [OF A v])
   2.478 +      hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
   2.479 +      thus "u * v \<in> A"
   2.480 +        by (force intro: preal_downwards_closed [OF A v] mult_pos_pos 
   2.481 +          upos vpos)
   2.482 +    qed
   2.483 +  next
   2.484 +    show "A \<subseteq> ?lhs"
   2.485 +    proof clarify
   2.486 +      fix x::rat
   2.487 +      assume x: "x \<in> A"
   2.488 +      have xpos: "0<x" by (rule preal_imp_pos [OF A x])
   2.489 +      from preal_exists_greater [OF A x]
   2.490 +      obtain v where v: "v \<in> A" and xlessv: "x < v" ..
   2.491 +      have vpos: "0<v" by (rule preal_imp_pos [OF A v])
   2.492 +      show "\<exists>u. 0 < u \<and> u < 1 \<and> (\<exists>v\<in>A. x = u * v)"
   2.493 +      proof (intro exI conjI)
   2.494 +        show "0 < x/v"
   2.495 +          by (simp add: zero_less_divide_iff xpos vpos)
   2.496 +        show "x / v < 1"
   2.497 +          by (simp add: pos_divide_less_eq vpos xlessv)
   2.498 +        show "\<exists>v'\<in>A. x = (x / v) * v'"
   2.499 +        proof
   2.500 +          show "x = (x/v)*v"
   2.501 +            by (simp add: divide_inverse mult_assoc vpos
   2.502 +                          order_less_imp_not_eq2)
   2.503 +          show "v \<in> A" by fact
   2.504 +        qed
   2.505 +      qed
   2.506 +    qed
   2.507 +  qed
   2.508 +  thus "1 * Abs_preal A = Abs_preal A"
   2.509 +    by (simp add: preal_one_def preal_mult_def mult_set_def 
   2.510 +                  rat_mem_preal A)
   2.511 +qed
   2.512 +
   2.513 +instance preal :: comm_monoid_mult
   2.514 +by intro_classes (rule preal_mult_1)
   2.515 +
   2.516 +
   2.517 +subsection{*Distribution of Multiplication across Addition*}
   2.518 +
   2.519 +lemma mem_Rep_preal_add_iff:
   2.520 +      "(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x + y)"
   2.521 +apply (simp add: preal_add_def mem_add_set Rep_preal)
   2.522 +apply (simp add: add_set_def) 
   2.523 +done
   2.524 +
   2.525 +lemma mem_Rep_preal_mult_iff:
   2.526 +      "(z \<in> Rep_preal(R*S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x * y)"
   2.527 +apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   2.528 +apply (simp add: mult_set_def) 
   2.529 +done
   2.530 +
   2.531 +lemma distrib_subset1:
   2.532 +     "Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)"
   2.533 +apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
   2.534 +apply (force simp add: right_distrib)
   2.535 +done
   2.536 +
   2.537 +lemma preal_add_mult_distrib_mean:
   2.538 +  assumes a: "a \<in> Rep_preal w"
   2.539 +    and b: "b \<in> Rep_preal w"
   2.540 +    and d: "d \<in> Rep_preal x"
   2.541 +    and e: "e \<in> Rep_preal y"
   2.542 +  shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
   2.543 +proof
   2.544 +  let ?c = "(a*d + b*e)/(d+e)"
   2.545 +  have [simp]: "0<a" "0<b" "0<d" "0<e" "0<d+e"
   2.546 +    by (blast intro: preal_imp_pos [OF Rep_preal] a b d e pos_add_strict)+
   2.547 +  have cpos: "0 < ?c"
   2.548 +    by (simp add: zero_less_divide_iff zero_less_mult_iff pos_add_strict)
   2.549 +  show "a * d + b * e = ?c * (d + e)"
   2.550 +    by (simp add: divide_inverse mult_assoc order_less_imp_not_eq2)
   2.551 +  show "?c \<in> Rep_preal w"
   2.552 +  proof (cases rule: linorder_le_cases)
   2.553 +    assume "a \<le> b"
   2.554 +    hence "?c \<le> b"
   2.555 +      by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   2.556 +                    order_less_imp_le)
   2.557 +    thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos])
   2.558 +  next
   2.559 +    assume "b \<le> a"
   2.560 +    hence "?c \<le> a"
   2.561 +      by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   2.562 +                    order_less_imp_le)
   2.563 +    thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos])
   2.564 +  qed
   2.565 +qed
   2.566 +
   2.567 +lemma distrib_subset2:
   2.568 +     "Rep_preal (w * x + w * y) \<subseteq> Rep_preal (w * (x + y))"
   2.569 +apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
   2.570 +apply (drule_tac w=w and x=x and y=y in preal_add_mult_distrib_mean, auto)
   2.571 +done
   2.572 +
   2.573 +lemma preal_add_mult_distrib2: "(w * ((x::preal) + y)) = (w * x) + (w * y)"
   2.574 +apply (rule Rep_preal_inject [THEN iffD1])
   2.575 +apply (rule equalityI [OF distrib_subset1 distrib_subset2])
   2.576 +done
   2.577 +
   2.578 +lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)"
   2.579 +by (simp add: preal_mult_commute preal_add_mult_distrib2)
   2.580 +
   2.581 +instance preal :: comm_semiring
   2.582 +by intro_classes (rule preal_add_mult_distrib)
   2.583 +
   2.584 +
   2.585 +subsection{*Existence of Inverse, a Positive Real*}
   2.586 +
   2.587 +lemma mem_inv_set_ex:
   2.588 +  assumes A: "A \<in> preal" shows "\<exists>x y. 0 < x & x < y & inverse y \<notin> A"
   2.589 +proof -
   2.590 +  from preal_exists_bound [OF A]
   2.591 +  obtain x where [simp]: "0<x" "x \<notin> A" by blast
   2.592 +  show ?thesis
   2.593 +  proof (intro exI conjI)
   2.594 +    show "0 < inverse (x+1)"
   2.595 +      by (simp add: order_less_trans [OF _ less_add_one]) 
   2.596 +    show "inverse(x+1) < inverse x"
   2.597 +      by (simp add: less_imp_inverse_less less_add_one)
   2.598 +    show "inverse (inverse x) \<notin> A"
   2.599 +      by (simp add: order_less_imp_not_eq2)
   2.600 +  qed
   2.601 +qed
   2.602 +
   2.603 +text{*Part 1 of Dedekind sections definition*}
   2.604 +lemma inverse_set_not_empty:
   2.605 +     "A \<in> preal ==> {} \<subset> inverse_set A"
   2.606 +apply (insert mem_inv_set_ex [of A])
   2.607 +apply (auto simp add: inverse_set_def)
   2.608 +done
   2.609 +
   2.610 +text{*Part 2 of Dedekind sections definition*}
   2.611 +
   2.612 +lemma preal_not_mem_inverse_set_Ex:
   2.613 +   assumes A: "A \<in> preal"  shows "\<exists>q. 0 < q & q \<notin> inverse_set A"
   2.614 +proof -
   2.615 +  from preal_nonempty [OF A]
   2.616 +  obtain x where x: "x \<in> A" and  xpos [simp]: "0<x" ..
   2.617 +  show ?thesis
   2.618 +  proof (intro exI conjI)
   2.619 +    show "0 < inverse x" by simp
   2.620 +    show "inverse x \<notin> inverse_set A"
   2.621 +    proof -
   2.622 +      { fix y::rat 
   2.623 +        assume ygt: "inverse x < y"
   2.624 +        have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
   2.625 +        have iyless: "inverse y < x" 
   2.626 +          by (simp add: inverse_less_imp_less [of x] ygt)
   2.627 +        have "inverse y \<in> A"
   2.628 +          by (simp add: preal_downwards_closed [OF A x] iyless)}
   2.629 +     thus ?thesis by (auto simp add: inverse_set_def)
   2.630 +    qed
   2.631 +  qed
   2.632 +qed
   2.633 +
   2.634 +lemma inverse_set_not_rat_set:
   2.635 +   assumes A: "A \<in> preal"  shows "inverse_set A < {r. 0 < r}"
   2.636 +proof
   2.637 +  show "inverse_set A \<subseteq> {r. 0 < r}"  by (force simp add: inverse_set_def)
   2.638 +next
   2.639 +  show "inverse_set A \<noteq> {r. 0 < r}"
   2.640 +    by (insert preal_not_mem_inverse_set_Ex [OF A], blast)
   2.641 +qed
   2.642 +
   2.643 +text{*Part 3 of Dedekind sections definition*}
   2.644 +lemma inverse_set_lemma3:
   2.645 +     "[|A \<in> preal; u \<in> inverse_set A; 0 < z; z < u|] 
   2.646 +      ==> z \<in> inverse_set A"
   2.647 +apply (auto simp add: inverse_set_def)
   2.648 +apply (auto intro: order_less_trans)
   2.649 +done
   2.650 +
   2.651 +text{*Part 4 of Dedekind sections definition*}
   2.652 +lemma inverse_set_lemma4:
   2.653 +     "[|A \<in> preal; y \<in> inverse_set A|] ==> \<exists>u \<in> inverse_set A. y < u"
   2.654 +apply (auto simp add: inverse_set_def)
   2.655 +apply (drule dense [of y]) 
   2.656 +apply (blast intro: order_less_trans)
   2.657 +done
   2.658 +
   2.659 +
   2.660 +lemma mem_inverse_set:
   2.661 +     "A \<in> preal ==> inverse_set A \<in> preal"
   2.662 +apply (simp (no_asm_simp) add: preal_def cut_def)
   2.663 +apply (blast intro!: inverse_set_not_empty inverse_set_not_rat_set
   2.664 +                     inverse_set_lemma3 inverse_set_lemma4)
   2.665 +done
   2.666 +
   2.667 +
   2.668 +subsection{*Gleason's Lemma 9-3.4, page 122*}
   2.669 +
   2.670 +lemma Gleason9_34_exists:
   2.671 +  assumes A: "A \<in> preal"
   2.672 +    and "\<forall>x\<in>A. x + u \<in> A"
   2.673 +    and "0 \<le> z"
   2.674 +  shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
   2.675 +proof (cases z rule: int_cases)
   2.676 +  case (nonneg n)
   2.677 +  show ?thesis
   2.678 +  proof (simp add: prems, induct n)
   2.679 +    case 0
   2.680 +      from preal_nonempty [OF A]
   2.681 +      show ?case  by force 
   2.682 +    case (Suc k)
   2.683 +      from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
   2.684 +      hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
   2.685 +      thus ?case by (force simp add: algebra_simps prems) 
   2.686 +  qed
   2.687 +next
   2.688 +  case (neg n)
   2.689 +  with prems show ?thesis by simp
   2.690 +qed
   2.691 +
   2.692 +lemma Gleason9_34_contra:
   2.693 +  assumes A: "A \<in> preal"
   2.694 +    shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
   2.695 +proof (induct u, induct y)
   2.696 +  fix a::int and b::int
   2.697 +  fix c::int and d::int
   2.698 +  assume bpos [simp]: "0 < b"
   2.699 +    and dpos [simp]: "0 < d"
   2.700 +    and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
   2.701 +    and upos: "0 < Fract c d"
   2.702 +    and ypos: "0 < Fract a b"
   2.703 +    and notin: "Fract a b \<notin> A"
   2.704 +  have cpos [simp]: "0 < c" 
   2.705 +    by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos) 
   2.706 +  have apos [simp]: "0 < a" 
   2.707 +    by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos) 
   2.708 +  let ?k = "a*d"
   2.709 +  have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
   2.710 +  proof -
   2.711 +    have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
   2.712 +      by (simp add: order_less_imp_not_eq2 mult_ac) 
   2.713 +    moreover
   2.714 +    have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
   2.715 +      by (rule mult_mono, 
   2.716 +          simp_all add: int_one_le_iff_zero_less zero_less_mult_iff 
   2.717 +                        order_less_imp_le)
   2.718 +    ultimately
   2.719 +    show ?thesis by simp
   2.720 +  qed
   2.721 +  have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff)  
   2.722 +  from Gleason9_34_exists [OF A closed k]
   2.723 +  obtain z where z: "z \<in> A" 
   2.724 +             and mem: "z + of_int ?k * Fract c d \<in> A" ..
   2.725 +  have less: "z + of_int ?k * Fract c d < Fract a b"
   2.726 +    by (rule not_in_preal_ub [OF A notin mem ypos])
   2.727 +  have "0<z" by (rule preal_imp_pos [OF A z])
   2.728 +  with frle and less show False by (simp add: Fract_of_int_eq) 
   2.729 +qed
   2.730 +
   2.731 +
   2.732 +lemma Gleason9_34:
   2.733 +  assumes A: "A \<in> preal"
   2.734 +    and upos: "0 < u"
   2.735 +  shows "\<exists>r \<in> A. r + u \<notin> A"
   2.736 +proof (rule ccontr, simp)
   2.737 +  assume closed: "\<forall>r\<in>A. r + u \<in> A"
   2.738 +  from preal_exists_bound [OF A]
   2.739 +  obtain y where y: "y \<notin> A" and ypos: "0 < y" by blast
   2.740 +  show False
   2.741 +    by (rule Gleason9_34_contra [OF A closed upos ypos y])
   2.742 +qed
   2.743 +
   2.744 +
   2.745 +
   2.746 +subsection{*Gleason's Lemma 9-3.6*}
   2.747 +
   2.748 +lemma lemma_gleason9_36:
   2.749 +  assumes A: "A \<in> preal"
   2.750 +    and x: "1 < x"
   2.751 +  shows "\<exists>r \<in> A. r*x \<notin> A"
   2.752 +proof -
   2.753 +  from preal_nonempty [OF A]
   2.754 +  obtain y where y: "y \<in> A" and  ypos: "0<y" ..
   2.755 +  show ?thesis 
   2.756 +  proof (rule classical)
   2.757 +    assume "~(\<exists>r\<in>A. r * x \<notin> A)"
   2.758 +    with y have ymem: "y * x \<in> A" by blast 
   2.759 +    from ypos mult_strict_left_mono [OF x]
   2.760 +    have yless: "y < y*x" by simp 
   2.761 +    let ?d = "y*x - y"
   2.762 +    from yless have dpos: "0 < ?d" and eq: "y + ?d = y*x" by auto
   2.763 +    from Gleason9_34 [OF A dpos]
   2.764 +    obtain r where r: "r\<in>A" and notin: "r + ?d \<notin> A" ..
   2.765 +    have rpos: "0<r" by (rule preal_imp_pos [OF A r])
   2.766 +    with dpos have rdpos: "0 < r + ?d" by arith
   2.767 +    have "~ (r + ?d \<le> y + ?d)"
   2.768 +    proof
   2.769 +      assume le: "r + ?d \<le> y + ?d" 
   2.770 +      from ymem have yd: "y + ?d \<in> A" by (simp add: eq)
   2.771 +      have "r + ?d \<in> A" by (rule preal_downwards_closed' [OF A yd rdpos le])
   2.772 +      with notin show False by simp
   2.773 +    qed
   2.774 +    hence "y < r" by simp
   2.775 +    with ypos have  dless: "?d < (r * ?d)/y"
   2.776 +      by (simp add: pos_less_divide_eq mult_commute [of ?d]
   2.777 +                    mult_strict_right_mono dpos)
   2.778 +    have "r + ?d < r*x"
   2.779 +    proof -
   2.780 +      have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
   2.781 +      also with ypos have "... = (r/y) * (y + ?d)"
   2.782 +        by (simp only: algebra_simps divide_inverse, simp)
   2.783 +      also have "... = r*x" using ypos
   2.784 +        by simp
   2.785 +      finally show "r + ?d < r*x" .
   2.786 +    qed
   2.787 +    with r notin rdpos
   2.788 +    show "\<exists>r\<in>A. r * x \<notin> A" by (blast dest:  preal_downwards_closed [OF A])
   2.789 +  qed  
   2.790 +qed
   2.791 +
   2.792 +subsection{*Existence of Inverse: Part 2*}
   2.793 +
   2.794 +lemma mem_Rep_preal_inverse_iff:
   2.795 +      "(z \<in> Rep_preal(inverse R)) = 
   2.796 +       (0 < z \<and> (\<exists>y. z < y \<and> inverse y \<notin> Rep_preal R))"
   2.797 +apply (simp add: preal_inverse_def mem_inverse_set Rep_preal)
   2.798 +apply (simp add: inverse_set_def) 
   2.799 +done
   2.800 +
   2.801 +lemma Rep_preal_one:
   2.802 +     "Rep_preal 1 = {x. 0 < x \<and> x < 1}"
   2.803 +by (simp add: preal_one_def rat_mem_preal)
   2.804 +
   2.805 +lemma subset_inverse_mult_lemma:
   2.806 +  assumes xpos: "0 < x" and xless: "x < 1"
   2.807 +  shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R & 
   2.808 +    u \<in> Rep_preal R & x = r * u"
   2.809 +proof -
   2.810 +  from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff)
   2.811 +  from lemma_gleason9_36 [OF Rep_preal this]
   2.812 +  obtain r where r: "r \<in> Rep_preal R" 
   2.813 +             and notin: "r * (inverse x) \<notin> Rep_preal R" ..
   2.814 +  have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
   2.815 +  from preal_exists_greater [OF Rep_preal r]
   2.816 +  obtain u where u: "u \<in> Rep_preal R" and rless: "r < u" ..
   2.817 +  have upos: "0<u" by (rule preal_imp_pos [OF Rep_preal u])
   2.818 +  show ?thesis
   2.819 +  proof (intro exI conjI)
   2.820 +    show "0 < x/u" using xpos upos
   2.821 +      by (simp add: zero_less_divide_iff)  
   2.822 +    show "x/u < x/r" using xpos upos rpos
   2.823 +      by (simp add: divide_inverse mult_less_cancel_left rless) 
   2.824 +    show "inverse (x / r) \<notin> Rep_preal R" using notin
   2.825 +      by (simp add: divide_inverse mult_commute) 
   2.826 +    show "u \<in> Rep_preal R" by (rule u) 
   2.827 +    show "x = x / u * u" using upos 
   2.828 +      by (simp add: divide_inverse mult_commute) 
   2.829 +  qed
   2.830 +qed
   2.831 +
   2.832 +lemma subset_inverse_mult: 
   2.833 +     "Rep_preal 1 \<subseteq> Rep_preal(inverse R * R)"
   2.834 +apply (auto simp add: Bex_def Rep_preal_one mem_Rep_preal_inverse_iff 
   2.835 +                      mem_Rep_preal_mult_iff)
   2.836 +apply (blast dest: subset_inverse_mult_lemma) 
   2.837 +done
   2.838 +
   2.839 +lemma inverse_mult_subset_lemma:
   2.840 +  assumes rpos: "0 < r" 
   2.841 +    and rless: "r < y"
   2.842 +    and notin: "inverse y \<notin> Rep_preal R"
   2.843 +    and q: "q \<in> Rep_preal R"
   2.844 +  shows "r*q < 1"
   2.845 +proof -
   2.846 +  have "q < inverse y" using rpos rless
   2.847 +    by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
   2.848 +  hence "r * q < r/y" using rpos
   2.849 +    by (simp add: divide_inverse mult_less_cancel_left)
   2.850 +  also have "... \<le> 1" using rpos rless
   2.851 +    by (simp add: pos_divide_le_eq)
   2.852 +  finally show ?thesis .
   2.853 +qed
   2.854 +
   2.855 +lemma inverse_mult_subset:
   2.856 +     "Rep_preal(inverse R * R) \<subseteq> Rep_preal 1"
   2.857 +apply (auto simp add: Bex_def Rep_preal_one mem_Rep_preal_inverse_iff
   2.858 +                      mem_Rep_preal_mult_iff)
   2.859 +apply (simp add: zero_less_mult_iff preal_imp_pos [OF Rep_preal]) 
   2.860 +apply (blast intro: inverse_mult_subset_lemma) 
   2.861 +done
   2.862 +
   2.863 +lemma preal_mult_inverse: "inverse R * R = (1::preal)"
   2.864 +apply (rule Rep_preal_inject [THEN iffD1])
   2.865 +apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) 
   2.866 +done
   2.867 +
   2.868 +lemma preal_mult_inverse_right: "R * inverse R = (1::preal)"
   2.869 +apply (rule preal_mult_commute [THEN subst])
   2.870 +apply (rule preal_mult_inverse)
   2.871 +done
   2.872 +
   2.873 +
   2.874 +text{*Theorems needing @{text Gleason9_34}*}
   2.875 +
   2.876 +lemma Rep_preal_self_subset: "Rep_preal (R) \<subseteq> Rep_preal(R + S)"
   2.877 +proof 
   2.878 +  fix r
   2.879 +  assume r: "r \<in> Rep_preal R"
   2.880 +  have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
   2.881 +  from mem_Rep_preal_Ex 
   2.882 +  obtain y where y: "y \<in> Rep_preal S" ..
   2.883 +  have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
   2.884 +  have ry: "r+y \<in> Rep_preal(R + S)" using r y
   2.885 +    by (auto simp add: mem_Rep_preal_add_iff)
   2.886 +  show "r \<in> Rep_preal(R + S)" using r ypos rpos 
   2.887 +    by (simp add:  preal_downwards_closed [OF Rep_preal ry]) 
   2.888 +qed
   2.889 +
   2.890 +lemma Rep_preal_sum_not_subset: "~ Rep_preal (R + S) \<subseteq> Rep_preal(R)"
   2.891 +proof -
   2.892 +  from mem_Rep_preal_Ex 
   2.893 +  obtain y where y: "y \<in> Rep_preal S" ..
   2.894 +  have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
   2.895 +  from  Gleason9_34 [OF Rep_preal ypos]
   2.896 +  obtain r where r: "r \<in> Rep_preal R" and notin: "r + y \<notin> Rep_preal R" ..
   2.897 +  have "r + y \<in> Rep_preal (R + S)" using r y
   2.898 +    by (auto simp add: mem_Rep_preal_add_iff)
   2.899 +  thus ?thesis using notin by blast
   2.900 +qed
   2.901 +
   2.902 +lemma Rep_preal_sum_not_eq: "Rep_preal (R + S) \<noteq> Rep_preal(R)"
   2.903 +by (insert Rep_preal_sum_not_subset, blast)
   2.904 +
   2.905 +text{*at last, Gleason prop. 9-3.5(iii) page 123*}
   2.906 +lemma preal_self_less_add_left: "(R::preal) < R + S"
   2.907 +apply (unfold preal_less_def less_le)
   2.908 +apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
   2.909 +done
   2.910 +
   2.911 +
   2.912 +subsection{*Subtraction for Positive Reals*}
   2.913 +
   2.914 +text{*Gleason prop. 9-3.5(iv), page 123: proving @{prop "A < B ==> \<exists>D. A + D =
   2.915 +B"}. We define the claimed @{term D} and show that it is a positive real*}
   2.916 +
   2.917 +text{*Part 1 of Dedekind sections definition*}
   2.918 +lemma diff_set_not_empty:
   2.919 +     "R < S ==> {} \<subset> diff_set (Rep_preal S) (Rep_preal R)"
   2.920 +apply (auto simp add: preal_less_def diff_set_def elim!: equalityE) 
   2.921 +apply (frule_tac x1 = S in Rep_preal [THEN preal_exists_greater])
   2.922 +apply (drule preal_imp_pos [OF Rep_preal], clarify)
   2.923 +apply (cut_tac a=x and b=u in add_eq_exists, force) 
   2.924 +done
   2.925 +
   2.926 +text{*Part 2 of Dedekind sections definition*}
   2.927 +lemma diff_set_nonempty:
   2.928 +     "\<exists>q. 0 < q & q \<notin> diff_set (Rep_preal S) (Rep_preal R)"
   2.929 +apply (cut_tac X = S in Rep_preal_exists_bound)
   2.930 +apply (erule exE)
   2.931 +apply (rule_tac x = x in exI, auto)
   2.932 +apply (simp add: diff_set_def) 
   2.933 +apply (auto dest: Rep_preal [THEN preal_downwards_closed])
   2.934 +done
   2.935 +
   2.936 +lemma diff_set_not_rat_set:
   2.937 +  "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
   2.938 +proof
   2.939 +  show "?lhs \<subseteq> ?rhs" by (auto simp add: diff_set_def) 
   2.940 +  show "?lhs \<noteq> ?rhs" using diff_set_nonempty by blast
   2.941 +qed
   2.942 +
   2.943 +text{*Part 3 of Dedekind sections definition*}
   2.944 +lemma diff_set_lemma3:
   2.945 +     "[|R < S; u \<in> diff_set (Rep_preal S) (Rep_preal R); 0 < z; z < u|] 
   2.946 +      ==> z \<in> diff_set (Rep_preal S) (Rep_preal R)"
   2.947 +apply (auto simp add: diff_set_def) 
   2.948 +apply (rule_tac x=x in exI) 
   2.949 +apply (drule Rep_preal [THEN preal_downwards_closed], auto)
   2.950 +done
   2.951 +
   2.952 +text{*Part 4 of Dedekind sections definition*}
   2.953 +lemma diff_set_lemma4:
   2.954 +     "[|R < S; y \<in> diff_set (Rep_preal S) (Rep_preal R)|] 
   2.955 +      ==> \<exists>u \<in> diff_set (Rep_preal S) (Rep_preal R). y < u"
   2.956 +apply (auto simp add: diff_set_def) 
   2.957 +apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
   2.958 +apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify)  
   2.959 +apply (rule_tac x="y+xa" in exI) 
   2.960 +apply (auto simp add: add_ac)
   2.961 +done
   2.962 +
   2.963 +lemma mem_diff_set:
   2.964 +     "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
   2.965 +apply (unfold preal_def cut_def)
   2.966 +apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
   2.967 +                     diff_set_lemma3 diff_set_lemma4)
   2.968 +done
   2.969 +
   2.970 +lemma mem_Rep_preal_diff_iff:
   2.971 +      "R < S ==>
   2.972 +       (z \<in> Rep_preal(S-R)) = 
   2.973 +       (\<exists>x. 0 < x & 0 < z & x \<notin> Rep_preal R & x + z \<in> Rep_preal S)"
   2.974 +apply (simp add: preal_diff_def mem_diff_set Rep_preal)
   2.975 +apply (force simp add: diff_set_def) 
   2.976 +done
   2.977 +
   2.978 +
   2.979 +text{*proving that @{term "R + D \<le> S"}*}
   2.980 +
   2.981 +lemma less_add_left_lemma:
   2.982 +  assumes Rless: "R < S"
   2.983 +    and a: "a \<in> Rep_preal R"
   2.984 +    and cb: "c + b \<in> Rep_preal S"
   2.985 +    and "c \<notin> Rep_preal R"
   2.986 +    and "0 < b"
   2.987 +    and "0 < c"
   2.988 +  shows "a + b \<in> Rep_preal S"
   2.989 +proof -
   2.990 +  have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
   2.991 +  moreover
   2.992 +  have "a < c" using prems
   2.993 +    by (blast intro: not_in_Rep_preal_ub ) 
   2.994 +  ultimately show ?thesis using prems
   2.995 +    by (simp add: preal_downwards_closed [OF Rep_preal cb]) 
   2.996 +qed
   2.997 +
   2.998 +lemma less_add_left_le1:
   2.999 +       "R < (S::preal) ==> R + (S-R) \<le> S"
  2.1000 +apply (auto simp add: Bex_def preal_le_def mem_Rep_preal_add_iff 
  2.1001 +                      mem_Rep_preal_diff_iff)
  2.1002 +apply (blast intro: less_add_left_lemma) 
  2.1003 +done
  2.1004 +
  2.1005 +subsection{*proving that @{term "S \<le> R + D"} --- trickier*}
  2.1006 +
  2.1007 +lemma lemma_sum_mem_Rep_preal_ex:
  2.1008 +     "x \<in> Rep_preal S ==> \<exists>e. 0 < e & x + e \<in> Rep_preal S"
  2.1009 +apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
  2.1010 +apply (cut_tac a=x and b=u in add_eq_exists, auto) 
  2.1011 +done
  2.1012 +
  2.1013 +lemma less_add_left_lemma2:
  2.1014 +  assumes Rless: "R < S"
  2.1015 +    and x:     "x \<in> Rep_preal S"
  2.1016 +    and xnot: "x \<notin>  Rep_preal R"
  2.1017 +  shows "\<exists>u v z. 0 < v & 0 < z & u \<in> Rep_preal R & z \<notin> Rep_preal R & 
  2.1018 +                     z + v \<in> Rep_preal S & x = u + v"
  2.1019 +proof -
  2.1020 +  have xpos: "0<x" by (rule preal_imp_pos [OF Rep_preal x])
  2.1021 +  from lemma_sum_mem_Rep_preal_ex [OF x]
  2.1022 +  obtain e where epos: "0 < e" and xe: "x + e \<in> Rep_preal S" by blast
  2.1023 +  from  Gleason9_34 [OF Rep_preal epos]
  2.1024 +  obtain r where r: "r \<in> Rep_preal R" and notin: "r + e \<notin> Rep_preal R" ..
  2.1025 +  with x xnot xpos have rless: "r < x" by (blast intro: not_in_Rep_preal_ub)
  2.1026 +  from add_eq_exists [of r x]
  2.1027 +  obtain y where eq: "x = r+y" by auto
  2.1028 +  show ?thesis 
  2.1029 +  proof (intro exI conjI)
  2.1030 +    show "r \<in> Rep_preal R" by (rule r)
  2.1031 +    show "r + e \<notin> Rep_preal R" by (rule notin)
  2.1032 +    show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac)
  2.1033 +    show "x = r + y" by (simp add: eq)
  2.1034 +    show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r]
  2.1035 +      by simp
  2.1036 +    show "0 < y" using rless eq by arith
  2.1037 +  qed
  2.1038 +qed
  2.1039 +
  2.1040 +lemma less_add_left_le2: "R < (S::preal) ==> S \<le> R + (S-R)"
  2.1041 +apply (auto simp add: preal_le_def)
  2.1042 +apply (case_tac "x \<in> Rep_preal R")
  2.1043 +apply (cut_tac Rep_preal_self_subset [of R], force)
  2.1044 +apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_diff_iff)
  2.1045 +apply (blast dest: less_add_left_lemma2)
  2.1046 +done
  2.1047 +
  2.1048 +lemma less_add_left: "R < (S::preal) ==> R + (S-R) = S"
  2.1049 +by (blast intro: antisym [OF less_add_left_le1 less_add_left_le2])
  2.1050 +
  2.1051 +lemma less_add_left_Ex: "R < (S::preal) ==> \<exists>D. R + D = S"
  2.1052 +by (fast dest: less_add_left)
  2.1053 +
  2.1054 +lemma preal_add_less2_mono1: "R < (S::preal) ==> R + T < S + T"
  2.1055 +apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc)
  2.1056 +apply (rule_tac y1 = D in preal_add_commute [THEN subst])
  2.1057 +apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric])
  2.1058 +done
  2.1059 +
  2.1060 +lemma preal_add_less2_mono2: "R < (S::preal) ==> T + R < T + S"
  2.1061 +by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of T])
  2.1062 +
  2.1063 +lemma preal_add_right_less_cancel: "R + T < S + T ==> R < (S::preal)"
  2.1064 +apply (insert linorder_less_linear [of R S], auto)
  2.1065 +apply (drule_tac R = S and T = T in preal_add_less2_mono1)
  2.1066 +apply (blast dest: order_less_trans) 
  2.1067 +done
  2.1068 +
  2.1069 +lemma preal_add_left_less_cancel: "T + R < T + S ==> R <  (S::preal)"
  2.1070 +by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T])
  2.1071 +
  2.1072 +lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)"
  2.1073 +by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
  2.1074 +
  2.1075 +lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
  2.1076 +by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left) 
  2.1077 +
  2.1078 +lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S"
  2.1079 +apply (insert linorder_less_linear [of R S], safe)
  2.1080 +apply (drule_tac [!] T = T in preal_add_less2_mono1, auto)
  2.1081 +done
  2.1082 +
  2.1083 +lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)"
  2.1084 +by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
  2.1085 +
  2.1086 +instance preal :: linordered_cancel_ab_semigroup_add
  2.1087 +proof
  2.1088 +  fix a b c :: preal
  2.1089 +  show "a + b = a + c \<Longrightarrow> b = c" by (rule preal_add_left_cancel)
  2.1090 +  show "a \<le> b \<Longrightarrow> c + a \<le> c + b" by (simp only: preal_add_le_cancel_left)
  2.1091 +qed
  2.1092 +
  2.1093 +
  2.1094 +subsection{*Completeness of type @{typ preal}*}
  2.1095 +
  2.1096 +text{*Prove that supremum is a cut*}
  2.1097 +
  2.1098 +text{*Part 1 of Dedekind sections definition*}
  2.1099 +
  2.1100 +lemma preal_sup_set_not_empty:
  2.1101 +     "P \<noteq> {} ==> {} \<subset> (\<Union>X \<in> P. Rep_preal(X))"
  2.1102 +apply auto
  2.1103 +apply (cut_tac X = x in mem_Rep_preal_Ex, auto)
  2.1104 +done
  2.1105 +
  2.1106 +
  2.1107 +text{*Part 2 of Dedekind sections definition*}
  2.1108 +
  2.1109 +lemma preal_sup_not_exists:
  2.1110 +     "\<forall>X \<in> P. X \<le> Y ==> \<exists>q. 0 < q & q \<notin> (\<Union>X \<in> P. Rep_preal(X))"
  2.1111 +apply (cut_tac X = Y in Rep_preal_exists_bound)
  2.1112 +apply (auto simp add: preal_le_def)
  2.1113 +done
  2.1114 +
  2.1115 +lemma preal_sup_set_not_rat_set:
  2.1116 +     "\<forall>X \<in> P. X \<le> Y ==> (\<Union>X \<in> P. Rep_preal(X)) < {r. 0 < r}"
  2.1117 +apply (drule preal_sup_not_exists)
  2.1118 +apply (blast intro: preal_imp_pos [OF Rep_preal])  
  2.1119 +done
  2.1120 +
  2.1121 +text{*Part 3 of Dedekind sections definition*}
  2.1122 +lemma preal_sup_set_lemma3:
  2.1123 +     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; u \<in> (\<Union>X \<in> P. Rep_preal(X)); 0 < z; z < u|]
  2.1124 +      ==> z \<in> (\<Union>X \<in> P. Rep_preal(X))"
  2.1125 +by (auto elim: Rep_preal [THEN preal_downwards_closed])
  2.1126 +
  2.1127 +text{*Part 4 of Dedekind sections definition*}
  2.1128 +lemma preal_sup_set_lemma4:
  2.1129 +     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; y \<in> (\<Union>X \<in> P. Rep_preal(X)) |]
  2.1130 +          ==> \<exists>u \<in> (\<Union>X \<in> P. Rep_preal(X)). y < u"
  2.1131 +by (blast dest: Rep_preal [THEN preal_exists_greater])
  2.1132 +
  2.1133 +lemma preal_sup:
  2.1134 +     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
  2.1135 +apply (unfold preal_def cut_def)
  2.1136 +apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
  2.1137 +                     preal_sup_set_lemma3 preal_sup_set_lemma4)
  2.1138 +done
  2.1139 +
  2.1140 +lemma preal_psup_le:
  2.1141 +     "[| \<forall>X \<in> P. X \<le> Y;  x \<in> P |] ==> x \<le> psup P"
  2.1142 +apply (simp (no_asm_simp) add: preal_le_def) 
  2.1143 +apply (subgoal_tac "P \<noteq> {}") 
  2.1144 +apply (auto simp add: psup_def preal_sup) 
  2.1145 +done
  2.1146 +
  2.1147 +lemma psup_le_ub: "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> Y"
  2.1148 +apply (simp (no_asm_simp) add: preal_le_def)
  2.1149 +apply (simp add: psup_def preal_sup) 
  2.1150 +apply (auto simp add: preal_le_def)
  2.1151 +done
  2.1152 +
  2.1153 +text{*Supremum property*}
  2.1154 +lemma preal_complete:
  2.1155 +     "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> (\<exists>X \<in> P. Z < X) = (Z < psup P)"
  2.1156 +apply (simp add: preal_less_def psup_def preal_sup)
  2.1157 +apply (auto simp add: preal_le_def)
  2.1158 +apply (rename_tac U) 
  2.1159 +apply (cut_tac x = U and y = Z in linorder_less_linear)
  2.1160 +apply (auto simp add: preal_less_def)
  2.1161 +done
  2.1162 +
  2.1163 +section {*Defining the Reals from the Positive Reals*}
  2.1164 +
  2.1165 +definition
  2.1166 +  realrel   ::  "((preal * preal) * (preal * preal)) set" where
  2.1167 +  [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
  2.1168 +
  2.1169 +typedef (Real)  real = "UNIV//realrel"
  2.1170 +  by (auto simp add: quotient_def)
  2.1171 +
  2.1172 +definition
  2.1173 +  (** these don't use the overloaded "real" function: users don't see them **)
  2.1174 +  real_of_preal :: "preal => real" where
  2.1175 +  [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
  2.1176 +
  2.1177 +instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
  2.1178 +begin
  2.1179 +
  2.1180 +definition
  2.1181 +  real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
  2.1182 +
  2.1183 +definition
  2.1184 +  real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
  2.1185 +
  2.1186 +definition
  2.1187 +  real_add_def [code del]: "z + w =
  2.1188 +       contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
  2.1189 +                 { Abs_Real(realrel``{(x+u, y+v)}) })"
  2.1190 +
  2.1191 +definition
  2.1192 +  real_minus_def [code del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
  2.1193 +
  2.1194 +definition
  2.1195 +  real_diff_def [code del]: "r - (s::real) = r + - s"
  2.1196 +
  2.1197 +definition
  2.1198 +  real_mult_def [code del]:
  2.1199 +    "z * w =
  2.1200 +       contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
  2.1201 +                 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
  2.1202 +
  2.1203 +definition
  2.1204 +  real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
  2.1205 +
  2.1206 +definition
  2.1207 +  real_divide_def [code del]: "R / (S::real) = R * inverse S"
  2.1208 +
  2.1209 +definition
  2.1210 +  real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
  2.1211 +    (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
  2.1212 +
  2.1213 +definition
  2.1214 +  real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
  2.1215 +
  2.1216 +definition
  2.1217 +  real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
  2.1218 +
  2.1219 +definition
  2.1220 +  real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0<x then 1 else - 1)"
  2.1221 +
  2.1222 +instance ..
  2.1223 +
  2.1224 +end
  2.1225 +
  2.1226 +subsection {* Equivalence relation over positive reals *}
  2.1227 +
  2.1228 +lemma preal_trans_lemma:
  2.1229 +  assumes "x + y1 = x1 + y"
  2.1230 +      and "x + y2 = x2 + y"
  2.1231 +  shows "x1 + y2 = x2 + (y1::preal)"
  2.1232 +proof -
  2.1233 +  have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
  2.1234 +  also have "... = (x2 + y) + x1"  by (simp add: prems)
  2.1235 +  also have "... = x2 + (x1 + y)"  by (simp add: add_ac)
  2.1236 +  also have "... = x2 + (x + y1)"  by (simp add: prems)
  2.1237 +  also have "... = (x2 + y1) + x"  by (simp add: add_ac)
  2.1238 +  finally have "(x1 + y2) + x = (x2 + y1) + x" .
  2.1239 +  thus ?thesis by (rule add_right_imp_eq)
  2.1240 +qed
  2.1241 +
  2.1242 +
  2.1243 +lemma realrel_iff [simp]: "(((x1,y1),(x2,y2)) \<in> realrel) = (x1 + y2 = x2 + y1)"
  2.1244 +by (simp add: realrel_def)
  2.1245 +
  2.1246 +lemma equiv_realrel: "equiv UNIV realrel"
  2.1247 +apply (auto simp add: equiv_def refl_on_def sym_def trans_def realrel_def)
  2.1248 +apply (blast dest: preal_trans_lemma) 
  2.1249 +done
  2.1250 +
  2.1251 +text{*Reduces equality of equivalence classes to the @{term realrel} relation:
  2.1252 +  @{term "(realrel `` {x} = realrel `` {y}) = ((x,y) \<in> realrel)"} *}
  2.1253 +lemmas equiv_realrel_iff = 
  2.1254 +       eq_equiv_class_iff [OF equiv_realrel UNIV_I UNIV_I]
  2.1255 +
  2.1256 +declare equiv_realrel_iff [simp]
  2.1257 +
  2.1258 +
  2.1259 +lemma realrel_in_real [simp]: "realrel``{(x,y)}: Real"
  2.1260 +by (simp add: Real_def realrel_def quotient_def, blast)
  2.1261 +
  2.1262 +declare Abs_Real_inject [simp]
  2.1263 +declare Abs_Real_inverse [simp]
  2.1264 +
  2.1265 +
  2.1266 +text{*Case analysis on the representation of a real number as an equivalence
  2.1267 +      class of pairs of positive reals.*}
  2.1268 +lemma eq_Abs_Real [case_names Abs_Real, cases type: real]: 
  2.1269 +     "(!!x y. z = Abs_Real(realrel``{(x,y)}) ==> P) ==> P"
  2.1270 +apply (rule Rep_Real [of z, unfolded Real_def, THEN quotientE])
  2.1271 +apply (drule arg_cong [where f=Abs_Real])
  2.1272 +apply (auto simp add: Rep_Real_inverse)
  2.1273 +done
  2.1274 +
  2.1275 +
  2.1276 +subsection {* Addition and Subtraction *}
  2.1277 +
  2.1278 +lemma real_add_congruent2_lemma:
  2.1279 +     "[|a + ba = aa + b; ab + bc = ac + bb|]
  2.1280 +      ==> a + ab + (ba + bc) = aa + ac + (b + (bb::preal))"
  2.1281 +apply (simp add: add_assoc)
  2.1282 +apply (rule add_left_commute [of ab, THEN ssubst])
  2.1283 +apply (simp add: add_assoc [symmetric])
  2.1284 +apply (simp add: add_ac)
  2.1285 +done
  2.1286 +
  2.1287 +lemma real_add:
  2.1288 +     "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) =
  2.1289 +      Abs_Real (realrel``{(x+u, y+v)})"
  2.1290 +proof -
  2.1291 +  have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
  2.1292 +        respects2 realrel"
  2.1293 +    by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
  2.1294 +  thus ?thesis
  2.1295 +    by (simp add: real_add_def UN_UN_split_split_eq
  2.1296 +                  UN_equiv_class2 [OF equiv_realrel equiv_realrel])
  2.1297 +qed
  2.1298 +
  2.1299 +lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
  2.1300 +proof -
  2.1301 +  have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
  2.1302 +    by (simp add: congruent_def add_commute) 
  2.1303 +  thus ?thesis
  2.1304 +    by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
  2.1305 +qed
  2.1306 +
  2.1307 +instance real :: ab_group_add
  2.1308 +proof
  2.1309 +  fix x y z :: real
  2.1310 +  show "(x + y) + z = x + (y + z)"
  2.1311 +    by (cases x, cases y, cases z, simp add: real_add add_assoc)
  2.1312 +  show "x + y = y + x"
  2.1313 +    by (cases x, cases y, simp add: real_add add_commute)
  2.1314 +  show "0 + x = x"
  2.1315 +    by (cases x, simp add: real_add real_zero_def add_ac)
  2.1316 +  show "- x + x = 0"
  2.1317 +    by (cases x, simp add: real_minus real_add real_zero_def add_commute)
  2.1318 +  show "x - y = x + - y"
  2.1319 +    by (simp add: real_diff_def)
  2.1320 +qed
  2.1321 +
  2.1322 +
  2.1323 +subsection {* Multiplication *}
  2.1324 +
  2.1325 +lemma real_mult_congruent2_lemma:
  2.1326 +     "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==>
  2.1327 +          x * x1 + y * y1 + (x * y2 + y * x2) =
  2.1328 +          x * x2 + y * y2 + (x * y1 + y * x1)"
  2.1329 +apply (simp add: add_left_commute add_assoc [symmetric])
  2.1330 +apply (simp add: add_assoc right_distrib [symmetric])
  2.1331 +apply (simp add: add_commute)
  2.1332 +done
  2.1333 +
  2.1334 +lemma real_mult_congruent2:
  2.1335 +    "(%p1 p2.
  2.1336 +        (%(x1,y1). (%(x2,y2). 
  2.1337 +          { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)
  2.1338 +     respects2 realrel"
  2.1339 +apply (rule congruent2_commuteI [OF equiv_realrel], clarify)
  2.1340 +apply (simp add: mult_commute add_commute)
  2.1341 +apply (auto simp add: real_mult_congruent2_lemma)
  2.1342 +done
  2.1343 +
  2.1344 +lemma real_mult:
  2.1345 +      "Abs_Real((realrel``{(x1,y1)})) * Abs_Real((realrel``{(x2,y2)})) =
  2.1346 +       Abs_Real(realrel `` {(x1*x2+y1*y2,x1*y2+y1*x2)})"
  2.1347 +by (simp add: real_mult_def UN_UN_split_split_eq
  2.1348 +         UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2])
  2.1349 +
  2.1350 +lemma real_mult_commute: "(z::real) * w = w * z"
  2.1351 +by (cases z, cases w, simp add: real_mult add_ac mult_ac)
  2.1352 +
  2.1353 +lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
  2.1354 +apply (cases z1, cases z2, cases z3)
  2.1355 +apply (simp add: real_mult algebra_simps)
  2.1356 +done
  2.1357 +
  2.1358 +lemma real_mult_1: "(1::real) * z = z"
  2.1359 +apply (cases z)
  2.1360 +apply (simp add: real_mult real_one_def algebra_simps)
  2.1361 +done
  2.1362 +
  2.1363 +lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)"
  2.1364 +apply (cases z1, cases z2, cases w)
  2.1365 +apply (simp add: real_add real_mult algebra_simps)
  2.1366 +done
  2.1367 +
  2.1368 +text{*one and zero are distinct*}
  2.1369 +lemma real_zero_not_eq_one: "0 \<noteq> (1::real)"
  2.1370 +proof -
  2.1371 +  have "(1::preal) < 1 + 1"
  2.1372 +    by (simp add: preal_self_less_add_left)
  2.1373 +  thus ?thesis
  2.1374 +    by (simp add: real_zero_def real_one_def)
  2.1375 +qed
  2.1376 +
  2.1377 +instance real :: comm_ring_1
  2.1378 +proof
  2.1379 +  fix x y z :: real
  2.1380 +  show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
  2.1381 +  show "x * y = y * x" by (rule real_mult_commute)
  2.1382 +  show "1 * x = x" by (rule real_mult_1)
  2.1383 +  show "(x + y) * z = x * z + y * z" by (rule real_add_mult_distrib)
  2.1384 +  show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
  2.1385 +qed
  2.1386 +
  2.1387 +subsection {* Inverse and Division *}
  2.1388 +
  2.1389 +lemma real_zero_iff: "Abs_Real (realrel `` {(x, x)}) = 0"
  2.1390 +by (simp add: real_zero_def add_commute)
  2.1391 +
  2.1392 +text{*Instead of using an existential quantifier and constructing the inverse
  2.1393 +within the proof, we could define the inverse explicitly.*}
  2.1394 +
  2.1395 +lemma real_mult_inverse_left_ex: "x \<noteq> 0 ==> \<exists>y. y*x = (1::real)"
  2.1396 +apply (simp add: real_zero_def real_one_def, cases x)
  2.1397 +apply (cut_tac x = xa and y = y in linorder_less_linear)
  2.1398 +apply (auto dest!: less_add_left_Ex simp add: real_zero_iff)
  2.1399 +apply (rule_tac
  2.1400 +        x = "Abs_Real (realrel``{(1, inverse (D) + 1)})"
  2.1401 +       in exI)
  2.1402 +apply (rule_tac [2]
  2.1403 +        x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})" 
  2.1404 +       in exI)
  2.1405 +apply (auto simp add: real_mult preal_mult_inverse_right algebra_simps)
  2.1406 +done
  2.1407 +
  2.1408 +lemma real_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::real)"
  2.1409 +apply (simp add: real_inverse_def)
  2.1410 +apply (drule real_mult_inverse_left_ex, safe)
  2.1411 +apply (rule theI, assumption, rename_tac z)
  2.1412 +apply (subgoal_tac "(z * x) * y = z * (x * y)")
  2.1413 +apply (simp add: mult_commute)
  2.1414 +apply (rule mult_assoc)
  2.1415 +done
  2.1416 +
  2.1417 +
  2.1418 +subsection{*The Real Numbers form a Field*}
  2.1419 +
  2.1420 +instance real :: field_inverse_zero
  2.1421 +proof
  2.1422 +  fix x y z :: real
  2.1423 +  show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
  2.1424 +  show "x / y = x * inverse y" by (simp add: real_divide_def)
  2.1425 +  show "inverse 0 = (0::real)" by (simp add: real_inverse_def)
  2.1426 +qed
  2.1427 +
  2.1428 +
  2.1429 +subsection{*The @{text "\<le>"} Ordering*}
  2.1430 +
  2.1431 +lemma real_le_refl: "w \<le> (w::real)"
  2.1432 +by (cases w, force simp add: real_le_def)
  2.1433 +
  2.1434 +text{*The arithmetic decision procedure is not set up for type preal.
  2.1435 +  This lemma is currently unused, but it could simplify the proofs of the
  2.1436 +  following two lemmas.*}
  2.1437 +lemma preal_eq_le_imp_le:
  2.1438 +  assumes eq: "a+b = c+d" and le: "c \<le> a"
  2.1439 +  shows "b \<le> (d::preal)"
  2.1440 +proof -
  2.1441 +  have "c+d \<le> a+d" by (simp add: prems)
  2.1442 +  hence "a+b \<le> a+d" by (simp add: prems)
  2.1443 +  thus "b \<le> d" by simp
  2.1444 +qed
  2.1445 +
  2.1446 +lemma real_le_lemma:
  2.1447 +  assumes l: "u1 + v2 \<le> u2 + v1"
  2.1448 +      and "x1 + v1 = u1 + y1"
  2.1449 +      and "x2 + v2 = u2 + y2"
  2.1450 +  shows "x1 + y2 \<le> x2 + (y1::preal)"
  2.1451 +proof -
  2.1452 +  have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: prems)
  2.1453 +  hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: add_ac)
  2.1454 +  also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: prems)
  2.1455 +  finally show ?thesis by simp
  2.1456 +qed
  2.1457 +
  2.1458 +lemma real_le: 
  2.1459 +     "(Abs_Real(realrel``{(x1,y1)}) \<le> Abs_Real(realrel``{(x2,y2)})) =  
  2.1460 +      (x1 + y2 \<le> x2 + y1)"
  2.1461 +apply (simp add: real_le_def)
  2.1462 +apply (auto intro: real_le_lemma)
  2.1463 +done
  2.1464 +
  2.1465 +lemma real_le_antisym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
  2.1466 +by (cases z, cases w, simp add: real_le)
  2.1467 +
  2.1468 +lemma real_trans_lemma:
  2.1469 +  assumes "x + v \<le> u + y"
  2.1470 +      and "u + v' \<le> u' + v"
  2.1471 +      and "x2 + v2 = u2 + y2"
  2.1472 +  shows "x + v' \<le> u' + (y::preal)"
  2.1473 +proof -
  2.1474 +  have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac)
  2.1475 +  also have "... \<le> (u+y) + (u+v')" by (simp add: prems)
  2.1476 +  also have "... \<le> (u+y) + (u'+v)" by (simp add: prems)
  2.1477 +  also have "... = (u'+y) + (u+v)"  by (simp add: add_ac)
  2.1478 +  finally show ?thesis by simp
  2.1479 +qed
  2.1480 +
  2.1481 +lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
  2.1482 +apply (cases i, cases j, cases k)
  2.1483 +apply (simp add: real_le)
  2.1484 +apply (blast intro: real_trans_lemma)
  2.1485 +done
  2.1486 +
  2.1487 +instance real :: order
  2.1488 +proof
  2.1489 +  fix u v :: real
  2.1490 +  show "u < v \<longleftrightarrow> u \<le> v \<and> \<not> v \<le> u" 
  2.1491 +    by (auto simp add: real_less_def intro: real_le_antisym)
  2.1492 +qed (assumption | rule real_le_refl real_le_trans real_le_antisym)+
  2.1493 +
  2.1494 +(* Axiom 'linorder_linear' of class 'linorder': *)
  2.1495 +lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
  2.1496 +apply (cases z, cases w)
  2.1497 +apply (auto simp add: real_le real_zero_def add_ac)
  2.1498 +done
  2.1499 +
  2.1500 +instance real :: linorder
  2.1501 +  by (intro_classes, rule real_le_linear)
  2.1502 +
  2.1503 +
  2.1504 +lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
  2.1505 +apply (cases x, cases y) 
  2.1506 +apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
  2.1507 +                      add_ac)
  2.1508 +apply (simp_all add: add_assoc [symmetric])
  2.1509 +done
  2.1510 +
  2.1511 +lemma real_add_left_mono: 
  2.1512 +  assumes le: "x \<le> y" shows "z + x \<le> z + (y::real)"
  2.1513 +proof -
  2.1514 +  have "z + x - (z + y) = (z + -z) + (x - y)" 
  2.1515 +    by (simp add: algebra_simps) 
  2.1516 +  with le show ?thesis 
  2.1517 +    by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"] diff_minus)
  2.1518 +qed
  2.1519 +
  2.1520 +lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
  2.1521 +by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
  2.1522 +
  2.1523 +lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))"
  2.1524 +by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
  2.1525 +
  2.1526 +lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
  2.1527 +apply (cases x, cases y)
  2.1528 +apply (simp add: linorder_not_le [where 'a = real, symmetric] 
  2.1529 +                 linorder_not_le [where 'a = preal] 
  2.1530 +                  real_zero_def real_le real_mult)
  2.1531 +  --{*Reduce to the (simpler) @{text "\<le>"} relation *}
  2.1532 +apply (auto dest!: less_add_left_Ex
  2.1533 +     simp add: algebra_simps preal_self_less_add_left)
  2.1534 +done
  2.1535 +
  2.1536 +lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
  2.1537 +apply (rule real_sum_gt_zero_less)
  2.1538 +apply (drule real_less_sum_gt_zero [of x y])
  2.1539 +apply (drule real_mult_order, assumption)
  2.1540 +apply (simp add: right_distrib)
  2.1541 +done
  2.1542 +
  2.1543 +instantiation real :: distrib_lattice
  2.1544 +begin
  2.1545 +
  2.1546 +definition
  2.1547 +  "(inf \<Colon> real \<Rightarrow> real \<Rightarrow> real) = min"
  2.1548 +
  2.1549 +definition
  2.1550 +  "(sup \<Colon> real \<Rightarrow> real \<Rightarrow> real) = max"
  2.1551 +
  2.1552 +instance
  2.1553 +  by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
  2.1554 +
  2.1555 +end
  2.1556 +
  2.1557 +
  2.1558 +subsection{*The Reals Form an Ordered Field*}
  2.1559 +
  2.1560 +instance real :: linordered_field_inverse_zero
  2.1561 +proof
  2.1562 +  fix x y z :: real
  2.1563 +  show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
  2.1564 +  show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2)
  2.1565 +  show "\<bar>x\<bar> = (if x < 0 then -x else x)" by (simp only: real_abs_def)
  2.1566 +  show "sgn x = (if x=0 then 0 else if 0<x then 1 else - 1)"
  2.1567 +    by (simp only: real_sgn_def)
  2.1568 +qed
  2.1569 +
  2.1570 +text{*The function @{term real_of_preal} requires many proofs, but it seems
  2.1571 +to be essential for proving completeness of the reals from that of the
  2.1572 +positive reals.*}
  2.1573 +
  2.1574 +lemma real_of_preal_add:
  2.1575 +     "real_of_preal ((x::preal) + y) = real_of_preal x + real_of_preal y"
  2.1576 +by (simp add: real_of_preal_def real_add algebra_simps)
  2.1577 +
  2.1578 +lemma real_of_preal_mult:
  2.1579 +     "real_of_preal ((x::preal) * y) = real_of_preal x* real_of_preal y"
  2.1580 +by (simp add: real_of_preal_def real_mult algebra_simps)
  2.1581 +
  2.1582 +
  2.1583 +text{*Gleason prop 9-4.4 p 127*}
  2.1584 +lemma real_of_preal_trichotomy:
  2.1585 +      "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
  2.1586 +apply (simp add: real_of_preal_def real_zero_def, cases x)
  2.1587 +apply (auto simp add: real_minus add_ac)
  2.1588 +apply (cut_tac x = x and y = y in linorder_less_linear)
  2.1589 +apply (auto dest!: less_add_left_Ex simp add: add_assoc [symmetric])
  2.1590 +done
  2.1591 +
  2.1592 +lemma real_of_preal_leD:
  2.1593 +      "real_of_preal m1 \<le> real_of_preal m2 ==> m1 \<le> m2"
  2.1594 +by (simp add: real_of_preal_def real_le)
  2.1595 +
  2.1596 +lemma real_of_preal_lessI: "m1 < m2 ==> real_of_preal m1 < real_of_preal m2"
  2.1597 +by (auto simp add: real_of_preal_leD linorder_not_le [symmetric])
  2.1598 +
  2.1599 +lemma real_of_preal_lessD:
  2.1600 +      "real_of_preal m1 < real_of_preal m2 ==> m1 < m2"
  2.1601 +by (simp add: real_of_preal_def real_le linorder_not_le [symmetric])
  2.1602 +
  2.1603 +lemma real_of_preal_less_iff [simp]:
  2.1604 +     "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)"
  2.1605 +by (blast intro: real_of_preal_lessI real_of_preal_lessD)
  2.1606 +
  2.1607 +lemma real_of_preal_le_iff:
  2.1608 +     "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
  2.1609 +by (simp add: linorder_not_less [symmetric])
  2.1610 +
  2.1611 +lemma real_of_preal_zero_less: "0 < real_of_preal m"
  2.1612 +apply (insert preal_self_less_add_left [of 1 m])
  2.1613 +apply (auto simp add: real_zero_def real_of_preal_def
  2.1614 +                      real_less_def real_le_def add_ac)
  2.1615 +apply (rule_tac x="m + 1" in exI, rule_tac x="1" in exI)
  2.1616 +apply (simp add: add_ac)
  2.1617 +done
  2.1618 +
  2.1619 +lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0"
  2.1620 +by (simp add: real_of_preal_zero_less)
  2.1621 +
  2.1622 +lemma real_of_preal_not_minus_gt_zero: "~ 0 < - real_of_preal m"
  2.1623 +proof -
  2.1624 +  from real_of_preal_minus_less_zero
  2.1625 +  show ?thesis by (blast dest: order_less_trans)
  2.1626 +qed
  2.1627 +
  2.1628 +
  2.1629 +subsection{*Theorems About the Ordering*}
  2.1630 +
  2.1631 +lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)"
  2.1632 +apply (auto simp add: real_of_preal_zero_less)
  2.1633 +apply (cut_tac x = x in real_of_preal_trichotomy)
  2.1634 +apply (blast elim!: real_of_preal_not_minus_gt_zero [THEN notE])
  2.1635 +done
  2.1636 +
  2.1637 +lemma real_gt_preal_preal_Ex:
  2.1638 +     "real_of_preal z < x ==> \<exists>y. x = real_of_preal y"
  2.1639 +by (blast dest!: real_of_preal_zero_less [THEN order_less_trans]
  2.1640 +             intro: real_gt_zero_preal_Ex [THEN iffD1])
  2.1641 +
  2.1642 +lemma real_ge_preal_preal_Ex:
  2.1643 +     "real_of_preal z \<le> x ==> \<exists>y. x = real_of_preal y"
  2.1644 +by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex)
  2.1645 +
  2.1646 +lemma real_less_all_preal: "y \<le> 0 ==> \<forall>x. y < real_of_preal x"
  2.1647 +by (auto elim: order_le_imp_less_or_eq [THEN disjE] 
  2.1648 +            intro: real_of_preal_zero_less [THEN [2] order_less_trans] 
  2.1649 +            simp add: real_of_preal_zero_less)
  2.1650 +
  2.1651 +lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
  2.1652 +by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
  2.1653 +
  2.1654 +
  2.1655 +subsection{*Numerals and Arithmetic*}
  2.1656 +
  2.1657 +instantiation real :: number_ring
  2.1658 +begin
  2.1659 +
  2.1660 +definition
  2.1661 +  real_number_of_def [code del]: "(number_of w :: real) = of_int w"
  2.1662 +
  2.1663 +instance
  2.1664 +  by intro_classes (simp add: real_number_of_def)
  2.1665 +
  2.1666 +end
  2.1667 +
  2.1668 +subsection {* Completeness of Positive Reals *}
  2.1669 +
  2.1670 +text {*
  2.1671 +  Supremum property for the set of positive reals
  2.1672 +
  2.1673 +  Let @{text "P"} be a non-empty set of positive reals, with an upper
  2.1674 +  bound @{text "y"}.  Then @{text "P"} has a least upper bound
  2.1675 +  (written @{text "S"}).
  2.1676 +
  2.1677 +  FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}?
  2.1678 +*}
  2.1679 +
  2.1680 +lemma posreal_complete:
  2.1681 +  assumes positive_P: "\<forall>x \<in> P. (0::real) < x"
  2.1682 +    and not_empty_P: "\<exists>x. x \<in> P"
  2.1683 +    and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
  2.1684 +  shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
  2.1685 +proof (rule exI, rule allI)
  2.1686 +  fix y
  2.1687 +  let ?pP = "{w. real_of_preal w \<in> P}"
  2.1688 +
  2.1689 +  show "(\<exists>x\<in>P. y < x) = (y < real_of_preal (psup ?pP))"
  2.1690 +  proof (cases "0 < y")
  2.1691 +    assume neg_y: "\<not> 0 < y"
  2.1692 +    show ?thesis
  2.1693 +    proof
  2.1694 +      assume "\<exists>x\<in>P. y < x"
  2.1695 +      have "\<forall>x. y < real_of_preal x"
  2.1696 +        using neg_y by (rule real_less_all_real2)
  2.1697 +      thus "y < real_of_preal (psup ?pP)" ..
  2.1698 +    next
  2.1699 +      assume "y < real_of_preal (psup ?pP)"
  2.1700 +      obtain "x" where x_in_P: "x \<in> P" using not_empty_P ..
  2.1701 +      hence "0 < x" using positive_P by simp
  2.1702 +      hence "y < x" using neg_y by simp
  2.1703 +      thus "\<exists>x \<in> P. y < x" using x_in_P ..
  2.1704 +    qed
  2.1705 +  next
  2.1706 +    assume pos_y: "0 < y"
  2.1707 +
  2.1708 +    then obtain py where y_is_py: "y = real_of_preal py"
  2.1709 +      by (auto simp add: real_gt_zero_preal_Ex)
  2.1710 +
  2.1711 +    obtain a where "a \<in> P" using not_empty_P ..
  2.1712 +    with positive_P have a_pos: "0 < a" ..
  2.1713 +    then obtain pa where "a = real_of_preal pa"
  2.1714 +      by (auto simp add: real_gt_zero_preal_Ex)
  2.1715 +    hence "pa \<in> ?pP" using `a \<in> P` by auto
  2.1716 +    hence pP_not_empty: "?pP \<noteq> {}" by auto
  2.1717 +
  2.1718 +    obtain sup where sup: "\<forall>x \<in> P. x < sup"
  2.1719 +      using upper_bound_Ex ..
  2.1720 +    from this and `a \<in> P` have "a < sup" ..
  2.1721 +    hence "0 < sup" using a_pos by arith
  2.1722 +    then obtain possup where "sup = real_of_preal possup"
  2.1723 +      by (auto simp add: real_gt_zero_preal_Ex)
  2.1724 +    hence "\<forall>X \<in> ?pP. X \<le> possup"
  2.1725 +      using sup by (auto simp add: real_of_preal_lessI)
  2.1726 +    with pP_not_empty have psup: "\<And>Z. (\<exists>X \<in> ?pP. Z < X) = (Z < psup ?pP)"
  2.1727 +      by (rule preal_complete)
  2.1728 +
  2.1729 +    show ?thesis
  2.1730 +    proof
  2.1731 +      assume "\<exists>x \<in> P. y < x"
  2.1732 +      then obtain x where x_in_P: "x \<in> P" and y_less_x: "y < x" ..
  2.1733 +      hence "0 < x" using pos_y by arith
  2.1734 +      then obtain px where x_is_px: "x = real_of_preal px"
  2.1735 +        by (auto simp add: real_gt_zero_preal_Ex)
  2.1736 +
  2.1737 +      have py_less_X: "\<exists>X \<in> ?pP. py < X"
  2.1738 +      proof
  2.1739 +        show "py < px" using y_is_py and x_is_px and y_less_x
  2.1740 +          by (simp add: real_of_preal_lessI)
  2.1741 +        show "px \<in> ?pP" using x_in_P and x_is_px by simp
  2.1742 +      qed
  2.1743 +
  2.1744 +      have "(\<exists>X \<in> ?pP. py < X) ==> (py < psup ?pP)"
  2.1745 +        using psup by simp
  2.1746 +      hence "py < psup ?pP" using py_less_X by simp
  2.1747 +      thus "y < real_of_preal (psup {w. real_of_preal w \<in> P})"
  2.1748 +        using y_is_py and pos_y by (simp add: real_of_preal_lessI)
  2.1749 +    next
  2.1750 +      assume y_less_psup: "y < real_of_preal (psup ?pP)"
  2.1751 +
  2.1752 +      hence "py < psup ?pP" using y_is_py
  2.1753 +        by (simp add: real_of_preal_lessI)
  2.1754 +      then obtain "X" where py_less_X: "py < X" and X_in_pP: "X \<in> ?pP"
  2.1755 +        using psup by auto
  2.1756 +      then obtain x where x_is_X: "x = real_of_preal X"
  2.1757 +        by (simp add: real_gt_zero_preal_Ex)
  2.1758 +      hence "y < x" using py_less_X and y_is_py
  2.1759 +        by (simp add: real_of_preal_lessI)
  2.1760 +
  2.1761 +      moreover have "x \<in> P" using x_is_X and X_in_pP by simp
  2.1762 +
  2.1763 +      ultimately show "\<exists> x \<in> P. y < x" ..
  2.1764 +    qed
  2.1765 +  qed
  2.1766 +qed
  2.1767 +
  2.1768 +text {*
  2.1769 +  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
  2.1770 +*}
  2.1771 +
  2.1772 +lemma posreals_complete:
  2.1773 +  assumes positive_S: "\<forall>x \<in> S. 0 < x"
  2.1774 +    and not_empty_S: "\<exists>x. x \<in> S"
  2.1775 +    and upper_bound_Ex: "\<exists>u. isUb (UNIV::real set) S u"
  2.1776 +  shows "\<exists>t. isLub (UNIV::real set) S t"
  2.1777 +proof
  2.1778 +  let ?pS = "{w. real_of_preal w \<in> S}"
  2.1779 +
  2.1780 +  obtain u where "isUb UNIV S u" using upper_bound_Ex ..
  2.1781 +  hence sup: "\<forall>x \<in> S. x \<le> u" by (simp add: isUb_def setle_def)
  2.1782 +
  2.1783 +  obtain x where x_in_S: "x \<in> S" using not_empty_S ..
  2.1784 +  hence x_gt_zero: "0 < x" using positive_S by simp
  2.1785 +  have  "x \<le> u" using sup and x_in_S ..
  2.1786 +  hence "0 < u" using x_gt_zero by arith
  2.1787 +
  2.1788 +  then obtain pu where u_is_pu: "u = real_of_preal pu"
  2.1789 +    by (auto simp add: real_gt_zero_preal_Ex)
  2.1790 +
  2.1791 +  have pS_less_pu: "\<forall>pa \<in> ?pS. pa \<le> pu"
  2.1792 +  proof
  2.1793 +    fix pa
  2.1794 +    assume "pa \<in> ?pS"
  2.1795 +    then obtain a where "a \<in> S" and "a = real_of_preal pa"
  2.1796 +      by simp
  2.1797 +    moreover hence "a \<le> u" using sup by simp
  2.1798 +    ultimately show "pa \<le> pu"
  2.1799 +      using sup and u_is_pu by (simp add: real_of_preal_le_iff)
  2.1800 +  qed
  2.1801 +
  2.1802 +  have "\<forall>y \<in> S. y \<le> real_of_preal (psup ?pS)"
  2.1803 +  proof
  2.1804 +    fix y
  2.1805 +    assume y_in_S: "y \<in> S"
  2.1806 +    hence "0 < y" using positive_S by simp
  2.1807 +    then obtain py where y_is_py: "y = real_of_preal py"
  2.1808 +      by (auto simp add: real_gt_zero_preal_Ex)
  2.1809 +    hence py_in_pS: "py \<in> ?pS" using y_in_S by simp
  2.1810 +    with pS_less_pu have "py \<le> psup ?pS"
  2.1811 +      by (rule preal_psup_le)
  2.1812 +    thus "y \<le> real_of_preal (psup ?pS)"
  2.1813 +      using y_is_py by (simp add: real_of_preal_le_iff)
  2.1814 +  qed
  2.1815 +
  2.1816 +  moreover {
  2.1817 +    fix x
  2.1818 +    assume x_ub_S: "\<forall>y\<in>S. y \<le> x"
  2.1819 +    have "real_of_preal (psup ?pS) \<le> x"
  2.1820 +    proof -
  2.1821 +      obtain "s" where s_in_S: "s \<in> S" using not_empty_S ..
  2.1822 +      hence s_pos: "0 < s" using positive_S by simp
  2.1823 +
  2.1824 +      hence "\<exists> ps. s = real_of_preal ps" by (simp add: real_gt_zero_preal_Ex)
  2.1825 +      then obtain "ps" where s_is_ps: "s = real_of_preal ps" ..
  2.1826 +      hence ps_in_pS: "ps \<in> {w. real_of_preal w \<in> S}" using s_in_S by simp
  2.1827 +
  2.1828 +      from x_ub_S have "s \<le> x" using s_in_S ..
  2.1829 +      hence "0 < x" using s_pos by simp
  2.1830 +      hence "\<exists> px. x = real_of_preal px" by (simp add: real_gt_zero_preal_Ex)
  2.1831 +      then obtain "px" where x_is_px: "x = real_of_preal px" ..
  2.1832 +
  2.1833 +      have "\<forall>pe \<in> ?pS. pe \<le> px"
  2.1834 +      proof
  2.1835 +        fix pe
  2.1836 +        assume "pe \<in> ?pS"
  2.1837 +        hence "real_of_preal pe \<in> S" by simp
  2.1838 +        hence "real_of_preal pe \<le> x" using x_ub_S by simp
  2.1839 +        thus "pe \<le> px" using x_is_px by (simp add: real_of_preal_le_iff)
  2.1840 +      qed
  2.1841 +
  2.1842 +      moreover have "?pS \<noteq> {}" using ps_in_pS by auto
  2.1843 +      ultimately have "(psup ?pS) \<le> px" by (simp add: psup_le_ub)
  2.1844 +      thus "real_of_preal (psup ?pS) \<le> x" using x_is_px by (simp add: real_of_preal_le_iff)
  2.1845 +    qed
  2.1846 +  }
  2.1847 +  ultimately show "isLub UNIV S (real_of_preal (psup ?pS))"
  2.1848 +    by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
  2.1849 +qed
  2.1850 +
  2.1851 +text {*
  2.1852 +  \medskip reals Completeness (again!)
  2.1853 +*}
  2.1854 +
  2.1855 +lemma reals_complete:
  2.1856 +  assumes notempty_S: "\<exists>X. X \<in> S"
  2.1857 +    and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"
  2.1858 +  shows "\<exists>t. isLub (UNIV :: real set) S t"
  2.1859 +proof -
  2.1860 +  obtain X where X_in_S: "X \<in> S" using notempty_S ..
  2.1861 +  obtain Y where Y_isUb: "isUb (UNIV::real set) S Y"
  2.1862 +    using exists_Ub ..
  2.1863 +  let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (-X) + 1} \<inter> {x. 0 < x}"
  2.1864 +
  2.1865 +  {
  2.1866 +    fix x
  2.1867 +    assume "isUb (UNIV::real set) S x"
  2.1868 +    hence S_le_x: "\<forall> y \<in> S. y <= x"
  2.1869 +      by (simp add: isUb_def setle_def)
  2.1870 +    {
  2.1871 +      fix s
  2.1872 +      assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}"
  2.1873 +      hence "\<exists> x \<in> S. s = x + -X + 1" ..
  2.1874 +      then obtain x1 where "x1 \<in> S" and "s = x1 + (-X) + 1" ..
  2.1875 +      moreover hence "x1 \<le> x" using S_le_x by simp
  2.1876 +      ultimately have "s \<le> x + - X + 1" by arith
  2.1877 +    }
  2.1878 +    then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)"
  2.1879 +      by (auto simp add: isUb_def setle_def)
  2.1880 +  } note S_Ub_is_SHIFT_Ub = this
  2.1881 +
  2.1882 +  hence "isUb UNIV ?SHIFT (Y + (-X) + 1)" using Y_isUb by simp
  2.1883 +  hence "\<exists>Z. isUb UNIV ?SHIFT Z" ..
  2.1884 +  moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto
  2.1885 +  moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT"
  2.1886 +    using X_in_S and Y_isUb by auto
  2.1887 +  ultimately obtain t where t_is_Lub: "isLub UNIV ?SHIFT t"
  2.1888 +    using posreals_complete [of ?SHIFT] by blast
  2.1889 +
  2.1890 +  show ?thesis
  2.1891 +  proof
  2.1892 +    show "isLub UNIV S (t + X + (-1))"
  2.1893 +    proof (rule isLubI2)
  2.1894 +      {
  2.1895 +        fix x
  2.1896 +        assume "isUb (UNIV::real set) S x"
  2.1897 +        hence "isUb (UNIV::real set) (?SHIFT) (x + (-X) + 1)"
  2.1898 +          using S_Ub_is_SHIFT_Ub by simp
  2.1899 +        hence "t \<le> (x + (-X) + 1)"
  2.1900 +          using t_is_Lub by (simp add: isLub_le_isUb)
  2.1901 +        hence "t + X + -1 \<le> x" by arith
  2.1902 +      }
  2.1903 +      then show "(t + X + -1) <=* Collect (isUb UNIV S)"
  2.1904 +        by (simp add: setgeI)
  2.1905 +    next
  2.1906 +      show "isUb UNIV S (t + X + -1)"
  2.1907 +      proof -
  2.1908 +        {
  2.1909 +          fix y
  2.1910 +          assume y_in_S: "y \<in> S"
  2.1911 +          have "y \<le> t + X + -1"
  2.1912 +          proof -
  2.1913 +            obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
  2.1914 +            hence "\<exists> x \<in> S. u = x + - X + 1" by simp
  2.1915 +            then obtain "x" where x_and_u: "u = x + - X + 1" ..
  2.1916 +            have u_le_t: "u \<le> t" using u_in_shift and t_is_Lub by (simp add: isLubD2)
  2.1917 +
  2.1918 +            show ?thesis
  2.1919 +            proof cases
  2.1920 +              assume "y \<le> x"
  2.1921 +              moreover have "x = u + X + - 1" using x_and_u by arith
  2.1922 +              moreover have "u + X + - 1  \<le> t + X + -1" using u_le_t by arith
  2.1923 +              ultimately show "y  \<le> t + X + -1" by arith
  2.1924 +            next
  2.1925 +              assume "~(y \<le> x)"
  2.1926 +              hence x_less_y: "x < y" by arith
  2.1927 +
  2.1928 +              have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
  2.1929 +              hence "0 < x + (-X) + 1" by simp
  2.1930 +              hence "0 < y + (-X) + 1" using x_less_y by arith
  2.1931 +              hence "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
  2.1932 +              hence "y + (-X) + 1 \<le> t" using t_is_Lub  by (simp add: isLubD2)
  2.1933 +              thus ?thesis by simp
  2.1934 +            qed
  2.1935 +          qed
  2.1936 +        }
  2.1937 +        then show ?thesis by (simp add: isUb_def setle_def)
  2.1938 +      qed
  2.1939 +    qed
  2.1940 +  qed
  2.1941 +qed
  2.1942 +
  2.1943 +text{*A version of the same theorem without all those predicates!*}
  2.1944 +lemma reals_complete2:
  2.1945 +  fixes S :: "(real set)"
  2.1946 +  assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
  2.1947 +  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & 
  2.1948 +               (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
  2.1949 +proof -
  2.1950 +  have "\<exists>x. isLub UNIV S x" 
  2.1951 +    by (rule reals_complete)
  2.1952 +       (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def prems)
  2.1953 +  thus ?thesis
  2.1954 +    by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
  2.1955 +qed
  2.1956 +
  2.1957 +
  2.1958 +subsection {* The Archimedean Property of the Reals *}
  2.1959 +
  2.1960 +theorem reals_Archimedean:
  2.1961 +  fixes x :: real
  2.1962 +  assumes x_pos: "0 < x"
  2.1963 +  shows "\<exists>n. inverse (of_nat (Suc n)) < x"
  2.1964 +proof (rule ccontr)
  2.1965 +  assume contr: "\<not> ?thesis"
  2.1966 +  have "\<forall>n. x * of_nat (Suc n) <= 1"
  2.1967 +  proof
  2.1968 +    fix n
  2.1969 +    from contr have "x \<le> inverse (of_nat (Suc n))"
  2.1970 +      by (simp add: linorder_not_less)
  2.1971 +    hence "x \<le> (1 / (of_nat (Suc n)))"
  2.1972 +      by (simp add: inverse_eq_divide)
  2.1973 +    moreover have "(0::real) \<le> of_nat (Suc n)"
  2.1974 +      by (rule of_nat_0_le_iff)
  2.1975 +    ultimately have "x * of_nat (Suc n) \<le> (1 / of_nat (Suc n)) * of_nat (Suc n)"
  2.1976 +      by (rule mult_right_mono)
  2.1977 +    thus "x * of_nat (Suc n) \<le> 1" by (simp del: of_nat_Suc)
  2.1978 +  qed
  2.1979 +  hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= 1"
  2.1980 +    by (simp add: setle_def del: of_nat_Suc, safe, rule spec)
  2.1981 +  hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} 1"
  2.1982 +    by (simp add: isUbI)
  2.1983 +  hence "\<exists>Y. isUb (UNIV::real set) {z. \<exists>n. z = x* (of_nat (Suc n))} Y" ..
  2.1984 +  moreover have "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
  2.1985 +  ultimately have "\<exists>t. isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t"
  2.1986 +    by (simp add: reals_complete)
  2.1987 +  then obtain "t" where
  2.1988 +    t_is_Lub: "isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t" ..
  2.1989 +
  2.1990 +  have "\<forall>n::nat. x * of_nat n \<le> t + - x"
  2.1991 +  proof
  2.1992 +    fix n
  2.1993 +    from t_is_Lub have "x * of_nat (Suc n) \<le> t"
  2.1994 +      by (simp add: isLubD2)
  2.1995 +    hence  "x * (of_nat n) + x \<le> t"
  2.1996 +      by (simp add: right_distrib)
  2.1997 +    thus  "x * (of_nat n) \<le> t + - x" by arith
  2.1998 +  qed
  2.1999 +
  2.2000 +  hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
  2.2001 +  hence "{z. \<exists>n. z = x * (of_nat (Suc n))}  *<= (t + - x)"
  2.2002 +    by (auto simp add: setle_def)
  2.2003 +  hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} (t + (-x))"
  2.2004 +    by (simp add: isUbI)
  2.2005 +  hence "t \<le> t + - x"
  2.2006 +    using t_is_Lub by (simp add: isLub_le_isUb)
  2.2007 +  thus False using x_pos by arith
  2.2008 +qed
  2.2009 +
  2.2010 +text {*
  2.2011 +  There must be other proofs, e.g. @{text "Suc"} of the largest
  2.2012 +  integer in the cut representing @{text "x"}.
  2.2013 +*}
  2.2014 +
  2.2015 +lemma reals_Archimedean2: "\<exists>n. (x::real) < of_nat (n::nat)"
  2.2016 +proof cases
  2.2017 +  assume "x \<le> 0"
  2.2018 +  hence "x < of_nat (1::nat)" by simp
  2.2019 +  thus ?thesis ..
  2.2020 +next
  2.2021 +  assume "\<not> x \<le> 0"
  2.2022 +  hence x_greater_zero: "0 < x" by simp
  2.2023 +  hence "0 < inverse x" by simp
  2.2024 +  then obtain n where "inverse (of_nat (Suc n)) < inverse x"
  2.2025 +    using reals_Archimedean by blast
  2.2026 +  hence "inverse (of_nat (Suc n)) * x < inverse x * x"
  2.2027 +    using x_greater_zero by (rule mult_strict_right_mono)
  2.2028 +  hence "inverse (of_nat (Suc n)) * x < 1"
  2.2029 +    using x_greater_zero by simp
  2.2030 +  hence "of_nat (Suc n) * (inverse (of_nat (Suc n)) * x) < of_nat (Suc n) * 1"
  2.2031 +    by (rule mult_strict_left_mono) (simp del: of_nat_Suc)
  2.2032 +  hence "x < of_nat (Suc n)"
  2.2033 +    by (simp add: algebra_simps del: of_nat_Suc)
  2.2034 +  thus "\<exists>(n::nat). x < of_nat n" ..
  2.2035 +qed
  2.2036 +
  2.2037 +instance real :: archimedean_field
  2.2038 +proof
  2.2039 +  fix r :: real
  2.2040 +  obtain n :: nat where "r < of_nat n"
  2.2041 +    using reals_Archimedean2 ..
  2.2042 +  then have "r \<le> of_int (int n)"
  2.2043 +    by simp
  2.2044 +  then show "\<exists>z. r \<le> of_int z" ..
  2.2045 +qed
  2.2046 +
  2.2047 +end
     3.1 --- a/src/HOL/ex/ROOT.ML	Mon May 10 17:37:32 2010 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Mon May 10 11:30:05 2010 -0700
     3.3 @@ -65,7 +65,8 @@
     3.4    "Landau",
     3.5    "Execute_Choice",
     3.6    "Summation",
     3.7 -  "Gauge_Integration"
     3.8 +  "Gauge_Integration",
     3.9 +  "Dedekind_Real"
    3.10  ];
    3.11  
    3.12  HTML.with_charset "utf-8" (no_document use_thys)