# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1556391638 -3600
# Node ID 2e496190039d62b49bab8931ff4a2d65908710be
# Parent  81c1d043c2300f2bee27586a49ce69d7be53d5ba
some variable renaming

diff -r 81c1d043c230 -r 2e496190039d src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Sat Apr 27 18:54:32 2019 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Sat Apr 27 20:00:38 2019 +0100
@@ -73,29 +73,29 @@
 
 definition
   preal_less_def:
-    "R < S \<equiv> Rep_preal R < Rep_preal S"
+    "r < s \<equiv> Rep_preal r < Rep_preal s"
 
 definition
   preal_le_def:
-    "R \<le> S \<equiv> Rep_preal R \<subseteq> Rep_preal S"
+    "r \<le> s \<equiv> Rep_preal r \<subseteq> Rep_preal s"
 
 definition
   preal_add_def:
-    "R + S \<equiv> Abs_preal (add_set (Rep_preal R) (Rep_preal S))"
+    "r + s \<equiv> Abs_preal (add_set (Rep_preal r) (Rep_preal s))"
 
 definition
   preal_diff_def:
-    "R - S \<equiv> Abs_preal (diff_set (Rep_preal R) (Rep_preal S))"
+    "r - s \<equiv> Abs_preal (diff_set (Rep_preal r) (Rep_preal s))"
 
 definition
   preal_mult_def:
-    "R * S \<equiv> Abs_preal (mult_set (Rep_preal R) (Rep_preal S))"
+    "r * s \<equiv> Abs_preal (mult_set (Rep_preal r) (Rep_preal s))"
 
 definition
   preal_inverse_def:
-    "inverse R \<equiv> Abs_preal (inverse_set (Rep_preal R))"
+    "inverse r \<equiv> Abs_preal (inverse_set (Rep_preal r))"
 
-definition "R div S = R * inverse (S::preal)"
+definition "r div s = r * inverse (s::preal)"
 
 definition
   preal_one_def:
@@ -283,7 +283,7 @@
 qed
 
 lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
-  apply (simp add: preal_add_def mem_add_set cut_Rep_preal)
+  apply (simp add: preal_add_def mem_add_set)
   apply (force simp: add_set_def ac_simps)
   done
 
@@ -433,13 +433,13 @@
 subsection\<open>Distribution of Multiplication across Addition\<close>
 
 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)"
+  "(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)"
+  "(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
@@ -666,7 +666,7 @@
 subsection\<open>Existence of Inverse: Part 2\<close>
 
 lemma mem_Rep_preal_inverse_iff:
-  "(z \<in> Rep_preal(inverse R)) \<longleftrightarrow> (0 < z \<and> (\<exists>y. z < y \<and> inverse y \<notin> Rep_preal R))"
+  "(z \<in> Rep_preal(inverse r)) \<longleftrightarrow> (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
@@ -677,24 +677,24 @@
 
 lemma subset_inverse_mult_lemma:
   assumes xpos: "0 < x" and xless: "x < 1"
-  shows "\<exists>r u y. 0 < r \<and> r < y \<and> inverse y \<notin> Rep_preal R \<and> 
-    u \<in> Rep_preal R \<and> x = r * u"
+  shows "\<exists>v u y. 0 < v \<and> v < y \<and> inverse y \<notin> Rep_preal R \<and> 
+    u \<in> Rep_preal R \<and> x = v * u"
 proof -
   from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff)
   from lemma_gleason9_36 [OF cut_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 cut_Rep_preal r])
