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/UNITY.thy 
2 
Author: Sidi O Ehmety, Computer Laboratory 

3 
Copyright 2001 University of Cambridge 

4 
*) 

5 

14077  6 
header {*The Basic UNITY Theory*} 
7 

16417  8 
theory UNITY imports State begin 
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

9 

052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

10 
text{*The basic UNITY theory (revised version, based upon the "co" operator) 
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

11 
From Misra, "A Logic for Concurrent Programming", 1994. 
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

12 

052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

13 
This ZF theory was ported from its HOL equivalent.*} 
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

14 

11479  15 
consts 
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

16 
"constrains" :: "[i, i] => i" (infixl "co" 60) 
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

17 
op_unless :: "[i, i] => i" (infixl "unless" 60) 
11479  18 

24893  19 
definition 
20 
program :: i where 

12195  21 
"program == {<init, acts, allowed>: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

22 
Pow(state) * Pow(Pow(state*state)) * Pow(Pow(state*state)). 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

23 
id(state) \<in> acts & id(state) \<in> allowed}" 
11479  24 

24893  25 
definition 
26 
mk_program :: "[i,i,i]=>i" where 

14077  27 
{* The definition yields a program thanks to the coercions 
28 
init \<inter> state, acts \<inter> Pow(state*state), etc. *} 

11479  29 
"mk_program(init, acts, allowed) == 
14077  30 
<init \<inter> state, cons(id(state), acts \<inter> Pow(state*state)), 
31 
cons(id(state), allowed \<inter> Pow(state*state))>" 

11479  32 

24893  33 
definition 
34 
SKIP :: i where 

12195  35 
"SKIP == mk_program(state, 0, Pow(state*state))" 
11479  36 

12195  37 
(* Coercion from anything to program *) 
24893  38 
definition 
39 
programify :: "i=>i" where 

14077  40 
"programify(F) == if F \<in> program then F else SKIP" 
12195  41 

24893  42 
definition 
43 
RawInit :: "i=>i" where 

11479  44 
"RawInit(F) == fst(F)" 
14077  45 

24893  46 
definition 
47 
Init :: "i=>i" where 

11479  48 
"Init(F) == RawInit(programify(F))" 
49 

24893  50 
definition 
51 
RawActs :: "i=>i" where 

12195  52 
"RawActs(F) == cons(id(state), fst(snd(F)))" 
11479  53 

24893  54 
definition 
55 
Acts :: "i=>i" where 

11479  56 
"Acts(F) == RawActs(programify(F))" 
57 

24893  58 
definition 
59 
RawAllowedActs :: "i=>i" where 

12195  60 
"RawAllowedActs(F) == cons(id(state), snd(snd(F)))" 
11479  61 

24893  62 
definition 
63 
AllowedActs :: "i=>i" where 

11479  64 
"AllowedActs(F) == RawAllowedActs(programify(F))" 
65 

14077  66 

24893  67 
definition 
68 
Allowed :: "i =>i" where 

14077  69 
"Allowed(F) == {G \<in> program. Acts(G) \<subseteq> AllowedActs(F)}" 
11479  70 

24893  71 
definition 
72 
initially :: "i=>i" where 

14077  73 
"initially(A) == {F \<in> program. Init(F)\<subseteq>A}" 
74 

24893  75 
definition 
76 
stable :: "i=>i" where 

11479  77 
"stable(A) == A co A" 
78 

24893  79 
definition 
80 
strongest_rhs :: "[i, i] => i" where 

46823  81 
"strongest_rhs(F, A) == \<Inter>({B \<in> Pow(state). F \<in> A co B})" 
11479  82 

24893  83 
definition 
84 
invariant :: "i => i" where 

14077  85 
"invariant(A) == initially(A) \<inter> stable(A)" 
86 

14046  87 
(* metafunction composition *) 
24893  88 
definition 
89 
metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl "comp" 65) where 

