author  haftmann 
Mon, 26 Apr 2010 15:37:50 +0200  
changeset 36409  d323e7773aa8 
parent 36349  39be26d1bc28 
child 39246  9e58f0499f57 
permissions  rwrr 
33154  1 
(* Title: HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy 
2 
Author: Amine Chaieb 

3 
*) 

4 

35046  5 
header {* Implementation and verification of multivariate polynomials *} 
33154  6 

7 
theory Reflected_Multivariate_Polynomial 

35046  8 
imports Complex_Main Abstract_Rat Polynomial_List 
33154  9 
begin 
10 

35046  11 
(* Implementation *) 
33154  12 

13 
subsection{* Datatype of polynomial expressions *} 

14 

15 
datatype poly = C Num Bound nat Add poly polySub poly poly 

16 
 Mul poly poly Neg poly Pw poly nat CN poly nat poly 

17 

35054  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)" 

33154  20 

21 
subsection{* Boundedness, substitution and all that *} 

22 
consts polysize:: "poly \<Rightarrow> nat" 

23 
primrec 

24 
"polysize (C c) = 1" 

25 
"polysize (Bound n) = 1" 

26 
"polysize (Neg p) = 1 + polysize p" 

27 
"polysize (Add 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" 

30 
"polysize (Pw p n) = 1 + polysize p" 

31 
"polysize (CN c n p) = 4 + polysize c + polysize p" 

32 

33 
consts 

34 
polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) 

35 
polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) 

36 
primrec 

37 
"polybound0 (C c) = True" 

38 
"polybound0 (Bound n) = (n>0)" 

39 
"polybound0 (Neg a) = polybound0 a" 

40 
"polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)" 

41 
"polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" 

42 
"polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)" 

43 
"polybound0 (Pw p n) = (polybound0 p)" 

44 
"polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)" 

45 
primrec 

46 
"polysubst0 t (C c) = (C c)" 

47 
"polysubst0 t (Bound n) = (if n=0 then t else Bound n)" 

48 
"polysubst0 t (Neg a) = Neg (polysubst0 t a)" 

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

51 
"polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)" 

52 
"polysubst0 t (Pw p n) = Pw (polysubst0 t p) n" 

53 
"polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p)) 

54 
else CN (polysubst0 t c) n (polysubst0 t p))" 

55 

56 
consts 

57 
decrpoly:: "poly \<Rightarrow> poly" 

58 
recdef decrpoly "measure polysize" 

59 
"decrpoly (Bound n) = Bound (n  1)" 

60 
"decrpoly (Neg a) = Neg (decrpoly a)" 

61 
"decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)" 

62 
"decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)" 

63 
"decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)" 

64 
"decrpoly (Pw p n) = Pw (decrpoly p) n" 

65 
"decrpoly (CN c n p) = CN (decrpoly c) (n  1) (decrpoly p)" 

66 
"decrpoly a = a" 

67 

68 
subsection{* Degrees and heads and coefficients *} 

69 

70 
consts degree:: "poly \<Rightarrow> nat" 

71 
recdef degree "measure size" 

72 
"degree (CN c 0 p) = 1 + degree p" 

73 
"degree p = 0" 

74 
consts head:: "poly \<Rightarrow> poly" 

75 

76 
recdef head "measure size" 

77 
"head (CN c 0 p) = head p" 

78 
"head p = p" 

79 
(* More general notions of degree and head *) 

80 
consts degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat" 

81 
recdef degreen "measure size" 

82 
"degreen (CN c n p) = (\<lambda>m. if n=m then 1 + degreen p n else 0)" 

83 
"degreen p = (\<lambda>m. 0)" 

84 

85 
consts headn:: "poly \<Rightarrow> nat \<Rightarrow> poly" 

86 
recdef headn "measure size" 

87 
"headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)" 

88 
"headn p = (\<lambda>m. p)" 

89 

90 
consts coefficients:: "poly \<Rightarrow> poly list" 

91 
recdef coefficients "measure size" 

92 
"coefficients (CN c 0 p) = c#(coefficients p)" 

93 
"coefficients p = [p]" 

94 

95 
consts isconstant:: "poly \<Rightarrow> bool" 

96 
recdef isconstant "measure size" 

97 
"isconstant (CN c 0 p) = False" 

98 
"isconstant p = True" 

99 

100 
consts behead:: "poly \<Rightarrow> poly" 

101 
recdef behead "measure size" 

102 
"behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')" 

103 
"behead p = 0\<^sub>p" 

104 

105 
consts headconst:: "poly \<Rightarrow> Num" 

106 
recdef headconst "measure size" 

107 
"headconst (CN c n p) = headconst p" 

108 
"headconst (C n) = n" 

109 

110 
subsection{* Operations for normalization *} 

111 
consts 

112 
polyadd :: "poly\<times>poly \<Rightarrow> poly" 

113 
polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p") 

114 
polysub :: "poly\<times>poly \<Rightarrow> poly" 

115 
polymul :: "poly\<times>poly \<Rightarrow> poly" 

116 
polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly" 

35054  117 
abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60) 
118 
where "a +\<^sub>p b \<equiv> polyadd (a,b)" 

119 
abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60) 

120 
where "a *\<^sub>p b \<equiv> polymul (a,b)" 

121 
abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "\<^sub>p" 60) 

122 
where "a \<^sub>p b \<equiv> polysub (a,b)" 

123 
abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60) 

124 
where "a ^\<^sub>p k \<equiv> polypow k a" 

33154  125 

126 
recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)" 

127 
"polyadd (C c, C c') = C (c+\<^sub>Nc')" 

128 
"polyadd (C c, CN c' n' p') = CN (polyadd (C c, c')) n' p'" 

129 
"polyadd (CN c n p, C c') = CN (polyadd (c, C c')) n p" 

130 
stupid: "polyadd (CN c n p, CN c' n' p') = 

131 
(if n < n' then CN (polyadd(c,CN c' n' p')) n p 

132 
else if n'<n then CN (polyadd(CN c n p, c')) n' p' 

133 
else (let cc' = polyadd (c,c') ; 

134 
pp' = polyadd (p,p') 

135 
in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))" 

136 
"polyadd (a, b) = Add a b" 

137 
(hints recdef_simp add: Let_def measure_def split_def inv_image_def) 

138 

139 
(* 

140 
declare stupid [simp del, code del] 

141 

142 
lemma [simp,code]: "polyadd (CN c n p, CN c' n' p') = 

143 
(if n < n' then CN (polyadd(c,CN c' n' p')) n p 

144 
else if n'<n then CN (polyadd(CN c n p, c')) n' p' 

145 
else (let cc' = polyadd (c,c') ; 

146 
pp' = polyadd (p,p') 

147 
in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))" 