-  from preal_exists_greater [OF cut_Rep_preal r]
-  obtain u where u: "u \<in> Rep_preal R" and rless: "r < u" ..
+  obtain t where t: "t \<in> Rep_preal R" 
+             and notin: "t * (inverse x) \<notin> Rep_preal R" ..
+  have rpos: "0<t" by (rule preal_imp_pos [OF cut_Rep_preal t])
+  from preal_exists_greater [OF cut_Rep_preal t]
+  obtain u where u: "u \<in> Rep_preal R" and rless: "t < u" ..
   have upos: "0<u" by (rule preal_imp_pos [OF cut_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
+    show "x/u < x/t" using xpos upos rpos
       by (simp add: divide_inverse mult_less_cancel_left rless) 
-    show "inverse (x / r) \<notin> Rep_preal R" using notin
+    show "inverse (x / t) \<notin> Rep_preal R" using notin
       by (simp add: divide_inverse mult.commute) 
     show "u \<in> Rep_preal R" by (rule u) 
     show "x = x / u * u" using upos 
@@ -703,20 +703,20 @@
 qed
 
 lemma subset_inverse_mult: 
-     "Rep_preal 1 \<subseteq> Rep_preal(inverse R * R)"
+     "Rep_preal 1 \<subseteq> Rep_preal(inverse r * r)"
   by (force simp: Rep_preal_one mem_Rep_preal_inverse_iff mem_Rep_preal_mult_iff dest: subset_inverse_mult_lemma)
 
-lemma inverse_mult_subset: "Rep_preal(inverse R * R) \<subseteq> Rep_preal 1"
+lemma inverse_mult_subset: "Rep_preal(inverse r * r) \<subseteq> Rep_preal 1"
   proof -
-  have "0 < u * v" if "v \<in> Rep_preal R" "0 < u" "u < r" for u v r :: rat
+  have "0 < u * v" if "v \<in> Rep_preal r" "0 < u" "u < t" for u v t :: rat
     using that by (simp add: zero_less_mult_iff preal_imp_pos [OF cut_Rep_preal]) 
-  moreover have "r * q < 1"
-    if "q \<in> Rep_preal R" "0 < r" "r < y" "inverse y \<notin> Rep_preal R"
-    for r q y :: rat
+  moreover have "t * q < 1"
+    if "q \<in> Rep_preal r" "0 < t" "t < y" "inverse y \<notin> Rep_preal r"
+    for t q y :: rat
   proof -
     have "q < inverse y"
       using not_in_Rep_preal_ub that by auto 
-    hence "r * q < r/y" 
+    hence "t * q < t/y" 
       using that by (simp add: divide_inverse mult_less_cancel_left)
     also have "\<dots> \<le> 1" 
       using that by (simp add: pos_divide_le_eq)
@@ -726,77 +726,77 @@
     by (auto simp: Rep_preal_one mem_Rep_preal_inverse_iff mem_Rep_preal_mult_iff)
 qed 
 
-lemma preal_mult_inverse: "inverse R * R = (1::preal)"
+lemma preal_mult_inverse: "inverse r * r = (1::preal)"
   by (meson Rep_preal_inject inverse_mult_subset subset_antisym subset_inverse_mult)
 
-lemma preal_mult_inverse_right: "R * inverse R = (1::preal)"
+lemma preal_mult_inverse_right: "r * inverse r = (1::preal)"
   using preal_mult_commute preal_mult_inverse by auto
 
 
 text\<open>Theorems needing \<open>Gleason9_34\<close>\<close>
 
-lemma Rep_preal_self_subset: "Rep_preal (R) \<subseteq> Rep_preal(R + S)"
+lemma Rep_preal_self_subset: "Rep_preal (r) \<subseteq> Rep_preal(r + s)"
 proof 
-  fix r
-  assume r: "r \<in> Rep_preal R"
-  obtain y where y: "y \<in> Rep_preal S" and "y > 0"
+  fix x
+  assume x: "x \<in> Rep_preal r"
+  obtain y where y: "y \<in> Rep_preal s" and "y > 0"
     using Rep_preal preal_nonempty by blast
-  have ry: "r+y \<in> Rep_preal(R + S)" using r y
+  have ry: "x+y \<in> Rep_preal(r + s)" using x y
     by (auto simp: mem_Rep_preal_add_iff)
-  then show "r \<in> Rep_preal(R + S)"
-    by (meson \<open>0 < y\<close> add_less_same_cancel1 not_in_Rep_preal_ub order.asym preal_imp_pos [OF cut_Rep_preal r])
+  then show "x \<in> Rep_preal(r + s)"
+    by (meson \<open>0 < y\<close> add_less_same_cancel1 not_in_Rep_preal_ub order.asym preal_imp_pos [OF cut_Rep_preal x])
 qed
 
-lemma Rep_preal_sum_not_subset: "~ Rep_preal (R + S) \<subseteq> Rep_preal(R)"
+lemma Rep_preal_sum_not_subset: "~ Rep_preal (r + s) \<subseteq> Rep_preal(r)"
 proof -
-  obtain y where y: "y \<in> Rep_preal S" and "y > 0"
+  obtain y where y: "y \<in> Rep_preal s" and "y > 0"
     using Rep_preal preal_nonempty by blast
-  obtain r where r: "r \<in> Rep_preal R" and notin: "r + y \<notin> Rep_preal R"
+  obtain x where "x \<in> Rep_preal r" and notin: "x + y \<notin> Rep_preal r"
     using Dedekind_Real.Rep_preal Gleason9_34 \<open>0 < y\<close> by blast 
-  have "r + y \<in> Rep_preal (R + S)" using r y
+  then have "x + y \<in> Rep_preal (r + s)" using y
     by (auto simp: mem_Rep_preal_add_iff)
   thus ?thesis using notin by blast
 qed
 
 text\<open>at last, Gleason prop. 9-3.5(iii) page 123\<close>
-proposition preal_self_less_add_left: "(R::preal) < R + S"
+proposition preal_self_less_add_left: "(r::preal) < r + s"
   by (meson Rep_preal_sum_not_subset not_less preal_le_def)
 
 
 subsection\<open>Subtraction for Positive Reals\<close>
 
-text\<open>Gleason prop. 9-3.5(iv), page 123: proving \<^prop>\<open>A < B \<Longrightarrow> \<exists>D. A + D = B\<close>. 
+text\<open>gleason prop. 9-3.5(iv), page 123: proving \<^prop>\<open>a < b \<Longrightarrow> \<exists>d. a + d = b\<close>. 
 We define the claimed \<^term>\<open>D\<close> and show that it is a positive real\<close>
 
 lemma mem_diff_set:
-  assumes "R < S"
-  shows "cut (diff_set (Rep_preal S) (Rep_preal R))"
+  assumes "r < s"
+  shows "cut (diff_set (Rep_preal s) (Rep_preal r))"
 proof -
-  obtain p where "Rep_preal R \<subseteq> Rep_preal S" "p \<in> Rep_preal S" "p \<notin> Rep_preal R"
+  obtain p where "Rep_preal r \<subseteq> Rep_preal s" "p \<in> Rep_preal s" "p \<notin> Rep_preal r"
     using assms unfolding preal_less_def by auto
-  then have "{} \<subset> diff_set (Rep_preal S) (Rep_preal R)"
+  then have "{} \<subset> diff_set (Rep_preal s) (Rep_preal r)"
     apply (simp add: diff_set_def psubset_eq)
     by (metis cut_Rep_preal add_eq_exists less_add_same_cancel1 preal_exists_greater preal_imp_pos)
   moreover
-  obtain q where "q > 0" "q \<notin> Rep_preal S"
+  obtain q where "q > 0" "q \<notin> Rep_preal s"
     using Rep_preal_exists_bound by blast
-  then have qnot: "q \<notin> diff_set (Rep_preal S) (Rep_preal R)"
+  then have qnot: "q \<notin> diff_set (Rep_preal s) (Rep_preal r)"
     by (auto simp: diff_set_def dest: cut_Rep_preal [THEN preal_downwards_closed])
-  moreover have "diff_set (Rep_preal S) (Rep_preal R) \<subset> {0<..}" (is "?lhs < ?rhs")
+  moreover have "diff_set (Rep_preal s) (Rep_preal r) \<subset> {0<..}" (is "?lhs < ?rhs")
     using \<open>0 < q\<close> diff_set_def qnot by blast
-  moreover have "z \<in> diff_set (Rep_preal S) (Rep_preal R)"
-    if u: "u \<in> diff_set (Rep_preal S) (Rep_preal R)" and "0 < z" "z < u" for u z
+  moreover have "z \<in> diff_set (Rep_preal s) (Rep_preal r)"
+    if u: "u \<in> diff_set (Rep_preal s) (Rep_preal r)" and "0 < z" "z < u" for u z
     using u that less_trans Rep_preal unfolding diff_set_def Dedekind_Real.cut_def by auto
-  moreover have "\<exists>u \<in> diff_set (Rep_preal S) (Rep_preal R). y < u"
-    if y: "y \<in> diff_set (Rep_preal S) (Rep_preal R)" for y
+  moreover have "\<exists>u \<in> diff_set (Rep_preal s) (Rep_preal r). y < u"
+    if y: "y \<in> diff_set (Rep_preal s) (Rep_preal r)" for y
   proof -
-    obtain a b where "0 < a" "0 < b" "a \<notin> Rep_preal R" "a + y + b \<in> Rep_preal S"
+    obtain a b where "0 < a" "0 < b" "a \<notin> Rep_preal r" "a + y + b \<in> Rep_preal s"
       using y
       by (simp add: diff_set_def) (metis cut_Rep_preal add_eq_exists less_add_same_cancel1 preal_exists_greater) 
-    then have "a + (y + b) \<in> Rep_preal S"
+    then have "a + (y + b) \<in> Rep_preal s"
       by (simp add: add.assoc)
-    then have "y + b \<in> diff_set (Rep_preal S) (Rep_preal R)"
-      using \<open>0 < a\<close> \<open>0 < b\<close> \<open>a \<notin> Rep_preal R\<close> y
+    then have "y + b \<in> diff_set (Rep_preal s) (Rep_preal r)"
+      using \<open>0 < a\<close> \<open>0 < b\<close> \<open>a \<notin> Rep_preal r\<close> y
       by (auto simp: diff_set_def)
     then show ?thesis
       using \<open>0 < b\<close> less_add_same_cancel1 by blast
@@ -806,88 +806,88 @@
 qed
 
 lemma mem_Rep_preal_diff_iff:
-  "R < S \<Longrightarrow>
-       (z \<in> Rep_preal (S - R)) \<longleftrightarrow> 
-       (\<exists>x. 0 < x \<and> 0 < z \<and> x \<notin> Rep_preal R \<and> x + z \<in> Rep_preal S)"
+  "r < s \<Longrightarrow>
+       (z \<in> Rep_preal (s - r)) \<longleftrightarrow> 
+       (\<exists>x. 0 < x \<and> 0 < z \<and> x \<notin> Rep_preal r \<and> x + z \<in> Rep_preal s)"
   apply (simp add: preal_diff_def mem_diff_set Rep_preal)
   apply (force simp: diff_set_def) 
   done
 
 proposition less_add_left:
-  fixes R::preal 
-  assumes "R < S"
-  shows "R + (S-R) = S"
+  fixes r::preal 
+  assumes "r < s"
+  shows "r + (s-r) = s"
 proof -
-  have "a + b \<in> Rep_preal S"
-    if "a \<in> Rep_preal R" "c + b \<in> Rep_preal S" "c \<notin> Rep_preal R"
+  have "a + b \<in> Rep_preal s"
+    if "a \<in> Rep_preal r" "c + b \<in> Rep_preal s" "c \<notin> Rep_preal r"
     and "0 < b" "0 < c" for a b c
     by (meson cut_Rep_preal add_less_imp_less_right add_pos_pos not_in_Rep_preal_ub preal_downwards_closed preal_imp_pos that)
-  then have "R + (S-R) \<le> S"
+  then have "r + (s-r) \<le> s"
     using assms mem_Rep_preal_add_iff mem_Rep_preal_diff_iff preal_le_def by auto
-  have "x \<in> Rep_preal (R + (S - R))" if "x \<in> Rep_preal S" for x
-  proof (cases "x \<in> Rep_preal R")
+  have "x \<in> Rep_preal (r + (s - r))" if "x \<in> Rep_preal s" for x
+  proof (cases "x \<in> Rep_preal r")
     case True
     then show ?thesis
       using Rep_preal_self_subset by blast
   next
     case False
-    have "\<exists>u v z. 0 < v \<and> 0 < z \<and> u \<in> Rep_preal R \<and> z \<notin> Rep_preal R \<and> z + v \<in> Rep_preal S \<and> x = u + v"
-      if x: "x \<in> Rep_preal S"
+    have "\<exists>u v z. 0 < v \<and> 0 < z \<and> u \<in> Rep_preal r \<and> z \<notin> Rep_preal r \<and> z + v \<in> Rep_preal s \<and> x = u + v"
+      if x: "x \<in> Rep_preal s"
     proof -
       have xpos: "x > 0"
         using Rep_preal preal_imp_pos that by blast 
-      obtain e where epos: "0 < e" and xe: "x + e \<in> Rep_preal S"
+      obtain e where epos: "0 < e" and xe: "x + e \<in> Rep_preal s"
         by (metis cut_Rep_preal x add_eq_exists less_add_same_cancel1 preal_exists_greater)
       from  Gleason9_34 [OF cut_Rep_preal epos]
-      obtain r where r: "r \<in> Rep_preal R" and notin: "r + e \<notin> Rep_preal R" ..
-      with x False 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
+      obtain u where r: "u \<in> Rep_preal r" and notin: "u + e \<notin> Rep_preal r" ..
+      with x False xpos have rless: "u < x" by (blast intro: not_in_Rep_preal_ub)
+      from add_eq_exists [of u x]
+      obtain y where eq: "x = u+y" by auto
       show ?thesis 
       proof (intro exI conjI)
-        show "r + e \<notin> Rep_preal R" by (rule notin)
-        show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: ac_simps)
-        show "0 < r + e" 
+        show "u + e \<notin> Rep_preal r" by (rule notin)
+        show "u + e + y \<in> Rep_preal s" using xe eq by (simp add: ac_simps)
+        show "0 < u + e" 
           using epos preal_imp_pos [OF cut_Rep_preal r] by simp
       qed (use r rless eq in auto)
     qed
     then show ?thesis
       using assms mem_Rep_preal_add_iff mem_Rep_preal_diff_iff that by blast
   qed
-  then have "S \<le> R + (S-R)"
+  then have "s \<le> r + (s-r)"
     by (auto simp: preal_le_def)
   then show ?thesis
-    by (simp add: \<open>R + (S - R) \<le> S\<close> antisym)
+    by (simp add: \<open>r + (s - r) \<le> s\<close> antisym)
 qed
 
-lemma preal_add_less2_mono1: "R < (S::preal) \<Longrightarrow> R + T < S + T"
+lemma preal_add_less2_mono1: "r < (s::preal) \<Longrightarrow> r + t < s + t"
   by (metis add.assoc add.commute less_add_left preal_self_less_add_left)
 
-lemma preal_add_less2_mono2: "R < (S::preal) \<Longrightarrow> T + R < T + S"
-  by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of T])
+lemma preal_add_less2_mono2: "r < (s::preal) \<Longrightarrow> t + r < t + s"
+  by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of t])
 
