author  paulson 
Mon, 09 May 2005 16:38:56 +0200  
changeset 15944  9b00875e21f7 
parent 15763  b901a127ac73 
child 16417  9bc16273c2d4 
permissions  rwrr 
13940  1 
(* 
14706  2 
Title: HOL/Algebra/UnivPoly.thy 
13940  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 {* 
14666  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"}). The 

16 
carrier set is a set of bounded functions from Nat to the 

17 
coefficient domain. Bounded means that these functions return zero 

18 
above a certain bound (the degree). There is a chapter on the 

14706  19 
formalisation of polynomials in the PhD thesis \cite{Ballarin:1999}, 
20 
which was implemented with axiomatic type classes. This was later 

21 
ported to Locales. 

14553  22 
*} 
23 

14666  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 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

27 
text {* 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

28 
Functions with finite support. 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

29 
*} 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

30 

14666  31 
locale bound = 
32 
fixes z :: 'a 

33 
and n :: nat 

34 
and f :: "nat => 'a" 

35 
assumes bound: "!!m. n < m \<Longrightarrow> f m = z" 

13940  36 

14666  37 
declare bound.intro [intro!] 
38 
and bound.bound [dest] 

13940  39 

40 
lemma bound_below: 

14666  41 
assumes bound: "bound z m f" and nonzero: "f n \<noteq> z" shows "n \<le> m" 
13940  42 
proof (rule classical) 
43 
assume "~ ?thesis" 

44 
then have "m < n" by arith 

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

46 
with nonzero show ?thesis by contradiction 

47 
qed 

48 

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

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

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

52 

14651  53 
constdefs (structure R) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

54 
up :: "('a, 'm) ring_scheme => (nat => 'a) set" 
14651  55 
"up R == {f. f \<in> UNIV > carrier R & (EX n. bound \<zero> n f)}" 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

56 
UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring" 
13940  57 
"UP R == ( 
58 
carrier = up R, 

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

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

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

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

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

13940  65 
coeff = (%p:up R. %n. p n) )" 
66 

67 
text {* 

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

69 
*} 

70 

71 
lemma mem_upI [intro]: 

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

73 
by (simp add: up_def Pi_def) 

74 

75 
lemma mem_upD [dest]: 

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

77 
by (simp add: up_def Pi_def) 

78 

79 
lemma (in cring) bound_upD [dest]: 

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

81 
by (simp add: up_def) 

82 

83 
lemma (in cring) up_one_closed: 

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

85 
using up_def by force 

86 

87 
lemma (in cring) up_smult_closed: 

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

89 
by force 

90 

91 
lemma (in cring) up_add_closed: 

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

93 
proof 

94 
fix n 

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

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

97 
by auto 

98 
next 

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

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

101 
proof  

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

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

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

105 
proof 

106 
fix i 

107 
assume "max n m < i" 

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

109 
qed 

110 
then show ?thesis .. 

111 
qed 

112 
qed 

113 

114 
lemma (in cring) up_a_inv_closed: 

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

116 
proof 

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

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

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

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

121 
qed auto 

122 

123 
lemma (in cring) up_mult_closed: 

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

14666  125 
(%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (ni)) \<in> up R" 
13940  126 
proof 
127 
fix n 

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

14666  129 
then show "(\<Oplus>i \<in> {..n}. p i \<otimes> q (ni)) \<in> carrier R" 
13940  130 
by (simp add: mem_upD funcsetI) 
131 
next 

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

14666  133 
show "EX n. bound \<zero> n (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (ni))" 
13940  134 
proof  
135 
from UP obtain n where boundn: "bound \<zero> n p" by fast 

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

14666  137 
have "bound \<zero> (n + m) (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n  i))" 
13940  138 
proof 
14666  139 
fix k assume bound: "n + m < k" 
13940  140 
{ 
14666  141 
fix i 
142 
have "p i \<otimes> q (ki) = \<zero>" 

143 
proof (cases "n < i") 

144 
case True 

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

13940  146 
moreover from UP have "q (ki) \<in> carrier R" by auto 
14666  147 
ultimately show ?thesis by simp 
148 
next 

149 
case False 

150 
with bound have "m < ki" by arith 

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

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

153 
ultimately show ?thesis by simp 

154 
qed 

13940  155 
} 
14666  156 
then show "(\<Oplus>i \<in> {..k}. p i \<otimes> q (ki)) = \<zero>" 
157 
by (simp add: Pi_def) 

13940  158 
qed 
159 
then show ?thesis by fast 

160 
qed 

161 
qed 

162 

14666  163 

13940  164 
subsection {* Effect of operations on coefficients *} 
165 

166 
locale UP = struct R + struct P + 

167 
defines P_def: "P == UP R" 

168 

169 
locale UP_cring = UP + cring R 

170 

171 
locale UP_domain = UP_cring + "domain" R 

172 

173 
text {* 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

174 
Temporarily declare @{thm [locale=UP] P_def} as simp rule. 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

175 
*} 
13940  176 

177 
declare (in UP) P_def [simp] 

178 

179 
lemma (in UP_cring) coeff_monom [simp]: 

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

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

182 
proof  

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

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

185 
using up_def by force 

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

187 
qed 

188 

