author  wenzelm 
Sun, 08 Mar 2009 17:19:15 +0100  
changeset 30363  9b8d9b6ef803 
parent 29246  3593802c9cf1 
child 30729  461ee3e49ad3 
permissions  rwrr 
13940  1 
(* 
14706  2 
Title: HOL/Algebra/UnivPoly.thy 
13940  3 
Author: Clemens Ballarin, started 9 December 1996 
4 
Copyright: Clemens Ballarin 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

5 

27933  6 
Contributions, in particular on long division, by Jesus Aransay. 
13940  7 
*) 
8 

28823  9 
theory UnivPoly 
10 
imports Module RingHom 

11 
begin 

13940  12 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

13 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

14 
section {* Univariate Polynomials *} 
13940  15 

14553  16 
text {* 
14666  17 
Polynomials are formalised as modules with additional operations for 
18 
extracting coefficients from polynomials and for obtaining monomials 

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

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

21 
coefficient domain. Bounded means that these functions return zero 

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

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

25 
ported to Locales. 

14553  26 
*} 
27 

14666  28 

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

29 
subsection {* The Constructor for Univariate Polynomials *} 
13940  30 

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

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

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

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

34 

14666  35 
locale bound = 
36 
fixes z :: 'a 

37 
and n :: nat 

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

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

13940  40 

14666  41 
declare bound.intro [intro!] 
42 
and bound.bound [dest] 

13940  43 

44 
lemma bound_below: 

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

48 
then have "m < n" by arith 

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

50 
with nonzero show ?thesis by contradiction 

51 
qed 

52 

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

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

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

56 

27933  57 
definition up :: "('a, 'm) ring_scheme => (nat => 'a) set" 
58 
where up_def: "up R == {f. f \<in> UNIV > carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}" 

59 

60 
definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring" 

61 
where UP_def: "UP R == ( 

62 
carrier = up R, 

63 
mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (ni)), 

64 
one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>), 

65 
zero = (%i. \<zero>\<^bsub>R\<^esub>), 

66 
add = (%p:up R. %q:up R. %i. p i \<oplus>\<^bsub>R\<^esub> q i), 

67 
smult = (%a:carrier R. %p:up R. %i. a \<otimes>\<^bsub>R\<^esub> p i), 

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

69 
coeff = (%p:up R. %n. p n) )" 

13940  70 

71 
text {* 

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

73 
*} 

74 

75 
lemma mem_upI [intro]: 

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

77 
by (simp add: up_def Pi_def) 

78 

79 
lemma mem_upD [dest]: 

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

81 
by (simp add: up_def Pi_def) 

82 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

83 
context ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

84 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

85 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

86 
lemma bound_upD [dest]: "f \<in> up R ==> EX n. bound \<zero> n f" by (simp add: up_def) 
13940  87 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

88 
lemma up_one_closed: "(%n. if n = 0 then \<one> else \<zero>) \<in> up R" using up_def by force 
13940  89 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

90 
lemma up_smult_closed: "[ a \<in> carrier R; p \<in> up R ] ==> (%i. a \<otimes> p i) \<in> up R" by force 
13940  91 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

92 
lemma up_add_closed: 
13940  93 
"[ p \<in> up R; q \<in> up R ] ==> (%i. p i \<oplus> q i) \<in> up R" 
94 
proof 

95 
fix n 

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

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

98 
by auto 

99 
next 

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

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

102 
proof  

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

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

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

106 
proof 

107 
fix i 

108 
assume "max n m < i" 

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

110 
qed 

111 
then show ?thesis .. 

112 
qed 

113 
qed 

114 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

115 
lemma up_a_inv_closed: 
13940  116 
"p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R" 
117 
proof 

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

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

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

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

122 
qed auto 

123 

27933  124 
lemma up_minus_closed: 
125 
"[ p \<in> up R; q \<in> up R ] ==> (%i. p i \<ominus> q i) \<in> up R" 

126 
using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed a_minus_def [of _ R] 

127 
by auto 

128 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

129 
lemma up_mult_closed: 
13940  130 
"[ p \<in> up R; q \<in> up R ] ==> 
14666  131 
(%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (ni)) \<in> up R" 
13940  132 
proof 
133 
fix n 

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

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

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

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

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

