author  wenzelm 
Sun, 20 May 2018 22:04:46 +0200  
changeset 68238  eb57621568bb 
parent 67613  ce654b0e6d69 
child 69313  b021008c5397 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23767
diff
changeset

1 
(* Title: HOL/UNITY/Constrains.thy 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

3 
Copyright 1998 University of Cambridge 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

4 

13797  5 
Weak safety relations: restricted to the set of reachable states. 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

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

7 

63146  8 
section\<open>Weak Safety\<close> 
13798  9 

16417  10 
theory Constrains imports UNITY begin 
6535  11 

12 
(*Initial states and program => (final state, reversed trace to it)... 

13 
Arguments MUST be curried in an inductive definition*) 

14 

23767  15 
inductive_set 
16 
traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" 

17 
for init :: "'a set" and acts :: "('a * 'a)set set" 

18 
where 

6535  19 
(*Initial trace is empty*) 
13805  20 
Init: "s \<in> init ==> (s,[]) \<in> traces init acts" 
6535  21 

67613  22 
 Acts: "[ act \<in> acts; (s,evs) \<in> traces init acts; (s,s') \<in> act ] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23767
diff
changeset

23 
==> (s', s#evs) \<in> traces init acts" 
6535  24 

25 

23767  26 
inductive_set 
27 
reachable :: "'a program => 'a set" 

28 
for F :: "'a program" 

29 
where 

13805  30 
Init: "s \<in> Init F ==> s \<in> reachable F" 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

31 

67613  32 
 Acts: "[ act \<in> Acts F; s \<in> reachable F; (s,s') \<in> act ] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23767
diff
changeset

33 
==> s' \<in> reachable F" 
6536  34 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

35 
definition Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) where 
13805  36 
"A Co B == {F. F \<in> (reachable F \<inter> A) co B}" 
6536  37 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

38 
definition Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) where 
13805  39 
"A Unless B == (AB) Co (A \<union> B)" 
6536  40 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

41 
definition Stable :: "'a set => 'a program set" where 
6536  42 
"Stable A == A Co A" 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

43 

6570  44 
(*Always is the weak form of "invariant"*) 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

45 
definition Always :: "'a set => 'a program set" where 
13805  46 
"Always A == {F. Init F \<subseteq> A} \<inter> Stable A" 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset

47 

13805  48 
(*Polymorphic in both states and the meaning of \<le> *) 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

49 
definition Increasing :: "['a => 'b::{order}] => 'a program set" where 
13805  50 
"Increasing f == \<Inter>z. Stable {s. z \<le> f s}" 
5784  51 

13797  52 

63146  53 
subsection\<open>traces and reachable\<close> 
13797  54 

55 
lemma reachable_equiv_traces: 

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

56 
"reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}" 
13797  57 
apply safe 
58 
apply (erule_tac [2] traces.induct) 

59 
apply (erule reachable.induct) 

60 
apply (blast intro: reachable.intros traces.intros)+ 

61 
done 

62 

13805  63 
lemma Init_subset_reachable: "Init F \<subseteq> reachable F" 
13797  64 
by (blast intro: reachable.intros) 
65 

66 
lemma stable_reachable [intro!,simp]: 

13805  67 
"Acts G \<subseteq> Acts F ==> G \<in> stable (reachable F)" 
13797  68 
by (blast intro: stableI constrainsI reachable.intros) 
69 

70 
(*The set of all reachable states is an invariant...*) 

13805  71 
lemma invariant_reachable: "F \<in> invariant (reachable F)" 
13797  72 
apply (simp add: invariant_def) 
73 
apply (blast intro: reachable.intros) 

74 
done 

75 

76 
(*...in fact the strongest invariant!*) 

13805  77 
lemma invariant_includes_reachable: "F \<in> invariant A ==> reachable F \<subseteq> A" 
13797  78 
apply (simp add: stable_def constrains_def invariant_def) 
79 
apply (rule subsetI) 

80 
apply (erule reachable.induct) 

81 
apply (blast intro: reachable.intros)+ 

82 
done 

83 

84 

63146  85 
subsection\<open>Co\<close> 
13797  86 

