author  wenzelm 
Mon, 01 Aug 2005 19:20:31 +0200  
changeset 16977  7c04742abac3 
parent 16417  9bc16273c2d4 
child 30304  d8e4cd2ac2a1 
permissions  rwrr 
5252  1 
(* Title: HOL/UNITY/Union.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset

6 
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs 
5252  7 
*) 
8 

13798  9 
header{*Unions of Programs*} 
10 

16417  11 
theory Union imports SubstAx FP begin 
5252  12 

13 
constdefs 

10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset

14 

13805  15 
(*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) 
13792  16 
ok :: "['a program, 'a program] => bool" (infixl "ok" 65) 
13805  17 
"F ok G == Acts F \<subseteq> AllowedActs G & 
18 
Acts G \<subseteq> AllowedActs F" 

10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset

19 

13805  20 
(*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *) 
13792  21 
OK :: "['a set, 'a => 'b program] => bool" 
13805  22 
"OK I F == (\<forall>i \<in> I. \<forall>j \<in> I{i}. Acts (F i) \<subseteq> AllowedActs (F j))" 
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset

23 

13792  24 
JOIN :: "['a set, 'a => 'b program] => 'b program" 
13805  25 
"JOIN I F == mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i), 
26 
\<Inter>i \<in> I. AllowedActs (F i))" 

5252  27 

13792  28 
Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65) 
13805  29 
"F Join G == mk_program (Init F \<inter> Init G, Acts F \<union> Acts G, 
30 
AllowedActs F \<inter> AllowedActs G)" 

5252  31 

13792  32 
SKIP :: "'a program" 
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset

33 
"SKIP == mk_program (UNIV, {}, UNIV)" 
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset

34 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

35 
(*Characterizes safety properties. Used with specifying Allowed*) 
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset

36 
safety_prop :: "'a program set => bool" 
13805  37 
"safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts > G \<in> X)" 
5259  38 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

39 
syntax 
13792  40 
"@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10) 
41 
"@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10) 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

42 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

43 
translations 
13805  44 
"JN x : A. B" == "JOIN A (%x. B)" 
7359  45 
"JN x y. B" == "JN x. JN y. B" 
46 
"JN x. B" == "JOIN UNIV (%x. B)" 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

47 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
10064
diff
changeset

48 
syntax (xsymbols) 
13819  49 
SKIP :: "'a program" ("\<bottom>") 
50 
Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65) 

51 
"@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10) 

52 
"@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10) 

13792  53 

54 

13798  55 
subsection{*SKIP*} 
13792  56 

57 
lemma Init_SKIP [simp]: "Init SKIP = UNIV" 

58 
by (simp add: SKIP_def) 

59 

60 
lemma Acts_SKIP [simp]: "Acts SKIP = {Id}" 

61 
by (simp add: SKIP_def) 

62 

63 
lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV" 

64 
by (auto simp add: SKIP_def) 

65 

66 
lemma reachable_SKIP [simp]: "reachable SKIP = UNIV" 

67 
by (force elim: reachable.induct intro: reachable.intros) 

68 

13798  69 
subsection{*SKIP and safety properties*} 
13792  70 

13805  71 
lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) = (A \<subseteq> B)" 
13792  72 
by (unfold constrains_def, auto) 
73 

13805  74 
lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B) = (A \<subseteq> B)" 
13792  75 
by (unfold Constrains_def, auto) 
76 

13805  77 
lemma SKIP_in_stable [iff]: "SKIP \<in> stable A" 
13792  78 
by (unfold stable_def, auto) 
79 

80 
declare SKIP_in_stable [THEN stable_imp_Stable, iff] 

81 

82 

13798  83 
subsection{*Join*} 
13792  84 

13819  85 
lemma Init_Join [simp]: "Init (F\<squnion>G) = Init F \<inter> Init G" 
13792  86 
by (simp add: Join_def) 
87 

13819  88 
lemma Acts_Join [simp]: "Acts (F\<squnion>G) = Acts F \<union> Acts G" 
13792  89 
by (auto simp add: Join_def) 
90 

91 
lemma AllowedActs_Join [simp]: 

13819  92 
"AllowedActs (F\<squnion>G) = AllowedActs F \<inter> AllowedActs G" 
13792  93 
by (auto simp add: Join_def) 
94 

95 

13798  96 
subsection{*JN*} 
13792  97 

13805  98 
lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP" 
13792  99 
by (unfold JOIN_def SKIP_def, auto) 
100 

