# HG changeset patch
# User huffman
# Date 1181178691 -7200
# Node ID 063039db59ddedb66299572cc62ec0e5fc1d1608
# Parent  85e7e043b980c6cd885e334a35195d8f7b8e246f
define (1::preal); clean up instance declarations

diff -r 85e7e043b980 -r 063039db59dd src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Thu Jun 07 02:34:37 2007 +0200
+++ b/src/HOL/Real/PReal.thy	Thu Jun 07 03:11:31 2007 +0200
@@ -53,7 +53,7 @@
 typedef preal = "{A. cut A}"
   by (blast intro: cut_of_rat [OF zero_less_one])
 
-instance preal :: "{ord, plus, minus, times, inverse}" ..
+instance preal :: "{ord, plus, minus, times, inverse, one}" ..
 
 definition
   preal_of_rat :: "rat => preal" where
@@ -100,6 +100,9 @@
   preal_inverse_def:
     "inverse R == Abs_preal (inverse_set (Rep_preal R))"
 
+  preal_one_def:
+    "1 == preal_of_rat 1"
+
 
 text{*Reduces equality on abstractions to equality on representatives*}
 declare Abs_preal_inject [simp]
@@ -334,11 +337,15 @@
 apply (force simp add: add_set_def add_ac)
 done
 
+instance preal :: ab_semigroup_add
+proof
+  fix a b c :: preal
+  show "(a + b) + c = a + (b + c)" by (rule preal_add_assoc)
+  show "a + b = b + a" by (rule preal_add_commute)
+qed
+
 lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
-  apply (rule mk_left_commute [of "op +"])
-  apply (rule preal_add_assoc)
-  apply (rule preal_add_commute)
-  done
+by (rule add_left_commute)
 
 text{* Positive Real addition is an AC operator *}
 lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
@@ -465,11 +472,15 @@
 apply (force simp add: mult_set_def mult_ac)
 done
 
+instance preal :: ab_semigroup_mult
+proof
+  fix a b c :: preal
+  show "(a * b) * c = a * (b * c)" by (rule preal_mult_assoc)
+  show "a * b = b * a" by (rule preal_mult_commute)
+qed
+
 lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
-  apply (rule mk_left_commute [of "op *"])
-  apply (rule preal_mult_assoc)
-  apply (rule preal_mult_commute)
-  done
+by (rule mult_left_commute)
 
 
 text{* Positive Real multiplication is an AC operator *}
@@ -479,7 +490,8 @@
 
 text{* Positive real 1 is the multiplicative identity element *}
 
-lemma preal_mult_1: "(preal_of_rat 1) * z = z"
+lemma preal_mult_1: "(1::preal) * z = z"
+unfolding preal_one_def
 proof (induct z)
   fix A :: "rat set"
   assume A: "A \<in> preal"
@@ -525,11 +537,11 @@
                   rat_mem_preal A)
 qed
 
+instance preal :: comm_monoid_mult
+by intro_classes (rule preal_mult_1)
 
-lemma preal_mult_1_right: "z * (preal_of_rat 1) = z"
-apply (rule preal_mult_commute [THEN subst])
-apply (rule preal_mult_1)
-done
+lemma preal_mult_1_right: "z * (1::preal) = z"
+by (rule mult_1_right)
 
 
 subsection{*Distribution of Multiplication across Addition*}
@@ -596,6 +608,9 @@
 lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)"
 by (simp add: preal_mult_commute preal_add_mult_distrib2)
 
+instance preal :: comm_semiring
+by intro_classes (rule preal_add_mult_distrib)
+
 
 subsection{*Existence of Inverse, a Positive Real*}
 
@@ -875,12 +890,13 @@
 apply (blast intro: inverse_mult_subset_lemma) 
 done
 
-lemma preal_mult_inverse: "inverse R * R = (preal_of_rat 1)"
+lemma preal_mult_inverse: "inverse R * R = (1::preal)"
+unfolding preal_one_def
 apply (rule Rep_preal_inject [THEN iffD1])
 apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) 
 done
 
-lemma preal_mult_inverse_right: "R * inverse R = (preal_of_rat 1)"
+lemma preal_mult_inverse_right: "R * inverse R = (1::preal)"
 apply (rule preal_mult_commute [THEN subst])
 apply (rule preal_mult_inverse)
 done
