src/HOL/Real/PReal.thy

--- a/src/HOL/Real/PReal.thy	Tue Jan 27 09:44:14 2004 +0100
+++ b/src/HOL/Real/PReal.thy	Tue Jan 27 15:39:51 2004 +0100
@@ -7,44 +7,95 @@
                   provides some of the definitions.
 *)
 
-theory PReal = PRat:
+theory PReal = RatArith:
+
+text{*Could be generalized and moved to @{text Ring_and_Field}*}
+lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"
+by (rule_tac x="b-a" in exI, simp)
 
-typedef preal = "{A::prat set. {} < A & A < UNIV &
-                               (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
-                                        (\<exists>u \<in> A. y < u)))}"
-apply (rule exI) 
-apply (rule preal_1) 
-done
+text{*As a special case, the sum of two positives is positive.  One of the
+premises could be weakened to the relation @{text "\<le>"}.*}
+lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semiring)"
+by (insert add_strict_mono [of 0 a b c], simp)
 
-
-instance preal :: ord ..
-instance preal :: plus ..
-instance preal :: times ..
+lemma interval_empty_iff:
+     "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))"
+by (blast dest: dense intro: order_less_trans)
 
 
 constdefs
-  preal_of_prat :: "prat => preal"
-   "preal_of_prat q     == Abs_preal({x::prat. x < q})"
+  cut :: "rat set => bool"
+    "cut A == {} \<subset> A &
+              A < {r. 0 < r} &
+              (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u)))"
+
 
-  pinv       :: "preal => preal"
-  "pinv(R)   == Abs_preal({w. \<exists>y. w < y & qinv y \<notin> Rep_preal(R)})"
+lemma cut_of_rat: 
+  assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}"
+proof -
+  let ?A = "{r::rat. 0 < r & r < q}"
+  from q have pos: "?A < {r. 0 < r}" by force
+  have nonempty: "{} \<subset> ?A"
+  proof
+    show "{} \<subseteq> ?A" by simp
+    show "{} \<noteq> ?A"
+      by (force simp only: q eq_commute [of "{}"] interval_empty_iff)
+  qed
+  show ?thesis
+    by (simp add: cut_def pos nonempty,
+        blast dest: dense intro: order_less_trans)
+qed
+
+
+typedef preal = "{A. cut A}"
+  by (blast intro: cut_of_rat [OF zero_less_one])
+
+instance preal :: ord ..
+instance preal :: plus ..
+instance preal :: minus ..
+instance preal :: times ..
+instance preal :: inverse ..
+
+
+constdefs
+  preal_of_rat :: "rat => preal"
+     "preal_of_rat q == Abs_preal({x::rat. 0 < x & x < q})"
 
   psup       :: "preal set => preal"
-  "psup(P)   == Abs_preal({w. \<exists>X \<in> P. w \<in> Rep_preal(X)})"
+    "psup(P)   == Abs_preal(\<Union>X \<in> P. Rep_preal(X))"
+
+  add_set :: "[rat set,rat set] => rat set"
+    "add_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
+
+  diff_set :: "[rat set,rat set] => rat set"
+    "diff_set A B == {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
+
+  mult_set :: "[rat set,rat set] => rat set"
+    "mult_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
+
+  inverse_set :: "rat set => rat set"
+    "inverse_set A == {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
+
 
 defs (overloaded)
 
+  preal_less_def:
+    "R < (S::preal) == Rep_preal R < Rep_preal S"
+
+  preal_le_def:
+    "R \<le> (S::preal) == Rep_preal R \<subseteq> Rep_preal S"
+
   preal_add_def:
-    "R + S == Abs_preal({w. \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). w = x + y})"
+    "R + S == Abs_preal (add_set (Rep_preal R) (Rep_preal S))"
+
+  preal_diff_def:
+    "R - S == Abs_preal (diff_set (Rep_preal R) (Rep_preal S))"
 
   preal_mult_def:
-    "R * S == Abs_preal({w. \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). w = x * y})"
+    "R * S == Abs_preal(mult_set (Rep_preal R) (Rep_preal S))"
 
-  preal_less_def:
-    "R < (S::preal) == Rep_preal(R) < Rep_preal(S)"
-
-  preal_le_def:
-    "R \<le> (S::preal) == Rep_preal(R) \<subseteq> Rep_preal(S)"
+  preal_inverse_def:
+    "inverse R == Abs_preal(inverse_set (Rep_preal R))"
 
 
 lemma inj_on_Abs_preal: "inj_on Abs_preal preal"
@@ -59,108 +110,61 @@
 apply (rule Rep_preal_inverse)
 done
 
-lemma empty_not_mem_preal [simp]: "{} \<notin> preal"
-by (unfold preal_def, fast)
+lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
+by (unfold preal_def cut_def, blast)
 
-lemma one_set_mem_preal: "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} \<in> preal"
-apply (unfold preal_def)
-apply (rule preal_1)
-done
+lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
+by (force simp add: preal_def cut_def)
 
-declare one_set_mem_preal [simp]
+lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
+by (drule preal_imp_psubset_positives, auto)
 
-lemma preal_psubset_empty: "x \<in> preal ==> {} < x"
-by (unfold preal_def, fast)
-
-lemma Rep_preal_psubset_empty: "{} < Rep_preal x"
-by (rule Rep_preal [THEN preal_psubset_empty])
+lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
+by (unfold preal_def cut_def, blast)
 
 lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X"
-apply (cut_tac x = X in Rep_preal_psubset_empty)
-apply (auto intro: equals0I [symmetric] simp add: psubset_def)
-done
-
-lemma prealI1:
-      "[| {} < A; A < UNIV;
-               (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
-                         (\<exists>u \<in> A. y < u))) |] ==> A \<in> preal"
-apply (unfold preal_def, fast)
+apply (insert Rep_preal [of X])
+apply (unfold preal_def cut_def, blast)
 done
 
-lemma prealI2:
-      "[| {} < A; A < UNIV;
-               \<forall>y \<in> A. (\<forall>z. z < y --> z \<in> A);
-               \<forall>y \<in> A. (\<exists>u \<in> A. y < u) |] ==> A \<in> preal"
-
-apply (unfold preal_def, best)
-done
-
-lemma prealE_lemma:
-      "A \<in> preal ==> {} < A & A < UNIV &
-                          (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
-                                   (\<exists>u \<in> A. y < u)))"
-apply (unfold preal_def, fast)
-done
-
-declare prealI1 [intro!] prealI2 [intro!]
-
 declare Abs_preal_inverse [simp]
 
-
-lemma prealE_lemma1: "A \<in> preal ==> {} < A"
-by (unfold preal_def, fast)
-
-lemma prealE_lemma2: "A \<in> preal ==> A < UNIV"
-by (unfold preal_def, fast)
-
-lemma prealE_lemma3: "A \<in> preal ==> \<forall>y \<in> A. (\<forall>z. z < y --> z \<in> A)"
-by (unfold preal_def, fast)
-
-lemma prealE_lemma3a: "[| A \<in> preal; y \<in> A |] ==> (\<forall>z. z < y --> z \<in> A)"
-by (fast dest!: prealE_lemma3)
+lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
+by (unfold preal_def cut_def, blast)
 
-lemma prealE_lemma3b: "[| A \<in> preal; y \<in> A; z < y |] ==> z \<in> A"
-by (fast dest!: prealE_lemma3a)
-
-lemma prealE_lemma4: "A \<in> preal ==> \<forall>y \<in> A. (\<exists>u \<in> A. y < u)"
-by (unfold preal_def, fast)
+text{*Relaxing the final premise*}
+lemma preal_downwards_closed':
+     "[| A \<in> preal; y \<in> A; 0 < z; z \<le> y |] ==> z \<in> A"
+apply (simp add: order_le_less)
+apply (blast intro: preal_downwards_closed)
+done
 
-lemma prealE_lemma4a: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
-by (fast dest!: prealE_lemma4)
-
-lemma not_mem_Rep_preal_Ex: "\<exists>x. x\<notin> Rep_preal X"
+lemma Rep_preal_exists_bound: "\<exists>x. 0 < x & x \<notin> Rep_preal X"
 apply (cut_tac x = X in Rep_preal)
-apply (drule prealE_lemma2)
+apply (drule preal_imp_psubset_positives)
 apply (auto simp add: psubset_def)
 done
 
 
 subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
 
-text{*A few lemmas*}
-
-lemma lemma_prat_less_set_mem_preal: "{u::prat. u < y} \<in> preal"
-apply (cut_tac qless_Ex)
-apply (auto intro: prat_less_trans elim!: prat_less_irrefl)
-apply (blast dest: prat_dense)
+lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal"
+apply (auto simp add: preal_def cut_def intro: order_less_trans)
+apply (force simp only: eq_commute [of "{}"] interval_empty_iff)
+apply (blast dest: dense intro: order_less_trans)
 done
 
-lemma lemma_prat_set_eq: "{u::prat. u < x} = {x. x < y} ==> x = y"
-apply (insert prat_linear [of x y], safe)
-apply (drule_tac [2] prat_dense, erule_tac [2] exE)
-apply (drule prat_dense, erule exE)
-apply (blast dest: prat_less_not_sym)
-apply (blast dest: prat_less_not_sym)
+lemma rat_subset_imp_le:
+     "[|{u::rat. 0 < u & u < x} \<subseteq> {u. 0 < u & u < y}; 0<x|] ==> x \<le> y"
+apply (simp add: linorder_not_less [symmetric])
+apply (blast dest: dense intro: order_less_trans)
 done
 
-lemma inj_preal_of_prat: "inj(preal_of_prat)"
-apply (rule inj_onI)
-apply (unfold preal_of_prat_def)
-apply (drule inj_on_Abs_preal [THEN inj_onD])
-apply (rule lemma_prat_less_set_mem_preal)
-apply (rule lemma_prat_less_set_mem_preal)
-apply (erule lemma_prat_set_eq)
-done
+lemma rat_set_eq_imp_eq:
+     "[|{u::rat. 0 < u & u < x} = {u. 0 < u & u < y};
+        0 < x; 0 < y|] ==> x = y"
+by (blast intro: rat_subset_imp_le order_antisym)
+
 
 
 subsection{*Theorems for Ordering*}
@@ -168,127 +172,173 @@
 text{*A positive fraction not in a positive real is an upper bound.
  Gleason p. 122 - Remark (1)*}
 
-lemma not_in_preal_ub: "x \<notin> Rep_preal(R) ==> \<forall>y \<in> Rep_preal(R). y < x"
-apply (cut_tac x1 = R in Rep_preal [THEN prealE_lemma]) 
-apply (blast intro: not_less_not_eq_prat_less)
-done
+lemma not_in_preal_ub:
+     assumes A: "A \<in> preal"
+         and notx: "x \<notin> A"
+         and y: "y \<in> A"
+         and pos: "0 < x"
+        shows "y < x"
+proof (cases rule: linorder_cases)
+  assume "x<y"
+  with notx show ?thesis
+    by (simp add:  preal_downwards_closed [OF A y] pos)
+next
+  assume "x=y"
+  with notx and y show ?thesis by simp
+next
+  assume "y<x"
+  thus ?thesis by assumption
+qed
+
+lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal]
 
 
-text{*@{text preal_less} is a strict order: nonreflexive and transitive *}
+subsection{*The @{text "\<le>"} Ordering*}
+
+lemma preal_le_refl: "w \<le> (w::preal)"
+by (simp add: preal_le_def)
 
-lemma preal_less_not_refl: "~ (x::preal) < x"
-apply (unfold preal_less_def)
-apply (simp (no_asm) add: psubset_def)
+lemma preal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::preal)"
+by (force simp add: preal_le_def)
+
+lemma preal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::preal)"
+apply (simp add: preal_le_def)
+apply (rule Rep_preal_inject [THEN iffD1], blast)
 done
 
-lemmas preal_less_irrefl = preal_less_not_refl [THEN notE, standard]
+(* Axiom 'order_less_le' of class 'order': *)
+lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
+by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def)
+
+instance preal :: order
+proof qed
+ (assumption |
+  rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
 
-lemma preal_not_refl2: "!!(x::preal). x < y ==> x \<noteq> y"
-by (auto simp add: preal_less_not_refl)
+lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
+by (insert preal_imp_psubset_positives, blast)
 
-lemma preal_less_trans: "!!(x::preal). [| x < y; y < z |] ==> x < z"
-apply (unfold preal_less_def)
-apply (auto dest: subsetD equalityI simp add: psubset_def)
+lemma preal_le_linear: "x <= y | y <= (x::preal)"
+apply (auto simp add: preal_le_def)
+apply (rule ccontr)
+apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
+             elim: order_less_asym)
 done
 
-lemma preal_less_not_sym: "!! (q1::preal). q1 < q2 ==> ~ q2 < q1"
-apply (rule notI)
-apply (drule preal_less_trans, assumption)
-apply (simp add: preal_less_not_refl)
-done
+instance preal :: linorder
+  by (intro_classes, rule preal_le_linear)
 