13805  87 
(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*) 
13797  88 
lemmas constrains_reachable_Int = 
45605  89 
subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int] 
13797  90 

91 
(*Resembles the previous definition of Constrains*) 

92 
lemma Constrains_eq_constrains: 

13805  93 
"A Co B = {F. F \<in> (reachable F \<inter> A) co (reachable F \<inter> B)}" 
13797  94 
apply (unfold Constrains_def) 
95 
apply (blast dest: constrains_reachable_Int intro: constrains_weaken) 

96 
done 

97 

13805  98 
lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'" 
13797  99 
apply (unfold Constrains_def) 
100 
apply (blast intro: constrains_weaken_L) 

101 
done 

102 

13805  103 
lemma stable_imp_Stable: "F \<in> stable A ==> F \<in> Stable A" 
13797  104 
apply (unfold stable_def Stable_def) 
105 
apply (erule constrains_imp_Constrains) 

106 
done 

107 

108 
lemma ConstrainsI: 

67613  109 
"(!!act s s'. [ act \<in> Acts F; (s,s') \<in> act; s \<in> A ] ==> s' \<in> A') 
13805  110 
==> F \<in> A Co A'" 
13797  111 
apply (rule constrains_imp_Constrains) 
112 
apply (blast intro: constrainsI) 

113 
done 

114 

13805  115 
lemma Constrains_empty [iff]: "F \<in> {} Co B" 
13797  116 
by (unfold Constrains_def constrains_def, blast) 
117 

13805  118 
lemma Constrains_UNIV [iff]: "F \<in> A Co UNIV" 
13797  119 
by (blast intro: ConstrainsI) 
120 

121 
lemma Constrains_weaken_R: 

13805  122 
"[ F \<in> A Co A'; A'<=B' ] ==> F \<in> A Co B'" 
13797  123 
apply (unfold Constrains_def) 
124 
apply (blast intro: constrains_weaken_R) 

125 
done 

126 

127 
lemma Constrains_weaken_L: 

13805  128 
"[ F \<in> A Co A'; B \<subseteq> A ] ==> F \<in> B Co A'" 
13797  129 
apply (unfold Constrains_def) 
130 
apply (blast intro: constrains_weaken_L) 

131 
done 

132 

133 
lemma Constrains_weaken: 

13805  134 
"[ F \<in> A Co A'; B \<subseteq> A; A'<=B' ] ==> F \<in> B Co B'" 
13797  135 
apply (unfold Constrains_def) 
136 
apply (blast intro: constrains_weaken) 

137 
done 

138 

139 
(** Union **) 

140 

141 
lemma Constrains_Un: 

13805  142 
"[ F \<in> A Co A'; F \<in> B Co B' ] ==> F \<in> (A \<union> B) Co (A' \<union> B')" 
13797  143 
apply (unfold Constrains_def) 
144 
apply (blast intro: constrains_Un [THEN constrains_weaken]) 

145 
done 

146 

147 
lemma Constrains_UN: 

13805  148 
assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)" 
149 
shows "F \<in> (\<Union>i \<in> I. A i) Co (\<Union>i \<in> I. A' i)" 

13797  150 
apply (unfold Constrains_def) 
151 
apply (rule CollectI) 

152 
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, 

153 
THEN constrains_weaken], auto) 

154 
done 

155 

156 
(** Intersection **) 

157 

158 
lemma Constrains_Int: 

13805  159 
"[ F \<in> A Co A'; F \<in> B Co B' ] ==> F \<in> (A \<inter> B) Co (A' \<inter> B')" 
13797  160 
apply (unfold Constrains_def) 
161 
apply (blast intro: constrains_Int [THEN constrains_weaken]) 

162 
done 

163 

164 
lemma Constrains_INT: 

13805  165 
assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)" 
166 
shows "F \<in> (\<Inter>i \<in> I. A i) Co (\<Inter>i \<in> I. A' i)" 

13797  167 
apply (unfold Constrains_def) 
168 
apply (rule CollectI) 

169 
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, 

170 
THEN constrains_weaken], auto) 

171 
done 

172 

