author | paulson |
Thu, 02 Jun 2005 13:17:06 +0200 | |
changeset 16183 | 052d9aba392d |
parent 15634 | bca33c49b083 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
1 |
(* Title: ZF/UNITY/ClientImpl.thy |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
4 |
Copyright 2002 University of Cambridge |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
5 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
6 |
Distributed Resource Management System: Client Implementation |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
7 |
*) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
8 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
9 |
|
14061 | 10 |
theory ClientImpl = AllocBase + Guar: |
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
11 |
|
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
12 |
consts |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
13 |
ask :: i (* input history: tokens requested *) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
14 |
giv :: i (* output history: tokens granted *) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
15 |
rel :: i (* input history: tokens released *) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
16 |
tok :: i (* the number of available tokens *) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
17 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
18 |
translations |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
19 |
"ask" == "Var(Nil)" |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
20 |
"giv" == "Var([0])" |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
21 |
"rel" == "Var([1])" |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
22 |
"tok" == "Var([2])" |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
23 |
|
14061 | 24 |
axioms |
25 |
type_assumes: |
|
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
26 |
"type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
27 |
type_of(rel) = list(tokbag) & type_of(tok) = nat" |
14061 | 28 |
default_val_assumes: |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
29 |
"default_val(ask) = Nil & default_val(giv) = Nil & |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
30 |
default_val(rel) = Nil & default_val(tok) = 0" |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
31 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
32 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
33 |
(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
34 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
35 |
constdefs |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
36 |
(** Release some client_tokens **) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
37 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
38 |
client_rel_act ::i |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
39 |
"client_rel_act == |
14061 | 40 |
{<s,t> \<in> state*state. |
41 |
\<exists>nrel \<in> nat. nrel = length(s`rel) & |
|
14057 | 42 |
t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) & |
43 |
nrel < length(s`giv) & |
|
14061 | 44 |
nth(nrel, s`ask) \<le> nth(nrel, s`giv)}" |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
45 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
46 |
(** Choose a new token requirement **) |
14057 | 47 |
(** Including t=s suppresses fairness, allowing the non-trivial part |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
48 |
of the action to be ignored **) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
49 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
50 |
client_tok_act :: i |
14061 | 51 |
"client_tok_act == {<s,t> \<in> state*state. t=s | |
14057 | 52 |
t = s(tok:=succ(s`tok mod NbT))}" |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
53 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
54 |
client_ask_act :: i |
14061 | 55 |
"client_ask_act == {<s,t> \<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}" |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
56 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
57 |
client_prog :: i |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
58 |
"client_prog == |
14061 | 59 |
mk_program({s \<in> state. s`tok \<le> NbT & s`giv = Nil & |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
60 |
s`ask = Nil & s`rel = Nil}, |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
61 |
{client_rel_act, client_tok_act, client_ask_act}, |
14061 | 62 |
\<Union>G \<in> preserves(lift(rel)) Int |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
63 |
preserves(lift(ask)) Int |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
64 |
preserves(lift(tok)). Acts(G))" |
14061 | 65 |
|
66 |
||
67 |
declare type_assumes [simp] default_val_assumes [simp] |
|
68 |
(* This part should be automated *) |
|
69 |
||
70 |
lemma ask_value_type [simp,TC]: "s \<in> state ==> s`ask \<in> list(nat)" |
|
71 |
apply (unfold state_def) |
|
72 |
apply (drule_tac a = ask in apply_type, auto) |
|
73 |
done |
|
74 |
||
75 |
lemma giv_value_type [simp,TC]: "s \<in> state ==> s`giv \<in> list(nat)" |
|
76 |
apply (unfold state_def) |
|
77 |
apply (drule_tac a = giv in apply_type, auto) |
|
78 |
done |
|
79 |
||
80 |
lemma rel_value_type [simp,TC]: "s \<in> state ==> s`rel \<in> list(nat)" |
|
81 |
apply (unfold state_def) |
|
82 |
apply (drule_tac a = rel in apply_type, auto) |
|
83 |
done |
|
84 |
||
85 |
lemma tok_value_type [simp,TC]: "s \<in> state ==> s`tok \<in> nat" |
|
86 |
apply (unfold state_def) |
|
87 |
apply (drule_tac a = tok in apply_type, auto) |
|
88 |
done |
|
89 |
||
90 |
(** The Client Program **) |
|
91 |
||
92 |
lemma client_type [simp,TC]: "client_prog \<in> program" |
|
93 |
apply (unfold client_prog_def) |
|
94 |
apply (simp (no_asm)) |
|
95 |
done |
|
96 |
||
97 |
declare client_prog_def [THEN def_prg_Init, simp] |
|
98 |
declare client_prog_def [THEN def_prg_AllowedActs, simp] |
|
99 |
ML |
|
100 |
{* |
|
101 |
program_defs_ref := [thm"client_prog_def"] |
|
102 |
*} |
|
103 |
||
104 |
declare client_rel_act_def [THEN def_act_simp, simp] |
|
105 |
declare client_tok_act_def [THEN def_act_simp, simp] |
|
106 |
declare client_ask_act_def [THEN def_act_simp, simp] |
|
107 |
||
108 |
lemma client_prog_ok_iff: |
|
109 |
"\<forall>G \<in> program. (client_prog ok G) <-> |
|
110 |
(G \<in> preserves(lift(rel)) & G \<in> preserves(lift(ask)) & |
|
111 |
G \<in> preserves(lift(tok)) & client_prog \<in> Allowed(G))" |
|
112 |
by (auto simp add: ok_iff_Allowed client_prog_def [THEN def_prg_Allowed]) |
|
113 |
||
114 |
lemma client_prog_preserves: |
|
115 |
"client_prog:(\<Inter>x \<in> var-{ask, rel, tok}. preserves(lift(x)))" |
|
116 |
apply (rule Inter_var_DiffI, force) |
|
117 |
apply (rule ballI) |
|
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
118 |
apply (rule preservesI, safety, auto) |
14061 | 119 |
done |
120 |
||
121 |
||
122 |
lemma preserves_lift_imp_stable: |
|
123 |
"G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})"; |
|
124 |
apply (drule preserves_imp_stable) |
|
125 |
apply (simp add: lift_def) |
|
126 |
done |
|
127 |
||
128 |
lemma preserves_imp_prefix: |
|
129 |
"G \<in> preserves(lift(ff)) |
|
130 |
==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})"; |
|
131 |
by (erule preserves_lift_imp_stable) |
|
132 |
||
133 |
(*Safety property 1: ask, rel are increasing: (24) *) |
|
134 |
lemma client_prog_Increasing_ask_rel: |
|
135 |
"client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))" |
|
136 |
apply (unfold guar_def) |
|
137 |
apply (auto intro!: increasing_imp_Increasing |
|
138 |
simp add: client_prog_ok_iff increasing_def preserves_imp_prefix) |
|
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
139 |
apply (safety, force, force)+ |
14061 | 140 |
done |
141 |
||
142 |
declare nth_append [simp] append_one_prefix [simp] |
|
143 |
||
144 |
lemma NbT_pos2: "0<NbT" |
|
145 |
apply (cut_tac NbT_pos) |
|
146 |
apply (rule Ord_0_lt, auto) |
|
147 |
done |
|
148 |
||
149 |
(*Safety property 2: the client never requests too many tokens. |
|
150 |
With no Substitution Axiom, we must prove the two invariants simultaneously. *) |
|
151 |
||
152 |
lemma ask_Bounded_lemma: |
|
153 |
"[| client_prog ok G; G \<in> program |] |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
154 |
==> client_prog \<squnion> G \<in> |
14061 | 155 |
Always({s \<in> state. s`tok \<le> NbT} Int |
156 |
{s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})" |
|
157 |
apply (rotate_tac -1) |
|
158 |
apply (auto simp add: client_prog_ok_iff) |
|
159 |
apply (rule invariantI [THEN stable_Join_Always2], force) |
|
160 |
prefer 2 |
|
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
161 |
apply (fast intro: stable_Int preserves_lift_imp_stable, safety) |
14061 | 162 |
apply (auto dest: ActsD) |
163 |
apply (cut_tac NbT_pos) |
|
164 |
apply (rule NbT_pos2 [THEN mod_less_divisor]) |
|
165 |
apply (auto dest: ActsD preserves_imp_eq simp add: set_of_list_append) |
|
166 |
done |
|
167 |
||
168 |
(* Export version, with no mention of tok in the postcondition, but |
|
169 |
unfortunately tok must be declared local.*) |
|
170 |
lemma client_prog_ask_Bounded: |
|
171 |
"client_prog \<in> program guarantees |
|
172 |
Always({s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})" |
|
173 |
apply (rule guaranteesI) |
|
174 |
apply (erule ask_Bounded_lemma [THEN Always_weaken], auto) |
|
175 |
done |
|
176 |
||
177 |
(*** Towards proving the liveness property ***) |
|
178 |
||
179 |
lemma client_prog_stable_rel_le_giv: |
|
180 |
"client_prog \<in> stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})" |
|
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
181 |
by (safety, auto) |
14061 | 182 |
|
183 |
lemma client_prog_Join_Stable_rel_le_giv: |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
184 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |] |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
185 |
==> client_prog \<squnion> G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})" |
14061 | 186 |
apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable]) |
187 |
apply (auto simp add: lift_def) |
|
188 |
done |
|
189 |
||
190 |
lemma client_prog_Join_Always_rel_le_giv: |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
191 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |] |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
192 |
==> client_prog \<squnion> G \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})" |
14061 | 193 |
by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv) |
194 |
||
195 |
lemma def_act_eq: |
|
196 |
"A == {<s, t> \<in> state*state. P(s, t)} ==> A={<s, t> \<in> state*state. P(s, t)}" |
|
197 |
by auto |
|
198 |
||
199 |
lemma act_subset: "A={<s,t> \<in> state*state. P(s, t)} ==> A<=state*state" |
|
200 |
by auto |
|
201 |
||
202 |
lemma transient_lemma: |
|
203 |
"client_prog \<in> |
|
204 |
transient({s \<in> state. s`rel = k & <k, h> \<in> strict_prefix(nat) |
|
205 |
& <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask})" |
|
206 |
apply (rule_tac act = client_rel_act in transientI) |
|
207 |
apply (simp (no_asm) add: client_prog_def [THEN def_prg_Acts]) |
|
208 |
apply (simp (no_asm) add: client_rel_act_def [THEN def_act_eq, THEN act_subset]) |
|
209 |
apply (auto simp add: client_prog_def [THEN def_prg_Acts] domain_def) |
|
210 |
apply (rule ReplaceI) |
|
211 |
apply (rule_tac x = "x (rel:= x`rel @ [nth (length (x`rel), x`giv) ]) " in exI) |
|
212 |
apply (auto intro!: state_update_type app_type length_type nth_type, auto) |
|
213 |
apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt) |
|
214 |
apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt) |
|
215 |
apply (simp (no_asm_use) add: gen_prefix_iff_nth) |
|
216 |
apply (subgoal_tac "h \<in> list(nat)") |
|
217 |
apply (simp_all (no_asm_simp) add: prefix_type [THEN subsetD, THEN SigmaD1]) |
|
218 |
apply (auto simp add: prefix_def Ge_def) |
|
219 |
apply (drule strict_prefix_length_lt) |
|
220 |
apply (drule_tac x = "length (x`rel) " in spec) |
|
221 |
apply auto |
|
222 |
apply (simp (no_asm_use) add: gen_prefix_iff_nth) |
|
223 |
apply (auto simp add: id_def lam_def) |
|
224 |
done |
|
225 |
||
226 |
lemma strict_prefix_is_prefix: |
|
227 |
"<xs, ys> \<in> strict_prefix(A) <-> <xs, ys> \<in> prefix(A) & xs\<noteq>ys" |
|
228 |
apply (unfold strict_prefix_def id_def lam_def) |
|
229 |
apply (auto dest: prefix_type [THEN subsetD]) |
|
230 |
done |
|
231 |
||
232 |
lemma induct_lemma: |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
233 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
234 |
==> client_prog \<squnion> G \<in> |
14061 | 235 |
{s \<in> state. s`rel = k & <k,h> \<in> strict_prefix(nat) |
236 |
& <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask} |
|
237 |
LeadsTo {s \<in> state. <k, s`rel> \<in> strict_prefix(nat) |
|
238 |
& <s`rel, s`giv> \<in> prefix(nat) & |
|
239 |
<h, s`giv> \<in> prefix(nat) & |
|
240 |
h pfixGe s`ask}" |
|
241 |
apply (rule single_LeadsTo_I) |
|
242 |
prefer 2 apply simp |
|
243 |
apply (frule client_prog_Increasing_ask_rel [THEN guaranteesD]) |
|
244 |
apply (rotate_tac [3] 2) |
|
245 |
apply (auto simp add: client_prog_ok_iff) |
|
246 |
apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken]) |
|
247 |
apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int]) |
|
248 |
apply (erule_tac f = "lift (giv) " and a = "s`giv" in Increasing_imp_Stable) |
|
249 |
apply (simp (no_asm_simp)) |
|
250 |
apply (erule_tac f = "lift (ask) " and a = "s`ask" in Increasing_imp_Stable) |
|
251 |
apply (simp (no_asm_simp)) |
|
252 |
apply (erule_tac f = "lift (rel) " and a = "s`rel" in Increasing_imp_Stable) |
|
253 |
apply (simp (no_asm_simp)) |
|
254 |
apply (erule client_prog_Join_Stable_rel_le_giv, blast, simp_all) |
|
255 |
prefer 2 |
|
256 |
apply (blast intro: sym strict_prefix_is_prefix [THEN iffD2] prefix_trans prefix_imp_pfixGe pfixGe_trans) |
|
257 |
apply (auto intro: strict_prefix_is_prefix [THEN iffD1, THEN conjunct1] |
|
258 |
prefix_trans) |
|
259 |
done |
|
260 |
||
261 |
lemma rel_progress_lemma: |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
262 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
263 |
==> client_prog \<squnion> G \<in> |
14061 | 264 |
{s \<in> state. <s`rel, h> \<in> strict_prefix(nat) |
265 |
& <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask} |
|
266 |
LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}" |
|
267 |
apply (rule_tac f = "\<lambda>x \<in> state. length(h) #- length(x`rel)" |
|
268 |
in LessThan_induct) |
|
269 |
apply (auto simp add: vimage_def) |
|
270 |
prefer 2 apply (force simp add: lam_def) |
|
271 |
apply (rule single_LeadsTo_I) |
|
272 |
prefer 2 apply simp |
|
273 |
apply (subgoal_tac "h \<in> list(nat)") |
|
274 |
prefer 2 apply (blast dest: prefix_type [THEN subsetD]) |
|
275 |
apply (rule induct_lemma [THEN LeadsTo_weaken]) |
|
276 |
apply (simp add: length_type lam_def) |
|
277 |
apply (auto intro: strict_prefix_is_prefix [THEN iffD2] |
|
278 |
dest: common_prefix_linear prefix_type [THEN subsetD]) |
|
279 |
apply (erule swap) |
|
280 |
apply (rule imageI) |
|
281 |
apply (force dest!: simp add: lam_def) |
|
282 |
apply (simp add: length_type lam_def, clarify) |
|
283 |
apply (drule strict_prefix_length_lt)+ |
|
284 |
apply (drule less_imp_succ_add, simp)+ |
|
285 |
apply clarify |
|
286 |
apply simp |
|
287 |
apply (erule diff_le_self [THEN ltD]) |
|
288 |
done |
|
289 |
||
290 |
lemma progress_lemma: |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
291 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
292 |
==> client_prog \<squnion> G |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
293 |
\<in> {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask} |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
294 |
LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}" |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
295 |
apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
296 |
assumption) |
14061 | 297 |
apply (force simp add: client_prog_ok_iff) |
298 |
apply (rule LeadsTo_weaken_L) |
|
299 |
apply (rule LeadsTo_Un [OF rel_progress_lemma |
|
300 |
subset_refl [THEN subset_imp_LeadsTo]]) |
|
301 |
apply (auto intro: strict_prefix_is_prefix [THEN iffD2] |
|
302 |
dest: common_prefix_linear prefix_type [THEN subsetD]) |
|
303 |
done |
|
304 |
||
305 |
(*Progress property: all tokens that are given will be released*) |
|
306 |
lemma client_prog_progress: |
|
307 |
"client_prog \<in> Incr(lift(giv)) guarantees |
|
308 |
(\<Inter>h \<in> list(nat). {s \<in> state. <h, s`giv> \<in> prefix(nat) & |
|
309 |
h pfixGe s`ask} LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)})" |
|
310 |
apply (rule guaranteesI) |
|
311 |
apply (blast intro: progress_lemma, auto) |
|
312 |
done |
|
313 |
||
314 |
lemma client_prog_Allowed: |
|
315 |
"Allowed(client_prog) = |
|
316 |
preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok))" |
|
317 |
apply (cut_tac v = "lift (ask)" in preserves_type) |
|
318 |
apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed] |
|
319 |
cons_Int_distrib safety_prop_Acts_iff) |
|
320 |
done |
|
321 |
||
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
322 |
end |