author | wenzelm |
Sun, 15 Oct 2000 19:50:35 +0200 | |
changeset 10220 | 2a726de6e124 |
parent 10064 | 1a77667b21ef |
permissions | -rw-r--r-- |
9027 | 1 |
(* Title: HOL/UNITY/AllocImpl |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 2000 University of Cambridge |
|
5 |
||
6 |
Implementation of a multiple-client allocator from a single-client allocator |
|
7 |
*) |
|
8 |
||
9 |
AddIs [impOfSubs subset_preserves_o]; |
|
10 |
Addsimps [funPair_o_distrib]; |
|
11 |
Addsimps [Always_INT_distrib]; |
|
12 |
Delsimps [o_apply]; |
|
13 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
14 |
Open_locale "Merge"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
15 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
16 |
val Merge = thm "Merge_spec"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
17 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
18 |
Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
19 |
by (cut_facts_tac [Merge] 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
20 |
by (auto_tac (claset(), |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
21 |
simpset() addsimps [merge_spec_def, merge_allowed_acts_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
22 |
Allowed_def, safety_prop_Acts_iff])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
23 |
qed "Merge_Allowed"; |
9110 | 24 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
25 |
Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
26 |
\ M : Allowed G)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
27 |
by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
28 |
qed "M_ok_iff"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
29 |
AddIffs [M_ok_iff]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
30 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
31 |
Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
32 |
\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
33 |
by (cut_facts_tac [Merge] 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
34 |
by (force_tac (claset() addDs [guaranteesD], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
35 |
simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1); |
9027 | 36 |
qed "Merge_Always_Out_eq_iOut"; |
37 |
||
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
38 |
Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
39 |
\ ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
40 |
by (cut_facts_tac [Merge] 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
41 |
by (force_tac (claset() addDs [guaranteesD], |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
42 |
simpset() addsimps [merge_spec_def, merge_bounded_def]) 1); |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
43 |
qed "Merge_Bounded"; |
9091 | 44 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
45 |
Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \ |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
46 |
\ ==> M Join G : Always \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
47 |
\ {s. setsum (%i. bag_of (sublist (merge.Out s) \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
48 |
\ {k. k < length (iOut s) & iOut s ! k = i})) \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
49 |
\ (lessThan Nclients) = \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
50 |
\ (bag_of o merge.Out) s}"; |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
51 |
by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I, |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
52 |
UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
53 |
by Auto_tac; |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
54 |
by (stac (bag_of_sublist_UN_disjoint RS sym) 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
55 |
by (Simp_tac 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
56 |
by (Blast_tac 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
57 |
by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
58 |
by (subgoal_tac |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
59 |
"(UN i:lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
60 |
\ lessThan (length (iOut x))" 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
61 |
by (Blast_tac 2); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
62 |
by (asm_simp_tac (simpset() addsimps [o_def]) 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
63 |
qed "Merge_Bag_Follows_lemma"; |
9027 | 64 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
65 |
Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
66 |
\ guarantees \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
67 |
\ (bag_of o merge.Out) Fols \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
68 |
\ (%s. setsum (%i. (bag_of o sub i o merge.In) s) \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
69 |
\ (lessThan Nclients))"; |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
70 |
by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
71 |
by Auto_tac; |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
72 |
by (rtac Follows_setsum 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
73 |
by (cut_facts_tac [Merge] 1); |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
74 |
by (auto_tac (claset(), |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
75 |
simpset() addsimps [merge_spec_def, merge_follows_def, o_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
76 |
by (dtac guaranteesD 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
77 |
by (best_tac |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
78 |
(claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
79 |
by Auto_tac; |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
80 |
qed "Merge_Bag_Follows"; |
9091 | 81 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
82 |
Close_locale "Merge"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
83 |
|
9091 | 84 |
|
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
85 |
(** Distributor **) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
86 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
87 |
Open_locale "Distrib"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
88 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
89 |
val Distrib = thm "Distrib_spec"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
90 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
91 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
92 |
Goal "D : Increasing distr.In Int Increasing distr.iIn Int \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
93 |
\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
94 |
\ guarantees \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
95 |
\ (INT i : lessThan Nclients. Increasing (sub i o distr.Out))"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
96 |
by (cut_facts_tac [Distrib] 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
97 |
by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
98 |
by (Clarify_tac 1); |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
99 |
by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1] |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
100 |
addDs [guaranteesD]) 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
101 |
qed "Distr_Increasing_Out"; |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
102 |
|
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
103 |
Goal "[| G : preserves distr.Out; \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
104 |
\ D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
105 |
\ ==> D Join G : Always \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
106 |
\ {s. setsum (%i. bag_of (sublist (distr.In s) \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
107 |
\ {k. k < length (iIn s) & iIn s ! k = i})) \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
108 |
\ (lessThan Nclients) = \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
109 |
\ bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"; |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
110 |
by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
111 |
by Auto_tac; |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
112 |
by (stac (bag_of_sublist_UN_disjoint RS sym) 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
113 |
by (Simp_tac 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
114 |
by (Blast_tac 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
115 |
by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
116 |
by (subgoal_tac |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
117 |
"(UN i:lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
118 |
\ lessThan (length (iIn x))" 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
119 |
by (Blast_tac 2); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
120 |
by (Asm_simp_tac 1); |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
121 |
qed "Distr_Bag_Follows_lemma"; |
9027 | 122 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
123 |
Goal "D ok G = (G: preserves distr.Out & D : Allowed G)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
124 |
by (cut_facts_tac [Distrib] 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
125 |
by (auto_tac (claset(), |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
126 |
simpset() addsimps [distr_spec_def, distr_allowed_acts_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
127 |
Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
128 |
qed "D_ok_iff"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
129 |
AddIffs [D_ok_iff]; |
9027 | 130 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
131 |
Goal |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
132 |
"D : Increasing distr.In Int Increasing distr.iIn Int \ |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
133 |
\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \ |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
134 |
\ guarantees \ |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
135 |
\ (INT i : lessThan Nclients. \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
136 |
\ (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
137 |
\ Fols \ |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
138 |
\ (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"; |
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
139 |
by (rtac guaranteesI 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
140 |
by (Clarify_tac 1); |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
141 |
by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
142 |
by Auto_tac; |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
143 |
by (rtac Follows_setsum 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
144 |
by (cut_facts_tac [Distrib] 1); |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
145 |
by (auto_tac (claset(), |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
146 |
simpset() addsimps [distr_spec_def, distr_follows_def, o_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
147 |
by (dtac guaranteesD 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
148 |
by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
149 |
by Auto_tac; |
9106
0fe9200f64bd
working proofs of the basic merge and distributor properties
paulson
parents:
9091
diff
changeset
|
150 |
qed "Distr_Bag_Follows"; |
9027 | 151 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
152 |
Close_locale "Distrib"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
153 |
|
9110 | 154 |
|
155 |
Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s}) \ |
|
156 |
\ <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}"; |
|
157 |
by (induct_tac "n" 1); |
|
158 |
by (auto_tac (claset(), simpset() addsimps [lessThan_Suc])); |
|
159 |
qed "alloc_refinement_lemma"; |
|
160 |
||
161 |
Goal |
|
162 |
"(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \ |
|
163 |
\ Increasing (sub i o allocRel)) \ |
|
164 |
\ Int \ |
|
165 |
\ Always {s. ALL i. i<Nclients --> \ |
|
166 |
\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)} \ |
|
167 |
\ Int \ |
|
168 |
\ (INT i : lessThan Nclients. \ |
|
169 |
\ INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} \ |
|
170 |
\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s}) \ |
|
9150 | 171 |
\ <= \ |
9110 | 172 |
\(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \ |
173 |
\ Increasing (sub i o allocRel)) \ |
|
174 |
\ Int \ |
|
175 |
\ Always {s. ALL i. i<Nclients --> \ |
|
176 |
\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)} \ |
|
177 |
\ Int \ |
|
178 |
\ (INT hf. (INT i : lessThan Nclients. \ |
|
179 |
\ {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \ |
|
180 |
\ LeadsTo {s. setsum (%i. tokens (hf i)) (lessThan Nclients) <= \ |
|
181 |
\ setsum (%i. (tokens o sub i o allocRel)s) (lessThan Nclients) })"; |
|
182 |
by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib])); |
|
183 |
by (rename_tac "F hf" 1); |
|
184 |
by (rtac ([Finite_stable_completion, alloc_refinement_lemma] |
|
185 |
MRS LeadsTo_weaken_R) 1); |
|
186 |
by (Blast_tac 1); |
|
187 |
by (Blast_tac 1); |
|
188 |
by (subgoal_tac "F : Increasing (tokens o (sub i o allocRel))" 1); |
|
189 |
by (blast_tac |
|
190 |
(claset() addIs [impOfSubs (mono_tokens RS mono_Increasing_o)]) 2); |
|
191 |
by (asm_full_simp_tac (simpset() addsimps [Increasing_def, o_assoc]) 1); |
|
192 |
qed "alloc_refinement"; |
|
193 |
||
194 |