# HG changeset patch
# User haftmann
# Date 1194335250 -3600
# Node ID 7491c00f0915d99037a58e7c00faa94a780b1009
# Parent  0699e20feabd0e6c933fed30bb2ce285e0e167ac
removed subclass edge ordered_ring < lordered_ring

diff -r 0699e20feabd -r 7491c00f0915 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 06 08:47:25 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 06 08:47:30 2007 +0100
@@ -326,13 +326,19 @@
 instance star :: (pordered_ab_semigroup_add_imp_le) pordered_ab_semigroup_add_imp_le
 by (intro_classes, transfer, rule add_le_imp_le_left)
 
+instance star :: (pordered_comm_monoid_add) pordered_comm_monoid_add ..
 instance star :: (pordered_ab_group_add) pordered_ab_group_add ..
+
+instance star :: (pordered_ab_group_add_abs) pordered_ab_group_add_abs 
+  by intro_classes (transfer,
+    simp add: abs_ge_self abs_leI abs_triangle_ineq)+
+
 instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
-instance star :: (lordered_ab_group_meet) lordered_ab_group_meet ..
-instance star :: (lordered_ab_group_meet) lordered_ab_group_meet ..
-instance star :: (lordered_ab_group) lordered_ab_group ..
+instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet ..
+instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet ..
+instance star :: (lordered_ab_group_add) lordered_ab_group_add ..
 
-instance star :: (lordered_ab_group_abs) lordered_ab_group_abs
+instance star :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs
 by (intro_classes, transfer, rule abs_lattice)
 
 subsection {* Ring and field classes *}
@@ -411,6 +417,8 @@
 by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono)
 
 instance star :: (pordered_ring) pordered_ring ..
+instance star :: (pordered_ring_abs) pordered_ring_abs
+  by intro_classes  (transfer, rule abs_eq_mult)
 instance star :: (lordered_ring) lordered_ring ..
 
 instance star :: (abs_if) abs_if
diff -r 0699e20feabd -r 7491c00f0915 src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Tue Nov 06 08:47:25 2007 +0100
+++ b/src/HOL/MetisExamples/BigO.thy	Tue Nov 06 08:47:30 2007 +0100
@@ -25,8 +25,8 @@
   apply auto
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto);
-  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_le_mult)
+  apply (rule_tac x = "abs c" in exI, auto)
+  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult)
   done
 
 (*** Now various verions with an increasing modulus ***)
@@ -858,11 +858,12 @@
   apply (simp add: bigo_def abs_mult)
 proof (neg_clausify)
 fix x
-assume 0: "\<And>xa. \<not> \<bar>c\<bar> * \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
-have 1: "\<And>X2. \<not> \<bar>c * f (x X2)\<bar> \<le> X2 * \<bar>f (x X2)\<bar>"
-  by (metis 0 abs_mult)
+assume 0: "\<And>xa\<Colon>'b\<Colon>ordered_idom.
+   \<not> \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar> *
+     \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
+     \<le> xa * \<bar>f (x xa)\<bar>"
 show "False"
-  by (metis 1 abs_le_mult)
+  by (metis linorder_neq_iff linorder_antisym_conv1 0)
 qed
 
 lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
diff -r 0699e20feabd -r 7491c00f0915 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Nov 06 08:47:25 2007 +0100
+++ b/src/HOL/Ring_and_Field.thy	Tue Nov 06 08:47:30 2007 +0100
@@ -353,6 +353,8 @@
 
 subclass pordered_cancel_semiring by unfold_locales
 
+subclass pordered_comm_monoid_add by unfold_locales
+
 lemma mult_left_less_imp_less:
   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   by (force simp add: mult_left_mono not_le [symmetric])
@@ -514,14 +516,6 @@
 
 end
 
-class lordered_ring = pordered_ring + lordered_ab_group_abs
-begin
-
-subclass lordered_ab_group_meet by unfold_locales
-subclass lordered_ab_group_join by unfold_locales
-
-end
-
 class abs_if = minus + ord + zero + abs +
   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
 
@@ -529,30 +523,32 @@
   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
 
 class ordered_ring = ring + ordered_semiring
-  + lordered_ab_group + abs_if
-  -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
-         @{text lordered_ab_group}*}
-
-instance ordered_ring \<subseteq> lordered_ring
-proof 
-  fix x :: 'a
-  show "\<bar>x\<bar> = sup x (- x)"
-    by (simp only: abs_if sup_eq_if)
-qed
+  + ordered_ab_group_add + abs_if
+begin
+
+subclass pordered_ring by unfold_locales
+
+subclass pordered_ab_group_add_abs
+proof unfold_locales
+  fix a b
+  show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
+  by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
+   (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
+     neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
+      auto intro!: less_imp_le add_neg_neg)
+qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
+
+end
 
 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
  *)
 class ordered_ring_strict = ring + ordered_semiring_strict
