author  wenzelm 
Thu, 22 Apr 2004 11:01:34 +0200  
changeset 14651  02b8f3bcf7fe 
parent 14590  276ef51cedbf 
child 14666  65f8680c3f16 
permissions  rwrr 
13940  1 
(* 
2 
Title: Univariate Polynomials 

3 
Id: $Id$ 

4 
Author: Clemens Ballarin, started 9 December 1996 

5 
Copyright: Clemens Ballarin 

6 
*) 

7 

14577  8 
header {* Univariate Polynomials *} 
13940  9 

14577  10 
theory UnivPoly = Module: 
13940  11 

14553  12 
text {* 
13 
Polynomials are formalised as modules with additional operations for 

14 
extracting coefficients from polynomials and for obtaining monomials 

15 
from coefficients and exponents (record @{text "up_ring"}). 

16 
The carrier set is 

17 
a set of bounded functions from Nat to the coefficient domain. 

18 
Bounded means that these functions return zero above a certain bound 

19 
(the degree). There is a chapter on the formalisation of polynomials 

20 
in my PhD thesis (http://www4.in.tum.de/\~{}ballarin/publications/), 

21 
which was implemented with axiomatic type classes. This was later 

22 
ported to Locales. 

23 
*} 

24 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13940
diff
changeset

25 
subsection {* The Constructor for Univariate Polynomials *} 
13940  26 

27 
(* Could alternatively use locale ... 

28 
locale bound = cring + var bound + 

29 
defines ... 

30 
*) 

31 

32 
constdefs 

33 
bound :: "['a, nat, nat => 'a] => bool" 

34 
"bound z n f == (ALL i. n < i > f i = z)" 

35 

36 
lemma boundI [intro!]: 

37 
"[ !! m. n < m ==> f m = z ] ==> bound z n f" 

38 
by (unfold bound_def) fast 

39 

40 
lemma boundE [elim?]: 

41 
"[ bound z n f; (!! m. n < m ==> f m = z) ==> P ] ==> P" 

42 
by (unfold bound_def) fast 

43 

44 
lemma boundD [dest]: 

45 
"[ bound z n f; n < m ] ==> f m = z" 

46 
by (unfold bound_def) fast 

47 

48 
lemma bound_below: 

49 
assumes bound: "bound z m f" and nonzero: "f n ~= z" shows "n <= m" 

50 
proof (rule classical) 

51 
assume "~ ?thesis" 

52 
then have "m < n" by arith 

53 
with bound have "f n = z" .. 

54 
with nonzero show ?thesis by contradiction 

55 
qed 

56 

57 
record ('a, 'p) up_ring = "('a, 'p) module" + 

58 
monom :: "['a, nat] => 'p" 

59 
coeff :: "['p, nat] => 'a" 

60 

14651  61 
constdefs (structure R) 
62 
up :: "_ => (nat => 'a) set" 

63 
"up R == {f. f \<in> UNIV > carrier R & (EX n. bound \<zero> n f)}" 

64 
UP :: "_ => ('a, nat => 'a) up_ring" 

13940  65 
"UP R == ( 
66 
carrier = up R, 

14651  67 
mult = (%p:up R. %q:up R. %n. \<Oplus>i \<in> {..n}. p i \<otimes> q (ni)), 
68 
one = (%i. if i=0 then \<one> else \<zero>), 

69 
zero = (%i. \<zero>), 

70 
add = (%p:up R. %q:up R. %i. p i \<oplus> q i), 

71 
smult = (%a:carrier R. %p:up R. %i. a \<otimes> p i), 

72 
monom = (%a:carrier R. %n i. if i=n then a else \<zero>), 

13940  73 
coeff = (%p:up R. %n. p n) )" 
74 

75 
text {* 

76 
Properties of the set of polynomials @{term up}. 

77 
*} 

78 

79 
lemma mem_upI [intro]: 

80 
"[ !!n. f n \<in> carrier R; EX n. bound (zero R) n f ] ==> f \<in> up R" 

81 
by (simp add: up_def Pi_def) 

82 

83 
lemma mem_upD [dest]: 

84 
"f \<in> up R ==> f n \<in> carrier R" 

85 
by (simp add: up_def Pi_def) 

86 

87 
lemma (in cring) bound_upD [dest]: 

88 
"f \<in> up R ==> EX n. bound \<zero> n f" 

89 
by (simp add: up_def) 

90 

91 
lemma (in cring) up_one_closed: 

92 
"(%n. if n = 0 then \<one> else \<zero>) \<in> up R" 

93 
using up_def by force 

94 

95 
lemma (in cring) up_smult_closed: 

96 
"[ a \<in> carrier R; p \<in> up R ] ==> (%i. a \<otimes> p i) \<in> up R" 

97 
by force 

98 

99 
lemma (in cring) up_add_closed: 

100 
"[ p \<in> up R; q \<in> up R ] ==> (%i. p i \<oplus> q i) \<in> up R" 

101 
proof 

102 
fix n 

103 
assume "p \<in> up R" and "q \<in> up R" 

104 
then show "p n \<oplus> q n \<in> carrier R" 

105 
by auto 

106 
next 

107 
assume UP: "p \<in> up R" "q \<in> up R" 

108 
show "EX n. bound \<zero> n (%i. p i \<oplus> q i)" 

109 
proof  

110 
from UP obtain n where boundn: "bound \<zero> n p" by fast 

111 
from UP obtain m where boundm: "bound \<zero> m q" by fast 

112 
have "bound \<zero> (max n m) (%i. p i \<oplus> q i)" 

113 
proof 

114 
fix i 

115 
assume "max n m < i" 

116 
with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastsimp 

117 
qed 

118 
then show ?thesis .. 

119 
qed 

120 
qed 

121 

122 
lemma (in cring) up_a_inv_closed: 

123 
"p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R" 

124 
proof 

125 
assume R: "p \<in> up R" 

126 
then obtain n where "bound \<zero> n p" by auto 

127 
then have "bound \<zero> n (%i. \<ominus> p i)" by auto 

128 
then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto 

129 
qed auto 

130 

131 
lemma (in cring) up_mult_closed: 

132 
"[ p \<in> up R; q \<in> up R ] ==> 

133 
(%n. finsum R (%i. p i \<otimes> q (ni)) {..n}) \<in> up R" 

134 
proof 

135 
fix n 

136 
assume "p \<in> up R" "q \<in> up R" 

137 
then show "finsum R (%i. p i \<otimes> q (ni)) {..n} \<in> carrier R" 

138 
by (simp add: mem_upD funcsetI) 

139 
next 

140 
assume UP: "p \<in> up R" "q \<in> up R" 

141 
show "EX n. bound \<zero> n (%n. finsum R (%i. p i \<otimes> q (n  i)) {..n})" 

142 
proof  

143 
from UP obtain n where boundn: "bound \<zero> n p" by fast 

144 
from UP obtain m where boundm: "bound \<zero> m q" by fast 

145 
have "bound \<zero> (n + m) (%n. finsum R (%i. p i \<otimes> q (n  i)) {..n})" 

146 
proof 

147 
fix k 

148 
assume bound: "n + m < k" 

149 
{ 

150 
fix i 

151 
have "p i \<otimes> q (ki) = \<zero>" 

152 
proof (cases "n < i") 

153 
case True 

154 
with boundn have "p i = \<zero>" by auto 

155 
moreover from UP have "q (ki) \<in> carrier R" by auto 

156 
ultimately show ?thesis by simp 

157 
next 

158 
case False 

159 
with bound have "m < ki" by arith 

160 
with boundm have "q (ki) = \<zero>" by auto 

161 
moreover from UP have "p i \<in> carrier R" by auto 

162 
ultimately show ?thesis by simp 

163 
qed 

164 
} 

165 
then show "finsum R (%i. p i \<otimes> q (ki)) {..k} = \<zero>" 

166 
by (simp add: Pi_def) 

167 
qed 

168 
then show ?thesis by fast 

169 
qed 

170 
qed 

171 

172 
subsection {* Effect of operations on coefficients *} 

173 

174 
locale UP = struct R + struct P + 

175 
defines P_def: "P == UP R" 

176 

177 
locale UP_cring = UP + cring R 

178 

179 
locale UP_domain = UP_cring + "domain" R 

180 

181 
text {* 

14651  182 
Temporarily declare @{text UP.P_def} as simp rule. 
183 
*} (* TODO: use antiquotation once text (in locale) is supported. *) 

13940  184 

185 
declare (in UP) P_def [simp] 

186 

187 
lemma (in UP_cring) coeff_monom [simp]: 

188 
"a \<in> carrier R ==> 

189 
coeff P (monom P a m) n = (if m=n then a else \<zero>)" 

190 
proof  

191 
assume R: "a \<in> carrier R" 

192 
then have "(%n. if n = m then a else \<zero>) \<in> up R" 

193 
using up_def by force 

194 
with R show ?thesis by (simp add: UP_def) 

195 
qed 

196 

197 
lemma (in UP_cring) coeff_zero [simp]: 

198 
"coeff P \<zero>\<^sub>2 n = \<zero>" 