14666  143 
have "bound \<zero> (n + m) (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n  i))" 
13940  144 
proof 
14666  145 
fix k assume bound: "n + m < k" 
13940  146 
{ 
14666  147 
fix i 
148 
have "p i \<otimes> q (ki) = \<zero>" 

149 
proof (cases "n < i") 

150 
case True 

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

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

155 
case False 

156 
with bound have "m < ki" by arith 

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

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

159 
ultimately show ?thesis by simp 

160 
qed 

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

13940  164 
qed 
165 
then show ?thesis by fast 

166 
qed 

167 
qed 

168 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

169 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

170 

14666  171 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

172 
subsection {* Effect of Operations on Coefficients *} 
13940  173 

19783  174 
locale UP = 
175 
fixes R (structure) and P (structure) 

13940  176 
defines P_def: "P == UP R" 
177 

29240  178 
locale UP_ring = UP + R: ring R 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

179 

29240  180 
locale UP_cring = UP + R: cring R 
13940  181 

29237  182 
sublocale UP_cring < UP_ring 
29240  183 
by intro_locales [1] (rule P_def) 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

184 

29240  185 
locale UP_domain = UP + R: "domain" R 
13940  186 

29237  187 
sublocale UP_domain < UP_cring 
29240  188 
by intro_locales [1] (rule P_def) 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

189 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

190 
context UP 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

191 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

192 

30363
9b8d9b6ef803
proper local context for text with antiquotations;
wenzelm
parents:
29246
diff
changeset

193 
text {*Temporarily declare @{thm P_def} as simp rule.*} 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

194 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

195 
declare P_def [simp] 
13940  196 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

197 
lemma up_eqI: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

198 
assumes prem: "!!n. coeff P p n = coeff P q n" and R: "p \<in> carrier P" "q \<in> carrier P" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

199 
shows "p = q" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

200 
proof 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

201 
fix x 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

202 
from prem and R show "p x = q x" by (simp add: UP_def) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

203 
qed 
13940  204 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

205 
lemma coeff_closed [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

206 
"p \<in> carrier P ==> coeff P p n \<in> carrier R" by (auto simp add: UP_def) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

207 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

208 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

209 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

210 
context UP_ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

211 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

212 

27933  213 
(* Theorems generalised from commutative rings to rings by Jesus Aransay. *) 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

214 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

215 
lemma coeff_monom [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

216 
"a \<in> carrier R ==> coeff P (monom P a m) n = (if m=n then a else \<zero>)" 
13940  217 
proof  
218 
assume R: "a \<in> carrier R" 

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

220 
using up_def by force 

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

222 
qed 

223 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

224 
lemma coeff_zero [simp]: "coeff P \<zero>\<^bsub>P\<^esub> n = \<zero>" by (auto simp add: UP_def) 
13940  225 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

226 
lemma coeff_one [simp]: "coeff P \<one>\<^bsub>P\<^esub> n = (if n=0 then \<one> else \<zero>)" 
13940  227 
using up_one_closed by (simp add: UP_def) 
228 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

229 
lemma coeff_smult [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

230 
"[ a \<in> carrier R; p \<in> carrier P ] ==> coeff P (a \<odot>\<^bsub>P\<^esub> p) n = a \<otimes> coeff P p n" 
13940  231 
by (simp add: UP_def up_smult_closed) 
232 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

233 
lemma coeff_add [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

234 
"[ p \<in> carrier P; q \<in> carrier P ] ==> coeff P (p \<oplus>\<^bsub>P\<^esub> q) n = coeff P p n \<oplus> coeff P q n" 
13940  235 
by (simp add: UP_def up_add_closed) 
236 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

237 
lemma coeff_mult [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

238 
"[ p \<in> carrier P; q \<in> carrier P ] ==> coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (ni))" 
13940  239 
by (simp add: UP_def up_mult_closed) 
240 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

241 
end 
14666  242 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

243 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

244 
subsection {* Polynomials Form a Ring. *} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

245 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

246 
context UP_ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

247 
begin 
13940  248 

14666  249 
text {* Operations are closed over @{term P}. *} 
13940  250 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

251 
lemma UP_mult_closed [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

254 
lemma UP_one_closed [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

257 
lemma UP_zero_closed [intro, simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

260 
lemma UP_a_closed [intro, simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

263 
lemma monom_closed [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

264 
"a \<in> carrier R ==> monom P a n \<in> carrier P" by (auto simp add: UP_def up_def Pi_def) 
13940  265 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

266 
lemma UP_smult_closed [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

267 
"[ a \<in> carrier R; p \<in> carrier P ] ==> a \<odot>\<^bsub>P\<^esub> p \<in> carrier P" by (simp add: UP_def up_smult_closed) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

268 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

269 
end 
13940  270 

271 
declare (in UP) P_def [simp del] 

272 

273 
text {* Algebraic ring properties *} 

274 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

275 
context UP_ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

276 
begin 
13940  277 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

278 
lemma UP_a_assoc: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

279 
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

280 
shows "(p \<oplus>\<^bsub>P\<^esub> q) \<oplus>\<^bsub>P\<^esub> r = p \<oplus>\<^bsub>P\<^esub> (q \<oplus>\<^bsub>P\<^esub> r)" by (rule up_eqI, simp add: a_assoc R, simp_all add: R) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

281 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

282 
lemma UP_l_zero [simp]: 
13940  283 
assumes R: "p \<in> carrier P" 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

286 
lemma UP_l_neg_ex: 
13940  287 
assumes R: "p \<in> carrier P" 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

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

292 
by (simp add: UP_def P_def up_a_inv_closed) 

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

294 
by (simp add: UP_def P_def up_a_inv_closed) 

295 
show ?thesis 

296 
proof 

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

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

300 
qed 

301 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

302 
lemma UP_a_comm: 
13940  303 
assumes R: "p \<in> carrier P" "q \<in> carrier P" 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

304 
shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p" by (rule up_eqI, simp add: a_comm R, simp_all add: R) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

305 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

306 
lemma UP_m_assoc: 
13940  307 
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

308 
shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)" 
13940  309 
proof (rule up_eqI) 
310 
fix n 

311 
{ 

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

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

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

315 
then have "k <= n ==> 

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

19582  318 
(is "_ \<Longrightarrow> ?eq k") 
13940  319 
proof (induct k) 
320 
case 0 then show ?case by (simp add: Pi_def m_assoc) 

321 
next 

322 
case (Suc k) 

323 
then have "k <= n" by arith 

23350  324 
from this R have "?eq k" by (rule Suc) 
13940  325 
with R show ?case 
14666  326 
by (simp cong: finsum_cong 
13940  327 
add: Suc_diff_le Pi_def l_distr r_distr m_assoc) 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

328 
(simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc) 
13940  329 
qed 
330 
} 

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

331 
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  332 
by (simp add: Pi_def) 
333 
qed (simp_all add: R) 

334 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

335 
lemma UP_r_one [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

336 
assumes R: "p \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub> = p" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

337 
proof (rule up_eqI) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

338 
fix n 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

339 
show "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) n = coeff P p n" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

340 
proof (cases n) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

341 
case 0 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

342 
{ 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

343 
with R show ?thesis by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

344 
} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

345 
next 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

346 
case Suc 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

347 
{ 
27933  348 
(*JE: in the locale UP_cring the proof was solved only with "by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)", but I did not get it to work here*) 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

349 
fix nn assume Succ: "n = Suc nn" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

350 
have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = coeff P p (Suc nn)" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

351 
proof  
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

352 
have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = (\<Oplus>i\<in>{..Suc nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" using R by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

353 
also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>) \<oplus> (\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

354 
using finsum_Suc [of "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "nn"] unfolding Pi_def using R by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

355 
also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>)" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

356 
proof  
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

357 
have "(\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>)) = (\<Oplus>i\<in>{..nn}. \<zero>)" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

358 
using finsum_cong [of "{..nn}" "{..nn}" "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "(\<lambda>i::nat. \<zero>)"] using R 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

359 
unfolding Pi_def by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

360 
also have "\<dots> = \<zero>" by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

361 
finally show ?thesis using r_zero R by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

362 
qed 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

363 
also have "\<dots> = coeff P p (Suc nn)" using R by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

364 
finally show ?thesis by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

365 
qed 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

366 
then show ?thesis using Succ by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

367 
} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

368 
qed 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

369 
qed (simp_all add: R) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

370 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

371 
lemma UP_l_one [simp]: 
13940  372 
assumes R: "p \<in> carrier P" 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

373 
shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p" 
13940  374 
proof (rule up_eqI) 
375 
fix n 

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

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

379 
next 

380 
case Suc with R show ?thesis 

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

382 
qed 

383 
qed (simp_all add: R) 

384 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

385 
lemma UP_l_distr: 
13940  386 
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

387 
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  388 
by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R) 
389 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

390 
lemma UP_r_distr: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

391 
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

392 
shows "r \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = (r \<otimes>\<^bsub>P\<^esub> p) \<oplus>\<^bsub>P\<^esub> (r \<otimes>\<^bsub>P\<^esub> q)" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

393 
by (rule up_eqI) (simp add: r_distr R Pi_def, simp_all add: R) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

394 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

395 
theorem UP_ring: "ring P" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

396 
by (auto intro!: ringI abelian_groupI monoidI UP_a_assoc) 
27933  397 
(auto intro: UP_a_comm UP_l_neg_ex UP_m_assoc UP_l_distr UP_r_distr) 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

398 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

399 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

400 

27933  401 

402 
subsection {* Polynomials Form a Commutative Ring. *} 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

403 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

404 
context UP_cring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

405 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

406 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

407 
lemma UP_m_comm: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

408 
assumes R1: "p \<in> carrier P" and R2: "q \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p" 
13940  409 
proof (rule up_eqI) 
14666  410 
fix n 
13940  411 
{ 
412 
fix k and a b :: "nat=>'a" 

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

14666  414 
then have "k <= n ==> 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

415 
(\<Oplus>i \<in> {..k}. a i \<otimes> b (ni)) = (\<Oplus>i \<in> {..k}. a (ki) \<otimes> b (i+nk))" 
19582  416 
(is "_ \<Longrightarrow> ?eq k") 
13940  417 
proof (induct k) 
418 
case 0 then show ?case by (simp add: Pi_def) 

419 
next 

420 
case (Suc k) then show ?case 

15944  421 
by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+ 
13940  422 
qed 
423 
} 

424 
note l = this 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

425 
from R1 R2 show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = coeff P (q \<otimes>\<^bsub>P\<^esub> p) n" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

426 
unfolding coeff_mult [OF R1 R2, of n] 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

427 
unfolding coeff_mult [OF R2 R1, of n] 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

428 
using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

429 
qed (simp_all add: R1 R2) 
13940  430 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

431 
subsection{*Polynomials over a commutative ring for a commutative ring*} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

432 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

433 
theorem UP_cring: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

434 
"cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm) 
13940  435 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

436 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

437 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

438 
context UP_ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

440 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

442 
"p \<in> carrier P ==> \<ominus>\<^bsub>P\<^esub> p \<in> carrier P" 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

443 
by (rule abelian_group.a_inv_closed [OF ring.is_abelian_group [OF UP_ring]]) 
13940  444 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

445 
lemma coeff_a_inv [simp]: 
13940  446 
assumes R: "p \<in> carrier P" 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

447 
shows "coeff P (\<ominus>\<^bsub>P\<^esub> p) n = \<ominus> (coeff P p n)" 
13940  448 
proof  
449 
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

450 
"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  451 
by algebra 
452 
also from R have "... = \<ominus> (coeff P p n)" 

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

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

454 
abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]]) 
13940  455 
finally show ?thesis . 
456 
qed 

457 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

458 
end 
13940  459 

29240  460 
sublocale UP_ring < P: ring P using UP_ring . 
461 
sublocale UP_cring < P: cring P using UP_cring . 

13940  462 

14666  463 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

464 
subsection {* Polynomials Form an Algebra *} 
13940  465 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

466 
context UP_ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

467 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

468 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

469 
lemma UP_smult_l_distr: 
13940  470 
"[ 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

471 
(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  472 
by (rule up_eqI) (simp_all add: R.l_distr) 
473 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

474 
lemma UP_smult_r_distr: 
13940  475 
"[ 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

476 
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  477 
by (rule up_eqI) (simp_all add: R.r_distr) 
478 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

479 
lemma UP_smult_assoc1: 
13940  480 
"[ 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

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

484 
lemma UP_smult_zero [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

485 
"p \<in> carrier P ==> \<zero> \<odot>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

486 
by (rule up_eqI) simp_all 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

487 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

488 
lemma UP_smult_one [simp]: 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

489 
"p \<in> carrier P ==> \<one> \<odot>\<^bsub>P\<^esub> p = p" 
13940  490 
by (rule up_eqI) simp_all 
491 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

492 
lemma UP_smult_assoc2: 
13940  493 
"[ 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

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

497 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

498 

13940  499 
text {* 
17094  500 
Interpretation of lemmas from @{term algebra}. 
13940  501 
*} 
502 

503 
lemma (in cring) cring: 

28823  504 
"cring R" .. 
13940  505 

506 
lemma (in UP_cring) UP_algebra: 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

507 
"algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr 
13940  508 
UP_smult_assoc1 UP_smult_assoc2) 
509 

29237  510 
sublocale UP_cring < algebra R P using UP_algebra . 
13940  511 

512 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

513 
subsection {* Further Lemmas Involving Monomials *} 
13940  514 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

515 
context UP_ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

516 
begin 
13940  517 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

518 
lemma monom_zero [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

519 
"monom P \<zero> n = \<zero>\<^bsub>P\<^esub>" by (simp add: UP_def P_def) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

520 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

521 
lemma monom_mult_is_smult: 
13940  522 
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

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

526 
show "coeff P (monom P a 0 \<otimes>\<^bsub>P\<^esub> p) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n" 
13940  527 
proof (cases n) 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

528 
case 0 with R show ?thesis by simp 
13940  529 
next 
530 
case Suc with R show ?thesis 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

531 
using R.finsum_Suc2 by (simp del: R.finsum_Suc add: R.r_null Pi_def) 
13940  532 
qed 
533 
qed (simp_all add: R) 

534 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

535 
lemma monom_one [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

536 
"monom P \<one> 0 = \<one>\<^bsub>P\<^esub>" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

537 
by (rule up_eqI) simp_all 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

538 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

539 
lemma monom_add [simp]: 
13940  540 
"[ 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

541 
monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n" 
13940  542 
by (rule up_eqI) simp_all 
543 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

545 
"monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1" 
13940  546 
proof (rule up_eqI) 
547 
fix k 

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

548 
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  549 
proof (cases "k = Suc n") 
550 
case True show ?thesis 

551 
proof  

26934  552 
fix m 
14666  553 
from True have less_add_diff: 
554 
"!!i. [ n < i; i <= n + m ] ==> n + m  i < m" by arith 

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

15045  557 
have "... = (\<Oplus>i \<in> {..<n} \<union> {n}. coeff P (monom P \<one> n) i \<otimes> 
14666  558 
coeff P (monom P \<one> 1) (k  i))" 
17094  559 
by (simp cong: R.finsum_cong add: Pi_def) 
14666  560 
also have "... = (\<Oplus>i \<in> {..n}. coeff P (monom P \<one> n) i \<otimes> 
561 
coeff P (monom P \<one> 1) (k  i))" 

562 
by (simp only: ivl_disj_un_singleton) 

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

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

564 
have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. coeff P (monom P \<one> n) i \<otimes> 
14666  565 
coeff P (monom P \<one> 1) (k  i))" 
17094  566 
by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one 
14666  567 
order_less_imp_not_eq Pi_def) 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

572 
next 

573 
case False 

574 
note neq = False 

575 
let ?s = 

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

580 
have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>" 
17094  581 
by (simp cong: R.finsum_cong add: Pi_def) 
14666  582 
from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>" 
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20318
diff
changeset

583 
by (simp cong: R.finsum_cong add: Pi_def) arith 
15045  584 
have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>" 
17094  585 
by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def) 
13940  586 
show ?thesis 
587 
proof (cases "k < n") 

17094  588 
case True then show ?thesis by (simp cong: R.finsum_cong add: Pi_def) 
13940  589 
next 
14666  590 
case False then have n_le_k: "n <= k" by arith 
591 
show ?thesis 

592 
proof (cases "n = k") 

593 
case True 

15045  594 
then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)" 
17094  595 
by (simp cong: R.finsum_cong add: ivl_disj_int_singleton Pi_def) 
14666  596 
also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)" 
597 
by (simp only: ivl_disj_un_singleton) 

598 
finally show ?thesis . 

599 
next 

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

15045  601 
with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)" 
17094  602 
by (simp add: R.finsum_Un_disjoint f1 f2 
14666  603 
ivl_disj_int_singleton Pi_def del: Un_insert_right) 
604 
also have "... = (\<Oplus>i \<in> {..n}. ?s i)" 

605 
by (simp only: ivl_disj_un_singleton) 

15045  606 
also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)" 
17094  607 
by (simp add: R.finsum_Un_disjoint f3 ivl_disj_int_one Pi_def) 
14666  608 
also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)" 
609 
by (simp only: ivl_disj_un_one) 

610 
finally show ?thesis . 

611 
qed 

13940  612 
qed 
613 
qed 

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

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

617 
qed (simp_all) 

618 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

619 
lemma monom_one_Suc2: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

620 
"monom P \<one> (Suc n) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> n" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

621 
proof (induct n) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

622 
case 0 show ?case by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

623 
next 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

624 
case Suc 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

625 
{ 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

626 
fix k:: nat 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

627 
assume hypo: "monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

628 
then show "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k)" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

629 
proof  
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

630 
have lhs: "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

631 
unfolding monom_one_Suc [of "Suc k"] unfolding hypo .. 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

632 
note cl = monom_closed [OF R.one_closed, of 1] 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

633 
note clk = monom_closed [OF R.one_closed, of k] 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

634 
have rhs: "monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

635 
unfolding monom_one_Suc [of k] unfolding sym [OF m_assoc [OF cl clk cl]] .. 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

636 
from lhs rhs show ?thesis by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

637 
qed 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

638 
} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

639 
qed 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

640 

30363
9b8d9b6ef803
proper local context for text with antiquotations;
wenzelm
parents:
29246
diff
changeset

641 
text{*The following corollary follows from lemmas @{thm "monom_one_Suc"} 
9b8d9b6ef803
proper local context for text with antiquotations;
wenzelm
parents:
29246
diff
changeset

642 
and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*} 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

643 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

644 
corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

645 
unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] .. 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

646 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

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

655 
next 

656 
case Suc then show ?case 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

657 
unfolding add_Suc unfolding monom_one_Suc unfolding Suc.hyps 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

658 
using m_assoc monom_one_comm [of m] by simp 
13940  659 
qed 
660 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

661 
lemma monom_one_mult_comm: "monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m = monom P \<one> m \<otimes>\<^bsub>P\<^esub> monom P \<one> n" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

662 
unfolding monom_one_mult [symmetric] by (rule up_eqI) simp_all 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

663 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

664 
lemma monom_mult [simp]: 
27933  665 
assumes a_in_R: "a \<in> carrier R" and b_in_R: "b \<in> carrier R" 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

666 
shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m" 
27933  667 
proof (rule up_eqI) 
668 
fix k 

669 
show "coeff P (monom P (a \<otimes> b) (n + m)) k = coeff P (monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m) k" 

670 
proof (cases "n + m = k") 

671 
case True 

672 
{ 

673 
show ?thesis 

674 
unfolding True [symmetric] 

675 
coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of "n + m"] 

676 
coeff_monom [OF a_in_R, of n] coeff_monom [OF b_in_R, of m] 

677 
using R.finsum_cong [of "{.. n + m}" "{.. n + m}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = n + m  i then b else \<zero>))" 

678 
"(\<lambda>i. if n = i then a \<otimes> b else \<zero>)"] 

679 
a_in_R b_in_R 

680 
unfolding simp_implies_def 

681 
using R.finsum_singleton [of n "{.. n + m}" "(\<lambda>i. a \<otimes> b)"] 

682 
unfolding Pi_def by auto 

683 
} 

684 
next 

685 
case False 

686 
{ 

687 
show ?thesis 

688 
unfolding coeff_monom [OF R.m_closed [OF a_in_R b_in_R], of "n + m" k] apply (simp add: False) 

689 
unfolding coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of k] 

690 
unfolding coeff_monom [OF a_in_R, of n] unfolding coeff_monom [OF b_in_R, of m] using False 

691 
using R.finsum_cong [of "{..k}" "{..k}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = k  i then b else \<zero>))" "(\<lambda>i. \<zero>)"] 

692 
unfolding Pi_def simp_implies_def using a_in_R b_in_R by force 

693 
} 

694 
qed 

695 
qed (simp_all add: a_in_R b_in_R) 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

696 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

697 
lemma monom_a_inv [simp]: 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

698 
"a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n" 
13940  699 
by (rule up_eqI) simp_all 
700 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

701 
lemma monom_inj: 
13940  702 
"inj_on (%a. monom P a n) (carrier R)" 
703 
proof (rule inj_onI) 

704 
fix x y 

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

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

707 
with R show "x = y" by simp 

708 
qed 

709 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

710 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

711 

17094  712 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

713 
subsection {* The Degree Function *} 
13940  714 

27933  715 
definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat" 
716 
where "deg R p == LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p)" 

13940  717 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

718 
context UP_ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

719 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

720 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

721 
lemma deg_aboveI: 
14666  722 
"[ (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P ] ==> deg R p <= n" 
13940  723 
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

724 

13940  725 
(* 
726 
lemma coeff_bound_ex: "EX n. bound n (coeff p)" 

727 
proof  

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

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

730 
then show ?thesis .. 

731 
qed 

14666  732 

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

735 
proof  

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

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

738 
with prem show P . 

739 
qed 

740 
*) 

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

741 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

742 
lemma deg_aboveD: 
23350  743 
assumes "deg R p < m" and "p \<in> carrier P" 
744 
shows "coeff P p m = \<zero>" 

13940  745 
proof  
23350  746 
from `p \<in> carrier P` obtain n where "bound \<zero> n (coeff P p)" 
13940  747 
by (auto simp add: UP_def P_def) 
748 
then have "bound \<zero> (deg R p) (coeff P p)" 

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

23350  750 
from this and `deg R p < m` show ?thesis .. 
13940  751 
qed 
752 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

753 
lemma deg_belowI: 
13940  754 
assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>" 
755 
and R: "p \<in> carrier P" 

756 
shows "n <= deg R p" 

14666  757 
 {* 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

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

761 
next 

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

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

764 
then show ?thesis by arith 

765 
qed 

766 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

767 
lemma lcoeff_nonzero_deg: 
13940  768 
assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P" 
769 
shows "coeff P p (deg R p) ~= \<zero>" 

770 
proof  

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

772 
proof  

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

774 
by arith 

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

776 
by (unfold deg_def P_def) simp 
13940  777 
then have "~ bound \<zero> (deg R p  1) (coeff P p)" by (rule not_less_Least) 
778 
then have "EX m. deg R p  1 < m & coeff P p m ~= \<zero>" 

779 
by (unfold bound_def) fast 

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

23350  781 
then show ?thesis by (auto intro: that) 
13940  782 
qed 
783 
with deg_belowI R have "deg R p = m" by fastsimp 

784 
with m_coeff show ?thesis by simp 

785 
qed 

786 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

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

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

792 
proof (rule classical) 

793 
assume "~ ?thesis" 

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

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

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

23350  798 
from this and R have "m <= deg R p" by (rule deg_belowI) 
13940  799 
then have "m = 0" by (simp add: deg) 
800 
with coeff show ?thesis by simp 

801 
qed 

802 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

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

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

808 
next 

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

810 
qed 

811 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

812 
lemma deg_eqI: 
13940  813 
"[ !!m. n < m ==> coeff P p m = \<zero>; 
814 
!!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P ] ==> deg R p = n" 

815 
by (fast intro: le_anti_sym deg_aboveI deg_belowI) 

816 

17094  817 
text {* Degree and polynomial operations *} 
13940  818 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

819 
lemma deg_add [simp]: 
13940  820 
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

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

14666  824 
by (rule deg_aboveI) (simp_all add: True R deg_aboveD) 
13940  825 
next 
826 
case False show ?thesis 

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

828 
qed 

829 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

830 
lemma deg_monom_le: 
13940  831 
"a \<in> carrier R ==> deg R (monom P a n) <= n" 
832 
by (intro deg_aboveI) simp_all 

833 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

834 
lemma deg_monom [simp]: 
13940  835 
"[ a ~= \<zero>; a \<in> carrier R ] ==> deg R (monom P a n) = n" 
836 
by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) 

