src/HOL/UNITY/UNITY.ML
author paulson
Wed Apr 28 13:36:31 1999 +0200 (1999-04-28)
changeset 6535 880f31a62784
parent 6295 351b3c2b0d83
child 6536 281d44905cab
permissions -rw-r--r--
eliminated theory UNITY/Traces
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 "UNIV Times UNIV = UNIV";
paulson@6012
    18
by Auto_tac;
paulson@6012
    19
qed "UNIV_Times_UNIV"; 
paulson@6012
    20
Addsimps [UNIV_Times_UNIV];
paulson@6012
    21
paulson@6012
    22
Goal "- (UNIV Times A) = UNIV Times (-A)";
paulson@6012
    23
by Auto_tac;
paulson@6012
    24
qed "Compl_Times_UNIV1"; 
paulson@6012
    25
paulson@6012
    26
Goal "- (A Times UNIV) = (-A) Times UNIV";
paulson@6012
    27
by Auto_tac;
paulson@6012
    28
qed "Compl_Times_UNIV2"; 
paulson@6012
    29
paulson@6012
    30
Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
paulson@6012
    31
paulson@6012
    32
paulson@6535
    33
(*** The abstract type of programs ***)
paulson@6535
    34
paulson@6535
    35
val rep_ss = simpset() addsimps 
paulson@6535
    36
                [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, 
paulson@6535
    37
		 Rep_Program_inverse, Abs_Program_inverse];
paulson@6535
    38
paulson@6535
    39
paulson@6535
    40
Goal "Id : Acts F";
paulson@6535
    41
by (cut_inst_tac [("x", "F")] Rep_Program 1);
paulson@6535
    42
by (auto_tac (claset(), rep_ss));
paulson@6535
    43
qed "Id_in_Acts";
paulson@6535
    44
AddIffs [Id_in_Acts];
paulson@6535
    45
paulson@6535
    46
Goal "insert Id (Acts F) = Acts F";
paulson@6535
    47
by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1);
paulson@6535
    48
qed "insert_Id_Acts";
paulson@6535
    49
AddIffs [insert_Id_Acts];
paulson@6535
    50
paulson@6535
    51
(** Inspectors for type "program" **)
paulson@6535
    52
paulson@6535
    53
Goal "Init (mk_program (init,acts)) = init";
paulson@6535
    54
by (auto_tac (claset(), rep_ss));
paulson@6535
    55
qed "Init_eq";
paulson@6535
    56
paulson@6535
    57
Goal "Acts (mk_program (init,acts)) = insert Id acts";
paulson@6535
    58
by (auto_tac (claset(), rep_ss));
paulson@6535
    59
qed "Acts_eq";
paulson@6535
    60
paulson@6535
    61
Addsimps [Acts_eq, Init_eq];
paulson@6535
    62
paulson@6535
    63
paulson@6535
    64
(** The notation of equality for type "program" **)
paulson@6535
    65
paulson@6535
    66
Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
paulson@6535
    67
by (subgoals_tac ["EX x. Rep_Program F = x",
paulson@6535
    68
		  "EX x. Rep_Program G = x"] 1);
paulson@6535
    69
by (REPEAT (Blast_tac 2));
paulson@6535
    70
by (Clarify_tac 1);
paulson@6535
    71
by (auto_tac (claset(), rep_ss));
paulson@6535
    72
by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
paulson@6535
    73
by (asm_full_simp_tac rep_ss 1);
paulson@6535
    74
qed "program_equalityI";
paulson@6535
    75
paulson@6535
    76
val [major,minor] =
paulson@6535
    77
Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
paulson@6535
    78
by (rtac minor 1);
paulson@6535
    79
by (auto_tac (claset(), simpset() addsimps [major]));
paulson@6535
    80
qed "program_equalityE";
paulson@6535
    81
paulson@6535
    82
paulson@6535
    83
(*** These rules allow "lazy" definition expansion 
paulson@6535
    84
     They avoid expanding the full program, which is a large expression
paulson@6535
    85
***)
paulson@6535
    86
paulson@6535
    87
Goal "F == mk_program (init,acts) ==> Init F = init";
paulson@6535
    88
by Auto_tac;
paulson@6535
    89
