src/HOL/UNITY/Lift_prog.ML
changeset 7688 d106cad8f515
parent 7547 a72a551b6d79
child 7826 c6a8b73b6c2a
     1.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Oct 04 12:22:14 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Mon Oct 04 13:45:31 1999 +0200
     1.3 @@ -48,14 +48,23 @@
     1.4  qed "lift_act_Id";
     1.5  Addsimps [lift_act_Id];
     1.6  
     1.7 -Goalw [drop_act_def] "(s, s') : act ==> (s i, s' i) : drop_act i act";
     1.8 -by (auto_tac (claset() addSIs [image_eqI], simpset()));
     1.9 +(*For compatibility with the original definition and perhaps simpler proofs*)
    1.10 +Goalw [lift_act_def]
    1.11 +    "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
    1.12 +by Auto_tac;
    1.13 +by (rtac exI 1);
    1.14 +by Auto_tac;
    1.15 +qed "lift_act_eq";
    1.16 +AddIffs [lift_act_eq];
    1.17 +
    1.18 +Goalw [drop_act_def]
    1.19 +     "[| (s, s') : act;  s : C |] ==> (s i, s' i) : drop_act C i act";
    1.20 +by Auto_tac;
    1.21  qed "drop_act_I";
    1.22  
    1.23 -Goalw [drop_act_def] "drop_act i Id = Id";
    1.24 -by Auto_tac;
    1.25 -by (res_inst_tac [("x", "((%u. x), (%u. x))")] image_eqI 1);
    1.26 -by Auto_tac;
    1.27 +Goalw [drop_set_def, drop_act_def]
    1.28 +     "UNIV <= drop_set i C ==> drop_act C i Id = Id";
    1.29 +by (Blast_tac 1);
    1.30  qed "drop_act_Id";
    1.31  Addsimps [drop_act_Id];
    1.32  
    1.33 @@ -71,27 +80,38 @@
    1.34  qed "Acts_lift_prog";
    1.35  Addsimps [Acts_lift_prog];
    1.36  
    1.37 -Goalw [drop_prog_def] "Init (drop_prog i F) = drop_set i (Init F)";
    1.38 +Goalw [drop_prog_def] "Init (drop_prog C i F) = drop_set i (Init F)";
    1.39  by Auto_tac;
    1.40  qed "Init_drop_prog";
    1.41  Addsimps [Init_drop_prog];
    1.42  
    1.43 -Goalw [drop_prog_def] "Acts (drop_prog i F) = drop_act i `` Acts F";
    1.44 -by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
    1.45 +Goal "Acts (drop_prog C i F) = insert Id (drop_act C i `` Acts F)";
    1.46 +by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], 
    1.47 +	      simpset() addsimps [drop_prog_def]));
    1.48  qed "Acts_drop_prog";
    1.49  Addsimps [Acts_drop_prog];
    1.50  
    1.51 -(** These monotonicity results look natural but are UNUSED **)
    1.52 +
    1.53 +(*** sub ***)
    1.54 +
    1.55 +Addsimps [sub_def];
    1.56 +
    1.57 +Goal "lift_set i {s. P s} = {s. P (sub i s)}";
    1.58 +by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
    1.59 +qed "lift_set_sub";
    1.60  
    1.61 -Goal "F <= G ==> lift_prog i F <= lift_prog i G";
    1.62 -by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
    1.63 -by Auto_tac;
    1.64 -qed "lift_prog_mono";
    1.65 +Goal "{s. P (s i)} = lift_set i {s. P s}";
    1.66 +by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
    1.67 +qed "Collect_eq_lift_set";
    1.68  
    1.69 -Goal "F <= G ==> drop_prog i F <= drop_prog i G";
    1.70 -by (full_simp_tac (simpset() addsimps [component_eq_subset, drop_set_def]) 1);
    1.71 -by Auto_tac;
    1.72 -qed "drop_prog_mono";
    1.73 +Goal "sub i -`` A = lift_set i A";
    1.74 +by (Force_tac 1);
    1.75 +qed "sub_vimage";
    1.76 +Addsimps [sub_vimage];
    1.77 +
    1.78 +
    1.79 +
    1.80 +(*** lift_prog and the lattice operations ***)
    1.81  
    1.82  Goal "lift_prog i SKIP = SKIP";
    1.83  by (auto_tac (claset() addSIs [program_equalityI],
    1.84 @@ -108,79 +128,6 @@
    1.85  by Auto_tac;
    1.86  qed "lift_prog_JN";
    1.87  
    1.88 -Goal "drop_prog i SKIP = SKIP";
    1.89 -by (auto_tac (claset() addSIs [program_equalityI],
    1.90 -	      simpset() addsimps [SKIP_def, drop_set_def, drop_prog_def]));
    1.91 -qed "drop_prog_SKIP";
    1.92 -
    1.93 -
    1.94 -(** Injectivity of lift_set, lift_act, lift_prog **)
    1.95 -
    1.96 -Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F";
    1.97 -by Auto_tac;
    1.98 -qed "lift_set_inverse";
    1.99 -Addsimps [lift_set_inverse];
   1.100 -
   1.101 -Goal "inj (lift_set i)";
   1.102 -by (rtac inj_on_inverseI 1);
   1.103 -by (rtac lift_set_inverse 1);
   1.104 -qed "inj_lift_set";
   1.105 -
   1.106 -(*Because A and B could differ outside i, cannot generalize result to 
   1.107 -   drop_set i (A Int B) = drop_set i A Int drop_set i B
   1.108 -*)
   1.109 -Goalw [lift_set_def, drop_set_def]
   1.110 -     "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)";
   1.111 -by Auto_tac;
   1.112 -qed "drop_set_Int_lift_set";
   1.113 -
   1.114 -Goalw [lift_set_def, drop_set_def]
   1.115 -     "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A";
   1.116 -by Auto_tac;
   1.117 -qed "drop_set_Int_lift_set2";
   1.118 -
   1.119 -Goalw [drop_set_def]
   1.120 -     "i : I ==> drop_set i (INT j:I. lift_set j A) = A";
   1.121 -by Auto_tac;
   1.122 -qed "drop_set_INT";
   1.123 -
   1.124 -Goalw [lift_act_def, drop_act_def] "drop_act i (lift_act i act) = act";
   1.125 -by Auto_tac;
   1.126 -by (res_inst_tac [("x", "f(i:=a)")] exI 1);
   1.127 -by (Asm_simp_tac 1);
   1.128 -by (res_inst_tac [("x", "f(i:=b)")] exI 1);
   1.129 -by (Asm_simp_tac 1);
   1.130 -qed "lift_act_inverse";
   1.131 -Addsimps [lift_act_inverse];
   1.132 -
   1.133 -Goal "inj (lift_act i)";
   1.134 -by (rtac inj_on_inverseI 1);
   1.135 -by (rtac lift_act_inverse 1);
   1.136 -qed "inj_lift_act";
   1.137 -
   1.138 -Goal "drop_prog i (lift_prog i F) = F";
   1.139 -by (simp_tac (simpset() addsimps [lift_prog_def, drop_prog_def]) 1);
   1.140 -by (rtac program_equalityI 1);
   1.141 -by (simp_tac (simpset() addsimps [image_image_eq_UN]) 2);
   1.142 -by (Simp_tac 1);
   1.143 -qed "lift_prog_inverse";
   1.144 -Addsimps [lift_prog_inverse];
   1.145 -
   1.146 -Goal "inj (lift_prog i)";
   1.147 -by (rtac inj_on_inverseI 1);
   1.148 -by (rtac lift_prog_inverse 1);
   1.149 -qed "inj_lift_prog";
   1.150 -
   1.151 -
   1.152 -(*For compatibility with the original definition and perhaps simpler proofs*)
   1.153 -Goalw [lift_act_def]
   1.154 -    "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
   1.155 -by Auto_tac;
   1.156 -by (rtac exI 1);
   1.157 -by Auto_tac;
   1.158 -qed "lift_act_eq";
   1.159 -AddIffs [lift_act_eq];
   1.160 -
   1.161  
   1.162  (*** Equivalence with "extend" version ***)
   1.163  
   1.164 @@ -219,39 +166,93 @@
   1.165  by (rtac ext 1);
   1.166  by Auto_tac;
   1.167  by (forward_tac [lift_export extend_act_D] 2);
   1.168 +by (auto_tac (claset(), simpset() addsimps [extend_act_def]));
   1.169  by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def]));
   1.170  by (rtac bexI 1);
   1.171  by (auto_tac (claset() addSIs [exI], simpset()));
   1.172  qed "lift_act_correct";
   1.173  
   1.174 -Goal "drop_act i = project_act UNIV (lift_map i)";
   1.175 +Goal "drop_act C i = project_act C (lift_map i)";
   1.176  by (rtac ext 1);
   1.177  by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
   1.178  by Auto_tac;
   1.179 -by (rtac image_eqI 2);
   1.180 -by (REPEAT (rtac exI 1 ORELSE stac (refl RS fun_upd_idem) 1));
   1.181 +by (REPEAT_FIRST (ares_tac [exI, conjI]));
   1.182  by Auto_tac;
   1.183 +by (REPEAT_FIRST (assume_tac ORELSE' stac (refl RS fun_upd_idem)));
   1.184  qed "drop_act_correct";
   1.185  
   1.186 -Goal "lift_prog i F = extend (lift_map i) F";
   1.187 -by (rtac program_equalityI 1);
   1.188 +Goal "lift_prog i = extend (lift_map i)";
   1.189 +by (rtac (program_equalityI RS ext) 1);
   1.190  by (simp_tac (simpset() addsimps [lift_set_correct]) 1);
   1.191  by (simp_tac (simpset() 
   1.192  	      addsimps [lift_export Acts_extend, 
   1.193  			lift_act_correct]) 1);
   1.194  qed "lift_prog_correct";
   1.195  
   1.196 -Goal "drop_prog i F = project UNIV (lift_map i) F";
   1.197 -by (rtac program_equalityI 1);
   1.198 +Goal "drop_prog C i = project C (lift_map i)";
   1.199 +by (rtac (program_equalityI RS ext) 1);
   1.200  by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
   1.201  by (simp_tac (simpset() 
   1.202  	      addsimps [Acts_project, drop_act_correct]) 1);
   1.203 -by (rtac (insert_absorb RS sym) 1);
   1.204 -by (rtac (Id_in_Acts RSN (2,image_eqI)) 1);
   1.205 -by (rtac (project_set_UNIV RS lift_export project_act_Id RS sym) 1);
   1.206  qed "drop_prog_correct";
   1.207  
   1.208  
   1.209 +(** Injectivity of lift_set, lift_act, lift_prog **)
   1.210 +
   1.211 +Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F";
   1.212 +by Auto_tac;
   1.213 +qed "lift_set_inverse";
   1.214 +Addsimps [lift_set_inverse];
   1.215 +
   1.216 +Goal "inj (lift_set i)";
   1.217 +by (rtac inj_on_inverseI 1);
   1.218 +by (rtac lift_set_inverse 1);
   1.219 +qed "inj_lift_set";
   1.220 +
   1.221 +(*Because A and B could differ outside i, cannot generalize result to 
   1.222 +   drop_set i (A Int B) = drop_set i A Int drop_set i B
   1.223 +*)
   1.224 +Goalw [lift_set_def, drop_set_def]
   1.225 +     "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)";
   1.226 +by Auto_tac;
   1.227 +qed "drop_set_Int_lift_set";
   1.228 +
   1.229 +Goalw [lift_set_def, drop_set_def]
   1.230 +     "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A";
   1.231 +by Auto_tac;
   1.232 +qed "drop_set_Int_lift_set2";
   1.233 +
   1.234 +Goalw [drop_set_def]
   1.235 +     "i : I ==> drop_set i (INT j:I. lift_set j A) = A";
   1.236 +by Auto_tac;
   1.237 +qed "drop_set_INT";
   1.238 +
   1.239 +Goal "lift_set i UNIV = UNIV";
   1.240 +by (simp_tac
   1.241 +    (simpset() addsimps [lift_set_correct, lift_export extend_set_UNIV_eq]) 1);
   1.242 +qed "lift_set_UNIV_eq";
   1.243 +Addsimps [lift_set_UNIV_eq];
   1.244 +
   1.245 +Goal "Domain act <= drop_set i C ==> drop_act C i (lift_act i act) = act";
   1.246 +by (asm_full_simp_tac
   1.247 +    (simpset() addsimps [drop_set_correct, drop_act_correct, 
   1.248 +			 lift_act_correct, lift_export extend_act_inverse]) 1);
   1.249 +qed "lift_act_inverse";
   1.250 +Addsimps [lift_act_inverse];
   1.251 +
   1.252 +Goal "UNIV <= drop_set i C ==> drop_prog C i (lift_prog i F) = F";
   1.253 +by (asm_full_simp_tac
   1.254 +    (simpset() addsimps [drop_set_correct, drop_prog_correct, 
   1.255 +			 lift_prog_correct, lift_export extend_inverse]) 1);
   1.256 +qed "lift_prog_inverse";
   1.257 +Addsimps [lift_prog_inverse];
   1.258 +
   1.259 +Goal "inj (lift_prog i)";
   1.260 +by (simp_tac
   1.261 +    (simpset() addsimps [lift_prog_correct, lift_export inj_extend]) 1);
   1.262 +qed "inj_lift_prog";
   1.263 +
   1.264 +
   1.265  (*** More Lemmas ***)
   1.266  
   1.267  Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)";
   1.268 @@ -295,50 +296,48 @@
   1.269  
   1.270  (** Safety and drop_prog **)
   1.271  
   1.272 -Goalw [constrains_def]
   1.273 -     "(drop_prog i F : A co B)  =  (F : (lift_set i A) co (lift_set i B))";
   1.274 -by Auto_tac;
   1.275 -by (force_tac (claset(), 
   1.276 -	       simpset() addsimps [drop_act_def]) 2);
   1.277 -by (blast_tac (claset() addIs [drop_act_I]) 1);
   1.278 +Goal "(drop_prog C i F : A co B)  =  \
   1.279 +\     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
   1.280 +by (simp_tac
   1.281 +    (simpset() addsimps [drop_prog_correct, 
   1.282 +			 lift_set_correct, lift_export project_constrains]) 1);
   1.283  qed "drop_prog_constrains";
   1.284  
   1.285 -Goal "(drop_prog i F : stable A)  =  (F : stable (lift_set i A))";
   1.286 +Goal "(drop_prog UNIV i F : stable A)  =  (F : stable (lift_set i A))";
   1.287  by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1);
   1.288  qed "drop_prog_stable";
   1.289  
   1.290  
   1.291  (*** Diff, needed for localTo ***)
   1.292  
   1.293 -(** THESE PROOFS CAN BE GENERALIZED AS IN EXTEND.ML **)
   1.294 -
   1.295 -Goal "Diff G (lift_act i `` Acts F) : (lift_set i A) co (lift_set i B)  \
   1.296 -\     ==> Diff (drop_prog i G) (Acts F) : A co B";
   1.297 -by (auto_tac (claset(), 
   1.298 -	      simpset() addsimps [constrains_def, Diff_def]));
   1.299 -by (dtac bspec 1);
   1.300 -by (Force_tac 1);
   1.301 -by (auto_tac (claset(), simpset() addsimps [drop_act_def]));
   1.302 -by (auto_tac (claset(), simpset() addsimps [lift_set_def]));
   1.303 +Goal "[| (UN act:acts. Domain act) <= drop_set i C; \
   1.304 +\        Diff G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |]  \
   1.305 +\     ==> Diff (drop_prog C i G) acts : A co B";
   1.306 +by (asm_full_simp_tac
   1.307 +    (simpset() addsimps [drop_set_correct, drop_prog_correct, 
   1.308 +			 lift_set_correct, lift_act_correct, 
   1.309 +			 lift_export Diff_project_co]) 1);
   1.310  qed "Diff_drop_prog_co";
   1.311  
   1.312  Goalw [stable_def]
   1.313 -     "Diff G (lift_act i `` Acts F) : stable (lift_set i A)  \
   1.314 -\     ==> Diff (drop_prog i G) (Acts F) : stable A";
   1.315 +     "[| (UN act:acts. Domain act) <= drop_set i C; \
   1.316 +\        Diff G (lift_act i `` acts) : stable (lift_set i A) |]  \
   1.317 +\     ==> Diff (drop_prog C i G) acts : stable A";
   1.318  by (etac Diff_drop_prog_co 1);
   1.319 +by (assume_tac 1);
   1.320  qed "Diff_drop_prog_stable";
   1.321  
   1.322  Goalw [constrains_def, Diff_def]
   1.323 -     "Diff G (Acts F) : A co B  \
   1.324 -\     ==> Diff (lift_prog i G) (lift_act i `` Acts F) \
   1.325 +     "Diff G acts : A co B  \
   1.326 +\     ==> Diff (lift_prog i G) (lift_act i `` acts) \
   1.327  \         : (lift_set i A) co (lift_set i B)";
   1.328  by Auto_tac;
   1.329  by (Blast_tac 1);
   1.330  qed "Diff_lift_prog_co";
   1.331  
   1.332  Goalw [stable_def]
   1.333 -     "Diff G (Acts F) : stable A  \
   1.334 -\     ==> Diff (lift_prog i G) (lift_act i `` Acts F) : stable (lift_set i A)";
   1.335 +     "Diff G acts : stable A  \
   1.336 +\     ==> Diff (lift_prog i G) (lift_act i `` acts) : stable (lift_set i A)";
   1.337  by (etac Diff_lift_prog_co 1);
   1.338  qed "Diff_lift_prog_stable";
   1.339  
   1.340 @@ -347,25 +346,10 @@
   1.341  
   1.342  (** Reachability **)
   1.343  
   1.344 -Goal "s : reachable F ==> f(i:=s) : reachable (lift_prog i F)";
   1.345 -by (etac reachable.induct 1);
   1.346 -by (force_tac (claset() addIs [reachable.Acts, ext], 
   1.347 -	       simpset()) 2);
   1.348 -by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
   1.349 -qed "reachable_lift_progI";
   1.350 -
   1.351 -Goal "f : reachable (lift_prog i F) ==> f i : reachable F";
   1.352 -by (etac reachable.induct 1);
   1.353 -by Auto_tac;
   1.354 -by (ALLGOALS (blast_tac (claset() addIs reachable.intrs)));
   1.355 -qed "reachable_lift_progD";
   1.356 -
   1.357  Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
   1.358 -by Auto_tac;
   1.359 -by (etac reachable_lift_progD 1);
   1.360 -ren "f" 1;
   1.361 -by (dres_inst_tac [("f","f"),("i","i")] reachable_lift_progI 1);
   1.362 -by Auto_tac;
   1.363 +by (simp_tac
   1.364 +    (simpset() addsimps [lift_prog_correct, lift_set_correct, 
   1.365 +			 lift_export reachable_extend_eq]) 1);
   1.366  qed "reachable_lift_prog";
   1.367  
   1.368  Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
   1.369 @@ -378,87 +362,46 @@
   1.370  by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
   1.371  qed "lift_prog_Stable";
   1.372  
   1.373 -(** Reachability and drop_prog **)
   1.374 -
   1.375 -Goal "f : reachable F ==> f i : reachable (drop_prog i F)";
   1.376 -by (etac reachable.induct 1);
   1.377 -by (force_tac (claset() addIs [reachable.Acts, drop_act_I],
   1.378 -	       simpset()) 2);
   1.379 -by (force_tac (claset() addIs [reachable.Init, drop_set_I],
   1.380 -	       simpset()) 1);
   1.381 -qed "reachable_imp_reachable_drop_prog";
   1.382 -
   1.383 -(*Converse fails because it would require
   1.384 -  [| s i : reachable (drop_prog i F); s i : A |] ==> s : reachable F
   1.385 -*)
   1.386 -Goalw [Constrains_def]
   1.387 -     "drop_prog i F : A Co B ==> F : (lift_set i A) Co (lift_set i B)";
   1.388 -by (full_simp_tac (simpset() addsimps [drop_prog_constrains]) 1);
   1.389 -by (etac constrains_weaken_L 1);
   1.390 -by Auto_tac;
   1.391 -by (etac reachable_imp_reachable_drop_prog 1);
   1.392 +Goal "[| reachable (lift_prog i F Join G) <= C;    \
   1.393 +\        F Join drop_prog C i G : A Co B |] \
   1.394 +\     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
   1.395 +by (asm_full_simp_tac
   1.396 +    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   1.397 +		     lift_set_correct, lift_export project_Constrains_D]) 1);
   1.398  qed "drop_prog_Constrains_D";
   1.399  
   1.400  Goalw [Stable_def]
   1.401 -     "drop_prog i F : Stable A ==> F : Stable (lift_set i A)";
   1.402 +     "[| reachable (lift_prog i F Join G) <= C;    \
   1.403 +\        F Join drop_prog C i G : Stable A |]  \
   1.404 +\     ==> lift_prog i F Join G : Stable (lift_set i A)";
   1.405  by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
   1.406  qed "drop_prog_Stable_D";
   1.407  
   1.408 -
   1.409 -(*** Programs of the form lift_prog i F Join G
   1.410 -     in other words programs containing a replicated component ***)
   1.411 -
   1.412 -Goal "drop_prog i ((lift_prog i F) Join G) = F Join (drop_prog i G)";
   1.413 -by (rtac program_equalityI 1);
   1.414 -by (simp_tac (simpset() addsimps [image_Un, image_image_eq_UN]) 2);
   1.415 -by (simp_tac (simpset() addsimps [drop_set_Int_lift_set]) 1);
   1.416 -qed "drop_prog_lift_prog_Join";
   1.417 -
   1.418 -Goal "(lift_prog i F) Join G = lift_prog i H \
   1.419 -\     ==> H = F Join (drop_prog i G)";
   1.420 -by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
   1.421 -by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
   1.422 -by (etac sym 1);
   1.423 -qed "lift_prog_Join_eq_lift_prog_D";
   1.424 -
   1.425 -Goal "f : reachable (lift_prog i F Join G)  \
   1.426 -\     ==> f i : reachable (F Join drop_prog i G)";
   1.427 -by (etac reachable.induct 1);
   1.428 -by (force_tac (claset() addIs [reachable.Init, drop_set_I], simpset()) 1);
   1.429 -(*By case analysis on whether the action is of lift_prog i F  or  G*)
   1.430 -by (force_tac (claset() addIs [reachable.Acts, drop_act_I], 
   1.431 -	       simpset() addsimps [image_iff]) 1);
   1.432 -qed "reachable_lift_prog_Join_D";
   1.433 +Goal "[| reachable (lift_prog i F Join G) <= C;  \
   1.434 +\        F Join drop_prog C i G : Always A |]   \
   1.435 +\     ==> lift_prog i F Join G : Always (lift_set i A)";
   1.436 +by (asm_full_simp_tac
   1.437 +    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   1.438 +		     lift_set_correct, lift_export project_Always_D]) 1);
   1.439 +qed "drop_prog_Always_D";
   1.440  
   1.441 -(*Opposite inclusion fails, even for the initial state: lift_set i includes
   1.442 -  ALL functions determined only by their value at i.*)
   1.443 -Goal "reachable (lift_prog i F Join G) <= \
   1.444 -\     lift_set i (reachable (F Join drop_prog i G))";
   1.445 +Goalw [Increasing_def]
   1.446 +     "[| reachable (lift_prog i F Join G) <= C;  \
   1.447 +\        F Join drop_prog C i G : Increasing func |] \
   1.448 +\     ==> lift_prog i F Join G : Increasing (func o (sub i))";
   1.449  by Auto_tac;
   1.450 -by (etac reachable_lift_prog_Join_D 1);
   1.451 -qed "reachable_lift_prog_Join_subset";
   1.452 +by (stac Collect_eq_lift_set 1);
   1.453 +by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1); 
   1.454 +qed "project_Increasing_D";
   1.455  
   1.456 -Goalw [Constrains_def]
   1.457 -     "F Join drop_prog i G : A Co B    \
   1.458 -\     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
   1.459 -by (subgoal_tac 
   1.460 -    "lift_prog i F Join G : lift_set i (reachable (F Join drop_prog i G)) Int \
   1.461 -\                           lift_set i A \
   1.462 -\    co lift_set i B" 1);
   1.463 -by (asm_full_simp_tac 
   1.464 -    (simpset() addsimps [Int_lift_set,
   1.465 -			 lift_prog_constrains,
   1.466 -			 drop_prog_constrains RS sym,
   1.467 -			 drop_prog_lift_prog_Join]) 2);
   1.468 -by (blast_tac (claset() addIs [constrains_weaken, 
   1.469 -			       reachable_lift_prog_Join_D]) 1);
   1.470 -qed "lift_prog_Join_Constrains";
   1.471  
   1.472 -Goal "F Join drop_prog i G : Stable A    \
   1.473 -\     ==> lift_prog i F Join G : Stable (lift_set i A)";
   1.474 -by (asm_full_simp_tac (simpset() addsimps [Stable_def, 
   1.475 -					   lift_prog_Join_Constrains]) 1);
   1.476 -qed "lift_prog_Join_Stable";
   1.477 +(*UNUSED*)
   1.478 +Goal "UNIV <= drop_set i C \
   1.479 +\     ==> drop_prog C i ((lift_prog i F) Join G) = F Join (drop_prog C i G)";
   1.480 +by (asm_full_simp_tac
   1.481 +    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   1.482 +		     drop_set_correct, lift_export project_extend_Join]) 1);
   1.483 +qed "drop_prog_lift_prog_Join";
   1.484  
   1.485  
   1.486  (*** Progress: transient, ensures ***)
   1.487 @@ -479,50 +422,20 @@
   1.488  
   1.489  (*** guarantees properties ***)
   1.490  
   1.491 -(** It seems that neither of these can be proved from the other. **)
   1.492 -
   1.493 -(*Strong precondition and postcondition; doesn't seem very useful.
   1.494 -  Probably can be strengthened to an equivalance.*)
   1.495 -Goal "F : X guarantees Y \
   1.496 -\     ==> lift_prog i F : (lift_prog i `` X) guarantees (lift_prog i `` Y)";
   1.497 -by (rtac guaranteesI 1);
   1.498 -by Auto_tac;
   1.499 -by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
   1.500 -qed "lift_prog_guarantees";
   1.501 -
   1.502 -(*Weak precondition and postcondition; this is the good one!
   1.503 -CAN WEAKEN 2ND PREMISE TO  
   1.504 -      !!G. extend h F Join G : XX ==> F Join project h G : X; 
   1.505 -*)
   1.506 -val [xguary,drop_prog,lift_prog] =
   1.507 +val [xguary,project,lift_prog] =
   1.508  Goal "[| F : X guarantees Y;  \
   1.509 -\        !!H. H : XX ==> drop_prog i H : X;  \
   1.510 -\        !!G. F Join drop_prog i G : Y ==> lift_prog i F Join G : YY |] \
   1.511 -\     ==> lift_prog i F : XX guarantees YY";
   1.512 +\        !!G. lift_prog i F Join G : X' ==> F Join proj G : X;  \
   1.513 +\        !!G. [| F Join proj G : Y; lift_prog i F Join G : X'; \
   1.514 +\                Disjoint (lift_prog i F) G |] \
   1.515 +\             ==> lift_prog i F Join G : Y' |] \
   1.516 +\     ==> lift_prog i F : X' guarantees Y'";
   1.517  by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
   1.518 -by (dtac drop_prog 1);
   1.519 -by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
   1.520 +by (etac project 1);
   1.521 +by (assume_tac 1);
   1.522 +by (assume_tac 1);
   1.523  qed "drop_prog_guarantees";
   1.524  
   1.525  
   1.526 -(*** sub ***)
   1.527 -
   1.528 -Addsimps [sub_def];
   1.529 -
   1.530 -Goal "lift_set i {s. P s} = {s. P (sub i s)}";
   1.531 -by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
   1.532 -qed "lift_set_sub";
   1.533 -
   1.534 -Goal "{s. P (s i)} = lift_set i {s. P s}";
   1.535 -by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
   1.536 -qed "Collect_eq_lift_set";
   1.537 -
   1.538 -Goal "sub i -`` A = lift_set i A";
   1.539 -by (Force_tac 1);
   1.540 -qed "sub_vimage";
   1.541 -Addsimps [sub_vimage];
   1.542 -
   1.543 -
   1.544  (** Are these two useful?? **)
   1.545  
   1.546  (*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
   1.547 @@ -542,69 +455,42 @@
   1.548  
   1.549  (*** guarantees corollaries ***)
   1.550  
   1.551 -Goalw [increasing_def]
   1.552 -     "F : UNIV guarantees increasing f \
   1.553 +Goal "F : UNIV guarantees increasing f \
   1.554  \     ==> lift_prog i F : UNIV guarantees increasing (f o sub i)";
   1.555 -by (etac drop_prog_guarantees 1);
   1.556 -by Auto_tac;
   1.557 -by (stac Collect_eq_lift_set 1); 
   1.558 -by (asm_full_simp_tac
   1.559 -    (simpset() addsimps [lift_prog_stable, drop_prog_stable, 
   1.560 -			 Join_stable]) 1);
   1.561 +by (dtac (lift_export extend_guar_increasing) 1);
   1.562 +by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   1.563  qed "lift_prog_guar_increasing";
   1.564  
   1.565 -Goalw [Increasing_def]
   1.566 -     "F : UNIV guarantees Increasing f \
   1.567 +Goal "F : UNIV guarantees Increasing f \
   1.568  \     ==> lift_prog i F : UNIV guarantees Increasing (f o sub i)";
   1.569 -by (etac drop_prog_guarantees 1);
   1.570 -by Auto_tac;
   1.571 -by (stac Collect_eq_lift_set 1); 
   1.572 -by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable]) 1);
   1.573 +by (dtac (lift_export extend_guar_Increasing) 1);
   1.574 +by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   1.575  qed "lift_prog_guar_Increasing";
   1.576  
   1.577 -Goalw [localTo_def, increasing_def]
   1.578 -     "F : (f localTo F) guarantees increasing f  \
   1.579 -\     ==> lift_prog i F : (f o sub i) localTo (lift_prog i F)  \
   1.580 -\                         guarantees increasing (f o sub i)";
   1.581 -by (etac drop_prog_guarantees 1);
   1.582 -by Auto_tac;
   1.583 -by (stac Collect_eq_lift_set 2); 
   1.584 -(*the "increasing" guarantee*)
   1.585 -by (asm_full_simp_tac
   1.586 -    (simpset() addsimps [lift_prog_stable, drop_prog_stable, 
   1.587 -			 Join_stable]) 2);
   1.588 -(*the "localTo" requirement*)
   1.589 -by (asm_simp_tac
   1.590 -    (simpset() addsimps [Diff_drop_prog_stable, 
   1.591 -			 Collect_eq_lift_set RS sym]) 1); 
   1.592 +Goal "F : (v localTo G) guarantees increasing func  \
   1.593 +\     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
   1.594 +\                         guarantees increasing (func o sub i)";
   1.595 +by (dtac (lift_export extend_localTo_guar_increasing) 1);
   1.596 +by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   1.597  qed "lift_prog_localTo_guar_increasing";
   1.598  
   1.599 -Goalw [localTo_def, Increasing_def]
   1.600 -     "F : (f localTo F) guarantees Increasing f  \
   1.601 -\     ==> lift_prog i F : (f o sub i) localTo (lift_prog i F)  \
   1.602 -\                         guarantees Increasing (f o sub i)";
   1.603 -by (etac drop_prog_guarantees 1);
   1.604 -by Auto_tac;
   1.605 -by (stac Collect_eq_lift_set 2); 
   1.606 -(*the "Increasing" guarantee*)
   1.607 -by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable]) 2);
   1.608 -(*the "localTo" requirement*)
   1.609 -by (asm_simp_tac
   1.610 -    (simpset() addsimps [Diff_drop_prog_stable, 
   1.611 -			 Collect_eq_lift_set RS sym]) 1); 
   1.612 +Goal "F : (v localTo G) guarantees Increasing func  \
   1.613 +\     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
   1.614 +\                         guarantees Increasing (func o sub i)";
   1.615 +by (dtac (lift_export extend_localTo_guar_Increasing) 1);
   1.616 +by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   1.617  qed "lift_prog_localTo_guar_Increasing";
   1.618  
   1.619 -(*Converse fails.  Useful?*)
   1.620 -Goal "lift_prog i `` (f localTo F) <= (f o sub i) localTo (lift_prog i F)";
   1.621 -by (simp_tac (simpset() addsimps [localTo_def]) 1);
   1.622 -by Auto_tac;
   1.623 -by (stac Collect_eq_lift_set 1); 
   1.624 -by (asm_simp_tac (simpset() addsimps [Diff_lift_prog_stable]) 1); 
   1.625 -qed "localTo_lift_prog_I";
   1.626 +Goal "F : Always A guarantees Always B \
   1.627 +\ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
   1.628 +by (asm_simp_tac
   1.629 +    (simpset() addsimps [lift_set_correct, lift_prog_correct, 
   1.630 +			 lift_export extend_guar_Always]) 1);
   1.631 +qed "lift_prog_guar_Always";
   1.632  
   1.633  (*No analogue of this in Extend.ML!*)
   1.634 -Goal "[| lift_prog i F : AA co BB |] \
   1.635 -\     ==> F : (drop_set i AA) co (drop_set i BB)";
   1.636 +Goal "[| lift_prog i F : A co B |] \
   1.637 +\     ==> F : (drop_set i A) co (drop_set i B)";
   1.638  by (auto_tac (claset(), 
   1.639  	      simpset() addsimps [constrains_def, drop_set_def]));
   1.640  by (force_tac (claset() addSIs [image_eqI'], simpset()) 1);