--- 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