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