author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
11479  1 
(* Title: ZF/UNITY/Guar.thy 
2 
Author: Sidi O Ehmety, Computer Laboratory 

3 
Copyright 2001 University of Cambridge 

4 

5 
Guarantees, etc. 

6 

7 
From Chandy and Sanders, "Reasoning About Program Composition", 

8 
Technical Report 2000003, University of Florida, 2000. 

9 

10 
Revised by Sidi Ehmety on January 2001 

11 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

12 
Added \<in> Compatibility, weakest guarantees, etc. 
11479  13 

14 
and Weakest existential property, 

15 
from Charpentier and Chandy "Theorems about Composition", 

16 
Fifth International Conference on Mathematics of Program, 2000. 

17 

18 
Theory ported from HOL. 

19 
*) 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

20 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

21 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

22 
header{*The ChandySanders Guarantees Operator*} 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

23 

16417  24 
theory Guar imports Comp begin 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

25 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

26 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

27 
(* To be moved to theory WFair???? *) 
46823  28 
lemma leadsTo_Basis': "[ F \<in> A co A \<union> B; F \<in> transient(A); st_set(B) ] ==> F \<in> A leadsTo B" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

29 
apply (frule constrainsD2) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

30 
apply (drule_tac B = "AB" in constrains_weaken_L, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

31 
apply (drule_tac B = "AB" in transient_strengthen, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

32 
apply (blast intro: ensuresI [THEN leadsTo_Basis]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

33 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

34 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

35 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

36 
(*Existential and Universal properties. We formalize the twoprogram 
11479  37 
case, proving equivalence with Chandy and Sanders's nary definitions*) 
38 

24893  39 
definition 
40 
ex_prop :: "i => o" where 

12195  41 
"ex_prop(X) == X<=program & 
46823  42 
(\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X  G \<in> X \<longrightarrow> (F Join G) \<in> X)" 
11479  43 

24893  44 
definition 
45 
strict_ex_prop :: "i => o" where 

12195  46 
"strict_ex_prop(X) == X<=program & 
46823  47 
(\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<in> X  G \<in> X) \<longleftrightarrow> (F Join G \<in> X))" 
11479  48 

24893  49 
definition 
50 
uv_prop :: "i => o" where 

12195  51 
"uv_prop(X) == X<=program & 
46823  52 
(SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X & G \<in> X \<longrightarrow> (F Join G) \<in> X))" 
11479  53 

24893  54 
definition 
55 
strict_uv_prop :: "i => o" where 

12195  56 
"strict_uv_prop(X) == X<=program & 
46823  57 
(SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X & G \<in> X) \<longleftrightarrow> (F Join G \<in> X)))" 
11479  58 

24893  59 
definition 
60 
guar :: "[i, i] => i" (infixl "guarantees" 55) where 

11479  61 
(*higher than membership, lower than Co*) 
46823  62 
"X guarantees Y == {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F Join G \<in> X \<longrightarrow> F Join G \<in> Y}" 
11479  63 

24893  64 
definition 
11479  65 
(* Weakest guarantees *) 
24893  66 
wg :: "[i,i] => i" where 
46823  67 
"wg(F,Y) == \<Union>({X \<in> Pow(program). F:(X guarantees Y)})" 
11479  68 

24893  69 
definition 
11479  70 
(* Weakest existential property stronger than X *) 
24893  71 
wx :: "i =>i" where 
46823  72 
"wx(X) == \<Union>({Y \<in> Pow(program). Y<=X & ex_prop(Y)})" 
11479  73 

24893  74 
definition 
11479  75 
(*Illdefined programs can arise through "Join"*) 
24893  76 
welldef :: i where 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

77 
"welldef == {F \<in> program. Init(F) \<noteq> 0}" 
11479  78 

24893  79 
definition 
80 
refines :: "[i, i, i] => o" ("(3_ refines _ wrt _)" [10,10,10] 10) where 

11479  81 
"G refines F wrt X == 
46823  82 
\<forall>H \<in> program. (F ok H & G ok H & F Join H \<in> welldef \<inter> X) 
83 
\<longrightarrow> (G Join H \<in> welldef \<inter> X)" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

84 

24893  85 
definition 
86 
iso_refines :: "[i,i, i] => o" ("(3_ iso'_refines _ wrt _)" [10,10,10] 10) where 

