author | haftmann |
Fri, 15 Feb 2019 07:11:09 +0000 | |
changeset 69813 | 9d94a6c95113 |
parent 69768 | 7e4966eaf781 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/Comp/Alloc.thy |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 1998 University of Cambridge |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
Specification of Chandy and Charpentier's Allocator |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
|
17310 | 8 |
theory Alloc |
21710 | 9 |
imports AllocBase "../PPROD" |
17310 | 10 |
begin |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
|
63146 | 12 |
subsection\<open>State definitions. OUTPUT variables are locals\<close> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
record clientState = |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
15 |
giv :: "nat list" \<comment> \<open>client's INPUT history: tokens GRANTED\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
16 |
ask :: "nat list" \<comment> \<open>client's OUTPUT history: tokens REQUESTED\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
17 |
rel :: "nat list" \<comment> \<open>client's OUTPUT history: tokens RELEASED\<close> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
record 'a clientState_d = |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
clientState + |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
21 |
dummy :: 'a \<comment> \<open>dummy field for new variables\<close> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
|
36866 | 23 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
24 |
\<comment> \<open>DUPLICATED FROM Client.thy, but with "tok" removed\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
25 |
\<comment> \<open>Maybe want a special theory section to declare such maps\<close> |
17310 | 26 |
non_dummy :: "'a clientState_d => clientState" |
36866 | 27 |
where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s|)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
|
36866 | 29 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
30 |
\<comment> \<open>Renaming map to put a Client into the standard form\<close> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
client_map :: "'a clientState_d => clientState*'a" |
36866 | 32 |
where "client_map = funPair non_dummy dummy" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
|
24147 | 34 |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
record allocState = |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
36 |
allocGiv :: "nat => nat list" \<comment> \<open>OUTPUT history: source of "giv" for i\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
37 |
allocAsk :: "nat => nat list" \<comment> \<open>INPUT: allocator's copy of "ask" for i\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
38 |
allocRel :: "nat => nat list" \<comment> \<open>INPUT: allocator's copy of "rel" for i\<close> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
40 |
record 'a allocState_d = |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
41 |
allocState + |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
42 |
dummy :: 'a \<comment> \<open>dummy field for new variables\<close> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
43 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
44 |
record 'a systemState = |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
45 |
allocState + |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
46 |
client :: "nat => clientState" \<comment> \<open>states of all clients\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
47 |
dummy :: 'a \<comment> \<open>dummy field for new variables\<close> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
48 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
49 |
|
67445 | 50 |
subsubsection \<open>Resource allocation system specification\<close> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
51 |
|
36866 | 52 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
53 |
\<comment> \<open>spec (1)\<close> |
17310 | 54 |
system_safety :: "'a systemState program set" |
36866 | 55 |
where "system_safety = |
61954 | 56 |
Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o giv o sub i o client)s) |
57 |
\<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o rel o sub i o client)s)}" |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
58 |
|
36866 | 59 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
60 |
\<comment> \<open>spec (2)\<close> |
17310 | 61 |
system_progress :: "'a systemState program set" |
36866 | 62 |
where "system_progress = (INT i : lessThan Nclients. |
24147 | 63 |
INT h. |
64 |
{s. h \<le> (ask o sub i o client)s} LeadsTo |
|
36866 | 65 |
{s. h pfixLe (giv o sub i o client) s})" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
66 |
|
36866 | 67 |
definition |
17310 | 68 |
system_spec :: "'a systemState program set" |
36866 | 69 |
where "system_spec = system_safety Int system_progress" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
70 |
|
67445 | 71 |
|
72 |
subsubsection \<open>Client specification (required)\<close> |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
73 |
|
36866 | 74 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
75 |
\<comment> \<open>spec (3)\<close> |
17310 | 76 |
client_increasing :: "'a clientState_d program set" |
36866 | 77 |
where "client_increasing = UNIV guarantees Increasing ask Int Increasing rel" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
78 |
|
36866 | 79 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
80 |
\<comment> \<open>spec (4)\<close> |
17310 | 81 |
client_bounded :: "'a clientState_d program set" |
67613 | 82 |
where "client_bounded = UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
83 |
|
36866 | 84 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
85 |
\<comment> \<open>spec (5)\<close> |
17310 | 86 |
client_progress :: "'a clientState_d program set" |
36866 | 87 |
where "client_progress = |
24147 | 88 |
Increasing giv guarantees |
89 |
(INT h. {s. h \<le> giv s & h pfixGe ask s} |
|
90 |
LeadsTo {s. tokens h \<le> (tokens o rel) s})" |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
91 |
|
36866 | 92 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
93 |
\<comment> \<open>spec: preserves part\<close> |
17310 | 94 |
client_preserves :: "'a clientState_d program set" |
36866 | 95 |
where "client_preserves = preserves giv Int preserves clientState_d.dummy" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
96 |
|
36866 | 97 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
98 |
\<comment> \<open>environmental constraints\<close> |
17310 | 99 |
client_allowed_acts :: "'a clientState_d program set" |
36866 | 100 |
where "client_allowed_acts = |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
101 |
{F. AllowedActs F = |
69325 | 102 |
insert Id (\<Union> (Acts ` preserves (funPair rel ask)))}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
103 |
|
36866 | 104 |
definition |
17310 | 105 |
client_spec :: "'a clientState_d program set" |
36866 | 106 |
where "client_spec = client_increasing Int client_bounded Int client_progress |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
107 |
Int client_allowed_acts Int client_preserves" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
108 |
|
67445 | 109 |
|
110 |
subsubsection \<open>Allocator specification (required)\<close> |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
111 |
|
36866 | 112 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
113 |
\<comment> \<open>spec (6)\<close> |
17310 | 114 |
alloc_increasing :: "'a allocState_d program set" |
36866 | 115 |
where "alloc_increasing = |
24147 | 116 |
UNIV guarantees |
117 |
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))" |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
118 |
|
36866 | 119 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
120 |
\<comment> \<open>spec (7)\<close> |
17310 | 121 |
alloc_safety :: "'a allocState_d program set" |
36866 | 122 |
where "alloc_safety = |
24147 | 123 |
(INT i : lessThan Nclients. Increasing (sub i o allocRel)) |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
124 |
guarantees |
61954 | 125 |
Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv)s) |
126 |
\<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)}" |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
127 |
|
36866 | 128 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
129 |
\<comment> \<open>spec (8)\<close> |
17310 | 130 |
alloc_progress :: "'a allocState_d program set" |
36866 | 131 |
where "alloc_progress = |
24147 | 132 |
(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int |
133 |
Increasing (sub i o allocRel)) |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
134 |
Int |
67613 | 135 |
Always {s. \<forall>i<Nclients. |
136 |
\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT} |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
137 |
Int |
24147 | 138 |
(INT i : lessThan Nclients. |
139 |
INT h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} |
|
140 |
LeadsTo |
|
141 |
{s. tokens h \<le> (tokens o sub i o allocRel)s}) |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
142 |
guarantees |
24147 | 143 |
(INT i : lessThan Nclients. |
144 |
INT h. {s. h \<le> (sub i o allocAsk) s} |
|
145 |
LeadsTo |
|
146 |
{s. h pfixLe (sub i o allocGiv) s})" |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
147 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
148 |
(*NOTE: to follow the original paper, the formula above should have had |
24147 | 149 |
INT h. {s. h i \<le> (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s} |
150 |
LeadsTo |
|
151 |
{s. tokens h i \<le> (tokens o sub i o allocRel)s}) |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
152 |
thus h should have been a function variable. However, only h i is ever |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
153 |
looked at.*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
154 |
|
36866 | 155 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
156 |
\<comment> \<open>spec: preserves part\<close> |
17310 | 157 |
alloc_preserves :: "'a allocState_d program set" |
36866 | 158 |
where "alloc_preserves = preserves allocRel Int preserves allocAsk Int |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
159 |
preserves allocState_d.dummy" |
24147 | 160 |
|
36866 | 161 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
162 |
\<comment> \<open>environmental constraints\<close> |
17310 | 163 |
alloc_allowed_acts :: "'a allocState_d program set" |
36866 | 164 |
where "alloc_allowed_acts = |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
165 |
{F. AllowedActs F = |
69313 | 166 |
insert Id (\<Union>(Acts ` (preserves allocGiv)))}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
167 |
|
36866 | 168 |
definition |
17310 | 169 |
alloc_spec :: "'a allocState_d program set" |
36866 | 170 |
where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
171 |
alloc_allowed_acts Int alloc_preserves" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
172 |
|
67445 | 173 |
|
174 |
subsubsection \<open>Network specification\<close> |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
175 |
|
36866 | 176 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
177 |
\<comment> \<open>spec (9.1)\<close> |
17310 | 178 |
network_ask :: "'a systemState program set" |
36866 | 179 |
where "network_ask = (INT i : lessThan Nclients. |
24147 | 180 |
Increasing (ask o sub i o client) guarantees |
36866 | 181 |
((sub i o allocAsk) Fols (ask o sub i o client)))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
182 |
|
36866 | 183 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
184 |
\<comment> \<open>spec (9.2)\<close> |
17310 | 185 |
network_giv :: "'a systemState program set" |
36866 | 186 |
where "network_giv = (INT i : lessThan Nclients. |
24147 | 187 |
Increasing (sub i o allocGiv) |
188 |
guarantees |
|
36866 | 189 |
((giv o sub i o client) Fols (sub i o allocGiv)))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
190 |
|
36866 | 191 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
192 |
\<comment> \<open>spec (9.3)\<close> |
17310 | 193 |
network_rel :: "'a systemState program set" |
36866 | 194 |
where "network_rel = (INT i : lessThan Nclients. |
24147 | 195 |
Increasing (rel o sub i o client) |
196 |
guarantees |
|
36866 | 197 |
((sub i o allocRel) Fols (rel o sub i o client)))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
198 |
|
36866 | 199 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
200 |
\<comment> \<open>spec: preserves part\<close> |
17310 | 201 |
network_preserves :: "'a systemState program set" |
36866 | 202 |
where "network_preserves = |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
203 |
preserves allocGiv Int |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
204 |
(INT i : lessThan Nclients. preserves (rel o sub i o client) Int |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
205 |
preserves (ask o sub i o client))" |
24147 | 206 |
|
36866 | 207 |
definition |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
64267
diff
changeset
|
208 |
\<comment> \<open>environmental constraints\<close> |
17310 | 209 |
network_allowed_acts :: "'a systemState program set" |
36866 | 210 |
where "network_allowed_acts = |
69325 | 211 |
{F. AllowedActs F = insert Id |
212 |
(\<Union> (Acts ` (preserves allocRel \<inter> (\<Inter>i<Nclients. |
|
213 |
preserves (giv \<circ> sub i \<circ> client)))))}" |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
214 |
|
36866 | 215 |
definition |
17310 | 216 |
network_spec :: "'a systemState program set" |
36866 | 217 |
where "network_spec = network_ask Int network_giv Int |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
218 |
network_rel Int network_allowed_acts Int |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
219 |
network_preserves" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
220 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
221 |
|
67445 | 222 |
subsubsection \<open>State mappings\<close> |
223 |
||
36866 | 224 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
225 |
sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState" |
36866 | 226 |
where "sysOfAlloc = (%s. let (cl,xtr) = allocState_d.dummy s |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
227 |
in (| allocGiv = allocGiv s, |
24147 | 228 |
allocAsk = allocAsk s, |
229 |
allocRel = allocRel s, |
|
230 |
client = cl, |
|
36866 | 231 |
dummy = xtr|))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
232 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
233 |
|
36866 | 234 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
235 |
sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState" |
36866 | 236 |
where "sysOfClient = (%(cl,al). (| allocGiv = allocGiv al, |
24147 | 237 |
allocAsk = allocAsk al, |
238 |
allocRel = allocRel al, |
|
239 |
client = cl, |
|
36866 | 240 |
systemState.dummy = allocState_d.dummy al|))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
241 |
|
36866 | 242 |
axiomatization Alloc :: "'a allocState_d program" |
67613 | 243 |
where Alloc: "Alloc \<in> alloc_spec" |
24147 | 244 |
|
36866 | 245 |
axiomatization Client :: "'a clientState_d program" |
67613 | 246 |
where Client: "Client \<in> client_spec" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
247 |
|
36866 | 248 |
axiomatization Network :: "'a systemState program" |
67613 | 249 |
where Network: "Network \<in> network_spec" |
36866 | 250 |
|
251 |
definition System :: "'a systemState program" |
|
60773 | 252 |
where "System = rename sysOfAlloc Alloc \<squnion> Network \<squnion> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
253 |
(rename sysOfClient |
24147 | 254 |
(plam x: lessThan Nclients. rename client_map Client))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
255 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
256 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
257 |
(** |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
258 |
locale System = |
24147 | 259 |
fixes |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
260 |
Alloc :: 'a allocState_d program |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
261 |
Client :: 'a clientState_d program |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
262 |
Network :: 'a systemState program |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
263 |
System :: 'a systemState program |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
264 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
265 |
assumes |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
266 |
Alloc "Alloc : alloc_spec" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
267 |
Client "Client : client_spec" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
268 |
Network "Network : network_spec" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
269 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
270 |
defines |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
271 |
System_def |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
272 |
"System == rename sysOfAlloc Alloc |
60773 | 273 |
\<squnion> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
274 |
Network |
60773 | 275 |
\<squnion> |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
276 |
(rename sysOfClient |
24147 | 277 |
(plam x: lessThan Nclients. rename client_map Client))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
278 |
**) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
279 |
|
21632 | 280 |
declare subset_preserves_o [THEN [2] rev_subsetD, intro] |
281 |
declare subset_preserves_o [THEN [2] rev_subsetD, simp] |
|
282 |
declare funPair_o_distrib [simp] |
|
283 |
declare Always_INT_distrib [simp] |
|
284 |
declare o_apply [simp del] |
|
285 |
||
286 |
(*For rewriting of specifications related by "guarantees"*) |
|
287 |
lemmas [simp] = |
|
288 |
rename_image_constrains |
|
289 |
rename_image_stable |
|
290 |
rename_image_increasing |
|
291 |
rename_image_invariant |
|
292 |
rename_image_Constrains |
|
293 |
rename_image_Stable |
|
294 |
rename_image_Increasing |
|
295 |
rename_image_Always |
|
296 |
rename_image_leadsTo |
|
297 |
rename_image_LeadsTo |
|
298 |
rename_preserves |
|
299 |
rename_image_preserves |
|
300 |
lift_image_preserves |
|
301 |
bij_image_INT |
|
302 |
bij_is_inj [THEN image_Int] |
|
303 |
bij_image_Collect_eq |
|
304 |
||
63146 | 305 |
ML \<open> |
21632 | 306 |
(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*) |
24147 | 307 |
fun list_of_Int th = |
21632 | 308 |
(list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2)) |
309 |
handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2)) |
|
24147 | 310 |
handle THM _ => (list_of_Int (th RS @{thm INT_D})) |
21632 | 311 |
handle THM _ => (list_of_Int (th RS bspec)) |
312 |
handle THM _ => [th]; |
|
63146 | 313 |
\<close> |
21632 | 314 |
|
315 |
lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec] |
|
316 |
||
63146 | 317 |
attribute_setup normalized = \<open> |
24147 | 318 |
let |
319 |
fun normalized th = |
|
320 |
normalized (th RS spec |
|
321 |
handle THM _ => th RS @{thm lessThanBspec} |
|
322 |
handle THM _ => th RS bspec |
|
323 |
handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1)) |
|
324 |
handle THM _ => th; |
|
21632 | 325 |
in |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
60773
diff
changeset
|
326 |
Scan.succeed (Thm.rule_attribute [] (K normalized)) |
21632 | 327 |
end |
63146 | 328 |
\<close> |
21632 | 329 |
|
330 |
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***) |
|
63146 | 331 |
ML \<open> |
42767 | 332 |
fun record_auto_tac ctxt = |
42793 | 333 |
let val ctxt' = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
334 |
ctxt addSWrapper Record.split_wrapper |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
335 |
addsimps |
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
336 |
[@{thm sysOfAlloc_def}, @{thm sysOfClient_def}, |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
337 |
@{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def}, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
338 |
@{thm o_apply}, @{thm Let_def}] |
42793 | 339 |
in auto_tac ctxt' end; |
340 |
||
63146 | 341 |
\<close> |
21632 | 342 |
|
63146 | 343 |
method_setup record_auto = \<open>Scan.succeed (SIMPLE_METHOD o record_auto_tac)\<close> |
21632 | 344 |
|
345 |
lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc" |
|
346 |
apply (unfold sysOfAlloc_def Let_def) |
|
347 |
apply (rule inj_onI) |
|
24147 | 348 |
apply record_auto |
21632 | 349 |
done |
350 |
||
63146 | 351 |
text\<open>We need the inverse; also having it simplifies the proof of surjectivity\<close> |
24147 | 352 |
lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s = |
353 |
(| allocGiv = allocGiv s, |
|
354 |
allocAsk = allocAsk s, |
|
355 |
allocRel = allocRel s, |
|
21632 | 356 |
allocState_d.dummy = (client s, dummy s) |)" |
357 |
apply (rule inj_sysOfAlloc [THEN inv_f_eq]) |
|
24147 | 358 |
apply record_auto |
21632 | 359 |
done |
360 |
||
361 |
lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc" |
|
40702 | 362 |
apply (simp add: surj_iff_all) |
24147 | 363 |
apply record_auto |
21632 | 364 |
done |
365 |
||
366 |
lemma bij_sysOfAlloc [iff]: "bij sysOfAlloc" |
|
367 |
apply (blast intro: bijI) |
|
368 |
done |
|
369 |
||
370 |
||
69597 | 371 |
subsubsection\<open>bijectivity of \<^term>\<open>sysOfClient\<close>\<close> |
21632 | 372 |
|
373 |
lemma inj_sysOfClient [iff]: "inj sysOfClient" |
|
374 |
apply (unfold sysOfClient_def) |
|
375 |
apply (rule inj_onI) |
|
24147 | 376 |
apply record_auto |
21632 | 377 |
done |
378 |
||
24147 | 379 |
lemma inv_sysOfClient_eq [simp]: "!!s. inv sysOfClient s = |
380 |
(client s, |
|
381 |
(| allocGiv = allocGiv s, |
|
382 |
allocAsk = allocAsk s, |
|
383 |
allocRel = allocRel s, |
|
21632 | 384 |
allocState_d.dummy = systemState.dummy s|) )" |
385 |
apply (rule inj_sysOfClient [THEN inv_f_eq]) |
|
24147 | 386 |
apply record_auto |
21632 | 387 |
done |
388 |
||
389 |
lemma surj_sysOfClient [iff]: "surj sysOfClient" |
|
40702 | 390 |
apply (simp add: surj_iff_all) |
24147 | 391 |
apply record_auto |
21632 | 392 |
done |
393 |
||
394 |
lemma bij_sysOfClient [iff]: "bij sysOfClient" |
|
395 |
apply (blast intro: bijI) |
|
396 |
done |
|
397 |
||
398 |
||
69597 | 399 |
subsubsection\<open>bijectivity of \<^term>\<open>client_map\<close>\<close> |
21632 | 400 |
|
401 |
lemma inj_client_map [iff]: "inj client_map" |
|
402 |
apply (unfold inj_on_def) |
|
24147 | 403 |
apply record_auto |
21632 | 404 |
done |
405 |
||
24147 | 406 |
lemma inv_client_map_eq [simp]: "!!s. inv client_map s = |
407 |
(%(x,y).(|giv = giv x, ask = ask x, rel = rel x, |
|
21632 | 408 |
clientState_d.dummy = y|)) s" |
409 |
apply (rule inj_client_map [THEN inv_f_eq]) |
|
24147 | 410 |
apply record_auto |
21632 | 411 |
done |
412 |
||
413 |
lemma surj_client_map [iff]: "surj client_map" |
|
40702 | 414 |
apply (simp add: surj_iff_all) |
24147 | 415 |
apply record_auto |
21632 | 416 |
done |
417 |
||
418 |
lemma bij_client_map [iff]: "bij client_map" |
|
419 |
apply (blast intro: bijI) |
|
420 |
done |
|
421 |
||
422 |
||
69597 | 423 |
text\<open>o-simprules for \<^term>\<open>client_map\<close>\<close> |
21632 | 424 |
|
425 |
lemma fst_o_client_map: "fst o client_map = non_dummy" |
|
426 |
apply (unfold client_map_def) |
|
427 |
apply (rule fst_o_funPair) |
|
428 |
done |
|
429 |
||
69597 | 430 |
ML \<open>ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs \<^context> @{thm fst_o_client_map})\<close> |
21632 | 431 |
declare fst_o_client_map' [simp] |
432 |
||
433 |
lemma snd_o_client_map: "snd o client_map = clientState_d.dummy" |
|
434 |
apply (unfold client_map_def) |
|
435 |
apply (rule snd_o_funPair) |
|
436 |
done |
|
437 |
||
69597 | 438 |
ML \<open>ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs \<^context> @{thm snd_o_client_map})\<close> |
21632 | 439 |
declare snd_o_client_map' [simp] |
440 |
||
21710 | 441 |
|
69597 | 442 |
subsection\<open>o-simprules for \<^term>\<open>sysOfAlloc\<close> [MUST BE AUTOMATED]\<close> |
21632 | 443 |
|
444 |
lemma client_o_sysOfAlloc: "client o sysOfAlloc = fst o allocState_d.dummy " |
|
24147 | 445 |
apply record_auto |
21632 | 446 |
done |
447 |
||
69597 | 448 |
ML \<open>ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs \<^context> @{thm client_o_sysOfAlloc})\<close> |
21632 | 449 |
declare client_o_sysOfAlloc' [simp] |
450 |
||
451 |
lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv" |
|
24147 | 452 |
apply record_auto |
21632 | 453 |
done |
454 |
||
69597 | 455 |
ML \<open>ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs \<^context> @{thm allocGiv_o_sysOfAlloc_eq})\<close> |
21632 | 456 |
declare allocGiv_o_sysOfAlloc_eq' [simp] |
457 |
||
458 |
lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk" |
|
24147 | 459 |
apply record_auto |
21632 | 460 |
done |
461 |
||
69597 | 462 |
ML \<open>ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs \<^context> @{thm allocAsk_o_sysOfAlloc_eq})\<close> |
21632 | 463 |
declare allocAsk_o_sysOfAlloc_eq' [simp] |
464 |
||
465 |
lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel" |
|
24147 | 466 |
apply record_auto |
21632 | 467 |
done |
468 |
||
69597 | 469 |
ML \<open>ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs \<^context> @{thm allocRel_o_sysOfAlloc_eq})\<close> |
21632 | 470 |
declare allocRel_o_sysOfAlloc_eq' [simp] |
471 |
||
21710 | 472 |
|
69597 | 473 |
subsection\<open>o-simprules for \<^term>\<open>sysOfClient\<close> [MUST BE AUTOMATED]\<close> |
21632 | 474 |
|
475 |
lemma client_o_sysOfClient: "client o sysOfClient = fst" |
|
24147 | 476 |
apply record_auto |
21632 | 477 |
done |
478 |
||
69597 | 479 |
ML \<open>ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs \<^context> @{thm client_o_sysOfClient})\<close> |
21632 | 480 |
declare client_o_sysOfClient' [simp] |
481 |
||
482 |
lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd " |
|
24147 | 483 |
apply record_auto |
21632 | 484 |
done |
485 |
||
69597 | 486 |
ML \<open>ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs \<^context> @{thm allocGiv_o_sysOfClient_eq})\<close> |
21632 | 487 |
declare allocGiv_o_sysOfClient_eq' [simp] |
488 |
||
489 |
lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd " |
|
24147 | 490 |
apply record_auto |
21632 | 491 |
done |
492 |
||
69597 | 493 |
ML \<open>ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs \<^context> @{thm allocAsk_o_sysOfClient_eq})\<close> |
21632 | 494 |
declare allocAsk_o_sysOfClient_eq' [simp] |
495 |
||
496 |
lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd " |
|
24147 | 497 |
apply record_auto |
21632 | 498 |
done |
499 |
||
69597 | 500 |
ML \<open>ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs \<^context> @{thm allocRel_o_sysOfClient_eq})\<close> |
21632 | 501 |
declare allocRel_o_sysOfClient_eq' [simp] |
502 |
||
503 |
lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv" |
|
504 |
apply (simp add: o_def) |
|
505 |
done |
|
506 |
||
69597 | 507 |
ML \<open>ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs \<^context> @{thm allocGiv_o_inv_sysOfAlloc_eq})\<close> |
21632 | 508 |
declare allocGiv_o_inv_sysOfAlloc_eq' [simp] |
509 |
||
510 |
lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk" |
|
511 |
apply (simp add: o_def) |
|
512 |
done |
|
513 |
||
69597 | 514 |
ML \<open>ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs \<^context> @{thm allocAsk_o_inv_sysOfAlloc_eq})\<close> |
21632 | 515 |
declare allocAsk_o_inv_sysOfAlloc_eq' [simp] |
516 |
||
517 |
lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel" |
|
518 |
apply (simp add: o_def) |
|
519 |
done |
|
520 |
||
69597 | 521 |
ML \<open>ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs \<^context> @{thm allocRel_o_inv_sysOfAlloc_eq})\<close> |
21632 | 522 |
declare allocRel_o_inv_sysOfAlloc_eq' [simp] |
523 |
||
24147 | 524 |
lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) = |
21632 | 525 |
rel o sub i o client" |
526 |
apply (simp add: o_def drop_map_def) |
|
527 |
done |
|
528 |
||
69597 | 529 |
ML \<open>ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs \<^context> @{thm rel_inv_client_map_drop_map})\<close> |
21632 | 530 |
declare rel_inv_client_map_drop_map [simp] |
531 |
||
24147 | 532 |
lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) = |
21632 | 533 |
ask o sub i o client" |
534 |
apply (simp add: o_def drop_map_def) |
|
535 |
done |
|
536 |
||
69597 | 537 |
ML \<open>ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs \<^context> @{thm ask_inv_client_map_drop_map})\<close> |
21632 | 538 |
declare ask_inv_client_map_drop_map [simp] |
539 |
||
540 |
||
63146 | 541 |
text\<open>Client : <unfolded specification>\<close> |
21632 | 542 |
lemmas client_spec_simps = |
543 |
client_spec_def client_increasing_def client_bounded_def |
|
544 |
client_progress_def client_allowed_acts_def client_preserves_def |
|
545 |
guarantees_Int_right |
|
546 |
||
63146 | 547 |
ML \<open> |
21632 | 548 |
val [Client_Increasing_ask, Client_Increasing_rel, |
24147 | 549 |
Client_Bounded, Client_Progress, Client_AllowedActs, |
21632 | 550 |
Client_preserves_giv, Client_preserves_dummy] = |
69597 | 551 |
@{thm Client} |> simplify (\<^context> addsimps @{thms client_spec_simps}) |
21632 | 552 |
|> list_of_Int; |
553 |
||
56199 | 554 |
ML_Thms.bind_thm ("Client_Increasing_ask", Client_Increasing_ask); |
555 |
ML_Thms.bind_thm ("Client_Increasing_rel", Client_Increasing_rel); |
|
556 |
ML_Thms.bind_thm ("Client_Bounded", Client_Bounded); |
|
557 |
ML_Thms.bind_thm ("Client_Progress", Client_Progress); |
|
558 |
ML_Thms.bind_thm ("Client_AllowedActs", Client_AllowedActs); |
|
559 |
ML_Thms.bind_thm ("Client_preserves_giv", Client_preserves_giv); |
|
560 |
ML_Thms.bind_thm ("Client_preserves_dummy", Client_preserves_dummy); |
|
63146 | 561 |
\<close> |
21632 | 562 |
|
563 |
declare |
|
564 |
Client_Increasing_ask [iff] |
|
565 |
Client_Increasing_rel [iff] |
|
566 |
Client_Bounded [iff] |
|
567 |
Client_preserves_giv [iff] |
|
568 |
Client_preserves_dummy [iff] |
|
569 |
||
570 |
||
63146 | 571 |
text\<open>Network : <unfolded specification>\<close> |
21632 | 572 |
lemmas network_spec_simps = |
573 |
network_spec_def network_ask_def network_giv_def |
|
574 |
network_rel_def network_allowed_acts_def network_preserves_def |
|
575 |
ball_conj_distrib |
|
576 |
||
63146 | 577 |
ML \<open> |
21632 | 578 |
val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs, |
24147 | 579 |
Network_preserves_allocGiv, Network_preserves_rel, |
580 |
Network_preserves_ask] = |
|
69597 | 581 |
@{thm Network} |> simplify (\<^context> addsimps @{thms network_spec_simps}) |
21632 | 582 |
|> list_of_Int; |
583 |
||
56199 | 584 |
ML_Thms.bind_thm ("Network_Ask", Network_Ask); |
585 |
ML_Thms.bind_thm ("Network_Giv", Network_Giv); |
|
586 |
ML_Thms.bind_thm ("Network_Rel", Network_Rel); |
|
587 |
ML_Thms.bind_thm ("Network_AllowedActs", Network_AllowedActs); |
|
588 |
ML_Thms.bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv); |
|
589 |
ML_Thms.bind_thm ("Network_preserves_rel", Network_preserves_rel); |
|
590 |
ML_Thms.bind_thm ("Network_preserves_ask", Network_preserves_ask); |
|
63146 | 591 |
\<close> |
21632 | 592 |
|
593 |
declare Network_preserves_allocGiv [iff] |
|
594 |
||
595 |
declare |
|
596 |
Network_preserves_rel [simp] |
|
597 |
Network_preserves_ask [simp] |
|
598 |
||
599 |
declare |
|
600 |
Network_preserves_rel [simplified o_def, simp] |
|
601 |
Network_preserves_ask [simplified o_def, simp] |
|
602 |
||
63146 | 603 |
text\<open>Alloc : <unfolded specification>\<close> |
21632 | 604 |
lemmas alloc_spec_simps = |
605 |
alloc_spec_def alloc_increasing_def alloc_safety_def |
|
606 |
alloc_progress_def alloc_allowed_acts_def alloc_preserves_def |
|
607 |
||
63146 | 608 |
ML \<open> |
21632 | 609 |
val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs, |
24147 | 610 |
Alloc_preserves_allocRel, Alloc_preserves_allocAsk, |
611 |
Alloc_preserves_dummy] = |
|
69597 | 612 |
@{thm Alloc} |> simplify (\<^context> addsimps @{thms alloc_spec_simps}) |
21632 | 613 |
|> list_of_Int; |
614 |
||
56199 | 615 |
ML_Thms.bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0); |
616 |
ML_Thms.bind_thm ("Alloc_Safety", Alloc_Safety); |
|
617 |
ML_Thms.bind_thm ("Alloc_Progress", Alloc_Progress); |
|
618 |
ML_Thms.bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs); |
|
619 |
ML_Thms.bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel); |
|
620 |
ML_Thms.bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk); |
|
621 |
ML_Thms.bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy); |
|
63146 | 622 |
\<close> |
21632 | 623 |
|
63146 | 624 |
text\<open>Strip off the INT in the guarantees postcondition\<close> |
24147 | 625 |
|
626 |
lemmas Alloc_Increasing = Alloc_Increasing_0 [normalized] |
|
21632 | 627 |
|
628 |
declare |
|
629 |
Alloc_preserves_allocRel [iff] |
|
630 |
Alloc_preserves_allocAsk [iff] |
|
631 |
Alloc_preserves_dummy [iff] |
|
632 |
||
633 |
||
63146 | 634 |
subsection\<open>Components Lemmas [MUST BE AUTOMATED]\<close> |
21632 | 635 |
|
60773 | 636 |
lemma Network_component_System: "Network \<squnion> |
24147 | 637 |
((rename sysOfClient |
60773 | 638 |
(plam x: (lessThan Nclients). rename client_map Client)) \<squnion> |
24147 | 639 |
rename sysOfAlloc Alloc) |
21632 | 640 |
= System" |
21710 | 641 |
by (simp add: System_def Join_ac) |
21632 | 642 |
|
24147 | 643 |
lemma Client_component_System: "(rename sysOfClient |
60773 | 644 |
(plam x: (lessThan Nclients). rename client_map Client)) \<squnion> |
645 |
(Network \<squnion> rename sysOfAlloc Alloc) = System" |
|
21710 | 646 |
by (simp add: System_def Join_ac) |
21632 | 647 |
|
60773 | 648 |
lemma Alloc_component_System: "rename sysOfAlloc Alloc \<squnion> |
649 |
((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) \<squnion> |
|
21632 | 650 |
Network) = System" |
21710 | 651 |
by (simp add: System_def Join_ac) |
21632 | 652 |
|
653 |
declare |
|
654 |
Client_component_System [iff] |
|
655 |
Network_component_System [iff] |
|
656 |
Alloc_component_System [iff] |
|
657 |
||
21710 | 658 |
|
63146 | 659 |
text\<open>* These preservation laws should be generated automatically *\<close> |
21632 | 660 |
|
661 |
lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask" |
|
21710 | 662 |
by (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff) |
21632 | 663 |
|
24147 | 664 |
lemma Network_Allowed [simp]: "Allowed Network = |
665 |
preserves allocRel Int |
|
21632 | 666 |
(INT i: lessThan Nclients. preserves(giv o sub i o client))" |
21710 | 667 |
by (auto simp add: Allowed_def Network_AllowedActs safety_prop_Acts_iff) |
21632 | 668 |
|
669 |
lemma Alloc_Allowed [simp]: "Allowed Alloc = preserves allocGiv" |
|
21710 | 670 |
by (auto simp add: Allowed_def Alloc_AllowedActs safety_prop_Acts_iff) |
21632 | 671 |
|
63146 | 672 |
text\<open>needed in \<open>rename_client_map_tac\<close>\<close> |
21632 | 673 |
lemma OK_lift_rename_Client [simp]: "OK I (%i. lift i (rename client_map Client))" |
674 |
apply (rule OK_lift_I) |
|
675 |
apply auto |
|
676 |
apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD]) |
|
677 |
apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD]) |
|
678 |
apply (auto simp add: o_def split_def) |
|
679 |
done |
|
680 |
||
21710 | 681 |
lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x" |
682 |
apply (insert fst_o_lift_map [of i]) |
|
24147 | 683 |
apply (drule fun_cong [where x=x]) |
40702 | 684 |
apply (simp add: o_def) |
21710 | 685 |
done |
686 |
||
687 |
lemma fst_o_lift_map' [simp]: |
|
688 |
"(f \<circ> sub i \<circ> fst \<circ> lift_map i \<circ> g) = f o fst o g" |
|
24147 | 689 |
apply (subst fst_o_lift_map [symmetric]) |
690 |
apply (simp only: o_assoc) |
|
21710 | 691 |
done |
692 |
||
21632 | 693 |
|
694 |
(*The proofs of rename_Client_Increasing, rename_Client_Bounded and |
|
695 |
rename_Client_Progress are similar. All require copying out the original |
|
696 |
Client property. A forward proof can be constructed as follows: |
|
697 |
||
698 |
Client_Increasing_ask RS |
|
699 |
(bij_client_map RS rename_rename_guarantees_eq RS iffD2) |
|
700 |
RS (lift_lift_guarantees_eq RS iffD2) |
|
701 |
RS guarantees_PLam_I |
|
702 |
RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2) |
|
24147 | 703 |
|> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def, |
40702 | 704 |
surj_rename]) |
21632 | 705 |
|
706 |
However, the "preserves" property remains to be discharged, and the unfolding |
|
707 |
of "o" and "sub" complicates subsequent reasoning. |
|
708 |
||
709 |
The following tactic works for all three proofs, though it certainly looks |
|
710 |
ad-hoc! |
|
711 |
*) |
|
712 |
ML |
|
63146 | 713 |
\<open> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
714 |
fun rename_client_map_tac ctxt = |
21632 | 715 |
EVERY [ |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
716 |
simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1, |
60754 | 717 |
resolve_tac ctxt @{thms guarantees_PLam_I} 1, |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
56199
diff
changeset
|
718 |
assume_tac ctxt 2, |
24147 | 719 |
(*preserves: routine reasoning*) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
720 |
asm_simp_tac (ctxt addsimps [@{thm lift_preserves_sub}]) 2, |
24147 | 721 |
(*the guarantee for "lift i (rename client_map Client)" *) |
21632 | 722 |
asm_simp_tac |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
723 |
(ctxt addsimps [@{thm lift_guarantees_eq_lift_inv}, |
24147 | 724 |
@{thm rename_guarantees_eq_rename_inv}, |
40702 | 725 |
@{thm bij_imp_bij_inv}, @{thm surj_rename}, |
24147 | 726 |
@{thm inv_inv_eq}]) 1, |
52089 | 727 |
asm_simp_tac |
728 |
(ctxt addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1] |
|
63146 | 729 |
\<close> |
21632 | 730 |
|
63146 | 731 |
method_setup rename_client_map = \<open> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
732 |
Scan.succeed (fn ctxt => SIMPLE_METHOD (rename_client_map_tac ctxt)) |
63146 | 733 |
\<close> |
24147 | 734 |
|
69597 | 735 |
text\<open>Lifting \<open>Client_Increasing\<close> to \<^term>\<open>systemState\<close>\<close> |
67613 | 736 |
lemma rename_Client_Increasing: "i \<in> I |
737 |
==> rename sysOfClient (plam x: I. rename client_map Client) \<in> |
|
24147 | 738 |
UNIV guarantees |
739 |
Increasing (ask o sub i o client) Int |
|
21632 | 740 |
Increasing (rel o sub i o client)" |
24147 | 741 |
by rename_client_map |
21632 | 742 |
|
67613 | 743 |
lemma preserves_sub_fst_lift_map: "[| F \<in> preserves w; i \<noteq> j |] |
744 |
==> F \<in> preserves (sub i o fst o lift_map j o funPair v w)" |
|
21632 | 745 |
apply (auto simp add: lift_map_def split_def linorder_neq_iff o_def) |
746 |
apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD]) |
|
747 |
apply (auto simp add: o_def) |
|
748 |
done |
|
749 |
||
24147 | 750 |
lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |] |
67613 | 751 |
==> Client \<in> preserves (giv o sub i o fst o lift_map j o client_map)" |
46911 | 752 |
apply (cases "i=j") |
21710 | 753 |
apply (simp, simp add: o_def non_dummy_def) |
21632 | 754 |
apply (drule Client_preserves_dummy [THEN preserves_sub_fst_lift_map]) |
755 |
apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD]) |
|
756 |
apply (simp add: o_def client_map_def) |
|
757 |
done |
|
758 |
||
759 |
lemma rename_sysOfClient_ok_Network: |
|
24147 | 760 |
"rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) |
21632 | 761 |
ok Network" |
21710 | 762 |
by (auto simp add: ok_iff_Allowed client_preserves_giv_oo_client_map) |
21632 | 763 |
|
764 |
lemma rename_sysOfClient_ok_Alloc: |
|
24147 | 765 |
"rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) |
21632 | 766 |
ok rename sysOfAlloc Alloc" |
21710 | 767 |
by (simp add: ok_iff_Allowed) |
21632 | 768 |
|
769 |
lemma rename_sysOfAlloc_ok_Network: "rename sysOfAlloc Alloc ok Network" |
|
21710 | 770 |
by (simp add: ok_iff_Allowed) |
21632 | 771 |
|
772 |
declare |
|
773 |
rename_sysOfClient_ok_Network [iff] |
|
774 |
rename_sysOfClient_ok_Alloc [iff] |
|
775 |
rename_sysOfAlloc_ok_Network [iff] |
|
776 |
||
63146 | 777 |
text\<open>The "ok" laws, re-oriented. |
778 |
But not sure this works: theorem \<open>ok_commute\<close> is needed below\<close> |
|
21632 | 779 |
declare |
780 |
rename_sysOfClient_ok_Network [THEN ok_sym, iff] |
|
781 |
rename_sysOfClient_ok_Alloc [THEN ok_sym, iff] |
|
782 |
rename_sysOfAlloc_ok_Network [THEN ok_sym] |
|
783 |
||
784 |
lemma System_Increasing: "i < Nclients |
|
67613 | 785 |
==> System \<in> Increasing (ask o sub i o client) Int |
21632 | 786 |
Increasing (rel o sub i o client)" |
787 |
apply (rule component_guaranteesD [OF rename_Client_Increasing Client_component_System]) |
|
788 |
apply auto |
|
789 |
done |
|
790 |
||
791 |
lemmas rename_guarantees_sysOfAlloc_I = |
|
45605 | 792 |
bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2] |
21632 | 793 |
|
794 |
||
795 |
(*Lifting Alloc_Increasing up to the level of systemState*) |
|
21710 | 796 |
lemmas rename_Alloc_Increasing = |
797 |
Alloc_Increasing |
|
24147 | 798 |
[THEN rename_guarantees_sysOfAlloc_I, |
40702 | 799 |
simplified surj_rename o_def sub_apply |
24147 | 800 |
rename_image_Increasing bij_sysOfAlloc |
40702 | 801 |
allocGiv_o_inv_sysOfAlloc_eq'] |
21632 | 802 |
|
24147 | 803 |
lemma System_Increasing_allocGiv: |
67613 | 804 |
"i < Nclients \<Longrightarrow> System \<in> Increasing (sub i o allocGiv)" |
21632 | 805 |
apply (unfold System_def) |
806 |
apply (simp add: o_def) |
|
807 |
apply (rule rename_Alloc_Increasing [THEN guarantees_Join_I1, THEN guaranteesD]) |
|
808 |
apply auto |
|
809 |
done |
|
21710 | 810 |
|
21632 | 811 |
|
63146 | 812 |
ML \<open> |
56199 | 813 |
ML_Thms.bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing}) |
63146 | 814 |
\<close> |
21632 | 815 |
|
816 |
declare System_Increasing' [intro!] |
|
817 |
||
63146 | 818 |
text\<open>Follows consequences. |
21632 | 819 |
The "Always (INT ...) formulation expresses the general safety property |
63146 | 820 |
and allows it to be combined using \<open>Always_Int_rule\<close> below.\<close> |
21632 | 821 |
|
24147 | 822 |
lemma System_Follows_rel: |
67613 | 823 |
"i < Nclients ==> System \<in> ((sub i o allocRel) Fols (rel o sub i o client))" |
21632 | 824 |
apply (auto intro!: Network_Rel [THEN component_guaranteesD]) |
24147 | 825 |
apply (simp add: ok_commute [of Network]) |
21710 | 826 |
done |
21632 | 827 |
|
24147 | 828 |
lemma System_Follows_ask: |
67613 | 829 |
"i < Nclients ==> System \<in> ((sub i o allocAsk) Fols (ask o sub i o client))" |
21710 | 830 |
apply (auto intro!: Network_Ask [THEN component_guaranteesD]) |
24147 | 831 |
apply (simp add: ok_commute [of Network]) |
21632 | 832 |
done |
833 |
||
24147 | 834 |
lemma System_Follows_allocGiv: |
67613 | 835 |
"i < Nclients ==> System \<in> (giv o sub i o client) Fols (sub i o allocGiv)" |
21632 | 836 |
apply (auto intro!: Network_Giv [THEN component_guaranteesD] |
837 |
rename_Alloc_Increasing [THEN component_guaranteesD]) |
|
21710 | 838 |
apply (simp_all add: o_def non_dummy_def ok_commute [of Network]) |
21632 | 839 |
apply (auto intro!: rename_Alloc_Increasing [THEN component_guaranteesD]) |
840 |
done |
|
21710 | 841 |
|
21632 | 842 |
|
67613 | 843 |
lemma Always_giv_le_allocGiv: "System \<in> Always (INT i: lessThan Nclients. |
21710 | 844 |
{s. (giv o sub i o client) s \<le> (sub i o allocGiv) s})" |
21632 | 845 |
apply auto |
846 |
apply (erule System_Follows_allocGiv [THEN Follows_Bounded]) |
|
847 |
done |
|
21710 | 848 |
|
21632 | 849 |
|
67613 | 850 |
lemma Always_allocAsk_le_ask: "System \<in> Always (INT i: lessThan Nclients. |
21710 | 851 |
{s. (sub i o allocAsk) s \<le> (ask o sub i o client) s})" |
21632 | 852 |
apply auto |
853 |
apply (erule System_Follows_ask [THEN Follows_Bounded]) |
|
854 |
done |
|
21710 | 855 |
|
21632 | 856 |
|
67613 | 857 |
lemma Always_allocRel_le_rel: "System \<in> Always (INT i: lessThan Nclients. |
21710 | 858 |
{s. (sub i o allocRel) s \<le> (rel o sub i o client) s})" |
859 |
by (auto intro!: Follows_Bounded System_Follows_rel) |
|
860 |
||
21632 | 861 |
|
63146 | 862 |
subsection\<open>Proof of the safety property (1)\<close> |
21632 | 863 |
|
63146 | 864 |
text\<open>safety (1), step 1 is \<open>System_Follows_rel\<close>\<close> |
21632 | 865 |
|
63146 | 866 |
text\<open>safety (1), step 2\<close> |
21632 | 867 |
(* i < Nclients ==> System : Increasing (sub i o allocRel) *) |
45605 | 868 |
lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1] |
21632 | 869 |
|
870 |
(*Lifting Alloc_safety up to the level of systemState. |
|
21710 | 871 |
Simplifying with o_def gets rid of the translations but it unfortunately |
21632 | 872 |
gets rid of the other "o"s too.*) |
873 |
||
63146 | 874 |
text\<open>safety (1), step 3\<close> |
24147 | 875 |
lemma System_sum_bounded: |
67613 | 876 |
"System \<in> Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv) s) |
21710 | 877 |
\<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}" |
21632 | 878 |
apply (simp add: o_apply) |
24147 | 879 |
apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I]) |
40702 | 880 |
apply (simp add: o_def) |
24147 | 881 |
apply (erule component_guaranteesD) |
21710 | 882 |
apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def]) |
21632 | 883 |
done |
884 |
||
63146 | 885 |
text\<open>Follows reasoning\<close> |
21632 | 886 |
|
67613 | 887 |
lemma Always_tokens_giv_le_allocGiv: "System \<in> Always (INT i: lessThan Nclients. |
24147 | 888 |
{s. (tokens o giv o sub i o client) s |
21710 | 889 |
\<le> (tokens o sub i o allocGiv) s})" |
21632 | 890 |
apply (rule Always_giv_le_allocGiv [THEN Always_weaken]) |
891 |
apply (auto intro: tokens_mono_prefix simp add: o_apply) |
|
892 |
done |
|
893 |
||
67613 | 894 |
lemma Always_tokens_allocRel_le_rel: "System \<in> Always (INT i: lessThan Nclients. |
24147 | 895 |
{s. (tokens o sub i o allocRel) s |
21710 | 896 |
\<le> (tokens o rel o sub i o client) s})" |
21632 | 897 |
apply (rule Always_allocRel_le_rel [THEN Always_weaken]) |
898 |
apply (auto intro: tokens_mono_prefix simp add: o_apply) |
|
899 |
done |
|
900 |
||
63146 | 901 |
text\<open>safety (1), step 4 (final result!)\<close> |
67613 | 902 |
theorem System_safety: "System \<in> system_safety" |
21632 | 903 |
apply (unfold system_safety_def) |
69597 | 904 |
apply (tactic \<open>resolve_tac \<^context> [Always_Int_rule [@{thm System_sum_bounded}, |
39159 | 905 |
@{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS |
63146 | 906 |
@{thm Always_weaken}] 1\<close>) |
21632 | 907 |
apply auto |
64267 | 908 |
apply (rule sum_fun_mono [THEN order_trans]) |
21632 | 909 |
apply (drule_tac [2] order_trans) |
64267 | 910 |
apply (rule_tac [2] add_le_mono [OF order_refl sum_fun_mono]) |
21632 | 911 |
prefer 3 apply assumption |
912 |
apply auto |
|
913 |
done |
|
914 |
||
63146 | 915 |
subsection \<open>Proof of the progress property (2)\<close> |
21632 | 916 |
|
63146 | 917 |
text\<open>progress (2), step 1 is \<open>System_Follows_ask\<close> and |
918 |
\<open>System_Follows_rel\<close>\<close> |
|
21632 | 919 |
|
63146 | 920 |
text\<open>progress (2), step 2; see also \<open>System_Increasing_allocRel\<close>\<close> |
21632 | 921 |
(* i < Nclients ==> System : Increasing (sub i o allocAsk) *) |
45605 | 922 |
lemmas System_Increasing_allocAsk = System_Follows_ask [THEN Follows_Increasing1] |
21632 | 923 |
|
63146 | 924 |
text\<open>progress (2), step 3: lifting \<open>Client_Bounded\<close> to systemState\<close> |
67613 | 925 |
lemma rename_Client_Bounded: "i \<in> I |
926 |
==> rename sysOfClient (plam x: I. rename client_map Client) \<in> |
|
24147 | 927 |
UNIV guarantees |
67613 | 928 |
Always {s. \<forall>elt \<in> set ((ask o sub i o client) s). elt \<le> NbT}" |
69768 | 929 |
using image_cong_simp [cong del] by rename_client_map |
21632 | 930 |
|
24147 | 931 |
lemma System_Bounded_ask: "i < Nclients |
67613 | 932 |
==> System \<in> Always |
933 |
{s. \<forall>elt \<in> set ((ask o sub i o client) s). elt \<le> NbT}" |
|
21632 | 934 |
apply (rule component_guaranteesD [OF rename_Client_Bounded Client_component_System]) |
935 |
apply auto |
|
936 |
done |
|
937 |
||
67613 | 938 |
lemma Collect_all_imp_eq: "{x. \<forall>y. P y \<longrightarrow> Q x y} = (INT y: {y. P y}. {x. Q x y})" |
21632 | 939 |
apply blast |
940 |
done |
|
941 |
||
63146 | 942 |
text\<open>progress (2), step 4\<close> |
67717 | 943 |
lemma System_Bounded_allocAsk: "System \<in> Always {s. \<forall>i<Nclients. |
67613 | 944 |
\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT}" |
21632 | 945 |
apply (auto simp add: Collect_all_imp_eq) |
69597 | 946 |
apply (tactic \<open>resolve_tac \<^context> [Always_Int_rule [@{thm Always_allocAsk_le_ask}, |
63146 | 947 |
@{thm System_Bounded_ask}] RS @{thm Always_weaken}] 1\<close>) |
21632 | 948 |
apply (auto dest: set_mono) |
949 |
done |
|
950 |
||
63146 | 951 |
text\<open>progress (2), step 5 is \<open>System_Increasing_allocGiv\<close>\<close> |
21632 | 952 |
|
63146 | 953 |
text\<open>progress (2), step 6\<close> |
21632 | 954 |
(* i < Nclients ==> System : Increasing (giv o sub i o client) *) |
45605 | 955 |
lemmas System_Increasing_giv = System_Follows_allocGiv [THEN Follows_Increasing1] |
21632 | 956 |
|
957 |
||
67613 | 958 |
lemma rename_Client_Progress: "i \<in> I |
24147 | 959 |
==> rename sysOfClient (plam x: I. rename client_map Client) |
67613 | 960 |
\<in> Increasing (giv o sub i o client) |
24147 | 961 |
guarantees |
962 |
(INT h. {s. h \<le> (giv o sub i o client) s & |
|
963 |
h pfixGe (ask o sub i o client) s} |
|
21710 | 964 |
LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})" |
69813
9d94a6c95113
more idiomatic style for local declarations in apply scripts
haftmann
parents:
69768
diff
changeset
|
965 |
supply image_cong_simp [cong del] |
24147 | 966 |
apply rename_client_map |
21632 | 967 |
apply (simp add: Client_Progress [simplified o_def]) |
968 |
done |
|
969 |
||
970 |
||
63146 | 971 |
text\<open>progress (2), step 7\<close> |
24147 | 972 |
lemma System_Client_Progress: |
67613 | 973 |
"System \<in> (INT i : (lessThan Nclients). |
24147 | 974 |
INT h. {s. h \<le> (giv o sub i o client) s & |
975 |
h pfixGe (ask o sub i o client) s} |
|
21710 | 976 |
LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})" |
21632 | 977 |
apply (rule INT_I) |
978 |
(*Couldn't have just used Auto_tac since the "INT h" must be kept*) |
|
979 |
apply (rule component_guaranteesD [OF rename_Client_Progress Client_component_System]) |
|
980 |
apply (auto simp add: System_Increasing_giv) |
|
981 |
done |
|
982 |
||
983 |
(*Concludes |
|
24147 | 984 |
System : {s. k \<le> (sub i o allocGiv) s} |
21632 | 985 |
LeadsTo |
21710 | 986 |
{s. (sub i o allocAsk) s \<le> (ask o sub i o client) s} Int |
987 |
{s. k \<le> (giv o sub i o client) s} *) |
|
21632 | 988 |
|
21710 | 989 |
lemmas System_lemma1 = |
990 |
Always_LeadsToD [OF System_Follows_ask [THEN Follows_Bounded] |
|
991 |
System_Follows_allocGiv [THEN Follows_LeadsTo]] |
|
21632 | 992 |
|
21710 | 993 |
lemmas System_lemma2 = |
994 |
PSP_Stable [OF System_lemma1 |
|
24147 | 995 |
System_Follows_ask [THEN Follows_Increasing1, THEN IncreasingD]] |
21710 | 996 |
|
997 |
||
24147 | 998 |
lemma System_lemma3: "i < Nclients |
67613 | 999 |
==> System \<in> {s. h \<le> (sub i o allocGiv) s & |
24147 | 1000 |
h pfixGe (sub i o allocAsk) s} |
1001 |
LeadsTo |
|
1002 |
{s. h \<le> (giv o sub i o client) s & |
|
21632 | 1003 |
h pfixGe (ask o sub i o client) s}" |
1004 |
apply (rule single_LeadsTo_I) |
|
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
44871
diff
changeset
|
1005 |
apply (rule_tac k1 = h and x1 = "(sub i o allocAsk) s" |
21710 | 1006 |
in System_lemma2 [THEN LeadsTo_weaken]) |
21632 | 1007 |
apply auto |
21710 | 1008 |
apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe) |
21632 | 1009 |
done |
1010 |
||
1011 |
||
63146 | 1012 |
text\<open>progress (2), step 8: Client i's "release" action is visible system-wide\<close> |
24147 | 1013 |
lemma System_Alloc_Client_Progress: "i < Nclients |
67613 | 1014 |
==> System \<in> {s. h \<le> (sub i o allocGiv) s & |
24147 | 1015 |
h pfixGe (sub i o allocAsk) s} |
21710 | 1016 |
LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel) s}" |
21632 | 1017 |
apply (rule LeadsTo_Trans) |
1018 |
prefer 2 |
|
1019 |
apply (drule System_Follows_rel [THEN |
|
1020 |
mono_tokens [THEN mono_Follows_o, THEN [2] rev_subsetD], |
|
1021 |
THEN Follows_LeadsTo]) |
|
1022 |
apply (simp add: o_assoc) |
|
1023 |
apply (rule LeadsTo_Trans) |
|
1024 |
apply (cut_tac [2] System_Client_Progress) |
|
1025 |
prefer 2 |
|
1026 |
apply (blast intro: LeadsTo_Basis) |
|
21710 | 1027 |
apply (erule System_lemma3) |
21632 | 1028 |
done |
1029 |
||
63146 | 1030 |
text\<open>Lifting \<open>Alloc_Progress\<close> up to the level of systemState\<close> |
21632 | 1031 |
|
63146 | 1032 |
text\<open>progress (2), step 9\<close> |
24147 | 1033 |
lemma System_Alloc_Progress: |
67613 | 1034 |
"System \<in> (INT i : (lessThan Nclients). |
24147 | 1035 |
INT h. {s. h \<le> (sub i o allocAsk) s} |
21632 | 1036 |
LeadsTo {s. h pfixLe (sub i o allocGiv) s})" |
1037 |
apply (simp only: o_apply sub_def) |
|
24147 | 1038 |
apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I]) |
32139 | 1039 |
apply (simp add: o_def del: INT_iff) |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61954
diff
changeset
|
1040 |
apply (drule component_guaranteesD) |
24147 | 1041 |
apply (auto simp add: |
21710 | 1042 |
System_Increasing_allocRel [simplified sub_apply o_def] |
1043 |
System_Increasing_allocAsk [simplified sub_apply o_def] |
|
1044 |
System_Bounded_allocAsk [simplified sub_apply o_def] |
|
1045 |
System_Alloc_Client_Progress [simplified sub_apply o_def]) |
|
21632 | 1046 |
done |
1047 |
||
63146 | 1048 |
text\<open>progress (2), step 10 (final result!)\<close> |
67613 | 1049 |
lemma System_Progress: "System \<in> system_progress" |
21632 | 1050 |
apply (unfold system_progress_def) |
1051 |
apply (cut_tac System_Alloc_Progress) |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61954
diff
changeset
|
1052 |
apply auto |
21632 | 1053 |
apply (blast intro: LeadsTo_Trans |
1054 |
System_Follows_allocGiv [THEN Follows_LeadsTo_pfixLe] |
|
1055 |
System_Follows_ask [THEN Follows_LeadsTo]) |
|
1056 |
done |
|
1057 |
||
1058 |
||
67613 | 1059 |
theorem System_correct: "System \<in> system_spec" |
21632 | 1060 |
apply (unfold system_spec_def) |
1061 |
apply (blast intro: System_safety System_Progress) |
|
1062 |
done |
|
1063 |
||
1064 |
||
63146 | 1065 |
text\<open>Some obsolete lemmas\<close> |
21632 | 1066 |
|
24147 | 1067 |
lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o |
21632 | 1068 |
(funPair giv (funPair ask rel))" |
1069 |
apply (rule ext) |
|
1070 |
apply (auto simp add: o_def non_dummy_def) |
|
1071 |
done |
|
1072 |
||
24147 | 1073 |
lemma preserves_non_dummy_eq: "(preserves non_dummy) = |
21632 | 1074 |
(preserves rel Int preserves ask Int preserves giv)" |
1075 |
apply (simp add: non_dummy_eq_o_funPair) |
|
1076 |
apply auto |
|
1077 |
apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD]) |
|
1078 |
apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD]) |
|
1079 |
apply (drule_tac [3] w1 = giv in subset_preserves_o [THEN [2] rev_subsetD]) |
|
1080 |
apply (auto simp add: o_def) |
|
1081 |
done |
|
1082 |
||
63146 | 1083 |
text\<open>Could go to Extend.ML\<close> |
67613 | 1084 |
lemma bij_fst_inv_inv_eq: "bij f \<Longrightarrow> fst (inv (%(x, u). inv f x) z) = f z" |
21632 | 1085 |
apply (rule fst_inv_equalityI) |
59807 | 1086 |
apply (rule_tac f = "%z. (f z, h z)" for h in surjI) |
21632 | 1087 |
apply (simp add: bij_is_inj inv_f_f) |
1088 |
apply (simp add: bij_is_surj surj_f_inv_f) |
|
1089 |
done |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
1090 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
1091 |
end |