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