837 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

838 
lemma deg_const [simp]: 
13940  839 
assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0" 
840 
proof (rule le_anti_sym) 

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

842 
next 

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

844 
qed 

845 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

846 
lemma deg_zero [simp]: 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

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

851 
show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all 
13940  852 
qed 
853 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

854 
lemma deg_one [simp]: 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

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

859 
show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all 
13940  860 
qed 
861 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

862 
lemma deg_uminus [simp]: 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

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

867 
show "deg R p <= deg R (\<ominus>\<^bsub>P\<^esub> p)" 
13940  868 
by (simp add: deg_belowI lcoeff_nonzero_deg 
17094  869 
inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R) 
13940  870 
qed 
871 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

872 
text{*The following lemma is later \emph{overwritten} by the most 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

873 
specific one for domains, @{text deg_smult}.*} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

874 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

875 
lemma deg_smult_ring [simp]: 
13940  876 
"[ 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

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

880 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

881 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

882 
context UP_domain 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

883 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

884 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

885 
lemma deg_smult [simp]: 
13940  886 
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

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

889 
show "deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)" 
23350  890 
using R by (rule deg_smult_ring) 
13940  891 
next 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

895 
qed 

896 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

897 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

898 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

899 
context UP_ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

900 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

901 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

902 
lemma deg_mult_ring: 
13940  903 
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

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

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

