src/HOL/Ring_and_Field.thy
changeset 25304 7491c00f0915
parent 25267 1f745c599b5c
child 25450 c3b26e533b21
     1.1 --- a/src/HOL/Ring_and_Field.thy	Tue Nov 06 08:47:25 2007 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Nov 06 08:47:30 2007 +0100
     1.3 @@ -353,6 +353,8 @@
     1.4  
     1.5  subclass pordered_cancel_semiring by unfold_locales
     1.6  
     1.7 +subclass pordered_comm_monoid_add by unfold_locales
     1.8 +
     1.9  lemma mult_left_less_imp_less:
    1.10    "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
    1.11    by (force simp add: mult_left_mono not_le [symmetric])
    1.12 @@ -514,14 +516,6 @@
    1.13  
    1.14  end
    1.15  
    1.16 -class lordered_ring = pordered_ring + lordered_ab_group_abs
    1.17 -begin
    1.18 -
    1.19 -subclass lordered_ab_group_meet by unfold_locales
    1.20 -subclass lordered_ab_group_join by unfold_locales
    1.21 -
    1.22 -end
    1.23 -
    1.24  class abs_if = minus + ord + zero + abs +
    1.25    assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
    1.26  
    1.27 @@ -529,30 +523,32 @@
    1.28    assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
    1.29  
    1.30  class ordered_ring = ring + ordered_semiring
    1.31 -  + lordered_ab_group + abs_if
    1.32 -  -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
    1.33 -         @{text lordered_ab_group}*}
    1.34 -
    1.35 -instance ordered_ring \<subseteq> lordered_ring
    1.36 -proof 
    1.37 -  fix x :: 'a
    1.38 -  show "\<bar>x\<bar> = sup x (- x)"
    1.39 -    by (simp only: abs_if sup_eq_if)
    1.40 -qed
    1.41 +  + ordered_ab_group_add + abs_if
    1.42 +begin
    1.43 +
    1.44 +subclass pordered_ring by unfold_locales
    1.45 +
    1.46 +subclass pordered_ab_group_add_abs
    1.47 +proof unfold_locales
    1.48 +  fix a b
    1.49 +  show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
    1.50 +  by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
    1.51 +   (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
    1.52 +     neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
    1.53 +      auto intro!: less_imp_le add_neg_neg)
    1.54 +qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
    1.55 +
    1.56 +end
    1.57  
    1.58  (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
    1.59     Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
    1.60   *)
    1.61  class ordered_ring_strict = ring + ordered_semiring_strict
    1.62 -  + lordered_ab_group + abs_if
    1.63 -  -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
    1.64 -         @{text lordered_ab_group}*}
    1.65 -
    1.66 -instance ordered_ring_strict \<subseteq> ordered_ring by intro_classes
    1.67 -
    1.68 -context ordered_ring_strict
    1.69 +  + ordered_ab_group_add + abs_if
    1.70  begin
    1.71  
    1.72 +subclass ordered_ring by unfold_locales
    1.73 +
    1.74  lemma mult_strict_left_mono_neg:
    1.75    "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
    1.76    apply (drule mult_strict_left_mono [of _ _ "uminus c"])
    1.77 @@ -571,6 +567,12 @@
    1.78  
    1.79  end
    1.80  
    1.81 +instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
    1.82 +apply intro_classes
    1.83 +apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
    1.84 +apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
    1.85 +done
    1.86 +
    1.87  lemma zero_less_mult_iff:
    1.88    fixes a :: "'a::ordered_ring_strict"
    1.89    shows "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
    1.90 @@ -579,12 +581,6 @@
    1.91    apply (blast dest: zero_less_mult_pos2)
    1.92    done
    1.93  
    1.94 -instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
    1.95 -apply intro_classes
    1.96 -apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
    1.97 -apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+
    1.98 -done
    1.99 -
   1.100  lemma zero_le_mult_iff:
   1.101       "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
   1.102  by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less
   1.103 @@ -637,7 +633,7 @@
   1.104  class ordered_idom =
   1.105    comm_ring_1 +
   1.106    ordered_comm_semiring_strict +
   1.107 -  lordered_ab_group +
   1.108 +  ordered_ab_group_add +
   1.109    abs_if + sgn_if
   1.110    (*previously ordered_ring*)
   1.111  
   1.112 @@ -652,8 +648,6 @@
   1.113    assumes "x \<noteq> y" obtains "x < y" | "y < x"
   1.114    using assms by (rule linorder_neqE)
   1.115  
   1.116 --- {* FIXME continue localization here *}
   1.117 -
   1.118  
   1.119  text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}
   1.120        theorems available to members of @{term ordered_idom} *}
   1.121 @@ -2006,12 +2000,29 @@
   1.122  
   1.123  subsection {* Absolute Value *}
   1.124  
   1.125 -lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
   1.126 -using less_linear[of x 0]
   1.127 -by(auto simp: sgn_if abs_if)
   1.128 +context ordered_idom
   1.129 +begin
   1.130 +
   1.131 +lemma mult_sgn_abs: "sgn x * abs x = x"
   1.132 +  unfolding abs_if sgn_if by auto
   1.133 +
   1.134 +end
   1.135  
   1.136  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
   1.137 -by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
   1.138 +  by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
   1.139 +
   1.140 +class pordered_ring_abs = pordered_ring + pordered_ab_group_add_abs +
   1.141 +  assumes abs_eq_mult:
   1.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>"
   1.143 +
   1.144 +
   1.145 +class lordered_ring = pordered_ring + lordered_ab_group_add_abs
   1.146 +begin
   1.147 +
   1.148 +subclass lordered_ab_group_add_meet by unfold_locales
   1.149 +subclass lordered_ab_group_add_join by unfold_locales
   1.150 +
   1.151 +end
   1.152  
   1.153  lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 
   1.154  proof -
   1.155 @@ -2054,9 +2065,11 @@
   1.156      done
   1.157  qed
   1.158  
   1.159 -lemma abs_eq_mult: 
   1.160 -  assumes "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
   1.161 -  shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)"
   1.162 +instance lordered_ring \<subseteq> pordered_ring_abs
   1.163 +proof
   1.164 +  fix a b :: "'a\<Colon> lordered_ring"
   1.165 +  assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
   1.166 +  show "abs (a*b) = abs a * abs b"
   1.167  proof -
   1.168    have s: "(0 <= a*b) | (a*b <= 0)"
   1.169      apply (auto)    
   1.170 @@ -2094,12 +2107,17 @@
   1.171        done
   1.172    qed
   1.173  qed
   1.174 +qed
   1.175 +
   1.176 +instance ordered_idom \<subseteq> pordered_ring_abs
   1.177 +by default (auto simp add: abs_if not_less
   1.178 +  equal_neg_zero neg_equal_zero mult_less_0_iff)
   1.179  
   1.180  lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" 
   1.181 -by (simp add: abs_eq_mult linorder_linear)
   1.182 +  by (simp add: abs_eq_mult linorder_linear)
   1.183  
   1.184  lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
   1.185 -by (simp add: abs_if) 
   1.186 +  by (simp add: abs_if) 
   1.187  
   1.188  lemma nonzero_abs_inverse:
   1.189       "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"
   1.190 @@ -2134,29 +2152,27 @@
   1.191    thus ?thesis by (simp add: ac cpos mult_strict_mono) 
   1.192  qed
   1.193  
   1.194 -lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_idom))"
   1.195 -by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)
   1.196 +lemmas eq_minus_self_iff = equal_neg_zero
   1.197  
   1.198  lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
   1.199 -by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)
   1.200 +  unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
   1.201  
   1.202  lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))" 
   1.203  apply (simp add: order_less_le abs_le_iff)  
   1.204 -apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
   1.205 -apply (simp add: le_minus_self_iff linorder_neq_iff) 
   1.206 +apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
   1.207  done
   1.208  
   1.209  lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
   1.210 -    (abs y) * x = abs (y * x)";
   1.211 -  apply (subst abs_mult);
   1.212 -  apply simp;
   1.213 -done;
   1.214 +    (abs y) * x = abs (y * x)"
   1.215 +  apply (subst abs_mult)
   1.216 +  apply simp
   1.217 +done
   1.218  
   1.219  lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
   1.220 -    abs x / y = abs (x / y)";
   1.221 -  apply (subst abs_divide);
   1.222 -  apply (simp add: order_less_imp_le);
   1.223 -done;
   1.224 +    abs x / y = abs (x / y)"
   1.225 +  apply (subst abs_divide)
   1.226 +  apply (simp add: order_less_imp_le)
   1.227 +done
   1.228  
   1.229  
   1.230  subsection {* Bounds of products via negative and positive Part *}