qed "def_prg_Init";
paulson@6535
    90
paulson@6535
    91
(*The program is not expanded, but its Init and Acts are*)
paulson@6535
    92
val [rew] = goal thy
paulson@6535
    93
    "[| F == mk_program (init,acts) |] \
paulson@6535
    94
\    ==> Init F = init & Acts F = insert Id acts";
paulson@6535
    95
by (rewtac rew);
paulson@6535
    96
by Auto_tac;
paulson@6535
    97
qed "def_prg_simps";
paulson@6535
    98
paulson@6535
    99
(*An action is expanded only if a pair of states is being tested against it*)
paulson@6535
   100
Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
paulson@6535
   101
by Auto_tac;
paulson@6535
   102
qed "def_act_simp";
paulson@6535
   103
paulson@6535
   104
fun simp_of_act def = def RS def_act_simp;
paulson@6535
   105
paulson@6535
   106
(*A set is expanded only if an element is being tested against it*)
paulson@6535
   107
Goal "A == B ==> (x : A) = (x : B)";
paulson@6535
   108
by Auto_tac;
paulson@6535
   109
qed "def_set_simp";
paulson@6535
   110
paulson@6535
   111
fun simp_of_set def = def RS def_set_simp;
paulson@6535
   112
paulson@6535
   113
paulson@4776
   114
(*** constrains ***)
paulson@4776
   115
paulson@5648
   116
overload_1st_set "UNITY.constrains";
paulson@5648
   117
overload_1st_set "UNITY.stable";
paulson@5648
   118
overload_1st_set "UNITY.unless";
paulson@5340
   119
paulson@5277
   120
val prems = Goalw [constrains_def]
paulson@5648
   121
    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
paulson@5648
   122
\    ==> F : constrains A A'";
paulson@4776
   123
by (blast_tac (claset() addIs prems) 1);
paulson@4776
   124
qed "constrainsI";
paulson@4776
   125
wenzelm@5069
   126
Goalw [constrains_def]
paulson@5648
   127
    "[| F : constrains A A'; act: Acts F;  (s,s'): act;  s: A |] ==> s': A'";
paulson@4776
   128
by (Blast_tac 1);
paulson@4776
   129
qed "constrainsD";
paulson@4776
   130
paulson@5648
   131
Goalw [constrains_def] "F : constrains {} B";
paulson@4776
   132
by (Blast_tac 1);
paulson@4776
   133
qed "constrains_empty";
paulson@4776
   134
paulson@5648
   135
Goalw [constrains_def] "F : constrains A UNIV";
paulson@4776
   136
by (Blast_tac 1);
paulson@4776
   137
qed "constrains_UNIV";
paulson@4776
   138
AddIffs [constrains_empty, constrains_UNIV];
paulson@4776
   139
paulson@5648
   140
(*monotonic in 2nd argument*)
wenzelm@5069
   141
Goalw [constrains_def]
paulson@5648
   142
    "[| F : constrains A A'; A'<=B' |] ==> F : constrains A B'";
paulson@4776
   143
by (Blast_tac 1);
paulson@4776
   144
qed "constrains_weaken_R";
paulson@4776
   145
paulson@5648
   146
(*anti-monotonic in 1st argument*)
wenzelm@5069
   147
Goalw [constrains_def]
paulson@5648
   148
    "[| F : constrains A A'; B<=A |] ==> F : constrains B A'";
paulson@4776
   149
by (Blast_tac 1);
paulson@4776
   150
qed "constrains_weaken_L";
paulson@4776
   151
wenzelm@5069
   152
Goalw [constrains_def]
paulson@5648
   153
   "[| F : constrains A A'; B<=A; A'<=B' |] ==> F : constrains B B'";
paulson@4776
   154
by (Blast_tac 1);
paulson@4776
   155
qed "constrains_weaken";
paulson@4776
   156
paulson@4776
   157
(** Union **)
paulson@4776
   158
wenzelm@5069
   159
Goalw [constrains_def]
paulson@5648
   160
    "[| F : constrains A A'; F : constrains B B' |]   \
paulson@5648
   161
\    ==> F : constrains (A Un B) (A' Un B')";
paulson@4776
   162
by (Blast_tac 1);
paulson@4776
   163
