src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 author krauss Sat Dec 25 22:18:55 2010 +0100 (2010-12-25) changeset 41403 7eba049f7310 parent 39246 9e58f0499f57 child 41404 aae9f912cca8 permissions -rw-r--r--
partial_function (tailrec) replaces function (tailrec);
dropped unnecessary domain reasoning;
curried polydivide_aux
1 (*  Title:      HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
2     Author:     Amine Chaieb
3 *)
5 header {* Implementation and verification of multivariate polynomials *}
7 theory Reflected_Multivariate_Polynomial
8 imports Complex_Main Abstract_Rat Polynomial_List
9 begin
11   (* Implementation *)
13 subsection{* Datatype of polynomial expressions *}
15 datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
16   | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
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)"
21 subsection{* Boundedness, substitution and all that *}
22 primrec polysize:: "poly \<Rightarrow> nat" where
23   "polysize (C c) = 1"
24 | "polysize (Bound n) = 1"
25 | "polysize (Neg p) = 1 + polysize p"
26 | "polysize (Add p q) = 1 + polysize p + polysize q"
27 | "polysize (Sub p q) = 1 + polysize p + polysize q"
28 | "polysize (Mul p q) = 1 + polysize p + polysize q"
29 | "polysize (Pw p n) = 1 + polysize p"
30 | "polysize (CN c n p) = 4 + polysize c + polysize p"
32 primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where
33   "polybound0 (C c) = True"
34 | "polybound0 (Bound n) = (n>0)"
35 | "polybound0 (Neg a) = polybound0 a"
36 | "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
37 | "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)"
38 | "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
39 | "polybound0 (Pw p n) = (polybound0 p)"
40 | "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
42 primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) where
43   "polysubst0 t (C c) = (C c)"
44 | "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
45 | "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
46 | "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
47 | "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"
48 | "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
49 | "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
50 | "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
51                              else CN (polysubst0 t c) n (polysubst0 t p))"
53 consts
54   decrpoly:: "poly \<Rightarrow> poly"
55 recdef decrpoly "measure polysize"
56   "decrpoly (Bound n) = Bound (n - 1)"
57   "decrpoly (Neg a) = Neg (decrpoly a)"
59   "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"
60   "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"
61   "decrpoly (Pw p n) = Pw (decrpoly p) n"
62   "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
63   "decrpoly a = a"
65 subsection{* Degrees and heads and coefficients *}
67 consts degree:: "poly \<Rightarrow> nat"
68 recdef degree "measure size"
69   "degree (CN c 0 p) = 1 + degree p"
70   "degree p = 0"
71 consts head:: "poly \<Rightarrow> poly"
76   (* More general notions of degree and head *)
77 consts degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"
78 recdef degreen "measure size"
79   "degreen (CN c n p) = (\<lambda>m. if n=m then 1 + degreen p n else 0)"
80   "degreen p = (\<lambda>m. 0)"
82 consts headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
84   "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
85   "headn p = (\<lambda>m. p)"
87 consts coefficients:: "poly \<Rightarrow> poly list"
88 recdef coefficients "measure size"
89   "coefficients (CN c 0 p) = c#(coefficients p)"
90   "coefficients p = [p]"
92 consts isconstant:: "poly \<Rightarrow> bool"
93 recdef isconstant "measure size"
94   "isconstant (CN c 0 p) = False"
95   "isconstant p = True"
97 consts behead:: "poly \<Rightarrow> poly"
99   "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
102 consts headconst:: "poly \<Rightarrow> Num"
105   "headconst (C n) = n"
107 subsection{* Operations for normalization *}
108 consts
109   polyadd :: "poly\<times>poly \<Rightarrow> poly"
110   polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
111   polysub :: "poly\<times>poly \<Rightarrow> poly"
112   polymul :: "poly\<times>poly \<Rightarrow> poly"
113   polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
114 abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
115   where "a +\<^sub>p b \<equiv> polyadd (a,b)"
116 abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
117   where "a *\<^sub>p b \<equiv> polymul (a,b)"
118 abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
119   where "a -\<^sub>p b \<equiv> polysub (a,b)"
120 abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
121   where "a ^\<^sub>p k \<equiv> polypow k a"
123 recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
124   "polyadd (C c, C c') = C (c+\<^sub>Nc')"
125   "polyadd (C c, CN c' n' p') = CN (polyadd (C c, c')) n' p'"
126   "polyadd (CN c n p, C c') = CN (polyadd (c, C c')) n p"
127 stupid:  "polyadd (CN c n p, CN c' n' p') =
128     (if n < n' then CN (polyadd(c,CN c' n' p')) n p
129      else if n'<n then CN (polyadd(CN c n p, c')) n' p'
130      else (let cc' = polyadd (c,c') ;
132            in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
134 (hints recdef_simp add: Let_def measure_def split_def inv_image_def)
136 (*
137 declare stupid [simp del, code del]
139 lemma [simp,code]: "polyadd (CN c n p, CN c' n' p') =
140     (if n < n' then CN (polyadd(c,CN c' n' p')) n p
141      else if n'<n then CN (polyadd(CN c n p, c')) n' p'
142      else (let cc' = polyadd (c,c') ;
144            in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
145   by (simp add: Let_def stupid)
146 *)
148 recdef polyneg "measure size"
149   "polyneg (C c) = C (~\<^sub>N c)"
150   "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
151   "polyneg a = Neg a"
153 defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd (p,polyneg q)"
155 recdef polymul "measure (\<lambda>(a,b). size a + size b)"
156   "polymul(C c, C c') = C (c*\<^sub>Nc')"
157   "polymul(C c, CN c' n' p') =
158       (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul(C c,c')) n' (polymul(C c, p')))"
159   "polymul(CN c n p, C c') =
160       (if c' = 0\<^sub>N  then 0\<^sub>p else CN (polymul(c,C c')) n (polymul(p, C c')))"
161   "polymul(CN c n p, CN c' n' p') =
162   (if n<n' then CN (polymul(c,CN c' n' p')) n (polymul(p,CN c' n' p'))
163   else if n' < n
164   then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p'))
165   else polyadd(polymul(CN c n p, c'),CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
166   "polymul (a,b) = Mul a b"
167 recdef polypow "measure id"
168   "polypow 0 = (\<lambda>p. 1\<^sub>p)"
169   "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul(q,q) in
170                     if even n then d else polymul(p,d))"
172 consts polynate :: "poly \<Rightarrow> poly"
173 recdef polynate "measure polysize"
174   "polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p"
175   "polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
176   "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
177   "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
178   "polynate (Neg p) = (~\<^sub>p (polynate p))"
179   "polynate (Pw p n) = ((polynate p) ^\<^sub>p n)"
180   "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
181   "polynate (C c) = C (normNum c)"
183 fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" where
184   "poly_cmul y (C x) = C (y *\<^sub>N x)"
185 | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
186 | "poly_cmul y p = C y *\<^sub>p p"
188 definition monic :: "poly \<Rightarrow> (poly \<times> bool)" where
189   "monic p \<equiv> (let h = headconst p in if h = 0\<^sub>N then (p,False) else ((C (Ninv h)) *\<^sub>p p, 0>\<^sub>N h))"
191 subsection{* Pseudo-division *}
193 definition shift1 :: "poly \<Rightarrow> poly" where
194   "shift1 p \<equiv> CN 0\<^sub>p 0 p"
196 abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
197   "funpow \<equiv> compow"
199 partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
200   where
201   "polydivide_aux a n p k s =
202   (if s = 0\<^sub>p then (k,s)
203   else (let b = head s; m = degree s in
204   (if m < n then (k,s) else
205   (let p'= funpow (m - n) shift1 p in
206   (if a = b then polydivide_aux a n p k (s -\<^sub>p p')
207   else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
209 definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
210   "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
212 fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where
213   "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 p = poly_cmul ((int n)\<^sub>N) p"
216 fun poly_deriv :: "poly \<Rightarrow> poly" where
217   "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
218 | "poly_deriv p = 0\<^sub>p"
220   (* Verification *)
221 lemma nth_pos2[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
222 using Nat.gr0_conv_Suc
223 by clarsimp
225 subsection{* Semantics of the polynomial representation *}
227 primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
228   "Ipoly bs (C c) = INum c"
229 | "Ipoly bs (Bound n) = bs!n"
230 | "Ipoly bs (Neg a) = - Ipoly bs a"
231 | "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
232 | "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
233 | "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
234 | "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
235 | "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
237 abbreviation
238   Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
239   where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
241 lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i"
243 lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j"
246 lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat
248 subsection {* Normal form and normalization *}
250 consts isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
251 recdef isnpolyh "measure size"
252   "isnpolyh (C c) = (\<lambda>k. isnormNum c)"
253   "isnpolyh (CN c n p) = (\<lambda>k. n\<ge> k \<and> (isnpolyh c (Suc n)) \<and> (isnpolyh p n) \<and> (p \<noteq> 0\<^sub>p))"
254   "isnpolyh p = (\<lambda>k. False)"
256 lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"
257 by (induct p rule: isnpolyh.induct, auto)
259 definition isnpoly :: "poly \<Rightarrow> bool" where
260   "isnpoly p \<equiv> isnpolyh p 0"
262 text{* polyadd preserves normal forms *}
264 lemma polyadd_normh: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk>
265       \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)"
266 proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)
267   case (2 a b c' n' p' n0 n1)
268   from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp
269   from prems(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
270   with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
271   with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
272   from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp
273   thus ?case using prems th3 by simp
274 next
275   case (3 c' n' p' a b n1 n0)
276   from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp
277   from prems(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
278   with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
279   with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
280   from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp
281   thus ?case using prems th3 by simp
282 next
283   case (4 c n p c' n' p' n0 n1)
284   hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all
285   from prems have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all
286   from prems have ngen0: "n \<ge> n0" by simp
287   from prems have n'gen1: "n' \<ge> n1" by simp
288   have "n < n' \<or> n' < n \<or> n = n'" by auto
289   moreover {assume eq: "n = n'" hence eq': "\<not> n' < n \<and> \<not> n < n'" by simp
290     with prems(2)[rule_format, OF eq' nc nc']
291     have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
292     hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
293       using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
294     from eq prems(1)[rule_format, OF eq' np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
295     have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
296     from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
297   moreover {assume lt: "n < n'"
298     have "min n0 n1 \<le> n0" by simp
299     with prems have th1:"min n0 n1 \<le> n" by auto
300     from prems have th21: "isnpolyh c (Suc n)" by simp
301     from prems have th22: "isnpolyh (CN c' n' p') n'" by simp
302     from lt have th23: "min (Suc n) n' = Suc n" by arith
303     from prems(4)[rule_format, OF lt th21 th22]
304     have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
305     with prems th1 have ?case by simp }
306   moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
307     have "min n0 n1 \<le> n1"  by simp
308     with prems have th1:"min n0 n1 \<le> n'" by auto
309     from prems have th21: "isnpolyh c' (Suc n')" by simp_all
310     from prems have th22: "isnpolyh (CN c n p) n" by simp
311     from gt have th23: "min n (Suc n') = Suc n'" by arith
312     from prems(3)[rule_format, OF  gt' th22 th21]
313     have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
314     with prems th1 have ?case by simp}
315       ultimately show ?case by blast
316 qed auto
318 lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)"
319 by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
321 lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"
322   using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
324 text{* The degree of addition and other general lemmas needed for the normal form of polymul*}
327   "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow>
328   degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)"
329 proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
330   case (4 c n p c' n' p' m n0 n1)
331   thus ?case
332     apply (cases "n' < n", simp_all add: Let_def)
333     apply (cases "n = n'", simp_all)
334     apply (cases "n' = m", simp_all add: Let_def)
335     by (erule allE[where x="m"], erule allE[where x="Suc m"],
336            erule allE[where x="m"], erule allE[where x="Suc m"],
337            clarsimp,erule allE[where x="m"],erule allE[where x="Suc m"], simp)
338 qed simp_all
340 lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"
341   by (induct p arbitrary: n rule: headn.induct, auto)
342 lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0"
343   by (induct p arbitrary: n rule: degree.induct, auto)
344 lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0"
345   by (induct p arbitrary: n rule: degreen.induct, auto)
347 lemma degree_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> degree p = 0"
348   by (induct p arbitrary: n rule: degree.induct, auto)
350 lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0"
351   using degree_isnpolyh_Suc by auto
352 lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degreen c n = 0"
353   using degreen_0 by auto
357   assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> max n0 n1"
358   shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)"
359   using np nq m
360 proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)
361   case (2 c c' n' p' n0 n1) thus ?case  by (cases n', simp_all)
362 next
363   case (3 c n p c' n0 n1) thus ?case by (cases n, auto)
364 next
365   case (4 c n p c' n' p' n0 n1 m)
366   thus ?case
367     apply (cases "n < n'", simp_all add: Let_def)
368     apply (cases "n' < n", simp_all)
369     apply (erule allE[where x="n"],erule allE[where x="Suc n"],clarify)
370     apply (erule allE[where x="n'"],erule allE[where x="Suc n'"],clarify)
371     by (erule allE[where x="m"],erule allE[where x="m"], auto)
372 qed auto
375 lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk>
376   \<Longrightarrow> degreen p m = degreen q m"
377 proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
378   case (4 c n p c' n' p' m n0 n1 x)
379   hence z: "CN c n p +\<^sub>p CN c' n' p' = C x" by simp
380   {assume nn': "n' < n" hence ?case using prems by simp}
381   moreover
382   {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
383     moreover {assume "n < n'" with prems have ?case by simp }
384     moreover {assume eq: "n = n'" hence ?case using prems
385         by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
386     ultimately have ?case by blast}
387   ultimately show ?case by blast
388 qed simp_all
390 lemma polymul_properties:
391   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
392   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
393   shows "isnpolyh (p *\<^sub>p q) (min n0 n1)"
394   and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)"
395   and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0
396                              else degreen p m + degreen q m)"
397   using np nq m
398 proof(induct p q arbitrary: n0 n1 m rule: polymul.induct)
399   case (2 a b c' n' p')
400   let ?c = "(a,b)"
401   { case (1 n0 n1)
402     hence n: "isnpolyh (C ?c) n'" "isnpolyh c' (Suc n')" "isnpolyh p' n'" "isnormNum ?c"
403       "isnpolyh (CN c' n' p') n1"
404       by simp_all
405     {assume "?c = 0\<^sub>N" hence ?case by auto}
406       moreover {assume cnz: "?c \<noteq> 0\<^sub>N"
407         from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)]
408           "2.hyps"(2)[rule_format, where x="Suc n'"
409           and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
410           by (auto simp add: min_def)}
411       ultimately show ?case by blast
412   next
413     case (2 n0 n1) thus ?case by auto
414   next
415     case (3 n0 n1) thus ?case  using "2.hyps" by auto }
416 next
417   case (3 c n p a b){
418     let ?c' = "(a,b)"
419     case (1 n0 n1)
420     hence n: "isnpolyh (C ?c') n" "isnpolyh c (Suc n)" "isnpolyh p n" "isnormNum ?c'"
421       "isnpolyh (CN c n p) n0"
422       by simp_all
423     {assume "?c' = 0\<^sub>N" hence ?case by auto}
424       moreover {assume cnz: "?c' \<noteq> 0\<^sub>N"
425         from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)]
426           "3.hyps"(2)[rule_format, where x="Suc n"
427           and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
428           by (auto simp add: min_def)}
429       ultimately show ?case by blast
430   next
431     case (2 n0 n1) thus ?case apply auto done
432   next
433     case (3 n0 n1) thus ?case  using "3.hyps" by auto }
434 next
435   case (4 c n p c' n' p')
436   let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'"
437     {fix n0 n1
438       assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"
439       hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
440         and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)"
441         and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
442         and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
443         by simp_all
444       have "n < n' \<or> n' < n \<or> n' = n" by auto
445       moreover
446       {assume nn': "n < n'"
447         with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"]
448           "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
449         have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
450           by (simp add: min_def) }
451       moreover
453       {assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith
454         with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
455           "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"]
456           nn' nn0 nn1 cnp'
457         have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
458           by (cases "Suc n' = n", simp_all add: min_def)}
459       moreover
460       {assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith
461         from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
462           "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
464         have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
466       ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }
467     note th = this
468     {fix n0 n1 m
469       assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1"
470       and m: "m \<le> min n0 n1"
471       let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"
472       let ?d1 = "degreen ?cnp m"
473       let ?d2 = "degreen ?cnp' m"
474       let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0  else ?d1 + ?d2)"
475       have "n'<n \<or> n < n' \<or> n' = n" by auto
476       moreover
477       {assume "n' < n \<or> n < n'"
478         with "4.hyps" np np' m
479         have ?eq apply (cases "n' < n", simp_all)
480         apply (erule allE[where x="n"],erule allE[where x="n"],auto)
481         done }
482       moreover
483       {assume nn': "n' = n"  hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
484         from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
485           "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"]
486           np np' nn'
487         have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
488           "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
489           "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
490           "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
491         {assume mn: "m = n"
492           from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
493             "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
494           have degs:  "degreen (?cnp *\<^sub>p c') n =
495             (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
496             "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
497           from degs norm
498           have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
499           hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
500             by simp
501           have nmin: "n \<le> min n n" by (simp add: min_def)
502           from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
503           have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
504           from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
505             "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
506             mn norm m nn' deg
507           have ?eq by simp}
508         moreover
509         {assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
510           from nn' m np have max1: "m \<le> max n n"  by simp
511           hence min1: "m \<le> min n n" by simp
512           hence min2: "m \<le> min n (Suc n)" by simp
513           {assume "c' = 0\<^sub>p"
514             from `c' = 0\<^sub>p` have ?eq
515               using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
516             "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
517               apply simp
518               done}
519           moreover
520           {assume cnz: "c' \<noteq> 0\<^sub>p"
521             from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
522               "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
525             have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m
526               \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
527               using mn nn' cnz np np' by simp
528             with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
529               "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
530               degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
531           ultimately have ?eq by blast }
532         ultimately have ?eq by blast}
533       ultimately show ?eq by blast}
534     note degth = this
535     { case (2 n0 n1)
536       hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1"
537         and m: "m \<le> min n0 n1" by simp_all
538       hence mn: "m \<le> n" by simp
539       let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
540       {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
541         hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
542         from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"]
543           "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"]
544           np np' C(2) mn
545         have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
546           "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
547           "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
548           "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
549           "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
550             "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
553           from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
554           have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
555             using norm by simp
556         from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
557         have "False" by simp }
558       thus ?case using "4.hyps" by clarsimp}
559 qed auto
561 lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"
562 by(induct p q rule: polymul.induct, auto simp add: field_simps)
564 lemma polymul_normh:
565     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
566   shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
567   using polymul_properties(1)  by blast
568 lemma polymul_eq0_iff:
569   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
570   shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p) "
571   using polymul_properties(2)  by blast
572 lemma polymul_degreen:
573   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
574   shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<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)"
575   using polymul_properties(3) by blast
576 lemma polymul_norm:
577   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
578   shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"
579   using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
581 lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p"
582   by (induct p arbitrary: n0 rule: headconst.induct, auto)
585   by (induct p arbitrary: n0, auto)
587 lemma monic_eqI: assumes np: "isnpolyh p n0"
588   shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
589   unfolding monic_def Let_def
591   let ?h = "headconst p"
592   assume pz: "p \<noteq> 0\<^sub>p"
593   {assume hz: "INum ?h = (0::'a)"
594     from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all
595     from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp
596     with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast}
597   thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast
598 qed
603 text{* polyneg is a negation and preserves normal form *}
604 lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
605 by (induct p rule: polyneg.induct, auto)
607 lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)"
608   by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def)
609 lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p"
610   by (induct p arbitrary: n0 rule: polyneg.induct, auto)
611 lemma polyneg_normh: "\<And>n. isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n "
612 by (induct p rule: polyneg.induct, auto simp add: polyneg0)
614 lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)"
615   using isnpoly_def polyneg_normh by simp
618 text{* polysub is a substraction and preserves normalform *}
619 lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p) - (Ipoly bs q)"
621 lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)"
624 lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))"
626 lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
627   shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p"
628 unfolding polysub_def split_def fst_conv snd_conv
629 by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
631 lemma polysub_0:
632   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
633   shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
634   unfolding polysub_def split_def fst_conv snd_conv
635   apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def])
636   apply (clarsimp simp add: Let_def)
637   apply (case_tac "n < n'", simp_all)
638   apply (case_tac "n' < n", simp_all)
639   apply (erule impE)+
640   apply (rule_tac x="Suc n" in exI, simp)
641   apply (rule_tac x="n" in exI, simp)
642   apply (erule impE)+
643   apply (rule_tac x="n" in exI, simp)
644   apply (rule_tac x="Suc n" in exI, simp)
645   apply (erule impE)+
646   apply (rule_tac x="Suc n" in exI, simp)
647   apply (rule_tac x="n" in exI, simp)
648   apply (erule impE)+
649   apply (rule_tac x="Suc n" in exI, simp)
650   apply clarsimp
651   done
653 text{* polypow is a power function and preserves normal forms *}
654 lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
655 proof(induct n rule: polypow.induct)
656   case 1 thus ?case by simp
657 next
658   case (2 n)
659   let ?q = "polypow ((Suc n) div 2) p"
660   let ?d = "polymul(?q,?q)"
661   have "odd (Suc n) \<or> even (Suc n)" by simp
662   moreover
663   {assume odd: "odd (Suc n)"
664     have th: "(Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat))))) = Suc n div 2 + Suc n div 2 + 1" by arith
665     from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul(p, ?d))" by (simp add: Let_def)
666     also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)"
667       using "2.hyps" by simp
668     also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
669       apply (simp only: power_add power_one_right) by simp
670     also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat)))))"
671       by (simp only: th)
672     finally have ?case
673     using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp  }
674   moreover
675   {assume even: "even (Suc n)"
676     have th: "(Suc (Suc (0\<Colon>nat))) * (Suc n div Suc (Suc (0\<Colon>nat))) = Suc n div 2 + Suc n div 2" by arith
677     from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def)
678     also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
679       using "2.hyps" apply (simp only: power_add) by simp
680     finally have ?case using even_nat_div_two_times_two[OF even] by (simp only: th)}
681   ultimately show ?case by blast
682 qed
684 lemma polypow_normh:
685     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
686   shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
687 proof (induct k arbitrary: n rule: polypow.induct)
688   case (2 k n)
689   let ?q = "polypow (Suc k div 2) p"
690   let ?d = "polymul (?q,?q)"
691   from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
692   from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp
693   from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp
694   from dn on show ?case by (simp add: Let_def)
695 qed auto
697 lemma polypow_norm:
698   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
699   shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
700   by (simp add: polypow_normh isnpoly_def)
702 text{* Finally the whole normalization*}
704 lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
705 by (induct p rule:polynate.induct, auto)
707 lemma polynate_norm[simp]:
708   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
709   shows "isnpoly (polynate p)"
712 text{* shift1 *}
715 lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
716 by (simp add: shift1_def polymul)
718 lemma shift1_isnpoly:
719   assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) "
720   using pn pnz by (simp add: shift1_def isnpoly_def )
722 lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"
724 lemma funpow_shift1_isnpoly:
725   "\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)"
726   by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
728 lemma funpow_isnpolyh:
729   assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n"
730   shows "isnpolyh (funpow k f p) n"
731   using f np by (induct k arbitrary: p, auto)
733 lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
734   by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
736 lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
737   using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
739 lemma funpow_shift1_1:
740   "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
743 lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
744 by (induct p  arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps)
747   assumes np: "isnpolyh p n"
748   shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
749   using np
750 proof (induct p arbitrary: n rule: behead.induct)
751   case (1 c p n) hence pn: "isnpolyh p n" by simp
752   from prems(2)[OF pn]
753   have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .
754   then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
755     by (simp_all add: th[symmetric] field_simps power_Suc)
756 qed (auto simp add: Let_def)
759   assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n"
760   using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono)
762 subsection{* Miscilanious lemmas about indexes, decrementation, substitution  etc ... *}
763 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
764 proof(induct p arbitrary: n rule: poly.induct, auto)
765   case (goal1 c n p n')
766   hence "n = Suc (n - 1)" by simp
767   hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
768   with prems(2) show ?case by simp
769 qed
771 lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
772 by (induct p arbitrary: n0 rule: isconstant.induct, auto simp add: isnpolyh_polybound0)
774 lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p" by (induct p, auto)
776 lemma decrpoly_normh: "isnpolyh p n0 \<Longrightarrow> polybound0 p \<Longrightarrow> isnpolyh (decrpoly p) (n0 - 1)"
777   apply (induct p arbitrary: n0, auto)
778   apply (atomize)
779   apply (erule_tac x = "Suc nat" in allE)
780   apply auto
781   done
784  by (induct p  arbitrary: n0 rule: head.induct, auto intro: isnpolyh_polybound0)
786 lemma polybound0_I:
787   assumes nb: "polybound0 a"
788   shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
789 using nb
790 by (induct a rule: poly.induct) auto
791 lemma polysubst0_I:
792   shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
793   by (induct t) simp_all
795 lemma polysubst0_I':
796   assumes nb: "polybound0 a"
797   shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b'#bs) a)#bs) t"
798   by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
800 lemma decrpoly: assumes nb: "polybound0 t"
801   shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)"
802   using nb by (induct t rule: decrpoly.induct, simp_all)
804 lemma polysubst0_polybound0: assumes nb: "polybound0 t"
805   shows "polybound0 (polysubst0 t a)"
806 using nb by (induct a rule: poly.induct, auto)
808 lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
809   by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)
811 primrec maxindex :: "poly \<Rightarrow> nat" where
812   "maxindex (Bound n) = n + 1"
813 | "maxindex (CN c n p) = max  (n + 1) (max (maxindex c) (maxindex p))"
814 | "maxindex (Add p q) = max (maxindex p) (maxindex q)"
815 | "maxindex (Sub p q) = max (maxindex p) (maxindex q)"
816 | "maxindex (Mul p q) = max (maxindex p) (maxindex q)"
817 | "maxindex (Neg p) = maxindex p"
818 | "maxindex (Pw p n) = maxindex p"
819 | "maxindex (C x) = 0"
821 definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool" where
822   "wf_bs bs p = (length bs \<ge> maxindex p)"
824 lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall> c \<in> set (coefficients p). wf_bs bs c"
825 proof(induct p rule: coefficients.induct)
826   case (1 c p)
827   show ?case
828   proof
829     fix x assume xc: "x \<in> set (coefficients (CN c 0 p))"
830     hence "x = c \<or> x \<in> set (coefficients p)" by simp
831     moreover
832     {assume "x = c" hence "wf_bs bs x" using "1.prems"  unfolding wf_bs_def by simp}
833     moreover
834     {assume H: "x \<in> set (coefficients p)"
835       from "1.prems" have "wf_bs bs p" unfolding wf_bs_def by simp
836       with "1.hyps" H have "wf_bs bs x" by blast }
837     ultimately  show "wf_bs bs x" by blast
838   qed
839 qed simp_all
841 lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
842 by (induct p rule: coefficients.induct, auto)
844 lemma length_exists: "\<exists>xs. length xs = n" by (rule exI[where x="replicate n x"], simp)
846 lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p"
847   unfolding wf_bs_def by (induct p, auto simp add: nth_append)
849 lemma take_maxindex_wf: assumes wf: "wf_bs bs p"
850   shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p"
851 proof-
852   let ?ip = "maxindex p"
853   let ?tbs = "take ?ip bs"
854   from wf have "length ?tbs = ?ip" unfolding wf_bs_def by simp
855   hence wf': "wf_bs ?tbs p" unfolding wf_bs_def by  simp
856   have eq: "bs = ?tbs @ (drop ?ip bs)" by simp
857   from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis using eq by simp
858 qed
860 lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
861   by (induct p, auto)
863 lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
864   unfolding wf_bs_def by simp
866 lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p"
867   unfolding wf_bs_def by simp
871 lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
872 by(induct p rule: coefficients.induct, auto simp add: wf_bs_def)
873 lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
874   by (induct p rule: coefficients.induct, simp_all)
878   by (induct p rule: coefficients.induct, auto)
880 lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
881   unfolding wf_bs_def by (induct p rule: decrpoly.induct, auto)
883 lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists> ys. length (xs @ ys) = n"
884   apply (rule exI[where x="replicate (n - length xs) z"])
885   by simp
886 lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
887 by (cases p, auto) (case_tac "nat", simp_all)
889 lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
890   unfolding wf_bs_def
891   apply (induct p q rule: polyadd.induct)
892   apply (auto simp add: Let_def)
893   done
895 lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)"
897  unfolding wf_bs_def
898   apply (induct p q arbitrary: bs rule: polymul.induct)
900   apply clarsimp
901   apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format])
902   apply auto
903   done
905 lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)"
906   unfolding wf_bs_def by (induct p rule: polyneg.induct, auto)
908 lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p -\<^sub>p q)"
909   unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast
911 subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*}
913 definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
914 definition "polypoly' bs p = map ((Ipoly bs o decrpoly)) (coefficients p)"
915 definition "poly_nate bs p = map ((Ipoly bs o decrpoly)) (coefficients (polynate p))"
917 lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall> q \<in> set (coefficients p). isnpolyh q n0"
918 proof (induct p arbitrary: n0 rule: coefficients.induct)
919   case (1 c p n0)
920   have cp: "isnpolyh (CN c 0 p) n0" by fact
921   hence norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0"
922     by (auto simp add: isnpolyh_mono[where n'=0])
923   from "1.hyps"[OF norm(2)] norm(1) norm(4)  show ?case by simp
924 qed auto
926 lemma coefficients_isconst:
927   "isnpolyh p n \<Longrightarrow> \<forall>q\<in>set (coefficients p). isconstant q"
928   by (induct p arbitrary: n rule: coefficients.induct,
931 lemma polypoly_polypoly':
932   assumes np: "isnpolyh p n0"
933   shows "polypoly (x#bs) p = polypoly' bs p"
934 proof-
935   let ?cf = "set (coefficients p)"
936   from coefficients_normh[OF np] have cn_norm: "\<forall> q\<in> ?cf. isnpolyh q n0" .
937   {fix q assume q: "q \<in> ?cf"
938     from q cn_norm have th: "isnpolyh q n0" by blast
939     from coefficients_isconst[OF np] q have "isconstant q" by blast
940     with isconstant_polybound0[OF th] have "polybound0 q" by blast}
941   hence "\<forall>q \<in> ?cf. polybound0 q" ..
942   hence "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)"
943     using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs]
944     by auto
946   thus ?thesis unfolding polypoly_def polypoly'_def by simp
947 qed
949 lemma polypoly_poly:
950   assumes np: "isnpolyh p n0" shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x"
951   using np
952 by (induct p arbitrary: n0 bs rule: coefficients.induct, auto simp add: polypoly_def)
954 lemma polypoly'_poly:
955   assumes np: "isnpolyh p n0" shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
956   using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] .
959 lemma polypoly_poly_polybound0:
960   assumes np: "isnpolyh p n0" and nb: "polybound0 p"
961   shows "polypoly bs p = [Ipoly bs p]"
962   using np nb unfolding polypoly_def
963   by (cases p, auto, case_tac nat, auto)
966   by (induct p rule: head.induct, auto)
968 lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)"
969   by (cases p,auto)
972   by (induct p rule: head.induct, simp_all)
974 lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (head p = 0\<^sub>p) = (p = 0\<^sub>p)"
977 lemma isnpolyh_zero_iff:
978   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})"
979   shows "p = 0\<^sub>p"
980 using nq eq
981 proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
982   case less
983   note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)`
984   {assume nz: "maxindex p = 0"
985     then obtain c where "p = C c" using np by (cases p, auto)
986     with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
987   moreover
988   {assume nz: "maxindex p \<noteq> 0"
989     let ?h = "head p"
990     let ?hd = "decrpoly ?h"
991     let ?ihd = "maxindex ?hd"
992     from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h"
993       by simp_all
994     hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast
996     from maxindex_coefficients[of p] coefficients_head[of p, symmetric]
997     have mihn: "maxindex ?h \<le> maxindex p" by auto
998     with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < maxindex p" by auto
999     {fix bs:: "'a list"  assume bs: "wf_bs bs ?hd"
1000       let ?ts = "take ?ihd bs"
1001       let ?rs = "drop ?ihd bs"
1002       have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp
1003       have bs_ts_eq: "?ts@ ?rs = bs" by simp
1004       from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp
1005       from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp
1006       with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast
1007       hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp
1008       with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast
1009       hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
1010       with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
1011       have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
1012       hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext)
1013       hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
1014         using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
1016       have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
1017       from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp
1018       with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp
1019       with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }
1020     then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast
1022     from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
1023     hence "?h = 0\<^sub>p" by simp
1024     with head_nz[OF np] have "p = 0\<^sub>p" by simp}
1025   ultimately show "p = 0\<^sub>p" by blast
1026 qed
1028 lemma isnpolyh_unique:
1029   assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
1030   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"
1031 proof(auto)
1032   assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
1033   hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
1034   hence "\<forall>bs. wf_bs bs (p -\<^sub>p q) \<longrightarrow> \<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)"
1035     using wf_bs_polysub[where p=p and q=q] by auto
1036   with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq]
1037   show "p = q" by blast
1038 qed
1041 text{* consequenses of unicity on the algorithms for polynomial normalization *}
1043 lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1044   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
1047 lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
1048 lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
1050   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1051   and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
1052   using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np]
1053     isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
1055 lemma polymul_1[simp]:
1056     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1057   and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
1058   using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]
1059     isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
1060 lemma polymul_0[simp]:
1061   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1062   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"
1063   using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh]
1064     isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
1066 lemma polymul_commute:
1067     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1068   and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
1069   shows "p *\<^sub>p q = q *\<^sub>p p"
1070 using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{field_char_0, field_inverse_zero, power}"] by simp
1072 declare polyneg_polyneg[simp]
1074 lemma isnpolyh_polynate_id[simp]:
1075   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1076   and np:"isnpolyh p n0" shows "polynate p = p"
1077   using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"] by simp
1079 lemma polynate_idempotent[simp]:
1080     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1081   shows "polynate (polynate p) = polynate p"
1082   using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
1084 lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
1085   unfolding poly_nate_def polypoly'_def ..
1086 lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0, field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
1087   using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
1088   unfolding poly_nate_polypoly' by (auto intro: ext)
1090 subsection{* heads, degrees and all that *}
1091 lemma degree_eq_degreen0: "degree p = degreen p 0"
1092   by (induct p rule: degree.induct, simp_all)
1094 lemma degree_polyneg: assumes n: "isnpolyh p n"
1095   shows "degree (polyneg p) = degree p"
1096   using n
1097   by (induct p arbitrary: n rule: polyneg.induct, simp_all) (case_tac na, auto)
1100   assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1101   shows "degree (p +\<^sub>p q) \<le> max (degree p) (degree q)"
1102 using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp
1105 lemma degree_polysub: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1106   shows "degree (p -\<^sub>p q) \<le> max (degree p) (degree q)"
1107 proof-
1108   from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp
1109   from degree_polyadd[OF np nq'] show ?thesis by (simp add: polysub_def degree_polyneg[OF nq])
1110 qed
1113   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1114   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q"
1115   and d: "degree p = degree q"
1116   shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
1117 unfolding polysub_def split_def fst_conv snd_conv
1118 using np nq h d
1120   case (1 a b a' b') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def])
1121 next
1122   case (2 a b c' n' p')
1123   let ?c = "(a,b)"
1124   from prems have "degree (C ?c) = degree (CN c' n' p')" by simp
1125   hence nz:"n' > 0" by (cases n', auto)
1126   hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
1127   with prems show ?case by simp
1128 next
1129   case (3 c n p a' b')
1130   let ?c' = "(a',b')"
1131   from prems have "degree (C ?c') = degree (CN c n p)" by simp
1132   hence nz:"n > 0" by (cases n, auto)
1133   hence "head (CN c n p) = CN c n p" by (cases n, auto)
1134   with prems show ?case by simp
1135 next
1136   case (4 c n p c' n' p')
1137   hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1"
1138     "head (CN c n p) = head (CN c' n' p')" "degree (CN c n p) = degree (CN c' n' p')" by simp+
1139   hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all
1140   hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0"
1141     using H(1-2) degree_polyneg by auto
1142   from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')"  by simp+
1143   from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' have degcmc': "degree (c +\<^sub>p  ~\<^sub>pc') = 0"  by simp
1144   from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" by auto
1145   have "n = n' \<or> n < n' \<or> n > n'" by arith
1146   moreover
1147   {assume nn': "n = n'"
1148     have "n = 0 \<or> n >0" by arith
1149     moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')}
1150     moreover {assume nz: "n > 0"
1151       with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
1152       hence ?case using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def split_def fst_conv snd_conv] using nn' prems by (simp add: Let_def)}
1153     ultimately have ?case by blast}
1154   moreover
1155   {assume nn': "n < n'" hence n'p: "n' > 0" by simp
1156     hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
1157     have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using prems by (cases n', simp_all)
1158     hence "n > 0" by (cases n, simp_all)
1159     hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)
1161   moreover
1162   {assume nn': "n > n'"  hence np: "n > 0" by simp
1163     hence headcnp:"head (CN c n p) = CN c n p"  by (cases n, simp_all)
1164     from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
1165     from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)
1166     with degcnpeq have "n' > 0" by (cases n', simp_all)
1167     hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
1169   ultimately show ?case  by blast
1170 qed auto
1175 lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
1176 proof(induct k arbitrary: n0 p)
1177   case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
1178   with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
1180   thus ?case by (simp add: funpow_swap1)
1181 qed auto
1183 lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
1185 lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "
1186   by (induct k arbitrary: p, auto simp add: shift1_degree)
1188 lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"
1189   by (induct n arbitrary: p, simp_all add: funpow_def)
1191 lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"
1192   by (induct p arbitrary: n rule: degree.induct, auto)
1193 lemma headn_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> headn p m = p"
1194   by (induct p arbitrary: n rule: degreen.induct, auto)
1195 lemma head_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> head p = p"
1196   by (induct p arbitrary: n rule: degree.induct, auto)
1198   by (induct p rule: head.induct, auto)
1201   "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> \<Longrightarrow> degree p = degree q"
1202   using polyadd_eq_const_degreen degree_eq_degreen0 by simp
1204 lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1205   and deg: "degree p \<noteq> degree q"
1206   shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"
1207 using np nq deg
1208 apply(induct p q arbitrary: n0 n1 rule: polyadd.induct,simp_all)
1209 apply (case_tac n', simp, simp)
1210 apply (case_tac n, simp, simp)
1211 apply (case_tac n, case_tac n', simp add: Let_def)
1212 apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
1214 apply clarsimp
1215 apply (erule_tac impE,blast)
1216 apply (erule_tac impE,blast)
1217 apply clarsimp
1218 apply simp
1219 apply (case_tac n', simp_all)
1220 done
1223    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1224   shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
1225 proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
1226   case (2 a b c' n' p' n0 n1)
1228   thus ?case using prems by (cases n', auto)
1229 next
1230   case (3 c n p a' b' n0 n1)
1232   thus ?case using prems by (cases n, auto)
1233 next
1234   case (4 c n p c' n' p' n0 n1)
1235   hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
1236     "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'"
1237     by simp_all
1238   have "n < n' \<or> n' < n \<or> n = n'" by arith
1239   moreover
1240   {assume nn': "n < n'" hence ?case
1241       thm prems
1242       using norm
1243     prems(6)[rule_format, OF nn' norm(1,6)]
1244     prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
1245   moreover {assume nn': "n'< n"
1246     hence stupid: "n' < n \<and> \<not> n < n'" by simp
1247     hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)]
1248       prems(5)[rule_format, OF stupid norm(5,4)]
1249       by (simp,cases n',simp,cases n,auto)}
1250   moreover {assume nn': "n' = n"
1251     hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp
1252     from nn' polymul_normh[OF norm(5,4)]
1253     have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
1254     from nn' polymul_normh[OF norm(5,3)] norm
1255     have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp
1256     from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6)
1257     have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
1259     have nth: "isnpolyh ((CN c n p *\<^sub>p c') +\<^sub>p (CN 0\<^sub>p n (CN c n p *\<^sub>p p'))) n"
1261     {assume np: "n > 0"
1262       with nn' head_isnpolyh_Suc'[OF np nth]
1264       have ?case by simp}
1265     moreover
1266     {moreover assume nz: "n = 0"
1267       from polymul_degreen[OF norm(5,4), where m="0"]
1268         polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
1269       norm(5,6) degree_npolyhCN[OF norm(6)]
1270     have dth:"degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
1271     hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
1273     have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
1274         prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
1275     ultimately have ?case by (cases n) auto}
1276   ultimately show ?case by blast
1277 qed simp_all
1279 lemma degree_coefficients: "degree p = length (coefficients p) - 1"
1280   by(induct p rule: degree.induct, auto)
1283   by (induct p rule: head.induct, auto)
1285 lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1+ degree p"
1286   by (cases n, simp_all)
1287 lemma degree_CN': "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<ge>  degree p"
1288   by (cases n, simp_all)
1290 lemma polyadd_different_degree: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degree p \<noteq> degree q\<rbrakk> \<Longrightarrow> degree (polyadd(p,q)) = max (degree p) (degree q)"
1291   using polyadd_different_degreen degree_eq_degreen0 by simp
1293 lemma degreen_polyneg: "isnpolyh p n0 \<Longrightarrow> degreen (~\<^sub>p p) m = degreen p m"
1294   by (induct p arbitrary: n0 rule: polyneg.induct, auto)
1296 lemma degree_polymul:
1297   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1298   and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1299   shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
1300   using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp
1302 lemma polyneg_degree: "isnpolyh p n \<Longrightarrow> degree (polyneg p) = degree p"
1303   by (induct p arbitrary: n rule: degree.induct, auto)
1306   by (induct p arbitrary: n rule: degree.induct, auto)
1308 subsection {* Correctness of polynomial pseudo division *}
1310 lemma polydivide_aux_properties:
1311   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1312   and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
1313   and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
1314   shows "(polydivide_aux a n p k s = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p)
1315           \<and> (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
1316   using ns
1317 proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
1318   case less
1319   let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
1320   let ?ths = "polydivide_aux a n p k s = (k', r) \<longrightarrow>  k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p)
1321     \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1322   let ?b = "head s"
1323   let ?p' = "funpow (degree s - n) shift1 p"
1324   let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p"
1325   let ?akk' = "a ^\<^sub>p (k' - k)"
1326   note ns = `isnpolyh s n1`
1327   from np have np0: "isnpolyh p 0"
1328     using isnpolyh_mono[where n="n0" and n'="0" and p="p"]  by simp
1329   have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def by simp
1331   from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
1332   from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap
1333   have nakk':"isnpolyh ?akk' 0" by blast
1334   {assume sz: "s = 0\<^sub>p"
1335    hence ?ths using np polydivide_aux.simps apply clarsimp by (rule exI[where x="0\<^sub>p"], simp) }
1336   moreover
1337   {assume sz: "s \<noteq> 0\<^sub>p"
1338     {assume dn: "degree s < n"
1339       hence "?ths" using ns ndp np polydivide_aux.simps by auto (rule exI[where x="0\<^sub>p"],simp) }
1340     moreover
1341     {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
1342       have degsp': "degree s = degree ?p'"
1343         using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] by simp
1344       {assume ba: "?b = a"
1346         have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
1348         have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
1349         moreover
1350         {assume deglt:"degree (s -\<^sub>p ?p') < degree s"
1351           from polydivide_aux.simps sz dn' ba
1352           have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1354           {assume h1: "polydivide_aux a n p k s = (k', r)"
1355             from less(1)[OF deglt nr, of k k' r]
1356               trans[OF eq[symmetric] h1]
1357             have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
1358               and q1:"\<exists>q nq. isnpolyh q nq \<and> (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" by auto
1359             from q1 obtain q n1 where nq: "isnpolyh q n1"
1360               and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"  by blast
1361             from nr obtain nr where nr': "isnpolyh r nr" by blast
1362             from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
1363             from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
1364             have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
1366               polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
1367             have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp
1368             from asp have "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
1369               Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
1370             hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
1371               Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1373             hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1374               Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p)
1375               + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1376               by (auto simp only: funpow_shift1_1)
1377             hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1378               Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p)
1379               + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps)
1380             hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1381               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
1382             with isnpolyh_unique[OF nakks' nqr']
1383             have "a ^\<^sub>p (k' - k) *\<^sub>p s =
1384               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 blast
1385             hence ?qths using nq'
1386               apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
1387               apply (rule_tac x="0" in exI) by simp
1388             with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1389               by blast } hence ?ths by blast }
1390         moreover
1391         {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
1392           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}"]
1393           have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp
1394           hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
1395             by (simp only: funpow_shift1_1) simp
1396           hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
1397           {assume h1: "polydivide_aux a n p k s = (k',r)"
1398             from polydivide_aux.simps sz dn' ba
1399             have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1401             also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.simps spz by simp
1402             finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
1403             with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
1404               polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths
1405               apply auto
1406               apply (rule exI[where x="?xdn"])
1407               apply (auto simp add: polymul_commute[of p])
1408               done} }
1409         ultimately have ?ths by blast }
1410       moreover
1411       {assume ba: "?b \<noteq> a"
1412         from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns]
1414         have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
1415         have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
1416           using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns]
1418             funpow_shift1_nz[OF pnz] by simp_all
1421         have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')"
1425         from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
1426           head_nz[OF np] pnz sz ap[symmetric]
1427           funpow_shift1_nz[OF pnz, where n="degree s - n"]
1429           ndp dn
1430         have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
1431           by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
1432         {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
1434           ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
1435           {assume h1:"polydivide_aux a n p k s = (k', r)"
1436             from h1 polydivide_aux.simps sz dn' ba
1437             have eq:"polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
1439             with less(1)[OF dth nasbp', of "Suc k" k' r]
1440             obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq"
1441               and dr: "degree r = 0 \<or> degree r < degree p"
1442               and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto
1443             from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
1444             {fix bs:: "'a::{field_char_0, field_inverse_zero} list"
1446             from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
1447             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
1448             hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
1449               by (simp add: field_simps power_Suc)
1450             hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r"
1451               by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
1452             hence "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"
1454             hence ieq:"\<forall>(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1455               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
1456             let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
1457             from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]]
1458             have nqw: "isnpolyh ?q 0" by simp
1459             from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]]
1460             have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r" by blast
1461             from dr kk' nr h1 asth nqw have ?ths apply simp
1462               apply (rule conjI)
1463               apply (rule exI[where x="nr"], simp)
1464               apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
1465               apply (rule exI[where x="0"], simp)
1466               done}
1467           hence ?ths by blast }
1468         moreover
1469         {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
1470           {fix bs :: "'a::{field_char_0, field_inverse_zero} list"
1471             from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
1472           have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
1473           hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
1474             by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
1475           hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
1476         }
1477         hence hth: "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
1478           from hth
1479           have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
1480             using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1481                     polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
1482               simplified ap] by simp
1483           {assume h1: "polydivide_aux a n p k s = (k', r)"
1484           from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps
1485           have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
1486           with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
1487             polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
1488           have ?ths apply (clarsimp simp add: Let_def)
1489             apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
1490             apply (rule exI[where x="0"], simp)
1491             done}
1492         hence ?ths by blast}
1493         ultimately have ?ths using  degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
1494           head_nz[OF np] pnz sz ap[symmetric]
1495           by (simp add: degree_eq_degreen0[symmetric]) blast }
1496       ultimately have ?ths by blast
1497     }
1498     ultimately have ?ths by blast}
1499   ultimately show ?ths by blast
1500 qed
1502 lemma polydivide_properties:
1503   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1504   and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
1505   shows "(\<exists> k r. polydivide s p = (k,r) \<and> (\<exists>nr. isnpolyh r nr) \<and> (degree r = 0 \<or> degree r < degree p)
1506   \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
1507 proof-
1508   have trv: "head p = head p" "degree p = degree p" by simp_all
1509   from polydivide_def[where s="s" and p="p"]
1510   have ex: "\<exists> k r. polydivide s p = (k,r)" by auto
1511   then obtain k r where kr: "polydivide s p = (k,r)" by blast
1512   from trans[OF meta_eq_to_obj_eq[OF polydivide_def[where s="s"and p="p"], symmetric] kr]
1513     polydivide_aux_properties[OF np ns trv pnz, where k="0" and k'="k" and r="r"]
1514   have "(degree r = 0 \<or> degree r < degree p) \<and>
1515    (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> head p ^\<^sub>p k - 0 *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" by blast
1516   with kr show ?thesis
1517     apply -
1518     apply (rule exI[where x="k"])
1519     apply (rule exI[where x="r"])
1520     apply simp
1521     done
1522 qed
1524 subsection{* More about polypoly and pnormal etc *}
1526 definition "isnonconstant p = (\<not> isconstant p)"
1528 lemma last_map: "xs \<noteq> [] ==> last (map f xs) = f (last xs)" by (induct xs, auto)
1530 lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p"
1531   shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
1532 proof
1533   let ?p = "polypoly bs p"
1534   assume H: "pnormal ?p"
1535   have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
1537   from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]
1538     pnormal_last_nonzero[OF H]
1539   show "Ipoly bs (head p) \<noteq> 0" by (simp add: polypoly_def)
1540 next
1541   assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1542   let ?p = "polypoly bs p"
1543   have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
1544   hence pz: "?p \<noteq> []" by (simp add: polypoly_def)
1545   hence lg: "length ?p > 0" by simp
1546   from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]
1547   have lz: "last ?p \<noteq> 0" by (simp add: polypoly_def)
1548   from pnormal_last_length[OF lg lz] show "pnormal ?p" .
1549 qed
1551 lemma isnonconstant_coefficients_length: "isnonconstant p \<Longrightarrow> length (coefficients p) > 1"
1552   unfolding isnonconstant_def
1553   apply (cases p, simp_all)
1554   apply (case_tac nat, auto)
1555   done
1556 lemma isnonconstant_nonconstant: assumes inc: "isnonconstant p"
1557   shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
1558 proof
1559   let ?p = "polypoly bs p"
1560   assume nc: "nonconstant ?p"
1561   from isnonconstant_pnormal_iff[OF inc, of bs] nc
1562   show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" unfolding nonconstant_def by blast
1563 next
1564   let ?p = "polypoly bs p"
1565   assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1566   from isnonconstant_pnormal_iff[OF inc, of bs] h
1567   have pn: "pnormal ?p" by blast
1568   {fix x assume H: "?p = [x]"
1569     from H have "length (coefficients p) = 1" unfolding polypoly_def by auto
1570     with isnonconstant_coefficients_length[OF inc] have False by arith}
1571   thus "nonconstant ?p" using pn unfolding nonconstant_def by blast
1572 qed
1574 lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
1575   unfolding pnormal_def
1576  apply (induct p)
1577  apply (simp_all, case_tac "p=[]", simp_all)
1578  done
1580 lemma degree_degree: assumes inc: "isnonconstant p"
1581   shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1582 proof
1583   let  ?p = "polypoly bs p"
1584   assume H: "degree p = Polynomial_List.degree ?p"
1585   from isnonconstant_coefficients_length[OF inc] have pz: "?p \<noteq> []"
1586     unfolding polypoly_def by auto
1587   from H degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
1588   have lg:"length (pnormalize ?p) = length ?p"
1589     unfolding Polynomial_List.degree_def polypoly_def by simp
1590   hence "pnormal ?p" using pnormal_length[OF pz] by blast
1591   with isnonconstant_pnormal_iff[OF inc]
1592   show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" by blast
1593 next
1594   let  ?p = "polypoly bs p"
1595   assume H: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1596   with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p" by blast
1597   with degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
1598   show "degree p = Polynomial_List.degree ?p"
1599     unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
1600 qed
1602 section{* Swaps ; Division by a certain variable *}
1603 primrec swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where
1604   "swap n m (C x) = C x"
1605 | "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
1606 | "swap n m (Neg t) = Neg (swap n m t)"
1607 | "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
1608 | "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
1609 | "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
1610 | "swap n m (Pw t k) = Pw (swap n m t) k"
1611 | "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)
1612   (swap n m p)"
1614 lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs"
1615   shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1616 proof (induct t)
1617   case (Bound k) thus ?case using nbs mbs by simp
1618 next
1619   case (CN c k p) thus ?case using nbs mbs by simp
1620 qed simp_all
1621 lemma swap_swap_id[simp]: "swap n m (swap m n t) = t"
1622   by (induct t,simp_all)
1624 lemma swap_commute: "swap n m p = swap m n p" by (induct p, simp_all)
1626 lemma swap_same_id[simp]: "swap n n t = t"
1627   by (induct t, simp_all)
1629 definition "swapnorm n m t = polynate (swap n m t)"
1631 lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
1632   shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1633   using swap[OF prems] swapnorm_def by simp
1635 lemma swapnorm_isnpoly[simp]:
1636     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1637   shows "isnpoly (swapnorm n m p)"
1638   unfolding swapnorm_def by simp
1640 definition "polydivideby n s p =
1641     (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp
1642      in (k,swapnorm 0 n h,swapnorm 0 n r))"
1644 lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p, simp_all)
1646 consts isweaknpoly :: "poly \<Rightarrow> bool"
1647 recdef isweaknpoly "measure size"
1648   "isweaknpoly (C c) = True"
1649   "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
1650   "isweaknpoly p = False"
1652 lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p"
1653   by (induct p arbitrary: n0, auto)
1655 lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)"
1656   by (induct p, auto)
1658 end