author  hoelzl 
Wed, 14 Sep 2011 10:08:52 0400  
changeset 44928  7ef6505bde7f 
parent 36866  426d5781bb25 
child 45605  a89b4bc311a5 
permissions  rwrr 
5252  1 
(* Title: HOL/UNITY/Union.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 1998 University of Cambridge 

4 

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

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

13798  8 
header{*Unions of Programs*} 
9 

16417  10 
theory Union imports SubstAx FP begin 
5252  11 

13805  12 
(*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) 
36866  13 
definition 
13792  14 
ok :: "['a program, 'a program] => bool" (infixl "ok" 65) 
36866  15 
where "F ok G == Acts F \<subseteq> AllowedActs G & 
13805  16 
Acts G \<subseteq> AllowedActs F" 
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset

17 

13805  18 
(*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *) 
36866  19 
definition 
13792  20 
OK :: "['a set, 'a => 'b program] => bool" 
36866  21 
where "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

22 

36866  23 
definition 
13792  24 
JOIN :: "['a set, 'a => 'b program] => 'b program" 
36866  25 
where "JOIN I F = mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30304
diff
changeset

26 
\<Inter>i \<in> I. AllowedActs (F i))" 
5252  27 

36866  28 
definition 
13792  29 
Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65) 
36866  30 
where "F Join G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30304
diff
changeset

31 
AllowedActs F \<inter> AllowedActs G)" 
5252  32 

36866  33 
definition 
13792  34 
SKIP :: "'a program" 
36866  35 
where "SKIP = mk_program (UNIV, {}, UNIV)" 
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset

36 

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

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

39 
safety_prop :: "'a program set => bool" 
36866  40 
where "safety_prop X <> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts > G \<in> X)" 
5259  41 

35434  42 
notation (xsymbols) 
35427  43 
SKIP ("\<bottom>") and 
44 
Join (infixl "\<squnion>" 65) 

45 

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

46 
syntax 
35054  47 
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10) 
48 
"_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10) 

35427  49 
syntax (xsymbols) 
50 
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10) 

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

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

52 

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

53 
translations 
35054  54 
"JN x: A. B" == "CONST JOIN A (%x. B)" 
55 
"JN x y. B" == "JN x. JN y. B" 

35068  56 
"JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)" 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

57 

13792  58 

13798  59 
subsection{*SKIP*} 
13792  60 

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

62 
by (simp add: SKIP_def) 

63 

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

65 
by (simp add: SKIP_def) 

66 

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

68 
by (auto simp add: SKIP_def) 

69 

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

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

72 

13798  73 
subsection{*SKIP and safety properties*} 
13792  74 

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

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

13805  81 
lemma SKIP_in_stable [iff]: "SKIP \<in> stable A" 
13792  82 
by (unfold stable_def, auto) 
83 

84 
declare SKIP_in_stable [THEN stable_imp_Stable, iff] 

85 

86 

13798  87 
subsection{*Join*} 
13792  88 

13819  89 
lemma Init_Join [simp]: "Init (F\<squnion>G) = Init F \<inter> Init G" 
13792  90 
by (simp add: Join_def) 
91 

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

95 
lemma AllowedActs_Join [simp]: 

13819  96 
"AllowedActs (F\<squnion>G) = AllowedActs F \<inter> AllowedActs G" 
13792  97 
by (auto simp add: Join_def) 
98 

99 

13798  100 
subsection{*JN*} 
13792  101 

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

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

108 
done 

109 

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

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

116 
lemma AllowedActs_JN [simp]: 

13805  117 
"AllowedActs (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. AllowedActs (F i))" 
13792  118 
by (auto simp add: JOIN_def) 
119 

120 

121 
lemma JN_cong [cong]: 

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

125 

13798  126 
subsection{*Algebraic laws*} 
13792  127 

13819  128 
lemma Join_commute: "F\<squnion>G = G\<squnion>F" 
13792  129 
by (simp add: Join_def Un_commute Int_commute) 
130 