189 
lemma (in UP_cring) coeff_zero [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

190 
"coeff P \<zero>\<^bsub>P\<^esub> n = \<zero>" 
13940  191 
by (auto simp add: UP_def) 
192 

193 
lemma (in UP_cring) coeff_one [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

194 
"coeff P \<one>\<^bsub>P\<^esub> n = (if n=0 then \<one> else \<zero>)" 
13940  195 
using up_one_closed by (simp add: UP_def) 
196 

197 
lemma (in UP_cring) coeff_smult [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

199 
coeff P (a \<odot>\<^bsub>P\<^esub> p) n = a \<otimes> coeff P p n" 
13940  200 
by (simp add: UP_def up_smult_closed) 
201 

202 
lemma (in UP_cring) coeff_add [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

204 
coeff P (p \<oplus>\<^bsub>P\<^esub> q) n = coeff P p n \<oplus> coeff P q n" 
13940  205 
by (simp add: UP_def up_add_closed) 
206 

207 
lemma (in UP_cring) coeff_mult [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

209 
coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (ni))" 
13940  210 
by (simp add: UP_def up_mult_closed) 
211 

212 
lemma (in UP) up_eqI: 

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

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

215 
shows "p = q" 

216 
proof 

217 
fix x 

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

219 
qed 

14666  220 

13940  221 
subsection {* Polynomials form a commutative ring. *} 
222 

14666  223 
text {* Operations are closed over @{term P}. *} 
13940  224 

225 
lemma (in UP_cring) UP_mult_closed [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

226 
"[ p \<in> carrier P; q \<in> carrier P ] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P" 
13940  227 
by (simp add: UP_def up_mult_closed) 
228 

229 
lemma (in UP_cring) UP_one_closed [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

230 
"\<one>\<^bsub>P\<^esub> \<in> carrier P" 
13940  231 
by (simp add: UP_def up_one_closed) 
232 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

234 
"\<zero>\<^bsub>P\<^esub> \<in> carrier P" 
13940  235 
by (auto simp add: UP_def) 
236 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

238 
"[ p \<in> carrier P; q \<in> carrier P ] ==> p \<oplus>\<^bsub>P\<^esub> q \<in> carrier P" 
13940  239 
by (simp add: UP_def up_add_closed) 
240 

241 
lemma (in UP_cring) monom_closed [simp]: 

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

243 
by (auto simp add: UP_def up_def Pi_def) 

244 

245 
lemma (in UP_cring) UP_smult_closed [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

246 
"[ a \<in> carrier R; p \<in> carrier P ] ==> a \<odot>\<^bsub>P\<^esub> p \<in> carrier P" 
13940  247 
by (simp add: UP_def up_smult_closed) 
248 

249 
lemma (in UP) coeff_closed [simp]: 

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

251 
by (auto simp add: UP_def) 

252 

253 
declare (in UP) P_def [simp del] 

254 

255 
text {* Algebraic ring properties *} 

256 

257 
lemma (in UP_cring) UP_a_assoc: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

259 
shows "(p \<oplus>\<^bsub>P\<^esub> q) \<oplus>\<^bsub>P\<^esub> r = p \<oplus>\<^bsub>P\<^esub> (q \<oplus>\<^bsub>P\<^esub> r)" 
13940  260 
by (rule up_eqI, simp add: a_assoc R, simp_all add: R) 
261 

262 
lemma (in UP_cring) UP_l_zero [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

264 
shows "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> p = p" 
13940  265 
by (rule up_eqI, simp_all add: R) 
266 

267 
lemma (in UP_cring) UP_l_neg_ex: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

269 
shows "EX q : carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>" 
13940  270 
proof  
271 
let ?q = "%i. \<ominus> (p i)" 

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

273 
by (simp add: UP_def P_def up_a_inv_closed) 

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

275 
by (simp add: UP_def P_def up_a_inv_closed) 

276 
show ?thesis 

277 
proof 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

278 
show "?q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>" 
13940  279 
by (auto intro!: up_eqI simp add: R closed coeff R.l_neg) 
280 
qed (rule closed) 

281 
qed 

282 

283 
lemma (in UP_cring) UP_a_comm: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

285 
shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p" 
13940  286 
by (rule up_eqI, simp add: a_comm R, simp_all add: R) 
287 

288 
ML_setup {* 

14590  289 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
290 
*} 

13940  291 

292 
lemma (in UP_cring) UP_m_assoc: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

294 
shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)" 
13940  295 
proof (rule up_eqI) 
296 
fix n 

297 
{ 

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

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

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

301 
then have "k <= n ==> 

14666  302 
(\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (ji)) \<otimes> c (nj)) = 
303 
(\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..kj}. b i \<otimes> c (nji)))" 

304 
(concl is "?eq k") 

13940  305 
proof (induct k) 
306 
case 0 then show ?case by (simp add: Pi_def m_assoc) 

307 
next 

308 
case (Suc k) 

309 
then have "k <= n" by arith 

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

311 
with R show ?case 

14666  312 
by (simp cong: finsum_cong 
13940  313 
add: Suc_diff_le Pi_def l_distr r_distr m_assoc) 
314 
(simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc) 

315 
qed 

316 
} 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

317 
with R show "coeff P ((p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r) n = coeff P (p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)) n" 
13940  318 
by (simp add: Pi_def) 
319 
qed (simp_all add: R) 

320 

321 
ML_setup {* 

14590  322 
simpset_ref() := simpset() setsubgoaler asm_simp_tac; 
323 
*} 

13940  324 

325 
lemma (in UP_cring) UP_l_one [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

327 
shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p" 
13940  328 
proof (rule up_eqI) 
329 
fix n 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

330 
show "coeff P (\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p) n = coeff P p n" 
13940  331 
proof (cases n) 
332 
case 0 with R show ?thesis by simp 

333 
next 

334 
case Suc with R show ?thesis 

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

336 
qed 

337 
qed (simp_all add: R) 

338 

339 
lemma (in UP_cring) UP_l_distr: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

341 
shows "(p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = (p \<otimes>\<^bsub>P\<^esub> r) \<oplus>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)" 
13940  342 
by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R) 
343 

344 
lemma (in UP_cring) UP_m_comm: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

346 
shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p" 
13940  347 
proof (rule up_eqI) 
14666  348 
fix n 
13940  349 
{ 
350 
fix k and a b :: "nat=>'a" 

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

14666  352 
then have "k <= n ==> 
353 
(\<Oplus>i \<in> {..k}. a i \<otimes> b (ni)) = 

354 
(\<Oplus>i \<in> {..k}. a (ki) \<otimes> b (i+nk))" 

355 
(concl is "?eq k") 

13940  356 
proof (induct k) 
357 
case 0 then show ?case by (simp add: Pi_def) 

358 
next 

359 
case (Suc k) then show ?case 

15944  360 
by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+ 
13940  361 
qed 
362 
} 

363 
note l = this 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

364 
from R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = coeff P (q \<otimes>\<^bsub>P\<^esub> p) n" 
13940  365 
apply (simp add: Pi_def) 
366 
apply (subst l) 

367 
apply (auto simp add: Pi_def) 

368 
apply (simp add: m_comm) 

369 
done 

370 
qed (simp_all add: R) 

371 

15596  372 
(* 
373 
Strange phenomenon in Isar: 

374 

375 
theorem (in UP_cring) UP_cring: 

376 
"cring P" 

377 
proof (rule cringI) 

378 
show "abelian_group P" proof (rule abelian_groupI) 

379 
fix x y z 

380 
assume "x \<in> carrier P" and "y \<in> carrier P" and "z \<in> carrier P" 

381 
{ 

382 
show "x \<oplus>\<^bsub>P\<^esub> y \<in> carrier P" sorry 

383 
next 

384 
show "x \<oplus>\<^bsub>P\<^esub> y \<oplus>\<^bsub>P\<^esub> z = x \<oplus>\<^bsub>P\<^esub> (y \<oplus>\<^bsub>P\<^esub> z)" sorry 

385 
next 

386 
show "x \<oplus>\<^bsub>P\<^esub> y = y \<oplus>\<^bsub>P\<^esub> x" sorry 

387 
next 

388 
show "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> x = x" sorry 

389 
next 

390 
show "\<exists>y\<in>carrier P. y \<oplus>\<^bsub>P\<^esub> x = \<zero>\<^bsub>P\<^esub>" sorry 

391 
next 

392 
show "\<zero>\<^bsub>P\<^esub> \<in> carrier P" sorry last goal rejected!!! 

393 
*) 

394 

13940  395 
theorem (in UP_cring) UP_cring: 
396 
"cring P" 

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

398 
UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr) 

399 

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

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

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

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

403 

13940  404 
lemma (in UP_cring) UP_a_inv_closed [intro, simp]: 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

405 
"p \<in> carrier P ==> \<ominus>\<^bsub>P\<^esub> p \<in> carrier P" 
13940  406 
by (rule abelian_group.a_inv_closed 
14399
dc677b35e54f
New lemmas about inversion of restricted functions.
ballarin
parents:
13975
diff
changeset

407 
[OF ring.is_abelian_group [OF UP_ring]]) 
13940  408 

409 
lemma (in UP_cring) coeff_a_inv [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

411 
shows "coeff P (\<ominus>\<^bsub>P\<^esub> p) n = \<ominus> (coeff P p n)" 
13940  412 
proof  
413 
from R coeff_closed UP_a_inv_closed have 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

414 
"coeff P (\<ominus>\<^bsub>P\<^esub> p) n = \<ominus> coeff P p n \<oplus> (coeff P p n \<oplus> coeff P (\<ominus>\<^bsub>P\<^esub> p) n)" 
13940  415 
by algebra 
416 
also from R have "... = \<ominus> (coeff P p n)" 

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

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

418 
abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]]) 
13940  419 
finally show ?thesis . 
420 
qed 

421 

422 
text {* 

423 
Instantiation of lemmas from @{term cring}. 

424 
*} 

425 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

426 
(* TODO: this should be automated with an instantiation command. *) 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

427 

13940  428 
lemma (in UP_cring) UP_monoid: 
429 
"monoid P" 

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

431 
UP_cring) 

432 
(* TODO: provide cring.is_monoid *) 

433 

434 
lemma (in UP_cring) UP_comm_monoid: 

435 
"comm_monoid P" 

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

437 

438 
lemma (in UP_cring) UP_abelian_monoid: 

439 
"abelian_monoid P" 

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

440 
by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring) 
13940  441 

