author | paulson |
Mon, 28 Feb 2000 10:49:42 +0100 | |
changeset 8311 | 6218522253e7 |
parent 8286 | d4b895d3afa7 |
child 8314 | 463f63a9a7f2 |
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 |
|
7540 | 7 |
|
7841 | 8 |
Stop using o (composition)? |
7689 | 9 |
|
10 |
guarantees_PLam_I looks wrong: refers to lift_prog |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
11 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
12 |
Goal "(plam x: lessThan Nclients. Client) = x"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
13 |
Client :: (clientState * ((nat => clientState) * 'b)) program |
6828 | 14 |
*) |
15 |
||
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
16 |
(***USEFUL??*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
17 |
Goal "surj h ==> h `` {s. P (h s)} = {s. P s}"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
18 |
by Auto_tac; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
19 |
by (force_tac (claset() addSIs [exI, surj_f_inv_f RS sym], |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
20 |
simpset() addsimps [surj_f_inv_f]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
21 |
qed "surj_image_Collect_lemma"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
22 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
23 |
(**To Lift_prog.ML???????????????????????????????????????????????????????????*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
24 |
(*Lets us prove one version of a theorem and store others*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
25 |
Goal "f o g = h ==> f' o f o g = f' o h"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
26 |
by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
27 |
qed "o_equiv_assoc"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
28 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
29 |
Goal "f o g = h ==> ALL x. f(g x) = h x"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
30 |
by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
31 |
qed "o_equiv_apply"; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
32 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
33 |
fun make_o_equivs th = |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
34 |
[th, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
35 |
th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]), |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
36 |
th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
37 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
38 |
Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair); |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
39 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
40 |
Goal "sub i o fst o lift_map i = fst"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
41 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
42 |
by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def, sub_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
43 |
qed "fst_o_lift_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
44 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
45 |
Goal "snd o lift_map i = snd o snd"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
46 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
47 |
by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
48 |
qed "snd_o_lift_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
49 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
50 |
Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
51 |
(**To Lift_prog.ML???????????????????????????????????????????????????????????*) |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
52 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
53 |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
54 |
AddIs [impOfSubs subset_preserves_o]; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
55 |
Addsimps [funPair_o_distrib]; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
56 |
Addsimps [rename_preserves]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
57 |
|
8067 | 58 |
Delsimps [o_apply]; |
59 |
||
7841 | 60 |
(*Eliminating the "o" operator gives associativity for free*) |
61 |
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
|
62 |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
63 |
(*for tidying up expressions, but LOOPS with standard simpset.*) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
64 |
Goal "(%u. f (u i)) = f o sub i"; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
65 |
by (asm_full_simp_tac (simpset() addsimps [o_def]) 1); |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
66 |
qed "sub_fold"; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
67 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
68 |
(*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
|
69 |
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
|
70 |
(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
|
71 |
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
|
72 |
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
|
73 |
handle THM _ => [th]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
74 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
75 |
(*useful??*) |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
76 |
val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec); |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
77 |
fun normalize th = |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
78 |
normalize (th RS spec |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
79 |
handle THM _ => th RS lessThanBspec |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
80 |
handle THM _ => th RS bspec |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
81 |
handle THM _ => th RS (guarantees_INT_right_iff RS iffD1)) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
82 |
handle THM _ => th; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
83 |
|
8067 | 84 |
(*Currently UNUSED, but possibly of interest*) |
85 |
Goal "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}"; |
|
86 |
by (asm_full_simp_tac |
|
87 |
(simpset() addsimps [Increasing_def, Stable_def, Constrains_def, |
|
88 |
constrains_def]) 1); |
|
89 |
by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD, |
|
90 |
prefix_imp_pfixGe]) 1); |
|
91 |
qed "Increasing_imp_Stable_pfixGe"; |
|
92 |
||
93 |
(*Currently UNUSED, but possibly of interest*) |
|
94 |
Goal "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s} \ |
|
95 |
\ ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}"; |
|
96 |
by (rtac single_LeadsTo_I 1); |
|
97 |
by (dres_inst_tac [("x", "f s")] spec 1); |
|
98 |
by (etac LeadsTo_weaken 1); |
|
99 |
by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD, |
|
100 |
prefix_imp_pfixGe]) 2); |
|
101 |
by (Blast_tac 1); |
|
102 |
qed "LeadsTo_le_imp_pfixGe"; |
|
103 |
||
104 |
||
7538 | 105 |
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n"; |
106 |
by (induct_tac "n" 1); |
|
107 |
by Auto_tac; |
|
108 |
by (dres_inst_tac [("x","n")] bspec 1); |
|
109 |
by Auto_tac; |
|
110 |
by (arith_tac 1); |
|
111 |
qed_spec_mp "sum_mono"; |
|
112 |
||
7540 | 113 |
Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys"; |
114 |
by (induct_tac "ys" 1); |
|
115 |
by (auto_tac (claset(), simpset() addsimps [prefix_Cons])); |
|
116 |
qed_spec_mp "tokens_mono_prefix"; |
|
117 |
||
118 |
Goalw [mono_def] "mono tokens"; |
|
119 |
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); |
|
120 |
qed "mono_tokens"; |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
121 |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
122 |
Goalw [sysOfAlloc_def, Let_def] "inj sysOfAlloc"; |
6828 | 123 |
by (rtac injI 1); |
7347 | 124 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
6828 | 125 |
qed "inj_sysOfAlloc"; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
126 |
AddIffs [inj_sysOfAlloc]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
127 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
128 |
(*MUST BE AUTOMATED: even the statement of such results*) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
129 |
Goal "!!s. inv sysOfAlloc s = \ |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
130 |
\ (| allocGiv = allocGiv s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
131 |
\ allocAsk = allocAsk s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
132 |
\ allocRel = allocRel s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
133 |
\ 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
|
134 |
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
135 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
136 |
simpset() addsimps [sysOfAlloc_def, Let_def])); |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
137 |
qed "inv_sysOfAlloc_eq"; |
7538 | 138 |
Addsimps [inv_sysOfAlloc_eq]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
139 |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
140 |
Goal "surj sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
141 |
by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def]) 1); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
142 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
143 |
simpset() addsimps [sysOfAlloc_def, Let_def])); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
144 |
qed "surj_sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
145 |
AddIffs [surj_sysOfAlloc]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
146 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
147 |
Goal "bij sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
148 |
by (blast_tac (claset() addIs [bijI]) 1); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
149 |
qed "bij_sysOfAlloc"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
150 |
AddIffs [bij_sysOfAlloc]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
151 |
|
7365 | 152 |
(**SHOULD NOT BE NECESSARY: The various injections into the system |
153 |
state need to be treated symmetrically or done automatically*) |
|
7347 | 154 |
Goalw [sysOfClient_def] "inj sysOfClient"; |
155 |
by (rtac injI 1); |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
156 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
7347 | 157 |
qed "inj_sysOfClient"; |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
158 |
AddIffs [inj_sysOfClient]; |
6828 | 159 |
|
7347 | 160 |
(*MUST BE AUTOMATED: even the statement of such results*) |
161 |
Goal "!!s. inv sysOfClient s = \ |
|
162 |
\ (client s, \ |
|
163 |
\ (| allocGiv = allocGiv s, \ |
|
164 |
\ allocAsk = allocAsk s, \ |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
165 |
\ allocRel = allocRel s, \ |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
166 |
\ allocState_u.extra = systemState.extra s|) )"; |
7347 | 167 |
by (rtac (inj_sysOfClient RS inv_f_eq) 1); |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
168 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
169 |
simpset() addsimps [sysOfClient_def])); |
7365 | 170 |
qed "inv_sysOfClient_eq"; |
7689 | 171 |
Addsimps [inv_sysOfClient_eq]; |
6837 | 172 |
|
8286
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
173 |
Goal "surj sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
174 |
by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def]) 1); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
175 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
176 |
simpset() addsimps [sysOfClient_def])); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
177 |
qed "surj_sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
178 |
AddIffs [surj_sysOfClient]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
179 |
|
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
180 |
Goal "bij sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
181 |
by (blast_tac (claset() addIs [bijI]) 1); |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
182 |
qed "bij_sysOfClient"; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
183 |
AddIffs [bij_sysOfClient]; |
d4b895d3afa7
not working yet. partial conversion to use "rename" instead of "extend"
paulson
parents:
8251
diff
changeset
|
184 |
|
6837 | 185 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
186 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
187 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
188 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
189 |
(** o-simprules for client_map **) |
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 "fst o client_map = non_extra"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
192 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
193 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
194 |
simpset() addsimps [o_def, client_map_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
195 |
qed "fst_o_client_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
196 |
Addsimps (make_o_equivs fst_o_client_map); |
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 "snd o client_map = clientState_u.extra"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
199 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
200 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
201 |
simpset() addsimps [o_def, client_map_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
202 |
qed "snd_o_client_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
203 |
Addsimps (make_o_equivs snd_o_client_map); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
204 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
205 |
(** o-simprules for sysOfAlloc **) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
206 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
207 |
Goal "client o sysOfAlloc = fst o allocState_u.extra "; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
208 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
209 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
210 |
simpset() addsimps [o_def, sysOfAlloc_def, Let_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
211 |
qed "client_o_sysOfAlloc"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
212 |
Addsimps (make_o_equivs client_o_sysOfAlloc); |
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 |
Goal "allocGiv o sysOfAlloc = allocGiv"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
215 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
216 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
217 |
simpset() addsimps [sysOfAlloc_def, Let_def, o_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
218 |
qed "allocGiv_o_sysOfAlloc_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
219 |
Addsimps (make_o_equivs allocGiv_o_sysOfAlloc_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
220 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
221 |
Goal "allocAsk o sysOfAlloc = allocAsk"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
222 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
223 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
224 |
simpset() addsimps [sysOfAlloc_def, Let_def, o_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
225 |
qed "allocAsk_o_sysOfAlloc_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
226 |
Addsimps (make_o_equivs allocAsk_o_sysOfAlloc_eq); |
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 |
Goal "allocRel o sysOfAlloc = allocRel"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
229 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
230 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
231 |
simpset() addsimps [sysOfAlloc_def, Let_def, o_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
232 |
qed "allocRel_o_sysOfAlloc_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
233 |
Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
234 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
235 |
(** o-simprules for sysOfClient **) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
236 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
237 |
Goal "client o sysOfClient = fst"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
238 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
239 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
240 |
simpset() addsimps [o_def, sysOfClient_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
241 |
qed "client_o_sysOfClient"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
242 |
Addsimps (make_o_equivs client_o_sysOfClient); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
243 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
244 |
Goal "allocGiv o sysOfClient = allocGiv o snd "; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
245 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
246 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
247 |
simpset() addsimps [sysOfClient_def, o_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
248 |
qed "allocGiv_o_sysOfClient_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
249 |
Addsimps (make_o_equivs allocGiv_o_sysOfClient_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
250 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
251 |
Goal "allocAsk o sysOfClient = allocAsk o snd "; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
252 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
253 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
254 |
simpset() addsimps [sysOfClient_def, o_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
255 |
qed "allocAsk_o_sysOfClient_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
256 |
Addsimps (make_o_equivs allocAsk_o_sysOfClient_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
257 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
258 |
Goal "allocRel o sysOfClient = allocRel o snd "; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
259 |
by (rtac ext 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
260 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
261 |
simpset() addsimps [sysOfClient_def, o_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
262 |
qed "allocRel_o_sysOfClient_eq"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
263 |
Addsimps (make_o_equivs allocRel_o_sysOfClient_eq); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
264 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
265 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
266 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
267 |
(** |
7365 | 268 |
Open_locale "System"; |
269 |
||
270 |
val Alloc = thm "Alloc"; |
|
271 |
val Client = thm "Client"; |
|
272 |
val Network = thm "Network"; |
|
273 |
val System_def = thm "System_def"; |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
274 |
**) |
7365 | 275 |
|
276 |
AddIffs [finite_lessThan]; |
|
277 |
||
278 |
(*Client : <unfolded specification> *) |
|
279 |
val Client_Spec = |
|
280 |
rewrite_rule [client_spec_def, client_increasing_def, |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
281 |
client_bounded_def, client_progress_def, |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
282 |
client_preserves_def] Client; |
7365 | 283 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
284 |
val [Client_Increasing_ask, Client_Increasing_rel, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
285 |
Client_Bounded, Client_Progress, Client_preserves_giv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
286 |
Client_preserves_extra] = |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
287 |
Client_Spec |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
288 |
|> simplify (simpset() addsimps [guarantees_Int_right]) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
289 |
|> list_of_Int; |
7365 | 290 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
291 |
(** Showing that a renamed Client is in "preserves snd" **) |
7365 | 292 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
293 |
Goal "bij client_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
294 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
295 |
simpset() addsimps [client_map_def, non_extra_def, bij_def, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
296 |
inj_on_def, surj_def])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
297 |
by (res_inst_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
298 |
[("x", "(|giv=?a, ask=?b, rel=?c, clientState_u.extra=?e|)")] exI 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
299 |
by (Force_tac 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
300 |
qed "bij_client_map"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
301 |
AddIffs [bij_client_map]; |
7365 | 302 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
303 |
(**no longer needed |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
304 |
Goal "rename client_map Client : preserves snd"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
305 |
by (simp_tac (simpset() addsimps [Client_preserves_extra]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
306 |
qed "rename_Client_preserves_snd"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
307 |
**) |
7365 | 308 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
309 |
AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
310 |
Client_preserves_giv, Client_preserves_extra]; |
6828 | 311 |
|
312 |
||
7365 | 313 |
(*Network : <unfolded specification> *) |
314 |
val Network_Spec = |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
315 |
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
|
316 |
network_rel_def, network_preserves_def] Network; |
7365 | 317 |
|
318 |
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect |
|
319 |
exporting it from the locale*) |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
320 |
val [Network_Ask, Network_Giv, Network_Rel, |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
321 |
Network_preserves_allocGiv, Network_preserves_rel_ask] = |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
322 |
list_of_Int Network_Spec; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
323 |
|
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
324 |
AddIffs [Network_preserves_allocGiv]; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
325 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
326 |
Addsimps (Network_preserves_rel_ask |> simplify (simpset()) |> list_of_Int); |
7365 | 327 |
|
328 |
||
329 |
(*Alloc : <unfolded specification> *) |
|
330 |
val Alloc_Spec = |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
331 |
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
|
332 |
alloc_progress_def, alloc_preserves_def] Alloc; |
7365 | 333 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
334 |
val [Alloc_Increasing_0, Alloc_Safety, |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
335 |
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
|
336 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
337 |
(*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
|
338 |
val Alloc_Increasing = normalize Alloc_Increasing_0; |
7365 | 339 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
340 |
(*???????????????????????????????????????????????????????????????? |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
341 |
fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset()); |
7689 | 342 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
343 |
fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset()); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
344 |
*) |
7689 | 345 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
346 |
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
|
347 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
348 |
(** Components lemmas **) |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
349 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
350 |
(*Alternative is to say that System = Network Join F such that F preserves |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
351 |
certain state variables*) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
352 |
Goal "Network Join \ |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
353 |
\ ((rename sysOfClient \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
354 |
\ (plam x: lessThan Nclients. rename client_map Client)) Join \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
355 |
\ rename sysOfAlloc Alloc) \ |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
356 |
\ = System"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
357 |
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
|
358 |
qed "Network_component_System"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
359 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
360 |
Goal "(rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)) Join \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
361 |
\ (Network Join rename sysOfAlloc Alloc) = System"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
362 |
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
|
363 |
qed "Client_component_System"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
364 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
365 |
Goal "rename sysOfAlloc Alloc Join \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
366 |
\ ((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
|
367 |
\ Network) = System"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
368 |
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
|
369 |
qed "Alloc_component_System"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
370 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
371 |
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
|
372 |
Alloc_component_System]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
373 |
|
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
374 |
(** These preservation laws should be generated automatically **) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
375 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
376 |
AddIs [impOfSubs subset_preserves_o]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
377 |
Addsimps [impOfSubs subset_preserves_o]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
378 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
379 |
(*** Lemmas about "preserves" |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
380 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
381 |
val preserves_imp_preserves_apply = |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
382 |
impOfSubs subset_preserves_o |> simplify (simpset() addsimps [o_def]); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
383 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
384 |
Goal "F : preserves snd ==> rename sysOfClient F : preserves allocGiv"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
385 |
by (simp_tac (simpset() addsimps [rename_preserves]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
386 |
by (asm_simp_tac (simpset() addsimps [sysOfClient_def, o_def, split_def, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
387 |
preserves_imp_preserves_apply]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
388 |
qed "rename_sysOfClient_preserves_allocGiv"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
389 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
390 |
Goal "F : preserves snd ==> rename sysOfClient F : preserves allocAsk"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
391 |
by (simp_tac (simpset() addsimps [rename_preserves]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
392 |
by (asm_simp_tac (simpset() addsimps [sysOfClient_def, o_def, split_def, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
393 |
preserves_imp_preserves_apply]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
394 |
qed "rename_sysOfClient_preserves_allocAsk"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
395 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
396 |
Goal "F : preserves snd ==> rename sysOfClient F : preserves allocRel"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
397 |
by (simp_tac (simpset() addsimps [rename_preserves]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
398 |
by (asm_simp_tac (simpset() addsimps [sysOfClient_def, o_def, split_def, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
399 |
preserves_imp_preserves_apply]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
400 |
qed "rename_sysOfClient_preserves_allocRel"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
401 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
402 |
Addsimps [rename_sysOfClient_preserves_allocGiv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
403 |
rename_sysOfClient_preserves_allocAsk, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
404 |
rename_sysOfClient_preserves_allocRel]; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
405 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
406 |
AddIs [rename_sysOfClient_preserves_allocGiv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
407 |
rename_sysOfClient_preserves_allocAsk, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
408 |
rename_sysOfClient_preserves_allocRel]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
409 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
410 |
Goal "(rename sysOfClient F : preserves (v o client)) = \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
411 |
\ (F : preserves (v o fst))"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
412 |
by (simp_tac (simpset() addsimps [rename_preserves]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
413 |
by (asm_simp_tac (simpset() addsimps [sysOfClient_def, o_def, split_def]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
414 |
qed "rename_sysOfClient_preserves_client"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
415 |
AddIffs [rename_sysOfClient_preserves_client]; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
416 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
417 |
Goal "rename sysOfAlloc Alloc : preserves client"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
418 |
by (simp_tac (simpset() addsimps [rename_preserves]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
419 |
result(); |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
420 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
421 |
***) |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
422 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
423 |
(*Lifting Client_Increasing to systemState*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
424 |
Goal "i : I \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
425 |
\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
426 |
\ UNIV \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
427 |
\ guarantees[(funPair rel ask) o sub i o client] \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
428 |
\ Increasing (ask o sub i o client) Int \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
429 |
\ Increasing (rel o sub i o client)"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
430 |
by (simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
431 |
by (rtac guarantees_PLam_I 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
432 |
ba 2; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
433 |
(*preserves: routine reasoning*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
434 |
by (asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
435 |
(*the guarantee for "lift i (rename client_map Client)" *) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
436 |
by (asm_simp_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
437 |
(simpset() addsimps [lift_guarantees_eq_lift_inv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
438 |
rename_guarantees_eq_rename_inv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
439 |
bij_imp_bij_inv, surj_rename RS surj_range, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
440 |
bij_rename, bij_image_INT, bij_is_inj RS image_Int, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
441 |
rename_image_Increasing, inv_inv_eq]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
442 |
by (asm_simp_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
443 |
(simpset() addsimps [o_def, non_extra_def, guarantees_Int_right]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
444 |
qed "rename_Client_Increasing"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
445 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
446 |
(*Lifting Alloc_Increasing to systemState*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
447 |
Goal "i < Nclients \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
448 |
\ ==> rename sysOfAlloc Alloc : \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
449 |
\ UNIV guarantees[allocGiv] Increasing (sub i o allocGiv)"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
450 |
by (asm_simp_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
451 |
(simpset() addsimps [rename_guarantees_eq_rename_inv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
452 |
bij_imp_bij_inv, surj_rename RS surj_range, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
453 |
bij_rename, bij_image_INT, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
454 |
rename_image_Increasing, inv_inv_eq, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
455 |
Alloc_Increasing]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
456 |
qed "rename_Alloc_Increasing"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
457 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
458 |
Goal "i < Nclients \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
459 |
\ ==> System : Increasing (ask o sub i o client) Int \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
460 |
\ Increasing (rel o sub i o client)"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
461 |
by (rtac ([rename_Client_Increasing, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
462 |
Client_component_System] MRS component_guaranteesD) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
463 |
by Auto_tac; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
464 |
qed "System_Increasing"; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
465 |
|
7841 | 466 |
Goalw [System_def] |
467 |
"i < Nclients ==> System : Increasing (sub i o allocGiv)"; |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
468 |
by (rtac (rename_Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1); |
7841 | 469 |
by Auto_tac; |
470 |
qed "System_Increasing_allocGiv"; |
|
7365 | 471 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
472 |
AddSIs (list_of_Int System_Increasing); |
6828 | 473 |
|
7841 | 474 |
(** Follows consequences. |
475 |
The "Always (INT ...) formulation expresses the general safety property |
|
476 |
and allows it to be combined using Always_Int_rule below. **) |
|
477 |
||
8067 | 478 |
Goal |
479 |
"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
|
480 |
by (auto_tac (claset() addSIs [Network_Rel RS component_guaranteesD], |
8067 | 481 |
simpset())); |
482 |
qed "System_Follows_rel"; |
|
483 |
||
484 |
Goal |
|
485 |
"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
|
486 |
by (auto_tac (claset() addSIs [Network_Ask RS component_guaranteesD], |
8067 | 487 |
simpset())); |
488 |
qed "System_Follows_ask"; |
|
489 |
||
490 |
Goal |
|
491 |
"i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)"; |
|
492 |
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
|
493 |
rename_Alloc_Increasing RS component_guaranteesD], |
8067 | 494 |
simpset())); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
495 |
by (simp_tac (simpset() addsimps [o_def, non_extra_def]) 1); |
8067 | 496 |
qed "System_Follows_allocGiv"; |
497 |
||
7841 | 498 |
Goal "System : Always (INT i: lessThan Nclients. \ |
499 |
\ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})"; |
|
500 |
by (auto_tac (claset(), |
|
8067 | 501 |
simpset() addsimps [Always_INT_distrib])); |
502 |
by (etac (System_Follows_allocGiv RS Follows_Bounded) 1); |
|
7841 | 503 |
qed "Always_giv_le_allocGiv"; |
504 |
||
505 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
506 |
\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})"; |
|
8067 | 507 |
by (auto_tac (claset(), |
508 |
simpset() addsimps [Always_INT_distrib])); |
|
509 |
by (etac (System_Follows_ask RS Follows_Bounded) 1); |
|
7841 | 510 |
qed "Always_allocAsk_le_ask"; |
511 |
||
512 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
513 |
\ {s. (sub i o allocRel) s <= (rel o sub i o client) s})"; |
|
8067 | 514 |
by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel], |
515 |
simpset() addsimps [Always_INT_distrib])); |
|
7841 | 516 |
qed "Always_allocRel_le_rel"; |
517 |
||
518 |
||
519 |
(*** Proof of the safety property (1) ***) |
|
520 |
||
521 |
(*safety (1), step 1 is System_Increasing_rel*) |
|
522 |
||
7689 | 523 |
(*safety (1), step 2*) |
7365 | 524 |
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)"; |
8067 | 525 |
by (etac (System_Follows_rel RS Follows_Increasing1) 1); |
7365 | 526 |
qed "System_Increasing_allocRel"; |
6828 | 527 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
528 |
Goal "rename sysOfAlloc Alloc : \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
529 |
\ (INT i : lessThan Nclients. Increasing (sub i o allocRel)) \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
530 |
\ guarantees[allocGiv] \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
531 |
\ Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
532 |
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
533 |
by (asm_simp_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
534 |
(simpset() addsimps [rename_guarantees_eq_rename_inv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
535 |
bij_imp_bij_inv, bij_rename, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
536 |
bij_image_INT, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
537 |
rename_image_Increasing, rename_image_Always, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
538 |
inv_inv_eq, bij_image_Collect_eq]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
539 |
by (cut_facts_tac [Alloc_Safety] 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
540 |
by (full_simp_tac (simpset() addsimps [o_def]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
541 |
qed "rename_Alloc_Safety"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
542 |
|
7689 | 543 |
(*safety (1), step 3*) |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
544 |
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
|
545 |
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
546 |
by (rtac ([rename_Alloc_Safety, Alloc_component_System] MRS |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
547 |
component_guaranteesD) 1); |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
548 |
(*preserves*) |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
549 |
by (Simp_tac 2); |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
550 |
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 1); |
7538 | 551 |
qed "System_sum_bounded"; |
7537 | 552 |
|
7841 | 553 |
(** Follows reasoning **) |
554 |
||
7540 | 555 |
Goal "System : Always (INT i: lessThan Nclients. \ |
556 |
\ {s. (tokens o giv o sub i o client) s \ |
|
557 |
\ <= (tokens o sub i o allocGiv) s})"; |
|
7841 | 558 |
by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1); |
8067 | 559 |
by (auto_tac (claset() addIs [tokens_mono_prefix], |
560 |
simpset() addsimps [o_apply])); |
|
7841 | 561 |
qed "Always_tokens_giv_le_allocGiv"; |
7540 | 562 |
|
563 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
564 |
\ {s. (tokens o sub i o allocRel) s \ |
|
565 |
\ <= (tokens o rel o sub i o client) s})"; |
|
7841 | 566 |
by (rtac (Always_allocRel_le_rel RS Always_weaken) 1); |
8067 | 567 |
by (auto_tac (claset() addIs [tokens_mono_prefix], |
568 |
simpset() addsimps [o_apply])); |
|
7841 | 569 |
qed "Always_tokens_allocRel_le_rel"; |
7540 | 570 |
|
7841 | 571 |
(*safety (1), step 4 (final result!) *) |
8128 | 572 |
Goalw [system_safety_def] "System : system_safety"; |
7841 | 573 |
by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv, |
574 |
Always_tokens_allocRel_le_rel] RS Always_weaken) 1); |
|
7538 | 575 |
by Auto_tac; |
7540 | 576 |
by (rtac (sum_mono RS order_trans) 1); |
577 |
by (dtac order_trans 2); |
|
578 |
by (rtac ([order_refl, sum_mono] MRS add_le_mono) 2); |
|
579 |
by (assume_tac 3); |
|
7482 | 580 |
by Auto_tac; |
7540 | 581 |
qed "System_safety"; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
582 |
|
7689 | 583 |
|
584 |
(*** Proof of the progress property (2) ***) |
|
585 |
||
7965 | 586 |
(*Now there are proofs identical to System_Increasing_rel and |
7689 | 587 |
System_Increasing_allocRel: tactics needed!*) |
588 |
||
7841 | 589 |
(*progress (2), step 1 is System_Increasing_ask and System_Increasing_rel*) |
7689 | 590 |
|
7841 | 591 |
(*progress (2), step 2; see also System_Increasing_allocRel*) |
7689 | 592 |
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
|
593 |
by (etac (System_Follows_ask RS Follows_Increasing1) 1); |
7689 | 594 |
qed "System_Increasing_allocAsk"; |
595 |
||
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
596 |
(*progress (2), step 3*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
597 |
(*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
|
598 |
(though it is similar to that for Client_Increasing*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
599 |
Goal "i : I \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
600 |
\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
601 |
\ UNIV \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
602 |
\ guarantees[ask o sub i o client] \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
603 |
\ Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
604 |
by (simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
605 |
by (rtac guarantees_PLam_I 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
606 |
ba 2; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
607 |
(*preserves: routine reasoning*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
608 |
by (asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
609 |
(*the guarantee for "lift i (rename client_map Client)" *) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
610 |
by (asm_simp_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
611 |
(simpset() addsimps [lift_guarantees_eq_lift_inv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
612 |
rename_guarantees_eq_rename_inv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
613 |
bij_imp_bij_inv, surj_rename RS surj_range, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
614 |
bij_rename, bij_image_INT, bij_is_inj RS image_Int, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
615 |
rename_image_Always, inv_inv_eq, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
616 |
bij_image_Collect_eq]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
617 |
by (asm_simp_tac (simpset() addsimps [o_def, non_extra_def]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
618 |
qed "rename_Client_Bounded"; |
7841 | 619 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
620 |
Goal "i < Nclients \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
621 |
\ ==> System : Always \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
622 |
\ {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
|
623 |
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
|
624 |
Client_component_System] MRS component_guaranteesD) 1); |
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
625 |
by Auto_tac; |
7841 | 626 |
qed "System_Bounded_ask"; |
627 |
||
628 |
(*progress (2), step 4*) |
|
629 |
Goal "System : Always {s. ALL i : lessThan Nclients. \ |
|
630 |
\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}"; |
|
631 |
by (auto_tac (claset(), |
|
632 |
simpset() addsimps [Collect_ball_eq, Always_INT_distrib])); |
|
633 |
by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask] |
|
634 |
RS Always_weaken) 1); |
|
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
635 |
by (auto_tac (claset() addDs [set_mono], simpset())); |
7841 | 636 |
qed "System_Bounded_allocAsk"; |
637 |
||
7965 | 638 |
(*progress (2), step 5 is System_Increasing_allocGiv*) |
7841 | 639 |
|
7965 | 640 |
(*progress (2), step 6*) |
7841 | 641 |
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
|
642 |
by (etac (System_Follows_allocGiv RS Follows_Increasing1) 1); |
7841 | 643 |
qed "System_Increasing_giv"; |
644 |
||
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
645 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
646 |
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
647 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
648 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
649 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
650 |
(** A LOT of work just to lift "Client_Progress" to the array **) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
651 |
|
8311
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
652 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
653 |
Goal "i: I \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
654 |
\ ==> rename sysOfClient (plam x: I. rename client_map Client) \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
655 |
\ : Increasing (giv o sub i o client) \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
656 |
\ guarantees[funPair rel ask o sub i o client] \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
657 |
\ (INT h. {s. h <= (giv o sub i o client) s & \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
658 |
\ h pfixGe (ask o sub i o client) s} \ |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
659 |
\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
660 |
by (simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
661 |
by (rtac guarantees_PLam_I 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
662 |
ba 2; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
663 |
(*preserves: routine reasoning*) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
664 |
by (asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
665 |
(*the guarantee for "lift i (rename client_map Client)" *) |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
666 |
by (asm_simp_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
667 |
(simpset() addsimps [lift_guarantees_eq_lift_inv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
668 |
rename_guarantees_eq_rename_inv, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
669 |
bij_imp_bij_inv, surj_rename RS surj_range, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
670 |
bij_rename, bij_image_INT, bij_is_inj RS image_Int, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
671 |
(****rename_image_LeadsTo,***) rename_image_Increasing, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
672 |
inv_inv_eq, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
673 |
bij_image_Collect_eq]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
674 |
by (asm_simp_tac (simpset() addsimps [o_def, non_extra_def]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
675 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
676 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
677 |
by (rtac (lemma2 RS client_export project_guarantees_raw) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
678 |
by (assume_tac 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
679 |
by (rtac (client_export project_Increasing_I) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
680 |
by (Simp_tac 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
681 |
by (rtac INT_I 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
682 |
by (simp_tac (simpset() addsimps [o_apply]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
683 |
by (REPEAT (stac (client_export extend_set_eq_Collect RS sym) 1)); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
684 |
by (rtac (client_export project_Ensures_D) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
685 |
by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
686 |
by (asm_full_simp_tac |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
687 |
(simpset() addsimps [all_conj_distrib, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
688 |
Increasing_def, Stable_eq_stable, Join_stable, |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
689 |
extend_set_eq_Collect]) 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
690 |
by (Clarify_tac 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
691 |
by (dtac G_stable_sysOfClient 1); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
692 |
by (auto_tac (claset(), |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
693 |
simpset() addsimps [o_apply, client_export extend_set_eq_Collect])); |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
694 |
qed "rename_Client_Progress"; |
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
695 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
696 |
|
6218522253e7
new mostly working version; Alloc nearly converted to "Rename"
paulson
parents:
8286
diff
changeset
|
697 |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
698 |
|
7841 | 699 |
Goal "lift_prog i Client \ |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
700 |
\ : Increasing (giv o sub i) \ |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
701 |
\ guarantees[funPair rel ask o sub i] \ |
8041 | 702 |
\ (INT h. {s. h <= (giv o sub i) s & \ |
703 |
\ h pfixGe (ask o sub i) s} \ |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
704 |
\ Ensures {s. tokens h <= (tokens o rel o sub i) s})"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
705 |
by (rtac (Client_Progress RS drop_prog_guarantees_raw) 1); |
8128 | 706 |
by (rtac (lift_export project_Increasing_I) 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
707 |
by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1); |
8128 | 708 |
by (rtac INT_I 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
709 |
by (simp_tac (simpset() addsimps [o_apply]) 1); |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8128
diff
changeset
|
710 |
by (REPEAT (stac (lift_export extend_set_eq_Collect RS sym) 1)); |
8128 | 711 |
by (rtac (lift_export project_Ensures_D) 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
712 |
by (asm_full_simp_tac (simpset() addsimps [o_apply, lift_prog_correct, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
713 |
drop_prog_correct]) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
714 |
by (asm_full_simp_tac |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
715 |
(simpset() addsimps [all_conj_distrib, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
716 |
Increasing_def, Stable_eq_stable, Join_stable, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
717 |
lift_set_correct RS sym, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
718 |
Collect_eq_lift_set RS sym, |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
719 |
lift_prog_correct RS sym]) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
720 |
by (Clarify_tac 1); |
8128 | 721 |
by (dtac G_stable_lift_prog 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
722 |
by (auto_tac (claset(), |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
723 |
simpset() addsimps [o_apply])); |
7841 | 724 |
qed "Client_i_Progress"; |
725 |
||
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
726 |
Goal "i < Nclients \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
727 |
\ ==> (plam x: lessThan Nclients. Client) \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
728 |
\ : Increasing (giv o sub i) \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
729 |
\ guarantees[funPair rel ask o sub i] \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
730 |
\ (INT h. {s. h <= (giv o sub i) s & \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
731 |
\ h pfixGe (ask o sub i) s} \ |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
732 |
\ Ensures {s. tokens h <= (tokens o rel o sub i) s})"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
733 |
by (rtac guarantees_PLam_I 1); |
8128 | 734 |
by (rtac Client_i_Progress 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
735 |
by Auto_tac; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
736 |
val lemma2 = result(); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
737 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
738 |
|
7965 | 739 |
(*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
|
740 |
Goal |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
741 |
"System : (INT i : lessThan Nclients. \ |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
742 |
\ 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
|
743 |
\ h pfixGe (ask 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
|
744 |
\ Ensures {s. tokens h <= (tokens o rel o sub i o client) s})"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
745 |
by (rtac INT_I 1); |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
746 |
(*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
|
747 |
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
|
748 |
Client_component_System] MRS component_guaranteesD) 1); |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
749 |
by (asm_full_simp_tac |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
750 |
(simpset() addsimps [System_Increasing_giv]) 2); |
8128 | 751 |
by Auto_tac; |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
752 |
qed "System_Client_Progress"; |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
753 |
|
8067 | 754 |
val lemma = |
755 |
[System_Follows_ask RS Follows_Bounded, |
|
756 |
System_Follows_allocGiv RS Follows_LeadsTo] MRS Always_LeadsToD; |
|
8041 | 757 |
|
8067 | 758 |
val lemma2 = [lemma, |
759 |
System_Follows_ask RS Follows_Increasing1 RS IncreasingD] |
|
760 |
MRS PSP_Stable; |
|
761 |
||
762 |
Goal "i < Nclients \ |
|
763 |
\ ==> System : {s. h <= (sub i o allocGiv) s & \ |
|
764 |
\ h pfixGe (sub i o allocAsk) s} \ |
|
765 |
\ LeadsTo \ |
|
766 |
\ {s. h <= (giv o sub i o client) s & \ |
|
767 |
\ h pfixGe (ask o sub i o client) s}"; |
|
768 |
by (rtac single_LeadsTo_I 1); |
|
769 |
by (res_inst_tac [("k6", "h"), ("x2", "(sub i o allocAsk) s")] |
|
770 |
(lemma2 RS LeadsTo_weaken) 1); |
|
771 |
by Auto_tac; |
|
772 |
by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD, |
|
773 |
prefix_imp_pfixGe]) 1); |
|
774 |
val lemma3 = result(); |
|
775 |
||
776 |
||
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
777 |
(*progress (2), step 8: Client i's "release" action is visible system-wide*) |
8075 | 778 |
Goal "i < Nclients \ |
779 |
\ ==> System : {s. h <= (sub i o allocGiv) s & \ |
|
8067 | 780 |
\ h pfixGe (sub i o allocAsk) s} \ |
8075 | 781 |
\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s}"; |
8067 | 782 |
by (rtac LeadsTo_Trans 1); |
783 |
by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS |
|
8113 | 784 |
Follows_LeadsTo) 2); |
8067 | 785 |
by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2); |
786 |
by (rtac LeadsTo_Trans 1); |
|
787 |
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
|
788 |
by (blast_tac (claset() addIs [LeadsTo_Basis]) 2); |
8067 | 789 |
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
|
790 |
qed "System_Alloc_Client_Progress"; |
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
791 |
|
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
792 |
|
8075 | 793 |
|
8069
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
794 |
(*progress (2), step 9*) |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
795 |
Goal |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
796 |
"System : (INT i : lessThan Nclients. \ |
19b9f92ca503
working with weak LeadsTo in guarantees precondition\!
paulson
parents:
8067
diff
changeset
|
797 |
\ 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
|
798 |
\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
799 |
by (rtac ([Alloc_Progress, Alloc_component_System] |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
800 |
MRS component_guaranteesD) 1); |
8075 | 801 |
(*preserves*) |
802 |
by (asm_full_simp_tac (simpset() addsimps [o_def]) 2); |
|
803 |
(*the guarantees precondition*) |
|
804 |
by (auto_tac (claset(), |
|
805 |
simpset() addsimps [System_Increasing_allocRel, |
|
806 |
System_Increasing_allocAsk])); |
|
8113 | 807 |
by (rtac System_Bounded_allocAsk 1); |
8128 | 808 |
by (etac System_Alloc_Client_Progress 1); |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
809 |
qed "System_Alloc_Progress"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
810 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
811 |
|
8128 | 812 |
(*progress (2), step 10 (final result!) *) |
813 |
Goalw [system_progress_def] "System : system_progress"; |
|
814 |
by (Clarify_tac 1); |
|
815 |
by (rtac LeadsTo_Trans 1); |
|
816 |
by (etac (System_Follows_allocGiv RS Follows_LeadsTo_pfixLe) 2); |
|
817 |
by (rtac LeadsTo_Trans 1); |
|
818 |
by (cut_facts_tac [System_Alloc_Progress] 2); |
|
819 |
by (Blast_tac 2); |
|
820 |
by (etac (System_Follows_ask RS Follows_LeadsTo) 1); |
|
821 |
qed "System_Progress"; |
|
822 |
||
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
823 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
824 |
(*Ultimate goal*) |
8128 | 825 |
Goalw [system_spec_def] "System : system_spec"; |
826 |
by (blast_tac (claset() addIs [System_safety, System_Progress]) 1); |
|
827 |
qed "System_correct"; |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8113
diff
changeset
|
828 |