@@ -1131,11 +1147,8 @@
 instance preal :: ordered_cancel_ab_semigroup_add
 proof
   fix a b c :: preal
-  show "a + b + c = a + (b + c)" by (rule preal_add_assoc)
-  show "a + b = b + a" by (rule preal_add_commute)
   show "a + b = a + c \<Longrightarrow> b = c" by (rule preal_add_left_cancel)
-  show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
-    by (simp only: preal_add_le_cancel_left)
+  show "a \<le> b \<Longrightarrow> c + a \<le> c + b" by (simp only: preal_add_le_cancel_left)
 qed
 
 
diff -r 85e7e043b980 -r 063039db59dd src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Thu Jun 07 02:34:37 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Thu Jun 07 03:11:31 2007 +0200
@@ -37,12 +37,10 @@
 defs (overloaded)
 
   real_zero_def:
-  "0 == Abs_Real(realrel``{(preal_of_rat 1, preal_of_rat 1)})"
+  "0 == Abs_Real(realrel``{(1, 1)})"
 
   real_one_def:
-  "1 == Abs_Real(realrel``
-               {(preal_of_rat 1 + preal_of_rat 1,
-		 preal_of_rat 1)})"
+  "1 == Abs_Real(realrel``{(1 + 1, 1)})"
 
   real_minus_def:
   "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
@@ -61,7 +59,7 @@
 		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
 
   real_inverse_def:
-  "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)"
+  "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
 
   real_divide_def:
   "R / (S::real) == R * inverse S"
@@ -75,21 +73,20 @@
   real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)"
 
 
-
-subsection{*Proving that realrel is an equivalence relation*}
+subsection {* Equivalence relation over positive reals *}
 
 lemma preal_trans_lemma:
   assumes "x + y1 = x1 + y"
       and "x + y2 = x2 + y"
   shows "x1 + y2 = x2 + (y1::preal)"
 proof -
-  have "(x1 + y2) + x = (x + y2) + x1" by (simp add: preal_add_ac) 
+  have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
   also have "... = (x2 + y) + x1"  by (simp add: prems)
-  also have "... = x2 + (x1 + y)"  by (simp add: preal_add_ac)
+  also have "... = x2 + (x1 + y)"  by (simp add: add_ac)
   also have "... = x2 + (x + y1)"  by (simp add: prems)
-  also have "... = (x2 + y1) + x"  by (simp add: preal_add_ac)
+  also have "... = (x2 + y1) + x"  by (simp add: add_ac)
   finally have "(x1 + y2) + x = (x2 + y1) + x" .
-  thus ?thesis by (simp add: preal_add_right_cancel_iff) 
+  thus ?thesis by (rule add_right_imp_eq)
 qed
 
 
@@ -126,15 +123,15 @@
 done
 
 
-subsection{*Congruence property for addition*}
+subsection {* Addition and Subtraction *}
 
 lemma real_add_congruent2_lemma:
      "[|a + ba = aa + b; ab + bc = ac + bb|]
       ==> a + ab + (ba + bc) = aa + ac + (b + (bb::preal))"
-apply (simp add: preal_add_assoc) 
-apply (rule preal_add_left_commute [of ab, THEN ssubst])
-apply (simp add: preal_add_assoc [symmetric])
-apply (simp add: preal_add_ac)
+apply (simp add: add_assoc)
+apply (rule add_left_commute [of ab, THEN ssubst])
+apply (simp add: add_assoc [symmetric])
+apply (simp add: add_ac)
 done
 
 lemma real_add:
@@ -149,23 +146,6 @@
                   UN_equiv_class2 [OF equiv_realrel equiv_realrel])
 qed
 
-lemma real_add_commute: "(z::real) + w = w + z"
-by (cases z, cases w, simp add: real_add preal_add_ac)
-
-lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)"
-by (cases z1, cases z2, cases z3, simp add: real_add preal_add_assoc)
-
-lemma real_add_zero_left: "(0::real) + z = z"
-by (cases z, simp add: real_add real_zero_def preal_add_ac)
-
-instance real :: comm_monoid_add
-  by (intro_classes,
-      (assumption | 
-       rule real_add_commute real_add_assoc real_add_zero_left)+)
-
-
-subsection{*Additive Inverse on real*}
-
 lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
 proof -
   have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
