src/HOL/UNITY/UNITY.ML
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5340 d75c03cf77b5
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
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
(*** constrains ***)
paulson@4776
    16
paulson@5277
    17
val prems = Goalw [constrains_def]
paulson@5253
    18
    "(!!act s s'. [| act: acts;  (s,s') : act;  s: A |] ==> s': A') \
paulson@5253
    19
\    ==> constrains acts A A'";
paulson@4776
    20
by (blast_tac (claset() addIs prems) 1);
paulson@4776
    21
qed "constrainsI";
paulson@4776
    22
wenzelm@5069
    23
Goalw [constrains_def]
paulson@5313
    24
    "[| constrains acts A A'; act: acts;  (s,s'): act;  s: A |] ==> s': A'";
paulson@4776
    25
by (Blast_tac 1);
paulson@4776
    26
qed "constrainsD";
paulson@4776
    27
paulson@5253
    28
Goalw [constrains_def] "constrains acts {} B";
paulson@4776
    29
by (Blast_tac 1);
paulson@4776
    30
qed "constrains_empty";
paulson@4776
    31
paulson@5253
    32
Goalw [constrains_def] "constrains acts A UNIV";
paulson@4776
    33
by (Blast_tac 1);
paulson@4776
    34
qed "constrains_UNIV";
paulson@4776
    35
AddIffs [constrains_empty, constrains_UNIV];
paulson@4776
    36
wenzelm@5069
    37
Goalw [constrains_def]
paulson@5253
    38
    "[| constrains acts A A'; A'<=B' |] ==> constrains acts A B'";
paulson@4776
    39
by (Blast_tac 1);
paulson@4776
    40
qed "constrains_weaken_R";
paulson@4776
    41
wenzelm@5069
    42
Goalw [constrains_def]
paulson@5253
    43
    "[| constrains acts A A'; B<=A |] ==> constrains acts B A'";
paulson@4776
    44
by (Blast_tac 1);
paulson@4776
    45
qed "constrains_weaken_L";
paulson@4776
    46
wenzelm@5069
    47
Goalw [constrains_def]
paulson@5253
    48
   "[| constrains acts A A'; B<=A; A'<=B' |] ==> constrains acts B B'";
paulson@4776
    49
by (Blast_tac 1);
paulson@4776
    50
qed "constrains_weaken";
paulson@4776
    51
paulson@4776
    52
(** Union **)
paulson@4776
    53
wenzelm@5069
    54
Goalw [constrains_def]
paulson@5253
    55
    "[| constrains acts A A'; constrains acts B B' |]   \
paulson@5277
    56
\    ==> constrains acts (A Un B) (A' Un B')";
paulson@4776
    57
by (Blast_tac 1);
paulson@4776
    58
qed "constrains_Un";
paulson@4776
    59
wenzelm@5069
    60
Goalw [constrains_def]
paulson@5253
    61
    "ALL i:I. constrains acts (A i) (A' i) \
paulson@5253
    62
