4776

1 
(* Title: HOL/UNITY/WFair


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1998 University of Cambridge


5 


6 
Weak Fairness versions of transient, ensures, leadsTo.


7 


8 
From Misra, "A Logic for Concurrent Programming", 1994


9 
*)


10 


11 
open WFair;


12 


13 
goal thy "Union(B) Int A = Union((%C. C Int A)``B)";


14 
by (Blast_tac 1);


15 
qed "Int_Union_Union";


16 


17 


18 
(*** transient ***)


19 


20 
goalw thy [stable_def, constrains_def, transient_def]


21 
"!!A. [ stable Acts A; transient Acts A ] ==> A = {}";


22 
by (Blast_tac 1);


23 
qed "stable_transient_empty";


24 


25 
goalw thy [transient_def]


26 
"!!A. [ transient Acts A; B<=A ] ==> transient Acts B";


27 
by (Clarify_tac 1);


28 
by (rtac bexI 1 THEN assume_tac 2);


29 
by (Blast_tac 1);


30 
qed "transient_strengthen";


31 


32 
goalw thy [transient_def]


33 
"!!A. [ act:Acts; A <= Domain act; act^^A <= Compl A ] \


34 
\ ==> transient Acts A";


35 
by (Blast_tac 1);


36 
qed "transient_mem";


37 


38 


39 
(*** ensures ***)


40 


41 
goalw thy [ensures_def]


42 
"!!Acts. [ constrains Acts (AB) (A Un B); transient Acts (AB) ] \


43 
\ ==> ensures Acts A B";


44 
by (Blast_tac 1);


45 
qed "ensuresI";


46 


47 
goalw thy [ensures_def]


48 
"!!Acts. ensures Acts A B \


49 
\ ==> constrains Acts (AB) (A Un B) & transient Acts (AB)";


50 
by (Blast_tac 1);


51 
qed "ensuresD";


52 


53 
(*The Lversion (precondition strengthening) doesn't hold for ENSURES*)


54 
goalw thy [ensures_def]


55 
"!!Acts. [ ensures Acts A A'; A'<=B' ] ==> ensures Acts A B'";


56 
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);


57 
qed "ensures_weaken_R";


58 


59 
goalw thy [ensures_def, constrains_def, transient_def]


60 
"!!Acts. Acts ~= {} ==> ensures Acts A UNIV";


61 
by (Asm_simp_tac 1); (*omitting this causes PROOF FAILED, even with Safe_tac*)


62 
by (Blast_tac 1);


63 
qed "ensures_UNIV";


64 


65 
goalw thy [ensures_def]


66 
"!!Acts. [ stable Acts C; \


67 
\ constrains Acts (C Int (A  A')) (A Un A'); \


68 
\ transient Acts (C Int (AA')) ] \


69 
\ ==> ensures Acts (C Int A) (C Int A')";


70 
by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,


71 
Diff_Int_distrib RS sym,


72 
stable_constrains_Int]) 1);


73 
qed "stable_ensures_Int";


74 


75 


76 
(*** leadsTo ***)


77 


78 
(*Synonyms for the theorems produced by the inductive defn package*)


79 
bind_thm ("leadsTo_Basis", leadsto.Basis);


80 
bind_thm ("leadsTo_Trans", leadsto.Trans);


81 


82 
goal thy "!!Acts. act: Acts ==> leadsTo Acts A UNIV";


83 
by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);


84 
qed "leadsTo_UNIV";


85 
Addsimps [leadsTo_UNIV];


86 


87 
(*Useful with cancellation, disjunction*)


88 
goal thy "!!Acts. leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'";


89 
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);


90 
qed "leadsTo_Un_duplicate";


91 


92 
goal thy "!!Acts. leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts A (A' Un C)";


93 
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);


94 
qed "leadsTo_Un_duplicate2";


95 


96 
(*The Union introduction rule as we should have liked to state it*)


97 
val prems = goal thy


98 
"(!!A. A : S ==> leadsTo Acts A B) ==> leadsTo Acts (Union S) B";


99 
by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);


100 
qed "leadsTo_Union";


101 


102 
val prems = goal thy


103 
"(!!i. i : I ==> leadsTo Acts (A i) B) ==> leadsTo Acts (UN i:I. A i) B";


104 
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);


105 
by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);


106 
qed "leadsTo_UN";


107 


