author  wenzelm 
Fri, 11 May 2007 00:43:45 +0200  
changeset 22931  11cc1ccad58e 
parent 21502  7f3ea2b3bab6 
child 23350  50c5b0912a0c 
permissions  rwrr 
13940  1 
(* 
14706  2 
Title: HOL/Algebra/UnivPoly.thy 
13940  3 
Id: $Id$ 
4 
Author: Clemens Ballarin, started 9 December 1996 

5 
Copyright: Clemens Ballarin 

6 
*) 

7 

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

8 
theory UnivPoly imports Module begin 
13940  9 

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

10 

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

11 
section {* Univariate Polynomials *} 
13940  12 

14553  13 
text {* 
14666  14 
Polynomials are formalised as modules with additional operations for 
15 
extracting coefficients from polynomials and for obtaining monomials 

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

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

18 
coefficient domain. Bounded means that these functions return zero 

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

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

22 
ported to Locales. 

14553  23 
*} 
24 

14666  25 

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

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

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

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

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

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

31 

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

34 
and n :: nat 

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

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

13940  37 

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

13940  40 

41 
lemma bound_below: 

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

45 
then have "m < n" by arith 

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

47 
with nonzero show ?thesis by contradiction 

48 
qed 

49 

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

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

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

53 

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

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

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

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

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

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

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

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

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

68 
text {* 

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

70 
*} 

71 

72 
lemma mem_upI [intro]: 

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

74 
by (simp add: up_def Pi_def) 

75 

76 
lemma mem_upD [dest]: 

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

78 
by (simp add: up_def Pi_def) 

79 

80 
lemma (in cring) bound_upD [dest]: 

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

82 
by (simp add: up_def) 

83 

84 
lemma (in cring) up_one_closed: 

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

86 
using up_def by force 

87 

88 
lemma (in cring) up_smult_closed: 

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

90 
by force 

91 

92 
lemma (in cring) up_add_closed: 

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 

115 
lemma (in cring) up_a_inv_closed: 

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 

124 
lemma (in cring) up_mult_closed: 

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

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

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

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

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

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

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

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

144 
proof (cases "n < i") 

145 
case True 

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

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

150 
case False 

151 
with bound have "m < ki" by arith 

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

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

154 
ultimately show ?thesis by simp 

155 
qed 

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

13940  159 
qed 
160 
then show ?thesis by fast 

161 
qed 

162 
qed 

163 

14666  164 

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

165 
subsection {* Effect of Operations on Coefficients *} 
13940  166 

19783  167 
locale UP = 
168 
fixes R (structure) and P (structure) 

13940  169 
defines P_def: "P == UP R" 
170 

171 
locale UP_cring = UP + cring R 

172 

173 
locale UP_domain = UP_cring + "domain" R 

174 

175 
text {* 

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

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

177 
*} 
13940  178 

179 
declare (in UP) P_def [simp] 

180 

181 
lemma (in UP_cring) coeff_monom [simp]: 

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

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

184 
proof  

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

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

187 
using up_def by force 

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

189 
qed 

190 

191 
lemma (in UP_cring) coeff_zero [simp]: 

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

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

195 
lemma (in UP_cring) coeff_one [simp]: 

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

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

199 
lemma (in UP_cring) coeff_smult [simp]: 

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

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

204 
lemma (in UP_cring) coeff_add [simp]: 

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

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

209 
lemma (in UP_cring) coeff_mult [simp]: 

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

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

214 
lemma (in UP) up_eqI: 

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

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

217 
shows "p = q" 

218 
proof 

219 
fix x 

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

221 
qed 

14666  222 

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

223 

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

224 
subsection {* Polynomials Form a Commutative Ring. *} 
13940  225 

14666  226 
text {* Operations are closed over @{term P}. *} 
13940  227 

228 
lemma (in UP_cring) UP_mult_closed [simp]: 

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

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

232 
lemma (in UP_cring) UP_one_closed [simp]: 

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

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

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

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

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

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

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

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

244 
lemma (in UP_cring) monom_closed [simp]: 

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

246 
by (auto simp add: UP_def up_def Pi_def) 

