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