1(*  Title:      HOL/UNITY/Comp/Client.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4*)
5
6section\<open>Distributed Resource Management System: the Client\<close>
7
8theory Client imports "../Rename" AllocBase begin
9
10type_synonym
11  tokbag = nat     \<comment> \<open>tokbags could be multisets...or any ordered type?\<close>
12
13record state =
14  giv :: "tokbag list" \<comment> \<open>input history: tokens granted\<close>
15  ask :: "tokbag list" \<comment> \<open>output history: tokens requested\<close>
16  rel :: "tokbag list" \<comment> \<open>output history: tokens released\<close>
17  tok :: tokbag        \<comment> \<open>current token request\<close>
18
19record 'a state_d =
20  state +  
21  dummy :: 'a          \<comment> \<open>new variables\<close>
22
23
24(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
25
26  
27  (** Release some tokens **)
28  
29definition
30  rel_act :: "('a state_d * 'a state_d) set"
31  where "rel_act = {(s,s').
32                  \<exists>nrel. nrel = size (rel s) &
33                         s' = s (| rel := rel s @ [giv s!nrel] |) &
34                         nrel < size (giv s) &
35                         ask s!nrel \<le> giv s!nrel}"
36
37  (** Choose a new token requirement **)
38
39  (** Including s'=s suppresses fairness, allowing the non-trivial part
40      of the action to be ignored **)
41
42definition
43  tok_act :: "('a state_d * 'a state_d) set"
44  where "tok_act = {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
45  
46definition
47  ask_act :: "('a state_d * 'a state_d) set"
48  where "ask_act = {(s,s'). s'=s |
49                         (s' = s (|ask := ask s @ [tok s]|))}"
50
51definition
52  Client :: "'a state_d program"
53  where "Client =
54       mk_total_program
55            ({s. tok s \<in> atMost NbT &
56                 giv s = [] & ask s = [] & rel s = []},
57             {rel_act, tok_act, ask_act},
58             \<Union>G \<in> preserves rel Int preserves ask Int preserves tok.
59                   Acts G)"
60
61definition
62  (*Maybe want a special theory section to declare such maps*)
63  non_dummy :: "'a state_d => state"
64  where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
65
66definition
67  (*Renaming map to put a Client into the standard form*)
68  client_map :: "'a state_d => state*'a"
69  where "client_map = funPair non_dummy dummy"
70
71
72declare Client_def [THEN def_prg_Init, simp]
73declare Client_def [THEN def_prg_AllowedActs, simp]
74declare rel_act_def [THEN def_act_simp, simp]
75declare tok_act_def [THEN def_act_simp, simp]
76declare ask_act_def [THEN def_act_simp, simp]
77
78lemma Client_ok_iff [iff]:
79     "(Client ok G) =  
80      (G \<in> preserves rel & G \<in> preserves ask & G \<in> preserves tok & 
81       Client \<in> Allowed G)"
82by (auto simp add: ok_iff_Allowed Client_def [THEN def_total_prg_Allowed])
83
84
85text\<open>Safety property 1: ask, rel are increasing\<close>
86lemma increasing_ask_rel:
87     "Client \<in> UNIV guarantees Increasing ask Int Increasing rel"
88apply (auto intro!: increasing_imp_Increasing simp add: guar_def preserves_subset_increasing [THEN subsetD])
89apply (auto simp add: Client_def increasing_def)
90apply (safety, auto)+
91done
92
93declare nth_append [simp] append_one_prefix [simp]
94
95
96text\<open>Safety property 2: the client never requests too many tokens.
97      With no Substitution Axiom, we must prove the two invariants 
98      simultaneously.\<close>
99lemma ask_bounded_lemma:
100     "Client ok G   
101      ==> Client \<squnion> G \<in>   
102              Always ({s. tok s \<le> NbT}  Int   
103                      {s. \<forall>elt \<in> set (ask s). elt \<le> NbT})"
104apply auto
105apply (rule invariantI [THEN stable_Join_Always2], force) 
106 prefer 2
107 apply (fast elim!: preserves_subset_stable [THEN subsetD] intro!: stable_Int) 
108apply (simp add: Client_def, safety)
109apply (cut_tac m = "tok s" in NbT_pos [THEN mod_less_divisor], auto)
110done
111
112text\<open>export version, with no mention of tok in the postcondition, but
113  unfortunately tok must be declared local.\<close>
114lemma ask_bounded:
115     "Client \<in> UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}"
116apply (rule guaranteesI)
117apply (erule ask_bounded_lemma [THEN Always_weaken])
118apply (rule Int_lower2)
119done
120
121
122text\<open>** Towards proving the liveness property **\<close>
123
124lemma stable_rel_le_giv: "Client \<in> stable {s. rel s \<le> giv s}"
125by (simp add: Client_def, safety, auto)
126
127lemma Join_Stable_rel_le_giv:
128     "[| Client \<squnion> G \<in> Increasing giv;  G \<in> preserves rel |]  
129      ==> Client \<squnion> G \<in> Stable {s. rel s \<le> giv s}"
130by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto)
131
132lemma Join_Always_rel_le_giv:
133     "[| Client \<squnion> G \<in> Increasing giv;  G \<in> preserves rel |]  
134      ==> Client \<squnion> G \<in> Always {s. rel s \<le> giv s}"
135by (force intro: AlwaysI Join_Stable_rel_le_giv)
136
137lemma transient_lemma:
138     "Client \<in> transient {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}"
139apply (simp add: Client_def mk_total_program_def)
140apply (rule_tac act = rel_act in totalize_transientI)
141  apply (auto simp add: Domain_unfold Client_def)
142 apply (blast intro: less_le_trans prefix_length_le strict_prefix_length_less)
143apply (auto simp add: prefix_def genPrefix_iff_nth Ge_def)
144apply (blast intro: strict_prefix_length_less)
145done
146
147
148lemma induct_lemma:
149     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
150  ==> Client \<squnion> G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
151                      LeadsTo {s. k < rel s & rel s \<le> giv s &  
152                                  h \<le> giv s & h pfixGe ask s}"
153apply (rule single_LeadsTo_I)
154apply (frule increasing_ask_rel [THEN guaranteesD], auto)
155apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken])
156  apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int])
157     apply (erule_tac f = giv and x = "giv s" in IncreasingD)
158    apply (erule_tac f = ask and x = "ask s" in IncreasingD)
159   apply (erule_tac f = rel and x = "rel s" in IncreasingD)
160  apply (erule Join_Stable_rel_le_giv, blast)
161 apply (blast intro: order_less_imp_le order_trans)
162apply (blast intro: sym order_less_le [THEN iffD2] order_trans
163                    prefix_imp_pfixGe pfixGe_trans)
164done
165
166
167lemma rel_progress_lemma:
168     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
169  ==> Client \<squnion> G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
170                      LeadsTo {s. h \<le> rel s}"
171apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct)
172apply (auto simp add: vimage_def)
173apply (rule single_LeadsTo_I)
174apply (rule induct_lemma [THEN LeadsTo_weaken], auto)
175 apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
176apply (drule strict_prefix_length_less)+
177apply arith
178done
179
180
181lemma client_progress_lemma:
182     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
183      ==> Client \<squnion> G \<in> {s. h \<le> giv s & h pfixGe ask s}   
184                          LeadsTo {s. h \<le> rel s}"
185apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all) 
186apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L])
187  apply (blast intro: rel_progress_lemma) 
188 apply (rule subset_refl [THEN subset_imp_LeadsTo])
189apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
190done
191
192text\<open>Progress property: all tokens that are given will be released\<close>
193lemma client_progress:
194     "Client \<in>  
195       Increasing giv  guarantees   
196       (INT h. {s. h \<le> giv s & h pfixGe ask s} LeadsTo {s. h \<le> rel s})"
197apply (rule guaranteesI, clarify)
198apply (blast intro: client_progress_lemma)
199done
200
201text\<open>This shows that the Client won't alter other variables in any state
202  that it is combined with\<close>
203lemma client_preserves_dummy: "Client \<in> preserves dummy"
204by (simp add: Client_def preserves_def, clarify, safety, auto)
205
206
207text\<open>* Obsolete lemmas from first version of the Client *\<close>
208
209lemma stable_size_rel_le_giv:
210     "Client \<in> stable {s. size (rel s) \<le> size (giv s)}"
211by (simp add: Client_def, safety, auto)
212
213text\<open>clients return the right number of tokens\<close>
214lemma ok_guar_rel_prefix_giv:
215     "Client \<in> Increasing giv  guarantees  Always {s. rel s \<le> giv s}"
216apply (rule guaranteesI)
217apply (rule AlwaysI, force)
218apply (blast intro: Increasing_preserves_Stable stable_rel_le_giv)
219done
220
221
222end
223