--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Jun 14 10:51:12 2018 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Jun 14 15:45:53 2018 +0200
@@ -4601,7 +4601,7 @@
subsection \<open>Hypergeometric series\<close>
-definition "fps_hypergeo as bs (c::'a::{field_char_0,field}) =
+definition "fps_hypergeo as bs (c::'a::field_char_0) =
Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
(foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
@@ -4686,11 +4686,11 @@
by (simp add: fps_eq_iff fps_integral_def)
lemma fps_hypergeo_minus_nat:
- "fps_hypergeo [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
+ "fps_hypergeo [- of_nat n] [- of_nat (n + m)] (c::'a::field_char_0) $ k =
(if k \<le> n then
pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
else 0)"
- "fps_hypergeo [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
+ "fps_hypergeo [- of_nat m] [- of_nat (m + n)] (c::'a::field_char_0) $ k =
(if k \<le> m then
pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
else 0)"
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Jun 14 10:51:12 2018 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Jun 14 15:45:53 2018 +0200
@@ -35,7 +35,7 @@
end
text \<open>Semantics of terms tm.\<close>
-primrec Itm :: "'a::{field_char_0,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
+primrec Itm :: "'a::field_char_0 list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
where
"Itm vs bs (CP c) = (Ipoly vs c)"
| "Itm vs bs (Bound n) = bs!n"
@@ -319,7 +319,7 @@
by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
lemma tmmul_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)"
by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)
@@ -345,7 +345,7 @@
by (simp add: isnpoly_def)
lemma tmneg_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
by (auto simp: tmneg_def)
@@ -362,7 +362,7 @@
using tmsub_def by simp
lemma tmsub_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
by (simp add: tmsub_def isnpoly_def)
@@ -379,7 +379,7 @@
(let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p)) (simptm t))"
lemma polynate_stupid:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
apply (subst polynate[symmetric])
apply simp
@@ -402,7 +402,7 @@
by (simp_all add: isnpoly_def)
lemma simptm_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "allpolys isnpoly (simptm p)"
by (induct p rule: simptm.induct) (auto simp add: Let_def)
@@ -452,7 +452,7 @@
qed
lemma split0_nb0:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "split0 t = (c',t') \<Longrightarrow> tmbound 0 t'"
proof -
fix c' t'
@@ -464,7 +464,7 @@
qed
lemma split0_nb0'[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "tmbound0 (snd (split0 t))"
using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
by (simp add: tmbound0_tmbound_iff)
@@ -492,7 +492,7 @@
by (induct p rule: split0.induct) (auto simp add: isnpoly_def Let_def split_def)
lemma isnpoly_fst_split0:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
by (induct p rule: split0.induct)
(auto simp add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)
@@ -1172,7 +1172,7 @@
definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"
lemma simplt_islin [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "islin (simplt t)"
unfolding simplt_def
using split0_nb0'
@@ -1180,7 +1180,7 @@
islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
lemma simple_islin [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "islin (simple t)"
unfolding simple_def
using split0_nb0'
@@ -1188,7 +1188,7 @@
islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
lemma simpeq_islin [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "islin (simpeq t)"
unfolding simpeq_def
using split0_nb0'
@@ -1196,7 +1196,7 @@
islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
lemma simpneq_islin [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "islin (simpneq t)"
unfolding simpneq_def
using split0_nb0'
@@ -1207,7 +1207,7 @@
by (cases "split0 s") auto
lemma split0_npoly:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and *: "allpolys isnpoly t"
shows "isnpoly (fst (split0 t))"
and "allpolys isnpoly (snd (split0 t))"
@@ -1323,7 +1323,7 @@
done
lemma simplt_nb[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
proof (simp add: simplt_def Let_def split_def)
assume "tmbound0 t"
@@ -1344,7 +1344,7 @@
qed
lemma simple_nb[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
proof(simp add: simple_def Let_def split_def)
assume "tmbound0 t"
@@ -1365,7 +1365,7 @@
qed
lemma simpeq_nb[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
proof (simp add: simpeq_def Let_def split_def)
assume "tmbound0 t"
@@ -1386,7 +1386,7 @@
qed
lemma simpneq_nb[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
proof (simp add: simpneq_def Let_def split_def)
assume "tmbound0 t"
@@ -1541,7 +1541,7 @@
by (induct p arbitrary: bs rule: simpfm.induct) auto
lemma simpfm_bound0:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
by (induct p rule: simpfm.induct) auto
@@ -1591,7 +1591,7 @@
by (simp add: conj_def)
lemma
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
@@ -3313,7 +3313,7 @@
qed
lemma simpfm_lin:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)
@@ -3627,7 +3627,7 @@
(auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
lemma msubstneg_nb:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and lp: "islin p"
and tnb: "tmbound0 t"
shows "bound0 (msubstneg p c t)"
@@ -3636,7 +3636,7 @@
(auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
lemma msubst2_nb:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and lp: "islin p"
and tnb: "tmbound0 t"
shows "bound0 (msubst2 p c t)"
--- a/src/HOL/Decision_Procs/Rat_Pair.thy Thu Jun 14 10:51:12 2018 +0200
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy Thu Jun 14 15:45:53 2018 +0200
@@ -177,7 +177,7 @@
lemma isnormNum_unique[simp]:
assumes na: "isnormNum x"
and nb: "isnormNum y"
- shows "(INum x ::'a::{field_char_0,field}) = INum y \<longleftrightarrow> x = y"
+ shows "(INum x ::'a::field_char_0) = INum y \<longleftrightarrow> x = y"
(is "?lhs = ?rhs")
proof
obtain a b where x: "x = (a, b)" by (cases x)
@@ -217,7 +217,7 @@
using that by simp
qed
-lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> INum x = (0::'a::{field_char_0,field}) \<longleftrightarrow> x = 0\<^sub>N"
+lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> INum x = (0::'a::field_char_0) \<longleftrightarrow> x = 0\<^sub>N"
unfolding INum_int(2)[symmetric]
by (rule isnormNum_unique) simp_all
@@ -244,7 +244,7 @@
shows "(of_int (n div d) ::'a::field_char_0) = of_int n / of_int d"
using assms of_int_div_aux [of d n, where ?'a = 'a] by simp
-lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0,field})"
+lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::field_char_0)"
proof -
obtain a b where x: "x = (a, b)" by (cases x)
consider "a = 0 \<or> b = 0" | "a \<noteq> 0" "b \<noteq> 0" by blast
@@ -262,7 +262,7 @@
qed
qed
-lemma INum_normNum_iff: "(INum x ::'a::{field_char_0,field}) = INum y \<longleftrightarrow> normNum x = normNum y"
+lemma INum_normNum_iff: "(INum x ::'a::field_char_0) = INum y \<longleftrightarrow> normNum x = normNum y"
(is "?lhs \<longleftrightarrow> _")
proof -
have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
@@ -271,7 +271,7 @@
finally show ?thesis by simp
qed
-lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0,field})"
+lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: field_char_0)"
proof -
let ?z = "0::'a"
obtain a b where x: "x = (a, b)" by (cases x)
@@ -319,7 +319,7 @@
qed
qed
-lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a::{field_char_0,field})"
+lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a::field_char_0)"
proof -
let ?z = "0::'a"
obtain a b where x: "x = (a, b)" by (cases x)
@@ -346,13 +346,13 @@
lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x :: 'a::field)"
by (simp add: Nneg_def split_def INum_def)
-lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a::{field_char_0,field})"
+lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a::field_char_0)"
by (simp add: Nsub_def split_def)
lemma Ninv[simp]: "INum (Ninv x) = (1 :: 'a::field) / INum x"
by (simp add: Ninv_def INum_def split_def)
-lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y :: 'a::{field_char_0,field})"
+lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y :: 'a::field_char_0)"
by (simp add: Ndiv_def)
lemma Nlt0_iff[simp]:
@@ -463,7 +463,7 @@
qed
lemma Nadd_commute:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "x +\<^sub>N y = y +\<^sub>N x"
proof -
have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)"
@@ -475,7 +475,7 @@
qed
lemma [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "(0, b) +\<^sub>N y = normNum y"
and "(a, 0) +\<^sub>N y = normNum y"
and "x +\<^sub>N (0, b) = normNum x"
@@ -489,7 +489,7 @@
done
lemma normNum_nilpotent_aux[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
assumes nx: "isnormNum x"
shows "normNum x = x"
proof -
@@ -500,7 +500,7 @@
qed
lemma normNum_nilpotent[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "normNum (normNum x) = normNum x"
by simp
@@ -508,12 +508,12 @@
by (simp_all add: normNum_def)
lemma normNum_Nadd:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "normNum (x +\<^sub>N y) = x +\<^sub>N y"
by simp
lemma Nadd_normNum1[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "normNum x +\<^sub>N y = x +\<^sub>N y"
proof -
have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)"
@@ -527,7 +527,7 @@
qed
lemma Nadd_normNum2[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "x +\<^sub>N normNum y = x +\<^sub>N y"
proof -
have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)"
@@ -541,7 +541,7 @@
qed
lemma Nadd_assoc:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
proof -
have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))"
@@ -556,7 +556,7 @@
by (simp add: Nmul_def split_def Let_def gcd.commute mult.commute)
lemma Nmul_assoc:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
assumes nx: "isnormNum x"
and ny: "isnormNum y"
and nz: "isnormNum z"
@@ -571,7 +571,7 @@
qed
lemma Nsub0:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
assumes x: "isnormNum x"
and y: "isnormNum y"
shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
@@ -590,7 +590,7 @@
by (simp_all add: Nmul_def Let_def split_def)
lemma Nmul_eq0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
assumes nx: "isnormNum x"
and ny: "isnormNum y"
shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Jun 14 10:51:12 2018 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Jun 14 15:45:53 2018 +0200
@@ -234,7 +234,7 @@
subsection \<open>Semantics of the polynomial representation\<close>
-primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
+primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,power}"
where
"Ipoly bs (C c) = INum c"
| "Ipoly bs (Bound n) = bs!n"
@@ -245,7 +245,7 @@
| "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
| "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
-abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
+abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i"
@@ -462,7 +462,7 @@
qed simp_all
lemma polymul_properties:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
and m: "m \<le> min n0 n1"
@@ -646,23 +646,23 @@
by (induct p q rule: polymul.induct) (auto simp add: field_simps)
lemma polymul_normh:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
using polymul_properties(1) by blast
lemma polymul_eq0_iff:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
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"
using polymul_properties(2) by blast
lemma polymul_degreen:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
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)"
by (fact polymul_properties(3))
lemma polymul_norm:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)"
using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
@@ -675,7 +675,7 @@
lemma monic_eqI:
assumes np: "isnpolyh p n0"
shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
- (Ipoly bs p ::'a::{field_char_0,field, power})"
+ (Ipoly bs p ::'a::{field_char_0, power})"
unfolding monic_def Let_def
proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
let ?h = "headconst p"
@@ -726,13 +726,13 @@
using polyadd_norm polyneg_norm by (simp add: polysub_def)
lemma polysub_same_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p"
unfolding polysub_def split_def fst_conv snd_conv
by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def])
lemma polysub_0:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p -\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = q"
unfolding polysub_def split_def fst_conv snd_conv
by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
@@ -740,7 +740,7 @@
text \<open>polypow is a power function and preserves normal forms\<close>
-lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
+lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::field_char_0) ^ n"
proof (induct n rule: polypow.induct)
case 1
then show ?case by simp
@@ -777,7 +777,7 @@
qed
lemma polypow_normh:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
proof (induct k arbitrary: n rule: polypow.induct)
case 1
@@ -796,17 +796,17 @@
qed
lemma polypow_norm:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
by (simp add: polypow_normh isnpoly_def)
text \<open>Finally the whole normalization\<close>
-lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
+lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::field_char_0)"
by (induct p rule:polynate.induct) auto
lemma polynate_norm[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "isnpoly (polynate p)"
by (induct p rule: polynate.induct)
(simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
@@ -836,7 +836,7 @@
using assms by (induct k arbitrary: p) auto
lemma funpow_shift1:
- "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
+ "(Ipoly bs (funpow n shift1 p) :: 'a :: field_char_0) =
Ipoly bs (Mul (Pw (Bound 0) n) p)"
by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
@@ -844,7 +844,7 @@
using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
lemma funpow_shift1_1:
- "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
+ "(Ipoly bs (funpow n shift1 p) :: 'a :: field_char_0) =
Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
by (simp add: funpow_shift1)
@@ -854,7 +854,7 @@
lemma behead:
assumes "isnpolyh p n"
shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
- (Ipoly bs p :: 'a :: {field_char_0,field})"
+ (Ipoly bs p :: 'a :: field_char_0)"
using assms
proof (induct p arbitrary: n rule: behead.induct)
case (1 c p n)
@@ -1120,7 +1120,7 @@
lemma isnpolyh_zero_iff:
assumes nq: "isnpolyh p n0"
- and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field, power})"
+ and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, power})"
shows "p = 0\<^sub>p"
using nq eq
proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
@@ -1197,7 +1197,7 @@
lemma isnpolyh_unique:
assumes np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
- 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"
+ 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"
proof auto
assume "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)"
@@ -1212,7 +1212,7 @@
text \<open>Consequences of unicity on the algorithms for polynomial normalization.\<close>
lemma polyadd_commute:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
shows "p +\<^sub>p q = q +\<^sub>p p"
@@ -1226,7 +1226,7 @@
by simp
lemma polyadd_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
shows "p +\<^sub>p 0\<^sub>p = p"
and "0\<^sub>p +\<^sub>p p = p"
@@ -1234,7 +1234,7 @@
isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
lemma polymul_1[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
shows "p *\<^sub>p (1)\<^sub>p = p"
and "(1)\<^sub>p *\<^sub>p p = p"
@@ -1242,7 +1242,7 @@
isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
lemma polymul_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p"
and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
@@ -1250,27 +1250,27 @@
isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
lemma polymul_commute:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
shows "p *\<^sub>p q = q *\<^sub>p p"
using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np],
- where ?'a = "'a::{field_char_0,field, power}"]
+ where ?'a = "'a::{field_char_0, power}"]
by simp
declare polyneg_polyneg [simp]
lemma isnpolyh_polynate_id [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
shows "polynate p = p"
- using isnpolyh_unique[where ?'a= "'a::{field_char_0,field}",
+ using isnpolyh_unique[where ?'a= "'a::field_char_0",
OF polynate_norm[of p, unfolded isnpoly_def] np]
- polynate[where ?'a = "'a::{field_char_0,field}"]
+ polynate[where ?'a = "'a::field_char_0"]
by simp
lemma polynate_idempotent[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "polynate (polynate p) = polynate p"
using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
@@ -1278,7 +1278,7 @@
unfolding poly_nate_def polypoly'_def ..
lemma poly_nate_poly:
- "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
+ "poly (poly_nate bs p) = (\<lambda>x:: 'a ::field_char_0. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
unfolding poly_nate_polypoly' by auto
@@ -1317,7 +1317,7 @@
qed
lemma degree_polysub_samehead:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
and h: "head p = head q"
@@ -1478,7 +1478,7 @@
done
lemma polymul_head_polyeq:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
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"
proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
case (2 c c' n' p' n0 n1)
@@ -1575,7 +1575,7 @@
by (induct p arbitrary: n0 rule: polyneg.induct) auto
lemma degree_polymul:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
@@ -1591,7 +1591,7 @@
subsection \<open>Correctness of polynomial pseudo division\<close>
lemma polydivide_aux_properties:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
and ns: "isnpolyh s n1"
and ap: "head p = a"
@@ -1684,24 +1684,24 @@
polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0"
by simp
- from asp have "\<forall>bs :: 'a::{field_char_0,field} list.
+ from asp have "\<forall>bs :: 'a::field_char_0 list.
Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
by simp
- then have "\<forall>bs :: 'a::{field_char_0,field} list.
+ then have "\<forall>bs :: 'a::field_char_0 list.
Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
by (simp add: field_simps)
- then have "\<forall>bs :: 'a::{field_char_0,field} list.
+ then have "\<forall>bs :: 'a::field_char_0 list.
Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) +
Ipoly bs p * Ipoly bs q + Ipoly bs r"
by (auto simp only: funpow_shift1_1)
- then have "\<forall>bs:: 'a::{field_char_0,field} list.
+ then have "\<forall>bs:: 'a::field_char_0 list.
Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) +
Ipoly bs q) + Ipoly bs r"
by (simp add: field_simps)
- then have "\<forall>bs:: 'a::{field_char_0,field} list.
+ then have "\<forall>bs:: 'a::field_char_0 list.
Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
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)"
by simp
@@ -1720,10 +1720,10 @@
then show ?thesis by blast
next
case spz: 2
- from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"]
- have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'"
+ from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::field_char_0"]
+ have "\<forall>bs:: 'a::field_char_0 list. Ipoly bs s = Ipoly bs ?p'"
by simp
- with np nxdn have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
+ with np nxdn have "\<forall>bs:: 'a::field_char_0 list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
by (simp only: funpow_shift1_1) simp
then have sp': "s = ?xdn *\<^sub>p p"
using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
@@ -1801,7 +1801,7 @@
by arith
have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
- for bs :: "'a::{field_char_0,field} list"
+ for bs :: "'a::field_char_0 list"
proof -
from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
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)"
@@ -1815,7 +1815,7 @@
then show ?thesis
by (simp add: field_simps)
qed
- then have ieq: "\<forall>bs :: 'a::{field_char_0,field} list.
+ then have ieq: "\<forall>bs :: 'a::field_char_0 list.
Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
by auto
@@ -1837,10 +1837,10 @@
then show ?thesis by blast
next
case spz: 2
- have hth: "\<forall>bs :: 'a::{field_char_0,field} list.
+ have hth: "\<forall>bs :: 'a::field_char_0 list.
Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
proof
- fix bs :: "'a::{field_char_0,field} list"
+ fix bs :: "'a::field_char_0 list"
from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'"
by simp
@@ -1850,7 +1850,7 @@
by simp
qed
from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
- using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
+ using isnpolyh_unique[where ?'a = "'a::field_char_0", OF polymul_normh[OF head_isnpolyh[OF np] ns]
polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
simplified ap]
by simp
@@ -1876,7 +1876,7 @@
qed
lemma polydivide_properties:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
and np: "isnpolyh p n0"
and ns: "isnpolyh s n1"
and pnz: "p \<noteq> 0\<^sub>p"
@@ -2041,12 +2041,12 @@
lemma swapnorm:
assumes nbs: "n < length bs"
and mbs: "m < length bs"
- shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field})) =
+ shows "((Ipoly bs (swapnorm n m t) :: 'a::field_char_0)) =
Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
using swap[OF assms] swapnorm_def by simp
lemma swapnorm_isnpoly [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+ assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "isnpoly (swapnorm n m p)"
unfolding swapnorm_def by simp