merged
authorhaftmann
Fri Apr 23 19:32:37 2010 +0200 (2010-04-23)
changeset 36313f2753d6b0859
parent 36295 9eaaa05c972c
parent 36312 26eea417ccc4
child 36314 cf1abb4daae6
merged
     1.1 --- a/NEWS	Fri Apr 23 16:12:57 2010 +0200
     1.2 +++ b/NEWS	Fri Apr 23 19:32:37 2010 +0200
     1.3 @@ -112,6 +112,13 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Abstract algebra:
     1.8 +  * class division_by_zero includes division_ring;
     1.9 +  * numerous lemmas have been ported from field to division_ring;
    1.10 +  * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
    1.11 +
    1.12 +  INCOMPATIBILITY.
    1.13 +
    1.14  * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
    1.15  provides abstract red-black tree type which is backed by RBT_Impl
    1.16  as implementation.  INCOMPATIBILTY.
     2.1 --- a/src/HOL/Big_Operators.thy	Fri Apr 23 16:12:57 2010 +0200
     2.2 +++ b/src/HOL/Big_Operators.thy	Fri Apr 23 19:32:37 2010 +0200
     2.3 @@ -555,7 +555,7 @@
     2.4  qed
     2.5  
     2.6  lemma setsum_mono2:
     2.7 -fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}"
     2.8 +fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
     2.9  assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
    2.10  shows "setsum f A \<le> setsum f B"
    2.11  proof -
    2.12 @@ -1030,7 +1030,7 @@
    2.13  lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
    2.14    (setprod f (A - {a}) :: 'a :: {field}) =
    2.15    (if a:A then setprod f A / f a else setprod f A)"
    2.16 -by (erule finite_induct) (auto simp add: insert_Diff_if)
    2.17 +  by (erule finite_induct) (auto simp add: insert_Diff_if)
    2.18  
    2.19  lemma setprod_inversef: 
    2.20    fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
     3.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Apr 23 16:12:57 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Apr 23 19:32:37 2010 +0200
     3.3 @@ -33,7 +33,7 @@
     3.4               @{thm "real_of_nat_number_of"},
     3.5               @{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"},
     3.6               @{thm "real_of_int_zero"}, @{thm "real_of_nat_zero"},
     3.7 -             @{thm "Fields.divide_zero"}, 
     3.8 +             @{thm "divide_zero"}, 
     3.9               @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
    3.10               @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
    3.11               @{thm "diff_def"}, @{thm "minus_divide_left"}]
     4.1 --- a/src/HOL/Fields.thy	Fri Apr 23 16:12:57 2010 +0200
     4.2 +++ b/src/HOL/Fields.thy	Fri Apr 23 19:32:37 2010 +0200
     4.3 @@ -31,34 +31,6 @@
     4.4  
     4.5  subclass idom ..
     4.6  
     4.7 -lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
     4.8 -proof
     4.9 -  assume neq: "b \<noteq> 0"
    4.10 -  {
    4.11 -    hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
    4.12 -    also assume "a / b = 1"
    4.13 -    finally show "a = b" by simp
    4.14 -  next
    4.15 -    assume "a = b"
    4.16 -    with neq show "a / b = 1" by (simp add: divide_inverse)
    4.17 -  }
    4.18 -qed
    4.19 -
    4.20 -lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
    4.21 -by (simp add: divide_inverse)
    4.22 -
    4.23 -lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
    4.24 -by (simp add: divide_inverse)
    4.25 -
    4.26 -lemma divide_zero_left [simp]: "0 / a = 0"
    4.27 -by (simp add: divide_inverse)
    4.28 -
    4.29 -lemma inverse_eq_divide: "inverse a = 1 / a"
    4.30 -by (simp add: divide_inverse)
    4.31 -
    4.32 -lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
    4.33 -by (simp add: divide_inverse algebra_simps)
    4.34 -
    4.35  text{*There is no slick version using division by zero.*}
    4.36  lemma inverse_add:
    4.37    "[| a \<noteq> 0;  b \<noteq> 0 |]
    4.38 @@ -80,14 +52,8 @@
    4.39    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
    4.40  by (simp add: mult_commute [of _ c])
    4.41  
    4.42 -lemma divide_1 [simp]: "a / 1 = a"
    4.43 -by (simp add: divide_inverse)
    4.44 -
    4.45 -lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
    4.46 -by (simp add: divide_inverse mult_assoc)
    4.47 -
    4.48 -lemma times_divide_eq_left: "(b / c) * a = (b * a) / c"
    4.49 -by (simp add: divide_inverse mult_ac)
    4.50 +lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
    4.51 +  by (simp add: divide_inverse mult_ac)
    4.52  
    4.53  text {* These are later declared as simp rules. *}
    4.54  lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
    4.55 @@ -108,7 +74,7 @@
    4.56  
    4.57  lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
    4.58    "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
    4.59 -using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
    4.60 +  using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
    4.61  
    4.62  lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
    4.63    "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
    4.64 @@ -130,58 +96,21 @@
    4.65    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
    4.66  using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
    4.67  
    4.68 -lemma minus_divide_left: "- (a / b) = (-a) / b"
    4.69 -by (simp add: divide_inverse)
    4.70 -
    4.71 -lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
    4.72 -by (simp add: divide_inverse nonzero_inverse_minus_eq)
    4.73 -
    4.74 -lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
    4.75 -by (simp add: divide_inverse nonzero_inverse_minus_eq)
    4.76 -
    4.77 -lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
    4.78 -by (simp add: divide_inverse)
    4.79 -
    4.80 -lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
    4.81 -by (simp add: diff_minus add_divide_distrib)
    4.82 -
    4.83  lemma add_divide_eq_iff:
    4.84    "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
    4.85 -by (simp add: add_divide_distrib)
    4.86 +  by (simp add: add_divide_distrib)
    4.87  
    4.88  lemma divide_add_eq_iff:
    4.89    "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
    4.90 -by (simp add: add_divide_distrib)
    4.91 +  by (simp add: add_divide_distrib)
    4.92  
    4.93  lemma diff_divide_eq_iff:
    4.94    "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
    4.95 -by (simp add: diff_divide_distrib)
    4.96 +  by (simp add: diff_divide_distrib)
    4.97  
    4.98  lemma divide_diff_eq_iff:
    4.99    "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
   4.100 -by (simp add: diff_divide_distrib)
   4.101 -
   4.102 -lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
   4.103 -proof -
   4.104 -  assume [simp]: "c \<noteq> 0"
   4.105 -  have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
   4.106 -  also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
   4.107 -  finally show ?thesis .
   4.108 -qed
   4.109 -
   4.110 -lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
   4.111 -proof -
   4.112 -  assume [simp]: "c \<noteq> 0"
   4.113 -  have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
   4.114 -  also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc) 
   4.115 -  finally show ?thesis .
   4.116 -qed
   4.117 -
   4.118 -lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
   4.119 -by simp
   4.120 -
   4.121 -lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
   4.122 -by (erule subst, simp)
   4.123 +  by (simp add: diff_divide_distrib)
   4.124  
   4.125  lemmas field_eq_simps[no_atp] = algebra_simps
   4.126    (* pull / out*)
   4.127 @@ -189,9 +118,7 @@
   4.128    diff_divide_eq_iff divide_diff_eq_iff
   4.129    (* multiply eqn *)
   4.130    nonzero_eq_divide_eq nonzero_divide_eq_eq
   4.131 -(* is added later:
   4.132    times_divide_eq_left times_divide_eq_right
   4.133 -*)
   4.134  
   4.135  text{*An example:*}
   4.136  lemma "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f\<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
   4.137 @@ -202,68 +129,21 @@
   4.138  
   4.139  lemma diff_frac_eq:
   4.140    "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
   4.141 -by (simp add: field_eq_simps times_divide_eq)
   4.142 +  by (simp add: field_eq_simps times_divide_eq)
   4.143  
   4.144  lemma frac_eq_eq:
   4.145    "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
   4.146 -by (simp add: field_eq_simps times_divide_eq)
   4.147 +  by (simp add: field_eq_simps times_divide_eq)
   4.148  
   4.149  end
   4.150  
   4.151 -class division_by_zero = zero + inverse +
   4.152 -  assumes inverse_zero [simp]: "inverse 0 = 0"
   4.153 -
   4.154 -lemma divide_zero [simp]:
   4.155 -  "a / 0 = (0::'a::{field,division_by_zero})"
   4.156 -by (simp add: divide_inverse)
   4.157 -
   4.158 -lemma divide_self_if [simp]:
   4.159 -  "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
   4.160 -by simp
   4.161 -
   4.162 -class linordered_field = field + linordered_idom
   4.163 -
   4.164 -lemma inverse_nonzero_iff_nonzero [simp]:
   4.165 -   "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
   4.166 -by (force dest: inverse_zero_imp_zero) 
   4.167 -
   4.168 -lemma inverse_minus_eq [simp]:
   4.169 -   "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
   4.170 -proof cases
   4.171 -  assume "a=0" thus ?thesis by simp
   4.172 -next
   4.173 -  assume "a\<noteq>0" 
   4.174 -  thus ?thesis by (simp add: nonzero_inverse_minus_eq)
   4.175 -qed
   4.176 -
   4.177 -lemma inverse_eq_imp_eq:
   4.178 -  "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
   4.179 -apply (cases "a=0 | b=0") 
   4.180 - apply (force dest!: inverse_zero_imp_zero
   4.181 -              simp add: eq_commute [of "0::'a"])
   4.182 -apply (force dest!: nonzero_inverse_eq_imp_eq) 
   4.183 -done
   4.184 -
   4.185 -lemma inverse_eq_iff_eq [simp]:
   4.186 -  "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
   4.187 -by (force dest!: inverse_eq_imp_eq)
   4.188 -
   4.189 -lemma inverse_inverse_eq [simp]:
   4.190 -     "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
   4.191 -  proof cases
   4.192 -    assume "a=0" thus ?thesis by simp
   4.193 -  next
   4.194 -    assume "a\<noteq>0" 
   4.195 -    thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
   4.196 -  qed
   4.197 -
   4.198  text{*This version builds in division by zero while also re-orienting
   4.199        the right-hand side.*}
   4.200  lemma inverse_mult_distrib [simp]:
   4.201       "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
   4.202    proof cases
   4.203      assume "a \<noteq> 0 & b \<noteq> 0" 
   4.204 -    thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
   4.205 +    thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
   4.206    next
   4.207      assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
   4.208      thus ?thesis by force
   4.209 @@ -271,10 +151,10 @@
   4.210  
   4.211  lemma inverse_divide [simp]:
   4.212    "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
   4.213 -by (simp add: divide_inverse mult_commute)
   4.214 +  by (simp add: divide_inverse mult_commute)
   4.215  
   4.216  
   4.217 -subsection {* Calculations with fractions *}
   4.218 +text {* Calculations with fractions *}
   4.219  
   4.220  text{* There is a whole bunch of simp-rules just for class @{text
   4.221  field} but none for class @{text field} and @{text nonzero_divides}
   4.222 @@ -301,7 +181,7 @@
   4.223  by (simp add: divide_inverse mult_assoc)
   4.224  
   4.225  
   4.226 -subsubsection{*Special Cancellation Simprules for Division*}
   4.227 +text {*Special Cancellation Simprules for Division*}
   4.228  
   4.229  lemma mult_divide_mult_cancel_left_if[simp,no_atp]:
   4.230  fixes c :: "'a :: {field,division_by_zero}"
   4.231 @@ -309,7 +189,7 @@
   4.232  by (simp add: mult_divide_mult_cancel_left)
   4.233  
   4.234  
   4.235 -subsection {* Division and Unary Minus *}
   4.236 +text {* Division and Unary Minus *}
   4.237  
   4.238  lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
   4.239  by (simp add: divide_inverse)
   4.240 @@ -332,40 +212,74 @@
   4.241    "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
   4.242  by (force simp add: nonzero_divide_eq_eq)
   4.243  
   4.244 +lemma inverse_eq_1_iff [simp]:
   4.245 +  "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
   4.246 +by (insert inverse_eq_iff_eq [of x 1], simp) 
   4.247  
   4.248 -subsection {* Ordered Fields *}
   4.249 +lemma divide_eq_0_iff [simp,no_atp]:
   4.250 +     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
   4.251 +by (simp add: divide_inverse)
   4.252 +
   4.253 +lemma divide_cancel_right [simp,no_atp]:
   4.254 +     "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
   4.255 +apply (cases "c=0", simp)
   4.256 +apply (simp add: divide_inverse)
   4.257 +done
   4.258 +
   4.259 +lemma divide_cancel_left [simp,no_atp]:
   4.260 +     "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
   4.261 +apply (cases "c=0", simp)
   4.262 +apply (simp add: divide_inverse)
   4.263 +done
   4.264 +
   4.265 +lemma divide_eq_1_iff [simp,no_atp]:
   4.266 +     "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   4.267 +apply (cases "b=0", simp)
   4.268 +apply (simp add: right_inverse_eq)
   4.269 +done
   4.270 +
   4.271 +lemma one_eq_divide_iff [simp,no_atp]:
   4.272 +     "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   4.273 +by (simp add: eq_commute [of 1])
   4.274 +
   4.275 +
   4.276 +text {* Ordered Fields *}
   4.277 +
   4.278 +class linordered_field = field + linordered_idom
   4.279 +begin
   4.280  
   4.281  lemma positive_imp_inverse_positive: 
   4.282 -assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::linordered_field)"
   4.283 +  assumes a_gt_0: "0 < a" 
   4.284 +  shows "0 < inverse a"
   4.285  proof -
   4.286    have "0 < a * inverse a" 
   4.287 -    by (simp add: a_gt_0 [THEN order_less_imp_not_eq2])
   4.288 +    by (simp add: a_gt_0 [THEN less_imp_not_eq2])
   4.289    thus "0 < inverse a" 
   4.290 -    by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
   4.291 +    by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff)
   4.292  qed
   4.293  
   4.294  lemma negative_imp_inverse_negative:
   4.295 -  "a < 0 ==> inverse a < (0::'a::linordered_field)"
   4.296 -by (insert positive_imp_inverse_positive [of "-a"], 
   4.297 -    simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
   4.298 +  "a < 0 \<Longrightarrow> inverse a < 0"
   4.299 +  by (insert positive_imp_inverse_positive [of "-a"], 
   4.300 +    simp add: nonzero_inverse_minus_eq less_imp_not_eq)
   4.301  
   4.302  lemma inverse_le_imp_le:
   4.303 -assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
   4.304 -shows "b \<le> (a::'a::linordered_field)"
   4.305 +  assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
   4.306 +  shows "b \<le> a"
   4.307  proof (rule classical)
   4.308    assume "~ b \<le> a"
   4.309    hence "a < b"  by (simp add: linorder_not_le)
   4.310 -  hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
   4.311 +  hence bpos: "0 < b"  by (blast intro: apos less_trans)
   4.312    hence "a * inverse a \<le> a * inverse b"
   4.313 -    by (simp add: apos invle order_less_imp_le mult_left_mono)
   4.314 +    by (simp add: apos invle less_imp_le mult_left_mono)
   4.315    hence "(a * inverse a) * b \<le> (a * inverse b) * b"
   4.316 -    by (simp add: bpos order_less_imp_le mult_right_mono)
   4.317 -  thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
   4.318 +    by (simp add: bpos less_imp_le mult_right_mono)
   4.319 +  thus "b \<le> a"  by (simp add: mult_assoc apos bpos less_imp_not_eq2)
   4.320  qed
   4.321  
   4.322  lemma inverse_positive_imp_positive:
   4.323 -assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
   4.324 -shows "0 < (a::'a::linordered_field)"
   4.325 +  assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
   4.326 +  shows "0 < a"
   4.327  proof -
   4.328    have "0 < inverse (inverse a)"
   4.329      using inv_gt_0 by (rule positive_imp_inverse_positive)
   4.330 @@ -373,21 +287,392 @@
   4.331      using nz by (simp add: nonzero_inverse_inverse_eq)
   4.332  qed
   4.333  
   4.334 +lemma inverse_negative_imp_negative:
   4.335 +  assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0"
   4.336 +  shows "a < 0"
   4.337 +proof -
   4.338 +  have "inverse (inverse a) < 0"
   4.339 +    using inv_less_0 by (rule negative_imp_inverse_negative)
   4.340 +  thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
   4.341 +qed
   4.342 +
   4.343 +lemma linordered_field_no_lb:
   4.344 +  "\<forall>x. \<exists>y. y < x"
   4.345 +proof
   4.346 +  fix x::'a
   4.347 +  have m1: "- (1::'a) < 0" by simp
   4.348 +  from add_strict_right_mono[OF m1, where c=x] 
   4.349 +  have "(- 1) + x < x" by simp
   4.350 +  thus "\<exists>y. y < x" by blast
   4.351 +qed
   4.352 +
   4.353 +lemma linordered_field_no_ub:
   4.354 +  "\<forall> x. \<exists>y. y > x"
   4.355 +proof
   4.356 +  fix x::'a
   4.357 +  have m1: " (1::'a) > 0" by simp
   4.358 +  from add_strict_right_mono[OF m1, where c=x] 
   4.359 +  have "1 + x > x" by simp
   4.360 +  thus "\<exists>y. y > x" by blast
   4.361 +qed
   4.362 +
   4.363 +lemma less_imp_inverse_less:
   4.364 +  assumes less: "a < b" and apos:  "0 < a"
   4.365 +  shows "inverse b < inverse a"
   4.366 +proof (rule ccontr)
   4.367 +  assume "~ inverse b < inverse a"
   4.368 +  hence "inverse a \<le> inverse b" by simp
   4.369 +  hence "~ (a < b)"
   4.370 +    by (simp add: not_less inverse_le_imp_le [OF _ apos])
   4.371 +  thus False by (rule notE [OF _ less])
   4.372 +qed
   4.373 +
   4.374 +lemma inverse_less_imp_less:
   4.375 +  "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a"
   4.376 +apply (simp add: less_le [of "inverse a"] less_le [of "b"])
   4.377 +apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
   4.378 +done
   4.379 +
   4.380 +text{*Both premises are essential. Consider -1 and 1.*}
   4.381 +lemma inverse_less_iff_less [simp,no_atp]:
   4.382 +  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
   4.383 +  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
   4.384 +
   4.385 +lemma le_imp_inverse_le:
   4.386 +  "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
   4.387 +  by (force simp add: le_less less_imp_inverse_less)
   4.388 +
   4.389 +lemma inverse_le_iff_le [simp,no_atp]:
   4.390 +  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   4.391 +  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
   4.392 +
   4.393 +
   4.394 +text{*These results refer to both operands being negative.  The opposite-sign
   4.395 +case is trivial, since inverse preserves signs.*}
   4.396 +lemma inverse_le_imp_le_neg:
   4.397 +  "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a"
   4.398 +apply (rule classical) 
   4.399 +apply (subgoal_tac "a < 0") 
   4.400 + prefer 2 apply force
   4.401 +apply (insert inverse_le_imp_le [of "-b" "-a"])
   4.402 +apply (simp add: nonzero_inverse_minus_eq) 
   4.403 +done
   4.404 +
   4.405 +lemma less_imp_inverse_less_neg:
   4.406 +   "a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a"
   4.407 +apply (subgoal_tac "a < 0") 
   4.408 + prefer 2 apply (blast intro: less_trans) 
   4.409 +apply (insert less_imp_inverse_less [of "-b" "-a"])
   4.410 +apply (simp add: nonzero_inverse_minus_eq) 
   4.411 +done
   4.412 +
   4.413 +lemma inverse_less_imp_less_neg:
   4.414 +   "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a"
   4.415 +apply (rule classical) 
   4.416 +apply (subgoal_tac "a < 0") 
   4.417 + prefer 2
   4.418 + apply force
   4.419 +apply (insert inverse_less_imp_less [of "-b" "-a"])
   4.420 +apply (simp add: nonzero_inverse_minus_eq) 
   4.421 +done
   4.422 +
   4.423 +lemma inverse_less_iff_less_neg [simp,no_atp]:
   4.424 +  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
   4.425 +apply (insert inverse_less_iff_less [of "-b" "-a"])
   4.426 +apply (simp del: inverse_less_iff_less 
   4.427 +            add: nonzero_inverse_minus_eq)
   4.428 +done
   4.429 +
   4.430 +lemma le_imp_inverse_le_neg:
   4.431 +  "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
   4.432 +  by (force simp add: le_less less_imp_inverse_less_neg)
   4.433 +
   4.434 +lemma inverse_le_iff_le_neg [simp,no_atp]:
   4.435 +  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   4.436 +  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
   4.437 +
   4.438 +lemma pos_le_divide_eq: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
   4.439 +proof -
   4.440 +  assume less: "0<c"
   4.441 +  hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
   4.442 +    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   4.443 +  also have "... = (a*c \<le> b)"
   4.444 +    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   4.445 +  finally show ?thesis .
   4.446 +qed
   4.447 +
   4.448 +lemma neg_le_divide_eq: "c < 0 ==> (a \<le> b/c) = (b \<le> a*c)"
   4.449 +proof -
   4.450 +  assume less: "c<0"
   4.451 +  hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
   4.452 +    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   4.453 +  also have "... = (b \<le> a*c)"
   4.454 +    by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   4.455 +  finally show ?thesis .
   4.456 +qed
   4.457 +
   4.458 +lemma pos_less_divide_eq:
   4.459 +     "0 < c ==> (a < b/c) = (a*c < b)"
   4.460 +proof -
   4.461 +  assume less: "0<c"
   4.462 +  hence "(a < b/c) = (a*c < (b/c)*c)"
   4.463 +    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
   4.464 +  also have "... = (a*c < b)"
   4.465 +    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   4.466 +  finally show ?thesis .
   4.467 +qed
   4.468 +
   4.469 +lemma neg_less_divide_eq:
   4.470 + "c < 0 ==> (a < b/c) = (b < a*c)"
   4.471 +proof -
   4.472 +  assume less: "c<0"
   4.473 +  hence "(a < b/c) = ((b/c)*c < a*c)"
   4.474 +    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
   4.475 +  also have "... = (b < a*c)"
   4.476 +    by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   4.477 +  finally show ?thesis .
   4.478 +qed
   4.479 +
   4.480 +lemma pos_divide_less_eq:
   4.481 +     "0 < c ==> (b/c < a) = (b < a*c)"
   4.482 +proof -
   4.483 +  assume less: "0<c"
   4.484 +  hence "(b/c < a) = ((b/c)*c < a*c)"
   4.485 +    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
   4.486 +  also have "... = (b < a*c)"
   4.487 +    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   4.488 +  finally show ?thesis .
   4.489 +qed
   4.490 +
   4.491 +lemma neg_divide_less_eq:
   4.492 + "c < 0 ==> (b/c < a) = (a*c < b)"
   4.493 +proof -
   4.494 +  assume less: "c<0"
   4.495 +  hence "(b/c < a) = (a*c < (b/c)*c)"
   4.496 +    by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
   4.497 +  also have "... = (a*c < b)"
   4.498 +    by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   4.499 +  finally show ?thesis .
   4.500 +qed
   4.501 +
   4.502 +lemma pos_divide_le_eq: "0 < c ==> (b/c \<le> a) = (b \<le> a*c)"
   4.503 +proof -
   4.504 +  assume less: "0<c"
   4.505 +  hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
   4.506 +    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   4.507 +  also have "... = (b \<le> a*c)"
   4.508 +    by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   4.509 +  finally show ?thesis .
   4.510 +qed
   4.511 +
   4.512 +lemma neg_divide_le_eq: "c < 0 ==> (b/c \<le> a) = (a*c \<le> b)"
   4.513 +proof -
   4.514 +  assume less: "c<0"
   4.515 +  hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
   4.516 +    by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
   4.517 +  also have "... = (a*c \<le> b)"
   4.518 +    by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   4.519 +  finally show ?thesis .
   4.520 +qed
   4.521 +
   4.522 +text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
   4.523 +if they can be proved to be non-zero (for equations) or positive/negative
   4.524 +(for inequations). Can be too aggressive and is therefore separate from the
   4.525 +more benign @{text algebra_simps}. *}
   4.526 +
   4.527 +lemmas field_simps[no_atp] = field_eq_simps
   4.528 +  (* multiply ineqn *)
   4.529 +  pos_divide_less_eq neg_divide_less_eq
   4.530 +  pos_less_divide_eq neg_less_divide_eq
   4.531 +  pos_divide_le_eq neg_divide_le_eq
   4.532 +  pos_le_divide_eq neg_le_divide_eq
   4.533 +
   4.534 +text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
   4.535 +of positivity/negativity needed for @{text field_simps}. Have not added @{text
   4.536 +sign_simps} to @{text field_simps} because the former can lead to case
   4.537 +explosions. *}
   4.538 +
   4.539 +lemmas sign_simps[no_atp] = group_simps
   4.540 +  zero_less_mult_iff mult_less_0_iff
   4.541 +
   4.542 +(* Only works once linear arithmetic is installed:
   4.543 +text{*An example:*}
   4.544 +lemma fixes a b c d e f :: "'a::linordered_field"
   4.545 +shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
   4.546 + ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
   4.547 + ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
   4.548 +apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
   4.549 + prefer 2 apply(simp add:sign_simps)
   4.550 +apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
   4.551 + prefer 2 apply(simp add:sign_simps)
   4.552 +apply(simp add:field_simps)
   4.553 +done
   4.554 +*)
   4.555 +
   4.556 +lemma divide_pos_pos:
   4.557 +  "0 < x ==> 0 < y ==> 0 < x / y"
   4.558 +by(simp add:field_simps)
   4.559 +
   4.560 +lemma divide_nonneg_pos:
   4.561 +  "0 <= x ==> 0 < y ==> 0 <= x / y"
   4.562 +by(simp add:field_simps)
   4.563 +
   4.564 +lemma divide_neg_pos:
   4.565 +  "x < 0 ==> 0 < y ==> x / y < 0"
   4.566 +by(simp add:field_simps)
   4.567 +
   4.568 +lemma divide_nonpos_pos:
   4.569 +  "x <= 0 ==> 0 < y ==> x / y <= 0"
   4.570 +by(simp add:field_simps)
   4.571 +
   4.572 +lemma divide_pos_neg:
   4.573 +  "0 < x ==> y < 0 ==> x / y < 0"
   4.574 +by(simp add:field_simps)
   4.575 +
   4.576 +lemma divide_nonneg_neg:
   4.577 +  "0 <= x ==> y < 0 ==> x / y <= 0" 
   4.578 +by(simp add:field_simps)
   4.579 +
   4.580 +lemma divide_neg_neg:
   4.581 +  "x < 0 ==> y < 0 ==> 0 < x / y"
   4.582 +by(simp add:field_simps)
   4.583 +
   4.584 +lemma divide_nonpos_neg:
   4.585 +  "x <= 0 ==> y < 0 ==> 0 <= x / y"
   4.586 +by(simp add:field_simps)
   4.587 +
   4.588 +lemma divide_strict_right_mono:
   4.589 +     "[|a < b; 0 < c|] ==> a / c < b / c"
   4.590 +by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono 
   4.591 +              positive_imp_inverse_positive)
   4.592 +
   4.593 +
   4.594 +lemma divide_strict_right_mono_neg:
   4.595 +     "[|b < a; c < 0|] ==> a / c < b / c"
   4.596 +apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
   4.597 +apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric])
   4.598 +done
   4.599 +
   4.600 +text{*The last premise ensures that @{term a} and @{term b} 
   4.601 +      have the same sign*}
   4.602 +lemma divide_strict_left_mono:
   4.603 +  "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
   4.604 +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
   4.605 +
   4.606 +lemma divide_left_mono:
   4.607 +  "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
   4.608 +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
   4.609 +
   4.610 +lemma divide_strict_left_mono_neg:
   4.611 +  "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
   4.612 +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
   4.613 +
   4.614 +lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
   4.615 +    x / y <= z"
   4.616 +by (subst pos_divide_le_eq, assumption+)
   4.617 +
   4.618 +lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==>
   4.619 +    z <= x / y"
   4.620 +by(simp add:field_simps)
   4.621 +
   4.622 +lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==>
   4.623 +    x / y < z"
   4.624 +by(simp add:field_simps)
   4.625 +
   4.626 +lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==>
   4.627 +    z < x / y"
   4.628 +by(simp add:field_simps)
   4.629 +
   4.630 +lemma frac_le: "0 <= x ==> 
   4.631 +    x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
   4.632 +  apply (rule mult_imp_div_pos_le)
   4.633 +  apply simp
   4.634 +  apply (subst times_divide_eq_left)
   4.635 +  apply (rule mult_imp_le_div_pos, assumption)
   4.636 +  apply (rule mult_mono)
   4.637 +  apply simp_all
   4.638 +done
   4.639 +
   4.640 +lemma frac_less: "0 <= x ==> 
   4.641 +    x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
   4.642 +  apply (rule mult_imp_div_pos_less)
   4.643 +  apply simp
   4.644 +  apply (subst times_divide_eq_left)
   4.645 +  apply (rule mult_imp_less_div_pos, assumption)
   4.646 +  apply (erule mult_less_le_imp_less)
   4.647 +  apply simp_all
   4.648 +done
   4.649 +
   4.650 +lemma frac_less2: "0 < x ==> 
   4.651 +    x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
   4.652 +  apply (rule mult_imp_div_pos_less)
   4.653 +  apply simp_all
   4.654 +  apply (rule mult_imp_less_div_pos, assumption)
   4.655 +  apply (erule mult_le_less_imp_less)
   4.656 +  apply simp_all
   4.657 +done
   4.658 +
   4.659 +text{*It's not obvious whether these should be simprules or not. 
   4.660 +  Their effect is to gather terms into one big fraction, like
   4.661 +  a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
   4.662 +  seem to need them.*}
   4.663 +
   4.664 +lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
   4.665 +by (simp add: field_simps zero_less_two)
   4.666 +
   4.667 +lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
   4.668 +by (simp add: field_simps zero_less_two)
   4.669 +
   4.670 +subclass dense_linorder
   4.671 +proof
   4.672 +  fix x y :: 'a
   4.673 +  from less_add_one show "\<exists>y. x < y" .. 
   4.674 +  from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
   4.675 +  then have "x - 1 < x + 1 - 1" by (simp only: diff_minus [symmetric])
   4.676 +  then have "x - 1 < x" by (simp add: algebra_simps)
   4.677 +  then show "\<exists>y. y < x" ..
   4.678 +  show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
   4.679 +qed
   4.680 +
   4.681 +lemma nonzero_abs_inverse:
   4.682 +     "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
   4.683 +apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq 
   4.684 +                      negative_imp_inverse_negative)
   4.685 +apply (blast intro: positive_imp_inverse_positive elim: less_asym) 
   4.686 +done
   4.687 +
   4.688 +lemma nonzero_abs_divide:
   4.689 +     "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
   4.690 +  by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
   4.691 +
   4.692 +lemma field_le_epsilon:
   4.693 +  assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
   4.694 +  shows "x \<le> y"
   4.695 +proof (rule dense_le)
   4.696 +  fix t assume "t < x"
   4.697 +  hence "0 < x - t" by (simp add: less_diff_eq)
   4.698 +  from e [OF this] have "x + 0 \<le> x + (y - t)" by (simp add: algebra_simps)
   4.699 +  then have "0 \<le> y - t" by (simp only: add_le_cancel_left)
   4.700 +  then show "t \<le> y" by (simp add: algebra_simps)
   4.701 +qed
   4.702 +
   4.703 +end
   4.704 +
   4.705 +lemma le_divide_eq:
   4.706 +  "(a \<le> b/c) = 
   4.707 +   (if 0 < c then a*c \<le> b
   4.708 +             else if c < 0 then b \<le> a*c
   4.709 +             else  a \<le> (0::'a::{linordered_field,division_by_zero}))"
   4.710 +apply (cases "c=0", simp) 
   4.711 +apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
   4.712 +done
   4.713 +
   4.714  lemma inverse_positive_iff_positive [simp]:
   4.715    "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))"
   4.716  apply (cases "a = 0", simp)
   4.717  apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
   4.718  done
   4.719  
   4.720 -lemma inverse_negative_imp_negative:
   4.721 -assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
   4.722 -shows "a < (0::'a::linordered_field)"
   4.723 -proof -
   4.724 -  have "inverse (inverse a) < 0"
   4.725 -    using inv_less_0 by (rule negative_imp_inverse_negative)
   4.726 -  thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
   4.727 -qed
   4.728 -
   4.729  lemma inverse_negative_iff_negative [simp]:
   4.730    "(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))"
   4.731  apply (cases "a = 0", simp)
   4.732 @@ -402,104 +687,6 @@
   4.733    "(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_by_zero}))"
   4.734  by (simp add: linorder_not_less [symmetric])
   4.735  
   4.736 -lemma linordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)"
   4.737 -proof
   4.738 -  fix x::'a
   4.739 -  have m1: "- (1::'a) < 0" by simp
   4.740 -  from add_strict_right_mono[OF m1, where c=x] 
   4.741 -  have "(- 1) + x < x" by simp
   4.742 -  thus "\<exists>y. y < x" by blast
   4.743 -qed
   4.744 -
   4.745 -lemma linordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)"
   4.746 -proof
   4.747 -  fix x::'a
   4.748 -  have m1: " (1::'a) > 0" by simp
   4.749 -  from add_strict_right_mono[OF m1, where c=x] 
   4.750 -  have "1 + x > x" by simp
   4.751 -  thus "\<exists>y. y > x" by blast
   4.752 -qed
   4.753 -
   4.754 -subsection{*Anti-Monotonicity of @{term inverse}*}
   4.755 -
   4.756 -lemma less_imp_inverse_less:
   4.757 -assumes less: "a < b" and apos:  "0 < a"
   4.758 -shows "inverse b < inverse (a::'a::linordered_field)"
   4.759 -proof (rule ccontr)
   4.760 -  assume "~ inverse b < inverse a"
   4.761 -  hence "inverse a \<le> inverse b" by (simp add: linorder_not_less)
   4.762 -  hence "~ (a < b)"
   4.763 -    by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
   4.764 -  thus False by (rule notE [OF _ less])
   4.765 -qed
   4.766 -
   4.767 -lemma inverse_less_imp_less:
   4.768 -  "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::linordered_field)"
   4.769 -apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
   4.770 -apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
   4.771 -done
   4.772 -
   4.773 -text{*Both premises are essential. Consider -1 and 1.*}
   4.774 -lemma inverse_less_iff_less [simp,no_atp]:
   4.775 -  "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
   4.776 -by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
   4.777 -
   4.778 -lemma le_imp_inverse_le:
   4.779 -  "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
   4.780 -by (force simp add: order_le_less less_imp_inverse_less)
   4.781 -
   4.782 -lemma inverse_le_iff_le [simp,no_atp]:
   4.783 - "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
   4.784 -by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
   4.785 -
   4.786 -
   4.787 -text{*These results refer to both operands being negative.  The opposite-sign
   4.788 -case is trivial, since inverse preserves signs.*}
   4.789 -lemma inverse_le_imp_le_neg:
   4.790 -  "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::linordered_field)"
   4.791 -apply (rule classical) 
   4.792 -apply (subgoal_tac "a < 0") 
   4.793 - prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
   4.794 -apply (insert inverse_le_imp_le [of "-b" "-a"])
   4.795 -apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.796 -done
   4.797 -
   4.798 -lemma less_imp_inverse_less_neg:
   4.799 -   "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::linordered_field)"
   4.800 -apply (subgoal_tac "a < 0") 
   4.801 - prefer 2 apply (blast intro: order_less_trans) 
   4.802 -apply (insert less_imp_inverse_less [of "-b" "-a"])
   4.803 -apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.804 -done
   4.805 -
   4.806 -lemma inverse_less_imp_less_neg:
   4.807 -   "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::linordered_field)"
   4.808 -apply (rule classical) 
   4.809 -apply (subgoal_tac "a < 0") 
   4.810 - prefer 2
   4.811 - apply (force simp add: linorder_not_less intro: order_le_less_trans) 
   4.812 -apply (insert inverse_less_imp_less [of "-b" "-a"])
   4.813 -apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.814 -done
   4.815 -
   4.816 -lemma inverse_less_iff_less_neg [simp,no_atp]:
   4.817 -  "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
   4.818 -apply (insert inverse_less_iff_less [of "-b" "-a"])
   4.819 -apply (simp del: inverse_less_iff_less 
   4.820 -            add: order_less_imp_not_eq nonzero_inverse_minus_eq)
   4.821 -done
   4.822 -
   4.823 -lemma le_imp_inverse_le_neg:
   4.824 -  "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
   4.825 -by (force simp add: order_le_less less_imp_inverse_less_neg)
   4.826 -
   4.827 -lemma inverse_le_iff_le_neg [simp,no_atp]:
   4.828 - "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
   4.829 -by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
   4.830 -
   4.831 -
   4.832 -subsection{*Inverses and the Number One*}
   4.833 -
   4.834  lemma one_less_inverse_iff:
   4.835    "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))"
   4.836  proof cases
   4.837 @@ -518,10 +705,6 @@
   4.838    with notless show ?thesis by simp
   4.839  qed
   4.840  
   4.841 -lemma inverse_eq_1_iff [simp]:
   4.842 -  "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
   4.843 -by (insert inverse_eq_iff_eq [of x 1], simp) 
   4.844 -
   4.845  lemma one_le_inverse_iff:
   4.846    "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_by_zero}))"
   4.847  by (force simp add: order_le_less one_less_inverse_iff)
   4.848 @@ -534,58 +717,6 @@
   4.849    "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{linordered_field,division_by_zero}))"
   4.850  by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
   4.851  
   4.852 -
   4.853 -subsection{*Simplification of Inequalities Involving Literal Divisors*}
   4.854 -
   4.855 -lemma pos_le_divide_eq: "0 < (c::'a::linordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
   4.856 -proof -
   4.857 -  assume less: "0<c"
   4.858 -  hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
   4.859 -    by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
   4.860 -  also have "... = (a*c \<le> b)"
   4.861 -    by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   4.862 -  finally show ?thesis .
   4.863 -qed
   4.864 -
   4.865 -lemma neg_le_divide_eq: "c < (0::'a::linordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
   4.866 -proof -
   4.867 -  assume less: "c<0"
   4.868 -  hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
   4.869 -    by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
   4.870 -  also have "... = (b \<le> a*c)"
   4.871 -    by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   4.872 -  finally show ?thesis .
   4.873 -qed
   4.874 -
   4.875 -lemma le_divide_eq:
   4.876 -  "(a \<le> b/c) = 
   4.877 -   (if 0 < c then a*c \<le> b
   4.878 -             else if c < 0 then b \<le> a*c
   4.879 -             else  a \<le> (0::'a::{linordered_field,division_by_zero}))"
   4.880 -apply (cases "c=0", simp) 
   4.881 -apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
   4.882 -done
   4.883 -
   4.884 -lemma pos_divide_le_eq: "0 < (c::'a::linordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
   4.885 -proof -
   4.886 -  assume less: "0<c"
   4.887 -  hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
   4.888 -    by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
   4.889 -  also have "... = (b \<le> a*c)"
   4.890 -    by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   4.891 -  finally show ?thesis .
   4.892 -qed
   4.893 -
   4.894 -lemma neg_divide_le_eq: "c < (0::'a::linordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
   4.895 -proof -
   4.896 -  assume less: "c<0"
   4.897 -  hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
   4.898 -    by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
   4.899 -  also have "... = (a*c \<le> b)"
   4.900 -    by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   4.901 -  finally show ?thesis .
   4.902 -qed
   4.903 -
   4.904  lemma divide_le_eq:
   4.905    "(b/c \<le> a) = 
   4.906     (if 0 < c then b \<le> a*c
   4.907 @@ -595,28 +726,6 @@
   4.908  apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
   4.909  done
   4.910  
   4.911 -lemma pos_less_divide_eq:
   4.912 -     "0 < (c::'a::linordered_field) ==> (a < b/c) = (a*c < b)"
   4.913 -proof -
   4.914 -  assume less: "0<c"
   4.915 -  hence "(a < b/c) = (a*c < (b/c)*c)"
   4.916 -    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
   4.917 -  also have "... = (a*c < b)"
   4.918 -    by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   4.919 -  finally show ?thesis .
   4.920 -qed
   4.921 -
   4.922 -lemma neg_less_divide_eq:
   4.923 - "c < (0::'a::linordered_field) ==> (a < b/c) = (b < a*c)"
   4.924 -proof -
   4.925 -  assume less: "c<0"
   4.926 -  hence "(a < b/c) = ((b/c)*c < a*c)"
   4.927 -    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
   4.928 -  also have "... = (b < a*c)"
   4.929 -    by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   4.930 -  finally show ?thesis .
   4.931 -qed
   4.932 -
   4.933  lemma less_divide_eq:
   4.934    "(a < b/c) = 
   4.935     (if 0 < c then a*c < b
   4.936 @@ -626,28 +735,6 @@
   4.937  apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
   4.938  done
   4.939  
   4.940 -lemma pos_divide_less_eq:
   4.941 -     "0 < (c::'a::linordered_field) ==> (b/c < a) = (b < a*c)"
   4.942 -proof -
   4.943 -  assume less: "0<c"
   4.944 -  hence "(b/c < a) = ((b/c)*c < a*c)"
   4.945 -    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
   4.946 -  also have "... = (b < a*c)"
   4.947 -    by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   4.948 -  finally show ?thesis .
   4.949 -qed
   4.950 -
   4.951 -lemma neg_divide_less_eq:
   4.952 - "c < (0::'a::linordered_field) ==> (b/c < a) = (a*c < b)"
   4.953 -proof -
   4.954 -  assume less: "c<0"
   4.955 -  hence "(b/c < a) = (a*c < (b/c)*c)"
   4.956 -    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
   4.957 -  also have "... = (a*c < b)"
   4.958 -    by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   4.959 -  finally show ?thesis .
   4.960 -qed
   4.961 -
   4.962  lemma divide_less_eq:
   4.963    "(b/c < a) = 
   4.964     (if 0 < c then b < a*c
   4.965 @@ -657,45 +744,7 @@
   4.966  apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
   4.967  done
   4.968  
   4.969 -
   4.970 -subsection{*Field simplification*}
   4.971 -
   4.972 -text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
   4.973 -if they can be proved to be non-zero (for equations) or positive/negative
   4.974 -(for inequations). Can be too aggressive and is therefore separate from the
   4.975 -more benign @{text algebra_simps}. *}
   4.976 -
   4.977 -lemmas field_simps[no_atp] = field_eq_simps
   4.978 -  (* multiply ineqn *)
   4.979 -  pos_divide_less_eq neg_divide_less_eq
   4.980 -  pos_less_divide_eq neg_less_divide_eq
   4.981 -  pos_divide_le_eq neg_divide_le_eq
   4.982 -  pos_le_divide_eq neg_le_divide_eq
   4.983 -
   4.984 -text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
   4.985 -of positivity/negativity needed for @{text field_simps}. Have not added @{text
   4.986 -sign_simps} to @{text field_simps} because the former can lead to case
   4.987 -explosions. *}
   4.988 -
   4.989 -lemmas sign_simps[no_atp] = group_simps
   4.990 -  zero_less_mult_iff  mult_less_0_iff
   4.991 -
   4.992 -(* Only works once linear arithmetic is installed:
   4.993 -text{*An example:*}
   4.994 -lemma fixes a b c d e f :: "'a::linordered_field"
   4.995 -shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
   4.996 - ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
   4.997 - ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
   4.998 -apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
   4.999 - prefer 2 apply(simp add:sign_simps)
  4.1000 -apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
  4.1001 - prefer 2 apply(simp add:sign_simps)
  4.1002 -apply(simp add:field_simps)
  4.1003 -done
  4.1004 -*)
  4.1005 -
  4.1006 -
  4.1007 -subsection{*Division and Signs*}
  4.1008 +text {*Division and Signs*}
  4.1009  
  4.1010  lemma zero_less_divide_iff:
  4.1011       "((0::'a::{linordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  4.1012 @@ -716,71 +765,9 @@
  4.1013        (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  4.1014  by (simp add: divide_inverse mult_le_0_iff)
  4.1015  
  4.1016 -lemma divide_eq_0_iff [simp,no_atp]:
  4.1017 -     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  4.1018 -by (simp add: divide_inverse)
  4.1019 -
  4.1020 -lemma divide_pos_pos:
  4.1021 -  "0 < (x::'a::linordered_field) ==> 0 < y ==> 0 < x / y"
  4.1022 -by(simp add:field_simps)
  4.1023 -
  4.1024 -
  4.1025 -lemma divide_nonneg_pos:
  4.1026 -  "0 <= (x::'a::linordered_field) ==> 0 < y ==> 0 <= x / y"
  4.1027 -by(simp add:field_simps)
  4.1028 -
  4.1029 -lemma divide_neg_pos:
  4.1030 -  "(x::'a::linordered_field) < 0 ==> 0 < y ==> x / y < 0"
  4.1031 -by(simp add:field_simps)
  4.1032 -
  4.1033 -lemma divide_nonpos_pos:
  4.1034 -  "(x::'a::linordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
  4.1035 -by(simp add:field_simps)
  4.1036 -
  4.1037 -lemma divide_pos_neg:
  4.1038 -  "0 < (x::'a::linordered_field) ==> y < 0 ==> x / y < 0"
  4.1039 -by(simp add:field_simps)
  4.1040 -
  4.1041 -lemma divide_nonneg_neg:
  4.1042 -  "0 <= (x::'a::linordered_field) ==> y < 0 ==> x / y <= 0" 
  4.1043 -by(simp add:field_simps)
  4.1044 -
  4.1045 -lemma divide_neg_neg:
  4.1046 -  "(x::'a::linordered_field) < 0 ==> y < 0 ==> 0 < x / y"
  4.1047 -by(simp add:field_simps)
  4.1048 -
  4.1049 -lemma divide_nonpos_neg:
  4.1050 -  "(x::'a::linordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
  4.1051 -by(simp add:field_simps)
  4.1052 -
  4.1053 -
  4.1054 -subsection{*Cancellation Laws for Division*}
  4.1055 -
  4.1056 -lemma divide_cancel_right [simp,no_atp]:
  4.1057 -     "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
  4.1058 -apply (cases "c=0", simp)
  4.1059 -apply (simp add: divide_inverse)
  4.1060 -done
  4.1061 -
  4.1062 -lemma divide_cancel_left [simp,no_atp]:
  4.1063 -     "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
  4.1064 -apply (cases "c=0", simp)
  4.1065 -apply (simp add: divide_inverse)
  4.1066 -done
  4.1067 -
  4.1068 -
  4.1069 -subsection {* Division and the Number One *}
  4.1070 +text {* Division and the Number One *}
  4.1071  
  4.1072  text{*Simplify expressions equated with 1*}
  4.1073 -lemma divide_eq_1_iff [simp,no_atp]:
  4.1074 -     "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  4.1075 -apply (cases "b=0", simp)
  4.1076 -apply (simp add: right_inverse_eq)
  4.1077 -done
  4.1078 -
  4.1079 -lemma one_eq_divide_iff [simp,no_atp]:
  4.1080 -     "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  4.1081 -by (simp add: eq_commute [of 1])
  4.1082  
  4.1083  lemma zero_eq_1_divide_iff [simp,no_atp]:
  4.1084       "((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)"
  4.1085 @@ -806,49 +793,22 @@
  4.1086  declare zero_le_divide_1_iff [simp,no_atp]
  4.1087  declare divide_le_0_1_iff [simp,no_atp]
  4.1088  
  4.1089 -
  4.1090 -subsection {* Ordering Rules for Division *}
  4.1091 -
  4.1092 -lemma divide_strict_right_mono:
  4.1093 -     "[|a < b; 0 < c|] ==> a / c < b / (c::'a::linordered_field)"
  4.1094 -by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
  4.1095 -              positive_imp_inverse_positive)
  4.1096 -
  4.1097  lemma divide_right_mono:
  4.1098       "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{linordered_field,division_by_zero})"
  4.1099  by (force simp add: divide_strict_right_mono order_le_less)
  4.1100  
  4.1101 -lemma divide_right_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b 
  4.1102 +lemma divide_right_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= b 
  4.1103      ==> c <= 0 ==> b / c <= a / c"
  4.1104  apply (drule divide_right_mono [of _ _ "- c"])
  4.1105  apply auto
  4.1106  done
  4.1107  
  4.1108 -lemma divide_strict_right_mono_neg:
  4.1109 -     "[|b < a; c < 0|] ==> a / c < b / (c::'a::linordered_field)"
  4.1110 -apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
  4.1111 -apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
  4.1112 -done
  4.1113 -
  4.1114 -text{*The last premise ensures that @{term a} and @{term b} 
  4.1115 -      have the same sign*}
  4.1116 -lemma divide_strict_left_mono:
  4.1117 -  "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)"
  4.1118 -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
  4.1119 -
  4.1120 -lemma divide_left_mono:
  4.1121 -  "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::linordered_field)"
  4.1122 -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
  4.1123 -
  4.1124 -lemma divide_left_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b 
  4.1125 +lemma divide_left_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= b 
  4.1126      ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
  4.1127    apply (drule divide_left_mono [of _ _ "- c"])
  4.1128    apply (auto simp add: mult_commute)
  4.1129  done
  4.1130  
  4.1131 -lemma divide_strict_left_mono_neg:
  4.1132 -  "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)"
  4.1133 -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
  4.1134  
  4.1135  
  4.1136  text{*Simplify quotients that are compared with the value 1.*}
  4.1137 @@ -874,7 +834,7 @@
  4.1138  by (auto simp add: divide_less_eq)
  4.1139  
  4.1140  
  4.1141 -subsection{*Conditional Simplification Rules: No Case Splits*}
  4.1142 +text {*Conditional Simplification Rules: No Case Splits*}
  4.1143  
  4.1144  lemma le_divide_eq_1_pos [simp,no_atp]:
  4.1145    fixes a :: "'a :: {linordered_field,division_by_zero}"
  4.1146 @@ -926,125 +886,25 @@
  4.1147    shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  4.1148  by (auto simp add: divide_eq_eq)
  4.1149  
  4.1150 -
  4.1151 -subsection {* Reasoning about inequalities with division *}
  4.1152 -
  4.1153 -lemma mult_imp_div_pos_le: "0 < (y::'a::linordered_field) ==> x <= z * y ==>
  4.1154 -    x / y <= z"
  4.1155 -by (subst pos_divide_le_eq, assumption+)
  4.1156 -
  4.1157 -lemma mult_imp_le_div_pos: "0 < (y::'a::linordered_field) ==> z * y <= x ==>
  4.1158 -    z <= x / y"
  4.1159 -by(simp add:field_simps)
  4.1160 -
  4.1161 -lemma mult_imp_div_pos_less: "0 < (y::'a::linordered_field) ==> x < z * y ==>
  4.1162 -    x / y < z"
  4.1163 -by(simp add:field_simps)
  4.1164 -
  4.1165 -lemma mult_imp_less_div_pos: "0 < (y::'a::linordered_field) ==> z * y < x ==>
  4.1166 -    z < x / y"
  4.1167 -by(simp add:field_simps)
  4.1168 -
  4.1169 -lemma frac_le: "(0::'a::linordered_field) <= x ==> 
  4.1170 -    x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
  4.1171 -  apply (rule mult_imp_div_pos_le)
  4.1172 -  apply simp
  4.1173 -  apply (subst times_divide_eq_left)
  4.1174 -  apply (rule mult_imp_le_div_pos, assumption)
  4.1175 -  apply (rule mult_mono)
  4.1176 -  apply simp_all
  4.1177 -done
  4.1178 -
  4.1179 -lemma frac_less: "(0::'a::linordered_field) <= x ==> 
  4.1180 -    x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
  4.1181 -  apply (rule mult_imp_div_pos_less)
  4.1182 -  apply simp
  4.1183 -  apply (subst times_divide_eq_left)
  4.1184 -  apply (rule mult_imp_less_div_pos, assumption)
  4.1185 -  apply (erule mult_less_le_imp_less)
  4.1186 -  apply simp_all
  4.1187 -done
  4.1188 -
  4.1189 -lemma frac_less2: "(0::'a::linordered_field) < x ==> 
  4.1190 -    x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
  4.1191 -  apply (rule mult_imp_div_pos_less)
  4.1192 -  apply simp_all
  4.1193 -  apply (subst times_divide_eq_left)
  4.1194 -  apply (rule mult_imp_less_div_pos, assumption)
  4.1195 -  apply (erule mult_le_less_imp_less)
  4.1196 -  apply simp_all
  4.1197 -done
  4.1198 -
  4.1199 -text{*It's not obvious whether these should be simprules or not. 
  4.1200 -  Their effect is to gather terms into one big fraction, like
  4.1201 -  a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
  4.1202 -  seem to need them.*}
  4.1203 -
  4.1204 -declare times_divide_eq [simp]
  4.1205 -
  4.1206 -
  4.1207 -subsection {* Ordered Fields are Dense *}
  4.1208 -
  4.1209 -lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::linordered_field)"
  4.1210 -by (simp add: field_simps zero_less_two)
  4.1211 -
  4.1212 -lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::linordered_field) < b"
  4.1213 -by (simp add: field_simps zero_less_two)
  4.1214 -
  4.1215 -instance linordered_field < dense_linorder
  4.1216 -proof
  4.1217 -  fix x y :: 'a
  4.1218 -  have "x < x + 1" by simp
  4.1219 -  then show "\<exists>y. x < y" .. 
  4.1220 -  have "x - 1 < x" by simp
  4.1221 -  then show "\<exists>y. y < x" ..
  4.1222 -  show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
  4.1223 -qed
  4.1224 -
  4.1225 -
  4.1226 -subsection {* Absolute Value *}
  4.1227 -
  4.1228 -lemma nonzero_abs_inverse:
  4.1229 -     "a \<noteq> 0 ==> abs (inverse (a::'a::linordered_field)) = inverse (abs a)"
  4.1230 -apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq 
  4.1231 -                      negative_imp_inverse_negative)
  4.1232 -apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) 
  4.1233 -done
  4.1234 -
  4.1235  lemma abs_inverse [simp]:
  4.1236 -     "abs (inverse (a::'a::{linordered_field,division_by_zero})) = 
  4.1237 -      inverse (abs a)"
  4.1238 +     "\<bar>inverse (a::'a::{linordered_field,division_by_zero})\<bar> = 
  4.1239 +      inverse \<bar>a\<bar>"
  4.1240  apply (cases "a=0", simp) 
  4.1241  apply (simp add: nonzero_abs_inverse) 
  4.1242  done
  4.1243  
  4.1244 -lemma nonzero_abs_divide:
  4.1245 -     "b \<noteq> 0 ==> abs (a / (b::'a::linordered_field)) = abs a / abs b"
  4.1246 -by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
  4.1247 -
  4.1248  lemma abs_divide [simp]:
  4.1249 -     "abs (a / (b::'a::{linordered_field,division_by_zero})) = abs a / abs b"
  4.1250 +     "\<bar>a / (b::'a::{linordered_field,division_by_zero})\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
  4.1251  apply (cases "b=0", simp) 
  4.1252  apply (simp add: nonzero_abs_divide) 
  4.1253  done
  4.1254  
  4.1255 -lemma abs_div_pos: "(0::'a::{division_by_zero,linordered_field}) < y ==> 
  4.1256 -    abs x / y = abs (x / y)"
  4.1257 +lemma abs_div_pos: "(0::'a::{linordered_field,division_by_zero}) < y ==> 
  4.1258 +    \<bar>x\<bar> / y = \<bar>x / y\<bar>"
  4.1259    apply (subst abs_divide)
  4.1260    apply (simp add: order_less_imp_le)
  4.1261  done
  4.1262  
  4.1263 -lemma field_le_epsilon:
  4.1264 -  fixes x y :: "'a\<Colon>linordered_field"
  4.1265 -  assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
  4.1266 -  shows "x \<le> y"
  4.1267 -proof (rule dense_le)
  4.1268 -  fix t assume "t < x"
  4.1269 -  hence "0 < x - t" by (simp add: less_diff_eq)
  4.1270 -  from e[OF this]
  4.1271 -  show "t \<le> y" by (simp add: field_simps)
  4.1272 -qed
  4.1273 -
  4.1274  lemma field_le_mult_one_interval:
  4.1275    fixes x :: "'a\<Colon>{linordered_field,division_by_zero}"
  4.1276    assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
     5.1 --- a/src/HOL/Groebner_Basis.thy	Fri Apr 23 16:12:57 2010 +0200
     5.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Apr 23 19:32:37 2010 +0200
     5.3 @@ -627,7 +627,7 @@
     5.4  
     5.5  val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
     5.6             @{thm "divide_Numeral1"},
     5.7 -           @{thm "Fields.divide_zero"}, @{thm "divide_Numeral0"},
     5.8 +           @{thm "divide_zero"}, @{thm "divide_Numeral0"},
     5.9             @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
    5.10             @{thm "mult_num_frac"}, @{thm "mult_frac_num"},
    5.11             @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
     6.1 --- a/src/HOL/Groups.thy	Fri Apr 23 16:12:57 2010 +0200
     6.2 +++ b/src/HOL/Groups.thy	Fri Apr 23 19:32:37 2010 +0200
     6.3 @@ -757,7 +757,7 @@
     6.4  done
     6.5  
     6.6  lemma less_diff_eq[algebra_simps]: "a < c - b \<longleftrightarrow> a + b < c"
     6.7 -apply (subst less_iff_diff_less_0 [of "plus a b"])
     6.8 +apply (subst less_iff_diff_less_0 [of "a + b"])
     6.9  apply (subst less_iff_diff_less_0 [of a])
    6.10  apply (simp add: diff_minus add_ac)
    6.11  done
    6.12 @@ -966,27 +966,26 @@
    6.13  
    6.14  end
    6.15  
    6.16 --- {* FIXME localize the following *}
    6.17 +context ordered_comm_monoid_add
    6.18 +begin
    6.19  
    6.20  lemma add_increasing:
    6.21 -  fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}"
    6.22 -  shows  "[|0\<le>a; b\<le>c|] ==> b \<le> a + c"
    6.23 -by (insert add_mono [of 0 a b c], simp)
    6.24 +  "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
    6.25 +  by (insert add_mono [of 0 a b c], simp)
    6.26  
    6.27  lemma add_increasing2:
    6.28 -  fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}"
    6.29 -  shows  "[|0\<le>c; b\<le>a|] ==> b \<le> a + c"
    6.30 -by (simp add:add_increasing add_commute[of a])
    6.31 +  "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
    6.32 +  by (simp add: add_increasing add_commute [of a])
    6.33  
    6.34  lemma add_strict_increasing:
    6.35 -  fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}"
    6.36 -  shows "[|0<a; b\<le>c|] ==> b < a + c"
    6.37 -by (insert add_less_le_mono [of 0 a b c], simp)
    6.38 +  "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
    6.39 +  by (insert add_less_le_mono [of 0 a b c], simp)
    6.40  
    6.41  lemma add_strict_increasing2:
    6.42 -  fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}"
    6.43 -  shows "[|0\<le>a; b<c|] ==> b < a + c"
    6.44 -by (insert add_le_less_mono [of 0 a b c], simp)
    6.45 +  "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
    6.46 +  by (insert add_le_less_mono [of 0 a b c], simp)
    6.47 +
    6.48 +end
    6.49  
    6.50  class abs =
    6.51    fixes abs :: "'a \<Rightarrow> 'a"
    6.52 @@ -1036,7 +1035,7 @@
    6.53  
    6.54  lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
    6.55  by (rule antisym)
    6.56 -   (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"])
    6.57 +   (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
    6.58  
    6.59  lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
    6.60  proof -
    6.61 @@ -1045,7 +1044,7 @@
    6.62      assume zero: "\<bar>a\<bar> = 0"
    6.63      with abs_ge_self show "a \<le> 0" by auto
    6.64      from zero have "\<bar>-a\<bar> = 0" by simp
    6.65 -    with abs_ge_self [of "uminus a"] have "- a \<le> 0" by auto
    6.66 +    with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
    6.67      with neg_le_0_iff_le show "0 \<le> a" by auto
    6.68    qed
    6.69    then show ?thesis by auto
    6.70 @@ -1114,32 +1113,31 @@
    6.71  by (insert abs_ge_self, blast intro: order_trans)
    6.72  
    6.73  lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
    6.74 -by (insert abs_le_D1 [of "uminus a"], simp)
    6.75 +by (insert abs_le_D1 [of "- a"], simp)
    6.76  
    6.77  lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
    6.78  by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
    6.79  
    6.80  lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
    6.81 -  apply (simp add: algebra_simps)
    6.82 -  apply (subgoal_tac "abs a = abs (plus b (minus a b))")
    6.83 -  apply (erule ssubst)
    6.84 -  apply (rule abs_triangle_ineq)
    6.85 -  apply (rule arg_cong[of _ _ abs])
    6.86 -  apply (simp add: algebra_simps)
    6.87 -done
    6.88 +proof -
    6.89 +  have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
    6.90 +    by (simp add: algebra_simps add_diff_cancel)
    6.91 +  then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
    6.92 +    by (simp add: abs_triangle_ineq)
    6.93 +  then show ?thesis
    6.94 +    by (simp add: algebra_simps)
    6.95 +qed
    6.96 +
    6.97 +lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
    6.98 +  by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
    6.99  
   6.100  lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
   6.101 -  apply (subst abs_le_iff)
   6.102 -  apply auto
   6.103 -  apply (rule abs_triangle_ineq2)
   6.104 -  apply (subst abs_minus_commute)
   6.105 -  apply (rule abs_triangle_ineq2)
   6.106 -done
   6.107 +  by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
   6.108  
   6.109  lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   6.110  proof -
   6.111 -  have "abs(a - b) = abs(a + - b)" by (subst diff_minus, rule refl)
   6.112 -  also have "... <= abs a + abs (- b)" by (rule abs_triangle_ineq)
   6.113 +  have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
   6.114 +  also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
   6.115    finally show ?thesis by simp
   6.116  qed
   6.117  
     7.1 --- a/src/HOL/Library/Binomial.thy	Fri Apr 23 16:12:57 2010 +0200
     7.2 +++ b/src/HOL/Library/Binomial.thy	Fri Apr 23 19:32:37 2010 +0200
     7.3 @@ -391,13 +391,13 @@
     7.4    assumes kn: "k \<le> n" 
     7.5    shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
     7.6    using binomial_fact_lemma[OF kn]
     7.7 -  by (simp add: field_simps of_nat_mult[symmetric])
     7.8 +  by (simp add: field_eq_simps of_nat_mult [symmetric])
     7.9  
    7.10  lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
    7.11  proof-
    7.12    {assume kn: "k > n" 
    7.13      from kn binomial_eq_0[OF kn] have ?thesis 
    7.14 -      by (simp add: gbinomial_pochhammer field_simps
    7.15 +      by (simp add: gbinomial_pochhammer field_eq_simps
    7.16          pochhammer_of_nat_eq_0_iff)}
    7.17    moreover
    7.18    {assume "k=0" then have ?thesis by simp}
    7.19 @@ -420,7 +420,7 @@
    7.20      from eq[symmetric]
    7.21      have ?thesis using kn
    7.22        apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
    7.23 -        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
    7.24 +        gbinomial_pochhammer field_eq_simps pochhammer_Suc_setprod)
    7.25        apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
    7.26        unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
    7.27        unfolding mult_assoc[symmetric] 
    7.28 @@ -449,7 +449,7 @@
    7.29    have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
    7.30      unfolding gbinomial_pochhammer
    7.31      pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
    7.32 -    by (simp add:  field_simps del: of_nat_Suc)
    7.33 +    by (simp add:  field_eq_simps del: of_nat_Suc)
    7.34    also have "\<dots> = ?l" unfolding gbinomial_pochhammer
    7.35      by (simp add: ring_simps)
    7.36    finally show ?thesis ..
     8.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 23 16:12:57 2010 +0200
     8.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 23 19:32:37 2010 +0200
     8.3 @@ -388,6 +388,8 @@
     8.4    then show "a*b \<noteq> 0" unfolding fps_nonzero_nth by blast
     8.5  qed
     8.6  
     8.7 +instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
     8.8 +
     8.9  instance fps :: (idom) idom ..
    8.10  
    8.11  instantiation fps :: (comm_ring_1) number_ring
    8.12 @@ -586,7 +588,7 @@
    8.13    from k have "real k > - log y x" by simp
    8.14    then have "ln y * real k > - ln x" unfolding log_def
    8.15      using ln_gt_zero_iff[OF yp] y1
    8.16 -    by (simp add: minus_divide_left field_simps del:minus_divide_left[symmetric] )
    8.17 +    by (simp add: minus_divide_left field_simps field_eq_simps del:minus_divide_left[symmetric])
    8.18    then have "ln y * real k + ln x > 0" by simp
    8.19    then have "exp (real k * ln y + ln x) > exp 0"
    8.20      by (simp add: mult_ac)
    8.21 @@ -594,7 +596,7 @@
    8.22      unfolding exp_zero exp_add exp_real_of_nat_mult
    8.23      exp_ln[OF xp] exp_ln[OF yp] by simp
    8.24    then have "x > (1/y)^k" using yp 
    8.25 -    by (simp add: field_simps nonzero_power_divide )
    8.26 +    by (simp add: field_simps field_eq_simps nonzero_power_divide)
    8.27    then show ?thesis using kp by blast
    8.28  qed
    8.29  lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def)
    8.30 @@ -649,8 +651,7 @@
    8.31  
    8.32  declare setsum_cong[fundef_cong]
    8.33  
    8.34 -
    8.35 -instantiation fps :: ("{comm_monoid_add,inverse, times, uminus}") inverse
    8.36 +instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse
    8.37  begin
    8.38  
    8.39  fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a" where
    8.40 @@ -658,9 +659,12 @@
    8.41  | "natfun_inverse f n = - inverse (f$0) * setsum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n}"
    8.42  
    8.43  definition fps_inverse_def:
    8.44 -  "inverse f = (if f$0 = 0 then 0 else Abs_fps (natfun_inverse f))"
    8.45 +  "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))"
    8.46 +
    8.47  definition fps_divide_def: "divide = (\<lambda>(f::'a fps) g. f * inverse g)"
    8.48 +
    8.49  instance ..
    8.50 +
    8.51  end
    8.52  
    8.53  lemma fps_inverse_zero[simp]:
    8.54 @@ -671,10 +675,7 @@
    8.55    apply (auto simp add: expand_fps_eq fps_inverse_def)
    8.56    by (case_tac n, auto)
    8.57  
    8.58 -instance fps :: ("{comm_monoid_add,inverse, times, uminus}")  division_by_zero
    8.59 -  by default (rule fps_inverse_zero)
    8.60 -
    8.61 -lemma inverse_mult_eq_1[intro]: assumes f0: "f$0 \<noteq> (0::'a::field)"
    8.62 +lemma inverse_mult_eq_1 [intro]: assumes f0: "f$0 \<noteq> (0::'a::field)"
    8.63    shows "inverse f * f = 1"
    8.64  proof-
    8.65    have c: "inverse f * f = f * inverse f" by (simp add: mult_commute)
    8.66 @@ -1687,7 +1688,7 @@
    8.67          then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
    8.68            by (simp add: natpermute_max_card[OF nz, simplified])
    8.69          also have "\<dots> = a$n - setsum ?f ?Pnknn"
    8.70 -          unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc )
    8.71 +          unfolding n1 using r00 a0 by (simp add: field_eq_simps fps_radical_def del: of_nat_Suc)
    8.72          finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" .
    8.73          have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn"
    8.74            unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] ..
    8.75 @@ -1763,7 +1764,7 @@
    8.76    shows "a = b / c"
    8.77  proof-
    8.78    from eq have "a * c * inverse c = b * inverse c" by simp
    8.79 -  hence "a * (inverse c * c) = b/c" by (simp only: field_simps divide_inverse)
    8.80 +  hence "a * (inverse c * c) = b/c" by (simp only: field_eq_simps divide_inverse)
    8.81    then show "a = b/c" unfolding  field_inverse[OF c0] by simp
    8.82  qed
    8.83  
    8.84 @@ -1836,7 +1837,7 @@
    8.85            show "a$(xs !i) = ?r$(xs!i)" .
    8.86          qed
    8.87          have th00: "\<And>(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x"
    8.88 -          by (simp add: field_simps del: of_nat_Suc)
    8.89 +          by (simp add: field_eq_simps del: of_nat_Suc)
    8.90          from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff)
    8.91          also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn"
    8.92            unfolding fps_power_nth_Suc
    8.93 @@ -1853,7 +1854,7 @@
    8.94          then have "a$n = ?r $n"
    8.95            apply (simp del: of_nat_Suc)
    8.96            unfolding fps_radical_def n1
    8.97 -          by (simp add: field_simps n1 th00 del: of_nat_Suc)}
    8.98 +          by (simp add: field_eq_simps n1 th00 del: of_nat_Suc)}
    8.99          ultimately show "a$n = ?r $ n" by (cases n, auto)
   8.100        qed}
   8.101      then have "a = ?r" by (simp add: fps_eq_iff)}
   8.102 @@ -2468,7 +2469,7 @@
   8.103  proof-
   8.104    let ?r = "fps_inv"
   8.105    have ra0: "?r a $ 0 = 0" by (simp add: fps_inv_def)
   8.106 -  from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_simps)
   8.107 +  from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_eq_simps)
   8.108    have X0: "X$0 = 0" by simp
   8.109    from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" .
   8.110    then have "?r (?r a) oo ?r a oo a = X oo a" by simp
   8.111 @@ -2485,7 +2486,7 @@
   8.112  proof-
   8.113    let ?r = "fps_ginv"
   8.114    from c0 have rca0: "?r c a $0 = 0" by (simp add: fps_ginv_def)
   8.115 -  from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_simps)
   8.116 +  from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_eq_simps)
   8.117    from fps_ginv[OF rca0 rca1] 
   8.118    have "?r b (?r c a) oo ?r c a = b" .
   8.119    then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp
   8.120 @@ -2533,7 +2534,7 @@
   8.121  proof-
   8.122    {fix n
   8.123      have "?l$n = ?r $ n"
   8.124 -  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
   8.125 +  apply (auto simp add: E_def field_eq_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
   8.126    by (simp add: of_nat_mult ring_simps)}
   8.127  then show ?thesis by (simp add: fps_eq_iff)
   8.128  qed
   8.129 @@ -2544,13 +2545,13 @@
   8.130  proof-
   8.131    {assume d: ?lhs
   8.132    from d have th: "\<And>n. a $ Suc n = c * a$n / of_nat (Suc n)"
   8.133 -    by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc)
   8.134 +    by (simp add: fps_deriv_def fps_eq_iff field_eq_simps del: of_nat_Suc)
   8.135    {fix n have "a$n = a$0 * c ^ n/ (of_nat (fact n))"
   8.136        apply (induct n)
   8.137        apply simp
   8.138        unfolding th
   8.139        using fact_gt_zero_nat
   8.140 -      apply (simp add: field_simps del: of_nat_Suc fact_Suc)
   8.141 +      apply (simp add: field_eq_simps del: of_nat_Suc fact_Suc)
   8.142        apply (drule sym)
   8.143        by (simp add: ring_simps of_nat_mult power_Suc)}
   8.144    note th' = this
   8.145 @@ -2653,13 +2654,13 @@
   8.146    from E_add_mult[of a b] 
   8.147    have "(E (a + b)) $ n = (E a * E b)$n" by simp
   8.148    then have "(a + b) ^ n = (\<Sum>i\<Colon>nat = 0\<Colon>nat..n. a ^ i * b ^ (n - i)  * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
   8.149 -    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
   8.150 +    by (simp add: field_eq_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
   8.151    then show ?thesis 
   8.152      apply simp
   8.153      apply (rule setsum_cong2)
   8.154      apply simp
   8.155      apply (frule binomial_fact[where ?'a = 'a, symmetric])
   8.156 -    by (simp add: field_simps of_nat_mult)
   8.157 +    by (simp add: field_eq_simps of_nat_mult)
   8.158  qed
   8.159  
   8.160  text{* And the nat-form -- also available from Binomial.thy *}
   8.161 @@ -2682,7 +2683,7 @@
   8.162    by (simp add: L_def fps_eq_iff del: of_nat_Suc)
   8.163  
   8.164  lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
   8.165 -  by (simp add: L_def field_simps)
   8.166 +  by (simp add: L_def field_eq_simps)
   8.167  
   8.168  lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def)
   8.169  lemma L_E_inv:
   8.170 @@ -2712,7 +2713,7 @@
   8.171    shows "L c + L d = fps_const (c+d) * L (c*d)"
   8.172    (is "?r = ?l")
   8.173  proof-
   8.174 -  from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
   8.175 +  from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_eq_simps)
   8.176    have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
   8.177      by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add)
   8.178    also have "\<dots> = fps_deriv ?l"
   8.179 @@ -2752,7 +2753,7 @@
   8.180        from lrn 
   8.181        have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" 
   8.182          apply (simp add: ring_simps del: of_nat_Suc)
   8.183 -        by (cases n, simp_all add: field_simps del: of_nat_Suc)
   8.184 +        by (cases n, simp_all add: field_eq_simps del: of_nat_Suc)
   8.185      }
   8.186      note th0 = this
   8.187      {fix n have "a$n = (c gchoose n) * a$0"
   8.188 @@ -2761,7 +2762,7 @@
   8.189        next
   8.190          case (Suc m)
   8.191          thus ?case unfolding th0
   8.192 -          apply (simp add: field_simps del: of_nat_Suc)
   8.193 +          apply (simp add: field_eq_simps del: of_nat_Suc)
   8.194            unfolding mult_assoc[symmetric] gbinomial_mult_1
   8.195            by (simp add: ring_simps)
   8.196        qed}
   8.197 @@ -2879,7 +2880,7 @@
   8.198            using kn pochhammer_minus'[where k=k and n=n and b=b]
   8.199            apply (simp add:  pochhammer_same)
   8.200            using bn0
   8.201 -          by (simp add: field_simps power_add[symmetric])}
   8.202 +          by (simp add: field_eq_simps power_add[symmetric])}
   8.203        moreover
   8.204        {assume nk: "k \<noteq> n"
   8.205          have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" 
   8.206 @@ -2904,7 +2905,7 @@
   8.207            unfolding m1nk 
   8.208            
   8.209            unfolding m h pochhammer_Suc_setprod
   8.210 -          apply (simp add: field_simps del: fact_Suc id_def)
   8.211 +          apply (simp add: field_eq_simps del: fact_Suc id_def)
   8.212            unfolding fact_altdef_nat id_def
   8.213            unfolding of_nat_setprod
   8.214            unfolding setprod_timesf[symmetric]
   8.215 @@ -2941,10 +2942,10 @@
   8.216            apply auto
   8.217            done
   8.218          then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {0.. n - k - 1}" 
   8.219 -          using nz' by (simp add: field_simps)
   8.220 +          using nz' by (simp add: field_eq_simps)
   8.221          have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) = ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)"
   8.222            using bnz0
   8.223 -          by (simp add: field_simps)
   8.224 +          by (simp add: field_eq_simps)
   8.225          also have "\<dots> = b gchoose (n - k)" 
   8.226            unfolding th1 th2
   8.227            using kn' by (simp add: gbinomial_def)
   8.228 @@ -2958,15 +2959,15 @@
   8.229    note th00 = this
   8.230    have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))"
   8.231      unfolding gbinomial_pochhammer 
   8.232 -    using bn0 by (auto simp add: field_simps)
   8.233 +    using bn0 by (auto simp add: field_eq_simps)
   8.234    also have "\<dots> = ?l"
   8.235      unfolding gbinomial_Vandermonde[symmetric]
   8.236      apply (simp add: th00)
   8.237      unfolding gbinomial_pochhammer
   8.238 -    using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps)
   8.239 +    using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_eq_simps)
   8.240      apply (rule setsum_cong2)
   8.241      apply (drule th00(2))
   8.242 -    by (simp add: field_simps power_add[symmetric])
   8.243 +    by (simp add: field_eq_simps power_add[symmetric])
   8.244    finally show ?thesis by simp
   8.245  qed 
   8.246  
   8.247 @@ -2991,7 +2992,7 @@
   8.248    have nz: "pochhammer c n \<noteq> 0" using c
   8.249      by (simp add: pochhammer_eq_0_iff)
   8.250    from Vandermonde_pochhammer_lemma[where a = "?a" and b="?b" and n=n, OF h, unfolded th0 th1]
   8.251 -  show ?thesis using nz by (simp add: field_simps setsum_right_distrib)
   8.252 +  show ?thesis using nz by (simp add: field_eq_simps setsum_right_distrib)
   8.253  qed
   8.254  
   8.255  subsubsection{* Formal trigonometric functions  *}
   8.256 @@ -3013,9 +3014,9 @@
   8.257          using en by (simp add: fps_sin_def)
   8.258        also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
   8.259          unfolding fact_Suc of_nat_mult
   8.260 -        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   8.261 +        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   8.262        also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
   8.263 -        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   8.264 +        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   8.265        finally have "?lhs $n = ?rhs$n" using en
   8.266          by (simp add: fps_cos_def ring_simps power_Suc )}
   8.267      then show "?lhs $ n = ?rhs $ n"
   8.268 @@ -3037,9 +3038,9 @@
   8.269          using en by (simp add: fps_cos_def)
   8.270        also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
   8.271          unfolding fact_Suc of_nat_mult
   8.272 -        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   8.273 +        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   8.274        also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
   8.275 -        by (simp add: field_simps del: of_nat_add of_nat_Suc)
   8.276 +        by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
   8.277        also have "\<dots> = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)"
   8.278          unfolding th0 unfolding th1[OF en] by simp
   8.279        finally have "?lhs $n = ?rhs$n" using en
   8.280 @@ -3345,6 +3346,6 @@
   8.281  
   8.282    shows "foldr (%c r. f c o r) cs (%c. g c a) c0 $ n = 
   8.283    foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
   8.284 -  by (induct cs arbitrary: c0, auto simp add: algebra_simps f )
   8.285 +  by (induct cs arbitrary: c0, auto simp add: algebra_simps f)
   8.286  
   8.287  end
     9.1 --- a/src/HOL/Library/Fraction_Field.thy	Fri Apr 23 16:12:57 2010 +0200
     9.2 +++ b/src/HOL/Library/Fraction_Field.thy	Fri Apr 23 19:32:37 2010 +0200
     9.3 @@ -232,7 +232,7 @@
     9.4  thm mult_eq_0_iff
     9.5  end
     9.6  
     9.7 -instantiation fract :: (idom) "{field, division_by_zero}"
     9.8 +instantiation fract :: (idom) field
     9.9  begin
    9.10  
    9.11  definition
    9.12 @@ -256,9 +256,6 @@
    9.13    by (simp add: divide_fract_def)
    9.14  
    9.15  instance proof
    9.16 -  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
    9.17 -    (simp add: fract_collapse)
    9.18 -next
    9.19    fix q :: "'a fract"
    9.20    assume "q \<noteq> 0"
    9.21    then show "inverse q * q = 1" apply (cases q rule: Fract_cases_nonzero)
    9.22 @@ -270,5 +267,11 @@
    9.23  
    9.24  end
    9.25  
    9.26 +instance fract :: (idom) division_by_zero
    9.27 +proof
    9.28 +  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
    9.29 +    (simp add: fract_collapse)
    9.30 +qed
    9.31 +
    9.32  
    9.33  end
    9.34 \ No newline at end of file
    10.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Apr 23 16:12:57 2010 +0200
    10.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Apr 23 19:32:37 2010 +0200
    10.3 @@ -2780,7 +2780,7 @@
    10.4      from geometric_sum[OF x1, of "Suc n", unfolded x1']
    10.5      have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
    10.6        unfolding atLeastLessThanSuc_atLeastAtMost
    10.7 -      using x1' apply (auto simp only: field_simps)
    10.8 +      using x1' apply (auto simp only: field_eq_simps)
    10.9        apply (simp add: ring_simps)
   10.10        done
   10.11      then have ?thesis by (simp add: ring_simps) }
   10.12 @@ -2815,7 +2815,7 @@
   10.13      {assume x: "x = 1"  hence ?thesis by simp}
   10.14      moreover
   10.15      {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
   10.16 -      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
   10.17 +      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_eq_simps)}
   10.18      ultimately have ?thesis by metis
   10.19    }
   10.20    ultimately show ?thesis by metis
    11.1 --- a/src/HOL/NSA/HDeriv.thy	Fri Apr 23 16:12:57 2010 +0200
    11.2 +++ b/src/HOL/NSA/HDeriv.thy	Fri Apr 23 19:32:37 2010 +0200
    11.3 @@ -204,7 +204,7 @@
    11.4  apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib)
    11.5  apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
    11.6  apply (auto simp add: times_divide_eq_right [symmetric]
    11.7 -            simp del: times_divide_eq)
    11.8 +            simp del: times_divide_eq_right times_divide_eq_left)
    11.9  apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
   11.10  apply (drule_tac
   11.11       approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
    12.1 --- a/src/HOL/Rat.thy	Fri Apr 23 16:12:57 2010 +0200
    12.2 +++ b/src/HOL/Rat.thy	Fri Apr 23 19:32:37 2010 +0200
    12.3 @@ -411,7 +411,7 @@
    12.4  
    12.5  subsubsection {* The field of rational numbers *}
    12.6  
    12.7 -instantiation rat :: "{field, division_by_zero}"
    12.8 +instantiation rat :: field
    12.9  begin
   12.10  
   12.11  definition
   12.12 @@ -433,9 +433,6 @@
   12.13    by (simp add: divide_rat_def)
   12.14  
   12.15  instance proof
   12.16 -  show "inverse 0 = (0::rat)" by (simp add: rat_number_expand)
   12.17 -    (simp add: rat_number_collapse)
   12.18 -next
   12.19    fix q :: rat
   12.20    assume "q \<noteq> 0"
   12.21    then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
   12.22 @@ -447,6 +444,9 @@
   12.23  
   12.24  end
   12.25  
   12.26 +instance rat :: division_by_zero proof
   12.27 +qed (simp add: rat_number_expand, simp add: rat_number_collapse)
   12.28 +
   12.29  
   12.30  subsubsection {* Various *}
   12.31  
    13.1 --- a/src/HOL/Rings.thy	Fri Apr 23 16:12:57 2010 +0200
    13.2 +++ b/src/HOL/Rings.thy	Fri Apr 23 19:32:37 2010 +0200
    13.3 @@ -487,6 +487,125 @@
    13.4    "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
    13.5  by (simp add: algebra_simps)
    13.6  
    13.7 +lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
    13.8 +proof
    13.9 +  assume neq: "b \<noteq> 0"
   13.10 +  {
   13.11 +    hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)
   13.12 +    also assume "a / b = 1"
   13.13 +    finally show "a = b" by simp
   13.14 +  next
   13.15 +    assume "a = b"
   13.16 +    with neq show "a / b = 1" by (simp add: divide_inverse)
   13.17 +  }
   13.18 +qed
   13.19 +
   13.20 +lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
   13.21 +by (simp add: divide_inverse)
   13.22 +
   13.23 +lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
   13.24 +by (simp add: divide_inverse)
   13.25 +
   13.26 +lemma divide_zero_left [simp]: "0 / a = 0"
   13.27 +by (simp add: divide_inverse)
   13.28 +
   13.29 +lemma inverse_eq_divide: "inverse a = 1 / a"
   13.30 +by (simp add: divide_inverse)
   13.31 +
   13.32 +lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
   13.33 +by (simp add: divide_inverse algebra_simps)
   13.34 +
   13.35 +lemma divide_1 [simp]: "a / 1 = a"
   13.36 +  by (simp add: divide_inverse)
   13.37 +
   13.38 +lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
   13.39 +  by (simp add: divide_inverse mult_assoc)
   13.40 +
   13.41 +lemma minus_divide_left: "- (a / b) = (-a) / b"
   13.42 +  by (simp add: divide_inverse)
   13.43 +
   13.44 +lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
   13.45 +  by (simp add: divide_inverse nonzero_inverse_minus_eq)
   13.46 +
   13.47 +lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
   13.48 +  by (simp add: divide_inverse nonzero_inverse_minus_eq)
   13.49 +
   13.50 +lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
   13.51 +  by (simp add: divide_inverse)
   13.52 +
   13.53 +lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
   13.54 +  by (simp add: diff_minus add_divide_distrib)
   13.55 +
   13.56 +lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
   13.57 +proof -
   13.58 +  assume [simp]: "c \<noteq> 0"
   13.59 +  have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
   13.60 +  also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
   13.61 +  finally show ?thesis .
   13.62 +qed
   13.63 +
   13.64 +lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
   13.65 +proof -
   13.66 +  assume [simp]: "c \<noteq> 0"
   13.67 +  have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
   13.68 +  also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc) 
   13.69 +  finally show ?thesis .
   13.70 +qed
   13.71 +
   13.72 +lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
   13.73 +  by (simp add: divide_inverse mult_assoc)
   13.74 +
   13.75 +lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
   13.76 +  by (drule sym) (simp add: divide_inverse mult_assoc)
   13.77 +
   13.78 +end
   13.79 +
   13.80 +class division_by_zero = division_ring +
   13.81 +  assumes inverse_zero [simp]: "inverse 0 = 0"
   13.82 +begin
   13.83 +
   13.84 +lemma divide_zero [simp]:
   13.85 +  "a / 0 = 0"
   13.86 +  by (simp add: divide_inverse)
   13.87 +
   13.88 +lemma divide_self_if [simp]:
   13.89 +  "a / a = (if a = 0 then 0 else 1)"
   13.90 +  by simp
   13.91 +
   13.92 +lemma inverse_nonzero_iff_nonzero [simp]:
   13.93 +  "inverse a = 0 \<longleftrightarrow> a = 0"
   13.94 +  by rule (fact inverse_zero_imp_zero, simp)
   13.95 +
   13.96 +lemma inverse_minus_eq [simp]:
   13.97 +  "inverse (- a) = - inverse a"
   13.98 +proof cases
   13.99 +  assume "a=0" thus ?thesis by simp
  13.100 +next
  13.101 +  assume "a\<noteq>0" 
  13.102 +  thus ?thesis by (simp add: nonzero_inverse_minus_eq)
  13.103 +qed
  13.104 +
  13.105 +lemma inverse_eq_imp_eq:
  13.106 +  "inverse a = inverse b \<Longrightarrow> a = b"
  13.107 +apply (cases "a=0 | b=0") 
  13.108 + apply (force dest!: inverse_zero_imp_zero
  13.109 +              simp add: eq_commute [of "0::'a"])
  13.110 +apply (force dest!: nonzero_inverse_eq_imp_eq) 
  13.111 +done
  13.112 +
  13.113 +lemma inverse_eq_iff_eq [simp]:
  13.114 +  "inverse a = inverse b \<longleftrightarrow> a = b"
  13.115 +  by (force dest!: inverse_eq_imp_eq)
  13.116 +
  13.117 +lemma inverse_inverse_eq [simp]:
  13.118 +  "inverse (inverse a) = a"
  13.119 +proof cases
  13.120 +  assume "a=0" thus ?thesis by simp
  13.121 +next
  13.122 +  assume "a\<noteq>0" 
  13.123 +  thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
  13.124 +qed
  13.125 +
  13.126  end
  13.127  
  13.128  class mult_mono = times + zero + ord +
  13.129 @@ -533,17 +652,17 @@
  13.130  subclass ordered_semiring ..
  13.131  
  13.132  lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
  13.133 -using mult_left_mono [of zero b a] by simp
  13.134 +using mult_left_mono [of 0 b a] by simp
  13.135  
  13.136  lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
  13.137 -using mult_left_mono [of b zero a] by simp
  13.138 +using mult_left_mono [of b 0 a] by simp
  13.139  
  13.140  lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
  13.141 -using mult_right_mono [of a zero b] by simp
  13.142 +using mult_right_mono [of a 0 b] by simp
  13.143  
  13.144  text {* Legacy - use @{text mult_nonpos_nonneg} *}
  13.145  lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
  13.146 -by (drule mult_right_mono [of b zero], auto)
  13.147 +by (drule mult_right_mono [of b 0], auto)
  13.148  
  13.149  lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
  13.150  by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
  13.151 @@ -597,17 +716,17 @@
  13.152  by (force simp add: mult_strict_right_mono not_less [symmetric])
  13.153  
  13.154  lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
  13.155 -using mult_strict_left_mono [of zero b a] by simp
  13.156 +using mult_strict_left_mono [of 0 b a] by simp
  13.157  
  13.158  lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
  13.159 -using mult_strict_left_mono [of b zero a] by simp
  13.160 +using mult_strict_left_mono [of b 0 a] by simp
  13.161  
  13.162  lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
  13.163 -using mult_strict_right_mono [of a zero b] by simp
  13.164 +using mult_strict_right_mono [of a 0 b] by simp
  13.165  
  13.166  text {* Legacy - use @{text mult_neg_pos} *}
  13.167  lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
  13.168 -by (drule mult_strict_right_mono [of b zero], auto)
  13.169 +by (drule mult_strict_right_mono [of b 0], auto)
  13.170  
  13.171  lemma zero_less_mult_pos:
  13.172    "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
  13.173 @@ -763,18 +882,18 @@
  13.174  
  13.175  lemma mult_left_mono_neg:
  13.176    "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
  13.177 -  apply (drule mult_left_mono [of _ _ "uminus c"])
  13.178 +  apply (drule mult_left_mono [of _ _ "- c"])
  13.179    apply simp_all
  13.180    done
  13.181  
  13.182  lemma mult_right_mono_neg:
  13.183    "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
  13.184 -  apply (drule mult_right_mono [of _ _ "uminus c"])
  13.185 +  apply (drule mult_right_mono [of _ _ "- c"])
  13.186    apply simp_all
  13.187    done
  13.188  
  13.189  lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
  13.190 -using mult_right_mono_neg [of a zero b] by simp
  13.191 +using mult_right_mono_neg [of a 0 b] by simp
  13.192  
  13.193  lemma split_mult_pos_le:
  13.194    "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
  13.195 @@ -821,7 +940,7 @@
  13.196  using mult_strict_right_mono [of b a "- c"] by simp
  13.197  
  13.198  lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
  13.199 -using mult_strict_right_mono_neg [of a zero b] by simp
  13.200 +using mult_strict_right_mono_neg [of a 0 b] by simp
  13.201  
  13.202  subclass ring_no_zero_divisors
  13.203  proof
  13.204 @@ -973,7 +1092,7 @@
  13.205  
  13.206  lemma pos_add_strict:
  13.207    shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  13.208 -  using add_strict_mono [of zero a b c] by simp
  13.209 +  using add_strict_mono [of 0 a b c] by simp
  13.210  
  13.211  lemma zero_le_one [simp]: "0 \<le> 1"
  13.212  by (rule zero_less_one [THEN less_imp_le]) 
  13.213 @@ -1074,7 +1193,7 @@
  13.214    "sgn (a * b) = sgn a * sgn b"
  13.215  by (auto simp add: sgn_if zero_less_mult_iff)
  13.216  
  13.217 -lemma abs_sgn: "abs k = k * sgn k"
  13.218 +lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
  13.219  unfolding sgn_if abs_if by auto
  13.220  
  13.221  lemma sgn_greater [simp]:
  13.222 @@ -1085,14 +1204,14 @@
  13.223    "sgn a < 0 \<longleftrightarrow> a < 0"
  13.224    unfolding sgn_if by auto
  13.225  
  13.226 -lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
  13.227 +lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  13.228    by (simp add: abs_if)
  13.229  
  13.230 -lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
  13.231 +lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
  13.232    by (simp add: abs_if)
  13.233  
  13.234  lemma dvd_if_abs_eq:
  13.235 -  "abs l = abs (k) \<Longrightarrow> l dvd k"
  13.236 +  "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
  13.237  by(subst abs_dvd_iff[symmetric]) simp
  13.238  
  13.239  end
  13.240 @@ -1110,17 +1229,7 @@
  13.241      mult_cancel_right1 mult_cancel_right2
  13.242      mult_cancel_left1 mult_cancel_left2
  13.243  
  13.244 --- {* FIXME continue localization here *}
  13.245 -
  13.246 -subsection {* Reasoning about inequalities with division *}
  13.247 -
  13.248 -lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  13.249 -    ==> x * y <= x"
  13.250 -by (auto simp add: mult_le_cancel_left2)
  13.251 -
  13.252 -lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
  13.253 -    ==> y * x <= x"
  13.254 -by (auto simp add: mult_le_cancel_right2)
  13.255 +text {* Reasoning about inequalities with division *}
  13.256  
  13.257  context linordered_semidom
  13.258  begin
  13.259 @@ -1137,20 +1246,34 @@
  13.260  
  13.261  end
  13.262  
  13.263 +context linordered_idom
  13.264 +begin
  13.265  
  13.266 -subsection {* Absolute Value *}
  13.267 +lemma mult_right_le_one_le:
  13.268 +  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  13.269 +  by (auto simp add: mult_le_cancel_left2)
  13.270 +
  13.271 +lemma mult_left_le_one_le:
  13.272 +  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  13.273 +  by (auto simp add: mult_le_cancel_right2)
  13.274 +
  13.275 +end
  13.276 +
  13.277 +text {* Absolute Value *}
  13.278  
  13.279  context linordered_idom
  13.280  begin
  13.281  
  13.282 -lemma mult_sgn_abs: "sgn x * abs x = x"
  13.283 +lemma mult_sgn_abs:
  13.284 +  "sgn x * \<bar>x\<bar> = x"
  13.285    unfolding abs_if sgn_if by auto
  13.286  
  13.287 +lemma abs_one [simp]:
  13.288 +  "\<bar>1\<bar> = 1"
  13.289 +  by (simp add: abs_if zero_less_one [THEN less_not_sym])
  13.290 +
  13.291  end
  13.292  
  13.293 -lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)"
  13.294 -by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
  13.295 -
  13.296  class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
  13.297    assumes abs_eq_mult:
  13.298      "(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>"
  13.299 @@ -1162,39 +1285,35 @@
  13.300  qed (auto simp add: abs_if not_less mult_less_0_iff)
  13.301  
  13.302  lemma abs_mult:
  13.303 -  "abs (a * b) = abs a * abs b" 
  13.304 +  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
  13.305    by (rule abs_eq_mult) auto
  13.306  
  13.307  lemma abs_mult_self:
  13.308 -  "abs a * abs a = a * a"
  13.309 +  "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  13.310    by (simp add: abs_if) 
  13.311  
  13.312 -end
  13.313 -
  13.314  lemma abs_mult_less:
  13.315 -     "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)"
  13.316 +  "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
  13.317  proof -
  13.318 -  assume ac: "abs a < c"
  13.319 -  hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
  13.320 -  assume "abs b < d"
  13.321 +  assume ac: "\<bar>a\<bar> < c"
  13.322 +  hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
  13.323 +  assume "\<bar>b\<bar> < d"
  13.324    thus ?thesis by (simp add: ac cpos mult_strict_mono) 
  13.325  qed
  13.326  
  13.327 -lemmas eq_minus_self_iff[no_atp] = equal_neg_zero
  13.328 -
  13.329 -lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
  13.330 -  unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
  13.331 +lemma less_minus_self_iff:
  13.332 +  "a < - a \<longleftrightarrow> a < 0"
  13.333 +  by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)
  13.334  
  13.335 -lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))" 
  13.336 -apply (simp add: order_less_le abs_le_iff)  
  13.337 -apply (auto simp add: abs_if)
  13.338 -done
  13.339 +lemma abs_less_iff:
  13.340 +  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
  13.341 +  by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
  13.342  
  13.343 -lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> 
  13.344 -    (abs y) * x = abs (y * x)"
  13.345 -  apply (subst abs_mult)
  13.346 -  apply simp
  13.347 -done
  13.348 +lemma abs_mult_pos:
  13.349 +  "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
  13.350 +  by (simp add: abs_mult)
  13.351 +
  13.352 +end
  13.353  
  13.354  code_modulename SML
  13.355    Rings Arith
    14.1 --- a/src/HOL/SetInterval.thy	Fri Apr 23 16:12:57 2010 +0200
    14.2 +++ b/src/HOL/SetInterval.thy	Fri Apr 23 19:32:37 2010 +0200
    14.3 @@ -1012,7 +1012,7 @@
    14.4  qed
    14.5  
    14.6  lemma setsum_le_included:
    14.7 -  fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,ordered_ab_semigroup_add_imp_le}"
    14.8 +  fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
    14.9    assumes "finite s" "finite t"
   14.10    and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)"
   14.11    shows "setsum f s \<le> setsum g t"
   14.12 @@ -1085,9 +1085,21 @@
   14.13  subsection {* The formula for geometric sums *}
   14.14  
   14.15  lemma geometric_sum:
   14.16 -  "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
   14.17 -  (x ^ n - 1) / (x - 1::'a::{field})"
   14.18 -by (induct "n") (simp_all add: field_simps)
   14.19 +  assumes "x \<noteq> 1"
   14.20 +  shows "(\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)"
   14.21 +proof -
   14.22 +  from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
   14.23 +  moreover have "(\<Sum>i=0..<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
   14.24 +  proof (induct n)
   14.25 +    case 0 then show ?case by simp
   14.26 +  next
   14.27 +    case (Suc n)
   14.28 +    moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp 
   14.29 +    ultimately show ?case by (simp add: field_eq_simps divide_inverse)
   14.30 +  qed
   14.31 +  ultimately show ?thesis by simp
   14.32 +qed
   14.33 +
   14.34  
   14.35  subsection {* The formula for arithmetic sums *}
   14.36  
    15.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Apr 23 16:12:57 2010 +0200
    15.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Apr 23 19:32:37 2010 +0200
    15.3 @@ -12,6 +12,137 @@
    15.4  structure Datatype_Codegen : DATATYPE_CODEGEN =
    15.5  struct
    15.6  
    15.7 +(** generic code generator **)
    15.8 +
    15.9 +(* liberal addition of code data for datatypes *)
   15.10 +
   15.11 +fun mk_constr_consts thy vs dtco cos =
   15.12 +  let
   15.13 +    val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
   15.14 +    val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
   15.15 +  in if is_some (try (Code.constrset_of_consts thy) cs')
   15.16 +    then SOME cs
   15.17 +    else NONE
   15.18 +  end;
   15.19 +
   15.20 +
   15.21 +(* case certificates *)
   15.22 +
   15.23 +fun mk_case_cert thy tyco =
   15.24 +  let
   15.25 +    val raw_thms =
   15.26 +      (#case_rewrites o Datatype_Data.the_info thy) tyco;
   15.27 +    val thms as hd_thm :: _ = raw_thms
   15.28 +      |> Conjunction.intr_balanced
   15.29 +      |> Thm.unvarify_global
   15.30 +      |> Conjunction.elim_balanced (length raw_thms)
   15.31 +      |> map Simpdata.mk_meta_eq
   15.32 +      |> map Drule.zero_var_indexes
   15.33 +    val params = fold_aterms (fn (Free (v, _)) => insert (op =) v
   15.34 +      | _ => I) (Thm.prop_of hd_thm) [];
   15.35 +    val rhs = hd_thm
   15.36 +      |> Thm.prop_of
   15.37 +      |> Logic.dest_equals
   15.38 +      |> fst
   15.39 +      |> Term.strip_comb
   15.40 +      |> apsnd (fst o split_last)
   15.41 +      |> list_comb;
   15.42 +    val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
   15.43 +    val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
   15.44 +  in
   15.45 +    thms
   15.46 +    |> Conjunction.intr_balanced
   15.47 +    |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
   15.48 +    |> Thm.implies_intr asm
   15.49 +    |> Thm.generalize ([], params) 0
   15.50 +    |> AxClass.unoverload thy
   15.51 +    |> Thm.varifyT_global
   15.52 +  end;
   15.53 +
   15.54 +
   15.55 +(* equality *)
   15.56 +
   15.57 +fun mk_eq_eqns thy dtco =
   15.58 +  let
   15.59 +    val (vs, cos) = Datatype_Data.the_spec thy dtco;
   15.60 +    val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
   15.61 +      Datatype_Data.the_info thy dtco;
   15.62 +    val ty = Type (dtco, map TFree vs);
   15.63 +    fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
   15.64 +      $ t1 $ t2;
   15.65 +    fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
   15.66 +    fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
   15.67 +    val triv_injects = map_filter
   15.68 +     (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
   15.69 +       | _ => NONE) cos;
   15.70 +    fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
   15.71 +      trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
   15.72 +    val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
   15.73 +    fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
   15.74 +      [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
   15.75 +    val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
   15.76 +    val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
   15.77 +    val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps 
   15.78 +      (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
   15.79 +    fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
   15.80 +      |> Simpdata.mk_eq;
   15.81 +  in (map prove (triv_injects @ injects @ distincts), prove refl) end;
   15.82 +
   15.83 +fun add_equality vs dtcos thy =
   15.84 +  let
   15.85 +    fun add_def dtco lthy =
   15.86 +      let
   15.87 +        val ty = Type (dtco, map TFree vs);
   15.88 +        fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
   15.89 +          $ Free ("x", ty) $ Free ("y", ty);
   15.90 +        val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
   15.91 +          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
   15.92 +        val def' = Syntax.check_term lthy def;
   15.93 +        val ((_, (_, thm)), lthy') = Specification.definition
   15.94 +          (NONE, (Attrib.empty_binding, def')) lthy;
   15.95 +        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
   15.96 +        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   15.97 +      in (thm', lthy') end;
   15.98 +    fun tac thms = Class.intro_classes_tac []
   15.99 +      THEN ALLGOALS (ProofContext.fact_tac thms);
  15.100 +    fun add_eq_thms dtco =
  15.101 +      Theory.checkpoint
  15.102 +      #> `(fn thy => mk_eq_eqns thy dtco)
  15.103 +      #-> (fn (thms, thm) =>
  15.104 +        Code.add_nbe_eqn thm
  15.105 +        #> fold_rev Code.add_eqn thms);
  15.106 +  in
  15.107 +    thy
  15.108 +    |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
  15.109 +    |> fold_map add_def dtcos
  15.110 +    |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
  15.111 +         (fn _ => fn def_thms => tac def_thms) def_thms)
  15.112 +    |-> (fn def_thms => fold Code.del_eqn def_thms)
  15.113 +    |> fold add_eq_thms dtcos
  15.114 +  end;
  15.115 +
  15.116 +
  15.117 +(* register a datatype etc. *)
  15.118 +
  15.119 +fun add_all_code config dtcos thy =
  15.120 +  let
  15.121 +    val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) dtcos;
  15.122 +    val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
  15.123 +    val css = if exists is_none any_css then []
  15.124 +      else map_filter I any_css;
  15.125 +    val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) dtcos;
  15.126 +    val certs = map (mk_case_cert thy) dtcos;
  15.127 +  in
  15.128 +    if null css then thy
  15.129 +    else thy
  15.130 +      |> tap (fn _ => Datatype_Aux.message config "Registering datatype for code generator ...")
  15.131 +      |> fold Code.add_datatype css
  15.132 +      |> fold_rev Code.add_default_eqn case_rewrites
  15.133 +      |> fold Code.add_case certs
  15.134 +      |> add_equality vs dtcos
  15.135 +   end;
  15.136 +
  15.137 +
  15.138  (** SML code generator **)
  15.139  
  15.140  open Codegen;
  15.141 @@ -288,142 +419,11 @@
  15.142    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
  15.143  
  15.144  
  15.145 -(** generic code generator **)
  15.146 -
  15.147 -(* liberal addition of code data for datatypes *)
  15.148 -
  15.149 -fun mk_constr_consts thy vs dtco cos =
  15.150 -  let
  15.151 -    val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
  15.152 -    val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
  15.153 -  in if is_some (try (Code.constrset_of_consts thy) cs')
  15.154 -    then SOME cs
  15.155 -    else NONE
  15.156 -  end;
  15.157 -
  15.158 -
  15.159 -(* case certificates *)
  15.160 -
  15.161 -fun mk_case_cert thy tyco =
  15.162 -  let
  15.163 -    val raw_thms =
  15.164 -      (#case_rewrites o Datatype_Data.the_info thy) tyco;
  15.165 -    val thms as hd_thm :: _ = raw_thms
  15.166 -      |> Conjunction.intr_balanced
  15.167 -      |> Thm.unvarify_global
  15.168 -      |> Conjunction.elim_balanced (length raw_thms)
  15.169 -      |> map Simpdata.mk_meta_eq
  15.170 -      |> map Drule.zero_var_indexes
  15.171 -    val params = fold_aterms (fn (Free (v, _)) => insert (op =) v
  15.172 -      | _ => I) (Thm.prop_of hd_thm) [];
  15.173 -    val rhs = hd_thm
  15.174 -      |> Thm.prop_of
  15.175 -      |> Logic.dest_equals
  15.176 -      |> fst
  15.177 -      |> Term.strip_comb
  15.178 -      |> apsnd (fst o split_last)
  15.179 -      |> list_comb;
  15.180 -    val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
  15.181 -    val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
  15.182 -  in
  15.183 -    thms
  15.184 -    |> Conjunction.intr_balanced
  15.185 -    |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
  15.186 -    |> Thm.implies_intr asm
  15.187 -    |> Thm.generalize ([], params) 0
  15.188 -    |> AxClass.unoverload thy
  15.189 -    |> Thm.varifyT_global
  15.190 -  end;
  15.191 -
  15.192 -
  15.193 -(* equality *)
  15.194 -
  15.195 -fun mk_eq_eqns thy dtco =
  15.196 -  let
  15.197 -    val (vs, cos) = Datatype_Data.the_spec thy dtco;
  15.198 -    val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
  15.199 -      Datatype_Data.the_info thy dtco;
  15.200 -    val ty = Type (dtco, map TFree vs);
  15.201 -    fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
  15.202 -      $ t1 $ t2;
  15.203 -    fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
  15.204 -    fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
  15.205 -    val triv_injects = map_filter
  15.206 -     (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
  15.207 -       | _ => NONE) cos;
  15.208 -    fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
  15.209 -      trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
  15.210 -    val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
  15.211 -    fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
  15.212 -      [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
  15.213 -    val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
  15.214 -    val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
  15.215 -    val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps 
  15.216 -      (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
  15.217 -    fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
  15.218 -      |> Simpdata.mk_eq;
  15.219 -  in (map prove (triv_injects @ injects @ distincts), prove refl) end;
  15.220 -
  15.221 -fun add_equality vs dtcos thy =
  15.222 -  let
  15.223 -    fun add_def dtco lthy =
  15.224 -      let
  15.225 -        val ty = Type (dtco, map TFree vs);
  15.226 -        fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
  15.227 -          $ Free ("x", ty) $ Free ("y", ty);
  15.228 -        val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
  15.229 -          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
  15.230 -        val def' = Syntax.check_term lthy def;
  15.231 -        val ((_, (_, thm)), lthy') = Specification.definition
  15.232 -          (NONE, (Attrib.empty_binding, def')) lthy;
  15.233 -        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
  15.234 -        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
  15.235 -      in (thm', lthy') end;
  15.236 -    fun tac thms = Class.intro_classes_tac []
  15.237 -      THEN ALLGOALS (ProofContext.fact_tac thms);
  15.238 -    fun add_eq_thms dtco =
  15.239 -      Theory.checkpoint
  15.240 -      #> `(fn thy => mk_eq_eqns thy dtco)
  15.241 -      #-> (fn (thms, thm) =>
  15.242 -        Code.add_nbe_eqn thm
  15.243 -        #> fold_rev Code.add_eqn thms);
  15.244 -  in
  15.245 -    thy
  15.246 -    |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
  15.247 -    |> fold_map add_def dtcos
  15.248 -    |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
  15.249 -         (fn _ => fn def_thms => tac def_thms) def_thms)
  15.250 -    |-> (fn def_thms => fold Code.del_eqn def_thms)
  15.251 -    |> fold add_eq_thms dtcos
  15.252 -  end;
  15.253 -
  15.254 -
  15.255 -(* register a datatype etc. *)
  15.256 -
  15.257 -fun add_all_code config dtcos thy =
  15.258 -  let
  15.259 -    val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) dtcos;
  15.260 -    val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
  15.261 -    val css = if exists is_none any_css then []
  15.262 -      else map_filter I any_css;
  15.263 -    val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) dtcos;
  15.264 -    val certs = map (mk_case_cert thy) dtcos;
  15.265 -  in
  15.266 -    if null css then thy
  15.267 -    else thy
  15.268 -      |> tap (fn _ => Datatype_Aux.message config "Registering datatype for code generator ...")
  15.269 -      |> fold Code.add_datatype css
  15.270 -      |> fold_rev Code.add_default_eqn case_rewrites
  15.271 -      |> fold Code.add_case certs
  15.272 -      |> add_equality vs dtcos
  15.273 -   end;
  15.274 -
  15.275 -
  15.276  (** theory setup **)
  15.277  
  15.278  val setup = 
  15.279 -  add_codegen "datatype" datatype_codegen
  15.280 -  #> add_tycodegen "datatype" datatype_tycodegen
  15.281 -  #> Datatype_Data.interpretation add_all_code
  15.282 +  Datatype_Data.interpretation add_all_code
  15.283 +  #> add_codegen "datatype" datatype_codegen
  15.284 +  #> add_tycodegen "datatype" datatype_tycodegen;
  15.285  
  15.286  end;