199 
by (auto simp add: UP_def) 

200 

201 
lemma (in UP_cring) coeff_one [simp]: 

202 
"coeff P \<one>\<^sub>2 n = (if n=0 then \<one> else \<zero>)" 

203 
using up_one_closed by (simp add: UP_def) 

204 

205 
lemma (in UP_cring) coeff_smult [simp]: 

206 
"[ a \<in> carrier R; p \<in> carrier P ] ==> 

207 
coeff P (a \<odot>\<^sub>2 p) n = a \<otimes> coeff P p n" 

208 
by (simp add: UP_def up_smult_closed) 

209 

210 
lemma (in UP_cring) coeff_add [simp]: 

211 
"[ p \<in> carrier P; q \<in> carrier P ] ==> 

212 
coeff P (p \<oplus>\<^sub>2 q) n = coeff P p n \<oplus> coeff P q n" 

213 
by (simp add: UP_def up_add_closed) 

214 

215 
lemma (in UP_cring) coeff_mult [simp]: 

216 
"[ p \<in> carrier P; q \<in> carrier P ] ==> 

217 
coeff P (p \<otimes>\<^sub>2 q) n = finsum R (%i. coeff P p i \<otimes> coeff P q (ni)) {..n}" 

218 
by (simp add: UP_def up_mult_closed) 

219 

220 
lemma (in UP) up_eqI: 

221 
assumes prem: "!!n. coeff P p n = coeff P q n" 

222 
and R: "p \<in> carrier P" "q \<in> carrier P" 

223 
shows "p = q" 

224 
proof 

225 
fix x 

226 
from prem and R show "p x = q x" by (simp add: UP_def) 

227 
qed 

228 

229 
subsection {* Polynomials form a commutative ring. *} 

230 

231 
text {* Operations are closed over @{term "P"}. *} 

232 

233 
lemma (in UP_cring) UP_mult_closed [simp]: 

234 
"[ p \<in> carrier P; q \<in> carrier P ] ==> p \<otimes>\<^sub>2 q \<in> carrier P" 

235 
by (simp add: UP_def up_mult_closed) 

236 

237 
lemma (in UP_cring) UP_one_closed [simp]: 

238 
"\<one>\<^sub>2 \<in> carrier P" 

239 
by (simp add: UP_def up_one_closed) 

240 

241 
lemma (in UP_cring) UP_zero_closed [intro, simp]: 

242 
"\<zero>\<^sub>2 \<in> carrier P" 

243 
by (auto simp add: UP_def) 

244 

245 
lemma (in UP_cring) UP_a_closed [intro, simp]: 

246 
"[ p \<in> carrier P; q \<in> carrier P ] ==> p \<oplus>\<^sub>2 q \<in> carrier P" 

247 
by (simp add: UP_def up_add_closed) 

248 

249 
lemma (in UP_cring) monom_closed [simp]: 

250 
"a \<in> carrier R ==> monom P a n \<in> carrier P" 

251 
by (auto simp add: UP_def up_def Pi_def) 

252 

253 
lemma (in UP_cring) UP_smult_closed [simp]: 

254 
"[ a \<in> carrier R; p \<in> carrier P ] ==> a \<odot>\<^sub>2 p \<in> carrier P" 

255 
by (simp add: UP_def up_smult_closed) 

256 

257 
lemma (in UP) coeff_closed [simp]: 

258 
"p \<in> carrier P ==> coeff P p n \<in> carrier R" 

259 
by (auto simp add: UP_def) 

260 

261 
declare (in UP) P_def [simp del] 

262 

263 
text {* Algebraic ring properties *} 

264 

265 
lemma (in UP_cring) UP_a_assoc: 

266 
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P" 

267 
shows "(p \<oplus>\<^sub>2 q) \<oplus>\<^sub>2 r = p \<oplus>\<^sub>2 (q \<oplus>\<^sub>2 r)" 

268 
by (rule up_eqI, simp add: a_assoc R, simp_all add: R) 

269 

270 
lemma (in UP_cring) UP_l_zero [simp]: 

271 
assumes R: "p \<in> carrier P" 

272 
shows "\<zero>\<^sub>2 \<oplus>\<^sub>2 p = p" 

273 
by (rule up_eqI, simp_all add: R) 

274 

275 
lemma (in UP_cring) UP_l_neg_ex: 

276 
assumes R: "p \<in> carrier P" 

277 
shows "EX q : carrier P. q \<oplus>\<^sub>2 p = \<zero>\<^sub>2" 

278 
proof  

279 
let ?q = "%i. \<ominus> (p i)" 

280 
from R have closed: "?q \<in> carrier P" 

281 
by (simp add: UP_def P_def up_a_inv_closed) 

282 
from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)" 

283 
by (simp add: UP_def P_def up_a_inv_closed) 

284 
show ?thesis 

285 
proof 

286 
show "?q \<oplus>\<^sub>2 p = \<zero>\<^sub>2" 

287 
by (auto intro!: up_eqI simp add: R closed coeff R.l_neg) 

288 
qed (rule closed) 

289 
qed 

290 

291 
lemma (in UP_cring) UP_a_comm: 

292 
assumes R: "p \<in> carrier P" "q \<in> carrier P" 

293 
shows "p \<oplus>\<^sub>2 q = q \<oplus>\<^sub>2 p" 

294 
by (rule up_eqI, simp add: a_comm R, simp_all add: R) 

295 

296 
ML_setup {* 

14590  297 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
298 
*} 

13940  299 

300 
lemma (in UP_cring) UP_m_assoc: 

301 
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P" 

302 
shows "(p \<otimes>\<^sub>2 q) \<otimes>\<^sub>2 r = p \<otimes>\<^sub>2 (q \<otimes>\<^sub>2 r)" 

303 
proof (rule up_eqI) 

304 
fix n 

305 
{ 

306 
fix k and a b c :: "nat=>'a" 

307 
assume R: "a \<in> UNIV > carrier R" "b \<in> UNIV > carrier R" 

308 
"c \<in> UNIV > carrier R" 

309 
then have "k <= n ==> 

310 
finsum R (%j. finsum R (%i. a i \<otimes> b (ji)) {..j} \<otimes> c (nj)) {..k} = 

311 
finsum R (%j. a j \<otimes> finsum R (%i. b i \<otimes> c (nji)) {..kj}) {..k}" 

312 
(is "_ ==> ?eq k") 

313 
proof (induct k) 

314 
case 0 then show ?case by (simp add: Pi_def m_assoc) 

315 
next 

316 
case (Suc k) 

317 
then have "k <= n" by arith 

318 
then have "?eq k" by (rule Suc) 

319 
with R show ?case 

320 
by (simp cong: finsum_cong 

321 
add: Suc_diff_le Pi_def l_distr r_distr m_assoc) 

322 
(simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc) 

323 
qed 

324 
} 

325 
with R show "coeff P ((p \<otimes>\<^sub>2 q) \<otimes>\<^sub>2 r) n = coeff P (p \<otimes>\<^sub>2 (q \<otimes>\<^sub>2 r)) n" 

326 
by (simp add: Pi_def) 

327 
qed (simp_all add: R) 

328 

329 
ML_setup {* 

14590  330 
simpset_ref() := simpset() setsubgoaler asm_simp_tac; 
331 
*} 

13940  332 

333 
lemma (in UP_cring) UP_l_one [simp]: 

334 
assumes R: "p \<in> carrier P" 

335 
shows "\<one>\<^sub>2 \<otimes>\<^sub>2 p = p" 

336 
proof (rule up_eqI) 

337 
fix n 

338 
show "coeff P (\<one>\<^sub>2 \<otimes>\<^sub>2 p) n = coeff P p n" 

339 
proof (cases n) 

340 
case 0 with R show ?thesis by simp 

341 
next 

342 
case Suc with R show ?thesis 

343 
by (simp del: finsum_Suc add: finsum_Suc2 Pi_def) 

344 
qed 

345 
qed (simp_all add: R) 

346 

347 
lemma (in UP_cring) UP_l_distr: 

348 
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P" 

349 
shows "(p \<oplus>\<^sub>2 q) \<otimes>\<^sub>2 r = (p \<otimes>\<^sub>2 r) \<oplus>\<^sub>2 (q \<otimes>\<^sub>2 r)" 

350 
by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R) 

351 

352 
lemma (in UP_cring) UP_m_comm: 

353 
assumes R: "p \<in> carrier P" "q \<in> carrier P" 

354 
shows "p \<otimes>\<^sub>2 q = q \<otimes>\<^sub>2 p" 

355 
proof (rule up_eqI) 

356 
fix n 

357 
{ 

358 
fix k and a b :: "nat=>'a" 

359 
assume R: "a \<in> UNIV > carrier R" "b \<in> UNIV > carrier R" 

360 
then have "k <= n ==> 

361 
finsum R (%i. a i \<otimes> b (ni)) {..k} = 

362 
finsum R (%i. a (ki) \<otimes> b (i+nk)) {..k}" 

363 
(is "_ ==> ?eq k") 

364 
proof (induct k) 

365 
case 0 then show ?case by (simp add: Pi_def) 

366 
next 

367 
case (Suc k) then show ?case 

368 
by (subst finsum_Suc2) (simp add: Pi_def a_comm)+ 

369 
qed 

370 
} 