247 

248 
lemma (in UP_cring) UP_smult_closed [simp]: 

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

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

252 
lemma (in UP) coeff_closed [simp]: 

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

254 
by (auto simp add: UP_def) 

255 

256 
declare (in UP) P_def [simp del] 

257 

258 
text {* Algebraic ring properties *} 

259 

260 
lemma (in UP_cring) UP_a_assoc: 

261 
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

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

265 
lemma (in UP_cring) UP_l_zero [simp]: 

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

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

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

270 
lemma (in UP_cring) UP_l_neg_ex: 

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

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

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

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

276 
by (simp add: UP_def P_def up_a_inv_closed) 

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

278 
by (simp add: UP_def P_def up_a_inv_closed) 

279 
show ?thesis 

280 
proof 

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

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

284 
qed 

285 

286 
lemma (in UP_cring) UP_a_comm: 

287 
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

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

291 
lemma (in UP_cring) UP_m_assoc: 

292 
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

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

296 
{ 

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

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

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

300 
then have "k <= n ==> 

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

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

306 
next 

307 
case (Suc k) 

308 
then have "k <= n" by arith 

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

310 
with R show ?case 

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

314 
qed 

315 
} 

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

316 
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  317 
by (simp add: Pi_def) 
318 
qed (simp_all add: R) 

319 

320 
lemma (in UP_cring) UP_l_one [simp]: 

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

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

322 
shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p" 
13940  323 
proof (rule up_eqI) 
324 
fix n 

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

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

328 
next 

329 
case Suc with R show ?thesis 

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

331 
qed 

332 
qed (simp_all add: R) 

333 

334 
lemma (in UP_cring) UP_l_distr: 

335 
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

336 
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  337 
by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R) 
338 

339 
lemma (in UP_cring) UP_m_comm: 

340 
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

341 
shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p" 
13940  342 
proof (rule up_eqI) 
14666  343 
fix n 
13940  344 
{ 
345 
fix k and a b :: "nat=>'a" 

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

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

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

19582  350 
(is "_ \<Longrightarrow> ?eq k") 
13940  351 
proof (induct k) 
352 
case 0 then show ?case by (simp add: Pi_def) 

353 
next 

354 
case (Suc k) then show ?case 

15944  355 
by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+ 
13940  356 
qed 
357 
} 

358 
note l = this 

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

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

362 
apply (auto simp add: Pi_def) 

363 
apply (simp add: m_comm) 

364 
done 

365 
qed (simp_all add: R) 

366 

367 
theorem (in UP_cring) UP_cring: 

368 
"cring P" 

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

370 
UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr) 

371 

17094  372 
lemma (in UP_cring) UP_ring: 
373 
(* preliminary, 

374 
we want "UP_ring R P ==> ring P", not "UP_cring R P ==> ring P" *) 

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

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

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

377 

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

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

381 
[OF ring.is_abelian_group [OF UP_ring]]) 
13940  382 

383 
lemma (in UP_cring) coeff_a_inv [simp]: 

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

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

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

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

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

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

392 
abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]]) 
13940  393 
finally show ?thesis . 
394 
qed 

395 

396 
text {* 

17094  397 
Interpretation of lemmas from @{term cring}. Saves lifting 43 
398 
lemmas manually. 

13940  399 
*} 
400 

17094  401 
interpretation UP_cring < cring P 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

402 
by intro_locales 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

