src/HOL/UNITY/Constrains.ML
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
child 5319 7356d0c88b1b
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
paulson@5313
     1
(*  Title:      HOL/UNITY/Constrains
paulson@5313
     2
    ID:         $Id$
paulson@5313
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5313
     4
    Copyright   1998  University of Cambridge
paulson@5313
     5
paulson@5313
     6
Safety relations: restricted to the set of reachable states.
paulson@5313
     7
*)
paulson@5313
     8
paulson@5313
     9
paulson@5313
    10
paulson@5313
    11
(**MOVE TO EQUALITIES.ML**)
paulson@5313
    12
paulson@5313
    13
Goal "(A Un B <= C) = (A <= C & B <= C)";
paulson@5313
    14
by (Blast_tac 1);
paulson@5313
    15
qed "Un_subset_iff";
paulson@5313
    16
paulson@5313
    17
Goal "(C <= A Int B) = (C <= A & C <= B)";
paulson@5313
    18
by (Blast_tac 1);
paulson@5313
    19
qed "Int_subset_iff";
paulson@5313
    20
paulson@5313
    21
paulson@5313
    22
(*** Constrains ***)
paulson@5313
    23
paulson@5313
    24
(*constrains (Acts prg) B B'
paulson@5313
    25
  ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
paulson@5313
    26
bind_thm ("constrains_reachable_Int",
paulson@5313
    27
	  subset_refl RS
paulson@5313
    28
	  rewrite_rule [stable_def] stable_reachable RS 
paulson@5313
    29
	  constrains_Int);
paulson@5313
    30
paulson@5313
    31
Goalw [Constrains_def]
paulson@5313
    32
    "constrains (Acts prg) A A' ==> Constrains prg A A'";
paulson@5313
    33
by (etac constrains_reachable_Int 1);
paulson@5313
    34
qed "constrains_imp_Constrains";
paulson@5313
    35
paulson@5313
    36
val prems = Goal
paulson@5313
    37
    "(!!act s s'. [| act: Acts prg;  (s,s') : act;  s: A |] ==> s': A') \
paulson@5313
    38
\    ==> Constrains prg A A'";
paulson@5313
    39
by (rtac constrains_imp_Constrains 1);
paulson@5313
    40
by (blast_tac (claset() addIs (constrainsI::prems)) 1);
paulson@5313
    41
qed "ConstrainsI";
paulson@5313
    42
paulson@5313
    43
Goalw [Constrains_def, constrains_def] "Constrains prg {} B";
paulson@5313
    44
by (Blast_tac 1);
paulson@5313
    45
qed "Constrains_empty";
paulson@5313
    46
paulson@5313
    47
Goal "Constrains prg A UNIV";
paulson@5313
    48
by (blast_tac (claset() addIs [ConstrainsI]) 1);
paulson@5313
    49
qed "Constrains_UNIV";
paulson@5313
    50
AddIffs [Constrains_empty, Constrains_UNIV];
paulson@5313
    51
paulson@5313
    52
paulson@5313
    53
Goalw [Constrains_def]
paulson@5313
    54
    "[| Constrains prg A A'; A'<=B' |] ==> Constrains prg A B'";
paulson@5313
    55
by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
paulson@5313
    56
qed "Constrains_weaken_R";
paulson@5313
    57
paulson@5313
    58
Goalw [Constrains_def]
paulson@5313
    59
    "[| Constrains prg A A'; B<=A |] ==> Constrains prg B A'";
paulson@5313
    60
by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
paulson@5313
    61
qed "Constrains_weaken_L";
paulson@5313
    62
paulson@5313
    63
Goalw [Constrains_def]
paulson@5313
    64
   "[| Constrains prg A A'; B<=A; A'<=B' |] ==> Constrains prg B B'";
paulson@5313
    65
by (blast_tac (claset() addIs [constrains_weaken]) 1);
paulson@5313
    66
qed "Constrains_weaken";
paulson@5313
    67
paulson@5313
    68
(** Union **)
paulson@5313
    69
paulson@5313
    70
Goalw [Constrains_def]
paulson@5313
    71
    "[| Constrains prg A A'; Constrains prg B B' |]   \
paulson@5313
    72
\    ==> Constrains prg (A Un B) (A' Un B')";
paulson@5313
    73
by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
paulson@5313
    74
qed "Constrains_Un";
paulson@5313
    75
paulson@5313
    76
Goalw [Constrains_def]
paulson@5313
    77
    "ALL i:I. Constrains prg (A i) (A' i) \
paulson@5313
    78
\    ==> Constrains prg (UN i:I. A i) (UN i:I. A' i)";
paulson@5313
    79
by (dtac ball_constrains_UN 1);
paulson@5313
    80
by (blast_tac (claset() addIs [constrains_weaken]) 1);
paulson@5313
    81
qed "ball_Constrains_UN";
paulson@5313
    82
paulson@5313
    83
(** Intersection **)
paulson@5313
    84
paulson@5313
    85
Goalw [Constrains_def]
paulson@5313
    86
    "[| Constrains prg A A'; Constrains prg B B' |]   \
paulson@5313
    87
\    ==> Constrains prg (A Int B) (A' Int B')";
paulson@5313
    88
by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
paulson@5313
    89
qed "Constrains_Int";
paulson@5313
    90
paulson@5313
    91
Goalw [Constrains_def]
paulson@5313
    92
    "[| ALL i:I. Constrains prg (A i) (A' i) |]   \
paulson@5313
    93
\    ==> Constrains prg (INT i:I. A i) (INT i:I. A' i)";
paulson@5313
    94
by (dtac ball_constrains_INT 1);
paulson@5313
    95
by (blast_tac (claset() addIs [constrains_reachable_Int, constrains_weaken]) 1);
paulson@5313
    96
qed "ball_Constrains_INT";
paulson@5313
    97
paulson@5313
    98
Goalw [Constrains_def]
paulson@5313
    99
     "[| Constrains prg A A'; id: Acts prg |] ==> reachable prg Int A <= A'";
paulson@5313
   100
by (dtac constrains_imp_subset 1);
paulson@5313
   101
by (assume_tac 1);
paulson@5313
   102
by (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]) 1);
paulson@5313
   103
qed "Constrains_imp_subset";
paulson@5313
   104
paulson@5313
   105
Goalw [Constrains_def]
paulson@5313
   106
    "[| id: Acts prg; Constrains prg A B; Constrains prg B C |]   \
paulson@5313
   107
\    ==> Constrains prg A C";
paulson@5313
   108
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
paulson@5313
   109
qed "Constrains_trans";
paulson@5313
   110
paulson@5313
   111
paulson@5313
   112
(*** Stable ***)
paulson@5313
   113
paulson@5313
   114
Goal "Stable prg A = stable (Acts prg) (reachable prg Int A)";
paulson@5313
   115
by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
paulson@5313
   116
qed "Stable_eq_stable";
paulson@5313
   117
paulson@5313
   118
Goalw [Stable_def] "Constrains prg A A ==> Stable prg A";
paulson@5313
   119
by (assume_tac 1);
paulson@5313
   120
qed "StableI";
paulson@5313
   121
paulson@5313
   122
Goalw [Stable_def] "Stable prg A ==> Constrains prg A A";
paulson@5313
   123
by (assume_tac 1);
paulson@5313
   124
qed "StableD";
paulson@5313
   125
paulson@5313
   126
Goalw [Stable_def]
paulson@5313
   127
    "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Un A')";
paulson@5313
   128
by (blast_tac (claset() addIs [Constrains_Un]) 1);
paulson@5313
   129
qed "Stable_Un";
paulson@5313
   130
paulson@5313
   131
Goalw [Stable_def]
paulson@5313
   132
    "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Int A')";
paulson@5313
   133
by (blast_tac (claset() addIs [Constrains_Int]) 1);
paulson@5313
   134
qed "Stable_Int";
paulson@5313
   135
paulson@5313
   136
Goalw [Stable_def]
paulson@5313
   137
    "[| Stable prg C; Constrains prg A (C Un A') |]   \
paulson@5313
   138
\    ==> Constrains prg (C Un A) (C Un A')";
paulson@5313
   139
by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
paulson@5313
   140
qed "Stable_Constrains_Un";
paulson@5313
   141
paulson@5313
   142
Goalw [Stable_def]
paulson@5313
   143
    "[| Stable prg C; Constrains prg (C Int A) A' |]   \
paulson@5313
   144
\    ==> Constrains prg (C Int A) (C Int A')";
paulson@5313
   145
by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
paulson@5313
   146
qed "Stable_Constrains_Int";
paulson@5313
   147
paulson@5313
   148
Goalw [Stable_def]
paulson@5313
   149
    "(ALL i:I. Stable prg (A i)) ==> Stable prg (INT i:I. A i)";
paulson@5313
   150
by (etac ball_Constrains_INT 1);
paulson@5313
   151
qed "ball_Stable_INT";
paulson@5313
   152
paulson@5313
   153
Goal "Stable prg (reachable prg)";
paulson@5313
   154
by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
paulson@5313
   155
qed "Stable_reachable";
paulson@5313
   156
paulson@5313
   157
paulson@5313
   158
paulson@5313
   159
(*** The Elimination Theorem.  The "free" m has become universally quantified!
paulson@5313
   160
     Should the premise be !!m instead of ALL m ?  Would make it harder to use
paulson@5313
   161
     in forward proof. ***)
paulson@5313
   162
paulson@5313
   163
Goalw [Constrains_def, constrains_def]
paulson@5313
   164
    "[| ALL m. Constrains prg {s. s x = m} (B m) |] \
paulson@5313
   165
\    ==> Constrains prg {s. s x : M} (UN m:M. B m)";
paulson@5313
   166
by (Blast_tac 1);
paulson@5313
   167
qed "Elimination";
paulson@5313
   168
paulson@5313
   169
(*As above, but for the trivial case of a one-variable state, in which the
paulson@5313
   170
  state is identified with its one variable.*)
paulson@5313
   171
Goalw [Constrains_def, constrains_def]
paulson@5313
   172
    "(ALL m. Constrains prg {m} (B m)) ==> Constrains prg M (UN m:M. B m)";
paulson@5313
   173
by (Blast_tac 1);
paulson@5313
   174
qed "Elimination_sing";
paulson@5313
   175
paulson@5313
   176
Goalw [Constrains_def, constrains_def]
paulson@5313
   177
   "[| Constrains prg A (A' Un B); Constrains prg B B'; id: Acts prg |] \
paulson@5313
   178
\   ==> Constrains prg A (A' Un B')";
paulson@5313
   179
by (Blast_tac 1);
paulson@5313
   180
qed "Constrains_cancel";
paulson@5313
   181
paulson@5313
   182
paulson@5313
   183
(*** Specialized laws for handling Invariants ***)
paulson@5313
   184
paulson@5313
   185
(** Natural deduction rules for "Invariant prg A" **)
paulson@5313
   186
paulson@5313
   187
Goal "[| Init prg<=A;  Stable prg A |] ==> Invariant prg A";
paulson@5313
   188
by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1);
paulson@5313
   189
qed "InvariantI";
paulson@5313
   190
paulson@5313
   191
Goal "Invariant prg A ==> Init prg<=A & Stable prg A";
paulson@5313
   192
by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1);
paulson@5313
   193
qed "InvariantD";
paulson@5313
   194
paulson@5313
   195
bind_thm ("InvariantE", InvariantD RS conjE);
paulson@5313
   196
paulson@5313
   197
paulson@5313
   198
(*The set of all reachable states is an Invariant...*)
paulson@5313
   199
Goal "Invariant prg (reachable prg)";
paulson@5313
   200
by (simp_tac (simpset() addsimps [Invariant_def]) 1);
paulson@5313
   201
by (blast_tac (claset() addIs (Stable_reachable::reachable.intrs)) 1);
paulson@5313
   202
qed "Invariant_reachable";
paulson@5313
   203
paulson@5313
   204
(*...in fact the strongest Invariant!*)
paulson@5313
   205
Goal "Invariant prg A ==> reachable prg <= A";
paulson@5313
   206
by (full_simp_tac 
paulson@5313
   207
    (simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
paulson@5313
   208
			 Invariant_def]) 1);