@@ -174,17 +154,29 @@
     by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
 qed
 
-lemma real_add_minus_left: "(-z) + z = (0::real)"
-by (cases z, simp add: real_minus real_add real_zero_def preal_add_commute)
+instance real :: ab_group_add
+proof
+  fix x y z :: real
+  show "(x + y) + z = x + (y + z)"
+    by (cases x, cases y, cases z, simp add: real_add add_assoc)
+  show "x + y = y + x"
+    by (cases x, cases y, simp add: real_add add_commute)
+  show "0 + x = x"
+    by (cases x, simp add: real_add real_zero_def add_ac)
+  show "- x + x = 0"
+    by (cases x, simp add: real_minus real_add real_zero_def add_commute)
+  show "x - y = x + - y"
+    by (simp add: real_diff_def)
+qed
 
 
-subsection{*Congruence property for multiplication*}
+subsection {* Multiplication *}
 
 lemma real_mult_congruent2_lemma:
      "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==>
           x * x1 + y * y1 + (x * y2 + y * x2) =
           x * x2 + y * y2 + (x * y1 + y * x1)"
-apply (simp add: preal_add_left_commute preal_add_assoc [symmetric])
+apply (simp add: add_left_commute add_assoc [symmetric])
 apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric])
 apply (simp add: preal_add_commute)
 done
@@ -228,13 +220,23 @@
 text{*one and zero are distinct*}
 lemma real_zero_not_eq_one: "0 \<noteq> (1::real)"
 proof -
-  have "preal_of_rat 1 < preal_of_rat 1 + preal_of_rat 1"
-    by (simp add: preal_self_less_add_left) 
+  have "(1::preal) < 1 + 1"
+    by (simp add: preal_self_less_add_left)
   thus ?thesis
     by (simp add: real_zero_def real_one_def preal_add_right_cancel_iff)
 qed
 
-subsection{*existence of inverse*}
+instance real :: comm_ring_1
+proof
+  fix x y z :: real
+  show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
+  show "x * y = y * x" by (rule real_mult_commute)
+  show "1 * x = x" by (rule real_mult_1)
+  show "(x + y) * z = x * z + y * z" by (rule real_add_mult_distrib)
+  show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
+qed
+
+subsection {* Inverse and Division *}
 
 lemma real_zero_iff: "Abs_Real (realrel `` {(x, x)}) = 0"
 by (simp add: real_zero_def preal_add_commute)
@@ -247,12 +249,10 @@
 apply (cut_tac x = xa and y = y in linorder_less_linear)
 apply (auto dest!: less_add_left_Ex simp add: real_zero_iff)
 apply (rule_tac
-        x = "Abs_Real (realrel `` { (preal_of_rat 1, 
-                            inverse (D) + preal_of_rat 1)}) " 
+        x = "Abs_Real (realrel``{(1, inverse (D) + 1)})"
        in exI)
 apply (rule_tac [2]
-        x = "Abs_Real (realrel `` { (inverse (D) + preal_of_rat 1,
-                   preal_of_rat 1)})" 
+        x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})" 
        in exI)
 apply (auto simp add: real_mult preal_mult_1_right
               preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1
@@ -261,8 +261,11 @@
 
 lemma real_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::real)"
 apply (simp add: real_inverse_def)
-apply (frule real_mult_inverse_left_ex, safe)
-apply (rule someI2, auto)
+apply (drule real_mult_inverse_left_ex, safe)
+apply (rule theI, assumption, rename_tac z)
+apply (subgoal_tac "(z * x) * y = z * (x * y)")
+apply (simp add: mult_commute)
+apply (rule mult_assoc)
 done
 
 
@@ -271,13 +274,6 @@
 instance real :: field
 proof
   fix x y z :: real
-  show "- x + x = 0" by (rule real_add_minus_left)
-  show "x - y = x + (-y)" by (simp add: real_diff_def)
-  show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
-  show "x * y = y * x" by (rule real_mult_commute)
-  show "1 * x = x" by (rule real_mult_1)
-  show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib)
-  show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
   show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
   show "x / y = x * inverse y" by (simp add: real_divide_def)
 qed