given up separate type classes demanding `inverse 0 = 0`
authorhaftmann
Tue Mar 31 21:54:32 2015 +0200 (2015-03-31)
changeset 5986758043346ca64
parent 59866 eebe69f31474
child 59868 b1cd0c962780
given up separate type classes demanding `inverse 0 = 0`
src/HOL/Binomial.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy
src/HOL/Deriv.thy
src/HOL/Enum.thy
src/HOL/Fields.thy
src/HOL/Groups_Big.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Bit.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Limits.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/Multivariate_Analysis/PolyRoots.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/StarDef.thy
src/HOL/Num.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Power.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Interval_Integral.thy
src/HOL/Probability/Set_Integral.thy
src/HOL/Quotient_Examples/Quotient_Rat.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Transcendental.thy
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/Simproc_Tests.thy
     1.1 --- a/src/HOL/Binomial.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Binomial.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -549,11 +549,7 @@
     1.4      (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / (fact n))"
     1.5  
     1.6  lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
     1.7 -  apply (simp_all add: gbinomial_def)
     1.8 -  apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
     1.9 -   apply (simp del:setprod_zero_iff)
    1.10 -  apply simp
    1.11 -  done
    1.12 +  by (simp_all add: gbinomial_def)
    1.13  
    1.14  lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"
    1.15  proof (cases "n = 0")
    1.16 @@ -721,7 +717,7 @@
    1.17    Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"} *}
    1.18  lemma gbinomial_altdef_of_nat:
    1.19    fixes k :: nat
    1.20 -    and x :: "'a :: {field_char_0,field_inverse_zero}"
    1.21 +    and x :: "'a :: {field_char_0,field}"
    1.22    shows "x gchoose k = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
    1.23  proof -
    1.24    have "(x gchoose k) = (\<Prod>i<k. x - of_nat i) / of_nat (fact k)"
    1.25 @@ -735,7 +731,7 @@
    1.26  
    1.27  lemma gbinomial_ge_n_over_k_pow_k:
    1.28    fixes k :: nat
    1.29 -    and x :: "'a :: linordered_field_inverse_zero"
    1.30 +    and x :: "'a :: linordered_field"
    1.31    assumes "of_nat k \<le> x"
    1.32    shows "(x / of_nat k :: 'a) ^ k \<le> x gchoose k"
    1.33  proof -
    1.34 @@ -765,7 +761,7 @@
    1.35  text{*Versions of the theorems above for the natural-number version of "choose"*}
    1.36  lemma binomial_altdef_of_nat:
    1.37    fixes n k :: nat
    1.38 -    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}*}
    1.39 +    and x :: "'a :: {field_char_0,field}"  --{*the point is to constrain @{typ 'a}*}
    1.40    assumes "k \<le> n"
    1.41    shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
    1.42  using assms
    1.43 @@ -773,7 +769,7 @@
    1.44  
    1.45  lemma binomial_ge_n_over_k_pow_k:
    1.46    fixes k n :: nat
    1.47 -    and x :: "'a :: linordered_field_inverse_zero"
    1.48 +    and x :: "'a :: linordered_field"
    1.49    assumes "k \<le> n"
    1.50    shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
    1.51  by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)
     2.1 --- a/src/HOL/Complex.thy	Tue Mar 31 16:49:41 2015 +0100
     2.2 +++ b/src/HOL/Complex.thy	Tue Mar 31 21:54:32 2015 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4  
     2.5  subsection {* Multiplication and Division *}
     2.6  
     2.7 -instantiation complex :: field_inverse_zero
     2.8 +instantiation complex :: field
     2.9  begin
    2.10  
    2.11  primcorec one_complex where
     3.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Mar 31 16:49:41 2015 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Mar 31 21:54:32 2015 +0200
     3.3 @@ -30,7 +30,7 @@
     3.4  | "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
     3.5  
     3.6  (* Semantics of terms tm *)
     3.7 -primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     3.8 +primrec Itm :: "'a::{field_char_0, field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     3.9  where
    3.10    "Itm vs bs (CP c) = (Ipoly vs c)"
    3.11  | "Itm vs bs (Bound n) = bs!n"
    3.12 @@ -311,7 +311,7 @@
    3.13    by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
    3.14  
    3.15  lemma tmmul_allpolys_npoly[simp]:
    3.16 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.17 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
    3.18    shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)"
    3.19    by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)
    3.20  
    3.21 @@ -337,7 +337,7 @@
    3.22    unfolding isnpoly_def by simp
    3.23  
    3.24  lemma tmneg_allpolys_npoly[simp]:
    3.25 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.26 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
    3.27    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
    3.28    unfolding tmneg_def by auto
    3.29  
    3.30 @@ -354,7 +354,7 @@
    3.31    using tmsub_def by simp
    3.32  
    3.33  lemma tmsub_allpolys_npoly[simp]:
    3.34 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.35 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
    3.36    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
    3.37    unfolding tmsub_def by (simp add: isnpoly_def)
    3.38  
    3.39 @@ -371,7 +371,7 @@
    3.40      (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
    3.41  
    3.42  lemma polynate_stupid:
    3.43 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.44 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
    3.45    shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
    3.46    apply (subst polynate[symmetric])
    3.47    apply simp
    3.48 @@ -394,7 +394,7 @@
    3.49    by (simp_all add: isnpoly_def)
    3.50  
    3.51  lemma simptm_allpolys_npoly[simp]:
    3.52 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.53 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
    3.54    shows "allpolys isnpoly (simptm p)"
    3.55    by (induct p rule: simptm.induct) (auto simp add: Let_def)
    3.56  
    3.57 @@ -445,7 +445,7 @@
    3.58  qed
    3.59  
    3.60  lemma split0_nb0:
    3.61 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.62 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
    3.63    shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
    3.64  proof -
    3.65    fix c' t'
    3.66 @@ -457,7 +457,7 @@
    3.67  qed
    3.68  
    3.69  lemma split0_nb0'[simp]:
    3.70 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.71 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
    3.72    shows "tmbound0 (snd (split0 t))"
    3.73    using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
    3.74    by (simp add: tmbound0_tmbound_iff)
    3.75 @@ -485,7 +485,7 @@
    3.76    by (induct p rule: split0.induct) (auto simp  add: isnpoly_def Let_def split_def)
    3.77  
    3.78  lemma isnpoly_fst_split0:
    3.79 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.80 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
    3.81    shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
    3.82    by (induct p rule: split0.induct)
    3.83      (auto simp  add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)
    3.84 @@ -514,7 +514,7 @@
    3.85    by (induct p rule: fmsize.induct) simp_all
    3.86  
    3.87    (* Semantics of formulae (fm) *)
    3.88 -primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
    3.89 +primrec Ifm ::"'a::{linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
    3.90  where
    3.91    "Ifm vs bs T = True"
    3.92  | "Ifm vs bs F = False"
    3.93 @@ -1146,7 +1146,7 @@
    3.94  definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"
    3.95  
    3.96  lemma simplt_islin[simp]:
    3.97 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.98 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
    3.99    shows "islin (simplt t)"
   3.100    unfolding simplt_def
   3.101    using split0_nb0'
   3.102 @@ -1154,7 +1154,7 @@
   3.103        islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
   3.104  
   3.105  lemma simple_islin[simp]:
   3.106 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.107 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.108    shows "islin (simple t)"
   3.109    unfolding simple_def
   3.110    using split0_nb0'
   3.111 @@ -1162,7 +1162,7 @@
   3.112        islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
   3.113  
   3.114  lemma simpeq_islin[simp]:
   3.115 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.116 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.117    shows "islin (simpeq t)"
   3.118    unfolding simpeq_def
   3.119    using split0_nb0'
   3.120 @@ -1170,7 +1170,7 @@
   3.121        islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
   3.122  
   3.123  lemma simpneq_islin[simp]:
   3.124 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.125 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.126    shows "islin (simpneq t)"
   3.127    unfolding simpneq_def
   3.128    using split0_nb0'
   3.129 @@ -1181,7 +1181,7 @@
   3.130    by (cases "split0 s") auto
   3.131  
   3.132  lemma split0_npoly:
   3.133 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.134 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.135      and n: "allpolys isnpoly t"
   3.136    shows "isnpoly (fst (split0 t))"
   3.137      and "allpolys isnpoly (snd (split0 t))"
   3.138 @@ -1305,7 +1305,7 @@
   3.139    done
   3.140  
   3.141  lemma simplt_nb[simp]:
   3.142 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.143 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.144    shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
   3.145  proof (simp add: simplt_def Let_def split_def)
   3.146    assume nb: "tmbound0 t"
   3.147 @@ -1326,7 +1326,7 @@
   3.148  qed
   3.149  
   3.150  lemma simple_nb[simp]:
   3.151 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.152 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.153    shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
   3.154  proof(simp add: simple_def Let_def split_def)
   3.155    assume nb: "tmbound0 t"
   3.156 @@ -1347,7 +1347,7 @@
   3.157  qed
   3.158  
   3.159  lemma simpeq_nb[simp]:
   3.160 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.161 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.162    shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
   3.163  proof (simp add: simpeq_def Let_def split_def)
   3.164    assume nb: "tmbound0 t"
   3.165 @@ -1368,7 +1368,7 @@
   3.166  qed
   3.167  
   3.168  lemma simpneq_nb[simp]:
   3.169 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.170 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.171    shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
   3.172  proof (simp add: simpneq_def Let_def split_def)
   3.173    assume nb: "tmbound0 t"
   3.174 @@ -1526,7 +1526,7 @@
   3.175    by (induct p arbitrary: bs rule: simpfm.induct) auto
   3.176  
   3.177  lemma simpfm_bound0:
   3.178 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.179 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.180    shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   3.181    by (induct p rule: simpfm.induct) auto
   3.182  
   3.183 @@ -1567,7 +1567,7 @@
   3.184    by (simp add: conj_def)
   3.185  
   3.186  lemma
   3.187 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.188 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.189    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   3.190    by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
   3.191  
   3.192 @@ -3379,7 +3379,7 @@
   3.193  qed
   3.194  
   3.195  lemma simpfm_lin:
   3.196 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.197 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.198    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   3.199    by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)
   3.200  
   3.201 @@ -3704,7 +3704,7 @@
   3.202      (auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
   3.203  
   3.204  lemma msubstneg_nb:
   3.205 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.206 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.207      and lp: "islin p"
   3.208      and tnb: "tmbound0 t"
   3.209    shows "bound0 (msubstneg p c t)"
   3.210 @@ -3713,7 +3713,7 @@
   3.211      (auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
   3.212  
   3.213  lemma msubst2_nb:
   3.214 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.215 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   3.216      and lp: "islin p"
   3.217      and tnb: "tmbound0 t"
   3.218    shows "bound0 (msubst2 p c t)"
   3.219 @@ -4196,7 +4196,7 @@
   3.220    Parametric_Ferrante_Rackoff.method true
   3.221  *} "parametric QE for linear Arithmetic over fields, Version 2"
   3.222  
   3.223 -lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
   3.224 +lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
   3.225    apply (frpar type: 'a pars: y)
   3.226    apply (simp add: field_simps)
   3.227    apply (rule spec[where x=y])
   3.228 @@ -4204,7 +4204,7 @@
   3.229    apply simp
   3.230    done
   3.231  
   3.232 -lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   3.233 +lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   3.234    apply (frpar2 type: 'a pars: y)
   3.235    apply (simp add: field_simps)
   3.236    apply (rule spec[where x=y])
   3.237 @@ -4214,38 +4214,38 @@
   3.238  
   3.239  text{* Collins/Jones Problem *}
   3.240  (*
   3.241 -lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   3.242 +lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   3.243  proof-
   3.244 -  have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   3.245 +  have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   3.246  by (simp add: field_simps)
   3.247  have "?rhs"
   3.248  
   3.249 -  apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "a::'a::{linordered_field_inverse_zero, number_ring}" "b::'a::{linordered_field_inverse_zero, number_ring}")
   3.250 +  apply (frpar type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")
   3.251    apply (simp add: field_simps)
   3.252  oops
   3.253  *)
   3.254  (*
   3.255 -lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   3.256 -apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
   3.257 +lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   3.258 +apply (frpar type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
   3.259  oops
   3.260  *)
   3.261  
   3.262  text{* Collins/Jones Problem *}
   3.263  
   3.264  (*
   3.265 -lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   3.266 +lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   3.267  proof-
   3.268 -  have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   3.269 +  have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   3.270  by (simp add: field_simps)
   3.271  have "?rhs"
   3.272 -  apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "a::'a::{linordered_field_inverse_zero, number_ring}" "b::'a::{linordered_field_inverse_zero, number_ring}")
   3.273 +  apply (frpar2 type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")
   3.274    apply simp
   3.275  oops
   3.276  *)
   3.277  
   3.278  (*
   3.279 -lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   3.280 -apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
   3.281 +lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   3.282 +apply (frpar2 type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
   3.283  apply (simp add: field_simps linorder_neq_iff[symmetric])
   3.284  apply ferrack
   3.285  oops
     4.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Tue Mar 31 16:49:41 2015 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Tue Mar 31 21:54:32 2015 +0200
     4.3 @@ -156,7 +156,7 @@
     4.4  
     4.5  lemma isnormNum_unique[simp]:
     4.6    assumes na: "isnormNum x" and nb: "isnormNum y"
     4.7 -  shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
     4.8 +  shows "((INum x ::'a::{field_char_0, field}) = INum y) = (x = y)" (is "?lhs = ?rhs")
     4.9  proof
    4.10    obtain a b where x: "x = (a, b)" by (cases x)
    4.11    obtain a' b' where y: "y = (a', b')" by (cases y)
    4.12 @@ -190,7 +190,7 @@
    4.13  
    4.14  
    4.15  lemma isnormNum0[simp]:
    4.16 -    "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
    4.17 +    "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field})) = (x = 0\<^sub>N)"
    4.18    unfolding INum_int(2)[symmetric]
    4.19    by (rule isnormNum_unique) simp_all
    4.20  
    4.21 @@ -213,7 +213,7 @@
    4.22      (of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
    4.23    using of_int_div_aux [of d n, where ?'a = 'a] by simp
    4.24  
    4.25 -lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
    4.26 +lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field})"
    4.27  proof -
    4.28    obtain a b where x: "x = (a, b)" by (cases x)
    4.29    { assume "a = 0 \<or> b = 0"
    4.30 @@ -228,7 +228,7 @@
    4.31  qed
    4.32  
    4.33  lemma INum_normNum_iff:
    4.34 -  "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y"
    4.35 +  "(INum x ::'a::{field_char_0, field}) = INum y \<longleftrightarrow> normNum x = normNum y"
    4.36    (is "?lhs = ?rhs")
    4.37  proof -
    4.38    have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
    4.39 @@ -237,7 +237,7 @@
    4.40    finally show ?thesis by simp
    4.41  qed
    4.42  
    4.43 -lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
    4.44 +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field})"
    4.45  proof -
    4.46    let ?z = "0:: 'a"
    4.47    obtain a b where x: "x = (a, b)" by (cases x)
    4.48 @@ -274,7 +274,7 @@
    4.49    ultimately show ?thesis by blast
    4.50  qed
    4.51  
    4.52 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})"
    4.53 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field})"
    4.54  proof -
    4.55    let ?z = "0::'a"
    4.56    obtain a b where x: "x = (a, b)" by (cases x)
    4.57 @@ -298,18 +298,18 @@
    4.58  lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
    4.59    by (simp add: Nneg_def split_def INum_def)
    4.60  
    4.61 -lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
    4.62 +lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field})"
    4.63    by (simp add: Nsub_def split_def)
    4.64  
    4.65 -lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
    4.66 +lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field) / (INum x)"
    4.67    by (simp add: Ninv_def INum_def split_def)
    4.68  
    4.69 -lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})"
    4.70 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field})"
    4.71    by (simp add: Ndiv_def)
    4.72  
    4.73  lemma Nlt0_iff[simp]:
    4.74    assumes nx: "isnormNum x"
    4.75 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x"
    4.76 +  shows "((INum x :: 'a :: {field_char_0, linordered_field})< 0) = 0>\<^sub>N x"
    4.77  proof -
    4.78    obtain a b where x: "x = (a, b)" by (cases x)
    4.79    { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) }
    4.80 @@ -323,7 +323,7 @@
    4.81  
    4.82  lemma Nle0_iff[simp]:
    4.83    assumes nx: "isnormNum x"
    4.84 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
    4.85 +  shows "((INum x :: 'a :: {field_char_0, linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
    4.86  proof -
    4.87    obtain a b where x: "x = (a, b)" by (cases x)
    4.88    { assume "a = 0" hence ?thesis by (simp add: x Nle0_def INum_def) }
    4.89 @@ -337,7 +337,7 @@
    4.90  
    4.91  lemma Ngt0_iff[simp]:
    4.92    assumes nx: "isnormNum x"
    4.93 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
    4.94 +  shows "((INum x :: 'a :: {field_char_0, linordered_field})> 0) = 0<\<^sub>N x"
    4.95  proof -
    4.96    obtain a b where x: "x = (a, b)" by (cases x)
    4.97    { assume "a = 0" hence ?thesis by (simp add: x Ngt0_def INum_def) }
    4.98 @@ -351,7 +351,7 @@
    4.99  
   4.100  lemma Nge0_iff[simp]:
   4.101    assumes nx: "isnormNum x"
   4.102 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
   4.103 +  shows "((INum x :: 'a :: {field_char_0, linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
   4.104  proof -
   4.105    obtain a b where x: "x = (a, b)" by (cases x)
   4.106    { assume "a = 0" hence ?thesis by (simp add: x Nge0_def INum_def) }
   4.107 @@ -365,7 +365,7 @@
   4.108  
   4.109  lemma Nlt_iff[simp]:
   4.110    assumes nx: "isnormNum x" and ny: "isnormNum y"
   4.111 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
   4.112 +  shows "((INum x :: 'a :: {field_char_0, linordered_field}) < INum y) = (x <\<^sub>N y)"
   4.113  proof -
   4.114    let ?z = "0::'a"
   4.115    have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)"
   4.116 @@ -377,7 +377,7 @@
   4.117  
   4.118  lemma Nle_iff[simp]:
   4.119    assumes nx: "isnormNum x" and ny: "isnormNum y"
   4.120 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
   4.121 +  shows "((INum x :: 'a :: {field_char_0, linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
   4.122  proof -
   4.123    have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))"
   4.124      using nx ny by simp
   4.125 @@ -387,7 +387,7 @@
   4.126  qed
   4.127  
   4.128  lemma Nadd_commute:
   4.129 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.130 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.131    shows "x +\<^sub>N y = y +\<^sub>N x"
   4.132  proof -
   4.133    have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
   4.134 @@ -396,7 +396,7 @@
   4.135  qed
   4.136  
   4.137  lemma [simp]:
   4.138 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.139 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.140    shows "(0, b) +\<^sub>N y = normNum y"
   4.141      and "(a, 0) +\<^sub>N y = normNum y"
   4.142      and "x +\<^sub>N (0, b) = normNum x"
   4.143 @@ -408,7 +408,7 @@
   4.144    done
   4.145  
   4.146  lemma normNum_nilpotent_aux[simp]:
   4.147 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.148 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.149    assumes nx: "isnormNum x"
   4.150    shows "normNum x = x"
   4.151  proof -
   4.152 @@ -419,7 +419,7 @@
   4.153  qed
   4.154  
   4.155  lemma normNum_nilpotent[simp]:
   4.156 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.157 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.158    shows "normNum (normNum x) = normNum x"
   4.159    by simp
   4.160  
   4.161 @@ -427,11 +427,11 @@
   4.162    by (simp_all add: normNum_def)
   4.163  
   4.164  lemma normNum_Nadd:
   4.165 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.166 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.167    shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
   4.168  
   4.169  lemma Nadd_normNum1[simp]:
   4.170 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.171 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.172    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
   4.173  proof -
   4.174    have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   4.175 @@ -441,7 +441,7 @@
   4.176  qed
   4.177  
   4.178  lemma Nadd_normNum2[simp]:
   4.179 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.180 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.181    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
   4.182  proof -
   4.183    have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   4.184 @@ -451,7 +451,7 @@
   4.185  qed
   4.186  
   4.187  lemma Nadd_assoc:
   4.188 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.189 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.190    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   4.191  proof -
   4.192    have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
   4.193 @@ -463,7 +463,7 @@
   4.194    by (simp add: Nmul_def split_def Let_def gcd_commute_int mult.commute)
   4.195  
   4.196  lemma Nmul_assoc:
   4.197 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.198 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.199    assumes nx: "isnormNum x" and ny: "isnormNum y" and nz: "isnormNum z"
   4.200    shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
   4.201  proof -
   4.202 @@ -474,7 +474,7 @@
   4.203  qed
   4.204  
   4.205  lemma Nsub0:
   4.206 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.207 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.208    assumes x: "isnormNum x" and y: "isnormNum y"
   4.209    shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
   4.210  proof -
   4.211 @@ -490,7 +490,7 @@
   4.212    by (simp_all add: Nmul_def Let_def split_def)
   4.213  
   4.214  lemma Nmul_eq0[simp]:
   4.215 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.216 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
   4.217    assumes nx: "isnormNum x" and ny: "isnormNum y"
   4.218    shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
   4.219  proof -
     5.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Mar 31 16:49:41 2015 +0100
     5.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Mar 31 21:54:32 2015 +0200
     5.3 @@ -235,7 +235,7 @@
     5.4  
     5.5  subsection{* Semantics of the polynomial representation *}
     5.6  
     5.7 -primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field_inverse_zero,power}"
     5.8 +primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
     5.9  where
    5.10    "Ipoly bs (C c) = INum c"
    5.11  | "Ipoly bs (Bound n) = bs!n"
    5.12 @@ -246,7 +246,7 @@
    5.13  | "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
    5.14  | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
    5.15  
    5.16 -abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field_inverse_zero,power}"
    5.17 +abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"
    5.18      ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    5.19    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
    5.20  
    5.21 @@ -481,7 +481,7 @@
    5.22  qed simp_all
    5.23  
    5.24  lemma polymul_properties:
    5.25 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    5.26 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    5.27      and np: "isnpolyh p n0"
    5.28      and nq: "isnpolyh q n1"
    5.29      and m: "m \<le> min n0 n1"
    5.30 @@ -670,23 +670,23 @@
    5.31    by (induct p q rule: polymul.induct) (auto simp add: field_simps)
    5.32  
    5.33  lemma polymul_normh:
    5.34 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    5.35 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    5.36    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
    5.37    using polymul_properties(1) by blast
    5.38  
    5.39  lemma polymul_eq0_iff:
    5.40 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    5.41 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    5.42    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p"
    5.43    using polymul_properties(2) by blast
    5.44  
    5.45  lemma polymul_degreen:
    5.46 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    5.47 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    5.48    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
    5.49      degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \<or> q = 0\<^sub>p then 0 else degreen p m + degreen q m)"
    5.50    by (fact polymul_properties(3))
    5.51  
    5.52  lemma polymul_norm:
    5.53 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    5.54 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    5.55    shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)"
    5.56    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
    5.57  
    5.58 @@ -699,7 +699,7 @@
    5.59  lemma monic_eqI:
    5.60    assumes np: "isnpolyh p n0"
    5.61    shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
    5.62 -    (Ipoly bs p ::'a::{field_char_0,field_inverse_zero, power})"
    5.63 +    (Ipoly bs p ::'a::{field_char_0,field, power})"
    5.64    unfolding monic_def Let_def
    5.65  proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
    5.66    let ?h = "headconst p"
    5.67 @@ -750,13 +750,13 @@
    5.68    using polyadd_norm polyneg_norm by (simp add: polysub_def)
    5.69  
    5.70  lemma polysub_same_0[simp]:
    5.71 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    5.72 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    5.73    shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p"
    5.74    unfolding polysub_def split_def fst_conv snd_conv
    5.75    by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def])
    5.76  
    5.77  lemma polysub_0:
    5.78 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    5.79 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    5.80    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p -\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = q"
    5.81    unfolding polysub_def split_def fst_conv snd_conv
    5.82    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
    5.83 @@ -765,7 +765,7 @@
    5.84  text{* polypow is a power function and preserves normal forms *}
    5.85  
    5.86  lemma polypow[simp]:
    5.87 -  "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n"
    5.88 +  "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
    5.89  proof (induct n rule: polypow.induct)
    5.90    case 1
    5.91    then show ?case
    5.92 @@ -806,7 +806,7 @@
    5.93  qed
    5.94  
    5.95  lemma polypow_normh:
    5.96 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    5.97 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    5.98    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
    5.99  proof (induct k arbitrary: n rule: polypow.induct)
   5.100    case 1
   5.101 @@ -826,18 +826,18 @@
   5.102  qed
   5.103  
   5.104  lemma polypow_norm:
   5.105 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.106 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.107    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   5.108    by (simp add: polypow_normh isnpoly_def)
   5.109  
   5.110  text{* Finally the whole normalization *}
   5.111  
   5.112  lemma polynate [simp]:
   5.113 -  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field_inverse_zero})"
   5.114 +  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
   5.115    by (induct p rule:polynate.induct) auto
   5.116  
   5.117  lemma polynate_norm[simp]:
   5.118 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.119 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.120    shows "isnpoly (polynate p)"
   5.121    by (induct p rule: polynate.induct)
   5.122       (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
   5.123 @@ -868,7 +868,7 @@
   5.124    using assms by (induct k arbitrary: p) auto
   5.125  
   5.126  lemma funpow_shift1:
   5.127 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
   5.128 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
   5.129      Ipoly bs (Mul (Pw (Bound 0) n) p)"
   5.130    by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
   5.131  
   5.132 @@ -876,7 +876,7 @@
   5.133    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   5.134  
   5.135  lemma funpow_shift1_1:
   5.136 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
   5.137 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
   5.138      Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
   5.139    by (simp add: funpow_shift1)
   5.140  
   5.141 @@ -886,7 +886,7 @@
   5.142  lemma behead:
   5.143    assumes "isnpolyh p n"
   5.144    shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
   5.145 -    (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})"
   5.146 +    (Ipoly bs p :: 'a :: {field_char_0,field})"
   5.147    using assms
   5.148  proof (induct p arbitrary: n rule: behead.induct)
   5.149    case (1 c p n)
   5.150 @@ -1160,7 +1160,7 @@
   5.151  
   5.152  lemma isnpolyh_zero_iff:
   5.153    assumes nq: "isnpolyh p n0"
   5.154 -    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field_inverse_zero, power})"
   5.155 +    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field, power})"
   5.156    shows "p = 0\<^sub>p"
   5.157    using nq eq
   5.158  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   5.159 @@ -1242,7 +1242,7 @@
   5.160  lemma isnpolyh_unique:
   5.161    assumes np: "isnpolyh p n0"
   5.162      and nq: "isnpolyh q n1"
   5.163 -  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field_inverse_zero,power})) \<longleftrightarrow> p = q"
   5.164 +  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field,power})) \<longleftrightarrow> p = q"
   5.165  proof auto
   5.166    assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
   5.167    then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)"
   5.168 @@ -1257,7 +1257,7 @@
   5.169  text{* consequences of unicity on the algorithms for polynomial normalization *}
   5.170  
   5.171  lemma polyadd_commute:
   5.172 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.173 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.174      and np: "isnpolyh p n0"
   5.175      and nq: "isnpolyh q n1"
   5.176    shows "p +\<^sub>p q = q +\<^sub>p p"
   5.177 @@ -1271,7 +1271,7 @@
   5.178    by simp
   5.179  
   5.180  lemma polyadd_0[simp]:
   5.181 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.182 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.183      and np: "isnpolyh p n0"
   5.184    shows "p +\<^sub>p 0\<^sub>p = p"
   5.185      and "0\<^sub>p +\<^sub>p p = p"
   5.186 @@ -1279,7 +1279,7 @@
   5.187      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   5.188  
   5.189  lemma polymul_1[simp]:
   5.190 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.191 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.192      and np: "isnpolyh p n0"
   5.193    shows "p *\<^sub>p (1)\<^sub>p = p"
   5.194      and "(1)\<^sub>p *\<^sub>p p = p"
   5.195 @@ -1287,7 +1287,7 @@
   5.196      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   5.197  
   5.198  lemma polymul_0[simp]:
   5.199 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.200 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.201      and np: "isnpolyh p n0"
   5.202    shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p"
   5.203      and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
   5.204 @@ -1295,27 +1295,27 @@
   5.205      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
   5.206  
   5.207  lemma polymul_commute:
   5.208 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.209 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.210      and np: "isnpolyh p n0"
   5.211      and nq: "isnpolyh q n1"
   5.212    shows "p *\<^sub>p q = q *\<^sub>p p"
   5.213    using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np],
   5.214 -    where ?'a = "'a::{field_char_0,field_inverse_zero, power}"]
   5.215 +    where ?'a = "'a::{field_char_0,field, power}"]
   5.216    by simp
   5.217  
   5.218  declare polyneg_polyneg [simp]
   5.219  
   5.220  lemma isnpolyh_polynate_id [simp]:
   5.221 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.222 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.223      and np: "isnpolyh p n0"
   5.224    shows "polynate p = p"
   5.225 -  using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}",
   5.226 +  using isnpolyh_unique[where ?'a= "'a::{field_char_0,field}",
   5.227        OF polynate_norm[of p, unfolded isnpoly_def] np]
   5.228 -    polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"]
   5.229 +    polynate[where ?'a = "'a::{field_char_0,field}"]
   5.230    by simp
   5.231  
   5.232  lemma polynate_idempotent[simp]:
   5.233 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.234 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.235    shows "polynate (polynate p) = polynate p"
   5.236    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
   5.237  
   5.238 @@ -1323,7 +1323,7 @@
   5.239    unfolding poly_nate_def polypoly'_def ..
   5.240  
   5.241  lemma poly_nate_poly:
   5.242 -  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   5.243 +  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   5.244    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
   5.245    unfolding poly_nate_polypoly' by auto
   5.246  
   5.247 @@ -1362,7 +1362,7 @@
   5.248  qed
   5.249  
   5.250  lemma degree_polysub_samehead:
   5.251 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.252 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.253      and np: "isnpolyh p n0"
   5.254      and nq: "isnpolyh q n1"
   5.255      and h: "head p = head q"
   5.256 @@ -1531,7 +1531,7 @@
   5.257    done
   5.258  
   5.259  lemma polymul_head_polyeq:
   5.260 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.261 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.262    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> q \<noteq> 0\<^sub>p \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
   5.263  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   5.264    case (2 c c' n' p' n0 n1)
   5.265 @@ -1634,7 +1634,7 @@
   5.266    by (induct p arbitrary: n0 rule: polyneg.induct) auto
   5.267  
   5.268  lemma degree_polymul:
   5.269 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.270 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.271      and np: "isnpolyh p n0"
   5.272      and nq: "isnpolyh q n1"
   5.273    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
   5.274 @@ -1650,7 +1650,7 @@
   5.275  subsection {* Correctness of polynomial pseudo division *}
   5.276  
   5.277  lemma polydivide_aux_properties:
   5.278 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.279 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.280      and np: "isnpolyh p n0"
   5.281      and ns: "isnpolyh s n1"
   5.282      and ap: "head p = a"
   5.283 @@ -1745,24 +1745,24 @@
   5.284                polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
   5.285              have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0"
   5.286                by simp
   5.287 -            from asp have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   5.288 +            from asp have "\<forall>bs :: 'a::{field_char_0,field} list.
   5.289                Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
   5.290                by simp
   5.291 -            then have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   5.292 +            then have "\<forall>bs :: 'a::{field_char_0,field} list.
   5.293                Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
   5.294                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   5.295                by (simp add: field_simps)
   5.296 -            then have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   5.297 +            then have "\<forall>bs :: 'a::{field_char_0,field} list.
   5.298                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   5.299                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) +
   5.300                Ipoly bs p * Ipoly bs q + Ipoly bs r"
   5.301                by (auto simp only: funpow_shift1_1)
   5.302 -            then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
   5.303 +            then have "\<forall>bs:: 'a::{field_char_0,field} list.
   5.304                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   5.305                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) +
   5.306                Ipoly bs q) + Ipoly bs r"
   5.307                by (simp add: field_simps)
   5.308 -            then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
   5.309 +            then have "\<forall>bs:: 'a::{field_char_0,field} list.
   5.310                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   5.311                Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r)"
   5.312                by simp
   5.313 @@ -1784,10 +1784,10 @@
   5.314          moreover
   5.315          {
   5.316            assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
   5.317 -          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field_inverse_zero}"]
   5.318 -          have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs ?p'"
   5.319 +          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"]
   5.320 +          have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'"
   5.321              by simp
   5.322 -          then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
   5.323 +          then have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
   5.324              using np nxdn
   5.325              apply simp
   5.326              apply (simp only: funpow_shift1_1)
   5.327 @@ -1861,7 +1861,7 @@
   5.328              from kk' have kk'': "Suc (k' - Suc k) = k' - k"
   5.329                by arith
   5.330              {
   5.331 -              fix bs :: "'a::{field_char_0,field_inverse_zero} list"
   5.332 +              fix bs :: "'a::{field_char_0,field} list"
   5.333                from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
   5.334                have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
   5.335                  by simp
   5.336 @@ -1875,7 +1875,7 @@
   5.337                  Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
   5.338                  by (simp add: field_simps)
   5.339              }
   5.340 -            then have ieq:"\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   5.341 +            then have ieq:"\<forall>bs :: 'a::{field_char_0,field} list.
   5.342                  Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   5.343                  Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
   5.344                by auto
   5.345 @@ -1900,7 +1900,7 @@
   5.346          {
   5.347            assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
   5.348            {
   5.349 -            fix bs :: "'a::{field_char_0,field_inverse_zero} list"
   5.350 +            fix bs :: "'a::{field_char_0,field} list"
   5.351              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   5.352              have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'"
   5.353                by simp
   5.354 @@ -1909,10 +1909,10 @@
   5.355              then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
   5.356                by simp
   5.357            }
   5.358 -          then have hth: "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   5.359 +          then have hth: "\<forall>bs :: 'a::{field_char_0,field} list.
   5.360              Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
   5.361            from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
   5.362 -            using isnpolyh_unique[where ?'a = "'a::{field_char_0,field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
   5.363 +            using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
   5.364                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
   5.365                simplified ap]
   5.366              by simp
   5.367 @@ -1945,7 +1945,7 @@
   5.368  qed
   5.369  
   5.370  lemma polydivide_properties:
   5.371 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.372 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.373      and np: "isnpolyh p n0"
   5.374      and ns: "isnpolyh s n1"
   5.375      and pnz: "p \<noteq> 0\<^sub>p"
   5.376 @@ -2112,12 +2112,12 @@
   5.377  lemma swapnorm:
   5.378    assumes nbs: "n < length bs"
   5.379      and mbs: "m < length bs"
   5.380 -  shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field_inverse_zero})) =
   5.381 +  shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field})) =
   5.382      Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
   5.383    using swap[OF assms] swapnorm_def by simp
   5.384  
   5.385  lemma swapnorm_isnpoly [simp]:
   5.386 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   5.387 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.388    shows "isnpoly (swapnorm n m p)"
   5.389    unfolding swapnorm_def by simp
   5.390  
     6.1 --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Tue Mar 31 16:49:41 2015 +0100
     6.2 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Tue Mar 31 21:54:32 2015 +0200
     6.3 @@ -7,147 +7,147 @@
     6.4  begin
     6.5  
     6.6  lemma
     6.7 -  "\<exists>(y::'a::{linordered_field_inverse_zero}) <2. x + 3* y < 0 \<and> x - y >0"
     6.8 +  "\<exists>(y::'a::{linordered_field}) <2. x + 3* y < 0 \<and> x - y >0"
     6.9    by ferrack
    6.10  
    6.11 -lemma "~ (ALL x (y::'a::{linordered_field_inverse_zero}). x < y --> 10*x < 11*y)"
    6.12 +lemma "~ (ALL x (y::'a::{linordered_field}). x < y --> 10*x < 11*y)"
    6.13    by ferrack
    6.14  
    6.15 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
    6.16 +lemma "ALL (x::'a::{linordered_field}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
    6.17    by ferrack
    6.18  
    6.19 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. x ~= y --> x < y"
    6.20 +lemma "EX (x::'a::{linordered_field}) y. x ~= y --> x < y"
    6.21    by ferrack
    6.22  
    6.23 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
    6.24 +lemma "EX (x::'a::{linordered_field}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
    6.25    by ferrack
    6.26  
    6.27 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
    6.28 +lemma "ALL (x::'a::{linordered_field}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
    6.29    by ferrack
    6.30  
    6.31 -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX (y::'a::{linordered_field_inverse_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
    6.32 +lemma "ALL (x::'a::{linordered_field}). (EX (y::'a::{linordered_field}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
    6.33    by ferrack
    6.34  
    6.35 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) < 0. (EX (y::'a::{linordered_field_inverse_zero}) > 0. 7*x + y > 0 & x - y <= 9)"
    6.36 +lemma "ALL (x::'a::{linordered_field}) < 0. (EX (y::'a::{linordered_field}) > 0. 7*x + y > 0 & x - y <= 9)"
    6.37    by ferrack
    6.38  
    6.39 -lemma "EX (x::'a::{linordered_field_inverse_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
    6.40 +lemma "EX (x::'a::{linordered_field}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
    6.41    by ferrack
    6.42  
    6.43 -lemma "EX x. (ALL (y::'a::{linordered_field_inverse_zero}). y < 2 -->  2*(y - x) \<le> 0 )"
    6.44 +lemma "EX x. (ALL (y::'a::{linordered_field}). y < 2 -->  2*(y - x) \<le> 0 )"
    6.45    by ferrack
    6.46  
    6.47 -lemma "ALL (x::'a::{linordered_field_inverse_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
    6.48 +lemma "ALL (x::'a::{linordered_field}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
    6.49    by ferrack
    6.50  
    6.51 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y z. x + y < z --> y >= z --> x < 0"
    6.52 +lemma "ALL (x::'a::{linordered_field}) y z. x + y < z --> y >= z --> x < 0"
    6.53    by ferrack
    6.54  
    6.55 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
    6.56 +lemma "EX (x::'a::{linordered_field}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
    6.57    by ferrack
    6.58  
    6.59 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y z. abs (x + y) <= z --> (abs z = z)"
    6.60 +lemma "ALL (x::'a::{linordered_field}) y z. abs (x + y) <= z --> (abs z = z)"
    6.61    by ferrack
    6.62  
    6.63 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
    6.64 +lemma "EX (x::'a::{linordered_field}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
    6.65    by ferrack
    6.66  
    6.67 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
    6.68 +lemma "ALL (x::'a::{linordered_field}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
    6.69    by ferrack
    6.70  
    6.71 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. x < y --> (EX z>0. x+z = y)"
    6.72 +lemma "ALL (x::'a::{linordered_field}) y. x < y --> (EX z>0. x+z = y)"
    6.73    by ferrack
    6.74  
    6.75 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. x < y --> (EX z>0. x+z = y)"
    6.76 +lemma "ALL (x::'a::{linordered_field}) y. x < y --> (EX z>0. x+z = y)"
    6.77    by ferrack
    6.78  
    6.79 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (EX z>0. abs (x - y) <= z )"
    6.80 +lemma "ALL (x::'a::{linordered_field}) y. (EX z>0. abs (x - y) <= z )"
    6.81    by ferrack
    6.82  
    6.83 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    6.84 +lemma "EX (x::'a::{linordered_field}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    6.85    by ferrack
    6.86  
    6.87 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
    6.88 +lemma "EX (x::'a::{linordered_field}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
    6.89    by ferrack
    6.90  
    6.91 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    6.92 +lemma "EX (x::'a::{linordered_field}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    6.93    by ferrack
    6.94  
    6.95 -lemma "EX (x::'a::{linordered_field_inverse_zero})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
    6.96 +lemma "EX (x::'a::{linordered_field})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
    6.97    by ferrack
    6.98  
    6.99 -lemma "EX (x::'a::{linordered_field_inverse_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
   6.100 +lemma "EX (x::'a::{linordered_field}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
   6.101    by ferrack
   6.102  
   6.103 -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
   6.104 +lemma "ALL (x::'a::{linordered_field}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
   6.105    by ferrack
   6.106  
   6.107 -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
   6.108 +lemma "ALL (x::'a::{linordered_field}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
   6.109    by ferrack
   6.110  
   6.111 -lemma "EX (x::'a::{linordered_field_inverse_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
   6.112 +lemma "EX (x::'a::{linordered_field}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
   6.113    by ferrack
   6.114  
   6.115 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
   6.116 +lemma "ALL (x::'a::{linordered_field}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
   6.117    by ferrack
   6.118  
   6.119 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
   6.120 +lemma "EX (x::'a::{linordered_field}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
   6.121    by ferrack
   6.122  
   6.123 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
   6.124 +lemma "EX (x::'a::{linordered_field}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
   6.125    by ferrack
   6.126  
   6.127 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   6.128 +lemma "EX (x::'a::{linordered_field}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   6.129    by ferrack
   6.130  
   6.131 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
   6.132 +lemma "ALL (x::'a::{linordered_field}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
   6.133    by ferrack
   6.134  
   6.135 -lemma "~(ALL (x::'a::{linordered_field_inverse_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
   6.136 +lemma "~(ALL (x::'a::{linordered_field}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
   6.137    by ferrack
   6.138  
   6.139 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
   6.140 +lemma "ALL (x::'a::{linordered_field}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
   6.141    by ferrack
   6.142  
   6.143 -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
   6.144 +lemma "ALL (x::'a::{linordered_field}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
   6.145    by ferrack
   6.146  
   6.147 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
   6.148 +lemma "EX (x::'a::{linordered_field}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
   6.149    by ferrack
   6.150  
   6.151 -lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
   6.152 +lemma "EX z. (ALL (x::'a::{linordered_field}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
   6.153    by ferrack
   6.154  
   6.155 -lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
   6.156 +lemma "EX z. (ALL (x::'a::{linordered_field}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
   6.157    by ferrack
   6.158  
   6.159 -lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
   6.160 +lemma "ALL (x::'a::{linordered_field}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
   6.161    by ferrack
   6.162  
   6.163 -lemma "EX y. (ALL (x::'a::{linordered_field_inverse_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
   6.164 +lemma "EX y. (ALL (x::'a::{linordered_field}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
   6.165    by ferrack
   6.166  
   6.167 -lemma "EX (x::'a::{linordered_field_inverse_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
   6.168 +lemma "EX (x::'a::{linordered_field}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
   6.169    by ferrack
   6.170  
   6.171 -lemma "EX (x::'a::{linordered_field_inverse_zero}). (ALL y < x. (EX z > (x+y).
   6.172 +lemma "EX (x::'a::{linordered_field}). (ALL y < x. (EX z > (x+y).
   6.173    (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
   6.174    by ferrack
   6.175  
   6.176 -lemma "EX (x::'a::{linordered_field_inverse_zero}). (ALL y. (EX z > y.
   6.177 +lemma "EX (x::'a::{linordered_field}). (ALL y. (EX z > y.
   6.178    (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
   6.179    by ferrack
   6.180  
   6.181 -lemma "EX (x::'a::{linordered_field_inverse_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   6.182 +lemma "EX (x::'a::{linordered_field}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   6.183    by ferrack
   6.184  
   6.185 -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
   6.186 +lemma "ALL (x::'a::{linordered_field}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
   6.187    by ferrack
   6.188  
   6.189 -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
   6.190 +lemma "ALL (x::'a::{linordered_field}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
   6.191    by ferrack
   6.192  
   6.193 -lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
   6.194 +lemma "ALL (x::'a::{linordered_field}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
   6.195    by ferrack
   6.196  
   6.197  end
     7.1 --- a/src/HOL/Deriv.thy	Tue Mar 31 16:49:41 2015 +0100
     7.2 +++ b/src/HOL/Deriv.thy	Tue Mar 31 21:54:32 2015 +0200
     7.3 @@ -698,10 +698,17 @@
     7.4       (auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative)
     7.5  
     7.6  lemma DERIV_inverse'[derivative_intros]:
     7.7 -  "(f has_field_derivative D) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
     7.8 -  ((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
     7.9 -  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_inverse])
    7.10 -     (auto dest: has_field_derivative_imp_has_derivative)
    7.11 +  assumes "(f has_field_derivative D) (at x within s)"
    7.12 +    and "f x \<noteq> 0"
    7.13 +  shows "((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
    7.14 +proof -
    7.15 +  have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative op * D)"
    7.16 +    by (rule arg_cong [of "\<lambda>x. x * D"]) (simp add: fun_eq_iff)
    7.17 +  with assms have "(f has_derivative (\<lambda>x. x * D)) (at x within s)"
    7.18 +    by (auto dest!: has_field_derivative_imp_has_derivative)
    7.19 +  then show ?thesis using `f x \<noteq> 0`
    7.20 +    by (auto intro: has_derivative_imp_has_field_derivative has_derivative_inverse)
    7.21 +qed
    7.22  
    7.23  text {* Power of @{text "-1"} *}
    7.24  
     8.1 --- a/src/HOL/Enum.thy	Tue Mar 31 16:49:41 2015 +0100
     8.2 +++ b/src/HOL/Enum.thy	Tue Mar 31 21:54:32 2015 +0200
     8.3 @@ -683,7 +683,7 @@
     8.4  
     8.5  instance finite_2 :: complete_linorder ..
     8.6  
     8.7 -instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, sgn_if, semiring_div}" begin
     8.8 +instantiation finite_2 :: "{field, abs_if, ring_div, sgn_if, semiring_div}" begin
     8.9  definition [simp]: "0 = a\<^sub>1"
    8.10  definition [simp]: "1 = a\<^sub>2"
    8.11  definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
    8.12 @@ -807,7 +807,7 @@
    8.13  
    8.14  instance finite_3 :: complete_linorder ..
    8.15  
    8.16 -instantiation finite_3 :: "{field_inverse_zero, abs_if, ring_div, semiring_div, sgn_if}" begin
    8.17 +instantiation finite_3 :: "{field, abs_if, ring_div, semiring_div, sgn_if}" begin
    8.18  definition [simp]: "0 = a\<^sub>1"
    8.19  definition [simp]: "1 = a\<^sub>2"
    8.20  definition
     9.1 --- a/src/HOL/Fields.thy	Tue Mar 31 16:49:41 2015 +0100
     9.2 +++ b/src/HOL/Fields.thy	Tue Mar 31 21:54:32 2015 +0200
     9.3 @@ -56,6 +56,7 @@
     9.4    assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
     9.5    assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
     9.6    assumes divide_inverse: "a / b = a * inverse b"
     9.7 +  assumes inverse_zero [simp]: "inverse 0 = 0"
     9.8  begin
     9.9  
    9.10  subclass ring_1_no_zero_divisors
    9.11 @@ -239,12 +240,6 @@
    9.12    "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
    9.13    by (simp add: divide_diff_eq_iff[symmetric])
    9.14  
    9.15 -end
    9.16 -
    9.17 -class division_ring_inverse_zero = division_ring +
    9.18 -  assumes inverse_zero [simp]: "inverse 0 = 0"
    9.19 -begin
    9.20 -
    9.21  lemma divide_zero [simp]:
    9.22    "a / 0 = 0"
    9.23    by (simp add: divide_inverse)
    9.24 @@ -307,6 +302,7 @@
    9.25  class field = comm_ring_1 + inverse +
    9.26    assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    9.27    assumes field_divide_inverse: "a / b = a * inverse b"
    9.28 +  assumes field_inverse_zero: "inverse 0 = 0"
    9.29  begin
    9.30  
    9.31  subclass division_ring
    9.32 @@ -318,6 +314,9 @@
    9.33  next
    9.34    fix a b :: 'a
    9.35    show "a / b = a * inverse b" by (rule field_divide_inverse)
    9.36 +next
    9.37 +  show "inverse 0 = 0"
    9.38 +    by (fact field_inverse_zero) 
    9.39  qed
    9.40  
    9.41  subclass idom ..
    9.42 @@ -395,15 +394,6 @@
    9.43  lemma divide_minus1 [simp]: "x / - 1 = - x"
    9.44    using nonzero_minus_divide_right [of "1" x] by simp
    9.45  
    9.46 -end
    9.47 -
    9.48 -class field_inverse_zero = field +
    9.49 -  assumes field_inverse_zero: "inverse 0 = 0"
    9.50 -begin
    9.51 -
    9.52 -subclass division_ring_inverse_zero proof
    9.53 -qed (fact field_inverse_zero)
    9.54 -
    9.55  text{*This version builds in division by zero while also re-orienting
    9.56        the right-hand side.*}
    9.57  lemma inverse_mult_distrib [simp]:
    9.58 @@ -963,11 +953,6 @@
    9.59    then show "t \<le> y" by (simp add: algebra_simps)
    9.60  qed
    9.61  
    9.62 -end
    9.63 -
    9.64 -class linordered_field_inverse_zero = linordered_field + field_inverse_zero
    9.65 -begin
    9.66 -
    9.67  lemma inverse_positive_iff_positive [simp]:
    9.68    "(0 < inverse a) = (0 < a)"
    9.69  apply (cases "a = 0", simp)
    10.1 --- a/src/HOL/Groups_Big.thy	Tue Mar 31 16:49:41 2015 +0100
    10.2 +++ b/src/HOL/Groups_Big.thy	Tue Mar 31 21:54:32 2015 +0200
    10.3 @@ -1158,11 +1158,11 @@
    10.4      (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
    10.5    by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
    10.6  
    10.7 -lemma (in field_inverse_zero) setprod_inversef: 
    10.8 +lemma (in field) setprod_inversef: 
    10.9    "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
   10.10    by (induct A rule: finite_induct) simp_all
   10.11  
   10.12 -lemma (in field_inverse_zero) setprod_dividef:
   10.13 +lemma (in field) setprod_dividef:
   10.14    "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
   10.15    using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
   10.16  
    11.1 --- a/src/HOL/Library/BigO.thy	Tue Mar 31 16:49:41 2015 +0100
    11.2 +++ b/src/HOL/Library/BigO.thy	Tue Mar 31 21:54:32 2015 +0200
    11.3 @@ -489,7 +489,7 @@
    11.4    shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
    11.5    apply (simp add: bigo_def)
    11.6    apply (rule_tac x = "abs (inverse c)" in exI)
    11.7 -  apply (simp add: abs_mult [symmetric] mult.assoc [symmetric])
    11.8 +  apply (simp add: abs_mult mult.assoc [symmetric])
    11.9    done
   11.10  
   11.11  lemma bigo_const_mult4:
   11.12 @@ -519,11 +519,7 @@
   11.13    apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
   11.14    apply (simp add: mult.assoc [symmetric] abs_mult)
   11.15    apply (rule_tac x = "abs (inverse c) * ca" in exI)
   11.16 -  apply (rule allI)
   11.17 -  apply (subst mult.assoc)
   11.18 -  apply (rule mult_left_mono)
   11.19 -  apply (erule spec)
   11.20 -  apply force
   11.21 +  apply auto
   11.22    done
   11.23  
   11.24  lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
    12.1 --- a/src/HOL/Library/Bit.thy	Tue Mar 31 16:49:41 2015 +0100
    12.2 +++ b/src/HOL/Library/Bit.thy	Tue Mar 31 21:54:32 2015 +0200
    12.3 @@ -98,7 +98,7 @@
    12.4    
    12.5  subsection {* Type @{typ bit} forms a field *}
    12.6  
    12.7 -instantiation bit :: field_inverse_zero
    12.8 +instantiation bit :: field
    12.9  begin
   12.10  
   12.11  definition plus_bit_def:
    13.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 31 16:49:41 2015 +0100
    13.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 31 21:54:32 2015 +0200
    13.3 @@ -3628,7 +3628,7 @@
    13.4  
    13.5  subsection {* Hypergeometric series *}
    13.6  
    13.7 -definition "F as bs (c::'a::{field_char_0,field_inverse_zero}) =
    13.8 +definition "F as bs (c::'a::{field_char_0,field}) =
    13.9    Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
   13.10      (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
   13.11  
   13.12 @@ -3711,11 +3711,11 @@
   13.13    by (simp add: fps_eq_iff fps_integral_def)
   13.14  
   13.15  lemma F_minus_nat:
   13.16 -  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field_inverse_zero}) $ k =
   13.17 +  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
   13.18      (if k \<le> n then
   13.19        pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
   13.20       else 0)"
   13.21 -  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field_inverse_zero}) $ k =
   13.22 +  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
   13.23      (if k \<le> m then
   13.24        pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
   13.25       else 0)"
    14.1 --- a/src/HOL/Library/Fraction_Field.thy	Tue Mar 31 16:49:41 2015 +0100
    14.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Mar 31 21:54:32 2015 +0200
    14.3 @@ -224,7 +224,7 @@
    14.4  
    14.5  end
    14.6  
    14.7 -instantiation fract :: (idom) field_inverse_zero
    14.8 +instantiation fract :: (idom) field
    14.9  begin
   14.10  
   14.11  definition inverse_fract_def:
   14.12 @@ -428,7 +428,7 @@
   14.13  
   14.14  end
   14.15  
   14.16 -instance fract :: (linordered_idom) linordered_field_inverse_zero
   14.17 +instance fract :: (linordered_idom) linordered_field
   14.18  proof
   14.19    fix q r s :: "'a fract"
   14.20    assume "q \<le> r"
    15.1 --- a/src/HOL/Limits.thy	Tue Mar 31 16:49:41 2015 +0100
    15.2 +++ b/src/HOL/Limits.thy	Tue Mar 31 21:54:32 2015 +0200
    15.3 @@ -1062,7 +1062,7 @@
    15.4    unfolding filterlim_def at_top_to_right filtermap_filtermap ..
    15.5  
    15.6  lemma filterlim_inverse_at_infinity:
    15.7 -  fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
    15.8 +  fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring}"
    15.9    shows "filterlim inverse at_infinity (at (0::'a))"
   15.10    unfolding filterlim_at_infinity[OF order_refl]
   15.11  proof safe
   15.12 @@ -1074,7 +1074,7 @@
   15.13  qed
   15.14  
   15.15  lemma filterlim_inverse_at_iff:
   15.16 -  fixes g :: "'a \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
   15.17 +  fixes g :: "'a \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring}"
   15.18    shows "(LIM x F. inverse (g x) :> at 0) \<longleftrightarrow> (LIM x F. g x :> at_infinity)"
   15.19    unfolding filterlim_def filtermap_filtermap[symmetric]
   15.20  proof
   15.21 @@ -1099,7 +1099,7 @@
   15.22  
   15.23  
   15.24  lemma at_to_infinity:
   15.25 -  fixes x :: "'a \<Colon> {real_normed_field,field_inverse_zero}"
   15.26 +  fixes x :: "'a \<Colon> {real_normed_field,field}"
   15.27    shows "(at (0::'a)) = filtermap inverse at_infinity"
   15.28  proof (rule antisym)
   15.29    have "(inverse ---> (0::'a)) at_infinity"
   15.30 @@ -1117,12 +1117,12 @@
   15.31  qed
   15.32  
   15.33  lemma lim_at_infinity_0:
   15.34 -  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
   15.35 +  fixes l :: "'a :: {real_normed_field,field}"
   15.36    shows "(f ---> l) at_infinity \<longleftrightarrow> ((f o inverse) ---> l) (at (0::'a))"
   15.37  by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap)
   15.38  
   15.39  lemma lim_zero_infinity:
   15.40 -  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
   15.41 +  fixes l :: "'a :: {real_normed_field,field}"
   15.42    shows "((\<lambda>x. f(1 / x)) ---> l) (at (0::'a)) \<Longrightarrow> (f ---> l) at_infinity"
   15.43  by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def)
   15.44  
   15.45 @@ -1241,7 +1241,7 @@
   15.46  qed
   15.47  
   15.48  lemma tendsto_divide_0:
   15.49 -  fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
   15.50 +  fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring}"
   15.51    assumes f: "(f ---> c) F"
   15.52    assumes g: "LIM x F. g x :> at_infinity"
   15.53    shows "((\<lambda>x. f x / g x) ---> 0) F"
    16.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Tue Mar 31 16:49:41 2015 +0100
    16.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Tue Mar 31 21:54:32 2015 +0200
    16.3 @@ -333,8 +333,7 @@
    16.4      also have "... <= O((\<lambda>x. 1 / f x) * (f * g))"
    16.5        by (rule bigo_mult2)
    16.6      also have "(\<lambda>x. 1 / f x) * (f * g) = g"
    16.7 -      apply (simp add: func_times)
    16.8 -      by (metis (lifting, no_types) a ext mult.commute nonzero_divide_eq_eq)
    16.9 +      by (simp add: fun_eq_iff a)
   16.10      finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
   16.11      then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
   16.12        by auto
   16.13 @@ -458,8 +457,8 @@
   16.14      using F3 by metis
   16.15    hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
   16.16      by (metis mult_left_mono)
   16.17 -  thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
   16.18 -    using A2 F4 by (metis mult.assoc mult_left_mono)
   16.19 +  then show "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. inverse \<bar>c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
   16.20 +    using A2 F4 by (metis F1 `0 < \<bar>inverse c\<bar>` linordered_field_class.sign_simps(23) mult_le_cancel_left_pos)
   16.21  qed
   16.22  
   16.23  lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
    17.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Mar 31 16:49:41 2015 +0100
    17.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Mar 31 21:54:32 2015 +0200
    17.3 @@ -64,7 +64,7 @@
    17.4  
    17.5  (* FIXME: In Finite_Set there is a useless further assumption *)
    17.6  lemma setprod_inversef:
    17.7 -  "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)"
    17.8 +  "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field)"
    17.9    apply (erule finite_induct)
   17.10    apply (simp)
   17.11    apply simp
    18.1 --- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Tue Mar 31 16:49:41 2015 +0100
    18.2 +++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Tue Mar 31 21:54:32 2015 +0200
    18.3 @@ -17,7 +17,7 @@
    18.4    by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
    18.5  
    18.6  lemma setsum_gp0:
    18.7 -  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
    18.8 +  fixes x :: "'a::{comm_ring,division_ring}"
    18.9    shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
   18.10    using setsum_gp_basic[of x n]
   18.11    by (simp add: real_of_nat_def mult.commute divide_simps)
   18.12 @@ -55,7 +55,7 @@
   18.13  qed
   18.14  
   18.15  lemma setsum_gp:
   18.16 -  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
   18.17 +  fixes x :: "'a::{comm_ring,division_ring}"
   18.18    shows   "(\<Sum>i=m..n. x^i) =
   18.19                 (if n < m then 0
   18.20                  else if x = 1 then of_nat((n + 1) - m)
   18.21 @@ -65,14 +65,14 @@
   18.22  by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
   18.23  
   18.24  lemma setsum_gp_offset:
   18.25 -  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
   18.26 +  fixes x :: "'a::{comm_ring,division_ring}"
   18.27    shows   "(\<Sum>i=m..m+n. x^i) =
   18.28         (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
   18.29    using setsum_gp [of x m "m+n"]
   18.30    by (auto simp: power_add algebra_simps)
   18.31  
   18.32  lemma setsum_gp_strict:
   18.33 -  fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
   18.34 +  fixes x :: "'a::{comm_ring,division_ring}"
   18.35    shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
   18.36    by (induct n) (auto simp: algebra_simps divide_simps)
   18.37      
    19.1 --- a/src/HOL/NSA/HDeriv.thy	Tue Mar 31 16:49:41 2015 +0100
    19.2 +++ b/src/HOL/NSA/HDeriv.thy	Tue Mar 31 21:54:32 2015 +0200
    19.3 @@ -366,7 +366,7 @@
    19.4        done
    19.5      ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
    19.6        - (inverse (star_of x) * inverse (star_of x))"
    19.7 -      using assms by (simp add: nonzero_inverse_mult_distrib [symmetric] nonzero_inverse_minus_eq [symmetric])
    19.8 +      using assms by simp 
    19.9    } then show ?thesis by (simp add: nsderiv_def)
   19.10  qed
   19.11  
    20.1 --- a/src/HOL/NSA/HyperDef.thy	Tue Mar 31 16:49:41 2015 +0100
    20.2 +++ b/src/HOL/NSA/HyperDef.thy	Tue Mar 31 21:54:32 2015 +0200
    20.3 @@ -140,12 +140,12 @@
    20.4  
    20.5  lemma of_hypreal_inverse [simp]:
    20.6    "\<And>x. of_hypreal (inverse x) =
    20.7 -   inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring_inverse_zero} star)"
    20.8 +   inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring} star)"
    20.9  by transfer (rule of_real_inverse)
   20.10  
   20.11  lemma of_hypreal_divide [simp]:
   20.12    "\<And>x y. of_hypreal (x / y) =
   20.13 -   (of_hypreal x / of_hypreal y :: 'a::{real_field, field_inverse_zero} star)"
   20.14 +   (of_hypreal x / of_hypreal y :: 'a::{real_field, field} star)"
   20.15  by transfer (rule of_real_divide)
   20.16  
   20.17  lemma of_hypreal_eq_iff [simp]:
   20.18 @@ -445,7 +445,7 @@
   20.19  by transfer (rule field_power_not_zero)
   20.20  
   20.21  lemma hyperpow_inverse:
   20.22 -  "\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
   20.23 +  "\<And>r n. r \<noteq> (0::'a::field star)
   20.24     \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
   20.25  by transfer (rule power_inverse)
   20.26  
    21.1 --- a/src/HOL/NSA/NSA.thy	Tue Mar 31 16:49:41 2015 +0100
    21.2 +++ b/src/HOL/NSA/NSA.thy	Tue Mar 31 21:54:32 2015 +0200
    21.3 @@ -145,12 +145,12 @@
    21.4  by transfer (rule nonzero_norm_inverse)
    21.5  
    21.6  lemma hnorm_inverse:
    21.7 -  "\<And>a::'a::{real_normed_div_algebra, division_ring_inverse_zero} star.
    21.8 +  "\<And>a::'a::{real_normed_div_algebra, division_ring} star.
    21.9     hnorm (inverse a) = inverse (hnorm a)"
   21.10  by transfer (rule norm_inverse)
   21.11  
   21.12  lemma hnorm_divide:
   21.13 -  "\<And>a b::'a::{real_normed_field, field_inverse_zero} star.
   21.14 +  "\<And>a b::'a::{real_normed_field, field} star.
   21.15     hnorm (a / b) = hnorm a / hnorm b"
   21.16  by transfer (rule norm_divide)
   21.17  
    22.1 --- a/src/HOL/NSA/StarDef.thy	Tue Mar 31 16:49:41 2015 +0100
    22.2 +++ b/src/HOL/NSA/StarDef.thy	Tue Mar 31 21:54:32 2015 +0200
    22.3 @@ -881,20 +881,14 @@
    22.4  apply (transfer, erule left_inverse)
    22.5  apply (transfer, erule right_inverse)
    22.6  apply (transfer, fact divide_inverse)
    22.7 +apply (transfer, fact inverse_zero)
    22.8  done
    22.9  
   22.10 -instance star :: (division_ring_inverse_zero) division_ring_inverse_zero
   22.11 -by (intro_classes, transfer, rule inverse_zero)
   22.12 -
   22.13  instance star :: (field) field
   22.14  apply (intro_classes)
   22.15  apply (transfer, erule left_inverse)
   22.16  apply (transfer, rule divide_inverse)
   22.17 -done
   22.18 -
   22.19 -instance star :: (field_inverse_zero) field_inverse_zero
   22.20 -apply intro_classes
   22.21 -apply (rule inverse_zero)
   22.22 +apply (transfer, fact inverse_zero)
   22.23  done
   22.24  
   22.25  instance star :: (ordered_semiring) ordered_semiring
   22.26 @@ -937,7 +931,6 @@
   22.27  
   22.28  instance star :: (linordered_idom) linordered_idom ..
   22.29  instance star :: (linordered_field) linordered_field ..
   22.30 -instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero ..
   22.31  
   22.32  subsection {* Power *}
   22.33  
    23.1 --- a/src/HOL/Num.thy	Tue Mar 31 16:49:41 2015 +0100
    23.2 +++ b/src/HOL/Num.thy	Tue Mar 31 21:54:32 2015 +0200
    23.3 @@ -1075,7 +1075,7 @@
    23.4  
    23.5  subsection {* Particular lemmas concerning @{term 2} *}
    23.6  
    23.7 -context linordered_field_inverse_zero
    23.8 +context linordered_field
    23.9  begin
   23.10  
   23.11  lemma half_gt_zero_iff:
    24.1 --- a/src/HOL/Numeral_Simprocs.thy	Tue Mar 31 16:49:41 2015 +0100
    24.2 +++ b/src/HOL/Numeral_Simprocs.thy	Tue Mar 31 21:54:32 2015 +0200
    24.3 @@ -115,8 +115,8 @@
    24.4    {* fn phi => Numeral_Simprocs.combine_numerals *}
    24.5  
    24.6  simproc_setup field_combine_numerals
    24.7 -  ("(i::'a::{field_inverse_zero,ring_char_0}) + j"
    24.8 -  |"(i::'a::{field_inverse_zero,ring_char_0}) - j") =
    24.9 +  ("(i::'a::{field,ring_char_0}) + j"
   24.10 +  |"(i::'a::{field,ring_char_0}) - j") =
   24.11    {* fn phi => Numeral_Simprocs.field_combine_numerals *}
   24.12  
   24.13  simproc_setup inteq_cancel_numerals
   24.14 @@ -174,9 +174,9 @@
   24.15    {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
   24.16  
   24.17  simproc_setup divide_cancel_numeral_factor
   24.18 -  ("((l::'a::{field_inverse_zero,ring_char_0}) * m) / n"
   24.19 -  |"(l::'a::{field_inverse_zero,ring_char_0}) / (m * n)"
   24.20 -  |"((numeral v)::'a::{field_inverse_zero,ring_char_0}) / (numeral w)") =
   24.21 +  ("((l::'a::{field,ring_char_0}) * m) / n"
   24.22 +  |"(l::'a::{field,ring_char_0}) / (m * n)"
   24.23 +  |"((numeral v)::'a::{field,ring_char_0}) / (numeral w)") =
   24.24    {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
   24.25  
   24.26  simproc_setup ring_eq_cancel_factor
   24.27 @@ -209,8 +209,8 @@
   24.28    {* fn phi => Numeral_Simprocs.dvd_cancel_factor *}
   24.29  
   24.30  simproc_setup divide_cancel_factor
   24.31 -  ("((l::'a::field_inverse_zero) * m) / n"
   24.32 -  |"(l::'a::field_inverse_zero) / (m * n)") =
   24.33 +  ("((l::'a::field) * m) / n"
   24.34 +  |"(l::'a::field) / (m * n)") =
   24.35    {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
   24.36  
   24.37  ML_file "Tools/nat_numeral_simprocs.ML"
    25.1 --- a/src/HOL/Power.thy	Tue Mar 31 16:49:41 2015 +0100
    25.2 +++ b/src/HOL/Power.thy	Tue Mar 31 21:54:32 2015 +0200
    25.3 @@ -705,7 +705,7 @@
    25.4  
    25.5  text{*Perhaps these should be simprules.*}
    25.6  lemma power_inverse:
    25.7 -  fixes a :: "'a::division_ring_inverse_zero"
    25.8 +  fixes a :: "'a::division_ring"
    25.9    shows "inverse (a ^ n) = inverse a ^ n"
   25.10  apply (cases "a = 0")
   25.11  apply (simp add: power_0_left)
   25.12 @@ -713,11 +713,11 @@
   25.13  done (* TODO: reorient or rename to inverse_power *)
   25.14  
   25.15  lemma power_one_over:
   25.16 -  "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
   25.17 +  "1 / (a::'a::{field, power}) ^ n =  (1 / a) ^ n"
   25.18    by (simp add: divide_inverse) (rule power_inverse)
   25.19  
   25.20  lemma power_divide [field_simps, divide_simps]:
   25.21 -  "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
   25.22 +  "(a / b) ^ n = (a::'a::field) ^ n / b ^ n"
   25.23  apply (cases "b = 0")
   25.24  apply (simp add: power_0_left)
   25.25  apply (rule nonzero_power_divide)
    26.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Tue Mar 31 16:49:41 2015 +0100
    26.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Mar 31 21:54:32 2015 +0200
    26.3 @@ -676,7 +676,7 @@
    26.4    has_bochner_integral_bounded_linear[OF bounded_linear_divide]
    26.5  
    26.6  lemma has_bochner_integral_divide_zero[intro]:
    26.7 -  fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
    26.8 +  fixes c :: "_::{real_normed_field, field, second_countable_topology}"
    26.9    shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x / c) (x / c)"
   26.10    using has_bochner_integral_divide by (cases "c = 0") auto
   26.11  
   26.12 @@ -990,7 +990,7 @@
   26.13    unfolding integrable.simps by fastforce
   26.14  
   26.15  lemma integrable_divide_zero[simp, intro]:
   26.16 -  fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
   26.17 +  fixes c :: "_::{real_normed_field, field, second_countable_topology}"
   26.18    shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)"
   26.19    unfolding integrable.simps by fastforce
   26.20  
   26.21 @@ -1098,7 +1098,7 @@
   26.22    by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right)
   26.23  
   26.24  lemma integral_divide_zero[simp]:
   26.25 -  fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
   26.26 +  fixes c :: "_::{real_normed_field, field, second_countable_topology}"
   26.27    shows "integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c"
   26.28    by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp
   26.29  
    27.1 --- a/src/HOL/Probability/Interval_Integral.thy	Tue Mar 31 16:49:41 2015 +0100
    27.2 +++ b/src/HOL/Probability/Interval_Integral.thy	Tue Mar 31 21:54:32 2015 +0200
    27.3 @@ -220,7 +220,7 @@
    27.4    by (simp add: interval_lebesgue_integrable_def)
    27.5  
    27.6  lemma interval_lebesgue_integrable_divide [intro, simp]:
    27.7 -  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
    27.8 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
    27.9    shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
   27.10      interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
   27.11    by (simp add: interval_lebesgue_integrable_def)
   27.12 @@ -238,7 +238,7 @@
   27.13    by (simp add: interval_lebesgue_integral_def)
   27.14  
   27.15  lemma interval_lebesgue_integral_divide [simp]:
   27.16 -  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
   27.17 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
   27.18    shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) =
   27.19      interval_lebesgue_integral M a b f / c"
   27.20    by (simp add: interval_lebesgue_integral_def)
    28.1 --- a/src/HOL/Probability/Set_Integral.thy	Tue Mar 31 16:49:41 2015 +0100
    28.2 +++ b/src/HOL/Probability/Set_Integral.thy	Tue Mar 31 21:54:32 2015 +0200
    28.3 @@ -125,7 +125,7 @@
    28.4    by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
    28.5  
    28.6  lemma set_integral_divide_zero [simp]: 
    28.7 -  fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}"
    28.8 +  fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
    28.9    shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
   28.10    by (subst integral_divide_zero[symmetric], intro integral_cong)
   28.11       (auto split: split_indicator)
   28.12 @@ -150,7 +150,7 @@
   28.13    using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   28.14  
   28.15  lemma set_integrable_divide [simp, intro]:
   28.16 -  fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}"
   28.17 +  fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   28.18    assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
   28.19    shows "set_integrable M A (\<lambda>t. f t / a)"
   28.20  proof -
    29.1 --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Tue Mar 31 16:49:41 2015 +0100
    29.2 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Tue Mar 31 21:54:32 2015 +0200
    29.3 @@ -161,7 +161,7 @@
    29.4    apply auto
    29.5    done
    29.6  
    29.7 -instantiation rat :: field_inverse_zero begin
    29.8 +instantiation rat :: field begin
    29.9  
   29.10  fun rat_inverse_raw where
   29.11    "rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))"
    30.1 --- a/src/HOL/Rat.thy	Tue Mar 31 16:49:41 2015 +0100
    30.2 +++ b/src/HOL/Rat.thy	Tue Mar 31 21:54:32 2015 +0200
    30.3 @@ -101,7 +101,7 @@
    30.4    shows "P q"
    30.5    using assms by (cases q) simp
    30.6  
    30.7 -instantiation rat :: field_inverse_zero
    30.8 +instantiation rat :: field
    30.9  begin
   30.10  
   30.11  lift_definition zero_rat :: "rat" is "(0, 1)"
   30.12 @@ -441,7 +441,7 @@
   30.13    "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
   30.14  by transfer (force simp: neq_iff zero_less_mult_iff mult_less_0_iff)
   30.15  
   30.16 -instantiation rat :: linordered_field_inverse_zero
   30.17 +instantiation rat :: linordered_field
   30.18  begin
   30.19  
   30.20  definition
   30.21 @@ -689,7 +689,7 @@
   30.22  done
   30.23  
   30.24  lemma of_rat_inverse:
   30.25 -  "(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) =
   30.26 +  "(of_rat (inverse a)::'a::{field_char_0, field}) =
   30.27     inverse (of_rat a)"
   30.28  by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
   30.29  
   30.30 @@ -698,7 +698,7 @@
   30.31  by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
   30.32  
   30.33  lemma of_rat_divide:
   30.34 -  "(of_rat (a / b)::'a::{field_char_0, field_inverse_zero})
   30.35 +  "(of_rat (a / b)::'a::{field_char_0, field})
   30.36     = of_rat a / of_rat b"
   30.37  by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
   30.38  
   30.39 @@ -875,7 +875,7 @@
   30.40  done
   30.41  
   30.42  lemma Rats_inverse [simp]:
   30.43 -  fixes a :: "'a::{field_char_0, field_inverse_zero}"
   30.44 +  fixes a :: "'a::{field_char_0, field}"
   30.45    shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
   30.46  apply (auto simp add: Rats_def)
   30.47  apply (rule range_eqI)
   30.48 @@ -891,7 +891,7 @@
   30.49  done
   30.50  
   30.51  lemma Rats_divide [simp]:
   30.52 -  fixes a b :: "'a::{field_char_0, field_inverse_zero}"
   30.53 +  fixes a b :: "'a::{field_char_0, field}"
   30.54    shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
   30.55  apply (auto simp add: Rats_def)
   30.56  apply (rule range_eqI)
    31.1 --- a/src/HOL/Real.thy	Tue Mar 31 16:49:41 2015 +0100
    31.2 +++ b/src/HOL/Real.thy	Tue Mar 31 21:54:32 2015 +0200
    31.3 @@ -393,7 +393,7 @@
    31.4  lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy"
    31.5  by (simp add: real.domain_eq realrel_def)
    31.6  
    31.7 -instantiation real :: field_inverse_zero
    31.8 +instantiation real :: field
    31.9  begin
   31.10  
   31.11  lift_definition zero_real :: "real" is "\<lambda>n. 0"
   31.12 @@ -575,7 +575,7 @@
   31.13  apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)
   31.14  done
   31.15  
   31.16 -instantiation real :: linordered_field_inverse_zero
   31.17 +instantiation real :: linordered_field
   31.18  begin
   31.19  
   31.20  definition
    32.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 31 16:49:41 2015 +0100
    32.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Mar 31 21:54:32 2015 +0200
    32.3 @@ -221,7 +221,7 @@
    32.4  by (rule inverse_unique, simp)
    32.5  
    32.6  lemma inverse_scaleR_distrib:
    32.7 -  fixes x :: "'a::{real_div_algebra, division_ring_inverse_zero}"
    32.8 +  fixes x :: "'a::{real_div_algebra, division_ring}"
    32.9    shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
   32.10  apply (case_tac "a = 0", simp)
   32.11  apply (case_tac "x = 0", simp)
   32.12 @@ -270,7 +270,7 @@
   32.13  
   32.14  lemma of_real_inverse [simp]:
   32.15    "of_real (inverse x) =
   32.16 -   inverse (of_real x :: 'a::{real_div_algebra, division_ring_inverse_zero})"
   32.17 +   inverse (of_real x :: 'a::{real_div_algebra, division_ring})"
   32.18  by (simp add: of_real_def inverse_scaleR_distrib)
   32.19  
   32.20  lemma nonzero_of_real_divide:
   32.21 @@ -280,7 +280,7 @@
   32.22  
   32.23  lemma of_real_divide [simp]:
   32.24    "of_real (x / y) =
   32.25 -   (of_real x / of_real y :: 'a::{real_field, field_inverse_zero})"
   32.26 +   (of_real x / of_real y :: 'a::{real_field, field})"
   32.27  by (simp add: divide_inverse)
   32.28  
   32.29  lemma of_real_power [simp]:
   32.30 @@ -398,7 +398,7 @@
   32.31  done
   32.32  
   32.33  lemma Reals_inverse:
   32.34 -  fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}"
   32.35 +  fixes a :: "'a::{real_div_algebra, division_ring}"
   32.36    shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
   32.37  apply (auto simp add: Reals_def)
   32.38  apply (rule range_eqI)
   32.39 @@ -406,7 +406,7 @@
   32.40  done
   32.41  
   32.42  lemma Reals_inverse_iff [simp]: 
   32.43 -  fixes x:: "'a :: {real_div_algebra, division_ring_inverse_zero}"
   32.44 +  fixes x:: "'a :: {real_div_algebra, division_ring}"
   32.45    shows "inverse x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
   32.46  by (metis Reals_inverse inverse_inverse_eq)
   32.47  
   32.48 @@ -419,7 +419,7 @@
   32.49  done
   32.50  
   32.51  lemma Reals_divide [simp]:
   32.52 -  fixes a b :: "'a::{real_field, field_inverse_zero}"
   32.53 +  fixes a b :: "'a::{real_field, field}"
   32.54    shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
   32.55  apply (auto simp add: Reals_def)
   32.56  apply (rule range_eqI)
   32.57 @@ -819,7 +819,7 @@
   32.58  done
   32.59  
   32.60  lemma norm_inverse:
   32.61 -  fixes a :: "'a::{real_normed_div_algebra, division_ring_inverse_zero}"
   32.62 +  fixes a :: "'a::{real_normed_div_algebra, division_ring}"
   32.63    shows "norm (inverse a) = inverse (norm a)"
   32.64  apply (case_tac "a = 0", simp)
   32.65  apply (erule nonzero_norm_inverse)
   32.66 @@ -831,7 +831,7 @@
   32.67  by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
   32.68  
   32.69  lemma norm_divide:
   32.70 -  fixes a b :: "'a::{real_normed_field, field_inverse_zero}"
   32.71 +  fixes a b :: "'a::{real_normed_field, field}"
   32.72    shows "norm (a / b) = norm a / norm b"
   32.73  by (simp add: divide_inverse norm_mult norm_inverse)
   32.74  
    33.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Tue Mar 31 16:49:41 2015 +0100
    33.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Mar 31 21:54:32 2015 +0200
    33.3 @@ -449,12 +449,12 @@
    33.4  val field_divide_cancel_numeral_factor =
    33.5    [prep_simproc @{theory}
    33.6      ("field_divide_cancel_numeral_factor",
    33.7 -     ["((l::'a::field_inverse_zero) * m) / n",
    33.8 -      "(l::'a::field_inverse_zero) / (m * n)",
    33.9 -      "((numeral v)::'a::field_inverse_zero) / (numeral w)",
   33.10 -      "((numeral v)::'a::field_inverse_zero) / (- numeral w)",
   33.11 -      "((- numeral v)::'a::field_inverse_zero) / (numeral w)",
   33.12 -      "((- numeral v)::'a::field_inverse_zero) / (- numeral w)"],
   33.13 +     ["((l::'a::field) * m) / n",
   33.14 +      "(l::'a::field) / (m * n)",
   33.15 +      "((numeral v)::'a::field) / (numeral w)",
   33.16 +      "((numeral v)::'a::field) / (- numeral w)",
   33.17 +      "((- numeral v)::'a::field) / (numeral w)",
   33.18 +      "((- numeral v)::'a::field) / (- numeral w)"],
   33.19       DivideCancelNumeralFactor.proc)];
   33.20  
   33.21  val field_cancel_numeral_factors =
    34.1 --- a/src/HOL/Transcendental.thy	Tue Mar 31 16:49:41 2015 +0100
    34.2 +++ b/src/HOL/Transcendental.thy	Tue Mar 31 21:54:32 2015 +0200
    34.3 @@ -2231,7 +2231,7 @@
    34.4  
    34.5  lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
    34.6    by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
    34.7 -            order.strict_trans2 powr_gt_zero zero_less_one)
    34.8 +            powr_gt_zero)
    34.9  
   34.10  lemma ln_powr_bound2:
   34.11    assumes "1 < x" and "0 < a"
   34.12 @@ -3109,29 +3109,29 @@
   34.13    shows "cos(w) * cos(z) = (cos(w - z) + cos(w + z)) / 2"
   34.14    by (simp add: cos_diff cos_add)
   34.15  
   34.16 -lemma sin_plus_sin:  (*FIXME field_inverse_zero should not be necessary*)
   34.17 -  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
   34.18 +lemma sin_plus_sin:  (*FIXME field should not be necessary*)
   34.19 +  fixes w :: "'a::{real_normed_field,banach,field}"
   34.20    shows "sin(w) + sin(z) = 2 * sin((w + z) / 2) * cos((w - z) / 2)"
   34.21    apply (simp add: mult.assoc sin_times_cos)
   34.22    apply (simp add: field_simps)
   34.23    done
   34.24  
   34.25  lemma sin_diff_sin: 
   34.26 -  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
   34.27 +  fixes w :: "'a::{real_normed_field,banach,field}"
   34.28    shows "sin(w) - sin(z) = 2 * sin((w - z) / 2) * cos((w + z) / 2)"
   34.29    apply (simp add: mult.assoc sin_times_cos)
   34.30    apply (simp add: field_simps)
   34.31    done
   34.32  
   34.33  lemma cos_plus_cos: 
   34.34 -  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
   34.35 +  fixes w :: "'a::{real_normed_field,banach,field}"
   34.36    shows "cos(w) + cos(z) = 2 * cos((w + z) / 2) * cos((w - z) / 2)"
   34.37    apply (simp add: mult.assoc cos_times_cos)
   34.38    apply (simp add: field_simps)
   34.39    done
   34.40  
   34.41  lemma cos_diff_cos: 
   34.42 -  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
   34.43 +  fixes w :: "'a::{real_normed_field,banach,field}"
   34.44    shows "cos(w) - cos(z) = 2 * sin((w + z) / 2) * sin((z - w) / 2)"
   34.45    apply (simp add: mult.assoc sin_times_sin)
   34.46    apply (simp add: field_simps)
   34.47 @@ -3671,12 +3671,12 @@
   34.48    where "tan = (\<lambda>x. sin x / cos x)"
   34.49  
   34.50  lemma tan_of_real:
   34.51 -  fixes XXX :: "'a::{real_normed_field,banach,field_inverse_zero}"
   34.52 +  fixes XXX :: "'a::{real_normed_field,banach}"
   34.53    shows  "of_real(tan x) = (tan(of_real x) :: 'a)"
   34.54    by (simp add: tan_def sin_of_real cos_of_real)
   34.55  
   34.56  lemma tan_in_Reals [simp]:
   34.57 -  fixes z :: "'a::{real_normed_field,banach,field_inverse_zero}"
   34.58 +  fixes z :: "'a::{real_normed_field,banach}"
   34.59    shows "z \<in> \<real> \<Longrightarrow> tan z \<in> \<real>"
   34.60    by (simp add: tan_def)
   34.61  
   34.62 @@ -3730,7 +3730,7 @@
   34.63  qed
   34.64  
   34.65  lemma tan_half:
   34.66 -  fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}"
   34.67 +  fixes x :: "'a::{real_normed_field,banach,field}"
   34.68    shows  "tan x = sin (2 * x) / (cos (2 * x) + 1)"
   34.69    unfolding tan_def sin_double cos_double sin_squared_eq
   34.70    by (simp add: power2_eq_square)
   34.71 @@ -4137,7 +4137,7 @@
   34.72    by (simp add: eq_divide_eq)
   34.73  
   34.74  lemma tan_sec:
   34.75 -  fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}"
   34.76 +  fixes x :: "'a::{real_normed_field,banach,field}"
   34.77    shows "cos x \<noteq> 0 \<Longrightarrow> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
   34.78    apply (rule power_inverse [THEN subst])
   34.79    apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
    35.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Mar 31 16:49:41 2015 +0100
    35.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Mar 31 21:54:32 2015 +0200
    35.3 @@ -1435,7 +1435,7 @@
    35.4  
    35.5  subsection{*The Real Numbers form a Field*}
    35.6  
    35.7 -instance real :: field_inverse_zero
    35.8 +instance real :: field
    35.9  proof
   35.10    fix x y z :: real
   35.11    show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
   35.12 @@ -1574,7 +1574,7 @@
   35.13  
   35.14  subsection{*The Reals Form an Ordered Field*}
   35.15  
   35.16 -instance real :: linordered_field_inverse_zero
   35.17 +instance real :: linordered_field
   35.18  proof
   35.19    fix x y z :: real
   35.20    show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
    36.1 --- a/src/HOL/ex/Simproc_Tests.thy	Tue Mar 31 16:49:41 2015 +0100
    36.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Tue Mar 31 21:54:32 2015 +0200
    36.3 @@ -279,7 +279,7 @@
    36.4  subsection {* @{text divide_cancel_numeral_factor} *}
    36.5  
    36.6  notepad begin
    36.7 -  fix x y z :: "'a::{field_inverse_zero,ring_char_0}"
    36.8 +  fix x y z :: "'a::{field,ring_char_0}"
    36.9    {
   36.10      assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
   36.11        by (tactic {* test @{context} [@{simproc divide_cancel_numeral_factor}] *}) fact
   36.12 @@ -346,13 +346,13 @@
   36.13    }
   36.14  end
   36.15  
   36.16 -lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field_inverse_zero)*(x*a)/z"
   36.17 +lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field)*(x*a)/z"
   36.18  oops -- "FIXME: need simproc to cover this case"
   36.19  
   36.20  subsection {* @{text divide_cancel_factor} *}
   36.21  
   36.22  notepad begin
   36.23 -  fix a b c d k uu x y :: "'a::field_inverse_zero"
   36.24 +  fix a b c d k uu x y :: "'a::field"
   36.25    {
   36.26      assume "(if k = 0 then 0 else x / y) = uu"
   36.27      have "(x*k) / (k*y) = uu"
   36.28 @@ -373,7 +373,7 @@
   36.29  end
   36.30  
   36.31  lemma
   36.32 -  fixes a b c d x y z :: "'a::linordered_field_inverse_zero"
   36.33 +  fixes a b c d x y z :: "'a::linordered_field"
   36.34    shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
   36.35  oops -- "FIXME: need simproc to cover this case"
   36.36  
   36.37 @@ -420,7 +420,7 @@
   36.38  subsection {* @{text field_combine_numerals} *}
   36.39  
   36.40  notepad begin
   36.41 -  fix x y z uu :: "'a::{field_inverse_zero,ring_char_0}"
   36.42 +  fix x y z uu :: "'a::{field,ring_char_0}"
   36.43    {
   36.44      assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
   36.45        by (tactic {* test @{context} [@{simproc field_combine_numerals}] *}) fact
   36.46 @@ -442,7 +442,7 @@
   36.47  end
   36.48  
   36.49  lemma
   36.50 -  fixes x :: "'a::{linordered_field_inverse_zero}"
   36.51 +  fixes x :: "'a::{linordered_field}"
   36.52    shows "2/3 * x + x / 3 = uu"
   36.53  apply (tactic {* test @{context} [@{simproc field_combine_numerals}] *})?
   36.54  oops -- "FIXME: test fails"