13819  101 
lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a)\<squnion>(\<Squnion>i \<in> I. F i)" 
13792  102 
apply (rule program_equalityI) 
103 
apply (auto simp add: JOIN_def Join_def) 

104 
done 

105 

13805  106 
lemma Init_JN [simp]: "Init (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. Init (F i))" 
13792  107 
by (simp add: JOIN_def) 
108 

13805  109 
lemma Acts_JN [simp]: "Acts (\<Squnion>i \<in> I. F i) = insert Id (\<Union>i \<in> I. Acts (F i))" 
13792  110 
by (auto simp add: JOIN_def) 
111 

112 
lemma AllowedActs_JN [simp]: 

13805  113 
"AllowedActs (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. AllowedActs (F i))" 
13792  114 
by (auto simp add: JOIN_def) 
115 

116 

117 
lemma JN_cong [cong]: 

13805  118 
"[ I=J; !!i. i \<in> J ==> F i = G i ] ==> (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> J. G i)" 
13792  119 
by (simp add: JOIN_def) 
120 

121 

13798  122 
subsection{*Algebraic laws*} 
13792  123 

13819  124 
lemma Join_commute: "F\<squnion>G = G\<squnion>F" 
13792  125 
by (simp add: Join_def Un_commute Int_commute) 
126 

13819  127 
lemma Join_assoc: "(F\<squnion>G)\<squnion>H = F\<squnion>(G\<squnion>H)" 
13792  128 
by (simp add: Un_ac Join_def Int_assoc insert_absorb) 
129 

13819  130 
lemma Join_left_commute: "A\<squnion>(B\<squnion>C) = B\<squnion>(A\<squnion>C)" 
13792  131 
by (simp add: Un_ac Int_ac Join_def insert_absorb) 
132 

13819  133 
lemma Join_SKIP_left [simp]: "SKIP\<squnion>F = F" 
13792  134 
apply (unfold Join_def SKIP_def) 
135 
apply (rule program_equalityI) 

136 
apply (simp_all (no_asm) add: insert_absorb) 

137 
done 

138 

13819  139 
lemma Join_SKIP_right [simp]: "F\<squnion>SKIP = F" 
13792  140 
apply (unfold Join_def SKIP_def) 
141 
apply (rule program_equalityI) 

142 
apply (simp_all (no_asm) add: insert_absorb) 

143 
done 

144 

13819  145 
lemma Join_absorb [simp]: "F\<squnion>F = F" 
13792  146 
apply (unfold Join_def) 
147 
apply (rule program_equalityI, auto) 

148 
done 

149 

13819  150 
lemma Join_left_absorb: "F\<squnion>(F\<squnion>G) = F\<squnion>G" 
13792  151 
apply (unfold Join_def) 
152 
apply (rule program_equalityI, auto) 

153 
done 

154 

155 
(*Join is an ACoperator*) 

156 
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute 

157 

158 

14150  159 
subsection{*Laws Governing @{text "\<Squnion>"}*} 
13792  160 

161 
(*Also follows by JN_insert and insert_absorb, but the proof is longer*) 

13819  162 
lemma JN_absorb: "k \<in> I ==> F k\<squnion>(\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)" 
13792  163 
by (auto intro!: program_equalityI) 
164 

13819  165 
lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i)\<squnion>(\<Squnion>i \<in> J. F i))" 
13792  166 
by (auto intro!: program_equalityI) 
167 

13805  168 
lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I={} then SKIP else c)" 
13792  169 
by (rule program_equalityI, auto) 
170 

171 
lemma JN_Join_distrib: 

13819  172 
"(\<Squnion>i \<in> I. F i\<squnion>G i) = (\<Squnion>i \<in> I. F i) \<squnion> (\<Squnion>i \<in> I. G i)" 
13792  173 
by (auto intro!: program_equalityI) 
174 

175 
lemma JN_Join_miniscope: 

13819  176 
"i \<in> I ==> (\<Squnion>i \<in> I. F i\<squnion>G) = ((\<Squnion>i \<in> I. F i)\<squnion>G)" 
13792  177 
by (auto simp add: JN_Join_distrib JN_constant) 
178 

179 
(*Used to prove guarantees_JN_I*) 

13819  180 
lemma JN_Join_diff: "i \<in> I ==> F i\<squnion>JOIN (I  {i}) F = JOIN I F" 
13792  181 
apply (unfold JOIN_def Join_def) 
182 
apply (rule program_equalityI, auto) 

183 
done 

184 

185 

