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