5636
|
1 |
(* Title: HOL/UNITY/Client
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
|
|
6 |
Distributed Resource Management System: the Client
|
|
7 |
*)
|
|
8 |
|
|
9 |
|
|
10 |
(*MOVE higher-up: UNITY.thy or Traces.thy ???*)
|
|
11 |
|
|
12 |
(*[| stable acts C; constrains acts (C Int A) A |] ==> stable acts (C Int A)*)
|
|
13 |
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
|
|
14 |
|
|
15 |
|
|
16 |
(*"raw" notion of invariant. Yields a SET of programs*)
|
|
17 |
Goal "[| Init F<=A; stable (Acts F) A |] ==> F : invariant A";
|
|
18 |
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
|
|
19 |
qed "invariantI";
|
|
20 |
|
|
21 |
Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
|
|
22 |
"F : invariant A ==> Invariant F A";
|
|
23 |
by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
|
|
24 |
qed "invariant_imp_Invariant";
|
|
25 |
|
|
26 |
|
|
27 |
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
|
|
28 |
Goal "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)";
|
|
29 |
by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
|
|
30 |
qed "invariant_Int";
|
|
31 |
|
|
32 |
Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
|
|
33 |
"Invariant F A = (F : invariant (reachable F Int A))";
|
|
34 |
by (blast_tac (claset() addIs reachable.intrs) 1);
|
|
35 |
qed "Invariant_eq_invariant_reachable";
|
|
36 |
|
|
37 |
|
|
38 |
bind_thm ("invariant_includes_reachable",
|
|
39 |
invariant_imp_Invariant RS Invariant_includes_reachable);
|
|
40 |
|
|
41 |
Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
|
|
42 |
by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable,
|
|
43 |
stable_reachable,
|
|
44 |
impOfSubs invariant_includes_reachable]) 1);
|
|
45 |
qed "always_eq_UN_invariant";
|
|
46 |
|
|
47 |
Goal "F : always A = (EX I. F: invariant I & I <= A)";
|
|
48 |
by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
|
|
49 |
by (Blast_tac 1);
|
|
50 |
qed "always_iff_ex_invariant";
|
|
51 |
|
|
52 |
|
|
53 |
Goalw [increasing_def, stable_def, constrains_def]
|
|
54 |
"increasing f <= increasing (length o f)";
|
|
55 |
by Auto_tac;
|
|
56 |
by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
|
|
57 |
qed "increasing_length";
|
|
58 |
|
|
59 |
|
|
60 |
Goalw [increasing_def]
|
|
61 |
"increasing f <= {F. ALL z::nat. stable (Acts F) {s. z < f s}}";
|
|
62 |
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
|
|
63 |
by (Blast_tac 1);
|
|
64 |
qed "increasing_less";
|
|
65 |
|
|
66 |
|
|
67 |
Goal "[| F Join G : f localTo F; (s,s') : act; \
|
|
68 |
\ act : Acts G; act ~: Acts F |] ==> f s' = f s";
|
|
69 |
by (asm_full_simp_tac
|
|
70 |
(simpset() addsimps [localTo_def, Acts_Join, stable_def,
|
|
71 |
constrains_def]) 1);
|
|
72 |
by (Blast_tac 1);
|
|
73 |
qed "localTo_imp_equals";
|
|
74 |
|
|
75 |
|
|
76 |
Goal "[| Stable F A; transient (Acts F) C; \
|
|
77 |
\ reachable F <= (-A Un B Un C) |] ==> LeadsTo F A B";
|
|
78 |
by (etac reachable_LeadsTo_weaken 1);
|
|
79 |
by (rtac LeadsTo_Diff 1);
|
|
80 |
by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
|
|
81 |
by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
|
|
82 |
qed "Stable_transient_reachable_LeadsTo";
|
|
83 |
|
|
84 |
|
|
85 |
(**** things that definitely belong in Client.ML ****)
|
|
86 |
|
|
87 |
(*split_all_tac causes a big blow-up*)
|
|
88 |
claset_ref() := claset() delSWrapper "split_all_tac";
|
|
89 |
|
|
90 |
val Client_simp = Cli_prg_def RS def_prg_simps;
|
|
91 |
|
|
92 |
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
|
|
93 |
|
|
94 |
DelIffs [length_Suc_conv];
|
|
95 |
|
|
96 |
(*Simplification for records*)
|
|
97 |
Addsimps (thms"state.update_defs");
|
|
98 |
|
|
99 |
|
|
100 |
(*CAN THIS be generalized?
|
|
101 |
Importantly, the second case considers actions that are in G
|
|
102 |
and NOT in Cli_prg (needed to use localTo_imp_equals) *)
|
|
103 |
Goal "(act : Acts (Cli_prg Join G)) = \
|
|
104 |
\ (act : {Id, rel_act, tok_act, ask_act} | \
|
|
105 |
\ act : Acts G & act ~: Acts Cli_prg)";
|
|
106 |
by (asm_full_simp_tac (simpset() addsimps [Client_simp, Acts_Join]) 1);
|
|
107 |
(*don't unfold definitions of actions*)
|
|
108 |
by (blast_tac HOL_cs 1);
|
|
109 |
qed "Acts_Cli_Join_eq";
|
|
110 |
|
|
111 |
|
|
112 |
fun invariant_tac i =
|
|
113 |
rtac invariantI i THEN
|
|
114 |
auto_tac (claset(), simpset() addsimps [Client_simp]) THEN
|
|
115 |
constrains_tac i;
|
|
116 |
|
|
117 |
(*Safety property 1(a): ask is nondecreasing*)
|
|
118 |
Goalw [increasing_def] "Cli_prg: increasing ask";
|
|
119 |
by (auto_tac (claset(), simpset() addsimps [Client_simp]));
|
|
120 |
by (constrains_tac 1);
|
|
121 |
by Auto_tac;
|
|
122 |
qed "increasing_ask";
|
|
123 |
|
|
124 |
(*Safety property 1(b): rel is nondecreasing*)
|
|
125 |
Goalw [increasing_def] "Cli_prg: increasing rel";
|
|
126 |
by (auto_tac (claset(), simpset() addsimps [Client_simp]));
|
|
127 |
by (constrains_tac 1);
|
|
128 |
by Auto_tac;
|
|
129 |
qed "increasing_rel";
|
|
130 |
|
|
131 |
Addsimps [nth_append, append_one_prefix];
|
|
132 |
|
|
133 |
Goal "Cli_prg: invariant {s. tok s <= Max}";
|
|
134 |
by (invariant_tac 1);
|
|
135 |
by Auto_tac;
|
|
136 |
qed "tok_bounded";
|
|
137 |
|
|
138 |
(*Safety property 3: no client requests "too many" tokens.
|
|
139 |
With no Substitution Axiom, we must prove the two invariants
|
|
140 |
simultaneously. Could combine tok_bounded, stable_constrains_stable
|
|
141 |
and a rule invariant_implies_stable...
|
|
142 |
*)
|
|
143 |
Goal "Cli_prg: \
|
|
144 |
\ invariant ({s. tok s <= Max} Int \
|
|
145 |
\ {s. ALL n: lessThan (length (ask s)). ask s!n <= Max})";
|
|
146 |
by (invariant_tac 1);
|
|
147 |
by (auto_tac (claset() addSEs [less_SucE], simpset()));
|
|
148 |
qed "ask_bounded";
|
|
149 |
|
|
150 |
|
|
151 |
(*Safety property 2: clients return the right number of tokens*)
|
|
152 |
Goalw [increasing_def]
|
|
153 |
"Cli_prg : (increasing giv Int (rel localTo Cli_prg)) \
|
|
154 |
\ guarantees invariant {s. rel s <= giv s}";
|
|
155 |
by (rtac guaranteesI 1);
|
|
156 |
by (Clarify_tac 1);
|
|
157 |
by (invariant_tac 1);
|
|
158 |
by (subgoal_tac "rel s <= giv s'" 1);
|
|
159 |
by (force_tac (claset(),
|
|
160 |
simpset() addsimps [stable_def, constrains_def]) 2);
|
|
161 |
by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
|
|
162 |
(*we note that "rel" is local to Client*)
|
|
163 |
by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
|
|
164 |
qed "ok_guar_rel_prefix_giv";
|
|
165 |
|
|
166 |
|
|
167 |
(*** Towards proving the liveness property ***)
|
|
168 |
|
|
169 |
Goal "transient (Acts (Cli_prg Join G)) \
|
|
170 |
\ {s. length (giv s) = Suc k & \
|
|
171 |
\ length (rel s) = k & ask s ! k <= giv s ! k}";
|
|
172 |
by (res_inst_tac [("act", "rel_act")] transient_mem 1);
|
|
173 |
by (auto_tac (claset(),
|
|
174 |
simpset() addsimps [Domain_def, Acts_Join, Client_simp]));
|
|
175 |
qed "transient_lemma";
|
|
176 |
|
|
177 |
Goal "Cli_prg : \
|
|
178 |
\ (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
|
|
179 |
\ Int invariant giv_meets_ask) \
|
|
180 |
\ guarantees invariant {s. length (ask s) <= Suc (length (rel s)) & \
|
|
181 |
\ length (rel s) <= length (giv s)}";
|
|
182 |
by (rtac guaranteesI 1);
|
|
183 |
by (Clarify_tac 1);
|
|
184 |
by (dtac (impOfSubs increasing_length) 1);
|
|
185 |
by (invariant_tac 1);
|
|
186 |
by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
|
|
187 |
by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
|
|
188 |
by (force_tac (claset(),
|
|
189 |
simpset() addsimps [increasing_def, Acts_Join, stable_def,
|
|
190 |
constrains_def]) 1);
|
|
191 |
val lemma1 = result();
|
|
192 |
|
|
193 |
|
|
194 |
Goal "Cli_prg : \
|
|
195 |
\ (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
|
|
196 |
\ Int invariant giv_meets_ask) \
|
|
197 |
\ guarantees {F. LeadsTo F {s. k < length (giv s)} \
|
|
198 |
\ {s. k < length (rel s)}}";
|
|
199 |
by (rtac guaranteesI 1);
|
|
200 |
by (Clarify_tac 1);
|
|
201 |
by (rtac Stable_transient_reachable_LeadsTo 1);
|
|
202 |
by (res_inst_tac [("k", "k")] transient_lemma 2);
|
|
203 |
by (rtac stable_imp_Stable 1);
|
|
204 |
by (dtac (impOfSubs increasing_length) 1);
|
|
205 |
by (force_tac (claset(),
|
|
206 |
simpset() addsimps [increasing_def,
|
|
207 |
stable_def, constrains_def]) 1);
|
|
208 |
(** LEVEL 7 **)
|
|
209 |
(* Invariant (Cli_prg Join G)
|
|
210 |
(- {s. k < length (giv s)} Un {s. k < length (rel s)} Un
|
|
211 |
{s. length (giv s) = Suc k &
|
|
212 |
length (rel s) = k & ask s ! k <= giv s ! k})
|
|
213 |
*)
|
|
214 |
by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
|
|
215 |
by (Blast_tac 1);
|
|
216 |
by (auto_tac (claset() addSDs [invariant_includes_reachable],
|
|
217 |
simpset() addsimps [giv_meets_ask_def]));
|
|
218 |
qed "client_correct";
|