author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58860  fee7cfa69c50 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

1 
(* Title: ZF/UNITY/AllocImpl.thy 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

2 
Author: Sidi O Ehmety, Cambridge University Computer Laboratory 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

3 
Copyright 2002 University of Cambridge 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

4 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

5 
Singleclient allocator implementation. 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

6 
Charpentier and Chandy, section 7 (page 17). 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

7 
*) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

8 

16417  9 
theory AllocImpl imports ClientImpl begin 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

10 

24892  11 
abbreviation 
12 
NbR :: i (*number of consumed messages*) where 

13 
"NbR == Var([succ(2)])" 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

14 

24892  15 
abbreviation 
16 
available_tok :: i (*number of free tokens (T in paper)*) where 

17 
"available_tok == Var([succ(succ(2))])" 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

18 

41779  19 
axiomatization where 
14071  20 
alloc_type_assumes [simp]: 
41779  21 
"type_of(NbR) = nat & type_of(available_tok)=nat" and 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

22 

14071  23 
alloc_default_val_assumes [simp]: 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

24 
"default_val(NbR) = 0 & default_val(available_tok)=0" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

25 

24893  26 
definition 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

27 
"alloc_giv_act == 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

28 
{<s, t> \<in> state*state. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

29 
\<exists>k. k = length(s`giv) & 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

30 
t = s(giv := s`giv @ [nth(k, s`ask)], 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

31 
available_tok := s`available_tok # nth(k, s`ask)) & 
46823  32 
k < length(s`ask) & nth(k, s`ask) \<le> s`available_tok}" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

33 

24893  34 
definition 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

35 
"alloc_rel_act == 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

36 
{<s, t> \<in> state*state. 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

37 
t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

38 
NbR := succ(s`NbR)) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

39 
s`NbR < length(s`rel)}" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

40 

24893  41 
definition 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