148 
by (simp add: Let_def stupid) 

149 
*) 

150 

151 
recdef polyneg "measure size" 

152 
"polyneg (C c) = C (~\<^sub>N c)" 

153 
"polyneg (CN c n p) = CN (polyneg c) n (polyneg p)" 

154 
"polyneg a = Neg a" 

155 

156 
defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd (p,polyneg q)" 

157 

158 
recdef polymul "measure (\<lambda>(a,b). size a + size b)" 

159 
"polymul(C c, C c') = C (c*\<^sub>Nc')" 

160 
"polymul(C c, CN c' n' p') = 

161 
(if c = 0\<^sub>N then 0\<^sub>p else CN (polymul(C c,c')) n' (polymul(C c, p')))" 

162 
"polymul(CN c n p, C c') = 

163 
(if c' = 0\<^sub>N then 0\<^sub>p else CN (polymul(c,C c')) n (polymul(p, C c')))" 

164 
"polymul(CN c n p, CN c' n' p') = 

165 
(if n<n' then CN (polymul(c,CN c' n' p')) n (polymul(p,CN c' n' p')) 

166 
else if n' < n 

167 
then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p')) 

168 
else polyadd(polymul(CN c n p, c'),CN 0\<^sub>p n' (polymul(CN c n p, p'))))" 

169 
"polymul (a,b) = Mul a b" 

170 
recdef polypow "measure id" 

171 
"polypow 0 = (\<lambda>p. 1\<^sub>p)" 

172 
"polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul(q,q) in 

173 
if even n then d else polymul(p,d))" 

174 

175 
consts polynate :: "poly \<Rightarrow> poly" 

176 
recdef polynate "measure polysize" 

177 
"polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p" 

178 
"polynate (Add p q) = (polynate p +\<^sub>p polynate q)" 

179 
"polynate (Sub p q) = (polynate p \<^sub>p polynate q)" 

180 
"polynate (Mul p q) = (polynate p *\<^sub>p polynate q)" 

181 
"polynate (Neg p) = (~\<^sub>p (polynate p))" 

182 
"polynate (Pw p n) = ((polynate p) ^\<^sub>p n)" 

183 
"polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))" 

184 
"polynate (C c) = C (normNum c)" 

185 

186 
fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" where 

187 
"poly_cmul y (C x) = C (y *\<^sub>N x)" 

188 
 "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)" 

189 
 "poly_cmul y p = C y *\<^sub>p p" 

190 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

191 
definition monic :: "poly \<Rightarrow> (poly \<times> bool)" where 
33154  192 
"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))" 
193 

194 
subsection{* Pseudodivision *} 

195 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

196 
definition shift1 :: "poly \<Rightarrow> poly" where 
33154  197 
"shift1 p \<equiv> CN 0\<^sub>p 0 p" 
198 
consts funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" 

199 

200 
primrec 

201 
"funpow 0 f x = x" 

202 
"funpow (Suc n) f x = funpow n f (f x)" 

203 
function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)" 

204 
where 

205 
"polydivide_aux (a,n,p,k,s) = 

206 
(if s = 0\<^sub>p then (k,s) 

207 
else (let b = head s; m = degree s in 

208 
(if m < n then (k,s) else 

209 
(let p'= funpow (m  n) shift1 p in 

210 
(if a = b then polydivide_aux (a,n,p,k,s \<^sub>p p') 

211 
else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) \<^sub>p (b *\<^sub>p p')))))))" 

212 
by pat_completeness auto 

213 

214 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

215 
definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where 
33154  216 
"polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)" 
217 

218 
fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where 

219 
"poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)" 

220 
 "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p" 

221 

222 
fun poly_deriv :: "poly \<Rightarrow> poly" where 

223 
"poly_deriv (CN c 0 p) = poly_deriv_aux 1 p" 

224 
 "poly_deriv p = 0\<^sub>p" 

225 

226 
(* Verification *) 

227 
lemma nth_pos2[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n  1)" 

228 
using Nat.gr0_conv_Suc 

229 
by clarsimp 

230 

231 
subsection{* Semantics of the polynomial representation *} 

232 

36409  233 
consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" 
33154  234 
primrec 
235 
"Ipoly bs (C c) = INum c" 

236 
"Ipoly bs (Bound n) = bs!n" 

237 
"Ipoly bs (Neg a) =  Ipoly bs a" 

238 
"Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b" 

239 
"Ipoly bs (Sub a b) = Ipoly bs a  Ipoly bs b" 

240 
"Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b" 

241 
"Ipoly bs (Pw t n) = (Ipoly bs t) ^ n" 

242 
"Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)" 

35054  243 
abbreviation 
36409  244 
Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>") 
35054  245 
where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p" 
33154  246 

247 
lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" 

248 
by (simp add: INum_def) 

249 
lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j" 

250 
by (simp add: INum_def) 

251 

252 
lemmas RIpoly_eqs = Ipoly.simps(27) Ipoly_CInt Ipoly_CRat 

253 

254 
subsection {* Normal form and normalization *} 

255 

256 
consts isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool" 

257 
recdef isnpolyh "measure size" 

258 
"isnpolyh (C c) = (\<lambda>k. isnormNum c)" 

259 
"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))" 

260 
"isnpolyh p = (\<lambda>k. False)" 

261 

262 
lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'" 

263 
by (induct p rule: isnpolyh.induct, auto) 

264 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

265 
definition isnpoly :: "poly \<Rightarrow> bool" where 
33154  266 
"isnpoly p \<equiv> isnpolyh p 0" 
267 

268 
text{* polyadd preserves normal forms *} 

269 

270 
lemma polyadd_normh: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> 

271 
\<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)" 

272 
proof(induct p q arbitrary: n0 n1 rule: polyadd.induct) 

273 
case (2 a b c' n' p' n0 n1) 

274 
from prems have th1: "isnpolyh (C (a,b)) (Suc n')" by simp 

275 
from prems(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all 

276 
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp 

277 
with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp 

278 
from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 

279 
thus ?case using prems th3 by simp 

280 
next 

281 
case (3 c' n' p' a b n1 n0) 

282 
from prems have th1: "isnpolyh (C (a,b)) (Suc n')" by simp 

283 
from prems(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all 

284 
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp 

285 
with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp 

286 
from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 

287 
thus ?case using prems th3 by simp 

288 
next 

289 
case (4 c n p c' n' p' n0 n1) 

290 
hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all 

291 
from prems have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all 

292 
from prems have ngen0: "n \<ge> n0" by simp 

293 
from prems have n'gen1: "n' \<ge> n1" by simp 

294 
have "n < n' \<or> n' < n \<or> n = n'" by auto 

295 
moreover {assume eq: "n = n'" hence eq': "\<not> n' < n \<and> \<not> n < n'" by simp 

296 
with prems(2)[rule_format, OF eq' nc nc'] 

297 
have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto 

298 
hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)" 

299 
using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto 

300 
from eq prems(1)[rule_format, OF eq' np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp 

301 
have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp 

302 
from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)} 

303 
moreover {assume lt: "n < n'" 

304 
have "min n0 n1 \<le> n0" by simp 

305 
with prems have th1:"min n0 n1 \<le> n" by auto 

306 
from prems have th21: "isnpolyh c (Suc n)" by simp 

307 
from prems have th22: "isnpolyh (CN c' n' p') n'" by simp 

308 
from lt have th23: "min (Suc n) n' = Suc n" by arith 

309 
from prems(4)[rule_format, OF lt th21 th22] 

310 
have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp 

311 
with prems th1 have ?case by simp } 

312 
moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp 

313 
have "min n0 n1 \<le> n1" by simp 

314 
with prems have th1:"min n0 n1 \<le> n'" by auto 

315 
from prems have th21: "isnpolyh c' (Suc n')" by simp_all 

316 
from prems have th22: "isnpolyh (CN c n p) n" by simp 

317 
from gt have th23: "min n (Suc n') = Suc n'" by arith 

318 
from prems(3)[rule_format, OF gt' th22 th21] 

319 
have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp 

320 
with prems th1 have ?case by simp} 

321 
ultimately show ?case by blast 

322 
qed auto 

323 

324 
lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)" 

36349  325 
by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib) 
33154  326 

327 
lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))" 

328 
using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp 

329 

330 
text{* The degree of addition and other general lemmas needed for the normal form of polymul*} 

331 

332 
lemma polyadd_different_degreen: 

333 
"\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> 

334 
degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)" 

335 
proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct) 

336 
case (4 c n p c' n' p' m n0 n1) 

337 
thus ?case 

338 
apply (cases "n' < n", simp_all add: Let_def) 

339 
apply (cases "n = n'", simp_all) 

340 
apply (cases "n' = m", simp_all add: Let_def) 

341 
by (erule allE[where x="m"], erule allE[where x="Suc m"], 

342 
erule allE[where x="m"], erule allE[where x="Suc m"], 

343 
clarsimp,erule allE[where x="m"],erule allE[where x="Suc m"], simp) 

344 
qed simp_all 

345 

346 
lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p" 

347 
by (induct p arbitrary: n rule: headn.induct, auto) 

348 
lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0" 

349 
by (induct p arbitrary: n rule: degree.induct, auto) 

350 
lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0" 

351 
by (induct p arbitrary: n rule: degreen.induct, auto) 

352 

353 
lemma degree_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> degree p = 0" 

354 
by (induct p arbitrary: n rule: degree.induct, auto) 

355 

356 
lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0" 

357 
using degree_isnpolyh_Suc by auto 

358 
lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degreen c n = 0" 

359 
using degreen_0 by auto 

360 

361 

362 
lemma degreen_polyadd: 

363 
assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> max n0 n1" 

364 
shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)" 

365 
using np nq m 

366 
proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct) 

367 
case (2 c c' n' p' n0 n1) thus ?case by (cases n', simp_all) 

368 
next 

369 
case (3 c n p c' n0 n1) thus ?case by (cases n, auto) 

370 
next 

371 
case (4 c n p c' n' p' n0 n1 m) 

372 
thus ?case 

373 
apply (cases "n < n'", simp_all add: Let_def) 

374 
apply (cases "n' < n", simp_all) 

375 
apply (erule allE[where x="n"],erule allE[where x="Suc n"],clarify) 

376 
apply (erule allE[where x="n'"],erule allE[where x="Suc n'"],clarify) 

377 
by (erule allE[where x="m"],erule allE[where x="m"], auto) 

378 
qed auto 

379 

380 

381 
lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> 

382 
\<Longrightarrow> degreen p m = degreen q m" 

383 
proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct) 

384 
case (4 c n p c' n' p' m n0 n1 x) 

385 
hence z: "CN c n p +\<^sub>p CN c' n' p' = C x" by simp 

386 
{assume nn': "n' < n" hence ?case using prems by simp} 

387 
moreover 

388 
{assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith 

389 
moreover {assume "n < n'" with prems have ?case by simp } 

390 
moreover {assume eq: "n = n'" hence ?case using prems 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

391 
by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) } 
33154  392 
ultimately have ?case by blast} 
393 
ultimately show ?case by blast 

394 
qed simp_all 

395 

396 
lemma polymul_properties: 

36409  397 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  398 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1" 
399 
shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" 

400 
and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)" 

401 
and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 

402 
else degreen p m + degreen q m)" 

403 
using np nq m 

404 
proof(induct p q arbitrary: n0 n1 m rule: polymul.induct) 

405 
case (2 a b c' n' p') 

406 
let ?c = "(a,b)" 

407 
{ case (1 n0 n1) 

408 
hence n: "isnpolyh (C ?c) n'" "isnpolyh c' (Suc n')" "isnpolyh p' n'" "isnormNum ?c" 

409 
"isnpolyh (CN c' n' p') n1" 

410 
by simp_all 

411 
{assume "?c = 0\<^sub>N" hence ?case by auto} 

412 
moreover {assume cnz: "?c \<noteq> 0\<^sub>N" 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

413 
from "2.hyps"(1)[rule_format,where xb="n'", OF cnz n(1) n(3)] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

414 
"2.hyps"(2)[rule_format, where x="Suc n'" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

415 
and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

416 
by (auto simp add: min_def)} 
33154  417 
ultimately show ?case by blast 
418 
next 

419 
case (2 n0 n1) thus ?case by auto 

420 
next 

421 
case (3 n0 n1) thus ?case using "2.hyps" by auto } 

422 
next 

423 
case (3 c n p a b){ 

424 
let ?c' = "(a,b)" 

425 
case (1 n0 n1) 

426 
hence n: "isnpolyh (C ?c') n" "isnpolyh c (Suc n)" "isnpolyh p n" "isnormNum ?c'" 

427 
"isnpolyh (CN c n p) n0" 

428 
by simp_all 

429 
{assume "?c' = 0\<^sub>N" hence ?case by auto} 

430 
moreover {assume cnz: "?c' \<noteq> 0\<^sub>N" 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

431 
from "3.hyps"(1)[rule_format,where xb="n", OF cnz n(3) n(1)] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

432 
"3.hyps"(2)[rule_format, where x="Suc n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

433 
and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

434 
by (auto simp add: min_def)} 
33154  435 
ultimately show ?case by blast 
436 
next 

437 
case (2 n0 n1) thus ?case apply auto done 

438 
next 

439 
case (3 n0 n1) thus ?case using "3.hyps" by auto } 

440 
next 

441 
case (4 c n p c' n' p') 

442 
let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'" 

443 
{fix n0 n1 

444 
assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1" 

445 
hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'" 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

446 
and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

447 
and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

448 
and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

449 
by simp_all 
33154  450 
have "n < n' \<or> n' < n \<or> n' = n" by auto 
451 
moreover 

452 
{assume nn': "n < n'" 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

453 
with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

454 
"4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

455 
have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

456 
by (simp add: min_def) } 
33154  457 
moreover 
458 

459 
{assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

460 
with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

461 
"4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

462 
nn' nn0 nn1 cnp' 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

463 
have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

464 
by (cases "Suc n' = n", simp_all add: min_def)} 
33154  465 
moreover 
466 
{assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

467 
from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

468 
"4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

469 

02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

470 
have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

471 
by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) } 
33154  472 
ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast } 
473 
note th = this 

474 
{fix n0 n1 m 

475 
assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1" 

476 
and m: "m \<le> min n0 n1" 

477 
let ?d = "degreen (?cnp *\<^sub>p ?cnp') m" 

478 
let ?d1 = "degreen ?cnp m" 

479 
let ?d2 = "degreen ?cnp' m" 

480 
let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)" 

481 
have "n'<n \<or> n < n' \<or> n' = n" by auto 

482 
moreover 

483 
{assume "n' < n \<or> n < n'" 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

484 
with "4.hyps" np np' m 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

485 
have ?eq apply (cases "n' < n", simp_all) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

486 
apply (erule allE[where x="n"],erule allE[where x="n"],auto) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

487 
done } 
33154  488 
moreover 
489 
{assume nn': "n' = n" hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

490 
from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

491 
"4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

492 
np np' nn' 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

493 
have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

494 
"isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

495 
"(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

496 
"?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

497 
{assume mn: "m = n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

498 
from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

499 
"4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

500 
have degs: "degreen (?cnp *\<^sub>p c') n = 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

501 
(if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

502 
"degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" by (simp_all add: min_def) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

503 
from degs norm 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

504 
have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

505 
hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

506 
by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

507 
have nmin: "n \<le> min n n" by (simp add: min_def) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

508 
from polyadd_different_degreen[OF norm(3,6) neq nmin] th1 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

509 
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 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

510 
from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

511 
"4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

512 
mn norm m nn' deg 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

513 
have ?eq by simp} 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

514 
moreover 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

515 
{assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

516 
from nn' m np have max1: "m \<le> max n n" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

517 
hence min1: "m \<le> min n n" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

518 
hence min2: "m \<le> min n (Suc n)" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

519 
{assume "c' = 0\<^sub>p" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

520 
from `c' = 0\<^sub>p` have ?eq 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

521 
using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

522 
"4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn' 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

523 
apply simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

524 
done} 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

525 
moreover 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

526 
{assume cnz: "c' \<noteq> 0\<^sub>p" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

527 
from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

528 
"4.hyps"(2)[rule_format, OF nn norm(1,2) min2] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

529 
degreen_polyadd[OF norm(3,6) max1] 
33154  530 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

531 
have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

532 
\<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

533 
using mn nn' cnz np np' by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

534 
with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

535 
"4.hyps"(2)[rule_format, OF nn norm(1,2) min2] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

536 
degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp} 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

537 
ultimately have ?eq by blast } 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

538 
ultimately have ?eq by blast} 
33154  539 
ultimately show ?eq by blast} 
540 
note degth = this 

541 
{ case (2 n0 n1) 

542 
hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

543 
and m: "m \<le> min n0 n1" by simp_all 
33154  544 
hence mn: "m \<le> n" by simp 
545 
let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')" 

546 
{assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n" 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

547 
hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

548 
from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

549 
"4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"] 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

550 
np np' C(2) mn 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

551 
have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

552 
"isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

553 
"(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

554 
"?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

555 
"degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

556 
"degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

557 
by (simp_all add: min_def) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

558 

02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

559 
from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

560 
have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

561 
using norm by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

562 
from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

563 
have "False" by simp } 
33154  564 
thus ?case using "4.hyps" by clarsimp} 
565 
qed auto 

566 

567 
lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)" 

36349  568 
by(induct p q rule: polymul.induct, auto simp add: field_simps) 
33154  569 

570 
lemma polymul_normh: 

36409  571 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  572 
shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)" 
573 
using polymul_properties(1) by blast 

574 
lemma polymul_eq0_iff: 

36409  575 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  576 
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) " 
577 
using polymul_properties(2) by blast 

578 
lemma polymul_degreen: 

36409  579 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  580 
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)" 
581 
using polymul_properties(3) by blast 

582 
lemma polymul_norm: 

36409  583 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  584 
shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))" 
585 
using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp 

586 

587 
lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p" 

588 
by (induct p arbitrary: n0 rule: headconst.induct, auto) 

589 

590 
lemma headconst_isnormNum: "isnpolyh p n0 \<Longrightarrow> isnormNum (headconst p)" 

591 
by (induct p arbitrary: n0, auto) 

592 

593 
lemma monic_eqI: assumes np: "isnpolyh p n0" 

36409  594 
shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})" 
33154  595 
unfolding monic_def Let_def 
596 
proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) 

597 
let ?h = "headconst p" 

598 
assume pz: "p \<noteq> 0\<^sub>p" 

599 
{assume hz: "INum ?h = (0::'a)" 

600 
from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all 

601 
from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp 

602 
with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast} 

603 
thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast 

604 
qed 

605 

606 

607 

608 

609 
text{* polyneg is a negation and preserves normal form *} 

610 
lemma polyneg[simp]: "Ipoly bs (polyneg p) =  Ipoly bs p" 

611 
by (induct p rule: polyneg.induct, auto) 

612 

613 
lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)" 

614 
by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def) 

615 
lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p" 

616 
by (induct p arbitrary: n0 rule: polyneg.induct, auto) 

617 
lemma polyneg_normh: "\<And>n. isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n " 

618 
by (induct p rule: polyneg.induct, auto simp add: polyneg0) 

619 

620 
lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)" 

621 
using isnpoly_def polyneg_normh by simp 

622 

623 

624 
text{* polysub is a substraction and preserves normalform *} 

625 
lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p)  (Ipoly bs q)" 