-(* [| x < y;  ~P ==> y < x |] ==> P *)
-lemmas preal_less_asym = preal_less_not_sym [THEN contrapos_np, standard]
-
-lemma preal_linear:
-      "(x::preal) < y | x = y | y < x"
-apply (unfold preal_less_def)
-apply (auto dest!: inj_Rep_preal [THEN injD] simp add: psubset_def)
-apply (rule prealE_lemma3b, rule Rep_preal, assumption)
-apply (fast dest: not_in_preal_ub)
-done
 
 
 subsection{*Properties of Addition*}
 
 lemma preal_add_commute: "(x::preal) + y = y + x"
-apply (unfold preal_add_def)
+apply (unfold preal_add_def add_set_def)
 apply (rule_tac f = Abs_preal in arg_cong)
-apply (blast intro: prat_add_commute [THEN subst])
-done
-
-text{*Addition of two positive reals gives a positive real*}
-
-text{*Lemmas for proving positive reals addition set in @{typ preal}*}
-
-text{*Part 1 of Dedekind sections definition*}
-lemma preal_add_set_not_empty:
-     "{} < {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}"
-apply (cut_tac mem_Rep_preal_Ex mem_Rep_preal_Ex)
-apply (auto intro!: psubsetI)
+apply (force simp add: add_commute)
 done
 
-text{*Part 2 of Dedekind sections definition*}
-lemma preal_not_mem_add_set_Ex:
-     "\<exists>q. q  \<notin> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}"
-apply (cut_tac X = R in not_mem_Rep_preal_Ex)
-apply (cut_tac X = S in not_mem_Rep_preal_Ex, clarify) 
-apply (drule not_in_preal_ub)+
-apply (rule_tac x = "x+xa" in exI)
-apply (auto dest!: bspec) 
-apply (drule prat_add_less_mono)
-apply (auto simp add: prat_less_not_refl)
+text{*Lemmas for proving that addition of two positive reals gives
+ a positive real*}
+
+lemma empty_psubset_nonempty: "a \<in> A ==> {} \<subset> A"
+by blast
+
+text{*Part 1 of Dedekind sections definition*}
+lemma add_set_not_empty:
+     "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> add_set A B"
+apply (insert preal_nonempty [of A] preal_nonempty [of B]) 
+apply (auto simp add: add_set_def)
 done
 
-lemma preal_add_set_not_prat_set:
-     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y} < UNIV"
-apply (auto intro!: psubsetI)
-apply (cut_tac R = R and S = S in preal_not_mem_add_set_Ex, auto)
+text{*Part 2 of Dedekind sections definition.  A structured version of
+this proof is @{text preal_not_mem_mult_set_Ex} below.*}
+lemma preal_not_mem_add_set_Ex:
+     "[|A \<in> preal; B \<in> preal|] ==> \<exists>q. 0 < q & q \<notin> add_set A B"
+apply (insert preal_exists_bound [of A] preal_exists_bound [of B], auto) 
+apply (rule_tac x = "x+xa" in exI)
+apply (simp add: add_set_def, clarify)
+apply (drule not_in_preal_ub, assumption+)+
+apply (force dest: add_strict_mono)
 done
 
+lemma add_set_not_rat_set:
+   assumes A: "A \<in> preal" 
+       and B: "B \<in> preal"
+     shows "add_set A B < {r. 0 < r}"
+proof
+  from preal_imp_pos [OF A] preal_imp_pos [OF B]
+  show "add_set A B \<subseteq> {r. 0 < r}" by (force simp add: add_set_def) 
+next
+  show "add_set A B \<noteq> {r. 0 < r}"
+    by (insert preal_not_mem_add_set_Ex [OF A B], blast) 
+qed
+
 text{*Part 3 of Dedekind sections definition*}
-lemma preal_add_set_lemma3:
-     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}.
-         \<forall>z. z < y --> z \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x+y}"
-apply auto
-apply (frule prat_mult_qinv_less_1)
-apply (frule_tac x = x 
-       in prat_mult_less2_mono1 [of _ "prat_of_pnat (Abs_pnat (Suc 0))"])
-apply (frule_tac x = ya 
-       in prat_mult_less2_mono1 [of _ "prat_of_pnat (Abs_pnat (Suc 0))"])
-apply simp
-apply (drule Rep_preal [THEN prealE_lemma3a])+
-apply (erule allE)+
-apply auto
-apply (rule bexI)+
-apply (auto simp add: prat_add_mult_distrib2 [symmetric] 
-      prat_add_assoc [symmetric] prat_mult_assoc)
+lemma add_set_lemma3:
+     "[|A \<in> preal; B \<in> preal; u \<in> add_set A B; 0 < z; z < u|] 
+      ==> z \<in> add_set A B"
+proof (unfold add_set_def, clarify)
+  fix x::rat and y::rat
+  assume A: "A \<in> preal" 
+     and B: "B \<in> preal"
+     and [simp]: "0 < z"
+     and zless: "z < x + y"
+     and x:  "x \<in> A"
+     and y:  "y \<in> B"
+  have xpos [simp]: "0<x" by (rule preal_imp_pos [OF A x])
+  have ypos [simp]: "0<y" by (rule preal_imp_pos [OF B y])
+  have xypos [simp]: "0 < x+y" by (simp add: pos_add_strict)
+  let ?f = "z/(x+y)"
+  have fless: "?f < 1" by (simp add: zless pos_divide_less_eq)
+  show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
+  proof
+    show "\<exists>y' \<in> B. z = x*?f + y'"
+    proof
+      show "z = x*?f + y*?f"
+	by (simp add: left_distrib [symmetric] divide_inverse_zero mult_ac
+		      order_less_imp_not_eq2)
+    next
+      show "y * ?f \<in> B"
+      proof (rule preal_downwards_closed [OF B y])
+        show "0 < y * ?f"
+          by (simp add: divide_inverse_zero zero_less_mult_iff)
+      next
+        show "y * ?f < y"
+          by (insert mult_strict_left_mono [OF fless ypos], simp)
+      qed
+    qed
+  next
+    show "x * ?f \<in> A"
+    proof (rule preal_downwards_closed [OF A x])
+      show "0 < x * ?f"
+	by (simp add: divide_inverse_zero zero_less_mult_iff)
+    next
+      show "x * ?f < x"
+	by (insert mult_strict_left_mono [OF fless xpos], simp)
+    qed
+  qed
+qed
+
+text{*Part 4 of Dedekind sections definition*}
+lemma add_set_lemma4:
+     "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
+apply (auto simp add: add_set_def)
+apply (frule preal_exists_greater [of A], auto) 
+apply (rule_tac x="u + y" in exI)
+apply (auto intro: add_strict_left_mono)
 done
 
-lemma preal_add_set_lemma4:
-     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}.
-          \<exists>u \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}. y < u"
-apply auto
-apply (drule Rep_preal [THEN prealE_lemma4a])
-apply (auto intro: prat_add_less2_mono1)
-done
-
-lemma preal_mem_add_set:
-     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y} \<in> preal"
-apply (rule prealI2)
-apply (rule preal_add_set_not_empty)
-apply (rule preal_add_set_not_prat_set)
-apply (rule preal_add_set_lemma3)
-apply (rule preal_add_set_lemma4)
+lemma mem_add_set:
+     "[|A \<in> preal; B \<in> preal|] ==> add_set A B \<in> preal"
+apply (simp (no_asm_simp) add: preal_def cut_def)
+apply (blast intro!: add_set_not_empty add_set_not_rat_set
+                     add_set_lemma3 add_set_lemma4)
 done
 
 lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
-apply (unfold preal_add_def)
-apply (rule_tac f = Abs_preal in arg_cong)
-apply (simp (no_asm) add: preal_mem_add_set [THEN Abs_preal_inverse])
-apply (auto simp add: prat_add_ac)
-apply (rule bexI)
-apply (auto intro!: exI simp add: prat_add_ac)
+apply (simp add: preal_add_def mem_add_set Rep_preal)
+apply (force simp add: add_set_def add_ac)
 done
 
 lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
@@ -297,7 +347,7 @@
   apply (rule preal_add_commute)
   done
 
-(* Positive Reals addition is an AC operator *)
+text{* Positive Real addition is an AC operator *}
 lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
 
 
@@ -306,9 +356,9 @@
 text{*Proofs essentially same as for addition*}
 
 lemma preal_mult_commute: "(x::preal) * y = y * x"
-apply (unfold preal_mult_def)
+apply (unfold preal_mult_def mult_set_def)
 apply (rule_tac f = Abs_preal in arg_cong)
-apply (blast intro: prat_mult_commute [THEN subst])
+apply (force simp add: mult_commute)
 done
 
 text{*Multiplication of two positive reals gives a positive real.}
@@ -316,68 +366,109 @@
 text{*Lemmas for proving positive reals multiplication set in @{typ preal}*}
 
 text{*Part 1 of Dedekind sections definition*}
-lemma preal_mult_set_not_empty:
-     "{} < {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}"
-apply (cut_tac mem_Rep_preal_Ex mem_Rep_preal_Ex)
-apply (auto intro!: psubsetI)
+lemma mult_set_not_empty:
+     "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> mult_set A B"
+apply (insert preal_nonempty [of A] preal_nonempty [of B]) 
+apply (auto simp add: mult_set_def)
 done
 
 text{*Part 2 of Dedekind sections definition*}
 lemma preal_not_mem_mult_set_Ex:
-     "\<exists>q. q  \<notin> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}"
-apply (cut_tac X = R in not_mem_Rep_preal_Ex)
-apply (cut_tac X = S in not_mem_Rep_preal_Ex)
-apply (erule exE)+
-apply (drule not_in_preal_ub)+
-apply (rule_tac x = "x*xa" in exI)
-apply (auto, (erule ballE)+, auto)
-apply (drule prat_mult_less_mono)
-apply (auto simp add: prat_less_not_refl)
-done
+   assumes A: "A \<in> preal" 
+       and B: "B \<in> preal"
+     shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
+proof -
+  from preal_exists_bound [OF A]
+  obtain x where [simp]: "0 < x" "x \<notin> A" by blast
+  from preal_exists_bound [OF B]
+  obtain y where [simp]: "0 < y" "y \<notin> B" by blast
+  show ?thesis
+  proof (intro exI conjI)
+    show "0 < x*y" by (simp add: mult_pos)
+    show "x * y \<notin> mult_set A B"
+    proof (auto simp add: mult_set_def)
+      fix u::rat and v::rat
+      assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
+      moreover
+      with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
+      moreover
+      with prems have "0\<le>v"
+        by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
+      moreover
+      hence "u*v < x*y" by (blast intro: mult_strict_mono prems)
+      ultimately show False by force
+    qed
+  qed
+qed
 
-lemma preal_mult_set_not_prat_set:
-     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y} < UNIV"
-apply (auto intro!: psubsetI)
-apply (cut_tac R = R and S = S in preal_not_mem_mult_set_Ex, auto)
-done
+lemma mult_set_not_rat_set:
+   assumes A: "A \<in> preal" 
+       and B: "B \<in> preal"
+     shows "mult_set A B < {r. 0 < r}"
+proof
+  show "mult_set A B \<subseteq> {r. 0 < r}"
+    by (force simp add: mult_set_def
+              intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos)
+next
+  show "mult_set A B \<noteq> {r. 0 < r}"
+    by (insert preal_not_mem_mult_set_Ex [OF A B], blast)
+qed
+
+
 
 text{*Part 3 of Dedekind sections definition*}
-lemma preal_mult_set_lemma3:
-     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}.
-         \<forall>z. z < y --> z \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x*y}"
-apply auto
-apply (frule_tac x = "qinv (ya)" in prat_mult_left_less2_mono1)
-apply (simp add: prat_mult_ac)
-apply (drule Rep_preal [THEN prealE_lemma3a])
-apply (erule allE)
-apply (rule bexI)+
-apply (auto simp add: prat_mult_assoc)
+lemma mult_set_lemma3:
+     "[|A \<in> preal; B \<in> preal; u \<in> mult_set A B; 0 < z; z < u|] 
+      ==> z \<in> mult_set A B"
+proof (unfold mult_set_def, clarify)
+  fix x::rat and y::rat
+  assume A: "A \<in> preal" 
+     and B: "B \<in> preal"
+     and [simp]: "0 < z"
+     and zless: "z < x * y"
+     and x:  "x \<in> A"
+     and y:  "y \<in> B"
+  have [simp]: "0<y" by (rule preal_imp_pos [OF B y])
+  show "\<exists>x' \<in> A. \<exists>y' \<in> B. z = x' * y'"
+  proof
+    show "\<exists>y'\<in>B. z = (z/y) * y'"
+    proof
+      show "z = (z/y)*y"
+	by (simp add: divide_inverse_zero mult_commute [of y] mult_assoc
+		      order_less_imp_not_eq2)
+      show "y \<in> B" .
+    qed
+  next
+    show "z/y \<in> A"
+    proof (rule preal_downwards_closed [OF A x])
+      show "0 < z/y"
+	by (simp add: zero_less_divide_iff)
+      show "z/y < x" by (simp add: pos_divide_less_eq zless)
+    qed
+  qed
+qed
+
+text{*Part 4 of Dedekind sections definition*}
+lemma mult_set_lemma4:
+     "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
+apply (auto simp add: mult_set_def)
+apply (frule preal_exists_greater [of A], auto) 
+apply (rule_tac x="u * y" in exI)
+apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B] 
+                   mult_strict_right_mono)
 done
 
