author | wenzelm |
Wed, 15 Aug 2018 16:15:23 +0200 | |
changeset 68753 | b0ed78ffa4d9 |
parent 68608 | 4a4c2bc4b869 |
child 68975 | 5ce4d117cea7 |
permissions | -rw-r--r-- |
68582 | 1 |
(* Title: HOL/Algebra/Chinese_Remainder.thy |
2 |
Author: Paulo Emílio de Vilhena |
|
3 |
*) |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
5 |
theory Chinese_Remainder |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
imports QuotRing Ideal_Product |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
begin |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
9 |
section \<open>Chinese Remainder Theorem\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
10 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
11 |
subsection \<open>Direct Product of Rings\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
12 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
13 |
definition |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
14 |
RDirProd :: "[ ('a, 'n) ring_scheme, ('b, 'm) ring_scheme ] \<Rightarrow> ('a \<times> 'b) ring" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
15 |
where "RDirProd R S = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
16 |
\<lparr> carrier = carrier R \<times> carrier S, |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
17 |
mult = (\<lambda>(r, s). \<lambda>(r', s'). (r \<otimes>\<^bsub>R\<^esub> r', s \<otimes>\<^bsub>S\<^esub> s')), |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
18 |
one = (\<one>\<^bsub>R\<^esub>, \<one>\<^bsub>S\<^esub>), |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
19 |
zero = (\<zero>\<^bsub>R\<^esub>, \<zero>\<^bsub>S\<^esub>), |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
20 |
add = (\<lambda>(r, s). \<lambda>(r', s'). (r \<oplus>\<^bsub>R\<^esub> r', s \<oplus>\<^bsub>S\<^esub> s')) \<rparr>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
21 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
22 |
lemma RDirProd_monoid: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
23 |
assumes "ring R" and "ring S" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
24 |
shows "monoid (RDirProd R S)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
25 |
by (rule monoidI) (auto simp add: RDirProd_def assms ring.ring_simprules ring.is_monoid) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
26 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
27 |
lemma RDirProd_abelian_group: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
28 |
assumes "ring R" and "ring S" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
29 |
shows "abelian_group (RDirProd R S)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
30 |
by (auto intro!: abelian_groupI |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
31 |
simp add: RDirProd_def assms ring.ring_simprules) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
32 |
(meson assms ring.ring_simprules(3,16))+ |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
34 |
lemma RDirProd_group: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
35 |
assumes "ring R" and "ring S" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
36 |
shows "ring (RDirProd R S)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
37 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
38 |
show ?thesis |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
39 |
apply (rule ringI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
40 |
apply (simp_all add: assms RDirProd_abelian_group RDirProd_monoid) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
41 |
by (auto simp add: RDirProd_def assms ring.ring_simprules) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
42 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
43 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
44 |
lemma RDirProd_isomorphism1: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
45 |
"(\<lambda>(x, y). (y, x)) \<in> ring_iso (RDirProd R S) (RDirProd S R)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
46 |
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def RDirProd_def by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
47 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
48 |
lemma RDirProd_isomorphism2: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
49 |
"(\<lambda>(x, (y, z)). ((x, y), z)) \<in> ring_iso (RDirProd R (RDirProd S T)) (RDirProd (RDirProd R S) T)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
50 |
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def RDirProd_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
51 |
by (auto simp add: image_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
52 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
53 |
lemma RDirProd_isomorphism3: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
54 |
"(\<lambda>((x, y), z). (x, (y, z))) \<in> ring_iso (RDirProd (RDirProd R S) T) (RDirProd R (RDirProd S T))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
55 |
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def RDirProd_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
56 |
by (auto simp add: image_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
57 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
58 |
lemma RDirProd_isomorphism4: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
59 |
assumes "f \<in> ring_iso R S" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
60 |
shows "(\<lambda>(r, t). (f r, t)) \<in> ring_iso (RDirProd R T) (RDirProd S T)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
61 |
using assms unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def RDirProd_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
62 |
by (auto simp add: image_iff)+ |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
63 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
64 |
lemma RDirProd_isomorphism5: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
65 |
assumes "f \<in> ring_iso S T" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
66 |
shows "(\<lambda>(r, s). (r, f s)) \<in> ring_iso (RDirProd R S) (RDirProd R T)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
67 |
using ring_iso_set_trans[OF ring_iso_set_trans[OF RDirProd_isomorphism1[of R S] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
68 |
RDirProd_isomorphism4[OF assms, of R]] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
69 |
RDirProd_isomorphism1[of T R]] |
68608
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
70 |
by (simp add: case_prod_unfold comp_def) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
71 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
72 |
lemma RDirProd_isomorphism6: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
73 |
assumes "f \<in> ring_iso R R'" and "g \<in> ring_iso S S'" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
74 |
shows "(\<lambda>(r, s). (f r, g s)) \<in> ring_iso (RDirProd R S) (RDirProd R' S')" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
75 |
using ring_iso_set_trans[OF RDirProd_isomorphism4[OF assms(1)] RDirProd_isomorphism5[OF assms(2)]] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
76 |
by (simp add: case_prod_beta' comp_def) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
77 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
78 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
79 |
subsection \<open>Simple Version of The Theorem\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
80 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
81 |
text \<open>We start by proving a simpler version of the theorem. The rest of the theory is |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
82 |
dedicated to its generalization\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
83 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
84 |
lemma (in ideal) set_add_zero: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
85 |
assumes "i \<in> I" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
86 |
shows "I +> i = I" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
87 |
by (simp add: a_rcos_const assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
88 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
89 |
lemma (in ideal) set_add_zero_imp_mem: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
90 |
assumes "i \<in> carrier R" "I +> i = I" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
91 |
shows "i \<in> I" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
92 |
using a_rcos_self assms(1-2) by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
93 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
94 |
lemma (in ring) canonical_proj_is_surj: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
95 |
assumes "ideal I R" "ideal J R" "I <+> J = carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
96 |
shows "\<And>x y. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
97 |
\<exists>a \<in> carrier R. I +> a = I +> x \<and> J +> a = J +> y" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
98 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
99 |
{ fix I J i j assume A: "ideal I R" "ideal J R" "i \<in> I" "j \<in> J" "\<one> = i \<oplus> j" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
100 |
have "I +> \<one> = I +> j" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
101 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
102 |
have "I +> \<one> = I +> (i \<oplus> j)" using A(5) by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
103 |
also have " ... = (I +> i) <+> (I +> j)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
104 |
by (metis abelian_subgroup.a_rcos_sum abelian_subgroupI3 A(1-4) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
105 |
ideal.Icarr ideal.axioms(1) is_abelian_group) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
106 |
also have " ... = (I +> \<zero>) <+> (I +> j)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
107 |
using ideal.set_add_zero[OF A(1) A(3)] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
108 |
by (simp add: A(1) additive_subgroup.a_subset ideal.axioms(1)) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
109 |
also have " ... = I +> (\<zero> \<oplus> j)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
110 |
by (meson A abelian_subgroup.a_rcos_sum abelian_subgroupI3 |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
111 |
additive_subgroup.a_Hcarr ideal.axioms(1) is_abelian_group zero_closed) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
112 |
finally show "I +> \<one> = I +> j" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
113 |
using A(2) A(4) ideal.Icarr by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
114 |
qed } note aux_lemma = this |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
115 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
116 |
fix x y assume x: "x \<in> carrier R" and y: "y \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
117 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
118 |
have "\<one> \<in> I <+> J" using assms by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
119 |
then obtain i j where i: "i \<in> I" and j: "j \<in> J" and ij: "\<one> = i \<oplus> j" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
120 |
using set_add_def'[of R I J] by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
121 |
have mod_I: "I +> j = I +> \<one>" and mod_J: "J +> i = J +> \<one>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
122 |
using aux_lemma[OF assms(1-2) i j ij] apply simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
123 |
using aux_lemma[OF assms(2) assms(1) j i] ij |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
124 |
by (metis add.m_comm assms(1) assms(2) i ideal.Icarr j) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
125 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
126 |
have "I +> ((j \<otimes> x) \<oplus> (i \<otimes> y)) = (I +> (j \<otimes> x)) <+> (I +> (i \<otimes> y))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
127 |
by (metis abelian_subgroup.a_rcos_sum abelian_subgroupI3 assms i ideal.Icarr |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
128 |
ideal.axioms(1) is_abelian_group j m_closed x y) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
129 |
also have " ... = (I +> (j \<otimes> x)) <+> (I +> \<zero>)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
130 |
using ideal.set_add_zero[OF assms(1), of "i \<otimes> y"] i assms(1) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
131 |
by (simp add: additive_subgroup.a_subset ideal.I_r_closed ideal.axioms(1) y) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
132 |
also have " ... = I +> (j \<otimes> x)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
133 |
by (metis abelian_subgroup.a_rcos_sum abelian_subgroupI3 additive_subgroup.a_Hcarr assms(1-2) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
134 |
ideal.axioms(1) is_abelian_group j m_closed r_zero x zero_closed) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
135 |
finally have Ix: "I +> ((j \<otimes> x) \<oplus> (i \<otimes> y)) = I +> x" using mod_I |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
136 |
by (metis (full_types) assms ideal.Icarr ideal.rcoset_mult_add is_monoid j monoid.l_one one_closed x) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
137 |
have "J +> ((j \<otimes> x) \<oplus> (i \<otimes> y)) = (J +> (j \<otimes> x)) <+> (J +> (i \<otimes> y))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
138 |
by (metis abelian_subgroup.a_rcos_sum abelian_subgroupI3 assms i ideal.Icarr |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
139 |
ideal.axioms(1) is_abelian_group j m_closed x y) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
140 |
also have " ... = (J +> \<zero>) <+> (J +> (i \<otimes> y))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
141 |
using ideal.set_add_zero[OF assms(2), of "j \<otimes> x"] j assms(2) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
142 |
by (simp add: additive_subgroup.a_subset ideal.I_r_closed ideal.axioms(1) x) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
143 |
also have " ... = J +> (i \<otimes> y)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
144 |
by (metis a_coset_add_zero a_rcosetsI abelian_subgroup.rcosets_add_eq abelian_subgroupI3 |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
145 |
additive_subgroup.a_Hcarr additive_subgroup.a_subset assms i ideal.axioms(1) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
146 |
is_abelian_group m_closed y) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
147 |
finally have Jy: "J +> ((j \<otimes> x) \<oplus> (i \<otimes> y)) = J +> y" using mod_J |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
148 |
by (metis (full_types) assms i ideal.Icarr ideal.rcoset_mult_add local.semiring_axioms one_closed semiring.semiring_simprules(9) y) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
149 |
have "(j \<otimes> x) \<oplus> (i \<otimes> y) \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
150 |
by (meson x y i j assms add.m_closed additive_subgroup.a_Hcarr ideal.axioms(1) m_closed) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
151 |
thus "\<exists>a \<in> carrier R. I +> a = I +> x \<and> J +> a = J +> y" using Ix Jy by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
152 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
153 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
154 |
lemma (in ring) canonical_proj_is_hom: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
155 |
assumes "ideal I R" "ideal J R" "I <+> J = carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
156 |
shows "(\<lambda>a. (I +> a, J +> a)) \<in> ring_hom R (RDirProd (R Quot I) (R Quot J))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
157 |
proof (rule ring_hom_memI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
158 |
fix x y assume x: "x \<in> carrier R" and y: "y \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
159 |
show "(I +> x, J +> x) \<in> carrier (RDirProd (R Quot I) (R Quot J))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
160 |
using A_RCOSETS_def'[of R I] A_RCOSETS_def'[of R J] x |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
161 |
unfolding RDirProd_def FactRing_def by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
162 |
show "(I +> x \<otimes> y, J +> x \<otimes> y) = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
163 |
(I +> x, J +> x) \<otimes>\<^bsub>RDirProd (R Quot I) (R Quot J)\<^esub> (I +> y, J +> y)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
164 |
unfolding RDirProd_def FactRing_def by (simp add: assms ideal.rcoset_mult_add x y) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
165 |
show "(I +> x \<oplus> y, J +> x \<oplus> y) = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
166 |
(I +> x, J +> x) \<oplus>\<^bsub>RDirProd (R Quot I) (R Quot J)\<^esub> (I +> y, J +> y)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
167 |
unfolding RDirProd_def FactRing_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
168 |
by (simp add: abelian_subgroup.a_rcos_sum abelian_subgroupI3 assms ideal.axioms(1) is_abelian_group x y) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
169 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
170 |
show "(I +> \<one>, J +> \<one>) = \<one>\<^bsub>RDirProd (R Quot I) (R Quot J)\<^esub>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
171 |
unfolding RDirProd_def FactRing_def by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
172 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
173 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
174 |
theorem (in ring) chinese_remainder_simple: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
175 |
assumes "ideal I R" "ideal J R" "I <+> J = carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
176 |
shows "(R Quot (I \<inter> J)) \<simeq> (RDirProd (R Quot I) (R Quot J))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
177 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
178 |
let ?\<phi> = "\<lambda>a. (I +> a, J +> a)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
179 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
180 |
have phi_hom: "?\<phi> \<in> ring_hom R (RDirProd (R Quot I) (R Quot J))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
181 |
using canonical_proj_is_hom[OF assms] . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
182 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
183 |
moreover have "?\<phi> ` (carrier R) = carrier (RDirProd (R Quot I) (R Quot J))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
184 |
proof |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
185 |
show "carrier (RDirProd (R Quot I) (R Quot J)) \<subseteq> ?\<phi> ` (carrier R)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
186 |
proof |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
187 |
fix t assume "t \<in> carrier (RDirProd (R Quot I) (R Quot J))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
188 |
then obtain x y where x: "x \<in> carrier R" and y: "y \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
189 |
and t: "t = (I +> x, J +> y)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
190 |
using A_RCOSETS_def'[of R I] A_RCOSETS_def'[of R J] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
191 |
unfolding RDirProd_def FactRing_def by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
192 |
then obtain a where "a \<in> carrier R" "I +> a = I +> x" "J +> a = J +> y" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
193 |
using canonical_proj_is_surj[OF assms x y] by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
194 |
hence "?\<phi> a = t" using t by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
195 |
thus "t \<in> (?\<phi> ` carrier R)" using \<open>a \<in> carrier R\<close> by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
196 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
197 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
198 |
show "?\<phi> ` carrier R \<subseteq> carrier (RDirProd (R Quot I) (R Quot J))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
199 |
using phi_hom unfolding ring_hom_def by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
200 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
201 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
202 |
moreover have "a_kernel R (RDirProd (R Quot I) (R Quot J)) ?\<phi> = I \<inter> J" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
203 |
proof |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
204 |
show "I \<inter> J \<subseteq> a_kernel R (RDirProd (R Quot I) (R Quot J)) ?\<phi>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
205 |
proof |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
206 |
fix s assume s: "s \<in> I \<inter> J" hence "I +> s = I \<and> J +> s = J" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
207 |
by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1) ideal.set_add_zero) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
208 |
thus "s \<in> a_kernel R (RDirProd (R Quot I) (R Quot J)) ?\<phi>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
209 |
unfolding FactRing_def RDirProd_def a_kernel_def kernel_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
210 |
using s additive_subgroup.a_Hcarr assms(1) ideal.axioms(1) by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
211 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
212 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
213 |
show "a_kernel R (RDirProd (R Quot I) (R Quot J)) ?\<phi> \<subseteq> I \<inter> J" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
214 |
unfolding FactRing_def RDirProd_def a_kernel_def kernel_def apply simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
215 |
using ideal.set_add_zero_imp_mem assms(1-2) by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
216 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
217 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
218 |
moreover have "ring (RDirProd (R Quot I) (R Quot J))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
219 |
by (simp add: RDirProd_group assms(1) assms(2) ideal.quotient_is_ring) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
220 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
221 |
ultimately show ?thesis |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
222 |
using ring_hom_ring.FactRing_iso[of R "RDirProd (R Quot I) (R Quot J)" ?\<phi>] is_ring |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
223 |
by (simp add: ring_hom_ringI2) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
224 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
225 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
226 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
227 |
subsection \<open>First Generalization - The Extended Canonical Projection is Surjective\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
228 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
229 |
lemma (in cring) canonical_proj_ext_is_surj: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
230 |
fixes n::nat |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
231 |
assumes "\<And>i. i \<le> n \<Longrightarrow> x i \<in> carrier R" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
232 |
and "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
233 |
and "\<And>i j. \<lbrakk> i \<le> n; j \<le> n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
234 |
shows "\<exists> a \<in> carrier R. \<forall> i \<le> n. (I i) +> a = (I i) +> (x i)" using assms |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
235 |
proof (induct n) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
236 |
case 0 thus ?case by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
237 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
238 |
case (Suc n) |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
239 |
then obtain a where a: "a \<in> carrier R" "\<And>i. i \<le> n \<Longrightarrow> (I i) +> a = (I i) +> (x i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
240 |
by force |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
241 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
242 |
have inter_is_ideal: "ideal (\<Inter> i \<le> n. I i) R" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
243 |
by (metis (mono_tags, lifting) Suc.prems(2) atMost_iff i_Intersect imageE image_is_empty le_SucI not_empty_eq_Iic_eq_empty) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
244 |
have "(\<Inter> i \<le> n. I i) <+> I (Suc n) = carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
245 |
using inter_plus_ideal_eq_carrier Suc by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
246 |
then obtain b where b: "b \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
247 |
and "(\<Inter> i \<le> n. I i) +> b = (\<Inter> i \<le> n. I i) +> \<zero>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
248 |
and S: "I (Suc n) +> b = I (Suc n) +> (x (Suc n) \<ominus> a)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
249 |
using canonical_proj_is_surj[OF inter_is_ideal, of "I (Suc n)" \<zero> "x (Suc n) \<ominus> a"] Suc a by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
250 |
hence b_inter: "b \<in> (\<Inter> i \<le> n. I i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
251 |
using ideal.set_add_zero_imp_mem[OF inter_is_ideal b] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
252 |
by (metis additive_subgroup.zero_closed ideal.axioms(1) ideal.set_add_zero inter_is_ideal) |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
253 |
hence eq_zero: "\<And>i. i \<le> n \<Longrightarrow> (I i) +> b = (I i) +> \<zero>" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
254 |
proof - |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
255 |
fix i assume i: "i \<le> n" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
256 |
hence "b \<in> I i" using b_inter by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
257 |
moreover have "ideal (I i) R" using Suc i by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
258 |
ultimately show "(I i) +> b = (I i) +> \<zero>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
259 |
by (metis b ideal.I_r_closed ideal.set_add_zero r_null zero_closed) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
260 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
261 |
|
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
262 |
have "(I i) +> (a \<oplus> b) = (I i) +> (x i)" if "i \<le> Suc n" for i |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
263 |
proof - |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
264 |
show "(I i) +> (a \<oplus> b) = (I i) +> (x i)" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
265 |
using that |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
266 |
proof (cases) |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
267 |
assume 1: "i \<le> n" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
268 |
hence "(I i) +> (a \<oplus> b) = ((I i) +> (x i)) <+> ((I i) +> b)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
269 |
by (metis Suc.prems(2) a abelian_subgroup.a_rcos_sum abelian_subgroupI3 b ideal_def le_SucI ring_def) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
270 |
also have " ... = ((I i) +> (x i)) <+> ((I i) +> \<zero>)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
271 |
using eq_zero[OF 1] by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
272 |
also have " ... = I i +> ((x i) \<oplus> \<zero>)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
273 |
by (meson Suc.prems abelian_subgroup.a_rcos_sum abelian_subgroupI3 atMost_iff that ideal_def ring_def zero_closed) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
274 |
finally show "(I i) +> (a \<oplus> b) = (I i) +> (x i)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
275 |
using Suc.prems(1) that by auto |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
276 |
next |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
277 |
assume "\<not> i \<le> n" hence 2: "i = Suc n" using that by simp |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
278 |
hence "I i +> (a \<oplus> b) = I (Suc n) +> (a \<oplus> b)" by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
279 |
also have " ... = (I (Suc n) +> a) <+> (I (Suc n) +> (x (Suc n) \<ominus> a))" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
280 |
by (metis le_Suc_eq S a b Suc.prems(2)[of "Suc n"] 2 abelian_subgroup.a_rcos_sum |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
281 |
abelian_subgroupI3 ideal.axioms(1) is_abelian_group) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
282 |
also have " ... = I (Suc n) +> (a \<oplus> (x (Suc n) \<ominus> a))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
283 |
by (simp add: Suc.prems(1-2) a(1) abelian_subgroup.a_rcos_sum |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
284 |
abelian_subgroupI3 ideal.axioms(1) is_abelian_group) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
285 |
also have " ... = I (Suc n) +> (x (Suc n))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
286 |
using a(1) Suc.prems(1)[of "Suc n"] abelian_group.minus_eq |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
287 |
abelian_group.r_neg add.m_lcomm is_abelian_group by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
288 |
finally show "I i +> (a \<oplus> b) = (I i) +> (x i)" using 2 by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
289 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
290 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
291 |
thus ?case using a b by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
292 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
293 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
294 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
295 |
subsection \<open>Direct Product of a List of Monoid Structures\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
296 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
297 |
fun DirProd_list :: "(('a, 'b) monoid_scheme) list \<Rightarrow> (('a list), 'b) monoid_scheme" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
298 |
where |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
299 |
"DirProd_list [] = \<lparr> carrier = {[]}, mult = (\<lambda>a b. []), one = [], \<dots> = (undefined :: 'b) \<rparr>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
300 |
| "DirProd_list (Cons R Rs) = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
301 |
\<lparr> carrier = { r # rs | r rs. r \<in> carrier R \<and> rs \<in> carrier (DirProd_list Rs) }, |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
302 |
mult = (\<lambda>r1 r2. ((hd r1) \<otimes>\<^bsub>R\<^esub> (hd r2)) # ((tl r1) \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> (tl r2))), |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
303 |
one = (\<one>\<^bsub>R\<^esub>) # (\<one>\<^bsub>(DirProd_list Rs)\<^esub>), \<dots> = (undefined :: 'b) \<rparr>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
304 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
305 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
306 |
lemma DirProd_list_carrier_elts: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
307 |
assumes "rs \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
308 |
shows "length rs = length Rs" using assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
309 |
proof (induct Rs arbitrary: rs rule: DirProd_list.induct) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
310 |
case 1 thus ?case by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
311 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
312 |
case (2 R Rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
313 |
then obtain r' rs' where "r' \<in> carrier R" "rs' \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
314 |
and "rs = r' # rs'" by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
315 |
thus ?case by (simp add: "2.hyps"(1)) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
316 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
317 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
318 |
lemma DirProd_list_in_carrierI: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
319 |
assumes "\<And>i. i < length rs \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
320 |
and "length rs = length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
321 |
shows "rs \<in> carrier (DirProd_list Rs)" using assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
322 |
proof (induct Rs arbitrary: rs rule: DirProd_list.induct) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
323 |
case 1 thus ?case by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
324 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
325 |
case (2 R Rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
326 |
then obtain r' rs' where rs: "r' \<in> carrier R" "rs = r' # rs'" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
327 |
by (metis Suc_length_conv lessThan_iff nth_Cons_0 zero_less_Suc) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
328 |
hence "rs' \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
329 |
using "2.hyps"(1) "2.prems"(1) "2.prems"(2) by force |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
330 |
thus ?case by (simp add: rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
331 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
332 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
333 |
lemma DirProd_list_in_carrierE: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
334 |
assumes "rs \<in> carrier (DirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
335 |
shows "\<And>i. i < length rs \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)" using assms |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
336 |
proof (induct Rs arbitrary: rs rule: DirProd_list.induct) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
337 |
case 1 thus ?case by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
338 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
339 |
case (2 R Rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
340 |
then obtain r' rs' where r': " r' \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
341 |
and rs': "rs' \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
342 |
and rs: "rs = r' # rs'" by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
343 |
hence "\<And>i. i \<in> {..<(length rs')} \<Longrightarrow> rs' ! i \<in> carrier (Rs ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
344 |
using "2.hyps"(1) by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
345 |
hence "\<And>i. i \<in> {(Suc 0 :: nat)..<(length rs)} \<Longrightarrow> rs ! i \<in> carrier ((R # Rs) ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
346 |
by (simp add: less_eq_Suc_le rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
347 |
moreover have "i = 0 \<Longrightarrow> rs ! i \<in> carrier ((R # Rs) ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
348 |
using r' rs r' by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
349 |
ultimately show ?case |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
350 |
using "2.prems"(1) by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
351 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
352 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
353 |
lemma DirProd_list_m_closed: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
354 |
assumes "r1 \<in> carrier (DirProd_list Rs)" "r2 \<in> carrier (DirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
355 |
and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
356 |
shows "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2 \<in> carrier (DirProd_list Rs)" using assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
357 |
proof (induct Rs arbitrary: r1 r2 rule: DirProd_list.induct) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
358 |
case 1 thus ?case by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
359 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
360 |
case (2 R Rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
361 |
then obtain r1' rs1' r2' rs2' |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
362 |
where r12': "r1' \<in> carrier R" "r2' \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
363 |
and "rs1' \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
364 |
and "rs2' \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
365 |
and r1: "r1 = r1' # rs1'" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
366 |
and r2: "r2 = r2' # rs2'" by auto |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
367 |
moreover have "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
368 |
using "2.prems"(3) by force |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
369 |
ultimately have "rs1' \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> rs2' \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
370 |
using "2.hyps"(1) by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
371 |
moreover have "monoid R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
372 |
using "2.prems"(3) by force |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
373 |
hence "r1' \<otimes>\<^bsub>R\<^esub> r2' \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
374 |
by (simp add: r12' monoid.m_closed) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
375 |
ultimately show ?case by (simp add: r1 r2) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
376 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
377 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
378 |
lemma DirProd_list_m_output: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
379 |
assumes "r1 \<in> carrier (DirProd_list Rs)" "r2 \<in> carrier (DirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
380 |
shows "\<And>i. i < length Rs \<Longrightarrow> |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
381 |
(r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2) ! i = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)" using assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
382 |
proof (induct Rs arbitrary: r1 r2 rule: DirProd_list.induct) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
383 |
case 1 thus ?case by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
384 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
385 |
case (2 R Rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
386 |
hence "\<And>i. i \<in> {(Suc 0)..<(length (R # Rs))} \<Longrightarrow> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
387 |
(r1 \<otimes>\<^bsub>(DirProd_list (R # Rs))\<^esub> r2) ! i = (r1 ! i) \<otimes>\<^bsub>((R # Rs) ! i)\<^esub> (r2 ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
388 |
using "2"(5) "2"(6) by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
389 |
moreover have "(r1 \<otimes>\<^bsub>(DirProd_list (R # Rs))\<^esub> r2) ! 0 = (r1 ! 0) \<otimes>\<^bsub>R\<^esub> (r2 ! 0)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
390 |
using "2.prems"(2) "2.prems"(3) by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
391 |
ultimately show ?case |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
392 |
by (metis "2.prems"(1) atLeastLessThan_iff le_0_eq lessThan_iff not_less_eq_eq nth_Cons') |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
393 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
394 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
395 |
lemma DirProd_list_m_comm: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
396 |
assumes "r1 \<in> carrier (DirProd_list Rs)" "r2 \<in> carrier (DirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
397 |
and "\<And>i. i < length Rs \<Longrightarrow> comm_monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
398 |
shows "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2 = r2 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
399 |
apply (rule nth_equalityI) apply auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
400 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
401 |
show "length (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) = length (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
402 |
by (metis DirProd_list_carrier_elts DirProd_list_m_closed Group.comm_monoid.axioms(1) assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
403 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
404 |
fix i assume "i < length (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
405 |
hence i: "i < length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
406 |
by (metis DirProd_list_carrier_elts DirProd_list_m_closed Group.comm_monoid.axioms(1) assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
407 |
have "(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) ! i = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
408 |
using i DirProd_list_m_output[OF assms(1-2)] by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
409 |
also have " ... = (r2 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r1 ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
410 |
by (metis DirProd_list_carrier_elts DirProd_list_in_carrierE assms comm_monoid.m_comm i lessThan_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
411 |
also have " ... = (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
412 |
using i DirProd_list_m_output[OF assms(2) assms(1)] by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
413 |
finally show "(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) ! i = (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i" . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
414 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
415 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
416 |
lemma DirProd_list_m_assoc: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
417 |
assumes "r1 \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
418 |
and "r2 \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
419 |
and "r3 \<in> carrier (DirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
420 |
and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
421 |
shows "(r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r2) \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r3 = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
422 |
r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> (r2 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r3)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
423 |
apply (rule nth_equalityI) apply auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
424 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
425 |
show "length ((r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3) = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
426 |
length (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
427 |
by (metis DirProd_list_carrier_elts DirProd_list_m_closed assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
428 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
429 |
fix i assume "i < length (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
430 |
hence i: "i < length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
431 |
by (metis DirProd_list_carrier_elts DirProd_list_m_closed assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
432 |
have "((r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
433 |
((r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r3 ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
434 |
by (metis DirProd_list_m_closed DirProd_list_m_output i assms lessThan_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
435 |
also have " ... = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> ((r2 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r3 ! i))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
436 |
by (metis DirProd_list_carrier_elts DirProd_list_in_carrierE assms i lessThan_iff monoid.m_assoc) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
437 |
also have " ... = (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3)) ! i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
438 |
by (metis DirProd_list_m_closed DirProd_list_m_output i assms lessThan_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
439 |
finally show "((r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r2) \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
440 |
(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> (r2 \<otimes>\<^bsub>DirProd_list Rs\<^esub> r3))! i" . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
441 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
442 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
443 |
lemma DirProd_list_one: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
444 |
"\<And>i. i < length Rs \<Longrightarrow> (\<one>\<^bsub>(DirProd_list Rs)\<^esub>) ! i = \<one>\<^bsub>(Rs ! i)\<^esub>" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
445 |
by (induct Rs rule: DirProd_list.induct) (simp_all add: nth_Cons') |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
446 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
447 |
lemma DirProd_list_one_closed: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
448 |
assumes "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
449 |
shows "\<one>\<^bsub>(DirProd_list Rs)\<^esub> \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
450 |
proof (rule DirProd_list_in_carrierI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
451 |
show eq_len: "length \<one>\<^bsub>DirProd_list Rs\<^esub> = length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
452 |
by (induct Rs rule: DirProd_list.induct) (simp_all) |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
453 |
show "\<And>i. i < length \<one>\<^bsub>DirProd_list Rs\<^esub> \<Longrightarrow> \<one>\<^bsub>DirProd_list Rs\<^esub> ! i \<in> carrier (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
454 |
using eq_len DirProd_list_one[where ?Rs = Rs] monoid.one_closed by (simp add: assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
455 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
456 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
457 |
lemma DirProd_list_l_one: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
458 |
assumes "r1 \<in> carrier (DirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
459 |
and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
460 |
shows "\<one>\<^bsub>(DirProd_list Rs)\<^esub> \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r1 = r1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
461 |
apply (rule nth_equalityI) apply auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
462 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
463 |
show eq_len: "length (\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) = length r1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
464 |
using DirProd_list_carrier_elts[of "\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1" Rs] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
465 |
DirProd_list_carrier_elts[OF assms(1)] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
466 |
DirProd_list_m_closed[OF DirProd_list_one_closed[OF assms(2)] assms(1)] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
467 |
by (simp add: assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
468 |
fix i assume "i < length (\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
469 |
hence i: "i < length Rs" using DirProd_list_carrier_elts[OF assms(1)] eq_len by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
470 |
hence "(\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
471 |
(\<one>\<^bsub>DirProd_list Rs\<^esub> ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r1 ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
472 |
using DirProd_list_m_output DirProd_list_one_closed assms by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
473 |
also have " ... = \<one>\<^bsub>(Rs ! i)\<^esub> \<otimes>\<^bsub>(Rs ! i)\<^esub> (r1 ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
474 |
by (simp add: DirProd_list_one i) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
475 |
also have " ... = (r1 ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
476 |
using DirProd_list_carrier_elts DirProd_list_in_carrierE i assms by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
477 |
finally show "(\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i = (r1 ! i)" . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
478 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
479 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
480 |
lemma DirProd_list_r_one: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
481 |
assumes "r1 \<in> carrier (DirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
482 |
and "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
483 |
shows "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> \<one>\<^bsub>(DirProd_list Rs)\<^esub> = r1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
484 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
485 |
have "r1 \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> \<one>\<^bsub>(DirProd_list Rs)\<^esub> = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
486 |
\<one>\<^bsub>(DirProd_list Rs)\<^esub> \<otimes>\<^bsub>(DirProd_list Rs)\<^esub> r1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
487 |
apply (rule nth_equalityI) apply auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
488 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
489 |
show " length (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> \<one>\<^bsub>DirProd_list Rs\<^esub>) = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
490 |
length (\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
491 |
by (metis DirProd_list_carrier_elts DirProd_list_m_closed DirProd_list_one_closed assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
492 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
493 |
fix i assume "i < length (r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> \<one>\<^bsub>DirProd_list Rs\<^esub>)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
494 |
hence i: "i < length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
495 |
by (metis DirProd_list_carrier_elts DirProd_list_m_closed DirProd_list_one_closed assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
496 |
hence "(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> \<one>\<^bsub>DirProd_list Rs\<^esub>) ! i = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> \<one>\<^bsub>(Rs ! i)\<^esub>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
497 |
by (metis DirProd_list_m_output DirProd_list_one DirProd_list_one_closed assms lessThan_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
498 |
also have " ... = \<one>\<^bsub>(Rs ! i)\<^esub> \<otimes>\<^bsub>(Rs ! i)\<^esub> (r1 ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
499 |
using DirProd_list_carrier_elts DirProd_list_in_carrierE assms i by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
500 |
also have " ... = (\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
501 |
by (metis DirProd_list_m_output DirProd_list_one DirProd_list_one_closed assms i lessThan_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
502 |
finally show "(r1 \<otimes>\<^bsub>DirProd_list Rs\<^esub> \<one>\<^bsub>DirProd_list Rs\<^esub>) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
503 |
(\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> r1) ! i" . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
504 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
505 |
thus ?thesis using DirProd_list_l_one assms by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
506 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
507 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
508 |
lemma DirProd_list_monoid: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
509 |
assumes "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
510 |
shows "monoid (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
511 |
unfolding monoid_def apply auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
512 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
513 |
show "\<one>\<^bsub>DirProd_list Rs\<^esub> \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
514 |
using DirProd_list_one_closed[of Rs] assms by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
515 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
516 |
fix x y z |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
517 |
assume x: "x \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
518 |
and y: "y \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
519 |
and z: "z \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
520 |
show "x \<otimes>\<^bsub>DirProd_list Rs\<^esub> y \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
521 |
using DirProd_list_m_closed[OF x y] assms by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
522 |
show "x \<otimes>\<^bsub>DirProd_list Rs\<^esub> y \<otimes>\<^bsub>DirProd_list Rs\<^esub> z = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
523 |
x \<otimes>\<^bsub>DirProd_list Rs\<^esub> (y \<otimes>\<^bsub>DirProd_list Rs\<^esub> z)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
524 |
using DirProd_list_m_assoc[OF x y z] assms by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
525 |
show "\<one>\<^bsub>DirProd_list Rs\<^esub> \<otimes>\<^bsub>DirProd_list Rs\<^esub> x = x" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
526 |
using DirProd_list_l_one[OF x] assms by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
527 |
show "x \<otimes>\<^bsub>DirProd_list Rs\<^esub> \<one>\<^bsub>DirProd_list Rs\<^esub> = x" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
528 |
using DirProd_list_r_one[OF x] assms by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
529 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
530 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
531 |
lemma DirProd_list_comm_monoid: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
532 |
assumes "\<And>i. i < length Rs \<Longrightarrow> comm_monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
533 |
shows "comm_monoid (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
534 |
unfolding comm_monoid_def comm_monoid_axioms_def apply auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
535 |
using DirProd_list_monoid Group.comm_monoid.axioms(1) assms apply blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
536 |
using DirProd_list_m_comm assms by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
537 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
538 |
lemma DirProd_list_isomorphism1: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
539 |
"(\<lambda>(hd, tl). hd # tl) \<in> iso (R \<times>\<times> (DirProd_list Rs)) (DirProd_list (R # Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
540 |
unfolding iso_def hom_def bij_betw_def inj_on_def by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
541 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
542 |
lemma DirProd_list_isomorphism2: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
543 |
"(\<lambda>r. (hd r, tl r)) \<in> iso (DirProd_list (R # Rs)) (R \<times>\<times> (DirProd_list Rs))" (is "?\<phi> \<in> ?A") |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
544 |
unfolding iso_def hom_def bij_betw_def inj_on_def apply auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
545 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
546 |
fix a b assume "a \<in> carrier R" "b \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
547 |
hence "a # b \<in> {r # rs |r rs. r \<in> carrier R \<and> rs \<in> carrier (DirProd_list Rs)} \<and> ?\<phi> (a # b) = (a, b)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
548 |
by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
549 |
thus "(a, b) \<in> ?\<phi> ` {r # rs |r rs. r \<in> carrier R \<and> rs \<in> carrier (DirProd_list Rs)}" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
550 |
by (metis (no_types, lifting) image_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
551 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
552 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
553 |
lemma DirProd_list_group: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
554 |
assumes "\<And>i. i < length Rs \<Longrightarrow> group (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
555 |
shows "group (DirProd_list Rs)" using assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
556 |
proof (induction Rs rule: DirProd_list.induct) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
557 |
case 1 thus ?case |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
558 |
unfolding group_def group_axioms_def Units_def monoid_def by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
559 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
560 |
case (2 R Rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
561 |
hence "group (DirProd_list Rs)" by force |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
562 |
moreover have "group R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
563 |
using "2.prems" by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
564 |
moreover have "monoid (DirProd_list (R # Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
565 |
using DirProd_list_monoid 2 group.is_monoid by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
566 |
moreover have "R \<times>\<times> DirProd_list Rs \<cong> DirProd_list (R # Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
567 |
unfolding is_iso_def using DirProd_list_isomorphism1 by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
568 |
ultimately show ?case |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
569 |
using group.iso_imp_group[of "R \<times>\<times> (DirProd_list Rs)" "DirProd_list (R # Rs)"] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
570 |
DirProd_group[of R "DirProd_list Rs"] by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
571 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
572 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
573 |
lemma DirProd_list_comm_group: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
574 |
assumes "\<And>i. i < length Rs \<Longrightarrow> comm_group (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
575 |
shows "comm_group (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
576 |
using assms unfolding comm_group_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
577 |
using DirProd_list_group DirProd_list_comm_monoid by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
578 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
579 |
lemma DirProd_list_group_hom: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
580 |
assumes "\<And>i. i \<in> {..<(length (R # Rs))} \<Longrightarrow> group ((R # Rs) ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
581 |
shows "group_hom (R \<times>\<times> DirProd_list Rs) (DirProd_list (R # Rs)) (\<lambda>(hd, tl). hd # tl)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
582 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
583 |
have "group R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
584 |
using assms by force |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
585 |
moreover have "group (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
586 |
using DirProd_list_group assms by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
587 |
ultimately |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
588 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
589 |
have "group (R \<times>\<times> DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
590 |
using DirProd_group[of R "DirProd_list Rs"] by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
591 |
moreover have "group (DirProd_list (R # Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
592 |
using DirProd_list_group assms by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
593 |
moreover have "(\<lambda>(x, y). x # y) \<in> hom (R \<times>\<times> DirProd_list Rs) (DirProd_list (R # Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
594 |
using DirProd_list_isomorphism1[of R Rs] unfolding iso_def by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
595 |
ultimately show ?thesis |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
596 |
unfolding group_hom_def group_hom_axioms_def by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
597 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
598 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
599 |
lemma DirProd_list_m_inv: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
600 |
assumes "r \<in> carrier (DirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
601 |
and "\<And>i. i < length Rs \<Longrightarrow> group (Rs ! i)" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
602 |
shows "\<And>i. i < length Rs \<Longrightarrow> (inv\<^bsub>(DirProd_list Rs)\<^esub> r) ! i = inv\<^bsub>(Rs ! i)\<^esub> (r ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
603 |
using assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
604 |
proof (induct Rs arbitrary: r rule: DirProd_list.induct) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
605 |
case 1 |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
606 |
have "group (DirProd_list [])" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
607 |
unfolding group_def group_axioms_def Units_def monoid_def by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
608 |
thus ?case using "1.prems"(1) group.inv_equality by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
609 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
610 |
case (2 R Rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
611 |
then obtain r' rs' where r': "r' \<in> carrier R" and rs': "rs' \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
612 |
and r: "r = r' # rs'" by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
613 |
hence "(r', rs') \<in> carrier (R \<times>\<times> DirProd_list Rs)" by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
614 |
moreover have "group_hom (R \<times>\<times> DirProd_list Rs) (DirProd_list (R # Rs)) (\<lambda>(hd, tl). hd # tl)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
615 |
using DirProd_list_group_hom[of R Rs] 2 by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
616 |
moreover have "inv\<^bsub>(R \<times>\<times> DirProd_list Rs)\<^esub> (r', rs') = (inv\<^bsub>R\<^esub> r', inv\<^bsub>(DirProd_list Rs)\<^esub> rs')" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
617 |
using inv_DirProd[of R "DirProd_list Rs" r' rs'] "2.prems"(3) DirProd_list_group r' rs' by force |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
618 |
ultimately have "inv\<^bsub>(DirProd_list (R # Rs))\<^esub> r = (inv\<^bsub>R\<^esub> r') # (inv\<^bsub>(DirProd_list Rs)\<^esub> rs')" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
619 |
using group_hom.hom_inv[of "R \<times>\<times> DirProd_list Rs" "DirProd_list (R # Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
620 |
"\<lambda>(hd, tl). hd # tl" "(r', rs')"] r by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
621 |
thus ?case |
68608
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
622 |
using 2 by simp (metis (no_types, lifting) less_Suc_eq_0_disj list.sel(3) nth_Cons_0 nth_Cons_Suc r) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
623 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
624 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
625 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
626 |
subsection \<open>Direct Product for of a List of Rings\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
627 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
628 |
text \<open>In order to state a more general version of the Chinese Remainder Theorem, we need a new |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
629 |
structure: the direct product of a variable number of rings. The construction of this |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
630 |
structure as well as its algebraic properties are the subject of this subsection and follow |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
631 |
the similar study that has already been done for monoids in the previous subsection.\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
632 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
633 |
fun RDirProd_list :: "('a ring) list \<Rightarrow> ('a list) ring" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
634 |
where "RDirProd_list Rs = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
635 |
monoid.extend (monoid.truncate (DirProd_list Rs)) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
636 |
\<lparr> zero = one (DirProd_list (map add_monoid Rs)), |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
637 |
add = mult (DirProd_list (map add_monoid Rs)) \<rparr>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
638 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
639 |
lemma RDirProd_list_add_monoid: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
640 |
"add_monoid (RDirProd_list Rs) = DirProd_list (map add_monoid Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
641 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
642 |
have "carrier (RDirProd_list Rs) = carrier (DirProd_list (map add_monoid Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
643 |
by (induct Rs rule: DirProd_list.induct) (simp_all add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
644 |
thus ?thesis by (simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
645 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
646 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
647 |
lemma RDirProd_list_mult_monoid: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
648 |
"monoid.truncate (RDirProd_list Rs) = monoid.truncate (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
649 |
by (simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
650 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
651 |
lemma RDirProd_list_monoid: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
652 |
assumes "\<And>i. i < length Rs \<Longrightarrow> monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
653 |
shows "monoid (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
654 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
655 |
have "monoid (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
656 |
using DirProd_list_monoid assms by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
657 |
hence "monoid (monoid.truncate (DirProd_list Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
658 |
unfolding monoid_def by (auto intro: monoid.intro simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
659 |
hence "monoid (monoid.truncate (RDirProd_list Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
660 |
by (simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
661 |
thus ?thesis |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
662 |
unfolding monoid_def by (auto intro: monoid.intro simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
663 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
664 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
665 |
lemma RDirProd_list_comm_monoid: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
666 |
assumes "\<And>i. i < length Rs \<Longrightarrow> comm_monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
667 |
shows "comm_monoid (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
668 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
669 |
have "comm_monoid (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
670 |
using DirProd_list_comm_monoid assms by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
671 |
hence "comm_monoid (monoid.truncate (DirProd_list Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
672 |
unfolding comm_monoid_def monoid_def comm_monoid_axioms_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
673 |
by (auto simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
674 |
hence "comm_monoid (monoid.truncate (RDirProd_list Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
675 |
by (simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
676 |
thus ?thesis |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
677 |
unfolding comm_monoid_def monoid_def comm_monoid_axioms_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
678 |
by (auto simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
679 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
680 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
681 |
lemma RDirProd_list_abelian_monoid: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
682 |
assumes "\<And>i. i < length Rs \<Longrightarrow> abelian_monoid (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
683 |
shows "abelian_monoid (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
684 |
proof - |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
685 |
have "\<And>i. i < length Rs \<Longrightarrow> comm_monoid ((map add_monoid Rs) ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
686 |
using assms unfolding abelian_monoid_def by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
687 |
hence "comm_monoid (DirProd_list (map add_monoid Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
688 |
by (metis (no_types, lifting) DirProd_list_comm_monoid length_map) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
689 |
thus ?thesis |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
690 |
unfolding abelian_monoid_def by (metis RDirProd_list_add_monoid) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
691 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
692 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
693 |
lemma RDirProd_list_abelian_group: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
694 |
assumes "\<And>i. i < length Rs \<Longrightarrow> abelian_group (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
695 |
shows "abelian_group (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
696 |
proof - |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
697 |
have "\<And>i. i < length Rs \<Longrightarrow> comm_group ((map add_monoid Rs) ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
698 |
using assms unfolding abelian_group_def abelian_group_axioms_def by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
699 |
hence "comm_group (DirProd_list (map add_monoid Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
700 |
by (metis (no_types, lifting) DirProd_list_comm_group length_map) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
701 |
thus ?thesis |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
702 |
unfolding abelian_group_def abelian_group_axioms_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
703 |
by (metis RDirProd_list_abelian_monoid RDirProd_list_add_monoid abelian_group_def assms) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
704 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
705 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
706 |
lemma RDirProd_list_carrier_elts: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
707 |
assumes "rs \<in> carrier (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
708 |
shows "length rs = length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
709 |
using assms by (simp add: DirProd_list_carrier_elts monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
710 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
711 |
lemma RDirProd_list_in_carrierE: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
712 |
assumes "rs \<in> carrier (RDirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
713 |
shows "\<And>i. i < length rs \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
714 |
using assms by (simp add: DirProd_list_in_carrierE monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
715 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
716 |
lemma RDirProd_list_in_carrierI: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
717 |
assumes "\<And>i. i < length rs \<Longrightarrow> rs ! i \<in> carrier (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
718 |
and "length rs = length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
719 |
shows "rs \<in> carrier (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
720 |
using DirProd_list_in_carrierI assms by (simp add: monoid.defs, blast) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
721 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
722 |
lemma RDirProd_list_one: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
723 |
"\<And>i. i < length Rs \<Longrightarrow> (\<one>\<^bsub>(RDirProd_list Rs)\<^esub>) ! i = \<one>\<^bsub>(Rs ! i)\<^esub>" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
724 |
by (simp add: DirProd_list_one monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
725 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
726 |
lemma RDirProd_list_zero: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
727 |
"\<And>i. i < length Rs \<Longrightarrow> (\<zero>\<^bsub>(RDirProd_list Rs)\<^esub>) ! i = \<zero>\<^bsub>(Rs ! i)\<^esub>" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
728 |
by (induct Rs rule: DirProd_list.induct) (simp_all add: monoid.defs nth_Cons') |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
729 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
730 |
lemma RDirProd_list_m_output: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
731 |
assumes "r1 \<in> carrier (RDirProd_list Rs)" "r2 \<in> carrier (RDirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
732 |
shows "\<And>i. i < length Rs \<Longrightarrow> |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
733 |
(r1 \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> r2) ! i = (r1 ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
734 |
using assms by (simp add: DirProd_list_m_output monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
735 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
736 |
lemma RDirProd_list_a_output: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
737 |
fixes i |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
738 |
assumes "r1 \<in> carrier (RDirProd_list Rs)" "r2 \<in> carrier (RDirProd_list Rs)" "i < length Rs" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
739 |
shows "(r1 \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> r2) ! i = (r1 ! i) \<oplus>\<^bsub>(Rs ! i)\<^esub> (r2 ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
740 |
using RDirProd_list_add_monoid[of Rs] monoid.defs(3) |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
741 |
proof - |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
742 |
have "(\<otimes>\<^bsub>DirProd_list (map add_monoid Rs)\<^esub>) = (\<oplus>\<^bsub>RDirProd_list Rs\<^esub>)" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
743 |
by (metis \<open>add_monoid (RDirProd_list Rs) = DirProd_list (map add_monoid Rs)\<close> monoid.select_convs(1)) |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
744 |
moreover have "r1 \<in> carrier (DirProd_list (map add_monoid Rs))" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
745 |
by (metis \<open>add_monoid (RDirProd_list Rs) = DirProd_list (map add_monoid Rs)\<close> assms(1) partial_object.select_convs(1)) |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
746 |
moreover have "r2 \<in> carrier (DirProd_list (map add_monoid Rs))" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
747 |
by (metis \<open>add_monoid (RDirProd_list Rs) = DirProd_list (map add_monoid Rs)\<close> assms(2) partial_object.select_convs(1)) |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
748 |
ultimately show ?thesis |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
749 |
by (simp add: DirProd_list_m_output assms(3)) |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
750 |
qed |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
751 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
752 |
lemma RDirProd_list_a_inv: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
753 |
fixes i |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
754 |
assumes "r \<in> carrier (RDirProd_list Rs)" |
68608
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
755 |
and "\<And>i. i < length Rs \<Longrightarrow> abelian_group (Rs ! i)" |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
756 |
and i: "i < length Rs" |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
757 |
shows "(\<ominus>\<^bsub>(RDirProd_list Rs)\<^esub> r) ! i = \<ominus>\<^bsub>(Rs ! i)\<^esub> (r ! i)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
758 |
proof - |
68608
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
759 |
have "m_inv (DirProd_list (map add_monoid Rs)) = a_inv (RDirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
760 |
by (metis RDirProd_list_add_monoid a_inv_def) |
68608
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
761 |
moreover have "r \<in> carrier (DirProd_list (map add_monoid Rs))" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
762 |
by (metis RDirProd_list_add_monoid assms(1) partial_object.select_convs(1)) |
68608
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
763 |
moreover have "a_inv (Rs ! i) = m_inv (map add_monoid Rs ! i)" |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
764 |
by (simp add: a_inv_def i) |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
765 |
ultimately show ?thesis |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
766 |
by (metis (no_types, lifting) DirProd_list_carrier_elts DirProd_list_m_inv RDirProd_list_carrier_elts |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
767 |
abelian_group.a_group assms list_update_same_conv map_update) |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
768 |
qed |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
769 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
770 |
lemma RDirProd_list_l_distr: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
771 |
assumes "x \<in> carrier (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
772 |
and "y \<in> carrier (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
773 |
and "z \<in> carrier (RDirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
774 |
and "\<And>i. i < length Rs \<Longrightarrow> ring (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
775 |
shows "(x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y) \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
776 |
(x \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (y \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
777 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
778 |
have "length ((x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y) \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
779 |
length ((x \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (y \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
780 |
by (metis RDirProd_list_abelian_group RDirProd_list_carrier_elts RDirProd_list_monoid |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
781 |
abelian_groupE(1) assms monoid.m_closed ring.is_abelian_group ring.is_monoid) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
782 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
783 |
moreover |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
784 |
have "\<And>i. i < length Rs \<Longrightarrow> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
785 |
((x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y) \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
786 |
((x \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (y \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z)) ! i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
787 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
788 |
fix i assume i: "i < length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
789 |
hence "((x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y) \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
790 |
((x ! i) \<oplus>\<^bsub>(Rs ! i)\<^esub> (y ! i)) \<otimes>\<^bsub>(Rs ! i)\<^esub> (z ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
791 |
using RDirProd_list_m_output RDirProd_list_a_output assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
792 |
by (metis RDirProd_list_abelian_group abelian_groupE(1) lessThan_iff ring.is_abelian_group) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
793 |
also have " ... = ((x ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (z ! i)) \<oplus>\<^bsub>(Rs ! i)\<^esub> ((y ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (z ! i))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
794 |
by (metis RDirProd_list_carrier_elts RDirProd_list_in_carrierE |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
795 |
i assms lessThan_iff ring.ring_simprules(13)) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
796 |
also |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
797 |
have " ... = ((x \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (y \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z)) ! i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
798 |
using RDirProd_list_m_output RDirProd_list_a_output assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
799 |
by (metis RDirProd_list_monoid i lessThan_iff monoid.m_closed ring.is_monoid) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
800 |
finally |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
801 |
show "((x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y) \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
802 |
((x \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (y \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z)) ! i" . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
803 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
804 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
805 |
moreover have "length ((x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y) \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> z) = length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
806 |
by (meson RDirProd_list_abelian_group RDirProd_list_carrier_elts RDirProd_list_monoid |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
807 |
abelian_groupE(1) assms monoid.m_closed ring.is_abelian_group ring.is_monoid) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
808 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
809 |
ultimately show ?thesis by (simp add: nth_equalityI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
810 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
811 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
812 |
lemma RDirProd_list_r_distr: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
813 |
assumes "x \<in> carrier (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
814 |
and "y \<in> carrier (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
815 |
and "z \<in> carrier (RDirProd_list Rs)" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
816 |
and "\<And>i. i < length Rs \<Longrightarrow> ring (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
817 |
shows "z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> (x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y) = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
818 |
(z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> x) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> y)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
819 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
820 |
have "length (z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> (x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y)) = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
821 |
length ((z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> x) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> y))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
822 |
by (metis RDirProd_list_abelian_group RDirProd_list_carrier_elts RDirProd_list_monoid |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
823 |
abelian_groupE(1) assms monoid.m_closed ring.is_abelian_group ring.is_monoid) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
824 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
825 |
moreover |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
826 |
have "\<And>i. i < length Rs \<Longrightarrow> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
827 |
(z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> (x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y)) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
828 |
((z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> x) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> y)) ! i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
829 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
830 |
fix i assume i: "i < length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
831 |
hence "(z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> (x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y)) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
832 |
(z ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> ((x ! i) \<oplus>\<^bsub>(Rs ! i)\<^esub> (y ! i))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
833 |
using RDirProd_list_m_output RDirProd_list_a_output assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
834 |
by (metis RDirProd_list_abelian_group abelian_groupE(1) lessThan_iff ring.is_abelian_group) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
835 |
also have " ... = ((z ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (x ! i)) \<oplus>\<^bsub>(Rs ! i)\<^esub> ((z ! i) \<otimes>\<^bsub>(Rs ! i)\<^esub> (y ! i))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
836 |
by (metis RDirProd_list_carrier_elts RDirProd_list_in_carrierE |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
837 |
assms i lessThan_iff ring.ring_simprules(23)) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
838 |
also |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
839 |
have " ... = ((z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> x) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> y)) ! i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
840 |
using RDirProd_list_m_output RDirProd_list_a_output assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
841 |
by (metis RDirProd_list_monoid i lessThan_iff monoid.m_closed ring.is_monoid) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
842 |
finally |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
843 |
show "(z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> (x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y)) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
844 |
((z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> x) \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> (z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> y)) ! i" . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
845 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
846 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
847 |
moreover have "length (z \<otimes>\<^bsub>(RDirProd_list Rs)\<^esub> (x \<oplus>\<^bsub>(RDirProd_list Rs)\<^esub> y)) = length Rs" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
848 |
by (meson RDirProd_list_abelian_group RDirProd_list_carrier_elts RDirProd_list_monoid |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
849 |
abelian_groupE(1) assms monoid.m_closed ring.is_abelian_group ring.is_monoid) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
850 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
851 |
ultimately show ?thesis by (simp add: nth_equalityI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
852 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
853 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
854 |
theorem RDirProd_list_ring: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
855 |
assumes "\<And>i. i < length Rs \<Longrightarrow> ring (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
856 |
shows "ring (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
857 |
using assms unfolding ring_def ring_axioms_def using assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
858 |
by (meson RDirProd_list_abelian_group RDirProd_list_l_distr |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
859 |
RDirProd_list_monoid RDirProd_list_r_distr) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
860 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
861 |
theorem RDirProd_list_cring: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
862 |
assumes "\<And>i. i < length Rs \<Longrightarrow> cring (Rs ! i)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
863 |
shows "cring (RDirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
864 |
by (meson RDirProd_list_comm_monoid RDirProd_list_ring assms cring_def) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
865 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
866 |
corollary (in cring) RDirProd_list_of_quot_is_cring: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
867 |
assumes "\<And>i. i < n \<Longrightarrow> ideal (I i) R" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
868 |
shows "cring (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< n]))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
869 |
(is "cring (RDirProd_list ?Rs)") |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
870 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
871 |
have "\<And>i. i \<in> {..<(length ?Rs)} \<Longrightarrow> cring (?Rs ! i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
872 |
by (simp add: assms ideal.quotient_is_cring is_cring) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
873 |
thus ?thesis |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
874 |
using RDirProd_list_cring by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
875 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
876 |
|
68608
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
877 |
lemma length_RDirProd_list_0: |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
878 |
assumes "\<And>i. i < n \<Longrightarrow> cring (F i)" |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
879 |
shows "length (\<zero>\<^bsub>(RDirProd_list (map F [0..< n]))\<^esub>) = n" |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
880 |
by (metis (no_types, lifting) add_cancel_right_left RDirProd_list_carrier_elts RDirProd_list_cring cring.cring_simprules(2) diff_zero length_map length_upt nth_map_upt assms) |
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
881 |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
882 |
lemma RDirProd_list_isomorphism1: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
883 |
"(\<lambda>(hd, tl). hd # tl) \<in> ring_iso (RDirProd R (RDirProd_list Rs)) (RDirProd_list (R # Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
884 |
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def RDirProd_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
885 |
by (auto simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
886 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
887 |
lemma RDirProd_list_isomorphism1': |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
888 |
"(RDirProd R (RDirProd_list Rs)) \<simeq> (RDirProd_list (R # Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
889 |
unfolding is_ring_iso_def using RDirProd_list_isomorphism1 by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
890 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
891 |
lemma RDirProd_list_isomorphism2: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
892 |
"(\<lambda>r. (hd r, tl r)) \<in> ring_iso (RDirProd_list (R # Rs)) (RDirProd R (RDirProd_list Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
893 |
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def RDirProd_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
894 |
proof (auto simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
895 |
let ?\<phi> = "\<lambda>r. (hd r, tl r)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
896 |
fix a b assume "a \<in> carrier R" "b \<in> carrier (DirProd_list Rs)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
897 |
hence "a # b \<in> {r # rs |r rs. r \<in> carrier R \<and> rs \<in> carrier (DirProd_list Rs)} \<and> ?\<phi> (a # b) = (a, b)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
898 |
by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
899 |
thus "(a, b) \<in> ?\<phi> ` {r # rs |r rs. r \<in> carrier R \<and> rs \<in> carrier (DirProd_list Rs)}" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
900 |
by (metis (no_types, lifting) image_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
901 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
902 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
903 |
lemma RDirProd_list_isomorphism3: |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
904 |
"(\<lambda>(r, l). r @ [l]) \<in> ring_iso (RDirProd (RDirProd_list Rs) S) (RDirProd_list (Rs @ [S]))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
905 |
proof (induction Rs rule: DirProd_list.induct) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
906 |
case 1 thus ?case |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
907 |
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def RDirProd_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
908 |
by (auto simp add: monoid.defs image_iff) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
909 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
910 |
case (2 R Rs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
911 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
912 |
{ fix r1 r2 assume A0: "r1 \<in> carrier (RDirProd_list (R # Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
913 |
and A1: "r2 \<in> carrier (RDirProd_list (R # Rs))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
914 |
have "length r1 \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
915 |
and "length r2 \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
916 |
and "length (r1 \<otimes>\<^bsub>(RDirProd_list (R # Rs))\<^esub> r2) \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
917 |
and "length (r1 \<oplus>\<^bsub>(RDirProd_list (R # Rs))\<^esub> r2) \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
918 |
and "length (\<one>\<^bsub>(RDirProd_list (R # Rs))\<^esub>) \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
919 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
920 |
show len_r1: "length r1 \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
921 |
and len_r2: "length r2 \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
922 |
by (metis RDirProd_list_carrier_elts A0 A1 length_Cons less_one nat.simps(3) not_less)+ |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
923 |
show "length (r1 \<otimes>\<^bsub>(RDirProd_list (R # Rs))\<^esub> r2) \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
924 |
and "length (r1 \<oplus>\<^bsub>(RDirProd_list (R # Rs))\<^esub> r2) \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
925 |
and "length (\<one>\<^bsub>(RDirProd_list (R # Rs))\<^esub>) \<ge> 1" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
926 |
using len_r1 len_r2 by (simp_all add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
927 |
qed } note aux_lemma = this |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
928 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
929 |
moreover |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
930 |
have "(\<lambda>(r, s). (hd r, (tl r, s))) \<in> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
931 |
ring_iso (RDirProd (RDirProd_list (R # Rs)) S) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
932 |
(RDirProd R (RDirProd (RDirProd_list Rs) S))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
933 |
using ring_iso_set_trans[OF RDirProd_isomorphism4[OF RDirProd_list_isomorphism2[of R Rs],of S] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
934 |
RDirProd_isomorphism3[of R "RDirProd_list Rs" S]] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
935 |
by (simp add: case_prod_beta' comp_def) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
936 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
937 |
moreover |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
938 |
have "(\<lambda>(hd, (tl, s)). hd # (tl @ [s])) \<in> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
939 |
ring_iso (RDirProd R (RDirProd (RDirProd_list Rs) S)) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
940 |
(RDirProd_list (R # (Rs @ [S])))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
941 |
using ring_iso_set_trans[OF RDirProd_isomorphism5[OF 2(1), of R] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
942 |
RDirProd_list_isomorphism1[of R "Rs @ [S]"]] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
943 |
by (simp add: case_prod_beta' comp_def) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
944 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
945 |
moreover |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
946 |
have "(\<lambda>(r, s). (hd r) # ((tl r) @ [s])) \<in> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
947 |
ring_iso (RDirProd (RDirProd_list (R # Rs)) S) (RDirProd_list (R # (Rs @ [S])))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
948 |
using ring_iso_set_trans[OF calculation(6-7)] by (simp add: case_prod_beta' comp_def) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
949 |
hence iso: "(\<lambda>(r, s). (hd r # tl r) @ [s]) \<in> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
950 |
ring_iso (RDirProd (RDirProd_list (R # Rs)) S) (RDirProd_list ((R # Rs) @ [S]))" by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
951 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
952 |
show ?case |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
953 |
proof (rule ring_iso_morphic_prop[OF iso, of "\<lambda>r. length (fst r) \<ge> 1" "\<lambda>(r, s). r @ [s]"]) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
954 |
show "\<And>r. 1 \<le> length (fst r) \<Longrightarrow> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
955 |
(case r of (r, s) \<Rightarrow> (hd r # tl r) @ [s]) = (case r of (r, s) \<Rightarrow> r @ [s])" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
956 |
by (simp add: Suc_le_eq case_prod_beta') |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
957 |
show "morphic_prop (RDirProd (RDirProd_list (R # Rs)) S) (\<lambda>r. 1 \<le> length (fst r))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
958 |
unfolding RDirProd_def by (rule morphic_propI) (auto simp add: monoid.defs aux_lemma) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
959 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
960 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
961 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
962 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
963 |
subsection \<open>Second Generalization - The Extended Canonical Projection is a Homomorphism and |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
964 |
Description of its Kernel\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
965 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
966 |
theorem (in cring) canonical_proj_ext_is_hom: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
967 |
fixes n::nat |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
968 |
assumes "\<And>i. i < n \<Longrightarrow> ideal (I i) R" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
969 |
and "\<And>i j. \<lbrakk> i < n; j < n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
970 |
shows "(\<lambda>a. (map (\<lambda>i. (I i) +> a) [0..< n])) \<in> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
971 |
ring_hom R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< n]))" (is "?\<phi> \<in> ?ring_hom") |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
972 |
proof (rule ring_hom_memI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
973 |
{ fix x assume x: "x \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
974 |
have "?\<phi> x \<in> carrier (RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n]))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
975 |
apply (rule RDirProd_list_in_carrierI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
976 |
by (simp_all add: FactRing_def a_rcosetsI additive_subgroup.a_subset assms(1) ideal.axioms(1) x) } |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
977 |
note aux_lemma = this |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
978 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
979 |
fix x y assume x: "x \<in> carrier R" and y: "y \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
980 |
show x': "?\<phi> x \<in> carrier (RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n]))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
981 |
using aux_lemma[OF x] . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
982 |
hence x'': "?\<phi> x \<in> carrier (DirProd_list (map (\<lambda>i. R Quot I i) [0..<n]))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
983 |
by (simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
984 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
985 |
have y': "?\<phi> y \<in> carrier (RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n]))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
986 |
using aux_lemma[OF y] . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
987 |
hence y'': "map (\<lambda>i. I i +> y) [0..<n] \<in> carrier (DirProd_list (map (\<lambda>i. R Quot I i) [0..<n]))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
988 |
by (simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
989 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
990 |
show "?\<phi> (x \<otimes> y) = ?\<phi> x \<otimes>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> ?\<phi> y" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
991 |
apply (rule nth_equalityI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
992 |
apply (metis RDirProd_list_carrier_elts RDirProd_list_of_quot_is_cring assms(1) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
993 |
cring.cring_simprules(5) length_map x' y') |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
994 |
apply (simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
995 |
using DirProd_list_m_output [of "?\<phi> x" "(map (\<lambda>i. R Quot I i) [0..<n])" "?\<phi> y"] x'' y'' |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
996 |
by (simp add: x'' y'' FactRing_def assms(1) ideal.rcoset_mult_add x y) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
997 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
998 |
show "?\<phi> (x \<oplus> y) = ?\<phi> x \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> ?\<phi> y" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
999 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1000 |
have "length (?\<phi> (x \<oplus> y)) = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1001 |
length ((?\<phi> x) \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> (?\<phi> y))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1002 |
by (metis RDirProd_list_carrier_elts RDirProd_list_of_quot_is_cring assms(1) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1003 |
cring.cring_simprules(1) length_map x' y') |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1004 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1005 |
moreover |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1006 |
have "\<And>j. j < n \<Longrightarrow> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1007 |
(?\<phi> (x \<oplus> y)) ! j = ((?\<phi> x) \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> (?\<phi> y)) ! j" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1008 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1009 |
fix j assume j: "j < n" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1010 |
have "(?\<phi> (x \<oplus> y)) ! j = I j +> x \<oplus> y" using j by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1011 |
also have " ... = (I j +> x) \<oplus>\<^bsub>(R Quot I j)\<^esub> (I j +> y)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1012 |
by (simp add: FactRing_def abelian_subgroup.a_rcos_sum abelian_subgroupI3 |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1013 |
assms(1) ideal.axioms(1) is_abelian_group j x y) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1014 |
also have " ... = ((?\<phi> x) \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> (?\<phi> y)) ! j" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1015 |
proof - |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1016 |
have "R Quot I j = map (\<lambda>n. R Quot I n) [0..<n] ! j" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1017 |
"I j +> x = I ([0..<n] ! j) +> x" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1018 |
"I j +> y = I ([0..<n] ! j) +> y" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1019 |
by (simp_all add: j) |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1020 |
moreover have "\<And>n ns f. n < length ns \<Longrightarrow> map f ns ! n = (f (ns ! n::nat)::'a set)" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1021 |
by simp |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1022 |
moreover have "\<And>B ps C n. \<lbrakk>B \<in> carrier (RDirProd_list ps); C \<in> carrier (RDirProd_list ps); n < length ps\<rbrakk> |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1023 |
\<Longrightarrow> (B \<oplus>\<^bsub>RDirProd_list ps\<^esub> C) ! n = (B ! n::'a set) \<oplus>\<^bsub>ps ! n\<^esub> C ! n" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1024 |
by (meson RDirProd_list_a_output) |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1025 |
ultimately show ?thesis |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1026 |
by (metis (mono_tags, lifting) diff_zero j length_map length_upt x' y') |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1027 |
qed |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1028 |
finally show "(?\<phi> (x \<oplus> y)) ! j = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1029 |
((?\<phi> x) \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> (?\<phi> y)) ! j" . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1030 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1031 |
ultimately show "?\<phi> (x \<oplus> y) = ?\<phi> x \<oplus>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub> ?\<phi> y" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1032 |
by (simp add: nth_equalityI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1033 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1034 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1035 |
show "(?\<phi> \<one>) = \<one>\<^bsub>RDirProd_list (map (\<lambda>i. R Quot I i) [0..<n])\<^esub>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1036 |
apply (rule nth_equalityI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1037 |
apply (metis RDirProd_list_carrier_elts cring.cring_simprules(6) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1038 |
RDirProd_list_of_quot_is_cring assms(1) length_map) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1039 |
using DirProd_list_one[where ?Rs = "map (\<lambda>i. R Quot I i) [0..<n]"] |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1040 |
by (simp add: FactRing_def monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1041 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1042 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1043 |
theorem (in cring) canonical_proj_ext_kernel: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1044 |
fixes n::nat |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1045 |
assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1046 |
and "\<And>i j. \<lbrakk> i \<le> n; j \<le> n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1047 |
shows "(\<Inter>i \<le> n. I i) = a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1048 |
(\<lambda>a. (map (\<lambda>i. (I i) +> a) [0..< Suc n]))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1049 |
proof - |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1050 |
let ?\<phi> = "\<lambda>a. (map (\<lambda>i. (I i) +> a) [0..< Suc n])" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1051 |
show ?thesis |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1052 |
proof |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1053 |
show "(\<Inter>i \<le> n. I i) \<subseteq> a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) ?\<phi>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1054 |
proof |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1055 |
fix s assume s: "s \<in> (\<Inter>i \<le> n. I i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1056 |
hence "\<And>i. i \<le> n \<Longrightarrow> (I i) +> s = I i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1057 |
by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1) ideal.set_add_zero) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1058 |
hence "\<And>i. i \<le> n \<Longrightarrow> (?\<phi> s) ! i = I i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1059 |
by (metis add.left_neutral diff_zero le_imp_less_Suc nth_map_upt) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1060 |
moreover have |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1061 |
"\<And>i. i \<le> n \<Longrightarrow> (\<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>) ! i = |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1062 |
\<zero>\<^bsub>(R Quot (I i))\<^esub>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1063 |
using RDirProd_list_zero[where ?Rs = "map (\<lambda>i. R Quot I i) [0..<Suc n]"] |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1064 |
by (metis (no_types, lifting) add.left_neutral le_imp_less_Suc |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1065 |
length_map length_upt nth_map_upt diff_zero) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1066 |
hence |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1067 |
"\<And>i. i \<le> n \<Longrightarrow> (\<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>) ! i = I i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1068 |
unfolding FactRing_def by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1069 |
moreover |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1070 |
have "length (\<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>) = Suc n" |
68608
4a4c2bc4b869
final removal of smt from Algebra
paulson <lp15@cam.ac.uk>
parents:
68606
diff
changeset
|
1071 |
by (subst length_RDirProd_list_0) (simp_all add: length_RDirProd_list_0 assms(1) ideal.quotient_is_cring is_cring) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1072 |
moreover have "length (?\<phi> s) = Suc n" by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1073 |
ultimately have "?\<phi> s = \<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1074 |
by (simp add: nth_equalityI) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1075 |
moreover have "s \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1076 |
using additive_subgroup.a_Hcarr assms(1) ideal.axioms(1) s by fastforce |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1077 |
ultimately show "s \<in> a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) ?\<phi>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1078 |
using a_kernel_def'[of R "RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])"] by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1079 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1080 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1081 |
show "a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) ?\<phi> \<subseteq> (\<Inter>i \<le> n. I i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1082 |
proof |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1083 |
fix s assume s: "s \<in> a_kernel R (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) ?\<phi>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1084 |
hence "?\<phi> s = \<zero>\<^bsub>(RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n]))\<^esub>" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1085 |
unfolding a_kernel_def kernel_def by (simp add: monoid.defs) |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1086 |
hence "(I i) +> s = \<zero>\<^bsub>(R Quot (I i))\<^esub>" if "i \<le> n" for i |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1087 |
using RDirProd_list_zero[where ?Rs = "map (\<lambda>i. R Quot I i) [0..<Suc n]"] |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1088 |
by (metis (no_types) that add.left_neutral diff_zero le_imp_less_Suc length_map length_upt nth_map_upt) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1089 |
hence "\<And>i. i \<le> n \<Longrightarrow> (I i) +> s = I i" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1090 |
unfolding FactRing_def by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1091 |
moreover have "s \<in> carrier R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1092 |
using s unfolding a_kernel_def kernel_def by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1093 |
ultimately show "s \<in> (\<Inter>i \<le> n. I i)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1094 |
using ideal.set_add_zero_imp_mem[where ?i = s and ?R = R] by (simp add: assms(1)) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1095 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1096 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1097 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1098 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1099 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1100 |
subsection \<open>Final Generalization\<close> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1101 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1102 |
theorem (in cring) chinese_remainder: |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1103 |
fixes n::nat |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1104 |
assumes "\<And>i. i \<le> n \<Longrightarrow> ideal (I i) R" |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1105 |
and "\<And>i j. \<lbrakk> i \<le> n; j \<le> n; i \<noteq> j \<rbrakk> \<Longrightarrow> I i <+> I j = carrier R" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1106 |
shows "R Quot (\<Inter>i \<le> n. I i) \<simeq> RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1107 |
using assms |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1108 |
proof (induct n) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1109 |
case 0 |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1110 |
have "(\<lambda>r. (r, [])) \<in> ring_iso (R Quot (I 0)) (RDirProd (R Quot (I 0)) (RDirProd_list []))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1111 |
unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def RDirProd_def |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1112 |
by (auto simp add: monoid.defs) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1113 |
hence "(R Quot (I 0)) \<simeq> (RDirProd (R Quot (I 0)) (RDirProd_list []))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1114 |
unfolding is_ring_iso_def by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1115 |
moreover |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1116 |
have "RDirProd ((R Quot (I 0)) :: 'a set ring) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1117 |
(RDirProd_list ([] :: (('a set) ring) list)) \<simeq> (RDirProd_list [ (R Quot (I 0)) ])" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1118 |
using RDirProd_list_isomorphism1'[of "(R Quot (I 0)) :: 'a set ring" "[] :: (('a set) ring) list"] . |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1119 |
ultimately show ?case |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1120 |
using ring_iso_trans by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1121 |
next |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1122 |
case (Suc n) |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1123 |
have inter_ideal: "ideal (\<Inter> i \<le> n. I i) R" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1124 |
using Suc.prems(1) i_Intersect[of "I ` {..n}"] atMost_Suc atLeast1_atMost_eq_remove0 by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1125 |
hence "R Quot (\<Inter> i \<le> Suc n. I i) \<simeq> RDirProd (R Quot (\<Inter> i \<le> n. I i)) (R Quot (I (Suc n)))" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1126 |
using chinese_remainder_simple[of "\<Inter> i \<le> n. I i" "I (Suc n)"] inter_plus_ideal_eq_carrier[of n I] |
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
68582
diff
changeset
|
1127 |
by (simp add: Int_commute Suc.prems(1-2) atMost_Suc) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1128 |
moreover have "R Quot (\<Inter> i \<le> n. I i) \<simeq> RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1129 |
using Suc.hyps Suc.prems(1-2) by auto |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1130 |
hence "RDirProd (R Quot (\<Inter> i \<le> n. I i)) (R Quot (I (Suc n))) \<simeq> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1131 |
RDirProd (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (R Quot (I (Suc n)))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1132 |
unfolding is_ring_iso_def using RDirProd_isomorphism4 by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1133 |
ultimately |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1134 |
have "R Quot (\<Inter> i \<le> Suc n. I i) \<simeq> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1135 |
RDirProd (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (R Quot (I (Suc n)))" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1136 |
using ring_iso_trans by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1137 |
moreover |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1138 |
have "RDirProd (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (R Quot (I (Suc n))) \<simeq> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1139 |
RDirProd_list ((map (\<lambda>i. R Quot (I i)) [0..< Suc n]) @ [ R Quot (I (Suc n)) ])" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1140 |
using RDirProd_list_isomorphism3 unfolding is_ring_iso_def by blast |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1141 |
hence "RDirProd (RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc n])) (R Quot (I (Suc n))) \<simeq> |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1142 |
RDirProd_list (map (\<lambda>i. R Quot (I i)) [0..< Suc (Suc n)])" by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1143 |
ultimately show ?case using ring_iso_trans by simp |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1144 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1145 |
|
68582 | 1146 |
end |