626 
by (simp add: polysub_def polyneg polyadd) 

627 
lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)" 

628 
by (simp add: polysub_def polyneg_normh polyadd_normh) 

629 

630 
lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))" 

631 
using polyadd_norm polyneg_norm by (simp add: polysub_def) 

36409  632 
lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  633 
shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p" 
634 
unfolding polysub_def split_def fst_conv snd_conv 

635 
by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def]) 

636 

637 
lemma polysub_0: 

36409  638 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  639 
shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p \<^sub>p q = 0\<^sub>p) = (p = q)" 
640 
unfolding polysub_def split_def fst_conv snd_conv 

641 
apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def]) 

642 
apply (clarsimp simp add: Let_def) 

643 
apply (case_tac "n < n'", simp_all) 

644 
apply (case_tac "n' < n", simp_all) 

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="n" in exI, simp) 

650 
apply (rule_tac x="Suc n" in exI, simp) 

651 
apply (erule impE)+ 

652 
apply (rule_tac x="Suc n" in exI, simp) 

653 
apply (rule_tac x="n" in exI, simp) 

654 
apply (erule impE)+ 

655 
apply (rule_tac x="Suc n" in exI, simp) 

656 
apply clarsimp 

657 
done 

658 

659 
text{* polypow is a power function and preserves normal forms *} 