42 
(*The initial condition s`giv=[] is missing from the 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

43 
original definition: S. O. Ehmety *) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

44 
"alloc_prog == 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

45 
mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil}, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

46 
{alloc_giv_act, alloc_rel_act}, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

47 
\<Union>G \<in> preserves(lift(available_tok)) \<inter> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

48 
preserves(lift(NbR)) \<inter> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

49 
preserves(lift(giv)). Acts(G))" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

50 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

51 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

52 
lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

53 
apply (unfold state_def) 
14071  54 
apply (drule_tac a = available_tok in apply_type, auto) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

55 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

56 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

57 
lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

58 
apply (unfold state_def) 
14071  59 
apply (drule_tac a = NbR in apply_type, auto) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

60 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

61 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

62 
(** The Alloc Program **) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

63 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

64 
lemma alloc_prog_type [simp,TC]: "alloc_prog \<in> program" 
14071  65 
by (simp add: alloc_prog_def) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

66 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

67 
declare alloc_prog_def [THEN def_prg_Init, simp] 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

68 
declare alloc_prog_def [THEN def_prg_AllowedActs, simp] 
24051
896fb015079c
replaced program_defs_ref by proper context data (via attribute "program");
wenzelm
parents:
16417
diff
changeset

69 
declare alloc_prog_def [program] 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

70 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

71 
declare alloc_giv_act_def [THEN def_act_simp, simp] 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

72 
declare alloc_rel_act_def [THEN def_act_simp, simp] 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

73 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

74 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

75 
lemma alloc_prog_ok_iff: 
46823  76 
"\<forall>G \<in> program. (alloc_prog ok G) \<longleftrightarrow> 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

77 
(G \<in> preserves(lift(giv)) & G \<in> preserves(lift(available_tok)) & 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

78 
G \<in> preserves(lift(NbR)) & alloc_prog \<in> Allowed(G))" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

79 
by (auto simp add: ok_iff_Allowed alloc_prog_def [THEN def_prg_Allowed]) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

80 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

81 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

82 
lemma alloc_prog_preserves: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

83 
"alloc_prog \<in> (\<Inter>x \<in> var{giv, available_tok, NbR}. preserves(lift(x)))" 
14071  84 
apply (rule Inter_var_DiffI, force) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

85 
apply (rule ballI) 
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15481
diff
changeset

86 
apply (rule preservesI, safety) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

87 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

88 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

89 
(* As a special case of the rule above *) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

90 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

91 
lemma alloc_prog_preserves_rel_ask_tok: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

92 
"alloc_prog \<in> 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

93 
preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

94 
apply auto 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

95 
apply (insert alloc_prog_preserves) 
14071  96 
apply (drule_tac [3] x = tok in Inter_var_DiffD) 
97 
apply (drule_tac [2] x = ask in Inter_var_DiffD) 

98 
apply (drule_tac x = rel in Inter_var_DiffD, auto) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

99 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

100 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

101 
lemma alloc_prog_Allowed: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

102 
"Allowed(alloc_prog) = 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

103 
preserves(lift(giv)) \<inter> preserves(lift(available_tok)) \<inter> preserves(lift(NbR))" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

104 
apply (cut_tac v="lift(giv)" in preserves_type) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

105 
apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed] 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

106 
cons_Int_distrib safety_prop_Acts_iff) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

107 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

108 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

109 
(* In particular we have *) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

110 
lemma alloc_prog_ok_client_prog: "alloc_prog ok client_prog" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

111 
apply (auto simp add: ok_iff_Allowed) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

112 
apply (cut_tac alloc_prog_preserves) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

113 
apply (cut_tac [2] client_prog_preserves) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

114 
apply (auto simp add: alloc_prog_Allowed client_prog_Allowed) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

115 
apply (drule_tac [6] B = "preserves (lift (NbR))" in InterD) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

116 
apply (drule_tac [5] B = "preserves (lift (available_tok))" in InterD) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

117 
apply (drule_tac [4] B = "preserves (lift (giv))" in InterD) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

118 
apply (drule_tac [3] B = "preserves (lift (tok))" in InterD) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

119 
apply (drule_tac [2] B = "preserves (lift (ask))" in InterD) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

120 
apply (drule_tac B = "preserves (lift (rel))" in InterD) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

121 
apply auto 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

122 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

123 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

124 
(** Safety property: (28) **) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

125 
lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))" 
26289  126 
apply (auto intro!: increasing_imp_Increasing simp add: guar_def 
127 
Increasing.increasing_def alloc_prog_ok_iff alloc_prog_Allowed, safety+) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

128 
apply (auto dest: ActsD) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

129 
apply (drule_tac f = "lift (giv) " in preserves_imp_eq) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

130 
apply auto 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

131 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

132 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

133 
lemma giv_Bounded_lamma1: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

134 
"alloc_prog \<in> stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter> 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

135 
{s\<in>state. s`available_tok #+ tokens(s`giv) = 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

136 
NbT #+ tokens(take(s`NbR, s`rel))})" 
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15481
diff
changeset

137 
apply safety 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

138 
apply auto 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

139 
apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

140 
apply (simp (no_asm_simp) add: take_succ) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

141 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

142 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

143 
lemma giv_Bounded_lemma2: 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

144 
"[ G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)) ] 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

145 
==> alloc_prog \<squnion> G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter> 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

146 
{s\<in>state. s`available_tok #+ tokens(s`giv) = 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

147 
NbT #+ tokens(take(s`NbR, s`rel))})" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

148 
apply (cut_tac giv_Bounded_lamma1) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

149 
apply (cut_tac alloc_prog_preserves_rel_ask_tok) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

150 
apply (auto simp add: Collect_conj_eq [symmetric] alloc_prog_ok_iff) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

151 
apply (subgoal_tac "G \<in> preserves (fun_pair (lift (available_tok), fun_pair (lift (NbR), lift (giv))))") 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

152 
apply (rotate_tac 1) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

153 
apply (cut_tac A = "nat * nat * list(nat)" 
14071  154 
and P = "%<m,n,l> y. n \<le> length(y) & 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

155 
m #+ tokens(l) = NbT #+ tokens(take(n,y))" 
14071  156 
and g = "lift(rel)" and F = alloc_prog 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

157 
in stable_Join_Stable) 
14071  158 
prefer 3 apply assumption 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

159 
apply (auto simp add: Collect_conj_eq) 
14071  160 
apply (frule_tac g = length in imp_Increasing_comp) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

161 
apply (blast intro: mono_length) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

162 
apply (auto simp add: refl_prefix) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

163 
apply (drule_tac a=xa and f = "length comp lift(rel)" in Increasing_imp_Stable) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

164 
apply assumption 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

165 
apply (auto simp add: Le_def length_type) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

166 
apply (auto dest: ActsD simp add: Stable_def Constrains_def constrains_def) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

167 
apply (drule_tac f = "lift (rel) " in preserves_imp_eq) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

168 
apply assumption+ 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

169 
apply (force dest: ActsD) 
46823  170 
apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) \<union> Acts (G). ?P(x)" in thin_rl) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

171 
apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

172 
apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

173 
apply (auto simp add: Stable_def Constrains_def constrains_def) 
14071  174 
apply (drule bspec, force) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