108 
(*Binary union introduction rule*)


109 
goal thy


110 
"!!C. [ leadsTo Acts A C; leadsTo Acts B C ] ==> leadsTo Acts (A Un B) C";


111 
by (stac Un_eq_Union 1);


112 
by (blast_tac (claset() addIs [leadsTo_Union]) 1);


113 
qed "leadsTo_Un";


114 


115 


116 
(*The INDUCTION rule as we should have liked to state it*)


117 
val major::prems = goal thy


118 
"[ leadsTo Acts za zb; \


119 
\ !!A B. ensures Acts A B ==> P A B; \


120 
\ !!A B C. [ leadsTo Acts A B; P A B; leadsTo Acts B C; P B C ] \


121 
\ ==> P A C; \


122 
\ !!B S. ALL A:S. leadsTo Acts A B & P A B ==> P (Union S) B \


123 
\ ] ==> P za zb";


124 
br (major RS leadsto.induct) 1;


125 
by (REPEAT (blast_tac (claset() addIs prems) 1));


126 
qed "leadsTo_induct";


127 


128 


129 
goal thy "!!A B. [ A<=B; id: Acts ] ==> leadsTo Acts A B";


130 
by (rtac leadsTo_Basis 1);


131 
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);


132 
by (Blast_tac 1);


133 
qed "subset_imp_leadsTo";


134 


135 
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);


136 
Addsimps [empty_leadsTo];


137 


138 


139 
(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it


140 
needs the extra premise id:Acts*)


141 
goal thy "!!Acts. leadsTo Acts A A' ==> A'<=B' > leadsTo Acts A B'";


142 
by (etac leadsTo_induct 1);


143 
by (Clarify_tac 3);


144 
by (blast_tac (claset() addIs [leadsTo_Union]) 3);


145 
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);


146 
by (blast_tac (claset() addIs [leadsTo_Basis, ensures_weaken_R]) 1);


147 
qed_spec_mp "leadsTo_weaken_R";


148 


149 


150 
goal thy "!!Acts. [ leadsTo Acts A A'; B<=A; id: Acts ] ==> \


151 
\ leadsTo Acts B A'";


152 
by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans,


153 
subset_imp_leadsTo]) 1);


154 
qed_spec_mp "leadsTo_weaken_L";


155 


156 
(*Distributes over binary unions*)


157 
goal thy


158 
"!!C. id: Acts ==> \


159 
\ leadsTo Acts (A Un B) C = (leadsTo Acts A C & leadsTo Acts B C)";


160 
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);


161 
qed "leadsTo_Un_distrib";


162 


163 
goal thy


164 
"!!C. id: Acts ==> \


165 
\ leadsTo Acts (UN i:I. A i) B = (ALL i : I. leadsTo Acts (A i) B)";


166 
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);


167 
qed "leadsTo_UN_distrib";


168 


169 
goal thy


170 
"!!C. id: Acts ==> \


171 
\ leadsTo Acts (Union S) B = (ALL A : S. leadsTo Acts A B)";


172 
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);


173 
qed "leadsTo_Union_distrib";


174 


175 


176 
goal thy


177 
"!!Acts. [ leadsTo Acts A A'; id: Acts; B<=A; A'<=B' ] \


178 
\ ==> leadsTo Acts B B'";


179 
(*PROOF FAILED: why?*)


180 
by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,


181 
leadsTo_weaken_L]) 1);


182 
qed "leadsTo_weaken";


183 


184 


185 
(*Set difference: maybe combine with leadsTo_weaken_L??*)


186 
goal thy


187 
"!!C. [ leadsTo Acts (AB) C; leadsTo Acts B C; id: Acts ] \


188 
\ ==> leadsTo Acts A C";


189 
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);


190 
qed "leadsTo_Diff";


191 


192 


193 
(** Meta or object quantifier ???


194 
see ball_constrains_UN in UNITY.ML***)


195 


196 
val prems = goal thy


197 
"(!! i. i:I ==> leadsTo Acts (A i) (A' i)) \


198 
\ ==> leadsTo Acts (UN i:I. A i) (UN i:I. A' i)";


199 
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);


200 
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R]


201 
addIs prems) 1);


202 
qed "leadsTo_UN_UN";


203 


204 


205 
(*Version with no index set*)


206 
val prems = goal thy


207 
"(!! i. leadsTo Acts (A i) (A' i)) \