13798  186 
subsection{*Safety: co, stable, FP*} 
13792  187 

13805  188 
(*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B. So an 
189 
alternative precondition is A \<subseteq> B, but most proofs using this rule require 

13792  190 
I to be nonempty for other reasons anyway.*) 
191 
lemma JN_constrains: 

13805  192 
"i \<in> I ==> (\<Squnion>i \<in> I. F i) \<in> A co B = (\<forall>i \<in> I. F i \<in> A co B)" 
13792  193 
by (simp add: constrains_def JOIN_def, blast) 
194 

195 
lemma Join_constrains [simp]: 

13819  196 
"(F\<squnion>G \<in> A co B) = (F \<in> A co B & G \<in> A co B)" 
13792  197 
by (auto simp add: constrains_def Join_def) 
198 

199 
lemma Join_unless [simp]: 

13819  200 
"(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)" 
13792  201 
by (simp add: Join_constrains unless_def) 
202 

203 
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. 

13819  204 
reachable (F\<squnion>G) could be much bigger than reachable F, reachable G 
13792  205 
*) 
206 

207 

208 
lemma Join_constrains_weaken: 

13805  209 
"[ F \<in> A co A'; G \<in> B co B' ] 
13819  210 
==> F\<squnion>G \<in> (A \<inter> B) co (A' \<union> B')" 
13792  211 
by (simp, blast intro: constrains_weaken) 
212 

13805  213 
(*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*) 
13792  214 
lemma JN_constrains_weaken: 
13805  215 
"[ \<forall>i \<in> I. F i \<in> A i co A' i; i \<in> I ] 
216 
==> (\<Squnion>i \<in> I. F i) \<in> (\<Inter>i \<in> I. A i) co (\<Union>i \<in> I. A' i)" 

13792  217 
apply (simp (no_asm_simp) add: JN_constrains) 
218 
apply (blast intro: constrains_weaken) 

219 
done 

220 

13805  221 
lemma JN_stable: "(\<Squnion>i \<in> I. F i) \<in> stable A = (\<forall>i \<in> I. F i \<in> stable A)" 
13792  222 
by (simp add: stable_def constrains_def JOIN_def) 
223 

224 
lemma invariant_JN_I: 

13805  225 
"[ !!i. i \<in> I ==> F i \<in> invariant A; i \<in> I ] 
226 
==> (\<Squnion>i \<in> I. F i) \<in> invariant A" 

13792  227 
by (simp add: invariant_def JN_stable, blast) 
228 

229 
lemma Join_stable [simp]: 

13819  230 
"(F\<squnion>G \<in> stable A) = 
13805  231 
(F \<in> stable A & G \<in> stable A)" 
13792  232 
by (simp add: stable_def) 
233 

234 
lemma Join_increasing [simp]: 

13819  235 
"(F\<squnion>G \<in> increasing f) = 
13805  236 
(F \<in> increasing f & G \<in> increasing f)" 
13792  237 
by (simp add: increasing_def Join_stable, blast) 
238 

239 
lemma invariant_JoinI: 

13805  240 
"[ F \<in> invariant A; G \<in> invariant A ] 
13819  241 
==> F\<squnion>G \<in> invariant A" 
13792  242 
by (simp add: invariant_def, blast) 
243 

13805  244 
lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))" 
13792  245 
by (simp add: FP_def JN_stable INTER_def) 
246 

247 

13798  248 
subsection{*Progress: transient, ensures*} 
13792  249 

250 
lemma JN_transient: 

13805  251 
"i \<in> I ==> 
252 
(\<Squnion>i \<in> I. F i) \<in> transient A = (\<exists>i \<in> I. F i \<in> transient A)" 

13792  253 
by (auto simp add: transient_def JOIN_def) 
254 

255 
lemma Join_transient [simp]: 

13819  256 
"F\<squnion>G \<in> transient A = 
13805  257 
(F \<in> transient A  G \<in> transient A)" 
13792  258 
by (auto simp add: bex_Un transient_def Join_def) 
259 

13819  260 
lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A" 
13792  261 
by (simp add: Join_transient) 
262 

13819  263 
lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A" 
13792  264 
by (simp add: Join_transient) 
265 

13805  266 
(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *) 
13792  267 
lemma JN_ensures: 
13805  268 
"i \<in> I ==> 
269 
(\<Squnion>i \<in> I. F i) \<in> A ensures B = 

270 
((\<forall>i \<in> I. F i \<in> (AB) co (A \<union> B)) & (\<exists>i \<in> I. F i \<in> A ensures B))" 