175 
apply (drule subsetD) 
14071  176 
apply (rule imageI, assumption) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

177 
apply (auto simp add: prefix_take_iff) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

178 
apply (rotate_tac 1) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

179 
apply (erule ssubst) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

180 
apply (auto simp add: take_take min_def) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

181 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

182 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

183 
(*Property (29), page 18: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

184 
the number of tokens in circulation never exceeds NbT*) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

185 
lemma alloc_prog_giv_Bounded: "alloc_prog \<in> Incr(lift(rel)) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

186 
guarantees Always({s\<in>state. tokens(s`giv) \<le> NbT #+ tokens(s`rel)})" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

187 
apply (cut_tac NbT_pos) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

188 
apply (auto simp add: guar_def) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

189 
apply (rule Always_weaken) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

190 
apply (rule AlwaysI) 
14071  191 
apply (rule_tac [2] giv_Bounded_lemma2, auto) 
192 
apply (rule_tac j = "NbT #+ tokens(take (x` NbR, x`rel))" in le_trans) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

193 
apply (erule subst) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

194 
apply (auto intro!: tokens_mono simp add: prefix_take_iff min_def length_take) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

195 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

196 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

197 
(*Property (30), page 18: the number of tokens given never exceeds the number 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

198 
asked for*) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

199 
lemma alloc_prog_ask_prefix_giv: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

200 
"alloc_prog \<in> Incr(lift(ask)) guarantees 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

201 
Always({s\<in>state. <s`giv, s`ask> \<in> prefix(tokbag)})" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

202 
apply (auto intro!: AlwaysI simp add: guar_def) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

203 
apply (subgoal_tac "G \<in> preserves (lift (giv))") 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

204 
prefer 2 apply (simp add: alloc_prog_ok_iff) 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

205 
apply (rule_tac P = "%x y. <x,y> \<in> prefix(tokbag)" and A = "list(nat)" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

206 
in stable_Join_Stable) 
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15481
diff
changeset

207 
apply safety 
14071  208 
prefer 2 apply (simp add: lift_def, clarify) 
209 
apply (drule_tac a = k in Increasing_imp_Stable, auto) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

210 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

211 

14071  212 
subsection{* Towards proving the liveness property, (31) *} 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

213 

14071  214 
subsubsection{*First, we lead up to a proof of Lemma 49, page 28.*} 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

215 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

216 
lemma alloc_prog_transient_lemma: 
14071  217 
"[G \<in> program; k\<in>nat] 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

218 
==> alloc_prog \<squnion> G \<in> 
14071  219 
transient({s\<in>state. k \<le> length(s`rel)} \<inter> 
220 
{s\<in>state. succ(s`NbR) = k})" 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

221 
apply auto 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

222 
apply (erule_tac V = "G\<notin>?u" in thin_rl) 
14071  223 
apply (rule_tac act = alloc_rel_act in transientI) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

224 
apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts]) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

225 
apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset]) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

226 
apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

227 
apply (rule ReplaceI) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

228 
apply (rule_tac x = "x (available_tok:= x`available_tok #+ nth (x`NbR, x`rel), 
14071  229 
NbR:=succ (x`NbR))" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

230 
in exI) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

231 
apply (auto intro!: state_update_type) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

232 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

233 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

234 
lemma alloc_prog_rel_Stable_NbR_lemma: 
14071  235 
"[ G \<in> program; alloc_prog ok G; k\<in>nat ] 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

236 
==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})" 
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15481
diff
changeset

237 
apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety, auto) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

238 
apply (blast intro: le_trans leI) 
14071  239 
apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing) 
240 
apply (drule_tac [2] g = succ in imp_increasing_comp) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

241 
apply (rule_tac [2] mono_succ) 
14071  242 
apply (drule_tac [4] x = k in increasing_imp_stable) 
243 
prefer 5 apply (simp add: Le_def comp_def, auto) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

244 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

245 

14071  246 
lemma alloc_prog_NbR_LeadsTo_lemma: 
247 
"[ G \<in> program; alloc_prog ok G; 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

248 
alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat ] 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

249 
==> alloc_prog \<squnion> G \<in> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

250 
{s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

251 
LeadsTo {s\<in>state. k \<le> s`NbR}" 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

252 
apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})") 
14071  253 
apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable]) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

254 
apply (rule_tac [2] mono_length) 
14071  255 
prefer 3 apply simp 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

256 
apply (simp_all add: refl_prefix Le_def comp_def length_type) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

257 
apply (rule LeadsTo_weaken) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

258 
apply (rule PSP_Stable) 
14071  259 
prefer 2 apply assumption 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