371 
note l = this 

372 
from R show "coeff P (p \<otimes>\<^sub>2 q) n = coeff P (q \<otimes>\<^sub>2 p) n" 

373 
apply (simp add: Pi_def) 

374 
apply (subst l) 

375 
apply (auto simp add: Pi_def) 

376 
apply (simp add: m_comm) 

377 
done 

378 
qed (simp_all add: R) 

379 

380 
theorem (in UP_cring) UP_cring: 

381 
"cring P" 

382 
by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero 

383 
UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr) 

384 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

385 
lemma (in UP_cring) UP_ring: (* preliminary *) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

386 
"ring P" 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

387 
by (auto intro: ring.intro cring.axioms UP_cring) 
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

388 

13940  389 
lemma (in UP_cring) UP_a_inv_closed [intro, simp]: 
390 
"p \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> carrier P" 

391 
by (rule abelian_group.a_inv_closed 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

392 
[OF ring.is_abelian_group [OF UP_ring]]) 
13940  393 

394 
lemma (in UP_cring) coeff_a_inv [simp]: 

395 
assumes R: "p \<in> carrier P" 

396 
shows "coeff P (\<ominus>\<^sub>2 p) n = \<ominus> (coeff P p n)" 

397 
proof  

398 
from R coeff_closed UP_a_inv_closed have 

399 
"coeff P (\<ominus>\<^sub>2 p) n = \<ominus> coeff P p n \<oplus> (coeff P p n \<oplus> coeff P (\<ominus>\<^sub>2 p) n)" 

400 
by algebra 

401 
also from R have "... = \<ominus> (coeff P p n)" 

402 
by (simp del: coeff_add add: coeff_add [THEN sym] 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

403 
abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]]) 
13940  404 
finally show ?thesis . 
405 
qed 

406 

407 
text {* 

408 
Instantiation of lemmas from @{term cring}. 

409 
*} 

410 

411 
lemma (in UP_cring) UP_monoid: 

412 
"monoid P" 

413 
by (fast intro!: cring.is_comm_monoid comm_monoid.axioms monoid.intro 

414 
UP_cring) 

415 
(* TODO: provide cring.is_monoid *) 

416 

417 
lemma (in UP_cring) UP_comm_semigroup: 

418 
"comm_semigroup P" 

419 
by (fast intro!: cring.is_comm_monoid comm_monoid.axioms comm_semigroup.intro 

420 
UP_cring) 

421 

422 
lemma (in UP_cring) UP_comm_monoid: 

423 
"comm_monoid P" 

424 
by (fast intro!: cring.is_comm_monoid UP_cring) 

425 

426 
lemma (in UP_cring) UP_abelian_monoid: 

427 
"abelian_monoid P" 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

428 
by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring) 
13940  429 

430 
lemma (in UP_cring) UP_abelian_group: 

431 
"abelian_group P" 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

432 
by (fast intro!: ring.is_abelian_group UP_ring) 
13940  433 

434 
lemmas (in UP_cring) UP_r_one [simp] = 

435 
monoid.r_one [OF UP_monoid] 

436 

437 
lemmas (in UP_cring) UP_nat_pow_closed [intro, simp] = 

438 
monoid.nat_pow_closed [OF UP_monoid] 

439 

440 
lemmas (in UP_cring) UP_nat_pow_0 [simp] = 

441 
monoid.nat_pow_0 [OF UP_monoid] 

442 

443 
lemmas (in UP_cring) UP_nat_pow_Suc [simp] = 

444 
monoid.nat_pow_Suc [OF UP_monoid] 

445 

446 
lemmas (in UP_cring) UP_nat_pow_one [simp] = 

447 
monoid.nat_pow_one [OF UP_monoid] 

448 

449 
lemmas (in UP_cring) UP_nat_pow_mult = 

450 
monoid.nat_pow_mult [OF UP_monoid] 

451 

452 
lemmas (in UP_cring) UP_nat_pow_pow = 

453 
monoid.nat_pow_pow [OF UP_monoid] 

454 

455 
lemmas (in UP_cring) UP_m_lcomm = 

456 
comm_semigroup.m_lcomm [OF UP_comm_semigroup] 

457 

458 
lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm 

459 

460 
lemmas (in UP_cring) UP_nat_pow_distr = 

461 
comm_monoid.nat_pow_distr [OF UP_comm_monoid] 

462 

463 
lemmas (in UP_cring) UP_a_lcomm = abelian_monoid.a_lcomm [OF UP_abelian_monoid] 

464 

465 
lemmas (in UP_cring) UP_r_zero [simp] = 

466 
abelian_monoid.r_zero [OF UP_abelian_monoid] 

467 

468 
lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm 

469 

470 
lemmas (in UP_cring) UP_finsum_empty [simp] = 

471 
abelian_monoid.finsum_empty [OF UP_abelian_monoid] 

472 

473 
lemmas (in UP_cring) UP_finsum_insert [simp] = 

474 
abelian_monoid.finsum_insert [OF UP_abelian_monoid] 

475 

476 
lemmas (in UP_cring) UP_finsum_zero [simp] = 

477 
abelian_monoid.finsum_zero [OF UP_abelian_monoid] 

478 

479 
lemmas (in UP_cring) UP_finsum_closed [simp] = 

480 
abelian_monoid.finsum_closed [OF UP_abelian_monoid] 

481 

482 
lemmas (in UP_cring) UP_finsum_Un_Int = 

483 
abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid] 

484 

485 
lemmas (in UP_cring) UP_finsum_Un_disjoint = 

486 
abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid] 

487 

488 
lemmas (in UP_cring) UP_finsum_addf = 

489 
abelian_monoid.finsum_addf [OF UP_abelian_monoid] 

490 

491 
lemmas (in UP_cring) UP_finsum_cong' = 

492 
abelian_monoid.finsum_cong' [OF UP_abelian_monoid] 

493 

494 
lemmas (in UP_cring) UP_finsum_0 [simp] = 

495 
abelian_monoid.finsum_0 [OF UP_abelian_monoid] 

496 

497 
lemmas (in UP_cring) UP_finsum_Suc [simp] = 

498 
abelian_monoid.finsum_Suc [OF UP_abelian_monoid] 

499 

500 
lemmas (in UP_cring) UP_finsum_Suc2 = 

501 
abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid] 

502 

503 
lemmas (in UP_cring) UP_finsum_add [simp] = 

504 
abelian_monoid.finsum_add [OF UP_abelian_monoid] 

505 

506 
lemmas (in UP_cring) UP_finsum_cong = 

507 
abelian_monoid.finsum_cong [OF UP_abelian_monoid] 

508 

509 
lemmas (in UP_cring) UP_minus_closed [intro, simp] = 

510 
abelian_group.minus_closed [OF UP_abelian_group] 

511 

512 
lemmas (in UP_cring) UP_a_l_cancel [simp] = 

513 
abelian_group.a_l_cancel [OF UP_abelian_group] 

514 

515 
lemmas (in UP_cring) UP_a_r_cancel [simp] = 

516 
abelian_group.a_r_cancel [OF UP_abelian_group] 

517 

518 
lemmas (in UP_cring) UP_l_neg = 

519 
abelian_group.l_neg [OF UP_abelian_group] 

520 

521 
lemmas (in UP_cring) UP_r_neg = 

522 
abelian_group.r_neg [OF UP_abelian_group] 

523 

524 
lemmas (in UP_cring) UP_minus_zero [simp] = 

525 
abelian_group.minus_zero [OF UP_abelian_group] 

526 

527 
lemmas (in UP_cring) UP_minus_minus [simp] = 

528 
abelian_group.minus_minus [OF UP_abelian_group] 

529 

530 
lemmas (in UP_cring) UP_minus_add = 

531 
abelian_group.minus_add [OF UP_abelian_group] 

532 

533 
lemmas (in UP_cring) UP_r_neg2 = 

534 
abelian_group.r_neg2 [OF UP_abelian_group] 

535 

536 
lemmas (in UP_cring) UP_r_neg1 = 

537 
abelian_group.r_neg1 [OF UP_abelian_group] 

538 

539 
lemmas (in UP_cring) UP_r_distr = 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

540 
ring.r_distr [OF UP_ring] 
13940  541 

542 
lemmas (in UP_cring) UP_l_null [simp] = 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

543 
ring.l_null [OF UP_ring] 
13940  544 

545 
lemmas (in UP_cring) UP_r_null [simp] = 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

546 
ring.r_null [OF UP_ring] 
13940  547 

548 
lemmas (in UP_cring) UP_l_minus = 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

549 
ring.l_minus [OF UP_ring] 
13940  550 

551 
lemmas (in UP_cring) UP_r_minus = 

14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

552 
ring.r_minus [OF UP_ring] 
13940  553 

554 
lemmas (in UP_cring) UP_finsum_ldistr = 

555 
cring.finsum_ldistr [OF UP_cring] 

556 

