src/HOL/UNITY/Lift_prog.ML
author paulson
Mon Oct 11 10:53:39 1999 +0200 (1999-10-11)
changeset 7826 c6a8b73b6c2a
parent 7688 d106cad8f515
child 7840 e1fd12b864a1
permissions -rw-r--r--
working shapshot with "projecting" and "extending"
     1 (*  Title:      HOL/UNITY/Lift_prog.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Arrays of processes.  Many results are instances of those in Extend & Project.
     7 *)
     8 
     9 
    10 (*** Basic properties ***)
    11 
    12 (** lift_set and drop_set **)
    13 
    14 Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)";
    15 by Auto_tac;
    16 qed "lift_set_iff";
    17 AddIffs [lift_set_iff];
    18 
    19 Goalw [lift_set_def] "lift_set i A Int lift_set i B = lift_set i (A Int B)";
    20 by Auto_tac;
    21 qed "Int_lift_set";
    22 
    23 Goalw [lift_set_def] "lift_set i A Un lift_set i B = lift_set i (A Un B)";
    24 by Auto_tac;
    25 qed "Un_lift_set";
    26 
    27 Goalw [lift_set_def] "lift_set i A - lift_set i B = lift_set i (A-B)";
    28 by Auto_tac;
    29 qed "Diff_lift_set";
    30 
    31 Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set];
    32 
    33 (*Converse fails*)
    34 Goalw [drop_set_def] "f : A ==> f i : drop_set i A";
    35 by Auto_tac;
    36 qed "drop_set_I";
    37 
    38 (** lift_act and drop_act **)
    39 
    40 Goalw [lift_act_def] "lift_act i Id = Id";
    41 by Auto_tac;
    42 by (etac rev_mp 1);
    43 by (dtac sym 1);
    44 by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
    45 qed "lift_act_Id";
    46 Addsimps [lift_act_Id];
    47 
    48 (*For compatibility with the original definition and perhaps simpler proofs*)
    49 Goalw [lift_act_def]
    50     "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
    51 by Auto_tac;
    52 by (rtac exI 1);
    53 by Auto_tac;
    54 qed "lift_act_eq";
    55 AddIffs [lift_act_eq];
    56 
    57 Goalw [drop_act_def]
    58      "[| (s, s') : act;  s : C |] ==> (s i, s' i) : drop_act C i act";
    59 by Auto_tac;
    60 qed "drop_act_I";
    61 
    62 Goalw [drop_set_def, drop_act_def]
    63      "UNIV <= drop_set i C ==> drop_act C i Id = Id";
    64 by (Blast_tac 1);
    65 qed "drop_act_Id";
    66 Addsimps [drop_act_Id];
    67 
    68 (** lift_prog and drop_prog **)
    69 
    70 Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
    71 by Auto_tac;
    72 qed "Init_lift_prog";
    73 Addsimps [Init_lift_prog];
    74 
    75 Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
    76 by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
    77 qed "Acts_lift_prog";
    78 Addsimps [Acts_lift_prog];
    79 
    80 Goalw [drop_prog_def] "Init (drop_prog C i F) = drop_set i (Init F)";
    81 by Auto_tac;
    82 qed "Init_drop_prog";
    83 Addsimps [Init_drop_prog];
    84 
    85 Goal "Acts (drop_prog C i F) = insert Id (drop_act C i `` Acts F)";
    86 by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], 
    87 	      simpset() addsimps [drop_prog_def]));
    88 qed "Acts_drop_prog";
    89 Addsimps [Acts_drop_prog];
    90 
    91 
    92 (*** sub ***)
    93 
    94 Addsimps [sub_def];
    95 
    96 Goal "lift_set i {s. P s} = {s. P (sub i s)}";
    97 by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
    98 qed "lift_set_sub";
    99 
   100 Goal "{s. P (s i)} = lift_set i {s. P s}";
   101 by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
   102 qed "Collect_eq_lift_set";
   103 
   104 Goal "sub i -`` A = lift_set i A";
   105 by (Force_tac 1);
   106 qed "sub_vimage";
   107 Addsimps [sub_vimage];
   108 
   109 
   110 
   111 (*** lift_prog and the lattice operations ***)
   112 
   113 Goal "lift_prog i SKIP = SKIP";
   114 by (auto_tac (claset() addSIs [program_equalityI],
   115 	      simpset() addsimps [SKIP_def, lift_prog_def]));
   116 qed "lift_prog_SKIP";
   117 
   118 Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)";
   119 by (rtac program_equalityI 1);
   120 by Auto_tac;
   121 qed "lift_prog_Join";
   122 
   123 Goal "lift_prog i (JOIN J F) = (JN j:J. lift_prog i (F j))";
   124 by (rtac program_equalityI 1);
   125 by Auto_tac;
   126 qed "lift_prog_JN";
   127 
   128 
   129 (*** Equivalence with "extend" version ***)
   130 
   131 Goalw [lift_map_def] "good_map (lift_map i)";
   132 by (rtac good_mapI 1);
   133 by (res_inst_tac [("f", "%f. (f i, f)")] surjI 1);
   134 by Auto_tac;
   135 by (dres_inst_tac [("f", "%f. f i")] arg_cong 1);
   136 by Auto_tac;
   137 qed "good_map_lift_map";
   138 
   139 fun lift_export th = good_map_lift_map RS export th;
   140 
   141 Goal "fst (inv (lift_map i) g) = g i";
   142 by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1);
   143 by (auto_tac (claset(), simpset() addsimps [lift_map_def]));
   144 qed "fst_inv_lift_map";
   145 Addsimps [fst_inv_lift_map];
   146 
   147 
   148 Goal "lift_set i A = extend_set (lift_map i) A";
   149 by (auto_tac (claset(), 
   150      simpset() addsimps [lift_export mem_extend_set_iff]));
   151 qed "lift_set_correct";
   152 
   153 Goalw [drop_set_def, project_set_def, lift_map_def]
   154      "drop_set i A = project_set (lift_map i) A";
   155 by Auto_tac;
   156 by (rtac image_eqI 2);
   157 by (rtac exI 1);
   158 by (stac (refl RS fun_upd_idem) 1);
   159 by Auto_tac;
   160 qed "drop_set_correct";
   161 
   162 Goal "lift_act i = extend_act (lift_map i)";
   163 by (rtac ext 1);
   164 by Auto_tac;
   165 by (forward_tac [lift_export extend_act_D] 2);
   166 by (auto_tac (claset(), simpset() addsimps [extend_act_def]));
   167 by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def]));
   168 by (rtac bexI 1);
   169 by (auto_tac (claset() addSIs [exI], simpset()));
   170 qed "lift_act_correct";
   171 
   172 Goal "drop_act C i = project_act C (lift_map i)";
   173 by (rtac ext 1);
   174 by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
   175 by Auto_tac;
   176 by (REPEAT_FIRST (ares_tac [exI, conjI]));
   177 by Auto_tac;
   178 by (REPEAT_FIRST (assume_tac ORELSE' stac (refl RS fun_upd_idem)));
   179 qed "drop_act_correct";
   180 
   181 Goal "lift_prog i = extend (lift_map i)";
   182 by (rtac (program_equalityI RS ext) 1);
   183 by (simp_tac (simpset() addsimps [lift_set_correct]) 1);
   184 by (simp_tac (simpset() 
   185 	      addsimps [lift_export Acts_extend, 
   186 			lift_act_correct]) 1);
   187 qed "lift_prog_correct";
   188 
   189 Goal "drop_prog C i = project C (lift_map i)";
   190 by (rtac (program_equalityI RS ext) 1);
   191 by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
   192 by (simp_tac (simpset() 
   193 	      addsimps [Acts_project, drop_act_correct]) 1);
   194 qed "drop_prog_correct";
   195 
   196 
   197 (** Injectivity of lift_set, lift_act, lift_prog **)
   198 
   199 Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F";
   200 by Auto_tac;
   201 qed "lift_set_inverse";
   202 Addsimps [lift_set_inverse];
   203 
   204 Goal "inj (lift_set i)";
   205 by (rtac inj_on_inverseI 1);
   206 by (rtac lift_set_inverse 1);
   207 qed "inj_lift_set";
   208 
   209 (*Because A and B could differ outside i, cannot generalize result to 
   210    drop_set i (A Int B) = drop_set i A Int drop_set i B
   211 *)
   212 Goalw [lift_set_def, drop_set_def]
   213      "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)";
   214 by Auto_tac;
   215 qed "drop_set_Int_lift_set";
   216 
   217 Goalw [lift_set_def, drop_set_def]
   218      "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A";
   219 by Auto_tac;
   220 qed "drop_set_Int_lift_set2";
   221 
   222 Goalw [drop_set_def]
   223      "i : I ==> drop_set i (INT j:I. lift_set j A) = A";
   224 by Auto_tac;
   225 qed "drop_set_INT";
   226 
   227 Goal "lift_set i UNIV = UNIV";
   228 by (simp_tac
   229     (simpset() addsimps [lift_set_correct, lift_export extend_set_UNIV_eq]) 1);
   230 qed "lift_set_UNIV_eq";
   231 Addsimps [lift_set_UNIV_eq];
   232 
   233 Goal "Domain act <= drop_set i C ==> drop_act C i (lift_act i act) = act";
   234 by (asm_full_simp_tac
   235     (simpset() addsimps [drop_set_correct, drop_act_correct, 
   236 			 lift_act_correct, lift_export extend_act_inverse]) 1);
   237 qed "lift_act_inverse";
   238 Addsimps [lift_act_inverse];
   239 
   240 Goal "UNIV <= drop_set i C ==> drop_prog C i (lift_prog i F) = F";
   241 by (asm_full_simp_tac
   242     (simpset() addsimps [drop_set_correct, drop_prog_correct, 
   243 			 lift_prog_correct, lift_export extend_inverse]) 1);
   244 qed "lift_prog_inverse";
   245 Addsimps [lift_prog_inverse];
   246 
   247 Goal "inj (lift_prog i)";
   248 by (simp_tac
   249     (simpset() addsimps [lift_prog_correct, lift_export inj_extend]) 1);
   250 qed "inj_lift_prog";
   251 
   252 
   253 (*** More Lemmas ***)
   254 
   255 Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)";
   256 by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct,
   257 				      lift_export extend_act_Image]) 1);
   258 qed "lift_act_Image";
   259 Addsimps [lift_act_Image];
   260 
   261 
   262 
   263 (*** Safety: co, stable, invariant ***)
   264 
   265 (** Safety and lift_prog **)
   266 
   267 Goal "(lift_prog i F : (lift_set i A) co (lift_set i B))  =  \
   268 \     (F : A co B)";
   269 by (auto_tac (claset(), 
   270 	      simpset() addsimps [constrains_def]));
   271 by (Force_tac 1);
   272 qed "lift_prog_constrains";
   273 
   274 Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)";
   275 by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains]) 1);
   276 qed "lift_prog_stable";
   277 
   278 Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
   279 by (auto_tac (claset(),
   280 	      simpset() addsimps [invariant_def, lift_prog_stable]));
   281 qed "lift_prog_invariant";
   282 
   283 Goal "[| lift_prog i F : A co B |] \
   284 \     ==> F : (drop_set i A) co (drop_set i B)";
   285 by (asm_full_simp_tac
   286     (simpset() addsimps [drop_set_correct, lift_prog_correct, 
   287 			 lift_export extend_constrains_project_set]) 1);
   288 qed "lift_prog_constrains_drop_set";
   289 
   290 (*This one looks strange!  Proof probably is by case analysis on i=j.
   291   If i~=j then lift_prog j (F j) does nothing to lift_set i, and the 
   292   premise ensures A<=B.*)
   293 Goal "F i : A co B  \
   294 \     ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
   295 by (auto_tac (claset(), 
   296 	      simpset() addsimps [constrains_def]));
   297 by (REPEAT (Blast_tac 1));
   298 qed "constrains_imp_lift_prog_constrains";
   299 
   300 
   301 (** Safety and drop_prog **)
   302 
   303 Goal "(drop_prog C i F : A co B)  =  \
   304 \     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
   305 by (simp_tac
   306     (simpset() addsimps [drop_prog_correct, 
   307 			 lift_set_correct, lift_export project_constrains]) 1);
   308 qed "drop_prog_constrains";
   309 
   310 Goal "(drop_prog UNIV i F : stable A)  =  (F : stable (lift_set i A))";
   311 by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1);
   312 qed "drop_prog_stable";
   313 
   314 
   315 (*** Diff, needed for localTo ***)
   316 
   317 Goal "[| (UN act:acts. Domain act) <= drop_set i C; \
   318 \        Diff G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |]  \
   319 \     ==> Diff (drop_prog C i G) acts : A co B";
   320 by (asm_full_simp_tac
   321     (simpset() addsimps [drop_set_correct, drop_prog_correct, 
   322 			 lift_set_correct, lift_act_correct, 
   323 			 lift_export Diff_project_constrains]) 1);
   324 qed "Diff_drop_prog_constrains";
   325 
   326 Goalw [stable_def]
   327      "[| (UN act:acts. Domain act) <= drop_set i C; \
   328 \        Diff G (lift_act i `` acts) : stable (lift_set i A) |]  \
   329 \     ==> Diff (drop_prog C i G) acts : stable A";
   330 by (etac Diff_drop_prog_constrains 1);
   331 by (assume_tac 1);
   332 qed "Diff_drop_prog_stable";
   333 
   334 Goalw [constrains_def, Diff_def]
   335      "Diff G acts : A co B  \
   336 \     ==> Diff (lift_prog i G) (lift_act i `` acts) \
   337 \         : (lift_set i A) co (lift_set i B)";
   338 by Auto_tac;
   339 by (Blast_tac 1);
   340 qed "Diff_lift_prog_co";
   341 
   342 Goalw [stable_def]
   343      "Diff G acts : stable A  \
   344 \     ==> Diff (lift_prog i G) (lift_act i `` acts) : stable (lift_set i A)";
   345 by (etac Diff_lift_prog_co 1);
   346 qed "Diff_lift_prog_stable";
   347 
   348 
   349 (*** Weak safety primitives: Co, Stable ***)
   350 
   351 (** Reachability **)
   352 
   353 Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
   354 by (simp_tac
   355     (simpset() addsimps [lift_prog_correct, lift_set_correct, 
   356 			 lift_export reachable_extend_eq]) 1);
   357 qed "reachable_lift_prog";
   358 
   359 Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
   360 \     (F : A Co B)";
   361 by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog,
   362 				  lift_prog_constrains]) 1);
   363 qed "lift_prog_Constrains";
   364 
   365 Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
   366 by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
   367 qed "lift_prog_Stable";
   368 
   369 Goal "[| reachable (lift_prog i F Join G) <= C;    \
   370 \        F Join drop_prog C i G : A Co B |] \
   371 \     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
   372 by (asm_full_simp_tac
   373     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   374 		     lift_set_correct, lift_export project_Constrains_D]) 1);
   375 qed "drop_prog_Constrains_D";
   376 
   377 Goalw [Stable_def]
   378      "[| reachable (lift_prog i F Join G) <= C;    \
   379 \        F Join drop_prog C i G : Stable A |]  \
   380 \     ==> lift_prog i F Join G : Stable (lift_set i A)";
   381 by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
   382 qed "drop_prog_Stable_D";
   383 
   384 Goal "[| reachable (lift_prog i F Join G) <= C;  \
   385 \        F Join drop_prog C i G : Always A |]   \
   386 \     ==> lift_prog i F Join G : Always (lift_set i A)";
   387 by (asm_full_simp_tac
   388     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   389 		     lift_set_correct, lift_export project_Always_D]) 1);
   390 qed "drop_prog_Always_D";
   391 
   392 Goalw [Increasing_def]
   393      "[| reachable (lift_prog i F Join G) <= C;  \
   394 \        F Join drop_prog C i G : Increasing func |] \
   395 \     ==> lift_prog i F Join G : Increasing (func o (sub i))";
   396 by Auto_tac;
   397 by (stac Collect_eq_lift_set 1);
   398 by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1); 
   399 qed "project_Increasing_D";
   400 
   401 
   402 (*UNUSED*)
   403 Goal "UNIV <= drop_set i C \
   404 \     ==> drop_prog C i ((lift_prog i F) Join G) = F Join (drop_prog C i G)";
   405 by (asm_full_simp_tac
   406     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   407 		     drop_set_correct, lift_export project_extend_Join]) 1);
   408 qed "drop_prog_lift_prog_Join";
   409 
   410 
   411 (*** Progress: transient, ensures ***)
   412 
   413 Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
   414 by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct,
   415 			  lift_export extend_transient]) 1);
   416 qed "lift_prog_transient";
   417 
   418 Goal "(lift_prog i F : transient (lift_set j A)) = \
   419 \     (i=j & F : transient A | A={})";
   420 by (case_tac "i=j" 1);
   421 by (auto_tac (claset(), simpset() addsimps [lift_prog_transient]));
   422 by (auto_tac (claset(), simpset() addsimps [lift_prog_def, transient_def]));
   423 by (Force_tac 1);
   424 qed "lift_prog_transient_eq_disj";
   425 
   426 
   427 (*** guarantees properties ***)
   428 
   429 val [xguary,project,lift_prog] =
   430 Goal "[| F : X guarantees Y;  \
   431 \        !!G. lift_prog i F Join G : X' ==> F Join proj G : X;  \
   432 \        !!G. [| F Join proj G : Y; lift_prog i F Join G : X'; \
   433 \                Disjoint (lift_prog i F) G |] \
   434 \             ==> lift_prog i F Join G : Y' |] \
   435 \     ==> lift_prog i F : X' guarantees Y'";
   436 by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
   437 by (etac project 1);
   438 by (assume_tac 1);
   439 by (assume_tac 1);
   440 qed "drop_prog_guarantees";
   441 
   442 
   443 (** Are these two useful?? **)
   444 
   445 (*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
   446   ensure that F has the form lift_prog i F for some F.*)
   447 Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}";
   448 by Auto_tac;
   449 by (stac Collect_eq_lift_set 1); 
   450 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable]) 1);
   451 qed "image_lift_prog_Stable";
   452 
   453 Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
   454 by (simp_tac (simpset() addsimps [Increasing_def,
   455 				  inj_lift_prog RS image_INT]) 1);
   456 by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1);
   457 qed "image_lift_prog_Increasing";
   458 
   459 
   460 (*** guarantees corollaries ***)
   461 
   462 Goal "F : UNIV guarantees increasing f \
   463 \     ==> lift_prog i F : UNIV guarantees increasing (f o sub i)";
   464 by (dtac (lift_export extend_guar_increasing) 1);
   465 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   466 qed "lift_prog_guar_increasing";
   467 
   468 Goal "F : UNIV guarantees Increasing f \
   469 \     ==> lift_prog i F : UNIV guarantees Increasing (f o sub i)";
   470 by (dtac (lift_export extend_guar_Increasing) 1);
   471 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   472 qed "lift_prog_guar_Increasing";
   473 
   474 Goal "F : (v localTo G) guarantees increasing func  \
   475 \     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
   476 \                         guarantees increasing (func o sub i)";
   477 by (dtac (lift_export extend_localTo_guar_increasing) 1);
   478 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   479 qed "lift_prog_localTo_guar_increasing";
   480 
   481 Goal "F : (v localTo G) guarantees Increasing func  \
   482 \     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
   483 \                         guarantees Increasing (func o sub i)";
   484 by (dtac (lift_export extend_localTo_guar_Increasing) 1);
   485 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   486 qed "lift_prog_localTo_guar_Increasing";
   487 
   488 Goal "F : Always A guarantees Always B \
   489 \ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
   490 by (asm_simp_tac
   491     (simpset() addsimps [lift_set_correct, lift_prog_correct, 
   492 			 lift_export extend_guar_Always]) 1);
   493 qed "lift_prog_guar_Always";