author | wenzelm |
Sat, 14 Jun 2008 23:19:51 +0200 | |
changeset 27208 | 5fe899199f85 |
parent 24147 | edc90be09ac1 |
child 32960 | 69916a850301 |
permissions | -rw-r--r-- |
24147 | 1 |
(* Title: HOL/UNITY/Project.thy |
7630 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Projections of state sets (also of actions and programs) |
|
7 |
||
8 |
Inheritance of GUARANTEES properties under extension |
|
9 |
*) |
|
10 |
||
13798 | 11 |
header{*Projections of State Sets*} |
12 |
||
16417 | 13 |
theory Project imports Extend begin |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
14 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
15 |
constdefs |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
16 |
projecting :: "['c program => 'c set, 'a*'b => 'c, |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
17 |
'a program, 'c program set, 'a program set] => bool" |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
8055
diff
changeset
|
18 |
"projecting C h F X' X == |
13819 | 19 |
\<forall>G. extend h F\<squnion>G \<in> X' --> F\<squnion>project h (C G) G \<in> X" |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
20 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
8055
diff
changeset
|
21 |
extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7947
diff
changeset
|
22 |
'c program set, 'a program set] => bool" |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
8055
diff
changeset
|
23 |
"extending C h F Y' Y == |
13819 | 24 |
\<forall>G. extend h F ok G --> F\<squnion>project h (C G) G \<in> Y |
25 |
--> extend h F\<squnion>G \<in> Y'" |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
8055
diff
changeset
|
26 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
8055
diff
changeset
|
27 |
subset_closed :: "'a set set => bool" |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
28 |
"subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U" |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
29 |
|
13790 | 30 |
|
31 |
lemma (in Extend) project_extend_constrains_I: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
32 |
"F \<in> A co B ==> project h C (extend h F) \<in> A co B" |
13790 | 33 |
apply (auto simp add: extend_act_def project_act_def constrains_def) |
34 |
done |
|
35 |
||
36 |
||
13798 | 37 |
subsection{*Safety*} |
13790 | 38 |
|
39 |
(*used below to prove Join_project_ensures*) |
|
13798 | 40 |
lemma (in Extend) project_unless [rule_format]: |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
41 |
"[| G \<in> stable C; project h C G \<in> A unless B |] |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
42 |
==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)" |
13790 | 43 |
apply (simp add: unless_def project_constrains) |
44 |
apply (blast dest: stable_constrains_Int intro: constrains_weaken) |
|
45 |
done |
|
46 |
||
13819 | 47 |
(*Generalizes project_constrains to the program F\<squnion>project h C G |
13790 | 48 |
useful with guarantees reasoning*) |
49 |
lemma (in Extend) Join_project_constrains: |
|
13819 | 50 |
"(F\<squnion>project h C G \<in> A co B) = |
51 |
(extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) & |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
52 |
F \<in> A co B)" |
13790 | 53 |
apply (simp (no_asm) add: project_constrains) |
54 |
apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] |
|
55 |
dest: constrains_imp_subset) |
|
56 |
done |
|
57 |
||
58 |
(*The condition is required to prove the left-to-right direction |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
59 |
could weaken it to G \<in> (C \<inter> extend_set h A) co C*) |
13790 | 60 |
lemma (in Extend) Join_project_stable: |
13819 | 61 |
"extend h F\<squnion>G \<in> stable C |
62 |
==> (F\<squnion>project h C G \<in> stable A) = |
|
63 |
(extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) & |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
64 |
F \<in> stable A)" |
13790 | 65 |
apply (unfold stable_def) |
66 |
apply (simp only: Join_project_constrains) |
|
67 |
apply (blast intro: constrains_weaken dest: constrains_Int) |
|
68 |
done |
|
69 |
||
70 |
(*For using project_guarantees in particular cases*) |
|
71 |
lemma (in Extend) project_constrains_I: |
|
13819 | 72 |
"extend h F\<squnion>G \<in> extend_set h A co extend_set h B |
73 |
==> F\<squnion>project h C G \<in> A co B" |
|
13790 | 74 |
apply (simp add: project_constrains extend_constrains) |
75 |
apply (blast intro: constrains_weaken dest: constrains_imp_subset) |
|
76 |
done |
|
77 |
||
78 |
lemma (in Extend) project_increasing_I: |
|
13819 | 79 |
"extend h F\<squnion>G \<in> increasing (func o f) |
80 |
==> F\<squnion>project h C G \<in> increasing func" |
|
13790 | 81 |
apply (unfold increasing_def stable_def) |
82 |
apply (simp del: Join_constrains |
|
83 |
add: project_constrains_I extend_set_eq_Collect) |
|
84 |
done |
|
85 |
||
86 |
lemma (in Extend) Join_project_increasing: |
|
13819 | 87 |
"(F\<squnion>project h UNIV G \<in> increasing func) = |
88 |
(extend h F\<squnion>G \<in> increasing (func o f))" |
|
13790 | 89 |
apply (rule iffI) |
90 |
apply (erule_tac [2] project_increasing_I) |
|
91 |
apply (simp del: Join_stable |
|
92 |
add: increasing_def Join_project_stable) |
|
93 |
apply (auto simp add: extend_set_eq_Collect extend_stable [THEN iffD1]) |
|
94 |
done |
|
95 |
||
96 |
(*The UNIV argument is essential*) |
|
97 |
lemma (in Extend) project_constrains_D: |
|
13819 | 98 |
"F\<squnion>project h UNIV G \<in> A co B |
99 |
==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B" |
|
13790 | 100 |
by (simp add: project_constrains extend_constrains) |
101 |
||
102 |
||
13798 | 103 |
subsection{*"projecting" and union/intersection (no converses)*} |
13790 | 104 |
|
105 |
lemma projecting_Int: |
|
106 |
"[| projecting C h F XA' XA; projecting C h F XB' XB |] |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
107 |
==> projecting C h F (XA' \<inter> XB') (XA \<inter> XB)" |
13790 | 108 |
by (unfold projecting_def, blast) |
109 |
||
110 |
lemma projecting_Un: |
|
111 |
"[| projecting C h F XA' XA; projecting C h F XB' XB |] |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
112 |
==> projecting C h F (XA' \<union> XB') (XA \<union> XB)" |
13790 | 113 |
by (unfold projecting_def, blast) |
114 |
||
115 |
lemma projecting_INT: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
116 |
"[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |] |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
117 |
==> projecting C h F (\<Inter>i \<in> I. X' i) (\<Inter>i \<in> I. X i)" |
13790 | 118 |
by (unfold projecting_def, blast) |
119 |
||
120 |
lemma projecting_UN: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
121 |
"[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |] |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
122 |
==> projecting C h F (\<Union>i \<in> I. X' i) (\<Union>i \<in> I. X i)" |
13790 | 123 |
by (unfold projecting_def, blast) |
124 |
||
125 |
lemma projecting_weaken: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
126 |
"[| projecting C h F X' X; U'<=X'; X \<subseteq> U |] ==> projecting C h F U' U" |
13790 | 127 |
by (unfold projecting_def, auto) |
128 |
||
129 |
lemma projecting_weaken_L: |
|
130 |
"[| projecting C h F X' X; U'<=X' |] ==> projecting C h F U' X" |
|
131 |
by (unfold projecting_def, auto) |
|
132 |
||
133 |
lemma extending_Int: |
|
134 |
"[| extending C h F YA' YA; extending C h F YB' YB |] |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
135 |
==> extending C h F (YA' \<inter> YB') (YA \<inter> YB)" |
13790 | 136 |
by (unfold extending_def, blast) |
137 |
||
138 |
lemma extending_Un: |
|
139 |
"[| extending C h F YA' YA; extending C h F YB' YB |] |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
140 |
==> extending C h F (YA' \<union> YB') (YA \<union> YB)" |
13790 | 141 |
by (unfold extending_def, blast) |
142 |
||
143 |
lemma extending_INT: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
144 |
"[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |] |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
145 |
==> extending C h F (\<Inter>i \<in> I. Y' i) (\<Inter>i \<in> I. Y i)" |
13790 | 146 |
by (unfold extending_def, blast) |
147 |
||
148 |
lemma extending_UN: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
149 |
"[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |] |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
150 |
==> extending C h F (\<Union>i \<in> I. Y' i) (\<Union>i \<in> I. Y i)" |
13790 | 151 |
by (unfold extending_def, blast) |
152 |
||
153 |
lemma extending_weaken: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
154 |
"[| extending C h F Y' Y; Y'<=V'; V \<subseteq> Y |] ==> extending C h F V' V" |
13790 | 155 |
by (unfold extending_def, auto) |
156 |
||
157 |
lemma extending_weaken_L: |
|
158 |
"[| extending C h F Y' Y; Y'<=V' |] ==> extending C h F V' Y" |
|
159 |
by (unfold extending_def, auto) |
|
160 |
||
161 |
lemma projecting_UNIV: "projecting C h F X' UNIV" |
|
162 |
by (simp add: projecting_def) |
|
163 |
||
164 |
lemma (in Extend) projecting_constrains: |
|
165 |
"projecting C h F (extend_set h A co extend_set h B) (A co B)" |
|
166 |
apply (unfold projecting_def) |
|
167 |
apply (blast intro: project_constrains_I) |
|
168 |
done |
|
169 |
||
170 |
lemma (in Extend) projecting_stable: |
|
171 |
"projecting C h F (stable (extend_set h A)) (stable A)" |
|
172 |
apply (unfold stable_def) |
|
173 |
apply (rule projecting_constrains) |
|
174 |
done |
|
175 |
||
176 |
lemma (in Extend) projecting_increasing: |
|
177 |
"projecting C h F (increasing (func o f)) (increasing func)" |
|
178 |
apply (unfold projecting_def) |
|
179 |
apply (blast intro: project_increasing_I) |
|
180 |
done |
|
181 |
||
182 |
lemma (in Extend) extending_UNIV: "extending C h F UNIV Y" |
|
183 |
apply (simp (no_asm) add: extending_def) |
|
184 |
done |
|
185 |
||
186 |
lemma (in Extend) extending_constrains: |
|
187 |
"extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)" |
|
188 |
apply (unfold extending_def) |
|
189 |
apply (blast intro: project_constrains_D) |
|
190 |
done |
|
191 |
||
192 |
lemma (in Extend) extending_stable: |
|
193 |
"extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)" |
|
194 |
apply (unfold stable_def) |
|
195 |
apply (rule extending_constrains) |
|
196 |
done |
|
197 |
||
198 |
lemma (in Extend) extending_increasing: |
|
199 |
"extending (%G. UNIV) h F (increasing (func o f)) (increasing func)" |
|
200 |
by (force simp only: extending_def Join_project_increasing) |
|
201 |
||
202 |
||
13798 | 203 |
subsection{*Reachability and project*} |
13790 | 204 |
|
205 |
(*In practice, C = reachable(...): the inclusion is equality*) |
|
206 |
lemma (in Extend) reachable_imp_reachable_project: |
|
13819 | 207 |
"[| reachable (extend h F\<squnion>G) \<subseteq> C; |
208 |
z \<in> reachable (extend h F\<squnion>G) |] |
|
209 |
==> f z \<in> reachable (F\<squnion>project h C G)" |
|
13790 | 210 |
apply (erule reachable.induct) |
211 |
apply (force intro!: reachable.Init simp add: split_extended_all, auto) |
|
212 |
apply (rule_tac act = x in reachable.Acts) |
|
213 |
apply auto |
|
214 |
apply (erule extend_act_D) |
|
215 |
apply (rule_tac act1 = "Restrict C act" |
|
216 |
in project_act_I [THEN [3] reachable.Acts], auto) |
|
217 |
done |
|
218 |
||
219 |
lemma (in Extend) project_Constrains_D: |
|
13819 | 220 |
"F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B |
221 |
==> extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)" |
|
13790 | 222 |
apply (unfold Constrains_def) |
223 |
apply (simp del: Join_constrains |
|
224 |
add: Join_project_constrains, clarify) |
|
225 |
apply (erule constrains_weaken) |
|
226 |
apply (auto intro: reachable_imp_reachable_project) |
|
227 |
done |
|
228 |
||
229 |
lemma (in Extend) project_Stable_D: |
|
13819 | 230 |
"F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A |
231 |
==> extend h F\<squnion>G \<in> Stable (extend_set h A)" |
|
13790 | 232 |
apply (unfold Stable_def) |
233 |
apply (simp (no_asm_simp) add: project_Constrains_D) |
|
234 |
done |
|
235 |
||
236 |
lemma (in Extend) project_Always_D: |
|
13819 | 237 |
"F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A |
238 |
==> extend h F\<squnion>G \<in> Always (extend_set h A)" |
|
13790 | 239 |
apply (unfold Always_def) |
240 |
apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all) |
|
241 |
done |
|
242 |
||
243 |
lemma (in Extend) project_Increasing_D: |
|
13819 | 244 |
"F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func |
245 |
==> extend h F\<squnion>G \<in> Increasing (func o f)" |
|
13790 | 246 |
apply (unfold Increasing_def, auto) |
247 |
apply (subst extend_set_eq_Collect [symmetric]) |
|
248 |
apply (simp (no_asm_simp) add: project_Stable_D) |
|
249 |
done |
|
250 |
||
251 |
||
13798 | 252 |
subsection{*Converse results for weak safety: benefits of the argument C *} |
13790 | 253 |
|
254 |
(*In practice, C = reachable(...): the inclusion is equality*) |
|
255 |
lemma (in Extend) reachable_project_imp_reachable: |
|
13819 | 256 |
"[| C \<subseteq> reachable(extend h F\<squnion>G); |
257 |
x \<in> reachable (F\<squnion>project h C G) |] |
|
258 |
==> \<exists>y. h(x,y) \<in> reachable (extend h F\<squnion>G)" |
|
13790 | 259 |
apply (erule reachable.induct) |
260 |
apply (force intro: reachable.Init) |
|
261 |
apply (auto simp add: project_act_def) |
|
262 |
apply (force del: Id_in_Acts intro: reachable.Acts extend_act_D)+ |
|
263 |
done |
|
264 |
||
265 |
lemma (in Extend) project_set_reachable_extend_eq: |
|
13819 | 266 |
"project_set h (reachable (extend h F\<squnion>G)) = |
267 |
reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)" |
|
13790 | 268 |
by (auto dest: subset_refl [THEN reachable_imp_reachable_project] |
269 |
subset_refl [THEN reachable_project_imp_reachable]) |
|
270 |
||
271 |
(*UNUSED*) |
|
272 |
lemma (in Extend) reachable_extend_Join_subset: |
|
13819 | 273 |
"reachable (extend h F\<squnion>G) \<subseteq> C |
274 |
==> reachable (extend h F\<squnion>G) \<subseteq> |
|
275 |
extend_set h (reachable (F\<squnion>project h C G))" |
|
13790 | 276 |
apply (auto dest: reachable_imp_reachable_project) |
277 |
done |
|
278 |
||
279 |
lemma (in Extend) project_Constrains_I: |
|
13819 | 280 |
"extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B) |
281 |
==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B" |
|
13790 | 282 |
apply (unfold Constrains_def) |
283 |
apply (simp del: Join_constrains |
|
284 |
add: Join_project_constrains extend_set_Int_distrib) |
|
285 |
apply (rule conjI) |
|
286 |
prefer 2 |
|
287 |
apply (force elim: constrains_weaken_L |
|
288 |
dest!: extend_constrains_project_set |
|
289 |
subset_refl [THEN reachable_project_imp_reachable]) |
|
290 |
apply (blast intro: constrains_weaken_L) |
|
291 |
done |
|
292 |
||
293 |
lemma (in Extend) project_Stable_I: |
|
13819 | 294 |
"extend h F\<squnion>G \<in> Stable (extend_set h A) |
295 |
==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A" |
|
13790 | 296 |
apply (unfold Stable_def) |
297 |
apply (simp (no_asm_simp) add: project_Constrains_I) |
|
298 |
done |
|
299 |
||
300 |
lemma (in Extend) project_Always_I: |
|
13819 | 301 |
"extend h F\<squnion>G \<in> Always (extend_set h A) |
302 |
==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A" |
|
13790 | 303 |
apply (unfold Always_def) |
304 |
apply (auto simp add: project_Stable_I) |
|
305 |
apply (unfold extend_set_def, blast) |
|
306 |
done |
|
307 |
||
308 |
lemma (in Extend) project_Increasing_I: |
|
13819 | 309 |
"extend h F\<squnion>G \<in> Increasing (func o f) |
310 |
==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func" |
|
13790 | 311 |
apply (unfold Increasing_def, auto) |
312 |
apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I) |
|
313 |
done |
|
314 |
||
315 |
lemma (in Extend) project_Constrains: |
|
13819 | 316 |
"(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B) = |
317 |
(extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))" |
|
13790 | 318 |
apply (blast intro: project_Constrains_I project_Constrains_D) |
319 |
done |
|
320 |
||
321 |
lemma (in Extend) project_Stable: |
|
13819 | 322 |
"(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A) = |
323 |
(extend h F\<squnion>G \<in> Stable (extend_set h A))" |
|
13790 | 324 |
apply (unfold Stable_def) |
325 |
apply (rule project_Constrains) |
|
326 |
done |
|
327 |
||
328 |
lemma (in Extend) project_Increasing: |
|
13819 | 329 |
"(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func) = |
330 |
(extend h F\<squnion>G \<in> Increasing (func o f))" |
|
13790 | 331 |
apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect) |
332 |
done |
|
333 |
||
13798 | 334 |
subsection{*A lot of redundant theorems: all are proved to facilitate reasoning |
335 |
about guarantees.*} |
|
13790 | 336 |
|
337 |
lemma (in Extend) projecting_Constrains: |
|
13819 | 338 |
"projecting (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 339 |
(extend_set h A Co extend_set h B) (A Co B)" |
340 |
||
341 |
apply (unfold projecting_def) |
|
342 |
apply (blast intro: project_Constrains_I) |
|
343 |
done |
|
344 |
||
345 |
lemma (in Extend) projecting_Stable: |
|
13819 | 346 |
"projecting (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 347 |
(Stable (extend_set h A)) (Stable A)" |
348 |
apply (unfold Stable_def) |
|
349 |
apply (rule projecting_Constrains) |
|
350 |
done |
|
351 |
||
352 |
lemma (in Extend) projecting_Always: |
|
13819 | 353 |
"projecting (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 354 |
(Always (extend_set h A)) (Always A)" |
355 |
apply (unfold projecting_def) |
|
356 |
apply (blast intro: project_Always_I) |
|
357 |
done |
|
358 |
||
359 |
lemma (in Extend) projecting_Increasing: |
|
13819 | 360 |
"projecting (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 361 |
(Increasing (func o f)) (Increasing func)" |
362 |
apply (unfold projecting_def) |
|
363 |
apply (blast intro: project_Increasing_I) |
|
364 |
done |
|
365 |
||
366 |
lemma (in Extend) extending_Constrains: |
|
13819 | 367 |
"extending (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 368 |
(extend_set h A Co extend_set h B) (A Co B)" |
369 |
apply (unfold extending_def) |
|
370 |
apply (blast intro: project_Constrains_D) |
|
371 |
done |
|
372 |
||
373 |
lemma (in Extend) extending_Stable: |
|
13819 | 374 |
"extending (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 375 |
(Stable (extend_set h A)) (Stable A)" |
376 |
apply (unfold extending_def) |
|
377 |
apply (blast intro: project_Stable_D) |
|
378 |
done |
|
379 |
||
380 |
lemma (in Extend) extending_Always: |
|
13819 | 381 |
"extending (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 382 |
(Always (extend_set h A)) (Always A)" |
383 |
apply (unfold extending_def) |
|
384 |
apply (blast intro: project_Always_D) |
|
385 |
done |
|
386 |
||
387 |
lemma (in Extend) extending_Increasing: |
|
13819 | 388 |
"extending (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 389 |
(Increasing (func o f)) (Increasing func)" |
390 |
apply (unfold extending_def) |
|
391 |
apply (blast intro: project_Increasing_D) |
|
392 |
done |
|
393 |
||
394 |
||
13798 | 395 |
subsection{*leadsETo in the precondition (??)*} |
13790 | 396 |
|
13798 | 397 |
subsubsection{*transient*} |
13790 | 398 |
|
399 |
lemma (in Extend) transient_extend_set_imp_project_transient: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
400 |
"[| G \<in> transient (C \<inter> extend_set h A); G \<in> stable C |] |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
401 |
==> project h C G \<in> transient (project_set h C \<inter> A)" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
402 |
apply (auto simp add: transient_def Domain_project_act) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
403 |
apply (subgoal_tac "act `` (C \<inter> extend_set h A) \<subseteq> - extend_set h A") |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
404 |
prefer 2 |
13790 | 405 |
apply (simp add: stable_def constrains_def, blast) |
406 |
(*back to main goal*) |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
407 |
apply (erule_tac V = "?AA \<subseteq> -C \<union> ?BB" in thin_rl) |
13790 | 408 |
apply (drule bspec, assumption) |
409 |
apply (simp add: extend_set_def project_act_def, blast) |
|
410 |
done |
|
411 |
||
412 |
(*converse might hold too?*) |
|
413 |
lemma (in Extend) project_extend_transient_D: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
414 |
"project h C (extend h F) \<in> transient (project_set h C \<inter> D) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
415 |
==> F \<in> transient (project_set h C \<inter> D)" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
416 |
apply (simp add: transient_def Domain_project_act, safe) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
417 |
apply blast+ |
13790 | 418 |
done |
419 |
||
420 |
||
13798 | 421 |
subsubsection{*ensures -- a primitive combining progress with safety*} |
13790 | 422 |
|
423 |
(*Used to prove project_leadsETo_I*) |
|
424 |
lemma (in Extend) ensures_extend_set_imp_project_ensures: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
425 |
"[| extend h F \<in> stable C; G \<in> stable C; |
13819 | 426 |
extend h F\<squnion>G \<in> A ensures B; A-B = C \<inter> extend_set h D |] |
427 |
==> F\<squnion>project h C G |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
428 |
\<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
429 |
apply (simp add: ensures_def project_constrains Join_transient extend_transient, |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
430 |
clarify) |
13790 | 431 |
apply (intro conjI) |
432 |
(*first subgoal*) |
|
433 |
apply (blast intro: extend_stable_project_set |
|
434 |
[THEN stableD, THEN constrains_Int, THEN constrains_weaken] |
|
435 |
dest!: extend_constrains_project_set equalityD1) |
|
436 |
(*2nd subgoal*) |
|
437 |
apply (erule stableD [THEN constrains_Int, THEN constrains_weaken]) |
|
438 |
apply assumption |
|
439 |
apply (simp (no_asm_use) add: extend_set_def) |
|
440 |
apply blast |
|
441 |
apply (simp add: extend_set_Int_distrib extend_set_Un_distrib) |
|
442 |
apply (blast intro!: extend_set_project_set [THEN subsetD], blast) |
|
443 |
(*The transient part*) |
|
444 |
apply auto |
|
445 |
prefer 2 |
|
446 |
apply (force dest!: equalityD1 |
|
447 |
intro: transient_extend_set_imp_project_transient |
|
448 |
[THEN transient_strengthen]) |
|
449 |
apply (simp (no_asm_use) add: Int_Diff) |
|
450 |
apply (force dest!: equalityD1 |
|
451 |
intro: transient_extend_set_imp_project_transient |
|
452 |
[THEN project_extend_transient_D, THEN transient_strengthen]) |
|
453 |
done |
|
454 |
||
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
455 |
text{*Transferring a transient property upwards*} |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
456 |
lemma (in Extend) project_transient_extend_set: |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
457 |
"project h C G \<in> transient (project_set h C \<inter> A - B) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
458 |
==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
459 |
apply (simp add: transient_def project_set_def extend_set_def project_act_def) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
460 |
apply (elim disjE bexE) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
461 |
apply (rule_tac x=Id in bexI) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
462 |
apply (blast intro!: rev_bexI )+ |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
463 |
done |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
464 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
465 |
lemma (in Extend) project_unless2 [rule_format]: |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
466 |
"[| G \<in> stable C; project h C G \<in> (project_set h C \<inter> A) unless B |] |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
467 |
==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
468 |
by (auto dest: stable_constrains_Int intro: constrains_weaken |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
469 |
simp add: unless_def project_constrains Diff_eq Int_assoc |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
470 |
Int_extend_set_lemma) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
471 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
472 |
|
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
473 |
lemma (in Extend) extend_unless: |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
474 |
"[|extend h F \<in> stable C; F \<in> A unless B|] |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
475 |
==> extend h F \<in> C \<inter> extend_set h A unless extend_set h B" |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
476 |
apply (simp add: unless_def stable_def) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
477 |
apply (drule constrains_Int) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
478 |
apply (erule extend_constrains [THEN iffD2]) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
479 |
apply (erule constrains_weaken, blast) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
480 |
apply blast |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
481 |
done |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
482 |
|
13790 | 483 |
(*Used to prove project_leadsETo_D*) |
13798 | 484 |
lemma (in Extend) Join_project_ensures [rule_format]: |
13819 | 485 |
"[| extend h F\<squnion>G \<in> stable C; |
486 |
F\<squnion>project h C G \<in> A ensures B |] |
|
487 |
==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)" |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
488 |
apply (auto simp add: ensures_eq extend_unless project_unless) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
489 |
apply (blast intro: extend_transient [THEN iffD2] transient_strengthen) |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
490 |
apply (blast intro: project_transient_extend_set transient_strengthen) |
13790 | 491 |
done |
492 |
||
13798 | 493 |
text{*Lemma useful for both STRONG and WEAK progress, but the transient |
494 |
condition's very strong*} |
|
13790 | 495 |
|
496 |
(*The strange induction formula allows induction over the leadsTo |
|
497 |
assumption's non-atomic precondition*) |
|
498 |
lemma (in Extend) PLD_lemma: |
|
13819 | 499 |
"[| extend h F\<squnion>G \<in> stable C; |
500 |
F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |] |
|
501 |
==> extend h F\<squnion>G \<in> |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
502 |
C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)" |
13790 | 503 |
apply (erule leadsTo_induct) |
504 |
apply (blast intro: leadsTo_Basis Join_project_ensures) |
|
505 |
apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans) |
|
506 |
apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union) |
|
507 |
done |
|
508 |
||
509 |
lemma (in Extend) project_leadsTo_D_lemma: |
|
13819 | 510 |
"[| extend h F\<squnion>G \<in> stable C; |
511 |
F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |] |
|
512 |
==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)" |
|
13790 | 513 |
apply (rule PLD_lemma [THEN leadsTo_weaken]) |
514 |
apply (auto simp add: split_extended_all) |
|
515 |
done |
|
516 |
||
517 |
lemma (in Extend) Join_project_LeadsTo: |
|
13819 | 518 |
"[| C = (reachable (extend h F\<squnion>G)); |
519 |
F\<squnion>project h C G \<in> A LeadsTo B |] |
|
520 |
==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)" |
|
13790 | 521 |
by (simp del: Join_stable add: LeadsTo_def project_leadsTo_D_lemma |
522 |
project_set_reachable_extend_eq) |
|
523 |
||
524 |
||
13798 | 525 |
subsection{*Towards the theorem @{text project_Ensures_D}*} |
13790 | 526 |
|
527 |
lemma (in Extend) project_ensures_D_lemma: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
528 |
"[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B)); |
13819 | 529 |
F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B; |
530 |
extend h F\<squnion>G \<in> stable C |] |
|
531 |
==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)" |
|
13790 | 532 |
(*unless*) |
533 |
apply (auto intro!: project_unless2 [unfolded unless_def] |
|
534 |
intro: project_extend_constrains_I |
|
535 |
simp add: ensures_def) |
|
536 |
(*transient*) |
|
537 |
(*A G-action cannot occur*) |
|
538 |
prefer 2 |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
539 |
apply (blast intro: project_transient_extend_set) |
13790 | 540 |
(*An F-action*) |
541 |
apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen] |
|
542 |
simp add: split_extended_all) |
|
543 |
done |
|
544 |
||
545 |
lemma (in Extend) project_ensures_D: |
|
13819 | 546 |
"[| F\<squnion>project h UNIV G \<in> A ensures B; |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
547 |
G \<in> stable (extend_set h A - extend_set h B) |] |
13819 | 548 |
==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)" |
13790 | 549 |
apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto) |
550 |
done |
|
551 |
||
552 |
lemma (in Extend) project_Ensures_D: |
|
13819 | 553 |
"[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Ensures B; |
554 |
G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A - |
|
13790 | 555 |
extend_set h B) |] |
13819 | 556 |
==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)" |
13790 | 557 |
apply (unfold Ensures_def) |
558 |
apply (rule project_ensures_D_lemma [THEN revcut_rl]) |
|
559 |
apply (auto simp add: project_set_reachable_extend_eq [symmetric]) |
|
560 |
done |
|
561 |
||
562 |
||
13798 | 563 |
subsection{*Guarantees*} |
13790 | 564 |
|
565 |
lemma (in Extend) project_act_Restrict_subset_project_act: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
566 |
"project_act h (Restrict C act) \<subseteq> project_act h act" |
13790 | 567 |
apply (auto simp add: project_act_def) |
568 |
done |
|
569 |
||
570 |
||
571 |
lemma (in Extend) subset_closed_ok_extend_imp_ok_project: |
|
572 |
"[| extend h F ok G; subset_closed (AllowedActs F) |] |
|
573 |
==> F ok project h C G" |
|
574 |
apply (auto simp add: ok_def) |
|
575 |
apply (rename_tac act) |
|
576 |
apply (drule subsetD, blast) |
|
577 |
apply (rule_tac x = "Restrict C (extend_act h act)" in rev_image_eqI) |
|
578 |
apply simp + |
|
579 |
apply (cut_tac project_act_Restrict_subset_project_act) |
|
580 |
apply (auto simp add: subset_closed_def) |
|
581 |
done |
|
582 |
||
583 |
||
584 |
(*Weak precondition and postcondition |
|
585 |
Not clear that it has a converse [or that we want one!]*) |
|
586 |
||
587 |
(*The raw version; 3rd premise could be weakened by adding the |
|
13819 | 588 |
precondition extend h F\<squnion>G \<in> X' *) |
13790 | 589 |
lemma (in Extend) project_guarantees_raw: |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
590 |
assumes xguary: "F \<in> X guarantees Y" |
13790 | 591 |
and closed: "subset_closed (AllowedActs F)" |
13819 | 592 |
and project: "!!G. extend h F\<squnion>G \<in> X' |
593 |
==> F\<squnion>project h (C G) G \<in> X" |
|
594 |
and extend: "!!G. [| F\<squnion>project h (C G) G \<in> Y |] |
|
595 |
==> extend h F\<squnion>G \<in> Y'" |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
596 |
shows "extend h F \<in> X' guarantees Y'" |
13790 | 597 |
apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI]) |
598 |
apply (blast intro: closed subset_closed_ok_extend_imp_ok_project) |
|
599 |
apply (erule project) |
|
600 |
done |
|
601 |
||
602 |
lemma (in Extend) project_guarantees: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
603 |
"[| F \<in> X guarantees Y; subset_closed (AllowedActs F); |
13790 | 604 |
projecting C h F X' X; extending C h F Y' Y |] |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
605 |
==> extend h F \<in> X' guarantees Y'" |
13790 | 606 |
apply (rule guaranteesI) |
607 |
apply (auto simp add: guaranteesD projecting_def extending_def |
|
608 |
subset_closed_ok_extend_imp_ok_project) |
|
609 |
done |
|
610 |
||
611 |
||
612 |
(*It seems that neither "guarantees" law can be proved from the other.*) |
|
613 |
||
614 |
||
13798 | 615 |
subsection{*guarantees corollaries*} |
13790 | 616 |
|
13798 | 617 |
subsubsection{*Some could be deleted: the required versions are easy to prove*} |
13790 | 618 |
|
619 |
lemma (in Extend) extend_guar_increasing: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
620 |
"[| F \<in> UNIV guarantees increasing func; |
13790 | 621 |
subset_closed (AllowedActs F) |] |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
622 |
==> extend h F \<in> X' guarantees increasing (func o f)" |
13790 | 623 |
apply (erule project_guarantees) |
624 |
apply (rule_tac [3] extending_increasing) |
|
625 |
apply (rule_tac [2] projecting_UNIV, auto) |
|
626 |
done |
|
627 |
||
628 |
lemma (in Extend) extend_guar_Increasing: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
629 |
"[| F \<in> UNIV guarantees Increasing func; |
13790 | 630 |
subset_closed (AllowedActs F) |] |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
631 |
==> extend h F \<in> X' guarantees Increasing (func o f)" |
13790 | 632 |
apply (erule project_guarantees) |
633 |
apply (rule_tac [3] extending_Increasing) |
|
634 |
apply (rule_tac [2] projecting_UNIV, auto) |
|
635 |
done |
|
636 |
||
637 |
lemma (in Extend) extend_guar_Always: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
638 |
"[| F \<in> Always A guarantees Always B; |
13790 | 639 |
subset_closed (AllowedActs F) |] |
640 |
==> extend h F |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
641 |
\<in> Always(extend_set h A) guarantees Always(extend_set h B)" |
13790 | 642 |
apply (erule project_guarantees) |
643 |
apply (rule_tac [3] extending_Always) |
|
644 |
apply (rule_tac [2] projecting_Always, auto) |
|
645 |
done |
|
646 |
||
647 |
||
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
648 |
subsubsection{*Guarantees with a leadsTo postcondition*} |
13790 | 649 |
|
650 |
lemma (in Extend) project_leadsTo_D: |
|
13819 | 651 |
"F\<squnion>project h UNIV G \<in> A leadsTo B |
652 |
==> extend h F\<squnion>G \<in> (extend_set h A) leadsTo (extend_set h B)" |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
653 |
apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto) |
13790 | 654 |
done |
655 |
||
656 |
lemma (in Extend) project_LeadsTo_D: |
|
13819 | 657 |
"F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A LeadsTo B |
658 |
==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)" |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
659 |
apply (rule refl [THEN Join_project_LeadsTo], auto) |
13790 | 660 |
done |
661 |
||
662 |
lemma (in Extend) extending_leadsTo: |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
663 |
"extending (%G. UNIV) h F |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
664 |
(extend_set h A leadsTo extend_set h B) (A leadsTo B)" |
13790 | 665 |
apply (unfold extending_def) |
666 |
apply (blast intro: project_leadsTo_D) |
|
667 |
done |
|
668 |
||
669 |
lemma (in Extend) extending_LeadsTo: |
|
13819 | 670 |
"extending (%G. reachable (extend h F\<squnion>G)) h F |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
671 |
(extend_set h A LeadsTo extend_set h B) (A LeadsTo B)" |
13790 | 672 |
apply (unfold extending_def) |
673 |
apply (blast intro: project_LeadsTo_D) |
|
674 |
done |
|
675 |
||
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
676 |
end |