src/HOL/UNITY/WFair.ML
author paulson
Mon Oct 11 10:53:39 1999 +0200 (1999-10-11)
changeset 7826 c6a8b73b6c2a
parent 7594 8a188ef6545e
child 7963 e7beff82e1ba
permissions -rw-r--r--
working shapshot with "projecting" and "extending"
     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 
    12 overload_1st_set "WFair.transient";
    13 overload_1st_set "WFair.ensures";
    14 overload_1st_set "WFair.op leadsTo";
    15 
    16 (*** transient ***)
    17 
    18 Goalw [stable_def, constrains_def, transient_def]
    19     "[| F : stable A; F : transient A |] ==> A = {}";
    20 by (Blast_tac 1);
    21 qed "stable_transient_empty";
    22 
    23 Goalw [transient_def]
    24     "[| F : transient A; B<=A |] ==> F : transient B";
    25 by (Clarify_tac 1);
    26 by (blast_tac (claset() addSIs [rev_bexI]) 1);
    27 qed "transient_strengthen";
    28 
    29 Goalw [transient_def]
    30     "[| act: Acts F;  A <= Domain act;  act^^A <= -A |] ==> F : transient A";
    31 by (Blast_tac 1);
    32 qed "transient_mem";
    33 
    34 Goalw [transient_def] "transient UNIV = {}";
    35 by Auto_tac;
    36 qed "transient_UNIV";
    37 
    38 Goalw [transient_def] "transient {} = UNIV";
    39 by Auto_tac;
    40 qed "transient_empty";
    41 Addsimps [transient_UNIV, transient_empty];
    42 
    43 
    44 (*** ensures ***)
    45 
    46 Goalw [ensures_def]
    47     "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B";
    48 by (Blast_tac 1);
    49 qed "ensuresI";
    50 
    51 Goalw [ensures_def]
    52     "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)";
    53 by (Blast_tac 1);
    54 qed "ensuresD";
    55 
    56 (*The L-version (precondition strengthening) doesn't hold for ENSURES*)
    57 Goalw [ensures_def]
    58     "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'";
    59 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
    60 qed "ensures_weaken_R";
    61 
    62 Goalw [ensures_def, constrains_def, transient_def]
    63     "F : A ensures UNIV";
    64 by Auto_tac;
    65 qed "ensures_UNIV";
    66 
    67 Goalw [ensures_def]
    68     "[| F : stable C; \
    69 \       F : (C Int (A - A')) co (A Un A'); \
    70 \       F : transient (C Int (A-A')) |]   \
    71 \   ==> F : (C Int A) ensures (C Int A')";
    72 by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
    73 				      Diff_Int_distrib RS sym,
    74 				      stable_constrains_Int]) 1);
    75 qed "stable_ensures_Int";
    76 
    77 Goal "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B";
    78 by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
    79 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
    80 qed "stable_transient_ensures";
    81 
    82 
    83 (*** leadsTo ***)
    84 
    85 Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B";
    86 by (blast_tac (claset() addIs [leads.Basis]) 1);
    87 qed "leadsTo_Basis";
    88 
    89 Goalw [leadsTo_def]
    90      "[| F : A leadsTo B;  F : B leadsTo C |] ==> F : A leadsTo C";
    91 by (blast_tac (claset() addIs [leads.Trans]) 1);
    92 qed "leadsTo_Trans";
    93 
    94 Goal "F : transient A ==> F : A leadsTo (-A)";
    95 by (asm_simp_tac 
    96     (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
    97 qed "transient_imp_leadsTo";
    98 
    99 Goal "F : A leadsTo UNIV";
   100 by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
   101 qed "leadsTo_UNIV";
   102 Addsimps [leadsTo_UNIV];
   103 
   104 (*Useful with cancellation, disjunction*)
   105 Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
   106 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   107 qed "leadsTo_Un_duplicate";
   108 
   109 Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)";
   110 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   111 qed "leadsTo_Un_duplicate2";
   112 
   113 (*The Union introduction rule as we should have liked to state it*)
   114 val prems = Goalw [leadsTo_def]
   115     "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B";
   116 by (blast_tac (claset() addIs [leads.Union] addDs prems) 1);
   117 qed "leadsTo_Union";
   118 
   119 val prems = Goalw [leadsTo_def]
   120  "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B";
   121 by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
   122 by (blast_tac (claset() addIs [leads.Union] addDs prems) 1);
   123 qed "leadsTo_Union_Int";
   124 
   125 val prems = Goal
   126     "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B";
   127 by (stac (Union_image_eq RS sym) 1);
   128 by (blast_tac (claset() addIs leadsTo_Union::prems) 1);
   129 qed "leadsTo_UN";
   130 
   131 (*Binary union introduction rule*)
   132 Goal "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C";
   133 by (stac Un_eq_Union 1);
   134 by (blast_tac (claset() addIs [leadsTo_Union]) 1);
   135 qed "leadsTo_Un";
   136 
   137 val prems = 
   138 Goal "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B";
   139 by (stac (UN_singleton RS sym) 1 THEN rtac leadsTo_UN 1);
   140 by (blast_tac (claset() addIs prems) 1);
   141 qed "single_leadsTo_I";
   142 
   143 
   144 (*The INDUCTION rule as we should have liked to state it*)
   145 val major::prems = Goalw [leadsTo_def]
   146   "[| F : za leadsTo zb;  \
   147 \     !!A B. F : A ensures B ==> P A B; \
   148 \     !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |] \
   149 \              ==> P A C; \
   150 \     !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \
   151 \  |] ==> P za zb";
   152 by (rtac (major RS CollectD RS leads.induct) 1);
   153 by (REPEAT (blast_tac (claset() addIs prems) 1));
   154 qed "leadsTo_induct";
   155 
   156 
   157 Goal "A<=B ==> F : A ensures B";
   158 by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
   159 by (Blast_tac 1);
   160 qed "subset_imp_ensures";
   161 
   162 bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis);
   163 
   164 bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
   165 Addsimps [empty_leadsTo];
   166 
   167 
   168 Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'";
   169 by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
   170 qed "leadsTo_weaken_R";
   171 
   172 Goal "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'";
   173 by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
   174 qed_spec_mp "leadsTo_weaken_L";
   175 
   176 (*Distributes over binary unions*)
   177 Goal "F : (A Un B) leadsTo C  =  (F : A leadsTo C & F : B leadsTo C)";
   178 by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
   179 qed "leadsTo_Un_distrib";
   180 
   181 Goal "F : (UN i:I. A i) leadsTo B  =  (ALL i : I. F : (A i) leadsTo B)";
   182 by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
   183 qed "leadsTo_UN_distrib";
   184 
   185 Goal "F : (Union S) leadsTo B  =  (ALL A : S. F : A leadsTo B)";
   186 by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
   187 qed "leadsTo_Union_distrib";
   188 
   189 
   190 Goal "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'";
   191 by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
   192 			       leadsTo_Trans]) 1);
   193 qed "leadsTo_weaken";
   194 
   195 
   196 (*Set difference: maybe combine with leadsTo_weaken_L??*)
   197 Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C";
   198 by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
   199 qed "leadsTo_Diff";
   200 
   201 
   202 (** Meta or object quantifier ???
   203     see ball_constrains_UN in UNITY.ML***)
   204 
   205 val prems = goal thy
   206    "(!! i. i:I ==> F : (A i) leadsTo (A' i)) \
   207 \   ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)";
   208 by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
   209 by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] 
   210                         addIs prems) 1);
   211 qed "leadsTo_UN_UN";
   212 
   213 
   214 (*Version with no index set*)
   215 val prems = goal thy
   216    "(!! i. F : (A i) leadsTo (A' i)) \
   217 \   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
   218 by (blast_tac (claset() addIs [leadsTo_UN_UN] 
   219                         addIs prems) 1);
   220 qed "leadsTo_UN_UN_noindex";
   221 
   222 (*Version with no index set*)
   223 Goal "ALL i. F : (A i) leadsTo (A' i) \
   224 \   ==> F : (UN i. A i) leadsTo (UN i. A' i)";
   225 by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
   226 qed "all_leadsTo_UN_UN";
   227 
   228 
   229 (*Binary union version*)
   230 Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \
   231 \     ==> F : (A Un B) leadsTo (A' Un B')";
   232 by (blast_tac (claset() addIs [leadsTo_Un, 
   233 			       leadsTo_weaken_R]) 1);
   234 qed "leadsTo_Un_Un";
   235 
   236 
   237 (** The cancellation law **)
   238 
   239 Goal "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] \
   240 \     ==> F : A leadsTo (A' Un B')";
   241 by (blast_tac (claset() addIs [leadsTo_Un_Un, 
   242 			       subset_imp_leadsTo, leadsTo_Trans]) 1);
   243 qed "leadsTo_cancel2";
   244 
   245 Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \
   246 \     ==> F : A leadsTo (A' Un B')";
   247 by (rtac leadsTo_cancel2 1);
   248 by (assume_tac 2);
   249 by (ALLGOALS Asm_simp_tac);
   250 qed "leadsTo_cancel_Diff2";
   251 
   252 Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] \
   253 \   ==> F : A leadsTo (B' Un A')";
   254 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
   255 by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
   256 qed "leadsTo_cancel1";
   257 
   258 Goal "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] \
   259 \   ==> F : A leadsTo (B' Un A')";
   260 by (rtac leadsTo_cancel1 1);
   261 by (assume_tac 2);
   262 by (ALLGOALS Asm_simp_tac);
   263 qed "leadsTo_cancel_Diff1";
   264 
   265 
   266 
   267 (** The impossibility law **)
   268 
   269 Goal "F : A leadsTo B ==> B={} --> A={}";
   270 by (etac leadsTo_induct 1);
   271 by (ALLGOALS Asm_simp_tac);
   272 by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
   273 by (Blast_tac 1);
   274 val lemma = result() RS mp;
   275 
   276 Goal "F : A leadsTo {} ==> A={}";
   277 by (blast_tac (claset() addSIs [lemma]) 1);
   278 qed "leadsTo_empty";
   279 
   280 
   281 (** PSP: Progress-Safety-Progress **)
   282 
   283 (*Special case of PSP: Misra's "stable conjunction"*)
   284 Goalw [stable_def]
   285    "[| F : A leadsTo A'; F : stable B |] \
   286 \   ==> F : (A Int B) leadsTo (A' Int B)";
   287 by (etac leadsTo_induct 1);
   288 by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
   289 by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
   290 by (rtac leadsTo_Basis 1);
   291 by (asm_full_simp_tac
   292     (simpset() addsimps [ensures_def, 
   293 			 Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
   294 by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
   295 qed "psp_stable";
   296 
   297 Goal
   298    "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')";
   299 by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
   300 qed "psp_stable2";
   301 
   302 Goalw [ensures_def, constrains_def]
   303    "[| F : A ensures A'; F : B co B' |] \
   304 \   ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))";
   305 by (Clarify_tac 1);  (*speeds up the proof*)
   306 by (blast_tac (claset() addIs [transient_strengthen]) 1);
   307 qed "psp_ensures";
   308 
   309 Goal "[| F : A leadsTo A'; F : B co B' |] \
   310 \     ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))";
   311 by (etac leadsTo_induct 1);
   312 by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
   313 (*Transitivity case has a delicate argument involving "cancellation"*)
   314 by (rtac leadsTo_Un_duplicate2 2);
   315 by (etac leadsTo_cancel_Diff1 2);
   316 by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
   317 by (blast_tac (claset() addIs [leadsTo_weaken_L] 
   318                         addDs [constrains_imp_subset]) 2);
   319 (*Basis case*)
   320 by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
   321 qed "psp";
   322 
   323 Goal "[| F : A leadsTo A'; F : B co B' |] \
   324 \   ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))";
   325 by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
   326 qed "psp2";
   327 
   328 
   329 Goalw [unless_def]
   330    "[| F : A leadsTo A';  F : B unless B' |] \
   331 \   ==> F : (A Int B) leadsTo ((A' Int B) Un B')";
   332 by (dtac psp 1);
   333 by (assume_tac 1);
   334 by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   335 qed "psp_unless";
   336 
   337 
   338 (*** Proving the induction rules ***)
   339 
   340 (** The most general rule: r is any wf relation; f is any variant function **)
   341 
   342 Goal "[| wf r;     \
   343 \        ALL m. F : (A Int f-``{m}) leadsTo                     \
   344 \                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   345 \     ==> F : (A Int f-``{m}) leadsTo B";
   346 by (eres_inst_tac [("a","m")] wf_induct 1);
   347 by (subgoal_tac "F : (A Int (f -`` (r^-1 ^^ {x}))) leadsTo B" 1);
   348 by (stac vimage_eq_UN 2);
   349 by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
   350 by (blast_tac (claset() addIs [leadsTo_UN]) 2);
   351 by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
   352 val lemma = result();
   353 
   354 
   355 (** Meta or object quantifier ????? **)
   356 Goal "[| wf r;     \
   357 \        ALL m. F : (A Int f-``{m}) leadsTo                     \
   358 \                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   359 \     ==> F : A leadsTo B";
   360 by (res_inst_tac [("t", "A")] subst 1);
   361 by (rtac leadsTo_UN 2);
   362 by (etac lemma 2);
   363 by (REPEAT (assume_tac 2));
   364 by (Fast_tac 1);    (*Blast_tac: Function unknown's argument not a parameter*)
   365 qed "leadsTo_wf_induct";
   366 
   367 
   368 Goal "[| wf r;     \
   369 \        ALL m:I. F : (A Int f-``{m}) leadsTo                   \
   370 \                     ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   371 \     ==> F : A leadsTo ((A - (f-``I)) Un B)";
   372 by (etac leadsTo_wf_induct 1);
   373 by Safe_tac;
   374 by (case_tac "m:I" 1);
   375 by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   376 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   377 qed "bounded_induct";
   378 
   379 
   380 (*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
   381 Goal "[| ALL m. F : (A Int f-``{m}) leadsTo                     \
   382 \                   ((A Int f-``(lessThan m)) Un B) |] \
   383 \     ==> F : A leadsTo B";
   384 by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
   385 by (Asm_simp_tac 1);
   386 qed "lessThan_induct";
   387 
   388 Goal "[| ALL m:(greaterThan l).    \
   389 \           F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
   390 \     ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
   391 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
   392 			       Compl_greaterThan RS sym]) 1);
   393 by (rtac (wf_less_than RS bounded_induct) 1);
   394 by (Asm_simp_tac 1);
   395 qed "lessThan_bounded_induct";
   396 
   397 Goal "[| ALL m:(lessThan l).    \
   398 \           F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \
   399 \     ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
   400 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
   401     (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
   402 by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
   403 by (Clarify_tac 1);
   404 by (case_tac "m<l" 1);
   405 by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2);
   406 by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1);
   407 qed "greaterThan_bounded_induct";
   408 
   409 
   410 (*** wlt ****)
   411 
   412 (*Misra's property W3*)
   413 Goalw [wlt_def] "F : (wlt F B) leadsTo B";
   414 by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
   415 qed "wlt_leadsTo";
   416 
   417 Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt F B";
   418 by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
   419 qed "leadsTo_subset";
   420 
   421 (*Misra's property W2*)
   422 Goal "F : A leadsTo B = (A <= wlt F B)";
   423 by (blast_tac (claset() addSIs [leadsTo_subset, 
   424 				wlt_leadsTo RS leadsTo_weaken_L]) 1);
   425 qed "leadsTo_eq_subset_wlt";
   426 
   427 (*Misra's property W4*)
   428 Goal "B <= wlt F B";
   429 by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
   430 				      subset_imp_leadsTo]) 1);
   431 qed "wlt_increasing";
   432 
   433 
   434 (*Used in the Trans case below*)
   435 Goalw [constrains_def]
   436    "[| B <= A2;  \
   437 \      F : (A1 - B) co (A1 Un B); \
   438 \      F : (A2 - C) co (A2 Un C) |] \
   439 \   ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
   440 by (Clarify_tac 1);
   441 by (Blast_tac 1);
   442 val lemma1 = result();
   443 
   444 
   445 (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
   446 Goal "F : A leadsTo A' ==> \
   447 \     EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')";
   448 by (etac leadsTo_induct 1);
   449 (*Basis*)
   450 by (blast_tac (claset() addIs [leadsTo_Basis]
   451                         addDs [ensuresD]) 1);
   452 (*Trans*)
   453 by (Clarify_tac 1);
   454 by (res_inst_tac [("x", "Ba Un Bb")] exI 1);
   455 by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1,
   456 			       leadsTo_Un_duplicate]) 1);
   457 (*Union*)
   458 by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1,
   459 				  bchoice, ball_constrains_UN]) 1);;
   460 by (res_inst_tac [("x", "UN A:S. f A")] exI 1);
   461 by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1);
   462 qed "leadsTo_123";
   463 
   464 
   465 (*Misra's property W5*)
   466 Goal "F : (wlt F B - B) co (wlt F B)";
   467 by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1);
   468 by (Clarify_tac 1);
   469 by (subgoal_tac "Ba = wlt F B" 1);
   470 by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2);
   471 by (Clarify_tac 1);
   472 by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1);
   473 qed "wlt_constrains_wlt";
   474 
   475 
   476 (*** Completion: Binary and General Finite versions ***)
   477 
   478 Goal "[| F : A leadsTo A';  F : stable A';   \
   479 \        F : B leadsTo B';  F : stable B' |] \
   480 \   ==> F : (A Int B) leadsTo (A' Int B')";
   481 by (subgoal_tac "F : stable (wlt F B')" 1);
   482 by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
   483 by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
   484 	   rtac wlt_constrains_wlt 2,
   485 	   fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
   486 	   Blast_tac 2]);
   487 by (subgoal_tac "F : (A Int wlt F B') leadsTo (A' Int wlt F B')" 1);
   488 by (blast_tac (claset() addIs [psp_stable]) 2);
   489 by (subgoal_tac "F : (A' Int wlt F B') leadsTo (A' Int B')" 1);
   490 by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2);
   491 by (subgoal_tac "F : (A Int B) leadsTo (A Int wlt F B')" 1);
   492 by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
   493 			       subset_imp_leadsTo]) 2);
   494 by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
   495 qed "stable_completion";
   496 
   497 
   498 Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i)) -->  \
   499 \                  (ALL i:I. F : stable (A' i)) -->         \
   500 \                  F : (INT i:I. A i) leadsTo (INT i:I. A' i)";
   501 by (etac finite_induct 1);
   502 by (Asm_simp_tac 1);
   503 by (asm_simp_tac 
   504     (simpset() addsimps [stable_completion, stable_def, 
   505 			 ball_constrains_INT]) 1);
   506 qed_spec_mp "finite_stable_completion";
   507 
   508 
   509 Goal "[| W = wlt F (B' Un C);     \
   510 \      F : A leadsTo (A' Un C);  F : A' co (A' Un C);   \
   511 \      F : B leadsTo (B' Un C);  F : B' co (B' Un C) |] \
   512 \   ==> F : (A Int B) leadsTo ((A' Int B') Un C)";
   513 by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1);
   514 by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
   515 			       MRS constrains_Un RS constrains_weaken]) 2);
   516 by (subgoal_tac "F : (W-C) co W" 1);
   517 by (asm_full_simp_tac 
   518     (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
   519 by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1);
   520 by (simp_tac (simpset() addsimps [Int_Diff]) 2);
   521 by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2);
   522 (** LEVEL 7 **)
   523 by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
   524 by (rtac leadsTo_Un_duplicate2 2);
   525 by (blast_tac (claset() addIs [leadsTo_Un_Un, 
   526                                wlt_leadsTo RS psp2 RS leadsTo_weaken, 
   527                                subset_refl RS subset_imp_leadsTo]) 2);
   528 by (dtac leadsTo_Diff 1);
   529 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   530 by (subgoal_tac "A Int B <= A Int W" 1);
   531 by (blast_tac (claset() addSDs [leadsTo_subset]
   532 			addSIs [subset_refl RS Int_mono]) 2);
   533 by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
   534 bind_thm("completion", refl RS result());
   535 
   536 
   537 Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) -->  \
   538 \                  (ALL i:I. F : (A' i) co (A' i Un C)) --> \
   539 \                  F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)";
   540 by (etac finite_induct 1);
   541 by (ALLGOALS Asm_simp_tac);
   542 by (Clarify_tac 1);
   543 by (dtac ball_constrains_INT 1);
   544 by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 
   545 qed_spec_mp "finite_completion";
   546