author | huffman |
Thu, 18 Feb 2010 08:08:51 -0800 | |
changeset 35213 | b9866ad4e3be |
parent 35068 | 544867142ea4 |
child 35427 | ad039d29e01c |
permissions | -rw-r--r-- |
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 tab-width;
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 tab-width;
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 tab-width;
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 |
35054 | 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 |
35054 | 43 |
"JN x: A. B" == "CONST JOIN A (%x. B)" |
44 |
"JN x y. B" == "JN x. JN y. B" |
|
35068 | 45 |
"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
|
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) |
|
35054 | 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 AC-operator*) |
|
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> (A-B) 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> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) & |
275 |
(F \<in> transient (A-B) | G \<in> transient (A-B)))" |
|
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 tab-width;
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 |