442 
lemma (in UP_cring) UP_abelian_group: 

443 
"abelian_group P" 

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

444 
by (fast intro!: ring.is_abelian_group UP_ring) 
13940  445 

446 
lemmas (in UP_cring) UP_r_one [simp] = 

447 
monoid.r_one [OF UP_monoid] 

448 

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

450 
monoid.nat_pow_closed [OF UP_monoid] 

451 

452 
lemmas (in UP_cring) UP_nat_pow_0 [simp] = 

453 
monoid.nat_pow_0 [OF UP_monoid] 

454 

455 
lemmas (in UP_cring) UP_nat_pow_Suc [simp] = 

456 
monoid.nat_pow_Suc [OF UP_monoid] 

457 

458 
lemmas (in UP_cring) UP_nat_pow_one [simp] = 

459 
monoid.nat_pow_one [OF UP_monoid] 

460 

461 
lemmas (in UP_cring) UP_nat_pow_mult = 

462 
monoid.nat_pow_mult [OF UP_monoid] 

463 

464 
lemmas (in UP_cring) UP_nat_pow_pow = 

465 
monoid.nat_pow_pow [OF UP_monoid] 

466 

467 
lemmas (in UP_cring) UP_m_lcomm = 

14963  468 
comm_monoid.m_lcomm [OF UP_comm_monoid] 
13940  469 

470 
lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm 

471 

472 
lemmas (in UP_cring) UP_nat_pow_distr = 

473 
comm_monoid.nat_pow_distr [OF UP_comm_monoid] 

474 

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

476 

477 
lemmas (in UP_cring) UP_r_zero [simp] = 

478 
abelian_monoid.r_zero [OF UP_abelian_monoid] 

479 

480 
lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm 

481 

482 
lemmas (in UP_cring) UP_finsum_empty [simp] = 

483 
abelian_monoid.finsum_empty [OF UP_abelian_monoid] 

484 

485 
lemmas (in UP_cring) UP_finsum_insert [simp] = 

486 
abelian_monoid.finsum_insert [OF UP_abelian_monoid] 

487 

488 
lemmas (in UP_cring) UP_finsum_zero [simp] = 

489 
abelian_monoid.finsum_zero [OF UP_abelian_monoid] 

490 

491 
lemmas (in UP_cring) UP_finsum_closed [simp] = 

492 
abelian_monoid.finsum_closed [OF UP_abelian_monoid] 

493 

494 
lemmas (in UP_cring) UP_finsum_Un_Int = 

495 
abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid] 

496 

497 
lemmas (in UP_cring) UP_finsum_Un_disjoint = 

498 
abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid] 

499 

500 
lemmas (in UP_cring) UP_finsum_addf = 

501 
abelian_monoid.finsum_addf [OF UP_abelian_monoid] 

502 

503 
lemmas (in UP_cring) UP_finsum_cong' = 

504 
abelian_monoid.finsum_cong' [OF UP_abelian_monoid] 

505 

506 
lemmas (in UP_cring) UP_finsum_0 [simp] = 

507 
abelian_monoid.finsum_0 [OF UP_abelian_monoid] 

508 

509 
lemmas (in UP_cring) UP_finsum_Suc [simp] = 

510 
abelian_monoid.finsum_Suc [OF UP_abelian_monoid] 

511 

512 
lemmas (in UP_cring) UP_finsum_Suc2 = 

513 
abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid] 

514 

515 
lemmas (in UP_cring) UP_finsum_add [simp] = 

516 
abelian_monoid.finsum_add [OF UP_abelian_monoid] 

517 

518 
lemmas (in UP_cring) UP_finsum_cong = 

519 
abelian_monoid.finsum_cong [OF UP_abelian_monoid] 

520 

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

522 
abelian_group.minus_closed [OF UP_abelian_group] 

523 

524 
lemmas (in UP_cring) UP_a_l_cancel [simp] = 

525 
abelian_group.a_l_cancel [OF UP_abelian_group] 

526 

527 
lemmas (in UP_cring) UP_a_r_cancel [simp] = 

528 
abelian_group.a_r_cancel [OF UP_abelian_group] 

529 

530 
lemmas (in UP_cring) UP_l_neg = 

531 
abelian_group.l_neg [OF UP_abelian_group] 

532 

533 
lemmas (in UP_cring) UP_r_neg = 

534 
abelian_group.r_neg [OF UP_abelian_group] 

535 

536 
lemmas (in UP_cring) UP_minus_zero [simp] = 

537 
abelian_group.minus_zero [OF UP_abelian_group] 

538 

539 
lemmas (in UP_cring) UP_minus_minus [simp] = 

540 
abelian_group.minus_minus [OF UP_abelian_group] 

541 

542 
lemmas (in UP_cring) UP_minus_add = 

543 
abelian_group.minus_add [OF UP_abelian_group] 

544 

545 
lemmas (in UP_cring) UP_r_neg2 = 