208 
\ ==> leadsTo Acts (UN i. A i) (UN i. A' i)";


209 
by (blast_tac (claset() addIs [leadsTo_UN_UN]


210 
addIs prems) 1);


211 
qed "leadsTo_UN_UN_noindex";


212 


213 
(*Version with no index set*)


214 
goal thy


215 
"!!Acts. ALL i. leadsTo Acts (A i) (A' i) \


216 
\ ==> leadsTo Acts (UN i. A i) (UN i. A' i)";


217 
by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);


218 
qed "all_leadsTo_UN_UN";


219 


220 


221 
(*Binary union version*)


222 
goal thy "!!Acts. [ leadsTo Acts A A'; leadsTo Acts B B' ] \


223 
\ ==> leadsTo Acts (A Un B) (A' Un B')";


224 
by (blast_tac (claset() addIs [leadsTo_Un,


225 
leadsTo_weaken_R]) 1);


226 
qed "leadsTo_Un_Un";


227 


228 


229 
(** The cancellation law **)


230 


231 
goal thy


232 
"!!Acts. [ leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts ] \


233 
\ ==> leadsTo Acts A (A' Un B')";


234 
by (blast_tac (claset() addIs [leadsTo_Un_Un,


235 
subset_imp_leadsTo, leadsTo_Trans]) 1);


236 
qed "leadsTo_cancel2";


237 


238 
goal thy


239 
"!!Acts. [ leadsTo Acts A (A' Un B); leadsTo Acts (BA') B'; id: Acts ] \


240 
\ ==> leadsTo Acts A (A' Un B')";


241 
by (rtac leadsTo_cancel2 1);


242 
by (assume_tac 2);


243 
by (ALLGOALS Asm_simp_tac);


244 
qed "leadsTo_cancel_Diff2";


245 


246 
goal thy


247 
"!!Acts. [ leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts ] \


248 
\ ==> leadsTo Acts A (B' Un A')";


249 
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);


250 
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);


251 
qed "leadsTo_cancel1";


252 


253 
goal thy


254 
"!!Acts. [ leadsTo Acts A (B Un A'); leadsTo Acts (BA') B'; id: Acts ] \


255 
\ ==> leadsTo Acts A (B' Un A')";


256 
by (rtac leadsTo_cancel1 1);


257 
by (assume_tac 2);


258 
by (ALLGOALS Asm_simp_tac);


259 
qed "leadsTo_cancel_Diff1";


260 


261 


262 


263 
(** The impossibility law **)


264 


265 
goal thy "!!Acts. leadsTo Acts A B ==> B={} > A={}";


266 
by (etac leadsTo_induct 1);


267 
by (ALLGOALS Asm_simp_tac);


268 
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);


269 
by (Blast_tac 1);


270 
val lemma = result() RS mp;


271 


272 
goal thy "!!Acts. leadsTo Acts A {} ==> A={}";


273 
by (blast_tac (claset() addSIs [lemma]) 1);


274 
qed "leadsTo_empty";


275 


276 


277 
(** PSP: ProgressSafetyProgress **)


278 


279 
(*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *)


280 
goalw thy [stable_def]


281 
"!!Acts. [ leadsTo Acts A A'; stable Acts B ] \


282 
\ ==> leadsTo Acts (A Int B) (A' Int B)";


283 
by (etac leadsTo_induct 1);


284 
by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);


285 
by (blast_tac (claset() addIs [leadsTo_Union]) 3);


286 
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);


287 
by (rtac leadsTo_Basis 1);


288 
by (asm_full_simp_tac


289 
(simpset() addsimps [ensures_def,


290 
Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);


291 
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);


292 
qed "PSP_stable";


293 


294 
goal thy


295 
"!!Acts. [ leadsTo Acts A A'; stable Acts B ] \


296 
\ ==> leadsTo Acts (B Int A) (B Int A')";


297 
by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);


298 
qed "PSP_stable2";


299 


300 


301 
goalw thy [ensures_def]


302 
"!!Acts. [ ensures Acts A A'; constrains Acts B B' ] \


303 
\ ==> ensures Acts (A Int B) ((A' Int B) Un (B'  B))";


304 
by Safe_tac;


305 
by (blast_tac (claset() addIs [constrainsI] addDs [constrainsD]) 1);


306 
by (etac transient_strengthen 1);


307 
by (Blast_tac 1);


308 
qed "PSP_ensures";


309 


310 


311 
goal thy


312 
"!!Acts. [ leadsTo Acts A A'; constrains Acts B B'; id: Acts ] \


313 
\ ==> leadsTo Acts (A Int B) ((A' Int B) Un (B'  B))";


314 
by (etac leadsTo_induct 1);


315 
by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);