36409  660 
lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n" 
33154  661 
proof(induct n rule: polypow.induct) 
662 
case 1 thus ?case by simp 

663 
next 

664 
case (2 n) 

665 
let ?q = "polypow ((Suc n) div 2) p" 

666 
let ?d = "polymul(?q,?q)" 

667 
have "odd (Suc n) \<or> even (Suc n)" by simp 

668 
moreover 

669 
{assume odd: "odd (Suc n)" 

670 
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 

671 
from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul(p, ?d))" by (simp add: Let_def) 

672 
also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)" 

673 
using "2.hyps" by simp 

674 
also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)" 

675 
apply (simp only: power_add power_one_right) by simp 

676 
also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat)))))" 

677 
by (simp only: th) 

678 
finally have ?case 

679 
using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp } 

680 
moreover 

681 
{assume even: "even (Suc n)" 

682 
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 

683 
from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def) 

684 
also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)" 

685 
using "2.hyps" apply (simp only: power_add) by simp 

686 
finally have ?case using even_nat_div_two_times_two[OF even] by (simp only: th)} 

687 
ultimately show ?case by blast 

688 
qed 

689 

690 
lemma polypow_normh: 

36409  691 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  692 
shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n" 
693 
proof (induct k arbitrary: n rule: polypow.induct) 