13805  173 
lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable F \<inter> A \<subseteq> A'" 
13797  174 
by (simp add: constrains_imp_subset Constrains_def) 
175 

13805  176 
lemma Constrains_trans: "[ F \<in> A Co B; F \<in> B Co C ] ==> F \<in> A Co C" 
13797  177 
apply (simp add: Constrains_eq_constrains) 
178 
apply (blast intro: constrains_trans constrains_weaken) 

179 
done 

180 

181 
lemma Constrains_cancel: 

13805  182 
"[ F \<in> A Co (A' \<union> B); F \<in> B Co B' ] ==> F \<in> A Co (A' \<union> B')" 
44870  183 
apply (simp add: Constrains_eq_constrains constrains_def) 
184 
apply best 

185 
done 

13797  186 

187 

63146  188 
subsection\<open>Stable\<close> 
13797  189 

190 
(*Useful because there's no Stable_weaken. [Tanja Vos]*) 

13805  191 
lemma Stable_eq: "[ F \<in> Stable A; A = B ] ==> F \<in> Stable B" 
13797  192 
by blast 
193 

13805  194 
lemma Stable_eq_stable: "(F \<in> Stable A) = (F \<in> stable (reachable F \<inter> A))" 
13797  195 
by (simp add: Stable_def Constrains_eq_constrains stable_def) 
196 

13805  197 
lemma StableI: "F \<in> A Co A ==> F \<in> Stable A" 
13797  198 
by (unfold Stable_def, assumption) 
199 

13805  200 
lemma StableD: "F \<in> Stable A ==> F \<in> A Co A" 
13797  201 
by (unfold Stable_def, assumption) 
202 

203 
lemma Stable_Un: 

13805  204 
"[ F \<in> Stable A; F \<in> Stable A' ] ==> F \<in> Stable (A \<union> A')" 
13797  205 
apply (unfold Stable_def) 
206 
apply (blast intro: Constrains_Un) 

207 
done 

208 

209 
lemma Stable_Int: 

13805  210 
"[ F \<in> Stable A; F \<in> Stable A' ] ==> F \<in> Stable (A \<inter> A')" 
13797  211 
apply (unfold Stable_def) 
212 
apply (blast intro: Constrains_Int) 

213 
done 

214 

215 
lemma Stable_Constrains_Un: 

13805  216 
"[ F \<in> Stable C; F \<in> A Co (C \<union> A') ] 
217 
==> F \<in> (C \<union> A) Co (C \<union> A')" 

13797  218 
apply (unfold Stable_def) 
219 
apply (blast intro: Constrains_Un [THEN Constrains_weaken]) 

220 
done 

221 

222 
lemma Stable_Constrains_Int: 

13805  223 
"[ F \<in> Stable C; F \<in> (C \<inter> A) Co A' ] 
224 
==> F \<in> (C \<inter> A) Co (C \<inter> A')" 

13797  225 
apply (unfold Stable_def) 
226 
apply (blast intro: Constrains_Int [THEN Constrains_weaken]) 

227 
done 

228 

229 
lemma Stable_UN: 

13805  230 
"(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Union>i \<in> I. A i)" 
13797  231 
by (simp add: Stable_def Constrains_UN) 
232 

233 
lemma Stable_INT: 

13805  234 
"(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Inter>i \<in> I. A i)" 
13797  235 
by (simp add: Stable_def Constrains_INT) 
236 

13805  237 
lemma Stable_reachable: "F \<in> Stable (reachable F)" 
13797  238 
by (simp add: Stable_eq_stable) 
239 

240 

241 

63146  242 
subsection\<open>Increasing\<close> 
13797  243 

244 
lemma IncreasingD: 

13805  245 
"F \<in> Increasing f ==> F \<in> Stable {s. x \<le> f s}" 
13797  246 
by (unfold Increasing_def, blast) 
247 

248 
lemma mono_Increasing_o: 

13805  249 
"mono g ==> Increasing f \<subseteq> Increasing (g o f)" 
13797  250 
apply (simp add: Increasing_def Stable_def Constrains_def stable_def 
251 
constrains_def) 

252 
apply (blast intro: monoD order_trans) 

253 
done 

254 

255 
lemma strict_IncreasingD: 

13805  256 
"!!z::nat. F \<in> Increasing f ==> F \<in> Stable {s. z < f s}" 
13797  257 
by (simp add: Increasing_def Suc_le_eq [symmetric]) 
258 

259 
lemma increasing_imp_Increasing: 

13805  260 
"F \<in> increasing f ==> F \<in> Increasing f" 
13797  261 
apply (unfold increasing_def Increasing_def) 
262 
apply (blast intro: stable_imp_Stable) 

263 
done 

264 

45605  265 
lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff] 
13797  266 

267 

63146  268 
subsection\<open>The Elimination Theorem\<close> 
13798  269 

270 
(*The "free" m has become universally quantified! Should the premise be !!m 

13805  271 
instead of \<forall>m ? Would make it harder to use in forward proof.*) 
13797  272 

273 
lemma Elimination: 

13805  274 
"[ \<forall>m. F \<in> {s. s x = m} Co (B m) ] 
275 
==> F \<in> {s. s x \<in> M} Co (\<Union>m \<in> M. B m)" 

13797  276 
by (unfold Constrains_def constrains_def, blast) 
277 

278 
(*As above, but for the trivial case of a onevariable state, in which the 

279 
state is identified with its one variable.*) 

280 
lemma Elimination_sing: 

13805  281 
"(\<forall>m. F \<in> {m} Co (B m)) ==> F \<in> M Co (\<Union>m \<in> M. B m)" 
13797  282 
by (unfold Constrains_def constrains_def, blast) 
283 

284 

63146  285 
subsection\<open>Specialized laws for handling Always\<close> 
13797  286 

287 
(** Natural deduction rules for "Always A" **) 

288 

13805  289 
lemma AlwaysI: "[ Init F \<subseteq> A; F \<in> Stable A ] ==> F \<in> Always A" 
13797  290 
by (simp add: Always_def) 
291 

13805  292 
lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A" 
13797  293 
by (simp add: Always_def) 
294 

45605  295 
lemmas AlwaysE = AlwaysD [THEN conjE] 
296 
lemmas Always_imp_Stable = AlwaysD [THEN conjunct2] 

13797  297 

298 

299 
(*The set of all reachable states is Always*) 

13805  300 
lemma Always_includes_reachable: "F \<in> Always A ==> reachable F \<subseteq> A" 
13797  301 
apply (simp add: Stable_def Constrains_def constrains_def Always_def) 
302 
apply (rule subsetI) 

303 
apply (erule reachable.induct) 

304 
apply (blast intro: reachable.intros)+ 

305 
done 

306 

307 
lemma invariant_imp_Always: 

13805  308 
"F \<in> invariant A ==> F \<in> Always A" 
13797  309 
apply (unfold Always_def invariant_def Stable_def stable_def) 
310 
apply (blast intro: constrains_imp_Constrains) 

311 
done 

312 

45605  313 
lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always] 
13797  314 

315 
lemma Always_eq_invariant_reachable: 

13805  316 
"Always A = {F. F \<in> invariant (reachable F \<inter> A)}" 
13797  317 
apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains 
318 
stable_def) 

