14052
|
1 |
(* Title: ZF/UNITY/AllocBase.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2001 University of Cambridge
|
|
5 |
|
|
6 |
*)
|
|
7 |
|
14076
|
8 |
header{*Common declarations for Chandy and Charpentier's Allocator*}
|
|
9 |
|
|
10 |
theory AllocBase = Follows + MultisetSum + Guar:
|
14052
|
11 |
|
|
12 |
consts
|
|
13 |
tokbag :: i (* tokbags could be multisets...or any ordered type?*)
|
|
14 |
NbT :: i (* Number of tokens in system *)
|
|
15 |
Nclients :: i (* Number of clients *)
|
14076
|
16 |
|
|
17 |
translations "tokbag" => "nat"
|
|
18 |
|
|
19 |
axioms
|
|
20 |
NbT_pos: "NbT \<in> nat-{0}"
|
|
21 |
Nclients_pos: "Nclients \<in> nat-{0}"
|
14052
|
22 |
|
14076
|
23 |
text{*This function merely sums the elements of a list*}
|
|
24 |
consts tokens :: "i =>i"
|
14052
|
25 |
item :: i (* Items to be merged/distributed *)
|
|
26 |
primrec
|
|
27 |
"tokens(Nil) = 0"
|
|
28 |
"tokens (Cons(x,xs)) = x #+ tokens(xs)"
|
|
29 |
|
|
30 |
consts
|
14076
|
31 |
bag_of :: "i => i"
|
14052
|
32 |
|
|
33 |
primrec
|
|
34 |
"bag_of(Nil) = 0"
|
|
35 |
"bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
|
|
36 |
|
14076
|
37 |
|
|
38 |
text{*Definitions needed in Client.thy. We define a recursive predicate
|
|
39 |
using 0 and 1 to code the truth values.*}
|
|
40 |
consts all_distinct0 :: "i=>i"
|
|
41 |
primrec
|
14052
|
42 |
"all_distinct0(Nil) = 1"
|
|
43 |
"all_distinct0(Cons(a, l)) =
|
14076
|
44 |
(if a \<in> set_of_list(l) then 0 else all_distinct0(l))"
|
14052
|
45 |
|
14076
|
46 |
constdefs
|
|
47 |
all_distinct :: "i=>o"
|
|
48 |
"all_distinct(l) == all_distinct0(l)=1"
|
14052
|
49 |
|
|
50 |
constdefs
|
14076
|
51 |
state_of :: "i =>i" --{* coersion from anyting to state *}
|
|
52 |
"state_of(s) == if s \<in> state then s else st0"
|
14052
|
53 |
|
14076
|
54 |
lift :: "i =>(i=>i)" --{* simplifies the expression of programs*}
|
|
55 |
"lift(x) == %s. s`x"
|
14052
|
56 |
|
14076
|
57 |
text{* function to show that the set of variables is infinite *}
|
|
58 |
consts
|
|
59 |
nat_list_inj :: "i=>i"
|
|
60 |
nat_var_inj :: "i=>i"
|
|
61 |
var_inj :: "i=>i"
|
14052
|
62 |
|
|
63 |
defs
|
14076
|
64 |
nat_var_inj_def: "nat_var_inj(n) == Var(nat_list_inj(n))"
|
14052
|
65 |
primrec
|
|
66 |
"nat_list_inj(0) = Nil"
|
|
67 |
"nat_list_inj(succ(n)) = Cons(n, nat_list_inj(n))"
|
|
68 |
|
|
69 |
primrec
|
|
70 |
"var_inj(Var(l)) = length(l)"
|
|
71 |
|
14076
|
72 |
|
|
73 |
subsection{*Various simple lemmas*}
|
|
74 |
|
|
75 |
lemma Nclients_NbT_gt_0 [simp]: "0 < Nclients & 0 < NbT"
|
|
76 |
apply (cut_tac Nclients_pos NbT_pos)
|
|
77 |
apply (auto intro: Ord_0_lt)
|
|
78 |
done
|
|
79 |
|
|
80 |
lemma Nclients_NbT_not_0 [simp]: "Nclients \<noteq> 0 & NbT \<noteq> 0"
|
|
81 |
by (cut_tac Nclients_pos NbT_pos, auto)
|
|
82 |
|
|
83 |
lemma Nclients_type [simp,TC]: "Nclients\<in>nat"
|
|
84 |
by (cut_tac Nclients_pos NbT_pos, auto)
|
|
85 |
|
|
86 |
lemma NbT_type [simp,TC]: "NbT\<in>nat"
|
|
87 |
by (cut_tac Nclients_pos NbT_pos, auto)
|
|
88 |
|
|
89 |
lemma INT_Nclient_iff [iff]:
|
|
90 |
"b\<in>Inter(RepFun(Nclients, B)) <-> (\<forall>x\<in>Nclients. b\<in>B(x))"
|
|
91 |
apply (auto simp add: INT_iff)
|
|
92 |
apply (rule_tac x = 0 in exI)
|
|
93 |
apply (rule ltD, auto)
|
|
94 |
done
|
|
95 |
|
|
96 |
lemma setsum_fun_mono [rule_format]:
|
|
97 |
"n\<in>nat ==>
|
|
98 |
(\<forall>i\<in>nat. i<n --> f(i) $<= g(i)) -->
|
|
99 |
setsum(f, n) $<= setsum(g,n)"
|
|
100 |
apply (induct_tac "n", simp_all)
|
|
101 |
apply (subgoal_tac "Finite(x) & x\<notin>x")
|
|
102 |
prefer 2 apply (simp add: nat_into_Finite mem_not_refl, clarify)
|
|
103 |
apply (simp (no_asm_simp) add: succ_def)
|
|
104 |
apply (subgoal_tac "\<forall>i\<in>nat. i<x--> f(i) $<= g(i) ")
|
|
105 |
prefer 2 apply (force dest: leI)
|
|
106 |
apply (rule zadd_zle_mono, simp_all)
|
|
107 |
done
|
|
108 |
|
|
109 |
lemma tokens_type [simp,TC]: "l\<in>list(A) ==> tokens(l)\<in>nat"
|
|
110 |
by (erule list.induct, auto)
|
|
111 |
|
|
112 |
lemma tokens_mono_aux [rule_format]:
|
|
113 |
"xs\<in>list(A) ==> \<forall>ys\<in>list(A). <xs, ys>\<in>prefix(A)
|
|
114 |
--> tokens(xs) \<le> tokens(ys)"
|
|
115 |
apply (induct_tac "xs")
|
|
116 |
apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: prefix_def)
|
|
117 |
done
|
|
118 |
|
|
119 |
lemma tokens_mono: "<xs, ys>\<in>prefix(A) ==> tokens(xs) \<le> tokens(ys)"
|
|
120 |
apply (cut_tac prefix_type)
|
|
121 |
apply (blast intro: tokens_mono_aux)
|
|
122 |
done
|
|
123 |
|
|
124 |
lemma mono_tokens [iff]: "mono1(list(A), prefix(A), nat, Le,tokens)"
|
|
125 |
apply (unfold mono1_def)
|
|
126 |
apply (auto intro: tokens_mono simp add: Le_def)
|
|
127 |
done
|
|
128 |
|
|
129 |
lemma tokens_append [simp]:
|
|
130 |
"[| xs\<in>list(A); ys\<in>list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)"
|
|
131 |
apply (induct_tac "xs", auto)
|
|
132 |
done
|
|
133 |
|
|
134 |
subsection{*The function @{term bag_of}*}
|
|
135 |
|
|
136 |
lemma bag_of_type [simp,TC]: "l\<in>list(A) ==>bag_of(l)\<in>Mult(A)"
|
|
137 |
apply (induct_tac "l")
|
|
138 |
apply (auto simp add: Mult_iff_multiset)
|
|
139 |
done
|
|
140 |
|
|
141 |
lemma bag_of_multiset:
|
|
142 |
"l\<in>list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A"
|
|
143 |
apply (drule bag_of_type)
|
|
144 |
apply (auto simp add: Mult_iff_multiset)
|
|
145 |
done
|
|
146 |
|
|
147 |
lemma bag_of_append [simp]:
|
|
148 |
"[| xs\<in>list(A); ys\<in>list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)"
|
|
149 |
apply (induct_tac "xs")
|
|
150 |
apply (auto simp add: bag_of_multiset munion_assoc)
|
|
151 |
done
|
|
152 |
|
|
153 |
lemma bag_of_mono_aux [rule_format]:
|
|
154 |
"xs\<in>list(A) ==> \<forall>ys\<in>list(A). <xs, ys>\<in>prefix(A)
|
|
155 |
--> <bag_of(xs), bag_of(ys)>\<in>MultLe(A, r)"
|
|
156 |
apply (induct_tac "xs", simp_all, clarify)
|
|
157 |
apply (frule_tac l = ys in bag_of_multiset)
|
|
158 |
apply (auto intro: empty_le_MultLe simp add: prefix_def)
|
|
159 |
apply (rule munion_mono)
|
|
160 |
apply (force simp add: MultLe_def Mult_iff_multiset)
|
|
161 |
apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
|
|
162 |
done
|
|
163 |
|
|
164 |
lemma bag_of_mono [intro]:
|
|
165 |
"[| <xs, ys>\<in>prefix(A); xs\<in>list(A); ys\<in>list(A) |]
|
|
166 |
==> <bag_of(xs), bag_of(ys)>\<in>MultLe(A, r)"
|
|
167 |
apply (blast intro: bag_of_mono_aux)
|
|
168 |
done
|
|
169 |
|
|
170 |
lemma mono_bag_of [simp]:
|
|
171 |
"mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)"
|
|
172 |
by (auto simp add: mono1_def bag_of_type)
|
|
173 |
|
|
174 |
|
|
175 |
subsection{*The function @{term msetsum}*}
|
|
176 |
|
|
177 |
lemmas nat_into_Fin = eqpoll_refl [THEN [2] Fin_lemma]
|
|
178 |
|
|
179 |
lemma list_Int_length_Fin: "l \<in> list(A) ==> C Int length(l) \<in> Fin(length(l))"
|
|
180 |
apply (drule length_type)
|
|
181 |
apply (rule Fin_subset)
|
|
182 |
apply (rule Int_lower2)
|
|
183 |
apply (erule nat_into_Fin)
|
|
184 |
done
|
|
185 |
|
|
186 |
|
|
187 |
|
|
188 |
lemma mem_Int_imp_lt_length:
|
|
189 |
"[|xs \<in> list(A); k \<in> C \<inter> length(xs)|] ==> k < length(xs)"
|
|
190 |
apply (simp add: ltI)
|
|
191 |
done
|
|
192 |
|
|
193 |
|
|
194 |
lemma bag_of_sublist_lemma:
|
|
195 |
"[|C \<subseteq> nat; x \<in> A; xs \<in> list(A)|]
|
|
196 |
==> msetsum(\<lambda>i. {#nth(i, xs @ [x])#}, C \<inter> succ(length(xs)), A) =
|
|
197 |
(if length(xs) \<in> C then
|
|
198 |
{#x#} +# msetsum(\<lambda>x. {#nth(x, xs)#}, C \<inter> length(xs), A)
|
|
199 |
else msetsum(\<lambda>x. {#nth(x, xs)#}, C \<inter> length(xs), A))"
|
|
200 |
apply (simp add: subsetD nth_append lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
|
|
201 |
apply (simp add: Int_succ_right)
|
|
202 |
apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong, clarify)
|
|
203 |
apply (subst msetsum_cons)
|
|
204 |
apply (rule_tac [3] succI1)
|
|
205 |
apply (blast intro: list_Int_length_Fin subset_succI [THEN Fin_mono, THEN subsetD])
|
|
206 |
apply (simp add: mem_not_refl)
|
|
207 |
apply (simp add: nth_type lt_not_refl)
|
|
208 |
apply (blast intro: nat_into_Ord ltI length_type)
|
|
209 |
apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
|
|
210 |
done
|
|
211 |
|
|
212 |
lemma bag_of_sublist_lemma2:
|
|
213 |
"l\<in>list(A) ==>
|
|
214 |
C <= nat ==>
|
|
215 |
bag_of(sublist(l, C)) =
|
|
216 |
msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"
|
|
217 |
apply (erule list_append_induct)
|
|
218 |
apply (simp (no_asm))
|
|
219 |
apply (simp (no_asm_simp) add: sublist_append nth_append bag_of_sublist_lemma munion_commute bag_of_sublist_lemma msetsum_multiset munion_0)
|
|
220 |
done
|
|
221 |
|
|
222 |
|
|
223 |
lemma nat_Int_length_eq: "l \<in> list(A) ==> nat \<inter> length(l) = length(l)"
|
|
224 |
apply (rule Int_absorb1)
|
|
225 |
apply (rule OrdmemD, auto)
|
|
226 |
done
|
|
227 |
|
|
228 |
(*eliminating the assumption C<=nat*)
|
|
229 |
lemma bag_of_sublist:
|
|
230 |
"l\<in>list(A) ==>
|
|
231 |
bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)"
|
|
232 |
apply (subgoal_tac " bag_of (sublist (l, C Int nat)) = msetsum (%i. {#nth (i, l) #}, C Int length (l), A) ")
|
|
233 |
apply (simp add: sublist_Int_eq)
|
|
234 |
apply (simp add: bag_of_sublist_lemma2 Int_lower2 Int_assoc nat_Int_length_eq)
|
|
235 |
done
|
|
236 |
|
|
237 |
lemma bag_of_sublist_Un_Int:
|
|
238 |
"l\<in>list(A) ==>
|
|
239 |
bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) =
|
|
240 |
bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
|
|
241 |
apply (subgoal_tac "B Int C Int length (l) = (B Int length (l)) Int (C Int length (l))")
|
|
242 |
prefer 2 apply blast
|
|
243 |
apply (simp (no_asm_simp) add: bag_of_sublist Int_Un_distrib2 msetsum_Un_Int)
|
|
244 |
apply (rule msetsum_Un_Int)
|
|
245 |
apply (erule list_Int_length_Fin)+
|
|
246 |
apply (simp add: ltI nth_type)
|
|
247 |
done
|
|
248 |
|
|
249 |
|
|
250 |
lemma bag_of_sublist_Un_disjoint:
|
|
251 |
"[| l\<in>list(A); B Int C = 0 |]
|
|
252 |
==> bag_of(sublist(l, B Un C)) =
|
|
253 |
bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
|
|
254 |
by (simp add: bag_of_sublist_Un_Int [symmetric] bag_of_multiset)
|
|
255 |
|
|
256 |
|
|
257 |
lemma bag_of_sublist_UN_disjoint [rule_format]:
|
|
258 |
"[|Finite(I); \<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> A(i) \<inter> A(j) = 0;
|
|
259 |
l\<in>list(B) |]
|
|
260 |
==> bag_of(sublist(l, \<Union>i\<in>I. A(i))) =
|
|
261 |
(msetsum(%i. bag_of(sublist(l, A(i))), I, B)) "
|
|
262 |
apply (simp (no_asm_simp) del: UN_simps
|
|
263 |
add: UN_simps [symmetric] bag_of_sublist)
|
|
264 |
apply (subst msetsum_UN_disjoint [of _ _ _ "length (l)"])
|
|
265 |
apply (drule Finite_into_Fin, assumption)
|
|
266 |
prefer 3 apply force
|
|
267 |
apply (auto intro!: Fin_IntI2 Finite_into_Fin simp add: ltI nth_type length_type nat_into_Finite)
|
|
268 |
done
|
|
269 |
|
|
270 |
|
|
271 |
lemma part_ord_Lt [simp]: "part_ord(nat, Lt)"
|
|
272 |
apply (unfold part_ord_def Lt_def irrefl_def trans_on_def)
|
|
273 |
apply (auto intro: lt_trans)
|
|
274 |
done
|
|
275 |
|
|
276 |
subsubsection{*The function @{term all_distinct}*}
|
|
277 |
|
|
278 |
lemma all_distinct_Nil [simp]: "all_distinct(Nil)"
|
|
279 |
by (unfold all_distinct_def, auto)
|
|
280 |
|
|
281 |
lemma all_distinct_Cons [simp]:
|
|
282 |
"all_distinct(Cons(a,l)) <->
|
|
283 |
(a\<in>set_of_list(l) --> False) & (a \<notin> set_of_list(l) --> all_distinct(l))"
|
|
284 |
apply (unfold all_distinct_def)
|
|
285 |
apply (auto elim: list.cases)
|
|
286 |
done
|
|
287 |
|
|
288 |
subsubsection{*The function @{term state_of}*}
|
|
289 |
|
|
290 |
lemma state_of_state: "s\<in>state ==> state_of(s)=s"
|
|
291 |
by (unfold state_of_def, auto)
|
|
292 |
declare state_of_state [simp]
|
|
293 |
|
|
294 |
|
|
295 |
lemma state_of_idem: "state_of(state_of(s))=state_of(s)"
|
|
296 |
|
|
297 |
apply (unfold state_of_def, auto)
|
|
298 |
done
|
|
299 |
declare state_of_idem [simp]
|
|
300 |
|
|
301 |
|
|
302 |
lemma state_of_type [simp,TC]: "state_of(s)\<in>state"
|
|
303 |
by (unfold state_of_def, auto)
|
|
304 |
|
|
305 |
lemma lift_apply [simp]: "lift(x, s)=s`x"
|
|
306 |
by (simp add: lift_def)
|
|
307 |
|
|
308 |
|
|
309 |
(** Used in ClientImp **)
|
|
310 |
|
|
311 |
lemma gen_Increains_state_of_eq:
|
|
312 |
"Increasing(A, r, %s. f(state_of(s))) = Increasing(A, r, f)"
|
|
313 |
apply (unfold Increasing_def, auto)
|
|
314 |
done
|
|
315 |
|
|
316 |
lemmas Increasing_state_ofD1 =
|
|
317 |
gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD, standard]
|
|
318 |
lemmas Increasing_state_ofD2 =
|
|
319 |
gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD, standard]
|
|
320 |
|
|
321 |
lemma Follows_state_of_eq:
|
|
322 |
"Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =
|
|
323 |
Follows(A, r, f, g)"
|
|
324 |
apply (unfold Follows_def Increasing_def, auto)
|
|
325 |
done
|
|
326 |
|
|
327 |
lemmas Follows_state_ofD1 =
|
|
328 |
Follows_state_of_eq [THEN equalityD1, THEN subsetD, standard]
|
|
329 |
lemmas Follows_state_ofD2 =
|
|
330 |
Follows_state_of_eq [THEN equalityD2, THEN subsetD, standard]
|
|
331 |
|
|
332 |
lemma nat_list_inj_type: "n\<in>nat ==> nat_list_inj(n)\<in>list(nat)"
|
|
333 |
by (induct_tac "n", auto)
|
|
334 |
|
|
335 |
lemma length_nat_list_inj: "n\<in>nat ==> length(nat_list_inj(n)) = n"
|
|
336 |
by (induct_tac "n", auto)
|
|
337 |
|
|
338 |
lemma var_infinite_lemma:
|
|
339 |
"(\<lambda>x\<in>nat. nat_var_inj(x))\<in>inj(nat, var)"
|
|
340 |
apply (unfold nat_var_inj_def)
|
|
341 |
apply (rule_tac d = var_inj in lam_injective)
|
|
342 |
apply (auto simp add: var.intros nat_list_inj_type)
|
|
343 |
apply (simp add: length_nat_list_inj)
|
|
344 |
done
|
|
345 |
|
|
346 |
lemma nat_lepoll_var: "nat lepoll var"
|
|
347 |
apply (unfold lepoll_def)
|
|
348 |
apply (rule_tac x = " (\<lambda>x\<in>nat. nat_var_inj (x))" in exI)
|
|
349 |
apply (rule var_infinite_lemma)
|
|
350 |
done
|
|
351 |
|
|
352 |
(*Surely a simpler proof uses lepoll_Finite and the following lemma:*)
|
|
353 |
|
|
354 |
(*????Cardinal*)
|
|
355 |
lemma nat_not_Finite: "~Finite(nat)"
|
|
356 |
apply (unfold Finite_def, clarify)
|
|
357 |
apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp)
|
|
358 |
apply (insert Card_nat)
|
|
359 |
apply (simp add: Card_def)
|
|
360 |
apply (drule le_imp_subset)
|
|
361 |
apply (blast elim: mem_irrefl)
|
|
362 |
done
|
|
363 |
|
|
364 |
lemma var_not_Finite: "~Finite(var)"
|
|
365 |
apply (insert nat_not_Finite)
|
|
366 |
apply (blast intro: lepoll_Finite [OF nat_lepoll_var])
|
|
367 |
done
|
|
368 |
|
|
369 |
lemma not_Finite_imp_exist: "~Finite(A) ==> \<exists>x. x\<in>A"
|
|
370 |
apply (subgoal_tac "A\<noteq>0")
|
|
371 |
apply (auto simp add: Finite_0)
|
|
372 |
done
|
|
373 |
|
|
374 |
lemma Inter_Diff_var_iff:
|
|
375 |
"Finite(A) ==> b\<in>(Inter(RepFun(var-A, B))) <-> (\<forall>x\<in>var-A. b\<in>B(x))"
|
|
376 |
apply (subgoal_tac "\<exists>x. x\<in>var-A", auto)
|
|
377 |
apply (subgoal_tac "~Finite (var-A) ")
|
|
378 |
apply (drule not_Finite_imp_exist, auto)
|
|
379 |
apply (cut_tac var_not_Finite)
|
|
380 |
apply (erule swap)
|
|
381 |
apply (rule_tac B = A in Diff_Finite, auto)
|
|
382 |
done
|
|
383 |
|
|
384 |
lemma Inter_var_DiffD:
|
|
385 |
"[| b\<in>Inter(RepFun(var-A, B)); Finite(A); x\<in>var-A |] ==> b\<in>B(x)"
|
|
386 |
by (simp add: Inter_Diff_var_iff)
|
|
387 |
|
|
388 |
(* [| Finite(A); (\<forall>x\<in>var-A. b\<in>B(x)) |] ==> b\<in>Inter(RepFun(var-A, B)) *)
|
|
389 |
lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2, standard]
|
|
390 |
|
|
391 |
declare Inter_var_DiffI [intro!]
|
|
392 |
|
|
393 |
lemma Acts_subset_Int_Pow_simp [simp]:
|
|
394 |
"Acts(F)<= A \<inter> Pow(state*state) <-> Acts(F)<=A"
|
|
395 |
by (insert Acts_type [of F], auto)
|
|
396 |
|
|
397 |
lemma setsum_nsetsum_eq:
|
|
398 |
"[| Finite(A); \<forall>x\<in>A. g(x)\<in>nat |]
|
|
399 |
==> setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)"
|
|
400 |
apply (erule Finite_induct)
|
|
401 |
apply (auto simp add: int_of_add)
|
|
402 |
done
|
|
403 |
|
|
404 |
lemma nsetsum_cong:
|
|
405 |
"[| A=B; \<forall>x\<in>A. f(x)=g(x); \<forall>x\<in>A. g(x)\<in>nat; Finite(A) |]
|
|
406 |
==> nsetsum(f, A) = nsetsum(g, B)"
|
|
407 |
apply (subgoal_tac "$# nsetsum (f, A) = $# nsetsum (g, B)", simp)
|
|
408 |
apply (simp add: setsum_nsetsum_eq [symmetric] cong: setsum_cong)
|
|
409 |
done
|
|
410 |
|
14052
|
411 |
end
|