-lemma preal_mult_set_lemma4:
-     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}.
-          \<exists>u \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}. y < u"
-apply auto
-apply (drule Rep_preal [THEN prealE_lemma4a])
-apply (auto intro: prat_mult_less2_mono1)
-done
 
-lemma preal_mem_mult_set:
-     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y} \<in> preal"
-apply (rule prealI2)
-apply (rule preal_mult_set_not_empty)
-apply (rule preal_mult_set_not_prat_set)
-apply (rule preal_mult_set_lemma3)
-apply (rule preal_mult_set_lemma4)
+lemma mem_mult_set:
+     "[|A \<in> preal; B \<in> preal|] ==> mult_set A B \<in> preal"
+apply (simp (no_asm_simp) add: preal_def cut_def)
+apply (blast intro!: mult_set_not_empty mult_set_not_rat_set
+                     mult_set_lemma3 mult_set_lemma4)
 done
 
 lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
-apply (unfold preal_mult_def)
-apply (rule_tac f = Abs_preal in arg_cong)
-apply (simp (no_asm) add: preal_mem_mult_set [THEN Abs_preal_inverse])
-apply (auto simp add: prat_mult_ac)
-apply (rule bexI)
-apply (auto intro!: exI simp add: prat_mult_ac)
+apply (simp add: preal_mult_def mem_mult_set Rep_preal)
+apply (force simp add: mult_set_def mult_ac)
 done
 
 lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
@@ -386,32 +477,64 @@
   apply (rule preal_mult_commute)
   done
 
-(* Positive Reals multiplication is an AC operator *)
+
+text{* Positive Real multiplication is an AC operator *}
 lemmas preal_mult_ac =
        preal_mult_assoc preal_mult_commute preal_mult_left_commute
 
-(* Positive Real 1 is the multiplicative identity element *)
-(* long *)
-lemma preal_mult_1:
-      "(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) * z = z"
-apply (unfold preal_of_prat_def preal_mult_def)
-apply (rule Rep_preal_inverse [THEN subst])
-apply (rule_tac f = Abs_preal in arg_cong)
-apply (rule one_set_mem_preal [THEN Abs_preal_inverse, THEN ssubst])
-apply (auto simp add: Rep_preal_inverse)
-apply (drule Rep_preal [THEN prealE_lemma4a]) 
-apply (erule bexE) 
-apply (drule prat_mult_less_mono)
-apply (auto dest: Rep_preal [THEN prealE_lemma3a])
-apply (frule Rep_preal [THEN prealE_lemma4a]) 
-apply (erule bexE) 
-apply (frule_tac x = "qinv (u)" in prat_mult_less2_mono1)
-apply (rule exI, auto, rule_tac x = u in bexI)
-apply (auto simp add: prat_mult_assoc)
-done
+
+text{* Positive real 1 is the multiplicative identity element *}
+
+lemma rat_mem_preal: "0 < q ==> {r::rat. 0 < r & r < q} \<in> preal"
+by (simp add: preal_def cut_of_rat)
 
-lemma preal_mult_1_right:
-     "z * (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) = z"
+lemma preal_mult_1: "(preal_of_rat 1) * z = z"
+proof (induct z)
+  fix A :: "rat set"
+  assume A: "A \<in> preal"
+  have "{w. \<exists>u. 0 < u \<and> u < 1 & (\<exists>v \<in> A. w = u * v)} = A" (is "?lhs = A")
+  proof
+    show "?lhs \<subseteq> A"
+    proof clarify
+      fix x::rat and u::rat and v::rat
+      assume upos: "0<u" and "u<1" and v: "v \<in> A"
+      have vpos: "0<v" by (rule preal_imp_pos [OF A v])
+      hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
+      thus "u * v \<in> A"
+        by (force intro: preal_downwards_closed [OF A v] mult_pos upos vpos)
+    qed
+  next
+    show "A \<subseteq> ?lhs"
+    proof clarify
+      fix x::rat
+      assume x: "x \<in> A"
+      have xpos: "0<x" by (rule preal_imp_pos [OF A x])
+      from preal_exists_greater [OF A x]
+      obtain v where v: "v \<in> A" and xlessv: "x < v" ..
+      have vpos: "0<v" by (rule preal_imp_pos [OF A v])
+      show "\<exists>u. 0 < u \<and> u < 1 \<and> (\<exists>v\<in>A. x = u * v)"
+      proof (intro exI conjI)
+        show "0 < x/v"
+          by (simp add: zero_less_divide_iff xpos vpos)
+	show "x / v < 1"
+          by (simp add: pos_divide_less_eq vpos xlessv)
+        show "\<exists>v'\<in>A. x = (x / v) * v'"
+        proof
+          show "x = (x/v)*v"
+	    by (simp add: divide_inverse_zero mult_assoc vpos
+                          order_less_imp_not_eq2)
+          show "v \<in> A" .
+        qed
+      qed
+    qed
+  qed
+  thus "preal_of_rat 1 * Abs_preal A = Abs_preal A"
+    by (simp add: preal_of_rat_def preal_mult_def mult_set_def 
+                  rat_mem_preal A)
+qed
+
+
+lemma preal_mult_1_right: "z * (preal_of_rat 1) = z"
 apply (rule preal_mult_commute [THEN subst])
 apply (rule preal_mult_1)
 done
@@ -419,884 +542,821 @@
 
 subsection{*Distribution of Multiplication across Addition*}
 
-lemma mem_Rep_preal_addD:
-      "z \<in> Rep_preal(R+S) ==>
-            \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x + y"
-apply (unfold preal_add_def)
-apply (drule preal_mem_add_set [THEN Abs_preal_inverse, THEN subst], fast)
-done
-
-lemma mem_Rep_preal_addI:
-      "\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x + y
-       ==> z \<in> Rep_preal(R+S)"
-apply (unfold preal_add_def)
-apply (rule preal_mem_add_set [THEN Abs_preal_inverse, THEN ssubst], fast)
-done
-
 lemma mem_Rep_preal_add_iff:
-     "(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal(R).
-                                  \<exists>y \<in> Rep_preal(S). z = x + y)"
-apply (fast intro!: mem_Rep_preal_addD mem_Rep_preal_addI)
-done
-
-lemma mem_Rep_preal_multD:
-      "z \<in> Rep_preal(R*S) ==>
-            \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y"
-apply (unfold preal_mult_def)
-apply (drule preal_mem_mult_set [THEN Abs_preal_inverse, THEN subst], fast)
-done
-
-lemma mem_Rep_preal_multI:
-      "\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y
-       ==> z \<in> Rep_preal(R*S)"
-apply (unfold preal_mult_def)
-apply (rule preal_mem_mult_set [THEN Abs_preal_inverse, THEN ssubst], fast)
+      "(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x + y)"
+apply (simp add: preal_add_def mem_add_set Rep_preal)
+apply (simp add: add_set_def) 
 done
 
 lemma mem_Rep_preal_mult_iff:
-     "(z \<in> Rep_preal(R*S)) =
-      (\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y)"
-by (fast intro!: mem_Rep_preal_multD mem_Rep_preal_multI)
-
-lemma lemma_add_mult_mem_Rep_preal:
-     "[| xb \<in> Rep_preal z1; xc \<in> Rep_preal z2; ya:
-                   Rep_preal w; yb \<in> Rep_preal w |] ==>
-                   xb * ya + xc * yb \<in> Rep_preal (z1 * w + z2 * w)"
-by (fast intro: mem_Rep_preal_addI mem_Rep_preal_multI)
+      "(z \<in> Rep_preal(R*S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x * y)"
+apply (simp add: preal_mult_def mem_mult_set Rep_preal)
+apply (simp add: mult_set_def) 
+done
 
-lemma lemma_add_mult_mem_Rep_preal1:
-     "[| xb \<in> Rep_preal z1; xc \<in> Rep_preal z2; ya:
-                   Rep_preal w; yb \<in> Rep_preal w |] ==>
-                   yb*(xb + xc) \<in> Rep_preal (w*(z1 + z2))"
-by (fast intro: mem_Rep_preal_addI mem_Rep_preal_multI)
-
-lemma lemma_preal_add_mult_distrib:
-     "x \<in> Rep_preal (w * z1 + w * z2) ==>
-               x \<in> Rep_preal (w * (z1 + z2))"
-apply (auto dest!: mem_Rep_preal_addD mem_Rep_preal_multD)
-apply (frule_tac ya = xa and yb = xb and xb = ya and xc = yb in lemma_add_mult_mem_Rep_preal1, auto)
-apply (rule_tac x = xa and y = xb in prat_linear_less2)
-apply (drule_tac b = ya and c = yb in lemma_prat_add_mult_mono)
-apply (rule Rep_preal [THEN prealE_lemma3b])
-apply (auto simp add: prat_add_mult_distrib2)
-apply (drule_tac ya = xb and yb = xa and xc = ya and xb = yb in lemma_add_mult_mem_Rep_preal1, auto)
-apply (drule_tac b = yb and c = ya in lemma_prat_add_mult_mono)
-apply (rule Rep_preal [THEN prealE_lemma3b])
-apply (erule_tac V = "xb * ya + xb * yb \<in> Rep_preal (w * (z1 + z2))" in thin_rl)
-apply (auto simp add: prat_add_mult_distrib prat_add_commute preal_add_ac)
+lemma distrib_subset1:
+     "Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)"
+apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
+apply (force simp add: right_distrib)
 done
 
-lemma lemma_preal_add_mult_distrib2:
-     "x \<in> Rep_preal (w * (z1 + z2)) ==>
-               x \<in> Rep_preal (w * z1 + w * z2)"
-by (auto dest!: mem_Rep_preal_addD mem_Rep_preal_multD
-         intro!: bexI mem_Rep_preal_addI mem_Rep_preal_multI 
-         simp add: prat_add_mult_distrib2)
+lemma linorder_le_cases [case_names le ge]:
+    "((x::'a::linorder) <= y ==> P) ==> (y <= x ==> P) ==> P"
+  apply (insert linorder_linear, blast)
+  done
 
-lemma preal_add_mult_distrib2: "(w * ((z1::preal) + z2)) = (w * z1) + (w * z2)"
-apply (rule inj_Rep_preal [THEN injD])
-apply (fast intro: lemma_preal_add_mult_distrib lemma_preal_add_mult_distrib2)
+lemma preal_add_mult_distrib_mean:
+  assumes a: "a \<in> Rep_preal w"
+      and b: "b \<in> Rep_preal w"
+      and d: "d \<in> Rep_preal x"
+      and e: "e \<in> Rep_preal y"
+     shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
+proof
+  let ?c = "(a*d + b*e)/(d+e)"
+  have [simp]: "0<a" "0<b" "0<d" "0<e" "0<d+e"
+    by (blast intro: preal_imp_pos [OF Rep_preal] a b d e pos_add_strict)+
+  have cpos: "0 < ?c"
+    by (simp add: zero_less_divide_iff zero_less_mult_iff pos_add_strict)
+  show "a * d + b * e = ?c * (d + e)"
+    by (simp add: divide_inverse_zero mult_assoc order_less_imp_not_eq2)
+  show "?c \<in> Rep_preal w"
+    proof (cases rule: linorder_le_cases)
+      assume "a \<le> b"
+      hence "?c \<le> b"
+	by (simp add: pos_divide_le_eq right_distrib mult_right_mono
+                      order_less_imp_le)
+      thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos])
+    next
+      assume "b \<le> a"
+      hence "?c \<le> a"
+	by (simp add: pos_divide_le_eq right_distrib mult_right_mono
+                      order_less_imp_le)
+      thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos])
+    qed
+  qed
+
+lemma distrib_subset2:
+     "Rep_preal (w * x + w * y) \<subseteq> Rep_preal (w * (x + y))"
+apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
+apply (drule_tac w=w and x=x and y=y in preal_add_mult_distrib_mean, auto)
 done
 
-lemma preal_add_mult_distrib: "(((z1::preal) + z2) * w) = (z1 * w) + (z2 * w)"
-apply (simp (no_asm) add: preal_mult_commute preal_add_mult_distrib2)
+lemma preal_add_mult_distrib2: "(w * ((x::preal) + y)) = (w * x) + (w * y)"
+apply (rule inj_Rep_preal [THEN injD])
+apply (rule equalityI [OF distrib_subset1 distrib_subset2])
 done
 
+lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)"
+by (simp add: preal_mult_commute preal_add_mult_distrib2)
+
 
 subsection{*Existence of Inverse, a Positive Real*}
 
-lemma qinv_not_mem_Rep_preal_Ex: "\<exists>y. qinv(y) \<notin>  Rep_preal X"
-apply (cut_tac X = X in not_mem_Rep_preal_Ex)
-apply (erule exE, cut_tac x = x in prat_as_inverse_ex, auto)
-done
-
-lemma lemma_preal_mem_inv_set_ex:
-     "\<exists>q. q \<in> {x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A}"
-apply (cut_tac X = A in qinv_not_mem_Rep_preal_Ex, auto)
-apply (cut_tac y = y in qless_Ex, fast)
-done
+lemma mem_inv_set_ex:
+  assumes A: "A \<in> preal" shows "\<exists>x y. 0 < x & x < y & inverse y \<notin> A"
+proof -
+  from preal_exists_bound [OF A]
+  obtain x where [simp]: "0<x" "x \<notin> A" by blast
+  show ?thesis
+  proof (intro exI conjI)
+    show "0 < inverse (x+1)"
+      by (simp add: order_less_trans [OF _ less_add_one]) 
+    show "inverse(x+1) < inverse x"
+      by (simp add: less_imp_inverse_less less_add_one)
+    show "inverse (inverse x) \<notin> A"
+      by (simp add: order_less_imp_not_eq2)
+  qed
+qed
 
 text{*Part 1 of Dedekind sections definition*}
