src/HOL/UNITY/UNITY.ML
author paulson
Thu Oct 15 11:35:07 1998 +0200 (1998-10-15)
changeset 5648 fe887910e32e
parent 5608 a82a038a3e7a
child 5669 f5d9caafc3bd
permissions -rw-r--r--
specifications as sets of programs
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@5648
    17
overload_1st_set "UNITY.constrains";
paulson@5648
    18
overload_1st_set "UNITY.stable";
paulson@5648
    19
overload_1st_set "UNITY.unless";
paulson@5340
    20
paulson@5277
    21
val prems = Goalw [constrains_def]
paulson@5648
    22
    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
paulson@5648
    23
\    ==> F : constrains A A'";
paulson@4776
    24
by (blast_tac (claset() addIs prems) 1);
paulson@4776
    25
qed "constrainsI";
paulson@4776
    26
wenzelm@5069
    27
Goalw [constrains_def]
paulson@5648
    28
    "[| F : constrains A A'; act: Acts F;  (s,s'): act;  s: A |] ==> s': A'";
paulson@4776
    29
by (Blast_tac 1);
paulson@4776
    30
qed "constrainsD";
paulson@4776
    31
paulson@5648
    32
Goalw [constrains_def] "F : constrains {} B";
paulson@4776
    33
by (Blast_tac 1);
paulson@4776
    34
qed "constrains_empty";
paulson@4776
    35
paulson@5648
    36
Goalw [constrains_def] "F : constrains A UNIV";
paulson@4776
    37
by (Blast_tac 1);
paulson@4776
    38
qed "constrains_UNIV";
paulson@4776
    39
AddIffs [constrains_empty, constrains_UNIV];
paulson@4776
    40
paulson@5648
    41
(*monotonic in 2nd argument*)
wenzelm@5069
    42
Goalw [constrains_def]
paulson@5648
    43
    "[| F : constrains A A'; A'<=B' |] ==> F : constrains A B'";
paulson@4776
    44
by (Blast_tac 1);
paulson@4776
    45
qed "constrains_weaken_R";
paulson@4776
    46
paulson@5648
    47
(*anti-monotonic in 1st argument*)
wenzelm@5069
    48
Goalw [constrains_def]
paulson@5648
    49
    "[| F : constrains A A'; B<=A |] ==> F : constrains B A'";
paulson@4776
    50
by (Blast_tac 1);
paulson@4776
    51
qed "constrains_weaken_L";
paulson@4776
    52
wenzelm@5069
    53
Goalw [constrains_def]
paulson@5648
    54
   "[| F : constrains A A'; B<=A; A'<=B' |] ==> F : constrains B B'";
paulson@4776
    55
by (Blast_tac 1);
paulson@4776
    56
qed "constrains_weaken";
paulson@4776
    57
paulson@4776
    58
(** Union **)
paulson@4776
    59
wenzelm@5069
    60
Goalw [constrains_def]
paulson@5648
    61
    "[| F : constrains A A'; F : constrains B B' |]   \
paulson@5648
    62
\    ==> F : constrains (A Un B) (A' Un B')";
paulson@4776
    63
by (Blast_tac 1);
paulson@4776
    64
qed "constrains_Un";
paulson@4776
    65
wenzelm@5069
    66
Goalw [constrains_def]
paulson@5648
    67
    "ALL i:I. F : constrains (A i) (A' i) \
paulson@5648
    68
