author | paulson |
Sat, 23 Sep 2000 16:02:01 +0200 | |
changeset 10064 | 1a77667b21ef |
parent 9403 | aad13b59b8d9 |
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 |
||
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8930
diff
changeset
|
9 |
(*Perhaps equalities.ML shouldn't add this in the first place!*) |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8930
diff
changeset
|
10 |
Delsimps [image_Collect]; |
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8930
diff
changeset
|
11 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
12 |
AddIs [impOfSubs subset_preserves_o]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
13 |
Addsimps [impOfSubs subset_preserves_o]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
14 |
Addsimps [funPair_o_distrib]; |
8327 | 15 |
Addsimps [Always_INT_distrib]; |
8067 | 16 |
Delsimps [o_apply]; |
17 |
||
8314 | 18 |
(*Eliminate the "o" operator*) |
7841 | 19 |
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
|
20 |
|
8314 | 21 |
(*For rewriting of specifications related by "guarantees"*) |
22 |
Addsimps [rename_image_constrains, rename_image_stable, |
|
23 |
rename_image_increasing, rename_image_invariant, |
|
24 |
rename_image_Constrains, rename_image_Stable, |
|
25 |
rename_image_Increasing, rename_image_Always, |
|
8327 | 26 |
rename_image_leadsTo, rename_image_LeadsTo, |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
27 |
rename_preserves, rename_image_preserves, lift_image_preserves, |
8327 | 28 |
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
|
29 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
30 |
(*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
|
31 |
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
|
32 |
(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
|
33 |
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
|
34 |
handle THM _ => (list_of_Int (th RS INT_D)) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
35 |
handle THM _ => (list_of_Int (th RS bspec)) |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
36 |
handle THM _ => [th]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
37 |
|
8314 | 38 |
(*Used just once, for Alloc_Increasing*) |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
39 |
val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec); |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
40 |
fun normalize th = |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
41 |
normalize (th RS spec |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
42 |
handle THM _ => th RS lessThanBspec |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
43 |
handle THM _ => th RS bspec |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
44 |
handle THM _ => th RS (guarantees_INT_right_iff RS iffD1)) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
45 |
handle THM _ => th; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
46 |
|
8067 | 47 |
|
8314 | 48 |
|
49 |
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***) |
|
50 |
||
8849 | 51 |
val record_auto_tac = |
52 |
auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper, |
|
53 |
simpset() addsimps [sysOfAlloc_def, sysOfClient_def, |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
54 |
client_map_def, non_dummy_def, funPair_def, |
8849 | 55 |
o_apply, Let_def]); |
56 |
||
57 |
||
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
58 |
Goalw [sysOfAlloc_def, Let_def] "inj sysOfAlloc"; |
6828 | 59 |
by (rtac injI 1); |
8849 | 60 |
by record_auto_tac; |
6828 | 61 |
qed "inj_sysOfAlloc"; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
62 |
AddIffs [inj_sysOfAlloc]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
63 |
|
8314 | 64 |
(*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
|
65 |
Goal "!!s. inv sysOfAlloc s = \ |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
66 |
\ (| allocGiv = allocGiv s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
67 |
\ allocAsk = allocAsk s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
68 |
\ allocRel = allocRel s, \ |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
69 |
\ allocState_d.dummy = (client s, dummy s) |)"; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
70 |
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); |
8849 | 71 |
by record_auto_tac; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
72 |
qed "inv_sysOfAlloc_eq"; |
7538 | 73 |
Addsimps [inv_sysOfAlloc_eq]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
74 |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
75 |
Goal "surj sysOfAlloc"; |
8327 | 76 |
by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); |
8849 | 77 |
by record_auto_tac; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
78 |
qed "surj_sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
79 |
AddIffs [surj_sysOfAlloc]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
80 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
81 |
Goal "bij sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
82 |
by (blast_tac (claset() addIs [bijI]) 1); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
83 |
qed "bij_sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
84 |
AddIffs [bij_sysOfAlloc]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
85 |
|
8314 | 86 |
|
87 |
(*** bijectivity of sysOfClient ***) |
|
88 |
||
7347 | 89 |
Goalw [sysOfClient_def] "inj sysOfClient"; |
90 |
by (rtac injI 1); |
|
8849 | 91 |
by record_auto_tac; |
7347 | 92 |
qed "inj_sysOfClient"; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
93 |
AddIffs [inj_sysOfClient]; |
6828 | 94 |
|
7347 | 95 |
Goal "!!s. inv sysOfClient s = \ |
96 |
\ (client s, \ |
|
97 |
\ (| allocGiv = allocGiv s, \ |
|
98 |
\ allocAsk = allocAsk s, \ |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
99 |
\ allocRel = allocRel s, \ |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
100 |
\ allocState_d.dummy = systemState.dummy s|) )"; |
7347 | 101 |
by (rtac (inj_sysOfClient RS inv_f_eq) 1); |
8849 | 102 |
by record_auto_tac; |
7365 | 103 |
qed "inv_sysOfClient_eq"; |
7689 | 104 |
Addsimps [inv_sysOfClient_eq]; |
6837 | 105 |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
106 |
Goal "surj sysOfClient"; |
8327 | 107 |
by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); |
8849 | 108 |
by record_auto_tac; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
109 |
qed "surj_sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
110 |
AddIffs [surj_sysOfClient]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
111 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
112 |
Goal "bij sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
113 |
by (blast_tac (claset() addIs [bijI]) 1); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
114 |
qed "bij_sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
115 |
AddIffs [bij_sysOfClient]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
116 |
|
6837 | 117 |
|
8314 | 118 |
(*** bijectivity of client_map ***) |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
119 |
|
8849 | 120 |
Goalw [inj_on_def] "inj client_map"; |
121 |
by record_auto_tac; |
|
8314 | 122 |
qed "inj_client_map"; |
123 |
AddIffs [inj_client_map]; |
|
124 |
||
125 |
Goal "!!s. inv client_map s = \ |
|
126 |
\ (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, \ |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
127 |
\ clientState_d.dummy = y|)) s"; |
8314 | 128 |
by (rtac (inj_client_map RS inv_f_eq) 1); |
8849 | 129 |
by record_auto_tac; |
8314 | 130 |
qed "inv_client_map_eq"; |
131 |
Addsimps [inv_client_map_eq]; |
|
132 |
||
133 |
Goal "surj client_map"; |
|
8327 | 134 |
by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); |
8849 | 135 |
by record_auto_tac; |
8314 | 136 |
qed "surj_client_map"; |
137 |
AddIffs [surj_client_map]; |
|
138 |
||
139 |
Goal "bij client_map"; |
|
140 |
by (blast_tac (claset() addIs [bijI]) 1); |
|
141 |
qed "bij_client_map"; |
|
142 |
AddIffs [bij_client_map]; |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
143 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
144 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
145 |
(** o-simprules for client_map **) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
146 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
147 |
Goalw [client_map_def] "fst o client_map = non_dummy"; |
8327 | 148 |
by (rtac fst_o_funPair 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
149 |
qed "fst_o_client_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
150 |
Addsimps (make_o_equivs fst_o_client_map); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
151 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
152 |
Goalw [client_map_def] "snd o client_map = clientState_d.dummy"; |
8327 | 153 |
by (rtac snd_o_funPair 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
154 |
qed "snd_o_client_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
155 |
Addsimps (make_o_equivs snd_o_client_map); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
156 |
|
8327 | 157 |
(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **) |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
158 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
159 |
Goal "client o sysOfAlloc = fst o allocState_d.dummy "; |
8849 | 160 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
161 |
qed "client_o_sysOfAlloc"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
162 |
Addsimps (make_o_equivs client_o_sysOfAlloc); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
163 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
164 |
Goal "allocGiv o sysOfAlloc = allocGiv"; |
8849 | 165 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
166 |
qed "allocGiv_o_sysOfAlloc_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
167 |
Addsimps (make_o_equivs allocGiv_o_sysOfAlloc_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
168 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
169 |
Goal "allocAsk o sysOfAlloc = allocAsk"; |
8849 | 170 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
171 |
qed "allocAsk_o_sysOfAlloc_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
172 |
Addsimps (make_o_equivs allocAsk_o_sysOfAlloc_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
173 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
174 |
Goal "allocRel o sysOfAlloc = allocRel"; |
8849 | 175 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
176 |
qed "allocRel_o_sysOfAlloc_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
177 |
Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
178 |
|
8327 | 179 |
(** o-simprules for sysOfClient [MUST BE AUTOMATED] **) |
8311
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 "client o sysOfClient = fst"; |
8849 | 182 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
183 |
qed "client_o_sysOfClient"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
184 |
Addsimps (make_o_equivs client_o_sysOfClient); |
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 "allocGiv o sysOfClient = allocGiv o snd "; |
8849 | 187 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
188 |
qed "allocGiv_o_sysOfClient_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
189 |
Addsimps (make_o_equivs allocGiv_o_sysOfClient_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
190 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
191 |
Goal "allocAsk o sysOfClient = allocAsk o snd "; |
8849 | 192 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
193 |
qed "allocAsk_o_sysOfClient_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
194 |
Addsimps (make_o_equivs allocAsk_o_sysOfClient_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
195 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
196 |
Goal "allocRel o sysOfClient = allocRel o snd "; |
8849 | 197 |
by record_auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
198 |
qed "allocRel_o_sysOfClient_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
199 |
Addsimps (make_o_equivs allocRel_o_sysOfClient_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
200 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
201 |
Goal "allocGiv o inv sysOfAlloc = allocGiv"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
202 |
by (simp_tac (simpset() addsimps [o_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
203 |
qed "allocGiv_o_inv_sysOfAlloc_eq"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
204 |
Addsimps (make_o_equivs allocGiv_o_inv_sysOfAlloc_eq); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
205 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
206 |
Goal "allocAsk o inv sysOfAlloc = allocAsk"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
207 |
by (simp_tac (simpset() addsimps [o_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
208 |
qed "allocAsk_o_inv_sysOfAlloc_eq"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
209 |
Addsimps (make_o_equivs allocAsk_o_inv_sysOfAlloc_eq); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
210 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
211 |
Goal "allocRel o inv sysOfAlloc = allocRel"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
212 |
by (simp_tac (simpset() addsimps [o_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
213 |
qed "allocRel_o_inv_sysOfAlloc_eq"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
214 |
Addsimps (make_o_equivs allocRel_o_inv_sysOfAlloc_eq); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
215 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
216 |
Goal "(rel o inv client_map o drop_map i o inv sysOfClient) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
217 |
\ rel o sub i o client"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
218 |
by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
219 |
qed "rel_inv_client_map_drop_map"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
220 |
Addsimps (make_o_equivs rel_inv_client_map_drop_map); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
221 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
222 |
Goal "(ask o inv client_map o drop_map i o inv sysOfClient) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
223 |
\ ask o sub i o client"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
224 |
by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
225 |
qed "ask_inv_client_map_drop_map"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
226 |
Addsimps (make_o_equivs ask_inv_client_map_drop_map); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
227 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
228 |
(** |
7365 | 229 |
Open_locale "System"; |
230 |
||
231 |
val Alloc = thm "Alloc"; |
|
232 |
val Client = thm "Client"; |
|
233 |
val Network = thm "Network"; |
|
234 |
val System_def = thm "System_def"; |
|
8314 | 235 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
236 |
CANNOT use bind_thm: it puts the theorem into standard form, in effect |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
237 |
exporting it from the locale |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
238 |
**) |
7365 | 239 |
|
240 |
AddIffs [finite_lessThan]; |
|
241 |
||
242 |
(*Client : <unfolded specification> *) |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
243 |
val client_spec_simps = |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
244 |
[client_spec_def, client_increasing_def, client_bounded_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
245 |
client_progress_def, client_allowed_acts_def, client_preserves_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
246 |
guarantees_Int_right]; |
7365 | 247 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
248 |
val [Client_Increasing_ask, Client_Increasing_rel, |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
249 |
Client_Bounded, Client_Progress, Client_AllowedActs, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
250 |
Client_preserves_giv, Client_preserves_dummy] = |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
251 |
Client |> simplify (simpset() addsimps client_spec_simps) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
252 |
|> list_of_Int; |
7365 | 253 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
254 |
AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded, |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
255 |
Client_preserves_giv, Client_preserves_dummy]; |
6828 | 256 |
|
257 |
||
7365 | 258 |
(*Network : <unfolded specification> *) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
259 |
val network_spec_simps = |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
260 |
[network_spec_def, network_ask_def, network_giv_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
261 |
network_rel_def, network_allowed_acts_def, network_preserves_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
262 |
ball_conj_distrib]; |
7365 | 263 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
264 |
val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
265 |
Network_preserves_allocGiv, Network_preserves_rel, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
266 |
Network_preserves_ask] = |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
267 |
Network |> simplify (simpset() addsimps network_spec_simps) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
268 |
|> list_of_Int; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
269 |
|
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
270 |
AddIffs [Network_preserves_allocGiv]; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
271 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
272 |
Addsimps [Network_preserves_rel, Network_preserves_ask]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
273 |
Addsimps [o_simp Network_preserves_rel, o_simp Network_preserves_ask]; |
7365 | 274 |
|
275 |
||
276 |
(*Alloc : <unfolded specification> *) |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
277 |
val alloc_spec_simps = |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
278 |
[alloc_spec_def, alloc_increasing_def, alloc_safety_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
279 |
alloc_progress_def, alloc_allowed_acts_def, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
280 |
alloc_preserves_def]; |
7365 | 281 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
282 |
val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
283 |
Alloc_preserves_allocRel, Alloc_preserves_allocAsk, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
284 |
Alloc_preserves_dummy] = |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
285 |
Alloc |> simplify (simpset() addsimps alloc_spec_simps) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
286 |
|> list_of_Int; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
287 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
288 |
(*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
|
289 |
val Alloc_Increasing = normalize Alloc_Increasing_0; |
7365 | 290 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
291 |
AddIffs [Alloc_preserves_allocRel, Alloc_preserves_allocAsk, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
292 |
Alloc_preserves_dummy]; |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
293 |
|
8327 | 294 |
(** Components lemmas [MUST BE AUTOMATED] **) |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
295 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
296 |
Goal "Network Join \ |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
297 |
\ ((rename sysOfClient \ |
8985 | 298 |
\ (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
|
299 |
\ rename sysOfAlloc Alloc) \ |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
300 |
\ = System"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
301 |
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
|
302 |
qed "Network_component_System"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
303 |
|
8314 | 304 |
Goal "(rename sysOfClient \ |
8985 | 305 |
\ (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
|
306 |
\ (Network Join rename sysOfAlloc Alloc) = System"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
307 |
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
|
308 |
qed "Client_component_System"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
309 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
310 |
Goal "rename sysOfAlloc Alloc Join \ |
8985 | 311 |
\ ((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
|
312 |
\ Network) = System"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
313 |
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
|
314 |
qed "Alloc_component_System"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
315 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
316 |
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
|
317 |
Alloc_component_System]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
318 |
|
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
319 |
(** These preservation laws should be generated automatically **) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
320 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
321 |
Goal "Allowed Client = preserves rel Int preserves ask"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
322 |
by (auto_tac (claset(), |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
323 |
simpset() addsimps [Allowed_def, Client_AllowedActs, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
324 |
safety_prop_Acts_iff])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
325 |
qed "Client_Allowed"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
326 |
Addsimps [Client_Allowed]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
327 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
328 |
Goal "Allowed Network = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
329 |
\ preserves allocRel Int \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
330 |
\ (INT i: lessThan Nclients. preserves(giv o sub i o client))"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
331 |
by (auto_tac (claset(), |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
332 |
simpset() addsimps [Allowed_def, Network_AllowedActs, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
333 |
safety_prop_Acts_iff])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
334 |
qed "Network_Allowed"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
335 |
Addsimps [Network_Allowed]; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
336 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
337 |
Goal "Allowed Alloc = preserves allocGiv"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
338 |
by (auto_tac (claset(), |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
339 |
simpset() addsimps [Allowed_def, Alloc_AllowedActs, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
340 |
safety_prop_Acts_iff])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
341 |
qed "Alloc_Allowed"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
342 |
Addsimps [Alloc_Allowed]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
343 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
344 |
Goal "OK I (%i. lift i (rename client_map Client))"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
345 |
by (rtac OK_lift_I 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
346 |
by Auto_tac; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
347 |
by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
348 |
by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
349 |
by (auto_tac (claset(), simpset() addsimps [o_def, split_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
350 |
qed "OK_lift_rename_Client"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
351 |
Addsimps [OK_lift_rename_Client]; (*needed in rename_client_map_tac* |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
352 |
|
8872 | 353 |
(*The proofs of rename_Client_Increasing, rename_Client_Bounded and |
354 |
rename_Client_Progress are similar. All require copying out the original |
|
355 |
Client property. A forward proof can be constructed as follows: |
|
8327 | 356 |
|
357 |
Client_Increasing_ask RS |
|
358 |
(bij_client_map RS rename_rename_guarantees_eq RS iffD2) |
|
359 |
RS (lift_lift_guarantees_eq RS iffD2) |
|
360 |
RS guarantees_PLam_I |
|
361 |
RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2) |
|
362 |
|> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def, |
|
363 |
surj_rename RS surj_range]); |
|
364 |
||
365 |
However, the "preserves" property remains to be discharged, and the unfolding |
|
366 |
of "o" and "sub" complicates subsequent reasoning. |
|
8872 | 367 |
|
368 |
The following tactic works for all three proofs, though it certainly looks |
|
369 |
ad-hoc! |
|
8327 | 370 |
*) |
8872 | 371 |
val rename_client_map_tac = |
372 |
EVERY [ |
|
373 |
simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1, |
|
374 |
rtac guarantees_PLam_I 1, |
|
375 |
assume_tac 2, |
|
376 |
(*preserves: routine reasoning*) |
|
377 |
asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2, |
|
378 |
(*the guarantee for "lift i (rename client_map Client)" *) |
|
379 |
asm_simp_tac |
|
380 |
(simpset() addsimps [lift_guarantees_eq_lift_inv, |
|
381 |
rename_guarantees_eq_rename_inv, |
|
382 |
bij_imp_bij_inv, surj_rename RS surj_range, |
|
383 |
inv_inv_eq]) 1, |
|
384 |
asm_simp_tac |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
385 |
(simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1]; |
8872 | 386 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
387 |
|
8872 | 388 |
(*Lifting Client_Increasing to systemState*) |
389 |
Goal "i : I \ |
|
390 |
\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \ |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
391 |
\ UNIV guarantees \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
392 |
\ Increasing (ask o sub i o client) Int \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
393 |
\ Increasing (rel o sub i o client)"; |
8872 | 394 |
by rename_client_map_tac; |
395 |
qed "rename_Client_Increasing"; |
|
8327 | 396 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
397 |
Goal "[| F : preserves w; i ~= j |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
398 |
\ ==> F : preserves (sub i o fst o lift_map j o funPair v w)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
399 |
by (auto_tac (claset(), |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
400 |
simpset() addsimps [lift_map_def, split_def, linorder_neq_iff, o_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
401 |
by (ALLGOALS (dtac (impOfSubs subset_preserves_o))); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
402 |
by (auto_tac (claset(), simpset() addsimps [o_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
403 |
qed "preserves_sub_fst_lift_map"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
404 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
405 |
Goal "[| i < Nclients; j < Nclients |] \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
406 |
\ ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
407 |
by (case_tac "i=j" 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
408 |
by (asm_full_simp_tac (simpset() addsimps [o_def, non_dummy_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
409 |
by (dtac (Client_preserves_dummy RS preserves_sub_fst_lift_map) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
410 |
by (ALLGOALS (dtac (impOfSubs subset_preserves_o))); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
411 |
by (asm_full_simp_tac (simpset() addsimps [o_def, client_map_def]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
412 |
qed "client_preserves_giv_oo_client_map"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
413 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
414 |
Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
415 |
\ ok Network"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
416 |
by (auto_tac (claset(), simpset() addsimps [ok_iff_Allowed, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
417 |
client_preserves_giv_oo_client_map])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
418 |
qed "rename_sysOfClient_ok_Network"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
419 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
420 |
Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
421 |
\ ok rename sysOfAlloc Alloc"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
422 |
by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
423 |
qed "rename_sysOfClient_ok_Alloc"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
424 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
425 |
Goal "rename sysOfAlloc Alloc ok Network"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
426 |
by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
427 |
qed "rename_sysOfAlloc_ok_Network"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
428 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
429 |
AddIffs [rename_sysOfClient_ok_Network, rename_sysOfClient_ok_Alloc, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
430 |
rename_sysOfAlloc_ok_Network]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
431 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
432 |
(*The "ok" laws, re-oriented*) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
433 |
AddIffs [rename_sysOfClient_ok_Network RS ok_sym, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
434 |
rename_sysOfClient_ok_Alloc RS ok_sym, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
435 |
rename_sysOfAlloc_ok_Network RS ok_sym]; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
436 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
437 |
Goal "i < Nclients \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
438 |
\ ==> System : Increasing (ask o sub i o client) Int \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
439 |
\ Increasing (rel o sub i o client)"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
440 |
by (rtac ([rename_Client_Increasing, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
441 |
Client_component_System] MRS component_guaranteesD) 1); |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
442 |
by Auto_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
443 |
qed "System_Increasing"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
444 |
|
8327 | 445 |
bind_thm ("rename_guarantees_sysOfAlloc_I", |
446 |
bij_sysOfAlloc RS rename_rename_guarantees_eq RS iffD2); |
|
447 |
||
448 |
||
8314 | 449 |
(*Lifting Alloc_Increasing up to the level of systemState*) |
450 |
val rename_Alloc_Increasing = |
|
8327 | 451 |
Alloc_Increasing RS rename_guarantees_sysOfAlloc_I |
452 |
|> simplify (simpset() addsimps [surj_rename RS surj_range, o_def]); |
|
8314 | 453 |
|
7841 | 454 |
Goalw [System_def] |
455 |
"i < Nclients ==> System : Increasing (sub i o allocGiv)"; |
|
8314 | 456 |
by (simp_tac (simpset() addsimps [o_def]) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
457 |
by (rtac (rename_Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1); |
7841 | 458 |
by Auto_tac; |
459 |
qed "System_Increasing_allocGiv"; |
|
7365 | 460 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
461 |
AddSIs (list_of_Int System_Increasing); |
6828 | 462 |
|
7841 | 463 |
(** Follows consequences. |
464 |
The "Always (INT ...) formulation expresses the general safety property |
|
465 |
and allows it to be combined using Always_Int_rule below. **) |
|
466 |
||
8067 | 467 |
Goal |
468 |
"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
|
469 |
by (auto_tac (claset() addSIs [Network_Rel RS component_guaranteesD], |
8067 | 470 |
simpset())); |
471 |
qed "System_Follows_rel"; |
|
472 |
||
473 |
Goal |
|
474 |
"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
|
475 |
by (auto_tac (claset() addSIs [Network_Ask RS component_guaranteesD], |
8067 | 476 |
simpset())); |
477 |
qed "System_Follows_ask"; |
|
478 |
||
479 |
Goal |
|
480 |
"i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)"; |
|
481 |
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
|
482 |
rename_Alloc_Increasing RS component_guaranteesD], |
8067 | 483 |
simpset())); |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
484 |
by (ALLGOALS (simp_tac (simpset() addsimps [o_def, non_dummy_def]))); |
8314 | 485 |
by (auto_tac |
486 |
(claset() addSIs [rename_Alloc_Increasing RS component_guaranteesD], |
|
487 |
simpset())); |
|
8067 | 488 |
qed "System_Follows_allocGiv"; |
489 |
||
8985 | 490 |
Goal "System : Always (INT i: lessThan Nclients. \ |
7841 | 491 |
\ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})"; |
8327 | 492 |
by Auto_tac; |
8067 | 493 |
by (etac (System_Follows_allocGiv RS Follows_Bounded) 1); |
7841 | 494 |
qed "Always_giv_le_allocGiv"; |
495 |
||
8985 | 496 |
Goal "System : Always (INT i: lessThan Nclients. \ |
7841 | 497 |
\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})"; |
8327 | 498 |
by Auto_tac; |
8067 | 499 |
by (etac (System_Follows_ask RS Follows_Bounded) 1); |
7841 | 500 |
qed "Always_allocAsk_le_ask"; |
501 |
||
8985 | 502 |
Goal "System : Always (INT i: lessThan Nclients. \ |
7841 | 503 |
\ {s. (sub i o allocRel) s <= (rel o sub i o client) s})"; |
8067 | 504 |
by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel], |
8327 | 505 |
simpset())); |
7841 | 506 |
qed "Always_allocRel_le_rel"; |
507 |
||
508 |
||
509 |
(*** Proof of the safety property (1) ***) |
|
510 |
||
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
511 |
(*safety (1), step 1 is System_Follows_rel*) |
7841 | 512 |
|
7689 | 513 |
(*safety (1), step 2*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
514 |
(* i < Nclients ==> System : Increasing (sub i o allocRel) *) |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
515 |
bind_thm ("System_Increasing_allocRel", |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
516 |
System_Follows_rel RS Follows_Increasing1); |
6828 | 517 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
518 |
(*Lifting Alloc_safety up to the level of systemState. |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
519 |
Simplififying with o_def gets rid of the translations but it unfortunately |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
520 |
gets rid of the other "o"s too.*) |
8314 | 521 |
val rename_Alloc_Safety = |
8327 | 522 |
Alloc_Safety RS rename_guarantees_sysOfAlloc_I |
523 |
|> simplify (simpset() addsimps [o_def]); |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
524 |
|
7689 | 525 |
(*safety (1), step 3*) |
8930 | 526 |
Goal |
9109 | 527 |
"System : Always {s. setsum (%i. (tokens o sub i o allocGiv) s) \ |
528 |
\ (lessThan Nclients) \ |
|
529 |
\ <= NbT + setsum (%i. (tokens o sub i o allocRel) s) \ |
|
530 |
\ (lessThan Nclients)}"; |
|
8327 | 531 |
by (simp_tac (simpset() addsimps [o_apply]) 1); |
532 |
by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1); |
|
533 |
by (auto_tac (claset(), |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
534 |
simpset() addsimps [o_simp System_Increasing_allocRel])); |
7538 | 535 |
qed "System_sum_bounded"; |
7537 | 536 |
|
8314 | 537 |
|
7841 | 538 |
(** Follows reasoning **) |
539 |
||
8985 | 540 |
Goal "System : Always (INT i: lessThan Nclients. \ |
7540 | 541 |
\ {s. (tokens o giv o sub i o client) s \ |
542 |
\ <= (tokens o sub i o allocGiv) s})"; |
|
7841 | 543 |
by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1); |
8067 | 544 |
by (auto_tac (claset() addIs [tokens_mono_prefix], |
545 |
simpset() addsimps [o_apply])); |
|
7841 | 546 |
qed "Always_tokens_giv_le_allocGiv"; |
7540 | 547 |
|
8985 | 548 |
Goal "System : Always (INT i: lessThan Nclients. \ |
7540 | 549 |
\ {s. (tokens o sub i o allocRel) s \ |
550 |
\ <= (tokens o rel o sub i o client) s})"; |
|
7841 | 551 |
by (rtac (Always_allocRel_le_rel RS Always_weaken) 1); |
8067 | 552 |
by (auto_tac (claset() addIs [tokens_mono_prefix], |
553 |
simpset() addsimps [o_apply])); |
|
7841 | 554 |
qed "Always_tokens_allocRel_le_rel"; |
7540 | 555 |
|
7841 | 556 |
(*safety (1), step 4 (final result!) *) |
8128 | 557 |
Goalw [system_safety_def] "System : system_safety"; |
7841 | 558 |
by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv, |
559 |
Always_tokens_allocRel_le_rel] RS Always_weaken) 1); |
|
7538 | 560 |
by Auto_tac; |
9109 | 561 |
by (rtac (setsum_fun_mono RS order_trans) 1); |
7540 | 562 |
by (dtac order_trans 2); |
9109 | 563 |
by (rtac ([order_refl, setsum_fun_mono] MRS add_le_mono) 2); |
7540 | 564 |
by (assume_tac 3); |
7482 | 565 |
by Auto_tac; |
7540 | 566 |
qed "System_safety"; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
567 |
|
7689 | 568 |
|
569 |
(*** Proof of the progress property (2) ***) |
|
570 |
||
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
571 |
(*progress (2), step 1 is System_Follows_ask and System_Follows_rel*) |
7689 | 572 |
|
7841 | 573 |
(*progress (2), step 2; see also System_Increasing_allocRel*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
574 |
(* i < Nclients ==> System : Increasing (sub i o allocAsk) *) |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
575 |
bind_thm ("System_Increasing_allocAsk", |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
576 |
System_Follows_ask RS Follows_Increasing1); |
7689 | 577 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
578 |
(*progress (2), step 3: lifting "Client_Bounded" to systemState*) |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
579 |
Goal "i : I \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
580 |
\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \ |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
581 |
\ UNIV guarantees \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
582 |
\ Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}"; |
8872 | 583 |
by rename_client_map_tac; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
584 |
qed "rename_Client_Bounded"; |
7841 | 585 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
586 |
Goal "i < Nclients \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
587 |
\ ==> System : Always \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
588 |
\ {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
|
589 |
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
|
590 |
Client_component_System] MRS component_guaranteesD) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
591 |
by Auto_tac; |
7841 | 592 |
qed "System_Bounded_ask"; |
593 |
||
8930 | 594 |
Goal "{x. ALL y. P y --> Q x y} = (INT y: {y. P y}. {x. Q x y})"; |
595 |
by (Blast_tac 1); |
|
596 |
qed "Collect_all_imp_eq"; |
|
597 |
||
7841 | 598 |
(*progress (2), step 4*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
599 |
Goal "System : Always {s. ALL i<Nclients. \ |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
600 |
\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}"; |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
601 |
by (auto_tac (claset(), simpset() addsimps [Collect_all_imp_eq])); |
7841 | 602 |
by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask] |
603 |
RS Always_weaken) 1); |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
604 |
by (auto_tac (claset() addDs [set_mono], simpset())); |
7841 | 605 |
qed "System_Bounded_allocAsk"; |
606 |
||
7965 | 607 |
(*progress (2), step 5 is System_Increasing_allocGiv*) |
7841 | 608 |
|
7965 | 609 |
(*progress (2), step 6*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
610 |
(* i < Nclients ==> System : Increasing (giv o sub i o client) *) |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
611 |
bind_thm ("System_Increasing_giv", |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
612 |
System_Follows_allocGiv RS Follows_Increasing1); |
7841 | 613 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
614 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
615 |
Goal "i: I \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
616 |
\ ==> rename sysOfClient (plam x: I. rename client_map Client) \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
617 |
\ : Increasing (giv o sub i o client) \ |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
618 |
\ guarantees \ |
8314 | 619 |
\ (INT h. {s. h <= (giv o sub i o client) s & \ |
620 |
\ 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
|
621 |
\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})"; |
8872 | 622 |
by rename_client_map_tac; |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
623 |
by (asm_simp_tac (simpset() addsimps [o_simp Client_Progress]) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
624 |
qed "rename_Client_Progress"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
625 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
626 |
|
7965 | 627 |
(*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
|
628 |
Goal |
8985 | 629 |
"System : (INT i : (lessThan Nclients). \ |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
630 |
\ 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
|
631 |
\ h pfixGe (ask o sub i o client) s} \ |
8314 | 632 |
\ 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
|
633 |
by (rtac INT_I 1); |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
634 |
(*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
|
635 |
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
|
636 |
Client_component_System] MRS component_guaranteesD) 1); |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
637 |
by (auto_tac (claset(), simpset() addsimps [System_Increasing_giv])); |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
638 |
qed "System_Client_Progress"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
639 |
|
8314 | 640 |
(*Concludes |
641 |
System : {s. k <= (sub i o allocGiv) s} |
|
642 |
LeadsTo |
|
643 |
{s. (sub i o allocAsk) s <= (ask o sub i o client) s} Int |
|
644 |
{s. k <= (giv o sub i o client) s} *) |
|
8067 | 645 |
val lemma = |
646 |
[System_Follows_ask RS Follows_Bounded, |
|
647 |
System_Follows_allocGiv RS Follows_LeadsTo] MRS Always_LeadsToD; |
|
8041 | 648 |
|
8314 | 649 |
(*A more complicated variant of the previous one*) |
8067 | 650 |
val lemma2 = [lemma, |
651 |
System_Follows_ask RS Follows_Increasing1 RS IncreasingD] |
|
652 |
MRS PSP_Stable; |
|
653 |
||
654 |
Goal "i < Nclients \ |
|
655 |
\ ==> System : {s. h <= (sub i o allocGiv) s & \ |
|
656 |
\ h pfixGe (sub i o allocAsk) s} \ |
|
657 |
\ LeadsTo \ |
|
658 |
\ {s. h <= (giv o sub i o client) s & \ |
|
659 |
\ h pfixGe (ask o sub i o client) s}"; |
|
660 |
by (rtac single_LeadsTo_I 1); |
|
661 |
by (res_inst_tac [("k6", "h"), ("x2", "(sub i o allocAsk) s")] |
|
662 |
(lemma2 RS LeadsTo_weaken) 1); |
|
663 |
by Auto_tac; |
|
664 |
by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD, |
|
665 |
prefix_imp_pfixGe]) 1); |
|
666 |
val lemma3 = result(); |
|
667 |
||
668 |
||
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
669 |
(*progress (2), step 8: Client i's "release" action is visible system-wide*) |
8075 | 670 |
Goal "i < Nclients \ |
671 |
\ ==> System : {s. h <= (sub i o allocGiv) s & \ |
|
8067 | 672 |
\ h pfixGe (sub i o allocAsk) s} \ |
8075 | 673 |
\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s}"; |
8067 | 674 |
by (rtac LeadsTo_Trans 1); |
675 |
by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS |
|
8113 | 676 |
Follows_LeadsTo) 2); |
8067 | 677 |
by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2); |
678 |
by (rtac LeadsTo_Trans 1); |
|
679 |
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
|
680 |
by (blast_tac (claset() addIs [LeadsTo_Basis]) 2); |
8067 | 681 |
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
|
682 |
qed "System_Alloc_Client_Progress"; |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
683 |
|
8314 | 684 |
(*Lifting Alloc_Progress up to the level of systemState*) |
685 |
val rename_Alloc_Progress = |
|
8327 | 686 |
Alloc_Progress RS rename_guarantees_sysOfAlloc_I |
687 |
|> simplify (simpset() addsimps [o_def]); |
|
8075 | 688 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
689 |
(*progress (2), step 9*) |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
690 |
Goal |
8985 | 691 |
"System : (INT i : (lessThan Nclients). \ |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
692 |
\ 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
|
693 |
\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})"; |
8314 | 694 |
(*Can't use simpset(): the "INT h" must be kept*) |
8327 | 695 |
by (simp_tac (HOL_ss addsimps [o_apply, sub_def]) 1); |
696 |
by (rtac (rename_Alloc_Progress RS component_guaranteesD) 1); |
|
8075 | 697 |
by (auto_tac (claset(), |
8314 | 698 |
simpset() addsimps [o_simp System_Increasing_allocRel, |
699 |
o_simp System_Increasing_allocAsk, |
|
700 |
o_simp System_Bounded_allocAsk, |
|
701 |
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
|
702 |
qed "System_Alloc_Progress"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
703 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
704 |
|
8128 | 705 |
(*progress (2), step 10 (final result!) *) |
706 |
Goalw [system_progress_def] "System : system_progress"; |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
707 |
by (cut_facts_tac [System_Alloc_Progress] 1); |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
708 |
by (blast_tac (claset() addIs [LeadsTo_Trans, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
709 |
System_Follows_allocGiv RS Follows_LeadsTo_pfixLe, |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
9109
diff
changeset
|
710 |
System_Follows_ask RS Follows_LeadsTo]) 1); |
8128 | 711 |
qed "System_Progress"; |
712 |
||
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
713 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
714 |
(*Ultimate goal*) |
8128 | 715 |
Goalw [system_spec_def] "System : system_spec"; |
716 |
by (blast_tac (claset() addIs [System_safety, System_Progress]) 1); |
|
717 |
qed "System_correct"; |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
718 |
|
8314 | 719 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
720 |
(** Some lemmas no longer used **) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
721 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
722 |
Goal "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
723 |
\ (funPair giv (funPair ask rel))"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
724 |
by (rtac ext 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
725 |
by (auto_tac (claset(), simpset() addsimps [o_def, non_dummy_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
726 |
qed "non_dummy_eq_o_funPair"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
727 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
728 |
Goal "(preserves non_dummy) = \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
729 |
\ (preserves rel Int preserves ask Int preserves giv)"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
730 |
by (simp_tac (simpset() addsimps [non_dummy_eq_o_funPair]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
731 |
by Auto_tac; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
732 |
by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
733 |
by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
734 |
by (dres_inst_tac [("w1", "giv")] (impOfSubs subset_preserves_o) 3); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
735 |
by (auto_tac (claset(), simpset() addsimps [o_def])); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
736 |
qed "preserves_non_dummy_eq"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
737 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
738 |
(*Could go to Extend.ML*) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
739 |
Goal "bij f ==> fst (inv (%(x, u). inv f x) z) = f z"; |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
740 |
by (rtac fst_inv_equalityI 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
741 |
by (res_inst_tac [("f","%z. (f z, ?h z)")] surjI 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
742 |
by (asm_full_simp_tac (simpset() addsimps [bij_is_inj, inv_f_f]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
743 |
by (asm_full_simp_tac (simpset() addsimps [bij_is_surj, surj_f_inv_f]) 1); |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
744 |
qed "bij_fst_inv_inv_eq"; |