author nipkow Thu Jun 14 15:45:53 2018 +0200 (10 days ago) changeset 68442 477b3f7067c9 parent 68441 3b11d48a711a child 68448 3d1517f3ba49
tuned
```     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.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.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.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.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.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.71
3.72  lemma Nlt0_iff[simp]:
3.73 @@ -463,7 +463,7 @@
3.74  qed
3.75
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.111
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.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.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.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.66    let ?h = "headconst p"
4.67 @@ -726,13 +726,13 @@
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.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.139
4.140 @@ -854,7 +854,7 @@
4.142    assumes "isnpolyh p n"
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.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.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.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.255 @@ -1478,7 +1478,7 @@
4.256    done
4.257
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.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.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.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
```