319 
apply (blast intro: reachable.intros) 

320 
done 

321 

322 
(*the RHS is the traditional definition of the "always" operator*) 

13805  323 
lemma Always_eq_includes_reachable: "Always A = {F. reachable F \<subseteq> A}" 
13797  324 
by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable) 
325 

326 
lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV" 

327 
by (auto simp add: Always_eq_includes_reachable) 

328 

13805  329 
lemma UNIV_AlwaysI: "UNIV \<subseteq> A ==> F \<in> Always A" 
13797  330 
by (auto simp add: Always_eq_includes_reachable) 
331 

13805  332 
lemma Always_eq_UN_invariant: "Always A = (\<Union>I \<in> Pow A. invariant I)" 
13797  333 
apply (simp add: Always_eq_includes_reachable) 
334 
apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] 

335 
invariant_includes_reachable [THEN subsetD]) 

336 
done 

337 

13805  338 
lemma Always_weaken: "[ F \<in> Always A; A \<subseteq> B ] ==> F \<in> Always B" 
13797  339 
by (auto simp add: Always_eq_includes_reachable) 
340 

341 

63146  342 
subsection\<open>"Co" rules involving Always\<close> 
13797  343 

344 
lemma Always_Constrains_pre: 

13805  345 
"F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')" 
13797  346 
by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def 
347 
Int_assoc [symmetric]) 