546 
abelian_group.r_neg2 [OF UP_abelian_group] 

547 

548 
lemmas (in UP_cring) UP_r_neg1 = 

549 
abelian_group.r_neg1 [OF UP_abelian_group] 

550 

551 
lemmas (in UP_cring) UP_r_distr = 

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

552 
ring.r_distr [OF UP_ring] 
13940  553 

554 
lemmas (in UP_cring) UP_l_null [simp] = 

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

555 
ring.l_null [OF UP_ring] 
13940  556 

557 
lemmas (in UP_cring) UP_r_null [simp] = 

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

558 
ring.r_null [OF UP_ring] 
13940  559 

560 
lemmas (in UP_cring) UP_l_minus = 

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

561 
ring.l_minus [OF UP_ring] 
13940  562 

563 
lemmas (in UP_cring) UP_r_minus = 

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

564 
ring.r_minus [OF UP_ring] 
13940  565 

566 
lemmas (in UP_cring) UP_finsum_ldistr = 

567 
cring.finsum_ldistr [OF UP_cring] 

568 

569 
lemmas (in UP_cring) UP_finsum_rdistr = 

570 
cring.finsum_rdistr [OF UP_cring] 

571 

14666  572 

13940  573 
subsection {* Polynomials form an Algebra *} 
574 

575 
lemma (in UP_cring) UP_smult_l_distr: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

577 
(a \<oplus> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> b \<odot>\<^bsub>P\<^esub> p" 
13940  578 
by (rule up_eqI) (simp_all add: R.l_distr) 
579 

580 
lemma (in UP_cring) UP_smult_r_distr: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

582 
a \<odot>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> a \<odot>\<^bsub>P\<^esub> q" 
13940  583 
by (rule up_eqI) (simp_all add: R.r_distr) 
584 

585 
lemma (in UP_cring) UP_smult_assoc1: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

587 
(a \<otimes> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> p)" 
13940  588 
by (rule up_eqI) (simp_all add: R.m_assoc) 
589 

590 
lemma (in UP_cring) UP_smult_one [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

591 
"p \<in> carrier P ==> \<one> \<odot>\<^bsub>P\<^esub> p = p" 
13940  592 
by (rule up_eqI) simp_all 
593 

594 
lemma (in UP_cring) UP_smult_assoc2: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

596 
(a \<odot>\<^bsub>P\<^esub> p) \<otimes>\<^bsub>P\<^esub> q = a \<odot>\<^bsub>P\<^esub> (p \<otimes>\<^bsub>P\<^esub> q)" 
13940  597 
by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def) 
598 

599 
text {* 

600 
Instantiation of lemmas from @{term algebra}. 

601 
*} 

602 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

603 
(* TODO: this should be automated with an instantiation command. *) 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

604 

13940  605 
(* TODO: move to CRing.thy, really a fact missing from the locales package *) 
606 
lemma (in cring) cring: 

607 
"cring R" 

608 
by (fast intro: cring.intro prems) 

609 

610 
lemma (in UP_cring) UP_algebra: 

611 
"algebra R P" 

612 
by (auto intro: algebraI cring UP_cring UP_smult_l_distr UP_smult_r_distr 

613 
UP_smult_assoc1 UP_smult_assoc2) 

614 

615 
lemmas (in UP_cring) UP_smult_l_null [simp] = 

616 
algebra.smult_l_null [OF UP_algebra] 

617 

618 
lemmas (in UP_cring) UP_smult_r_null [simp] = 

619 
algebra.smult_r_null [OF UP_algebra] 

620 

621 
lemmas (in UP_cring) UP_smult_l_minus = 

622 
algebra.smult_l_minus [OF UP_algebra] 

623 

624 
lemmas (in UP_cring) UP_smult_r_minus = 

625 
algebra.smult_r_minus [OF UP_algebra] 

626 

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

627 
subsection {* Further lemmas involving monomials *} 
13940  628 

629 
lemma (in UP_cring) monom_zero [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

630 
"monom P \<zero> n = \<zero>\<^bsub>P\<^esub>" 
13940  631 
by (simp add: UP_def P_def) 
632 

633 
ML_setup {* 

14590  634 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
635 
*} 

13940  636 

637 
lemma (in UP_cring) monom_mult_is_smult: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

639 
shows "monom P a 0 \<otimes>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p" 
13940  640 
proof (rule up_eqI) 
641 
fix n 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

642 
have "coeff P (p \<otimes>\<^bsub>P\<^esub> monom P a 0) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n" 
13940  643 
proof (cases n) 
644 
case 0 with R show ?thesis by (simp add: R.m_comm) 

645 
next 

646 
case Suc with R show ?thesis 

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

648 
(simp add: m_comm) 

649 
qed 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

650 
with R show "coeff P (monom P a 0 \<otimes>\<^bsub>P\<^esub> p) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n" 
13940  651 
by (simp add: UP_m_comm) 
652 
qed (simp_all add: R) 

653 

654 
ML_setup {* 

14590  655 
simpset_ref() := simpset() setsubgoaler asm_simp_tac; 
656 
*} 

13940  657 

658 
lemma (in UP_cring) monom_add [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

660 
monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n" 
13940  661 
by (rule up_eqI) simp_all 
662 

663 
ML_setup {* 

14590  664 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
665 
*} 

13940  666 

667 
lemma (in UP_cring) monom_one_Suc: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

668 
"monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1" 
13940  669 
proof (rule up_eqI) 
670 
fix k 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

671 
show "coeff P (monom P \<one> (Suc n)) k = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k" 
13940  672 
proof (cases "k = Suc n") 
673 
case True show ?thesis 

674 
proof  

14666  675 
from True have less_add_diff: 
676 
"!!i. [ n < i; i <= n + m ] ==> n + m  i < m" by arith 

13940  677 
from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp 
678 
also from True 

15045  679 
have "... = (\<Oplus>i \<in> {..<n} \<union> {n}. coeff P (monom P \<one> n) i \<otimes> 
14666  680 
coeff P (monom P \<one> 1) (k  i))" 
681 
by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def) 

682 
also have "... = (\<Oplus>i \<in> {..n}. coeff P (monom P \<one> n) i \<otimes> 

683 
coeff P (monom P \<one> 1) (k  i))" 

684 
by (simp only: ivl_disj_un_singleton) 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

685 
also from True 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

686 
have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. coeff P (monom P \<one> n) i \<otimes> 
14666  687 
coeff P (monom P \<one> 1) (k  i))" 
688 
by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one 

689 
order_less_imp_not_eq Pi_def) 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

690 
also from True have "... = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k" 
14666  691 
by (simp add: ivl_disj_un_one) 
13940  692 
finally show ?thesis . 
693 
qed 

694 
next 

695 
case False 

696 
note neq = False 

697 
let ?s = 

14666  698 
"\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k  i then \<one> else \<zero>)" 
13940  699 
from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp 
14666  700 
also have "... = (\<Oplus>i \<in> {..k}. ?s i)" 
13940  701 
proof  
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