316 
by (blast_tac (claset() addIs [leadsTo_Union]) 3);


317 
(*Transitivity case has a delicate argument involving "cancellation"*)


318 
by (rtac leadsTo_Un_duplicate2 2);


319 
by (etac leadsTo_cancel_Diff1 2);


320 
by (assume_tac 3);


321 
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);


322 
(*Basis case*)


323 
by (blast_tac (claset() addIs [leadsTo_Basis, PSP_ensures]) 1);


324 
qed "PSP";


325 


326 
goal thy


327 
"!!Acts. [ leadsTo Acts A A'; constrains Acts B B'; id: Acts ] \


328 
\ ==> leadsTo Acts (B Int A) ((B Int A') Un (B'  B))";


329 
by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);


330 
qed "PSP2";


331 


332 


333 
goalw thy [unless_def]


334 
"!!Acts. [ leadsTo Acts A A'; unless Acts B B'; id: Acts ] \


335 
\ ==> leadsTo Acts (A Int B) ((A' Int B) Un B')";


336 
by (dtac PSP 1);


337 
by (assume_tac 1);


338 
by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);


339 
by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);


340 
by (etac leadsTo_Diff 2);


341 
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 2);


342 
by Auto_tac;


343 
qed "PSP_unless";


344 


345 


346 
(*** Proving the induction rules ***)


347 


348 
goal thy


349 
"!!Acts. [ wf r; \


350 
\ ALL m. leadsTo Acts (A Int f``{m}) \


351 
\ ((A Int f``(r^1 ^^ {m})) Un B); \


352 
\ id: Acts ] \


353 
\ ==> leadsTo Acts (A Int f``{m}) B";


354 
by (eres_inst_tac [("a","m")] wf_induct 1);


355 
by (subgoal_tac "leadsTo Acts (A Int (f `` (r^1 ^^ {x}))) B" 1);


356 
by (stac vimage_eq_UN 2);


357 
by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);


358 
by (blast_tac (claset() addIs [leadsTo_UN]) 2);


359 
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);


360 
val lemma = result();


361 


362 


363 
(** Meta or object quantifier ????? **)


364 
goal thy


365 
"!!Acts. [ wf r; \


366 
\ ALL m. leadsTo Acts (A Int f``{m}) \


367 
\ ((A Int f``(r^1 ^^ {m})) Un B); \


368 
\ id: Acts ] \


369 
\ ==> leadsTo Acts A B";


370 
by (res_inst_tac [("t", "A")] subst 1);


371 
by (rtac leadsTo_UN 2);


372 
by (etac lemma 2);


373 
by (REPEAT (assume_tac 2));


374 
by (Fast_tac 1); (*Blast_tac: Function unknown's argument not a parameter*)


375 
qed "leadsTo_wf_induct";


376 


377 


378 
goal thy


379 
"!!Acts. [ wf r; \


380 
\ ALL m:I. leadsTo Acts (A Int f``{m}) \


381 
\ ((A Int f``(r^1 ^^ {m})) Un B); \


382 
\ id: Acts ] \


383 
\ ==> leadsTo Acts A ((A  (f``I)) Un B)";


384 
by (etac leadsTo_wf_induct 1);


385 
by Safe_tac;


386 
by (case_tac "m:I" 1);


387 
by (blast_tac (claset() addIs [leadsTo_weaken]) 1);


388 
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);


389 
qed "bounded_induct";


390 


391 


392 
(*Alternative proof is via the lemma leadsTo Acts (A Int f``(lessThan m)) B*)


393 
goal thy


394 
"!!Acts. [ ALL m. leadsTo Acts (A Int f``{m}) \


395 
\ ((A Int f``(lessThan m)) Un B); \


396 
\ id: Acts ] \


397 
\ ==> leadsTo Acts A B";


398 
by (rtac (wf_less_than RS leadsTo_wf_induct) 1);


399 
by (assume_tac 2);


400 
by (Asm_simp_tac 1);


401 
qed "lessThan_induct";


402 