13792  271 
by (auto simp add: ensures_def JN_constrains JN_transient) 
272 

273 
lemma Join_ensures: 

13819  274 
"F\<squnion>G \<in> A ensures B = 
13805  275 
(F \<in> (AB) co (A \<union> B) & G \<in> (AB) co (A \<union> B) & 
276 
(F \<in> transient (AB)  G \<in> transient (AB)))" 

13792  277 
by (auto simp add: ensures_def Join_transient) 
278 

279 
lemma stable_Join_constrains: 

13805  280 
"[ F \<in> stable A; G \<in> A co A' ] 
13819  281 
==> F\<squnion>G \<in> A co A'" 
13792  282 
apply (unfold stable_def constrains_def Join_def) 
283 
apply (simp add: ball_Un, blast) 

284 
done 

285 

13805  286 
(*Premise for G cannot use Always because F \<in> Stable A is weaker than 
287 
G \<in> stable A *) 

13792  288 
lemma stable_Join_Always1: 
13819  289 
"[ F \<in> stable A; G \<in> invariant A ] ==> F\<squnion>G \<in> Always A" 
13792  290 
apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable) 
291 
apply (force intro: stable_Int) 

292 
done 

293 

294 
(*As above, but exchanging the roles of F and G*) 

295 
lemma stable_Join_Always2: 

13819  296 
"[ F \<in> invariant A; G \<in> stable A ] ==> F\<squnion>G \<in> Always A" 
13792  297 
apply (subst Join_commute) 
298 
apply (blast intro: stable_Join_Always1) 

299 
done 

300 

301 
lemma stable_Join_ensures1: 

13819  302 
"[ F \<in> stable A; G \<in> A ensures B ] ==> F\<squnion>G \<in> A ensures B" 
13792  303 
apply (simp (no_asm_simp) add: Join_ensures) 
304 
apply (simp add: stable_def ensures_def) 

305 
apply (erule constrains_weaken, auto) 

306 
done 

307 

308 
(*As above, but exchanging the roles of F and G*) 

309 
lemma stable_Join_ensures2: 

13819  310 
"[ F \<in> A ensures B; G \<in> stable A ] ==> F\<squnion>G \<in> A ensures B" 
13792  311 
apply (subst Join_commute) 
312 
apply (blast intro: stable_Join_ensures1) 

313 
done 

314 

315 

13798  316 
subsection{*the ok and OK relations*} 
13792  317 

318 
lemma ok_SKIP1 [iff]: "SKIP ok F" 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

319 
by (simp add: ok_def) 
13792  320 

321 
lemma ok_SKIP2 [iff]: "F ok SKIP" 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

322 
by (simp add: ok_def) 
13792  323 

324 
lemma ok_Join_commute: 

13819  325 
"(F ok G & (F\<squnion>G) ok H) = (G ok H & F ok (G\<squnion>H))" 
13792  326 
by (auto simp add: ok_def) 
327 

328 
lemma ok_commute: "(F ok G) = (G ok F)" 

329 
by (auto simp add: ok_def) 

330 

331 
lemmas ok_sym = ok_commute [THEN iffD1, standard] 

332 

333 
lemma ok_iff_OK: 

13819  334 
"OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)" 
16977  335 
apply (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb 
336 
all_conj_distrib) 

337 
apply blast 

338 
done 

13792  339 

13819  340 
lemma ok_Join_iff1 [iff]: "F ok (G\<squnion>H) = (F ok G & F ok H)" 
13792  341 
by (auto simp add: ok_def) 
342 

13819  343 
lemma ok_Join_iff2 [iff]: "(G\<squnion>H) ok F = (G ok F & H ok F)" 
13792  344 
by (auto simp add: ok_def) 
345 

346 
(*useful? Not with the previous two around*) 

13819  347 
lemma ok_Join_commute_I: "[ F ok G; (F\<squnion>G) ok H ] ==> F ok (G\<squnion>H)" 
13792  348 
by (auto simp add: ok_def) 
349 

13805  350 
lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\<forall>i \<in> I. F ok G i)" 
13792  351 
by (auto simp add: ok_def) 
352 

13805  353 
lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (\<forall>i \<in> I. G i ok F)" 
13792  354 
by (auto simp add: ok_def) 
355 

13805  356 
lemma OK_iff_ok: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I{i}. (F i) ok (F j))" 
13792  357 
by (auto simp add: ok_def OK_def) 
358 