13819  131 
lemma Join_assoc: "(F\<squnion>G)\<squnion>H = F\<squnion>(G\<squnion>H)" 
13792  132 
by (simp add: Un_ac Join_def Int_assoc insert_absorb) 
133 

13819  134 
lemma Join_left_commute: "A\<squnion>(B\<squnion>C) = B\<squnion>(A\<squnion>C)" 
13792  135 
by (simp add: Un_ac Int_ac Join_def insert_absorb) 
136 

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

140 
apply (simp_all (no_asm) add: insert_absorb) 

141 
done 

142 

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

146 
apply (simp_all (no_asm) add: insert_absorb) 

147 
done 

148 

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

152 
done 

153 

13819  154 
lemma Join_left_absorb: "F\<squnion>(F\<squnion>G) = F\<squnion>G" 
13792  155 
apply (unfold Join_def) 
156 
apply (rule program_equalityI, auto) 

157 
done 

158 

159 
(*Join is an ACoperator*) 

160 
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute 

161 

162 

14150  163 
subsection{*Laws Governing @{text "\<Squnion>"}*} 
13792  164 

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

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

13819  169 
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  170 
by (auto intro!: program_equalityI) 
171 

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

175 
lemma JN_Join_distrib: 

13819  176 
"(\<Squnion>i \<in> I. F i\<squnion>G i) = (\<Squnion>i \<in> I. F i) \<squnion> (\<Squnion>i \<in> I. G i)" 
13792  177 
by (auto intro!: program_equalityI) 
178 

179 
lemma JN_Join_miniscope: 

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

183 
(*Used to prove guarantees_JN_I*) 

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

187 
done 

188 

189 

13798  190 
subsection{*Safety: co, stable, FP*} 
13792  191 

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

13792  194 
I to be nonempty for other reasons anyway.*) 
195 
lemma JN_constrains: 

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

199 
lemma Join_constrains [simp]: 

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

203 
lemma Join_unless [simp]: 

13819  204 
"(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)" 
13792  205 
by (simp add: Join_constrains unless_def) 
206 

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

13819  208 
reachable (F\<squnion>G) could be much bigger than reachable F, reachable G 
13792  209 
*) 
210 

211 

212 
lemma Join_constrains_weaken: 

13805  213 
"[ F \<in> A co A'; G \<in> B co B' ] 
13819  214 
==> F\<squnion>G \<in> (A \<inter> B) co (A' \<union> B')" 
13792  215 
by (simp, blast intro: constrains_weaken) 
216 

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

13792  221 
apply (simp (no_asm_simp) add: JN_constrains) 
222 
apply (blast intro: constrains_weaken) 

223 
done 

224 

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

228 
lemma invariant_JN_I: 

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

13792  231 
by (simp add: invariant_def JN_stable, blast) 
232 

233 
lemma Join_stable [simp]: 

13819  234 
"(F\<squnion>G \<in> stable A) = 
13805  235 
(F \<in> stable A & G \<in> stable A)" 
13792  236 
by (simp add: stable_def) 
237 

238 
lemma Join_increasing [simp]: 

13819  239 
"(F\<squnion>G \<in> increasing f) = 
13805  240 
(F \<in> increasing f & G \<in> increasing f)" 
13792  241 
by (simp add: increasing_def Join_stable, blast) 
242 

243 
lemma invariant_JoinI: 

13805  244 
"[ F \<in> invariant A; G \<in> invariant A ] 
13819  245 
==> F\<squnion>G \<in> invariant A" 
13792  246 
by (simp add: invariant_def, blast) 
247 

13805  248 
lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))" 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
36866
diff
changeset

249 
by (simp add: FP_def JN_stable INTER_eq) 
13792  250 

251 

13798  252 
subsection{*Progress: transient, ensures*} 
13792  253 

254 
lemma JN_transient: 

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

13792  257 
by (auto simp add: transient_def JOIN_def) 
258 

