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";
```