46823  87 
"G iso_refines F wrt X == F \<in> welldef \<inter> X \<longrightarrow> G \<in> welldef \<inter> X" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

88 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

89 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

90 
(*** existential properties ***) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

91 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

92 
lemma ex_imp_subset_program: "ex_prop(X) ==> X\<subseteq>program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

93 
by (simp add: ex_prop_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

94 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

95 
lemma ex1 [rule_format]: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

96 
"GG \<in> Fin(program) 
46823  97 
==> ex_prop(X) \<longrightarrow> GG \<inter> X\<noteq>0 \<longrightarrow> OK(GG, (%G. G)) \<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

98 
apply (unfold ex_prop_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

99 
apply (erule Fin_induct) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

100 
apply (simp_all add: OK_cons_iff) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

101 
apply (safe elim!: not_emptyE, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

102 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

103 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

104 
lemma ex2 [rule_format]: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

105 
"X \<subseteq> program ==> 
46823  106 
(\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 \<longrightarrow> OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X) 
107 
\<longrightarrow> ex_prop(X)" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

108 
apply (unfold ex_prop_def, clarify) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

109 
apply (drule_tac x = "{F,G}" in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

110 
apply (simp_all add: OK_iff_ok) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

111 
apply (auto intro: ok_sym) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

112 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

113 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

114 
(*Chandy & Sanders take this as a definition*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

115 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

116 
lemma ex_prop_finite: 
46823  117 
"ex_prop(X) \<longleftrightarrow> (X\<subseteq>program & 
118 
(\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 & OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X))" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

119 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

120 
apply (blast intro: ex1 ex2 dest: ex_imp_subset_program)+ 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

121 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

122 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

123 
(* Equivalent definition of ex_prop given at the end of section 3*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

124 
lemma ex_prop_equiv: 
46823  125 
"ex_prop(X) \<longleftrightarrow> 
126 
X\<subseteq>program & (\<forall>G \<in> program. (G \<in> X \<longleftrightarrow> (\<forall>H \<in> program. (G component_of H) \<longrightarrow> H \<in> X)))" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

127 
apply (unfold ex_prop_def component_of_def, safe, force, force, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

128 
apply (subst Join_commute) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

129 
apply (blast intro: ok_sym) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

130 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

131 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

132 
(*** universal properties ***) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

133 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

134 
lemma uv_imp_subset_program: "uv_prop(X)==> X\<subseteq>program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

135 
apply (unfold uv_prop_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

136 
apply (simp (no_asm_simp)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

137 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

138 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

139 
lemma uv1 [rule_format]: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

140 
"GG \<in> Fin(program) ==> 
46823  141 
(uv_prop(X)\<longrightarrow> GG \<subseteq> X & OK(GG, (%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

142 
apply (unfold uv_prop_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

143 
apply (erule Fin_induct) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

144 
apply (auto simp add: OK_cons_iff) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

145 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

146 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

147 
lemma uv2 [rule_format]: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

148 
"X\<subseteq>program ==> 
46823  149 
(\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG,(%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X) 
150 
\<longrightarrow> uv_prop(X)" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

151 
apply (unfold uv_prop_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

152 
apply (drule_tac x = 0 in bspec, simp+) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

153 
apply (drule_tac x = "{F,G}" in bspec, simp) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

154 
apply (force dest: ok_sym simp add: OK_iff_ok) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

155 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

156 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

157 
(*Chandy & Sanders take this as a definition*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

158 
lemma uv_prop_finite: 
46823  159 
"uv_prop(X) \<longleftrightarrow> X\<subseteq>program & 
160 
(\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG, %G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

161 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

162 
apply (blast dest: uv_imp_subset_program) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

163 
apply (blast intro: uv1) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

164 
apply (blast intro!: uv2 dest:) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

165 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

166 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

167 
(*** guarantees ***) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

168 
lemma guaranteesI: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

169 
"[ (!!G. [ F ok G; F Join G \<in> X; G \<in> program ] ==> F Join G \<in> Y); 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

170 
F \<in> program ] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

171 
==> F \<in> X guarantees Y" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

172 
by (simp add: guar_def component_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

173 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

174 
lemma guaranteesD: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

175 
"[ F \<in> X guarantees Y; F ok G; F Join G \<in> X; G \<in> program ] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

176 
==> F Join G \<in> Y" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

177 
by (simp add: guar_def component_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

178 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

179 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

180 
(*This version of guaranteesD matches more easily in the conclusion 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

181 
The major premise can no longer be F\<subseteq>H since we need to reason about G*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

182 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

183 
lemma component_guaranteesD: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

184 
"[ F \<in> X guarantees Y; F Join G = H; H \<in> X; F ok G; G \<in> program ] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

185 
==> H \<in> Y" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

186 
by (simp add: guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

187 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

188 
lemma guarantees_weaken: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

189 
"[ F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' ] ==> F \<in> Y guarantees Y'" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

190 
by (simp add: guar_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

191 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

192 
lemma subset_imp_guarantees_program: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

193 
"X \<subseteq> Y ==> X guarantees Y = program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

194 
by (unfold guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

195 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

196 
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

197 
lemma subset_imp_guarantees: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

198 
"[ X \<subseteq> Y; F \<in> program ] ==> F \<in> X guarantees Y" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

199 
by (unfold guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

200 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

201 
lemma component_of_Join1: "F ok G ==> F component_of (F Join G)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

202 
by (unfold component_of_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

203 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

204 
lemma component_of_Join2: "F ok G ==> G component_of (F Join G)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

205 
apply (subst Join_commute) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

206 
apply (blast intro: ok_sym component_of_Join1) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

207 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

208 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

209 
(*Remark at end of section 4.1 *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

210 
lemma ex_prop_imp: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

211 
"ex_prop(Y) ==> (Y = (program guarantees Y))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

212 
apply (simp (no_asm_use) add: ex_prop_equiv guar_def component_of_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

213 
apply clarify 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

214 
apply (rule equalityI, blast, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

215 
apply (drule_tac x = x in bspec, assumption, force) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

216 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

217 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

218 
lemma guarantees_imp: "(Y = program guarantees Y) ==> ex_prop(Y)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

219 
apply (unfold guar_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

220 
apply (simp (no_asm_simp) add: ex_prop_equiv) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

221 
apply safe 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

222 
apply (blast intro: elim: equalityE) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

223 
apply (simp_all (no_asm_use) add: component_of_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

224 
apply (force elim: equalityE)+ 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

225 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

226 

46823  227 
lemma ex_prop_equiv2: "(ex_prop(Y)) \<longleftrightarrow> (Y = program guarantees Y)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

228 
by (blast intro: ex_prop_imp guarantees_imp) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

229 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

230 
(** Distributive laws. Reorient to perform miniscoping **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

231 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

232 
lemma guarantees_UN_left: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

233 
"i \<in> I ==>(\<Union>i \<in> I. X(i)) guarantees Y = (\<Inter>i \<in> I. X(i) guarantees Y)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

234 
apply (unfold guar_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

235 
apply (rule equalityI, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

236 
prefer 2 apply force 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

237 
apply blast+ 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

238 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

239 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

240 
lemma guarantees_Un_left: 
46823  241 
"(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

242 
apply (unfold guar_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

243 
apply (rule equalityI, safe, blast+) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

244 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

245 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

246 
lemma guarantees_INT_right: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

247 
"i \<in> I ==> X guarantees (\<Inter>i \<in> I. Y(i)) = (\<Inter>i \<in> I. X guarantees Y(i))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

248 
apply (unfold guar_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

249 
apply (rule equalityI, safe, blast+) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

250 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

251 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

252 
lemma guarantees_Int_right: 
46823  253 
"Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

254 
by (unfold guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

255 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

256 
lemma guarantees_Int_right_I: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

257 
"[ F \<in> Z guarantees X; F \<in> Z guarantees Y ] 
46823  258 
==> F \<in> Z guarantees (X \<inter> Y)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

259 
by (simp (no_asm_simp) add: guarantees_Int_right) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

260 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

261 
lemma guarantees_INT_right_iff: 
46823  262 
"i \<in> I==> (F \<in> X guarantees (\<Inter>i \<in> I. Y(i))) \<longleftrightarrow> 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

263 
(\<forall>i \<in> I. F \<in> X guarantees Y(i))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

264 
by (simp add: guarantees_INT_right INT_iff, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

265 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

266 

46823  267 
lemma shunting: "(X guarantees Y) = (program guarantees ((programX) \<union> Y))" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

268 
by (unfold guar_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

269 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

270 
lemma contrapositive: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

271 
"(X guarantees Y) = (program  Y) guarantees (program X)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

272 
by (unfold guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

273 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

274 
(** The following two can be expressed using intersection and subset, which 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

275 
is more faithful to the text but looks cryptic. 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

276 
**) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

277 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

278 
lemma combining1: 
46823  279 
"[ F \<in> V guarantees X; F \<in> (X \<inter> Y) guarantees Z ] 
280 
==> F \<in> (V \<inter> Y) guarantees Z" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

281 
by (unfold guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

282 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

283 
lemma combining2: 
46823  284 
"[ F \<in> V guarantees (X \<union> Y); F \<in> Y guarantees Z ] 
285 
==> F \<in> V guarantees (X \<union> Z)" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

286 
by (unfold guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

287 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

288 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

289 
(** The following two follow ChandySanders, but the use of objectquantifiers 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

290 
does not suit Isabelle... **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

291 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

292 
(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

293 
lemma all_guarantees: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

294 
"[ \<forall>i \<in> I. F \<in> X guarantees Y(i); i \<in> I ] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

295 
==> F \<in> X guarantees (\<Inter>i \<in> I. Y(i))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

296 
by (unfold guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

297 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

298 
(*Premises should be [ F \<in> X guarantees Y i; i \<in> I ] *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

299 
lemma ex_guarantees: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

300 
"\<exists>i \<in> I. F \<in> X guarantees Y(i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y(i))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

301 
by (unfold guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

302 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

303 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

304 
(*** Additional guarantees laws, by lcp ***) 
11479  305 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

306 
lemma guarantees_Join_Int: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

307 
"[ F \<in> U guarantees V; G \<in> X guarantees Y; F ok G ] 
46823  308 
==> F Join G: (U \<inter> X) guarantees (V \<inter> Y)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

309 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

310 
apply (unfold guar_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

311 
apply (simp (no_asm)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

312 
apply safe 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

313 
apply (simp add: Join_assoc) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

314 
apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

315 
apply (simp add: ok_commute) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

316 
apply (simp (no_asm_simp) add: Join_ac) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

317 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

318 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

319 
lemma guarantees_Join_Un: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

320 
"[ F \<in> U guarantees V; G \<in> X guarantees Y; F ok G ] 
46823  321 
==> F Join G: (U \<union> X) guarantees (V \<union> Y)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

322 
apply (unfold guar_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

323 
apply (simp (no_asm)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

324 
apply safe 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

325 
apply (simp add: Join_assoc) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

326 
apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

327 
apply (rotate_tac 4) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

328 
apply (drule_tac x = "F Join Ga" in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

329 
apply (simp (no_asm)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

330 
apply (force simp add: ok_commute) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

331 
apply (simp (no_asm_simp) add: Join_ac) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

332 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

333 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

334 
lemma guarantees_JN_INT: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

335 
"[ \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i); OK(I,F); i \<in> I ] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

336 
==> (\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. X(i)) guarantees (\<Inter>i \<in> I. Y(i))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

337 
apply (unfold guar_def, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

338 
prefer 2 apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

339 
apply (drule_tac x = xa in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

340 
apply (simp_all add: INT_iff, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

341 
apply (drule_tac x = "(\<Squnion>x \<in> (I{xa}) . F (x)) Join G" and A=program in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

342 
apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

343 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

344 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

345 
lemma guarantees_JN_UN: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

346 
"[ \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i); OK(I,F) ] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

347 
==> JOIN(I,F) \<in> (\<Union>i \<in> I. X(i)) guarantees (\<Union>i \<in> I. Y(i))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

348 
apply (unfold guar_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

349 
apply (drule_tac x = y in bspec, simp_all, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

350 
apply (rename_tac G y) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

351 
apply (drule_tac x = "JOIN (I{y}, F) Join G" and A=program in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

352 
apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

353 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

354 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

355 
(*** guarantees laws for breaking down the program, by lcp ***) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

356 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

357 
lemma guarantees_Join_I1: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

358 
"[ F \<in> X guarantees Y; F ok G ] ==> F Join G \<in> X guarantees Y" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

359 
apply (simp add: guar_def, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

360 
apply (simp add: Join_assoc) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

361 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

362 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

363 
lemma guarantees_Join_I2: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

364 
"[ G \<in> X guarantees Y; F ok G ] ==> F Join G \<in> X guarantees Y" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

365 
apply (simp add: Join_commute [of _ G] ok_commute [of _ G]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

366 
apply (blast intro: guarantees_Join_I1) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

367 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

368 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

369 
lemma guarantees_JN_I: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

370 
"[ i \<in> I; F(i) \<in> X guarantees Y; OK(I,F) ] 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

371 
==> (\<Squnion>i \<in> I. F(i)) \<in> X guarantees Y" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

372 
apply (unfold guar_def, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

373 
apply (drule_tac x = "JOIN (I{i},F) Join G" in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

374 
apply (simp (no_asm)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

375 
apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

376 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

377 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

378 
(*** welldefinedness ***) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

379 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

380 
lemma Join_welldef_D1: "F Join G \<in> welldef ==> programify(F) \<in> welldef" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

381 
by (unfold welldef_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

382 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

383 
lemma Join_welldef_D2: "F Join G \<in> welldef ==> programify(G) \<in> welldef" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

384 
by (unfold welldef_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

385 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

386 
(*** refinement ***) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

387 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

388 
lemma refines_refl: "F refines F wrt X" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

389 
by (unfold refines_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

390 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

391 
(* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

392 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

393 
lemma wg_type: "wg(F, X) \<subseteq> program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

394 
by (unfold wg_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

395 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

396 
lemma guarantees_type: "X guarantees Y \<subseteq> program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

397 
by (unfold guar_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

398 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

399 
lemma wgD2: "G \<in> wg(F, X) ==> G \<in> program & F \<in> program" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

400 
apply (unfold wg_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

401 
apply (blast dest: guarantees_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

402 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

403 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

404 
lemma guarantees_equiv: 
46823  405 
"(F \<in> X guarantees Y) \<longleftrightarrow> 
406 
F \<in> program & (\<forall>H \<in> program. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

407 
by (unfold guar_def component_of_def, force) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

408 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

409 
lemma wg_weakest: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

410 
"!!X. [ F \<in> (X guarantees Y); X \<subseteq> program ] ==> X \<subseteq> wg(F,Y)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

411 
by (unfold wg_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

412 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

413 
lemma wg_guarantees: "F \<in> program ==> F \<in> wg(F,Y) guarantees Y" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

414 
by (unfold wg_def guar_def, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

415 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

416 
lemma wg_equiv: 
46823  417 
"H \<in> wg(F,X) \<longleftrightarrow> 
418 
((F component_of H \<longrightarrow> H \<in> X) & F \<in> program & H \<in> program)" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

419 
apply (simp add: wg_def guarantees_equiv) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

420 
apply (rule iffI, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

421 
apply (rule_tac [4] x = "{H}" in bexI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

422 
apply (rule_tac [3] x = "{H}" in bexI, blast+) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

423 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

424 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

425 
lemma component_of_wg: 
46823  426 
"F component_of H ==> H \<in> wg(F,X) \<longleftrightarrow> (H \<in> X & F \<in> program & H \<in> program)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

427 
by (simp (no_asm_simp) add: wg_equiv) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

428 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

429 
lemma wg_finite [rule_format]: 
46823  430 
"\<forall>FF \<in> Fin(program). FF \<inter> X \<noteq> 0 \<longrightarrow> OK(FF, %F. F) 
431 
\<longrightarrow> (\<forall>F \<in> FF. ((\<Squnion>F \<in> FF. F) \<in> wg(F,X)) \<longleftrightarrow> ((\<Squnion>F \<in> FF. F) \<in> X))" 

14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

432 
apply clarify 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

433 
apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

434 
apply (drule_tac X = X in component_of_wg) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

435 
apply (force dest!: Fin.dom_subset [THEN subsetD, THEN PowD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

436 
apply (simp_all add: component_of_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

437 
apply (rule_tac x = "\<Squnion>F \<in> (FF{F}) . F" in exI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

438 
apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

439 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

440 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

441 
lemma wg_ex_prop: 
46823  442 
"ex_prop(X) ==> (F \<in> X) \<longleftrightarrow> (\<forall>H \<in> program. H \<in> wg(F,X) & F \<in> program)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

443 
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

444 
apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

445 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

446 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

447 
(** From Charpentier and Chandy "Theorems About Composition" **) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

448 
(* Proposition 2 *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

449 
lemma wx_subset: "wx(X)\<subseteq>X" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

450 
by (unfold wx_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

451 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

452 
lemma wx_ex_prop: "ex_prop(wx(X))" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

453 
apply (simp (no_asm_use) add: ex_prop_def wx_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

454 
apply safe 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

455 
apply blast 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

456 
apply (rule_tac x=x in bexI, force, simp)+ 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

457 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

458 

46823  459 
lemma wx_weakest: "\<forall>Z. Z\<subseteq>program \<longrightarrow> Z\<subseteq> X \<longrightarrow> ex_prop(Z) \<longrightarrow> Z \<subseteq> wx(X)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

460 
by (unfold wx_def, auto) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

461 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

462 
(* Proposition 6 *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

463 
lemma wx'_ex_prop: 
46823  464 
"ex_prop({F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F Join G \<in> X})" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

465 
apply (unfold ex_prop_def, safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

466 
apply (drule_tac x = "G Join Ga" in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

467 
apply (simp (no_asm)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

468 
apply (force simp add: Join_assoc) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

469 
apply (drule_tac x = "F Join Ga" in bspec) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

470 
apply (simp (no_asm)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

471 
apply (simp (no_asm_use)) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

472 
apply safe 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

473 
apply (simp (no_asm_simp) add: ok_commute) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

474 
apply (subgoal_tac "F Join G = G Join F") 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

475 
apply (simp (no_asm_simp) add: Join_assoc) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

476 
apply (simp (no_asm) add: Join_commute) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

477 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

478 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

479 
(* Equivalence with the other definition of wx *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

480 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

481 
lemma wx_equiv: 
46823  482 
"wx(X) = {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F Join G) \<in> X}" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

483 
apply (unfold wx_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

484 
apply (rule equalityI, safe, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

485 
apply (simp (no_asm_use) add: ex_prop_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

486 
apply blast 
46823  487 
apply (rule_tac B = "{F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F Join G \<in> X}" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

488 
in UnionI, 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

489 
safe) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

490 
apply (rule_tac [2] wx'_ex_prop) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

491 
apply (drule_tac x=SKIP in bspec, simp)+ 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

492 
apply auto 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

493 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

494 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

495 
(* Propositions 7 to 11 are all about this second definition of wx. And 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

496 
by equivalence between the two definition, they are the same as the ones proved *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

497 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

498 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

499 
(* Proposition 12 *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

500 
(* Main result of the paper *) 
46823  501 
lemma guarantees_wx_eq: "(X guarantees Y) = wx((programX) \<union> Y)" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

502 
by (auto simp add: guar_def wx_equiv) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

503 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

504 
(* 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

505 
{* Corollary, but this result has already been proved elsewhere *} 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

506 
"ex_prop(X guarantees Y)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

507 
*) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

508 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

509 
(* Rules given in section 7 of Chandy and Sander's 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

510 
Reasoning About Program composition paper *) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

511 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

512 
lemma stable_guarantees_Always: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

513 
"[ Init(F) \<subseteq> A; F \<in> program ] ==> F \<in> stable(A) guarantees Always(A)" 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

514 
apply (rule guaranteesI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

515 
prefer 2 apply assumption 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

516 
apply (simp (no_asm) add: Join_commute) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

517 
apply (rule stable_Join_Always1) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

518 
apply (simp_all add: invariant_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

519 
apply (auto simp add: programify_def initially_def) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

520 
done 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

521 

24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

522 
lemma constrains_guarantees_leadsTo: 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

523 
"[ F \<in> transient(A); st_set(B) ] 
46823  524 
==> F: (A co A \<union> B) guarantees (A leadsTo (BA))" 
14093
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

525 
apply (rule guaranteesI) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

526 
prefer 2 apply (blast dest: transient_type [THEN subsetD]) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

527 
apply (rule leadsTo_Basis') 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

528 
apply (blast intro: constrains_weaken_R) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

529 
apply (blast intro!: Join_transient_I1, blast) 
24382760fd89
converting more theories to Isar scripts, and tidying
paulson
parents:
12195
diff
changeset

530 
done 
11479  531 

532 
end 