702 
have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>" 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

703 
by (simp cong: finsum_cong add: Pi_def) 
14666  704 
from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>" 
705 
by (simp cong: finsum_cong add: Pi_def) arith 

15045  706 
have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>" 
14666  707 
by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def) 
13940  708 
show ?thesis 
709 
proof (cases "k < n") 

14666  710 
case True then show ?thesis by (simp cong: finsum_cong add: Pi_def) 
13940  711 
next 
14666  712 
case False then have n_le_k: "n <= k" by arith 
713 
show ?thesis 

714 
proof (cases "n = k") 

715 
case True 

15045  716 
then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)" 
14666  717 
by (simp cong: finsum_cong add: finsum_Un_disjoint 
718 
ivl_disj_int_singleton Pi_def) 

719 
also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)" 

720 
by (simp only: ivl_disj_un_singleton) 

721 
finally show ?thesis . 

722 
next 

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

15045  724 
with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)" 
14666  725 
by (simp add: finsum_Un_disjoint f1 f2 
726 
ivl_disj_int_singleton Pi_def del: Un_insert_right) 

727 
also have "... = (\<Oplus>i \<in> {..n}. ?s i)" 

728 
by (simp only: ivl_disj_un_singleton) 

15045  729 
also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)" 
14666  730 
by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def) 
731 
also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)" 

732 
by (simp only: ivl_disj_un_one) 

733 
finally show ?thesis . 

734 
qed 

13940  735 
qed 
736 
qed 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

737 
also have "... = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k" by simp 
13940  738 
finally show ?thesis . 
739 
qed 

740 
qed (simp_all) 

741 

742 
ML_setup {* 

14590  743 
simpset_ref() := simpset() setsubgoaler asm_simp_tac; 
744 
*} 

13940  745 

746 
lemma (in UP_cring) monom_mult_smult: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

747 
"[ a \<in> carrier R; b \<in> carrier R ] ==> monom P (a \<otimes> b) n = a \<odot>\<^bsub>P\<^esub> monom P b n" 
13940  748 
by (rule up_eqI) simp_all 
749 

750 
lemma (in UP_cring) monom_one [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

751 
"monom P \<one> 0 = \<one>\<^bsub>P\<^esub>" 
13940  752 
by (rule up_eqI) simp_all 
753 

754 
lemma (in UP_cring) monom_one_mult: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

755 
"monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m" 
13940  756 
proof (induct n) 
757 
case 0 show ?case by simp 

758 
next 

759 
case Suc then show ?case 

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

761 
qed 

762 

763 
lemma (in UP_cring) monom_mult [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

765 
shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m" 
13940  766 
proof  
767 
from R have "monom P (a \<otimes> b) (n + m) = monom P (a \<otimes> b \<otimes> \<one>) (n + m)" by simp 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

768 
also from R have "... = a \<otimes> b \<odot>\<^bsub>P\<^esub> monom P \<one> (n + m)" 
13940  769 
by (simp add: monom_mult_smult del: r_one) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

770 
also have "... = a \<otimes> b \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m)" 
13940  771 
by (simp only: monom_one_mult) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

772 
also from R have "... = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m))" 
13940  773 
by (simp add: UP_smult_assoc1) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

774 
also from R have "... = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> (monom P \<one> m \<otimes>\<^bsub>P\<^esub> monom P \<one> n))" 
13940  775 
by (simp add: UP_m_comm) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

776 
also from R have "... = a \<odot>\<^bsub>P\<^esub> ((b \<odot>\<^bsub>P\<^esub> monom P \<one> m) \<otimes>\<^bsub>P\<^esub> monom P \<one> n)" 
13940  777 
by (simp add: UP_smult_assoc2) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

778 
also from R have "... = a \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> monom P \<one> m))" 
13940  779 
by (simp add: UP_m_comm) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

780 
also from R have "... = (a \<odot>\<^bsub>P\<^esub> monom P \<one> n) \<otimes>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> monom P \<one> m)" 
13940  781 
by (simp add: UP_smult_assoc2) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

782 
also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^bsub>P\<^esub> monom P (b \<otimes> \<one>) m" 
13940  783 
by (simp add: monom_mult_smult del: r_one) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

784 
also from R have "... = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m" by simp 
13940  785 
finally show ?thesis . 
786 
qed 

787 

788 
lemma (in UP_cring) monom_a_inv [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

789 
"a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n" 
13940  790 
by (rule up_eqI) simp_all 
791 

792 
lemma (in UP_cring) monom_inj: 

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

794 
proof (rule inj_onI) 

795 
fix x y 

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

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

798 
with R show "x = y" by simp 

799 
qed 

800 

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

801 
subsection {* The degree function *} 
13940  802 

14651  803 
constdefs (structure R) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

804 
deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat" 
14651  805 
"deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)" 
13940  806 

807 
lemma (in UP_cring) deg_aboveI: 

14666  808 
"[ (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P ] ==> deg R p <= n" 
13940  809 
by (unfold deg_def P_def) (fast intro: Least_le) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

810 

13940  811 
(* 
812 
lemma coeff_bound_ex: "EX n. bound n (coeff p)" 

813 
proof  

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

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

816 
then show ?thesis .. 

817 
qed 

14666  818 

13940  819 
lemma bound_coeff_obtain: 
820 
assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P" 

821 
proof  

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

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

824 
with prem show P . 

825 
qed 

826 
*) 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

827 

13940  828 
lemma (in UP_cring) deg_aboveD: 
829 
"[ deg R p < m; p \<in> carrier P ] ==> coeff P p m = \<zero>" 

830 
proof  

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

14666  832 
from R obtain n where "bound \<zero> n (coeff P p)" 
13940  833 
by (auto simp add: UP_def P_def) 
834 
then have "bound \<zero> (deg R p) (coeff P p)" 

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

14666  836 
then show ?thesis .. 
13940  837 
qed 
838 

839 
lemma (in UP_cring) deg_belowI: 

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

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

842 
shows "n <= deg R p" 

14666  843 
 {* Logically, this is a slightly stronger version of 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

844 
@{thm [source] deg_aboveD} *} 
13940  845 
proof (cases "n=0") 
846 
case True then show ?thesis by simp 

847 
next 

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

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

850 
then show ?thesis by arith 

851 
qed 

852 

853 
lemma (in UP_cring) lcoeff_nonzero_deg: 

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

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

856 
proof  

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

858 
proof  

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

860 
by arith 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

861 
(* TODO: why does simplification below not work with "1" *) 
13940  862 
from deg have "deg R p  1 < (LEAST n. bound \<zero> n (coeff P p))" 
863 
by (unfold deg_def P_def) arith 

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

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

866 
by (unfold bound_def) fast 

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

14666  868 
then show ?thesis by auto 
13940  869 
qed 
870 
with deg_belowI R have "deg R p = m" by fastsimp 

871 
with m_coeff show ?thesis by simp 

872 
qed 

873 

874 
lemma (in UP_cring) lcoeff_nonzero_nonzero: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

875 
assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P" 
13940  876 
shows "coeff P p 0 ~= \<zero>" 
877 
proof  

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

879 
proof (rule classical) 

880 
assume "~ ?thesis" 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

881 
with R have "p = \<zero>\<^bsub>P\<^esub>" by (auto intro: up_eqI) 
13940  882 
with nonzero show ?thesis by contradiction 
883 
qed 

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

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

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

887 
with coeff show ?thesis by simp 

888 
qed 

889 

890 
lemma (in UP_cring) lcoeff_nonzero: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

891 
assumes neq: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P" 
13940  892 
shows "coeff P p (deg R p) ~= \<zero>" 
893 
proof (cases "deg R p = 0") 

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

895 
next 

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

897 
qed 

898 

899 
lemma (in UP_cring) deg_eqI: 

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

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

902 
by (fast intro: le_anti_sym deg_aboveI deg_belowI) 

903 

904 
(* Degree and polynomial operations *) 

905 

906 
lemma (in UP_cring) deg_add [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

908 
shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)" 
13940  909 
proof (cases "deg R p <= deg R q") 
910 
case True show ?thesis 

14666  911 
by (rule deg_aboveI) (simp_all add: True R deg_aboveD) 
13940  912 
next 
913 
case False show ?thesis 

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

915 
qed 

916 

917 
lemma (in UP_cring) deg_monom_le: 

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

919 
by (intro deg_aboveI) simp_all 

920 

921 
lemma (in UP_cring) deg_monom [simp]: 

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

923 
by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) 

924 

925 
lemma (in UP_cring) deg_const [simp]: 

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

927 
proof (rule le_anti_sym) 

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

929 
next 

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

931 
qed 

932 

933 
lemma (in UP_cring) deg_zero [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

934 
"deg R \<zero>\<^bsub>P\<^esub> = 0" 
13940  935 
proof (rule le_anti_sym) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

936 
show "deg R \<zero>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all 
13940  937 
next 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

938 
show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all 
13940  939 
qed 
940 

941 
lemma (in UP_cring) deg_one [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

942 
"deg R \<one>\<^bsub>P\<^esub> = 0" 
13940  943 
proof (rule le_anti_sym) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

944 
show "deg R \<one>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all 
13940  945 
next 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

946 
show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all 
13940  947 
qed 
948 

949 
lemma (in UP_cring) deg_uminus [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

950 
assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^bsub>P\<^esub> p) = deg R p" 
13940  951 
proof (rule le_anti_sym) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

952 
show "deg R (\<ominus>\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R) 
13940  953 
next 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

954 
show "deg R p <= deg R (\<ominus>\<^bsub>P\<^esub> p)" 
13940  955 
by (simp add: deg_belowI lcoeff_nonzero_deg 
956 
inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R) 

957 
qed 

958 

959 
lemma (in UP_domain) deg_smult_ring: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

961 
deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)" 
13940  962 
by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+ 
963 

964 
lemma (in UP_domain) deg_smult [simp]: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

966 
shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)" 
13940  967 
proof (rule le_anti_sym) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

968 
show "deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)" 
13940  969 
by (rule deg_smult_ring) 
970 
next 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

971 
show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^bsub>P\<^esub> p)" 
13940  972 
proof (cases "a = \<zero>") 
973 
qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R) 