694 
case (2 k n) 

695 
let ?q = "polypow (Suc k div 2) p" 

696 
let ?d = "polymul (?q,?q)" 

697 
from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+ 

698 
from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp 

699 
from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp 

700 
from dn on show ?case by (simp add: Let_def) 

701 
qed auto 

702 

703 
lemma polypow_norm: 

36409  704 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  705 
shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)" 
706 
by (simp add: polypow_normh isnpoly_def) 

707 

708 
text{* Finally the whole normalization*} 

709 

36409  710 
lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})" 
33154  711 
by (induct p rule:polynate.induct, auto) 
712 

713 
lemma polynate_norm[simp]: 

36409  714 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  715 
shows "isnpoly (polynate p)" 
716 
by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def) 

717 

718 
text{* shift1 *} 

719 

720 

721 
lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" 

722 
by (simp add: shift1_def polymul) 

723 

724 
lemma shift1_isnpoly: 

725 
assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) " 

726 
using pn pnz by (simp add: shift1_def isnpoly_def ) 

727 

728 
lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p" 

729 
by (simp add: shift1_def) 

730 
lemma funpow_shift1_isnpoly: 

731 
"\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)" 

732 
by (induct n arbitrary: p, auto simp add: shift1_isnpoly) 

733 

734 
lemma funpow_isnpolyh: 

735 
assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n" 

736 
shows "isnpolyh (funpow k f p) n" 

737 
using f np by (induct k arbitrary: p, auto) 

738 

36409  739 
lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)" 
33154  740 
by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc ) 
741 

742 
lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0" 

743 
using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) 

744 

745 
lemma funpow_shift1_1: 

36409  746 
"(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)" 
33154  747 
by (simp add: funpow_shift1) 
748 

749 
lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)" 

36349  750 
by (induct p arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps) 
33154  751 

752 
lemma behead: 

753 
assumes np: "isnpolyh p n" 

36409  754 
shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})" 
33154  755 
using np 
756 
proof (induct p arbitrary: n rule: behead.induct) 

757 
case (1 c p n) hence pn: "isnpolyh p n" by simp 

758 
from prems(2)[OF pn] 

759 
have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 

760 
then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p") 

36349  761 
by (simp_all add: th[symmetric] field_simps power_Suc) 
33154  762 
qed (auto simp add: Let_def) 
763 

764 
lemma behead_isnpolyh: 

765 
assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n" 

766 
using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono) 

767 

768 
subsection{* Miscilanious lemmas about indexes, decrementation, substitution etc ... *} 

769 
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p" 

770 
proof(induct p arbitrary: n rule: polybound0.induct, auto) 

771 
case (goal1 c n p n') 

772 
hence "n = Suc (n  1)" by simp 

773 
hence "isnpolyh p (Suc (n  1))" using `isnpolyh p n` by simp 

774 
with prems(2) show ?case by simp 

775 
qed 

776 

777 
lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p" 

778 
by (induct p arbitrary: n0 rule: isconstant.induct, auto simp add: isnpolyh_polybound0) 

779 

780 
lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p" by (induct p, auto) 

781 

782 
lemma decrpoly_normh: "isnpolyh p n0 \<Longrightarrow> polybound0 p \<Longrightarrow> isnpolyh (decrpoly p) (n0  1)" 

783 
apply (induct p arbitrary: n0, auto) 

784 
apply (atomize) 

785 
apply (erule_tac x = "Suc nat" in allE) 

786 
apply auto 

787 
done 

788 

789 
lemma head_polybound0: "isnpolyh p n0 \<Longrightarrow> polybound0 (head p)" 

790 
by (induct p arbitrary: n0 rule: head.induct, auto intro: isnpolyh_polybound0) 

791 

792 
lemma polybound0_I: 

793 
assumes nb: "polybound0 a" 

794 
shows "Ipoly (b#bs) a = Ipoly (b'#bs) a" 

795 
using nb 

796 
by (induct a rule: polybound0.induct) auto 

797 
lemma polysubst0_I: 

798 
shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t" 

799 
by (induct t) simp_all 

800 

801 
lemma polysubst0_I': 

802 
assumes nb: "polybound0 a" 

803 
shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b'#bs) a)#bs) t" 

804 
by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"]) 

805 

806 
lemma decrpoly: assumes nb: "polybound0 t" 

807 
shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)" 

808 
using nb by (induct t rule: decrpoly.induct, simp_all) 

809 

810 
lemma polysubst0_polybound0: assumes nb: "polybound0 t" 

811 
shows "polybound0 (polysubst0 t a)" 

812 
using nb by (induct a rule: polysubst0.induct, auto) 

813 

814 
lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p" 

815 
by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0) 

816 

817 
fun maxindex :: "poly \<Rightarrow> nat" where 