\    ==> constrains acts (UN i:I. A i) (UN i:I. A' i)";
paulson@4776
    63
by (Blast_tac 1);
paulson@4776
    64
qed "ball_constrains_UN";
paulson@4776
    65
wenzelm@5069
    66
Goalw [constrains_def]
paulson@5253
    67
    "[| ALL i. constrains acts (A i) (A' i) |] \
paulson@5277
    68
\    ==> constrains acts (UN i. A i) (UN i. A' i)";
paulson@4776
    69
by (Blast_tac 1);
paulson@4776
    70
qed "all_constrains_UN";
paulson@4776
    71
paulson@4776
    72
(** Intersection **)
paulson@4776
    73
wenzelm@5069
    74
Goalw [constrains_def]
paulson@5253
    75
    "[| constrains acts A A'; constrains acts B B' |]   \
paulson@5277
    76
\    ==> constrains acts (A Int B) (A' Int B')";
paulson@4776
    77
by (Blast_tac 1);
paulson@4776
    78
qed "constrains_Int";
paulson@4776
    79
wenzelm@5069
    80
Goalw [constrains_def]
paulson@5253
    81
    "ALL i:I. constrains acts (A i) (A' i) \
paulson@5253
    82
\    ==> constrains acts (INT i:I. A i) (INT i:I. A' i)";
paulson@4776
    83
by (Blast_tac 1);
paulson@4776
    84
qed "ball_constrains_INT";
paulson@4776
    85
wenzelm@5069
    86
Goalw [constrains_def]
paulson@5253
    87
    "[| ALL i. constrains acts (A i) (A' i) |] \
paulson@5277
    88
\    ==> constrains acts (INT i. A i) (INT i. A' i)";
paulson@4776
    89
by (Blast_tac 1);
paulson@4776
    90
qed "all_constrains_INT";
paulson@4776
    91
paulson@5313
    92
Goalw [constrains_def] "[| constrains acts A A'; id: acts |] ==> A<=A'";
paulson@4776
    93
by (Blast_tac 1);
paulson@5277
    94
qed "constrains_imp_subset";
paulson@4776
    95
paulson@5277
    96
Goalw [constrains_def]
paulson@5277
    97
    "[| id: acts; constrains acts A B; constrains acts B C |]   \
paulson@5277
    98
\    ==> constrains acts A C";
paulson@4776
    99
by (Blast_tac 1);
paulson@5277
   100
qed "constrains_trans";
paulson@4776
   101
paulson@4776
   102
paulson@4776
   103
(*** stable ***)
paulson@4776
   104
paulson@5313
   105
Goalw [stable_def] "constrains acts A A ==> stable acts A";
paulson@4776
   106
by (assume_tac 1);
paulson@4776
   107
qed "stableI";
paulson@4776
   108
paulson@5313
   109
Goalw [stable_def] "stable acts A ==> constrains acts A A";
paulson@4776
   110
by (assume_tac 1);
paulson@4776
   111
qed "stableD";
paulson@4776
   112
wenzelm@5069
   113
Goalw [stable_def]
paulson@5313
   114
    "[| stable acts A; stable acts A' |] ==> stable acts (A Un A')";
paulson@4776
   115
by (blast_tac (claset() addIs [constrains_Un]) 1);
paulson@4776
   116
qed "stable_Un";
paulson@4776
   117
wenzelm@5069
   118
Goalw [stable_def]
paulson@5313
   119
    "[| stable acts A; stable acts A' |] ==> stable acts (A Int A')";
paulson@4776
   120
by (blast_tac (claset() addIs [constrains_Int]) 1);
paulson@4776
   121
qed "stable_Int";
paulson@4776
   122
paulson@5277
   123
Goalw [stable_def, constrains_def]
paulson@5277
   124
    "[| stable acts C; constrains acts A (C Un A') |]   \
paulson@5277
   125
\    ==> constrains acts (C Un A) (C Un A')";
paulson@4776
   126
by (Blast_tac 1);
paulson@5277
   127
qed "stable_constrains_Un";
paulson@4776
   128
paulson@5277
   129
Goalw [stable_def, constrains_def]
paulson@5277
   130
    "[| stable acts C; constrains acts (C Int A) A' |]   \
paulson@5277
   131
\    ==> constrains acts (C Int A) (C Int A')";
paulson@4776
   132
by (Blast_tac 1);
paulson@5277
   133
qed "stable_constrains_Int";
paulson@4776
   134
paulson@4776
   135
paulson@4776
   136
(*The Elimination Theorem.  The "free" m has become universally quantified!
paulson@4776
   137
  Should the premise be !!m instead of ALL m ?  Would make it harder to use
paulson@4776
   138
  in forward proof.*)
wenzelm@5069
   139
Goalw [constrains_def]
paulson@5253
   140
    "[| ALL m. constrains acts {s. s x = m} (B m) |] \
paulson@5313
   141
\    ==> constrains acts {s. s x : M} (UN m:M. B m)";
paulson@4776
   142
by (Blast_tac 1);
paulson@4776
   143
qed "elimination";
paulson@4776
   144
paulson@5313
   145
paulson@4776
   146
(*As above, but for the trivial case of a one-variable state, in which the
paulson@4776
   147
  state is identified with its one variable.*)
wenzelm@5069
   148
Goalw [constrains_def]
paulson@5313
   149
    "(ALL m. constrains acts {m} (B m)) ==> constrains acts M (UN m:M. B m)";
paulson@4776
   150
by (Blast_tac 1);
paulson@4776
   151
qed "elimination_sing";
paulson@4776
   152
paulson@4776
   153
wenzelm@5069
   154
Goalw [constrains_def]
paulson@5253
   155
   "[| constrains acts A (A' Un B); constrains acts B B'; id: acts |] \
paulson@5277
   156
\   ==> constrains acts A (A' Un B')";
paulson@4776
   157
by (Blast_tac 1);
paulson@4776
   158
qed "constrains_cancel";
paulson@4776
   159
paulson@4776
   160
paulson@4776
   161
paulson@4776
   162
(*** Theoretical Results from Section 6 ***)
paulson@4776
   163
wenzelm@5069
   164
Goalw [constrains_def, strongest_rhs_def]
paulson@5253
   165
    "constrains acts A (strongest_rhs acts A )";
paulson@4776
   166
by (Blast_tac 1);
paulson@4776
   167
qed "constrains_strongest_rhs";
paulson@4776
   168
wenzelm@5069
   169
Goalw [constrains_def, strongest_rhs_def]
paulson@5253
   170
    "constrains acts A B ==> strongest_rhs acts A <= B";
paulson@4776
   171
by (Blast_tac 1);
paulson@4776
   172
qed "strongest_rhs_is_strongest";