continued localization
authorhaftmann
Tue Oct 30 08:45:54 2007 +0100 (2007-10-30)
changeset 25230022029099a83
parent 25229 2673709fb8f7
child 25231 1aa9c8f022d0
continued localization
src/HOL/Hyperreal/StarClasses.thy
src/HOL/IntArith.thy
src/HOL/IntDef.thy
src/HOL/OrderedGroup.thy
src/HOL/Presburger.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Mon Oct 29 17:08:01 2007 +0100
     1.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Oct 30 08:45:54 2007 +0100
     1.3 @@ -403,7 +403,7 @@
     1.4  done
     1.5  
     1.6  instance star :: (pordered_comm_semiring) pordered_comm_semiring
     1.7 -by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono)
     1.8 +by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono1)
     1.9  
    1.10  instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
    1.11  
    1.12 @@ -451,7 +451,7 @@
    1.13  subsection {* Number classes *}
    1.14  
    1.15  lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
    1.16 -by (induct_tac n, simp_all)
    1.17 +by (induct n, simp_all)
    1.18  
    1.19  lemma Standard_of_nat [simp]: "of_nat n \<in> Standard"
    1.20  by (simp add: star_of_nat_def)
     2.1 --- a/src/HOL/IntArith.thy	Mon Oct 29 17:08:01 2007 +0100
     2.2 +++ b/src/HOL/IntArith.thy	Tue Oct 30 08:45:54 2007 +0100
     2.3 @@ -208,9 +208,20 @@
     2.4    with False show ?thesis by simp
     2.5  qed
     2.6  
     2.7 -lemma of_int_of_nat: "of_int k = (if k < 0 then - of_nat (nat (- k))
     2.8 -  else of_nat (nat k))"
     2.9 -  by (auto simp add: of_nat_nat)
    2.10 +context ring_1
    2.11 +begin
    2.12 +
    2.13 +lemma of_int_of_nat:
    2.14 +  "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
    2.15 +proof (cases "k < 0")
    2.16 +  case True then have "0 \<le> - k" by simp
    2.17 +  then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
    2.18 +  with True show ?thesis by simp
    2.19 +next
    2.20 +  case False then show ?thesis by (simp add: not_less of_nat_nat)
    2.21 +qed
    2.22 +
    2.23 +end
    2.24  
    2.25  lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
    2.26  apply (cases "0 \<le> z'")
     3.1 --- a/src/HOL/IntDef.thy	Mon Oct 29 17:08:01 2007 +0100
     3.2 +++ b/src/HOL/IntDef.thy	Tue Oct 30 08:45:54 2007 +0100
     3.3 @@ -429,6 +429,8 @@
     3.4  context ring_1
     3.5  begin
     3.6  
     3.7 +term of_nat
     3.8 +
     3.9  definition
    3.10    of_int :: "int \<Rightarrow> 'a"
    3.11  where
    3.12 @@ -518,10 +520,15 @@
    3.13      by (cases z) (simp add: of_int add minus int_def diff_minus)
    3.14  qed
    3.15  
    3.16 +context ring_1
    3.17 +begin
    3.18 +
    3.19  lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
    3.20 -by (cases z rule: eq_Abs_Integ)
    3.21 +  by (cases z rule: eq_Abs_Integ)
    3.22     (simp add: nat le of_int Zero_int_def of_nat_diff)
    3.23  
    3.24 +end
    3.25 +
    3.26  
    3.27  subsection{*The Set of Integers*}
    3.28  
     4.1 --- a/src/HOL/OrderedGroup.thy	Mon Oct 29 17:08:01 2007 +0100
     4.2 +++ b/src/HOL/OrderedGroup.thy	Tue Oct 30 08:45:54 2007 +0100
     4.3 @@ -535,8 +535,21 @@
     4.4  lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
     4.5    by (simp add: compare_rls)
     4.6  
     4.7 +lemmas group_simps =
     4.8 +  add_ac
     4.9 +  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
    4.10 +  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
    4.11 +  diff_less_eq less_diff_eq diff_le_eq le_diff_eq
    4.12 +
    4.13  end
    4.14  
    4.15 +lemmas group_simps =
    4.16 +  mult_ac
    4.17 +  add_ac
    4.18 +  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
    4.19 +  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
    4.20 +  diff_less_eq less_diff_eq diff_le_eq le_diff_eq
    4.21 +
    4.22  class ordered_ab_semigroup_add =
    4.23    linorder + pordered_ab_semigroup_add
    4.24  
    4.25 @@ -565,6 +578,12 @@
    4.26    qed
    4.27  qed
    4.28  
    4.29 +class ordered_ab_group_add =
    4.30 +  linorder + pordered_ab_group_add
    4.31 +
    4.32 +subclass (in ordered_ab_group_add) ordered_cancel_ab_semigroup_add 
    4.33 +  by unfold_locales
    4.34 +
    4.35  -- {* FIXME localize the following *}
    4.36  
    4.37  lemma add_increasing:
    4.38 @@ -752,6 +771,12 @@
    4.39      (simp add: le_infI)
    4.40  qed
    4.41  
    4.42 +lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
    4.43 +  by (simp add: inf_eq_neg_sup)
    4.44 +
    4.45 +lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
    4.46 +  by (simp add: sup_eq_neg_inf)
    4.47 +
    4.48  lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
    4.49  proof -
    4.50    have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
    4.51 @@ -776,6 +801,21 @@
    4.52    pprt :: "'a \<Rightarrow> 'a" where
    4.53    "pprt x = sup x 0"
    4.54  
    4.55 +lemma pprt_neg: "pprt (- x) = - nprt x"
    4.56 +proof -
    4.57 +  have "sup (- x) 0 = sup (- x) (- 0)" unfolding minus_zero ..
    4.58 +  also have "\<dots> = - inf x 0" unfolding neg_inf_eq_sup ..
    4.59 +  finally have "sup (- x) 0 = - inf x 0" .
    4.60 +  then show ?thesis unfolding pprt_def nprt_def .
    4.61 +qed
    4.62 +
    4.63 +lemma nprt_neg: "nprt (- x) = - pprt x"
    4.64 +proof -
    4.65 +  from pprt_neg have "pprt (- (- x)) = - nprt (- x)" .
    4.66 +  then have "pprt x = - nprt (- x)" by simp
    4.67 +  then show ?thesis by simp
    4.68 +qed
    4.69 +
    4.70  lemma prts: "a = pprt a + nprt a"
    4.71    by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
    4.72  
    4.73 @@ -904,38 +944,67 @@
    4.74    ultimately show ?thesis by blast
    4.75  qed
    4.76  
    4.77 +declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp]
    4.78 +
    4.79 +lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
    4.80 +proof -
    4.81 +  from add_le_cancel_left [of "uminus a" "plus a a" zero]
    4.82 +  have "(a <= -a) = (a+a <= 0)" 
    4.83 +    by (simp add: add_assoc[symmetric])
    4.84 +  thus ?thesis by simp
    4.85 +qed
    4.86 +
    4.87 +lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
    4.88 +proof -
    4.89 +  from add_le_cancel_left [of "uminus a" zero "plus a a"]
    4.90 +  have "(-a <= a) = (0 <= a+a)" 
    4.91 +    by (simp add: add_assoc[symmetric])
    4.92 +  thus ?thesis by simp
    4.93 +qed
    4.94 +
    4.95 +lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
    4.96 +  by (simp add: le_iff_inf nprt_def inf_commute)
    4.97 +
    4.98 +lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
    4.99 +  by (simp add: le_iff_sup pprt_def sup_commute)
   4.100 +
   4.101 +lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
   4.102 +  by (simp add: le_iff_sup pprt_def sup_commute)
   4.103 +
   4.104 +lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
   4.105 +  by (simp add: le_iff_inf nprt_def inf_commute)
   4.106 +
   4.107 +lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
   4.108 +  by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
   4.109 +
   4.110 +lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
   4.111 +  by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
   4.112 +
   4.113  end
   4.114  
   4.115  lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   4.116  
   4.117 -class lordered_ab_group_abs = lordered_ab_group + abs +
   4.118 -  assumes abs_lattice: "\<bar>x\<bar> = sup x (- x)"
   4.119 +
   4.120 +class pordered_ab_group_add_abs = pordered_ab_group_add + abs +
   4.121 +  assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
   4.122 +    and abs_ge_self: "a \<le> \<bar>a\<bar>"
   4.123 +    and abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
   4.124 +    and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   4.125 +    and abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   4.126 +    and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
   4.127 +    and abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   4.128 +    and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   4.129  begin
   4.130  
   4.131  lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
   4.132 -  by (simp add: abs_lattice)
   4.133 -
   4.134 -lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   4.135 -  by (simp add: abs_lattice)
   4.136 +  by simp
   4.137  
   4.138  lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
   4.139  proof -
   4.140 -  have "(0 = abs a) = (abs a = 0)" by (simp only: eq_ac)
   4.141 +  have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
   4.142    thus ?thesis by simp
   4.143  qed
   4.144  
   4.145 -lemma neg_inf_eq_sup [simp]: "- inf a b = sup (-a) (-b)"
   4.146 -  by (simp add: inf_eq_neg_sup)
   4.147 -
   4.148 -lemma neg_sup_eq_inf [simp]: "- sup a b = inf (-a) (-b)"
   4.149 -  by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf)
   4.150 -
   4.151 -lemma abs_ge_zero [simp]: "0 \<le> \<bar>a\<bar>"
   4.152 -proof -
   4.153 -  have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
   4.154 -  show ?thesis by (rule add_mono [OF a b, simplified])
   4.155 -qed
   4.156 -  
   4.157  lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
   4.158  proof
   4.159    assume "\<bar>a\<bar> \<le> 0"
   4.160 @@ -955,20 +1024,11 @@
   4.161    show ?thesis by (simp add: a)
   4.162  qed
   4.163  
   4.164 -lemma abs_ge_self: "a \<le> \<bar>a\<bar>"
   4.165 -  by (auto simp add: abs_lattice)
   4.166 -
   4.167  lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
   4.168 -  by (auto simp add: abs_lattice)
   4.169 -
   4.170 -lemma abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
   4.171 -  by (simp add: abs_lattice sup_commute)
   4.172 -
   4.173 -lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   4.174 -apply (simp add: abs_lattice [of "abs a"])
   4.175 -apply (subst sup_absorb1)
   4.176 -apply (rule order_trans [of _ zero])
   4.177 -by auto
   4.178 +proof -
   4.179 +  have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
   4.180 +  then show ?thesis by simp
   4.181 +qed
   4.182  
   4.183  lemma abs_minus_commute: 
   4.184    "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
   4.185 @@ -978,73 +1038,24 @@
   4.186    finally show ?thesis .
   4.187  qed
   4.188  
   4.189 -lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a"
   4.190 +lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
   4.191 +  by (rule abs_of_nonneg, rule less_imp_le)
   4.192 +
   4.193 +lemma abs_of_nonpos [simp]:
   4.194 +  assumes "a \<le> 0"
   4.195 +  shows "\<bar>a\<bar> = - a"
   4.196  proof -
   4.197 -  have "0 \<le> \<bar>a\<bar>" by simp
   4.198 -  then have "0 \<le> sup a (- a)" unfolding abs_lattice .
   4.199 -  then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
   4.200 -  then show ?thesis
   4.201 -    by (simp add: add_sup_inf_distribs sup_ACI
   4.202 -      pprt_def nprt_def diff_minus abs_lattice)
   4.203 +  let ?b = "- a"
   4.204 +  have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
   4.205 +  unfolding abs_minus_cancel [of "?b"]
   4.206 +  unfolding neg_le_0_iff_le [of "?b"]
   4.207 +  unfolding minus_minus by (erule abs_of_nonneg)
   4.208 +  then show ?thesis using assms by auto
   4.209  qed
   4.210    
   4.211 -lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
   4.212 -  by (simp add: le_iff_inf nprt_def inf_commute)
   4.213 -
   4.214 -lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
   4.215 -  by (simp add: le_iff_sup pprt_def sup_commute)
   4.216 -
   4.217 -lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
   4.218 -  by (simp add: le_iff_sup pprt_def sup_commute)
   4.219 -
   4.220 -lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
   4.221 -by (simp add: le_iff_inf nprt_def inf_commute)
   4.222 -
   4.223 -lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
   4.224 -  by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
   4.225 -
   4.226 -lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
   4.227 -  by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
   4.228 -
   4.229 -lemma pprt_neg: "pprt (- x) = - nprt x"
   4.230 -  by (simp add: pprt_def nprt_def)
   4.231 -
   4.232 -lemma nprt_neg: "nprt (- x) = - pprt x"
   4.233 -  by (simp add: pprt_def nprt_def)
   4.234 -
   4.235 -lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
   4.236 -  by (simp add: iffD1 [OF zero_le_iff_zero_nprt]
   4.237 -    iffD1[OF le_zero_iff_pprt_id] abs_prts)
   4.238 -
   4.239 -lemma abs_of_pos: "0 < x \<Longrightarrow> \<bar>x\<bar> = x"
   4.240 -  by (rule abs_of_nonneg, rule less_imp_le)
   4.241 -
   4.242 -lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   4.243 -  by (simp add: iffD1 [OF le_zero_iff_zero_pprt]
   4.244 -    iffD1 [OF zero_le_iff_nprt_id] abs_prts)
   4.245 -
   4.246 -lemma abs_of_neg: "x < 0 \<Longrightarrow> \<bar>x\<bar> = - x"
   4.247 +lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   4.248    by (rule abs_of_nonpos, rule less_imp_le)
   4.249  
   4.250 -lemma abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   4.251 -  by (simp add: abs_lattice le_supI)
   4.252 -
   4.253 -lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
   4.254 -proof -
   4.255 -  from add_le_cancel_left [of "uminus a" "plus a a" zero]
   4.256 -  have "(a <= -a) = (a+a <= 0)" 
   4.257 -    by (simp add: add_assoc[symmetric])
   4.258 -  thus ?thesis by simp
   4.259 -qed
   4.260 -
   4.261 -lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   4.262 -proof -
   4.263 -  from add_le_cancel_left [of "uminus a" zero "plus a a"]
   4.264 -  have "(-a <= a) = (0 <= a+a)" 
   4.265 -    by (simp add: add_assoc[symmetric])
   4.266 -  thus ?thesis by simp
   4.267 -qed
   4.268 -
   4.269  lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
   4.270    by (insert abs_ge_self, blast intro: order_trans)
   4.271  
   4.272 @@ -1054,20 +1065,6 @@
   4.273  lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
   4.274    by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   4.275  
   4.276 -lemma abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   4.277 -proof -
   4.278 -  have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
   4.279 -    by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
   4.280 -  have a:"a+b <= sup ?m ?n" by (simp)
   4.281 -  have b:"-a-b <= ?n" by (simp) 
   4.282 -  have c:"?n <= sup ?m ?n" by (simp)
   4.283 -  from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
   4.284 -  have e:"-a-b = -(a+b)" by (simp add: diff_minus)
   4.285 -  from a d e have "abs(a+b) <= sup ?m ?n" 
   4.286 -    by (drule_tac abs_leI, auto)
   4.287 -  with g[symmetric] show ?thesis by simp
   4.288 -qed
   4.289 -
   4.290  lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
   4.291    apply (simp add: compare_rls)
   4.292    apply (subgoal_tac "abs a = abs (plus (minus a b) b)")
   4.293 @@ -1102,7 +1099,7 @@
   4.294    finally show ?thesis .
   4.295  qed
   4.296  
   4.297 -lemma abs_add_abs[simp]:
   4.298 +lemma abs_add_abs [simp]:
   4.299    "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
   4.300  proof (rule antisym)
   4.301    show "?L \<ge> ?R" by(rule abs_ge_self)
   4.302 @@ -1114,6 +1111,87 @@
   4.303  
   4.304  end
   4.305  
   4.306 +
   4.307 +class lordered_ab_group_abs = lordered_ab_group + abs +
   4.308 +  assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)"
   4.309 +begin
   4.310 +
   4.311 +lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a"
   4.312 +proof -
   4.313 +  have "0 \<le> \<bar>a\<bar>"
   4.314 +  proof -
   4.315 +    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
   4.316 +    show ?thesis by (rule add_mono [OF a b, simplified])
   4.317 +  qed
   4.318 +  then have "0 \<le> sup a (- a)" unfolding abs_lattice .
   4.319 +  then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
   4.320 +  then show ?thesis
   4.321 +    by (simp add: add_sup_inf_distribs sup_ACI
   4.322 +      pprt_def nprt_def diff_minus abs_lattice)
   4.323 +qed
   4.324 +
   4.325 +subclass pordered_ab_group_add_abs
   4.326 +proof -
   4.327 +  have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>"
   4.328 +  proof -
   4.329 +    fix a b
   4.330 +    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
   4.331 +    show "0 \<le> \<bar>a\<bar>" by (rule add_mono [OF a b, simplified])
   4.332 +  qed
   4.333 +  have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   4.334 +    by (simp add: abs_lattice le_supI)
   4.335 +  show ?thesis
   4.336 +  proof unfold_locales
   4.337 +    fix a
   4.338 +    show "0 \<le> \<bar>a\<bar>" by simp
   4.339 +  next
   4.340 +    fix a
   4.341 +    show "a \<le> \<bar>a\<bar>"
   4.342 +      by (auto simp add: abs_lattice)
   4.343 +  next
   4.344 +    fix a
   4.345 +    show "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   4.346 +      by (simp add: abs_lattice)
   4.347 +  next
   4.348 +    fix a
   4.349 +    show "\<bar>-a\<bar> = \<bar>a\<bar>"
   4.350 +      by (simp add: abs_lattice sup_commute)
   4.351 +  next
   4.352 +    fix a
   4.353 +    show "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   4.354 +    apply (simp add: abs_lattice [of "abs a"])
   4.355 +    apply (subst sup_absorb1)
   4.356 +    apply (rule order_trans [of _ zero])
   4.357 +    apply auto
   4.358 +    done
   4.359 +  next
   4.360 +    fix a
   4.361 +    show "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
   4.362 +      by (simp add: iffD1 [OF zero_le_iff_zero_nprt]
   4.363 +        iffD1[OF le_zero_iff_pprt_id] abs_prts)
   4.364 +  next
   4.365 +    fix a b
   4.366 +    show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (erule abs_leI)
   4.367 +  next
   4.368 +    fix a b
   4.369 +    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   4.370 +    proof -
   4.371 +      have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
   4.372 +        by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
   4.373 +      have a:"a+b <= sup ?m ?n" by (simp)
   4.374 +      have b:"-a-b <= ?n" by (simp) 
   4.375 +      have c:"?n <= sup ?m ?n" by (simp)
   4.376 +      from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
   4.377 +      have e:"-a-b = -(a+b)" by (simp add: diff_minus)
   4.378 +      from a d e have "abs(a+b) <= sup ?m ?n" 
   4.379 +        by (drule_tac abs_leI, auto)
   4.380 +      with g[symmetric] show ?thesis by simp
   4.381 +    qed
   4.382 +  qed auto
   4.383 +qed
   4.384 +
   4.385 +end
   4.386 +
   4.387  lemma sup_eq_if:
   4.388    fixes a :: "'a\<Colon>{lordered_ab_group, linorder}"
   4.389    shows "sup a (- a) = (if a < 0 then - a else a)"
   4.390 @@ -1168,13 +1246,6 @@
   4.391    apply (simp_all add: prems)
   4.392    done
   4.393  
   4.394 -lemmas group_simps =
   4.395 -  mult_ac
   4.396 -  add_ac
   4.397 -  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   4.398 -  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
   4.399 -  diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   4.400 -
   4.401  lemma estimate_by_abs:
   4.402    "a + b <= (c::'a::lordered_ab_group_abs) \<Longrightarrow> a <= c + abs b" 
   4.403  proof -
     5.1 --- a/src/HOL/Presburger.thy	Mon Oct 29 17:08:01 2007 +0100
     5.2 +++ b/src/HOL/Presburger.thy	Tue Oct 30 08:45:54 2007 +0100
     5.3 @@ -703,6 +703,8 @@
     5.4    less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
     5.5    less_number_of
     5.6  
     5.7 +context ring_1
     5.8 +begin
     5.9  
    5.10  lemma of_int_num [code func]:
    5.11    "of_int k = (if k = 0 then 0 else if k < 0 then
    5.12 @@ -737,3 +739,5 @@
    5.13  qed
    5.14  
    5.15  end
    5.16 +
    5.17 +end
     6.1 --- a/src/HOL/Ring_and_Field.thy	Mon Oct 29 17:08:01 2007 +0100
     6.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Oct 30 08:45:54 2007 +0100
     6.3 @@ -153,17 +153,25 @@
     6.4  lemmas ring_distribs =
     6.5    right_distrib left_distrib left_diff_distrib right_diff_distrib
     6.6  
     6.7 +lemmas ring_simps =
     6.8 +  add_ac
     6.9 +  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
    6.10 +  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
    6.11 +  ring_distribs
    6.12 +
    6.13 +lemma eq_add_iff1:
    6.14 +  "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
    6.15 +  by (simp add: ring_simps)
    6.16 +
    6.17 +lemma eq_add_iff2:
    6.18 +  "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d"
    6.19 +  by (simp add: ring_simps)
    6.20 +
    6.21  end
    6.22  
    6.23  lemmas ring_distribs =
    6.24    right_distrib left_distrib left_diff_distrib right_diff_distrib
    6.25  
    6.26 -text{*This list of rewrites simplifies ring terms by multiplying
    6.27 -everything out and bringing sums and products into a canonical form
    6.28 -(by ordered rewriting). As a result it decides ring equalities but
    6.29 -also helps with inequalities. *}
    6.30 -lemmas ring_simps = group_simps ring_distribs
    6.31 -
    6.32  class comm_ring = comm_semiring + ab_group_add
    6.33  
    6.34  subclass (in comm_ring) ring by unfold_locales
    6.35 @@ -180,6 +188,18 @@
    6.36  subclass (in comm_ring_1) comm_semiring_1_cancel by unfold_locales
    6.37  
    6.38  class ring_no_zero_divisors = ring + no_zero_divisors
    6.39 +begin
    6.40 +
    6.41 +lemma mult_eq_0_iff [simp]:
    6.42 +  shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
    6.43 +proof (cases "a = 0 \<or> b = 0")
    6.44 +  case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
    6.45 +    then show ?thesis using no_zero_divisors by simp
    6.46 +next
    6.47 +  case True then show ?thesis by auto
    6.48 +qed
    6.49 +
    6.50 +end
    6.51  
    6.52  class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
    6.53  
    6.54 @@ -226,16 +246,75 @@
    6.55    thus "inverse a * a = 1" by (rule field_inverse)
    6.56    thus "a * inverse a = 1" by (simp only: mult_commute)
    6.57  qed
    6.58 +
    6.59  subclass (in field) idom by unfold_locales
    6.60  
    6.61 +context field
    6.62 +begin
    6.63 +
    6.64 +lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
    6.65 +proof
    6.66 +  assume neq: "b \<noteq> 0"
    6.67 +  {
    6.68 +    hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
    6.69 +    also assume "a / b = 1"
    6.70 +    finally show "a = b" by simp
    6.71 +  next
    6.72 +    assume "a = b"
    6.73 +    with neq show "a / b = 1" by (simp add: divide_inverse)
    6.74 +  }
    6.75 +qed
    6.76 +
    6.77 +lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
    6.78 +  by (simp add: divide_inverse)
    6.79 +
    6.80 +lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
    6.81 +  by (simp add: divide_inverse)
    6.82 +
    6.83 +lemma divide_zero_left [simp]: "0 / a = 0"
    6.84 +  by (simp add: divide_inverse)
    6.85 +
    6.86 +lemma inverse_eq_divide: "inverse a = 1 / a"
    6.87 +  by (simp add: divide_inverse)
    6.88 +
    6.89 +lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
    6.90 +  by (simp add: divide_inverse ring_distribs) 
    6.91 +
    6.92 +end
    6.93 +
    6.94  class division_by_zero = zero + inverse +
    6.95    assumes inverse_zero [simp]: "inverse 0 = 0"
    6.96  
    6.97 +lemma divide_zero [simp]:
    6.98 +  "a / 0 = (0::'a::{field,division_by_zero})"
    6.99 +  by (simp add: divide_inverse)
   6.100 +
   6.101 +lemma divide_self_if [simp]:
   6.102 +  "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
   6.103 +  by (simp add: divide_self)
   6.104 +
   6.105  class mult_mono = times + zero + ord +
   6.106    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   6.107    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   6.108  
   6.109  class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
   6.110 +begin
   6.111 +
   6.112 +lemma mult_mono:
   6.113 +  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
   6.114 +     \<Longrightarrow> a * c \<le> b * d"
   6.115 +apply (erule mult_right_mono [THEN order_trans], assumption)
   6.116 +apply (erule mult_left_mono, assumption)
   6.117 +done
   6.118 +
   6.119 +lemma mult_mono':
   6.120 +  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
   6.121 +     \<Longrightarrow> a * c \<le> b * d"
   6.122 +apply (rule mult_mono)
   6.123 +apply (fast intro: order_trans)+
   6.124 +done
   6.125 +
   6.126 +end
   6.127  
   6.128  class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
   6.129    + semiring + comm_monoid_add + cancel_ab_semigroup_add
   6.130 @@ -243,10 +322,37 @@
   6.131  subclass (in pordered_cancel_semiring) semiring_0_cancel by unfold_locales
   6.132  subclass (in pordered_cancel_semiring) pordered_semiring by unfold_locales
   6.133  
   6.134 -class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
   6.135 +context pordered_cancel_semiring
   6.136  begin
   6.137  
   6.138 -subclass pordered_cancel_semiring by unfold_locales
   6.139 +lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   6.140 +  by (drule mult_left_mono [of zero b], auto)
   6.141 +
   6.142 +lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
   6.143 +  by (drule mult_left_mono [of b zero], auto)
   6.144 +
   6.145 +lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   6.146 +  by (drule mult_right_mono [of b zero], auto)
   6.147 +
   6.148 +lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (0::_::pordered_cancel_semiring)" 
   6.149 +  by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   6.150 +
   6.151 +end
   6.152 +
   6.153 +class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
   6.154 +
   6.155 +subclass (in ordered_semiring) pordered_cancel_semiring by unfold_locales
   6.156 +
   6.157 +context ordered_semiring
   6.158 +begin
   6.159 +
   6.160 +lemma mult_left_less_imp_less:
   6.161 +  "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   6.162 +  by (force simp add: mult_left_mono not_le [symmetric])
   6.163 + 
   6.164 +lemma mult_right_less_imp_less:
   6.165 +  "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   6.166 +  by (force simp add: mult_right_mono not_le [symmetric])
   6.167  
   6.168  end
   6.169  
   6.170 @@ -268,8 +374,49 @@
   6.171      using mult_strict_right_mono by (cases "c = 0") auto
   6.172  qed
   6.173  
   6.174 +context ordered_semiring_strict
   6.175 +begin
   6.176 +
   6.177 +lemma mult_left_le_imp_le:
   6.178 +  "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   6.179 +  by (force simp add: mult_strict_left_mono _not_less [symmetric])
   6.180 + 
   6.181 +lemma mult_right_le_imp_le:
   6.182 +  "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   6.183 +  by (force simp add: mult_strict_right_mono not_less [symmetric])
   6.184 +
   6.185 +lemma mult_pos_pos:
   6.186 +  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
   6.187 +  by (drule mult_strict_left_mono [of zero b], auto)
   6.188 +
   6.189 +lemma mult_pos_neg:
   6.190 +  "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
   6.191 +  by (drule mult_strict_left_mono [of b zero], auto)
   6.192 +
   6.193 +lemma mult_pos_neg2:
   6.194 +  "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   6.195 +  by (drule mult_strict_right_mono [of b zero], auto)
   6.196 +
   6.197 +lemma zero_less_mult_pos:
   6.198 +  "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   6.199 +apply (cases "b\<le>0") 
   6.200 + apply (auto simp add: le_less not_less)
   6.201 +apply (drule_tac mult_pos_neg [of a b]) 
   6.202 + apply (auto dest: less_not_sym)
   6.203 +done
   6.204 +
   6.205 +lemma zero_less_mult_pos2:
   6.206 +  "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
   6.207 +apply (cases "b\<le>0") 
   6.208 + apply (auto simp add: le_less not_less)
   6.209 +apply (drule_tac mult_pos_neg2 [of a b]) 
   6.210 + apply (auto dest: less_not_sym)
   6.211 +done
   6.212 +
   6.213 +end
   6.214 +
   6.215  class mult_mono1 = times + zero + ord +
   6.216 -  assumes mult_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   6.217 +  assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   6.218  
   6.219  class pordered_comm_semiring = comm_semiring_0
   6.220    + pordered_ab_semigroup_add + mult_mono1
   6.221 @@ -289,7 +436,7 @@
   6.222  proof unfold_locales
   6.223    fix a b c :: 'a
   6.224    assume "a \<le> b" "0 \<le> c"
   6.225 -  thus "c * a \<le> c * b" by (rule mult_mono)
   6.226 +  thus "c * a \<le> c * b" by (rule mult_mono1)
   6.227    thus "a * c \<le> b * c" by (simp only: mult_commute)
   6.228  qed
   6.229  
   6.230 @@ -314,9 +461,49 @@
   6.231  qed
   6.232  
   6.233  class pordered_ring = ring + pordered_cancel_semiring 
   6.234 +
   6.235 +subclass (in pordered_ring) pordered_ab_group_add by unfold_locales
   6.236 +
   6.237 +context pordered_ring
   6.238  begin
   6.239  
   6.240 -subclass pordered_ab_group_add by unfold_locales
   6.241 +lemmas ring_simps = ring_simps group_simps
   6.242 +
   6.243 +lemma less_add_iff1:
   6.244 +  "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
   6.245 +  by (simp add: ring_simps)
   6.246 +
   6.247 +lemma less_add_iff2:
   6.248 +  "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d"
   6.249 +  by (simp add: ring_simps)
   6.250 +
   6.251 +lemma le_add_iff1:
   6.252 +  "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d"
   6.253 +  by (simp add: ring_simps)
   6.254 +
   6.255 +lemma le_add_iff2:
   6.256 +  "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d"
   6.257 +  by (simp add: ring_simps)
   6.258 +
   6.259 +lemma mult_left_mono_neg:
   6.260 +  "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
   6.261 +  apply (drule mult_left_mono [of _ _ "uminus c"])
   6.262 +  apply (simp_all add: minus_mult_left [symmetric]) 
   6.263 +  done
   6.264 +
   6.265 +lemma mult_right_mono_neg:
   6.266 +  "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
   6.267 +  apply (drule mult_right_mono [of _ _ "uminus c"])
   6.268 +  apply (simp_all add: minus_mult_right [symmetric]) 
   6.269 +  done
   6.270 +
   6.271 +lemma mult_nonpos_nonpos:
   6.272 +  "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   6.273 +  by (drule mult_right_mono_neg [of a zero b]) auto
   6.274 +
   6.275 +lemma split_mult_pos_le:
   6.276 +  "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
   6.277 +  by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   6.278  
   6.279  end
   6.280  
   6.281 @@ -331,12 +518,10 @@
   6.282  class sgn_if = sgn + zero + one + minus + ord +
   6.283    assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   6.284  
   6.285 -(* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
   6.286 -   Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
   6.287 - *)
   6.288 -class ordered_ring = ring + ordered_semiring + lordered_ab_group + abs_if
   6.289 -
   6.290 --- {*FIXME: continue localization here*}
   6.291 +class ordered_ring = ring + ordered_semiring
   6.292 +  + lordered_ab_group + abs_if
   6.293 +  -- {*FIXME: should inherit from ordered_ab_group_add rather than
   6.294 +         lordered_ab_group*}
   6.295  
   6.296  instance ordered_ring \<subseteq> lordered_ring
   6.297  proof 
   6.298 @@ -345,167 +530,44 @@
   6.299      by (simp only: abs_if sup_eq_if)
   6.300  qed
   6.301  
   6.302 -class ordered_ring_strict =
   6.303 -  ring + ordered_semiring_strict + lordered_ab_group + abs_if
   6.304 -
   6.305 -instance ordered_ring_strict \<subseteq> ordered_ring ..
   6.306 -
   6.307 -class pordered_comm_ring = comm_ring + pordered_comm_semiring
   6.308 -
   6.309 -instance pordered_comm_ring \<subseteq> pordered_ring ..
   6.310 -
   6.311 -instance pordered_comm_ring \<subseteq> pordered_cancel_comm_semiring ..
   6.312 -
   6.313 -class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   6.314 -  (*previously ordered_semiring*)
   6.315 -  assumes zero_less_one [simp]: "0 < 1"
   6.316 -
   6.317 -lemma pos_add_strict:
   6.318 -  fixes a b c :: "'a\<Colon>ordered_semidom"
   6.319 -  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   6.320 -  using add_strict_mono [of 0 a b c] by simp
   6.321 -
   6.322 -class ordered_idom =
   6.323 -  comm_ring_1 +
   6.324 -  ordered_comm_semiring_strict +
   6.325 -  lordered_ab_group +
   6.326 -  abs_if + sgn_if
   6.327 -  (*previously ordered_ring*)
   6.328 -
   6.329 -instance ordered_idom \<subseteq> ordered_ring_strict ..
   6.330 -
   6.331 -instance ordered_idom \<subseteq> pordered_comm_ring ..
   6.332 -
   6.333 -class ordered_field = field + ordered_idom
   6.334 -
   6.335 -lemma linorder_neqE_ordered_idom:
   6.336 -  fixes x y :: "'a :: ordered_idom"
   6.337 -  assumes "x \<noteq> y" obtains "x < y" | "y < x"
   6.338 -  using assms by (rule linorder_neqE)
   6.339 +(* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
   6.340 +   Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
   6.341 + *)
   6.342 +class ordered_ring_strict = ring + ordered_semiring_strict
   6.343 +  + lordered_ab_group + abs_if
   6.344 +  -- {*FIXME: should inherit from ordered_ab_group_add rather than
   6.345 +         lordered_ab_group*}
   6.346  
   6.347 -lemma eq_add_iff1:
   6.348 -  "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
   6.349 -by (simp add: ring_simps)
   6.350 -
   6.351 -lemma eq_add_iff2:
   6.352 -  "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"
   6.353 -by (simp add: ring_simps)
   6.354 -
   6.355 -lemma less_add_iff1:
   6.356 -  "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))"
   6.357 -by (simp add: ring_simps)
   6.358 -
   6.359 -lemma less_add_iff2:
   6.360 -  "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))"
   6.361 -by (simp add: ring_simps)
   6.362 -
   6.363 -lemma le_add_iff1:
   6.364 -  "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))"
   6.365 -by (simp add: ring_simps)
   6.366 +instance ordered_ring_strict \<subseteq> ordered_ring by intro_classes
   6.367  
   6.368 -lemma le_add_iff2:
   6.369 -  "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))"
   6.370 -by (simp add: ring_simps)
   6.371 -
   6.372 -
   6.373 -subsection {* Ordering Rules for Multiplication *}
   6.374 -
   6.375 -lemma mult_left_le_imp_le:
   6.376 -  "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
   6.377 -by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
   6.378 - 
   6.379 -lemma mult_right_le_imp_le:
   6.380 -  "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"
   6.381 -by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
   6.382 -
   6.383 -lemma mult_left_less_imp_less:
   6.384 -  "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   6.385 -by (force simp add: mult_left_mono linorder_not_le [symmetric])
   6.386 - 
   6.387 -lemma mult_right_less_imp_less:
   6.388 -  "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   6.389 -by (force simp add: mult_right_mono linorder_not_le [symmetric])
   6.390 +context ordered_ring_strict
   6.391 +begin
   6.392  
   6.393  lemma mult_strict_left_mono_neg:
   6.394 -  "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)"
   6.395 -apply (drule mult_strict_left_mono [of _ _ "-c"])
   6.396 -apply (simp_all add: minus_mult_left [symmetric]) 
   6.397 -done
   6.398 -
   6.399 -lemma mult_left_mono_neg:
   6.400 -  "[|b \<le> a; c \<le> 0|] ==> c * a \<le>  c * (b::'a::pordered_ring)"
   6.401 -apply (drule mult_left_mono [of _ _ "-c"])
   6.402 -apply (simp_all add: minus_mult_left [symmetric]) 
   6.403 -done
   6.404 +  "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
   6.405 +  apply (drule mult_strict_left_mono [of _ _ "uminus c"])
   6.406 +  apply (simp_all add: minus_mult_left [symmetric]) 
   6.407 +  done
   6.408  
   6.409  lemma mult_strict_right_mono_neg:
   6.410 -  "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)"
   6.411 -apply (drule mult_strict_right_mono [of _ _ "-c"])
   6.412 -apply (simp_all add: minus_mult_right [symmetric]) 
   6.413 -done
   6.414 -
   6.415 -lemma mult_right_mono_neg:
   6.416 -  "[|b \<le> a; c \<le> 0|] ==> a * c \<le>  (b::'a::pordered_ring) * c"
   6.417 -apply (drule mult_right_mono [of _ _ "-c"])
   6.418 -apply (simp)
   6.419 -apply (simp_all add: minus_mult_right [symmetric]) 
   6.420 -done
   6.421 -
   6.422 -
   6.423 -subsection{* Products of Signs *}
   6.424 -
   6.425 -lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
   6.426 -by (drule mult_strict_left_mono [of 0 b], auto)
   6.427 -
   6.428 -lemma mult_nonneg_nonneg: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"
   6.429 -by (drule mult_left_mono [of 0 b], auto)
   6.430 -
   6.431 -lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> a*b < 0"
   6.432 -by (drule mult_strict_left_mono [of b 0], auto)
   6.433 -
   6.434 -lemma mult_nonneg_nonpos: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"
   6.435 -by (drule mult_left_mono [of b 0], auto)
   6.436 +  "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c"
   6.437 +  apply (drule mult_strict_right_mono [of _ _ "uminus c"])
   6.438 +  apply (simp_all add: minus_mult_right [symmetric]) 
   6.439 +  done
   6.440  
   6.441 -lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0" 
   6.442 -by (drule mult_strict_right_mono[of b 0], auto)
   6.443 -
   6.444 -lemma mult_nonneg_nonpos2: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0" 
   6.445 -by (drule mult_right_mono[of b 0], auto)
   6.446 -
   6.447 -lemma mult_neg_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b"
   6.448 -by (drule mult_strict_right_mono_neg, auto)
   6.449 -
   6.450 -lemma mult_nonpos_nonpos: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b"
   6.451 -by (drule mult_right_mono_neg[of a 0 b ], auto)
   6.452 +lemma mult_neg_neg:
   6.453 +  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
   6.454 +  by (drule mult_strict_right_mono_neg, auto)
   6.455  
   6.456 -lemma zero_less_mult_pos:
   6.457 -     "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)"
   6.458 -apply (cases "b\<le>0") 
   6.459 - apply (auto simp add: order_le_less linorder_not_less)
   6.460 -apply (drule_tac mult_pos_neg [of a b]) 
   6.461 - apply (auto dest: order_less_not_sym)
   6.462 -done
   6.463 -
   6.464 -lemma zero_less_mult_pos2:
   6.465 -     "[| 0 < b*a; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)"
   6.466 -apply (cases "b\<le>0") 
   6.467 - apply (auto simp add: order_le_less linorder_not_less)
   6.468 -apply (drule_tac mult_pos_neg2 [of a b]) 
   6.469 - apply (auto dest: order_less_not_sym)
   6.470 -done
   6.471 +end
   6.472  
   6.473  lemma zero_less_mult_iff:
   6.474 -     "((0::'a::ordered_ring_strict) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"
   6.475 -apply (auto simp add: order_le_less linorder_not_less mult_pos_pos 
   6.476 -  mult_neg_neg)
   6.477 -apply (blast dest: zero_less_mult_pos) 
   6.478 -apply (blast dest: zero_less_mult_pos2)
   6.479 -done
   6.480 -
   6.481 -lemma mult_eq_0_iff [simp]:
   6.482 -  fixes a b :: "'a::ring_no_zero_divisors"
   6.483 -  shows "(a * b = 0) = (a = 0 \<or> b = 0)"
   6.484 -by (cases "a = 0 \<or> b = 0", auto dest: no_zero_divisors)
   6.485 +  fixes a :: "'a::ordered_ring_strict"
   6.486 +  shows "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   6.487 +  apply (auto simp add: le_less not_less mult_pos_pos mult_neg_neg)
   6.488 +  apply (blast dest: zero_less_mult_pos) 
   6.489 +  apply (blast dest: zero_less_mult_pos2)
   6.490 +  done
   6.491  
   6.492  instance ordered_ring_strict \<subseteq> ring_no_zero_divisors
   6.493  apply intro_classes
   6.494 @@ -530,18 +592,57 @@
   6.495  apply (force simp add: minus_mult_left[symmetric]) 
   6.496  done
   6.497  
   6.498 -lemma split_mult_pos_le: "(0 \<le> a & 0 \<le> b) | (a \<le> 0 & b \<le> 0) \<Longrightarrow> 0 \<le> a * (b::_::pordered_ring)"
   6.499 -by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   6.500 -
   6.501 -lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (0::_::pordered_cancel_semiring)" 
   6.502 -by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   6.503 -
   6.504  lemma zero_le_square[simp]: "(0::'a::ordered_ring_strict) \<le> a*a"
   6.505  by (simp add: zero_le_mult_iff linorder_linear)
   6.506  
   6.507  lemma not_square_less_zero[simp]: "\<not> (a * a < (0::'a::ordered_ring_strict))"
   6.508  by (simp add: not_less)
   6.509  
   6.510 +text{*This list of rewrites simplifies ring terms by multiplying
   6.511 +everything out and bringing sums and products into a canonical form
   6.512 +(by ordered rewriting). As a result it decides ring equalities but
   6.513 +also helps with inequalities. *}
   6.514 +lemmas ring_simps = group_simps ring_distribs
   6.515 +
   6.516 +
   6.517 +class pordered_comm_ring = comm_ring + pordered_comm_semiring
   6.518 +
   6.519 +subclass (in pordered_comm_ring) pordered_ring by unfold_locales
   6.520 +
   6.521 +subclass (in pordered_comm_ring) pordered_cancel_comm_semiring by unfold_locales
   6.522 +
   6.523 +class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   6.524 +  (*previously ordered_semiring*)
   6.525 +  assumes zero_less_one [simp]: "0 < 1"
   6.526 +begin
   6.527 +
   6.528 +lemma pos_add_strict:
   6.529 +  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   6.530 +  using add_strict_mono [of zero a b c] by simp
   6.531 +
   6.532 +end
   6.533 +
   6.534 +class ordered_idom =
   6.535 +  comm_ring_1 +
   6.536 +  ordered_comm_semiring_strict +
   6.537 +  lordered_ab_group +
   6.538 +  abs_if + sgn_if
   6.539 +  (*previously ordered_ring*)
   6.540 +
   6.541 +instance ordered_idom \<subseteq> ordered_ring_strict ..
   6.542 +
   6.543 +instance ordered_idom \<subseteq> pordered_comm_ring ..
   6.544 +
   6.545 +class ordered_field = field + ordered_idom
   6.546 +
   6.547 +lemma linorder_neqE_ordered_idom:
   6.548 +  fixes x y :: "'a :: ordered_idom"
   6.549 +  assumes "x \<noteq> y" obtains "x < y" | "y < x"
   6.550 +  using assms by (rule linorder_neqE)
   6.551 +
   6.552 +-- {* FIXME continue localization here *}
   6.553 +
   6.554 +
   6.555  text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}
   6.556        theorems available to members of @{term ordered_idom} *}
   6.557  
   6.558 @@ -587,20 +688,6 @@
   6.559  apply (blast intro: order_le_less_trans)+
   6.560  done
   6.561  
   6.562 -lemma mult_mono:
   6.563 -     "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|] 
   6.564 -      ==> a * c  \<le>  b * (d::'a::pordered_semiring)"
   6.565 -apply (erule mult_right_mono [THEN order_trans], assumption)
   6.566 -apply (erule mult_left_mono, assumption)
   6.567 -done
   6.568 -
   6.569 -lemma mult_mono':
   6.570 -     "[|a \<le> b; c \<le> d; 0 \<le> a; 0 \<le> c|] 
   6.571 -      ==> a * c  \<le>  b * (d::'a::pordered_semiring)"
   6.572 -apply (rule mult_mono)
   6.573 -apply (fast intro: order_trans)+
   6.574 -done
   6.575 -
   6.576  lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)"
   6.577  apply (insert mult_strict_mono [of 1 m 1 n]) 
   6.578  apply (simp add:  order_less_trans [OF zero_less_one]) 
   6.579 @@ -805,43 +892,6 @@
   6.580      mult_cancel_left1 mult_cancel_left2
   6.581  
   6.582  
   6.583 -subsection {* Fields *}
   6.584 -
   6.585 -lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
   6.586 -proof
   6.587 -  assume neq: "b \<noteq> 0"
   6.588 -  {
   6.589 -    hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
   6.590 -    also assume "a / b = 1"
   6.591 -    finally show "a = b" by simp
   6.592 -  next
   6.593 -    assume "a = b"
   6.594 -    with neq show "a / b = 1" by (simp add: divide_inverse)
   6.595 -  }
   6.596 -qed
   6.597 -
   6.598 -lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
   6.599 -by (simp add: divide_inverse)
   6.600 -
   6.601 -lemma divide_self[simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
   6.602 -  by (simp add: divide_inverse)
   6.603 -
   6.604 -lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
   6.605 -by (simp add: divide_inverse)
   6.606 -
   6.607 -lemma divide_self_if [simp]:
   6.608 -     "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
   6.609 -  by (simp add: divide_self)
   6.610 -
   6.611 -lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
   6.612 -by (simp add: divide_inverse)
   6.613 -
   6.614 -lemma inverse_eq_divide: "inverse (a::'a::field) = 1/a"
   6.615 -by (simp add: divide_inverse)
   6.616 -
   6.617 -lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
   6.618 -by (simp add: divide_inverse ring_distribs) 
   6.619 -
   6.620  (* what ordering?? this is a straight instance of mult_eq_0_iff
   6.621  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
   6.622        of an ordering.*}
   6.623 @@ -1871,9 +1921,11 @@
   6.624  lemma frac_le: "(0::'a::ordered_field) <= x ==> 
   6.625      x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
   6.626    apply (rule mult_imp_div_pos_le)
   6.627 -  apply simp;
   6.628 -  apply (subst times_divide_eq_left);
   6.629 +  apply simp
   6.630 +  apply (subst times_divide_eq_left)
   6.631    apply (rule mult_imp_le_div_pos, assumption)
   6.632 +  thm mult_mono
   6.633 +  thm mult_mono'
   6.634    apply (rule mult_mono)
   6.635    apply simp_all
   6.636  done