-lemma preal_add_right_less_cancel: "R + T < S + T \<Longrightarrow> R < (S::preal)"
+lemma preal_add_right_less_cancel: "r + t < s + t \<Longrightarrow> r < (s::preal)"
   by (metis linorder_cases order.asym preal_add_less2_mono1)
 
-lemma preal_add_left_less_cancel: "T + R < T + S \<Longrightarrow> R < (S::preal)"
-  by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T])
+lemma preal_add_left_less_cancel: "t + r < t + s \<Longrightarrow> r < (s::preal)"
+  by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of t])
 
-lemma preal_add_less_cancel_left [simp]: "(T + (R::preal) < T + S) \<longleftrightarrow> (R < S)"
+lemma preal_add_less_cancel_left [simp]: "(t + (r::preal) < t + s) \<longleftrightarrow> (r < s)"
   by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
 
-lemma preal_add_less_cancel_right [simp]: "((R::preal) + T < S + T) = (R < S)"
-  using preal_add_less_cancel_left [symmetric, of R S T] by (simp add: ac_simps)
+lemma preal_add_less_cancel_right [simp]: "((r::preal) + t < s + t) = (r < s)"
+  using preal_add_less_cancel_left [symmetric, of r s t] by (simp add: ac_simps)
 
-lemma preal_add_le_cancel_left [simp]: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
+lemma preal_add_le_cancel_left [simp]: "(t + (r::preal) \<le> t + s) = (r \<le> s)"
   by (simp add: linorder_not_less [symmetric]) 
 
