author | wenzelm |
Tue, 13 Mar 2012 23:33:35 +0100 | |
changeset 46912 | e0cd5c4df8e6 |
parent 44871 | fbfdc5ac86be |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
1 |
(* Title: HOL/UNITY/Comp/AllocImpl.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 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
6 |
header{*Implementation of a multiple-client allocator from a single-client allocator*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
7 |
|
44871 | 8 |
theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
(** State definitions. OUTPUT variables are locals **) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
(*Type variable 'b is the type of items being merged*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
record 'b merge = |
14114 | 15 |
In :: "nat => 'b list" (*merge's INPUT histories: streams to merge*) |
16 |
Out :: "'b list" (*merge's OUTPUT history: merged items*) |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
17 |
iOut :: "nat list" (*merge's OUTPUT history: origins of merged items*) |
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,'b) merge_d = |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
20 |
"'b merge" + |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
dummy :: 'a (*dummy field for new variables*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
23 |
definition non_dummy :: "('a,'b) merge_d => 'b merge" where |
36866 | 24 |
"non_dummy s = (|In = In s, Out = Out s, iOut = iOut s|)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
record 'b distr = |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
27 |
In :: "'b list" (*items to distribute*) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
28 |
iIn :: "nat list" (*destinations of items to distribute*) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
29 |
Out :: "nat => 'b list" (*distributed items*) |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
record ('a,'b) distr_d = |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
32 |
"'b distr" + |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
dummy :: 'a (*dummy field for new variables*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
34 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
record allocState = |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
36 |
giv :: "nat list" (*OUTPUT history: source of tokens*) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
37 |
ask :: "nat list" (*INPUT: tokens requested from allocator*) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
38 |
rel :: "nat list" (*INPUT: tokens released to allocator*) |
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 + |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
42 |
dummy :: 'a (*dummy field for new variables*) |
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 + |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
46 |
mergeRel :: "nat merge" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
47 |
mergeAsk :: "nat merge" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
48 |
distr :: "nat distr" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
49 |
dummy :: 'a (*dummy field for new variables*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
50 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
51 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
52 |
(** Merge specification (the number of inputs is Nclients) ***) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
53 |
|
36866 | 54 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
55 |
(*spec (10)*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
56 |
merge_increasing :: "('a,'b) merge_d program set" |
36866 | 57 |
where "merge_increasing = |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
58 |
UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
59 |
|
36866 | 60 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
61 |
(*spec (11)*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
62 |
merge_eqOut :: "('a,'b) merge_d program set" |
36866 | 63 |
where "merge_eqOut = |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
64 |
UNIV guarantees |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
65 |
Always {s. length (merge.Out s) = length (merge.iOut s)}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
66 |
|
36866 | 67 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
68 |
(*spec (12)*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
69 |
merge_bounded :: "('a,'b) merge_d program set" |
36866 | 70 |
where "merge_bounded = |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
71 |
UNIV guarantees |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
72 |
Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
73 |
|
36866 | 74 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
75 |
(*spec (13)*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
76 |
merge_follows :: "('a,'b) merge_d program set" |
36866 | 77 |
where "merge_follows = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
78 |
(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
79 |
guarantees |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
80 |
(\<Inter>i \<in> lessThan Nclients. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
81 |
(%s. sublist (merge.Out s) |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
82 |
{k. k < size(merge.iOut s) & merge.iOut s! k = i}) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
83 |
Fols (sub i o merge.In))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
84 |
|
36866 | 85 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
86 |
(*spec: preserves part*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
87 |
merge_preserves :: "('a,'b) merge_d program set" |
36866 | 88 |
where "merge_preserves = preserves merge.In Int preserves merge_d.dummy" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
89 |
|
36866 | 90 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
91 |
(*environmental constraints*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
92 |
merge_allowed_acts :: "('a,'b) merge_d program set" |
36866 | 93 |
where "merge_allowed_acts = |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
94 |
{F. AllowedActs F = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
95 |
insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
96 |
|
36866 | 97 |
definition |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
98 |
merge_spec :: "('a,'b) merge_d program set" |
36866 | 99 |
where "merge_spec = merge_increasing Int merge_eqOut Int merge_bounded Int |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
100 |
merge_follows Int merge_allowed_acts Int merge_preserves" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
101 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
102 |
(** Distributor specification (the number of outputs is Nclients) ***) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
103 |
|
36866 | 104 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
105 |
(*spec (14)*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
106 |
distr_follows :: "('a,'b) distr_d program set" |
36866 | 107 |
where "distr_follows = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
108 |
Increasing distr.In Int Increasing distr.iIn Int |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
109 |
Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
110 |
guarantees |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
111 |
(\<Inter>i \<in> lessThan Nclients. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
112 |
(sub i o distr.Out) Fols |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
113 |
(%s. sublist (distr.In s) |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
114 |
{k. k < size(distr.iIn s) & distr.iIn s ! k = i}))" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
115 |
|
36866 | 116 |
definition |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
117 |
distr_allowed_acts :: "('a,'b) distr_d program set" |
36866 | 118 |
where "distr_allowed_acts = |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
119 |
{D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
120 |
|
36866 | 121 |
definition |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
122 |
distr_spec :: "('a,'b) distr_d program set" |
36866 | 123 |
where "distr_spec = distr_follows Int distr_allowed_acts" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
124 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
125 |
(** Single-client allocator specification (required) ***) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
126 |
|
36866 | 127 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
128 |
(*spec (18)*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
129 |
alloc_increasing :: "'a allocState_d program set" |
36866 | 130 |
where "alloc_increasing = UNIV guarantees Increasing giv" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
131 |
|
36866 | 132 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
133 |
(*spec (19)*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
134 |
alloc_safety :: "'a allocState_d program set" |
36866 | 135 |
where "alloc_safety = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
136 |
Increasing rel |
14114 | 137 |
guarantees Always {s. tokens (giv s) \<le> NbT + tokens (rel s)}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
138 |
|
36866 | 139 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
140 |
(*spec (20)*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
141 |
alloc_progress :: "'a allocState_d program set" |
36866 | 142 |
where "alloc_progress = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
143 |
Increasing ask Int Increasing rel Int |
14114 | 144 |
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
|
145 |
Int |
14114 | 146 |
(\<Inter>h. {s. h \<le> giv s & h pfixGe (ask s)} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
147 |
LeadsTo |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
148 |
{s. tokens h \<le> tokens (rel s)}) |
14114 | 149 |
guarantees (\<Inter>h. {s. h \<le> ask s} LeadsTo {s. h pfixLe giv s})" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
150 |
|
36866 | 151 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
152 |
(*spec: preserves part*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
153 |
alloc_preserves :: "'a allocState_d program set" |
36866 | 154 |
where "alloc_preserves = preserves rel Int |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
155 |
preserves ask Int |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
156 |
preserves allocState_d.dummy" |
14114 | 157 |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
158 |
|
36866 | 159 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
160 |
(*environmental constraints*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
161 |
alloc_allowed_acts :: "'a allocState_d program set" |
36866 | 162 |
where "alloc_allowed_acts = |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
163 |
{F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
164 |
|
36866 | 165 |
definition |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
166 |
alloc_spec :: "'a allocState_d program set" |
36866 | 167 |
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
|
168 |
alloc_allowed_acts Int alloc_preserves" |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
169 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
170 |
locale Merge = |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
171 |
fixes M :: "('a,'b::order) merge_d program" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
172 |
assumes |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
173 |
Merge_spec: "M \<in> merge_spec" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
174 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
175 |
locale Distrib = |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
176 |
fixes D :: "('a,'b::order) distr_d program" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
177 |
assumes |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
178 |
Distrib_spec: "D \<in> distr_spec" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
179 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
180 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
181 |
(**** |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
182 |
# {** Network specification ***} |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
183 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
184 |
# {*spec (9.1)*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
185 |
# network_ask :: "'a systemState program set |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
186 |
# "network_ask == \<Inter>i \<in> lessThan Nclients. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
187 |
# Increasing (ask o sub i o client) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
188 |
# guarantees[ask] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
189 |
# (ask Fols (ask o sub i o client))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
190 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
191 |
# {*spec (9.2)*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
192 |
# network_giv :: "'a systemState program set |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
193 |
# "network_giv == \<Inter>i \<in> lessThan Nclients. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
194 |
# Increasing giv |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
195 |
# guarantees[giv o sub i o client] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
196 |
# ((giv o sub i o client) Fols giv)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
197 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
198 |
# {*spec (9.3)*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
199 |
# network_rel :: "'a systemState program set |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
200 |
# "network_rel == \<Inter>i \<in> lessThan Nclients. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
201 |
# Increasing (rel o sub i o client) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
202 |
# guarantees[rel] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
203 |
# (rel Fols (rel o sub i o client))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
204 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
205 |
# {*spec: preserves part*} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
206 |
# network_preserves :: "'a systemState program set |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
207 |
# "network_preserves == preserves giv Int |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
208 |
# (\<Inter>i \<in> lessThan Nclients. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
209 |
# preserves (funPair rel ask o sub i o client))" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
210 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
211 |
# network_spec :: "'a systemState program set |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
212 |
# "network_spec == network_ask Int network_giv Int |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
213 |
# network_rel Int network_preserves" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
214 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
215 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
216 |
# {** State mappings **} |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
217 |
# sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
218 |
# "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
219 |
# in (| giv = giv s, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
220 |
# ask = ask s, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
221 |
# rel = rel s, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
222 |
# client = cl, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
223 |
# dummy = xtr|)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
224 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
225 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
226 |
# sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
227 |
# "sysOfClient == %(cl,al). (| giv = giv al, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
228 |
# ask = ask al, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
229 |
# rel = rel al, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
230 |
# client = cl, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
231 |
# systemState.dummy = allocState_d.dummy al|)" |
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 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
234 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
235 |
declare subset_preserves_o [THEN subsetD, intro] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
236 |
declare funPair_o_distrib [simp] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
237 |
declare Always_INT_distrib [simp] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
238 |
declare o_apply [simp del] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
239 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
240 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
241 |
subsection{*Theorems for Merge*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
242 |
|
46912 | 243 |
context Merge |
244 |
begin |
|
245 |
||
246 |
lemma Merge_Allowed: |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
247 |
"Allowed M = (preserves merge.Out) Int (preserves merge.iOut)" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
248 |
apply (cut_tac Merge_spec) |
14114 | 249 |
apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def |
250 |
safety_prop_Acts_iff) |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
251 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
252 |
|
46912 | 253 |
lemma M_ok_iff [iff]: |
14114 | 254 |
"M ok G = (G \<in> preserves merge.Out & G \<in> preserves merge.iOut & |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
255 |
M \<in> Allowed G)" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
256 |
by (auto simp add: Merge_Allowed ok_iff_Allowed) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
257 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
258 |
|
46912 | 259 |
lemma Merge_Always_Out_eq_iOut: |
14114 | 260 |
"[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |] |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
261 |
==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
262 |
apply (cut_tac Merge_spec) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
263 |
apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
264 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
265 |
|
46912 | 266 |
lemma Merge_Bounded: |
14114 | 267 |
"[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |] |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
268 |
==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
269 |
apply (cut_tac Merge_spec) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
270 |
apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
271 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
272 |
|
46912 | 273 |
lemma Merge_Bag_Follows_lemma: |
14114 | 274 |
"[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |] |
275 |
==> M Join G \<in> Always |
|
276 |
{s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (merge.Out s) |
|
277 |
{k. k < length (iOut s) & iOut s ! k = i})) = |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
278 |
(bag_of o merge.Out) s}" |
14114 | 279 |
apply (rule Always_Compl_Un_eq [THEN iffD1]) |
280 |
apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded]) |
|
281 |
apply (rule UNIV_AlwaysI, clarify) |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
282 |
apply (subst bag_of_sublist_UN_disjoint [symmetric]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
283 |
apply (simp) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
284 |
apply blast |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
285 |
apply (simp add: set_conv_nth) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
286 |
apply (subgoal_tac |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
287 |
"(\<Union>i \<in> lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
288 |
lessThan (length (iOut x))") |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
289 |
apply (simp (no_asm_simp) add: o_def) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
290 |
apply blast |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
291 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
292 |
|
46912 | 293 |
lemma Merge_Bag_Follows: |
14114 | 294 |
"M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In)) |
295 |
guarantees |
|
296 |
(bag_of o merge.Out) Fols |
|
297 |
(%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o merge.In) s)" |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
298 |
apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
299 |
apply (rule Follows_setsum) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
300 |
apply (cut_tac Merge_spec) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
301 |
apply (auto simp add: merge_spec_def merge_follows_def o_def) |
14114 | 302 |
apply (drule guaranteesD) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
303 |
prefer 3 |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
304 |
apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
305 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
306 |
|
46912 | 307 |
end |
308 |
||
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
309 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
310 |
subsection{*Theorems for Distributor*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
311 |
|
46912 | 312 |
context Distrib |
313 |
begin |
|
314 |
||
315 |
lemma Distr_Increasing_Out: |
|
14114 | 316 |
"D \<in> Increasing distr.In Int Increasing distr.iIn Int |
317 |
Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |
|
318 |
guarantees |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
319 |
(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o distr.Out))" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
320 |
apply (cut_tac Distrib_spec) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
321 |
apply (simp add: distr_spec_def distr_follows_def) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
322 |
apply clarify |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
323 |
apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
324 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
325 |
|
46912 | 326 |
lemma Distr_Bag_Follows_lemma: |
14114 | 327 |
"[| G \<in> preserves distr.Out; |
328 |
D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |] |
|
329 |
==> D Join G \<in> Always |
|
330 |
{s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s) |
|
331 |
{k. k < length (iIn s) & iIn s ! k = i})) = |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
332 |
bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
333 |
apply (erule Always_Compl_Un_eq [THEN iffD1]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
334 |
apply (rule UNIV_AlwaysI, clarify) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
335 |
apply (subst bag_of_sublist_UN_disjoint [symmetric]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
336 |
apply (simp (no_asm)) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
337 |
apply blast |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
338 |
apply (simp add: set_conv_nth) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
339 |
apply (subgoal_tac |
14114 | 340 |
"(\<Union>i \<in> lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
341 |
lessThan (length (iIn x))") |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
342 |
apply (simp (no_asm_simp)) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
343 |
apply blast |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
344 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
345 |
|
46912 | 346 |
lemma D_ok_iff [iff]: |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
347 |
"D ok G = (G \<in> preserves distr.Out & D \<in> Allowed G)" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
348 |
apply (cut_tac Distrib_spec) |
14114 | 349 |
apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
350 |
safety_prop_Acts_iff ok_iff_Allowed) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
351 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
352 |
|
46912 | 353 |
lemma Distr_Bag_Follows: |
14114 | 354 |
"D \<in> Increasing distr.In Int Increasing distr.iIn Int |
355 |
Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |
|
356 |
guarantees |
|
357 |
(\<Inter>i \<in> lessThan Nclients. |
|
358 |
(%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o distr.Out) s) |
|
359 |
Fols |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
360 |
(%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
361 |
apply (rule guaranteesI, clarify) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
362 |
apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
363 |
apply (rule Follows_setsum) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
364 |
apply (cut_tac Distrib_spec) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
365 |
apply (auto simp add: distr_spec_def distr_follows_def o_def) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
366 |
apply (drule guaranteesD) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
367 |
prefer 3 |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
368 |
apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
369 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
370 |
|
46912 | 371 |
end |
372 |
||
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
373 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
374 |
subsection{*Theorems for Allocator*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
375 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
376 |
lemma alloc_refinement_lemma: |
14114 | 377 |
"!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s}) |
15074 | 378 |
\<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}" |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
379 |
apply (induct_tac "n") |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
380 |
apply (auto simp add: lessThan_Suc) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
381 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
382 |
|
14114 | 383 |
lemma alloc_refinement: |
384 |
"(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int |
|
385 |
Increasing (sub i o allocRel)) |
|
386 |
Int |
|
387 |
Always {s. \<forall>i. i<Nclients --> |
|
388 |
(\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)} |
|
389 |
Int |
|
390 |
(\<Inter>i \<in> lessThan Nclients. |
|
391 |
\<Inter>h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} |
|
392 |
LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel)s}) |
|
393 |
\<subseteq> |
|
394 |
(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int |
|
395 |
Increasing (sub i o allocRel)) |
|
396 |
Int |
|
397 |
Always {s. \<forall>i. i<Nclients --> |
|
398 |
(\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)} |
|
399 |
Int |
|
400 |
(\<Inter>hf. (\<Inter>i \<in> lessThan Nclients. |
|
401 |
{s. hf i \<le> (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) |
|
402 |
LeadsTo {s. (\<Sum>i \<in> lessThan Nclients. tokens (hf i)) \<le> |
|
403 |
(\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)})" |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
404 |
apply (auto simp add: ball_conj_distrib) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
405 |
apply (rename_tac F hf) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
406 |
apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
407 |
apply (subgoal_tac "F \<in> Increasing (tokens o (sub i o allocRel))") |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
408 |
apply (simp add: Increasing_def o_assoc) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
409 |
apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
410 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
11194
diff
changeset
|
411 |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
412 |
end |