-lemma preal_inv_set_not_empty: "{} < {x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A}"
-apply (cut_tac lemma_preal_mem_inv_set_ex)
-apply (auto intro!: psubsetI)
+lemma inverse_set_not_empty:
+     "A \<in> preal ==> {} \<subset> inverse_set A"
+apply (insert mem_inv_set_ex [of A])
+apply (auto simp add: inverse_set_def)
 done
 
 text{*Part 2 of Dedekind sections definition*}
-lemma qinv_mem_Rep_preal_Ex: "\<exists>y. qinv(y) \<in>  Rep_preal X"
-apply (cut_tac X = X in mem_Rep_preal_Ex)
-apply (erule exE, cut_tac x = x in prat_as_inverse_ex, auto)
-done
 
-lemma preal_not_mem_inv_set_Ex:
-     "\<exists>x. x \<notin> {x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A}"
-apply (rule ccontr)
-apply (cut_tac X = A in qinv_mem_Rep_preal_Ex, auto)
-apply (erule allE, clarify) 
-apply (drule qinv_prat_less, drule not_in_preal_ub)
-apply (erule_tac x = "qinv y" in ballE)
-apply (drule prat_less_trans)
-apply (auto simp add: prat_less_not_refl)
-done
+lemma preal_not_mem_inverse_set_Ex:
+   assumes A: "A \<in> preal"  shows "\<exists>q. 0 < q & q \<notin> inverse_set A"
+proof -
+  from preal_nonempty [OF A]
+  obtain x where x: "x \<in> A" and  xpos [simp]: "0<x" ..
+  show ?thesis
+  proof (intro exI conjI)
+    show "0 < inverse x" by simp
+    show "inverse x \<notin> inverse_set A"
+    proof (auto simp add: inverse_set_def)
+      fix y::rat 
+      assume ygt: "inverse x < y"
+      have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
+      have iyless: "inverse y < x" 
+        by (simp add: inverse_less_imp_less [of x] ygt)
+      show "inverse y \<in> A"
+        by (simp add: preal_downwards_closed [OF A x] iyless) 
+    qed
+  qed
+qed
 
-lemma preal_inv_set_not_prat_set:
-     "{x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A} < UNIV"
-apply (auto intro!: psubsetI)
-apply (cut_tac A = A in preal_not_mem_inv_set_Ex, auto)
-done
+lemma inverse_set_not_rat_set:
+   assumes A: "A \<in> preal"  shows "inverse_set A < {r. 0 < r}"
+proof
+  show "inverse_set A \<subseteq> {r. 0 < r}"  by (force simp add: inverse_set_def)
+next
+  show "inverse_set A \<noteq> {r. 0 < r}"
+    by (insert preal_not_mem_inverse_set_Ex [OF A], blast)
+qed
 
 text{*Part 3 of Dedekind sections definition*}
-lemma preal_inv_set_lemma3:
-     "\<forall>y \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}.
-        \<forall>z. z < y --> z \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}"
-apply auto
-apply (rule_tac x = ya in exI)
-apply (auto intro: prat_less_trans)
+lemma inverse_set_lemma3:
+     "[|A \<in> preal; u \<in> inverse_set A; 0 < z; z < u|] 
+      ==> z \<in> inverse_set A"
+apply (auto simp add: inverse_set_def)
+apply (auto intro: order_less_trans)
 done
 
-lemma preal_inv_set_lemma4:
-     "\<forall>y \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}.
-        Bex {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A} (op < y)"
-by (blast dest: prat_dense)
-
-lemma preal_mem_inv_set: "{x. \<exists>y. x < y & qinv(y) \<notin> Rep_preal(A)} \<in> preal"
-apply (rule prealI2)
-apply (rule preal_inv_set_not_empty)
-apply (rule preal_inv_set_not_prat_set)
-apply (rule preal_inv_set_lemma3)
-apply (rule preal_inv_set_lemma4)
+text{*Part 4 of Dedekind sections definition*}
+lemma inverse_set_lemma4:
+     "[|A \<in> preal; y \<in> inverse_set A|] ==> \<exists>u \<in> inverse_set A. y < u"
+apply (auto simp add: inverse_set_def)
+apply (drule dense [of y]) 
+apply (blast intro: order_less_trans)
 done
 
-(*more lemmas for inverse *)
-lemma preal_mem_mult_invD:
-     "x \<in> Rep_preal(pinv(A)*A) ==>
-      x \<in> Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"
-apply (auto dest!: mem_Rep_preal_multD simp add: pinv_def preal_of_prat_def)
-apply (drule preal_mem_inv_set [THEN Abs_preal_inverse, THEN subst])
-apply (auto dest!: not_in_preal_ub)
-apply (drule prat_mult_less_mono, blast, auto)
+
+lemma mem_inverse_set:
+     "A \<in> preal ==> inverse_set A \<in> preal"
+apply (simp (no_asm_simp) add: preal_def cut_def)
+apply (blast intro!: inverse_set_not_empty inverse_set_not_rat_set
+                     inverse_set_lemma3 inverse_set_lemma4)
 done
 
+
 subsection{*Gleason's Lemma 9-3.4, page 122*}
 
-lemma lemma1_gleason9_34:
-     "\<forall>xa \<in> Rep_preal(A). xa + x \<in> Rep_preal(A) ==>
-             \<exists>xb \<in> Rep_preal(A). xb + (prat_of_pnat p)*x \<in> Rep_preal(A)"
-apply (cut_tac mem_Rep_preal_Ex)
-apply (induct_tac "p" rule: pnat_induct)
-apply (auto simp add: pnat_one_def pSuc_is_plus_one prat_add_mult_distrib 
-                      prat_of_pnat_add prat_add_assoc [symmetric])
-done
+(*????Why can't I get case_names like nonneg to work?*)
+lemma Gleason9_34_exists:
+  assumes A: "A \<in> preal"
+      and closed: "\<forall>x\<in>A. x + u \<in> A"
+      and nonneg: "0 \<le> z"
+     shows "\<exists>b\<in>A. b + (rat z) * u \<in> A"
+proof (cases z)
+  case (1 n)
+  show ?thesis
+  proof (simp add: prems, induct n)
+    case 0
+      from preal_nonempty [OF A]
+      show ?case  by force 
+    case (Suc k)
+      from this obtain b where "b \<in> A" "b + rat (int k) * u \<in> A" ..
+      hence "b + rat (int k)*u + u \<in> A" by (simp add: closed)
+      thus ?case by (force simp add: left_distrib add_ac prems) 
+  qed
+next
+  case (2 n)
+  with nonneg show ?thesis by simp
+qed
+
 
-lemma lemma1b_gleason9_34:
-     "Abs_prat (ratrel `` {(y, z)}) < 
-      xb +
-      Abs_prat (ratrel `` {(x*y, Abs_pnat (Suc 0))}) * 
-      Abs_prat (ratrel `` {(w, x)})"
-apply (rule_tac j =
-        "Abs_prat (ratrel `` 
-           { (x * y, Abs_pnat (Suc 0))}) * Abs_prat (ratrel `` {(w, x)})" 
-       in prat_le_less_trans)
-apply (rule_tac [2] prat_self_less_add_right)
-apply (auto intro: lemma_Abs_prat_le3 
-            simp add: prat_mult pre_lemma_gleason9_34b pnat_mult_assoc)
-done
+lemma Gleason9_34_contra:
+  assumes A: "A \<in> preal"
+    shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
+proof (induct u, induct y)
+  fix a::int and b::int
+  fix c::int and d::int
+  assume bpos [simp]: "0 < b"
+     and dpos [simp]: "0 < d"
+     and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
+     and upos: "0 < Fract c d"
+     and ypos: "0 < Fract a b"
+     and notin: "Fract a b \<notin> A"
+  have cpos [simp]: "0 < c" 
+    by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos) 
+  have apos [simp]: "0 < a" 
+    by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos) 
+  let ?k = "a*d"
+  have frle: "Fract a b \<le> rat ?k * (Fract c d)" 
+  proof -
+    have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
+      by (simp add: rat_def mult_rat le_rat order_less_imp_not_eq2 mult_ac) 
+    moreover
+    have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
+      by (rule mult_mono, 
+          simp_all add: int_one_le_iff_zero_less zero_less_mult_iff 
+                        order_less_imp_le)
+    ultimately
+    show ?thesis by simp
+  qed
+  have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff)  
+  from Gleason9_34_exists [OF A closed k]
+  obtain z where z: "z \<in> A" 
+             and mem: "z + rat ?k * Fract c d \<in> A" ..
+  have less: "z + rat ?k * Fract c d < Fract a b"
+    by (rule not_in_preal_ub [OF A notin mem ypos])
+  have "0<z" by (rule preal_imp_pos [OF A z])
+  with frle and less show False by arith 
+qed
 
-lemma lemma_gleason9_34a:
-     "\<forall>xa \<in> Rep_preal(A). xa + x \<in> Rep_preal(A) ==> False"
-apply (cut_tac X = A in not_mem_Rep_preal_Ex)
-apply (erule exE)
-apply (drule not_in_preal_ub)
-apply (rule_tac z = x in eq_Abs_prat)
-apply (rule_tac z = xa in eq_Abs_prat)
-apply (drule_tac p = "y*xb" in lemma1_gleason9_34)
-apply (erule bexE)
-apply (cut_tac x = y and y = xb and w = xaa and z = ya and xb = xba in lemma1b_gleason9_34)
-apply (drule_tac x = "xba + prat_of_pnat (y * xb) * x" in bspec)
-apply (auto intro: prat_less_asym simp add: prat_of_pnat_def)
-done
 
