17 |
17 |
18 abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)" |
18 abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)" |
19 abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)" |
19 abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)" |
20 |
20 |
21 subsection{* Boundedness, substitution and all that *} |
21 subsection{* Boundedness, substitution and all that *} |
22 consts polysize:: "poly \<Rightarrow> nat" |
22 primrec polysize:: "poly \<Rightarrow> nat" where |
23 primrec |
|
24 "polysize (C c) = 1" |
23 "polysize (C c) = 1" |
25 "polysize (Bound n) = 1" |
24 | "polysize (Bound n) = 1" |
26 "polysize (Neg p) = 1 + polysize p" |
25 | "polysize (Neg p) = 1 + polysize p" |
27 "polysize (Add p q) = 1 + polysize p + polysize q" |
26 | "polysize (Add p q) = 1 + polysize p + polysize q" |
28 "polysize (Sub p q) = 1 + polysize p + polysize q" |
27 | "polysize (Sub p q) = 1 + polysize p + polysize q" |
29 "polysize (Mul p q) = 1 + polysize p + polysize q" |
28 | "polysize (Mul p q) = 1 + polysize p + polysize q" |
30 "polysize (Pw p n) = 1 + polysize p" |
29 | "polysize (Pw p n) = 1 + polysize p" |
31 "polysize (CN c n p) = 4 + polysize c + polysize p" |
30 | "polysize (CN c n p) = 4 + polysize c + polysize p" |
32 |
31 |
33 consts |
32 primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where |
34 polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) |
|
35 polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) |
|
36 primrec |
|
37 "polybound0 (C c) = True" |
33 "polybound0 (C c) = True" |
38 "polybound0 (Bound n) = (n>0)" |
34 | "polybound0 (Bound n) = (n>0)" |
39 "polybound0 (Neg a) = polybound0 a" |
35 | "polybound0 (Neg a) = polybound0 a" |
40 "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)" |
36 | "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)" |
41 "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" |
37 | "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" |
42 "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)" |
38 | "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)" |
43 "polybound0 (Pw p n) = (polybound0 p)" |
39 | "polybound0 (Pw p n) = (polybound0 p)" |
44 "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)" |
40 | "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)" |
45 primrec |
41 |
|
42 primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) where |
46 "polysubst0 t (C c) = (C c)" |
43 "polysubst0 t (C c) = (C c)" |
47 "polysubst0 t (Bound n) = (if n=0 then t else Bound n)" |
44 | "polysubst0 t (Bound n) = (if n=0 then t else Bound n)" |
48 "polysubst0 t (Neg a) = Neg (polysubst0 t a)" |
45 | "polysubst0 t (Neg a) = Neg (polysubst0 t a)" |
49 "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)" |
46 | "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)" |
50 "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" |
47 | "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" |
51 "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)" |
48 | "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)" |
52 "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n" |
49 | "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n" |
53 "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p)) |
50 | "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p)) |
54 else CN (polysubst0 t c) n (polysubst0 t p))" |
51 else CN (polysubst0 t c) n (polysubst0 t p))" |
55 |
52 |
56 consts |
53 consts |
57 decrpoly:: "poly \<Rightarrow> poly" |
54 decrpoly:: "poly \<Rightarrow> poly" |
58 recdef decrpoly "measure polysize" |
55 recdef decrpoly "measure polysize" |
193 |
190 |
194 subsection{* Pseudo-division *} |
191 subsection{* Pseudo-division *} |
195 |
192 |
196 definition shift1 :: "poly \<Rightarrow> poly" where |
193 definition shift1 :: "poly \<Rightarrow> poly" where |
197 "shift1 p \<equiv> CN 0\<^sub>p 0 p" |
194 "shift1 p \<equiv> CN 0\<^sub>p 0 p" |
198 consts funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" |
195 |
199 |
196 abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where |
200 primrec |
197 "funpow \<equiv> compow" |
201 "funpow 0 f x = x" |
198 |
202 "funpow (Suc n) f x = funpow n f (f x)" |
|
203 function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)" |
199 function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)" |
204 where |
200 where |
205 "polydivide_aux (a,n,p,k,s) = |
201 "polydivide_aux (a,n,p,k,s) = |
206 (if s = 0\<^sub>p then (k,s) |
202 (if s = 0\<^sub>p then (k,s) |
207 else (let b = head s; m = degree s in |
203 else (let b = head s; m = degree s in |
209 (let p'= funpow (m - n) shift1 p in |
205 (let p'= funpow (m - n) shift1 p in |
210 (if a = b then polydivide_aux (a,n,p,k,s -\<^sub>p p') |
206 (if a = b then polydivide_aux (a,n,p,k,s -\<^sub>p p') |
211 else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))" |
207 else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))" |
212 by pat_completeness auto |
208 by pat_completeness auto |
213 |
209 |
214 |
|
215 definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where |
210 definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where |
216 "polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)" |
211 "polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)" |
217 |
212 |
218 fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where |
213 fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where |
219 "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)" |
214 "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)" |
228 using Nat.gr0_conv_Suc |
223 using Nat.gr0_conv_Suc |
229 by clarsimp |
224 by clarsimp |
230 |
225 |
231 subsection{* Semantics of the polynomial representation *} |
226 subsection{* Semantics of the polynomial representation *} |
232 |
227 |
233 consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" |
228 primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where |
234 primrec |
|
235 "Ipoly bs (C c) = INum c" |
229 "Ipoly bs (C c) = INum c" |
236 "Ipoly bs (Bound n) = bs!n" |
230 | "Ipoly bs (Bound n) = bs!n" |
237 "Ipoly bs (Neg a) = - Ipoly bs a" |
231 | "Ipoly bs (Neg a) = - Ipoly bs a" |
238 "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b" |
232 | "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b" |
239 "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b" |
233 | "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b" |
240 "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b" |
234 | "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b" |
241 "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n" |
235 | "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n" |
242 "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)" |
236 | "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)" |
|
237 |
243 abbreviation |
238 abbreviation |
244 Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>") |
239 Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>") |
245 where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p" |
240 where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p" |
246 |
241 |
247 lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" |
242 lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" |
727 |
722 |
728 lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p" |
723 lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p" |
729 by (simp add: shift1_def) |
724 by (simp add: shift1_def) |
730 lemma funpow_shift1_isnpoly: |
725 lemma funpow_shift1_isnpoly: |
731 "\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)" |
726 "\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)" |
732 by (induct n arbitrary: p, auto simp add: shift1_isnpoly) |
727 by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1) |
733 |
728 |
734 lemma funpow_isnpolyh: |
729 lemma funpow_isnpolyh: |
735 assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n" |
730 assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n" |
736 shows "isnpolyh (funpow k f p) n" |
731 shows "isnpolyh (funpow k f p) n" |
737 using f np by (induct k arbitrary: p, auto) |
732 using f np by (induct k arbitrary: p, auto) |
765 assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n" |
760 assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n" |
766 using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono) |
761 using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono) |
767 |
762 |
768 subsection{* Miscilanious lemmas about indexes, decrementation, substitution etc ... *} |
763 subsection{* Miscilanious lemmas about indexes, decrementation, substitution etc ... *} |
769 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p" |
764 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p" |
770 proof(induct p arbitrary: n rule: polybound0.induct, auto) |
765 proof(induct p arbitrary: n rule: poly.induct, auto) |
771 case (goal1 c n p n') |
766 case (goal1 c n p n') |
772 hence "n = Suc (n - 1)" by simp |
767 hence "n = Suc (n - 1)" by simp |
773 hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp |
768 hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp |
774 with prems(2) show ?case by simp |
769 with prems(2) show ?case by simp |
775 qed |
770 qed |
807 shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)" |
802 shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)" |
808 using nb by (induct t rule: decrpoly.induct, simp_all) |
803 using nb by (induct t rule: decrpoly.induct, simp_all) |
809 |
804 |
810 lemma polysubst0_polybound0: assumes nb: "polybound0 t" |
805 lemma polysubst0_polybound0: assumes nb: "polybound0 t" |
811 shows "polybound0 (polysubst0 t a)" |
806 shows "polybound0 (polysubst0 t a)" |
812 using nb by (induct a rule: polysubst0.induct, auto) |
807 using nb by (induct a rule: poly.induct, auto) |
813 |
808 |
814 lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p" |
809 lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p" |
815 by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0) |
810 by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0) |
816 |
811 |
817 fun maxindex :: "poly \<Rightarrow> nat" where |
812 primrec maxindex :: "poly \<Rightarrow> nat" where |
818 "maxindex (Bound n) = n + 1" |
813 "maxindex (Bound n) = n + 1" |
819 | "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" |
814 | "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" |
820 | "maxindex (Add p q) = max (maxindex p) (maxindex q)" |
815 | "maxindex (Add p q) = max (maxindex p) (maxindex q)" |
821 | "maxindex (Sub p q) = max (maxindex p) (maxindex q)" |
816 | "maxindex (Sub p q) = max (maxindex p) (maxindex q)" |
822 | "maxindex (Mul p q) = max (maxindex p) (maxindex q)" |
817 | "maxindex (Mul p q) = max (maxindex p) (maxindex q)" |
1181 lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p" |
1176 lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p" |
1182 proof(induct k arbitrary: n0 p) |
1177 proof(induct k arbitrary: n0 p) |
1183 case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) |
1178 case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) |
1184 with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" |
1179 with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" |
1185 and "head (shift1 p) = head p" by (simp_all add: shift1_head) |
1180 and "head (shift1 p) = head p" by (simp_all add: shift1_head) |
1186 thus ?case by simp |
1181 thus ?case by (simp add: funpow_swap1) |
1187 qed auto |
1182 qed auto |
1188 |
1183 |
1189 lemma shift1_degree: "degree (shift1 p) = 1 + degree p" |
1184 lemma shift1_degree: "degree (shift1 p) = 1 + degree p" |
1190 by (simp add: shift1_def) |
1185 by (simp add: shift1_def) |
1191 lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p " |
1186 lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p " |
1639 thus "nonconstant ?p" using pn unfolding nonconstant_def by blast |
1634 thus "nonconstant ?p" using pn unfolding nonconstant_def by blast |
1640 qed |
1635 qed |
1641 |
1636 |
1642 lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p" |
1637 lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p" |
1643 unfolding pnormal_def |
1638 unfolding pnormal_def |
1644 apply (induct p rule: pnormalize.induct, simp_all) |
1639 apply (induct p) |
1645 apply (case_tac "p=[]", simp_all) |
1640 apply (simp_all, case_tac "p=[]", simp_all) |
1646 done |
1641 done |
1647 |
1642 |
1648 lemma degree_degree: assumes inc: "isnonconstant p" |
1643 lemma degree_degree: assumes inc: "isnonconstant p" |
1649 shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
1644 shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
1650 proof |
1645 proof |
1666 show "degree p = Polynomial_List.degree ?p" |
1661 show "degree p = Polynomial_List.degree ?p" |
1667 unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto |
1662 unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto |
1668 qed |
1663 qed |
1669 |
1664 |
1670 section{* Swaps ; Division by a certain variable *} |
1665 section{* Swaps ; Division by a certain variable *} |
1671 consts swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" |
1666 primrec swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where |
1672 primrec |
|
1673 "swap n m (C x) = C x" |
1667 "swap n m (C x) = C x" |
1674 "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)" |
1668 | "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)" |
1675 "swap n m (Neg t) = Neg (swap n m t)" |
1669 | "swap n m (Neg t) = Neg (swap n m t)" |
1676 "swap n m (Add s t) = Add (swap n m s) (swap n m t)" |
1670 | "swap n m (Add s t) = Add (swap n m s) (swap n m t)" |
1677 "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)" |
1671 | "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)" |
1678 "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)" |
1672 | "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)" |
1679 "swap n m (Pw t k) = Pw (swap n m t) k" |
1673 | "swap n m (Pw t k) = Pw (swap n m t) k" |
1680 "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k) |
1674 | "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k) |
1681 (swap n m p)" |
1675 (swap n m p)" |
1682 |
1676 |
1683 lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs" |
1677 lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs" |
1684 shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" |
1678 shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" |
1685 proof (induct t) |
1679 proof (induct t) |