908 
{ 

909 
fix k i 

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

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

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

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

914 
next 

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

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

917 
qed 

918 
} 

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

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

922 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

923 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

924 
context UP_domain 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

925 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

926 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

927 
lemma deg_mult [simp]: 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

928 
"[ 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

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

932 
then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring) 
13940  933 
next 
934 
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

935 
assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^bsub>P\<^esub>" "q ~= \<zero>\<^bsub>P\<^esub>" 
13940  936 
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

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

939 
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

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

942 
also have "... = (\<Oplus>i \<in> {deg R p .. deg R p + deg R q}. ?s i)" 
17094  943 
by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one 
13940  944 
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

945 
also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)" 
13940  946 
by (simp only: ivl_disj_un_singleton) 
14666  947 
also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" 
17094  948 
by (simp cong: R.finsum_cong 
949 
add: 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

950 
finally have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) 
13940  951 
= 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

952 
with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>" 
13940  953 
by (simp add: integral_iff lcoeff_nonzero R) 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

954 
qed (simp add: R) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

955 
qed 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

956 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

957 
end 
13940  958 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

959 
text{*The following lemmas also can be lifted to @{term UP_ring}.*} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

960 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

961 
context UP_ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

962 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

963 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

964 
lemma coeff_finsum: 
13940  965 
assumes fin: "finite A" 
966 
shows "p \<in> A > carrier P ==> 

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

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

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