-  + lordered_ab_group + abs_if
-  -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
-         @{text lordered_ab_group}*}
-
-instance ordered_ring_strict \<subseteq> ordered_ring by intro_classes
-
-context ordered_ring_strict
+  + ordered_ab_group_add + abs_if
 begin
 
+subclass ordered_ring by unfold_locales
+
 lemma mult_strict_left_mono_neg:
   "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   apply (drule mult_strict_left_mono [of _ _ "uminus c"])
@@ -571,6 +567,12 @@
 
 end
 
+instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
+apply intro_classes
+apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
+apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
+done
+
 lemma zero_less_mult_iff:
   fixes a :: "'a::ordered_ring_strict"
   shows "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
@@ -579,12 +581,6 @@
   apply (blast dest: zero_less_mult_pos2)
   done
 
-instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
-apply intro_classes
-apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
-apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
-done
-
 lemma zero_le_mult_iff:
      "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
 by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less
@@ -637,7 +633,7 @@
 class ordered_idom =
   comm_ring_1 +
   ordered_comm_semiring_strict +
-  lordered_ab_group +
+  ordered_ab_group_add +
   abs_if + sgn_if
   (*previously ordered_ring*)
 
@@ -652,8 +648,6 @@
   assumes "x \<noteq> y" obtains "x < y" | "y < x"
   using assms by (rule linorder_neqE)
 
--- {* FIXME continue localization here *}
-
 
 text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}
       theorems available to members of @{term ordered_idom} *}
@@ -2006,12 +2000,29 @@
 
 subsection {* Absolute Value *}
 
-lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
-using less_linear[of x 0]
-by(auto simp: sgn_if abs_if)
+context ordered_idom
+begin
+
+lemma mult_sgn_abs: "sgn x * abs x = x"
+  unfolding abs_if sgn_if by auto
+
+end
 
 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
-by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
+  by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
+
+class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
+  assumes abs_eq_mult:
+    "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
+
+
+class lordered_ring = pordered_ring + lordered_ab_group_add_abs
+begin
+
+subclass lordered_ab_group_add_meet by unfold_locales
+subclass lordered_ab_group_add_join by unfold_locales
+
+end
 
 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
 proof -
@@ -2054,9 +2065,11 @@
     done
 qed
 
-lemma abs_eq_mult: 
-  assumes "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
-  shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)"
+instance lordered_ring \<subseteq> pordered_ring_abs
+proof
+  fix a b :: "'a\<Colon> lordered_ring"
+  assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
+  show "abs (a*b) = abs a * abs b"
 proof -
   have s: "(0 <= a*b) | (a*b <= 0)"
     apply (auto)    
@@ -2094,12 +2107,17 @@
       done
   qed
 qed
+qed
+
+instance ordered_idom \<subseteq> pordered_ring_abs
+by default (auto simp add: abs_if not_less
+  equal_neg_zero neg_equal_zero mult_less_0_iff)
 
 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" 
-by (simp add: abs_eq_mult linorder_linear)
+  by (simp add: abs_eq_mult linorder_linear)
 
 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
-by (simp add: abs_if) 
+  by (simp add: abs_if) 
 
 lemma nonzero_abs_inverse:
      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
@@ -2134,29 +2152,27 @@
   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
 qed
 
-lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_idom))"
-by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)
+lemmas eq_minus_self_iff = equal_neg_zero
 
 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
-by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)
+  unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
 
 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))" 
 apply (simp add: order_less_le abs_le_iff)  
-apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
-apply (simp add: le_minus_self_iff linorder_neq_iff) 
+apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
 done
 
 lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
-    (abs y) * x = abs (y * x)";
-  apply (subst abs_mult);
-  apply simp;
-done;
+    (abs y) * x = abs (y * x)"
+  apply (subst abs_mult)
+  apply simp
+done
 
 lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
-    abs x / y = abs (x / y)";
-  apply (subst abs_divide);
-  apply (simp add: order_less_imp_le);
-done;
+    abs x / y = abs (x / y)"
+  apply (subst abs_divide)
+  apply (simp add: order_less_imp_le)
+done
 
 
 subsection {* Bounds of products via negative and positive Part *}