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