71 lemma (in cring) a_abelian_semigroup: |
75 lemma (in cring) a_abelian_semigroup: |
72 "abelian_semigroup (| carrier = carrier R, |
76 "abelian_semigroup (| carrier = carrier R, |
73 mult = add R, one = zero R, m_inv = a_inv R |)" |
77 mult = add R, one = zero R, m_inv = a_inv R |)" |
74 by (simp add: abelian_semigroup_def) |
78 by (simp add: abelian_semigroup_def) |
75 |
79 |
76 lemma (in cring) a_abelian_group: |
80 lemmas group_record_simps = semigroup.simps monoid.simps group.simps |
77 "abelian_group (| carrier = carrier R, |
|
78 mult = add R, one = zero R, m_inv = a_inv R |)" |
|
79 by (simp add: abelian_group_def) |
|
80 |
81 |
81 lemmas (in cring) a_closed [intro, simp] = |
82 lemmas (in cring) a_closed [intro, simp] = |
82 magma.m_closed [OF a_magma, simplified] |
83 magma.m_closed [OF a_magma, simplified group_record_simps] |
83 |
84 |
84 lemmas (in cring) zero_closed [intro, simp] = |
85 lemmas (in cring) zero_closed [intro, simp] = |
85 l_one.one_closed [OF a_l_one, simplified] |
86 l_one.one_closed [OF a_l_one, simplified group_record_simps] |
86 |
87 |
87 lemmas (in cring) a_inv_closed [intro, simp] = |
88 lemmas (in cring) a_inv_closed [intro, simp] = |
88 group.inv_closed [OF a_group, simplified] |
89 group.inv_closed [OF a_group, simplified group_record_simps] |
89 |
90 |
90 lemma (in cring) minus_closed [intro, simp]: |
91 lemma (in cring) minus_closed [intro, simp]: |
91 "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R" |
92 "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R" |
92 by (simp add: minus_def) |
93 by (simp add: minus_def) |
93 |
94 |
94 lemmas (in cring) a_l_cancel [simp] = group.l_cancel [OF a_group, simplified] |
95 lemmas (in cring) a_l_cancel [simp] = |
95 |
96 group.l_cancel [OF a_group, simplified group_record_simps] |
96 lemmas (in cring) a_r_cancel [simp] = group.r_cancel [OF a_group, simplified] |
97 |
97 |
98 lemmas (in cring) a_r_cancel [simp] = |
98 lemmas (in cring) a_assoc = semigroup.m_assoc [OF a_semigroup, simplified] |
99 group.r_cancel [OF a_group, simplified group_record_simps] |
99 |
100 |
100 lemmas (in cring) l_zero [simp] = l_one.l_one [OF a_l_one, simplified] |
101 lemmas (in cring) a_assoc = |
101 |
102 semigroup.m_assoc [OF a_semigroup, simplified group_record_simps] |
102 lemmas (in cring) l_neg = group.l_inv [OF a_group, simplified] |
103 |
103 |
104 lemmas (in cring) l_zero [simp] = |
104 lemmas (in cring) a_comm = abelian_semigroup.m_comm [OF a_abelian_semigroup, |
105 l_one.l_one [OF a_l_one, simplified group_record_simps] |
105 simplified] |
106 |
|
107 lemmas (in cring) l_neg = |
|
108 group.l_inv [OF a_group, simplified group_record_simps] |
|
109 |
|
110 lemmas (in cring) a_comm = |
|
111 abelian_semigroup.m_comm [OF a_abelian_semigroup, |
|
112 simplified group_record_simps] |
106 |
113 |
107 lemmas (in cring) a_lcomm = |
114 lemmas (in cring) a_lcomm = |
108 abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified] |
115 abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified group_record_simps] |
109 |
116 |
110 lemma (in cring) r_zero [simp]: |
117 lemma (in cring) r_zero [simp]: |
111 "x \<in> carrier R ==> x \<oplus> \<zero> = x" |
118 "x \<in> carrier R ==> x \<oplus> \<zero> = x" |
112 using group.r_one [OF a_group] |
119 using group.r_one [OF a_group] |
113 by simp |
120 by simp |
226 lemma |
236 lemma |
227 includes cring |
237 includes cring |
228 shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b" |
238 shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b" |
229 by algebra |
239 by algebra |
230 |
240 |
|
241 subsection {* Sums over Finite Sets *} |
|
242 |
|
243 text {* |
|
244 This definition makes it easy to lift lemmas from @{term finprod}. |
|
245 *} |
|
246 |
|
247 constdefs |
|
248 finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" |
|
249 "finsum R f A == finprod (| carrier = carrier R, |
|
250 mult = add R, one = zero R, m_inv = a_inv R |) f A" |
|
251 |
|
252 lemma (in cring) a_abelian_monoid: |
|
253 "abelian_monoid (| carrier = carrier R, |
|
254 mult = add R, one = zero R, m_inv = a_inv R |)" |
|
255 by (simp add: abelian_monoid_def) |
|
256 |
|
257 (* |
|
258 lemmas (in cring) finsum_empty [simp] = |
|
259 abelian_monoid.finprod_empty [OF a_abelian_monoid, simplified] |
|
260 is dangeous, because attributes (like simplified) are applied upon opening |
|
261 the locale, simplified refers to the simpset at that time!!! |
|
262 *) |
|
263 |
|
264 lemmas (in cring) finsum_empty [simp] = |
|
265 abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def, |
|
266 simplified group_record_simps] |
|
267 |
|
268 lemmas (in cring) finsum_insert [simp] = |
|
269 abelian_monoid.finprod_insert [OF a_abelian_monoid, folded finsum_def, |
|
270 simplified group_record_simps] |
|
271 |
|
272 lemmas (in cring) finsum_zero = |
|
273 abelian_monoid.finprod_one [OF a_abelian_monoid, folded finsum_def, |
|
274 simplified group_record_simps] |
|
275 |
|
276 lemmas (in cring) finsum_closed [simp] = |
|
277 abelian_monoid.finprod_closed [OF a_abelian_monoid, folded finsum_def, |
|
278 simplified group_record_simps] |
|
279 |
|
280 lemmas (in cring) finsum_Un_Int = |
|
281 abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, folded finsum_def, |
|
282 simplified group_record_simps] |
|
283 |
|
284 lemmas (in cring) finsum_Un_disjoint = |
|
285 abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, folded finsum_def, |
|
286 simplified group_record_simps] |
|
287 |
|
288 lemmas (in cring) finsum_addf = |
|
289 abelian_monoid.finprod_multf [OF a_abelian_monoid, folded finsum_def, |
|
290 simplified group_record_simps] |
|
291 |
|
292 lemmas (in cring) finsum_cong = |
|
293 abelian_monoid.finprod_cong [OF a_abelian_monoid, folded finsum_def, |
|
294 simplified group_record_simps] |
|
295 |
|
296 lemmas (in cring) finsum_0 [simp] = |
|
297 abelian_monoid.finprod_0 [OF a_abelian_monoid, folded finsum_def, |
|
298 simplified group_record_simps] |
|
299 |
|
300 lemmas (in cring) finsum_Suc [simp] = |
|
301 abelian_monoid.finprod_Suc [OF a_abelian_monoid, folded finsum_def, |
|
302 simplified group_record_simps] |
|
303 |
|
304 lemmas (in cring) finsum_Suc2 = |
|
305 abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, folded finsum_def, |
|
306 simplified group_record_simps] |
|
307 |
|
308 lemmas (in cring) finsum_add [simp] = |
|
309 abelian_monoid.finprod_mult [OF a_abelian_monoid, folded finsum_def, |
|
310 simplified group_record_simps] |
|
311 |
|
312 lemmas (in cring) finsum_cong' [cong] = |
|
313 abelian_monoid.finprod_cong' [OF a_abelian_monoid, folded finsum_def, |
|
314 simplified group_record_simps] |
|
315 |
|
316 (* |
|
317 lemma (in cring) finsum_empty [simp]: |
|
318 "finsum R f {} = \<zero>" |
|
319 by (simp add: finsum_def |
|
320 abelian_monoid.finprod_empty [OF a_abelian_monoid]) |
|
321 |
|
322 lemma (in cring) finsum_insert [simp]: |
|
323 "[| finite F; a \<notin> F; f : F -> carrier R; f a \<in> carrier R |] ==> |
|
324 finsum R f (insert a F) = f a \<oplus> finsum R f F" |
|
325 by (simp add: finsum_def |
|
326 abelian_monoid.finprod_insert [OF a_abelian_monoid]) |
|
327 |
|
328 lemma (in cring) finsum_zero: |
|
329 "finite A ==> finsum R (%i. \<zero>) A = \<zero>" |
|
330 by (simp add: finsum_def |
|
331 abelian_monoid.finprod_one [OF a_abelian_monoid, simplified]) |
|
332 |
|
333 lemma (in cring) finsum_closed [simp]: |
|
334 "[| finite A; f : A -> carrier R |] ==> finsum R f A \<in> carrier R" |
|
335 by (simp only: finsum_def |
|
336 abelian_monoid.finprod_closed [OF a_abelian_monoid, simplified]) |
|
337 |
|
338 lemma (in cring) finsum_Un_Int: |
|
339 "[| finite A; finite B; g \<in> A -> carrier R; g \<in> B -> carrier R |] ==> |
|
340 finsum R g (A Un B) \<oplus> finsum R g (A Int B) = |
|
341 finsum R g A \<oplus> finsum R g B" |
|
342 by (simp only: finsum_def |
|
343 abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, simplified]) |
|
344 |
|
345 lemma (in cring) finsum_Un_disjoint: |
|
346 "[| finite A; finite B; A Int B = {}; |
|
347 g \<in> A -> carrier R; g \<in> B -> carrier R |] |
|
348 ==> finsum R g (A Un B) = finsum R g A \<oplus> finsum R g B" |
|
349 by (simp only: finsum_def |
|
350 abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, simplified]) |
|
351 |
|
352 lemma (in cring) finsum_addf: |
|
353 "[| finite A; f \<in> A -> carrier R; g \<in> A -> carrier R |] ==> |
|
354 finsum R (%x. f x \<oplus> g x) A = (finsum R f A \<oplus> finsum R g A)" |
|
355 by (simp only: finsum_def |
|
356 abelian_monoid.finprod_multf [OF a_abelian_monoid, simplified]) |
|
357 |
|
358 lemma (in cring) finsum_cong: |
|
359 "[| A = B; g : B -> carrier R; |
|
360 !!i. i : B ==> f i = g i |] ==> finsum R f A = finsum R g B" |
|
361 apply (simp only: finsum_def) |
|
362 apply (rule abelian_monoid.finprod_cong [OF a_abelian_monoid, simplified]) |
|
363 apply simp_all |
|
364 done |
|
365 |
|
366 lemma (in cring) finsum_0 [simp]: |
|
367 "f \<in> {0::nat} -> carrier R ==> finsum R f {..0} = f 0" |
|
368 by (simp add: finsum_def |
|
369 abelian_monoid.finprod_0 [OF a_abelian_monoid, simplified]) |
|
370 |
|
371 lemma (in cring) finsum_Suc [simp]: |
|
372 "f \<in> {..Suc n} -> carrier R ==> |
|
373 finsum R f {..Suc n} = (f (Suc n) \<oplus> finsum R f {..n})" |
|
374 by (simp add: finsum_def |
|
375 abelian_monoid.finprod_Suc [OF a_abelian_monoid, simplified]) |
|
376 |
|
377 lemma (in cring) finsum_Suc2: |
|
378 "f \<in> {..Suc n} -> carrier R ==> |
|
379 finsum R f {..Suc n} = (finsum R (%i. f (Suc i)) {..n} \<oplus> f 0)" |
|
380 by (simp only: finsum_def |
|
381 abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, simplified]) |
|
382 |
|
383 lemma (in cring) finsum_add [simp]: |
|
384 "[| f : {..n} -> carrier R; g : {..n} -> carrier R |] ==> |
|
385 finsum R (%i. f i \<oplus> g i) {..n::nat} = |
|
386 finsum R f {..n} \<oplus> finsum R g {..n}" |
|
387 by (simp only: finsum_def |
|
388 abelian_monoid.finprod_mult [OF a_abelian_monoid, simplified]) |
|
389 |
|
390 lemma (in cring) finsum_cong' [cong]: |
|
391 "[| A = B; !!i. i : B ==> f i = g i; |
|
392 g \<in> B -> carrier R = True |] ==> finsum R f A = finsum R g B" |
|
393 apply (simp only: finsum_def) |
|
394 apply (rule abelian_monoid.finprod_cong' [OF a_abelian_monoid, simplified]) |
|
395 apply simp_all |
|
396 done |
|
397 *) |
|
398 |
|
399 text {*Usually, if this rule causes a failed congruence proof error, |
|
400 the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown. |
|
401 Adding @{thm [source] Pi_def} to the simpset is often useful. *} |
|
402 |
|
403 lemma (in cring) finsum_ldistr: |
|
404 "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==> |
|
405 finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A" |
|
406 proof (induct set: Finites) |
|
407 case empty then show ?case by simp |
|
408 next |
|
409 case (insert F x) then show ?case by (simp add: Pi_def l_distr) |
|
410 qed |
|
411 |
|
412 lemma (in cring) finsum_rdistr: |
|
413 "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==> |
|
414 a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A" |
|
415 proof (induct set: Finites) |
|
416 case empty then show ?case by simp |
|
417 next |
|
418 case (insert F x) then show ?case by (simp add: Pi_def r_distr) |
|
419 qed |
|
420 |
|
421 subsection {* Facts of Integral Domains *} |
|
422 |
|
423 lemma (in "domain") zero_not_one [simp]: |
|
424 "\<zero> ~= \<one>" |
|
425 by (rule not_sym) simp |
|
426 |
|
427 lemma (in "domain") integral_iff: (* not by default a simp rule! *) |
|
428 "[| a \<in> carrier R; b \<in> carrier R |] ==> (a \<otimes> b = \<zero>) = (a = \<zero> | b = \<zero>)" |
|
429 proof |
|
430 assume "a \<in> carrier R" "b \<in> carrier R" "a \<otimes> b = \<zero>" |
|
431 then show "a = \<zero> | b = \<zero>" by (simp add: integral) |
|
432 next |
|
433 assume "a \<in> carrier R" "b \<in> carrier R" "a = \<zero> | b = \<zero>" |
|
434 then show "a \<otimes> b = \<zero>" by auto |
|
435 qed |
|
436 |
|
437 lemma (in "domain") m_lcancel: |
|
438 assumes prem: "a ~= \<zero>" |
|
439 and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R" |
|
440 shows "(a \<otimes> b = a \<otimes> c) = (b = c)" |
|
441 proof |
|
442 assume eq: "a \<otimes> b = a \<otimes> c" |
|
443 with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra |
|
444 with R have "a = \<zero> | (b \<ominus> c) = \<zero>" by (simp add: integral_iff) |
|
445 with prem and R have "b \<ominus> c = \<zero>" by auto |
|
446 with R have "b = b \<ominus> (b \<ominus> c)" by algebra |
|
447 also from R have "b \<ominus> (b \<ominus> c) = c" by algebra |
|
448 finally show "b = c" . |
|
449 next |
|
450 assume "b = c" then show "a \<otimes> b = a \<otimes> c" by simp |
|
451 qed |
|
452 |
|
453 lemma (in "domain") m_rcancel: |
|
454 assumes prem: "a ~= \<zero>" |
|
455 and R: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R" |
|
456 shows conc: "(b \<otimes> a = c \<otimes> a) = (b = c)" |
|
457 proof - |
|
458 from prem and R have "(a \<otimes> b = a \<otimes> c) = (b = c)" by (rule m_lcancel) |
|
459 with R show ?thesis by algebra |
|
460 qed |
|
461 |
231 end |
462 end |