818 
"maxindex (Bound n) = n + 1" 

819 
 "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" 

820 
 "maxindex (Add p q) = max (maxindex p) (maxindex q)" 

821 
 "maxindex (Sub p q) = max (maxindex p) (maxindex q)" 

822 
 "maxindex (Mul p q) = max (maxindex p) (maxindex q)" 

823 
 "maxindex (Neg p) = maxindex p" 

824 
 "maxindex (Pw p n) = maxindex p" 

825 
 "maxindex (C x) = 0" 

826 

827 
definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool" where 

828 
"wf_bs bs p = (length bs \<ge> maxindex p)" 

829 

830 
lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall> c \<in> set (coefficients p). wf_bs bs c" 

831 
proof(induct p rule: coefficients.induct) 

832 
case (1 c p) 

833 
show ?case 

834 
proof 

835 
fix x assume xc: "x \<in> set (coefficients (CN c 0 p))" 

836 
hence "x = c \<or> x \<in> set (coefficients p)" by simp 

837 
moreover 

838 
{assume "x = c" hence "wf_bs bs x" using "1.prems" unfolding wf_bs_def by simp} 

839 
moreover 

840 
{assume H: "x \<in> set (coefficients p)" 

841 
from "1.prems" have "wf_bs bs p" unfolding wf_bs_def by simp 

842 
with "1.hyps" H have "wf_bs bs x" by blast } 

843 
ultimately show "wf_bs bs x" by blast 

844 
qed 

845 
qed simp_all 

846 

847 
lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p" 

848 
by (induct p rule: coefficients.induct, auto) 

849 

850 
lemma length_exists: "\<exists>xs. length xs = n" by (rule exI[where x="replicate n x"], simp) 

851 

852 
lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p" 

853 
unfolding wf_bs_def by (induct p, auto simp add: nth_append) 

854 

855 
lemma take_maxindex_wf: assumes wf: "wf_bs bs p" 

856 
shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p" 

857 
proof 

858 
let ?ip = "maxindex p" 

859 
let ?tbs = "take ?ip bs" 

860 
from wf have "length ?tbs = ?ip" unfolding wf_bs_def by simp 

861 
hence wf': "wf_bs ?tbs p" unfolding wf_bs_def by simp 

862 
have eq: "bs = ?tbs @ (drop ?ip bs)" by simp 

863 
from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis using eq by simp 

864 
qed 

865 

866 
lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p  1" 

867 
by (induct p, auto) 

868 

869 
lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p" 

870 
unfolding wf_bs_def by simp 

871 

872 
lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p" 

873 
unfolding wf_bs_def by simp 

874 

875 

876 

877 
lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p" 

878 
by(induct p rule: coefficients.induct, auto simp add: wf_bs_def) 

879 
lemma coefficients_Nil[simp]: "coefficients p \<noteq> []" 

880 
by (induct p rule: coefficients.induct, simp_all) 

881 

882 

883 
lemma coefficients_head: "last (coefficients p) = head p" 

884 
by (induct p rule: coefficients.induct, auto) 

885 

886 
lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p" 

887 
unfolding wf_bs_def by (induct p rule: decrpoly.induct, auto) 

888 

889 
lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists> ys. length (xs @ ys) = n" 

890 
apply (rule exI[where x="replicate (n  length xs) z"]) 

891 
by simp 

892 
lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \<Longrightarrow> isconstant p" 

893 
by (cases p, auto) (case_tac "nat", simp_all) 

894 

895 
lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)" 

896 
unfolding wf_bs_def 

897 
apply (induct p q rule: polyadd.induct) 

898 
apply (auto simp add: Let_def) 

899 
done 

900 

901 
lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)" 

902 

903 
unfolding wf_bs_def 

904 
apply (induct p q arbitrary: bs rule: polymul.induct) 

905 
apply (simp_all add: wf_bs_polyadd) 

906 
apply clarsimp 

907 
apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format]) 

908 
apply auto 

909 
done 

910 

911 
lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)" 

912 
unfolding wf_bs_def by (induct p rule: polyneg.induct, auto) 

913 

914 
lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p \<^sub>p q)" 

915 
unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast 

916 

917 
subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*} 

918 

919 
definition "polypoly bs p = map (Ipoly bs) (coefficients p)" 

920 
definition "polypoly' bs p = map ((Ipoly bs o decrpoly)) (coefficients p)" 

921 
definition "poly_nate bs p = map ((Ipoly bs o decrpoly)) (coefficients (polynate p))" 

922 

923 
lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall> q \<in> set (coefficients p). isnpolyh q n0" 

924 
proof (induct p arbitrary: n0 rule: coefficients.induct) 

925 
case (1 c p n0) 

926 
have cp: "isnpolyh (CN c 0 p) n0" by fact 

927 
hence norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0" 

928 
by (auto simp add: isnpolyh_mono[where n'=0]) 

929 
from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case by simp 

930 
qed auto 

931 

932 
lemma coefficients_isconst: 

933 
"isnpolyh p n \<Longrightarrow> \<forall>q\<in>set (coefficients p). isconstant q" 

934 
by (induct p arbitrary: n rule: coefficients.induct, 

935 
auto simp add: isnpolyh_Suc_const) 

936 

937 
lemma polypoly_polypoly': 

938 
assumes np: "isnpolyh p n0" 

939 
shows "polypoly (x#bs) p = polypoly' bs p" 

940 
proof 

941 
let ?cf = "set (coefficients p)" 

942 
from coefficients_normh[OF np] have cn_norm: "\<forall> q\<in> ?cf. isnpolyh q n0" . 

943 
{fix q assume q: "q \<in> ?cf" 

944 
from q cn_norm have th: "isnpolyh q n0" by blast 

945 
from coefficients_isconst[OF np] q have "isconstant q" by blast 

946 
with isconstant_polybound0[OF th] have "polybound0 q" by blast} 

947 
hence "\<forall>q \<in> ?cf. polybound0 q" .. 

948 
hence "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)" 

949 
using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs] 

950 
by auto 

951 

952 
thus ?thesis unfolding polypoly_def polypoly'_def by simp 

953 
qed 

954 

955 
lemma polypoly_poly: 

956 
assumes np: "isnpolyh p n0" shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x" 

957 
using np 

958 
by (induct p arbitrary: n0 bs rule: coefficients.induct, auto simp add: polypoly_def) 

959 

960 
lemma polypoly'_poly: 

961 
assumes np: "isnpolyh p n0" shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x" 

962 
using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] . 

963 

964 

965 
lemma polypoly_poly_polybound0: 

966 
assumes np: "isnpolyh p n0" and nb: "polybound0 p" 

967 
shows "polypoly bs p = [Ipoly bs p]" 

968 
using np nb unfolding polypoly_def 