974 
qed 

975 

976 
lemma (in UP_cring) deg_mult_cring: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

978 
shows "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" 
13940  979 
proof (rule deg_aboveI) 
980 
fix m 

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

982 
{ 

983 
fix k i 

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

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

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

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

988 
next 

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

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

991 
qed 

992 
} 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

993 
with boundm R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) m = \<zero>" by simp 
13940  994 
qed (simp add: R) 
995 

996 
ML_setup {* 

14590  997 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
998 
*} 

13940  999 

1000 
lemma (in UP_domain) deg_mult [simp]: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1001 
"[ p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P ] ==> 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1002 
deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q" 
13940  1003 
proof (rule le_anti_sym) 
1004 
assume "p \<in> carrier P" " q \<in> carrier P" 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1005 
show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring) 
13940  1006 
next 
1007 
let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q  i))" 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1008 
assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^bsub>P\<^esub>" "q ~= \<zero>\<^bsub>P\<^esub>" 
13940  1009 
have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m  k" by arith 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1010 
show "deg R p + deg R q <= deg R (p \<otimes>\<^bsub>P\<^esub> q)" 
13940  1011 
proof (rule deg_belowI, simp add: R) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1012 
have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1013 
= (\<Oplus>i \<in> {..< deg R p} \<union> {deg R p .. deg R p + deg R q}. ?s i)" 
13940  1014 
by (simp only: ivl_disj_un_one) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1015 
also have "... = (\<Oplus>i \<in> {deg R p .. deg R p + deg R q}. ?s i)" 
13940  1016 
by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one 
1017 
deg_aboveD less_add_diff R Pi_def) 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1018 
also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)" 
13940  1019 
by (simp only: ivl_disj_un_singleton) 
14666  1020 
also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" 
13940  1021 
by (simp cong: finsum_cong add: finsum_Un_disjoint 
14666  1022 
ivl_disj_int_singleton deg_aboveD R Pi_def) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1023 
finally have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) 
13940  1024 
= coeff P p (deg R p) \<otimes> coeff P q (deg R q)" . 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1025 
with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>" 
13940  1026 
by (simp add: integral_iff lcoeff_nonzero R) 
1027 
qed (simp add: R) 

1028 
qed 

1029 

1030 
lemma (in UP_cring) coeff_finsum: 

1031 
assumes fin: "finite A" 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1033 
coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)" 
13940  1034 
using fin by induct (auto simp: Pi_def) 
1035 

1036 
ML_setup {* 

14590  1037 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
1038 
*} 

13940  1039 

1040 
lemma (in UP_cring) up_repr: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1042 
shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p" 
13940  1043 
proof (rule up_eqI) 
1044 
let ?s = "(%i. monom P (coeff P p i) i)" 

1045 
fix k 

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

1047 
by simp 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1048 
show "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k = coeff P p k" 
13940  1049 
proof (cases "k <= deg R p") 
1050 
case True 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1051 
hence "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k = 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1052 
coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..k} \<union> {k<..deg R p}. ?s i) k" 
13940  1053 
by (simp only: ivl_disj_un_one) 
1054 
also from True 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1055 
have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..k}. ?s i) k" 
13940  1056 
by (simp cong: finsum_cong add: finsum_Un_disjoint 
14666  1057 
ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def) 
13940  1058 
also 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1059 
have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<k} \<union> {k}. ?s i) k" 
13940  1060 
by (simp only: ivl_disj_un_singleton) 
1061 
also have "... = coeff P p k" 