260 
apply (rule PSP_Stable) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

261 
apply (rule_tac [2] alloc_prog_rel_Stable_NbR_lemma) 
14071  262 
apply (rule alloc_prog_transient_lemma [THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo], assumption+) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

263 
apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

264 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

265 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

266 
lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]: 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

267 
"[ G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)); 
14071  268 
k\<in>nat; n \<in> nat; n < k ] 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

269 
==> alloc_prog \<squnion> G \<in> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

270 
{s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

271 
LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

272 
(\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

273 
apply (unfold greater_than_def) 
14071  274 
apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}" 
275 
in LeadsTo_weaken_R) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

276 
apply safe 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

277 
apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ") 
14071  278 
apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable]) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

279 
apply (rule_tac [2] mono_length) 
14071  280 
prefer 3 apply simp 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

281 
apply (simp_all add: refl_prefix Le_def comp_def length_type) 
15481  282 
apply (subst Int_commute [of _ "{x \<in> state . n < x ` NbR}"]) 
283 
apply (rule_tac A = "({s \<in> state . k \<le> length (s ` rel) } \<inter> 

284 
{s\<in>state . s ` NbR = n}) \<inter> {s\<in>state. k \<le> length(s`rel)}" 

285 
in LeadsTo_weaken_L) 

14071  286 
apply (rule PSP_Stable, safe) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

287 
apply (rule_tac B = "{x \<in> state . n < length (x ` rel) } \<inter> {s\<in>state . s ` NbR = n}" in LeadsTo_Trans) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

288 
apply (rule_tac [2] LeadsTo_weaken) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

289 
apply (rule_tac [2] k = "succ (n)" in alloc_prog_NbR_LeadsTo_lemma) 
14071  290 
apply simp_all 
291 
apply (rule subset_imp_LeadsTo, auto) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

292 
apply (blast intro: lt_trans2) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

293 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

294 

14071  295 
lemma Collect_vimage_eq: "u\<in>nat ==> {<s,f(s)>. s \<in> A} `` u = {s\<in>A. f(s) < u}" 
296 
by (force simp add: lt_def) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

297 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

298 
(* Lemma 49, page 28 *) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

299 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

300 
lemma alloc_prog_NbR_LeadsTo_lemma3: 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

301 
"[G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)); 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

302 
k\<in>nat] 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

303 
==> alloc_prog \<squnion> G \<in> 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

304 
{s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

305 
(* Proof by induction over the difference between k and n *) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

306 
apply (rule_tac f = "\<lambda>s\<in>state. k # s`NbR" in LessThan_induct) 
14071  307 
apply (simp_all add: lam_def, auto) 
308 
apply (rule single_LeadsTo_I, auto) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

309 
apply (simp (no_asm_simp) add: Collect_vimage_eq) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

310 
apply (rename_tac "s0") 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

311 
apply (case_tac "s0`NbR < k") 
14071  312 
apply (rule_tac [2] subset_imp_LeadsTo, safe) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

313 
apply (auto dest!: not_lt_imp_le) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

314 
apply (rule LeadsTo_weaken) 
14071  315 
apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2, safe) 
316 
prefer 3 apply assumption 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

317 
apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

318 
apply (blast dest: lt_asym) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

319 
apply (force dest: add_lt_elim2) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

320 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

321 

14071  322 
subsubsection{*Towards proving lemma 50, page 29*} 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

323 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

324 
lemma alloc_prog_giv_Ensures_lemma: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

325 
"[ G \<in> program; k\<in>nat; alloc_prog ok G; 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

326 
alloc_prog \<squnion> G \<in> Incr(lift(ask)) ] ==> 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

327 
alloc_prog \<squnion> G \<in> 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

328 
{s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter> 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

329 
{s\<in>state. k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k} 
46823  330 
Ensures {s\<in>state. ~ k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}" 
14071  331 
apply (rule EnsuresI, auto) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

332 
apply (erule_tac [2] V = "G\<notin>?u" in thin_rl) 
14071  333 
apply (rule_tac [2] act = alloc_giv_act in transientI) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

334 
prefer 2 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

335 
apply (simp add: alloc_prog_def [THEN def_prg_Acts]) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

336 
apply (simp add: alloc_giv_act_def [THEN def_act_eq, THEN act_subset]) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

337 
apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

338 
apply (erule_tac [2] swap) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

339 
apply (rule_tac [2] ReplaceI) 
14071  340 
apply (rule_tac [2] x = "x (giv := x ` giv @ [nth (length(x`giv), x ` ask) ], available_tok := x ` available_tok # nth (length(x`giv), x ` ask))" in exI) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

341 
apply (auto intro!: state_update_type simp add: app_type) 
46823  342 
apply (rule_tac A = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} \<inter> {s\<in>state . k < length(s ` ask) } \<inter> {s\<in>state. length(s`giv) =k}" and A' = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} \<union> {s\<in>state. ~ k < length(s`ask) } \<union> {s\<in>state . length(s ` giv) \<noteq> k}" in Constrains_weaken) 
14071  343 
apply (auto dest: ActsD simp add: Constrains_def constrains_def alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff) 
344 
apply (subgoal_tac "length(xa ` giv @ [nth (length(xa ` giv), xa ` ask) ]) = length(xa ` giv) #+ 1") 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