403 
(rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+ 
13940  404 

14666  405 

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

406 
subsection {* Polynomials Form an Algebra *} 
13940  407 

408 
lemma (in UP_cring) UP_smult_l_distr: 

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

410 
(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  411 
by (rule up_eqI) (simp_all add: R.l_distr) 
412 

413 
lemma (in UP_cring) UP_smult_r_distr: 

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

415 
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  416 
by (rule up_eqI) (simp_all add: R.r_distr) 
417 

418 
lemma (in UP_cring) UP_smult_assoc1: 

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

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

423 
lemma (in UP_cring) UP_smult_one [simp]: 

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

424 
"p \<in> carrier P ==> \<one> \<odot>\<^bsub>P\<^esub> p = p" 
13940  425 
by (rule up_eqI) simp_all 
426 

427 
lemma (in UP_cring) UP_smult_assoc2: 

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

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

432 
text {* 

17094  433 
Interpretation of lemmas from @{term algebra}. 
13940  434 
*} 
435 

436 
lemma (in cring) cring: 

437 
"cring R" 

438 
by (fast intro: cring.intro prems) 

439 

440 
lemma (in UP_cring) UP_algebra: 

441 
"algebra R P" 

17094  442 
by (auto intro: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr 
13940  443 
UP_smult_assoc1 UP_smult_assoc2) 
444 

17094  445 
interpretation UP_cring < algebra R P 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

446 
by intro_locales 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

447 
(rule module.axioms algebra.axioms UP_algebra)+ 
13940  448 

449 

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

450 
subsection {* Further Lemmas Involving Monomials *} 
13940  451 

452 
lemma (in UP_cring) monom_zero [simp]: 

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

453 
"monom P \<zero> n = \<zero>\<^bsub>P\<^esub>" 
13940  454 
by (simp add: UP_def P_def) 
455 

456 
lemma (in UP_cring) monom_mult_is_smult: 

457 
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

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

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

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

464 
next 

465 
case Suc with R show ?thesis 

17094  466 
by (simp cong: R.finsum_cong add: R.r_null Pi_def) 
467 
(simp add: R.m_comm) 

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

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

472 

473 
lemma (in UP_cring) monom_add [simp]: 

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

475 
monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n" 
13940  476 
by (rule up_eqI) simp_all 
477 

478 
lemma (in UP_cring) monom_one_Suc: 

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

479 
"monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1" 
13940  480 
proof (rule up_eqI) 
481 
fix k 

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

482 
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  483 
proof (cases "k = Suc n") 
484 
case True show ?thesis 

485 
proof  

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

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

15045  490 
have "... = (\<Oplus>i \<in> {..<n} \<union> {n}. coeff P (monom P \<one> n) i \<otimes> 
14666  491 
coeff P (monom P \<one> 1) (k  i))" 
17094  492 
by (simp cong: R.finsum_cong add: Pi_def) 
14666  493 
also have "... = (\<Oplus>i \<in> {..n}. coeff P (monom P \<one> n) i \<otimes> 
494 
coeff P (monom P \<one> 1) (k  i))" 

495 
by (simp only: ivl_disj_un_singleton) 

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

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

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

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

505 
next 

506 
case False 

507 
note neq = False 

508 
let ?s = 

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

513 
have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>" 
17094  514 
by (simp cong: R.finsum_cong add: Pi_def) 
14666  515 
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

516 
by (simp cong: R.finsum_cong add: Pi_def) arith 
15045  517 
have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>" 
17094  518 
by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def) 
13940  519 
show ?thesis 
520 
proof (cases "k < n") 

17094  521 
case True then show ?thesis by (simp cong: R.finsum_cong add: Pi_def) 
13940  522 
next 
14666  523 
case False then have n_le_k: "n <= k" by arith 
524 
show ?thesis 

525 
proof (cases "n = k") 

526 
case True 

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

531 
finally show ?thesis . 

532 
next 

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

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

538 
by (simp only: ivl_disj_un_singleton) 

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

543 
finally show ?thesis . 

544 
qed 

13940  545 
qed 
546 
qed 

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

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

550 
qed (simp_all) 

551 

552 
lemma (in UP_cring) monom_mult_smult: 

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

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

556 
lemma (in UP_cring) monom_one [simp]: 

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

557 
"monom P \<one> 0 = \<one>\<^bsub>P\<^esub>" 
13940  558 
by (rule up_eqI) simp_all 
559 

560 
lemma (in UP_cring) monom_one_mult: 

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

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

564 
next 

565 
case Suc then show ?case 

17094  566 
by (simp only: add_Suc monom_one_Suc) (simp add: P.m_ac) 
13940  567 
qed 
568 

569 
lemma (in UP_cring) monom_mult [simp]: 

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

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

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

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

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

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

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

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

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

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

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

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

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

593 