1062 
by (simp cong: finsum_cong add: setsum_Un_disjoint 

14666  1063 
ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def) 
13940  1064 
finally show ?thesis . 
1065 
next 

1066 
case False 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1067 
hence "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k = 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1068 
coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<deg R p} \<union> {deg R p}. ?s i) k" 
13940  1069 
by (simp only: ivl_disj_un_singleton) 
1070 
also from False have "... = coeff P p k" 

1071 
by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton 

1072 
coeff_finsum deg_aboveD R Pi_def) 

1073 
finally show ?thesis . 

1074 
qed 

1075 
qed (simp_all add: R Pi_def) 

1076 

1077 
lemma (in UP_cring) up_repr_le: 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1079 
(\<Oplus>\<^bsub>P\<^esub> i \<in> {..n}. monom P (coeff P p i) i) = p" 
13940  1080 
proof  
1081 
let ?s = "(%i. monom P (coeff P p i) i)" 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1083 
then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} \<union> {deg R p<..n})" 
13940  1084 
by (simp only: ivl_disj_un_one) 
1085 
also have "... = finsum P ?s {..deg R p}" 

1086 
by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one 

1087 
deg_aboveD R Pi_def) 

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

1089 
finally show ?thesis . 

1090 
qed 

1091 

1092 
ML_setup {* 

14590  1093 
simpset_ref() := simpset() setsubgoaler asm_simp_tac; 
1094 
*} 

13940  1095 

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

1096 
subsection {* Polynomials over an integral domain form an integral domain *} 
13940  1097 

1098 
lemma domainI: 

1099 
assumes cring: "cring R" 

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

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

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

1103 
shows "domain R" 

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

1105 
del: disjCI) 

1106 

1107 
lemma (in UP_domain) UP_one_not_zero: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1108 
"\<one>\<^bsub>P\<^esub> ~= \<zero>\<^bsub>P\<^esub>" 
13940  1109 
proof 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1110 
assume "\<one>\<^bsub>P\<^esub> = \<zero>\<^bsub>P\<^esub>" 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1111 
hence "coeff P \<one>\<^bsub>P\<^esub> 0 = (coeff P \<zero>\<^bsub>P\<^esub> 0)" by simp 
13940  1112 
hence "\<one> = \<zero>" by simp 
1113 
with one_not_zero show "False" by contradiction 

1114 
qed 

1115 

1116 
lemma (in UP_domain) UP_integral: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1117 
"[ p \<otimes>\<^bsub>P\<^esub> q = \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P ] ==> p = \<zero>\<^bsub>P\<^esub>  q = \<zero>\<^bsub>P\<^esub>" 
13940  1118 
proof  
1119 
fix p q 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1120 
assume pq: "p \<otimes>\<^bsub>P\<^esub> q = \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P" "q \<in> carrier P" 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1121 
show "p = \<zero>\<^bsub>P\<^esub>  q = \<zero>\<^bsub>P\<^esub>" 
13940  1122 
proof (rule classical) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1123 
assume c: "~ (p = \<zero>\<^bsub>P\<^esub>  q = \<zero>\<^bsub>P\<^esub>)" 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1124 
with R have "deg R p + deg R q = deg R (p \<otimes>\<^bsub>P\<^esub> q)" by simp 
13940  1125 
also from pq have "... = 0" by simp 
1126 
finally have "deg R p + deg R q = 0" . 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1128 
from f1 R have "p = (\<Oplus>\<^bsub>P\<^esub> i \<in> {..0}. monom P (coeff P p i) i)" 
13940  1129 
by (simp only: up_repr_le) 
1130 
also from R have "... = monom P (coeff P p 0) 0" by simp 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1132 
from f1 R have "q = (\<Oplus>\<^bsub>P\<^esub> i \<in> {..0}. monom P (coeff P q i) i)" 
13940  1133 
by (simp only: up_repr_le) 
1134 
also from R have "... = monom P (coeff P q 0) 0" by simp 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1136 
from R have "coeff P p 0 \<otimes> coeff P q 0 = coeff P (p \<otimes>\<^bsub>P\<^esub> q) 0" by simp 
13940  1137 
also from pq have "... = \<zero>" by simp 
1138 
finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" . 

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

1140 
by (simp add: R.integral_iff) 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1141 
with p q show "p = \<zero>\<^bsub>P\<^esub>  q = \<zero>\<^bsub>P\<^esub>" by fastsimp 
13940  1142 
qed 
1143 
qed 

1144 

1145 
theorem (in UP_domain) UP_domain: 

1146 
"domain P" 

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

1148 

1149 
text {* 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1150 
Instantiation of theorems from @{term domain}. 
13940  1151 
*} 
1152 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1153 
(* TODO: this should be automated with an instantiation command. *) 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1154 

13940  1155 
lemmas (in UP_domain) UP_zero_not_one [simp] = 
1156 
domain.zero_not_one [OF UP_domain] 

1157 

1158 
lemmas (in UP_domain) UP_integral_iff = 

1159 
domain.integral_iff [OF UP_domain] 

1160 

1161 
lemmas (in UP_domain) UP_m_lcancel = 

1162 
domain.m_lcancel [OF UP_domain] 

1163 

1164 
lemmas (in UP_domain) UP_m_rcancel = 

1165 
domain.m_rcancel [OF UP_domain] 

1166 

1167 
lemma (in UP_domain) smult_integral: 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1168 
"[ a \<odot>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>; a \<in> carrier R; p \<in> carrier P ] ==> a = \<zero>  p = \<zero>\<^bsub>P\<^esub>" 
13940  1169 
by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff 
1170 
inj_on_iff [OF monom_inj, of _ "\<zero>", simplified]) 

1171 

14666  1172 

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

1173 
subsection {* Evaluation Homomorphism and Universal Property*} 
13940  1174 

14666  1175 
(* alternative congruence rule (possibly more efficient) 
1176 
lemma (in abelian_monoid) finsum_cong2: 

1177 
"[ !!i. i \<in> A ==> f i \<in> carrier G = True; A = B; 

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

1179 
sorry*) 

1180 

13940  1181 
ML_setup {* 
14590  1182 
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac; 
1183 
*} 

13940  1184 

1185 
theorem (in cring) diagonal_sum: 

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

14666  1187 
(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k  i)) = 
1188 
(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m  k}. f k \<otimes> g i)" 

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

1191 
{ 

1192 
fix j 

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

14666  1194 
(\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k  i)) = 
1195 
(\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..j  k}. f k \<otimes> g i)" 

13940  1196 
proof (induct j) 
1197 
case 0 from Rf Rg show ?case by (simp add: Pi_def) 

1198 
next 