345 
apply (rule_tac [2] trans) 
14071  346 
apply (rule_tac [2] length_app, auto) 
347 
apply (rule_tac j = "xa ` available_tok" in le_trans, auto) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

348 
apply (drule_tac f = "lift (available_tok)" in preserves_imp_eq) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

349 
apply assumption+ 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

350 
apply auto 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

351 
apply (drule_tac a = "xa ` ask" and r = "prefix(tokbag)" and A = "list(tokbag)" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

352 
in Increasing_imp_Stable) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

353 
apply (auto simp add: prefix_iff) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

354 
apply (drule StableD) 
14071  355 
apply (auto simp add: Constrains_def constrains_def, force) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

356 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

357 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

358 
lemma alloc_prog_giv_Stable_lemma: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

359 
"[ G \<in> program; alloc_prog ok G; k\<in>nat ] 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

360 
==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})" 
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15481
diff
changeset

361 
apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety) 
14071  362 
apply (auto intro: leI) 
363 
apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp) 

364 
apply (drule_tac f = "length comp lift (giv)" and A = nat and r = Le in preserves_imp_increasing) 

365 
apply (drule_tac [2] x = k in increasing_imp_stable) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

366 
prefer 3 apply (simp add: Le_def comp_def) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

367 
apply (auto simp add: length_type) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

368 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

369 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

370 
(* Lemma 50, page 29 *) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

371 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

372 
lemma alloc_prog_giv_LeadsTo_lemma: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

373 
"[ G \<in> program; alloc_prog ok G; 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

374 
alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat ] 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

375 
==> alloc_prog \<squnion> G \<in> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

376 
{s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

377 
{s\<in>state. k < length(s`ask)} \<inter> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

378 
{s\<in>state. length(s`giv) = k} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

379 
LeadsTo {s\<in>state. k < length(s`giv)}" 
46823  380 
apply (subgoal_tac "alloc_prog \<squnion> G \<in> {s\<in>state. nth (length(s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length(s`ask) } \<inter> {s\<in>state. length(s`giv) = k} LeadsTo {s\<in>state. ~ k <length(s`ask) } \<union> {s\<in>state. length(s`giv) \<noteq> k}") 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

381 
prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis]) 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

382 
apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k < length(s`ask) }) ") 
14071  383 
apply (drule PSP_Stable, assumption) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

384 
apply (rule LeadsTo_weaken) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

385 
apply (rule PSP_Stable) 
14071  386 
apply (rule_tac [2] k = k in alloc_prog_giv_Stable_lemma) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

387 
apply (auto simp add: le_iff) 
14071  388 
apply (drule_tac a = "succ (k)" and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable]) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

389 
apply (rule mono_length) 
14071  390 
prefer 2 apply simp 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

391 
apply (simp_all add: refl_prefix Le_def comp_def length_type) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

392 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

393 

14076  394 

395 
text{*Lemma 51, page 29. 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

396 
This theorem states as invariant that if the number of 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

397 
tokens given does not exceed the number returned, then the upper limit 
14076  398 
(@{term NbT}) does not exceed the number currently available.*} 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

399 
lemma alloc_prog_Always_lemma: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

400 
"[ G \<in> program; alloc_prog ok G; 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

401 
alloc_prog \<squnion> G \<in> Incr(lift(ask)); 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

402 
alloc_prog \<squnion> G \<in> Incr(lift(rel)) ] 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

403 
==> alloc_prog \<squnion> G \<in> 
46823  404 
Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) \<longrightarrow> 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

405 
NbT \<le> s`available_tok})" 
14076  406 
apply (subgoal_tac 
407 
"alloc_prog \<squnion> G 

408 
\<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter> 

409 
{s\<in>state. s`available_tok #+ tokens(s`giv) = 

410 
NbT #+ tokens(take (s`NbR, s`rel))})") 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