-lemma lemma_gleason9_34: "\<exists>r \<in> Rep_preal(R). r + x \<notin> Rep_preal(R)"
-apply (rule ccontr)
-apply (blast intro: lemma_gleason9_34a)
-done
+lemma Gleason9_34:
+  assumes A: "A \<in> preal"
+      and upos: "0 < u"
+    shows "\<exists>r \<in> A. r + u \<notin> A"
+proof (rule ccontr, simp)
+  assume closed: "\<forall>r\<in>A. r + u \<in> A"
+  from preal_exists_bound [OF A]
+  obtain y where y: "y \<notin> A" and ypos: "0 < y" by blast
+  show False
+    by (rule Gleason9_34_contra [OF A closed upos ypos y])
+qed
+
 
 
 subsection{*Gleason's Lemma 9-3.6*}
 
-lemma lemma1_gleason9_36: "r + r*qinv(xa)*Q3 = r*qinv(xa)*(xa + Q3)"
-apply (simp (no_asm_use) add: prat_add_mult_distrib2 prat_mult_assoc)
-done
+lemma lemma_gleason9_36:
+  assumes A: "A \<in> preal"
+      and x: "1 < x"
+    shows "\<exists>r \<in> A. r*x \<notin> A"
+proof -
+  from preal_nonempty [OF A]
+  obtain y where y: "y \<in> A" and  ypos: "0<y" ..
+  show ?thesis 
+  proof (rule classical)
+    assume "~(\<exists>r\<in>A. r * x \<notin> A)"
+    with y have ymem: "y * x \<in> A" by blast 
+    from ypos mult_strict_left_mono [OF x]
+    have yless: "y < y*x" by simp 
+    let ?d = "y*x - y"
+    from yless have dpos: "0 < ?d" and eq: "y + ?d = y*x" by auto
+    from Gleason9_34 [OF A dpos]
+    obtain r where r: "r\<in>A" and notin: "r + ?d \<notin> A" ..
+    have rpos: "0<r" by (rule preal_imp_pos [OF A r])
+    with dpos have rdpos: "0 < r + ?d" by arith
+    have "~ (r + ?d \<le> y + ?d)"
+    proof
+      assume le: "r + ?d \<le> y + ?d" 
+      from ymem have yd: "y + ?d \<in> A" by (simp add: eq)
+      have "r + ?d \<in> A" by (rule preal_downwards_closed' [OF A yd rdpos le])
+      with notin show False by simp
+    qed
+    hence "y < r" by simp
+    with ypos have  dless: "?d < (r * ?d)/y"
+      by (simp add: pos_less_divide_eq mult_commute [of ?d]
+                    mult_strict_right_mono dpos)
+    have "r + ?d < r*x"
+    proof -
+      have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
+      also with ypos have "... = (r/y) * (y + ?d)"
+	by (simp only: right_distrib divide_inverse_zero mult_ac, simp)
+      also have "... = r*x" using ypos
+	by simp
+      finally show "r + ?d < r*x" .
+    qed
+    with r notin rdpos
+    show "\<exists>r\<in>A. r * x \<notin> A" by (blast dest:  preal_downwards_closed [OF A])
+  qed  
+qed
 
-lemma lemma2_gleason9_36: "r*qinv(xa)*(xa*x) = r*x"
-apply (simp (no_asm_use) add: prat_mult_ac)
+subsection{*Existence of Inverse: Part 2*}
+
+lemma mem_Rep_preal_inverse_iff:
+      "(z \<in> Rep_preal(inverse R)) = 
+       (0 < z \<and> (\<exists>y. z < y \<and> inverse y \<notin> Rep_preal R))"
+apply (simp add: preal_inverse_def mem_inverse_set Rep_preal)
+apply (simp add: inverse_set_def) 
 done
 
-(*** FIXME: long! ***)
-lemma lemma_gleason9_36:
-     "prat_of_pnat 1 < x ==> \<exists>r \<in> Rep_preal(A). r*x \<notin> Rep_preal(A)"
-apply (rule_tac X1 = A in mem_Rep_preal_Ex [THEN exE])
-apply (rule_tac Q = "xa*x \<in> Rep_preal (A) " in excluded_middle [THEN disjE])
-apply fast
-apply (drule_tac x = xa in prat_self_less_mult_right)
-apply (erule prat_lessE)
-apply (cut_tac R = A and x = Q3 in lemma_gleason9_34)
-apply (drule sym, auto)
-apply (frule not_in_preal_ub)
-apply (drule_tac x = "xa + Q3" in bspec, assumption)
-apply (drule prat_add_right_less_cancel)
-apply (drule_tac x = "qinv (xa) *Q3" in prat_mult_less2_mono1)
-apply (drule_tac x = r in prat_add_less2_mono2)
-apply (simp add: prat_mult_assoc [symmetric] lemma1_gleason9_36)
-apply (drule sym)
-apply (auto simp add: lemma2_gleason9_36)
-apply (rule_tac x = r in bexI)
-apply (rule notI)
-apply (drule_tac y = "r*x" in Rep_preal [THEN prealE_lemma3b], auto)
+lemma Rep_preal_of_rat:
+     "0 < q ==> Rep_preal (preal_of_rat q) = {x. 0 < x \<and> x < q}"
+by (simp add: preal_of_rat_def rat_mem_preal) 
+
+lemma subset_inverse_mult_lemma:
+      assumes xpos: "0 < x" and xless: "x < 1"
+         shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R & 
+                        u \<in> Rep_preal R & x = r * u"
+proof -
+  from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff)
+  from lemma_gleason9_36 [OF Rep_preal this]
+  obtain r where r: "r \<in> Rep_preal R" 
+             and notin: "r * (inverse x) \<notin> Rep_preal R" ..
+  have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
+  from preal_exists_greater [OF Rep_preal r]
+  obtain u where u: "u \<in> Rep_preal R" and rless: "r < u" ..
+  have upos: "0<u" by (rule preal_imp_pos [OF Rep_preal u])
+  show ?thesis
+  proof (intro exI conjI)
+    show "0 < x/u" using xpos upos
+      by (simp add: zero_less_divide_iff)  
+    show "x/u < x/r" using xpos upos rpos
+      by (simp add: divide_inverse_zero mult_less_cancel_left rless) 
+    show "inverse (x / r) \<notin> Rep_preal R" using notin
+      by (simp add: divide_inverse_zero mult_commute) 
+    show "u \<in> Rep_preal R" by (rule u) 
+    show "x = x / u * u" using upos 
+      by (simp add: divide_inverse_zero mult_commute) 
+  qed
+qed
+
+lemma subset_inverse_mult: 
+     "Rep_preal(preal_of_rat 1) \<subseteq> Rep_preal(inverse R * R)"
+apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
+                      mem_Rep_preal_mult_iff)
+apply (blast dest: subset_inverse_mult_lemma) 
 done
 
-lemma lemma_gleason9_36a:
-     "prat_of_pnat (Abs_pnat (Suc 0)) < x ==>
-      \<exists>r \<in> Rep_preal(A). r*x \<notin> Rep_preal(A)"
-apply (rule lemma_gleason9_36)
-apply (simp (no_asm_simp) add: pnat_one_def)
+lemma inverse_mult_subset_lemma:
+     assumes rpos: "0 < r" 
+         and rless: "r < y"
+         and notin: "inverse y \<notin> Rep_preal R"
+         and q: "q \<in> Rep_preal R"
+     shows "r*q < 1"
+proof -
+  have "q < inverse y" using rpos rless
+    by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
+  hence "r * q < r/y" using rpos
+    by (simp add: divide_inverse_zero mult_less_cancel_left)
+  also have "... \<le> 1" using rpos rless
+    by (simp add: pos_divide_le_eq)
+  finally show ?thesis .
+qed
+
+lemma inverse_mult_subset:
+     "Rep_preal(inverse R * R) \<subseteq> Rep_preal(preal_of_rat 1)"
+apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
+                      mem_Rep_preal_mult_iff)
+apply (simp add: zero_less_mult_iff preal_imp_pos [OF Rep_preal]) 
+apply (blast intro: inverse_mult_subset_lemma) 
+done
+
+lemma preal_mult_inverse:
+     "inverse R * R = (preal_of_rat 1)"
+apply (rule inj_Rep_preal [THEN injD])
+apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) 
+done
+
+lemma preal_mult_inverse_right:
+     "R * inverse R = (preal_of_rat 1)"
+apply (rule preal_mult_commute [THEN subst])
+apply (rule preal_mult_inverse)
 done
 
 
-subsection{*Existence of Inverse: Part 2*}
-lemma preal_mem_mult_invI:
-     "x \<in> Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))
-      ==> x \<in> Rep_preal(pinv(A)*A)"
-apply (auto intro!: mem_Rep_preal_multI simp add: pinv_def preal_of_prat_def)
-apply (rule preal_mem_inv_set [THEN Abs_preal_inverse, THEN ssubst])
-apply (drule prat_qinv_gt_1)
-apply (drule_tac A = A in lemma_gleason9_36a, auto)
-apply (drule Rep_preal [THEN prealE_lemma4a])
-apply (auto, drule qinv_prat_less)
-apply (rule_tac x = "qinv (u) *x" in exI)
-apply (rule conjI)
-apply (rule_tac x = "qinv (r) *x" in exI)
-apply (auto intro: prat_mult_less2_mono1 simp add: qinv_mult_eq qinv_qinv)
-apply (rule_tac x = u in bexI)
-apply (auto simp add: prat_mult_assoc prat_mult_left_commute)
-done
-
-lemma preal_mult_inv:
-     "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"
-apply (rule inj_Rep_preal [THEN injD])
-apply (fast dest: preal_mem_mult_invD preal_mem_mult_invI)
-done
+text{*Theorems needing @{text Gleason9_34}*}
 
-lemma preal_mult_inv_right:
-     "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"
-apply (rule preal_mult_commute [THEN subst])
-apply (rule preal_mult_inv)
-done
-
-
-text{*Theorems needing @{text lemma_gleason9_34}*}
+lemma Rep_preal_self_subset: "Rep_preal (R) \<subseteq> Rep_preal(R + S)"
+proof 
+  fix r
+  assume r: "r \<in> Rep_preal R"
+  have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
+  from mem_Rep_preal_Ex 
+  obtain y where y: "y \<in> Rep_preal S" ..
+  have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
+  have ry: "r+y \<in> Rep_preal(R + S)" using r y
+    by (auto simp add: mem_Rep_preal_add_iff)
+  show "r \<in> Rep_preal(R + S)" using r ypos rpos 
+    by (simp add:  preal_downwards_closed [OF Rep_preal ry]) 
+qed
 
-lemma Rep_preal_self_subset: "Rep_preal (R1) \<subseteq> Rep_preal(R1 + R2)"
-apply (cut_tac X = R2 in mem_Rep_preal_Ex)
-apply (auto intro!: bexI 
-            intro: Rep_preal [THEN prealE_lemma3b] prat_self_less_add_left 
-                   mem_Rep_preal_addI)
-done
+lemma Rep_preal_sum_not_subset: "~ Rep_preal (R + S) \<subseteq> Rep_preal(R)"
+proof -
+  from mem_Rep_preal_Ex 
+  obtain y where y: "y \<in> Rep_preal S" ..
+  have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
+  from  Gleason9_34 [OF Rep_preal ypos]
+  obtain r where r: "r \<in> Rep_preal R" and notin: "r + y \<notin> Rep_preal R" ..
+  have "r + y \<in> Rep_preal (R + S)" using r y
+    by (auto simp add: mem_Rep_preal_add_iff)
+  thus ?thesis using notin by blast
+qed
 
-lemma Rep_preal_sum_not_subset: "~ Rep_preal (R1 + R2) \<subseteq> Rep_preal(R1)"
-apply (cut_tac X = R2 in mem_Rep_preal_Ex)
-apply (erule exE)
-apply (cut_tac R = R1 in lemma_gleason9_34)
-apply (auto intro: mem_Rep_preal_addI)
-done
-
-lemma Rep_preal_sum_not_eq: "Rep_preal (R1 + R2) \<noteq> Rep_preal(R1)"
-apply (rule notI)
-apply (erule equalityE)
-apply (simp add: Rep_preal_sum_not_subset)
-done
+lemma Rep_preal_sum_not_eq: "Rep_preal (R + S) \<noteq> Rep_preal(R)"
+by (insert Rep_preal_sum_not_subset, blast)
 
 text{*at last, Gleason prop. 9-3.5(iii) page 123*}
-lemma preal_self_less_add_left: "(R1::preal) < R1 + R2"
+lemma preal_self_less_add_left: "(R::preal) < R + S"
 apply (unfold preal_less_def psubset_def)
 apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
 done
 
-lemma preal_self_less_add_right: "(R1::preal) < R2 + R1"
-apply (simp add: preal_add_commute preal_self_less_add_left)
-done
+lemma preal_self_less_add_right: "(R::preal) < S + R"
+by (simp add: preal_add_commute preal_self_less_add_left)
+
+lemma preal_not_eq_self: "x \<noteq> x + (y::preal)"
+by (insert preal_self_less_add_left [of x y], auto)
 
 
-subsection{*The @{text "\<le>"} Ordering*}
-
-lemma preal_less_le_iff: "(~(w < z)) = (z \<le> (w::preal))"
-apply (unfold preal_le_def psubset_def preal_less_def)
-apply (insert preal_linear [of w z])
-apply (auto simp add: preal_less_def psubset_def)
-done
-
-lemma preal_le_iff_less_or_eq:
-     "((x::preal) \<le> y) = (x < y | x = y)"
-apply (unfold preal_le_def preal_less_def psubset_def)
-apply (auto intro: inj_Rep_preal [THEN injD])
-done
-
-lemma preal_le_refl: "w \<le> (w::preal)"
-apply (simp add: preal_le_def)
-done
-
-lemma preal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::preal)"
-apply (simp add: preal_le_iff_less_or_eq) 
-apply (blast intro: preal_less_trans)
-done
-
-lemma preal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::preal)"
-apply (simp add: preal_le_iff_less_or_eq) 
-apply (blast intro: preal_less_asym)
-done
+subsection{*Subtraction for Positive Reals*}
 