14046  90 
"f comp g == %x. f(g(x))" 
11479  91 

24893  92 
definition 
93 
pg_compl :: "i=>i" where 

14046  94 
"pg_compl(X)== program  X" 
14077  95 

11479  96 
defs 
14077  97 
constrains_def: 
98 
"A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}" 

99 
{* the condition @{term "st_set(A)"} makes the definition slightly 

100 
stronger than the HOL one *} 

101 

46823  102 
unless_def: "A unless B == (A  B) co (A \<union> B)" 
14077  103 

104 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

105 
text{*SKIP*} 
14077  106 
lemma SKIP_in_program [iff,TC]: "SKIP \<in> program" 
107 
by (force simp add: SKIP_def program_def mk_program_def) 

108 

109 

110 
subsection{*The function @{term programify}, the coercion from anything to 

111 
program*} 

112 

113 
lemma programify_program [simp]: "F \<in> program ==> programify(F)=F" 

114 
by (force simp add: programify_def) 

115 

116 
lemma programify_in_program [iff,TC]: "programify(F) \<in> program" 

117 
by (force simp add: programify_def) 

118 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

119 
text{*Collapsing rules: to remove programify from expressions*} 
14077  120 
lemma programify_idem [simp]: "programify(programify(F))=programify(F)" 
121 
by (force simp add: programify_def) 

122 

123 
lemma Init_programify [simp]: "Init(programify(F)) = Init(F)" 

124 
by (simp add: Init_def) 

125 

126 
lemma Acts_programify [simp]: "Acts(programify(F)) = Acts(F)" 

127 
by (simp add: Acts_def) 

128 

129 
lemma AllowedActs_programify [simp]: 

130 
"AllowedActs(programify(F)) = AllowedActs(F)" 

131 
by (simp add: AllowedActs_def) 

132 

133 
subsection{*The Inspectors for Programs*} 

134 

135 
lemma id_in_RawActs: "F \<in> program ==>id(state) \<in> RawActs(F)" 

136 
by (auto simp add: program_def RawActs_def) 

137 

138 
lemma id_in_Acts [iff,TC]: "id(state) \<in> Acts(F)" 

139 
by (simp add: id_in_RawActs Acts_def) 

140 

141 
lemma id_in_RawAllowedActs: "F \<in> program ==>id(state) \<in> RawAllowedActs(F)" 

142 
by (auto simp add: program_def RawAllowedActs_def) 

143 

144 
lemma id_in_AllowedActs [iff,TC]: "id(state) \<in> AllowedActs(F)" 

145 
by (simp add: id_in_RawAllowedActs AllowedActs_def) 

146 

147 
lemma cons_id_Acts [simp]: "cons(id(state), Acts(F)) = Acts(F)" 

148 
by (simp add: cons_absorb) 

149 

150 
lemma cons_id_AllowedActs [simp]: 

151 
"cons(id(state), AllowedActs(F)) = AllowedActs(F)" 

152 
by (simp add: cons_absorb) 

153 

154 

155 
subsection{*Types of the Inspectors*} 

156 

157 
lemma RawInit_type: "F \<in> program ==> RawInit(F)\<subseteq>state" 

158 
by (auto simp add: program_def RawInit_def) 

159 

160 
lemma RawActs_type: "F \<in> program ==> RawActs(F)\<subseteq>Pow(state*state)" 

161 
by (auto simp add: program_def RawActs_def) 

162 

163 
lemma RawAllowedActs_type: 

164 
"F \<in> program ==> RawAllowedActs(F)\<subseteq>Pow(state*state)" 

165 
by (auto simp add: program_def RawAllowedActs_def) 

166 

167 
lemma Init_type: "Init(F)\<subseteq>state" 

168 
by (simp add: RawInit_type Init_def) 

169 

45602  170 
lemmas InitD = Init_type [THEN subsetD] 
14077  171 

172 
lemma st_set_Init [iff]: "st_set(Init(F))" 