594 
lemma (in UP_cring) monom_a_inv [simp]: 

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

595 
"a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n" 
13940  596 
by (rule up_eqI) simp_all 
597 

598 
lemma (in UP_cring) monom_inj: 

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

600 
proof (rule inj_onI) 

601 
fix x y 

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

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

604 
with R show "x = y" by simp 

605 
qed 

606 

17094  607 

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

608 
subsection {* The Degree Function *} 
13940  609 

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

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

614 
lemma (in UP_cring) deg_aboveI: 

14666  615 
"[ (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P ] ==> deg R p <= n" 
13940  616 
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

617 

13940  618 
(* 
619 
lemma coeff_bound_ex: "EX n. bound n (coeff p)" 

620 
proof  

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

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

623 
then show ?thesis .. 

624 
qed 

14666  625 

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

628 
proof  

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

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

631 
with prem show P . 

632 
qed 

633 
*) 

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

634 

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

637 
proof  

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

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

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

14666  643 
then show ?thesis .. 
13940  644 
qed 
645 

646 
lemma (in UP_cring) deg_belowI: 

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

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

649 
shows "n <= deg R p" 

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

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

654 
next 

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

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

657 
then show ?thesis by arith 

658 
qed 

659 

660 
lemma (in UP_cring) lcoeff_nonzero_deg: 

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

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

663 
proof  

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

665 
proof  

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

667 
by arith 

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

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

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

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

673 
by (unfold bound_def) fast 

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

14666  675 
then show ?thesis by auto 
13940  676 
qed 
677 
with deg_belowI R have "deg R p = m" by fastsimp 

678 
with m_coeff show ?thesis by simp 

679 
qed 

680 

681 
lemma (in UP_cring) lcoeff_nonzero_nonzero: 

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

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

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

686 
proof (rule classical) 

687 
assume "~ ?thesis" 

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

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

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

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

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

694 
with coeff show ?thesis by simp 

695 
qed 

696 

697 
lemma (in UP_cring) lcoeff_nonzero: 

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

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

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

702 
next 

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

704 
qed 

705 

706 
lemma (in UP_cring) deg_eqI: 

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

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

709 
by (fast intro: le_anti_sym deg_aboveI deg_belowI) 

710 

17094  711 
text {* Degree and polynomial operations *} 
13940  712 

713 
lemma (in UP_cring) deg_add [simp]: 

714 
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

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

14666  718 
by (rule deg_aboveI) (simp_all add: True R deg_aboveD) 
13940  719 
next 
720 
case False show ?thesis 

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

722 
qed 

723 

724 
lemma (in UP_cring) deg_monom_le: 

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

726 
by (intro deg_aboveI) simp_all 

727 

728 
lemma (in UP_cring) deg_monom [simp]: 

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

730 
by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) 

731 

732 
lemma (in UP_cring) deg_const [simp]: 

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

734 
proof (rule le_anti_sym) 

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

736 
next 

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

738 
qed 

739 

740 
lemma (in UP_cring) deg_zero [simp]: 

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

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

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

745 
show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all 
13940  746 
qed 
747 

748 
lemma (in UP_cring) deg_one [simp]: 

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

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

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

753 
show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all 
13940  754 
qed 
755 

756 
lemma (in UP_cring) deg_uminus [simp]: 

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

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

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

761 
show "deg R p <= deg R (\<ominus>\<^bsub>P\<^esub> p)" 
13940  762 
by (simp add: deg_belowI lcoeff_nonzero_deg 
17094  763 
inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R) 
13940  764 
qed 
765 

766 
lemma (in UP_domain) deg_smult_ring: 

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

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

771 
lemma (in UP_domain) deg_smult [simp]: 

772 
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

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

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

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

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

781 
qed 

782 

783 
lemma (in UP_cring) deg_mult_cring: 

784 
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

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

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

789 
{ 

790 
fix k i 

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

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

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

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

795 
next 

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

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

798 
qed 

799 
} 

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

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

803 
lemma (in UP_domain) deg_mult [simp]: 

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

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

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

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

808 
show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring) 
13940  809 
next 
810 
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

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

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