259 
lemma Join_transient [simp]: 

13819  260 
"F\<squnion>G \<in> transient A = 
13805  261 
(F \<in> transient A  G \<in> transient A)" 
13792  262 
by (auto simp add: bex_Un transient_def Join_def) 
263 

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

13819  267 
lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A" 
13792  268 
by (simp add: Join_transient) 
269 

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

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

13792  275 
by (auto simp add: ensures_def JN_constrains JN_transient) 
276 

277 
lemma Join_ensures: 

13819  278 
"F\<squnion>G \<in> A ensures B = 
13805  279 
(F \<in> (AB) co (A \<union> B) & G \<in> (AB) co (A \<union> B) & 
280 
(F \<in> transient (AB)  G \<in> transient (AB)))" 

13792  281 
by (auto simp add: ensures_def Join_transient) 
282 

283 
lemma stable_Join_constrains: 

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

288 
done 

289 

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

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

296 
done 

297 

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

299 
lemma stable_Join_Always2: 

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

303 
done 

304 

305 
lemma stable_Join_ensures1: 

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

309 
apply (erule constrains_weaken, auto) 

310 
done 

311 

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

313 
lemma stable_Join_ensures2: 

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

317 
done 

318 

319 

13798  320 
subsection{*the ok and OK relations*} 
13792  321 

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

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

323 
by (simp add: ok_def) 
13792  324 

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

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

326 
by (simp add: ok_def) 
13792  327 

328 
lemma ok_Join_commute: 

13819  329 
"(F ok G & (F\<squnion>G) ok H) = (G ok H & F ok (G\<squnion>H))" 
13792  330 
by (auto simp add: ok_def) 
331 

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

333 
by (auto simp add: ok_def) 

334 

335 
lemmas ok_sym = ok_commute [THEN iffD1, standard] 

336 

337 
lemma ok_iff_OK: 

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

341 
apply blast 

342 
done 

13792  343 

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

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

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

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

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

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

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

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

366 

13798  367 
subsection{*Allowed*} 
13792  368 

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

370 
by (auto simp add: Allowed_def) 

371 

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

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

13805  378 
lemma ok_iff_Allowed: "F ok G = (F \<in> Allowed G & G \<in> Allowed F)" 
13792  379 
by (simp add: ok_def Allowed_def) 
380 

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

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

384 
subsection{*@{term safety_prop}, for reasoning about 
13798  385 
given instances of "ok"*} 
13792  386 

387 
lemma safety_prop_Acts_iff: 

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

391 
lemma safety_prop_AllowedActs_iff_Allowed: 

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

395 
lemma Allowed_eq: 

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

397 
by (simp add: Allowed_def safety_prop_Acts_iff) 

398 

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

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

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

404 
by (simp add: stable_def) 

405 

406 
lemma safety_prop_Int [simp]: 

13805  407 
"[ safety_prop X; safety_prop Y ] ==> safety_prop (X \<inter> Y)" 
13792  408 
by (simp add: safety_prop_def, blast) 
409 

410 
lemma safety_prop_INTER1 [simp]: 

13805  411 
"(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)" 
13792  412 
by (auto simp add: safety_prop_def, blast) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30304
diff
changeset

413 

13792  414 
lemma safety_prop_INTER [simp]: 
13805  415 
"(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)" 
13792  416 
by (auto simp add: safety_prop_def, blast) 
417 

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

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

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

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

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

422 

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

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

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

425 

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

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

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

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

430 

13792  431 
lemma def_UNION_ok_iff: 
36866  432 
"[ F = mk_program(init,acts,UNION X Acts); safety_prop X ] 
13805  433 
==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)" 
13792  434 
by (auto simp add: ok_def safety_prop_Acts_iff) 
9685  435 

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

436 
text{*The union of two total programs is total.*} 
13819  437 
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

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

439 

13819  440 
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

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

442 

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

443 
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

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

445 

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

446 
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

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

448 

5252  449 
end 