970 
lemma up_repr: 
13940  971 
assumes R: "p \<in> carrier P" 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

975 
fix k 

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

977 
by simp 

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

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

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

981 
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

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

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

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

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

17094  992 
by (simp cong: R.finsum_cong 
993 
add: ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def) 

13940  994 
finally show ?thesis . 
995 
next 

996 
case False 

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

997 
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

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

17094  1001 
by (simp cong: R.finsum_cong 
1002 
add: ivl_disj_int_singleton coeff_finsum deg_aboveD R Pi_def) 

13940  1003 
finally show ?thesis . 
1004 
qed 

1005 
qed (simp_all add: R Pi_def) 

1006 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1007 
lemma up_repr_le: 
13940  1008 
"[ 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

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

1012 
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

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

17094  1016 
by (simp cong: P.finsum_cong add: P.finsum_Un_disjoint ivl_disj_int_one 
13940  1017 
deg_aboveD R Pi_def) 
23350  1018 
also have "... = p" using R by (rule up_repr) 
13940  1019 
finally show ?thesis . 
1020 
qed 

1021 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1022 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1023 

17094  1024 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

1025 
subsection {* Polynomials over Integral Domains *} 
13940  1026 

1027 
lemma domainI: 

1028 
assumes cring: "cring R" 

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

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

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