173 
apply (unfold st_set_def) 

174 
apply (rule Init_type) 

175 
done 

176 

177 
lemma Acts_type: "Acts(F)\<subseteq>Pow(state*state)" 

178 
by (simp add: RawActs_type Acts_def) 

179 

180 
lemma AllowedActs_type: "AllowedActs(F) \<subseteq> Pow(state*state)" 

181 
by (simp add: RawAllowedActs_type AllowedActs_def) 

182 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

183 
text{*Needed in Behaviors*} 
14077  184 
lemma ActsD: "[ act \<in> Acts(F); <s,s'> \<in> act ] ==> s \<in> state & s' \<in> state" 
185 
by (blast dest: Acts_type [THEN subsetD]) 

186 

187 
lemma AllowedActsD: 

188 
"[ act \<in> AllowedActs(F); <s,s'> \<in> act ] ==> s \<in> state & s' \<in> state" 

189 
by (blast dest: AllowedActs_type [THEN subsetD]) 

190 

191 
subsection{*Simplification rules involving @{term state}, @{term Init}, 

192 
@{term Acts}, and @{term AllowedActs}*} 

193 

194 
text{*But are they really needed?*} 

195 

46823  196 
lemma state_subset_is_Init_iff [iff]: "state \<subseteq> Init(F) \<longleftrightarrow> Init(F)=state" 
14077  197 
by (cut_tac F = F in Init_type, auto) 
198 

199 
lemma Pow_state_times_state_is_subset_Acts_iff [iff]: 

46823  200 
"Pow(state*state) \<subseteq> Acts(F) \<longleftrightarrow> Acts(F)=Pow(state*state)" 
14077  201 
by (cut_tac F = F in Acts_type, auto) 
202 

203 
lemma Pow_state_times_state_is_subset_AllowedActs_iff [iff]: 

46823  204 
"Pow(state*state) \<subseteq> AllowedActs(F) \<longleftrightarrow> AllowedActs(F)=Pow(state*state)" 
14077  205 
by (cut_tac F = F in AllowedActs_type, auto) 
206 

207 
subsubsection{*Eliminating @{text "\<inter> state"} from expressions*} 

208 

209 
lemma Init_Int_state [simp]: "Init(F) \<inter> state = Init(F)" 

210 
by (cut_tac F = F in Init_type, blast) 

211 

212 
lemma state_Int_Init [simp]: "state \<inter> Init(F) = Init(F)" 

213 
by (cut_tac F = F in Init_type, blast) 

214 

215 
lemma Acts_Int_Pow_state_times_state [simp]: 

216 
"Acts(F) \<inter> Pow(state*state) = Acts(F)" 

217 
by (cut_tac F = F in Acts_type, blast) 

218 

219 
lemma state_times_state_Int_Acts [simp]: 

220 
"Pow(state*state) \<inter> Acts(F) = Acts(F)" 

221 
by (cut_tac F = F in Acts_type, blast) 

222 

223 
lemma AllowedActs_Int_Pow_state_times_state [simp]: 

224 
"AllowedActs(F) \<inter> Pow(state*state) = AllowedActs(F)" 

225 
by (cut_tac F = F in AllowedActs_type, blast) 

226 

227 
lemma state_times_state_Int_AllowedActs [simp]: 

228 
"Pow(state*state) \<inter> AllowedActs(F) = AllowedActs(F)" 

229 
by (cut_tac F = F in AllowedActs_type, blast) 

230 

231 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

232 
subsubsection{*The Operator @{term mk_program}*} 
14077  233 

234 
lemma mk_program_in_program [iff,TC]: 

235 
"mk_program(init, acts, allowed) \<in> program" 

236 
by (auto simp add: mk_program_def program_def) 

237 

238 
lemma RawInit_eq [simp]: 

239 
"RawInit(mk_program(init, acts, allowed)) = init \<inter> state" 

