|
1 (* Title: HOL/Library/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 |
|
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 definition listsum_set :: "('a::monoid_add set) list \<Rightarrow> 'a set" where |
|
45 "listsum_set = monoid_add.listsum set_plus {0}" |
|
46 |
|
47 interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where |
|
48 "monoid_add.listsum set_plus {0::'a} = listsum_set" |
|
49 proof - |
|
50 show "class.monoid_add set_plus {0::'a}" proof |
|
51 qed (simp_all add: set_add.assoc) |
|
52 then interpret set_add!: monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" . |
|
53 show "monoid_add.listsum set_plus {0::'a} = listsum_set" |
|
54 by (simp only: listsum_set_def) |
|
55 qed |
|
56 |
|
57 definition setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where |
|
58 "setsum_set f A = (if finite A then fold_image set_plus f {0} A else {0})" |
|
59 |
|
60 interpretation set_add!: |
|
61 comm_monoid_big "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" setsum_set |
|
62 proof |
|
63 qed (fact setsum_set_def) |
|
64 |
|
65 interpretation set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where |
|
66 "monoid_add.listsum set_plus {0::'a} = listsum_set" |
|
67 and "comm_monoid_add.setsum set_plus {0::'a} = setsum_set" |
|
68 proof - |
|
69 show "class.comm_monoid_add (set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {0}" proof |
|
70 qed (simp_all add: set_add.commute) |
|
71 then interpret set_add!: comm_monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" . |
|
72 show "monoid_add.listsum set_plus {0::'a} = listsum_set" |
|
73 by (simp only: listsum_set_def) |
|
74 show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set" |
|
75 by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq) |
|
76 qed |
|
77 |
|
78 interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof |
|
79 qed (force simp add: set_times_def mult.assoc) |
|
80 |
|
81 interpretation set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof |
|
82 qed (force simp add: set_times_def mult.commute) |
|
83 |
|
84 interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof |
|
85 qed (simp_all add: set_times_def) |
|
86 |
|
87 interpretation set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof |
|
88 qed (simp add: set_times_def) |
|
89 |
|
90 definition power_set :: "nat \<Rightarrow> ('a::monoid_mult set) \<Rightarrow> 'a set" where |
|
91 "power_set n A = power.power {1} set_times A n" |
|
92 |
|
93 interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
94 "power.power {1} set_times = (\<lambda>A n. power_set n A)" |
|
95 proof - |
|
96 show "class.monoid_mult {1} (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set)" proof |
|
97 qed (simp_all add: set_mult.assoc) |
|
98 show "power.power {1} set_times = (\<lambda>A n. power_set n A)" |
|
99 by (simp add: power_set_def) |
|
100 qed |
|
101 |
|
102 definition setprod_set :: "('b \<Rightarrow> ('a::comm_monoid_mult) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where |
|
103 "setprod_set f A = (if finite A then fold_image set_times f {1} A else {1})" |
|
104 |
|
105 interpretation set_mult!: |
|
106 comm_monoid_big "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" setprod_set |
|
107 proof |
|
108 qed (fact setprod_set_def) |
|
109 |
|
110 interpretation set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" where |
|
111 "power.power {1} set_times = (\<lambda>A n. power_set n A)" |
|
112 and "comm_monoid_mult.setprod set_times {1::'a} = setprod_set" |
|
113 proof - |
|
114 show "class.comm_monoid_mult (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {1}" proof |
|
115 qed (simp_all add: set_mult.commute) |
|
116 then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" . |
|
117 show "power.power {1} set_times = (\<lambda>A n. power_set n A)" |
|
118 by (simp add: power_set_def) |
|
119 show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set" |
|
120 by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq) |
|
121 qed |
|
122 |
|
123 lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D" |
|
124 by (auto simp add: set_plus_def) |
|
125 |
|
126 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C" |
|
127 by (auto simp add: elt_set_plus_def) |
|
128 |
|
129 lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus> |
|
130 (b +o D) = (a + b) +o (C \<oplus> D)" |
|
131 apply (auto simp add: elt_set_plus_def set_plus_def add_ac) |
|
132 apply (rule_tac x = "ba + bb" in exI) |
|
133 apply (auto simp add: add_ac) |
|
134 apply (rule_tac x = "aa + a" in exI) |
|
135 apply (auto simp add: add_ac) |
|
136 done |
|
137 |
|
138 lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = |
|
139 (a + b) +o C" |
|
140 by (auto simp add: elt_set_plus_def add_assoc) |
|
141 |
|
142 lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C = |
|
143 a +o (B \<oplus> C)" |
|
144 apply (auto simp add: elt_set_plus_def set_plus_def) |
|
145 apply (blast intro: add_ac) |
|
146 apply (rule_tac x = "a + aa" in exI) |
|
147 apply (rule conjI) |
|
148 apply (rule_tac x = "aa" in bexI) |
|
149 apply auto |
|
150 apply (rule_tac x = "ba" in bexI) |
|
151 apply (auto simp add: add_ac) |
|
152 done |
|
153 |
|
154 theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) = |
|
155 a +o (C \<oplus> D)" |
|
156 apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac) |
|
157 apply (rule_tac x = "aa + ba" in exI) |
|
158 apply (auto simp add: add_ac) |
|
159 done |
|
160 |
|
161 theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2 |
|
162 set_plus_rearrange3 set_plus_rearrange4 |
|
163 |
|
164 lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D" |
|
165 by (auto simp add: elt_set_plus_def) |
|
166 |
|
167 lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==> |
|
168 C \<oplus> E <= D \<oplus> F" |
|
169 by (auto simp add: set_plus_def) |
|
170 |
|
171 lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D" |
|
172 by (auto simp add: elt_set_plus_def set_plus_def) |
|
173 |
|
174 lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==> |
|
175 a +o D <= D \<oplus> C" |
|
176 by (auto simp add: elt_set_plus_def set_plus_def add_ac) |
|
177 |
|
178 lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D" |
|
179 apply (subgoal_tac "a +o B <= a +o D") |
|
180 apply (erule order_trans) |
|
181 apply (erule set_plus_mono3) |
|
182 apply (erule set_plus_mono) |
|
183 done |
|
184 |
|
185 lemma set_plus_mono_b: "C <= D ==> x : a +o C |
|
186 ==> x : a +o D" |
|
187 apply (frule set_plus_mono) |
|
188 apply auto |
|
189 done |
|
190 |
|
191 lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==> |
|
192 x : D \<oplus> F" |
|
193 apply (frule set_plus_mono2) |
|
194 prefer 2 |
|
195 apply force |
|
196 apply assumption |
|
197 done |
|
198 |
|
199 lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D" |
|
200 apply (frule set_plus_mono3) |
|
201 apply auto |
|
202 done |
|
203 |
|
204 lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==> |
|
205 x : a +o D ==> x : D \<oplus> C" |
|
206 apply (frule set_plus_mono4) |
|
207 apply auto |
|
208 done |
|
209 |
|
210 lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C" |
|
211 by (auto simp add: elt_set_plus_def) |
|
212 |
|
213 lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B" |
|
214 apply (auto intro!: subsetI simp add: set_plus_def) |
|
215 apply (rule_tac x = 0 in bexI) |
|
216 apply (rule_tac x = x in bexI) |
|
217 apply (auto simp add: add_ac) |
|
218 done |
|
219 |
|
220 lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C" |
|
221 by (auto simp add: elt_set_plus_def add_ac diff_minus) |
|
222 |
|
223 lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C" |
|
224 apply (auto simp add: elt_set_plus_def add_ac diff_minus) |
|
225 apply (subgoal_tac "a = (a + - b) + b") |
|
226 apply (rule bexI, assumption, assumption) |
|
227 apply (auto simp add: add_ac) |
|
228 done |
|
229 |
|
230 lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)" |
|
231 by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus, |
|
232 assumption) |
|
233 |
|
234 lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D" |
|
235 by (auto simp add: set_times_def) |
|
236 |
|
237 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C" |
|
238 by (auto simp add: elt_set_times_def) |
|
239 |
|
240 lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes> |
|
241 (b *o D) = (a * b) *o (C \<otimes> D)" |
|
242 apply (auto simp add: elt_set_times_def set_times_def) |
|
243 apply (rule_tac x = "ba * bb" in exI) |
|
244 apply (auto simp add: mult_ac) |
|
245 apply (rule_tac x = "aa * a" in exI) |
|
246 apply (auto simp add: mult_ac) |
|
247 done |
|
248 |
|
249 lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) = |
|
250 (a * b) *o C" |
|
251 by (auto simp add: elt_set_times_def mult_assoc) |
|
252 |
|
253 lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C = |
|
254 a *o (B \<otimes> C)" |
|
255 apply (auto simp add: elt_set_times_def set_times_def) |
|
256 apply (blast intro: mult_ac) |
|
257 apply (rule_tac x = "a * aa" in exI) |
|
258 apply (rule conjI) |
|
259 apply (rule_tac x = "aa" in bexI) |
|
260 apply auto |
|
261 apply (rule_tac x = "ba" in bexI) |
|
262 apply (auto simp add: mult_ac) |
|
263 done |
|
264 |
|
265 theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) = |
|
266 a *o (C \<otimes> D)" |
|
267 apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def |
|
268 mult_ac) |
|
269 apply (rule_tac x = "aa * ba" in exI) |
|
270 apply (auto simp add: mult_ac) |
|
271 done |
|
272 |
|
273 theorems set_times_rearranges = set_times_rearrange set_times_rearrange2 |
|
274 set_times_rearrange3 set_times_rearrange4 |
|
275 |
|
276 lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D" |
|
277 by (auto simp add: elt_set_times_def) |
|
278 |
|
279 lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==> |
|
280 C \<otimes> E <= D \<otimes> F" |
|
281 by (auto simp add: set_times_def) |
|
282 |
|
283 lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D" |
|
284 by (auto simp add: elt_set_times_def set_times_def) |
|
285 |
|
286 lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==> |
|
287 a *o D <= D \<otimes> C" |
|
288 by (auto simp add: elt_set_times_def set_times_def mult_ac) |
|
289 |
|
290 lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D" |
|
291 apply (subgoal_tac "a *o B <= a *o D") |
|
292 apply (erule order_trans) |
|
293 apply (erule set_times_mono3) |
|
294 apply (erule set_times_mono) |
|
295 done |
|
296 |
|
297 lemma set_times_mono_b: "C <= D ==> x : a *o C |
|
298 ==> x : a *o D" |
|
299 apply (frule set_times_mono) |
|
300 apply auto |
|
301 done |
|
302 |
|
303 lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==> |
|
304 x : D \<otimes> F" |
|
305 apply (frule set_times_mono2) |
|
306 prefer 2 |
|
307 apply force |
|
308 apply assumption |
|
309 done |
|
310 |
|
311 lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D" |
|
312 apply (frule set_times_mono3) |
|
313 apply auto |
|
314 done |
|
315 |
|
316 lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==> |
|
317 x : a *o D ==> x : D \<otimes> C" |
|
318 apply (frule set_times_mono4) |
|
319 apply auto |
|
320 done |
|
321 |
|
322 lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C" |
|
323 by (auto simp add: elt_set_times_def) |
|
324 |
|
325 lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)= |
|
326 (a * b) +o (a *o C)" |
|
327 by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs) |
|
328 |
|
329 lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) = |
|
330 (a *o B) \<oplus> (a *o C)" |
|
331 apply (auto simp add: set_plus_def elt_set_times_def ring_distribs) |
|
332 apply blast |
|
333 apply (rule_tac x = "b + bb" in exI) |
|
334 apply (auto simp add: ring_distribs) |
|
335 done |
|
336 |
|
337 lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <= |
|
338 a *o D \<oplus> C \<otimes> D" |
|
339 apply (auto intro!: subsetI simp add: |
|
340 elt_set_plus_def elt_set_times_def set_times_def |
|
341 set_plus_def ring_distribs) |
|
342 apply auto |
|
343 done |
|
344 |
|
345 theorems set_times_plus_distribs = |
|
346 set_times_plus_distrib |
|
347 set_times_plus_distrib2 |
|
348 |
|
349 lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==> |
|
350 - a : C" |
|
351 by (auto simp add: elt_set_times_def) |
|
352 |
|
353 lemma set_neg_intro2: "(a::'a::ring_1) : C ==> |
|
354 - a : (- 1) *o C" |
|
355 by (auto simp add: elt_set_times_def) |
|
356 |
|
357 end |