removed subclass edge ordered_ring < lordered_ring
authorhaftmann
Tue Nov 06 08:47:30 2007 +0100 (2007-11-06)
changeset 253047491c00f0915
parent 25303 0699e20feabd
child 25305 574c4964fe54
removed subclass edge ordered_ring < lordered_ring
src/HOL/Hyperreal/StarClasses.thy
src/HOL/MetisExamples/BigO.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 06 08:47:25 2007 +0100
     1.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 06 08:47:30 2007 +0100
     1.3 @@ -326,13 +326,19 @@
     1.4  instance star :: (pordered_ab_semigroup_add_imp_le) pordered_ab_semigroup_add_imp_le
     1.5  by (intro_classes, transfer, rule add_le_imp_le_left)
     1.6  
     1.7 +instance star :: (pordered_comm_monoid_add) pordered_comm_monoid_add ..
     1.8  instance star :: (pordered_ab_group_add) pordered_ab_group_add ..
     1.9 +
    1.10 +instance star :: (pordered_ab_group_add_abs) pordered_ab_group_add_abs 
    1.11 +  by intro_classes (transfer,
    1.12 +    simp add: abs_ge_self abs_leI abs_triangle_ineq)+
    1.13 +
    1.14  instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
    1.15 -instance star :: (lordered_ab_group_meet) lordered_ab_group_meet ..
    1.16 -instance star :: (lordered_ab_group_meet) lordered_ab_group_meet ..
    1.17 -instance star :: (lordered_ab_group) lordered_ab_group ..
    1.18 +instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet ..
    1.19 +instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet ..
    1.20 +instance star :: (lordered_ab_group_add) lordered_ab_group_add ..
    1.21  
    1.22 -instance star :: (lordered_ab_group_abs) lordered_ab_group_abs
    1.23 +instance star :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs
    1.24  by (intro_classes, transfer, rule abs_lattice)
    1.25  
    1.26  subsection {* Ring and field classes *}
    1.27 @@ -411,6 +417,8 @@
    1.28  by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono)
    1.29  
    1.30  instance star :: (pordered_ring) pordered_ring ..
    1.31 +instance star :: (pordered_ring_abs) pordered_ring_abs
    1.32 +  by intro_classes  (transfer, rule abs_eq_mult)
    1.33  instance star :: (lordered_ring) lordered_ring ..
    1.34  
    1.35  instance star :: (abs_if) abs_if
     2.1 --- a/src/HOL/MetisExamples/BigO.thy	Tue Nov 06 08:47:25 2007 +0100
     2.2 +++ b/src/HOL/MetisExamples/BigO.thy	Tue Nov 06 08:47:30 2007 +0100
     2.3 @@ -25,8 +25,8 @@
     2.4    apply auto
     2.5    apply (case_tac "c = 0", simp)
     2.6    apply (rule_tac x = "1" in exI, simp)
     2.7 -  apply (rule_tac x = "abs c" in exI, auto);
     2.8 -  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_le_mult)
     2.9 +  apply (rule_tac x = "abs c" in exI, auto)
    2.10 +  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult)
    2.11    done
    2.12  
    2.13  (*** Now various verions with an increasing modulus ***)
    2.14 @@ -858,11 +858,12 @@
    2.15    apply (simp add: bigo_def abs_mult)
    2.16  proof (neg_clausify)
    2.17  fix x
    2.18 -assume 0: "\<And>xa. \<not> \<bar>c\<bar> * \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
    2.19 -have 1: "\<And>X2. \<not> \<bar>c * f (x X2)\<bar> \<le> X2 * \<bar>f (x X2)\<bar>"
    2.20 -  by (metis 0 abs_mult)
    2.21 +assume 0: "\<And>xa\<Colon>'b\<Colon>ordered_idom.
    2.22 +   \<not> \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar> *
    2.23 +     \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
    2.24 +     \<le> xa * \<bar>f (x xa)\<bar>"
    2.25  show "False"
    2.26 -  by (metis 1 abs_le_mult)
    2.27 +  by (metis linorder_neq_iff linorder_antisym_conv1 0)
    2.28  qed
    2.29  
    2.30  lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
     3.1 --- a/src/HOL/Ring_and_Field.thy	Tue Nov 06 08:47:25 2007 +0100
     3.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Nov 06 08:47:30 2007 +0100
     3.3 @@ -353,6 +353,8 @@
     3.4  
     3.5  subclass pordered_cancel_semiring by unfold_locales
     3.6  
     3.7 +subclass pordered_comm_monoid_add by unfold_locales
     3.8 +
     3.9  lemma mult_left_less_imp_less:
    3.10    "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
    3.11    by (force simp add: mult_left_mono not_le [symmetric])
    3.12 @@ -514,14 +516,6 @@
    3.13  
    3.14  end
    3.15  
    3.16 -class lordered_ring = pordered_ring + lordered_ab_group_abs
    3.17 -begin
    3.18 -
    3.19 -subclass lordered_ab_group_meet by unfold_locales
    3.20 -subclass lordered_ab_group_join by unfold_locales
    3.21 -
    3.22 -end
    3.23 -
    3.24  class abs_if = minus + ord + zero + abs +
    3.25    assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
    3.26  
    3.27 @@ -529,30 +523,32 @@
    3.28    assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
    3.29  
    3.30  class ordered_ring = ring + ordered_semiring
    3.31 -  + lordered_ab_group + abs_if
    3.32 -  -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
    3.33 -         @{text lordered_ab_group}*}
    3.34 -
    3.35 -instance ordered_ring \<subseteq> lordered_ring
    3.36 -proof 
    3.37 -  fix x :: 'a
    3.38 -  show "\<bar>x\<bar> = sup x (- x)"
    3.39 -    by (simp only: abs_if sup_eq_if)
    3.40 -qed
    3.41 +  + ordered_ab_group_add + abs_if
    3.42 +begin
    3.43 +
    3.44 +subclass pordered_ring by unfold_locales
    3.45 +
    3.46 +subclass pordered_ab_group_add_abs
    3.47 +proof unfold_locales
    3.48 +  fix a b
    3.49 +  show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
    3.50 +  by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
    3.51 +   (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
    3.52 +     neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
    3.53 +      auto intro!: less_imp_le add_neg_neg)
    3.54 +qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
    3.55 +
    3.56 +end
    3.57  
    3.58  (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
    3.59     Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
    3.60   *)
    3.61  class ordered_ring_strict = ring + ordered_semiring_strict
    3.62 -  + lordered_ab_group + abs_if
    3.63 -  -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
    3.64 -         @{text lordered_ab_group}*}
    3.65 -
    3.66 -instance ordered_ring_strict \<subseteq> ordered_ring by intro_classes
    3.67 -
    3.68 -context ordered_ring_strict
    3.69 +  + ordered_ab_group_add + abs_if
    3.70  begin
    3.71  
    3.72 +subclass ordered_ring by unfold_locales
    3.73 +
    3.74  lemma mult_strict_left_mono_neg:
    3.75    "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
    3.76    apply (drule mult_strict_left_mono [of _ _ "uminus c"])
    3.77 @@ -571,6 +567,12 @@
    3.78  
    3.79  end
    3.80  
    3.81 +instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
    3.82 +apply intro_classes
    3.83 +apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
    3.84 +apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
    3.85 +done
    3.86 +
    3.87  lemma zero_less_mult_iff:
    3.88    fixes a :: "'a::ordered_ring_strict"
    3.89    shows "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
    3.90 @@ -579,12 +581,6 @@
    3.91    apply (blast dest: zero_less_mult_pos2)
    3.92    done
    3.93  
    3.94 -instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
    3.95 -apply intro_classes
    3.96 -apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
    3.97 -apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
    3.98 -done
    3.99 -
   3.100  lemma zero_le_mult_iff:
   3.101       "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
   3.102  by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less
   3.103 @@ -637,7 +633,7 @@
   3.104  class ordered_idom =
   3.105    comm_ring_1 +
   3.106    ordered_comm_semiring_strict +
   3.107 -  lordered_ab_group +
   3.108 +  ordered_ab_group_add +
   3.109    abs_if + sgn_if
   3.110    (*previously ordered_ring*)
   3.111  
   3.112 @@ -652,8 +648,6 @@
   3.113    assumes "x \<noteq> y" obtains "x < y" | "y < x"
   3.114    using assms by (rule linorder_neqE)
   3.115  
   3.116 --- {* FIXME continue localization here *}
   3.117 -
   3.118  
   3.119  text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}
   3.120        theorems available to members of @{term ordered_idom} *}
   3.121 @@ -2006,12 +2000,29 @@
   3.122  
   3.123  subsection {* Absolute Value *}
   3.124  
   3.125 -lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
   3.126 -using less_linear[of x 0]
   3.127 -by(auto simp: sgn_if abs_if)
   3.128 +context ordered_idom
   3.129 +begin
   3.130 +
   3.131 +lemma mult_sgn_abs: "sgn x * abs x = x"
   3.132 +  unfolding abs_if sgn_if by auto
   3.133 +
   3.134 +end
   3.135  
   3.136  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
   3.137 -by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
   3.138 +  by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
   3.139 +
   3.140 +class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
   3.141 +  assumes abs_eq_mult:
   3.142 +    "(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>"
   3.143 +
   3.144 +
   3.145 +class lordered_ring = pordered_ring + lordered_ab_group_add_abs
   3.146 +begin
   3.147 +
   3.148 +subclass lordered_ab_group_add_meet by unfold_locales
   3.149 +subclass lordered_ab_group_add_join by unfold_locales
   3.150 +
   3.151 +end
   3.152  
   3.153  lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
   3.154  proof -
   3.155 @@ -2054,9 +2065,11 @@
   3.156      done
   3.157  qed
   3.158  
   3.159 -lemma abs_eq_mult: 
   3.160 -  assumes "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
   3.161 -  shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)"
   3.162 +instance lordered_ring \<subseteq> pordered_ring_abs
   3.163 +proof
   3.164 +  fix a b :: "'a\<Colon> lordered_ring"
   3.165 +  assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
   3.166 +  show "abs (a*b) = abs a * abs b"
   3.167  proof -
   3.168    have s: "(0 <= a*b) | (a*b <= 0)"
   3.169      apply (auto)    
   3.170 @@ -2094,12 +2107,17 @@
   3.171        done
   3.172    qed
   3.173  qed
   3.174 +qed
   3.175 +
   3.176 +instance ordered_idom \<subseteq> pordered_ring_abs
   3.177 +by default (auto simp add: abs_if not_less
   3.178 +  equal_neg_zero neg_equal_zero mult_less_0_iff)
   3.179  
   3.180  lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" 
   3.181 -by (simp add: abs_eq_mult linorder_linear)
   3.182 +  by (simp add: abs_eq_mult linorder_linear)
   3.183  
   3.184  lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
   3.185 -by (simp add: abs_if) 
   3.186 +  by (simp add: abs_if) 
   3.187  
   3.188  lemma nonzero_abs_inverse:
   3.189       "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
   3.190 @@ -2134,29 +2152,27 @@
   3.191    thus ?thesis by (simp add: ac cpos mult_strict_mono) 
   3.192  qed
   3.193  
   3.194 -lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_idom))"
   3.195 -by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)
   3.196 +lemmas eq_minus_self_iff = equal_neg_zero
   3.197  
   3.198  lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
   3.199 -by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)
   3.200 +  unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
   3.201  
   3.202  lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))" 
   3.203  apply (simp add: order_less_le abs_le_iff)  
   3.204 -apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
   3.205 -apply (simp add: le_minus_self_iff linorder_neq_iff) 
   3.206 +apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
   3.207  done
   3.208  
   3.209  lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
   3.210 -    (abs y) * x = abs (y * x)";
   3.211 -  apply (subst abs_mult);
   3.212 -  apply simp;
   3.213 -done;
   3.214 +    (abs y) * x = abs (y * x)"
   3.215 +  apply (subst abs_mult)
   3.216 +  apply simp
   3.217 +done
   3.218  
   3.219  lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
   3.220 -    abs x / y = abs (x / y)";
   3.221 -  apply (subst abs_divide);
   3.222 -  apply (simp add: order_less_imp_le);
   3.223 -done;
   3.224 +    abs x / y = abs (x / y)"
   3.225 +  apply (subst abs_divide)
   3.226 +  apply (simp add: order_less_imp_le)
   3.227 +done
   3.228  
   3.229  
   3.230  subsection {* Bounds of products via negative and positive Part *}