815 
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

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

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

821 
also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)" 
13940  822 
by (simp only: ivl_disj_un_singleton) 
14666  823 
also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" 
17094  824 
by (simp cong: R.finsum_cong 
825 
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

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

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

831 
qed 

832 

833 
lemma (in UP_cring) coeff_finsum: 

834 
assumes fin: "finite A" 

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

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

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

839 
lemma (in UP_cring) up_repr: 

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

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

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

844 
fix k 

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

846 
by simp 

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

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

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

850 
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

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

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

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

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

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

13940  863 
finally show ?thesis . 
864 
next 

865 
case False 

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

866 
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

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

17094  870 
by (simp cong: R.finsum_cong 
871 
add: ivl_disj_int_singleton coeff_finsum deg_aboveD R Pi_def) 

13940  872 
finally show ?thesis . 
873 
qed 

874 
qed (simp_all add: R Pi_def) 

875 

876 
lemma (in UP_cring) up_repr_le: 

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

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

881 
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

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

17094  885 
by (simp cong: P.finsum_cong add: P.finsum_Un_disjoint ivl_disj_int_one 
13940  886 
deg_aboveD R Pi_def) 
887 
also have "... = p" by (rule up_repr) 

888 
finally show ?thesis . 

889 
qed 

890 

17094  891 

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

892 
subsection {* Polynomials over Integral Domains *} 
13940  893 

894 
lemma domainI: 

895 
assumes cring: "cring R" 

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

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

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

899 
shows "domain R" 

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

901 
del: disjCI) 

902 

903 
lemma (in UP_domain) UP_one_not_zero: 

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

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

906 
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

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

910 
qed 

911 

912 
lemma (in UP_domain) UP_integral: 

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

913 
"[ 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  914 
proof  
915 
fix p q 

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

916 
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

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

919 
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

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

923 
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

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

927 
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

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

931 
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

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

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

936 
by (simp add: R.integral_iff) 

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

937 
with p q show "p = \<zero>\<^bsub>P\<^esub>  q = \<zero>\<^bsub>P\<^esub>" by fastsimp 
13940  938 
qed 
939 
qed 

940 

941 
theorem (in UP_domain) UP_domain: 

942 
"domain P" 

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

944 

945 
text {* 

17094  946 
Interpretation of theorems from @{term domain}. 
13940  947 
*} 
948 

17094  949 
interpretation UP_domain < "domain" P 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

950 
by intro_locales (rule domain.axioms UP_domain)+ 
13940  951 

14666  952 

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

953 
subsection {* The Evaluation Homomorphism and Universal Property*} 
13940  954 

14666  955 
(* alternative congruence rule (possibly more efficient) 
956 
lemma (in abelian_monoid) finsum_cong2: 

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

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

959 
sorry*) 

960 

13940  961 
theorem (in cring) diagonal_sum: 
962 
"[ f \<in> {..n + m::nat} > carrier R; g \<in> {..n + m} > carrier R ] ==> 

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

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

967 
{ 

968 
fix j 

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

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

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

974 
next 

14666  975 
case (Suc j) 
13940  976 
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

977 
using Suc by (auto intro!: funcset_mem [OF Rg]) 
13940  978 
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

979 
using Suc by (auto intro!: funcset_mem [OF Rg]) 
13940  980 
have R9: "!!i k. [ k <= Suc j ] ==> f k \<in> carrier R" 
14666  981 
using Suc by (auto intro!: funcset_mem [OF Rf]) 
13940  982 
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

983 
using Suc by (auto intro!: funcset_mem [OF Rg]) 
13940  984 
have R11: "g 0 \<in> carrier R" 
14666  985 
using Suc by (auto intro!: funcset_mem [OF Rg]) 
13940  986 
from Suc show ?case 
14666  987 
by (simp cong: finsum_cong add: Suc_diff_le a_ac 
988 
Pi_def R6 R8 R9 R10 R11) 

13940  989 
qed 
990 
} 

991 
then show ?thesis by fast 

992 
qed 

993 

994 
lemma (in abelian_monoid) boundD_carrier: 

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

996 
by auto 

997 