1032 
shows "domain R" 

27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27611
diff
changeset

1033 
by (auto intro!: domain.intro domain_axioms.intro cring.axioms assms 
13940  1034 
del: disjCI) 
1035 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1036 
context UP_domain 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1037 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1038 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

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

1042 
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

1043 
hence "coeff P \<one>\<^bsub>P\<^esub> 0 = (coeff P \<zero>\<^bsub>P\<^esub> 0)" by simp 
13940  1044 
hence "\<one> = \<zero>" by simp 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1045 
with R.one_not_zero show "False" by contradiction 
13940  1046 
qed 
1047 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

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

1049 
"[ 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  1050 
proof  
1051 
fix p q 

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

1052 
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

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

1055 
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

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

1059 
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

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

1063 
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

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

1067 
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

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

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

1072 
by (simp add: R.integral_iff) 

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

1073 
with p q show "p = \<zero>\<^bsub>P\<^esub>  q = \<zero>\<^bsub>P\<^esub>" by fastsimp 
13940  1074 
qed 
1075 
qed 

1076 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1077 
theorem UP_domain: 
13940  1078 
"domain P" 
1079 
by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI) 

1080 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1081 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1082 

13940  1083 
text {* 
17094  1084 
Interpretation of theorems from @{term domain}. 
13940  1085 
*} 
1086 