-lemma preal_neq_iff: "(w \<noteq> z) = (w<z | z < (w::preal))"
-apply (insert preal_linear [of w z])
-apply (auto elim: preal_less_irrefl)
-done
-
-(* Axiom 'order_less_le' of class 'order': *)
-lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
-apply (simp (no_asm) add: preal_less_le_iff [symmetric] preal_neq_iff)
-apply (blast elim!: preal_less_asym)
-done
-
-instance preal :: order
-proof qed
- (assumption |
-  rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
-
-lemma preal_le_linear: "x <= y | y <= (x::preal)"
-apply (insert preal_linear [of x y]) 
-apply (auto simp add: order_less_le) 
-done
-
-instance preal :: linorder
-  by (intro_classes, rule preal_le_linear)
-
-
-subsection{*Gleason prop. 9-3.5(iv), page 123*}
-
-text{*Proving @{term "A < B ==> \<exists>D. A + D = B"}*}
-
-text{*Define the claimed D and show that it is a positive real*}
+text{*Gleason prop. 9-3.5(iv), page 123: proving @{term "A < B ==> \<exists>D. A + D =
+B"}. We define the claimed @{term D} and show that it is a positive real*}
 
 text{*Part 1 of Dedekind sections definition*}
-lemma lemma_ex_mem_less_left_add1:
-     "A < B ==>
-      \<exists>q. q \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
-apply (unfold preal_less_def psubset_def)
-apply (clarify) 
-apply (drule_tac x1 = B in Rep_preal [THEN prealE_lemma4a])
-apply (auto simp add: prat_less_def)
-done
-
-lemma preal_less_set_not_empty:
-     "A < B ==> {} < {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
-apply (drule lemma_ex_mem_less_left_add1)
-apply (auto intro!: psubsetI)
+lemma diff_set_not_empty:
+     "R < S ==> {} \<subset> diff_set (Rep_preal S) (Rep_preal R)"
+apply (auto simp add: preal_less_def diff_set_def elim!: equalityE) 
+apply (frule_tac x1 = S in Rep_preal [THEN preal_exists_greater])
+apply (drule preal_imp_pos [OF Rep_preal], clarify)
+apply (cut_tac a=x and b=u in add_eq_exists, force) 
 done
 
 text{*Part 2 of Dedekind sections definition*}
-lemma lemma_ex_not_mem_less_left_add1:
-     "\<exists>q. q \<notin> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
-apply (cut_tac X = B in not_mem_Rep_preal_Ex)
+lemma diff_set_nonempty:
+     "\<exists>q. 0 < q & q \<notin> diff_set (Rep_preal S) (Rep_preal R)"
+apply (cut_tac X = S in Rep_preal_exists_bound)
 apply (erule exE)
 apply (rule_tac x = x in exI, auto)
-apply (cut_tac x = x and y = n in prat_self_less_add_right)
-apply (auto dest: Rep_preal [THEN prealE_lemma3b])
+apply (simp add: diff_set_def) 
+apply (auto dest: Rep_preal [THEN preal_downwards_closed])
 done
 
-lemma preal_less_set_not_prat_set:
-     "{d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)} < UNIV"
-apply (auto intro!: psubsetI)
-apply (cut_tac A = A and B = B in lemma_ex_not_mem_less_left_add1, auto)
-done
+lemma diff_set_not_rat_set:
+     "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs" by (auto simp add: diff_set_def) 
+  show "?lhs \<noteq> ?rhs" using diff_set_nonempty by blast
+qed
 
 text{*Part 3 of Dedekind sections definition*}
-lemma preal_less_set_lemma3:
-     "A < B ==> \<forall>y \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}.
-     \<forall>z. z < y --> z \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
-apply auto
-apply (drule_tac x = n in prat_add_less2_mono2)
-apply (drule Rep_preal [THEN prealE_lemma3b], auto)
+lemma diff_set_lemma3:
+     "[|R < S; u \<in> diff_set (Rep_preal S) (Rep_preal R); 0 < z; z < u|] 
+      ==> z \<in> diff_set (Rep_preal S) (Rep_preal R)"
+apply (auto simp add: diff_set_def) 
+apply (rule_tac x=x in exI) 
+apply (drule Rep_preal [THEN preal_downwards_closed], auto)
 done
 
-lemma preal_less_set_lemma4:
-     "A < B ==> \<forall>y \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}.
-        Bex {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)} (op < y)"
-apply auto
-apply (drule Rep_preal [THEN prealE_lemma4a])
-apply (auto simp add: prat_less_def prat_add_assoc)
+text{*Part 4 of Dedekind sections definition*}
+lemma diff_set_lemma4:
+     "[|R < S; y \<in> diff_set (Rep_preal S) (Rep_preal R)|] 
+      ==> \<exists>u \<in> diff_set (Rep_preal S) (Rep_preal R). y < u"
+apply (auto simp add: diff_set_def) 
+apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
+apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify)  
+apply (rule_tac x="y+xa" in exI) 
+apply (auto simp add: add_ac)
 done
 
-lemma preal_mem_less_set:
-     "!! (A::preal). A < B ==>
-      {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}: preal"
-apply (rule prealI2)
-apply (rule preal_less_set_not_empty)
-apply (rule_tac [2] preal_less_set_not_prat_set)
-apply (rule_tac [2] preal_less_set_lemma3)
-apply (rule_tac [3] preal_less_set_lemma4, auto)
+lemma mem_diff_set:
+     "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
+apply (unfold preal_def cut_def)
+apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
+                     diff_set_lemma3 diff_set_lemma4)
+done
+
+lemma mem_Rep_preal_diff_iff:
+      "R < S ==>
+       (z \<in> Rep_preal(S-R)) = 
+       (\<exists>x. 0 < x & 0 < z & x \<notin> Rep_preal R & x + z \<in> Rep_preal S)"
+apply (simp add: preal_diff_def mem_diff_set Rep_preal)
+apply (force simp add: diff_set_def) 
 done
 
-text{*proving that @{term "A + D \<le> B"}*}
-lemma preal_less_add_left_subsetI:
-       "!! (A::preal). A < B ==>
-          A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}) \<le> B"
-apply (unfold preal_le_def)
-apply (rule subsetI)
-apply (drule mem_Rep_preal_addD)
-apply (auto simp add: preal_mem_less_set [THEN Abs_preal_inverse])
-apply (drule not_in_preal_ub)
-apply (drule bspec, assumption)
-apply (drule_tac x = y in prat_add_less2_mono1)
-apply (drule_tac x1 = B in Rep_preal [THEN prealE_lemma3b], auto)
+
+text{*proving that @{term "R + D \<le> S"}*}
+
+lemma less_add_left_lemma:
+  assumes Rless: "R < S"
+      and a: "a \<in> Rep_preal R"
+      and cb: "c + b \<in> Rep_preal S"
+      and "c \<notin> Rep_preal R"
+      and "0 < b"
+      and "0 < c"
+  shows "a + b \<in> Rep_preal S"
+proof -
+  have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
+  moreover
+  have "a < c" using prems
+    by (blast intro: not_in_Rep_preal_ub ) 
+  ultimately show ?thesis using prems
+    by (simp add: preal_downwards_closed [OF Rep_preal cb]) 
+qed
+
+lemma less_add_left_le1:
+       "R < (S::preal) ==> R + (S-R) \<le> S"
+apply (auto simp add: Bex_def preal_le_def mem_Rep_preal_add_iff 
+                      mem_Rep_preal_diff_iff)
+apply (blast intro: less_add_left_lemma) 
 done
 
-subsection{*proving that @{term "B \<le> A + D"} --- trickier*}
+subsection{*proving that @{term "S \<le> R + D"} --- trickier*}
 
 lemma lemma_sum_mem_Rep_preal_ex:
-     "x \<in> Rep_preal(B) ==> \<exists>e. x + e \<in> Rep_preal(B)"
-apply (drule Rep_preal [THEN prealE_lemma4a])
-apply (auto simp add: prat_less_def)
+     "x \<in> Rep_preal S ==> \<exists>e. 0 < e & x + e \<in> Rep_preal S"
+apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
+apply (cut_tac a=x and b=u in add_eq_exists, auto) 
 done
 
-lemma preal_less_add_left_subsetI2:
-       "!! (A::preal). A < B ==>
-          B \<le> A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)})"
-apply (unfold preal_le_def)
-apply (rule subsetI)
-apply (rule_tac Q = "x \<in> Rep_preal (A) " in excluded_middle [THEN disjE])
-apply (rule mem_Rep_preal_addI)
-apply (drule lemma_sum_mem_Rep_preal_ex)
-apply (erule exE)
-apply (cut_tac R = A and x = e in lemma_gleason9_34, erule bexE)
-apply (drule not_in_preal_ub, drule bspec, assumption)
-apply (erule prat_lessE)
-apply (rule_tac x = r in bexI)
-apply (rule_tac x = Q3 in bexI)
-apply (cut_tac [4] Rep_preal_self_subset)
-apply (auto simp add: preal_mem_less_set [THEN Abs_preal_inverse])
-apply (rule_tac x = "r+e" in exI)
-apply (simp add: prat_add_ac)
+lemma less_add_left_lemma2:
+  assumes Rless: "R < S"
+      and x:     "x \<in> Rep_preal S"
+      and xnot: "x \<notin>  Rep_preal R"
+  shows "\<exists>u v z. 0 < v & 0 < z & u \<in> Rep_preal R & z \<notin> Rep_preal R & 
+                     z + v \<in> Rep_preal S & x = u + v"
+proof -
+  have xpos: "0<x" by (rule preal_imp_pos [OF Rep_preal x])
+  from lemma_sum_mem_Rep_preal_ex [OF x]
+  obtain e where epos: "0 < e" and xe: "x + e \<in> Rep_preal S" by blast
+  from  Gleason9_34 [OF Rep_preal epos]
+  obtain r where r: "r \<in> Rep_preal R" and notin: "r + e \<notin> Rep_preal R" ..
+  with x xnot xpos have rless: "r < x" by (blast intro: not_in_Rep_preal_ub)
+  from add_eq_exists [of r x]
+  obtain y where eq: "x = r+y" by auto
+  show ?thesis 
+  proof (intro exI conjI)
+    show "r \<in> Rep_preal R" by (rule r)
+    show "r + e \<notin> Rep_preal R" by (rule notin)
+    show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac)
+    show "x = r + y" by (simp add: eq)
+    show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r]
+      by simp
+    show "0 < y" using rless eq by arith
+  qed
+qed
+
+lemma less_add_left_le2: "R < (S::preal) ==> S \<le> R + (S-R)"
+apply (auto simp add: preal_le_def)
+apply (case_tac "x \<in> Rep_preal R")
+apply (cut_tac Rep_preal_self_subset [of R], force)
+apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_diff_iff)
+apply (blast dest: less_add_left_lemma2)
 done
 
-(*** required proof ***)
-lemma preal_less_add_left:
-     "!! (A::preal). A < B ==>
-          A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}) = B"
-apply (blast intro: preal_le_anti_sym preal_less_add_left_subsetI preal_less_add_left_subsetI2)
-done
+lemma less_add_left: "R < (S::preal) ==> R + (S-R) = S"
+by (blast intro: preal_le_anti_sym [OF less_add_left_le1 less_add_left_le2])
 
-lemma preal_less_add_left_Ex: "!! (A::preal). A < B ==> \<exists>D. A + D = B"
-by (fast dest: preal_less_add_left)
+lemma less_add_left_Ex: "R < (S::preal) ==> \<exists>D. R + D = S"
+by (fast dest: less_add_left)
 
-lemma preal_add_less2_mono1: "!!(A::preal). A < B ==> A + C < B + C"
-apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_assoc)
+lemma preal_add_less2_mono1: "R < (S::preal) ==> R + T < S + T"
+apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc)
 apply (rule_tac y1 = D in preal_add_commute [THEN subst])
 apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric])
 done
 
-lemma preal_add_less2_mono2: "!!(A::preal). A < B ==> C + A < C + B"
-by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute)
+lemma preal_add_less2_mono2: "R < (S::preal) ==> T + R < T + S"
+by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of T])
 
-lemma preal_mult_less_mono1:
-      "!!(q1::preal). q1 < q2 ==> q1 * x < q2 * x"
-apply (drule preal_less_add_left_Ex)
-apply (auto simp add: preal_add_mult_distrib preal_self_less_add_left)
-done
-
-lemma preal_mult_left_less_mono1: "!!(q1::preal). q1 < q2  ==> x * q1 < x * q2"
-by (auto dest: preal_mult_less_mono1 simp add: preal_mult_commute)
-
-lemma preal_mult_left_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> x * q1 \<le> x * q2"
-apply (simp add: preal_le_iff_less_or_eq) 
-apply (blast intro!: preal_mult_left_less_mono1)
+lemma preal_add_right_less_cancel: "R + T < S + T ==> R < (S::preal)"
+apply (insert linorder_less_linear [of R S], auto)
+apply (drule_tac R = S and T = T in preal_add_less2_mono1)
+apply (blast dest: order_less_trans) 
 done
 
-lemma preal_mult_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> q1 * x \<le> q2 * x"
-by (auto dest: preal_mult_left_le_mono1 simp add: preal_mult_commute)
-
-lemma preal_add_left_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> x + q1 \<le> x + q2"
-apply (simp add: preal_le_iff_less_or_eq) 
-apply (auto intro!: preal_add_less2_mono1 simp add: preal_add_commute)
-done
-
-lemma preal_add_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> q1 + x \<le> q2 + x"
-by (auto dest: preal_add_left_le_mono1 simp add: preal_add_commute)
+lemma preal_add_left_less_cancel: "T + R < T + S ==> R <  (S::preal)"
+by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T])
 
-lemma preal_add_right_less_cancel: "!!(A::preal). A + C < B + C ==> A < B"
-apply (cut_tac preal_linear)
-apply (auto elim: preal_less_irrefl)
-apply (drule_tac A = B and C = C in preal_add_less2_mono1)
-apply (fast dest: preal_less_trans elim: preal_less_irrefl)
-done
-
-lemma preal_add_left_less_cancel: "!!(A::preal). C + A < C + B ==> A < B"
-by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute)
-
-lemma preal_add_less_iff1 [simp]: "((A::preal) + C < B + C) = (A < B)"
+lemma preal_add_less_cancel_right: "((R::preal) + T < S + T) = (R < S)"
 by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel)
 
-lemma preal_add_less_iff2 [simp]: "(C + (A::preal) < C + B) = (A < B)"
+lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)"
 by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
 
+lemma preal_add_le_cancel_right: "((R::preal) + T \<le> S + T) = (R \<le> S)"
+by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_right) 
+
+lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
+by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left) 
+
 lemma preal_add_less_mono:
      "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)"
-apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_ac)
+apply (auto dest!: less_add_left_Ex simp add: preal_add_ac)
 apply (rule preal_add_assoc [THEN subst])
 apply (rule preal_self_less_add_right)
 done
 
-lemma preal_mult_less_mono:
-     "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)"
-apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_mult_distrib preal_add_mult_distrib2 preal_self_less_add_left preal_add_assoc preal_mult_ac)
+lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S"
+apply (insert linorder_less_linear [of R S], safe)
+apply (drule_tac [!] T = T in preal_add_less2_mono1, auto)
 done
 
