equal
deleted
inserted
replaced
294 "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In)) |
294 "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In)) |
295 guarantees |
295 guarantees |
296 (bag_of o merge.Out) Fols |
296 (bag_of o merge.Out) Fols |
297 (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o merge.In) s)" |
297 (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o merge.In) s)" |
298 apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto) |
298 apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto) |
299 apply (rule Follows_setsum) |
299 apply (rule Follows_sum) |
300 apply (cut_tac Merge_spec) |
300 apply (cut_tac Merge_spec) |
301 apply (auto simp add: merge_spec_def merge_follows_def o_def) |
301 apply (auto simp add: merge_spec_def merge_follows_def o_def) |
302 apply (drule guaranteesD) |
302 apply (drule guaranteesD) |
303 prefer 3 |
303 prefer 3 |
304 apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto) |
304 apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto) |
358 (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o distr.Out) s) |
358 (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o distr.Out) s) |
359 Fols |
359 Fols |
360 (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))" |
360 (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))" |
361 apply (rule guaranteesI, clarify) |
361 apply (rule guaranteesI, clarify) |
362 apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto) |
362 apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto) |
363 apply (rule Follows_setsum) |
363 apply (rule Follows_sum) |
364 apply (cut_tac Distrib_spec) |
364 apply (cut_tac Distrib_spec) |
365 apply (auto simp add: distr_spec_def distr_follows_def o_def) |
365 apply (auto simp add: distr_spec_def distr_follows_def o_def) |
366 apply (drule guaranteesD) |
366 apply (drule guaranteesD) |
367 prefer 3 |
367 prefer 3 |
368 apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto) |
368 apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto) |