403 
goal thy


404 
"!!Acts. [ ALL m:(greaterThan l). leadsTo Acts (A Int f``{m}) \


405 
\ ((A Int f``(lessThan m)) Un B); \


406 
\ id: Acts ] \


407 
\ ==> leadsTo Acts A ((A Int (f``(atMost l))) Un B)";


408 
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);


409 
by (rtac (wf_less_than RS bounded_induct) 1);


410 
by (assume_tac 2);


411 
by (Asm_simp_tac 1);


412 
qed "lessThan_bounded_induct";


413 


414 
goal thy


415 
"!!Acts. [ ALL m:(lessThan l). leadsTo Acts (A Int f``{m}) \


416 
\ ((A Int f``(greaterThan m)) Un B); \


417 
\ id: Acts ] \


418 
\ ==> leadsTo Acts A ((A Int (f``(atLeast l))) Un B)";


419 
by (res_inst_tac [("f","f"),("f1", "%k. l  k")]


420 
(wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);


421 
by (assume_tac 2);


422 
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);


423 
by (Clarify_tac 1);


424 
by (case_tac "m<l" 1);


425 
by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2);


426 
by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1);


427 
qed "greaterThan_bounded_induct";


428 


429 


430 


431 
(*** wlt ****)


432 


433 
(*Misra's property W3*)


434 
goalw thy [wlt_def] "leadsTo Acts (wlt Acts B) B";


435 
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);


436 
qed "wlt_leadsTo";


437 


438 
goalw thy [wlt_def] "!!Acts. leadsTo Acts A B ==> A <= wlt Acts B";


439 
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);


440 
qed "leadsTo_subset";


441 


442 
(*Misra's property W2*)


443 
goal thy "!!Acts. id: Acts ==> leadsTo Acts A B = (A <= wlt Acts B)";


444 
by (blast_tac (claset() addSIs [leadsTo_subset,


445 
wlt_leadsTo RS leadsTo_weaken_L]) 1);


446 
qed "leadsTo_eq_subset_wlt";


447 


448 
(*Misra's property W4*)


449 
goal thy "!!Acts. id: Acts ==> B <= wlt Acts B";


450 
by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,


451 
subset_imp_leadsTo]) 1);


452 
qed "wlt_increasing";


453 


454 


455 
(*Used in the Trans case below*)


456 
goalw thy [constrains_def]


457 
"!!Acts. [ B <= A2; \


458 
\ constrains Acts (A1  B) (A1 Un B); \


459 
\ constrains Acts (A2  C) (A2 Un C) ] \


460 
\ ==> constrains Acts (A1 Un A2  C) (A1 Un A2 Un C)";


461 
by (Clarify_tac 1);


462 
by (blast_tac (claset() addSDs [bspec]) 1);


463 
val lemma1 = result();


464 


465 


466 
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)


467 
goal thy


468 
"!!Acts. [ leadsTo Acts A A'; id: Acts ] ==> \


469 
\ EX B. A<=B & leadsTo Acts B A' & constrains Acts (BA') (B Un A')";


470 
by (etac leadsTo_induct 1);


471 
(*Basis*)


472 
by (blast_tac (claset() addIs [leadsTo_Basis]


473 
addDs [ensuresD]) 1);


474 
(*Trans*)


475 
by (Clarify_tac 1);


476 
by (res_inst_tac [("x", "Ba Un Bb")] exI 1);


477 
by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1,


478 
leadsTo_Un_duplicate]) 1);


479 
(*Union*)


480 
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1,


481 
bchoice, ball_constrains_UN]) 1);;


482 
by (res_inst_tac [("x", "UN A:S. f A")] exI 1);


483 
by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1);


484 
qed "leadsTo_123";


485 


486 


487 
(*Misra's property W5*)


488 
goal thy "!!Acts. id: Acts ==> constrains Acts (wlt Acts B  B) (wlt Acts B)";


489 
by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);


490 
by (Clarify_tac 1);


491 
by (subgoal_tac "Ba = wlt Acts B" 1);


492 
by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt]) 2);


493 
by (Clarify_tac 1);


494 
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1);


495 
qed "wlt_constrains_wlt";


496 


497 


498 
(*** Completion: Binary and General Finite versions ***)


499 


500 
goal thy


501 
"!!Acts. [ leadsTo Acts A A'; stable Acts A'; \