240 
by (auto simp add: mk_program_def RawInit_def) 

241 

242 
lemma RawActs_eq [simp]: 

243 
"RawActs(mk_program(init, acts, allowed)) = 

244 
cons(id(state), acts \<inter> Pow(state*state))" 

245 
by (auto simp add: mk_program_def RawActs_def) 

246 

247 
lemma RawAllowedActs_eq [simp]: 

248 
"RawAllowedActs(mk_program(init, acts, allowed)) = 

249 
cons(id(state), allowed \<inter> Pow(state*state))" 

250 
by (auto simp add: mk_program_def RawAllowedActs_def) 

251 

252 
lemma Init_eq [simp]: "Init(mk_program(init, acts, allowed)) = init \<inter> state" 

253 
by (simp add: Init_def) 

254 

255 
lemma Acts_eq [simp]: 

256 
"Acts(mk_program(init, acts, allowed)) = 

257 
cons(id(state), acts \<inter> Pow(state*state))" 

258 
by (simp add: Acts_def) 

259 

260 
lemma AllowedActs_eq [simp]: 

261 
"AllowedActs(mk_program(init, acts, allowed))= 

262 
cons(id(state), allowed \<inter> Pow(state*state))" 

263 
by (simp add: AllowedActs_def) 

264 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

265 
text{*Init, Acts, and AlowedActs of SKIP *} 
14077  266 

267 
lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state" 

268 
by (simp add: SKIP_def) 

269 

270 
lemma RawAllowedActs_SKIP [simp]: "RawAllowedActs(SKIP) = Pow(state*state)" 

271 
by (force simp add: SKIP_def) 

272 

273 
lemma RawActs_SKIP [simp]: "RawActs(SKIP) = {id(state)}" 

274 
by (force simp add: SKIP_def) 

275 

276 
lemma Init_SKIP [simp]: "Init(SKIP) = state" 

277 
by (force simp add: SKIP_def) 

278 

279 
lemma Acts_SKIP [simp]: "Acts(SKIP) = {id(state)}" 

280 
by (force simp add: SKIP_def) 

281 

282 
lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)" 

283 
by (force simp add: SKIP_def) 

284 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

285 
text{*Equality of UNITY programs*} 
14077  286 

287 
lemma raw_surjective_mk_program: 

288 
"F \<in> program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F" 

289 
apply (auto simp add: program_def mk_program_def RawInit_def RawActs_def 

290 
RawAllowedActs_def, blast+) 

291 
done 

292 

293 
lemma surjective_mk_program [simp]: 

294 
"mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)" 

295 
by (auto simp add: raw_surjective_mk_program Init_def Acts_def AllowedActs_def) 

296 

297 
lemma program_equalityI: 

298 
"[Init(F) = Init(G); Acts(F) = Acts(G); 

299 
AllowedActs(F) = AllowedActs(G); F \<in> program; G \<in> program ] ==> F = G" 

300 
apply (subgoal_tac "programify(F) = programify(G)") 

301 
apply simp 

302 
apply (simp only: surjective_mk_program [symmetric]) 

303 
done 

304 

305 
lemma program_equalityE: 

306 
"[F = G; 

307 
[Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) ] 

308 
==> P ] 

309 
==> P" 

310 
by force 

311 

312 

313 
lemma program_equality_iff: 

46823  314 
"[ F \<in> program; G \<in> program ] ==>(F=G) \<longleftrightarrow> 
14077  315 
(Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))" 
316 
by (blast intro: program_equalityI program_equalityE) 

317 

318 
subsection{*These rules allow "lazy" definition expansion*} 

319 

320 
lemma def_prg_Init: 

321 
"F == mk_program (init,acts,allowed) ==> Init(F) = init \<inter> state" 

322 
by auto 

323 

324 
lemma def_prg_Acts: 

325 
"F == mk_program (init,acts,allowed) 

