|
1 (* Title: HOL/ex/Set_Algebras.thy |
|
2 Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM |
|
3 *) |
|
4 |
|
5 header {* Algebraic operations on sets *} |
|
6 |
|
7 theory Set_Algebras |
|
8 imports Main Interpretation_with_Defs |
|
9 begin |
|
10 |
|
11 text {* |
|
12 This library lifts operations like addition and muliplication to |
|
13 sets. It was designed to support asymptotic calculations. See the |
|
14 comments at the top of theory @{text BigO}. |
|
15 *} |
|
16 |
|
17 definition set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<oplus>" 65) where |
|
18 "A \<oplus> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}" |
|
19 |
|
20 definition set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<otimes>" 70) where |
|
21 "A \<otimes> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}" |
|
22 |
|
23 definition elt_set_plus :: "'a::plus \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "+o" 70) where |
|
24 "a +o B = {c. \<exists>b\<in>B. c = a + b}" |
|
25 |
|
26 definition elt_set_times :: "'a::times \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "*o" 80) where |
|
27 "a *o B = {c. \<exists>b\<in>B. c = a * b}" |
|
28 |
|
29 abbreviation (input) elt_set_eq :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infix "=o" 50) where |
|
30 "x =o A \<equiv> x \<in> A" |
|
31 |
|
32 interpretation set_add!: semigroup "set_plus :: 'a::semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof |
|
33 qed (force simp add: set_plus_def add.assoc) |
|
34 |
|
35 interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof |
|
36 qed (force simp add: set_plus_def add.commute) |
|
37 |
|
38 interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof |
|
39 qed (simp_all add: set_plus_def) |
|
40 |
|
41 interpretation set_add!: comm_monoid "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof |
|
42 qed (simp add: set_plus_def) |
|
43 |
|
44 interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" |
|
45 defines listsum_set is set_add.listsum |
|
46 proof |
|
47 qed (simp_all add: set_add.assoc) |
|
48 |
|
49 interpretation set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" |
|
50 defines setsum_set is set_add.setsum |
|
51 where "monoid_add.listsum set_plus {0::'a} = listsum_set" |
|
52 proof - |
|
53 show "class.comm_monoid_add (set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {0}" proof |
|
54 qed (simp_all add: set_add.commute) |
|
55 then interpret set_add!: comm_monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" . |
|
56 show "monoid_add.listsum set_plus {0::'a} = listsum_set" |
|
57 by (simp only: listsum_set_def) |
|
58 qed |
|
59 |
|
60 interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof |
|
61 qed (force simp add: set_times_def mult.assoc) |
|
62 |
|
63 interpretation set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof |
|
64 qed (force simp add: set_times_def mult.commute) |
|
65 |
|
66 interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof |
|
67 qed (simp_all add: set_times_def) |
|
68 |
|
69 interpretation set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof |
|
70 qed (simp add: set_times_def) |
|
71 |
|
72 interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
73 defines power_set is set_mult.power |
|
74 proof |
|
75 qed (simp_all add: set_mult.assoc) |
|
76 |
|
77 interpretation set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" |
|
78 defines setprod_set is set_mult.setprod |
|
79 where "power.power {1} set_times = power_set" |
|
80 proof - |
|
81 show "class.comm_monoid_mult (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {1}" proof |
|
82 qed (simp_all add: set_mult.commute) |
|
83 then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" . |
|
84 show "power.power {1} set_times = power_set" |
|
85 by (simp add: power_set_def) |
|
86 qed |
|
87 |
|
88 lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D" |
|
89 by (auto simp add: set_plus_def) |
|
90 |
|
91 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C" |
|
92 by (auto simp add: elt_set_plus_def) |
|
93 |
|
94 lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus> |
|
95 (b +o D) = (a + b) +o (C \<oplus> D)" |
|
96 apply (auto simp add: elt_set_plus_def set_plus_def add_ac) |
|
97 apply (rule_tac x = "ba + bb" in exI) |
|
98 apply (auto simp add: add_ac) |
|
99 apply (rule_tac x = "aa + a" in exI) |
|
100 apply (auto simp add: add_ac) |
|
101 done |
|
102 |
|
103 lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = |
|
104 (a + b) +o C" |
|
105 by (auto simp add: elt_set_plus_def add_assoc) |
|
106 |
|
107 lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C = |
|
108 a +o (B \<oplus> C)" |
|
109 apply (auto simp add: elt_set_plus_def set_plus_def) |
|
110 apply (blast intro: add_ac) |
|
111 apply (rule_tac x = "a + aa" in exI) |
|
112 apply (rule conjI) |
|
113 apply (rule_tac x = "aa" in bexI) |
|
114 apply auto |
|
115 apply (rule_tac x = "ba" in bexI) |
|
116 apply (auto simp add: add_ac) |
|
117 done |
|
118 |
|
119 theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) = |
|
120 a +o (C \<oplus> D)" |
|
121 apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac) |
|
122 apply (rule_tac x = "aa + ba" in exI) |
|
123 apply (auto simp add: add_ac) |
|
124 done |
|
125 |
|
126 theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2 |
|
127 set_plus_rearrange3 set_plus_rearrange4 |
|
128 |
|
129 lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D" |
|
130 by (auto simp add: elt_set_plus_def) |
|
131 |
|
132 lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==> |
|
133 C \<oplus> E <= D \<oplus> F" |
|
134 by (auto simp add: set_plus_def) |
|
135 |
|
136 lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D" |
|
137 by (auto simp add: elt_set_plus_def set_plus_def) |
|
138 |
|
139 lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==> |
|
140 a +o D <= D \<oplus> C" |
|
141 by (auto simp add: elt_set_plus_def set_plus_def add_ac) |
|
142 |
|
143 lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D" |
|
144 apply (subgoal_tac "a +o B <= a +o D") |
|
145 apply (erule order_trans) |
|
146 apply (erule set_plus_mono3) |
|
147 apply (erule set_plus_mono) |
|
148 done |
|
149 |
|
150 lemma set_plus_mono_b: "C <= D ==> x : a +o C |
|
151 ==> x : a +o D" |
|
152 apply (frule set_plus_mono) |
|
153 apply auto |
|
154 done |
|
155 |
|
156 lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==> |
|
157 x : D \<oplus> F" |
|
158 apply (frule set_plus_mono2) |
|
159 prefer 2 |
|
160 apply force |
|
161 apply assumption |
|
162 done |
|
163 |
|
164 lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D" |
|
165 apply (frule set_plus_mono3) |
|
166 apply auto |
|
167 done |
|
168 |
|
169 lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==> |
|
170 x : a +o D ==> x : D \<oplus> C" |
|
171 apply (frule set_plus_mono4) |
|
172 apply auto |
|
173 done |
|
174 |
|
175 lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C" |
|
176 by (auto simp add: elt_set_plus_def) |
|
177 |
|
178 lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B" |
|
179 apply (auto intro!: subsetI simp add: set_plus_def) |
|
180 apply (rule_tac x = 0 in bexI) |
|
181 apply (rule_tac x = x in bexI) |
|
182 apply (auto simp add: add_ac) |
|
183 done |
|
184 |
|
185 lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C" |
|
186 by (auto simp add: elt_set_plus_def add_ac diff_minus) |
|
187 |
|
188 lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C" |
|
189 apply (auto simp add: elt_set_plus_def add_ac diff_minus) |
|
190 apply (subgoal_tac "a = (a + - b) + b") |
|
191 apply (rule bexI, assumption, assumption) |
|
192 apply (auto simp add: add_ac) |
|
193 done |
|
194 |
|
195 lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)" |
|
196 by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus, |
|
197 assumption) |
|
198 |
|
199 lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D" |
|
200 by (auto simp add: set_times_def) |
|
201 |
|
202 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C" |
|
203 by (auto simp add: elt_set_times_def) |
|
204 |
|
205 lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes> |
|
206 (b *o D) = (a * b) *o (C \<otimes> D)" |
|
207 apply (auto simp add: elt_set_times_def set_times_def) |
|
208 apply (rule_tac x = "ba * bb" in exI) |
|
209 apply (auto simp add: mult_ac) |
|
210 apply (rule_tac x = "aa * a" in exI) |
|
211 apply (auto simp add: mult_ac) |
|
212 done |
|
213 |
|
214 lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) = |
|
215 (a * b) *o C" |
|
216 by (auto simp add: elt_set_times_def mult_assoc) |
|
217 |
|
218 lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C = |
|
219 a *o (B \<otimes> C)" |
|
220 apply (auto simp add: elt_set_times_def set_times_def) |
|
221 apply (blast intro: mult_ac) |
|
222 apply (rule_tac x = "a * aa" in exI) |
|
223 apply (rule conjI) |
|
224 apply (rule_tac x = "aa" in bexI) |
|
225 apply auto |
|
226 apply (rule_tac x = "ba" in bexI) |
|
227 apply (auto simp add: mult_ac) |
|
228 done |
|
229 |
|
230 theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) = |
|
231 a *o (C \<otimes> D)" |
|
232 apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def |
|
233 mult_ac) |
|
234 apply (rule_tac x = "aa * ba" in exI) |
|
235 apply (auto simp add: mult_ac) |
|
236 done |
|
237 |
|
238 theorems set_times_rearranges = set_times_rearrange set_times_rearrange2 |
|
239 set_times_rearrange3 set_times_rearrange4 |
|
240 |
|
241 lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D" |
|
242 by (auto simp add: elt_set_times_def) |
|
243 |
|
244 lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==> |
|
245 C \<otimes> E <= D \<otimes> F" |
|
246 by (auto simp add: set_times_def) |
|
247 |
|
248 lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D" |
|
249 by (auto simp add: elt_set_times_def set_times_def) |
|
250 |
|
251 lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==> |
|
252 a *o D <= D \<otimes> C" |
|
253 by (auto simp add: elt_set_times_def set_times_def mult_ac) |
|
254 |
|
255 lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D" |
|
256 apply (subgoal_tac "a *o B <= a *o D") |
|
257 apply (erule order_trans) |
|
258 apply (erule set_times_mono3) |
|
259 apply (erule set_times_mono) |
|
260 done |
|
261 |
|
262 lemma set_times_mono_b: "C <= D ==> x : a *o C |
|
263 ==> x : a *o D" |
|
264 apply (frule set_times_mono) |
|
265 apply auto |
|
266 done |
|
267 |
|
268 lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==> |
|
269 x : D \<otimes> F" |
|
270 apply (frule set_times_mono2) |
|
271 prefer 2 |
|
272 apply force |
|
273 apply assumption |
|
274 done |
|
275 |
|
276 lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D" |
|
277 apply (frule set_times_mono3) |
|
278 apply auto |
|
279 done |
|
280 |
|
281 lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==> |
|
282 x : a *o D ==> x : D \<otimes> C" |
|
283 apply (frule set_times_mono4) |
|
284 apply auto |
|
285 done |
|
286 |
|
287 lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C" |
|
288 by (auto simp add: elt_set_times_def) |
|
289 |
|
290 lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)= |
|
291 (a * b) +o (a *o C)" |
|
292 by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs) |
|
293 |
|
294 lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) = |
|
295 (a *o B) \<oplus> (a *o C)" |
|
296 apply (auto simp add: set_plus_def elt_set_times_def ring_distribs) |
|
297 apply blast |
|
298 apply (rule_tac x = "b + bb" in exI) |
|
299 apply (auto simp add: ring_distribs) |
|
300 done |
|
301 |
|
302 lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <= |
|
303 a *o D \<oplus> C \<otimes> D" |
|
304 apply (auto intro!: subsetI simp add: |
|
305 elt_set_plus_def elt_set_times_def set_times_def |
|
306 set_plus_def ring_distribs) |
|
307 apply auto |
|
308 done |
|
309 |
|
310 theorems set_times_plus_distribs = |
|
311 set_times_plus_distrib |
|
312 set_times_plus_distrib2 |
|
313 |
|
314 lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==> |
|
315 - a : C" |
|
316 by (auto simp add: elt_set_times_def) |
|
317 |
|
318 lemma set_neg_intro2: "(a::'a::ring_1) : C ==> |
|
319 - a : (- 1) *o C" |
|
320 by (auto simp add: elt_set_times_def) |
|
321 |
|
322 lemma set_plus_image: |
|
323 fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)" |
|
324 unfolding set_plus_def by (fastsimp simp: image_iff) |
|
325 |
|
326 lemma set_setsum_alt: |
|
327 assumes fin: "finite I" |
|
328 shows "setsum_set S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}" |
|
329 (is "_ = ?setsum I") |
|
330 using fin proof induct |
|
331 case (insert x F) |
|
332 have "setsum_set S (insert x F) = S x \<oplus> ?setsum F" |
|
333 using insert.hyps by auto |
|
334 also have "...= {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}" |
|
335 unfolding set_plus_def |
|
336 proof safe |
|
337 fix y s assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i" |
|
338 then show "\<exists>s'. y + setsum s F = s' x + setsum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)" |
|
339 using insert.hyps |
|
340 by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def) |
|
341 qed auto |
|
342 finally show ?case |
|
343 using insert.hyps by auto |
|
344 qed auto |
|
345 |
|
346 lemma setsum_set_cond_linear: |
|
347 fixes f :: "('a::comm_monoid_add) set \<Rightarrow> ('b::comm_monoid_add) set" |
|
348 assumes [intro!]: "\<And>A B. P A \<Longrightarrow> P B \<Longrightarrow> P (A \<oplus> B)" "P {0}" |
|
349 and f: "\<And>A B. P A \<Longrightarrow> P B \<Longrightarrow> f (A \<oplus> B) = f A \<oplus> f B" "f {0} = {0}" |
|
350 assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)" |
|
351 shows "f (setsum_set S I) = setsum_set (f \<circ> S) I" |
|
352 proof cases |
|
353 assume "finite I" from this all show ?thesis |
|
354 proof induct |
|
355 case (insert x F) |
|
356 from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum_set S F)" |
|
357 by induct auto |
|
358 with insert show ?case |
|
359 by (simp, subst f) auto |
|
360 qed (auto intro!: f) |
|
361 qed (auto intro!: f) |
|
362 |
|
363 lemma setsum_set_linear: |
|
364 fixes f :: "('a::comm_monoid_add) set => ('b::comm_monoid_add) set" |
|
365 assumes "\<And>A B. f(A) \<oplus> f(B) = f(A \<oplus> B)" "f {0} = {0}" |
|
366 shows "f (setsum_set S I) = setsum_set (f \<circ> S) I" |
|
367 using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto |
|
368 |
|
369 end |