14666  1199 
case (Suc j) 
13940  1200 
have R6: "!!i k. [ k <= j; i <= Suc j  k ] ==> g i \<in> carrier R" 
14666  1201 
using Suc by (auto intro!: funcset_mem [OF Rg]) arith 
13940  1202 
have R8: "!!i k. [ k <= Suc j; i <= k ] ==> g (k  i) \<in> carrier R" 
14666  1203 
using Suc by (auto intro!: funcset_mem [OF Rg]) arith 
13940  1204 
have R9: "!!i k. [ k <= Suc j ] ==> f k \<in> carrier R" 
14666  1205 
using Suc by (auto intro!: funcset_mem [OF Rf]) 
13940  1206 
have R10: "!!i k. [ k <= Suc j; i <= Suc j  k ] ==> g i \<in> carrier R" 
14666  1207 
using Suc by (auto intro!: funcset_mem [OF Rg]) arith 
13940  1208 
have R11: "g 0 \<in> carrier R" 
14666  1209 
using Suc by (auto intro!: funcset_mem [OF Rg]) 
13940  1210 
from Suc show ?case 
14666  1211 
by (simp cong: finsum_cong add: Suc_diff_le a_ac 
1212 
Pi_def R6 R8 R9 R10 R11) 

13940  1213 
qed 
1214 
} 

1215 
then show ?thesis by fast 

1216 
qed 

1217 

1218 
lemma (in abelian_monoid) boundD_carrier: 

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

1220 
by auto 

1221 

1222 
theorem (in cring) cauchy_product: 

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

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

14666  1225 
shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k  i)) = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1226 
(\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)" (* State revese direction? *) 
13940  1227 
proof  
1228 
have f: "!!x. f x \<in> carrier R" 

1229 
proof  

1230 
fix x 

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

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

1233 
qed 

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

1235 
proof  

1236 
fix x 

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

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

1239 
qed 

14666  1240 
from f g have "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k  i)) = 
1241 
(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m  k}. f k \<otimes> g i)" 

13940  1242 
by (simp add: diagonal_sum Pi_def) 
15045  1243 
also have "... = (\<Oplus>k \<in> {..n} \<union> {n<..n + m}. \<Oplus>i \<in> {..n + m  k}. f k \<otimes> g i)" 
13940  1244 
by (simp only: ivl_disj_un_one) 
14666  1245 
also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m  k}. f k \<otimes> g i)" 
13940  1246 
by (simp cong: finsum_cong 
14666  1247 
add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1248 
also from f g 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1249 
have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {m<..n + m  k}. f k \<otimes> g i)" 
13940  1250 
by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def) 
14666  1251 
also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)" 
13940  1252 
by (simp cong: finsum_cong 
14666  1253 
add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def) 
1254 
also from f g have "... = (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)" 

13940  1255 
by (simp add: finsum_ldistr diagonal_sum Pi_def, 
1256 
simp cong: finsum_cong add: finsum_rdistr Pi_def) 

1257 
finally show ?thesis . 

1258 
qed 

1259 

1260 
lemma (in UP_cring) const_ring_hom: 

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

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

1263 

14651  1264 
constdefs (structure S) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1265 
eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme, 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1266 
'a => 'b, 'b, nat => 'a] => 'b" 
14651  1267 
"eval R S phi s == \<lambda>p \<in> carrier (UP R). 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1268 
\<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> s (^) i" 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1269 

63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1270 
locale UP_univ_prop = ring_hom_cring R S + UP_cring R 
14666  1271 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1272 
lemma (in UP) eval_on_carrier: 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1273 
includes struct S 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1274 
shows "p \<in> carrier P ==> 
13940  1275 
eval R S phi s p = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1276 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1277 
by (unfold eval_def, fold P_def) simp 
1278 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1279 
lemma (in UP) eval_extensional: 
13940  1280 
"eval R S phi s \<in> extensional (carrier P)" 
1281 
by (unfold eval_def, fold P_def) simp 

1282 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1283 
theorem (in UP_univ_prop) eval_ring_hom: 
13940  1284 
"s \<in> carrier S ==> eval R S h s \<in> ring_hom P S" 
1285 
proof (rule ring_hom_memI) 

1286 
fix p 

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

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

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

1290 
next 

1291 
fix p q 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1293 
then show "eval R S h s (p \<otimes>\<^bsub>P\<^esub> q) = eval R S h s p \<otimes>\<^bsub>S\<^esub> eval R S h s q" 
13940  1294 
proof (simp only: eval_on_carrier UP_mult_closed) 
1295 
from RS have 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1296 
"(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1297 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<otimes>\<^bsub>P\<^esub> q)<..deg R p + deg R q}. 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1298 
h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1299 
by (simp cong: finsum_cong 
14666  1300 
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def 
1301 
del: coeff_mult) 

13940  1302 
also from RS have "... = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1303 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1304 
by (simp only: ivl_disj_un_one deg_mult_cring) 
1305 
also from RS have "... = 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1306 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1307 
\<Oplus>\<^bsub>S\<^esub> k \<in> {..i}. 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1308 
h (coeff P p k) \<otimes>\<^bsub>S\<^esub> h (coeff P q (i  k)) \<otimes>\<^bsub>S\<^esub> 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1309 
(s (^)\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> (i  k)))" 
13940  1310 
by (simp cong: finsum_cong add: nat_pow_mult Pi_def 
14666  1311 
S.m_ac S.finsum_rdistr) 
13940  1312 
also from RS have "... = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1313 
(\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub> 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1314 
(\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
14666  1315 
by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac 
1316 
Pi_def) 

13940  1317 
finally show 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1318 
"(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1319 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub> 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1320 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" . 
13940  1321 
qed 
1322 
next 

1323 
fix p q 

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

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1325 
then show "eval R S h s (p \<oplus>\<^bsub>P\<^esub> q) = eval R S h s p \<oplus>\<^bsub>S\<^esub> eval R S h s q" 
13940  1326 
proof (simp only: eval_on_carrier UP_a_closed) 
1327 
from RS have 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1328 
"(\<Oplus>\<^bsub>S \<^esub>i\<in>{..deg R (p \<oplus>\<^bsub>P\<^esub> q)}. h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1329 
(\<Oplus>\<^bsub>S \<^esub>i\<in>{..deg R (p \<oplus>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<oplus>\<^bsub>P\<^esub> q)<..max (deg R p) (deg R q)}. 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1330 
h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1331 
by (simp cong: finsum_cong 
14666  1332 
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def 
1333 
del: coeff_add) 

13940  1334 
also from RS have "... = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1335 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..max (deg R p) (deg R q)}. 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1336 
h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1337 
by (simp add: ivl_disj_un_one) 
1338 
also from RS have "... = 

15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1339 
(\<Oplus>\<^bsub>S\<^esub>i\<in>{..max (deg R p) (deg R q)}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub> 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1340 
(\<Oplus>\<^bsub>S\<^esub>i\<in>{..max (deg R p) (deg R q)}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1341 
by (simp cong: finsum_cong 
14666 