502 
\ leadsTo Acts B B'; stable Acts B'; id: Acts ] \


503 
\ ==> leadsTo Acts (A Int B) (A' Int B')";


504 
by (subgoal_tac "stable Acts (wlt Acts B')" 1);


505 
by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);


506 
by (EVERY [etac (constrains_Un RS constrains_weaken) 2,


507 
etac wlt_constrains_wlt 2,


508 
fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,


509 
Blast_tac 2]);


510 
by (subgoal_tac "leadsTo Acts (A Int wlt Acts B') (A' Int wlt Acts B')" 1);


511 
by (blast_tac (claset() addIs [PSP_stable]) 2);


512 
by (subgoal_tac "leadsTo Acts (A' Int wlt Acts B') (A' Int B')" 1);


513 
by (blast_tac (claset() addIs [wlt_leadsTo, PSP_stable2]) 2);


514 
by (subgoal_tac "leadsTo Acts (A Int B) (A Int wlt Acts B')" 1);


515 
by (blast_tac (claset() addIs [leadsTo_subset RS subsetD,


516 
subset_imp_leadsTo]) 2);


517 
(*Blast_tac gives PROOF FAILED*)


518 
by (best_tac (claset() addIs [leadsTo_Trans]) 1);


519 
qed "stable_completion";


520 


521 


522 
goal thy


523 
"!!Acts. [ finite I; id: Acts ] \


524 
\ ==> (ALL i:I. leadsTo Acts (A i) (A' i)) > \


525 
\ (ALL i:I. stable Acts (A' i)) > \


526 
\ leadsTo Acts (INT i:I. A i) (INT i:I. A' i)";


527 
by (etac finite_induct 1);


528 
by (Asm_simp_tac 1);


529 
by (asm_simp_tac


530 
(simpset() addsimps [stable_completion, stable_def,


531 
ball_constrains_INT]) 1);


532 
qed_spec_mp "finite_stable_completion";


533 


534 


535 
goal thy


536 
"!!Acts. [ W = wlt Acts (B' Un C); \


537 
\ leadsTo Acts A (A' Un C); constrains Acts A' (A' Un C); \


538 
\ leadsTo Acts B (B' Un C); constrains Acts B' (B' Un C); \


539 
\ id: Acts ] \


540 
\ ==> leadsTo Acts (A Int B) ((A' Int B') Un C)";


541 
by (subgoal_tac "constrains Acts (WC) (W Un B' Un C)" 1);


542 
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt]


543 
MRS constrains_Un RS constrains_weaken]) 2);


544 
by (subgoal_tac "constrains Acts (WC) W" 1);


545 
by (asm_full_simp_tac


546 
(simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);


547 
by (subgoal_tac "leadsTo Acts (A Int W  C) (A' Int W Un C)" 1);


548 
by (simp_tac (simpset() addsimps [Int_Diff]) 2);


549 
by (blast_tac (claset() addIs [wlt_leadsTo, PSP RS leadsTo_weaken_R]) 2);


550 
by (subgoal_tac "leadsTo Acts (A' Int W Un C) (A' Int B' Un C)" 1);


551 
by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un,


552 
PSP2 RS leadsTo_weaken_R,


553 
subset_refl RS subset_imp_leadsTo,


554 
leadsTo_Un_duplicate2]) 2);


555 
by (dtac leadsTo_Diff 1);


556 
by (assume_tac 2);


557 
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);


558 
by (subgoal_tac "A Int B <= A Int W" 1);


559 
by (blast_tac (claset() addIs [leadsTo_subset, Int_mono]


560 
delrules [subsetI]) 2);


561 
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);


562 
bind_thm("completion", refl RS result());


563 


564 


565 
goal thy


566 
"!!Acts. [ finite I; id: Acts ] \


567 
\ ==> (ALL i:I. leadsTo Acts (A i) (A' i Un C)) > \


568 
\ (ALL i:I. constrains Acts (A' i) (A' i Un C)) > \


569 
\ leadsTo Acts (INT i:I. A i) ((INT i:I. A' i) Un C)";


570 
by (etac finite_induct 1);


571 
by (ALLGOALS Asm_simp_tac);


572 
by (Clarify_tac 1);


573 
by (dtac ball_constrains_INT 1);


574 
by (asm_full_simp_tac (simpset() addsimps [completion]) 1);


575 
qed "finite_completion";


576 