557 
lemmas (in UP_cring) UP_finsum_rdistr = 

558 
cring.finsum_rdistr [OF UP_cring] 

559 

560 
subsection {* Polynomials form an Algebra *} 

561 

562 
lemma (in UP_cring) UP_smult_l_distr: 

563 
"[ a \<in> carrier R; b \<in> carrier R; p \<in> carrier P ] ==> 

564 
(a \<oplus> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 b \<odot>\<^sub>2 p" 

565 
by (rule up_eqI) (simp_all add: R.l_distr) 

566 

567 
lemma (in UP_cring) UP_smult_r_distr: 

568 
"[ a \<in> carrier R; p \<in> carrier P; q \<in> carrier P ] ==> 

569 
a \<odot>\<^sub>2 (p \<oplus>\<^sub>2 q) = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 a \<odot>\<^sub>2 q" 

570 
by (rule up_eqI) (simp_all add: R.r_distr) 

571 

572 
lemma (in UP_cring) UP_smult_assoc1: 

573 
"[ a \<in> carrier R; b \<in> carrier R; p \<in> carrier P ] ==> 

574 
(a \<otimes> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 p)" 

575 
by (rule up_eqI) (simp_all add: R.m_assoc) 

576 

577 
lemma (in UP_cring) UP_smult_one [simp]: 

578 
"p \<in> carrier P ==> \<one> \<odot>\<^sub>2 p = p" 

579 
by (rule up_eqI) simp_all 

580 

581 
lemma (in UP_cring) UP_smult_assoc2: 

582 
"[ a \<in> carrier R; p \<in> carrier P; q \<in> carrier P ] ==> 

583 
(a \<odot>\<^sub>2 p) \<otimes>\<^sub>2 q = a \<odot>\<^sub>2 (p \<otimes>\<^sub>2 q)" 

584 
by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def) 

585 

586 
text {* 

587 
Instantiation of lemmas from @{term algebra}. 

588 
*} 

589 

590 
(* TODO: move to CRing.thy, really a fact missing from the locales package *) 

591 

592 
lemma (in cring) cring: 

593 
"cring R" 

594 
by (fast intro: cring.intro prems) 

595 

596 
lemma (in UP_cring) UP_algebra: 

597 
"algebra R P" 

598 
by (auto intro: algebraI cring UP_cring UP_smult_l_distr UP_smult_r_distr 

599 
UP_smult_assoc1 UP_smult_assoc2) 

600 

601 
lemmas (in UP_cring) UP_smult_l_null [simp] = 

602 
algebra.smult_l_null [OF UP_algebra] 

603 

604 
lemmas (in UP_cring) UP_smult_r_null [simp] = 

605 
algebra.smult_r_null [OF UP_algebra] 

606 

607 
lemmas (in UP_cring) UP_smult_l_minus = 

608 
algebra.smult_l_minus [OF UP_algebra] 

609 

610 
lemmas (in UP_cring) UP_smult_r_minus = 

611 
algebra.smult_r_minus [OF UP_algebra] 

612 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13940
diff
changeset

613 
subsection {* Further lemmas involving monomials *} 
13940  614 

615 
lemma (in UP_cring) monom_zero [simp]: 

616 
"monom P \<zero> n = \<zero>\<^sub>2" 

617 
by (simp add: UP_def P_def) 

618 

619 
ML_setup {* 

14590  620 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
621 
*} 

13940  622 

623 
lemma (in UP_cring) monom_mult_is_smult: 

624 
assumes R: "a \<in> carrier R" "p \<in> carrier P" 

625 
shows "monom P a 0 \<otimes>\<^sub>2 p = a \<odot>\<^sub>2 p" 

626 
proof (rule up_eqI) 

627 
fix n 

628 
have "coeff P (p \<otimes>\<^sub>2 monom P a 0) n = coeff P (a \<odot>\<^sub>2 p) n" 

629 
proof (cases n) 

630 
case 0 with R show ?thesis by (simp add: R.m_comm) 

631 
next 

632 
case Suc with R show ?thesis 

633 
by (simp cong: finsum_cong add: R.r_null Pi_def) 

634 
(simp add: m_comm) 

635 
qed 

636 
with R show "coeff P (monom P a 0 \<otimes>\<^sub>2 p) n = coeff P (a \<odot>\<^sub>2 p) n" 

637 
by (simp add: UP_m_comm) 

638 
qed (simp_all add: R) 

639 

640 
ML_setup {* 

14590  641 
simpset_ref() := simpset() setsubgoaler asm_simp_tac; 
642 
*} 

13940  643 

644 
lemma (in UP_cring) monom_add [simp]: 

645 
"[ a \<in> carrier R; b \<in> carrier R ] ==> 

646 
monom P (a \<oplus> b) n = monom P a n \<oplus>\<^sub>2 monom P b n" 

647 
by (rule up_eqI) simp_all 

648 

649 
ML_setup {* 

14590  650 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
651 
*} 

13940  652 

653 
lemma (in UP_cring) monom_one_Suc: 

654 
"monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1" 

655 
proof (rule up_eqI) 

656 
fix k 

657 
show "coeff P (monom P \<one> (Suc n)) k = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" 

658 
proof (cases "k = Suc n") 

659 
case True show ?thesis 

660 
proof  

661 
from True have less_add_diff: 

662 
"!!i. [ n < i; i <= n + m ] ==> n + m  i < m" by arith 

663 
from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp 

664 
also from True 

665 
have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes> 

666 
coeff P (monom P \<one> 1) (k  i)) ({..n(} Un {n})" 

667 
by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def) 

668 
also have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes> 

669 
coeff P (monom P \<one> 1) (k  i)) {..n}" 

670 
by (simp only: ivl_disj_un_singleton) 

671 
also from True have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes> 

672 
coeff P (monom P \<one> 1) (k  i)) ({..n} Un {)n..k})" 

673 
by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one 

674 
order_less_imp_not_eq Pi_def) 

675 
also from True have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" 

676 
by (simp add: ivl_disj_un_one) 

677 
finally show ?thesis . 

678 
qed 

679 
next 

680 
case False 

681 
note neq = False 

682 
let ?s = 

683 
"(\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k  i then \<one> else \<zero>))" 

684 
from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp 

685 
also have "... = finsum R ?s {..k}" 

686 
proof  

687 
have f1: "finsum R ?s {..n(} = \<zero>" by (simp cong: finsum_cong add: Pi_def) 

688 
from neq have f2: "finsum R ?s {n} = \<zero>" 

689 
by (simp cong: finsum_cong add: Pi_def) arith 

690 
have f3: "n < k ==> finsum R ?s {)n..k} = \<zero>" 

691 
by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def) 

692 
show ?thesis 

693 
proof (cases "k < n") 

694 
case True then show ?thesis by (simp cong: finsum_cong add: Pi_def) 

695 
next 

696 
case False then have n_le_k: "n <= k" by arith 

697 
show ?thesis 

698 
proof (cases "n = k") 

699 
case True 

700 
then have "\<zero> = finsum R ?s ({..n(} \<union> {n})" 

701 
by (simp cong: finsum_cong add: finsum_Un_disjoint 

702 
ivl_disj_int_singleton Pi_def) 

703 
also from True have "... = finsum R ?s {..k}" 

704 
by (simp only: ivl_disj_un_singleton) 

705 
finally show ?thesis . 

706 
next 

707 
case False with n_le_k have n_less_k: "n < k" by arith 

708 
with neq have "\<zero> = finsum R ?s ({..n(} \<union> {n})" 

709 
by (simp add: finsum_Un_disjoint f1 f2 

710 
ivl_disj_int_singleton Pi_def del: Un_insert_right) 

711 
also have "... = finsum R ?s {..n}" 

712 
by (simp only: ivl_disj_un_singleton) 

713 
also from n_less_k neq have "... = finsum R ?s ({..n} \<union> {)n..k})" 

714 
by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def) 

715 
also from n_less_k have "... = finsum R ?s {..k}" 

716 
by (simp only: ivl_disj_un_one) 

717 
finally show ?thesis . 

718 
qed 

719 
qed 

720 
qed 

721 
also have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" by simp 

722 
finally show ?thesis . 

723 
qed 

724 
qed (simp_all) 

725 

726 
ML_setup {* 

14590  727 
simpset_ref() := simpset() setsubgoaler asm_simp_tac; 
728 
*} 

13940  729 

730 
lemma (in UP_cring) monom_mult_smult: 

731 
"[ a \<in> carrier R; b \<in> carrier R ] ==> monom P (a \<otimes> b) n = a \<odot>\<^sub>2 monom P b n" 

732 
by (rule up_eqI) simp_all 

733 

734 
lemma (in UP_cring) monom_one [simp]: 

735 
"monom P \<one> 0 = \<one>\<^sub>2" 

736 
by (rule up_eqI) simp_all 

737 

738 
lemma (in UP_cring) monom_one_mult: 

739 
"monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m" 

740 
proof (induct n) 

741 
case 0 show ?case by simp 

742 
next 

743 
case Suc then show ?case 

744 
by (simp only: add_Suc monom_one_Suc) (simp add: UP_m_ac) 

