author | wenzelm |
Mon, 08 Feb 2010 21:28:27 +0100 | |
changeset 35054 | a5db9779b026 |
parent 32960 | 69916a850301 |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 |
|
13798 | 8 |
header{*Weak Safety*} |
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 |
|
23767 | 22 |
| Acts: "[| act: acts; (s,evs) \<in> traces init acts; (s,s'): act |] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 |
|
23767 | 32 |
| Acts: "[| act: Acts F; s \<in> reachable F; (s,s'): act |] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23767
diff
changeset
|
33 |
==> s' \<in> reachable F" |
6536 | 34 |
|
13797 | 35 |
constdefs |
36 |
Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) |
|
13805 | 37 |
"A Co B == {F. F \<in> (reachable F \<inter> A) co B}" |
6536 | 38 |
|
13797 | 39 |
Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) |
13805 | 40 |
"A Unless B == (A-B) Co (A \<union> B)" |
6536 | 41 |
|
5648 | 42 |
Stable :: "'a set => 'a program set" |
6536 | 43 |
"Stable A == A Co A" |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
44 |
|
6570 | 45 |
(*Always is the weak form of "invariant"*) |
46 |
Always :: "'a set => 'a program set" |
|
13805 | 47 |
"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
|
48 |
|
13805 | 49 |
(*Polymorphic in both states and the meaning of \<le> *) |
6705 | 50 |
Increasing :: "['a => 'b::{order}] => 'a program set" |
13805 | 51 |
"Increasing f == \<Inter>z. Stable {s. z \<le> f s}" |
5784 | 52 |
|
13797 | 53 |
|
13798 | 54 |
subsection{*traces and reachable*} |
13797 | 55 |
|
56 |
lemma reachable_equiv_traces: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
57 |
"reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}" |
13797 | 58 |
apply safe |
59 |
apply (erule_tac [2] traces.induct) |
|
60 |
apply (erule reachable.induct) |
|
61 |
apply (blast intro: reachable.intros traces.intros)+ |
|
62 |
done |
|
63 |
||
13805 | 64 |
lemma Init_subset_reachable: "Init F \<subseteq> reachable F" |
13797 | 65 |
by (blast intro: reachable.intros) |
66 |
||
67 |
lemma stable_reachable [intro!,simp]: |
|
13805 | 68 |
"Acts G \<subseteq> Acts F ==> G \<in> stable (reachable F)" |
13797 | 69 |
by (blast intro: stableI constrainsI reachable.intros) |
70 |
||
71 |
(*The set of all reachable states is an invariant...*) |
|
13805 | 72 |
lemma invariant_reachable: "F \<in> invariant (reachable F)" |
13797 | 73 |
apply (simp add: invariant_def) |
74 |
apply (blast intro: reachable.intros) |
|
75 |
done |
|
76 |
||
77 |
(*...in fact the strongest invariant!*) |
|
13805 | 78 |
lemma invariant_includes_reachable: "F \<in> invariant A ==> reachable F \<subseteq> A" |
13797 | 79 |
apply (simp add: stable_def constrains_def invariant_def) |
80 |
apply (rule subsetI) |
|
81 |
apply (erule reachable.induct) |
|
82 |
apply (blast intro: reachable.intros)+ |
|
83 |
done |
|
84 |
||
85 |
||
13798 | 86 |
subsection{*Co*} |
13797 | 87 |
|
13805 | 88 |
(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*) |
13797 | 89 |
lemmas constrains_reachable_Int = |
90 |
subset_refl [THEN stable_reachable [unfolded stable_def], |
|
91 |
THEN constrains_Int, standard] |
|
92 |
||
93 |
(*Resembles the previous definition of Constrains*) |
|
94 |
lemma Constrains_eq_constrains: |
|
13805 | 95 |
"A Co B = {F. F \<in> (reachable F \<inter> A) co (reachable F \<inter> B)}" |
13797 | 96 |
apply (unfold Constrains_def) |
97 |
apply (blast dest: constrains_reachable_Int intro: constrains_weaken) |
|
98 |
done |
|
99 |
||
13805 | 100 |
lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'" |
13797 | 101 |
apply (unfold Constrains_def) |
102 |
apply (blast intro: constrains_weaken_L) |
|
103 |
done |
|
104 |
||
13805 | 105 |
lemma stable_imp_Stable: "F \<in> stable A ==> F \<in> Stable A" |
13797 | 106 |
apply (unfold stable_def Stable_def) |
107 |
apply (erule constrains_imp_Constrains) |
|
108 |
done |
|
109 |
||
110 |
lemma ConstrainsI: |
|
13805 | 111 |
"(!!act s s'. [| act: Acts F; (s,s') \<in> act; s \<in> A |] ==> s': A') |
112 |
==> F \<in> A Co A'" |
|
13797 | 113 |
apply (rule constrains_imp_Constrains) |
114 |
apply (blast intro: constrainsI) |
|
115 |
done |
|
116 |
||
13805 | 117 |
lemma Constrains_empty [iff]: "F \<in> {} Co B" |
13797 | 118 |
by (unfold Constrains_def constrains_def, blast) |
119 |
||
13805 | 120 |
lemma Constrains_UNIV [iff]: "F \<in> A Co UNIV" |
13797 | 121 |
by (blast intro: ConstrainsI) |
122 |
||
123 |
lemma Constrains_weaken_R: |
|
13805 | 124 |
"[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'" |
13797 | 125 |
apply (unfold Constrains_def) |
126 |
apply (blast intro: constrains_weaken_R) |
|
127 |
done |
|
128 |
||
129 |
lemma Constrains_weaken_L: |
|
13805 | 130 |
"[| F \<in> A Co A'; B \<subseteq> A |] ==> F \<in> B Co A'" |
13797 | 131 |
apply (unfold Constrains_def) |
132 |
apply (blast intro: constrains_weaken_L) |
|
133 |
done |
|
134 |
||
135 |
lemma Constrains_weaken: |
|
13805 | 136 |
"[| F \<in> A Co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B Co B'" |
13797 | 137 |
apply (unfold Constrains_def) |
138 |
apply (blast intro: constrains_weaken) |
|
139 |
done |
|
140 |
||
141 |
(** Union **) |
|
142 |
||
143 |
lemma Constrains_Un: |
|
13805 | 144 |
"[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<union> B) Co (A' \<union> B')" |
13797 | 145 |
apply (unfold Constrains_def) |
146 |
apply (blast intro: constrains_Un [THEN constrains_weaken]) |
|
147 |
done |
|
148 |
||
149 |
lemma Constrains_UN: |
|
13805 | 150 |
assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)" |
151 |
shows "F \<in> (\<Union>i \<in> I. A i) Co (\<Union>i \<in> I. A' i)" |
|
13797 | 152 |
apply (unfold Constrains_def) |
153 |
apply (rule CollectI) |
|
154 |
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, |
|
155 |
THEN constrains_weaken], auto) |
|
156 |
done |
|
157 |
||
158 |
(** Intersection **) |
|
159 |
||
160 |
lemma Constrains_Int: |
|
13805 | 161 |
"[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<inter> B) Co (A' \<inter> B')" |
13797 | 162 |
apply (unfold Constrains_def) |
163 |
apply (blast intro: constrains_Int [THEN constrains_weaken]) |
|
164 |
done |
|
165 |
||
166 |
lemma Constrains_INT: |
|
13805 | 167 |
assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)" |
168 |
shows "F \<in> (\<Inter>i \<in> I. A i) Co (\<Inter>i \<in> I. A' i)" |
|
13797 | 169 |
apply (unfold Constrains_def) |
170 |
apply (rule CollectI) |
|
171 |
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, |
|
172 |
THEN constrains_weaken], auto) |
|
173 |
done |
|
174 |
||
13805 | 175 |
lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable F \<inter> A \<subseteq> A'" |
13797 | 176 |
by (simp add: constrains_imp_subset Constrains_def) |
177 |
||
13805 | 178 |
lemma Constrains_trans: "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C" |
13797 | 179 |
apply (simp add: Constrains_eq_constrains) |
180 |
apply (blast intro: constrains_trans constrains_weaken) |
|
181 |
done |
|
182 |
||
183 |
lemma Constrains_cancel: |
|
13805 | 184 |
"[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')" |
13797 | 185 |
by (simp add: Constrains_eq_constrains constrains_def, blast) |
186 |
||
187 |
||
13798 | 188 |
subsection{*Stable*} |
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 |
||
13798 | 242 |
subsection{*Increasing*} |
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 |
||
265 |
lemmas Increasing_constant = |
|
266 |
increasing_constant [THEN increasing_imp_Increasing, standard, iff] |
|
267 |
||
268 |
||
13798 | 269 |
subsection{*The Elimination Theorem*} |
270 |
||
271 |
(*The "free" m has become universally quantified! Should the premise be !!m |
|
13805 | 272 |
instead of \<forall>m ? Would make it harder to use in forward proof.*) |
13797 | 273 |
|
274 |
lemma Elimination: |
|
13805 | 275 |
"[| \<forall>m. F \<in> {s. s x = m} Co (B m) |] |
276 |
==> F \<in> {s. s x \<in> M} Co (\<Union>m \<in> M. B m)" |
|
13797 | 277 |
by (unfold Constrains_def constrains_def, blast) |
278 |
||
279 |
(*As above, but for the trivial case of a one-variable state, in which the |
|
280 |
state is identified with its one variable.*) |
|
281 |
lemma Elimination_sing: |
|
13805 | 282 |
"(\<forall>m. F \<in> {m} Co (B m)) ==> F \<in> M Co (\<Union>m \<in> M. B m)" |
13797 | 283 |
by (unfold Constrains_def constrains_def, blast) |
284 |
||
285 |
||
13798 | 286 |
subsection{*Specialized laws for handling Always*} |
13797 | 287 |
|
288 |
(** Natural deduction rules for "Always A" **) |
|
289 |
||
13805 | 290 |
lemma AlwaysI: "[| Init F \<subseteq> A; F \<in> Stable A |] ==> F \<in> Always A" |
13797 | 291 |
by (simp add: Always_def) |
292 |
||
13805 | 293 |
lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A" |
13797 | 294 |
by (simp add: Always_def) |
295 |
||
296 |
lemmas AlwaysE = AlwaysD [THEN conjE, standard] |
|
297 |
lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard] |
|
298 |
||
299 |
||
300 |
(*The set of all reachable states is Always*) |
|
13805 | 301 |
lemma Always_includes_reachable: "F \<in> Always A ==> reachable F \<subseteq> A" |
13797 | 302 |
apply (simp add: Stable_def Constrains_def constrains_def Always_def) |
303 |
apply (rule subsetI) |
|
304 |
apply (erule reachable.induct) |
|
305 |
apply (blast intro: reachable.intros)+ |
|
306 |
done |
|
307 |
||
308 |
lemma invariant_imp_Always: |
|
13805 | 309 |
"F \<in> invariant A ==> F \<in> Always A" |
13797 | 310 |
apply (unfold Always_def invariant_def Stable_def stable_def) |
311 |
apply (blast intro: constrains_imp_Constrains) |
|
312 |
done |
|
313 |
||
314 |
lemmas Always_reachable = |
|
315 |
invariant_reachable [THEN invariant_imp_Always, standard] |
|
316 |
||
317 |
lemma Always_eq_invariant_reachable: |
|
13805 | 318 |
"Always A = {F. F \<in> invariant (reachable F \<inter> A)}" |
13797 | 319 |
apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains |
320 |
stable_def) |
|
321 |
apply (blast intro: reachable.intros) |
|
322 |
done |
|
323 |
||
324 |
(*the RHS is the traditional definition of the "always" operator*) |
|
13805 | 325 |
lemma Always_eq_includes_reachable: "Always A = {F. reachable F \<subseteq> A}" |
13797 | 326 |
by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable) |
327 |
||
328 |
lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV" |
|
329 |
by (auto simp add: Always_eq_includes_reachable) |
|
330 |
||
13805 | 331 |
lemma UNIV_AlwaysI: "UNIV \<subseteq> A ==> F \<in> Always A" |
13797 | 332 |
by (auto simp add: Always_eq_includes_reachable) |
333 |
||
13805 | 334 |
lemma Always_eq_UN_invariant: "Always A = (\<Union>I \<in> Pow A. invariant I)" |
13797 | 335 |
apply (simp add: Always_eq_includes_reachable) |
336 |
apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] |
|
337 |
invariant_includes_reachable [THEN subsetD]) |
|
338 |
done |
|
339 |
||
13805 | 340 |
lemma Always_weaken: "[| F \<in> Always A; A \<subseteq> B |] ==> F \<in> Always B" |
13797 | 341 |
by (auto simp add: Always_eq_includes_reachable) |
342 |
||
343 |
||
13798 | 344 |
subsection{*"Co" rules involving Always*} |
13797 | 345 |
|
346 |
lemma Always_Constrains_pre: |
|
13805 | 347 |
"F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')" |
13797 | 348 |
by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def |
349 |
Int_assoc [symmetric]) |
|
350 |
||
351 |
lemma Always_Constrains_post: |
|
13805 | 352 |
"F \<in> Always INV ==> (F \<in> A Co (INV \<inter> A')) = (F \<in> A Co A')" |
13797 | 353 |
by (simp add: Always_includes_reachable [THEN Int_absorb2] |
354 |
Constrains_eq_constrains Int_assoc [symmetric]) |
|
355 |
||
13805 | 356 |
(* [| F \<in> Always INV; F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *) |
13797 | 357 |
lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard] |
358 |
||
13805 | 359 |
(* [| F \<in> Always INV; F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *) |
13797 | 360 |
lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard] |
361 |
||
362 |
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) |
|
363 |
lemma Always_Constrains_weaken: |
|
13805 | 364 |
"[| F \<in> Always C; F \<in> A Co A'; |
365 |
C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |] |
|
366 |
==> F \<in> B Co B'" |
|
13797 | 367 |
apply (rule Always_ConstrainsI, assumption) |
368 |
apply (drule Always_ConstrainsD, assumption) |
|
369 |
apply (blast intro: Constrains_weaken) |
|
370 |
done |
|
371 |
||
372 |
||
373 |
(** Conjoining Always properties **) |
|
374 |
||
13805 | 375 |
lemma Always_Int_distrib: "Always (A \<inter> B) = Always A \<inter> Always B" |
13797 | 376 |
by (auto simp add: Always_eq_includes_reachable) |
377 |
||
13805 | 378 |
lemma Always_INT_distrib: "Always (INTER I A) = (\<Inter>i \<in> I. Always (A i))" |
13797 | 379 |
by (auto simp add: Always_eq_includes_reachable) |
380 |
||
381 |
lemma Always_Int_I: |
|
13805 | 382 |
"[| F \<in> Always A; F \<in> Always B |] ==> F \<in> Always (A \<inter> B)" |
13797 | 383 |
by (simp add: Always_Int_distrib) |
384 |
||
385 |
(*Allows a kind of "implication introduction"*) |
|
386 |
lemma Always_Compl_Un_eq: |
|
13805 | 387 |
"F \<in> Always A ==> (F \<in> Always (-A \<union> B)) = (F \<in> Always B)" |
13797 | 388 |
by (auto simp add: Always_eq_includes_reachable) |
389 |
||
390 |
(*Delete the nearest invariance assumption (which will be the second one |
|
391 |
used by Always_Int_I) *) |
|
13805 | 392 |
lemmas Always_thin = thin_rl [of "F \<in> Always A", standard] |
13797 | 393 |
|
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 |
subsection{*Totalize*} |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
396 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
397 |
lemma reachable_imp_reachable_tot: |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
398 |
"s \<in> reachable F ==> s \<in> reachable (totalize F)" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
399 |
apply (erule reachable.induct) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
400 |
apply (rule reachable.Init) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
401 |
apply simp |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
402 |
apply (rule_tac act = "totalize_act act" in reachable.Acts) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
403 |
apply (auto simp add: totalize_act_def) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
404 |
done |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
405 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
406 |
lemma reachable_tot_imp_reachable: |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
407 |
"s \<in> reachable (totalize F) ==> s \<in> reachable F" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
408 |
apply (erule reachable.induct) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
409 |
apply (rule reachable.Init, simp) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
410 |
apply (force simp add: totalize_act_def intro: reachable.Acts) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
411 |
done |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
412 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
413 |
lemma reachable_tot_eq [simp]: "reachable (totalize F) = reachable F" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
414 |
by (blast intro: reachable_imp_reachable_tot reachable_tot_imp_reachable) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
415 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
416 |
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
|
417 |
by (simp add: Constrains_def) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
418 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
419 |
lemma 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
|
420 |
by (simp add: Stable_def) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
421 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
422 |
lemma 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
|
423 |
by (simp add: Always_def) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
424 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
425 |
end |