src/HOL/UNITY/PPROD.ML
author paulson
Mon May 17 10:38:08 1999 +0200 (1999-05-17)
changeset 6646 3ea726909fff
parent 6575 70d758762c50
child 6826 02c4dd469ec0
permissions -rw-r--r--
"component" now an infix
     1 (*  Title:      HOL/UNITY/PPROD.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 *)
     6 
     7 
     8 val rinst = read_instantiate_sg (sign_of thy);
     9 
    10 (**** PPROD ****)
    11 
    12 (*** Basic properties ***)
    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_act_def] "lift_act i Id = Id";
    20 by Auto_tac;
    21 qed "lift_act_Id";
    22 Addsimps [lift_act_Id];
    23 
    24 Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
    25 by Auto_tac;
    26 qed "Init_lift_prog";
    27 Addsimps [Init_lift_prog];
    28 
    29 Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
    30 by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
    31 qed "Acts_lift_prog";
    32 
    33 Goalw [PPROD_def] "Init (PPROD I F) = (INT i:I. lift_set i (Init (F i)))";
    34 by Auto_tac;
    35 qed "Init_PPROD";
    36 Addsimps [Init_PPROD];
    37 
    38 Goalw [lift_act_def]
    39     "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
    40 by (Blast_tac 1);
    41 qed "lift_act_eq";
    42 AddIffs [lift_act_eq];
    43 
    44 Goal "Acts (PPROD I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
    45 by (auto_tac (claset(),
    46 	      simpset() addsimps [PPROD_def, Acts_lift_prog, Acts_JN]));
    47 qed "Acts_PPROD";
    48 
    49 Goal "PPROD {} F = SKIP";
    50 by (simp_tac (simpset() addsimps [PPROD_def]) 1);
    51 qed "PPROD_empty";
    52 
    53 Goal "(PPI i: I. SKIP) = SKIP";
    54 by (auto_tac (claset() addSIs [program_equalityI],
    55 	      simpset() addsimps [Acts_lift_prog, SKIP_def, Acts_PPROD]));
    56 qed "PPROD_SKIP";
    57 
    58 Addsimps [PPROD_SKIP, PPROD_empty];
    59 
    60 Goalw [PPROD_def]
    61     "PPROD (insert i I) F = (lift_prog i (F i)) Join (PPROD I F)";
    62 by Auto_tac;
    63 qed "PPROD_insert";
    64 
    65 Goalw [PPROD_def] "i : I ==> (lift_prog i (F i)) component (PPROD I F)";
    66 (*blast_tac doesn't use HO unification*)
    67 by (fast_tac (claset() addIs [component_JN]) 1);
    68 qed "component_PPROD";
    69 
    70 
    71 (*** Safety: co, stable, invariant ***)
    72 
    73 (** 1st formulation of lifting **)
    74 
    75 Goal "(lift_prog i F : (lift_set i A) co (lift_set i B))  =  \
    76 \     (F : A co B)";
    77 by (auto_tac (claset(), 
    78 	      simpset() addsimps [constrains_def, Acts_lift_prog]));
    79 by (Blast_tac 2);
    80 by (Force_tac 1);
    81 qed "lift_prog_constrains_eq";
    82 
    83 Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)";
    84 by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains_eq]) 1);
    85 qed "lift_prog_stable_eq";
    86 
    87 (*This one looks strange!  Proof probably is by case analysis on i=j.*)
    88 Goal "F i : A co B  \
    89 \     ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
    90 by (auto_tac (claset(), 
    91 	      simpset() addsimps [constrains_def, Acts_lift_prog]));
    92 by (REPEAT (Blast_tac 1));
    93 qed "constrains_imp_lift_prog_constrains";
    94 
    95 Goal "i : I ==>  \
    96 \     (PPROD I F : (lift_set i A) co (lift_set i B))  =  \
    97 \     (F i : A co B)";
    98 by (asm_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1);
    99 by (blast_tac (claset() addIs [lift_prog_constrains_eq RS iffD1, 
   100 			       constrains_imp_lift_prog_constrains]) 1);
   101 qed "PPROD_constrains";
   102 
   103 Goal "i : I ==> (PPROD I F : stable (lift_set i A)) = (F i : stable A)";
   104 by (asm_simp_tac (simpset() addsimps [stable_def, PPROD_constrains]) 1);
   105 qed "PPROD_stable";
   106 
   107 
   108 (** 2nd formulation of lifting **)
   109 
   110 Goal "[| lift_prog i F : AA co BB |] \
   111 \     ==> F : (Applyall AA i) co (Applyall BB i)";
   112 by (auto_tac (claset(), 
   113 	      simpset() addsimps [Applyall_def, constrains_def, 
   114 				  Acts_lift_prog]));
   115 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI],
   116 	       simpset()) 1);
   117 qed "lift_prog_constrains_projection";
   118 
   119 Goal "[| PPROD I F : AA co BB;  i: I |] \
   120 \     ==> F i : (Applyall AA i) co (Applyall BB i)";
   121 by (rtac lift_prog_constrains_projection 1);
   122 (*rotate this assumption to be last*)
   123 by (dres_inst_tac [("psi", "PPROD I F : ?C")] asm_rl 1);
   124 by (asm_full_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1);
   125 qed "PPROD_constrains_projection";
   126 
   127 
   128 (** invariant **)
   129 
   130 (*UNUSED*)
   131 Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
   132 by (auto_tac (claset(),
   133 	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
   134 qed "lift_prog_invariant_eq";
   135 
   136 Goal "[| F i : invariant A;  i : I |] \
   137 \     ==> PPROD I F : invariant (lift_set i A)";
   138 by (auto_tac (claset(),
   139 	      simpset() addsimps [invariant_def, PPROD_stable]));
   140 qed "invariant_imp_PPROD_invariant";
   141 
   142 (*The f0 premise ensures that the product is well-defined.*)
   143 Goal "[| PPROD I F : invariant (lift_set i A);  i : I;  \
   144 \        f0: Init (PPROD I F) |] ==> F i : invariant A";
   145 by (auto_tac (claset(),
   146 	      simpset() addsimps [invariant_def, PPROD_stable]));
   147 by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1);
   148 by Auto_tac;
   149 qed "PPROD_invariant_imp_invariant";
   150 
   151 Goal "[| i : I;  f0: Init (PPROD I F) |] \
   152 \     ==> (PPROD I F : invariant (lift_set i A)) = (F i : invariant A)";
   153 by (blast_tac (claset() addIs [invariant_imp_PPROD_invariant, 
   154 			       PPROD_invariant_imp_invariant]) 1);
   155 qed "PPROD_invariant";
   156 
   157 (*The f0 premise isn't needed if F is a constant program because then
   158   we get an initial state by replicating that of F*)
   159 Goal "i : I \
   160 \     ==> ((PPI x:I. F) : invariant (lift_set i A)) = (F : invariant A)";
   161 by (auto_tac (claset(),
   162 	      simpset() addsimps [invariant_def, PPROD_stable]));
   163 qed "PFUN_invariant";
   164 
   165 
   166 (*** Substitution Axiom versions: Co, Stable ***)
   167 
   168 (** Reachability **)
   169 
   170 Goal "[| f : reachable (PPROD I F);  i : I |] ==> f i : reachable (F i)";
   171 by (etac reachable.induct 1);
   172 by (auto_tac
   173     (claset() addIs reachable.intrs,
   174      simpset() addsimps [Acts_PPROD]));
   175 qed "reachable_PPROD";
   176 
   177 Goal "reachable (PPROD I F) <= {f. ALL i:I. f i : reachable (F i)}";
   178 by (force_tac (claset() addSDs [reachable_PPROD], simpset()) 1);
   179 qed "reachable_PPROD_subset1";
   180 
   181 Goal "[| i ~: I;  A : reachable (F i) |]     \
   182 \  ==> ALL f. f : reachable (PPROD I F)      \
   183 \             --> f(i:=A) : reachable (lift_prog i (F i) Join PPROD I F)";
   184 by (etac reachable.induct 1);
   185 by (ALLGOALS Clarify_tac);
   186 by (etac reachable.induct 1);
   187 (*Init, Init case*)
   188 by (force_tac (claset() addIs reachable.intrs,
   189 	       simpset() addsimps [Acts_lift_prog]) 1);
   190 (*Init of F, action of PPROD F case*)
   191 by (rtac reachable.Acts 1);
   192 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1);
   193 by (assume_tac 1);
   194 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1);
   195 (*induction over the 2nd "reachable" assumption*)
   196 by (eres_inst_tac [("xa","f")] reachable.induct 1);
   197 (*Init of PPROD F, action of F case*)
   198 by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1);
   199 by (force_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join]) 1);
   200 by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
   201 by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
   202 (*last case: an action of PPROD I F*)
   203 by (rtac reachable.Acts 1);
   204 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1);
   205 by (assume_tac 1);
   206 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1);
   207 qed_spec_mp "reachable_lift_Join_PPROD";
   208 
   209 
   210 (*The index set must be finite: otherwise infinitely many copies of F can
   211   perform actions, and PPROD can never catch up in finite time.*)
   212 Goal "finite I \
   213 \     ==> {f. ALL i:I. f i : reachable (F i)} <= reachable (PPROD I F)";
   214 by (etac finite_induct 1);
   215 by (Simp_tac 1);
   216 by (force_tac (claset() addDs [reachable_lift_Join_PPROD], 
   217 	       simpset() addsimps [PPROD_insert]) 1);
   218 qed "reachable_PPROD_subset2";
   219 
   220 Goal "finite I ==> \
   221 \     reachable (PPROD I F) = {f. ALL i:I. f i : reachable (F i)}";
   222 by (REPEAT_FIRST (ares_tac [equalityI,
   223 			    reachable_PPROD_subset1, 
   224 			    reachable_PPROD_subset2]));
   225 qed "reachable_PPROD_eq";
   226 
   227 
   228 (** Co **)
   229 
   230 Goal "[| F i : A Co B;  i: I;  finite I |]  \
   231 \     ==> PPROD I F : (lift_set i A) Co (lift_set i B)";
   232 by (auto_tac
   233     (claset(),
   234      simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
   235 			 reachable_PPROD_eq]));
   236 by (auto_tac (claset(), 
   237               simpset() addsimps [constrains_def, Acts_lift_prog, PPROD_def,
   238                                   Acts_JN]));
   239 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   240 qed "Constrains_imp_PPROD_Constrains";
   241 
   242 Goal "[| ALL i:I. f0 i : R i;   i: I |] \
   243 \     ==> Applyall ({f. (ALL i:I. f i : R i)} Int lift_set i A) i = R i Int A";
   244 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI],
   245 	       simpset() addsimps [Applyall_def, lift_set_def]) 1);
   246 qed "Applyall_Int_depend";
   247 
   248 (*Again, we need the f0 premise so that PPROD I F has an initial state;
   249   otherwise its Co-property is vacuous.*)
   250 Goal "[| PPROD I F : (lift_set i A) Co (lift_set i B);  \
   251 \        i: I;  finite I;  f0: Init (PPROD I F) |]  \
   252 \     ==> F i : A Co B";
   253 by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
   254 by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1);
   255 by (blast_tac (claset() addIs [reachable.Init]) 2);
   256 by (dtac PPROD_constrains_projection 1);
   257 by (assume_tac 1);
   258 by (asm_full_simp_tac
   259     (simpset() addsimps [Applyall_Int_depend, reachable_PPROD_eq]) 1);
   260 qed "PPROD_Constrains_imp_Constrains";
   261 
   262 
   263 Goal "[| i: I;  finite I;  f0: Init (PPROD I F) |]  \
   264 \     ==> (PPROD I F : (lift_set i A) Co (lift_set i B)) =  \
   265 \         (F i : A Co B)";
   266 by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, 
   267 			       PPROD_Constrains_imp_Constrains]) 1);
   268 qed "PPROD_Constrains";
   269 
   270 Goal "[| i: I;  finite I;  f0: Init (PPROD I F) |]  \
   271 \     ==> (PPROD I F : Stable (lift_set i A)) = (F i : Stable A)";
   272 by (asm_simp_tac (simpset() delsimps [Init_PPROD]
   273 			    addsimps [Stable_def, PPROD_Constrains]) 1);
   274 qed "PPROD_Stable";
   275 
   276 
   277 (** PFUN (no dependence on i) doesn't require the f0 premise **)
   278 
   279 Goal "i: I \
   280 \     ==> Applyall ({f. (ALL i:I. f i : R)} Int lift_set i A) i = R Int A";
   281 by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1);
   282 qed "Applyall_Int";
   283 
   284 Goal "[| (PPI x:I. F) : (lift_set i A) Co (lift_set i B);  \
   285 \        i: I;  finite I |]  \
   286 \     ==> F : A Co B";
   287 by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
   288 by (dtac PPROD_constrains_projection 1);
   289 by (assume_tac 1);
   290 by (asm_full_simp_tac
   291     (simpset() addsimps [Applyall_Int, Collect_conj_eq RS sym,
   292 			 reachable_PPROD_eq]) 1);
   293 qed "PFUN_Constrains_imp_Constrains";
   294 
   295 Goal "[| i: I;  finite I |]  \
   296 \     ==> ((PPI x:I. F) : (lift_set i A) Co (lift_set i B)) =  \
   297 \         (F : A Co B)";
   298 by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, 
   299 			       PFUN_Constrains_imp_Constrains]) 1);
   300 qed "PFUN_Constrains";
   301 
   302 Goal "[| i: I;  finite I |]  \
   303 \     ==> ((PPI x:I. F) : Stable (lift_set i A)) = (F : Stable A)";
   304 by (asm_simp_tac (simpset() addsimps [Stable_def, PFUN_Constrains]) 1);
   305 qed "PFUN_Stable";
   306 
   307 
   308 
   309 (*** guarantees properties ***)
   310 
   311 
   312 Goal "drop_act i (lift_act i act) = act";
   313 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI],
   314 	       simpset() addsimps [drop_act_def, lift_act_def]) 1);
   315 qed "lift_act_inverse";
   316 Addsimps [lift_act_inverse];
   317 
   318 
   319 Goal "(lift_prog i F) Join G = lift_prog i H \
   320 \     ==> EX J. H = F Join J";
   321 by (etac program_equalityE 1);
   322 by (auto_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join]));
   323 by (res_inst_tac [("x", 
   324 		   "mk_program(Applyall(Init G) i, drop_act i `` Acts G)")] 
   325     exI 1);
   326 by (rtac program_equalityI 1);
   327 (*Init*)
   328 by (simp_tac (simpset() addsimps [Applyall_def]) 1);
   329 (*Blast_tac can't do HO unification, needed to invent function states*)
   330 by (fast_tac (claset() addEs [equalityE]) 1);
   331 (*Now for the Actions*)
   332 by (dres_inst_tac [("f", "op `` (drop_act i)")] arg_cong 1);
   333 by (asm_full_simp_tac 
   334     (simpset() addsimps [insert_absorb, Acts_Join,
   335 			 image_Un, image_compose RS sym, o_def]) 1);
   336 qed "lift_prog_Join_eq_lift_prog_D";
   337 
   338 
   339 Goal "F : X guarantees Y \
   340 \     ==> lift_prog i F : (lift_prog i `` X) guarantees (lift_prog i `` Y)";
   341 by (rtac guaranteesI 1);
   342 by Auto_tac;
   343 by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
   344 qed "lift_prog_guarantees";
   345 
   346