qed "constrains_Un";
paulson@4776
   164
wenzelm@5069
   165
Goalw [constrains_def]
paulson@5648
   166
    "ALL i:I. F : constrains (A i) (A' i) \
paulson@5648
   167
\    ==> F : constrains (UN i:I. A i) (UN i:I. A' i)";
paulson@4776
   168
by (Blast_tac 1);
paulson@4776
   169
qed "ball_constrains_UN";
paulson@4776
   170
paulson@4776
   171
(** Intersection **)
paulson@4776
   172
wenzelm@5069
   173
Goalw [constrains_def]
paulson@5648
   174
    "[| F : constrains A A'; F : constrains B B' |]   \
paulson@5648
   175
\    ==> F : constrains (A Int B) (A' Int B')";
paulson@4776
   176
by (Blast_tac 1);
paulson@4776
   177
qed "constrains_Int";
paulson@4776
   178
wenzelm@5069
   179
Goalw [constrains_def]
paulson@5648
   180
    "ALL i:I. F : constrains (A i) (A' i) \
paulson@5648
   181
\    ==> F : constrains (INT i:I. A i) (INT i:I. A' i)";
paulson@4776
   182
by (Blast_tac 1);
paulson@4776
   183
qed "ball_constrains_INT";
paulson@4776
   184
paulson@6295
   185
Goalw [constrains_def] "F : constrains A A' ==> A <= A'";
paulson@6295
   186
by Auto_tac;
paulson@5277
   187
qed "constrains_imp_subset";
paulson@4776
   188
paulson@6012
   189
(*The reasoning is by subsets since "constrains" refers to single actions
paulson@6012
   190
  only.  So this rule isn't that useful.*)
paulson@6295
   191
Goalw [constrains_def]
paulson@6295
   192
    "[| F : constrains A B; F : constrains B C |]   \
paulson@5648
   193
\    ==> F : constrains A C";
paulson@6295
   194
by (Blast_tac 1);
paulson@5277
   195
qed "constrains_trans";
paulson@4776
   196
paulson@6295
   197
Goalw [constrains_def]
paulson@6295
   198
   "[| F : constrains A (A' Un B); F : constrains B B' |] \
paulson@6295
   199
\   ==> F : constrains A (A' Un B')";
paulson@6295
   200
by (Clarify_tac 1);
paulson@6295
   201
by (Blast_tac 1);
paulson@6012
   202
qed "constrains_cancel";
paulson@6012
   203
paulson@4776
   204
paulson@4776
   205
(*** stable ***)
paulson@4776
   206
paulson@5648
   207
Goalw [stable_def] "F : constrains A A ==> F : stable A";
paulson@4776
   208
by (assume_tac 1);
paulson@4776
   209
qed "stableI";
paulson@4776
   210
paulson@5648
   211
Goalw [stable_def] "F : stable A ==> F : constrains A A";
paulson@4776
   212
by (assume_tac 1);
paulson@4776
   213
qed "stableD";
paulson@4776
   214
paulson@5804
   215
(** Union **)
paulson@5804
   216
wenzelm@5069
   217
Goalw [stable_def]
paulson@5648
   218
    "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')";
paulson@4776
   219
by (blast_tac (claset() addIs [constrains_Un]) 1);
paulson@4776
   220
qed "stable_Un";
paulson@4776
   221
wenzelm@5069
   222
Goalw [stable_def]
paulson@5804
   223
    "ALL i:I. F : stable (A i) ==> F : stable (UN i:I. A i)";
paulson@5804
   224
by (blast_tac (claset() addIs [ball_constrains_UN]) 1);
paulson@5804
   225
qed "ball_stable_UN";
paulson@5804
   226
paulson@5804
   227
(** Intersection **)
paulson@5804
   228
paulson@5804
   229
Goalw [stable_def]
paulson@5648
   230
    "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
paulson@4776
   231
by (blast_tac (claset() addIs [constrains_Int]) 1);
paulson@4776
   232
qed "stable_Int";
paulson@4776
   233
paulson@5804
   234
Goalw [stable_def]
paulson@5804
   235
    "ALL i:I. F : stable (A i) ==> F : stable (INT i:I. A i)";
paulson@5804
   236
by (blast_tac (claset() addIs [ball_constrains_INT]) 1);
paulson@5804
   237
qed "ball_stable_INT";
paulson@5804
   238
paulson@5277
   239
Goalw [stable_def, constrains_def]
paulson@5648
   240
    "[| F : stable C; F : constrains A (C Un A') |]   \
paulson@5648
   241
\    ==> F : constrains (C Un A) (C Un A')";
paulson@4776
   242
by (Blast_tac 1);
paulson@5277
   243
qed "stable_constrains_Un";
paulson@4776
   244
paulson@5277
   245
Goalw [stable_def, constrains_def]
paulson@5648
   246
    "[| F : stable C; F : constrains (C Int A) A' |]   \
paulson@5648
   247
\    ==> F : constrains (C Int A) (C Int A')";
paulson@4776
   248
by (Blast_tac 1);
paulson@5277
   249
qed "stable_constrains_Int";
paulson@4776
   250
paulson@5648
   251
(*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*)
paulson@5648
   252
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
paulson@5648
   253
paulson@5648
   254
paulson@5804
   255
(*** invariant ***)
paulson@5648
   256
paulson@5648
   257
Goal "[| Init F<=A;  F: stable A |] ==> F : invariant A";
paulson@5648
   258
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
paulson@5648
   259
qed "invariantI";
paulson@5648
   260
paulson@5648
   261
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
paulson@5648
   262
Goal "[| F : invariant A;  F : invariant B |] ==> F : invariant (A Int B)";
paulson@5648
   263
by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
paulson@5648
   264
qed "invariant_Int";
paulson@5648
   265
paulson@5648
   266
paulson@5648
   267
(*** increasing ***)
paulson@5648
   268
paulson@5648
   269
Goalw [increasing_def, stable_def, constrains_def]
paulson@5648
   270
     "increasing f <= increasing (length o f)";
paulson@5648
   271
by Auto_tac;
paulson@5648
   272
by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
paulson@5804
   273
qed "increasing_size";
paulson@5648
   274
paulson@5648
   275
Goalw [increasing_def]
paulson@5648
   276
     "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}";
paulson@5648
   277
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
paulson@5648
   278
by (Blast_tac 1);
paulson@5804
   279
qed "increasing_stable_less";
paulson@5648
   280
paulson@5648
   281
paulson@5648
   282
(** The Elimination Theorem.  The "free" m has become universally quantified!
paulson@5648
   283
    Should the premise be !!m instead of ALL m ?  Would make it harder to use
paulson@5648
   284
    in forward proof. **)
paulson@5648
   285
wenzelm@5069
   286
Goalw [constrains_def]
paulson@5648
   287
    "[| ALL m. F : constrains {s. s x = m} (B m) |] \
paulson@5648
   288
\    ==> F : constrains {s. s x : M} (UN m:M. B m)";
paulson@4776
   289
by (Blast_tac 1);
paulson@4776
   290
qed "elimination";
paulson@4776
   291
paulson@4776
   292
(*As above, but for the trivial case of a one-variable state, in which the
paulson@4776
   293
  state is identified with its one variable.*)
wenzelm@5069
   294
Goalw [constrains_def]
paulson@5648
   295
    "(ALL m. F : constrains {m} (B m)) ==> F : constrains M (UN m:M. B m)";
paulson@4776
   296
by (Blast_tac 1);
paulson@4776
   297
qed "elimination_sing";
paulson@4776
   298
paulson@4776
   299
paulson@4776
   300
paulson@4776
   301
(*** Theoretical Results from Section 6 ***)
paulson@4776
   302
wenzelm@5069
   303
Goalw [constrains_def, strongest_rhs_def]
paulson@5648
   304
    "F : constrains A (strongest_rhs F A )";
paulson@4776
   305
by (Blast_tac 1);
paulson@4776
   306
qed "constrains_strongest_rhs";
paulson@4776
   307
wenzelm@5069
   308
Goalw [constrains_def, strongest_rhs_def]
paulson@5648
   309
    "F : constrains A B ==> strongest_rhs F A <= B";
paulson@4776
   310
by (Blast_tac 1);
paulson@4776
   311
qed "strongest_rhs_is_strongest";