13805  359 
lemma OK_imp_ok: "[ OK I F; i \<in> I; j \<in> I; i \<noteq> j] ==> (F i) ok (F j)" 
13792  360 
by (auto simp add: OK_iff_ok) 
361 

362 

13798  363 
subsection{*Allowed*} 
13792  364 

365 
lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV" 

366 
by (auto simp add: Allowed_def) 

367 

13819  368 
lemma Allowed_Join [simp]: "Allowed (F\<squnion>G) = Allowed F \<inter> Allowed G" 
13792  369 
by (auto simp add: Allowed_def) 
370 

13805  371 
lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i \<in> I. Allowed (F i))" 
13792  372 
by (auto simp add: Allowed_def) 
373 

13805  374 
lemma ok_iff_Allowed: "F ok G = (F \<in> Allowed G & G \<in> Allowed F)" 
13792  375 
by (simp add: ok_def Allowed_def) 
376 

13805  377 
lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I{i}. F i \<in> Allowed(F j))" 
13792  378 
by (auto simp add: OK_iff_ok ok_iff_Allowed) 
379 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

380 
subsection{*@{term safety_prop}, for reasoning about 
13798  381 
given instances of "ok"*} 
13792  382 

383 
lemma safety_prop_Acts_iff: 

13805  384 
"safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)" 
13792  385 
by (auto simp add: safety_prop_def) 
386 

387 
lemma safety_prop_AllowedActs_iff_Allowed: 

13805  388 
"safety_prop X ==> (UNION X Acts \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)" 
13792  389 
by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric]) 
390 

391 
lemma Allowed_eq: 

392 
"safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X" 

393 
by (simp add: Allowed_def safety_prop_Acts_iff) 

394 

395 
(*For safety_prop to hold, the property must be satisfiable!*) 

13805  396 
lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \<subseteq> B)" 
13792  397 
by (simp add: safety_prop_def constrains_def, blast) 
398 

399 
lemma safety_prop_stable [iff]: "safety_prop (stable A)" 

400 
by (simp add: stable_def) 

401 

402 
lemma safety_prop_Int [simp]: 

13805  403 
"[ safety_prop X; safety_prop Y ] ==> safety_prop (X \<inter> Y)" 
13792  404 
by (simp add: safety_prop_def, blast) 
405 

406 
lemma safety_prop_INTER1 [simp]: 

13805  407 
"(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)" 
13792  408 
by (auto simp add: safety_prop_def, blast) 
409 

410 
lemma safety_prop_INTER [simp]: 

13805  411 
"(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)" 
13792  412 
by (auto simp add: safety_prop_def, blast) 
413 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

414 
lemma def_prg_Allowed: 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

415 
"[ F == mk_program (init, acts, UNION X Acts) ; safety_prop X ] 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

416 
==> Allowed F = X" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

417 
by (simp add: Allowed_eq) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

418 

91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

419 
lemma Allowed_totalize [simp]: "Allowed (totalize F) = Allowed F" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

420 
by (simp add: Allowed_def) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

421 

91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

422 
lemma def_total_prg_Allowed: 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

423 
"[ F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X ] 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

424 
==> Allowed F = X" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

425 
by (simp add: mk_total_program_def def_prg_Allowed) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

426 

13792  427 
lemma def_UNION_ok_iff: 
428 
"[ F == mk_program(init,acts,UNION X Acts); safety_prop X ] 

13805  429 
==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)" 
13792  430 
by (auto simp add: ok_def safety_prop_Acts_iff) 
9685  431 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

432 
text{*The union of two total programs is total.*} 
13819  433 
lemma totalize_Join: "totalize F\<squnion>totalize G = totalize (F\<squnion>G)" 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

434 
by (simp add: program_equalityI totalize_def Join_def image_Un) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

435 

13819  436 
lemma all_total_Join: "[all_total F; all_total G] ==> all_total (F\<squnion>G)" 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

437 
by (simp add: all_total_def, blast) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

438 

91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

439 
lemma totalize_JN: "(\<Squnion>i \<in> I. totalize (F i)) = totalize(\<Squnion>i \<in> I. F i)" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

440 
by (simp add: program_equalityI totalize_def JOIN_def image_UN) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

441 

91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

442 
lemma all_total_JN: "(!!i. i\<in>I ==> all_total (F i)) ==> all_total(\<Squnion>i\<in>I. F i)" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

443 
by (simp add: all_total_iff_totalize totalize_JN [symmetric]) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

444 

5252  445 
end 