326 
==> Acts(F) = cons(id(state), acts \<inter> Pow(state*state))" 

327 
by auto 

328 

329 
lemma def_prg_AllowedActs: 

330 
"F == mk_program (init,acts,allowed) 

331 
==> AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))" 

332 
by auto 

333 

334 
lemma def_prg_simps: 

335 
"[ F == mk_program (init,acts,allowed) ] 

336 
==> Init(F) = init \<inter> state & 

337 
Acts(F) = cons(id(state), acts \<inter> Pow(state*state)) & 

338 
AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))" 

339 
by auto 

340 

341 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

342 
text{*An action is expanded only if a pair of states is being tested against it*} 
14077  343 
lemma def_act_simp: 
344 
"[ act == {<s,s'> \<in> A*B. P(s, s')} ] 

46823  345 
==> (<s,s'> \<in> act) \<longleftrightarrow> (<s,s'> \<in> A*B & P(s, s'))" 
14077  346 
by auto 
347 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

348 
text{*A set is expanded only if an element is being tested against it*} 
46823  349 
lemma def_set_simp: "A == B ==> (x \<in> A) \<longleftrightarrow> (x \<in> B)" 
14077  350 
by auto 
351 

352 

353 
subsection{*The Constrains Operator*} 

354 

355 
lemma constrains_type: "A co B \<subseteq> program" 

356 
by (force simp add: constrains_def) 

357 

358 
lemma constrainsI: 

359 
"[(!!act s s'. [ act: Acts(F); <s,s'> \<in> act; s \<in> A] ==> s' \<in> A'); 

360 
F \<in> program; st_set(A) ] ==> F \<in> A co A'" 

361 
by (force simp add: constrains_def) 

362 

363 
lemma constrainsD: 

364 
"F \<in> A co B ==> \<forall>act \<in> Acts(F). act``A\<subseteq>B" 

365 
by (force simp add: constrains_def) 

366 

367 
lemma constrainsD2: "F \<in> A co B ==> F \<in> program & st_set(A)" 

368 
by (force simp add: constrains_def) 

369 

46823  370 
lemma constrains_empty [iff]: "F \<in> 0 co B \<longleftrightarrow> F \<in> program" 
14077  371 
by (force simp add: constrains_def st_set_def) 
372 

46823  373 
lemma constrains_empty2 [iff]: "(F \<in> A co 0) \<longleftrightarrow> (A=0 & F \<in> program)" 
14077  374 
by (force simp add: constrains_def st_set_def) 
375 

46823  376 
lemma constrains_state [iff]: "(F \<in> state co B) \<longleftrightarrow> (state\<subseteq>B & F \<in> program)" 
14077  377 
apply (cut_tac F = F in Acts_type) 
378 
apply (force simp add: constrains_def st_set_def) 

379 
done 

380 

46823  381 
lemma constrains_state2 [iff]: "F \<in> A co state \<longleftrightarrow> (F \<in> program & st_set(A))" 
14077  382 
apply (cut_tac F = F in Acts_type) 
383 
apply (force simp add: constrains_def st_set_def) 

384 
done 

385 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

386 
text{*monotonic in 2nd argument*} 
14077  387 
lemma constrains_weaken_R: 
388 
"[ F \<in> A co A'; A'\<subseteq>B' ] ==> F \<in> A co B'" 

389 
apply (unfold constrains_def, blast) 

390 
done 

391 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

392 
text{*antimonotonic in 1st argument*} 
14077  393 
lemma constrains_weaken_L: 
394 
"[ F \<in> A co A'; B\<subseteq>A ] ==> F \<in> B co A'" 

395 
apply (unfold constrains_def st_set_def, blast) 

396 
done 

397 

398 
lemma constrains_weaken: 

399 
"[ F \<in> A co A'; B\<subseteq>A; A'\<subseteq>B' ] ==> F \<in> B co B'" 

400 
apply (drule constrains_weaken_R) 

401 
apply (drule_tac [2] constrains_weaken_L, blast+) 

402 
done 

403 

404 

405 
subsection{*Constrains and Union*} 

406 

407 
lemma constrains_Un: 

46823  408 
"[ F \<in> A co A'; F \<in> B co B' ] ==> F \<in> (A \<union> B) co (A' \<union> B')" 
14077  409 
by (auto simp add: constrains_def st_set_def, force) 
410 

411 
lemma constrains_UN: 

412 
"[!!i. i \<in> I ==> F \<in> A(i) co A'(i); F \<in> program ] 

413 
==> F \<in> (\<Union>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))" 