998 
theorem (in cring) cauchy_product: 

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

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

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

1005 
proof  

1006 
fix x 

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

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

1009 
qed 

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

1011 
proof  

1012 
fix x 

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

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

1015 
qed 

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

13940  1018 
by (simp add: diagonal_sum Pi_def) 
15045  1019 
also have "... = (\<Oplus>k \<in> {..n} \<union> {n<..n + m}. \<Oplus>i \<in> {..n + m  k}. f k \<otimes> g i)" 
13940  1020 
by (simp only: ivl_disj_un_one) 
14666  1021 
also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m  k}. f k \<otimes> g i)" 
13940  1022 
by (simp cong: finsum_cong 
14666  1023 
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

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

1025 
have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {m<..n + m  k}. f k \<otimes> g i)" 
13940  1026 
by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def) 
14666  1027 
also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)" 
13940  1028 
by (simp cong: finsum_cong 
14666  1029 
add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def) 
1030 
also from f g have "... = (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)" 

13940  1031 
by (simp add: finsum_ldistr diagonal_sum Pi_def, 
1032 
simp cong: finsum_cong add: finsum_rdistr Pi_def) 

1033 
finally show ?thesis . 

1034 
qed 

1035 

1036 
lemma (in UP_cring) const_ring_hom: 

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

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

1039 

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

1041 
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

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

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

1045 

14666  1046 

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

1047 
lemma (in UP) eval_on_carrier: 
19783  1048 
fixes S (structure) 
17094  1049 
shows "p \<in> carrier P ==> 
1050 
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  1051 
by (unfold eval_def, fold P_def) simp 
1052 

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

1053 
lemma (in UP) eval_extensional: 
17094  1054 
"eval R S phi p \<in> extensional (carrier P)" 
13940  1055 
by (unfold eval_def, fold P_def) simp 
1056 

17094  1057 

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

1059 

1060 
locale UP_pre_univ_prop = ring_hom_cring R S h + UP_cring R P 

1061 

19783  1062 
locale UP_univ_prop = UP_pre_univ_prop + 
1063 
fixes s and Eval 

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

1066 

1067 
theorem (in UP_pre_univ_prop) eval_ring_hom: 

1068 
assumes S: "s \<in> carrier S" 

1069 
shows "eval R S h s \<in> ring_hom P S" 

13940  1070 
proof (rule ring_hom_memI) 
1071 
fix p 

17094  1072 
assume R: "p \<in> carrier P" 
13940  1073 
then show "eval R S h s p \<in> carrier S" 
17094  1074 
by (simp only: eval_on_carrier) (simp add: S Pi_def) 
13940  1075 
next 
1076 
fix p q 

17094  1077 
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

1078 
then show "eval R S h s (p \<otimes>\<^bsub>P\<^esub> q) = eval R S h s p \<otimes>\<^bsub>S\<^esub> eval R S h s q" 
13940  1079 
proof (simp only: eval_on_carrier UP_mult_closed) 
17094  1080 
from R S have 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

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

1083 
h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
17094  1084 
by (simp cong: S.finsum_cong 
1085 
add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def 

14666  1086 
del: coeff_mult) 
17094  1087 
also from R have "... = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1088 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1089 
by (simp only: ivl_disj_un_one deg_mult_cring) 
17094  1090 
also from R S have "... = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

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

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

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

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

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

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

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

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

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

1108 
fix p q 

17094  1109 
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

1110 
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  1111 
proof (simp only: eval_on_carrier P.a_closed) 
1112 
from S R have 

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

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

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

1115 
h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
17094  1116 
by (simp cong: S.finsum_cong 
1117 
add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def 

14666  1118 
del: coeff_add) 
17094  1119 
also from R have "... = 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

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

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

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

