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 Addsimps [Client_def RS def_prg_Init, |
|
10 Client_def RS def_prg_AllowedActs]; |
|
11 program_defs_ref := [Client_def]; |
|
12 |
|
13 Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]); |
|
14 |
|
15 Goal "(Client ok G) = \ |
|
16 \ (G : preserves rel & G : preserves ask & G : preserves tok &\ |
|
17 \ Client : Allowed G)"; |
|
18 by (auto_tac (claset(), |
|
19 simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed])); |
|
20 qed "Client_ok_iff"; |
|
21 AddIffs [Client_ok_iff]; |
|
22 |
|
23 |
|
24 (*Safety property 1: ask, rel are increasing*) |
|
25 Goal "Client: UNIV guarantees Increasing ask Int Increasing rel"; |
|
26 by (auto_tac |
|
27 (claset() addSIs [increasing_imp_Increasing], |
|
28 simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing])); |
|
29 by (auto_tac (claset(), simpset() addsimps [increasing_def])); |
|
30 by (ALLGOALS constrains_tac); |
|
31 by Auto_tac; |
|
32 qed "increasing_ask_rel"; |
|
33 |
|
34 Addsimps [nth_append, append_one_prefix]; |
|
35 |
|
36 |
|
37 (*Safety property 2: the client never requests too many tokens. |
|
38 With no Substitution Axiom, we must prove the two invariants |
|
39 simultaneously. |
|
40 *) |
|
41 Goal "Client ok G \ |
|
42 \ ==> Client Join G : \ |
|
43 \ Always ({s. tok s <= NbT} Int \ |
|
44 \ {s. ALL elt : set (ask s). elt <= NbT})"; |
|
45 by Auto_tac; |
|
46 by (rtac (invariantI RS stable_Join_Always2) 1); |
|
47 by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable] |
|
48 addSIs [stable_Int]) 3); |
|
49 by (constrains_tac 2); |
|
50 by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2); |
|
51 by Auto_tac; |
|
52 qed "ask_bounded_lemma"; |
|
53 |
|
54 (*export version, with no mention of tok in the postcondition, but |
|
55 unfortunately tok must be declared local.*) |
|
56 Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"; |
|
57 by (rtac guaranteesI 1); |
|
58 by (etac (ask_bounded_lemma RS Always_weaken) 1); |
|
59 by (rtac Int_lower2 1); |
|
60 qed "ask_bounded"; |
|
61 |
|
62 |
|
63 (*** Towards proving the liveness property ***) |
|
64 |
|
65 Goal "Client: stable {s. rel s <= giv s}"; |
|
66 by (constrains_tac 1); |
|
67 by Auto_tac; |
|
68 qed "stable_rel_le_giv"; |
|
69 |
|
70 Goal "[| Client Join G : Increasing giv; G : preserves rel |] \ |
|
71 \ ==> Client Join G : Stable {s. rel s <= giv s}"; |
|
72 by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1); |
|
73 by Auto_tac; |
|
74 qed "Join_Stable_rel_le_giv"; |
|
75 |
|
76 Goal "[| Client Join G : Increasing giv; G : preserves rel |] \ |
|
77 \ ==> Client Join G : Always {s. rel s <= giv s}"; |
|
78 by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1); |
|
79 qed "Join_Always_rel_le_giv"; |
|
80 |
|
81 Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}"; |
|
82 by (res_inst_tac [("act", "rel_act")] transientI 1); |
|
83 by (auto_tac (claset(), |
|
84 simpset() addsimps [Domain_def, Client_def])); |
|
85 by (blast_tac (claset() addIs [less_le_trans, prefix_length_le, |
|
86 strict_prefix_length_less]) 1); |
|
87 by (auto_tac (claset(), |
|
88 simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def])); |
|
89 by (blast_tac (claset() addIs [strict_prefix_length_less]) 1); |
|
90 qed "transient_lemma"; |
|
91 |
|
92 |
|
93 Goal "[| Client Join G : Increasing giv; Client ok G |] \ |
|
94 \ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s} \ |
|
95 \ LeadsTo {s. k < rel s & rel s <= giv s & \ |
|
96 \ h <= giv s & h pfixGe ask s}"; |
|
97 by (rtac single_LeadsTo_I 1); |
|
98 by (ftac (increasing_ask_rel RS guaranteesD) 1); |
|
99 by Auto_tac; |
|
100 by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS |
|
101 leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1); |
|
102 by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1); |
|
103 by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1); |
|
104 by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1); |
|
105 by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1); |
|
106 by (etac Join_Stable_rel_le_giv 1); |
|
107 by (Blast_tac 1); |
|
108 by (blast_tac (claset() addIs [sym, order_less_le RS iffD2, |
|
109 order_trans, prefix_imp_pfixGe, |
|
110 pfixGe_trans]) 2); |
|
111 by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1); |
|
112 qed "induct_lemma"; |
|
113 |
|
114 |
|
115 Goal "[| Client Join G : Increasing giv; Client ok G |] \ |
|
116 \ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s} \ |
|
117 \ LeadsTo {s. h <= rel s}"; |
|
118 by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1); |
|
119 by (auto_tac (claset(), simpset() addsimps [vimage_def])); |
|
120 by (rtac single_LeadsTo_I 1); |
|
121 by (rtac (induct_lemma RS LeadsTo_weaken) 1); |
|
122 by Auto_tac; |
|
123 by (blast_tac (claset() addIs [order_less_le RS iffD2] |
|
124 addDs [common_prefix_linear]) 1); |
|
125 by (REPEAT (dtac strict_prefix_length_less 1)); |
|
126 by (arith_tac 1); |
|
127 qed "rel_progress_lemma"; |
|
128 |
|
129 |
|
130 Goal "[| Client Join G : Increasing giv; Client ok G |] \ |
|
131 \ ==> Client Join G : {s. h <= giv s & h pfixGe ask s} \ |
|
132 \ LeadsTo {s. h <= rel s}"; |
|
133 by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1); |
|
134 by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS |
|
135 LeadsTo_Un RS LeadsTo_weaken_L) 3); |
|
136 by Auto_tac; |
|
137 by (blast_tac (claset() addIs [order_less_le RS iffD2] |
|
138 addDs [common_prefix_linear]) 1); |
|
139 qed "client_progress_lemma"; |
|
140 |
|
141 (*Progress property: all tokens that are given will be released*) |
|
142 Goal "Client : \ |
|
143 \ Increasing giv guarantees \ |
|
144 \ (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})"; |
|
145 by (rtac guaranteesI 1); |
|
146 by (Clarify_tac 1); |
|
147 by (blast_tac (claset() addIs [client_progress_lemma]) 1); |
|
148 qed "client_progress"; |
|
149 |
|
150 (*This shows that the Client won't alter other variables in any state |
|
151 that it is combined with*) |
|
152 Goal "Client : preserves dummy"; |
|
153 by (rewtac preserves_def); |
|
154 by Auto_tac; |
|
155 by (constrains_tac 1); |
|
156 by Auto_tac; |
|
157 qed "client_preserves_dummy"; |
|
158 |
|
159 |
|
160 (** Obsolete lemmas from first version of the Client **) |
|
161 |
|
162 Goal "Client: stable {s. size (rel s) <= size (giv s)}"; |
|
163 by (constrains_tac 1); |
|
164 by Auto_tac; |
|
165 qed "stable_size_rel_le_giv"; |
|
166 |
|
167 (*clients return the right number of tokens*) |
|
168 Goal "Client : Increasing giv guarantees Always {s. rel s <= giv s}"; |
|
169 by (rtac guaranteesI 1); |
|
170 by (rtac AlwaysI 1); |
|
171 by (Force_tac 1); |
|
172 by (blast_tac (claset() addIs [Increasing_preserves_Stable, |
|
173 stable_rel_le_giv]) 1); |
|
174 qed "ok_guar_rel_prefix_giv"; |
|