414 
by (force simp add: constrains_def st_set_def) 

415 

416 
lemma constrains_Un_distrib: 

46823  417 
"(A \<union> B) co C = (A co C) \<inter> (B co C)" 
14077  418 
by (force simp add: constrains_def st_set_def) 
419 

420 
lemma constrains_UN_distrib: 

421 
"i \<in> I ==> (\<Union>i \<in> I. A(i)) co B = (\<Inter>i \<in> I. A(i) co B)" 

422 
by (force simp add: constrains_def st_set_def) 

423 

424 

425 
subsection{*Constrains and Intersection*} 

426 

427 
lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)" 

428 
by (force simp add: constrains_def st_set_def) 

429 

430 
lemma constrains_INT_distrib: 

431 
"x \<in> I ==> A co (\<Inter>i \<in> I. B(i)) = (\<Inter>i \<in> I. A co B(i))" 

432 
by (force simp add: constrains_def st_set_def) 

433 

434 
lemma constrains_Int: 

435 
"[ F \<in> A co A'; F \<in> B co B' ] ==> F \<in> (A \<inter> B) co (A' \<inter> B')" 

436 
by (force simp add: constrains_def st_set_def) 

437 

438 
lemma constrains_INT [rule_format]: 

439 
"[ \<forall>i \<in> I. F \<in> A(i) co A'(i); F \<in> program] 