348 

349 
lemma Always_Constrains_post: 

13805  350 
"F \<in> Always INV ==> (F \<in> A Co (INV \<inter> A')) = (F \<in> A Co A')" 
13797  351 
by (simp add: Always_includes_reachable [THEN Int_absorb2] 
352 
Constrains_eq_constrains Int_assoc [symmetric]) 

353 

13805  354 
(* [ F \<in> Always INV; F \<in> (INV \<inter> A) Co A' ] ==> F \<in> A Co A' *) 
45605  355 
lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1] 
13797  356 

13805  357 
(* [ F \<in> Always INV; F \<in> A Co A' ] ==> F \<in> A Co (INV \<inter> A') *) 
45605  358 
lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2] 
13797  359 

360 
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) 

361 
lemma Always_Constrains_weaken: 

13805  362 
"[ F \<in> Always C; F \<in> A Co A'; 
363 
C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' ] 

364 
==> F \<in> B Co B'" 

13797  365 
apply (rule Always_ConstrainsI, assumption) 
366 
apply (drule Always_ConstrainsD, assumption) 

367 
apply (blast intro: Constrains_weaken) 

368 
done 

369 

370 

371 
(** Conjoining Always properties **) 

372 

13805  373 
lemma Always_Int_distrib: "Always (A \<inter> B) = Always A \<inter> Always B" 
13797  374 
by (auto simp add: Always_eq_includes_reachable) 
375 

13805  376 
lemma Always_INT_distrib: "Always (INTER I A) = (\<Inter>i \<in> I. Always (A i))" 
13797  377 
by (auto simp add: Always_eq_includes_reachable) 
378 

379 
lemma Always_Int_I: 

13805  380 
"[ F \<in> Always A; F \<in> Always B ] ==> F \<in> Always (A \<inter> B)" 
13797  381 
by (simp add: Always_Int_distrib) 
382 

383 
(*Allows a kind of "implication introduction"*) 

384 
lemma Always_Compl_Un_eq: 

13805  385 
"F \<in> Always A ==> (F \<in> Always (A \<union> B)) = (F \<in> Always B)" 
13797  386 
by (auto simp add: Always_eq_includes_reachable) 
387 

388 
(*Delete the nearest invariance assumption (which will be the second one 

389 
used by Always_Int_I) *) 

68238  390 
lemmas Always_thin = thin_rl [of "F \<in> Always A"] for F A 
13797  391 

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

392 

63146  393 
subsection\<open>Totalize\<close> 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

394 

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

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

396 
"s \<in> reachable F ==> s \<in> reachable (totalize F)" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

397 
apply (erule reachable.induct) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

398 
apply (rule reachable.Init) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

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

400 
apply (rule_tac act = "totalize_act act" in reachable.Acts) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

401 
apply (auto simp add: totalize_act_def) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

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

403 

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

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

405 
"s \<in> reachable (totalize F) ==> s \<in> reachable F" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

406 
apply (erule reachable.induct) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

407 
apply (rule reachable.Init, simp) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

408 
apply (force simp add: totalize_act_def intro: reachable.Acts) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

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

410 

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

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

412 
by (blast intro: reachable_imp_reachable_tot reachable_tot_imp_reachable) 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

413 

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

414 
lemma totalize_Constrains_iff [simp]: "(totalize F \<in> A Co B) = (F \<in> A Co B)" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

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

416 

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

417 
lemma totalize_Stable_iff [simp]: "(totalize F \<in> Stable A) = (F \<in> Stable A)" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

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

419 

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

420 
lemma totalize_Always_iff [simp]: "(totalize F \<in> Always A) = (F \<in> Always A)" 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset

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

422 

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

423 
end 