29237  1087 
sublocale UP_domain < "domain" P 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

1088 
by intro_locales (rule domain.axioms UP_domain)+ 
13940  1089 

14666  1090 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

1091 
subsection {* The Evaluation Homomorphism and Universal Property*} 
13940  1092 

14666  1093 
(* alternative congruence rule (possibly more efficient) 
1094 
lemma (in abelian_monoid) finsum_cong2: 

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

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

1097 
sorry*) 

1098 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1099 
lemma (in abelian_monoid) boundD_carrier: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1100 
"[ bound \<zero> n f; n < m ] ==> f m \<in> carrier G" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1101 
by auto 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1102 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1103 
context ring 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1104 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1105 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1106 
theorem diagonal_sum: 
13940  1107 
"[ f \<in> {..n + m::nat} > carrier R; g \<in> {..n + m} > carrier R ] ==> 
14666  1108 
(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k  i)) = 
1109 
(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m  k}. f k \<otimes> g i)" 

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

1112 
{ 

1113 
fix j 

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

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

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

1119 
next 

14666  1120 
case (Suc j) 
13940  1121 
have R6: "!!i k. [ k <= j; i <= Suc j  k ] ==> g i \<in> carrier R" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19984
diff
changeset

1122 
using Suc by (auto intro!: funcset_mem [OF Rg]) 
13940  1123 
have R8: "!!i k. [ k <= Suc j; i <= k ] ==> g (k  i) \<in> carrier R" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19984
diff
changeset

1124 
using Suc by (auto intro!: funcset_mem [OF Rg]) 
13940  1125 
have R9: "!!i k. [ k <= Suc j ] ==> f k \<in> carrier R" 
14666  1126 
using Suc by (auto intro!: funcset_mem [OF Rf]) 
13940  1127 
have R10: "!!i k. [ k <= Suc j; i <= Suc j  k ] ==> g i \<in> carrier R" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19984
diff
changeset

1128 
using Suc by (auto intro!: funcset_mem [OF Rg]) 
13940  1129 
have R11: "g 0 \<in> carrier R" 
14666  1130 
using Suc by (auto intro!: funcset_mem [OF Rg]) 
13940  1131 
from Suc show ?case 
14666  1132 
by (simp cong: finsum_cong add: Suc_diff_le a_ac 
1133 
Pi_def R6 R8 R9 R10 R11) 

13940  1134 
qed 
1135 
} 

1136 
then show ?thesis by fast 

1137 
qed 

1138 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1139 
theorem cauchy_product: 
13940  1140 
assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g" 
1141 
and Rf: "f \<in> {..n} > carrier R" and Rg: "g \<in> {..m} > carrier R" 

14666  1142 
shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k  i)) = 
17094  1143 
(\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)" (* State reverse direction? *) 
13940  1144 
proof  
1145 
have f: "!!x. f x \<in> carrier R" 