440 
==> F \<in> (\<Inter>i \<in> I. A(i)) co (\<Inter>i \<in> I. A'(i))" 

441 
apply (case_tac "I=0") 

442 
apply (simp add: Inter_def) 

443 
apply (erule not_emptyE) 

444 
apply (auto simp add: constrains_def st_set_def, blast) 

445 
apply (drule bspec, assumption, force) 

446 
done 

447 

448 
(* The rule below simulates the HOL's one for (\<Inter>z. A i) co (\<Inter>z. B i) *) 

449 
lemma constrains_All: 

450 
"[ \<forall>z. F:{s \<in> state. P(s, z)} co {s \<in> state. Q(s, z)}; F \<in> program ]==> 

451 
F:{s \<in> state. \<forall>z. P(s, z)} co {s \<in> state. \<forall>z. Q(s, z)}" 

452 
by (unfold constrains_def, blast) 

453 

454 
lemma constrains_imp_subset: 

455 
"[ F \<in> A co A' ] ==> A \<subseteq> A'" 

456 
by (unfold constrains_def st_set_def, force) 

457 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

458 
text{*The reasoning is by subsets since "co" refers to single actions 
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

459 
only. So this rule isn't that useful.*} 
14077  460 

461 
lemma constrains_trans: "[ F \<in> A co B; F \<in> B co C ] ==> F \<in> A co C" 

462 
by (unfold constrains_def st_set_def, auto, blast) 

463 

464 
lemma constrains_cancel: 

46823  465 
"[ F \<in> A co (A' \<union> B); F \<in> B co B' ] ==> F \<in> A co (A' \<union> B')" 
14077  466 
apply (drule_tac A = B in constrains_imp_subset) 
467 
apply (blast intro: constrains_weaken_R) 

468 
done 

469 

470 

471 
subsection{*The Unless Operator*} 

472 

473 
lemma unless_type: "A unless B \<subseteq> program" 

474 
by (force simp add: unless_def constrains_def) 

475 

46823  476 
lemma unlessI: "[ F \<in> (AB) co (A \<union> B) ] ==> F \<in> A unless B" 
14077  477 
apply (unfold unless_def) 
478 
apply (blast dest: constrainsD2) 

479 
done 

480 

46823  481 
lemma unlessD: "F :A unless B ==> F \<in> (AB) co (A \<union> B)" 
14077  482 
by (unfold unless_def, auto) 
483 

484 

485 
subsection{*The Operator @{term initially}*} 

486 

487 
lemma initially_type: "initially(A) \<subseteq> program" 

488 
by (unfold initially_def, blast) 

489 

490 
lemma initiallyI: "[ F \<in> program; Init(F)\<subseteq>A ] ==> F \<in> initially(A)" 

491 
by (unfold initially_def, blast) 

492 

493 
lemma initiallyD: "F \<in> initially(A) ==> Init(F)\<subseteq>A" 

494 
by (unfold initially_def, blast) 

495 

496 

497 
subsection{*The Operator @{term stable}*} 

498 

499 
lemma stable_type: "stable(A)\<subseteq>program" 

500 
by (unfold stable_def constrains_def, blast) 

501 

502 
lemma stableI: "F \<in> A co A ==> F \<in> stable(A)" 

503 
by (unfold stable_def, assumption) 

504 

505 
lemma stableD: "F \<in> stable(A) ==> F \<in> A co A" 

506 
by (unfold stable_def, assumption) 

507 

508 
lemma stableD2: "F \<in> stable(A) ==> F \<in> program & st_set(A)" 

509 
by (unfold stable_def constrains_def, auto) 

510 

511 
lemma stable_state [simp]: "stable(state) = program" 

512 
by (auto simp add: stable_def constrains_def dest: Acts_type [THEN subsetD]) 

513 

514 

515 
lemma stable_unless: "stable(A)= A unless 0" 

516 
by (auto simp add: unless_def stable_def) 

517 

518 

519 
subsection{*Union and Intersection with @{term stable}*} 

520 

521 
lemma stable_Un: 

46823  522 
"[ F \<in> stable(A); F \<in> stable(A') ] ==> F \<in> stable(A \<union> A')" 
14077  523 
apply (unfold stable_def) 
524 
apply (blast intro: constrains_Un) 

525 
done 

526 

527 
lemma stable_UN: 

528 
"[!!i. i\<in>I ==> F \<in> stable(A(i)); F \<in> program ] 

529 
==> F \<in> stable (\<Union>i \<in> I. A(i))" 

530 
apply (unfold stable_def) 

531 
apply (blast intro: constrains_UN) 

532 
done 

533 

534 
lemma stable_Int: 

535 
"[ F \<in> stable(A); F \<in> stable(A') ] ==> F \<in> stable (A \<inter> A')" 

536 
apply (unfold stable_def) 

537 
apply (blast intro: constrains_Int) 

538 
done 

539 

540 
lemma stable_INT: 

541 
"[ !!i. i \<in> I ==> F \<in> stable(A(i)); F \<in> program ] 

542 
==> F \<in> stable (\<Inter>i \<in> I. A(i))" 

543 
apply (unfold stable_def) 

544 
apply (blast intro: constrains_INT) 

545 
done 

546 

547 
lemma stable_All: 

548 
"[\<forall>z. F \<in> stable({s \<in> state. P(s, z)}); F \<in> program] 

549 
==> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})" 

550 
apply (unfold stable_def) 

551 
apply (rule constrains_All, auto) 

552 
done 

553 

554 
lemma stable_constrains_Un: 

46823  555 
"[ F \<in> stable(C); F \<in> A co (C \<union> A') ] ==> F \<in> (C \<union> A) co (C \<union> A')" 
14077  556 
apply (unfold stable_def constrains_def st_set_def, auto) 
557 
apply (blast dest!: bspec) 

558 
done 

559 

560 
lemma stable_constrains_Int: 

561 
"[ F \<in> stable(C); F \<in> (C \<inter> A) co A' ] ==> F \<in> (C \<inter> A) co (C \<inter> A')" 

562 
by (unfold stable_def constrains_def st_set_def, blast) 

563 

564 
(* [ F \<in> stable(C); F \<in> (C \<inter> A) co A ] ==> F \<in> stable(C \<inter> A) *) 

45602  565 
lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI] 
14077  566 

