author  wenzelm 
Sat, 17 Oct 2009 14:43:18 +0200  
changeset 32960  69916a850301 
parent 30304  d8e4cd2ac2a1 
child 35054  a5db9779b026 
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 

12 
constdefs 

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

13 

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

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

18 

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

13792  23 
JOIN :: "['a set, 'a => 'b program] => 'b program" 
13805  24 
"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

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

13792  27 
Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65) 
13805  28 
"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

29 
AllowedActs F \<inter> AllowedActs G)" 
5252  30 

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

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

33 

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

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

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

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

38 
syntax 
13792  39 
"@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10) 
40 
"@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

41 

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

42 
translations 
13805  43 
"JN x : A. B" == "JOIN A (%x. B)" 
7359  44 
"JN x y. B" == "JN x. JN y. B" 
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
16977
diff
changeset

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

46 

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

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

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

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

13792  52 

53 

13798  54 
subsection{*SKIP*} 
13792  55 

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

57 
by (simp add: SKIP_def) 

58 

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

60 
by (simp add: SKIP_def) 

61 

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

63 
by (auto simp add: SKIP_def) 

64 

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

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

67 

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

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

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

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

79 
declare SKIP_in_stable [THEN stable_imp_Stable, iff] 

80 

81 

13798  82 
subsection{*Join*} 
13792  83 

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

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

90 
lemma AllowedActs_Join [simp]: 

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

94 

13798  95 
subsection{*JN*} 
13792  96 

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

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

103 
done 

104 

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

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

111 
lemma AllowedActs_JN [simp]: 

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

115 

116 
lemma JN_cong [cong]: 

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

120 

13798  121 
subsection{*Algebraic laws*} 
13792  122 

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

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

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

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

135 
apply (simp_all (no_asm) add: insert_absorb) 

136 
done 

137 

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

141 
apply (simp_all (no_asm) add: insert_absorb) 

142 
done 

143 

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

147 
done 

148 

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

152 
done 

153 

154 
(*Join is an ACoperator*) 

155 
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute 

156 

157 

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

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

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

13819  164 
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  165 
by (auto intro!: program_equalityI) 
166 

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

170 
lemma JN_Join_distrib: 

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

174 
lemma JN_Join_miniscope: 

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

178 
(*Used to prove guarantees_JN_I*) 

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

182 
done 

183 

184 

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

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

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

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

194 
lemma Join_constrains [simp]: 

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

198 
lemma Join_unless [simp]: 

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

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

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

206 

207 
lemma Join_constrains_weaken: 

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

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

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

218 
done 

219 

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

223 
lemma invariant_JN_I: 

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

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

228 
lemma Join_stable [simp]: 

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

233 
lemma Join_increasing [simp]: 

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

238 
lemma invariant_JoinI: 

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

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

246 

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

249 
lemma JN_transient: 

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

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

254 
lemma Join_transient [simp]: 

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

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

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

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

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

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

272 
lemma Join_ensures: 

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

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

278 
lemma stable_Join_constrains: 

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

283 
done 

284 

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

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

291 
done 

292 

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

294 
lemma stable_Join_Always2: 

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

298 
done 

299 

300 
lemma stable_Join_ensures1: 

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

304 
apply (erule constrains_weaken, auto) 

305 
done 

306 

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

308 
lemma stable_Join_ensures2: 

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

312 
done 

313 

314 

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

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

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

318 
by (simp add: ok_def) 
13792  319 

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

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

321 
by (simp add: ok_def) 
13792  322 

323 
lemma ok_Join_commute: 

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

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

328 
by (auto simp add: ok_def) 

329 

330 
lemmas ok_sym = ok_commute [THEN iffD1, standard] 

331 

332 
lemma ok_iff_OK: 

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

336 
apply blast 

337 
done 

13792  338 

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

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

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

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

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

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

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

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

361 

13798  362 
subsection{*Allowed*} 
13792  363 

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

365 
by (auto simp add: Allowed_def) 

366 

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

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

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

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

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

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

382 
lemma safety_prop_Acts_iff: 

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

386 
lemma safety_prop_AllowedActs_iff_Allowed: 

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

390 
lemma Allowed_eq: 

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

392 
by (simp add: Allowed_def safety_prop_Acts_iff) 

393 

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

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

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

399 
by (simp add: stable_def) 

400 

401 
lemma safety_prop_Int [simp]: 

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

405 
lemma safety_prop_INTER1 [simp]: 

13805  406 
"(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)" 
13792  407 
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

408 

13792  409 
lemma safety_prop_INTER [simp]: 
13805  410 
"(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)" 
13792  411 
by (auto simp add: safety_prop_def, blast) 
412 

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

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

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

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

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

417 

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

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

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

420 

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

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

422 
"[ 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

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

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

425 

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

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

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

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

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

434 

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

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

437 

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

438 
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

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

440 

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

441 
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

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

443 

5252  444 
end 