411 
apply (rule_tac [2] AlwaysI) 
14071  412 
apply (rule_tac [3] giv_Bounded_lemma2, auto) 
413 
apply (rule Always_weaken, assumption, auto) 

414 
apply (subgoal_tac "0 \<le> tokens(take (x ` NbR, x ` rel)) # tokens(x`giv) ") 

14076  415 
prefer 2 apply (force) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

416 
apply (subgoal_tac "x`available_tok = 
14071  417 
NbT #+ (tokens(take(x`NbR,x`rel)) # tokens(x`giv))") 
14076  418 
apply (simp add: ); 
419 
apply (auto split add: nat_diff_split dest: lt_trans2) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

420 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

421 

14076  422 

423 

14071  424 
subsubsection{* Main lemmas towards proving property (31)*} 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

425 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

426 
lemma LeadsTo_strength_R: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

427 
"[ F \<in> C LeadsTo B'; F \<in> AC LeadsTo B; B'<=B ] ==> F \<in> A LeadsTo B" 
14071  428 
by (blast intro: LeadsTo_weaken LeadsTo_Un_Un) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

429 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

430 
lemma PSP_StableI: 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

431 
"[ F \<in> Stable(C); F \<in> A  C LeadsTo B; 
46823  432 
F \<in> A \<inter> C LeadsTo B \<union> (state  C) ] ==> F \<in> A LeadsTo B" 
433 
apply (rule_tac A = " (AC) \<union> (A \<inter> C)" in LeadsTo_weaken_L) 

14071  434 
prefer 2 apply blast 
435 
apply (rule LeadsTo_Un, assumption) 

436 
apply (blast intro: LeadsTo_weaken dest: PSP_Stable) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

437 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

438 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

439 
lemma state_compl_eq [simp]: "state  {s\<in>state. P(s)} = {s\<in>state. ~P(s)}" 
14071  440 
by auto 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

441 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

442 
(*needed?*) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

443 
lemma single_state_Diff_eq [simp]: "{s}{x \<in> state. P(x)} = (if s\<in>state & P(s) then 0 else {s})" 
14071  444 
by auto 
445 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

446 

14071  447 
locale alloc_progress = 
448 
fixes G 

449 
assumes Gprog [intro,simp]: "G \<in> program" 

450 
and okG [iff]: "alloc_prog ok G" 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

451 
and Incr_rel [intro]: "alloc_prog \<squnion> G \<in> Incr(lift(rel))" 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

452 
and Incr_ask [intro]: "alloc_prog \<squnion> G \<in> Incr(lift(ask))" 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

453 
and safety: "alloc_prog \<squnion> G 
14071  454 
\<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})" 
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

455 
and progress: "alloc_prog \<squnion> G 
14071  456 
\<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo 
457 
{s\<in>state. k \<le> tokens(s`rel)})" 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

458 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

459 
(*First step in proof of (31)  the corrected version from Charpentier. 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

460 
This lemma implies that if a client releases some tokens then the Allocator 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

461 
will eventually recognize that they've been released.*) 
14071  462 
lemma (in alloc_progress) tokens_take_NbR_lemma: 
463 
"k \<in> tokbag 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

464 
==> alloc_prog \<squnion> G \<in> 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

465 
{s\<in>state. k \<le> tokens(s`rel)} 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

466 
LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}" 
14071  467 
apply (rule single_LeadsTo_I, safe) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