1125 
(\<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  1126 
by (simp cong: S.finsum_cong 
1127 
add: S.l_distr deg_aboveD ivl_disj_int_one Pi_def) 

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

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

1130 
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

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

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

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

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

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

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

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

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

17094  1145 
show "eval R S h s \<one>\<^bsub>P\<^esub> = \<one>\<^bsub>S\<^esub>" 
13940  1146 
by (simp only: eval_on_carrier UP_one_closed) simp 
1147 
qed 

1148 

17094  1149 
text {* Interpretation of ring homomorphism lemmas. *} 
13940  1150 

17094  1151 
interpretation UP_univ_prop < ring_hom_cring P S Eval 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1152 
apply (unfold Eval_def) 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

1153 
apply intro_locales 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1154 
apply (rule ring_hom_cring.axioms) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1155 
apply (rule ring_hom_cring.intro) 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

1156 
apply unfold_locales 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1157 
apply (rule eval_ring_hom) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1158 
apply rule 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1159 
done 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1160 

13940  1161 

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

1163 

21502  1164 
text {* 
1165 
The following lemma could be proved in @{text UP_cring} with the additional 

1166 
assumption that @{text h} is closed. *} 

13940  1167 

17094  1168 
lemma (in UP_pre_univ_prop) eval_const: 
13940  1169 
"[ s \<in> carrier S; r \<in> carrier R ] ==> eval R S h s (monom P r 0) = h r" 
1170 
by (simp only: eval_on_carrier monom_closed) simp 

1171 

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

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

1174 

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

1176 

17094  1177 
lemma (in UP_pre_univ_prop) eval_monom1: 
1178 
assumes S: "s \<in> carrier S" 

1179 
shows "eval R S h s (monom P \<one> 1) = s" 

13940  1180 
proof (simp only: eval_on_carrier monom_closed R.one_closed) 
17094  1181 
from S have 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1182 
"(\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R (monom P \<one> 1)}. h (coeff P (monom P \<one> 1) 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

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

1184 
h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
17094  1185 
by (simp cong: S.finsum_cong del: coeff_monom 
1186 
add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def) 

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

1188 
(\<Oplus>\<^bsub>S\<^esub> i \<in> {..1}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" 
13940  1189 
by (simp only: ivl_disj_un_one deg_monom_le R.one_closed) 
1190 
also have "... = s" 

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

1191 
proof (cases "s = \<zero>\<^bsub>S\<^esub>") 
13940  1192 
case True then show ?thesis by (simp add: Pi_def) 
1193 
next 

17094  1194 
case False then show ?thesis by (simp add: S Pi_def) 
13940  1195 
qed 
15095
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1196 
finally show "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (monom P \<one> 1)}. 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1197 
h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = s" . 
13940  1198 
qed 
1199 

1200 
lemma (in UP_cring) monom_pow: 

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

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

1202 
shows "(monom P a n) (^)\<^bsub>P\<^esub> m = monom P (a (^) m) (n * m)" 
13940  1203 
proof (induct m) 
1204 
case 0 from R show ?case by simp 

1205 
next 

1206 
case Suc with R show ?case 

1207 
by (simp del: monom_mult add: monom_mult [THEN sym] add_commute) 

1208 
qed 

1209 

1210 
lemma (in ring_hom_cring) hom_pow [simp]: 

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

1211 
"x \<in> carrier R ==> h (x (^) n) = h x (^)\<^bsub>S\<^esub> (n::nat)" 
13940  1212 
by (induct n) simp_all 
1213 

17094  1214 
lemma (in UP_univ_prop) Eval_monom: 
1215 
"r \<in> carrier R ==> Eval (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" 

13940  1216 
proof  
17094  1217 
assume R: "r \<in> carrier R" 
1218 
from R have "Eval (monom P r n) = Eval (monom P r 0 \<otimes>\<^bsub>P\<^esub> (monom P \<one> 1) (^)\<^bsub>P\<^esub> n)" 

1219 
by (simp del: monom_mult add: monom_mult [THEN sym] monom_pow) 

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

1220 
also 
17094  1221 
from R eval_monom1 [where s = s, folded Eval_def] 
1222 
have "... = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" 

1223 
by (simp add: eval_const [where s = s, folded Eval_def]) 

13940  1224 
finally show ?thesis . 
1225 
qed 

1226 

17094  1227 
lemma (in UP_pre_univ_prop) eval_monom: 
1228 
assumes R: "r \<in> carrier R" and S: "s \<in> carrier S" 

1229 
shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" 

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

1230 
proof  
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1231 
interpret UP_univ_prop [R S h P s _] 
22931  1232 
using `UP_pre_univ_prop R S h` P_def R S 
1233 
by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro) 

17094  1234 
from R 
1235 
show ?thesis by (rule Eval_monom) 

1236 
qed 

1237 

1238 
lemma (in UP_univ_prop) Eval_smult: 

1239 
"[ r \<in> carrier R; p \<in> carrier P ] ==> Eval (r \<odot>\<^bsub>P\<^esub> p) = h r \<otimes>\<^bsub>S\<^esub> Eval p" 

1240 
proof  

1241 
assume R: "r \<in> carrier R" and P: "p \<in> carrier P" 

1242 
then show ?thesis 

1243 
by (simp add: monom_mult_is_smult [THEN sym] 

1244 
eval_const [where s = s, folded Eval_def]) 

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

1245 
qed 
13940  1246 

1247 
lemma ring_hom_cringI: 

1248 
assumes "cring R" 

1249 
and "cring S" 

1250 
and "h \<in> ring_hom R S" 

1251 
shows "ring_hom_cring R S h" 

1252 
by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro 

1253 
cring.axioms prems) 