745 
qed 

746 

747 
lemma (in UP_cring) monom_mult [simp]: 

748 
assumes R: "a \<in> carrier R" "b \<in> carrier R" 

749 
shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^sub>2 monom P b m" 

750 
proof  

751 
from R have "monom P (a \<otimes> b) (n + m) = monom P (a \<otimes> b \<otimes> \<one>) (n + m)" by simp 

752 
also from R have "... = a \<otimes> b \<odot>\<^sub>2 monom P \<one> (n + m)" 

753 
by (simp add: monom_mult_smult del: r_one) 

754 
also have "... = a \<otimes> b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m)" 

755 
by (simp only: monom_one_mult) 

756 
also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m))" 

757 
by (simp add: UP_smult_assoc1) 

758 
also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> m \<otimes>\<^sub>2 monom P \<one> n))" 

759 
by (simp add: UP_m_comm) 

760 
also from R have "... = a \<odot>\<^sub>2 ((b \<odot>\<^sub>2 monom P \<one> m) \<otimes>\<^sub>2 monom P \<one> n)" 

761 
by (simp add: UP_smult_assoc2) 

762 
also from R have "... = a \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m))" 

763 
by (simp add: UP_m_comm) 

764 
also from R have "... = (a \<odot>\<^sub>2 monom P \<one> n) \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m)" 

765 
by (simp add: UP_smult_assoc2) 

766 
also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^sub>2 monom P (b \<otimes> \<one>) m" 

767 
by (simp add: monom_mult_smult del: r_one) 

768 
also from R have "... = monom P a n \<otimes>\<^sub>2 monom P b m" by simp 

769 
finally show ?thesis . 

770 
qed 

771 

772 
lemma (in UP_cring) monom_a_inv [simp]: 

773 
"a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^sub>2 monom P a n" 

774 
by (rule up_eqI) simp_all 

775 

776 
lemma (in UP_cring) monom_inj: 

777 
"inj_on (%a. monom P a n) (carrier R)" 

778 
proof (rule inj_onI) 

779 
fix x y 

780 
assume R: "x \<in> carrier R" "y \<in> carrier R" and eq: "monom P x n = monom P y n" 

781 
then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp 

782 
with R show "x = y" by simp 

783 
qed 

784 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13940
diff
changeset

785 
subsection {* The degree function *} 
13940  786 

14651  787 
constdefs (structure R) 
788 
deg :: "[_, nat => 'a] => nat" 

789 
"deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)" 

13940  790 

791 
lemma (in UP_cring) deg_aboveI: 

792 
"[ (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P ] ==> deg R p <= n" 

793 
by (unfold deg_def P_def) (fast intro: Least_le) 

794 
(* 

795 
lemma coeff_bound_ex: "EX n. bound n (coeff p)" 

796 
proof  

797 
have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) 

798 
then obtain n where "bound n (coeff p)" by (unfold UP_def) fast 

799 
then show ?thesis .. 

800 
qed 

801 

802 
lemma bound_coeff_obtain: 

803 
assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P" 

804 
proof  

805 
have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) 

806 
then obtain n where "bound n (coeff p)" by (unfold UP_def) fast 

807 
with prem show P . 

808 
qed 

809 
*) 

810 
lemma (in UP_cring) deg_aboveD: 

811 
"[ deg R p < m; p \<in> carrier P ] ==> coeff P p m = \<zero>" 

812 
proof  

813 
assume R: "p \<in> carrier P" and "deg R p < m" 

814 
from R obtain n where "bound \<zero> n (coeff P p)" 

815 
by (auto simp add: UP_def P_def) 

816 
then have "bound \<zero> (deg R p) (coeff P p)" 

817 
by (auto simp: deg_def P_def dest: LeastI) 

818 
then show ?thesis by (rule boundD) 

819 
qed 

820 

821 
lemma (in UP_cring) deg_belowI: 

822 
assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>" 

823 
and R: "p \<in> carrier P" 

824 
shows "n <= deg R p" 

825 
 {* Logically, this is a slightly stronger version of 

826 
@{thm [source] deg_aboveD} *} 

827 
proof (cases "n=0") 

828 
case True then show ?thesis by simp 

829 
next 

830 
case False then have "coeff P p n ~= \<zero>" by (rule non_zero) 

831 
then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R) 

832 
then show ?thesis by arith 

833 
qed 

834 

835 
lemma (in UP_cring) lcoeff_nonzero_deg: 

836 
assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P" 

837 
shows "coeff P p (deg R p) ~= \<zero>" 

838 
proof  

839 
from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \<zero>" 

840 
proof  

841 
have minus: "!!(n::nat) m. n ~= 0 ==> (n  Suc 0 < m) = (n <= m)" 

842 
by arith 

843 
(* TODO: why does proof not work with "1" *) 

844 
from deg have "deg R p  1 < (LEAST n. bound \<zero> n (coeff P p))" 

845 
by (unfold deg_def P_def) arith 

846 
then have "~ bound \<zero> (deg R p  1) (coeff P p)" by (rule not_less_Least) 

847 
then have "EX m. deg R p  1 < m & coeff P p m ~= \<zero>" 

848 
by (unfold bound_def) fast 

849 
then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus) 

850 
then show ?thesis by auto 

851 
qed 

852 
with deg_belowI R have "deg R p = m" by fastsimp 

853 
with m_coeff show ?thesis by simp 

854 
qed 

855 

856 
lemma (in UP_cring) lcoeff_nonzero_nonzero: 

857 
assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P" 

858 
shows "coeff P p 0 ~= \<zero>" 

859 
proof  

860 
have "EX m. coeff P p m ~= \<zero>" 

861 
proof (rule classical) 

862 
assume "~ ?thesis" 

863 
with R have "p = \<zero>\<^sub>2" by (auto intro: up_eqI) 

864 
with nonzero show ?thesis by contradiction 

865 
qed 

866 
then obtain m where coeff: "coeff P p m ~= \<zero>" .. 

867 
then have "m <= deg R p" by (rule deg_belowI) 

868 
then have "m = 0" by (simp add: deg) 

869 
with coeff show ?thesis by simp 

870 
qed 

871 

872 
lemma (in UP_cring) lcoeff_nonzero: 

873 
assumes neq: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P" 

874 
shows "coeff P p (deg R p) ~= \<zero>" 

875 
proof (cases "deg R p = 0") 

876 
case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero) 

877 
next 

878 
case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg) 

879 
qed 

880 

881 
lemma (in UP_cring) deg_eqI: 

882 
"[ !!m. n < m ==> coeff P p m = \<zero>; 

883 
!!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P ] ==> deg R p = n" 

884 
by (fast intro: le_anti_sym deg_aboveI deg_belowI) 

885 

886 
(* Degree and polynomial operations *) 

887 

888 
lemma (in UP_cring) deg_add [simp]: 

889 
assumes R: "p \<in> carrier P" "q \<in> carrier P" 

890 
shows "deg R (p \<oplus>\<^sub>2 q) <= max (deg R p) (deg R q)" 

891 
proof (cases "deg R p <= deg R q") 

892 
case True show ?thesis 

893 
by (rule deg_aboveI) (simp_all add: True R deg_aboveD) 

894 
next 

895 
case False show ?thesis 

896 
by (rule deg_aboveI) (simp_all add: False R deg_aboveD) 

897 
qed 

898 

899 
lemma (in UP_cring) deg_monom_le: 

900 
"a \<in> carrier R ==> deg R (monom P a n) <= n" 

901 
by (intro deg_aboveI) simp_all 

902 

903 
lemma (in UP_cring) deg_monom [simp]: 

904 
"[ a ~= \<zero>; a \<in> carrier R ] ==> deg R (monom P a n) = n" 

905 
by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) 

906 

907 
lemma (in UP_cring) deg_const [simp]: 

908 
assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0" 

909 
proof (rule le_anti_sym) 

910 
show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R) 

911 
next 

912 
show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R) 

913 
qed 

914 

915 
lemma (in UP_cring) deg_zero [simp]: 

916 
"deg R \<zero>\<^sub>2 = 0" 

917 
proof (rule le_anti_sym) 

918 
show "deg R \<zero>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all 

919 
next 

920 
show "0 <= deg R \<zero>\<^sub>2" by (rule deg_belowI) simp_all 

921 
qed 

922 

923 
lemma (in UP_cring) deg_one [simp]: 

924 
"deg R \<one>\<^sub>2 = 0" 

925 
proof (rule le_anti_sym) 

926 
show "deg R \<one>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all 

927 
next 

928 
show "0 <= deg R \<one>\<^sub>2" by (rule deg_belowI) simp_all 

929 
qed 

930 

931 
lemma (in UP_cring) deg_uminus [simp]: 

932 
assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^sub>2 p) = deg R p" 

933 
proof (rule le_anti_sym) 

934 
show "deg R (\<ominus>\<^sub>2 p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R) 

935 
next 

936 
show "deg R p <= deg R (\<ominus>\<^sub>2 p)" 

937 
by (simp add: deg_belowI lcoeff_nonzero_deg 

938 
inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R) 

