18 |
18 |
19 |
19 |
20 subsection\<open>Boundedness, substitution and all that\<close> |
20 subsection\<open>Boundedness, substitution and all that\<close> |
21 |
21 |
22 primrec polysize:: "poly \<Rightarrow> nat" |
22 primrec polysize:: "poly \<Rightarrow> nat" |
23 where |
23 where |
24 "polysize (C c) = 1" |
24 "polysize (C c) = 1" |
25 | "polysize (Bound n) = 1" |
25 | "polysize (Bound n) = 1" |
26 | "polysize (Neg p) = 1 + polysize p" |
26 | "polysize (Neg p) = 1 + polysize p" |
27 | "polysize (Add p q) = 1 + polysize p + polysize q" |
27 | "polysize (Add p q) = 1 + polysize p + polysize q" |
28 | "polysize (Sub p q) = 1 + polysize p + polysize q" |
28 | "polysize (Sub p q) = 1 + polysize p + polysize q" |
29 | "polysize (Mul p q) = 1 + polysize p + polysize q" |
29 | "polysize (Mul p q) = 1 + polysize p + polysize q" |
30 | "polysize (Pw p n) = 1 + polysize p" |
30 | "polysize (Pw p n) = 1 + polysize p" |
31 | "polysize (CN c n p) = 4 + polysize c + polysize p" |
31 | "polysize (CN c n p) = 4 + polysize c + polysize p" |
32 |
32 |
33 primrec polybound0:: "poly \<Rightarrow> bool" \<comment> \<open>a poly is INDEPENDENT of Bound 0\<close> |
33 primrec polybound0:: "poly \<Rightarrow> bool" \<comment> \<open>a poly is INDEPENDENT of Bound 0\<close> |
34 where |
34 where |
35 "polybound0 (C c) \<longleftrightarrow> True" |
35 "polybound0 (C c) \<longleftrightarrow> True" |
36 | "polybound0 (Bound n) \<longleftrightarrow> n > 0" |
36 | "polybound0 (Bound n) \<longleftrightarrow> n > 0" |
37 | "polybound0 (Neg a) \<longleftrightarrow> polybound0 a" |
37 | "polybound0 (Neg a) \<longleftrightarrow> polybound0 a" |
38 | "polybound0 (Add a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b" |
38 | "polybound0 (Add a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b" |
39 | "polybound0 (Sub a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b" |
39 | "polybound0 (Sub a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b" |
40 | "polybound0 (Mul a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b" |
40 | "polybound0 (Mul a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b" |
41 | "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p" |
41 | "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p" |
42 | "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p" |
42 | "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p" |
43 |
43 |
44 primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" \<comment> \<open>substitute a poly into a poly for Bound 0\<close> |
44 primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" \<comment> \<open>substitute a poly into a poly for Bound 0\<close> |
45 where |
45 where |
46 "polysubst0 t (C c) = C c" |
46 "polysubst0 t (C c) = C c" |
47 | "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)" |
47 | "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)" |
48 | "polysubst0 t (Neg a) = Neg (polysubst0 t a)" |
48 | "polysubst0 t (Neg a) = Neg (polysubst0 t a)" |
49 | "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)" |
49 | "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)" |
50 | "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)" |
51 | "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)" |
52 | "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n" |
52 | "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n" |
53 | "polysubst0 t (CN c n p) = |
53 | "polysubst0 t (CN c n p) = |
54 (if n = 0 then Add (polysubst0 t c) (Mul t (polysubst0 t p)) |
54 (if n = 0 then Add (polysubst0 t c) (Mul t (polysubst0 t p)) |
55 else CN (polysubst0 t c) n (polysubst0 t p))" |
55 else CN (polysubst0 t c) n (polysubst0 t p))" |
56 |
56 |
57 fun decrpoly:: "poly \<Rightarrow> poly" |
57 fun decrpoly:: "poly \<Rightarrow> poly" |
58 where |
58 where |
59 "decrpoly (Bound n) = Bound (n - 1)" |
59 "decrpoly (Bound n) = Bound (n - 1)" |
60 | "decrpoly (Neg a) = Neg (decrpoly a)" |
60 | "decrpoly (Neg a) = Neg (decrpoly a)" |
61 | "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)" |
61 | "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)" |
62 | "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)" |
62 | "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)" |
63 | "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)" |
63 | "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)" |
64 | "decrpoly (Pw p n) = Pw (decrpoly p) n" |
64 | "decrpoly (Pw p n) = Pw (decrpoly p) n" |
65 | "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)" |
65 | "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)" |
66 | "decrpoly a = a" |
66 | "decrpoly a = a" |
67 |
67 |
68 |
68 |
69 subsection \<open>Degrees and heads and coefficients\<close> |
69 subsection \<open>Degrees and heads and coefficients\<close> |
70 |
70 |
71 fun degree :: "poly \<Rightarrow> nat" |
71 fun degree :: "poly \<Rightarrow> nat" |
72 where |
72 where |
73 "degree (CN c 0 p) = 1 + degree p" |
73 "degree (CN c 0 p) = 1 + degree p" |
74 | "degree p = 0" |
74 | "degree p = 0" |
75 |
75 |
76 fun head :: "poly \<Rightarrow> poly" |
76 fun head :: "poly \<Rightarrow> poly" |
77 where |
77 where |
78 "head (CN c 0 p) = head p" |
78 "head (CN c 0 p) = head p" |
79 | "head p = p" |
79 | "head p = p" |
80 |
80 |
81 text \<open>More general notions of degree and head.\<close> |
81 text \<open>More general notions of degree and head.\<close> |
82 |
82 |
83 fun degreen :: "poly \<Rightarrow> nat \<Rightarrow> nat" |
83 fun degreen :: "poly \<Rightarrow> nat \<Rightarrow> nat" |
84 where |
84 where |
85 "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)" |
85 "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)" |
86 | "degreen p = (\<lambda>m. 0)" |
86 | "degreen p = (\<lambda>m. 0)" |
87 |
87 |
88 fun headn :: "poly \<Rightarrow> nat \<Rightarrow> poly" |
88 fun headn :: "poly \<Rightarrow> nat \<Rightarrow> poly" |
89 where |
89 where |
90 "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)" |
90 "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)" |
91 | "headn p = (\<lambda>m. p)" |
91 | "headn p = (\<lambda>m. p)" |
92 |
92 |
93 fun coefficients :: "poly \<Rightarrow> poly list" |
93 fun coefficients :: "poly \<Rightarrow> poly list" |
94 where |
94 where |
95 "coefficients (CN c 0 p) = c # coefficients p" |
95 "coefficients (CN c 0 p) = c # coefficients p" |
96 | "coefficients p = [p]" |
96 | "coefficients p = [p]" |
97 |
97 |
98 fun isconstant :: "poly \<Rightarrow> bool" |
98 fun isconstant :: "poly \<Rightarrow> bool" |
99 where |
99 where |
100 "isconstant (CN c 0 p) = False" |
100 "isconstant (CN c 0 p) = False" |
101 | "isconstant p = True" |
101 | "isconstant p = True" |
102 |
102 |
103 fun behead :: "poly \<Rightarrow> poly" |
103 fun behead :: "poly \<Rightarrow> poly" |
104 where |
104 where |
105 "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')" |
105 "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')" |
106 | "behead p = 0\<^sub>p" |
106 | "behead p = 0\<^sub>p" |
107 |
107 |
108 fun headconst :: "poly \<Rightarrow> Num" |
108 fun headconst :: "poly \<Rightarrow> Num" |
109 where |
109 where |
110 "headconst (CN c n p) = headconst p" |
110 "headconst (CN c n p) = headconst p" |
111 | "headconst (C n) = n" |
111 | "headconst (C n) = n" |
112 |
112 |
113 |
113 |
114 subsection \<open>Operations for normalization\<close> |
114 subsection \<open>Operations for normalization\<close> |
115 |
115 |
116 declare if_cong[fundef_cong del] |
116 declare if_cong[fundef_cong del] |
117 declare let_cong[fundef_cong del] |
117 declare let_cong[fundef_cong del] |
118 |
118 |
119 fun polyadd :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60) |
119 fun polyadd :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60) |
120 where |
120 where |
121 "polyadd (C c) (C c') = C (c +\<^sub>N c')" |
121 "polyadd (C c) (C c') = C (c +\<^sub>N c')" |
122 | "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'" |
122 | "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'" |
123 | "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p" |
123 | "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p" |
124 | "polyadd (CN c n p) (CN c' n' p') = |
124 | "polyadd (CN c n p) (CN c' n' p') = |
125 (if n < n' then CN (polyadd c (CN c' n' p')) n p |
125 (if n < n' then CN (polyadd c (CN c' n' p')) n p |
126 else if n' < n then CN (polyadd (CN c n p) c') n' p' |
126 else if n' < n then CN (polyadd (CN c n p) c') n' p' |
127 else |
127 else |
128 let |
128 let |
129 cc' = polyadd c c'; |
129 cc' = polyadd c c'; |
130 pp' = polyadd p p' |
130 pp' = polyadd p p' |
131 in if pp' = 0\<^sub>p then cc' else CN cc' n pp')" |
131 in if pp' = 0\<^sub>p then cc' else CN cc' n pp')" |
132 | "polyadd a b = Add a b" |
132 | "polyadd a b = Add a b" |
133 |
|
134 |
133 |
135 fun polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p") |
134 fun polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p") |
136 where |
135 where |
137 "polyneg (C c) = C (~\<^sub>N c)" |
136 "polyneg (C c) = C (~\<^sub>N c)" |
138 | "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)" |
137 | "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)" |
139 | "polyneg a = Neg a" |
138 | "polyneg a = Neg a" |
140 |
139 |
141 definition polysub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60) |
140 definition polysub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60) |
142 where "p -\<^sub>p q = polyadd p (polyneg q)" |
141 where "p -\<^sub>p q = polyadd p (polyneg q)" |
143 |
142 |
144 fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60) |
143 fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60) |
145 where |
144 where |
146 "polymul (C c) (C c') = C (c *\<^sub>N c')" |
145 "polymul (C c) (C c') = C (c *\<^sub>N c')" |
147 | "polymul (C c) (CN c' n' p') = |
146 | "polymul (C c) (CN c' n' p') = |
148 (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))" |
147 (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))" |
149 | "polymul (CN c n p) (C c') = |
148 | "polymul (CN c n p) (C c') = |
150 (if c' = 0\<^sub>N then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))" |
149 (if c' = 0\<^sub>N then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))" |
151 | "polymul (CN c n p) (CN c' n' p') = |
150 | "polymul (CN c n p) (CN c' n' p') = |
152 (if n < n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p')) |
151 (if n < n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p')) |
153 else if n' < n then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p') |
152 else if n' < n then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p') |
154 else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))" |
153 else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))" |
155 | "polymul a b = Mul a b" |
154 | "polymul a b = Mul a b" |
156 |
155 |
157 declare if_cong[fundef_cong] |
156 declare if_cong[fundef_cong] |
158 declare let_cong[fundef_cong] |
157 declare let_cong[fundef_cong] |
159 |
158 |
160 fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly" |
159 fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly" |
161 where |
160 where |
162 "polypow 0 = (\<lambda>p. (1)\<^sub>p)" |
161 "polypow 0 = (\<lambda>p. (1)\<^sub>p)" |
163 | "polypow n = |
162 | "polypow n = |
164 (\<lambda>p. |
163 (\<lambda>p. |
165 let |
164 let |
166 q = polypow (n div 2) p; |
165 q = polypow (n div 2) p; |
167 d = polymul q q |
166 d = polymul q q |
168 in if even n then d else polymul p d)" |
167 in if even n then d else polymul p d)" |
169 |
168 |
170 abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60) |
169 abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60) |
171 where "a ^\<^sub>p k \<equiv> polypow k a" |
170 where "a ^\<^sub>p k \<equiv> polypow k a" |
172 |
171 |
173 function polynate :: "poly \<Rightarrow> poly" |
172 function polynate :: "poly \<Rightarrow> poly" |
174 where |
173 where |
175 "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p" |
174 "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p" |
176 | "polynate (Add p q) = polynate p +\<^sub>p polynate q" |
175 | "polynate (Add p q) = polynate p +\<^sub>p polynate q" |
177 | "polynate (Sub p q) = polynate p -\<^sub>p polynate q" |
176 | "polynate (Sub p q) = polynate p -\<^sub>p polynate q" |
178 | "polynate (Mul p q) = polynate p *\<^sub>p polynate q" |
177 | "polynate (Mul p q) = polynate p *\<^sub>p polynate q" |
179 | "polynate (Neg p) = ~\<^sub>p (polynate p)" |
178 | "polynate (Neg p) = ~\<^sub>p (polynate p)" |
180 | "polynate (Pw p n) = polynate p ^\<^sub>p n" |
179 | "polynate (Pw p n) = polynate p ^\<^sub>p n" |
181 | "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))" |
180 | "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))" |
182 | "polynate (C c) = C (normNum c)" |
181 | "polynate (C c) = C (normNum c)" |
183 by pat_completeness auto |
182 by pat_completeness auto |
184 termination by (relation "measure polysize") auto |
183 termination by (relation "measure polysize") auto |
185 |
184 |
186 fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" |
185 fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" |
187 where |
186 where |
188 "poly_cmul y (C x) = C (y *\<^sub>N x)" |
187 "poly_cmul y (C x) = C (y *\<^sub>N x)" |
189 | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)" |
188 | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)" |
190 | "poly_cmul y p = C y *\<^sub>p p" |
189 | "poly_cmul y p = C y *\<^sub>p p" |
191 |
190 |
192 definition monic :: "poly \<Rightarrow> poly \<times> bool" |
191 definition monic :: "poly \<Rightarrow> poly \<times> bool" |
193 where |
192 where "monic p = |
194 "monic p = |
|
195 (let h = headconst p |
193 (let h = headconst p |
196 in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))" |
194 in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))" |
197 |
195 |
198 |
196 |
199 subsection \<open>Pseudo-division\<close> |
197 subsection \<open>Pseudo-division\<close> |
222 |
220 |
223 definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> nat \<times> poly" |
221 definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> nat \<times> poly" |
224 where "polydivide s p = polydivide_aux (head p) (degree p) p 0 s" |
222 where "polydivide s p = polydivide_aux (head p) (degree p) p 0 s" |
225 |
223 |
226 fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" |
224 fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" |
227 where |
225 where |
228 "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)" |
226 "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)" |
229 | "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p" |
227 | "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p" |
230 |
228 |
231 fun poly_deriv :: "poly \<Rightarrow> poly" |
229 fun poly_deriv :: "poly \<Rightarrow> poly" |
232 where |
230 where |
233 "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p" |
231 "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p" |
234 | "poly_deriv p = 0\<^sub>p" |
232 | "poly_deriv p = 0\<^sub>p" |
235 |
233 |
236 |
234 |
237 subsection \<open>Semantics of the polynomial representation\<close> |
235 subsection \<open>Semantics of the polynomial representation\<close> |
238 |
236 |
239 primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}" |
237 primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}" |
240 where |
238 where |
241 "Ipoly bs (C c) = INum c" |
239 "Ipoly bs (C c) = INum c" |
242 | "Ipoly bs (Bound n) = bs!n" |
240 | "Ipoly bs (Bound n) = bs!n" |
243 | "Ipoly bs (Neg a) = - Ipoly bs a" |
241 | "Ipoly bs (Neg a) = - Ipoly bs a" |
244 | "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b" |
242 | "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b" |
245 | "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b" |
243 | "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b" |
246 | "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b" |
244 | "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b" |
247 | "Ipoly bs (Pw t n) = Ipoly bs t ^ n" |
245 | "Ipoly bs (Pw t n) = Ipoly bs t ^ n" |
248 | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p" |
246 | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p" |
249 |
247 |
250 abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>") |
248 abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>") |
251 where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p" |
249 where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p" |
252 |
250 |
253 lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i" |
251 lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i" |
510 and np': "isnpolyh p' n'" |
508 and np': "isnpolyh p' n'" |
511 and nc': "isnpolyh c' (Suc n')" |
509 and nc': "isnpolyh c' (Suc n')" |
512 and nn0: "n \<ge> n0" |
510 and nn0: "n \<ge> n0" |
513 and nn1: "n' \<ge> n1" |
511 and nn1: "n' \<ge> n1" |
514 by simp_all |
512 by simp_all |
515 { |
513 consider "n < n'" | "n' < n" | "n' = n" by arith |
516 assume "n < n'" |
514 then show ?case |
|
515 proof cases |
|
516 case 1 |
517 with "4.hyps"(4-5)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp |
517 with "4.hyps"(4-5)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp |
518 have ?case by (simp add: min_def) |
518 show ?thesis by (simp add: min_def) |
519 } moreover { |
519 next |
520 assume "n' < n" |
520 case 2 |
521 with "4.hyps"(16-17)[OF cnp np', of "n'"] and "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp' |
521 with "4.hyps"(16-17)[OF cnp np', of "n'"] and "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp' |
522 have ?case by (cases "Suc n' = n") (simp_all add: min_def) |
522 show ?thesis by (cases "Suc n' = n") (simp_all add: min_def) |
523 } moreover { |
523 next |
524 assume "n' = n" |
524 case 3 |
525 with "4.hyps"(16-17)[OF cnp np', of n] and "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0 |
525 with "4.hyps"(16-17)[OF cnp np', of n] and "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0 |
526 have ?case |
526 show ?thesis |
527 apply (auto intro!: polyadd_normh) |
527 by (auto intro!: polyadd_normh) (simp_all add: min_def isnpolyh_mono[OF nn0]) |
528 apply (simp_all add: min_def isnpolyh_mono[OF nn0]) |
528 qed |
529 done |
|
530 } |
|
531 ultimately show ?case by arith |
|
532 next |
529 next |
533 fix n0 n1 m |
530 fix n0 n1 m |
534 assume np: "isnpolyh ?cnp n0" |
531 assume np: "isnpolyh ?cnp n0" |
535 assume np':"isnpolyh ?cnp' n1" |
532 assume np':"isnpolyh ?cnp' n1" |
536 assume m: "m \<le> min n0 n1" |
533 assume m: "m \<le> min n0 n1" |
537 let ?d = "degreen (?cnp *\<^sub>p ?cnp') m" |
534 let ?d = "degreen (?cnp *\<^sub>p ?cnp') m" |
538 let ?d1 = "degreen ?cnp m" |
535 let ?d1 = "degreen ?cnp m" |
539 let ?d2 = "degreen ?cnp' m" |
536 let ?d2 = "degreen ?cnp' m" |
540 let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)" |
537 let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)" |
541 have "n' < n \<or> n < n' \<or> n' = n" by auto |
538 consider "n' < n \<or> n < n'" | "n' = n" by linarith |
542 moreover |
539 then show ?eq |
543 { |
540 proof cases |
544 assume "n' < n \<or> n < n'" |
541 case 1 |
545 with "4.hyps"(3,6,18) np np' m have ?eq |
542 with "4.hyps"(3,6,18) np np' m show ?thesis by auto |
546 by auto |
543 next |
547 } |
544 case 2 |
548 moreover |
545 have nn': "n' = n" by fact |
549 { |
|
550 assume nn': "n' = n" |
|
551 then have nn: "\<not> n' < n \<and> \<not> n < n'" by arith |
546 then have nn: "\<not> n' < n \<and> \<not> n < n'" by arith |
552 from "4.hyps"(16,18)[of n n' n] |
547 from "4.hyps"(16,18)[of n n' n] |
553 "4.hyps"(13,14)[of n "Suc n'" n] |
548 "4.hyps"(13,14)[of n "Suc n'" n] |
554 np np' nn' |
549 np np' nn' |
555 have norm: |
550 have norm: |
745 by (induct p q arbitrary: n0 n1 rule:polyadd.induct) |
738 by (induct p q arbitrary: n0 n1 rule:polyadd.induct) |
746 (auto simp: Nsub0[simplified Nsub_def] Let_def) |
739 (auto simp: Nsub0[simplified Nsub_def] Let_def) |
747 |
740 |
748 text \<open>polypow is a power function and preserves normal forms\<close> |
741 text \<open>polypow is a power function and preserves normal forms\<close> |
749 |
742 |
750 lemma polypow[simp]: |
743 lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n" |
751 "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n" |
|
752 proof (induct n rule: polypow.induct) |
744 proof (induct n rule: polypow.induct) |
753 case 1 |
745 case 1 |
754 then show ?case |
746 then show ?case by simp |
755 by simp |
|
756 next |
747 next |
757 case (2 n) |
748 case (2 n) |
758 let ?q = "polypow ((Suc n) div 2) p" |
749 let ?q = "polypow ((Suc n) div 2) p" |
759 let ?d = "polymul ?q ?q" |
750 let ?d = "polymul ?q ?q" |
760 have "odd (Suc n) \<or> even (Suc n)" |
751 consider "odd (Suc n)" | "even (Suc n)" by auto |
761 by simp |
752 then show ?case |
762 moreover |
753 proof cases |
763 { |
754 case odd: 1 |
764 assume odd: "odd (Suc n)" |
755 have *: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1" |
765 have th: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1" |
|
766 by arith |
756 by arith |
767 from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" |
757 from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" |
768 by (simp add: Let_def) |
758 by (simp add: Let_def) |
769 also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2) * (Ipoly bs p)^(Suc n div 2)" |
759 also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2) * (Ipoly bs p)^(Suc n div 2)" |
770 using "2.hyps" by simp |
760 using "2.hyps" by simp |
771 also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)" |
761 also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)" |
772 by (simp only: power_add power_one_right) simp |
762 by (simp only: power_add power_one_right) simp |
773 also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))" |
763 also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))" |
774 by (simp only: th) |
764 by (simp only: *) |
775 finally have ?case unfolding numeral_2_eq_2 [symmetric] |
765 finally show ?thesis |
776 using odd_two_times_div_two_nat [OF odd] by simp |
766 unfolding numeral_2_eq_2 [symmetric] |
777 } |
767 using odd_two_times_div_two_nat [OF odd] by simp |
778 moreover |
768 next |
779 { |
769 case even: 2 |
780 assume even: "even (Suc n)" |
|
781 from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" |
770 from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" |
782 by (simp add: Let_def) |
771 by (simp add: Let_def) |
783 also have "\<dots> = (Ipoly bs p) ^ (2 * (Suc n div 2))" |
772 also have "\<dots> = (Ipoly bs p) ^ (2 * (Suc n div 2))" |
784 using "2.hyps" by (simp only: mult_2 power_add) simp |
773 using "2.hyps" by (simp only: mult_2 power_add) simp |
785 finally have ?case using even_two_times_div_two [OF even] |
774 finally show ?thesis |
786 by simp |
775 using even_two_times_div_two [OF even] by simp |
787 } |
776 qed |
788 ultimately show ?case by blast |
|
789 qed |
777 qed |
790 |
778 |
791 lemma polypow_normh: |
779 lemma polypow_normh: |
792 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
780 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
793 shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n" |
781 shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n" |
796 then show ?case by auto |
784 then show ?case by auto |
797 next |
785 next |
798 case (2 k n) |
786 case (2 k n) |
799 let ?q = "polypow (Suc k div 2) p" |
787 let ?q = "polypow (Suc k div 2) p" |
800 let ?d = "polymul ?q ?q" |
788 let ?d = "polymul ?q ?q" |
801 from 2 have th1: "isnpolyh ?q n" and th2: "isnpolyh p n" |
789 from 2 have *: "isnpolyh ?q n" and **: "isnpolyh p n" |
802 by blast+ |
790 by blast+ |
803 from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" |
791 from polymul_normh[OF * *] have dn: "isnpolyh ?d n" |
804 by simp |
792 by simp |
805 from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" |
793 from polymul_normh[OF ** dn] have on: "isnpolyh (polymul p ?d) n" |
806 by simp |
794 by simp |
807 from dn on show ?case by (simp, unfold Let_def) auto |
795 from dn on show ?case by (simp, unfold Let_def) auto |
808 |
|
809 qed |
796 qed |
810 |
797 |
811 lemma polypow_norm: |
798 lemma polypow_norm: |
812 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
799 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
813 shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)" |
800 shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)" |
814 by (simp add: polypow_normh isnpoly_def) |
801 by (simp add: polypow_normh isnpoly_def) |
815 |
802 |
816 text \<open>Finally the whole normalization\<close> |
803 text \<open>Finally the whole normalization\<close> |
817 |
804 |
818 lemma polynate [simp]: |
805 lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})" |
819 "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})" |
|
820 by (induct p rule:polynate.induct) auto |
806 by (induct p rule:polynate.induct) auto |
821 |
807 |
822 lemma polynate_norm[simp]: |
808 lemma polynate_norm[simp]: |
823 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
809 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
824 shows "isnpoly (polynate p)" |
810 shows "isnpoly (polynate p)" |
825 by (induct p rule: polynate.induct) |
811 by (induct p rule: polynate.induct) |
826 (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm, |
812 (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm, |
827 simp_all add: isnpoly_def) |
813 simp_all add: isnpoly_def) |
828 |
814 |
829 text \<open>shift1\<close> |
815 text \<open>shift1\<close> |
830 |
|
831 |
816 |
832 lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" |
817 lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" |
833 by (simp add: shift1_def) |
818 by (simp add: shift1_def) |
834 |
819 |
835 lemma shift1_isnpoly: |
820 lemma shift1_isnpoly: |
943 |
928 |
944 lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p" |
929 lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p" |
945 by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0) |
930 by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0) |
946 |
931 |
947 primrec maxindex :: "poly \<Rightarrow> nat" |
932 primrec maxindex :: "poly \<Rightarrow> nat" |
948 where |
933 where |
949 "maxindex (Bound n) = n + 1" |
934 "maxindex (Bound n) = n + 1" |
950 | "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" |
935 | "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" |
951 | "maxindex (Add p q) = max (maxindex p) (maxindex q)" |
936 | "maxindex (Add p q) = max (maxindex p) (maxindex q)" |
952 | "maxindex (Sub p q) = max (maxindex p) (maxindex q)" |
937 | "maxindex (Sub p q) = max (maxindex p) (maxindex q)" |
953 | "maxindex (Mul p q) = max (maxindex p) (maxindex q)" |
938 | "maxindex (Mul p q) = max (maxindex p) (maxindex q)" |
954 | "maxindex (Neg p) = maxindex p" |
939 | "maxindex (Neg p) = maxindex p" |
955 | "maxindex (Pw p n) = maxindex p" |
940 | "maxindex (Pw p n) = maxindex p" |
956 | "maxindex (C x) = 0" |
941 | "maxindex (C x) = 0" |
957 |
942 |
958 definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool" |
943 definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool" |
959 where "wf_bs bs p \<longleftrightarrow> length bs \<ge> maxindex p" |
944 where "wf_bs bs p \<longleftrightarrow> length bs \<ge> maxindex p" |
960 |
945 |
961 lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall>c \<in> set (coefficients p). wf_bs bs c" |
946 lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall>c \<in> set (coefficients p). wf_bs bs c" |
962 proof (induct p rule: coefficients.induct) |
947 proof (induct p rule: coefficients.induct) |
963 case (1 c p) |
948 case (1 c p) |
964 show ?case |
949 show ?case |
965 proof |
950 proof |
966 fix x |
951 fix x |
967 assume xc: "x \<in> set (coefficients (CN c 0 p))" |
952 assume "x \<in> set (coefficients (CN c 0 p))" |
968 then have "x = c \<or> x \<in> set (coefficients p)" |
953 then consider "x = c" | "x \<in> set (coefficients p)" |
969 by simp |
954 by auto |
970 moreover |
955 then show "wf_bs bs x" |
971 { |
956 proof cases |
972 assume "x = c" |
957 case prems: 1 |
973 then have "wf_bs bs x" |
958 then show ?thesis |
974 using "1.prems" unfolding wf_bs_def by simp |
959 using "1.prems" by (simp add: wf_bs_def) |
975 } |
960 next |
976 moreover |
961 case prems: 2 |
977 { |
|
978 assume H: "x \<in> set (coefficients p)" |
|
979 from "1.prems" have "wf_bs bs p" |
962 from "1.prems" have "wf_bs bs p" |
980 unfolding wf_bs_def by simp |
963 by (simp add: wf_bs_def) |
981 with "1.hyps" H have "wf_bs bs x" |
964 with "1.hyps" prems show ?thesis |
982 by blast |
965 by blast |
983 } |
966 qed |
984 ultimately show "wf_bs bs x" |
|
985 by blast |
|
986 qed |
967 qed |
987 qed simp_all |
968 qed simp_all |
988 |
969 |
989 lemma maxindex_coefficients: "\<forall>c \<in> set (coefficients p). maxindex c \<le> maxindex p" |
970 lemma maxindex_coefficients: "\<forall>c \<in> set (coefficients p). maxindex c \<le> maxindex p" |
990 by (induct p rule: coefficients.induct) auto |
971 by (induct p rule: coefficients.induct) auto |
991 |
972 |
992 lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> Ipoly (bs @ bs') p = Ipoly bs p" |
973 lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> Ipoly (bs @ bs') p = Ipoly bs p" |
993 unfolding wf_bs_def by (induct p) (auto simp add: nth_append) |
974 by (induct p) (auto simp add: nth_append wf_bs_def) |
994 |
975 |
995 lemma take_maxindex_wf: |
976 lemma take_maxindex_wf: |
996 assumes wf: "wf_bs bs p" |
977 assumes wf: "wf_bs bs p" |
997 shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p" |
978 shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p" |
998 proof - |
979 proof - |
1200 then have "poly (polypoly' (?ts @ xs) p) = poly []" |
1174 then have "poly (polypoly' (?ts @ xs) p) = poly []" |
1201 by auto |
1175 by auto |
1202 then have "\<forall>c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0" |
1176 then have "\<forall>c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0" |
1203 using poly_zero[where ?'a='a] by (simp add: polypoly'_def) |
1177 using poly_zero[where ?'a='a] by (simp add: polypoly'_def) |
1204 with coefficients_head[of p, symmetric] |
1178 with coefficients_head[of p, symmetric] |
1205 have th0: "Ipoly (?ts @ xs) ?hd = 0" |
1179 have *: "Ipoly (?ts @ xs) ?hd = 0" |
1206 by simp |
1180 by simp |
1207 from bs have wf'': "wf_bs ?ts ?hd" |
1181 from bs have wf'': "wf_bs ?ts ?hd" |
1208 unfolding wf_bs_def by simp |
1182 by (simp add: wf_bs_def) |
1209 with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" |
1183 with * wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" |
1210 by simp |
1184 by simp |
1211 with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" |
1185 with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq show ?thesis |
1212 by simp |
1186 by simp |
1213 } |
1187 qed |
1214 then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" |
1188 then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" |
1215 by blast |
1189 by blast |
1216 from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" |
1190 from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" |
1217 by blast |
1191 by blast |
1218 then have "?h = 0\<^sub>p" by simp |
1192 then have "?h = 0\<^sub>p" by simp |
1219 with head_nz[OF np] have "p = 0\<^sub>p" by simp |
1193 with head_nz[OF np] show ?thesis by simp |
1220 } |
1194 qed |
1221 ultimately show "p = 0\<^sub>p" |
|
1222 by blast |
|
1223 qed |
1195 qed |
1224 |
1196 |
1225 lemma isnpolyh_unique: |
1197 lemma isnpolyh_unique: |
1226 assumes np: "isnpolyh p n0" |
1198 assumes np: "isnpolyh p n0" |
1227 and nq: "isnpolyh q n1" |
1199 and nq: "isnpolyh q n1" |
1228 shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field,power})) \<longleftrightarrow> p = q" |
1200 shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field,power})) \<longleftrightarrow> p = q" |
1229 proof auto |
1201 proof auto |
1230 assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>" |
1202 assume "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>" |
1231 then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" |
1203 then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" |
1232 by simp |
1204 by simp |
1233 then have "\<forall>bs. wf_bs bs (p -\<^sub>p q) \<longrightarrow> \<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" |
1205 then have "\<forall>bs. wf_bs bs (p -\<^sub>p q) \<longrightarrow> \<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" |
1234 using wf_bs_polysub[where p=p and q=q] by auto |
1206 using wf_bs_polysub[where p=p and q=q] by auto |
1235 with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] show "p = q" |
1207 with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] show "p = q" |
1236 by blast |
1208 by blast |
1237 qed |
1209 qed |
1238 |
1210 |
1239 |
1211 |
1240 text \<open>consequences of unicity on the algorithms for polynomial normalization\<close> |
1212 text \<open>Consequences of unicity on the algorithms for polynomial normalization.\<close> |
1241 |
1213 |
1242 lemma polyadd_commute: |
1214 lemma polyadd_commute: |
1243 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
1215 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
1244 and np: "isnpolyh p n0" |
1216 and np: "isnpolyh p n0" |
1245 and nq: "isnpolyh q n1" |
1217 and nq: "isnpolyh q n1" |
1393 from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' |
1365 from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' |
1394 have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0" |
1366 have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0" |
1395 by simp |
1367 by simp |
1396 from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" |
1368 from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" |
1397 by auto |
1369 by auto |
1398 have "n = n' \<or> n < n' \<or> n > n'" |
1370 consider "n = n'" | "n < n'" | "n > n'" |
1399 by arith |
1371 by arith |
1400 moreover |
1372 then show ?case |
1401 { |
1373 proof cases |
1402 assume nn': "n = n'" |
1374 case nn': 1 |
1403 have "n = 0 \<or> n > 0" by arith |
1375 consider "n = 0" | "n > 0" by arith |
1404 moreover |
1376 then show ?thesis |
1405 { |
1377 proof cases |
1406 assume nz: "n = 0" |
1378 case 1 |
1407 then have ?case using 4 nn' |
1379 with 4 nn' show ?thesis |
1408 by (auto simp add: Let_def degcmc') |
1380 by (auto simp add: Let_def degcmc') |
1409 } |
1381 next |
1410 moreover |
1382 case 2 |
1411 { |
1383 with nn' H(3) have "c = c'" and "p = p'" |
1412 assume nz: "n > 0" |
1384 by (cases n; auto)+ |
1413 with nn' H(3) have cc': "c = c'" and pp': "p = p'" |
1385 with nn' 4 show ?thesis |
1414 by (cases n, auto)+ |
|
1415 then have ?case |
|
1416 using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] |
1386 using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] |
1417 using polysub_same_0[OF c'nh, simplified polysub_def] |
1387 using polysub_same_0[OF c'nh, simplified polysub_def] |
1418 using nn' 4 by (simp add: Let_def) |
1388 by (simp add: Let_def) |
1419 } |
1389 qed |
1420 ultimately have ?case by blast |
1390 next |
1421 } |
1391 case nn': 2 |
1422 moreover |
|
1423 { |
|
1424 assume nn': "n < n'" |
|
1425 then have n'p: "n' > 0" |
1392 then have n'p: "n' > 0" |
1426 by simp |
1393 by simp |
1427 then have headcnp':"head (CN c' n' p') = CN c' n' p'" |
1394 then have headcnp':"head (CN c' n' p') = CN c' n' p'" |
1428 by (cases n') simp_all |
1395 by (cases n') simp_all |
1429 have degcnp': "degree (CN c' n' p') = 0" |
1396 with 4 nn' have degcnp': "degree (CN c' n' p') = 0" |
1430 and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" |
1397 and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" |
1431 using 4 nn' by (cases n', simp_all) |
1398 by (cases n', simp_all) |
1432 then have "n > 0" |
1399 then have "n > 0" |
1433 by (cases n) simp_all |
1400 by (cases n) simp_all |
1434 then have headcnp: "head (CN c n p) = CN c n p" |
1401 then have headcnp: "head (CN c n p) = CN c n p" |
1435 by (cases n) auto |
1402 by (cases n) auto |
1436 from H(3) headcnp headcnp' nn' have ?case |
1403 from H(3) headcnp headcnp' nn' show ?thesis |
1437 by auto |
1404 by auto |
1438 } |
1405 next |
1439 moreover |
1406 case nn': 3 |
1440 { |
|
1441 assume nn': "n > n'" |
|
1442 then have np: "n > 0" by simp |
1407 then have np: "n > 0" by simp |
1443 then have headcnp:"head (CN c n p) = CN c n p" |
1408 then have headcnp:"head (CN c n p) = CN c n p" |
1444 by (cases n) simp_all |
1409 by (cases n) simp_all |
1445 from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" |
1410 from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" |
1446 by simp |
1411 by simp |
1531 next |
1495 next |
1532 case (4 c n p c' n' p' n0 n1) |
1496 case (4 c n p c' n' p' n0 n1) |
1533 then have norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')" |
1497 then have norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')" |
1534 "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'" |
1498 "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'" |
1535 by simp_all |
1499 by simp_all |
1536 have "n < n' \<or> n' < n \<or> n = n'" by arith |
1500 consider "n < n'" | "n' < n" | "n' = n" by arith |
1537 moreover |
1501 then show ?case |
1538 { |
1502 proof cases |
1539 assume nn': "n < n'" |
1503 case nn': 1 |
1540 then have ?case |
1504 then show ?thesis |
1541 using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)] |
1505 using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)] |
1542 apply simp |
1506 apply simp |
1543 apply (cases n) |
1507 apply (cases n) |
1544 apply simp |
1508 apply simp |
1545 apply (cases n') |
1509 apply (cases n') |
1546 apply simp_all |
1510 apply simp_all |
1547 done |
1511 done |
1548 } |
1512 next |
1549 moreover { |
1513 case nn': 2 |
1550 assume nn': "n'< n" |
1514 then show ?thesis |
1551 then have ?case |
|
1552 using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] |
1515 using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] |
1553 apply simp |
1516 apply simp |
1554 apply (cases n') |
1517 apply (cases n') |
1555 apply simp |
1518 apply simp |
1556 apply (cases n) |
1519 apply (cases n) |
1557 apply auto |
1520 apply auto |
1558 done |
1521 done |
1559 } |
1522 next |
1560 moreover |
1523 case nn': 3 |
1561 { |
|
1562 assume nn': "n' = n" |
|
1563 from nn' polymul_normh[OF norm(5,4)] |
1524 from nn' polymul_normh[OF norm(5,4)] |
1564 have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def) |
1525 have ncnpc': "isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def) |
1565 from nn' polymul_normh[OF norm(5,3)] norm |
1526 from nn' polymul_normh[OF norm(5,3)] norm |
1566 have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp |
1527 have ncnpp': "isnpolyh (CN c n p *\<^sub>p p') n" by simp |
1567 from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6) |
1528 from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6) |
1568 have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp |
1529 have ncnpp0': "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp |
1569 from polyadd_normh[OF ncnpc' ncnpp0'] |
1530 from polyadd_normh[OF ncnpc' ncnpp0'] |
1570 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" |
1531 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" |
1571 by (simp add: min_def) |
1532 by (simp add: min_def) |
1572 { |
1533 consider "n > 0" | "n = 0" by auto |
1573 assume np: "n > 0" |
1534 then show ?thesis |
|
1535 proof cases |
|
1536 case np: 1 |
1574 with nn' head_isnpolyh_Suc'[OF np nth] |
1537 with nn' head_isnpolyh_Suc'[OF np nth] |
1575 head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']] |
1538 head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']] |
1576 have ?case by simp |
1539 show ?thesis by simp |
1577 } |
1540 next |
1578 moreover |
1541 case nz: 2 |
1579 { |
|
1580 assume nz: "n = 0" |
|
1581 from polymul_degreen[OF norm(5,4), where m="0"] |
1542 from polymul_degreen[OF norm(5,4), where m="0"] |
1582 polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0 |
1543 polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0 |
1583 norm(5,6) degree_npolyhCN[OF norm(6)] |
1544 norm(5,6) degree_npolyhCN[OF norm(6)] |
1584 have dth: "degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" |
1545 have dth: "degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" |
1585 by simp |
1546 by simp |
1586 then have dth': "degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" |
1547 then have dth': "degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" |
1587 by simp |
1548 by simp |
1588 from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth |
1549 from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth |
1589 have ?case |
1550 show ?thesis |
1590 using norm "4.hyps"(6)[OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] nn' nz |
1551 using norm "4.hyps"(6)[OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] nn' nz |
1591 by simp |
1552 by simp |
1592 } |
1553 qed |
1593 ultimately have ?case |
1554 qed |
1594 by (cases n) auto |
|
1595 } |
|
1596 ultimately show ?case by blast |
|
1597 qed simp_all |
1555 qed simp_all |
1598 |
1556 |
1599 lemma degree_coefficients: "degree p = length (coefficients p) - 1" |
1557 lemma degree_coefficients: "degree p = length (coefficients p) - 1" |
1600 by (induct p rule: degree.induct) auto |
1558 by (induct p rule: degree.induct) auto |
1601 |
1559 |
1661 using funpow_shift1_head[OF np pnz] by simp |
1619 using funpow_shift1_head[OF np pnz] by simp |
1662 from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" |
1620 from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" |
1663 by (simp add: isnpoly_def) |
1621 by (simp add: isnpoly_def) |
1664 from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap |
1622 from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap |
1665 have nakk':"isnpolyh ?akk' 0" by blast |
1623 have nakk':"isnpolyh ?akk' 0" by blast |
1666 { |
1624 show ?ths |
1667 assume sz: "s = 0\<^sub>p" |
1625 proof (cases "s = 0\<^sub>p") |
1668 then have ?ths |
1626 case True |
1669 using np polydivide_aux.simps |
1627 with np show ?thesis |
1670 apply clarsimp |
1628 apply (clarsimp simp: polydivide_aux.simps) |
1671 apply (rule exI[where x="0\<^sub>p"]) |
1629 apply (rule exI[where x="0\<^sub>p"]) |
1672 apply simp |
1630 apply simp |
1673 done |
1631 done |
1674 } |
1632 next |
1675 moreover |
1633 case sz: False |
1676 { |
1634 show ?thesis |
1677 assume sz: "s \<noteq> 0\<^sub>p" |
1635 proof (cases "degree s < n") |
1678 { |
1636 case True |
1679 assume dn: "degree s < n" |
1637 then show ?thesis |
1680 then have "?ths" |
|
1681 using ns ndp np polydivide_aux.simps |
1638 using ns ndp np polydivide_aux.simps |
1682 apply auto |
1639 apply auto |
1683 apply (rule exI[where x="0\<^sub>p"]) |
1640 apply (rule exI[where x="0\<^sub>p"]) |
1684 apply simp |
1641 apply simp |
1685 done |
1642 done |
1686 } |
1643 next |
1687 moreover |
1644 case dn': False |
1688 { |
|
1689 assume dn': "\<not> degree s < n" |
|
1690 then have dn: "degree s \<ge> n" |
1645 then have dn: "degree s \<ge> n" |
1691 by arith |
1646 by arith |
1692 have degsp': "degree s = degree ?p'" |
1647 have degsp': "degree s = degree ?p'" |
1693 using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] |
1648 using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] |
1694 by simp |
1649 by simp |
1695 { |
1650 show ?thesis |
1696 assume ba: "?b = a" |
1651 proof (cases "?b = a") |
|
1652 case ba: True |
1697 then have headsp': "head s = head ?p'" |
1653 then have headsp': "head s = head ?p'" |
1698 using ap headp' by simp |
1654 using ap headp' by simp |
1699 have nr: "isnpolyh (s -\<^sub>p ?p') 0" |
1655 have nr: "isnpolyh (s -\<^sub>p ?p') 0" |
1700 using polysub_normh[OF ns np'] by simp |
1656 using polysub_normh[OF ns np'] by simp |
1701 from degree_polysub_samehead[OF ns np' headsp' degsp'] |
1657 from degree_polysub_samehead[OF ns np' headsp' degsp'] |
1702 have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" |
1658 consider "degree (s -\<^sub>p ?p') < degree s" | "s -\<^sub>p ?p' = 0\<^sub>p" by auto |
1703 by simp |
1659 then show ?thesis |
1704 moreover |
1660 proof cases |
1705 { |
1661 case deglt: 1 |
1706 assume deglt:"degree (s -\<^sub>p ?p') < degree s" |
|
1707 from polydivide_aux.simps sz dn' ba |
1662 from polydivide_aux.simps sz dn' ba |
1708 have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" |
1663 have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" |
1709 by (simp add: Let_def) |
1664 by (simp add: Let_def) |
1710 { |
1665 have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths" |
1711 assume h1: "polydivide_aux a n p k s = (k', r)" |
1666 if h1: "polydivide_aux a n p k s = (k', r)" |
|
1667 proof - |
1712 from less(1)[OF deglt nr, of k k' r] trans[OF eq[symmetric] h1] |
1668 from less(1)[OF deglt nr, of k k' r] trans[OF eq[symmetric] h1] |
1713 have kk': "k \<le> k'" |
1669 have kk': "k \<le> k'" |
1714 and nr: "\<exists>nr. isnpolyh r nr" |
1670 and nr: "\<exists>nr. isnpolyh r nr" |
1715 and dr: "degree r = 0 \<or> degree r < degree p" |
1671 and dr: "degree r = 0 \<or> degree r < degree p" |
1716 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" |
1672 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" |
1751 by simp |
1707 by simp |
1752 with isnpolyh_unique[OF nakks' nqr'] |
1708 with isnpolyh_unique[OF nakks' nqr'] |
1753 have "a ^\<^sub>p (k' - k) *\<^sub>p s = |
1709 have "a ^\<^sub>p (k' - k) *\<^sub>p s = |
1754 p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r" |
1710 p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r" |
1755 by blast |
1711 by blast |
1756 then have ?qths using nq' |
1712 with nq' have ?qths |
1757 apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q" in exI) |
1713 apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q" in exI) |
1758 apply (rule_tac x="0" in exI) |
1714 apply (rule_tac x="0" in exI) |
1759 apply simp |
1715 apply simp |
1760 done |
1716 done |
1761 with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> |
1717 with kk' nr dr show ?thesis |
1762 (\<exists>nr. isnpolyh r nr) \<and> ?qths" |
|
1763 by blast |
1718 by blast |
1764 } |
1719 qed |
1765 then have ?ths by blast |
1720 then show ?thesis by blast |
1766 } |
1721 next |
1767 moreover |
1722 case spz: 2 |
1768 { |
|
1769 assume spz:"s -\<^sub>p ?p' = 0\<^sub>p" |
|
1770 from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"] |
1723 from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"] |
1771 have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'" |
1724 have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'" |
1772 by simp |
1725 by simp |
1773 then have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" |
1726 with np nxdn have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" |
1774 using np nxdn |
1727 by (simp only: funpow_shift1_1) simp |
1775 apply simp |
|
1776 apply (simp only: funpow_shift1_1) |
|
1777 apply simp |
|
1778 done |
|
1779 then have sp': "s = ?xdn *\<^sub>p p" |
1728 then have sp': "s = ?xdn *\<^sub>p p" |
1780 using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] |
1729 using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] |
1781 by blast |
1730 by blast |
1782 { |
1731 have ?thesis if h1: "polydivide_aux a n p k s = (k', r)" |
1783 assume h1: "polydivide_aux a n p k s = (k', r)" |
1732 proof - |
1784 from polydivide_aux.simps sz dn' ba |
1733 from sz dn' ba |
1785 have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" |
1734 have "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" |
1786 by (simp add: Let_def) |
1735 by (simp add: Let_def polydivide_aux.simps) |
1787 also have "\<dots> = (k,0\<^sub>p)" |
1736 also have "\<dots> = (k,0\<^sub>p)" |
1788 using polydivide_aux.simps spz by simp |
1737 using spz by (simp add: polydivide_aux.simps) |
1789 finally have "(k', r) = (k, 0\<^sub>p)" |
1738 finally have "(k', r) = (k, 0\<^sub>p)" |
1790 using h1 by simp |
1739 by (simp add: h1) |
1791 with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] |
1740 with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] |
1792 polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths |
1741 polyadd_0(2)[OF polymul_normh[OF np nxdn]] show ?thesis |
1793 apply auto |
1742 apply auto |
1794 apply (rule exI[where x="?xdn"]) |
1743 apply (rule exI[where x="?xdn"]) |
1795 apply (auto simp add: polymul_commute[of p]) |
1744 apply (auto simp add: polymul_commute[of p]) |
1796 done |
1745 done |
1797 } |
1746 qed |
1798 } |
1747 then show ?thesis by blast |
1799 ultimately have ?ths by blast |
1748 qed |
1800 } |
1749 next |
1801 moreover |
1750 case ba: False |
1802 { |
|
1803 assume ba: "?b \<noteq> a" |
|
1804 from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] |
1751 from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] |
1805 polymul_normh[OF head_isnpolyh[OF ns] np']] |
1752 polymul_normh[OF head_isnpolyh[OF ns] np']] |
1806 have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" |
1753 have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" |
1807 by (simp add: min_def) |
1754 by (simp add: min_def) |
1808 have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p" |
1755 have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p" |
1809 using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] |
1756 using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] |
1810 polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns] |
1757 polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns] |
1811 funpow_shift1_nz[OF pnz] |
1758 funpow_shift1_nz[OF pnz] |
1812 by simp_all |
1759 by simp_all |
1813 from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz |
1760 from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz |
1814 polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="degree s - n"] |
1761 polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz |
|
1762 funpow_shift1_nz[OF pnz, where n="degree s - n"] |
1815 have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" |
1763 have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" |
1816 using head_head[OF ns] funpow_shift1_head[OF np pnz] |
1764 using head_head[OF ns] funpow_shift1_head[OF np pnz] |
1817 polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]] |
1765 polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]] |
1818 by (simp add: ap) |
1766 by (simp add: ap) |
1819 from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] |
1767 from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] |
1841 and dr: "degree r = 0 \<or> degree r < degree p" |
1797 and dr: "degree r = 0 \<or> degree r < degree p" |
1842 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" |
1798 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" |
1843 by auto |
1799 by auto |
1844 from kk' have kk'': "Suc (k' - Suc k) = k' - k" |
1800 from kk' have kk'': "Suc (k' - Suc k) = k' - k" |
1845 by arith |
1801 by arith |
1846 { |
1802 have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1847 fix bs :: "'a::{field_char_0,field} list" |
1803 Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" |
|
1804 for bs :: "'a::{field_char_0,field} list" |
|
1805 proof - |
1848 from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] |
1806 from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] |
1849 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)" |
1807 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)" |
1850 by simp |
1808 by simp |
1851 then have "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = |
1809 then have "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = |
1852 Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" |
1810 Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" |
1853 by (simp add: field_simps) |
1811 by (simp add: field_simps) |
1854 then have "Ipoly bs a ^ (k' - k) * Ipoly bs s = |
1812 then have "Ipoly bs a ^ (k' - k) * Ipoly bs s = |
1855 Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" |
1813 Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" |
1856 by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) |
1814 by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) |
1857 then have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1815 then show ?thesis |
1858 Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" |
|
1859 by (simp add: field_simps) |
1816 by (simp add: field_simps) |
1860 } |
1817 qed |
1861 then have ieq:"\<forall>bs :: 'a::{field_char_0,field} list. |
1818 then have ieq: "\<forall>bs :: 'a::{field_char_0,field} list. |
1862 Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1819 Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1863 Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" |
1820 Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" |
1864 by auto |
1821 by auto |
1865 let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)" |
1822 let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)" |
1866 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]] |
1823 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]] |
1867 have nqw: "isnpolyh ?q 0" |
1824 have nqw: "isnpolyh ?q 0" |
1868 by simp |
1825 by simp |
1869 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]] |
1826 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]] |
1870 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" |
1827 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" |
1871 by blast |
1828 by blast |
1872 from dr kk' nr h1 asth nqw have ?ths |
1829 from dr kk' nr h1 asth nqw show ?thesis |
1873 apply simp |
1830 apply simp |
1874 apply (rule conjI) |
1831 apply (rule conjI) |
1875 apply (rule exI[where x="nr"], simp) |
1832 apply (rule exI[where x="nr"], simp) |
1876 apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp) |
1833 apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp) |
1877 apply (rule exI[where x="0"], simp) |
1834 apply (rule exI[where x="0"], simp) |
1878 done |
1835 done |
1879 } |
1836 qed |
1880 then have ?ths by blast |
1837 then show ?thesis by blast |
1881 } |
1838 next |
1882 moreover |
1839 case spz: 2 |
1883 { |
1840 have hth: "\<forall>bs :: 'a::{field_char_0,field} list. |
1884 assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p" |
1841 Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" |
1885 { |
1842 proof |
1886 fix bs :: "'a::{field_char_0,field} list" |
1843 fix bs :: "'a::{field_char_0,field} list" |
1887 from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz |
1844 from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz |
1888 have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" |
1845 have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" |
1889 by simp |
1846 by simp |
1890 then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" |
1847 then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" |
1891 by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) |
1848 by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) |
1892 then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" |
1849 then show "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" |
1893 by simp |
1850 by simp |
1894 } |
1851 qed |
1895 then have hth: "\<forall>bs :: 'a::{field_char_0,field} list. |
|
1896 Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. |
|
1897 from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" |
1852 from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" |
1898 using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] |
1853 using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] |
1899 polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]], |
1854 polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]], |
1900 simplified ap] |
1855 simplified ap] |
1901 by simp |
1856 by simp |
1902 { |
1857 have ?ths if h1: "polydivide_aux a n p k s = (k', r)" |
1903 assume h1: "polydivide_aux a n p k s = (k', r)" |
1858 proof - |
1904 from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps |
1859 from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps |
1905 have "(k', r) = (Suc k, 0\<^sub>p)" |
1860 have "(k', r) = (Suc k, 0\<^sub>p)" |
1906 by (simp add: Let_def) |
1861 by (simp add: Let_def) |
1907 with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] |
1862 with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] |
1908 polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq |
1863 polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq |
1909 have ?ths |
1864 show ?thesis |
1910 apply (clarsimp simp add: Let_def) |
1865 apply (clarsimp simp add: Let_def) |
1911 apply (rule exI[where x="?b *\<^sub>p ?xdn"]) |
1866 apply (rule exI[where x="?b *\<^sub>p ?xdn"]) |
1912 apply simp |
1867 apply simp |
1913 apply (rule exI[where x="0"], simp) |
1868 apply (rule exI[where x="0"], simp) |
1914 done |
1869 done |
1915 } |
1870 qed |
1916 then have ?ths by blast |
1871 then show ?thesis by blast |
1917 } |
1872 qed |
1918 ultimately have ?ths |
1873 qed |
1919 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"] |
1874 qed |
1920 head_nz[OF np] pnz sz ap[symmetric] |
1875 qed |
1921 by (auto simp add: degree_eq_degreen0[symmetric]) |
|
1922 } |
|
1923 ultimately have ?ths by blast |
|
1924 } |
|
1925 ultimately have ?ths by blast |
|
1926 } |
|
1927 ultimately show ?ths by blast |
|
1928 qed |
1876 qed |
1929 |
1877 |
1930 lemma polydivide_properties: |
1878 lemma polydivide_properties: |
1931 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
1879 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
1932 and np: "isnpolyh p n0" |
1880 and np: "isnpolyh p n0" |
1997 lemma isnonconstant_nonconstant: |
1945 lemma isnonconstant_nonconstant: |
1998 assumes "isnonconstant p" |
1946 assumes "isnonconstant p" |
1999 shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0" |
1947 shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0" |
2000 proof |
1948 proof |
2001 let ?p = "polypoly bs p" |
1949 let ?p = "polypoly bs p" |
2002 assume nc: "nonconstant ?p" |
1950 assume "nonconstant ?p" |
2003 from isnonconstant_pnormal_iff[OF assms, of bs] nc |
1951 with isnonconstant_pnormal_iff[OF assms, of bs] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
2004 show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
|
2005 unfolding nonconstant_def by blast |
1952 unfolding nonconstant_def by blast |
2006 next |
1953 next |
2007 let ?p = "polypoly bs p" |
1954 let ?p = "polypoly bs p" |
2008 assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
1955 assume "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
2009 from isnonconstant_pnormal_iff[OF assms, of bs] h |
1956 with isnonconstant_pnormal_iff[OF assms, of bs] have pn: "pnormal ?p" |
2010 have pn: "pnormal ?p" |
|
2011 by blast |
1957 by blast |
2012 { |
1958 have False if H: "?p = [x]" for x |
2013 fix x |
1959 proof - |
2014 assume H: "?p = [x]" |
|
2015 from H have "length (coefficients p) = 1" |
1960 from H have "length (coefficients p) = 1" |
2016 unfolding polypoly_def by auto |
1961 by (auto simp: polypoly_def) |
2017 with isnonconstant_coefficients_length[OF assms] |
1962 with isnonconstant_coefficients_length[OF assms] |
2018 have False by arith |
1963 show ?thesis by arith |
2019 } |
1964 qed |
2020 then show "nonconstant ?p" |
1965 then show "nonconstant ?p" |
2021 using pn unfolding nonconstant_def by blast |
1966 using pn unfolding nonconstant_def by blast |
2022 qed |
1967 qed |
2023 |
1968 |
2024 lemma pnormal_length: "p \<noteq> [] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p" |
1969 lemma pnormal_length: "p \<noteq> [] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p" |
2025 apply (induct p) |
1970 apply (induct p) |
2026 apply (simp_all add: pnormal_def) |
1971 apply (simp_all add: pnormal_def) |
2027 apply (case_tac "p = []") |
1972 apply (case_tac "p = []") |
2028 apply simp_all |
1973 apply simp_all |
2029 done |
1974 done |
2030 |
1975 |
2031 lemma degree_degree: |
1976 lemma degree_degree: |
2032 assumes "isnonconstant p" |
1977 assumes "isnonconstant p" |
2033 shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
1978 shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
|
1979 (is "?lhs \<longleftrightarrow> ?rhs") |
2034 proof |
1980 proof |
2035 let ?p = "polypoly bs p" |
1981 let ?p = "polypoly bs p" |
2036 assume H: "degree p = Polynomial_List.degree ?p" |
1982 { |
2037 from isnonconstant_coefficients_length[OF assms] have pz: "?p \<noteq> []" |
1983 assume ?lhs |
2038 unfolding polypoly_def by auto |
1984 from isnonconstant_coefficients_length[OF assms] have "?p \<noteq> []" |
2039 from H degree_coefficients[of p] isnonconstant_coefficients_length[OF assms] |
1985 by (auto simp: polypoly_def) |
2040 have lg: "length (pnormalize ?p) = length ?p" |
1986 from \<open>?lhs\<close> degree_coefficients[of p] isnonconstant_coefficients_length[OF assms] |
2041 unfolding Polynomial_List.degree_def polypoly_def by simp |
1987 have "length (pnormalize ?p) = length ?p" |
2042 then have "pnormal ?p" |
1988 by (simp add: Polynomial_List.degree_def polypoly_def) |
2043 using pnormal_length[OF pz] by blast |
1989 with pnormal_length[OF \<open>?p \<noteq> []\<close>] have "pnormal ?p" |
2044 with isnonconstant_pnormal_iff[OF assms] show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
1990 by blast |
2045 by blast |
1991 with isnonconstant_pnormal_iff[OF assms] show ?rhs |
2046 next |
1992 by blast |
2047 let ?p = "polypoly bs p" |
1993 next |
2048 assume H: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" |
1994 assume ?rhs |
2049 with isnonconstant_pnormal_iff[OF assms] have "pnormal ?p" |
1995 with isnonconstant_pnormal_iff[OF assms] have "pnormal ?p" |
2050 by blast |
1996 by blast |
2051 with degree_coefficients[of p] isnonconstant_coefficients_length[OF assms] |
1997 with degree_coefficients[of p] isnonconstant_coefficients_length[OF assms] show ?lhs |
2052 show "degree p = Polynomial_List.degree ?p" |
1998 by (auto simp: polypoly_def pnormal_def Polynomial_List.degree_def) |
2053 unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto |
1999 } |
2054 qed |
2000 qed |
2055 |
2001 |
2056 |
2002 |
2057 section \<open>Swaps ; Division by a certain variable\<close> |
2003 section \<open>Swaps -- division by a certain variable\<close> |
2058 |
2004 |
2059 primrec swap :: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" |
2005 primrec swap :: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" |
2060 where |
2006 where |
2061 "swap n m (C x) = C x" |
2007 "swap n m (C x) = C x" |
2062 | "swap n m (Bound k) = Bound (if k = n then m else if k = m then n else k)" |
2008 | "swap n m (Bound k) = Bound (if k = n then m else if k = m then n else k)" |
2063 | "swap n m (Neg t) = Neg (swap n m t)" |
2009 | "swap n m (Neg t) = Neg (swap n m t)" |
2064 | "swap n m (Add s t) = Add (swap n m s) (swap n m t)" |
2010 | "swap n m (Add s t) = Add (swap n m s) (swap n m t)" |
2065 | "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)" |
2011 | "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)" |
2066 | "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)" |
2012 | "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)" |
2067 | "swap n m (Pw t k) = Pw (swap n m t) k" |
2013 | "swap n m (Pw t k) = Pw (swap n m t) k" |
2068 | "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) (swap n m p)" |
2014 | "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) (swap n m p)" |
2069 |
2015 |
2070 lemma swap: |
2016 lemma swap: |
2071 assumes "n < length bs" |
2017 assumes "n < length bs" |
2072 and "m < length bs" |
2018 and "m < length bs" |
2073 shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" |
2019 shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" |