-lemma preal_add_le_cancel_right [simp]: "((R::preal) + T \<le> S + T) = (R \<le> S)"
-  using preal_add_le_cancel_left [symmetric, of R S T] by (simp add: ac_simps)
+lemma preal_add_le_cancel_right [simp]: "((r::preal) + t \<le> s + t) = (r \<le> s)"
+  using preal_add_le_cancel_left [symmetric, of r s t] by (simp add: ac_simps)
 
-lemma preal_add_right_cancel: "(R::preal) + T = S + T \<Longrightarrow> R = S"
+lemma preal_add_right_cancel: "(r::preal) + t = s + t \<Longrightarrow> r = s"
   by (metis less_irrefl linorder_cases preal_add_less_cancel_right)
 
-lemma preal_add_left_cancel: "C + A = C + B \<Longrightarrow> A = (B::preal)"
+lemma preal_add_left_cancel: "c + a = c + b \<Longrightarrow> a = (b::preal)"
   by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
 
 instance preal :: linordered_ab_semigroup_add
@@ -991,10 +991,10 @@
                  { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
 
 definition
-  real_inverse_def: "inverse (R::real) = (THE S. (R = 0 \<and> S = 0) \<or> S * R = 1)"
+  real_inverse_def: "inverse (r::real) = (THE s. (r = 0 \<and> s = 0) \<or> s * r = 1)"
 
 definition
-  real_divide_def: "R div (S::real) = R * inverse S"
+  real_divide_def: "r div (s::real) = r * inverse s"
 
 definition
   real_le_def: "z \<le> (w::real) \<longleftrightarrow>
@@ -1172,7 +1172,7 @@
 proof -
   obtain y where "y*x = 1"
     using assms real_mult_inverse_left_ex by blast
-  then have "(THE S. S * x = 1) * x = 1"
+  then have "(THE s. s * x = 1) * x = 1"
   proof (rule theI)
     show "y' = y" if "y' * x = 1" for y'
       by (metis \<open>y * x = 1\<close> mult.left_commute mult.right_neutral that) 
@@ -1285,12 +1285,11 @@
     by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"])
 qed
 
+lemma real_sum_gt_zero_less: "(0 < s + (-w::real)) \<Longrightarrow> (w < s)"
+  by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of s])
 
-lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) \<Longrightarrow> (W < S)"
-  by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S])
-
-lemma real_less_sum_gt_zero: "(W < S) \<Longrightarrow> (0 < S + (-W::real))"
-  by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S])
+lemma real_less_sum_gt_zero: "(w < s) \<Longrightarrow> (0 < s + (-w::real))"
+  by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of s])
 
 lemma real_mult_order: 
   fixes x y::real
@@ -1404,7 +1403,7 @@
   assumes positive_P: "\<forall>x \<in> P. (0::real) < x"
     and not_empty_P: "\<exists>x. x \<in> P"
     and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
-  shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
+  shows "\<exists>s. \<forall>y. (\<exists>x \<in> P. y < x) = (y < s)"
 proof (rule exI, rule allI)
   fix y
   let ?pP = "{w. real_of_preal w \<in> P}"