939 
qed 

940 

941 
lemma (in UP_domain) deg_smult_ring: 

942 
"[ a \<in> carrier R; p \<in> carrier P ] ==> 

943 
deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)" 

944 
by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+ 

945 

946 
lemma (in UP_domain) deg_smult [simp]: 

947 
assumes R: "a \<in> carrier R" "p \<in> carrier P" 

948 
shows "deg R (a \<odot>\<^sub>2 p) = (if a = \<zero> then 0 else deg R p)" 

949 
proof (rule le_anti_sym) 

950 
show "deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)" 

951 
by (rule deg_smult_ring) 

952 
next 

953 
show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^sub>2 p)" 

954 
proof (cases "a = \<zero>") 

955 
qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R) 

956 
qed 

957 

958 
lemma (in UP_cring) deg_mult_cring: 

959 
assumes R: "p \<in> carrier P" "q \<in> carrier P" 

960 
shows "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q" 

961 
proof (rule deg_aboveI) 

962 
fix m 

963 
assume boundm: "deg R p + deg R q < m" 

964 
{ 

965 
fix k i 

966 
assume boundk: "deg R p + deg R q < k" 

967 
then have "coeff P p i \<otimes> coeff P q (k  i) = \<zero>" 

968 
proof (cases "deg R p < i") 

969 
case True then show ?thesis by (simp add: deg_aboveD R) 

970 
next 

971 
case False with boundk have "deg R q < k  i" by arith 

972 
then show ?thesis by (simp add: deg_aboveD R) 

973 
qed 

974 
} 

975 
with boundm R show "coeff P (p \<otimes>\<^sub>2 q) m = \<zero>" by simp 

976 
qed (simp add: R) 

977 

978 
ML_setup {* 

14590  979 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
980 
*} 

13940  981 

982 
lemma (in UP_domain) deg_mult [simp]: 

983 
"[ p ~= \<zero>\<^sub>2; q ~= \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P ] ==> 

984 
deg R (p \<otimes>\<^sub>2 q) = deg R p + deg R q" 

985 
proof (rule le_anti_sym) 

986 
assume "p \<in> carrier P" " q \<in> carrier P" 

987 
show "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q" by (rule deg_mult_cring) 

988 
next 

989 
let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q  i))" 

990 
assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^sub>2" "q ~= \<zero>\<^sub>2" 

991 
have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m  k" by arith 

992 
show "deg R p + deg R q <= deg R (p \<otimes>\<^sub>2 q)" 

993 
proof (rule deg_belowI, simp add: R) 

994 
have "finsum R ?s {.. deg R p + deg R q} 

995 
= finsum R ?s ({.. deg R p(} Un {deg R p .. deg R p + deg R q})" 

996 
by (simp only: ivl_disj_un_one) 

997 
also have "... = finsum R ?s {deg R p .. deg R p + deg R q}" 

998 
by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one 

999 
deg_aboveD less_add_diff R Pi_def) 

1000 
also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})" 

1001 
by (simp only: ivl_disj_un_singleton) 

1002 
also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" 

1003 
by (simp cong: finsum_cong add: finsum_Un_disjoint 

1004 
ivl_disj_int_singleton deg_aboveD R Pi_def) 

1005 
finally have "finsum R ?s {.. deg R p + deg R q} 

1006 
= coeff P p (deg R p) \<otimes> coeff P q (deg R q)" . 

1007 
with nz show "finsum R ?s {.. deg R p + deg R q} ~= \<zero>" 

1008 
by (simp add: integral_iff lcoeff_nonzero R) 

1009 
qed (simp add: R) 

1010 
qed 

1011 

1012 
lemma (in UP_cring) coeff_finsum: 

1013 
assumes fin: "finite A" 

1014 
shows "p \<in> A > carrier P ==> 

1015 
coeff P (finsum P p A) k == finsum R (%i. coeff P (p i) k) A" 

1016 
using fin by induct (auto simp: Pi_def) 

1017 

1018 
ML_setup {* 

14590  1019 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
1020 
*} 

13940  1021 

1022 
lemma (in UP_cring) up_repr: 

1023 
assumes R: "p \<in> carrier P" 

1024 
shows "finsum P (%i. monom P (coeff P p i) i) {..deg R p} = p" 

1025 
proof (rule up_eqI) 

1026 
let ?s = "(%i. monom P (coeff P p i) i)" 

1027 
fix k 

1028 
from R have RR: "!!i. (if i = k then coeff P p i else \<zero>) \<in> carrier R" 

1029 
by simp 

1030 
show "coeff P (finsum P ?s {..deg R p}) k = coeff P p k" 

1031 
proof (cases "k <= deg R p") 

1032 
case True 

1033 
hence "coeff P (finsum P ?s {..deg R p}) k = 

1034 
coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k" 

1035 
by (simp only: ivl_disj_un_one) 

1036 
also from True 

1037 
have "... = coeff P (finsum P ?s {..k}) k" 

1038 
by (simp cong: finsum_cong add: finsum_Un_disjoint 

1039 
ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def) 

1040 
also 

1041 
have "... = coeff P (finsum P ?s ({..k(} Un {k})) k" 

1042 
by (simp only: ivl_disj_un_singleton) 

1043 
also have "... = coeff P p k" 

1044 
by (simp cong: finsum_cong add: setsum_Un_disjoint 

1045 
ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def) 

1046 
finally show ?thesis . 

1047 
next 

1048 
case False 

1049 
hence "coeff P (finsum P ?s {..deg R p}) k = 

1050 
coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k" 

1051 
by (simp only: ivl_disj_un_singleton) 

1052 
also from False have "... = coeff P p k" 

1053 
by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton 

1054 
coeff_finsum deg_aboveD R Pi_def) 

1055 
finally show ?thesis . 

1056 
qed 

1057 
qed (simp_all add: R Pi_def) 

1058 

1059 
lemma (in UP_cring) up_repr_le: 

1060 
"[ deg R p <= n; p \<in> carrier P ] ==> 

1061 
finsum P (%i. monom P (coeff P p i) i) {..n} = p" 

1062 
proof  

1063 
let ?s = "(%i. monom P (coeff P p i) i)" 

1064 
assume R: "p \<in> carrier P" and "deg R p <= n" 

1065 
then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {)deg R p..n})" 

1066 
by (simp only: ivl_disj_un_one) 

1067 
also have "... = finsum P ?s {..deg R p}" 

1068 
by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one 

1069 
deg_aboveD R Pi_def) 

1070 
also have "... = p" by (rule up_repr) 

1071 
finally show ?thesis . 

1072 
qed 

1073 

1074 
ML_setup {* 

14590  1075 
simpset_ref() := simpset() setsubgoaler asm_simp_tac; 
1076 
*} 

13940  1077 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13940
diff
changeset

1078 
subsection {* Polynomials over an integral domain form an integral domain *} 
13940  1079 

1080 
lemma domainI: 

1081 
assumes cring: "cring R" 

1082 
and one_not_zero: "one R ~= zero R" 

1083 
and integral: "!!a b. [ mult R a b = zero R; a \<in> carrier R; 

1084 
b \<in> carrier R ] ==> a = zero R  b = zero R" 

1085 
shows "domain R" 

1086 
by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems 

1087 
del: disjCI) 

1088 

1089 
lemma (in UP_domain) UP_one_not_zero: 

1090 
"\<one>\<^sub>2 ~= \<zero>\<^sub>2" 

1091 
proof 

1092 
assume "\<one>\<^sub>2 = \<zero>\<^sub>2" 

1093 
hence "coeff P \<one>\<^sub>2 0 = (coeff P \<zero>\<^sub>2 0)" by simp 

1094 
hence "\<one> = \<zero>" by simp 

1095 
with one_not_zero show "False" by contradiction 

1096 
qed 

1097 

1098 
lemma (in UP_domain) UP_integral: 

1099 
"[ p \<otimes>\<^sub>2 q = \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P ] ==> p = \<zero>\<^sub>2  q = \<zero>\<^sub>2" 

1100 
proof  

1101 
fix p q 

1102 
assume pq: "p \<otimes>\<^sub>2 q = \<zero>\<^sub>2" and R: "p \<in> carrier P" "q \<in> carrier P" 

1103 
show "p = \<zero>\<^sub>2  q = \<zero>\<^sub>2" 

1104 
proof (rule classical) 

1105 
assume c: "~ (p = \<zero>\<^sub>2  q = \<zero>\<^sub>2)" 

1106 
with R have "deg R p + deg R q = deg R (p \<otimes>\<^sub>2 q)" by simp 

1107 
also from pq have "... = 0" by simp 

1108 
finally have "deg R p + deg R q = 0" . 

1109 
then have f1: "deg R p = 0 & deg R q = 0" by simp 

1110 
from f1 R have "p = finsum P (%i. (monom P (coeff P p i) i)) {..0}" 

1111 
by (simp only: up_repr_le) 

1112 
also from R have "... = monom P (coeff P p 0) 0" by simp 

1113 
finally have p: "p = monom P (coeff P p 0) 0" . 

