src/HOL/UNITY/SubstAx.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
permissions -rw-r--r--
New UNITY theory
     1 (*  Title:      HOL/UNITY/SubstAx
     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 SubstAx;
    12 
    13 (*constrains Acts B B' ==> constrains Acts (reachable Init Acts Int B)
    14                                            (reachable Init Acts Int B') *)
    15 bind_thm ("constrains_reachable",
    16 	  rewrite_rule [stable_def] stable_reachable RS constrains_Int);
    17 
    18 
    19 (*** Introduction rules: Basis, Trans, Union ***)
    20 
    21 goalw thy [LeadsTo_def]
    22     "!!Acts. leadsTo Acts A B ==> LeadsTo Init Acts A B";
    23 by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1);
    24 qed "leadsTo_imp_LeadsTo";
    25 
    26 goalw thy [LeadsTo_def]
    27     "!!Acts. [| constrains Acts (reachable Init Acts Int (A - A'))   \
    28 \                               (A Un A'); \
    29 \               transient  Acts (reachable Init Acts Int (A-A')) |]   \
    30 \           ==> LeadsTo Init Acts A A'";
    31 by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
    32 by (assume_tac 2);
    33 by (asm_simp_tac 
    34     (simpset() addsimps [Int_Un_distrib RS sym, Diff_Int_distrib RS sym,
    35 			 stable_constrains_Int]) 1);
    36 qed "LeadsTo_Basis";
    37 
    38 goalw thy [LeadsTo_def]
    39     "!!Acts. [| LeadsTo Init Acts A B;  LeadsTo Init Acts B C |] \
    40 \            ==> LeadsTo Init Acts A C";
    41 by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
    42 qed "LeadsTo_Trans";
    43 
    44 val prems = goalw thy [LeadsTo_def]
    45  "(!!A. A : S ==> LeadsTo Init Acts A B) ==> LeadsTo Init Acts (Union S) B";
    46 by (stac Int_Union 1);
    47 by (blast_tac (claset() addIs (leadsTo_UN::prems)) 1);
    48 qed "LeadsTo_Union";
    49 
    50 
    51 (*** Derived rules ***)
    52 
    53 goal thy "!!Acts. id: Acts ==> LeadsTo Init Acts A UNIV";
    54 by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
    55 				      Int_lower1 RS subset_imp_leadsTo]) 1);
    56 qed "LeadsTo_UNIV";
    57 Addsimps [LeadsTo_UNIV];
    58 
    59 (*Useful with cancellation, disjunction*)
    60 goal thy "!!Acts. LeadsTo Init Acts A (A' Un A') ==> LeadsTo Init Acts A A'";
    61 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
    62 qed "LeadsTo_Un_duplicate";
    63 
    64 goal thy "!!Acts. LeadsTo Init Acts A (A' Un C Un C) ==> LeadsTo Init Acts A (A' Un C)";
    65 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
    66 qed "LeadsTo_Un_duplicate2";
    67 
    68 val prems = goal thy
    69    "(!!i. i : I ==> LeadsTo Init Acts (A i) B) \
    70 \   ==> LeadsTo Init Acts (UN i:I. A i) B";
    71 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
    72 by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
    73 qed "LeadsTo_UN";
    74 
    75 (*Binary union introduction rule*)
    76 goal thy
    77   "!!C. [| LeadsTo Init Acts A C; LeadsTo Init Acts B C |] ==> LeadsTo Init Acts (A Un B) C";
    78 by (stac Un_eq_Union 1);
    79 by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
    80 qed "LeadsTo_Un";
    81 
    82 
    83 goalw thy [LeadsTo_def]
    84     "!!A B. [| reachable Init Acts Int A <= B;  id: Acts |] \
    85 \           ==> LeadsTo Init Acts A B";
    86 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
    87 qed "Int_subset_imp_LeadsTo";
    88 
    89 goalw thy [LeadsTo_def]
    90     "!!A B. [| A <= B;  id: Acts |] \
    91 \           ==> LeadsTo Init Acts A B";
    92 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
    93 qed "subset_imp_LeadsTo";
    94 
    95 bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
    96 Addsimps [empty_LeadsTo];
    97 
    98 goal thy
    99     "!!A B. [| reachable Init Acts Int A = {};  id: Acts |] \
   100 \           ==> LeadsTo Init Acts A B";
   101 by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
   102 qed "Int_empty_LeadsTo";
   103 
   104 
   105 goalw thy [LeadsTo_def]
   106     "!!Acts. [| LeadsTo Init Acts A A';   \
   107 \               reachable Init Acts Int A' <= B' |] \
   108 \            ==> LeadsTo Init Acts A B'";
   109 by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
   110 qed_spec_mp "LeadsTo_weaken_R";
   111 
   112 
   113 goalw thy [LeadsTo_def]
   114     "!!Acts. [| LeadsTo Init Acts A A'; \
   115      \               reachable Init Acts Int B <= A; id: Acts |]  \
   116 \            ==> LeadsTo Init Acts B A'";
   117 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
   118 qed_spec_mp "LeadsTo_weaken_L";
   119 
   120 
   121 (*Distributes over binary unions*)
   122 goal thy
   123   "!!C. id: Acts ==> \
   124 \       LeadsTo Init Acts (A Un B) C  =  \
   125 \       (LeadsTo Init Acts A C & LeadsTo Init Acts B C)";
   126 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
   127 qed "LeadsTo_Un_distrib";
   128 
   129 goal thy
   130   "!!C. id: Acts ==> \
   131 \       LeadsTo Init Acts (UN i:I. A i) B  =  \
   132 \       (ALL i : I. LeadsTo Init Acts (A i) B)";
   133 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
   134 qed "LeadsTo_UN_distrib";
   135 
   136 goal thy
   137   "!!C. id: Acts ==> \
   138 \       LeadsTo Init Acts (Union S) B  =  \
   139 \       (ALL A : S. LeadsTo Init Acts A B)";
   140 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
   141 qed "LeadsTo_Union_distrib";
   142 
   143 
   144 goal thy 
   145    "!!Acts. [| LeadsTo Init Acts A A'; id: Acts;   \
   146 \               reachable Init Acts Int B  <= A;     \
   147 \               reachable Init Acts Int A' <= B' |] \
   148 \           ==> LeadsTo Init Acts B B'";
   149 (*PROOF FAILED: why?*)
   150 by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
   151 			       LeadsTo_weaken_L]) 1);
   152 qed "LeadsTo_weaken";
   153 
   154 
   155 (*Set difference: maybe combine with leadsTo_weaken_L??*)
   156 goal thy
   157   "!!C. [| LeadsTo Init Acts (A-B) C; LeadsTo Init Acts B C; id: Acts |] \
   158 \       ==> LeadsTo Init Acts A C";
   159 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
   160 qed "LeadsTo_Diff";
   161 
   162 
   163 (** Meta or object quantifier ???????????????????
   164     see ball_constrains_UN in UNITY.ML***)
   165 
   166 val prems = goal thy
   167    "(!! i. i:I ==> LeadsTo Init Acts (A i) (A' i)) \
   168 \   ==> LeadsTo Init Acts (UN i:I. A i) (UN i:I. A' i)";
   169 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
   170 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
   171                         addIs prems) 1);
   172 qed "LeadsTo_UN_UN";
   173 
   174 
   175 (*Version with no index set*)
   176 val prems = goal thy
   177    "(!! i. LeadsTo Init Acts (A i) (A' i)) \
   178 \   ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)";
   179 by (blast_tac (claset() addIs [LeadsTo_UN_UN] 
   180                         addIs prems) 1);
   181 qed "LeadsTo_UN_UN_noindex";
   182 
   183 (*Version with no index set*)
   184 goal thy
   185    "!!Acts. ALL i. LeadsTo Init Acts (A i) (A' i) \
   186 \           ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)";
   187 by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
   188 qed "all_LeadsTo_UN_UN";
   189 
   190 
   191 (*Binary union version*)
   192 goal thy "!!Acts. [| LeadsTo Init Acts A A'; LeadsTo Init Acts B B' |] \
   193 \                 ==> LeadsTo Init Acts (A Un B) (A' Un B')";
   194 by (blast_tac (claset() addIs [LeadsTo_Un, 
   195 			       LeadsTo_weaken_R]) 1);
   196 qed "LeadsTo_Un_Un";
   197 
   198 
   199 (** The cancellation law **)
   200 
   201 goal thy
   202    "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts B B'; \
   203 \              id: Acts |]    \
   204 \           ==> LeadsTo Init Acts A (A' Un B')";
   205 by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
   206 			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
   207 qed "LeadsTo_cancel2";
   208 
   209 goal thy
   210    "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts (B-A') B'; id: Acts |] \
   211 \           ==> LeadsTo Init Acts A (A' Un B')";
   212 by (rtac LeadsTo_cancel2 1);
   213 by (assume_tac 2);
   214 by (ALLGOALS Asm_simp_tac);
   215 qed "LeadsTo_cancel_Diff2";
   216 
   217 goal thy
   218    "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts B B'; id: Acts |] \
   219 \           ==> LeadsTo Init Acts A (B' Un A')";
   220 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
   221 by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
   222 qed "LeadsTo_cancel1";
   223 
   224 goal thy
   225    "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts (B-A') B'; id: Acts |] \
   226 \           ==> LeadsTo Init Acts A (B' Un A')";
   227 by (rtac LeadsTo_cancel1 1);
   228 by (assume_tac 2);
   229 by (ALLGOALS Asm_simp_tac);
   230 qed "LeadsTo_cancel_Diff1";
   231 
   232 
   233 
   234 (** The impossibility law **)
   235 
   236 goalw thy [LeadsTo_def]
   237     "!!Acts. LeadsTo Init Acts A {} ==> reachable Init Acts Int A  = {}";
   238 by (Full_simp_tac 1);
   239 by (etac leadsTo_empty 1);
   240 qed "LeadsTo_empty";
   241 
   242 
   243 (** PSP: Progress-Safety-Progress **)
   244 
   245 (*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
   246 goalw thy [LeadsTo_def]
   247    "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
   248 \           ==> LeadsTo Init Acts (A Int B) (A' Int B)";
   249 by (asm_simp_tac (simpset() addsimps [Int_assoc RS sym, PSP_stable]) 1);
   250 qed "R_PSP_stable";
   251 
   252 goal thy
   253    "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
   254 \           ==> LeadsTo Init Acts (B Int A) (B Int A')";
   255 by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1);
   256 qed "R_PSP_stable2";
   257 
   258 
   259 goalw thy [LeadsTo_def]
   260    "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
   261 \           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un (B' - B))";
   262 by (dtac PSP 1);
   263 by (etac constrains_reachable 1);
   264 by (etac leadsTo_weaken 2);
   265 by (ALLGOALS Blast_tac);
   266 qed "R_PSP";
   267 
   268 goal thy
   269    "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
   270 \           ==> LeadsTo Init Acts (B Int A) ((B Int A') Un (B' - B))";
   271 by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
   272 qed "R_PSP2";
   273 
   274 goalw thy [unless_def]
   275    "!!Acts. [| LeadsTo Init Acts A A'; unless Acts B B'; id: Acts |] \
   276 \           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un B')";
   277 by (dtac R_PSP 1);
   278 by (assume_tac 1);
   279 by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
   280 by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
   281 by (etac LeadsTo_Diff 2);
   282 by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2);
   283 by Auto_tac;
   284 qed "R_PSP_unless";
   285 
   286 
   287 (*** Induction rules ***)
   288 
   289 (** Meta or object quantifier ????? **)
   290 goalw thy [LeadsTo_def]
   291    "!!Acts. [| wf r;     \
   292 \              ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
   293 \                                       ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   294 \              id: Acts |] \
   295 \           ==> LeadsTo Init Acts A B";
   296 by (etac leadsTo_wf_induct 1);
   297 by (assume_tac 2);
   298 by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   299 qed "LeadsTo_wf_induct";
   300 
   301 
   302 goal thy
   303    "!!Acts. [| wf r;     \
   304 \              ALL m:I. LeadsTo Init Acts (A Int f-``{m})                   \
   305 \                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   306 \              id: Acts |] \
   307 \           ==> LeadsTo Init Acts A ((A - (f-``I)) Un B)";
   308 by (etac LeadsTo_wf_induct 1);
   309 by Safe_tac;
   310 by (case_tac "m:I" 1);
   311 by (blast_tac (claset() addIs [LeadsTo_weaken]) 1);
   312 by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1);
   313 qed "R_bounded_induct";
   314 
   315 
   316 goal thy
   317    "!!Acts. [| ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
   318 \                                  ((A Int f-``(lessThan m)) Un B);   \
   319 \              id: Acts |] \
   320 \           ==> LeadsTo Init Acts A B";
   321 by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
   322 by (assume_tac 2);
   323 by (Asm_simp_tac 1);
   324 qed "R_lessThan_induct";
   325 
   326 goal thy
   327    "!!Acts. [| ALL m:(greaterThan l). LeadsTo Init Acts (A Int f-``{m})   \
   328 \                                        ((A Int f-``(lessThan m)) Un B);   \
   329 \              id: Acts |] \
   330 \           ==> LeadsTo Init Acts A ((A Int (f-``(atMost l))) Un B)";
   331 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
   332 by (rtac (wf_less_than RS R_bounded_induct) 1);
   333 by (assume_tac 2);
   334 by (Asm_simp_tac 1);
   335 qed "R_lessThan_bounded_induct";
   336 
   337 goal thy
   338    "!!Acts. [| ALL m:(lessThan l). LeadsTo Init Acts (A Int f-``{m})   \
   339 \                                    ((A Int f-``(greaterThan m)) Un B);   \
   340 \              id: Acts |] \
   341 \           ==> LeadsTo Init Acts A ((A Int (f-``(atLeast l))) Un B)";
   342 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
   343     (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
   344 by (assume_tac 2);
   345 by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
   346 by (Clarify_tac 1);
   347 by (case_tac "m<l" 1);
   348 by (blast_tac (claset() addIs [not_leE, subset_imp_LeadsTo]) 2);
   349 by (blast_tac (claset() addIs [LeadsTo_weaken_R, diff_less_mono2]) 1);
   350 qed "R_greaterThan_bounded_induct";
   351 
   352 
   353 
   354 (*** Completion: Binary and General Finite versions ***)
   355 
   356 goalw thy [LeadsTo_def]
   357    "!!Acts. [| LeadsTo Init Acts A A';  stable Acts A';   \
   358 \              LeadsTo Init Acts B B';  stable Acts B';  id: Acts |] \
   359 \           ==> LeadsTo Init Acts (A Int B) (A' Int B')";
   360 by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
   361                         addSIs [stable_Int, stable_reachable]) 1);
   362 qed "R_stable_completion";
   363 
   364 
   365 goal thy
   366    "!!Acts. [| finite I;  id: Acts |]                     \
   367 \           ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i)) -->  \
   368 \               (ALL i:I. stable Acts (A' i)) -->         \
   369 \               LeadsTo Init Acts (INT i:I. A i) (INT i:I. A' i)";
   370 by (etac finite_induct 1);
   371 by (Asm_simp_tac 1);
   372 by (asm_simp_tac 
   373     (simpset() addsimps [R_stable_completion, stable_def, 
   374 			 ball_constrains_INT]) 1);
   375 qed_spec_mp "R_finite_stable_completion";
   376 
   377 
   378 goalw thy [LeadsTo_def]
   379  "!!Acts. [| LeadsTo Init Acts A (A' Un C);  constrains Acts A' (A' Un C); \
   380 \            LeadsTo Init Acts B (B' Un C);  constrains Acts B' (B' Un C); \
   381 \            id: Acts |] \
   382 \         ==> LeadsTo Init Acts (A Int B) ((A' Int B') Un C)";
   383 
   384 by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
   385 by (dtac completion 1);
   386 by (assume_tac 2);
   387 by (ALLGOALS 
   388     (asm_simp_tac 
   389      (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
   390 by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   391 qed "R_completion";
   392 
   393 
   394 goal thy
   395    "!!Acts. [| finite I;  id: Acts |] \
   396 \           ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i Un C)) -->  \
   397 \               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
   398 \               LeadsTo Init Acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
   399 by (etac finite_induct 1);
   400 by (ALLGOALS Asm_simp_tac);
   401 by (Clarify_tac 1);
   402 by (dtac ball_constrains_INT 1);
   403 by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1); 
   404 qed "R_finite_completion";
   405