468 
apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI]) 
14071  469 
apply (rule_tac [4] k1 = "length(s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R]) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

470 
apply (rule_tac [8] subset_imp_LeadsTo) 
14071  471 
apply (auto intro!: Incr_rel) 
472 
apply (rule_tac j = "tokens(take (length(s`rel), x`rel))" in le_trans) 

473 
apply (rule_tac j = "tokens(take (length(s`rel), s`rel))" in le_trans) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

474 
apply (auto intro!: tokens_mono take_mono simp add: prefix_iff) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

475 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

476 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

477 
(*** Rest of proofs done by lcp ***) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

478 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

479 
(*Second step in proof of (31): by LHS of the guarantee and transivity of 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

480 
LeadsTo *) 
14071  481 
lemma (in alloc_progress) tokens_take_NbR_lemma2: 
482 
"k \<in> tokbag 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

483 
==> alloc_prog \<squnion> G \<in> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

484 
{s\<in>state. tokens(s`giv) = k} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

485 
LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

486 
apply (rule LeadsTo_Trans) 
14071  487 
apply (rule_tac [2] tokens_take_NbR_lemma) 
488 
prefer 2 apply assumption 

489 
apply (insert progress) 

490 
apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

491 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

492 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

493 
(*Third step in proof of (31): by PSP with the fact that giv increases *) 
14071  494 
lemma (in alloc_progress) length_giv_disj: 
495 
"[ k \<in> tokbag; n \<in> nat ] 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

496 
==> alloc_prog \<squnion> G \<in> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

497 
{s\<in>state. length(s`giv) = n & tokens(s`giv) = k} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

498 
LeadsTo 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

499 
{s\<in>state. (length(s`giv) = n & tokens(s`giv) = k & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

500 
k \<le> tokens(take(s`NbR, s`rel)))  n < length(s`giv)}" 
14071  501 
apply (rule single_LeadsTo_I, safe) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

502 
apply (rule_tac a1 = "s`giv" in Increasing_imp_Stable [THEN PSP_StableI]) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

503 
apply (rule alloc_prog_Increasing_giv [THEN guaranteesD]) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

504 
apply (simp_all add: Int_cons_left) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

505 
apply (rule LeadsTo_weaken) 
14071  506 
apply (rule_tac k = "tokens(s`giv)" in tokens_take_NbR_lemma2) 
507 
apply auto 

508 
apply (force dest: prefix_length_le [THEN le_iff [THEN iffD1]]) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

509 
apply (simp add: not_lt_iff_le) 
14071  510 
apply (force dest: prefix_length_le_equal) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

511 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

512 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

513 
(*Fourth step in proof of (31): we apply lemma (51) *) 
14071  514 
lemma (in alloc_progress) length_giv_disj2: 
515 
"[k \<in> tokbag; n \<in> nat] 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

516 
==> alloc_prog \<squnion> G \<in> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

517 
{s\<in>state. length(s`giv) = n & tokens(s`giv) = k} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

518 
LeadsTo 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

519 
{s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok)  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

520 
n < length(s`giv)}" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

521 
apply (rule LeadsTo_weaken_R) 
14071  522 
apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma length_giv_disj], auto) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

523 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

524 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

525 
(*Fifth step in proof of (31): from the fourth step, taking the union over all 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

526 
k\<in>nat *) 
14071  527 
lemma (in alloc_progress) length_giv_disj3: 
528 
"n \<in> nat 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

529 
==> alloc_prog \<squnion> G \<in> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

530 
{s\<in>state. length(s`giv) = n} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

531 
LeadsTo 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

532 
{s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok)  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

533 
n < length(s`giv)}" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

534 
apply (rule LeadsTo_weaken_L) 
14071  535 
apply (rule_tac I = nat in LeadsTo_UN) 
536 
apply (rule_tac k = i in length_giv_disj2) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

537 
apply (simp_all add: UN_conj_eq) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

538 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

539 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

540 
(*Sixth step in proof of (31): from the fifth step, by PSP with the 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

541 
assumption that ask increases *) 
14071  542 
lemma (in alloc_progress) length_ask_giv: 
543 
"[k \<in> nat; n < k] 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

544 
==> alloc_prog \<squnion> G \<in> 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

545 
{s\<in>state. length(s`ask) = k & length(s`giv) = n} 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

546 
LeadsTo 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

547 
{s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) & 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

548 
length(s`giv) = n)  
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

549 
n < length(s`giv)}" 
14071  550 
apply (rule single_LeadsTo_I, safe) 
551 
apply (rule_tac a1 = "s`ask" and f1 = "lift(ask)" 

552 
in Increasing_imp_Stable [THEN PSP_StableI]) 

553 
apply (rule Incr_ask, simp_all) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

554 
apply (rule LeadsTo_weaken) 
14071  555 
apply (rule_tac n = "length(s ` giv)" in length_giv_disj3) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

556 
apply simp_all 
14071  557 
apply blast 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

558 
apply clarify 
14071  559 
apply simp 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

560 
apply (blast dest!: prefix_length_le intro: lt_trans2) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

561 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

562 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

563 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

564 
(*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *) 
14071  565 
lemma (in alloc_progress) length_ask_giv2: 
566 
"[k \<in> nat; n < k] 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

567 
==> alloc_prog \<squnion> G \<in> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

568 
{s\<in>state. length(s`ask) = k & length(s`giv) = n} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

569 
LeadsTo 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

570 
{s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

571 
length(s`giv) < length(s`ask) & length(s`giv) = n)  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

572 
n < length(s`giv)}" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

573 
apply (rule LeadsTo_weaken_R) 
14071  574 
apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify) 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

575 
apply (simp add: INT_iff) 
14071  576 
apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec) 
577 
apply simp 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