1254 

17094  1255 
lemma (in UP_pre_univ_prop) UP_hom_unique: 
1256 
includes ring_hom_cring P S Phi 

1257 
assumes Phi: "Phi (monom P \<one> (Suc 0)) = s" 

13940  1258 
"!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r" 
17094  1259 
includes ring_hom_cring P S Psi 
1260 
assumes Psi: "Psi (monom P \<one> (Suc 0)) = s" 

13940  1261 
"!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r" 
17094  1262 
and P: "p \<in> carrier P" and S: "s \<in> carrier S" 
13940  1263 
shows "Phi p = Psi p" 
1264 
proof  

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

1265 
have "Phi p = 
63f5f4c265dd
Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents:
15076
diff
changeset

1266 
Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)" 
17094  1267 
by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult) 
15696  1268 
also 
1269 
have "... = 

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

1270 
Psi (\<Oplus>\<^bsub>P \<^esub>i\<in>{..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)" 
17094  1271 
by (simp add: Phi Psi P Pi_def comp_def) 
13940  1272 
also have "... = Psi p" 
17094  1273 
by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult) 
13940  1274 
finally show ?thesis . 
1275 
qed 

1276 

17094  1277 
lemma (in UP_pre_univ_prop) ring_homD: 
1278 
assumes Phi: "Phi \<in> ring_hom P S" 

1279 
shows "ring_hom_cring P S Phi" 

1280 
proof (rule ring_hom_cring.intro) 

1281 
show "ring_hom_cring_axioms P S Phi" 

1282 
by (rule ring_hom_cring_axioms.intro) (rule Phi) 

19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

1283 
qed unfold_locales 
17094  1284 

1285 
theorem (in UP_pre_univ_prop) UP_universal_property: 

1286 
assumes S: "s \<in> carrier S" 

1287 
shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) & 

14666  1288 
Phi (monom P \<one> 1) = s & 
13940  1289 
(ALL r : carrier R. Phi (monom P r 0) = h r)" 
17094  1290 
using S eval_monom1 
13940  1291 
apply (auto intro: eval_ring_hom eval_const eval_extensional) 
14666  1292 
apply (rule extensionalityI) 
17094  1293 
apply (auto intro: UP_hom_unique ring_homD) 
14666  1294 
done 
13940  1295 

17094  1296 

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

1297 
subsection {* Sample Application of Evaluation Homomorphism *} 
13940  1298 

17094  1299 
lemma UP_pre_univ_propI: 
13940  1300 
assumes "cring R" 
1301 
and "cring S" 

1302 
and "h \<in> ring_hom R S" 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1303 
shows "UP_pre_univ_prop R S h" 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1304 
by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

1305 
ring_hom_cring_axioms.intro UP_cring.intro) 
13940  1306 

13975  1307 
constdefs 
1308 
INTEG :: "int ring" 

1309 
"INTEG == ( 