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