1114 
from f1 R have "q = finsum P (%i. (monom P (coeff P q i) i)) {..0}" 

1115 
by (simp only: up_repr_le) 

1116 
also from R have "... = monom P (coeff P q 0) 0" by simp 

1117 
finally have q: "q = monom P (coeff P q 0) 0" . 

1118 
from R have "coeff P p 0 \<otimes> coeff P q 0 = coeff P (p \<otimes>\<^sub>2 q) 0" by simp 

1119 
also from pq have "... = \<zero>" by simp 

1120 
finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" . 

1121 
with R have "coeff P p 0 = \<zero>  coeff P q 0 = \<zero>" 

1122 
by (simp add: R.integral_iff) 

1123 
with p q show "p = \<zero>\<^sub>2  q = \<zero>\<^sub>2" by fastsimp 

1124 
qed 

1125 
qed 

1126 

1127 
theorem (in UP_domain) UP_domain: 

1128 
"domain P" 

1129 
by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI) 

1130 

1131 
text {* 

1132 
Instantiation of results from @{term domain}. 

1133 
*} 

1134 

1135 
lemmas (in UP_domain) UP_zero_not_one [simp] = 

1136 
domain.zero_not_one [OF UP_domain] 

1137 

1138 
lemmas (in UP_domain) UP_integral_iff = 

1139 
domain.integral_iff [OF UP_domain] 

1140 

1141 
lemmas (in UP_domain) UP_m_lcancel = 

1142 
domain.m_lcancel [OF UP_domain] 

1143 

1144 
lemmas (in UP_domain) UP_m_rcancel = 

1145 
domain.m_rcancel [OF UP_domain] 

1146 

1147 
lemma (in UP_domain) smult_integral: 

1148 
"[ a \<odot>\<^sub>2 p = \<zero>\<^sub>2; a \<in> carrier R; p \<in> carrier P ] ==> a = \<zero>  p = \<zero>\<^sub>2" 

1149 
by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff 

1150 
inj_on_iff [OF monom_inj, of _ "\<zero>", simplified]) 

1151 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13940
diff
changeset

1152 
subsection {* Evaluation Homomorphism and Universal Property*} 
13940  1153 

1154 
ML_setup {* 

14590  1155 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
1156 
*} 

13940  1157 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13940
diff
changeset

1158 
(* alternative congruence rule (possibly more efficient) 
13940  1159 
lemma (in abelian_monoid) finsum_cong2: 
1160 
"[ !!i. i \<in> A ==> f i \<in> carrier G = True; A = B; 

1161 
!!i. i \<in> B ==> f i = g i ] ==> finsum G f A = finsum G g B" 

1162 
sorry 

1163 
*) 

1164 

1165 
theorem (in cring) diagonal_sum: 

1166 
"[ f \<in> {..n + m::nat} > carrier R; g \<in> {..n + m} > carrier R ] ==> 

1167 
finsum R (%k. finsum R (%i. f i \<otimes> g (k  i)) {..k}) {..n + m} = 

1168 
finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m  k}) {..n + m}" 

1169 
proof  

1170 
assume Rf: "f \<in> {..n + m} > carrier R" and Rg: "g \<in> {..n + m} > carrier R" 

1171 
{ 

1172 
fix j 

1173 
have "j <= n + m ==> 

1174 
finsum R (%k. finsum R (%i. f i \<otimes> g (k  i)) {..k}) {..j} = 

1175 
finsum R (%k. finsum R (%i. f k \<otimes> g i) {..j  k}) {..j}" 

1176 
proof (induct j) 

1177 
case 0 from Rf Rg show ?case by (simp add: Pi_def) 

1178 
next 

1179 
case (Suc j) 

1180 
(* The following could be simplified if there was a reasoner for 

1181 
total orders integrated with simip. *) 

1182 
have R6: "!!i k. [ k <= j; i <= Suc j  k ] ==> g i \<in> carrier R" 

1183 
using Suc by (auto intro!: funcset_mem [OF Rg]) arith 

1184 
have R8: "!!i k. [ k <= Suc j; i <= k ] ==> g (k  i) \<in> carrier R" 

1185 
using Suc by (auto intro!: funcset_mem [OF Rg]) arith 

1186 
have R9: "!!i k. [ k <= Suc j ] ==> f k \<in> carrier R" 

1187 
using Suc by (auto intro!: funcset_mem [OF Rf]) 

1188 
have R10: "!!i k. [ k <= Suc j; i <= Suc j  k ] ==> g i \<in> carrier R" 

1189 
using Suc by (auto intro!: funcset_mem [OF Rg]) arith 

1190 
have R11: "g 0 \<in> carrier R" 

1191 
using Suc by (auto intro!: funcset_mem [OF Rg]) 

1192 
from Suc show ?case 

1193 
by (simp cong: finsum_cong add: Suc_diff_le a_ac 

1194 
Pi_def R6 R8 R9 R10 R11) 

1195 
qed 

1196 
} 

1197 
then show ?thesis by fast 

1198 
qed 

1199 

1200 
lemma (in abelian_monoid) boundD_carrier: 

1201 
"[ bound \<zero> n f; n < m ] ==> f m \<in> carrier G" 

1202 
by auto 

1203 

1204 
theorem (in cring) cauchy_product: 

1205 
assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g" 

1206 
and Rf: "f \<in> {..n} > carrier R" and Rg: "g \<in> {..m} > carrier R" 

1207 
shows "finsum R (%k. finsum R (%i. f i \<otimes> g (ki)) {..k}) {..n + m} = 

1208 
finsum R f {..n} \<otimes> finsum R g {..m}" 

1209 
(* State revese direction? *) 

1210 
proof  

1211 
have f: "!!x. f x \<in> carrier R" 

1212 
proof  

1213 
fix x 

1214 
show "f x \<in> carrier R" 

1215 
using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def) 

1216 
qed 

1217 
have g: "!!x. g x \<in> carrier R" 

1218 
proof  

1219 
fix x 

1220 
show "g x \<in> carrier R" 

1221 
using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def) 

1222 
qed 

1223 
from f g have "finsum R (%k. finsum R (%i. f i \<otimes> g (ki)) {..k}) {..n + m} = 

1224 
finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m  k}) {..n + m}" 

1225 
by (simp add: diagonal_sum Pi_def) 

1226 
also have "... = finsum R 

1227 
(%k. finsum R (%i. f k \<otimes> g i) {..n + m  k}) ({..n} Un {)n..n + m})" 

1228 
by (simp only: ivl_disj_un_one) 

1229 
also from f g have "... = finsum R 

1230 
(%k. finsum R (%i. f k \<otimes> g i) {..n + m  k}) {..n}" 

1231 
by (simp cong: finsum_cong 

1232 
add: boundD [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def) 

1233 
also from f g have "... = finsum R 

1234 
(%k. finsum R (%i. f k \<otimes> g i) ({..m} Un {)m..n + m  k})) {..n}" 

1235 
by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def) 

1236 
also from f g have "... = finsum R 

1237 
(%k. finsum R (%i. f k \<otimes> g i) {..m}) {..n}" 

1238 
by (simp cong: finsum_cong 

1239 
add: boundD [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def) 

1240 
also from f g have "... = finsum R f {..n} \<otimes> finsum R g {..m}" 

1241 
by (simp add: finsum_ldistr diagonal_sum Pi_def, 

1242 
simp cong: finsum_cong add: finsum_rdistr Pi_def) 

1243 
finally show ?thesis . 

1244 
qed 

1245 

1246 
lemma (in UP_cring) const_ring_hom: 

1247 
"(%a. monom P a 0) \<in> ring_hom R P" 

1248 
by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult) 

1249 

14651  1250 
constdefs (structure S) 
1251 
eval :: "[_, _, 'a => 'b, 'b, nat => 'a] => 'b" 

1252 
"eval R S phi s == \<lambda>p \<in> carrier (UP R). 

1253 
\<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> pow S s i" 

13940  1254 
(* 
1255 
"eval R S phi s p == if p \<in> carrier (UP R) 

1256 
then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p} 

1257 
else arbitrary" 

1258 
*) 

1259 

1260 
locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R 

1261 

1262 
lemma (in ring_hom_UP_cring) eval_on_carrier: 

1263 
"p \<in> carrier P ==> 

1264 
eval R S phi s p = 

1265 
finsum S (%i. mult S (phi (coeff P p i)) (pow S s i)) {..deg R p}" 

1266 
by (unfold eval_def, fold P_def) simp 

1267 

1268 
lemma (in ring_hom_UP_cring) eval_extensional: 

1269 
"eval R S phi s \<in> extensional (carrier P)" 

1270 
by (unfold eval_def, fold P_def) simp 

1271 

1272 
theorem (in ring_hom_UP_cring) eval_ring_hom: 

1273 
"s \<in> carrier S ==> eval R S h s \<in> ring_hom P S" 

1274 
proof (rule ring_hom_memI) 

1275 
fix p 

1276 
assume RS: "p \<in> carrier P" "s \<in> carrier S" 

1277 
then show "eval R S h s p \<in> carrier S" 