-lemma preal_add_right_cancel: "(A::preal) + C = B + C ==> A = B"
-apply (cut_tac preal_linear [of A B], safe)
-apply (drule_tac [!] C = C in preal_add_less2_mono1)
-apply (auto elim: preal_less_irrefl)
-done
-
-lemma preal_add_left_cancel: "!!(A::preal). C + A = C + B ==> A = B"
+lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)"
 by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
 
-lemma preal_add_left_cancel_iff [simp]: "(C + A = C + B) = ((A::preal) = B)"
+lemma preal_add_left_cancel_iff: "(C + A = C + B) = ((A::preal) = B)"
 by (fast intro: preal_add_left_cancel)
 
-lemma preal_add_right_cancel_iff [simp]: "(A + C = B + C) = ((A::preal) = B)"
+lemma preal_add_right_cancel_iff: "(A + C = B + C) = ((A::preal) = B)"
 by (fast intro: preal_add_right_cancel)
 
+lemmas preal_cancels =
+    preal_add_less_cancel_right preal_add_less_cancel_left
+    preal_add_le_cancel_right preal_add_le_cancel_left
+    preal_add_left_cancel_iff preal_add_right_cancel_iff
 
 
 subsection{*Completeness of type @{typ preal}*}
 
 text{*Prove that supremum is a cut*}
 
-lemma preal_sup_mem_Ex:
-     "\<exists>X. X \<in> P ==> \<exists>q.  q \<in> {w. \<exists>X. X \<in> P & w \<in> Rep_preal X}"
-apply safe
-apply (cut_tac X = X in mem_Rep_preal_Ex, auto)
+text{*Part 1 of Dedekind sections definition*}
+
+lemma preal_sup_set_not_empty:
+     "P \<noteq> {} ==> {} \<subset> (\<Union>X \<in> P. Rep_preal(X))"
+apply auto
+apply (cut_tac X = x in mem_Rep_preal_Ex, auto)
 done
 
-text{*Part 1 of Dedekind sections definition*}
-lemma preal_sup_set_not_empty:
-     "\<exists>(X::preal). X \<in> P ==>
-          {} < {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
-apply (drule preal_sup_mem_Ex)
-apply (auto intro!: psubsetI)
-done
 
 text{*Part 2 of Dedekind sections definition*}
-lemma preal_sup_not_mem_Ex:
-     "\<exists>Y. (\<forall>X \<in> P. X < Y)
-          ==> \<exists>q. q \<notin> {w. \<exists>X. X \<in> P & w \<in> Rep_preal(X)}"
-apply (unfold preal_less_def)
-apply (auto simp add: psubset_def)
-apply (cut_tac X = Y in not_mem_Rep_preal_Ex)
-apply (erule exE)
-apply (rule_tac x = x in exI)
-apply (auto dest!: bspec)
+
+lemma preal_sup_not_exists:
+     "\<forall>X \<in> P. X \<le> Y ==> \<exists>q. 0 < q & q \<notin> (\<Union>X \<in> P. Rep_preal(X))"
+apply (cut_tac X = Y in Rep_preal_exists_bound)
+apply (auto simp add: preal_le_def)
 done
 
-lemma preal_sup_not_mem_Ex1:
-     "\<exists>Y. (\<forall>X \<in> P. X \<le> Y)
-          ==> \<exists>q. q \<notin> {w. \<exists>X. X \<in> P & w \<in> Rep_preal(X)}"
-apply (unfold preal_le_def, safe)
-apply (cut_tac X = Y in not_mem_Rep_preal_Ex)
-apply (erule exE)
-apply (rule_tac x = x in exI)
-apply (auto dest!: bspec)
-done
-
-lemma preal_sup_set_not_prat_set:
-     "\<exists>Y. (\<forall>X \<in> P. X < Y) ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)} < UNIV"
-apply (drule preal_sup_not_mem_Ex)
-apply (auto intro!: psubsetI)
-done
-
-lemma preal_sup_set_not_prat_set1:
-     "\<exists>Y. (\<forall>X \<in> P. X \<le> Y) ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)} < UNIV"
-apply (drule preal_sup_not_mem_Ex1)
-apply (auto intro!: psubsetI)
+lemma preal_sup_set_not_rat_set:
+     "\<forall>X \<in> P. X \<le> Y ==> (\<Union>X \<in> P. Rep_preal(X)) < {r. 0 < r}"
+apply (drule preal_sup_not_exists)
+apply (blast intro: preal_imp_pos [OF Rep_preal])  
 done
 
 text{*Part 3 of Dedekind sections definition*}
 lemma preal_sup_set_lemma3:
-     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
-          ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
-              \<forall>z. z < y --> z \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
-apply (auto elim: Rep_preal [THEN prealE_lemma3b])
-done
-
-lemma preal_sup_set_lemma3_1:
-     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
-          ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
-              \<forall>z. z < y --> z \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
-apply (auto elim: Rep_preal [THEN prealE_lemma3b])
-done
+     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; u \<in> (\<Union>X \<in> P. Rep_preal(X)); 0 < z; z < u|]
+      ==> z \<in> (\<Union>X \<in> P. Rep_preal(X))"
+by (auto elim: Rep_preal [THEN preal_downwards_closed])
 
+text{*Part 4 of Dedekind sections definition*}
 lemma preal_sup_set_lemma4:
-     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
-          ==>  \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
-              Bex {w. \<exists>X \<in> P. w \<in> Rep_preal X} (op < y)"
-apply (blast dest: Rep_preal [THEN prealE_lemma4a])
-done
-
-lemma preal_sup_set_lemma4_1:
-     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
-          ==>  \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
-              Bex {w. \<exists>X \<in> P. w \<in> Rep_preal X} (op < y)"
-apply (blast dest: Rep_preal [THEN prealE_lemma4a])
-done
+     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; y \<in> (\<Union>X \<in> P. Rep_preal(X)) |]
+          ==> \<exists>u \<in> (\<Union>X \<in> P. Rep_preal(X)). y < u"
+by (blast dest: Rep_preal [THEN preal_exists_greater])
 
 lemma preal_sup:
-     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
-          ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)}: preal"
-apply (rule prealI2)
-apply (rule preal_sup_set_not_empty)
-apply (rule_tac [2] preal_sup_set_not_prat_set)
-apply (rule_tac [3] preal_sup_set_lemma3)
-apply (rule_tac [5] preal_sup_set_lemma4, auto)
+     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
+apply (unfold preal_def cut_def)
+apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
+                     preal_sup_set_lemma3 preal_sup_set_lemma4)
 done
 
-lemma preal_sup1:
-     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
-          ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)}: preal"
-apply (rule prealI2)
-apply (rule preal_sup_set_not_empty)
-apply (rule_tac [2] preal_sup_set_not_prat_set1)
-apply (rule_tac [3] preal_sup_set_lemma3_1)
-apply (rule_tac [5] preal_sup_set_lemma4_1, auto)
-done
-
-lemma preal_psup_leI: "\<exists>Y. (\<forall>X \<in> P. X < Y) ==> \<forall>x \<in> P. x \<le> psup P"
-apply (unfold psup_def)
-apply (auto simp add: preal_le_def)
-apply (rule preal_sup [THEN Abs_preal_inverse, THEN ssubst], auto)
-done
-
-lemma preal_psup_leI2: "\<exists>Y. (\<forall>X \<in> P. X \<le> Y) ==> \<forall>x \<in> P. x \<le> psup P"
-apply (unfold psup_def)
-apply (auto simp add: preal_le_def)
-apply (rule preal_sup1 [THEN Abs_preal_inverse, THEN ssubst])
-apply (auto simp add: preal_le_def)
+lemma preal_psup_le:
+     "[| \<forall>X \<in> P. X \<le> Y;  x \<in> P |] ==> x \<le> psup P"
+apply (simp (no_asm_simp) add: preal_le_def) 
+apply (subgoal_tac "P \<noteq> {}") 
+apply (auto simp add: psup_def preal_sup) 
 done
 
-lemma preal_psup_leI2b:
-     "[| \<exists>Y. (\<forall>X \<in> P. X < Y); x \<in> P |] ==> x \<le> psup P"
-apply (blast dest!: preal_psup_leI)
-done
-
-lemma preal_psup_leI2a:
-     "[| \<exists>Y. (\<forall>X \<in> P. X \<le> Y); x \<in> P |] ==> x \<le> psup P"
-apply (blast dest!: preal_psup_leI2)
-done
-
-lemma psup_le_ub: "[| \<exists>X. X \<in> P; \<forall>X \<in> P. X < Y |] ==> psup P \<le> Y"
-apply (unfold psup_def)
+lemma psup_le_ub: "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> Y"
+apply (simp (no_asm_simp) add: preal_le_def)
+apply (simp add: psup_def preal_sup) 
 apply (auto simp add: preal_le_def)
-apply (drule preal_sup [OF exI exI, THEN Abs_preal_inverse, THEN subst])
-apply (rotate_tac [2] 1)
-prefer 2 apply assumption
-apply (auto dest!: bspec simp add: preal_less_def psubset_def)
-done
-
-lemma psup_le_ub1: "[| \<exists>X. X \<in> P; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> Y"
-apply (unfold psup_def)
-apply (auto simp add: preal_le_def)
-apply (drule preal_sup1 [OF exI exI, THEN Abs_preal_inverse, THEN subst])
-apply (rotate_tac [2] 1)
-prefer 2 apply assumption
-apply (auto dest!: bspec simp add: preal_less_def psubset_def preal_le_def)
 done
 
 text{*Supremum property*}
 lemma preal_complete:
-     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
-          ==> (\<forall>Y. (\<exists>X \<in> P. Y < X) = (Y < psup P))"
-apply (frule preal_sup [THEN Abs_preal_inverse], fast)
-apply (auto simp add: psup_def preal_less_def)
-apply (cut_tac x = Xa and y = Ya in preal_linear)
-apply (auto dest: psubsetD simp add: preal_less_def)
+     "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> (\<exists>X \<in> P. Z < X) = (Z < psup P)"
+apply (simp add: preal_less_def psup_def preal_sup)
+apply (auto simp add: preal_le_def)
+apply (rename_tac U) 
+apply (cut_tac x = U and y = Z in linorder_less_linear)
+apply (auto simp add: preal_less_def)
 done
 
 
-subsection{*The Embadding from @{typ prat} into @{typ preal}*}
+subsection{*The Embadding from @{typ rat} into @{typ preal}*}
 
-lemma lemma_preal_rat_less: "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1"
-apply (drule_tac x = "z1 * qinv (z1 + z2) " in prat_mult_less2_mono1)
-apply (simp add: prat_mult_ac)
-done
-
-lemma lemma_preal_rat_less2: "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2"
-apply (subst prat_add_commute)
-apply (drule prat_add_commute [THEN subst])
-apply (erule lemma_preal_rat_less)
+lemma preal_of_rat_add_lemma1:
+     "[|x < y + z; 0 < x; 0 < y|] ==> x * y * inverse (y + z) < (y::rat)"
+apply (frule_tac c = "y * inverse (y + z) " in mult_strict_right_mono)
+apply (simp add: zero_less_mult_iff) 
+apply (simp add: mult_ac)
 done
 
-lemma preal_of_prat_add:
-      "preal_of_prat ((z1::prat) + z2) =
-       preal_of_prat z1 + preal_of_prat z2"
-apply (unfold preal_of_prat_def preal_add_def)
+lemma preal_of_rat_add_lemma2:
+  assumes "u < x + y"
+      and "0 < x"
+      and "0 < y"
+      and "0 < u"
+  shows "\<exists>v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w"
+proof (intro exI conjI)
+  show "u * x * inverse(x+y) < x" using prems 
+    by (simp add: preal_of_rat_add_lemma1) 
+  show "u * y * inverse(x+y) < y" using prems 
+    by (simp add: preal_of_rat_add_lemma1 add_commute [of x]) 
+  show "0 < u * x * inverse (x + y)" using prems
+    by (simp add: zero_less_mult_iff) 
+  show "0 < u * y * inverse (x + y)" using prems
+    by (simp add: zero_less_mult_iff) 
+  show "u = u * x * inverse (x + y) + u * y * inverse (x + y)" using prems
+    by (simp add: left_distrib [symmetric] right_distrib [symmetric] mult_ac)
+qed
+
+lemma preal_of_rat_add:
+     "[| 0 < x; 0 < y|] 
+      ==> preal_of_rat ((x::rat) + y) = preal_of_rat x + preal_of_rat y"
+apply (unfold preal_of_rat_def preal_add_def)
+apply (simp add: rat_mem_preal) 
 apply (rule_tac f = Abs_preal in arg_cong)
-apply (auto intro: prat_add_less_mono 
-            simp add: lemma_prat_less_set_mem_preal [THEN Abs_preal_inverse])
-apply (rule_tac x = "x*z1*qinv (z1+z2) " in exI, rule conjI)
-apply (erule lemma_preal_rat_less)
-apply (rule_tac x = "x*z2*qinv (z1+z2) " in exI, rule conjI)
-apply (erule lemma_preal_rat_less2)
-apply (simp add: prat_add_mult_distrib [symmetric] 
-                 prat_add_mult_distrib2 [symmetric] prat_mult_ac)
+apply (auto simp add: add_set_def) 
+apply (blast dest: preal_of_rat_add_lemma2) 
+done
+
+lemma preal_of_rat_mult_lemma1:
+     "[|x < y; 0 < x; 0 < z|] ==> x * z * inverse y < (z::rat)"
+apply (frule_tac c = "z * inverse y" in mult_strict_right_mono)
+apply (simp add: zero_less_mult_iff)
+apply (subgoal_tac "y * (z * inverse y) = z * (y * inverse y)")
+apply (simp_all add: mult_ac)
 done
 
