new theory UNITY/Lift_prog
authorpaulson
Fri Aug 06 17:27:51 1999 +0200 (1999-08-06)
changeset 7186860479291bb5
parent 7185 19672499bab6
child 7187 676027b1d770
new theory UNITY/Lift_prog
src/HOL/IsaMakefile
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Lift_prog.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Aug 06 15:38:07 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Aug 06 17:27:51 1999 +0200
     1.3 @@ -183,7 +183,8 @@
     1.4    UNITY/Extend.ML UNITY/Extend.thy\
     1.5    UNITY/Follows.ML UNITY/Follows.thy\
     1.6    UNITY/GenPrefix.thy UNITY/GenPrefix.ML \
     1.7 -  UNITY/LessThan.ML UNITY/LessThan.thy UNITY/ListOrder.thy\
     1.8 +  UNITY/LessThan.ML UNITY/LessThan.thy \
     1.9 +  UNITY/Lift_prog.ML UNITY/Lift_prog.thy UNITY/ListOrder.thy\
    1.10    UNITY/Mutex.ML UNITY/Mutex.thy\
    1.11    UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
    1.12    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Fri Aug 06 17:27:51 1999 +0200
     2.3 @@ -0,0 +1,478 @@
     2.4 +(*  Title:      HOL/UNITY/Lift_prog.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1998  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +
    2.11 +(*** Basic properties ***)
    2.12 +
    2.13 +(** lift_set and drop_set **)
    2.14 +
    2.15 +Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)";
    2.16 +by Auto_tac;
    2.17 +qed "lift_set_iff";
    2.18 +AddIffs [lift_set_iff];
    2.19 +
    2.20 +Goalw [lift_set_def] "lift_set i (A Int B) = lift_set i A Int lift_set i B";
    2.21 +by Auto_tac;
    2.22 +qed "lift_set_Int";
    2.23 +
    2.24 +(*Converse fails*)
    2.25 +Goalw [drop_set_def] "f : A ==> f i : drop_set i A";
    2.26 +by Auto_tac;
    2.27 +qed "drop_set_I";
    2.28 +
    2.29 +(** lift_act and drop_act **)
    2.30 +
    2.31 +Goalw [lift_act_def] "lift_act i Id = Id";
    2.32 +by Auto_tac;
    2.33 +by (etac rev_mp 1);
    2.34 +by (dtac sym 1);
    2.35 +by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
    2.36 +qed "lift_act_Id";
    2.37 +Addsimps [lift_act_Id];
    2.38 +
    2.39 +Goalw [drop_act_def] "(s, s') : act ==> (s i, s' i) : drop_act i act";
    2.40 +by (auto_tac (claset() addSIs [image_eqI], simpset()));
    2.41 +qed "drop_act_I";
    2.42 +
    2.43 +Goalw [drop_act_def] "drop_act i Id = Id";
    2.44 +by Auto_tac;
    2.45 +by (res_inst_tac [("x", "((%u. x), (%u. x))")] image_eqI 1);
    2.46 +by Auto_tac;
    2.47 +qed "drop_act_Id";
    2.48 +Addsimps [drop_act_Id];
    2.49 +
    2.50 +(** lift_prog and drop_prog **)
    2.51 +
    2.52 +Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
    2.53 +by Auto_tac;
    2.54 +qed "Init_lift_prog";
    2.55 +Addsimps [Init_lift_prog];
    2.56 +
    2.57 +Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
    2.58 +by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
    2.59 +qed "Acts_lift_prog";
    2.60 +Addsimps [Acts_lift_prog];
    2.61 +
    2.62 +Goalw [drop_prog_def] "Init (drop_prog i F) = drop_set i (Init F)";
    2.63 +by Auto_tac;
    2.64 +qed "Init_drop_prog";
    2.65 +Addsimps [Init_drop_prog];
    2.66 +
    2.67 +Goalw [drop_prog_def] "Acts (drop_prog i F) = drop_act i `` Acts F";
    2.68 +by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
    2.69 +qed "Acts_drop_prog";
    2.70 +Addsimps [Acts_drop_prog];
    2.71 +
    2.72 +Goal "F component G ==> lift_prog i F component lift_prog i G";
    2.73 +by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
    2.74 +by Auto_tac;
    2.75 +qed "lift_prog_mono";
    2.76 +
    2.77 +Goal "F component G ==> drop_prog i F component drop_prog i G";
    2.78 +by (full_simp_tac (simpset() addsimps [component_eq_subset, drop_set_def]) 1);
    2.79 +by Auto_tac;
    2.80 +qed "drop_prog_mono";
    2.81 +
    2.82 +Goal "lift_prog i SKIP = SKIP";
    2.83 +by (auto_tac (claset() addSIs [program_equalityI],
    2.84 +	      simpset() addsimps [SKIP_def, lift_prog_def]));
    2.85 +qed "lift_prog_SKIP";
    2.86 +
    2.87 +Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)";
    2.88 +by (rtac program_equalityI 1);
    2.89 +by (auto_tac (claset(), simpset() addsimps [Acts_Join]));
    2.90 +qed "lift_prog_Join";
    2.91 +
    2.92 +Goal "lift_prog i (JOIN I F) = (JN j:I. lift_prog i (F j))";
    2.93 +by (rtac program_equalityI 1);
    2.94 +by (auto_tac (claset(), simpset() addsimps [Acts_JN]));
    2.95 +qed "lift_prog_JN";
    2.96 +
    2.97 +Goal "drop_prog i SKIP = SKIP";
    2.98 +by (auto_tac (claset() addSIs [program_equalityI],
    2.99 +	      simpset() addsimps [SKIP_def, drop_set_def, drop_prog_def]));
   2.100 +qed "drop_prog_SKIP";
   2.101 +
   2.102 +
   2.103 +(** Injectivity of lift_set, lift_act, lift_prog **)
   2.104 +
   2.105 +Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F";
   2.106 +by Auto_tac;
   2.107 +qed "lift_set_inverse";
   2.108 +Addsimps [lift_set_inverse];
   2.109 +
   2.110 +Goal "inj (lift_set i)";
   2.111 +by (rtac inj_on_inverseI 1);
   2.112 +by (rtac lift_set_inverse 1);
   2.113 +qed "inj_lift_set";
   2.114 +
   2.115 +(*Because A and B could differ outside i, cannot generalize result to 
   2.116 +   drop_set i (A Int B) = drop_set i A Int drop_set i B
   2.117 +*)
   2.118 +Goalw [lift_set_def, drop_set_def]
   2.119 +     "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)";
   2.120 +by Auto_tac;
   2.121 +qed "drop_set_lift_set_Int";
   2.122 +
   2.123 +Goalw [lift_set_def, drop_set_def]
   2.124 +     "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A";
   2.125 +by Auto_tac;
   2.126 +qed "drop_set_lift_set_Int2";
   2.127 +
   2.128 +Goalw [drop_set_def]
   2.129 +     "i : I ==> drop_set i (INT j:I. lift_set j A) = A";
   2.130 +by Auto_tac;
   2.131 +qed "drop_set_INT";
   2.132 +
   2.133 +Goalw [lift_act_def, drop_act_def] "drop_act i (lift_act i act) = act";
   2.134 +by Auto_tac;
   2.135 +by (res_inst_tac [("x", "f(i:=a)")] exI 1);
   2.136 +by (Asm_simp_tac 1);
   2.137 +by (res_inst_tac [("x", "f(i:=b)")] exI 1);
   2.138 +by (Asm_simp_tac 1);
   2.139 +by (rtac ext 1);
   2.140 +by (Asm_simp_tac 1);
   2.141 +qed "lift_act_inverse";
   2.142 +Addsimps [lift_act_inverse];
   2.143 +
   2.144 +Goal "inj (lift_act i)";
   2.145 +by (rtac inj_on_inverseI 1);
   2.146 +by (rtac lift_act_inverse 1);
   2.147 +qed "inj_lift_act";
   2.148 +
   2.149 +Goal "drop_prog i (lift_prog i F) = F";
   2.150 +by (simp_tac (simpset() addsimps [lift_prog_def, drop_prog_def]) 1);
   2.151 +by (rtac program_equalityI 1);
   2.152 +by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 2);
   2.153 +by (Simp_tac 1);
   2.154 +qed "lift_prog_inverse";
   2.155 +Addsimps [lift_prog_inverse];
   2.156 +
   2.157 +Goal "inj (lift_prog i)";
   2.158 +by (rtac inj_on_inverseI 1);
   2.159 +by (rtac lift_prog_inverse 1);
   2.160 +qed "inj_lift_prog";
   2.161 +
   2.162 +
   2.163 +(*For compatibility with the original definition and perhaps simpler proofs*)
   2.164 +Goalw [lift_act_def]
   2.165 +    "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
   2.166 +by Auto_tac;
   2.167 +by (rtac exI 1);
   2.168 +by Auto_tac;
   2.169 +qed "lift_act_eq";
   2.170 +AddIffs [lift_act_eq];
   2.171 +
   2.172 +
   2.173 +(*** Safety: co, stable, invariant ***)
   2.174 +
   2.175 +(** Safety and lift_prog **)
   2.176 +
   2.177 +Goal "(lift_prog i F : (lift_set i A) co (lift_set i B))  =  \
   2.178 +\     (F : A co B)";
   2.179 +by (auto_tac (claset(), 
   2.180 +	      simpset() addsimps [constrains_def]));
   2.181 +by (Blast_tac 2);
   2.182 +by (Force_tac 1);
   2.183 +qed "lift_prog_constrains_eq";
   2.184 +
   2.185 +Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)";
   2.186 +by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains_eq]) 1);
   2.187 +qed "lift_prog_stable_eq";
   2.188 +
   2.189 +Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
   2.190 +by (auto_tac (claset(),
   2.191 +	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
   2.192 +qed "lift_prog_invariant_eq";
   2.193 +
   2.194 +(*This one looks strange!  Proof probably is by case analysis on i=j.
   2.195 +  If i~=j then lift_prog j (F j) does nothing to lift_set i, and the 
   2.196 +  premise ensures A<=B.*)
   2.197 +Goal "F i : A co B  \
   2.198 +\     ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
   2.199 +by (auto_tac (claset(), 
   2.200 +	      simpset() addsimps [constrains_def]));
   2.201 +by (REPEAT (Blast_tac 1));
   2.202 +qed "constrains_imp_lift_prog_constrains";
   2.203 +
   2.204 +
   2.205 +(** Safety and drop_prog **)
   2.206 +
   2.207 +Goalw [constrains_def]
   2.208 +     "(drop_prog i F : A co B)  =  (F : (lift_set i A) co (lift_set i B))";
   2.209 +by Auto_tac;
   2.210 +by (force_tac (claset(), 
   2.211 +	       simpset() addsimps [drop_act_def]) 2);
   2.212 +by (blast_tac (claset() addIs [drop_act_I]) 1);
   2.213 +qed "drop_prog_constrains_eq";
   2.214 +
   2.215 +Goal "(drop_prog i F : stable A)  =  (F : stable (lift_set i A))";
   2.216 +by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains_eq]) 1);
   2.217 +qed "drop_prog_stable_eq";
   2.218 +
   2.219 +
   2.220 +(** Diff, needed for localTo **)
   2.221 +
   2.222 +Goal "Diff G (lift_act i `` Acts F) : (lift_set i A) co (lift_set i B)  \
   2.223 +\     ==> Diff (drop_prog i G) (Acts F) : A co B";
   2.224 +by (auto_tac (claset(), 
   2.225 +	      simpset() addsimps [constrains_def, Diff_def]));
   2.226 +by (dtac bspec 1);
   2.227 +by (Force_tac 1);
   2.228 +by (auto_tac (claset(), simpset() addsimps [drop_act_def]));
   2.229 +by (auto_tac (claset(), simpset() addsimps [lift_set_def]));
   2.230 +qed "Diff_drop_prog_co";
   2.231 +
   2.232 +Goalw [stable_def]
   2.233 +     "Diff G (lift_act i `` Acts F) : stable (lift_set i A)  \
   2.234 +\     ==> Diff (drop_prog i G) (Acts F) : stable A";
   2.235 +by (etac Diff_drop_prog_co 1);
   2.236 +qed "Diff_drop_prog_stable";
   2.237 +
   2.238 +Goal "Diff G (Acts F) : A co B  \
   2.239 +\     ==> Diff (lift_prog i G) (lift_act i `` Acts F) \
   2.240 +\         : (lift_set i A) co (lift_set i B)";
   2.241 +by (auto_tac (claset(), 
   2.242 +	      simpset() addsimps [constrains_def, Diff_def]));
   2.243 +by (auto_tac (claset(), simpset() addsimps [drop_act_def]));
   2.244 +qed "Diff_lift_prog_co";
   2.245 +
   2.246 +Goalw [stable_def]
   2.247 +     "Diff G (Acts F) : stable A  \
   2.248 +\     ==> Diff (lift_prog i G) (lift_act i `` Acts F) : stable (lift_set i A)";
   2.249 +by (etac Diff_lift_prog_co 1);
   2.250 +qed "Diff_lift_prog_stable";
   2.251 +
   2.252 +
   2.253 +(*** Weak versions: Co, Stable ***)
   2.254 +
   2.255 +(** Reachability **)
   2.256 +
   2.257 +Goal "s : reachable F ==> f(i:=s) : reachable (lift_prog i F)";
   2.258 +by (etac reachable.induct 1);
   2.259 +by (force_tac (claset() addIs [reachable.Acts, ext], 
   2.260 +	       simpset()) 2);
   2.261 +by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
   2.262 +qed "reachable_lift_progI";
   2.263 +
   2.264 +Goal "f : reachable (lift_prog i F) ==> f i : reachable F";
   2.265 +by (etac reachable.induct 1);
   2.266 +by Auto_tac;
   2.267 +by (ALLGOALS (blast_tac (claset() addIs reachable.intrs)));
   2.268 +qed "reachable_lift_progD";
   2.269 +
   2.270 +Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
   2.271 +by Auto_tac;
   2.272 +by (etac reachable_lift_progD 1);
   2.273 +ren "f" 1;
   2.274 +by (dres_inst_tac [("f","f"),("i","i")] reachable_lift_progI 1);
   2.275 +by Auto_tac;
   2.276 +qed "reachable_lift_prog";
   2.277 +
   2.278 +Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
   2.279 +\     (F : A Co B)";
   2.280 +by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog,
   2.281 +				  lift_set_Int RS sym,
   2.282 +				  lift_prog_constrains_eq]) 1);
   2.283 +qed "lift_prog_Constrains_eq";
   2.284 +
   2.285 +Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
   2.286 +by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains_eq]) 1);
   2.287 +qed "lift_prog_Stable_eq";
   2.288 +
   2.289 +(** Reachability and drop_prog **)
   2.290 +
   2.291 +Goal "f : reachable F ==> f i : reachable (drop_prog i F)";
   2.292 +by (etac reachable.induct 1);
   2.293 +by (force_tac (claset() addIs [reachable.Acts, drop_act_I],
   2.294 +	       simpset()) 2);
   2.295 +by (force_tac (claset() addIs [reachable.Init, drop_set_I],
   2.296 +	       simpset()) 1);
   2.297 +qed "reachable_imp_reachable_drop_prog";
   2.298 +
   2.299 +(*Converse fails because it would require
   2.300 +  [| s i : reachable (drop_prog i F); s i : A |] ==> s : reachable F
   2.301 +*)
   2.302 +Goalw [Constrains_def]
   2.303 +     "drop_prog i F : A Co B ==> F : (lift_set i A) Co (lift_set i B)";
   2.304 +by (full_simp_tac (simpset() addsimps [drop_prog_constrains_eq]) 1);
   2.305 +by (etac constrains_weaken_L 1);
   2.306 +by Auto_tac;
   2.307 +by (etac reachable_imp_reachable_drop_prog 1);
   2.308 +qed "drop_prog_Constrains_D";
   2.309 +
   2.310 +Goalw [Stable_def]
   2.311 +     "drop_prog i F : Stable A ==> F : Stable (lift_set i A)";
   2.312 +by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
   2.313 +qed "drop_prog_Stable_D";
   2.314 +
   2.315 +
   2.316 +(*** Programs of the form lift_prog i F Join G
   2.317 +     in other words programs containing a replicated component ***)
   2.318 +
   2.319 +Goal "drop_prog i ((lift_prog i F) Join G) = F Join (drop_prog i G)";
   2.320 +by (rtac program_equalityI 1);
   2.321 +by (simp_tac (simpset() addsimps [Acts_Join, image_Un,
   2.322 +				  image_compose RS sym, o_def]) 2);
   2.323 +by (simp_tac (simpset() addsimps [drop_set_lift_set_Int]) 1);
   2.324 +qed "drop_prog_lift_prog_Join";
   2.325 +
   2.326 +Goal "(lift_prog i F) Join G = lift_prog i H \
   2.327 +\     ==> H = F Join (drop_prog i G)";
   2.328 +by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
   2.329 +by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
   2.330 +by (etac sym 1);
   2.331 +qed "lift_prog_Join_eq_lift_prog_D";
   2.332 +
   2.333 +Goal "f : reachable (lift_prog i F Join G)  \
   2.334 +\     ==> f i : reachable (F Join drop_prog i G)";
   2.335 +by (etac reachable.induct 1);
   2.336 +by (force_tac (claset() addIs [reachable.Init, drop_set_I], simpset()) 1);
   2.337 +(*By case analysis on whether the action is of lift_prog i F  or  G*)
   2.338 +by (force_tac (claset() addIs [reachable.Acts, drop_act_I], 
   2.339 +	       simpset() addsimps [Acts_Join, image_iff]) 1);
   2.340 +qed "reachable_lift_prog_Join_D";
   2.341 +
   2.342 +(*Opposite inclusion fails, even for the initial state: lift_set i includes
   2.343 +  ALL functions determined only by their value at i.*)
   2.344 +Goal "reachable (lift_prog i F Join G) <= \
   2.345 +\     lift_set i (reachable (F Join drop_prog i G))";
   2.346 +by Auto_tac;
   2.347 +by (etac reachable_lift_prog_Join_D 1);
   2.348 +qed "reachable_lift_prog_Join_subset";
   2.349 +
   2.350 +Goal "F Join drop_prog i G : Stable A    \
   2.351 +\     ==> lift_prog i F Join G : Stable (lift_set i A)";
   2.352 +by (full_simp_tac (simpset() addsimps [Stable_def, Constrains_def]) 1);
   2.353 +by (subgoal_tac 
   2.354 +    "lift_prog i F Join G : lift_set i (reachable (F Join drop_prog i G)) Int \
   2.355 +\                           lift_set i A \
   2.356 +\    co lift_set i A" 1);
   2.357 +by (asm_full_simp_tac 
   2.358 +    (simpset() addsimps [lift_set_Int RS sym,
   2.359 +			 lift_prog_constrains_eq,
   2.360 +			 drop_prog_constrains_eq RS sym,
   2.361 +			 drop_prog_lift_prog_Join]) 2);
   2.362 +by (blast_tac (claset() addIs [constrains_weaken, 
   2.363 +			       reachable_lift_prog_Join_D]) 1);
   2.364 +qed "lift_prog_Join_Stable_eq";
   2.365 +
   2.366 +
   2.367 +(*** guarantees properties ***)
   2.368 +
   2.369 +(** It seems that neither of these can be proved from the other. **)
   2.370 +
   2.371 +(*Strong precondition and postcondition; doesn't seem very useful*)
   2.372 +Goal "F : X guar Y \
   2.373 +\     ==> lift_prog i F : (lift_prog i `` X) guar (lift_prog i `` Y)";
   2.374 +by (rtac guaranteesI 1);
   2.375 +by Auto_tac;
   2.376 +by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
   2.377 +qed "lift_prog_guarantees";
   2.378 +
   2.379 +(*Weak precondition and postcondition; doesn't seem very useful*)
   2.380 +Goal "[| F : X guar Y;  drop_prog i `` XX <= X;  \
   2.381 +\        ALL G. F Join drop_prog i G : Y --> lift_prog i F Join G : YY |] \
   2.382 +\     ==> lift_prog i F : XX guar YY";
   2.383 +by (rtac guaranteesI 1);
   2.384 +by (dtac guaranteesD 1);
   2.385 +by (etac subsetD 1);
   2.386 +by (rtac image_eqI 1);
   2.387 +by (auto_tac (claset(), simpset() addsimps [drop_prog_lift_prog_Join]));
   2.388 +qed "drop_prog_guarantees";
   2.389 +
   2.390 +
   2.391 +(*** sub ***)
   2.392 +
   2.393 +Addsimps [sub_def];
   2.394 +
   2.395 +Goal "lift_set i {s. P s} = {s. P (sub i s)}";
   2.396 +by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
   2.397 +qed "lift_set_sub";
   2.398 +
   2.399 +Goal "{s. P (s i)} = lift_set i {s. P s}";
   2.400 +by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
   2.401 +qed "Collect_eq_lift_set";
   2.402 +
   2.403 +
   2.404 +(** Are these two useful?? **)
   2.405 +
   2.406 +(*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
   2.407 +  ensure that F has the form lift_prog i F for some F.*)
   2.408 +Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}";
   2.409 +by Auto_tac;
   2.410 +by (stac Collect_eq_lift_set 1); 
   2.411 +by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
   2.412 +qed "image_lift_prog_Stable";
   2.413 +
   2.414 +Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
   2.415 +by (simp_tac (simpset() addsimps [Increasing_def,
   2.416 +				  inj_lift_prog RS image_INT]) 1);
   2.417 +by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1);
   2.418 +qed "image_lift_prog_Increasing";
   2.419 +
   2.420 +
   2.421 +(*** guarantees corollaries ***)
   2.422 +
   2.423 +Goalw [increasing_def]
   2.424 +     "F : UNIV guar increasing f \
   2.425 +\     ==> lift_prog i F : UNIV guar increasing (f o sub i)";
   2.426 +by (etac drop_prog_guarantees 1);
   2.427 +by Auto_tac;
   2.428 +by (stac Collect_eq_lift_set 1); 
   2.429 +by (asm_full_simp_tac
   2.430 +    (simpset() addsimps [lift_prog_stable_eq, drop_prog_stable_eq, 
   2.431 +			 stable_Join]) 1);
   2.432 +qed "lift_prog_guar_increasing";
   2.433 +
   2.434 +Goalw [Increasing_def]
   2.435 +     "F : UNIV guar Increasing f \
   2.436 +\     ==> lift_prog i F : UNIV guar Increasing (f o sub i)";
   2.437 +by (etac drop_prog_guarantees 1);
   2.438 +by Auto_tac;
   2.439 +by (stac Collect_eq_lift_set 1); 
   2.440 +by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable_eq]) 1);
   2.441 +qed "lift_prog_guar_Increasing";
   2.442 +
   2.443 +Goalw [localTo_def, increasing_def]
   2.444 +     "F : (f localTo F) guar increasing f  \
   2.445 +\     ==> lift_prog i F : (f o sub i) localTo (lift_prog i F)  \
   2.446 +\                         guar increasing (f o sub i)";
   2.447 +by (etac drop_prog_guarantees 1);
   2.448 +by Auto_tac;
   2.449 +by (stac Collect_eq_lift_set 2); 
   2.450 +(*the "increasing" guarantee*)
   2.451 +by (asm_full_simp_tac
   2.452 +    (simpset() addsimps [lift_prog_stable_eq, drop_prog_stable_eq, 
   2.453 +			 stable_Join]) 2);
   2.454 +(*the "localTo" requirement*)
   2.455 +by (asm_simp_tac
   2.456 +    (simpset() addsimps [Diff_drop_prog_stable, 
   2.457 +			 Collect_eq_lift_set RS sym]) 1); 
   2.458 +qed "lift_prog_guar_increasing2";
   2.459 +
   2.460 +Goalw [localTo_def, Increasing_def]
   2.461 +     "F : (f localTo F) guar Increasing f  \
   2.462 +\     ==> lift_prog i F : (f o sub i) localTo (lift_prog i F)  \
   2.463 +\                         guar Increasing (f o sub i)";
   2.464 +by (etac drop_prog_guarantees 1);
   2.465 +by Auto_tac;
   2.466 +by (stac Collect_eq_lift_set 2); 
   2.467 +(*the "Increasing" guarantee*)
   2.468 +by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable_eq]) 2);
   2.469 +(*the "localTo" requirement*)
   2.470 +by (asm_simp_tac
   2.471 +    (simpset() addsimps [Diff_drop_prog_stable, 
   2.472 +			 Collect_eq_lift_set RS sym]) 1); 
   2.473 +qed "lift_prog_guar_Increasing2";
   2.474 +
   2.475 +(*Converse fails.  Useful?*)
   2.476 +Goal "lift_prog i `` (f localTo F) <= (f o sub i) localTo (lift_prog i F)";
   2.477 +by (simp_tac (simpset() addsimps [localTo_def]) 1);
   2.478 +by Auto_tac;
   2.479 +by (stac Collect_eq_lift_set 1); 
   2.480 +by (asm_simp_tac (simpset() addsimps [Diff_lift_prog_stable]) 1); 
   2.481 +qed "localTo_lift_prog_I";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Fri Aug 06 17:27:51 1999 +0200
     3.3 @@ -0,0 +1,41 @@
     3.4 +(*  Title:      HOL/UNITY/Lift_prog.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1999  University of Cambridge
     3.8 +
     3.9 +lift_prog, etc: replication of components
    3.10 +*)
    3.11 +
    3.12 +Lift_prog = Union + Comp +
    3.13 +
    3.14 +constdefs
    3.15 +
    3.16 +  lift_set :: "['a, 'b set] => ('a => 'b) set"
    3.17 +    "lift_set i A == {f. f i : A}"
    3.18 +
    3.19 +  drop_set :: "['a, ('a=>'b) set] => 'b set"
    3.20 +    "drop_set i A == (%f. f i) `` A"
    3.21 +
    3.22 +  lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
    3.23 +    "lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}"
    3.24 +
    3.25 +  drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
    3.26 +    "drop_act i act == (%(f,f'). (f i, f' i)) `` act"
    3.27 +
    3.28 +  lift_prog :: "['a, 'b program] => ('a => 'b) program"
    3.29 +    "lift_prog i F ==
    3.30 +       mk_program (lift_set i (Init F),
    3.31 +		   lift_act i `` Acts F)"
    3.32 +
    3.33 +  drop_prog :: "['a, ('a=>'b) program] => 'b program"
    3.34 +    "drop_prog i F ==
    3.35 +       mk_program (drop_set i (Init F),
    3.36 +		   drop_act i `` (Acts F))"
    3.37 +
    3.38 +  (*simplifies the expression of specifications*)
    3.39 +  constdefs
    3.40 +    sub :: ['a, 'a=>'b] => 'b
    3.41 +      "sub i f == f i"
    3.42 +
    3.43 +
    3.44 +end