--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Mar 31 21:54:32 2015 +0200
@@ -235,7 +235,7 @@
subsection{* Semantics of the polynomial representation *}
-primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field_inverse_zero,power}"
+primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
where
"Ipoly bs (C c) = INum c"
| "Ipoly bs (Bound n) = bs!n"
@@ -246,7 +246,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_inverse_zero,power}"
+abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"
("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
@@ -481,7 +481,7 @@
qed simp_all
lemma polymul_properties:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
and m: "m \<le> min n0 n1"
@@ -670,23 +670,23 @@
by (induct p q rule: polymul.induct) (auto simp add: field_simps)
lemma polymul_normh:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)"
using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
@@ -699,7 +699,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_inverse_zero, power})"
+ (Ipoly bs p ::'a::{field_char_0,field, power})"
unfolding monic_def Let_def
proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
let ?h = "headconst p"
@@ -750,13 +750,13 @@
using polyadd_norm polyneg_norm by (simp add: polysub_def)
lemma polysub_same_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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)
@@ -765,7 +765,7 @@
text{* polypow is a power function and preserves normal forms *}
lemma polypow[simp]:
- "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n"
+ "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
proof (induct n rule: polypow.induct)
case 1
then show ?case
@@ -806,7 +806,7 @@
qed
lemma polypow_normh:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
proof (induct k arbitrary: n rule: polypow.induct)
case 1
@@ -826,18 +826,18 @@
qed
lemma polypow_norm:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
by (simp add: polypow_normh isnpoly_def)
text{* Finally the whole normalization *}
lemma polynate [simp]:
- "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field_inverse_zero})"
+ "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
by (induct p rule:polynate.induct) auto
lemma polynate_norm[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpoly (polynate p)"
by (induct p rule: polynate.induct)
(simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
@@ -868,7 +868,7 @@
using assms by (induct k arbitrary: p) auto
lemma funpow_shift1:
- "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
+ "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
Ipoly bs (Mul (Pw (Bound 0) n) p)"
by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
@@ -876,7 +876,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_inverse_zero}) =
+ "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
by (simp add: funpow_shift1)
@@ -886,7 +886,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_inverse_zero})"
+ (Ipoly bs p :: 'a :: {field_char_0,field})"
using assms
proof (induct p arbitrary: n rule: behead.induct)
case (1 c p n)
@@ -1160,7 +1160,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_inverse_zero, power})"
+ and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field, power})"
shows "p = 0\<^sub>p"
using nq eq
proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
@@ -1242,7 +1242,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_inverse_zero,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,field,power})) \<longleftrightarrow> p = q"
proof auto
assume H: "\<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)"
@@ -1257,7 +1257,7 @@
text{* consequences of unicity on the algorithms for polynomial normalization *}
lemma polyadd_commute:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
shows "p +\<^sub>p q = q +\<^sub>p p"
@@ -1271,7 +1271,7 @@
by simp
lemma polyadd_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
shows "p +\<^sub>p 0\<^sub>p = p"
and "0\<^sub>p +\<^sub>p p = p"
@@ -1279,7 +1279,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_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
shows "p *\<^sub>p (1)\<^sub>p = p"
and "(1)\<^sub>p *\<^sub>p p = p"
@@ -1287,7 +1287,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_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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"
@@ -1295,27 +1295,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_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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_inverse_zero, power}"]
+ where ?'a = "'a::{field_char_0,field, power}"]
by simp
declare polyneg_polyneg [simp]
lemma isnpolyh_polynate_id [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
shows "polynate p = p"
- using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}",
+ using isnpolyh_unique[where ?'a= "'a::{field_char_0,field}",
OF polynate_norm[of p, unfolded isnpoly_def] np]
- polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"]
+ polynate[where ?'a = "'a::{field_char_0,field}"]
by simp
lemma polynate_idempotent[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "polynate (polynate p) = polynate p"
using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
@@ -1323,7 +1323,7 @@
unfolding poly_nate_def polypoly'_def ..
lemma poly_nate_poly:
- "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
+ "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field}. \<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
@@ -1362,7 +1362,7 @@
qed
lemma degree_polysub_samehead:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
and h: "head p = head q"
@@ -1531,7 +1531,7 @@
done
lemma polymul_head_polyeq:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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)
@@ -1634,7 +1634,7 @@
by (induct p arbitrary: n0 rule: polyneg.induct) auto
lemma degree_polymul:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
@@ -1650,7 +1650,7 @@
subsection {* Correctness of polynomial pseudo division *}
lemma polydivide_aux_properties:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and ns: "isnpolyh s n1"
and ap: "head p = a"
@@ -1745,24 +1745,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_inverse_zero} list.
+ from asp have "\<forall>bs :: 'a::{field_char_0,field} 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_inverse_zero} list.
+ then have "\<forall>bs :: 'a::{field_char_0,field} 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_inverse_zero} list.
+ then have "\<forall>bs :: 'a::{field_char_0,field} 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_inverse_zero} list.
+ then have "\<forall>bs:: 'a::{field_char_0,field} 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_inverse_zero} list.
+ then have "\<forall>bs:: 'a::{field_char_0,field} 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
@@ -1784,10 +1784,10 @@
moreover
{
assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
- from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field_inverse_zero}"]
- have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} 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,field}"]
+ have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'"
by simp
- then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
+ then have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
using np nxdn
apply simp
apply (simp only: funpow_shift1_1)
@@ -1861,7 +1861,7 @@
from kk' have kk'': "Suc (k' - Suc k) = k' - k"
by arith
{
- fix bs :: "'a::{field_char_0,field_inverse_zero} list"
+ fix bs :: "'a::{field_char_0,field} list"
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)"
by simp
@@ -1875,7 +1875,7 @@
Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
by (simp add: field_simps)
}
- then have ieq:"\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have ieq:"\<forall>bs :: 'a::{field_char_0,field} 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
@@ -1900,7 +1900,7 @@
{
assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
{
- fix bs :: "'a::{field_char_0,field_inverse_zero} list"
+ fix bs :: "'a::{field_char_0,field} 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
@@ -1909,10 +1909,10 @@
then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
by simp
}
- then have hth: "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have hth: "\<forall>bs :: 'a::{field_char_0,field} list.
Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
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_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
+ using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", 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
@@ -1945,7 +1945,7 @@
qed
lemma polydivide_properties:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and ns: "isnpolyh s n1"
and pnz: "p \<noteq> 0\<^sub>p"
@@ -2112,12 +2112,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_inverse_zero})) =
+ shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field})) =
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_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpoly (swapnorm n m p)"
unfolding swapnorm_def by simp