969 
by (cases p, auto, case_tac nat, auto) 

970 

971 
lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0" 

972 
by (induct p rule: head.induct, auto) 

973 

974 
lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)" 

975 
by (cases p,auto) 

976 

977 
lemma head_eq_headn0: "head p = headn p 0" 

978 
by (induct p rule: head.induct, simp_all) 

979 

980 
lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (head p = 0\<^sub>p) = (p = 0\<^sub>p)" 

981 
by (simp add: head_eq_headn0) 

982 

983 
lemma isnpolyh_zero_iff: 

36409  984 
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})" 
33154  985 
shows "p = 0\<^sub>p" 
986 
using nq eq 

34915  987 
proof (induct "maxindex p" arbitrary: p n0 rule: less_induct) 
988 
case less 

989 
note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)` 

990 
{assume nz: "maxindex p = 0" 

991 
then obtain c where "p = C c" using np by (cases p, auto) 

33154  992 
with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp} 
993 
moreover 

34915  994 
{assume nz: "maxindex p \<noteq> 0" 
33154  995 
let ?h = "head p" 
996 
let ?hd = "decrpoly ?h" 

997 
let ?ihd = "maxindex ?hd" 

998 
from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h" 

999 
by simp_all 

1000 
hence nhd: "isnpolyh ?hd (n0  1)" using decrpoly_normh by blast 

1001 

1002 
from maxindex_coefficients[of p] coefficients_head[of p, symmetric] 

34915  1003 
have mihn: "maxindex ?h \<le> maxindex p" by auto 
1004 
with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p" by auto 

33154  1005 
{fix bs:: "'a list" assume bs: "wf_bs bs ?hd" 
1006 
let ?ts = "take ?ihd bs" 

1007 
let ?rs = "drop ?ihd bs" 

1008 
have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp 

1009 
have bs_ts_eq: "?ts@ ?rs = bs" by simp 

1010 
from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp 

34915  1011 
from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp 
1012 
with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast 

1013 
hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp 

33154  1014 
with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast 
1015 
hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp 

1016 
with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a] 

1017 
have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x" by simp 

1018 
hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) 

1019 
hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0" 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

1020 
using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff) 
33154  1021 
with coefficients_head[of p, symmetric] 
1022 
have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp 

1023 
from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp 

1024 
with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp 

1025 
with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp } 

1026 
then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast 

1027 

34915  1028 
from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast 
33154  1029 
hence "?h = 0\<^sub>p" by simp 
1030 
with head_nz[OF np] have "p = 0\<^sub>p" by simp} 

1031 
ultimately show "p = 0\<^sub>p" by blast 

1032 
qed 

1033 

1034 
lemma isnpolyh_unique: 

1035 
assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1" 

36409  1036 
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" 
33154  1037 
proof(auto) 
1038 
assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>" 

1039 
hence "\<forall>bs.\<lparr>p \<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp 

1040 
hence "\<forall>bs. wf_bs bs (p \<^sub>p q) \<longrightarrow> \<lparr>p \<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" 

1041 
using wf_bs_polysub[where p=p and q=q] by auto 

1042 
with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] 

1043 
show "p = q" by blast 

1044 
qed 

1045 

1046 

1047 
text{* consequenses of unicity on the algorithms for polynomial normalization *} 

1048 

36409  1049 
lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1050 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p" 
1051 
using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp 

1052 

1053 
lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp 

1054 
lemma one_normh: "isnpolyh 1\<^sub>p n" by simp 

1055 
lemma polyadd_0[simp]: 

36409  1056 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1057 
and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p" 
1058 
using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] 

1059 
isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all 

1060 

1061 
lemma polymul_1[simp]: 

36409  1062 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1063 
and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p" 
1064 
using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 

1065 
isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all 

1066 
lemma polymul_0[simp]: 

36409  1067 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1068 
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" 
1069 
using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] 

1070 
isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all 

1071 

1072 
lemma polymul_commute: 

36409  1073 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1074 
and np:"isnpolyh p n0" and nq: "isnpolyh q n1" 
1075 
shows "p *\<^sub>p q = q *\<^sub>p p" 

36409  1076 
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 
33154  1077 

1078 
declare polyneg_polyneg[simp] 

1079 

1080 
lemma isnpolyh_polynate_id[simp]: 

36409  1081 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1082 
and np:"isnpolyh p n0" shows "polynate p = p" 
36409  1083 
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 
33154  1084 

1085 
lemma polynate_idempotent[simp]: 

36409  1086 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1087 
shows "polynate (polynate p) = polynate p" 
1088 
using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] . 

1089 

1090 
lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)" 

1091 
unfolding poly_nate_def polypoly'_def .. 

36409  1092 
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>)" 
33154  1093 
using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p] 
1094 
unfolding poly_nate_polypoly' by (auto intro: ext) 

1095 

1096 
subsection{* heads, degrees and all that *} 

1097 
lemma degree_eq_degreen0: "degree p = degreen p 0" 

1098 
by (induct p rule: degree.induct, simp_all) 

1099 

1100 
lemma degree_polyneg: assumes n: "isnpolyh p n" 

1101 
shows "degree (polyneg p) = degree p" 

1102 
using n 

1103 
by (induct p arbitrary: n rule: polyneg.induct, simp_all) (case_tac na, auto) 

1104 

1105 
lemma degree_polyadd: 

1106 
assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" 

1107 
shows "degree (p +\<^sub>p q) \<le> max (degree p) (degree q)" 

1108 
using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp 

1109 

1110 

1111 
lemma degree_polysub: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" 

1112 
shows "degree (p \<^sub>p q) \<le> max (degree p) (degree q)" 

1113 
proof 

1114 
from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp 

1115 
from degree_polyadd[OF np nq'] show ?thesis by (simp add: polysub_def degree_polyneg[OF nq]) 

1116 
qed 

1117 

1118 
lemma degree_polysub_samehead: 

36409  1119 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1120 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
1121 
and d: "degree p = degree q" 

1122 
shows "degree (p \<^sub>p q) < degree p \<or> (p \<^sub>p q = 0\<^sub>p)" 

1123 
unfolding polysub_def split_def fst_conv snd_conv 

1124 
using np nq h d 

1125 
proof(induct p q rule:polyadd.induct) 

1126 
case (1 a b a' b') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 

1127 
next 

1128 
case (2 a b c' n' p') 

1129 
let ?c = "(a,b)" 

1130 
from prems have "degree (C ?c) = degree (CN c' n' p')" by simp 

1131 
hence nz:"n' > 0" by (cases n', auto) 

1132 
hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto) 

1133 
with prems show ?case by simp 

1134 
next 

1135 
case (3 c n p a' b') 

1136 
let ?c' = "(a',b')" 

1137 
from prems have "degree (C ?c') = degree (CN c n p)" by simp 

1138 
hence nz:"n > 0" by (cases n, auto) 

1139 
hence "head (CN c n p) = CN c n p" by (cases n, auto) 

1140 
with prems show ?case by simp 

1141 
next 

1142 
case (4 c n p c' n' p') 

1143 
hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" 

1144 
"head (CN c n p) = head (CN c' n' p')" "degree (CN c n p) = degree (CN c' n' p')" by simp+ 

1145 
hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all 

1146 
hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" 

1147 
using H(12) degree_polyneg by auto 

1148 
from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')" by simp+ 

1149 
from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0" by simp 

1150 
from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" by auto 

1151 
have "n = n' \<or> n < n' \<or> n > n'" by arith 

1152 
moreover 

1153 
{assume nn': "n = n'" 

1154 
have "n = 0 \<or> n >0" by arith 

1155 
moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')} 

1156 
moreover {assume nz: "n > 0" 

1157 
with nn' H(3) have cc':"c = c'" and pp': "p = p'" by (cases n, auto)+ 

1158 
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)} 

1159 
ultimately have ?case by blast} 

1160 
moreover 

1161 
{assume nn': "n < n'" hence n'p: "n' > 0" by simp 

1162 
hence headcnp':"head (CN c' n' p') = CN c' n' p'" by (cases n', simp_all) 

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

1164 
hence "n > 0" by (cases n, simp_all) 

1165 
hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto) 

1166 
from H(3) headcnp headcnp' nn' have ?case by auto} 

1167 
moreover 

1168 
{assume nn': "n > n'" hence np: "n > 0" by simp 

1169 
hence headcnp:"head (CN c n p) = CN c n p" by (cases n, simp_all) 

1170 
from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp 

1171 
from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all) 

1172 
with degcnpeq have "n' > 0" by (cases n', simp_all) 

1173 
hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto) 

1174 
from H(3) headcnp headcnp' nn' have ?case by auto} 

1175 
ultimately show ?case by blast 

1176 
qed auto 

1177 

1178 
lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p" 

1179 
by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def) 

1180 

1181 
lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p" 

1182 
proof(induct k arbitrary: n0 p) 

1183 
case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) 

1184 
with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" 

1185 
and "head (shift1 p) = head p" by (simp_all add: shift1_head) 

1186 
thus ?case by simp 

1187 
qed auto 

1188 

1189 
lemma shift1_degree: "degree (shift1 p) = 1 + degree p" 

1190 
by (simp add: shift1_def) 

1191 
lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p " 

1192 
by (induct k arbitrary: p, auto simp add: shift1_degree) 

1193 

1194 
lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p" 

1195 
by (induct n arbitrary: p, simp_all add: funpow_def) 

1196 

1197 
lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p" 

1198 
by (induct p arbitrary: n rule: degree.induct, auto) 

1199 
lemma headn_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> headn p m = p" 

1200 
by (induct p arbitrary: n rule: degreen.induct, auto) 

1201 
lemma head_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> head p = p" 

1202 
by (induct p arbitrary: n rule: degree.induct, auto) 

1203 
lemma head_head[simp]: "isnpolyh p n0 \<Longrightarrow> head (head p) = head p" 

1204 
by (induct p rule: head.induct, auto) 

1205 

1206 
lemma polyadd_eq_const_degree: 

1207 
"\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> \<Longrightarrow> degree p = degree q" 

1208 
using polyadd_eq_const_degreen degree_eq_degreen0 by simp 

1209 

1210 
lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" 

1211 
and deg: "degree p \<noteq> degree q" 

1212 
shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)" 

1213 
using np nq deg 

1214 
apply(induct p q arbitrary: n0 n1 rule: polyadd.induct,simp_all) 

1215 
apply (case_tac n', simp, simp) 

1216 
apply (case_tac n, simp, simp) 

1217 
apply (case_tac n, case_tac n', simp add: Let_def) 

1218 
apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p") 

1219 
apply (clarsimp simp add: polyadd_eq_const_degree) 

1220 
apply clarsimp 

1221 
apply (erule_tac impE,blast) 

1222 
apply (erule_tac impE,blast) 

1223 
apply clarsimp 

1224 
apply simp 

1225 
apply (case_tac n', simp_all) 

1226 
done 

1227 

1228 
lemma polymul_head_polyeq: 

36409  1229 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1230 
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" 
1231 
proof (induct p q arbitrary: n0 n1 rule: polymul.induct) 

1232 
case (2 a b c' n' p' n0 n1) 

1233 
hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)" by (simp_all add: head_isnpolyh) 

1234 
thus ?case using prems by (cases n', auto) 

1235 
next 

1236 
case (3 c n p a' b' n0 n1) 

1237 
hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')" by (simp_all add: head_isnpolyh) 

1238 
thus ?case using prems by (cases n, auto) 

1239 
next 

1240 
case (4 c n p c' n' p' n0 n1) 

1241 
hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')" 

1242 
"isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'" 

1243 
by simp_all 

1244 
have "n < n' \<or> n' < n \<or> n = n'" by arith 

1245 
moreover 

1246 
{assume nn': "n < n'" hence ?case 

1247 
thm prems 

1248 
using norm 

1249 
prems(6)[rule_format, OF nn' norm(1,6)] 

1250 
prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)} 

1251 
moreover {assume nn': "n'< n" 

1252 
hence stupid: "n' < n \<and> \<not> n < n'" by simp 

1253 
hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)] 

1254 
prems(5)[rule_format, OF stupid norm(5,4)] 

1255 
by (simp,cases n',simp,cases n,auto)} 

1256 
moreover {assume nn': "n' = n" 

1257 
hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp 

1258 
from nn' polymul_normh[OF norm(5,4)] 

1259 
have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def) 

1260 
from nn' polymul_normh[OF norm(5,3)] norm 

1261 
have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp 

1262 
from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6) 

1263 
have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp 

1264 
from polyadd_normh[OF ncnpc' ncnpp0'] 

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

1266 
by (simp add: min_def) 

1267 
{assume np: "n > 0" 

1268 
with nn' head_isnpolyh_Suc'[OF np nth] 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

1269 
head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']] 
33154  1270 
have ?case by simp} 
1271 
moreover 

1272 
{moreover assume nz: "n = 0" 

1273 
from polymul_degreen[OF norm(5,4), where m="0"] 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

1274 
polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0 
33154  1275 
norm(5,6) degree_npolyhCN[OF norm(6)] 
1276 
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 

1277 
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 

1278 
from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth 

1279 
have ?case using norm prems(2)[rule_format, OF stupid norm(5,3)] 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

1280 
prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp } 
33154  1281 
ultimately have ?case by (cases n) auto} 
1282 
ultimately show ?case by blast 

1283 
qed simp_all 

1284 

