tuned
authornipkow
Thu Jun 14 15:45:53 2018 +0200 (3 months ago)
changeset 68442477b3f7067c9
parent 68441 3b11d48a711a
child 68448 3d1517f3ba49
tuned
src/HOL/Computational_Algebra/Formal_Power_Series.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     1.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Jun 14 10:51:12 2018 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Jun 14 15:45:53 2018 +0200
     1.3 @@ -4601,7 +4601,7 @@
     1.4  
     1.5  subsection \<open>Hypergeometric series\<close>
     1.6  
     1.7 -definition "fps_hypergeo as bs (c::'a::{field_char_0,field}) =
     1.8 +definition "fps_hypergeo as bs (c::'a::field_char_0) =
     1.9    Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
    1.10      (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
    1.11  
    1.12 @@ -4686,11 +4686,11 @@
    1.13    by (simp add: fps_eq_iff fps_integral_def)
    1.14  
    1.15  lemma fps_hypergeo_minus_nat:
    1.16 -  "fps_hypergeo [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
    1.17 +  "fps_hypergeo [- of_nat n] [- of_nat (n + m)] (c::'a::field_char_0) $ k =
    1.18      (if k \<le> n then
    1.19        pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
    1.20       else 0)"
    1.21 -  "fps_hypergeo [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
    1.22 +  "fps_hypergeo [- of_nat m] [- of_nat (m + n)] (c::'a::field_char_0) $ k =
    1.23      (if k \<le> m then
    1.24        pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
    1.25       else 0)"
     2.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jun 14 10:51:12 2018 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jun 14 15:45:53 2018 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4  end
     2.5  
     2.6  text \<open>Semantics of terms tm.\<close>
     2.7 -primrec Itm :: "'a::{field_char_0,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     2.8 +primrec Itm :: "'a::field_char_0 list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     2.9    where
    2.10      "Itm vs bs (CP c) = (Ipoly vs c)"
    2.11    | "Itm vs bs (Bound n) = bs!n"
    2.12 @@ -319,7 +319,7 @@
    2.13    by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
    2.14  
    2.15  lemma tmmul_allpolys_npoly[simp]:
    2.16 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.17 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.18    shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)"
    2.19    by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)
    2.20  
    2.21 @@ -345,7 +345,7 @@
    2.22    by (simp add: isnpoly_def)
    2.23  
    2.24  lemma tmneg_allpolys_npoly[simp]:
    2.25 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.26 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.27    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
    2.28    by (auto simp: tmneg_def)
    2.29  
    2.30 @@ -362,7 +362,7 @@
    2.31    using tmsub_def by simp
    2.32  
    2.33  lemma tmsub_allpolys_npoly[simp]:
    2.34 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.35 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.36    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
    2.37    by (simp add: tmsub_def isnpoly_def)
    2.38  
    2.39 @@ -379,7 +379,7 @@
    2.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))"
    2.41  
    2.42  lemma polynate_stupid:
    2.43 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.44 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.45    shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
    2.46    apply (subst polynate[symmetric])
    2.47    apply simp
    2.48 @@ -402,7 +402,7 @@
    2.49    by (simp_all add: isnpoly_def)
    2.50  
    2.51  lemma simptm_allpolys_npoly[simp]:
    2.52 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.53 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.54    shows "allpolys isnpoly (simptm p)"
    2.55    by (induct p rule: simptm.induct) (auto simp add: Let_def)
    2.56  
    2.57 @@ -452,7 +452,7 @@
    2.58  qed
    2.59  
    2.60  lemma split0_nb0:
    2.61 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.62 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.63    shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
    2.64  proof -
    2.65    fix c' t'
    2.66 @@ -464,7 +464,7 @@
    2.67  qed
    2.68  
    2.69  lemma split0_nb0'[simp]:
    2.70 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.71 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.72    shows "tmbound0 (snd (split0 t))"
    2.73    using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
    2.74    by (simp add: tmbound0_tmbound_iff)
    2.75 @@ -492,7 +492,7 @@
    2.76    by (induct p rule: split0.induct) (auto simp  add: isnpoly_def Let_def split_def)
    2.77  
    2.78  lemma isnpoly_fst_split0:
    2.79 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.80 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.81    shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
    2.82    by (induct p rule: split0.induct)
    2.83      (auto simp  add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)
    2.84 @@ -1172,7 +1172,7 @@
    2.85  definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"
    2.86  
    2.87  lemma simplt_islin [simp]:
    2.88 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.89 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.90    shows "islin (simplt t)"
    2.91    unfolding simplt_def
    2.92    using split0_nb0'
    2.93 @@ -1180,7 +1180,7 @@
    2.94        islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
    2.95  
    2.96  lemma simple_islin [simp]:
    2.97 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    2.98 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    2.99    shows "islin (simple t)"
   2.100    unfolding simple_def
   2.101    using split0_nb0'
   2.102 @@ -1188,7 +1188,7 @@
   2.103        islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
   2.104  
   2.105  lemma simpeq_islin [simp]:
   2.106 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.107 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.108    shows "islin (simpeq t)"
   2.109    unfolding simpeq_def
   2.110    using split0_nb0'
   2.111 @@ -1196,7 +1196,7 @@
   2.112        islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
   2.113  
   2.114  lemma simpneq_islin [simp]:
   2.115 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.116 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.117    shows "islin (simpneq t)"
   2.118    unfolding simpneq_def
   2.119    using split0_nb0'
   2.120 @@ -1207,7 +1207,7 @@
   2.121    by (cases "split0 s") auto
   2.122  
   2.123  lemma split0_npoly:
   2.124 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.125 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.126      and *: "allpolys isnpoly t"
   2.127    shows "isnpoly (fst (split0 t))"
   2.128      and "allpolys isnpoly (snd (split0 t))"
   2.129 @@ -1323,7 +1323,7 @@
   2.130    done
   2.131  
   2.132  lemma simplt_nb[simp]:
   2.133 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.134 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.135    shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
   2.136  proof (simp add: simplt_def Let_def split_def)
   2.137    assume "tmbound0 t"
   2.138 @@ -1344,7 +1344,7 @@
   2.139  qed
   2.140  
   2.141  lemma simple_nb[simp]:
   2.142 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.143 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.144    shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
   2.145  proof(simp add: simple_def Let_def split_def)
   2.146    assume "tmbound0 t"
   2.147 @@ -1365,7 +1365,7 @@
   2.148  qed
   2.149  
   2.150  lemma simpeq_nb[simp]:
   2.151 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.152 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.153    shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
   2.154  proof (simp add: simpeq_def Let_def split_def)
   2.155    assume "tmbound0 t"
   2.156 @@ -1386,7 +1386,7 @@
   2.157  qed
   2.158  
   2.159  lemma simpneq_nb[simp]:
   2.160 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.161 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.162    shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
   2.163  proof (simp add: simpneq_def Let_def split_def)
   2.164    assume "tmbound0 t"
   2.165 @@ -1541,7 +1541,7 @@
   2.166    by (induct p arbitrary: bs rule: simpfm.induct) auto
   2.167  
   2.168  lemma simpfm_bound0:
   2.169 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.170 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.171    shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   2.172    by (induct p rule: simpfm.induct) auto
   2.173  
   2.174 @@ -1591,7 +1591,7 @@
   2.175    by (simp add: conj_def)
   2.176  
   2.177  lemma
   2.178 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.179 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.180    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   2.181    by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
   2.182  
   2.183 @@ -3313,7 +3313,7 @@
   2.184  qed
   2.185  
   2.186  lemma simpfm_lin:
   2.187 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.188 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.189    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   2.190    by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)
   2.191  
   2.192 @@ -3627,7 +3627,7 @@
   2.193      (auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
   2.194  
   2.195  lemma msubstneg_nb:
   2.196 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.197 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.198      and lp: "islin p"
   2.199      and tnb: "tmbound0 t"
   2.200    shows "bound0 (msubstneg p c t)"
   2.201 @@ -3636,7 +3636,7 @@
   2.202      (auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
   2.203  
   2.204  lemma msubst2_nb:
   2.205 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.206 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   2.207      and lp: "islin p"
   2.208      and tnb: "tmbound0 t"
   2.209    shows "bound0 (msubst2 p c t)"
     3.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Jun 14 10:51:12 2018 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Jun 14 15:45:53 2018 +0200
     3.3 @@ -177,7 +177,7 @@
     3.4  lemma isnormNum_unique[simp]:
     3.5    assumes na: "isnormNum x"
     3.6      and nb: "isnormNum y"
     3.7 -  shows "(INum x ::'a::{field_char_0,field}) = INum y \<longleftrightarrow> x = y"
     3.8 +  shows "(INum x ::'a::field_char_0) = INum y \<longleftrightarrow> x = y"
     3.9    (is "?lhs = ?rhs")
    3.10  proof
    3.11    obtain a b where x: "x = (a, b)" by (cases x)
    3.12 @@ -217,7 +217,7 @@
    3.13      using that by simp
    3.14  qed
    3.15  
    3.16 -lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> INum x = (0::'a::{field_char_0,field}) \<longleftrightarrow> x = 0\<^sub>N"
    3.17 +lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> INum x = (0::'a::field_char_0) \<longleftrightarrow> x = 0\<^sub>N"
    3.18    unfolding INum_int(2)[symmetric]
    3.19    by (rule isnormNum_unique) simp_all
    3.20  
    3.21 @@ -244,7 +244,7 @@
    3.22    shows "(of_int (n div d) ::'a::field_char_0) = of_int n / of_int d"
    3.23    using assms of_int_div_aux [of d n, where ?'a = 'a] by simp
    3.24  
    3.25 -lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0,field})"
    3.26 +lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::field_char_0)"
    3.27  proof -
    3.28    obtain a b where x: "x = (a, b)" by (cases x)
    3.29    consider "a = 0 \<or> b = 0" | "a \<noteq> 0" "b \<noteq> 0" by blast
    3.30 @@ -262,7 +262,7 @@
    3.31    qed
    3.32  qed
    3.33  
    3.34 -lemma INum_normNum_iff: "(INum x ::'a::{field_char_0,field}) = INum y \<longleftrightarrow> normNum x = normNum y"
    3.35 +lemma INum_normNum_iff: "(INum x ::'a::field_char_0) = INum y \<longleftrightarrow> normNum x = normNum y"
    3.36    (is "?lhs \<longleftrightarrow> _")
    3.37  proof -
    3.38    have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
    3.39 @@ -271,7 +271,7 @@
    3.40    finally show ?thesis by simp
    3.41  qed
    3.42  
    3.43 -lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0,field})"
    3.44 +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: field_char_0)"
    3.45  proof -
    3.46    let ?z = "0::'a"
    3.47    obtain a b where x: "x = (a, b)" by (cases x)
    3.48 @@ -319,7 +319,7 @@
    3.49    qed
    3.50  qed
    3.51  
    3.52 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a::{field_char_0,field})"
    3.53 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a::field_char_0)"
    3.54  proof -
    3.55    let ?z = "0::'a"
    3.56    obtain a b where x: "x = (a, b)" by (cases x)
    3.57 @@ -346,13 +346,13 @@
    3.58  lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x :: 'a::field)"
    3.59    by (simp add: Nneg_def split_def INum_def)
    3.60  
    3.61 -lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a::{field_char_0,field})"
    3.62 +lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a::field_char_0)"
    3.63    by (simp add: Nsub_def split_def)
    3.64  
    3.65  lemma Ninv[simp]: "INum (Ninv x) = (1 :: 'a::field) / INum x"
    3.66    by (simp add: Ninv_def INum_def split_def)
    3.67  
    3.68 -lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y :: 'a::{field_char_0,field})"
    3.69 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y :: 'a::field_char_0)"
    3.70    by (simp add: Ndiv_def)
    3.71  
    3.72  lemma Nlt0_iff[simp]:
    3.73 @@ -463,7 +463,7 @@
    3.74  qed
    3.75  
    3.76  lemma Nadd_commute:
    3.77 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    3.78 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    3.79    shows "x +\<^sub>N y = y +\<^sub>N x"
    3.80  proof -
    3.81    have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)"
    3.82 @@ -475,7 +475,7 @@
    3.83  qed
    3.84  
    3.85  lemma [simp]:
    3.86 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    3.87 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    3.88    shows "(0, b) +\<^sub>N y = normNum y"
    3.89      and "(a, 0) +\<^sub>N y = normNum y"
    3.90      and "x +\<^sub>N (0, b) = normNum x"
    3.91 @@ -489,7 +489,7 @@
    3.92    done
    3.93  
    3.94  lemma normNum_nilpotent_aux[simp]:
    3.95 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    3.96 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    3.97    assumes nx: "isnormNum x"
    3.98    shows "normNum x = x"
    3.99  proof -
   3.100 @@ -500,7 +500,7 @@
   3.101  qed
   3.102  
   3.103  lemma normNum_nilpotent[simp]:
   3.104 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   3.105 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   3.106    shows "normNum (normNum x) = normNum x"
   3.107    by simp
   3.108  
   3.109 @@ -508,12 +508,12 @@
   3.110    by (simp_all add: normNum_def)
   3.111  
   3.112  lemma normNum_Nadd:
   3.113 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   3.114 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   3.115    shows "normNum (x +\<^sub>N y) = x +\<^sub>N y"
   3.116    by simp
   3.117  
   3.118  lemma Nadd_normNum1[simp]:
   3.119 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   3.120 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   3.121    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
   3.122  proof -
   3.123    have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)"
   3.124 @@ -527,7 +527,7 @@
   3.125  qed
   3.126  
   3.127  lemma Nadd_normNum2[simp]:
   3.128 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   3.129 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   3.130    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
   3.131  proof -
   3.132    have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)"
   3.133 @@ -541,7 +541,7 @@
   3.134  qed
   3.135  
   3.136  lemma Nadd_assoc:
   3.137 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   3.138 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   3.139    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   3.140  proof -
   3.141    have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))"
   3.142 @@ -556,7 +556,7 @@
   3.143    by (simp add: Nmul_def split_def Let_def gcd.commute mult.commute)
   3.144  
   3.145  lemma Nmul_assoc:
   3.146 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   3.147 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   3.148    assumes nx: "isnormNum x"
   3.149      and ny: "isnormNum y"
   3.150      and nz: "isnormNum z"
   3.151 @@ -571,7 +571,7 @@
   3.152  qed
   3.153  
   3.154  lemma Nsub0:
   3.155 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   3.156 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   3.157    assumes x: "isnormNum x"
   3.158      and y: "isnormNum y"
   3.159    shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
   3.160 @@ -590,7 +590,7 @@
   3.161    by (simp_all add: Nmul_def Let_def split_def)
   3.162  
   3.163  lemma Nmul_eq0[simp]:
   3.164 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   3.165 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   3.166    assumes nx: "isnormNum x"
   3.167      and ny: "isnormNum y"
   3.168    shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
     4.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 14 10:51:12 2018 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 14 15:45:53 2018 +0200
     4.3 @@ -234,7 +234,7 @@
     4.4  
     4.5  subsection \<open>Semantics of the polynomial representation\<close>
     4.6  
     4.7 -primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
     4.8 +primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,power}"
     4.9    where
    4.10      "Ipoly bs (C c) = INum c"
    4.11    | "Ipoly bs (Bound n) = bs!n"
    4.12 @@ -245,7 +245,7 @@
    4.13    | "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
    4.14    | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
    4.15  
    4.16 -abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"  ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    4.17 +abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,power}"  ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    4.18    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
    4.19  
    4.20  lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i"
    4.21 @@ -462,7 +462,7 @@
    4.22  qed simp_all
    4.23  
    4.24  lemma polymul_properties:
    4.25 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    4.26 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    4.27      and np: "isnpolyh p n0"
    4.28      and nq: "isnpolyh q n1"
    4.29      and m: "m \<le> min n0 n1"
    4.30 @@ -646,23 +646,23 @@
    4.31    by (induct p q rule: polymul.induct) (auto simp add: field_simps)
    4.32  
    4.33  lemma polymul_normh:
    4.34 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    4.35 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    4.36    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
    4.37    using polymul_properties(1) by blast
    4.38  
    4.39  lemma polymul_eq0_iff:
    4.40 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    4.41 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    4.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"
    4.43    using polymul_properties(2) by blast
    4.44  
    4.45  lemma polymul_degreen:
    4.46 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    4.47 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    4.48    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
    4.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)"
    4.50    by (fact polymul_properties(3))
    4.51  
    4.52  lemma polymul_norm:
    4.53 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    4.54 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    4.55    shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)"
    4.56    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
    4.57  
    4.58 @@ -675,7 +675,7 @@
    4.59  lemma monic_eqI:
    4.60    assumes np: "isnpolyh p n0"
    4.61    shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
    4.62 -    (Ipoly bs p ::'a::{field_char_0,field, power})"
    4.63 +    (Ipoly bs p ::'a::{field_char_0, power})"
    4.64    unfolding monic_def Let_def
    4.65  proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
    4.66    let ?h = "headconst p"
    4.67 @@ -726,13 +726,13 @@
    4.68    using polyadd_norm polyneg_norm by (simp add: polysub_def)
    4.69  
    4.70  lemma polysub_same_0[simp]:
    4.71 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    4.72 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    4.73    shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p"
    4.74    unfolding polysub_def split_def fst_conv snd_conv
    4.75    by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def])
    4.76  
    4.77  lemma polysub_0:
    4.78 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    4.79 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    4.80    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p -\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = q"
    4.81    unfolding polysub_def split_def fst_conv snd_conv
    4.82    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
    4.83 @@ -740,7 +740,7 @@
    4.84  
    4.85  text \<open>polypow is a power function and preserves normal forms\<close>
    4.86  
    4.87 -lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
    4.88 +lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::field_char_0) ^ n"
    4.89  proof (induct n rule: polypow.induct)
    4.90    case 1
    4.91    then show ?case by simp
    4.92 @@ -777,7 +777,7 @@
    4.93  qed
    4.94  
    4.95  lemma polypow_normh:
    4.96 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    4.97 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    4.98    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
    4.99  proof (induct k arbitrary: n rule: polypow.induct)
   4.100    case 1
   4.101 @@ -796,17 +796,17 @@
   4.102  qed
   4.103  
   4.104  lemma polypow_norm:
   4.105 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.106 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.107    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   4.108    by (simp add: polypow_normh isnpoly_def)
   4.109  
   4.110  text \<open>Finally the whole normalization\<close>
   4.111  
   4.112 -lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
   4.113 +lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::field_char_0)"
   4.114    by (induct p rule:polynate.induct) auto
   4.115  
   4.116  lemma polynate_norm[simp]:
   4.117 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.118 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.119    shows "isnpoly (polynate p)"
   4.120    by (induct p rule: polynate.induct)
   4.121       (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
   4.122 @@ -836,7 +836,7 @@
   4.123    using assms by (induct k arbitrary: p) auto
   4.124  
   4.125  lemma funpow_shift1:
   4.126 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
   4.127 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: field_char_0) =
   4.128      Ipoly bs (Mul (Pw (Bound 0) n) p)"
   4.129    by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
   4.130  
   4.131 @@ -844,7 +844,7 @@
   4.132    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   4.133  
   4.134  lemma funpow_shift1_1:
   4.135 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
   4.136 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: field_char_0) =
   4.137      Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
   4.138    by (simp add: funpow_shift1)
   4.139  
   4.140 @@ -854,7 +854,7 @@
   4.141  lemma behead:
   4.142    assumes "isnpolyh p n"
   4.143    shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
   4.144 -    (Ipoly bs p :: 'a :: {field_char_0,field})"
   4.145 +    (Ipoly bs p :: 'a :: field_char_0)"
   4.146    using assms
   4.147  proof (induct p arbitrary: n rule: behead.induct)
   4.148    case (1 c p n)
   4.149 @@ -1120,7 +1120,7 @@
   4.150  
   4.151  lemma isnpolyh_zero_iff:
   4.152    assumes nq: "isnpolyh p n0"
   4.153 -    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field, power})"
   4.154 +    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, power})"
   4.155    shows "p = 0\<^sub>p"
   4.156    using nq eq
   4.157  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   4.158 @@ -1197,7 +1197,7 @@
   4.159  lemma isnpolyh_unique:
   4.160    assumes np: "isnpolyh p n0"
   4.161      and nq: "isnpolyh q n1"
   4.162 -  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"
   4.163 +  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,power})) \<longleftrightarrow> p = q"
   4.164  proof auto
   4.165    assume "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
   4.166    then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)"
   4.167 @@ -1212,7 +1212,7 @@
   4.168  text \<open>Consequences of unicity on the algorithms for polynomial normalization.\<close>
   4.169  
   4.170  lemma polyadd_commute:
   4.171 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.172 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.173      and np: "isnpolyh p n0"
   4.174      and nq: "isnpolyh q n1"
   4.175    shows "p +\<^sub>p q = q +\<^sub>p p"
   4.176 @@ -1226,7 +1226,7 @@
   4.177    by simp
   4.178  
   4.179  lemma polyadd_0[simp]:
   4.180 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.181 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.182      and np: "isnpolyh p n0"
   4.183    shows "p +\<^sub>p 0\<^sub>p = p"
   4.184      and "0\<^sub>p +\<^sub>p p = p"
   4.185 @@ -1234,7 +1234,7 @@
   4.186      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   4.187  
   4.188  lemma polymul_1[simp]:
   4.189 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.190 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.191      and np: "isnpolyh p n0"
   4.192    shows "p *\<^sub>p (1)\<^sub>p = p"
   4.193      and "(1)\<^sub>p *\<^sub>p p = p"
   4.194 @@ -1242,7 +1242,7 @@
   4.195      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   4.196  
   4.197  lemma polymul_0[simp]:
   4.198 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.199 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.200      and np: "isnpolyh p n0"
   4.201    shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p"
   4.202      and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
   4.203 @@ -1250,27 +1250,27 @@
   4.204      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
   4.205  
   4.206  lemma polymul_commute:
   4.207 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.208 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.209      and np: "isnpolyh p n0"
   4.210      and nq: "isnpolyh q n1"
   4.211    shows "p *\<^sub>p q = q *\<^sub>p p"
   4.212    using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np],
   4.213 -    where ?'a = "'a::{field_char_0,field, power}"]
   4.214 +    where ?'a = "'a::{field_char_0, power}"]
   4.215    by simp
   4.216  
   4.217  declare polyneg_polyneg [simp]
   4.218  
   4.219  lemma isnpolyh_polynate_id [simp]:
   4.220 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.221 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.222      and np: "isnpolyh p n0"
   4.223    shows "polynate p = p"
   4.224 -  using isnpolyh_unique[where ?'a= "'a::{field_char_0,field}",
   4.225 +  using isnpolyh_unique[where ?'a= "'a::field_char_0",
   4.226        OF polynate_norm[of p, unfolded isnpoly_def] np]
   4.227 -    polynate[where ?'a = "'a::{field_char_0,field}"]
   4.228 +    polynate[where ?'a = "'a::field_char_0"]
   4.229    by simp
   4.230  
   4.231  lemma polynate_idempotent[simp]:
   4.232 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.233 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.234    shows "polynate (polynate p) = polynate p"
   4.235    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
   4.236  
   4.237 @@ -1278,7 +1278,7 @@
   4.238    unfolding poly_nate_def polypoly'_def ..
   4.239  
   4.240  lemma poly_nate_poly:
   4.241 -  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   4.242 +  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::field_char_0. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   4.243    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
   4.244    unfolding poly_nate_polypoly' by auto
   4.245  
   4.246 @@ -1317,7 +1317,7 @@
   4.247  qed
   4.248  
   4.249  lemma degree_polysub_samehead:
   4.250 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.251 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.252      and np: "isnpolyh p n0"
   4.253      and nq: "isnpolyh q n1"
   4.254      and h: "head p = head q"
   4.255 @@ -1478,7 +1478,7 @@
   4.256    done
   4.257  
   4.258  lemma polymul_head_polyeq:
   4.259 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.260 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.261    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"
   4.262  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   4.263    case (2 c c' n' p' n0 n1)
   4.264 @@ -1575,7 +1575,7 @@
   4.265    by (induct p arbitrary: n0 rule: polyneg.induct) auto
   4.266  
   4.267  lemma degree_polymul:
   4.268 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.269 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.270      and np: "isnpolyh p n0"
   4.271      and nq: "isnpolyh q n1"
   4.272    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
   4.273 @@ -1591,7 +1591,7 @@
   4.274  subsection \<open>Correctness of polynomial pseudo division\<close>
   4.275  
   4.276  lemma polydivide_aux_properties:
   4.277 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.278 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.279      and np: "isnpolyh p n0"
   4.280      and ns: "isnpolyh s n1"
   4.281      and ap: "head p = a"
   4.282 @@ -1684,24 +1684,24 @@
   4.283                polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
   4.284              have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0"
   4.285                by simp
   4.286 -            from asp have "\<forall>bs :: 'a::{field_char_0,field} list.
   4.287 +            from asp have "\<forall>bs :: 'a::field_char_0 list.
   4.288                Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
   4.289                by simp
   4.290 -            then have "\<forall>bs :: 'a::{field_char_0,field} list.
   4.291 +            then have "\<forall>bs :: 'a::field_char_0 list.
   4.292                Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
   4.293                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   4.294                by (simp add: field_simps)
   4.295 -            then have "\<forall>bs :: 'a::{field_char_0,field} list.
   4.296 +            then have "\<forall>bs :: 'a::field_char_0 list.
   4.297                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   4.298                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) +
   4.299                Ipoly bs p * Ipoly bs q + Ipoly bs r"
   4.300                by (auto simp only: funpow_shift1_1)
   4.301 -            then have "\<forall>bs:: 'a::{field_char_0,field} list.
   4.302 +            then have "\<forall>bs:: 'a::field_char_0 list.
   4.303                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   4.304                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) +
   4.305                Ipoly bs q) + Ipoly bs r"
   4.306                by (simp add: field_simps)
   4.307 -            then have "\<forall>bs:: 'a::{field_char_0,field} list.
   4.308 +            then have "\<forall>bs:: 'a::field_char_0 list.
   4.309                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   4.310                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)"
   4.311                by simp
   4.312 @@ -1720,10 +1720,10 @@
   4.313            then show ?thesis by blast
   4.314          next
   4.315            case spz: 2
   4.316 -          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"]
   4.317 -          have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'"
   4.318 +          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::field_char_0"]
   4.319 +          have "\<forall>bs:: 'a::field_char_0 list. Ipoly bs s = Ipoly bs ?p'"
   4.320              by simp
   4.321 -          with np nxdn have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
   4.322 +          with np nxdn have "\<forall>bs:: 'a::field_char_0 list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
   4.323              by (simp only: funpow_shift1_1) simp
   4.324            then have sp': "s = ?xdn *\<^sub>p p"
   4.325              using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
   4.326 @@ -1801,7 +1801,7 @@
   4.327                by arith
   4.328              have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   4.329                  Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
   4.330 -              for bs :: "'a::{field_char_0,field} list"
   4.331 +              for bs :: "'a::field_char_0 list"
   4.332              proof -
   4.333                from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
   4.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)"
   4.335 @@ -1815,7 +1815,7 @@
   4.336                then show ?thesis
   4.337                  by (simp add: field_simps)
   4.338              qed
   4.339 -            then have ieq: "\<forall>bs :: 'a::{field_char_0,field} list.
   4.340 +            then have ieq: "\<forall>bs :: 'a::field_char_0 list.
   4.341                  Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   4.342                  Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
   4.343                by auto
   4.344 @@ -1837,10 +1837,10 @@
   4.345            then show ?thesis by blast
   4.346          next
   4.347            case spz: 2
   4.348 -          have hth: "\<forall>bs :: 'a::{field_char_0,field} list.
   4.349 +          have hth: "\<forall>bs :: 'a::field_char_0 list.
   4.350              Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
   4.351            proof
   4.352 -            fix bs :: "'a::{field_char_0,field} list"
   4.353 +            fix bs :: "'a::field_char_0 list"
   4.354              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   4.355              have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'"
   4.356                by simp
   4.357 @@ -1850,7 +1850,7 @@
   4.358                by simp
   4.359            qed
   4.360            from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
   4.361 -            using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
   4.362 +            using isnpolyh_unique[where ?'a = "'a::field_char_0", OF polymul_normh[OF head_isnpolyh[OF np] ns]
   4.363                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
   4.364                simplified ap]
   4.365              by simp
   4.366 @@ -1876,7 +1876,7 @@
   4.367  qed
   4.368  
   4.369  lemma polydivide_properties:
   4.370 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.371 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.372      and np: "isnpolyh p n0"
   4.373      and ns: "isnpolyh s n1"
   4.374      and pnz: "p \<noteq> 0\<^sub>p"
   4.375 @@ -2041,12 +2041,12 @@
   4.376  lemma swapnorm:
   4.377    assumes nbs: "n < length bs"
   4.378      and mbs: "m < length bs"
   4.379 -  shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field})) =
   4.380 +  shows "((Ipoly bs (swapnorm n m t) :: 'a::field_char_0)) =
   4.381      Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
   4.382    using swap[OF assms] swapnorm_def by simp
   4.383  
   4.384  lemma swapnorm_isnpoly [simp]:
   4.385 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   4.386 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   4.387    shows "isnpoly (swapnorm n m p)"
   4.388    unfolding swapnorm_def by simp
   4.389