1146 
proof  

1147 
fix x 

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

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

1150 
qed 

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

1152 
proof  

1153 
fix x 

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

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

1156 
qed 

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

13940  1159 
by (simp add: diagonal_sum Pi_def) 
15045  1160 
also have "... = (\<Oplus>k \<in> {..n} \<union> {n<..n + m}. \<Oplus>i \<in> {..n + m  k}. f k \<otimes> g i)" 
13940  1161 
by (simp only: ivl_disj_un_one) 
14666  1162 
also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m  k}. f k \<otimes> g i)" 
13940  1163 
by (simp cong: finsum_cong 
14666  1164 
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

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

1166 
have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {m<..n + m  k}. f k \<otimes> g i)" 
13940  1167 
by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def) 
14666  1168 
also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)" 
13940  1169 
by (simp cong: finsum_cong 
14666  1170 
add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def) 
1171 
also from f g have "... = (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)" 

13940  1172 
by (simp add: finsum_ldistr diagonal_sum Pi_def, 
1173 
simp cong: finsum_cong add: finsum_rdistr Pi_def) 

1174 
finally show ?thesis . 

1175 
qed 

1176 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1177 
end 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1178 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1179 
lemma (in UP_ring) const_ring_hom: 
13940  1180 
"(%a. monom P a 0) \<in> ring_hom R P" 
1181 
by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult) 

1182 

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

1184 
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

1185 
'a => 'b, 'b, nat => 'a] => 'b" 
27933  1186 
where "eval R S phi s == \<lambda>p \<in> carrier (UP R). 
1187 
\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i" 

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

1188 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1189 
context UP 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1190 
begin 
14666  1191 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1192 
lemma eval_on_carrier: 
19783  1193 
fixes S (structure) 
17094  1194 
shows "p \<in> carrier P ==> 
1195 
eval R S phi s p = (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 

13940  1196 
by (unfold eval_def, fold P_def) simp 
1197 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1198 
lemma eval_extensional: 
17094  1199 
"eval R S phi p \<in> extensional (carrier P)" 
13940  1200 
by (unfold eval_def, fold P_def) simp 
1201 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1202 
end 
17094  1203 

1204 
text {* The universal property of the polynomial ring *} 

1205 

29240  1206 
locale UP_pre_univ_prop = ring_hom_cring + UP_cring 
1207 

1208 
(* FIXME print_locale ring_hom_cring fails *) 

17094  1209 

19783  1210 
locale UP_univ_prop = UP_pre_univ_prop + 
1211 
fixes s and Eval 

17094  1212 
assumes indet_img_carrier [simp, intro]: "s \<in> carrier S" 
1213 
defines Eval_def: "Eval == eval R S h s" 

1214 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1215 
text{*JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.*} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1216 
text{*JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1217 
maybe it is not that necessary.*} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1218 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1219 
lemma (in ring_hom_ring) hom_finsum [simp]: 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1220 
"[ finite A; f \<in> A > carrier R ] ==> 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1221 
h (finsum R f A) = finsum S (h o f) A" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1222 
proof (induct set: finite) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1223 
case empty then show ?case by simp 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1224 
next 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1225 
case insert then show ?case by (simp add: Pi_def) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1226 
qed 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1227 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1228 
context UP_pre_univ_prop 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1229 
begin 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1230 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1231 
theorem eval_ring_hom: 
17094  1232 
assumes S: "s \<in> carrier S" 
1233 
shows "eval R S h s \<in> ring_hom P S" 

13940  1234 
proof (rule ring_hom_memI) 
1235 
fix p 

17094  1236 
assume R: "p \<in> carrier P" 
13940  1237 
then show "eval R S h s p \<in> carrier S" 
17094  1238 
by (simp only: eval_on_carrier) (simp add: S Pi_def) 
13940  1239 
next 
1240 
fix p q 

17094  1241 
assume 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

1242 
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" 
17094  1243 
proof (simp only: eval_on_carrier P.a_closed) 
1244 
from S R have 

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

1245 
"(\<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

1246 
(\<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

1247 
h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
17094  1248 
by (simp cong: S.finsum_cong 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1249 
add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def del: coeff_add) 
17094  1250 
also from R have "... = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1251 
(\<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

1252 
h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1253 
by (simp add: ivl_disj_un_one) 
17094  1254 
also from R S have "... = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1255 
(\<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

1256 
(\<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)" 
17094  1257 
by (simp cong: S.finsum_cong 
1258 
add: S.l_distr deg_aboveD ivl_disj_int_one Pi_def) 

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

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

1261 
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

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

1263 
h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1264 
by (simp only: ivl_disj_un_one le_maxI1 le_maxI2) 
17094  1265 
also from R S have "... = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1266 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. 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

1267 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
17094  1268 
by (simp cong: S.finsum_cong 
1269 
add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def) 

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

1271 
"(\<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

1272 
(\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. 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

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

17094  1276 
show "eval R S h s \<one>\<^bsub>P\<^esub> = \<one>\<^bsub>S\<^esub>" 
13940  1277 
by (simp only: eval_on_carrier UP_one_closed) simp 
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1278 
next 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1279 
fix p q 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1280 
assume R: "p \<in> carrier P" "q \<in> carrier P" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1281 
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" 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1282 
proof (simp only: eval_on_carrier UP_mult_closed) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1283 
from R S have 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1284 
"(\<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) = 