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