move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings

--- a/src/HOL/Lubs.thy	Tue Mar 26 12:20:53 2013 +0100
+++ b/src/HOL/Lubs.thy	Tue Mar 26 12:20:54 2013 +0100
@@ -94,4 +94,10 @@
 lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
   unfolding ubs_def isLub_def by (rule leastPD2)
 
+lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
+  apply (frule isLub_isUb)
+  apply (frule_tac x = y in isLub_isUb)
+  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
+  done
+
 end

--- a/src/HOL/RComplete.thy	Tue Mar 26 12:20:53 2013 +0100
+++ b/src/HOL/RComplete.thy	Tue Mar 26 12:20:54 2013 +0100
@@ -8,29 +8,15 @@
 header {* Completeness of the Reals; Floor and Ceiling Functions *}
 
 theory RComplete
-imports Conditional_Complete_Lattices RealDef
+imports RealDef
 begin
 
-lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
-  by simp
-
-lemma abs_diff_less_iff:
-  "(\<bar>x - a\<bar> < (r::'a::linordered_idom)) = (a - r < x \<and> x < a + r)"
-  by auto
-
 subsection {* Completeness of Positive Reals *}
 
 text {*
   \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
 *}
 
-lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"
-  apply (frule isLub_isUb)
-  apply (frule_tac x = y in isLub_isUb)
-  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
-  done
-
-
 text {*
   \medskip reals Completeness (again!)
 *}

--- a/src/HOL/RealDef.thy	Tue Mar 26 12:20:53 2013 +0100
+++ b/src/HOL/RealDef.thy	Tue Mar 26 12:20:54 2013 +0100
@@ -1,7 +1,6 @@
 (*  Title       : HOL/RealDef.thy
     Author      : Jacques D. Fleuriot, 1998
     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
-    Additional contributions by Jeremy Avigad
     Construction of Cauchy Reals by Brian Huffman, 2010
 *)
 
@@ -1553,6 +1552,8 @@
 lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
   by auto
 
+lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
+  by simp
 
 subsection{*Absolute Value Function for the Reals*}
 

--- a/src/HOL/Rings.thy	Tue Mar 26 12:20:53 2013 +0100
+++ b/src/HOL/Rings.thy	Tue Mar 26 12:20:54 2013 +0100
@@ -1143,6 +1143,10 @@
   "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
   by (simp add: abs_mult)
 
+lemma abs_diff_less_iff:
+  "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
+  by (auto simp add: diff_less_eq ac_simps abs_less_iff)
+
 end
 
 code_modulename SML