src/HOL/UNITY/UNITY.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/UNITY
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The basic UNITY theory (revised version, based upon the "co" operator)
     7 
     8 From Misra, "A Logic for Concurrent Programming", 1994
     9 *)
    10 
    11 set proof_timing;
    12 HOL_quantifiers := false;
    13 
    14 
    15 (*CAN BOOLEAN SIMPLIFICATION BE AUTOMATED?*)
    16 
    17 (** Rewrites rules to eliminate A.  Conditions can be satisfied by letting B
    18     be any set including A Int C and contained in A Un C, such as B=A or B=C.
    19 **)
    20 
    21 goal thy "!!x. [| A Int C <= B; B <= A Un C |] \
    22 \              ==> (A Int B) Un (Compl A Int C) = B Un C";
    23 by (Blast_tac 1);
    24 
    25 goal thy "!!x. [| A Int C <= B; B <= A Un C |] \
    26 \              ==> (A Un B) Int (Compl A Un C) = B Int C";
    27 by (Blast_tac 1);
    28 
    29 (*The base B=A*)
    30 goal thy "A Un (Compl A Int C) = A Un C";
    31 by (Blast_tac 1);
    32 
    33 goal thy "A Int (Compl A Un C) = A Int C";
    34 by (Blast_tac 1);
    35 
    36 (*The base B=C*)
    37 goal thy "(A Int C) Un (Compl A Int C) = C";
    38 by (Blast_tac 1);
    39 
    40 goal thy "(A Un C) Int (Compl A Un C) = C";
    41 by (Blast_tac 1);
    42 
    43 
    44 (** More ad-hoc rules **)
    45 
    46 goal thy "A Un B - (A - B) = B";
    47 by (Blast_tac 1);
    48 qed "Un_Diff_Diff";
    49 
    50 goal thy "A Int (B - C) Un C = A Int B Un C";
    51 by (Blast_tac 1);
    52 qed "Int_Diff_Un";
    53 
    54 
    55 open UNITY;
    56 
    57 
    58 (*** constrains ***)
    59 
    60 val prems = goalw thy [constrains_def]
    61     "(!!act s s'. [| act: Acts;  (s,s') : act;  s: A |] ==> s': A') \
    62 \    ==> constrains Acts A A'";
    63 by (blast_tac (claset() addIs prems) 1);
    64 qed "constrainsI";
    65 
    66 goalw thy [constrains_def]
    67     "!!Acts. [| constrains Acts A A'; act: Acts;  (s,s'): act;  s: A |] \
    68 \            ==> s': A'";
    69 by (Blast_tac 1);
    70 qed "constrainsD";
    71 
    72 goalw thy [constrains_def] "constrains Acts {} B";
    73 by (Blast_tac 1);
    74 qed "constrains_empty";
    75 
    76 goalw thy [constrains_def] "constrains Acts A UNIV";
    77 by (Blast_tac 1);
    78 qed "constrains_UNIV";
    79 AddIffs [constrains_empty, constrains_UNIV];
    80 
    81 goalw thy [constrains_def]
    82     "!!Acts. [| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'";
    83 by (Blast_tac 1);
    84 qed "constrains_weaken_R";
    85 
    86 goalw thy [constrains_def]
    87     "!!Acts. [| constrains Acts A A'; B<=A |] ==> constrains Acts B A'";
    88 by (Blast_tac 1);
    89 qed "constrains_weaken_L";
    90 
    91 goalw thy [constrains_def]
    92    "!!Acts. [| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'";
    93 by (Blast_tac 1);
    94 qed "constrains_weaken";
    95 
    96 (*Set difference: UNUSED*)
    97 goalw thy [constrains_def]
    98   "!!C. [| constrains Acts (A-B) C; constrains Acts B C |] \
    99 \       ==> constrains Acts A C";
   100 by (Blast_tac 1);
   101 qed "constrains_Diff";
   102 
   103 (** Union **)
   104 
   105 goalw thy [constrains_def]
   106     "!!Acts. [| constrains Acts A A'; constrains Acts B B' |]   \
   107 \           ==> constrains Acts (A Un B) (A' Un B')";
   108 by (Blast_tac 1);
   109 qed "constrains_Un";
   110 
   111 goalw thy [constrains_def]
   112     "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
   113 \    ==> constrains Acts (UN i:I. A i) (UN i:I. A' i)";
   114 by (Blast_tac 1);
   115 qed "ball_constrains_UN";
   116 
   117 goalw thy [constrains_def]
   118     "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
   119 \           ==> constrains Acts (UN i. A i) (UN i. A' i)";
   120 by (Blast_tac 1);
   121 qed "all_constrains_UN";
   122 
   123 (** Intersection **)
   124 
   125 goalw thy [constrains_def]
   126     "!!Acts. [| constrains Acts A A'; constrains Acts B B' |]   \
   127 \           ==> constrains Acts (A Int B) (A' Int B')";
   128 by (Blast_tac 1);
   129 qed "constrains_Int";
   130 
   131 goalw thy [constrains_def]
   132     "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
   133 \    ==> constrains Acts (INT i:I. A i) (INT i:I. A' i)";
   134 by (Blast_tac 1);
   135 qed "ball_constrains_INT";
   136 
   137 goalw thy [constrains_def]
   138     "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
   139 \           ==> constrains Acts (INT i. A i) (INT i. A' i)";
   140 by (Blast_tac 1);
   141 qed "all_constrains_INT";
   142 
   143 goalw thy [stable_def, constrains_def]
   144     "!!Acts. [| stable Acts C; constrains Acts A (C Un A') |]   \
   145 \           ==> constrains Acts (C Un A) (C Un A')";
   146 by (Blast_tac 1);
   147 qed "stable_constrains_Un";
   148 
   149 goalw thy [stable_def, constrains_def]
   150     "!!Acts. [| stable Acts C; constrains Acts (C Int A) A' |]   \
   151 \           ==> constrains Acts (C Int A) (C Int A')";
   152 by (Blast_tac 1);
   153 qed "stable_constrains_Int";
   154 
   155 
   156 (*** stable ***)
   157 
   158 goalw thy [stable_def]
   159     "!!Acts. constrains Acts A A ==> stable Acts A";
   160 by (assume_tac 1);
   161 qed "stableI";
   162 
   163 goalw thy [stable_def]
   164     "!!Acts. stable Acts A ==> constrains Acts A A";
   165 by (assume_tac 1);
   166 qed "stableD";
   167 
   168 goalw thy [stable_def]
   169     "!!Acts. [| stable Acts A; stable Acts A' |]   \
   170 \           ==> stable Acts (A Un A')";
   171 by (blast_tac (claset() addIs [constrains_Un]) 1);
   172 qed "stable_Un";
   173 
   174 goalw thy [stable_def]
   175     "!!Acts. [| stable Acts A; stable Acts A' |]   \
   176 \           ==> stable Acts (A Int A')";
   177 by (blast_tac (claset() addIs [constrains_Int]) 1);
   178 qed "stable_Int";
   179 
   180 goalw thy [constrains_def]
   181     "!!Acts. [| constrains Acts A A'; id: Acts |] ==> A<=A'";
   182 by (Blast_tac 1);
   183 qed "constrains_imp_subset";
   184 
   185 
   186 goalw thy [constrains_def]
   187     "!!Acts. [| id: Acts; constrains Acts A B; constrains Acts B C |]   \
   188 \           ==> constrains Acts A C";
   189 by (Blast_tac 1);
   190 qed "constrains_trans";
   191 
   192 
   193 (*The Elimination Theorem.  The "free" m has become universally quantified!
   194   Should the premise be !!m instead of ALL m ?  Would make it harder to use
   195   in forward proof.*)
   196 goalw thy [constrains_def]
   197     "!!Acts. [| ALL m. constrains Acts {s. s x = m} (B m) |] \
   198 \           ==> constrains Acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
   199 by (Blast_tac 1);
   200 qed "elimination";
   201 
   202 (*As above, but for the trivial case of a one-variable state, in which the
   203   state is identified with its one variable.*)
   204 goalw thy [constrains_def]
   205     "!!Acts. [| ALL m. constrains Acts {m} (B m) |] \
   206 \           ==> constrains Acts {s. P s} (UN m. {s. P(m)} Int B m)";
   207 by (Blast_tac 1);
   208 qed "elimination_sing";
   209 
   210 
   211 goalw thy [constrains_def]
   212    "!!Acts. [| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \
   213 \           ==> constrains Acts A (A' Un B')";
   214 by (Blast_tac 1);
   215 qed "constrains_cancel";
   216 
   217 
   218 
   219 (*** Theoretical Results from Section 6 ***)
   220 
   221 goalw thy [constrains_def, strongest_rhs_def]
   222     "constrains Acts A (strongest_rhs Acts A )";
   223 by (Blast_tac 1);
   224 qed "constrains_strongest_rhs";
   225 
   226 goalw thy [constrains_def, strongest_rhs_def]
   227     "!!Acts. constrains Acts A B ==> strongest_rhs Acts A <= B";
   228 by (Blast_tac 1);
   229 qed "strongest_rhs_is_strongest";