1278 
by (simp only: eval_on_carrier) (simp add: Pi_def) 

1279 
next 

1280 
fix p q 

1281 
assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S" 

1282 
then show "eval R S h s (p \<otimes>\<^sub>3 q) = eval R S h s p \<otimes>\<^sub>2 eval R S h s q" 

1283 
proof (simp only: eval_on_carrier UP_mult_closed) 

1284 
from RS have 

1285 
"finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} = 

1286 
finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) 

1287 
({..deg R (p \<otimes>\<^sub>3 q)} Un {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q})" 

1288 
by (simp cong: finsum_cong 

1289 
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def 

1290 
del: coeff_mult) 

1291 
also from RS have "... = 

1292 
finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p + deg R q}" 

1293 
by (simp only: ivl_disj_un_one deg_mult_cring) 

1294 
also from RS have "... = 

1295 
finsum S (%i. 

1296 
finsum S (%k. 

1297 
(h (coeff P p k) \<otimes>\<^sub>2 h (coeff P q (ik))) \<otimes>\<^sub>2 (s (^)\<^sub>2 k \<otimes>\<^sub>2 s (^)\<^sub>2 (ik))) 

1298 
{..i}) {..deg R p + deg R q}" 

1299 
by (simp cong: finsum_cong add: nat_pow_mult Pi_def 

1300 
S.m_ac S.finsum_rdistr) 

1301 
also from RS have "... = 

1302 
finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2 

1303 
finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" 

1304 
by (simp add: S.cauchy_product [THEN sym] boundI deg_aboveD S.m_ac 

1305 
Pi_def) 

1306 
finally show 

1307 
"finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} = 

1308 
finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2 

1309 
finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" . 

1310 
qed 

1311 
next 

1312 
fix p q 

1313 
assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S" 

1314 
then show "eval R S h s (p \<oplus>\<^sub>3 q) = eval R S h s p \<oplus>\<^sub>2 eval R S h s q" 

1315 
proof (simp only: eval_on_carrier UP_a_closed) 

1316 
from RS have 

1317 
"finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} = 

1318 
finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) 

1319 
({..deg R (p \<oplus>\<^sub>3 q)} Un {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)})" 

1320 
by (simp cong: finsum_cong 

1321 
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def 

1322 
del: coeff_add) 

1323 
also from RS have "... = 

1324 
finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) 

1325 
{..max (deg R p) (deg R q)}" 

1326 
by (simp add: ivl_disj_un_one) 

1327 
also from RS have "... = 

1328 
finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)} \<oplus>\<^sub>2 

1329 
finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)}" 

1330 
by (simp cong: finsum_cong 

1331 
add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def) 

1332 
also have "... = 

1333 
finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) 

1334 
({..deg R p} Un {)deg R p..max (deg R p) (deg R q)}) \<oplus>\<^sub>2 

1335 
finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) 

1336 
({..deg R q} Un {)deg R q..max (deg R p) (deg R q)})" 

1337 
by (simp only: ivl_disj_un_one le_maxI1 le_maxI2) 

1338 
also from RS have "... = 

1339 
finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2 

1340 
finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" 

1341 
by (simp cong: finsum_cong 

1342 
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def) 

1343 
finally show 

1344 
"finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} = 

1345 
finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2 

1346 
finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" 

1347 
. 

1348 
qed 

1349 
next 

1350 
assume S: "s \<in> carrier S" 

1351 
then show "eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2" 

1352 
by (simp only: eval_on_carrier UP_one_closed) simp 

1353 
qed 

1354 

1355 
text {* Instantiation of ring homomorphism lemmas. *} 

1356 

1357 
lemma (in ring_hom_UP_cring) ring_hom_cring_P_S: 

1358 
"s \<in> carrier S ==> ring_hom_cring P S (eval R S h s)" 

1359 
by (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems 

1360 
intro: ring_hom_cring_axioms.intro eval_ring_hom) 

1361 

1362 
lemma (in ring_hom_UP_cring) UP_hom_closed [intro, simp]: 

1363 
"[ s \<in> carrier S; p \<in> carrier P ] ==> eval R S h s p \<in> carrier S" 

1364 
by (rule ring_hom_cring.hom_closed [OF ring_hom_cring_P_S]) 

1365 

1366 
lemma (in ring_hom_UP_cring) UP_hom_mult [simp]: 

1367 
"[ s \<in> carrier S; p \<in> carrier P; q \<in> carrier P ] ==> 

1368 
eval R S h s (p \<otimes>\<^sub>3 q) = eval R S h s p \<otimes>\<^sub>2 eval R S h s q" 

1369 
by (rule ring_hom_cring.hom_mult [OF ring_hom_cring_P_S]) 

1370 

1371 
lemma (in ring_hom_UP_cring) UP_hom_add [simp]: 

1372 
"[ s \<in> carrier S; p \<in> carrier P; q \<in> carrier P ] ==> 

1373 
eval R S h s (p \<oplus>\<^sub>3 q) = eval R S h s p \<oplus>\<^sub>2 eval R S h s q" 

1374 
by (rule ring_hom_cring.hom_add [OF ring_hom_cring_P_S]) 

1375 

1376 
lemma (in ring_hom_UP_cring) UP_hom_one [simp]: 

1377 
"s \<in> carrier S ==> eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2" 

1378 
by (rule ring_hom_cring.hom_one [OF ring_hom_cring_P_S]) 

1379 

1380 
lemma (in ring_hom_UP_cring) UP_hom_zero [simp]: 

1381 
"s \<in> carrier S ==> eval R S h s \<zero>\<^sub>3 = \<zero>\<^sub>2" 

1382 
by (rule ring_hom_cring.hom_zero [OF ring_hom_cring_P_S]) 

1383 

1384 
lemma (in ring_hom_UP_cring) UP_hom_a_inv [simp]: 

1385 
"[ s \<in> carrier S; p \<in> carrier P ] ==> 

1386 
(eval R S h s) (\<ominus>\<^sub>3 p) = \<ominus>\<^sub>2 (eval R S h s) p" 

1387 
by (rule ring_hom_cring.hom_a_inv [OF ring_hom_cring_P_S]) 

1388 

1389 
lemma (in ring_hom_UP_cring) UP_hom_finsum [simp]: 

1390 
"[ s \<in> carrier S; finite A; f \<in> A > carrier P ] ==> 

1391 
(eval R S h s) (finsum P f A) = finsum S (eval R S h s o f) A" 

1392 
by (rule ring_hom_cring.hom_finsum [OF ring_hom_cring_P_S]) 

1393 

1394 
lemma (in ring_hom_UP_cring) UP_hom_finprod [simp]: 

1395 
"[ s \<in> carrier S; finite A; f \<in> A > carrier P ] ==> 

1396 
(eval R S h s) (finprod P f A) = finprod S (eval R S h s o f) A" 

1397 
by (rule ring_hom_cring.hom_finprod [OF ring_hom_cring_P_S]) 

1398 

1399 
text {* Further properties of the evaluation homomorphism. *} 

1400 

1401 
(* The following lemma could be proved in UP\_cring with the additional 

1402 
assumption that h is closed. *) 

1403 

1404 
lemma (in ring_hom_UP_cring) eval_const: 

1405 
"[ s \<in> carrier S; r \<in> carrier R ] ==> eval R S h s (monom P r 0) = h r" 

1406 
by (simp only: eval_on_carrier monom_closed) simp 

1407 

1408 
text {* The following proof is complicated by the fact that in arbitrary 

1409 
rings one might have @{term "one R = zero R"}. *} 

1410 

1411 
(* TODO: simplify by cases "one R = zero R" *) 

1412 

1413 
lemma (in ring_hom_UP_cring) eval_monom1: 

1414 
"s \<in> carrier S ==> eval R S h s (monom P \<one> 1) = s" 

1415 
proof (simp only: eval_on_carrier monom_closed R.one_closed) 

1416 
assume S: "s \<in> carrier S" 

1417 
then have "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) 

1418 
{..deg R (monom P \<one> 1)} = 

1419 
finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) 

1420 
({..deg R (monom P \<one> 1)} Un {)deg R (monom P \<one> 1)..1})" 

1421 
by (simp cong: finsum_cong del: coeff_monom 

1422 
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def) 

1423 
also have "... = 

1424 
finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..1}" 

1425 
by (simp only: ivl_disj_un_one deg_monom_le R.one_closed) 

1426 
also have "... = s" 

1427 
proof (cases "s = \<zero>\<^sub>2") 

1428 
case True then show ?thesis by (simp add: Pi_def) 

1429 
next 

1430 
case False with S show ?thesis by (simp add: Pi_def) 

1431 
qed 

1432 
finally show "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) 

1433 
{..deg R (monom P \<one> 1)} = s" . 

1434 
qed 

1435 

1436 
lemma (in UP_cring) monom_pow: 

1437 
assumes R: "a \<in> carrier R" 

1438 
shows "(monom P a n) (^)\<^sub>2 m = monom P (a (^) m) (n * m)" 

c67798653056
HOLAlgebra: New polynomi 