\    ==> F : constrains (UN i:I. A i) (UN i:I. A' i)";
paulson@4776
    69
by (Blast_tac 1);
paulson@4776
    70
qed "ball_constrains_UN";
paulson@4776
    71
wenzelm@5069
    72
Goalw [constrains_def]
paulson@5648
    73
    "[| ALL i. F : constrains (A i) (A' i) |] \
paulson@5648
    74
\    ==> F : constrains (UN i. A i) (UN i. A' i)";
paulson@4776
    75
by (Blast_tac 1);
paulson@4776
    76
qed "all_constrains_UN";
paulson@4776
    77
paulson@4776
    78
(** Intersection **)
paulson@4776
    79
wenzelm@5069
    80
Goalw [constrains_def]
paulson@5648
    81
    "[| F : constrains A A'; F : constrains B B' |]   \
paulson@5648
    82
\    ==> F : constrains (A Int B) (A' Int B')";
paulson@4776
    83
by (Blast_tac 1);
paulson@4776
    84
qed "constrains_Int";
paulson@4776
    85
wenzelm@5069
    86
Goalw [constrains_def]
paulson@5648
    87
    "ALL i:I. F : constrains (A i) (A' i) \
paulson@5648
    88
\    ==> F : constrains (INT i:I. A i) (INT i:I. A' i)";
paulson@4776
    89
by (Blast_tac 1);
paulson@4776
    90
qed "ball_constrains_INT";
paulson@4776
    91
wenzelm@5069
    92
Goalw [constrains_def]
paulson@5648
    93
    "[| ALL i. F : constrains (A i) (A' i) |] \
paulson@5648
    94
\    ==> F : constrains (INT i. A i) (INT i. A' i)";
paulson@4776
    95
by (Blast_tac 1);
paulson@4776
    96
qed "all_constrains_INT";
paulson@4776
    97
paulson@5648
    98
Goalw [constrains_def] "[| F : constrains A A' |] ==> A<=A'";
paulson@4776
    99
by (Blast_tac 1);
paulson@5277
   100
qed "constrains_imp_subset";
paulson@4776
   101
paulson@5277
   102
Goalw [constrains_def]
paulson@5648
   103
    "[| F : constrains A B; F : constrains B C |]   \
paulson@5648
   104
\    ==> F : constrains A C";
paulson@4776
   105
by (Blast_tac 1);
paulson@5277
   106
qed "constrains_trans";
paulson@4776
   107
paulson@4776
   108
paulson@4776
   109
(*** stable ***)
paulson@4776
   110
paulson@5648
   111
Goalw [stable_def] "F : constrains A A ==> F : stable A";
paulson@4776
   112
by (assume_tac 1);
paulson@4776
   113
qed "stableI";
paulson@4776
   114
paulson@5648
   115
Goalw [stable_def] "F : stable A ==> F : constrains A A";
paulson@4776
   116
by (assume_tac 1);
paulson@4776
   117
qed "stableD";
paulson@4776
   118
wenzelm@5069
   119
Goalw [stable_def]
paulson@5648
   120
    "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')";
paulson@4776
   121
by (blast_tac (claset() addIs [constrains_Un]) 1);
paulson@4776
   122
qed "stable_Un";
paulson@4776
   123
wenzelm@5069
   124
Goalw [stable_def]
paulson@5648
   125
    "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
paulson@4776
   126
by (blast_tac (claset() addIs [constrains_Int]) 1);
paulson@4776
   127
qed "stable_Int";
paulson@4776
   128
paulson@5277
   129
Goalw [stable_def, constrains_def]
paulson@5648
   130
    "[| F : stable C; F : constrains A (C Un A') |]   \
paulson@5648
   131
\    ==> F : constrains (C Un A) (C Un A')";
paulson@4776
   132
by (Blast_tac 1);
paulson@5277
   133
qed "stable_constrains_Un";
paulson@4776
   134
paulson@5277
   135
Goalw [stable_def, constrains_def]
paulson@5648
   136
    "[| F : stable C; F : constrains (C Int A) A' |]   \
paulson@5648
   137
\    ==> F : constrains (C Int A) (C Int A')";
paulson@4776
   138
by (Blast_tac 1);
paulson@5277
   139
qed "stable_constrains_Int";
paulson@4776
   140
paulson@5648
   141
Goal "Init F <= reachable F";
paulson@5648
   142
by (blast_tac (claset() addIs reachable.intrs) 1);
paulson@5648
   143
qed "Init_subset_reachable";
paulson@4776
   144
paulson@5648
   145
Goal "Acts G <= Acts F ==> G : stable (reachable F)";
paulson@5648
   146
by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
paulson@5648
   147
qed "stable_reachable";
paulson@5648
   148
paulson@5648
   149
(*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*)
paulson@5648
   150
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
paulson@5648
   151
paulson@5648
   152
paulson@5648
   153
(*** invariant & always ***)
paulson@5648
   154
paulson@5648
   155
Goal "[| Init F<=A;  F: stable A |] ==> F : invariant A";
paulson@5648
   156
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
paulson@5648
   157
qed "invariantI";
paulson@5648
   158
paulson@5648
   159
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
paulson@5648
   160
Goal "[| F : invariant A;  F : invariant B |] ==> F : invariant (A Int B)";
paulson@5648
   161
by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
paulson@5648
   162
qed "invariant_Int";
paulson@5648
   163
paulson@5648
   164
(*The set of all reachable states is an invariant...*)
paulson@5648
   165
Goal "F : invariant (reachable F)";
paulson@5648
   166
by (simp_tac (simpset() addsimps [invariant_def]) 1);
paulson@5648
   167
by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
paulson@5648
   168
qed "invariant_reachable";
paulson@5648
   169
paulson@5648
   170
(*...in fact the strongest invariant!*)
paulson@5648
   171
Goal "F : invariant A ==> reachable F <= A";
paulson@5648
   172
by (full_simp_tac 
paulson@5648
   173
    (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
paulson@5648
   174
by (rtac subsetI 1);
paulson@5648
   175
by (etac reachable.induct 1);
paulson@5648
   176
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
paulson@5648
   177
qed "invariant_includes_reachable";
paulson@5648
   178
paulson@5648
   179
Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
paulson@5648
   180
by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
paulson@5648
   181
                               stable_reachable,
paulson@5648
   182
			       impOfSubs invariant_includes_reachable]) 1);
paulson@5648
   183
qed "always_eq_UN_invariant";
paulson@5648
   184
paulson@5648
   185
Goal "F : always A = (EX I. F: invariant I & I <= A)";
paulson@5648
   186
by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
paulson@5648
   187
by (Blast_tac 1);
paulson@5648
   188
qed "always_iff_ex_invariant";
paulson@5648
   189
paulson@5648
   190
paulson@5648
   191
(*** increasing ***)
paulson@5648
   192
paulson@5648
   193
Goalw [increasing_def, stable_def, constrains_def]
paulson@5648
   194
     "increasing f <= increasing (length o f)";
paulson@5648
   195
by Auto_tac;
paulson@5648
   196
by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
paulson@5648
   197
qed "increasing_length";
paulson@5648
   198
paulson@5648
   199
Goalw [increasing_def]
paulson@5648
   200
     "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}";
paulson@5648
   201
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
paulson@5648
   202
by (Blast_tac 1);
paulson@5648
   203
qed "increasing_less";
paulson@5648
   204
paulson@5648
   205
paulson@5648
   206
(** The Elimination Theorem.  The "free" m has become universally quantified!
paulson@5648
   207
    Should the premise be !!m instead of ALL m ?  Would make it harder to use
paulson@5648
   208
    in forward proof. **)
paulson@5648
   209
wenzelm@5069
   210
Goalw [constrains_def]
paulson@5648
   211
    "[| ALL m. F : constrains {s. s x = m} (B m) |] \
paulson@5648
   212
\    ==> F : constrains {s. s x : M} (UN m:M. B m)";
paulson@4776
   213
by (Blast_tac 1);
paulson@4776
   214
qed "elimination";
paulson@4776
   215
paulson@4776
   216
(*As above, but for the trivial case of a one-variable state, in which the
paulson@4776
   217
  state is identified with its one variable.*)
wenzelm@5069
   218
Goalw [constrains_def]
paulson@5648
   219
    "(ALL m. F : constrains {m} (B m)) ==> F : constrains M (UN m:M. B m)";
paulson@4776
   220
by (Blast_tac 1);
paulson@4776
   221
qed "elimination_sing";
paulson@4776
   222
paulson@4776
   223
wenzelm@5069
   224
Goalw [constrains_def]
paulson@5648
   225
   "[| F : constrains A (A' Un B); F : constrains B B' |] \
paulson@5648
   226
\   ==> F : constrains A (A' Un B')";
paulson@4776
   227
by (Blast_tac 1);
paulson@4776
   228
qed "constrains_cancel";
paulson@4776
   229
paulson@4776
   230
paulson@4776
   231
paulson@4776
   232
(*** Theoretical Results from Section 6 ***)
paulson@4776
   233
wenzelm@5069
   234
Goalw [constrains_def, strongest_rhs_def]
paulson@5648
   235
    "F : constrains A (strongest_rhs F A )";
paulson@4776
   236
by (Blast_tac 1);
paulson@4776
   237
qed "constrains_strongest_rhs";
paulson@4776
   238
wenzelm@5069
   239
Goalw [constrains_def, strongest_rhs_def]
paulson@5648
   240
    "F : constrains A B ==> strongest_rhs F A <= B";
paulson@4776
   241
by (Blast_tac 1);
paulson@4776
   242
qed "strongest_rhs_is_strongest";