author  paulson 
Wed, 16 Jul 2003 12:09:41 +0200  
changeset 14114  e97ca1034caa 
parent 14089  7b34f58b1b81 
child 15074  277b3a4da341 
permissions  rwrr 
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 multipleclient allocator from a singleclient 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 
(** Singleclient 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}) 
356 
\<subseteq> {s. (\<Sum>x \<in> 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 