1 (* Title: ZF/UNITY/AllocBase.ML |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 Common declarations for Chandy and Charpentier's Allocator |
|
7 *) |
|
8 |
|
9 (*????remove from Union.ML:AddSEs [not_emptyE];*) |
|
10 Delrules [not_emptyE]; |
|
11 |
|
12 Goal "0 < Nclients & 0 < NbT"; |
|
13 by (cut_facts_tac [Nclients_pos, NbT_pos] 1); |
|
14 by (auto_tac (claset() addIs [Ord_0_lt], simpset())); |
|
15 qed "Nclients_NbT_gt_0"; |
|
16 Addsimps [Nclients_NbT_gt_0 RS conjunct1, Nclients_NbT_gt_0 RS conjunct2]; |
|
17 |
|
18 Goal "Nclients \\<noteq> 0 & NbT \\<noteq> 0"; |
|
19 by (cut_facts_tac [Nclients_pos, NbT_pos] 1); |
|
20 by Auto_tac; |
|
21 qed "Nclients_NbT_not_0"; |
|
22 Addsimps [Nclients_NbT_not_0 RS conjunct1, Nclients_NbT_not_0 RS conjunct2]; |
|
23 |
|
24 Goal "Nclients\\<in>nat & NbT\\<in>nat"; |
|
25 by (cut_facts_tac [Nclients_pos, NbT_pos] 1); |
|
26 by Auto_tac; |
|
27 qed "Nclients_NbT_type"; |
|
28 Addsimps [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2]; |
|
29 AddTCs [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2]; |
|
30 |
|
31 Goal "b\\<in>Inter(RepFun(Nclients, B)) <-> (\\<forall>x\\<in>Nclients. b\\<in>B(x))"; |
|
32 by (auto_tac (claset(), simpset() addsimps [INT_iff])); |
|
33 by (res_inst_tac [("x", "0")] exI 1); |
|
34 by (rtac ltD 1); |
|
35 by Auto_tac; |
|
36 qed "INT_Nclient_iff"; |
|
37 AddIffs [INT_Nclient_iff]; |
|
38 |
|
39 val succ_def = thm "succ_def"; |
|
40 |
|
41 Goal "n\\<in>nat ==> \ |
|
42 \ (\\<forall>i\\<in>nat. i<n --> f(i) $<= g(i)) --> \ |
|
43 \ setsum(f, n) $<= setsum(g,n)"; |
|
44 by (induct_tac "n" 1); |
|
45 by (ALLGOALS Asm_full_simp_tac); |
|
46 by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x\\<notin>x" 1); |
|
47 by (Clarify_tac 1); |
|
48 by (Asm_simp_tac 1); |
|
49 by (subgoal_tac "\\<forall>i\\<in>nat. i<x--> f(i) $<= g(i)" 1); |
|
50 by (resolve_tac [zadd_zle_mono] 1); |
|
51 by (thin_tac "succ(x)=cons(x,x)" 1); |
|
52 by (ALLGOALS(Asm_simp_tac)); |
|
53 by (thin_tac "succ(x)=cons(x, x)" 1); |
|
54 by (Clarify_tac 1); |
|
55 by (dtac leI 1); |
|
56 by (Asm_simp_tac 1); |
|
57 by (asm_simp_tac (simpset() addsimps [nat_into_Finite, mem_not_refl, succ_def]) 1); |
|
58 qed_spec_mp "setsum_fun_mono"; |
|
59 |
|
60 Goal "l\\<in>list(A) ==> tokens(l)\\<in>nat"; |
|
61 by (etac list.induct 1); |
|
62 by Auto_tac; |
|
63 qed "tokens_type"; |
|
64 AddTCs [tokens_type]; |
|
65 Addsimps [tokens_type]; |
|
66 |
|
67 Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \ |
|
68 \ --> tokens(xs) \\<le> tokens(ys)"; |
|
69 by (induct_tac "xs" 1); |
|
70 by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], |
|
71 simpset() addsimps [prefix_def])); |
|
72 qed_spec_mp "tokens_mono_aux"; |
|
73 |
|
74 Goal "<xs, ys>\\<in>prefix(A) ==> tokens(xs) \\<le> tokens(ys)"; |
|
75 by (cut_facts_tac [prefix_type] 1); |
|
76 by (blast_tac (claset() addIs [tokens_mono_aux]) 1); |
|
77 qed "tokens_mono"; |
|
78 |
|
79 Goalw [mono1_def] "mono1(list(A), prefix(A), nat, Le ,tokens)"; |
|
80 by (auto_tac (claset() addIs [tokens_mono], |
|
81 simpset() addsimps [Le_def])); |
|
82 qed "mono_tokens"; |
|
83 Addsimps [mono_tokens]; |
|
84 AddIs [mono_tokens]; |
|
85 |
|
86 Goal |
|
87 "[| xs\\<in>list(A); ys\\<in>list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)"; |
|
88 by (induct_tac "xs" 1); |
|
89 by Auto_tac; |
|
90 qed "tokens_append"; |
|
91 Addsimps [tokens_append]; |
|
92 |
|
93 (*????????????????List.thy*) |
|
94 Goal "l\\<in>list(A) ==> \\<forall>n\\<in>nat. length(take(n, l))=min(n, length(l))"; |
|
95 by (induct_tac "l" 1); |
|
96 by Safe_tac; |
|
97 by (ALLGOALS(Asm_simp_tac)); |
|
98 by (etac natE 1); |
|
99 by (ALLGOALS(Asm_simp_tac)); |
|
100 qed "length_take"; |
|
101 |
|
102 (** bag_of **) |
|
103 |
|
104 Goal "l\\<in>list(A) ==>bag_of(l)\\<in>Mult(A)"; |
|
105 by (induct_tac "l" 1); |
|
106 by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); |
|
107 qed "bag_of_type"; |
|
108 AddTCs [bag_of_type]; |
|
109 Addsimps [bag_of_type]; |
|
110 |
|
111 Goal "l\\<in>list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A"; |
|
112 by (dtac bag_of_type 1); |
|
113 by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); |
|
114 qed "bag_of_multiset"; |
|
115 |
|
116 Goal "[| xs\\<in>list(A); ys\\<in>list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)"; |
|
117 by (induct_tac "xs" 1); |
|
118 by (auto_tac (claset(), simpset() |
|
119 addsimps [bag_of_multiset, munion_assoc])); |
|
120 qed "bag_of_append"; |
|
121 Addsimps [bag_of_append]; |
|
122 |
|
123 Goal "xs\\<in>list(A) ==> \\<forall>ys\\<in>list(A). <xs, ys>\\<in>prefix(A) \ |
|
124 \ --> <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)"; |
|
125 by (induct_tac "xs" 1); |
|
126 by (ALLGOALS(Clarify_tac)); |
|
127 by (ftac bag_of_multiset 1); |
|
128 by (forw_inst_tac [("l", "ys")] bag_of_multiset 2); |
|
129 by (auto_tac (claset() addIs [empty_le_MultLe], |
|
130 simpset() addsimps [prefix_def])); |
|
131 by (rtac munion_mono 1); |
|
132 by (force_tac (claset(), simpset() addsimps |
|
133 [MultLe_def, Mult_iff_multiset]) 1); |
|
134 by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 1); |
|
135 qed_spec_mp "bag_of_mono_aux"; |
|
136 |
|
137 Goal "[| <xs, ys>\\<in>prefix(A); xs\\<in>list(A); ys\\<in>list(A) |] ==> \ |
|
138 \ <bag_of(xs), bag_of(ys)>\\<in>MultLe(A, r)"; |
|
139 by (blast_tac (claset() addIs [bag_of_mono_aux]) 1); |
|
140 qed "bag_of_mono"; |
|
141 AddIs [bag_of_mono]; |
|
142 |
|
143 Goalw [mono1_def] |
|
144 "mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)"; |
|
145 by (auto_tac (claset(), simpset() addsimps [bag_of_type])); |
|
146 qed "mono_bag_of"; |
|
147 Addsimps [mono_bag_of]; |
|
148 |
|
149 |
|
150 (** msetsum **) |
|
151 |
|
152 bind_thm("nat_into_Fin", eqpoll_refl RSN (2,thm"Fin_lemma")); |
|
153 |
|
154 Goal "l \\<in> list(A) ==> C Int length(l) \\<in> Fin(length(l))"; |
|
155 by (dtac length_type 1); |
|
156 by (rtac Fin_subset 1); |
|
157 by (rtac Int_lower2 1); |
|
158 by (etac nat_into_Fin 1); |
|
159 qed "list_Int_length_Fin"; |
|
160 |
|
161 |
|
162 |
|
163 Goal "[|xs \\<in> list(A); k \\<in> C \\<inter> length(xs)|] ==> k < length(xs)"; |
|
164 by (asm_full_simp_tac (simpset() addsimps [ltI]) 1); |
|
165 qed "mem_Int_imp_lt_length"; |
|
166 |
|
167 |
|
168 Goal "[|C \\<subseteq> nat; x \\<in> A; xs \\<in> list(A)|] \ |
|
169 \ ==> msetsum(\\<lambda>i. {#nth(i, xs @ [x])#}, C \\<inter> succ(length(xs)), A) = \ |
|
170 \ (if length(xs) \\<in> C then \ |
|
171 \ {#x#} +# msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A) \ |
|
172 \ else msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A))"; |
|
173 by (asm_full_simp_tac (simpset() addsimps [subsetD, nth_append, lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); |
|
174 by (asm_full_simp_tac (simpset() addsimps [Int_succ_right]) 1); |
|
175 by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); |
|
176 by (Clarify_tac 1); |
|
177 by (stac msetsum_cons 1); |
|
178 by (rtac succI1 3); |
|
179 by (blast_tac (claset() addIs [list_Int_length_Fin, subset_succI RS Fin_mono RS subsetD]) 1); |
|
180 by (asm_full_simp_tac (simpset() addsimps [mem_not_refl]) 1); |
|
181 by (asm_full_simp_tac (simpset() addsimps [nth_type, lt_not_refl]) 1); |
|
182 by (blast_tac (claset() addIs [nat_into_Ord, ltI, length_type]) 1); |
|
183 by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); |
|
184 qed "bag_of_sublist_lemma"; |
|
185 |
|
186 Goal "l\\<in>list(A) ==> \ |
|
187 \ C <= nat ==> \ |
|
188 \ bag_of(sublist(l, C)) = \ |
|
189 \ msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"; |
|
190 by (etac list_append_induct 1); |
|
191 by (Simp_tac 1); |
|
192 by (asm_simp_tac (simpset() addsimps [sublist_append, nth_append, |
|
193 bag_of_sublist_lemma, munion_commute, bag_of_sublist_lemma, |
|
194 msetsum_multiset, munion_0]) 1); |
|
195 qed "bag_of_sublist_lemma2"; |
|
196 |
|
197 |
|
198 Goal "l \\<in> list(A) ==> nat \\<inter> length(l) = length(l)"; |
|
199 by (rtac Int_absorb1 1); |
|
200 by (rtac OrdmemD 1); |
|
201 by Auto_tac; |
|
202 qed "nat_Int_length_eq"; |
|
203 |
|
204 (*eliminating the assumption C<=nat*) |
|
205 Goal "l\\<in>list(A) ==> \ |
|
206 \ bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"; |
|
207 by (subgoal_tac |
|
208 " bag_of(sublist(l, C Int nat)) = \ |
|
209 \ msetsum(%i. {#nth(i, l)#}, C Int length(l), A)" 1); |
|
210 by (asm_full_simp_tac (simpset() addsimps [sublist_Int_eq]) 1); |
|
211 by (asm_full_simp_tac (simpset() addsimps [bag_of_sublist_lemma2, Int_lower2, Int_assoc, nat_Int_length_eq]) 1); |
|
212 qed "bag_of_sublist"; |
|
213 |
|
214 Goal |
|
215 "l\\<in>list(A) ==> \ |
|
216 \ bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) = \ |
|
217 \ bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"; |
|
218 by (subgoal_tac |
|
219 "B Int C Int length(l) = \ |
|
220 \ (B Int length(l)) Int (C Int length(l))" 1); |
|
221 by (Blast_tac 2); |
|
222 by (asm_simp_tac (simpset() addsimps [bag_of_sublist, |
|
223 Int_Un_distrib2, msetsum_Un_Int]) 1); |
|
224 by (resolve_tac [msetsum_Un_Int] 1); |
|
225 by (REPEAT (etac list_Int_length_Fin 1)); |
|
226 by (asm_full_simp_tac (simpset() addsimps [ltI, nth_type]) 1); |
|
227 qed "bag_of_sublist_Un_Int"; |
|
228 |
|
229 |
|
230 Goal "[| l\\<in>list(A); B Int C = 0 |]\ |
|
231 \ ==> bag_of(sublist(l, B Un C)) = \ |
|
232 \ bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"; |
|
233 by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym, |
|
234 sublist_type, bag_of_multiset]) 1); |
|
235 qed "bag_of_sublist_Un_disjoint"; |
|
236 |
|
237 Goal "[|Finite(I); \\<forall>i\\<in>I. \\<forall>j\\<in>I. i\\<noteq>j --> A(i) \\<inter> A(j) = 0; \ |
|
238 \ l\\<in>list(B) |] \ |
|
239 \ ==> bag_of(sublist(l, \\<Union>i\\<in>I. A(i))) = \ |
|
240 \ (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) "; |
|
241 by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym]) |
|
242 addsimps [bag_of_sublist]) 1); |
|
243 by (stac (inst "A" "length(l)" msetsum_UN_disjoint) 1); |
|
244 by (dresolve_tac [Finite_into_Fin] 1); |
|
245 by (assume_tac 1); |
|
246 by (Force_tac 3); |
|
247 by (auto_tac (claset() addSIs [Fin_IntI2, Finite_into_Fin], |
|
248 simpset() addsimps [ltI, nth_type, length_type, nat_into_Finite])); |
|
249 qed_spec_mp "bag_of_sublist_UN_disjoint"; |
|
250 |
|
251 |
|
252 Goalw [part_ord_def, Lt_def, irrefl_def, trans_on_def] |
|
253 "part_ord(nat, Lt)"; |
|
254 by (auto_tac (claset() addIs [lt_trans], simpset())); |
|
255 qed "part_ord_Lt"; |
|
256 Addsimps [part_ord_Lt]; |
|
257 |
|
258 |
|
259 (** all_distinct **) |
|
260 |
|
261 Goalw [all_distinct_def] "all_distinct(Nil)"; |
|
262 by Auto_tac; |
|
263 qed "all_distinct_Nil"; |
|
264 |
|
265 Goalw [all_distinct_def] |
|
266 "all_distinct(Cons(a, l)) <-> \ |
|
267 \ (a\\<in>set_of_list(l) --> False) & (a \\<notin> set_of_list(l) --> all_distinct(l))"; |
|
268 by (auto_tac (claset() addEs [list.elim], simpset())); |
|
269 qed "all_distinct_Cons"; |
|
270 Addsimps [all_distinct_Nil, all_distinct_Cons]; |
|
271 |
|
272 (** state_of **) |
|
273 Goalw [state_of_def] "s\\<in>state ==> state_of(s)=s"; |
|
274 by Auto_tac; |
|
275 qed "state_of_state"; |
|
276 Addsimps [state_of_state]; |
|
277 |
|
278 |
|
279 Goalw [state_of_def] "state_of(state_of(s))=state_of(s)"; |
|
280 by Auto_tac; |
|
281 qed "state_of_idem"; |
|
282 Addsimps [state_of_idem]; |
|
283 |
|
284 |
|
285 Goalw [state_of_def] "state_of(s)\\<in>state"; |
|
286 by Auto_tac; |
|
287 qed "state_of_type"; |
|
288 Addsimps [state_of_type]; |
|
289 AddTCs [state_of_type]; |
|
290 |
|
291 Goalw [lift_def] "lift(x, s)=s`x"; |
|
292 by (Simp_tac 1); |
|
293 qed "lift_apply"; |
|
294 Addsimps [lift_apply]; |
|
295 |
|
296 (** Used in ClientImp **) |
|
297 |
|
298 Goalw [Increasing_def] |
|
299 "Increasing(A, r, %s. f(state_of(s))) = \ |
|
300 \ Increasing(A, r, f)"; |
|
301 by Auto_tac; |
|
302 qed "gen_Increains_state_of_eq"; |
|
303 bind_thm("Increasing_state_ofD1", |
|
304 gen_Increains_state_of_eq RS equalityD1 RS subsetD); |
|
305 bind_thm("Increasing_state_ofD2", |
|
306 gen_Increains_state_of_eq RS equalityD2 RS subsetD); |
|
307 |
|
308 Goalw [Follows_def, Increasing_def] |
|
309 "Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) = \ |
|
310 \ Follows(A, r, f, g)"; |
|
311 by Auto_tac; |
|
312 qed "Follows_state_of_eq"; |
|
313 bind_thm("Follows_state_ofD1", Follows_state_of_eq RS equalityD1 RS subsetD); |
|
314 bind_thm("Follows_state_ofD2", Follows_state_of_eq RS equalityD2 RS subsetD); |
|
315 |
|
316 (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*) |
|
317 fun list_of_Int th = list_of_Int_aux (Drule.freeze_all th) |
|
318 and list_of_Int_aux th = |
|
319 (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2)) |
|
320 handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2)) |
|
321 handle THM _ => (list_of_Int (th RS InterD)) |
|
322 handle THM _ => (list_of_Int (th RS bspec)) |
|
323 handle THM _ => [th]; |
|
324 |
|
325 (*Used just once, for Alloc_Increasing*) |
|
326 |
|
327 fun normalize th = |
|
328 normalize (th RS spec |
|
329 handle THM _ => th RS bspec |
|
330 handle THM _ => th RS (guarantees_INT_right_iff RS iffD1)) |
|
331 handle THM _ => th; |
|
332 |
|
333 Goal "n\\<in>nat ==> nat_list_inj(n)\\<in>list(nat)"; |
|
334 by (induct_tac "n" 1); |
|
335 by Auto_tac; |
|
336 qed "nat_list_inj_type"; |
|
337 |
|
338 Goal "n\\<in>nat ==> length(nat_list_inj(n)) = n"; |
|
339 by (induct_tac "n" 1); |
|
340 by Auto_tac; |
|
341 qed "length_nat_list_inj"; |
|
342 |
|
343 Goalw [nat_var_inj_def] |
|
344 "(\\<lambda>x\\<in>nat. nat_var_inj(x))\\<in>inj(nat, var)"; |
|
345 by (res_inst_tac [("d", "var_inj")] lam_injective 1); |
|
346 by (asm_simp_tac (simpset() addsimps [length_nat_list_inj]) 2); |
|
347 by (auto_tac (claset(), simpset() addsimps var.intrs@[nat_list_inj_type])); |
|
348 qed "var_infinite_lemma"; |
|
349 |
|
350 Goalw [lepoll_def] "nat lepoll var"; |
|
351 by (res_inst_tac [("x", "(\\<lambda>x\\<in>nat. nat_var_inj(x))")] exI 1); |
|
352 by (rtac var_infinite_lemma 1); |
|
353 qed "nat_lepoll_var"; |
|
354 |
|
355 Goalw [Finite_def] "~Finite(var)"; |
|
356 by Auto_tac; |
|
357 by (dtac eqpoll_imp_lepoll 1); |
|
358 by (cut_facts_tac [nat_lepoll_var] 1); |
|
359 by (subgoal_tac "nat lepoll x" 1); |
|
360 by (blast_tac (claset() addIs [lepoll_trans]) 2); |
|
361 by (dres_inst_tac [("i", "x"), ("A", "nat")] lepoll_cardinal_le 1); |
|
362 by Auto_tac; |
|
363 by (subgoal_tac "Card(nat)" 1); |
|
364 by (rewrite_goal_tac [Card_def] 1); |
|
365 by (dtac sym 1); |
|
366 by Auto_tac; |
|
367 by (dtac le_imp_subset 1); |
|
368 by (dtac subsetD 1); |
|
369 by (auto_tac (claset(), simpset() addsimps [Card_nat])); |
|
370 by (blast_tac (claset() addEs [mem_irrefl]) 1); |
|
371 qed "var_not_Finite"; |
|
372 |
|
373 Goal "~Finite(A) ==> \\<exists>x. x\\<in>A"; |
|
374 by (etac swap 1); |
|
375 by Auto_tac; |
|
376 by (subgoal_tac "A=0" 1); |
|
377 by (auto_tac (claset(), simpset() addsimps [Finite_0])); |
|
378 qed "not_Finite_imp_exist"; |
|
379 |
|
380 Goal "Finite(A) ==> b\\<in>(Inter(RepFun(var-A, B))) <-> (\\<forall>x\\<in>var-A. b\\<in>B(x))"; |
|
381 by (subgoal_tac "\\<exists>x. x\\<in>var-A" 1); |
|
382 by Auto_tac; |
|
383 by (subgoal_tac "~Finite(var-A)" 1); |
|
384 by (dtac not_Finite_imp_exist 1); |
|
385 by Auto_tac; |
|
386 by (cut_facts_tac [var_not_Finite] 1); |
|
387 by (etac swap 1); |
|
388 by (res_inst_tac [("B", "A")] Diff_Finite 1); |
|
389 by Auto_tac; |
|
390 qed "Inter_Diff_var_iff"; |
|
391 |
|
392 Goal "[| b\\<in>Inter(RepFun(var-A, B)); Finite(A); x\\<in>var-A |] ==> b\\<in>B(x)"; |
|
393 by (rotate_tac 1 1); |
|
394 by (asm_full_simp_tac (simpset() addsimps [Inter_Diff_var_iff]) 1); |
|
395 qed "Inter_var_DiffD"; |
|
396 |
|
397 (* [| Finite(A); (\\<forall>x\\<in>var-A. b\\<in>B(x)) |] ==> b\\<in>Inter(RepFun(var-A, B)) *) |
|
398 bind_thm("Inter_var_DiffI", Inter_Diff_var_iff RS iffD2); |
|
399 |
|
400 AddSIs [Inter_var_DiffI]; |
|
401 Addsimps [Finite_0, Finite_cons]; |
|
402 |
|
403 Goal "Acts(F)<= A \\<inter> Pow(state*state) <-> Acts(F)<=A"; |
|
404 by (cut_facts_tac [inst "F" "F" Acts_type] 1); |
|
405 by Auto_tac; |
|
406 qed "Acts_subset_Int_Pow_simp"; |
|
407 Addsimps [Acts_subset_Int_Pow_simp]; |
|
408 |
|
409 (*for main zf?????*) |
|
410 Goal "cons(x, A \\<inter> B) = cons(x, A) \\<inter> cons(x, B)"; |
|
411 by Auto_tac; |
|
412 qed "cons_Int_distrib"; |
|
413 |
|
414 |
|
415 (* Currently not used, but of potential interest *) |
|
416 Goal |
|
417 "[| Finite(A); \\<forall>x\\<in>A. g(x)\\<in>nat |] ==> \ |
|
418 \ setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)"; |
|
419 by (etac Finite_induct 1); |
|
420 by (auto_tac (claset(), simpset() addsimps [int_of_add])); |
|
421 qed "setsum_nsetsum_eq"; |
|
422 |
|
423 Goal |
|
424 "[| A=B; \\<forall>x\\<in>A. f(x)=g(x); \\<forall>x\\<in>A. g(x)\\<in>nat; \ |
|
425 \ Finite(A) |] ==> nsetsum(f, A) = nsetsum(g, B)"; |
|
426 by (subgoal_tac "$# nsetsum(f, A) = $# nsetsum(g, B)" 1); |
|
427 by (rtac trans 2); |
|
428 by (rtac setsum_nsetsum_eq 3); |
|
429 by (rtac trans 2); |
|
430 by (rtac (setsum_nsetsum_eq RS sym) 2); |
|
431 by Auto_tac; |
|
432 by (rtac setsum_cong 1); |
|
433 by Auto_tac; |
|
434 qed "nsetsum_cong"; |
|
435 |
|
436 |
|
437 |
|
438 |
|