paulson@5313
   209
by (rtac subsetI 1);
paulson@5313
   210
by (etac reachable.induct 1);
paulson@5313
   211
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
paulson@5313
   212
qed "Invariant_includes_reachable";
paulson@5313
   213
paulson@5313
   214
paulson@5313
   215
Goal "Invariant prg INV ==> reachable prg Int INV = reachable prg";
paulson@5313
   216
by (dtac Invariant_includes_reachable 1);
paulson@5313
   217
by (Blast_tac 1);
paulson@5313
   218
qed "reachable_Int_INV";
paulson@5313
   219
paulson@5313
   220
Goal "[| Invariant prg INV;  Constrains prg (INV Int A) A' |]   \
paulson@5313
   221
\     ==> Constrains prg A A'";
paulson@5313
   222
by (asm_full_simp_tac
paulson@5313
   223
    (simpset() addsimps [Constrains_def, reachable_Int_INV,
paulson@5313
   224
			 Int_assoc RS sym]) 1);
paulson@5313
   225
qed "Invariant_ConstrainsI";
paulson@5313
   226
paulson@5313
   227
bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
paulson@5313
   228
paulson@5313
   229
Goal "[| Invariant prg INV;  Constrains prg A A' |]   \
paulson@5313
   230
\     ==> Constrains prg A (INV Int A')";
paulson@5313
   231
by (asm_full_simp_tac
paulson@5313
   232
    (simpset() addsimps [Constrains_def, reachable_Int_INV,
paulson@5313
   233
			 Int_assoc RS sym]) 1);
paulson@5313
   234
qed "Invariant_ConstrainsD";
paulson@5313
   235
paulson@5313
   236
bind_thm ("Invariant_StableD", StableD RSN (2,Invariant_ConstrainsD));
paulson@5313
   237
paulson@5313
   238
paulson@5313
   239
paulson@5313
   240
(** Conjoining Invariants **)
paulson@5313
   241
paulson@5313
   242
Goal "[| Invariant prg A;  Invariant prg B |] ==> Invariant prg (A Int B)";
paulson@5313
   243
by (auto_tac (claset(),
paulson@5313
   244
	      simpset() addsimps [Invariant_def, Stable_Int]));
paulson@5313
   245
qed "Invariant_Int";
paulson@5313
   246
paulson@5313
   247
(*Delete the nearest invariance assumption (which will be the second one
paulson@5313
   248
  used by Invariant_Int) *)
paulson@5313
   249
val Invariant_thin =
paulson@5313
   250
    read_instantiate_sg (sign_of thy)
paulson@5313
   251
                [("V", "Invariant ?Prg ?A")] thin_rl;
paulson@5313
   252
paulson@5313
   253
(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
paulson@5313
   254
val Invariant_Int_tac = dtac Invariant_Int THEN' 
paulson@5313
   255
                        assume_tac THEN'
paulson@5313
   256
			etac Invariant_thin;
paulson@5313
   257
paulson@5313
   258
(*Combines two invariance THEOREMS into one.*)
paulson@5313
   259
val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
paulson@5313
   260
paulson@5313
   261
paulson@5313
   262