-lemma lemma_preal_rat_less3: "x < xa ==> x*z1*qinv(xa) < z1"
-apply (drule_tac x = "z1 * qinv xa" in prat_mult_less2_mono1)
-apply (drule prat_mult_left_commute [THEN subst])
-apply (simp add: prat_mult_ac)
-done
+lemma preal_of_rat_mult_lemma2: 
+  assumes xless: "x < y * z"
+      and xpos: "0 < x"
+      and ypos: "0 < y"
+  shows "x * z * inverse y * inverse z < (z::rat)"
+proof -
+  have "0 < y * z" using prems by simp
+  hence zpos:  "0 < z" using prems by (simp add: zero_less_mult_iff)
+  have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
+    by (simp add: mult_ac)
+  also have "... = x/y" using zpos
+    by (simp add: divide_inverse_zero)
+  also have "... < z"
+    by (simp add: pos_divide_less_eq [OF ypos] mult_commute) 
+  finally show ?thesis .
+qed
 
-lemma lemma_preal_rat_less4: "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2"
-apply (drule_tac x = "z2 * qinv (z1*z2) " in prat_mult_less2_mono1)
-apply (drule prat_mult_left_commute [THEN subst])
-apply (simp add: prat_mult_ac)
+lemma preal_of_rat_mult_lemma3:
+  assumes uless: "u < x * y"
+      and "0 < x"
+      and "0 < y"
+      and "0 < u"
+  shows "\<exists>v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w"
+proof -
+  from dense [OF uless] 
+  obtain r where "u < r" "r < x * y" by blast
+  thus ?thesis
+  proof (intro exI conjI)
+  show "u * x * inverse r < x" using prems 
+    by (simp add: preal_of_rat_mult_lemma1) 
+  show "r * y * inverse x * inverse y < y" using prems
+    by (simp add: preal_of_rat_mult_lemma2)
+  show "0 < u * x * inverse r" using prems
+    by (simp add: zero_less_mult_iff) 
+  show "0 < r * y * inverse x * inverse y" using prems
+    by (simp add: zero_less_mult_iff) 
+  have "u * x * inverse r * (r * y * inverse x * inverse y) =
+        u * (r * inverse r) * (x * inverse x) * (y * inverse y)"
+    by (simp only: mult_ac)
+  thus "u = u * x * inverse r * (r * y * inverse x * inverse y)" using prems
+    by simp
+  qed
+qed
+
+lemma preal_of_rat_mult:
+     "[| 0 < x; 0 < y|] 
+      ==> preal_of_rat ((x::rat) * y) = preal_of_rat x * preal_of_rat y"
+apply (unfold preal_of_rat_def preal_mult_def)
+apply (simp add: rat_mem_preal) 
+apply (rule_tac f = Abs_preal in arg_cong)
+apply (auto simp add: zero_less_mult_iff mult_strict_mono mult_set_def) 
+apply (blast dest: preal_of_rat_mult_lemma3) 
 done
 
-lemma preal_of_prat_mult:
-      "preal_of_prat ((z1::prat) * z2) =
-       preal_of_prat z1 * preal_of_prat z2"
-apply (unfold preal_of_prat_def preal_mult_def)
-apply (rule_tac f = Abs_preal in arg_cong)
-apply (auto intro: prat_mult_less_mono 
-            simp add: lemma_prat_less_set_mem_preal [THEN Abs_preal_inverse])
-apply (drule prat_dense, safe)
-apply (rule_tac x = "x*z1*qinv (xa) " in exI, rule conjI)
-apply (erule lemma_preal_rat_less3)
-apply (rule_tac x = " xa*z2*qinv (z1*z2) " in exI, rule conjI)
-apply (erule lemma_preal_rat_less4)
-apply (simp add: qinv_mult_eq [symmetric] prat_mult_ac)
-apply (simp add: prat_mult_assoc [symmetric])
-done
+lemma preal_of_rat_less_iff:
+      "[| 0 < x; 0 < y|] ==> (preal_of_rat x < preal_of_rat y) = (x < y)"
+by (force simp add: preal_of_rat_def preal_less_def rat_mem_preal) 
 
-lemma preal_of_prat_less_iff [simp]:
-      "(preal_of_prat p < preal_of_prat q) = (p < q)"
-apply (unfold preal_of_prat_def preal_less_def)
-apply (auto dest!: lemma_prat_set_eq elim: prat_less_trans 
-        simp add: lemma_prat_less_set_mem_preal psubset_def prat_less_not_refl)
-apply (rule_tac x = p and y = q in prat_linear_less2)
-apply (auto intro: prat_less_irrefl)
-done
+lemma preal_of_rat_le_iff:
+      "[| 0 < x; 0 < y|] ==> (preal_of_rat x \<le> preal_of_rat y) = (x \<le> y)"
+by (simp add: preal_of_rat_less_iff linorder_not_less [symmetric]) 
+
+lemma preal_of_rat_eq_iff:
+      "[| 0 < x; 0 < y|] ==> (preal_of_rat x = preal_of_rat y) = (x = y)"
+by (simp add: preal_of_rat_le_iff order_eq_iff) 
 
 
 ML
 {*
 val inj_on_Abs_preal = thm"inj_on_Abs_preal";
 val inj_Rep_preal = thm"inj_Rep_preal";
-val empty_not_mem_preal = thm"empty_not_mem_preal";
-val one_set_mem_preal = thm"one_set_mem_preal";
-val preal_psubset_empty = thm"preal_psubset_empty";
 val mem_Rep_preal_Ex = thm"mem_Rep_preal_Ex";
-val inj_preal_of_prat = thm"inj_preal_of_prat";
-val not_in_preal_ub = thm"not_in_preal_ub";
-val preal_less_not_refl = thm"preal_less_not_refl";
-val preal_less_trans = thm"preal_less_trans";
-val preal_less_not_sym = thm"preal_less_not_sym";
-val preal_linear = thm"preal_linear";
 val preal_add_commute = thm"preal_add_commute";
-val preal_add_set_not_empty = thm"preal_add_set_not_empty";
-val preal_not_mem_add_set_Ex = thm"preal_not_mem_add_set_Ex";
-val preal_add_set_not_prat_set = thm"preal_add_set_not_prat_set";
-val preal_mem_add_set = thm"preal_mem_add_set";
 val preal_add_assoc = thm"preal_add_assoc";
 val preal_add_left_commute = thm"preal_add_left_commute";
 val preal_mult_commute = thm"preal_mult_commute";
-val preal_mult_set_not_empty = thm"preal_mult_set_not_empty";
-val preal_not_mem_mult_set_Ex = thm"preal_not_mem_mult_set_Ex";
-val preal_mult_set_not_prat_set = thm"preal_mult_set_not_prat_set";
-val preal_mem_mult_set = thm"preal_mem_mult_set";
 val preal_mult_assoc = thm"preal_mult_assoc";
 val preal_mult_left_commute = thm"preal_mult_left_commute";
-val preal_mult_1 = thm"preal_mult_1";
-val preal_mult_1_right = thm"preal_mult_1_right";
-val mem_Rep_preal_addD = thm"mem_Rep_preal_addD";
-val mem_Rep_preal_addI = thm"mem_Rep_preal_addI";
-val mem_Rep_preal_add_iff = thm"mem_Rep_preal_add_iff";
-val mem_Rep_preal_multD = thm"mem_Rep_preal_multD";
-val mem_Rep_preal_multI = thm"mem_Rep_preal_multI";
-val mem_Rep_preal_mult_iff = thm"mem_Rep_preal_mult_iff";
 val preal_add_mult_distrib2 = thm"preal_add_mult_distrib2";
 val preal_add_mult_distrib = thm"preal_add_mult_distrib";
-val qinv_not_mem_Rep_preal_Ex = thm"qinv_not_mem_Rep_preal_Ex";
-val preal_inv_set_not_empty = thm"preal_inv_set_not_empty";
-val qinv_mem_Rep_preal_Ex = thm"qinv_mem_Rep_preal_Ex";
-val preal_not_mem_inv_set_Ex = thm"preal_not_mem_inv_set_Ex";
-val preal_inv_set_not_prat_set = thm"preal_inv_set_not_prat_set";
-val preal_mem_inv_set = thm"preal_mem_inv_set";
-val preal_mem_mult_invD = thm"preal_mem_mult_invD";
-val preal_mem_mult_invI = thm"preal_mem_mult_invI";
-val preal_mult_inv = thm"preal_mult_inv";
-val preal_mult_inv_right = thm"preal_mult_inv_right";
-val Rep_preal_self_subset = thm"Rep_preal_self_subset";
-val Rep_preal_sum_not_subset = thm"Rep_preal_sum_not_subset";
-val Rep_preal_sum_not_eq = thm"Rep_preal_sum_not_eq";
 val preal_self_less_add_left = thm"preal_self_less_add_left";
 val preal_self_less_add_right = thm"preal_self_less_add_right";
-val preal_less_le_iff = thm"preal_less_le_iff";
-val preal_le_refl = thm"preal_le_refl";
-val preal_le_trans = thm"preal_le_trans";
-val preal_le_anti_sym = thm"preal_le_anti_sym";
-val preal_neq_iff = thm"preal_neq_iff";
-val preal_less_le = thm"preal_less_le";
-val psubset_trans = thm"psubset_trans";
-val preal_less_set_not_empty = thm"preal_less_set_not_empty";
-val preal_less_set_not_prat_set = thm"preal_less_set_not_prat_set";
-val preal_mem_less_set = thm"preal_mem_less_set";
-val preal_less_add_left_subsetI = thm"preal_less_add_left_subsetI";
-val preal_less_add_left_subsetI2 = thm"preal_less_add_left_subsetI2";
-val preal_less_add_left = thm"preal_less_add_left";
-val preal_less_add_left_Ex = thm"preal_less_add_left_Ex";
+val less_add_left = thm"less_add_left";
 val preal_add_less2_mono1 = thm"preal_add_less2_mono1";
 val preal_add_less2_mono2 = thm"preal_add_less2_mono2";
-val preal_mult_less_mono1 = thm"preal_mult_less_mono1";
-val preal_mult_left_less_mono1 = thm"preal_mult_left_less_mono1";
-val preal_mult_left_le_mono1 = thm"preal_mult_left_le_mono1";
-val preal_mult_le_mono1 = thm"preal_mult_le_mono1";
-val preal_add_left_le_mono1 = thm"preal_add_left_le_mono1";
-val preal_add_le_mono1 = thm"preal_add_le_mono1";
 val preal_add_right_less_cancel = thm"preal_add_right_less_cancel";
 val preal_add_left_less_cancel = thm"preal_add_left_less_cancel";
-val preal_add_less_iff1 = thm"preal_add_less_iff1";
-val preal_add_less_iff2 = thm"preal_add_less_iff2";
-val preal_add_less_mono = thm"preal_add_less_mono";
-val preal_mult_less_mono = thm"preal_mult_less_mono";
 val preal_add_right_cancel = thm"preal_add_right_cancel";
 val preal_add_left_cancel = thm"preal_add_left_cancel";
 val preal_add_left_cancel_iff = thm"preal_add_left_cancel_iff";
 val preal_add_right_cancel_iff = thm"preal_add_right_cancel_iff";
-val preal_sup_mem_Ex = thm"preal_sup_mem_Ex";
-val preal_sup_set_not_empty = thm"preal_sup_set_not_empty";
-val preal_sup_not_mem_Ex = thm"preal_sup_not_mem_Ex";
-val preal_sup_not_mem_Ex1 = thm"preal_sup_not_mem_Ex1";
-val preal_sup_set_not_prat_set = thm"preal_sup_set_not_prat_set";
-val preal_sup_set_not_prat_set1 = thm"preal_sup_set_not_prat_set1";
-val preal_sup = thm"preal_sup";
-val preal_sup1 = thm"preal_sup1";
-val preal_psup_leI = thm"preal_psup_leI";
-val preal_psup_leI2 = thm"preal_psup_leI2";
-val preal_psup_leI2b = thm"preal_psup_leI2b";
-val preal_psup_leI2a = thm"preal_psup_leI2a";
+val preal_psup_le = thm"preal_psup_le";
 val psup_le_ub = thm"psup_le_ub";
-val psup_le_ub1 = thm"psup_le_ub1";
 val preal_complete = thm"preal_complete";
-val preal_of_prat_add = thm"preal_of_prat_add";
-val preal_of_prat_mult = thm"preal_of_prat_mult";
+val preal_of_rat_add = thm"preal_of_rat_add";
+val preal_of_rat_mult = thm"preal_of_rat_mult";
 
 val preal_add_ac = thms"preal_add_ac";
 val preal_mult_ac = thms"preal_mult_ac";