|
1 (* Title: HOL/Computational_Algebra/Field_as_Ring.thy |
|
2 Author: Johannes Hoelzl, TU Muenchen |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 *) |
|
5 |
|
6 theory Group_Closure |
|
7 imports |
|
8 Main |
|
9 begin |
|
10 |
|
11 context ab_group_add |
|
12 begin |
|
13 |
|
14 inductive_set group_closure :: "'a set \<Rightarrow> 'a set" for S |
|
15 where base: "s \<in> insert 0 S \<Longrightarrow> s \<in> group_closure S" |
|
16 | diff: "s \<in> group_closure S \<Longrightarrow> t \<in> group_closure S \<Longrightarrow> s - t \<in> group_closure S" |
|
17 |
|
18 lemma zero_in_group_closure [simp]: |
|
19 "0 \<in> group_closure S" |
|
20 using group_closure.base [of 0 S] by simp |
|
21 |
|
22 lemma group_closure_minus_iff [simp]: |
|
23 "- s \<in> group_closure S \<longleftrightarrow> s \<in> group_closure S" |
|
24 using group_closure.diff [of 0 S s] group_closure.diff [of 0 S "- s"] by auto |
|
25 |
|
26 lemma group_closure_add: |
|
27 "s + t \<in> group_closure S" if "s \<in> group_closure S" and "t \<in> group_closure S" |
|
28 using that group_closure.diff [of s S "- t"] by auto |
|
29 |
|
30 lemma group_closure_empty [simp]: |
|
31 "group_closure {} = {0}" |
|
32 by (rule ccontr) (auto elim: group_closure.induct) |
|
33 |
|
34 lemma group_closure_insert_zero [simp]: |
|
35 "group_closure (insert 0 S) = group_closure S" |
|
36 by (auto elim: group_closure.induct intro: group_closure.intros) |
|
37 |
|
38 end |
|
39 |
|
40 context comm_ring_1 |
|
41 begin |
|
42 |
|
43 lemma group_closure_scalar_mult_left: |
|
44 "of_nat n * s \<in> group_closure S" if "s \<in> group_closure S" |
|
45 using that by (induction n) (auto simp add: algebra_simps intro: group_closure_add) |
|
46 |
|
47 lemma group_closure_scalar_mult_right: |
|
48 "s * of_nat n \<in> group_closure S" if "s \<in> group_closure S" |
|
49 using that group_closure_scalar_mult_left [of s S n] by (simp add: ac_simps) |
|
50 |
|
51 end |
|
52 |
|
53 lemma group_closure_abs_iff [simp]: |
|
54 "\<bar>s\<bar> \<in> group_closure S \<longleftrightarrow> s \<in> group_closure S" for s :: int |
|
55 by (simp add: abs_if) |
|
56 |
|
57 lemma group_closure_mult_left: |
|
58 "s * t \<in> group_closure S" if "s \<in> group_closure S" for s t :: int |
|
59 proof - |
|
60 from that group_closure_scalar_mult_right [of s S "nat \<bar>t\<bar>"] |
|
61 have "s * int (nat \<bar>t\<bar>) \<in> group_closure S" |
|
62 by (simp only:) |
|
63 then show ?thesis |
|
64 by (cases "t \<ge> 0") simp_all |
|
65 qed |
|
66 |
|
67 lemma group_closure_mult_right: |
|
68 "s * t \<in> group_closure S" if "t \<in> group_closure S" for s t :: int |
|
69 using that group_closure_mult_left [of t S s] by (simp add: ac_simps) |
|
70 |
|
71 context idom |
|
72 begin |
|
73 |
|
74 lemma group_closure_mult_all_eq: |
|
75 "group_closure (times k ` S) = times k ` group_closure S" |
|
76 proof (rule; rule) |
|
77 fix s |
|
78 have *: "k * a + k * b = k * (a + b)" |
|
79 "k * a - k * b = k * (a - b)" for a b |
|
80 by (simp_all add: algebra_simps) |
|
81 assume "s \<in> group_closure (times k ` S)" |
|
82 then show "s \<in> times k ` group_closure S" |
|
83 by induction (auto simp add: * image_iff intro: group_closure.base group_closure.diff bexI [of _ 0]) |
|
84 next |
|
85 fix s |
|
86 assume "s \<in> times k ` group_closure S" |
|
87 then obtain r where r: "r \<in> group_closure S" and s: "s = k * r" |
|
88 by auto |
|
89 from r have "k * r \<in> group_closure (times k ` S)" |
|
90 by (induction arbitrary: s) (auto simp add: algebra_simps intro: group_closure.intros) |
|
91 with s show "s \<in> group_closure (times k ` S)" |
|
92 by simp |
|
93 qed |
|
94 |
|
95 end |
|
96 |
|
97 lemma Gcd_group_closure_eq_Gcd: |
|
98 "Gcd (group_closure S) = Gcd S" for S :: "int set" |
|
99 proof (rule associated_eqI) |
|
100 have "Gcd S dvd s" if "s \<in> group_closure S" for s |
|
101 using that by induction auto |
|
102 then show "Gcd S dvd Gcd (group_closure S)" |
|
103 by auto |
|
104 have "Gcd (group_closure S) dvd s" if "s \<in> S" for s |
|
105 proof - |
|
106 from that have "s \<in> group_closure S" |
|
107 by (simp add: group_closure.base) |
|
108 then show ?thesis |
|
109 by (rule Gcd_dvd) |
|
110 qed |
|
111 then show "Gcd (group_closure S) dvd Gcd S" |
|
112 by auto |
|
113 qed simp_all |
|
114 |
|
115 lemma group_closure_sum: |
|
116 fixes S :: "int set" |
|
117 assumes X: "finite X" "X \<noteq> {}" "X \<subseteq> S" |
|
118 shows "(\<Sum>x\<in>X. a x * x) \<in> group_closure S" |
|
119 using X by (induction X rule: finite_ne_induct) |
|
120 (auto intro: group_closure_mult_right group_closure.base group_closure_add) |
|
121 |
|
122 lemma Gcd_group_closure_in_group_closure: |
|
123 "Gcd (group_closure S) \<in> group_closure S" for S :: "int set" |
|
124 proof (cases "S \<subseteq> {0}") |
|
125 case True |
|
126 then have "S = {} \<or> S = {0}" |
|
127 by auto |
|
128 then show ?thesis |
|
129 by auto |
|
130 next |
|
131 case False |
|
132 then obtain s where s: "s \<noteq> 0" "s \<in> S" |
|
133 by auto |
|
134 then have s': "\<bar>s\<bar> \<noteq> 0" "\<bar>s\<bar> \<in> group_closure S" |
|
135 by (auto intro: group_closure.base) |
|
136 define m where "m = (LEAST n. n > 0 \<and> int n \<in> group_closure S)" |
|
137 have "m > 0 \<and> int m \<in> group_closure S" |
|
138 unfolding m_def |
|
139 apply (rule LeastI [of _ "nat \<bar>s\<bar>"]) |
|
140 using s' |
|
141 by simp |
|
142 then have m: "int m \<in> group_closure S" and "0 < m" |
|
143 by auto |
|
144 |
|
145 have "Gcd (group_closure S) = int m" |
|
146 proof (rule associated_eqI) |
|
147 from m show "Gcd (group_closure S) dvd int m" |
|
148 by (rule Gcd_dvd) |
|
149 show "int m dvd Gcd (group_closure S)" |
|
150 proof (rule Gcd_greatest) |
|
151 fix s |
|
152 assume s: "s \<in> group_closure S" |
|
153 show "int m dvd s" |
|
154 proof (rule ccontr) |
|
155 assume "\<not> int m dvd s" |
|
156 then have *: "0 < s mod int m" |
|
157 using \<open>0 < m\<close> le_less by fastforce |
|
158 have "m \<le> nat (s mod int m)" |
|
159 proof (subst m_def, rule Least_le, rule) |
|
160 from * show "0 < nat (s mod int m)" |
|
161 by simp |
|
162 from minus_div_mult_eq_mod [symmetric, of s "int m"] |
|
163 have "s mod int m = s - s div int m * int m" |
|
164 by auto |
|
165 also have "s - s div int m * int m \<in> group_closure S" |
|
166 by (auto intro: group_closure.diff s group_closure_mult_right m) |
|
167 finally show "int (nat (s mod int m)) \<in> group_closure S" |
|
168 by simp |
|
169 qed |
|
170 with * have "int m \<le> s mod int m" |
|
171 by simp |
|
172 moreover have "s mod int m < int m" |
|
173 using \<open>0 < m\<close> by simp |
|
174 ultimately show False |
|
175 by auto |
|
176 qed |
|
177 qed |
|
178 qed simp_all |
|
179 with m show ?thesis |
|
180 by simp |
|
181 qed |
|
182 |
|
183 lemma Gcd_in_group_closure: |
|
184 "Gcd S \<in> group_closure S" for S :: "int set" |
|
185 using Gcd_group_closure_in_group_closure [of S] |
|
186 by (simp add: Gcd_group_closure_eq_Gcd) |
|
187 |
|
188 lemma group_closure_eq: |
|
189 "group_closure S = range (times (Gcd S))" for S :: "int set" |
|
190 proof (auto intro: Gcd_in_group_closure group_closure_mult_left) |
|
191 fix s |
|
192 assume "s \<in> group_closure S" |
|
193 then show "s \<in> range (times (Gcd S))" |
|
194 proof induction |
|
195 case (base s) |
|
196 then have "Gcd S dvd s" |
|
197 by (auto intro: Gcd_dvd) |
|
198 then obtain t where "s = Gcd S * t" .. |
|
199 then show ?case |
|
200 by auto |
|
201 next |
|
202 case (diff s t) |
|
203 moreover have "Gcd S * a - Gcd S * b = Gcd S * (a - b)" for a b |
|
204 by (simp add: algebra_simps) |
|
205 ultimately show ?case |
|
206 by auto |
|
207 qed |
|
208 qed |
|
209 |
|
210 end |