567 
subsection{*The Operator @{term invariant}*} 

568 

569 
lemma invariant_type: "invariant(A) \<subseteq> program" 

570 
apply (unfold invariant_def) 

571 
apply (blast dest: stable_type [THEN subsetD]) 

572 
done 

573 

574 
lemma invariantI: "[ Init(F)\<subseteq>A; F \<in> stable(A) ] ==> F \<in> invariant(A)" 

575 
apply (unfold invariant_def initially_def) 

576 
apply (frule stable_type [THEN subsetD], auto) 

577 
done 

578 

579 
lemma invariantD: "F \<in> invariant(A) ==> Init(F)\<subseteq>A & F \<in> stable(A)" 

580 
by (unfold invariant_def initially_def, auto) 

581 

582 
lemma invariantD2: "F \<in> invariant(A) ==> F \<in> program & st_set(A)" 

583 
apply (unfold invariant_def) 

584 
apply (blast dest: stableD2) 

585 
done 

586 

587 
text{*Could also say 

588 
@{term "invariant(A) \<inter> invariant(B) \<subseteq> invariant (A \<inter> B)"}*} 

589 
lemma invariant_Int: 

590 
"[ F \<in> invariant(A); F \<in> invariant(B) ] ==> F \<in> invariant(A \<inter> B)" 

591 
apply (unfold invariant_def initially_def) 

592 
apply (simp add: stable_Int, blast) 

593 
done 

594 

595 

596 
subsection{*The Elimination Theorem*} 

597 

598 
(** The "free" m has become universally quantified! 

599 
Should the premise be !!m instead of \<forall>m ? Would make it harder 

600 
to use in forward proof. **) 

601 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

602 
text{*The general case is easier to prove than the special case!*} 
14077  603 
lemma "elimination": 
604 
"[ \<forall>m \<in> M. F \<in> {s \<in> A. x(s) = m} co B(m); F \<in> program ] 

605 
==> F \<in> {s \<in> A. x(s) \<in> M} co (\<Union>m \<in> M. B(m))" 

606 
by (auto simp add: constrains_def st_set_def, blast) 

607 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset

608 
text{*As above, but for the special case of A=state*} 
14077  609 
lemma elimination2: 
610 
"[ \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} co B(m); F \<in> program ] 

611 
==> F:{s \<in> state. x(s) \<in> M} co (\<Union>m \<in> M. B(m))" 

612 
by (rule UNITY.elimination, auto) 

613 

614 
subsection{*The Operator @{term strongest_rhs}*} 

615 

616 
lemma constrains_strongest_rhs: 

617 
"[ F \<in> program; st_set(A) ] ==> F \<in> A co (strongest_rhs(F,A))" 

618 
by (auto simp add: constrains_def strongest_rhs_def st_set_def 

619 
dest: Acts_type [THEN subsetD]) 

620 

621 
lemma strongest_rhs_is_strongest: 

622 
"[ F \<in> A co B; st_set(B) ] ==> strongest_rhs(F,A) \<subseteq> B" 

623 
by (auto simp add: constrains_def strongest_rhs_def st_set_def) 

624 

24893  625 
ML {* 
626 
fun simp_of_act def = def RS @{thm def_act_simp}; 

627 
fun simp_of_set def = def RS @{thm def_set_simp}; 

14077  628 
*} 
629 

11479  630 
end 