578 
apply (blast intro: le_trans) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

579 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

580 

14071  581 
(*Eighth step in proof of (31): by 50, we get giv > n. *) 
582 
lemma (in alloc_progress) extend_giv: 

583 
"[ k \<in> nat; n < k] 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

584 
==> alloc_prog \<squnion> G \<in> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

585 
{s\<in>state. length(s`ask) = k & length(s`giv) = n} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

586 
LeadsTo {s\<in>state. n < length(s`giv)}" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

587 
apply (rule LeadsTo_Un_duplicate) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

588 
apply (rule LeadsTo_cancel1) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

589 
apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma) 
14071  590 
apply (simp_all add: Incr_ask lt_nat_in_nat) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

591 
apply (rule LeadsTo_weaken_R) 
14071  592 
apply (rule length_ask_giv2, auto) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

593 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

594 

14071  595 
(*Ninth and tenth steps in proof of (31): by 50, we get giv > n. 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

596 
The report has an error: putting ask=k for the precondition fails because 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

597 
we can't expect ask to remain fixed until giv increases.*) 
14071  598 
lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv: 
599 
"k \<in> nat 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

600 
==> alloc_prog \<squnion> G \<in> 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

601 
{s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

602 
(* Proof by induction over the difference between k and n *) 
14071  603 
apply (rule_tac f = "\<lambda>s\<in>state. k # length(s`giv)" in LessThan_induct) 
604 
apply (auto simp add: lam_def Collect_vimage_eq) 

605 
apply (rule single_LeadsTo_I, auto) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

606 
apply (rename_tac "s0") 
14071  607 
apply (case_tac "length(s0 ` giv) < length(s0 ` ask) ") 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

608 
apply (rule_tac [2] subset_imp_LeadsTo) 
14071  609 
apply (auto simp add: not_lt_iff_le) 
610 
prefer 2 apply (blast dest: le_imp_not_lt intro: lt_trans2) 

611 
apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)" 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

612 
in Increasing_imp_Stable [THEN PSP_StableI]) 
14071  613 
apply (rule Incr_ask, simp) 
614 
apply (force) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

615 
apply (rule LeadsTo_weaken) 
14071  616 
apply (rule_tac n = "length(s0 ` giv)" and k = "length(s0 ` ask)" 
617 
in extend_giv) 

618 
apply (auto dest: not_lt_imp_le simp add: leI diff_lt_iff_lt) 

619 
apply (blast dest!: prefix_length_le intro: lt_trans2) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

620 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

621 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

622 
(*Final lemma: combine previous result with lemma (30)*) 
14071  623 
lemma (in alloc_progress) final: 
624 
"h \<in> list(tokbag) 

14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

625 
==> alloc_prog \<squnion> G 
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidyup.
paulson
parents:
14071
diff
changeset

626 
\<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26289
diff
changeset

627 
{s\<in>state. <h, s`giv> \<in> prefix(tokbag)}" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

628 
apply (rule single_LeadsTo_I) 
14071  629 
prefer 2 apply simp 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

630 
apply (rename_tac s0) 
14071  631 
apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

632 
in Increasing_imp_Stable [THEN PSP_StableI]) 
14071  633 
apply (rule Incr_ask) 
634 
apply (simp_all add: Int_cons_left) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

635 
apply (rule LeadsTo_weaken) 
14071  636 
apply (rule_tac k1 = "length(s0 ` ask)" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

637 
in Always_LeadsToD [OF alloc_prog_ask_prefix_giv [THEN guaranteesD] 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

638 
alloc_prog_ask_LeadsTo_giv]) 
14071  639 
apply (auto simp add: Incr_ask) 
640 
apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le 

641 
lt_trans2) 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

642 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

643 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

644 
(** alloc_prog liveness property (31), page 18 **) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

645 

14071  646 
theorem alloc_prog_progress: 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

647 
"alloc_prog \<in> 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

648 
Incr(lift(ask)) \<inter> Incr(lift(rel)) \<inter> 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

649 
Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT}) \<inter> 
14071  650 
(\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

651 
{s\<in>state. k \<le> tokens(s`rel)}) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

652 
guarantees (\<Inter>h \<in> list(tokbag). 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

653 
{s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

654 
{s\<in>state. <h, s`giv> \<in> prefix(tokbag)})" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

655 
apply (rule guaranteesI) 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

656 
apply (rule INT_I) 
14071  657 
apply (rule alloc_progress.final) 
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset

658 
apply (auto simp add: alloc_progress_def) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

659 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

660 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff
changeset

661 
end 