author | paulson |
Mon, 15 May 2000 10:34:51 +0200 | |
changeset 8872 | 0ff5d55205a4 |
parent 8849 | f1933a670ae4 |
child 8930 | cb419b8498e5 |
permissions | -rw-r--r-- |
6828 | 1 |
(* Title: HOL/UNITY/Alloc |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Specification of Chandy and Charpentier's Allocator |
|
7 |
*) |
|
8 |
||
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
9 |
AddIs [impOfSubs subset_preserves_o]; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
10 |
Addsimps [funPair_o_distrib]; |
8327 | 11 |
Addsimps [Always_INT_distrib]; |
8067 | 12 |
Delsimps [o_apply]; |
13 |
||
8314 | 14 |
(*Eliminate the "o" operator*) |
7841 | 15 |
val o_simp = simplify (simpset() addsimps [o_def]); |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
16 |
|
8314 | 17 |
(*For rewriting of specifications related by "guarantees"*) |
18 |
Addsimps [rename_image_constrains, rename_image_stable, |
|
19 |
rename_image_increasing, rename_image_invariant, |
|
20 |
rename_image_Constrains, rename_image_Stable, |
|
21 |
rename_image_Increasing, rename_image_Always, |
|
8327 | 22 |
rename_image_leadsTo, rename_image_LeadsTo, |
23 |
rename_preserves, |
|
24 |
bij_image_INT, bij_is_inj RS image_Int, bij_image_Collect_eq]; |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
25 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
26 |
(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
27 |
fun list_of_Int th = |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
28 |
(list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2)) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
29 |
handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2)) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
30 |
handle THM _ => (list_of_Int (th RS INT_D)) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
31 |
handle THM _ => [th]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
32 |
|
8314 | 33 |
(*Used just once, for Alloc_Increasing*) |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
34 |
val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec); |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
35 |
fun normalize th = |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
36 |
normalize (th RS spec |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
37 |
handle THM _ => th RS lessThanBspec |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
38 |
handle THM _ => th RS bspec |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
39 |
handle THM _ => th RS (guarantees_INT_right_iff RS iffD1)) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
40 |
handle THM _ => th; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
41 |
|
8067 | 42 |
|
7538 | 43 |
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n"; |
44 |
by (induct_tac "n" 1); |
|
45 |
by Auto_tac; |
|
46 |
by (dres_inst_tac [("x","n")] bspec 1); |
|
47 |
by Auto_tac; |
|
48 |
by (arith_tac 1); |
|
49 |
qed_spec_mp "sum_mono"; |
|
50 |
||
7540 | 51 |
Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys"; |
52 |
by (induct_tac "ys" 1); |
|
53 |
by (auto_tac (claset(), simpset() addsimps [prefix_Cons])); |
|
54 |
qed_spec_mp "tokens_mono_prefix"; |
|
55 |
||
56 |
Goalw [mono_def] "mono tokens"; |
|
57 |
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); |
|
58 |
qed "mono_tokens"; |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
59 |
|
8314 | 60 |
|
61 |
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***) |
|
62 |
||
8849 | 63 |
val record_auto_tac = |
64 |
auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper, |
|
65 |
simpset() addsimps [sysOfAlloc_def, sysOfClient_def, |
|
66 |
client_map_def, non_extra_def, funPair_def, |
|
67 |
o_apply, Let_def]); |
|
68 |
||
69 |
||
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
70 |
Goalw [sysOfAlloc_def, Let_def] "inj sysOfAlloc"; |
6828 | 71 |
by (rtac injI 1); |
8849 | 72 |
by record_auto_tac; |
6828 | 73 |
qed "inj_sysOfAlloc"; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
74 |
AddIffs [inj_sysOfAlloc]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
75 |
|
8314 | 76 |
(*We need the inverse; also having it simplifies the proof of surjectivity*) |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
77 |
Goal "!!s. inv sysOfAlloc s = \ |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
78 |
\ (| allocGiv = allocGiv s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
79 |
\ allocAsk = allocAsk s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
80 |
\ allocRel = allocRel s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
81 |
\ allocState_u.extra = (client s, extra s) |)"; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
82 |
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); |
8849 | 83 |
by record_auto_tac; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
84 |
qed "inv_sysOfAlloc_eq"; |
7538 | 85 |
Addsimps [inv_sysOfAlloc_eq]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
86 |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
87 |
Goal "surj sysOfAlloc"; |
8327 | 88 |
by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); |
8849 | 89 |
by record_auto_tac; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
90 |
qed "surj_sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
91 |
AddIffs [surj_sysOfAlloc]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
92 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
93 |
Goal "bij sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
94 |
by (blast_tac (claset() addIs [bijI]) 1); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
95 |
qed "bij_sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
96 |
AddIffs [bij_sysOfAlloc]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
97 |
|
8314 | 98 |
|
99 |
(*** bijectivity of sysOfClient ***) |
|
100 |
||
7347 | 101 |
Goalw [sysOfClient_def] "inj sysOfClient"; |
102 |
by (rtac injI 1); |
|
8849 | 103 |
by record_auto_tac; |
7347 | 104 |
qed "inj_sysOfClient"; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
105 |
AddIffs [inj_sysOfClient]; |
6828 | 106 |
|
7347 | 107 |
Goal "!!s. inv sysOfClient s = \ |
108 |
\ (client s, \ |
|
109 |
\ (| allocGiv = allocGiv s, \ |
|
110 |
\ allocAsk = allocAsk s, \ |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
111 |
\ allocRel = allocRel s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
112 |
\ allocState_u.extra = systemState.extra s|) )"; |
7347 | 113 |
by (rtac (inj_sysOfClient RS inv_f_eq) 1); |
8849 | 114 |
by record_auto_tac; |
7365 | 115 |
qed "inv_sysOfClient_eq"; |
7689 | 116 |
Addsimps [inv_sysOfClient_eq]; |
6837 | 117 |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
118 |
Goal "surj sysOfClient"; |
8327 | 119 |
by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); |
8849 | 120 |
by record_auto_tac; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
121 |
qed "surj_sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
122 |
AddIffs [surj_sysOfClient]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
123 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
124 |
Goal "bij sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
125 |
by (blast_tac (claset() addIs [bijI]) 1); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
126 |
qed "bij_sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
127 |
AddIffs [bij_sysOfClient]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
128 |
|
6837 | 129 |
|
8314 | 130 |
(*** bijectivity of client_map ***) |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
131 |
|
8849 | 132 |
Goalw [inj_on_def] "inj client_map"; |
133 |
by record_auto_tac; |
|
8314 | 134 |
qed "inj_client_map"; |
135 |
AddIffs [inj_client_map]; |
|
136 |
||
137 |
Goal "!!s. inv client_map s = \ |
|
138 |
\ (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, \ |
|
139 |
\ clientState_u.extra = y|)) s"; |
|
140 |
by (rtac (inj_client_map RS inv_f_eq) 1); |
|
8849 | 141 |
by record_auto_tac; |
8314 | 142 |
qed "inv_client_map_eq"; |
143 |
Addsimps [inv_client_map_eq]; |
|
144 |
||
145 |
Goal "surj client_map"; |
|
8327 | 146 |
by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); |
8849 | 147 |
by record_auto_tac; |
8314 | 148 |
qed "surj_client_map"; |
149 |
AddIffs [surj_client_map]; |
|
150 |
||
151 |
Goal "bij client_map"; |
|
152 |
by (blast_tac (claset() addIs [bijI]) 1); |
|
153 |
qed "bij_client_map"; |
|
154 |
AddIffs [bij_client_map]; |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
155 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
156 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
157 |
(** o-simprules for client_map **) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
158 |
|
8327 | 159 |
Goalw [client_map_def] "fst o client_map = non_extra"; |
160 |
by (rtac fst_o_funPair 1); |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
161 |
qed "fst_o_client_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
162 |
Addsimps (make_o_equivs fst_o_client_map); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
163 |
|
8327 | 164 |
Goalw [client_map_def] "snd o client_map = clientState_u.extra"; |
165 |
by (rtac snd_o_funPair 1); |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
166 |
qed "snd_o_client_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
167 |
Addsimps (make_o_equivs snd_o_client_map); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
168 |
|
8327 | 169 |
(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **) |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
170 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
171 |
Goal "client o sysOfAlloc = fst o allocState_u.extra "; |
8849 | 172 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
173 |
qed "client_o_sysOfAlloc"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
174 |
Addsimps (make_o_equivs client_o_sysOfAlloc); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
175 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
176 |
Goal "allocGiv o sysOfAlloc = allocGiv"; |
8849 | 177 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
178 |
qed "allocGiv_o_sysOfAlloc_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
179 |
Addsimps (make_o_equivs allocGiv_o_sysOfAlloc_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
180 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
181 |
Goal "allocAsk o sysOfAlloc = allocAsk"; |
8849 | 182 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
183 |
qed "allocAsk_o_sysOfAlloc_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
184 |
Addsimps (make_o_equivs allocAsk_o_sysOfAlloc_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
185 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
186 |
Goal "allocRel o sysOfAlloc = allocRel"; |
8849 | 187 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
188 |
qed "allocRel_o_sysOfAlloc_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
189 |
Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
190 |
|
8327 | 191 |
(** o-simprules for sysOfClient [MUST BE AUTOMATED] **) |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
192 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
193 |
Goal "client o sysOfClient = fst"; |
8849 | 194 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
195 |
qed "client_o_sysOfClient"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
196 |
Addsimps (make_o_equivs client_o_sysOfClient); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
197 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
198 |
Goal "allocGiv o sysOfClient = allocGiv o snd "; |
8849 | 199 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
200 |
qed "allocGiv_o_sysOfClient_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
201 |
Addsimps (make_o_equivs allocGiv_o_sysOfClient_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
202 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
203 |
Goal "allocAsk o sysOfClient = allocAsk o snd "; |
8849 | 204 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
205 |
qed "allocAsk_o_sysOfClient_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
206 |
Addsimps (make_o_equivs allocAsk_o_sysOfClient_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
207 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
208 |
Goal "allocRel o sysOfClient = allocRel o snd "; |
8849 | 209 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
210 |
qed "allocRel_o_sysOfClient_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
211 |
Addsimps (make_o_equivs allocRel_o_sysOfClient_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
212 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
213 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
214 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
215 |
(** |
7365 | 216 |
Open_locale "System"; |
217 |
||
218 |
val Alloc = thm "Alloc"; |
|
219 |
val Client = thm "Client"; |
|
220 |
val Network = thm "Network"; |
|
221 |
val System_def = thm "System_def"; |
|
8314 | 222 |
|
223 |
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect |
|
224 |
exporting it from the locale*) |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
225 |
**) |
7365 | 226 |
|
227 |
AddIffs [finite_lessThan]; |
|
228 |
||
229 |
(*Client : <unfolded specification> *) |
|
230 |
val Client_Spec = |
|
231 |
rewrite_rule [client_spec_def, client_increasing_def, |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
232 |
client_bounded_def, client_progress_def, |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
233 |
client_preserves_def] Client; |
7365 | 234 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
235 |
val [Client_Increasing_ask, Client_Increasing_rel, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
236 |
Client_Bounded, Client_Progress, Client_preserves_giv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
237 |
Client_preserves_extra] = |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
238 |
Client_Spec |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
239 |
|> simplify (simpset() addsimps [guarantees_Int_right]) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
240 |
|> list_of_Int; |
7365 | 241 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
242 |
AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
243 |
Client_preserves_giv, Client_preserves_extra]; |
6828 | 244 |
|
245 |
||
7365 | 246 |
(*Network : <unfolded specification> *) |
247 |
val Network_Spec = |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
248 |
rewrite_rule [network_spec_def, network_ask_def, network_giv_def, |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
249 |
network_rel_def, network_preserves_def] Network; |
7365 | 250 |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
251 |
val [Network_Ask, Network_Giv, Network_Rel, |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
252 |
Network_preserves_allocGiv, Network_preserves_rel_ask] = |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
253 |
list_of_Int Network_Spec; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
254 |
|
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
255 |
AddIffs [Network_preserves_allocGiv]; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
256 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
257 |
Addsimps (Network_preserves_rel_ask |> simplify (simpset()) |> list_of_Int); |
7365 | 258 |
|
259 |
||
260 |
(*Alloc : <unfolded specification> *) |
|
261 |
val Alloc_Spec = |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
262 |
rewrite_rule [alloc_spec_def, alloc_increasing_def, alloc_safety_def, |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
263 |
alloc_progress_def, alloc_preserves_def] Alloc; |
7365 | 264 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
265 |
val [Alloc_Increasing_0, Alloc_Safety, |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
266 |
Alloc_Progress, Alloc_preserves] = list_of_Int Alloc_Spec; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
267 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
268 |
(*Strip off the INT in the guarantees postcondition*) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
269 |
val Alloc_Increasing = normalize Alloc_Increasing_0; |
7365 | 270 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
271 |
AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
272 |
|
8327 | 273 |
(** Components lemmas [MUST BE AUTOMATED] **) |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
274 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
275 |
Goal "Network Join \ |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
276 |
\ ((rename sysOfClient \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
277 |
\ (plam x: lessThan Nclients. rename client_map Client)) Join \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
278 |
\ rename sysOfAlloc Alloc) \ |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
279 |
\ = System"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
280 |
by (simp_tac (simpset() addsimps System_def::Join_ac) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
281 |
qed "Network_component_System"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
282 |
|
8314 | 283 |
Goal "(rename sysOfClient \ |
284 |
\ (plam x: lessThan Nclients. rename client_map Client)) Join \ |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
285 |
\ (Network Join rename sysOfAlloc Alloc) = System"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
286 |
by (simp_tac (simpset() addsimps System_def::Join_ac) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
287 |
qed "Client_component_System"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
288 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
289 |
Goal "rename sysOfAlloc Alloc Join \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
290 |
\ ((rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)) Join \ |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
291 |
\ Network) = System"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
292 |
by (simp_tac (simpset() addsimps System_def::Join_ac) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
293 |
qed "Alloc_component_System"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
294 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
295 |
AddIffs [Client_component_System, Network_component_System, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
296 |
Alloc_component_System]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
297 |
|
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
298 |
(** These preservation laws should be generated automatically **) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
299 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
300 |
AddIs [impOfSubs subset_preserves_o]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
301 |
Addsimps [impOfSubs subset_preserves_o]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
302 |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
303 |
|
8872 | 304 |
(*The proofs of rename_Client_Increasing, rename_Client_Bounded and |
305 |
rename_Client_Progress are similar. All require copying out the original |
|
306 |
Client property. A forward proof can be constructed as follows: |
|
8327 | 307 |
|
308 |
Client_Increasing_ask RS |
|
309 |
(bij_client_map RS rename_rename_guarantees_eq RS iffD2) |
|
310 |
RS (lift_lift_guarantees_eq RS iffD2) |
|
311 |
RS guarantees_PLam_I |
|
312 |
RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2) |
|
313 |
|> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def, |
|
314 |
surj_rename RS surj_range]); |
|
315 |
||
316 |
However, the "preserves" property remains to be discharged, and the unfolding |
|
317 |
of "o" and "sub" complicates subsequent reasoning. |
|
8872 | 318 |
|
319 |
The following tactic works for all three proofs, though it certainly looks |
|
320 |
ad-hoc! |
|
8327 | 321 |
*) |
8872 | 322 |
val rename_client_map_tac = |
323 |
EVERY [ |
|
324 |
simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1, |
|
325 |
rtac guarantees_PLam_I 1, |
|
326 |
assume_tac 2, |
|
327 |
(*preserves: routine reasoning*) |
|
328 |
asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2, |
|
329 |
(*the guarantee for "lift i (rename client_map Client)" *) |
|
330 |
asm_simp_tac |
|
331 |
(simpset() addsimps [lift_guarantees_eq_lift_inv, |
|
332 |
rename_guarantees_eq_rename_inv, |
|
333 |
bij_imp_bij_inv, surj_rename RS surj_range, |
|
334 |
inv_inv_eq]) 1, |
|
335 |
asm_simp_tac |
|
336 |
(simpset() addsimps [o_def, non_extra_def, guarantees_Int_right]) 1]; |
|
337 |
||
338 |
||
339 |
(*Lifting Client_Increasing to systemState*) |
|
340 |
Goal "i : I \ |
|
341 |
\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \ |
|
342 |
\ UNIV \ |
|
343 |
\ guarantees[(funPair rel ask) o sub i o client] \ |
|
344 |
\ Increasing (ask o sub i o client) Int \ |
|
345 |
\ Increasing (rel o sub i o client)"; |
|
346 |
by rename_client_map_tac; |
|
347 |
qed "rename_Client_Increasing"; |
|
8327 | 348 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
349 |
Goal "i < Nclients \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
350 |
\ ==> System : Increasing (ask o sub i o client) Int \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
351 |
\ Increasing (rel o sub i o client)"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
352 |
by (rtac ([rename_Client_Increasing, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
353 |
Client_component_System] MRS component_guaranteesD) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
354 |
by Auto_tac; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
355 |
qed "System_Increasing"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
356 |
|
8327 | 357 |
bind_thm ("rename_guarantees_sysOfAlloc_I", |
358 |
bij_sysOfAlloc RS rename_rename_guarantees_eq RS iffD2); |
|
359 |
||
360 |
||
8314 | 361 |
(*Lifting Alloc_Increasing up to the level of systemState*) |
362 |
val rename_Alloc_Increasing = |
|
8327 | 363 |
Alloc_Increasing RS rename_guarantees_sysOfAlloc_I |
364 |
|> simplify (simpset() addsimps [surj_rename RS surj_range, o_def]); |
|
8314 | 365 |
|
7841 | 366 |
Goalw [System_def] |
367 |
"i < Nclients ==> System : Increasing (sub i o allocGiv)"; |
|
8314 | 368 |
by (simp_tac (simpset() addsimps [o_def]) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
369 |
by (rtac (rename_Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1); |
7841 | 370 |
by Auto_tac; |
371 |
qed "System_Increasing_allocGiv"; |
|
7365 | 372 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
373 |
AddSIs (list_of_Int System_Increasing); |
6828 | 374 |
|
7841 | 375 |
(** Follows consequences. |
376 |
The "Always (INT ...) formulation expresses the general safety property |
|
377 |
and allows it to be combined using Always_Int_rule below. **) |
|
378 |
||
8067 | 379 |
Goal |
380 |
"i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))"; |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
381 |
by (auto_tac (claset() addSIs [Network_Rel RS component_guaranteesD], |
8067 | 382 |
simpset())); |
383 |
qed "System_Follows_rel"; |
|
384 |
||
385 |
Goal |
|
386 |
"i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))"; |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
387 |
by (auto_tac (claset() addSIs [Network_Ask RS component_guaranteesD], |
8067 | 388 |
simpset())); |
389 |
qed "System_Follows_ask"; |
|
390 |
||
391 |
Goal |
|
392 |
"i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)"; |
|
393 |
by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD, |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
394 |
rename_Alloc_Increasing RS component_guaranteesD], |
8067 | 395 |
simpset())); |
8314 | 396 |
by (ALLGOALS (simp_tac (simpset() addsimps [o_def, non_extra_def]))); |
397 |
by (auto_tac |
|
398 |
(claset() addSIs [rename_Alloc_Increasing RS component_guaranteesD], |
|
399 |
simpset())); |
|
8067 | 400 |
qed "System_Follows_allocGiv"; |
401 |
||
7841 | 402 |
Goal "System : Always (INT i: lessThan Nclients. \ |
403 |
\ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})"; |
|
8327 | 404 |
by Auto_tac; |
8067 | 405 |
by (etac (System_Follows_allocGiv RS Follows_Bounded) 1); |
7841 | 406 |
qed "Always_giv_le_allocGiv"; |
407 |
||
408 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
409 |
\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})"; |
|
8327 | 410 |
by Auto_tac; |
8067 | 411 |
by (etac (System_Follows_ask RS Follows_Bounded) 1); |
7841 | 412 |
qed "Always_allocAsk_le_ask"; |
413 |
||
414 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
415 |
\ {s. (sub i o allocRel) s <= (rel o sub i o client) s})"; |
|
8067 | 416 |
by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel], |
8327 | 417 |
simpset())); |
7841 | 418 |
qed "Always_allocRel_le_rel"; |
419 |
||
420 |
||
421 |
(*** Proof of the safety property (1) ***) |
|
422 |
||
423 |
(*safety (1), step 1 is System_Increasing_rel*) |
|
424 |
||
7689 | 425 |
(*safety (1), step 2*) |
7365 | 426 |
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)"; |
8067 | 427 |
by (etac (System_Follows_rel RS Follows_Increasing1) 1); |
7365 | 428 |
qed "System_Increasing_allocRel"; |
6828 | 429 |
|
8314 | 430 |
(*Lifting Alloc_safety up to the level of systemState*) |
431 |
val rename_Alloc_Safety = |
|
8327 | 432 |
Alloc_Safety RS rename_guarantees_sysOfAlloc_I |
433 |
|> simplify (simpset() addsimps [o_def]); |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
434 |
|
7689 | 435 |
(*safety (1), step 3*) |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
436 |
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
437 |
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; |
8327 | 438 |
by (simp_tac (simpset() addsimps [o_apply]) 1); |
439 |
by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1); |
|
440 |
by (auto_tac (claset(), |
|
441 |
simpset() addsimps [o_simp System_Increasing_allocRel])); |
|
7538 | 442 |
qed "System_sum_bounded"; |
7537 | 443 |
|
8314 | 444 |
|
7841 | 445 |
(** Follows reasoning **) |
446 |
||
7540 | 447 |
Goal "System : Always (INT i: lessThan Nclients. \ |
448 |
\ {s. (tokens o giv o sub i o client) s \ |
|
449 |
\ <= (tokens o sub i o allocGiv) s})"; |
|
7841 | 450 |
by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1); |
8067 | 451 |
by (auto_tac (claset() addIs [tokens_mono_prefix], |
452 |
simpset() addsimps [o_apply])); |
|
7841 | 453 |
qed "Always_tokens_giv_le_allocGiv"; |
7540 | 454 |
|
455 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
456 |
\ {s. (tokens o sub i o allocRel) s \ |
|
457 |
\ <= (tokens o rel o sub i o client) s})"; |
|
7841 | 458 |
by (rtac (Always_allocRel_le_rel RS Always_weaken) 1); |
8067 | 459 |
by (auto_tac (claset() addIs [tokens_mono_prefix], |
460 |
simpset() addsimps [o_apply])); |
|
7841 | 461 |
qed "Always_tokens_allocRel_le_rel"; |
7540 | 462 |
|
7841 | 463 |
(*safety (1), step 4 (final result!) *) |
8128 | 464 |
Goalw [system_safety_def] "System : system_safety"; |
7841 | 465 |
by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv, |
466 |
Always_tokens_allocRel_le_rel] RS Always_weaken) 1); |
|
7538 | 467 |
by Auto_tac; |
7540 | 468 |
by (rtac (sum_mono RS order_trans) 1); |
469 |
by (dtac order_trans 2); |
|
470 |
by (rtac ([order_refl, sum_mono] MRS add_le_mono) 2); |
|
471 |
by (assume_tac 3); |
|
7482 | 472 |
by Auto_tac; |
7540 | 473 |
qed "System_safety"; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
474 |
|
7689 | 475 |
|
476 |
(*** Proof of the progress property (2) ***) |
|
477 |
||
7965 | 478 |
(*Now there are proofs identical to System_Increasing_rel and |
7689 | 479 |
System_Increasing_allocRel: tactics needed!*) |
480 |
||
7841 | 481 |
(*progress (2), step 1 is System_Increasing_ask and System_Increasing_rel*) |
7689 | 482 |
|
7841 | 483 |
(*progress (2), step 2; see also System_Increasing_allocRel*) |
7689 | 484 |
Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)"; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
485 |
by (etac (System_Follows_ask RS Follows_Increasing1) 1); |
7689 | 486 |
qed "System_Increasing_allocAsk"; |
487 |
||
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
488 |
(*progress (2), step 3*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
489 |
(*All this trouble just to lift "Client_Bounded" to systemState |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
490 |
(though it is similar to that for Client_Increasing*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
491 |
Goal "i : I \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
492 |
\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
493 |
\ UNIV \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
494 |
\ guarantees[ask o sub i o client] \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
495 |
\ Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}"; |
8872 | 496 |
by rename_client_map_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
497 |
qed "rename_Client_Bounded"; |
7841 | 498 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
499 |
Goal "i < Nclients \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
500 |
\ ==> System : Always \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
501 |
\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}"; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
502 |
by (rtac ([rename_Client_Bounded, |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
503 |
Client_component_System] MRS component_guaranteesD) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
504 |
by Auto_tac; |
7841 | 505 |
qed "System_Bounded_ask"; |
506 |
||
507 |
(*progress (2), step 4*) |
|
508 |
Goal "System : Always {s. ALL i : lessThan Nclients. \ |
|
509 |
\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}"; |
|
510 |
by (auto_tac (claset(), |
|
8327 | 511 |
simpset() addsimps [Collect_ball_eq])); |
7841 | 512 |
by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask] |
513 |
RS Always_weaken) 1); |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
514 |
by (auto_tac (claset() addDs [set_mono], simpset())); |
7841 | 515 |
qed "System_Bounded_allocAsk"; |
516 |
||
7965 | 517 |
(*progress (2), step 5 is System_Increasing_allocGiv*) |
7841 | 518 |
|
7965 | 519 |
(*progress (2), step 6*) |
7841 | 520 |
Goal "i < Nclients ==> System : Increasing (giv o sub i o client)"; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
521 |
by (etac (System_Follows_allocGiv RS Follows_Increasing1) 1); |
7841 | 522 |
qed "System_Increasing_giv"; |
523 |
||
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
524 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
525 |
Goal "i: I \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
526 |
\ ==> rename sysOfClient (plam x: I. rename client_map Client) \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
527 |
\ : Increasing (giv o sub i o client) \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
528 |
\ guarantees[funPair rel ask o sub i o client] \ |
8314 | 529 |
\ (INT h. {s. h <= (giv o sub i o client) s & \ |
530 |
\ h pfixGe (ask o sub i o client) s} \ |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
531 |
\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})"; |
8872 | 532 |
by rename_client_map_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
533 |
by (asm_simp_tac |
8872 | 534 |
(simpset() addsimps [rewrite_rule [o_def] Client_Progress]) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
535 |
qed "rename_Client_Progress"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
536 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
537 |
|
7965 | 538 |
(*progress (2), step 7*) |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
539 |
Goal |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
540 |
"System : (INT i : lessThan Nclients. \ |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
541 |
\ INT h. {s. h <= (giv o sub i o client) s & \ |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
542 |
\ h pfixGe (ask o sub i o client) s} \ |
8314 | 543 |
\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})"; |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
544 |
by (rtac INT_I 1); |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
545 |
(*Couldn't have just used Auto_tac since the "INT h" must be kept*) |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
546 |
by (rtac ([rename_Client_Progress, |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
547 |
Client_component_System] MRS component_guaranteesD) 1); |
8327 | 548 |
by (asm_full_simp_tac (simpset() addsimps [System_Increasing_giv]) 2); |
8128 | 549 |
by Auto_tac; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
550 |
qed "System_Client_Progress"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
551 |
|
8314 | 552 |
(*Concludes |
553 |
System : {s. k <= (sub i o allocGiv) s} |
|
554 |
LeadsTo |
|
555 |
{s. (sub i o allocAsk) s <= (ask o sub i o client) s} Int |
|
556 |
{s. k <= (giv o sub i o client) s} *) |
|
8067 | 557 |
val lemma = |
558 |
[System_Follows_ask RS Follows_Bounded, |
|
559 |
System_Follows_allocGiv RS Follows_LeadsTo] MRS Always_LeadsToD; |
|
8041 | 560 |
|
8314 | 561 |
(*A more complicated variant of the previous one*) |
8067 | 562 |
val lemma2 = [lemma, |
563 |
System_Follows_ask RS Follows_Increasing1 RS IncreasingD] |
|
564 |
MRS PSP_Stable; |
|
565 |
||
566 |
Goal "i < Nclients \ |
|
567 |
\ ==> System : {s. h <= (sub i o allocGiv) s & \ |
|
568 |
\ h pfixGe (sub i o allocAsk) s} \ |
|
569 |
\ LeadsTo \ |
|
570 |
\ {s. h <= (giv o sub i o client) s & \ |
|
571 |
\ h pfixGe (ask o sub i o client) s}"; |
|
572 |
by (rtac single_LeadsTo_I 1); |
|
573 |
by (res_inst_tac [("k6", "h"), ("x2", "(sub i o allocAsk) s")] |
|
574 |
(lemma2 RS LeadsTo_weaken) 1); |
|
575 |
by Auto_tac; |
|
576 |
by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD, |
|
577 |
prefix_imp_pfixGe]) 1); |
|
578 |
val lemma3 = result(); |
|
579 |
||
580 |
||
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
581 |
(*progress (2), step 8: Client i's "release" action is visible system-wide*) |
8075 | 582 |
Goal "i < Nclients \ |
583 |
\ ==> System : {s. h <= (sub i o allocGiv) s & \ |
|
8067 | 584 |
\ h pfixGe (sub i o allocAsk) s} \ |
8075 | 585 |
\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s}"; |
8067 | 586 |
by (rtac LeadsTo_Trans 1); |
587 |
by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS |
|
8113 | 588 |
Follows_LeadsTo) 2); |
8067 | 589 |
by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2); |
590 |
by (rtac LeadsTo_Trans 1); |
|
591 |
by (cut_facts_tac [System_Client_Progress] 2); |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
592 |
by (blast_tac (claset() addIs [LeadsTo_Basis]) 2); |
8067 | 593 |
by (etac lemma3 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
594 |
qed "System_Alloc_Client_Progress"; |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
595 |
|
8314 | 596 |
(*Lifting Alloc_Progress up to the level of systemState*) |
597 |
val rename_Alloc_Progress = |
|
8327 | 598 |
Alloc_Progress RS rename_guarantees_sysOfAlloc_I |
599 |
|> simplify (simpset() addsimps [o_def]); |
|
8075 | 600 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
601 |
(*progress (2), step 9*) |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
602 |
Goal |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
603 |
"System : (INT i : lessThan Nclients. \ |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
604 |
\ INT h. {s. h <= (sub i o allocAsk) s} \ |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
605 |
\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})"; |
8314 | 606 |
(*Can't use simpset(): the "INT h" must be kept*) |
8327 | 607 |
by (simp_tac (HOL_ss addsimps [o_apply, sub_def]) 1); |
608 |
by (rtac (rename_Alloc_Progress RS component_guaranteesD) 1); |
|
8075 | 609 |
by (auto_tac (claset(), |
8314 | 610 |
simpset() addsimps [o_simp System_Increasing_allocRel, |
611 |
o_simp System_Increasing_allocAsk, |
|
612 |
o_simp System_Bounded_allocAsk, |
|
613 |
o_simp System_Alloc_Client_Progress])); |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
614 |
qed "System_Alloc_Progress"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
615 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
616 |
|
8128 | 617 |
(*progress (2), step 10 (final result!) *) |
618 |
Goalw [system_progress_def] "System : system_progress"; |
|
619 |
by (Clarify_tac 1); |
|
620 |
by (rtac LeadsTo_Trans 1); |
|
621 |
by (etac (System_Follows_allocGiv RS Follows_LeadsTo_pfixLe) 2); |
|
622 |
by (rtac LeadsTo_Trans 1); |
|
623 |
by (cut_facts_tac [System_Alloc_Progress] 2); |
|
624 |
by (Blast_tac 2); |
|
625 |
by (etac (System_Follows_ask RS Follows_LeadsTo) 1); |
|
626 |
qed "System_Progress"; |
|
627 |
||
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
628 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
629 |
(*Ultimate goal*) |
8128 | 630 |
Goalw [system_spec_def] "System : system_spec"; |
631 |
by (blast_tac (claset() addIs [System_safety, System_Progress]) 1); |
|
632 |
qed "System_correct"; |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
633 |
|
8314 | 634 |