working version with localTo[C] instead of localTo
authorpaulson
Mon Oct 18 15:18:24 1999 +0200 (1999-10-18)
changeset 787843b03d412b82
parent 7877 e5e019d60f71
child 7879 4547f0bd9454
working version with localTo[C] instead of localTo
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/LessThan.ML
src/HOL/UNITY/LessThan.thy
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/Project.ML
src/HOL/UNITY/Project.thy
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Mon Oct 18 15:17:35 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Mon Oct 18 15:18:24 1999 +0200
     1.3 @@ -388,35 +388,37 @@
     1.4  
     1.5  (*A LOT of work just to lift "Client_Progress" to the array*)
     1.6  Goal "lift_prog i Client \
     1.7 -\  : Increasing (giv o sub i) Int ((%z. z i) localTo (lift_prog i Client)) \
     1.8 +\  : Increasing (giv o sub i) Int ((%z. z i) localTo[UNIV] (lift_prog i Client)) \
     1.9  \    guarantees \
    1.10  \    (INT h. {s. h <=  (giv o sub i) s & \
    1.11  \                       h pfixGe (ask o sub i) s}  \
    1.12  \            LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
    1.13 -br (Client_Progress RS drop_prog_guarantees) 1;
    1.14 -br (lift_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
    1.15 -br subset_refl 4;
    1.16 +by (rtac (Client_Progress RS drop_prog_guarantees) 1);
    1.17 +by (rtac (lift_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
    1.18 +by (rtac subset_refl 4);
    1.19  by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3);
    1.20  by (force_tac (claset(), simpset() addsimps [lift_prog_correct]) 2);
    1.21  by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1);
    1.22  by (auto_tac (claset(), simpset() addsimps [o_def]));
    1.23  qed "Client_i_Progress";
    1.24  
    1.25 +xxxxxxxxxxxxxxxx;
    1.26 +
    1.27  Goalw [System_def]
    1.28       "i < Nclients \
    1.29  \ ==> System : (INT h. {s. h <=  (giv o sub i o client) s & \
    1.30  \                       h pfixGe (ask o sub i o client) s}  \
    1.31  \            LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
    1.32  by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
    1.33 -br (guarantees_PLam_I RS project_guarantees) 1;
    1.34 -br Client_i_Progress  1;
    1.35 +by (rtac (guarantees_PLam_I RS project_guarantees) 1);
    1.36 +by (rtac Client_i_Progress  1);
    1.37  by (Force_tac 1);
    1.38 -br (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
    1.39 -br subset_refl 4;
    1.40 +by (rtac (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
    1.41 +by (rtac subset_refl 4);
    1.42  by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
    1.43 -br projecting_Int 1;
    1.44 -br (client_export projecting_Increasing) 1;
    1.45 -br (client_export projecting_localTo) 1;
    1.46 +by (rtac projecting_Int 1);
    1.47 +by (rtac (client_export projecting_Increasing) 1);
    1.48 +by (rtac (client_export projecting_localTo) 1);
    1.49  
    1.50  by (simp_tac (simpset()addsimps [lift_prog_correct]) 1);
    1.51  
     2.1 --- a/src/HOL/UNITY/Client.ML	Mon Oct 18 15:17:35 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Client.ML	Mon Oct 18 15:18:24 1999 +0200
     2.3 @@ -73,7 +73,7 @@
     2.4  program_defs_ref := [];
     2.5  
     2.6  (*Safety property 2: clients return the right number of tokens*)
     2.7 -Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg))  \
     2.8 +Goal "Cli_prg : (Increasing giv Int (rel localTo[UNIV] Cli_prg))  \
     2.9  \               guarantees Always {s. rel s <= giv s}";
    2.10  by (rtac guaranteesI 1);
    2.11  by (rtac AlwaysI 1);
    2.12 @@ -101,7 +101,7 @@
    2.13  val Increasing_length = mono_length RS mono_Increasing_o;
    2.14  
    2.15  Goal "Cli_prg : \
    2.16 -\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
    2.17 +\      (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg)) \
    2.18  \      guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
    2.19  \                            {s. size (rel s) <= size (giv s)})";
    2.20  by (rtac guaranteesI 1);
    2.21 @@ -122,7 +122,7 @@
    2.22  
    2.23  
    2.24  Goal "Cli_prg : \
    2.25 -\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
    2.26 +\      (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg) \
    2.27  \                 Int Always giv_meets_ask) \
    2.28  \      guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
    2.29  by (rtac guaranteesI 1);
     3.1 --- a/src/HOL/UNITY/Comp.ML	Mon Oct 18 15:17:35 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Comp.ML	Mon Oct 18 15:18:24 1999 +0200
     3.3 @@ -62,7 +62,7 @@
     3.4  qed "component_antisym";
     3.5  
     3.6  Goalw [component_def]
     3.7 -      "F <= H = (EX G. F Join G = H & Disjoint F G)";
     3.8 +      "F <= H = (EX G. F Join G = H & Disjoint UNIV F G)";
     3.9  by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
    3.10  qed "component_eq";
    3.11  
    3.12 @@ -77,8 +77,3 @@
    3.13  qed "component_constrains";
    3.14  
    3.15  bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
    3.16 -
    3.17 -Goal "Diff F (Acts G) <= F";
    3.18 -by (auto_tac (claset() addSIs [program_equalityI],
    3.19 -	      simpset() addsimps [Diff_def, component_eq_subset]));
    3.20 -qed "Diff_component";
     4.1 --- a/src/HOL/UNITY/Extend.ML	Mon Oct 18 15:17:35 1999 +0200
     4.2 +++ b/src/HOL/UNITY/Extend.ML	Mon Oct 18 15:18:24 1999 +0200
     4.3 @@ -8,6 +8,17 @@
     4.4    function g (forgotten) maps the extended state to the "extending part"
     4.5  *)
     4.6  
     4.7 +
     4.8 +
     4.9 +		Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
    4.10 +		by  (Blast_tac 1);
    4.11 +		qed "disjoint_iff_not_equal";
    4.12 +
    4.13 +		Goal "ff -`` (ff `` A) = {y. EX x:A. ff x = ff y}";
    4.14 +		by (blast_tac (claset() addIs [sym]) 1);
    4.15 +		qed "vimage_image_eq";
    4.16 +
    4.17 +
    4.18  (** These we prove OUTSIDE the locale. **)
    4.19  
    4.20  (*Possibly easier than reasoning about "inv h"*)
    4.21 @@ -57,13 +68,41 @@
    4.22  (*FIXME: If locales worked properly we could put just "f" above*)
    4.23  by (full_simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1);
    4.24  qed "h_inject1";
    4.25 -AddSDs [h_inject1];
    4.26 +AddDs [h_inject1];
    4.27  
    4.28  Goal "h(f z, g z) = z";
    4.29  by (simp_tac (simpset() addsimps [f_def, g_def, surjective_pairing RS sym,
    4.30  				  surj_h RS surj_f_inv_f]) 1);
    4.31  qed "h_f_g_eq";
    4.32  
    4.33 +
    4.34 +(** A sequence of proof steps borrowed from Provers/split_paired_all.ML **)
    4.35 +
    4.36 +val cT = TFree ("'c", ["term"]);
    4.37 +
    4.38 +(* "PROP P x == PROP P (h (f x, g x))" *)
    4.39 +val lemma1 = Thm.combination
    4.40 +  (Thm.reflexive (cterm_of (sign_of thy) (Free ("P", cT --> propT))))
    4.41 +  (Drule.unvarify (h_f_g_eq RS sym RS eq_reflection));
    4.42 +
    4.43 +val prems = Goalw [lemma1] "(!!u y. PROP P (h (u, y))) ==> PROP P x";
    4.44 +by (resolve_tac prems 1);
    4.45 +val lemma2 = result();
    4.46 +
    4.47 +val prems = Goal "(!!u y. PROP P (h (u, y))) ==> (!!z. PROP P z)";
    4.48 +by (rtac lemma2 1);
    4.49 +by (resolve_tac prems 1);
    4.50 +val lemma3 = result();
    4.51 +
    4.52 +val prems = Goal "(!!z. PROP P z) ==> (!!u y. PROP P (h (u, y)))";
    4.53 +(*not needed for proof, but prevents generalization over h, 'c, etc.*)
    4.54 +by (cut_facts_tac [surj_h] 1);
    4.55 +by (resolve_tac prems 1);
    4.56 +val lemma4 = result();
    4.57 +
    4.58 +val split_extended_all = Thm.equal_intr lemma4 lemma3;
    4.59 +
    4.60 +
    4.61  (*** extend_set: basic properties ***)
    4.62  
    4.63  Goalw [extend_set_def] "A<=B ==> extend_set h A <= extend_set h B";
    4.64 @@ -101,9 +140,8 @@
    4.65  qed "inj_extend_set";
    4.66  
    4.67  Goalw [extend_set_def] "extend_set h UNIV = UNIV";
    4.68 -by Auto_tac;
    4.69 -by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
    4.70 -by Auto_tac;
    4.71 +by (auto_tac (claset(), 
    4.72 +	      simpset() addsimps [split_extended_all]));
    4.73  qed "extend_set_UNIV_eq";
    4.74  Addsimps [standard extend_set_UNIV_eq];
    4.75  
    4.76 @@ -111,14 +149,14 @@
    4.77  
    4.78  (*project_set is simply image!*)
    4.79  Goalw [project_set_def] "project_set h C = f `` C";
    4.80 -by (auto_tac (claset() addIs [f_h_eq RS sym, h_f_g_eq RS ssubst], 
    4.81 -	      simpset()));
    4.82 +by (auto_tac (claset() addIs [f_h_eq RS sym], 
    4.83 +	      simpset() addsimps [split_extended_all]));
    4.84  qed "project_set_eq";
    4.85  
    4.86  (*Converse appears to fail*)
    4.87 -Goalw [project_set_def] "z : C ==> f z : project_set h C";
    4.88 -by (auto_tac (claset() addIs [h_f_g_eq RS ssubst], 
    4.89 -	      simpset()));
    4.90 +Goalw [project_set_def] "!!z. z : C ==> f z : project_set h C";
    4.91 +by (auto_tac (claset(), 
    4.92 +	      simpset() addsimps [split_extended_all]));
    4.93  qed "project_set_I";
    4.94  
    4.95  
    4.96 @@ -160,31 +198,41 @@
    4.97  
    4.98  (*** extend_act ***)
    4.99  
   4.100 -(*Actions could affect the g-part, so result Cannot be strengthened to
   4.101 -   ((z, z') : extend_act h act) = ((f z, f z') : act)
   4.102 -*)
   4.103  Goalw [extend_act_def]
   4.104       "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)";
   4.105  by Auto_tac;
   4.106  qed "mem_extend_act_iff";
   4.107  AddIffs [mem_extend_act_iff]; 
   4.108  
   4.109 +(*Converse fails: (z,z') would include actions that changed the g-part*)
   4.110  Goalw [extend_act_def]
   4.111       "(z, z') : extend_act h act ==> (f z, f z') : act";
   4.112  by Auto_tac;
   4.113  qed "extend_act_D";
   4.114  
   4.115 +Goalw [extend_act_def, project_act_def, project_set_def]
   4.116 +     "project_act h (Restrict C (extend_act h act)) = \
   4.117 +\     Restrict (project_set h C) act";
   4.118 +by (Blast_tac 1);
   4.119 +qed "project_act_extend_act_restrict";
   4.120 +Addsimps [project_act_extend_act_restrict];
   4.121 +
   4.122 +Goalw [extend_act_def, project_act_def, project_set_def]
   4.123 +     "(Restrict C (extend_act h act) = Restrict C (extend_act h act')) \
   4.124 +\     = (Restrict (project_set h C) act = Restrict (project_set h C) act')";
   4.125 +by Auto_tac;
   4.126 +by (ALLGOALS (blast_tac (claset() addSEs [equalityE])));
   4.127 +qed "Restrict_extend_act_eq_Restrict_project_act";
   4.128 +
   4.129  (*Premise is still undesirably strong, since Domain act can include
   4.130    non-reachable states, but it seems necessary for this result.*)
   4.131 -Goalw [extend_act_def, project_set_def, project_act_def]
   4.132 - "Domain act <= project_set h C ==> project_act C h (extend_act h act) = act";
   4.133 -by (Force_tac 1);
   4.134 +Goal "Domain act <= project_set h C \
   4.135 +\     ==> project_act h (Restrict C (extend_act h act)) = act";
   4.136 +by (asm_simp_tac (simpset() addsimps [Restrict_triv]) 1);
   4.137  qed "extend_act_inverse";
   4.138 -Addsimps [extend_act_inverse];
   4.139  
   4.140 -(*By subset_refl, a corollary is project_act C h (extend_act h act) <= act*)
   4.141  Goalw [extend_act_def, project_act_def]
   4.142 -     "act' <= extend_act h act ==> project_act C h act' <= act";
   4.143 +     "act' <= extend_act h act ==> project_act h act' <= act";
   4.144  by (Force_tac 1);
   4.145  qed "subset_extend_act_D";
   4.146  
   4.147 @@ -218,22 +266,20 @@
   4.148  qed "extend_act_Id";
   4.149  
   4.150  Goalw [project_act_def]
   4.151 -     "[| (z, z') : act;  z: C |] \
   4.152 -\     ==> (f z, f z') : project_act C h act";
   4.153 -by (auto_tac (claset() addSIs [exI] addIs [h_f_g_eq RS ssubst], 
   4.154 -	      simpset()));
   4.155 +     "!!z z'. (z, z') : act ==> (f z, f z') : project_act h act";
   4.156 +by (force_tac (claset(), 
   4.157 +              simpset() addsimps [split_extended_all]) 1);
   4.158  qed "project_act_I";
   4.159  
   4.160  Goalw [project_set_def, project_act_def]
   4.161 -    "UNIV <= project_set h C ==> project_act C h Id = Id";
   4.162 +    "UNIV <= project_set h C ==> project_act h (Restrict C Id) = Id";
   4.163  by (Force_tac 1);
   4.164  qed "project_act_Id";
   4.165  
   4.166  Goalw [project_set_def, project_act_def]
   4.167 -    "Domain (project_act C h act) = project_set h (Domain act Int C)";
   4.168 -by Auto_tac;
   4.169 -by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1);
   4.170 -by Auto_tac;
   4.171 +  "Domain (project_act h (Restrict C act)) = project_set h (Domain act Int C)";
   4.172 +by (force_tac (claset(), 
   4.173 +              simpset() addsimps [split_extended_all]) 1);
   4.174  qed "Domain_project_act";
   4.175  
   4.176  Addsimps [extend_act_Id, project_act_Id];
   4.177 @@ -267,7 +313,7 @@
   4.178  	      simpset() addsimps [extend_def, image_iff]));
   4.179  qed "Acts_extend";
   4.180  
   4.181 -Goal "Acts (project C h F) = insert Id (project_act C h `` Acts F)";
   4.182 +Goal "Acts (project C h F) = insert Id (project_act h `` Restrict C `` Acts F)";
   4.183  by (auto_tac (claset(), 
   4.184  	      simpset() addsimps [project_def, image_iff]));
   4.185  qed "Acts_project";
   4.186 @@ -279,17 +325,18 @@
   4.187  by Auto_tac;
   4.188  qed "extend_SKIP";
   4.189  
   4.190 -Goalw [project_set_def] "UNIV <= project_set h UNIV";
   4.191 +Goalw [project_set_def] "project_set h UNIV = UNIV";
   4.192  by Auto_tac;
   4.193  qed "project_set_UNIV";
   4.194 +Addsimps [project_set_UNIV];
   4.195  
   4.196  (*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
   4.197  Goal "UNIV <= project_set h C \
   4.198  \     ==> project C h (extend h F) = F";
   4.199  by (simp_tac (simpset() addsimps [extend_def, project_def]) 1);
   4.200  by (rtac program_equalityI 1);
   4.201 -by (asm_simp_tac (simpset() addsimps [image_image_eq_UN,
   4.202 -                   subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
   4.203 +by (asm_simp_tac (simpset() addsimps [image_image_eq_UN, image_UN, 
   4.204 +                   subset_UNIV RS subset_trans RS Restrict_triv]) 2);
   4.205  by (Simp_tac 1);
   4.206  qed "extend_inverse";
   4.207  Addsimps [extend_inverse];
   4.208 @@ -354,43 +401,84 @@
   4.209  
   4.210  (*** Diff, needed for localTo ***)
   4.211  
   4.212 -Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
   4.213 +Goal "Restrict (extend_set h C) (extend_act h act) = \
   4.214 +\     extend_act h (Restrict C act)";
   4.215 +by (auto_tac (claset(), 
   4.216 +              simpset() addsimps [split_extended_all]));
   4.217 +by (auto_tac (claset(), 
   4.218 +              simpset() addsimps [extend_act_def]));
   4.219 +qed "Restrict_extend_set";
   4.220 +
   4.221 +Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts)) = \
   4.222 +\     extend h (Diff C G acts)";
   4.223  by (auto_tac (claset() addSIs [program_equalityI],
   4.224 -	      simpset() addsimps [Diff_def,
   4.225 +	      simpset() addsimps [Diff_def, image_image_eq_UN,
   4.226 +				  Restrict_extend_set,
   4.227  				  inj_extend_act RS image_set_diff]));
   4.228  qed "Diff_extend_eq";
   4.229  
   4.230 -Goal "(Diff (extend h G) (extend_act h `` acts) \
   4.231 +(*Opposite inclusion fails; this inclusion's more general than that of
   4.232 +  Diff_extend_eq*)     
   4.233 +Goal "Diff (project_set h C) G acts \
   4.234 +\     <= project C h (Diff C (extend h G) (extend_act h `` acts))";
   4.235 +by (simp_tac
   4.236 +    (simpset() addsimps [component_eq_subset, Diff_def,image_UN,
   4.237 +			 image_image, image_Diff_image_eq,
   4.238 +			 Restrict_extend_act_eq_Restrict_project_act,
   4.239 +			 vimage_image_eq]) 1);
   4.240 +by  (blast_tac (claset() addSEs [equalityE])1);
   4.241 +qed "Diff_project_set_component";
   4.242 +
   4.243 +Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
   4.244  \         : (extend_set h A) co (extend_set h B)) \
   4.245 -\     = (Diff G acts : A co B)";
   4.246 +\     = (Diff C G acts : A co B)";
   4.247  by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
   4.248  qed "Diff_extend_constrains";
   4.249  
   4.250 -Goal "(Diff (extend h G) (extend_act h `` acts) : stable (extend_set h A)) \
   4.251 -\     = (Diff G acts : stable A)";
   4.252 +Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
   4.253 +\       : stable (extend_set h A)) \
   4.254 +\     = (Diff C G acts : stable A)";
   4.255  by (simp_tac (simpset() addsimps [Diff_extend_constrains, stable_def]) 1);
   4.256  qed "Diff_extend_stable";
   4.257  
   4.258 -Goal "Diff (extend h G) (extend_act h `` acts) : A co B \
   4.259 -\     ==> Diff G acts : (project_set h A) co (project_set h B)";
   4.260 +(*UNUSED!!*)
   4.261 +Goal "Diff (extend_set h C) (extend h G) (extend_act h `` acts) : A co B \
   4.262 +\     ==> Diff C G acts : (project_set h A) co (project_set h B)";
   4.263  by (asm_full_simp_tac (simpset() addsimps [Diff_extend_eq, 
   4.264  					   extend_constrains_project_set]) 1);
   4.265  qed "Diff_extend_constrains_project_set";
   4.266  
   4.267 -Goalw [localTo_def]
   4.268 -     "(extend h F : (v o f) localTo extend h H) = (F : v localTo H)";
   4.269 -by (simp_tac (simpset() addsimps []) 1);
   4.270 +Goalw [LOCALTO_def]
   4.271 +     "(extend h F : (v o f) localTo[extend_set h C] extend h H) = \
   4.272 +\     (F : v localTo[C] H)";
   4.273 +by (Simp_tac 1);
   4.274  (*A trick to strip both quantifiers*)
   4.275  by (res_inst_tac [("f", "All")] (ext RS arg_cong) 1);
   4.276  by (stac Collect_eq_extend_set 1);
   4.277  by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
   4.278  qed "extend_localTo_extend_eq";
   4.279  
   4.280 -Goal "Disjoint (extend h F) (extend h G) = Disjoint F G";
   4.281 -by (simp_tac (simpset() addsimps [Disjoint_def,
   4.282 -				  inj_extend_act RS image_Int RS sym]) 1);
   4.283 -by (simp_tac (simpset() addsimps [image_subset_iff, extend_act_Id_iff]) 1);
   4.284 -by (blast_tac (claset() addEs [equalityE]) 1);
   4.285 +(*USED?? opposite inclusion fails*)
   4.286 +Goal "Restrict C (extend_act h act) <= \
   4.287 +\     extend_act h (Restrict (project_set h C) act)";
   4.288 +by (auto_tac (claset(), 
   4.289 +              simpset() addsimps [split_extended_all]));
   4.290 +by (auto_tac (claset(), 
   4.291 +              simpset() addsimps [extend_act_def, project_set_def]));
   4.292 +qed "Restrict_extend_set_subset";
   4.293 +
   4.294 +
   4.295 +Goal "(extend_act h `` Acts F) - {Id} = extend_act h `` (Acts F - {Id})";
   4.296 +by (stac (extend_act_Id RS sym) 1);
   4.297 +by (simp_tac (simpset() addsimps [inj_extend_act RS image_set_diff]) 1);
   4.298 +qed "extend_act_image_Id_eq";
   4.299 +
   4.300 +Goal "Disjoint C (extend h F) (extend h G) = Disjoint (project_set h C) F G";
   4.301 +by (simp_tac
   4.302 +    (simpset() addsimps [Disjoint_def, disjoint_iff_not_equal,
   4.303 +			 image_Diff_image_eq,
   4.304 +			 Restrict_extend_act_eq_Restrict_project_act,
   4.305 +			 extend_act_Id_iff, vimage_def]) 1);
   4.306  qed "Disjoint_extend_eq";
   4.307  Addsimps [Disjoint_extend_eq];
   4.308  
     5.1 --- a/src/HOL/UNITY/Extend.thy	Mon Oct 18 15:17:35 1999 +0200
     5.2 +++ b/src/HOL/UNITY/Extend.thy	Mon Oct 18 15:18:24 1999 +0200
     5.3 @@ -25,18 +25,17 @@
     5.4    extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
     5.5      "extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
     5.6  
     5.7 -  (*Argument C allows weak safety laws to be projected*)
     5.8 -  project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"
     5.9 -    "project_act C h act ==
    5.10 -         {(x,x'). EX y y'. (h(x,y), h(x',y')) : act & (h(x,y) : C)}"
    5.11 +  project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
    5.12 +    "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}"
    5.13  
    5.14    extend :: "['a*'b => 'c, 'a program] => 'c program"
    5.15      "extend h F == mk_program (extend_set h (Init F),
    5.16  			       extend_act h `` Acts F)"
    5.17  
    5.18 +  (*Argument C allows weak safety laws to be projected*)
    5.19    project :: "['c set, 'a*'b => 'c, 'c program] => 'a program"
    5.20      "project C h F == mk_program (project_set h (Init F),
    5.21 -		  	          project_act C h `` Acts F)"
    5.22 +		  	          project_act h `` Restrict C `` Acts F)"
    5.23  
    5.24  locale Extend =
    5.25    fixes 
     6.1 --- a/src/HOL/UNITY/Guar.ML	Mon Oct 18 15:17:35 1999 +0200
     6.2 +++ b/src/HOL/UNITY/Guar.ML	Mon Oct 18 15:18:24 1999 +0200
     6.3 @@ -65,7 +65,7 @@
     6.4  (*** guarantees ***)
     6.5  
     6.6  val prems = Goal
     6.7 -     "(!!G. [| F Join G : X;  Disjoint F G |] ==> F Join G : Y) \
     6.8 +     "(!!G. [| F Join G : X;  Disjoint UNIV F G |] ==> F Join G : Y) \
     6.9  \     ==> F : X guarantees Y";
    6.10  by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
    6.11  by (blast_tac (claset() addIs prems) 1);
    6.12 @@ -84,7 +84,7 @@
    6.13  
    6.14  (*This equation is more intuitive than the official definition*)
    6.15  Goal "(F : X guarantees Y) = \
    6.16 -\     (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
    6.17 +\     (ALL G. F Join G : X & Disjoint UNIV F G --> F Join G : Y)";
    6.18  by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
    6.19  by (Blast_tac 1);
    6.20  qed "guarantees_eq";
     7.1 --- a/src/HOL/UNITY/LessThan.ML	Mon Oct 18 15:17:35 1999 +0200
     7.2 +++ b/src/HOL/UNITY/LessThan.ML	Mon Oct 18 15:18:24 1999 +0200
     7.3 @@ -7,6 +7,61 @@
     7.4  *)
     7.5  
     7.6  
     7.7 +(*** Restrict [MOVE TO RELATION.THY??] ***)
     7.8 +
     7.9 +Goalw [Restrict_def] "((x,y): Restrict A r) = ((x,y): r & x: A)";
    7.10 +by (Blast_tac 1);
    7.11 +qed "Restrict_iff";
    7.12 +AddIffs [Restrict_iff];
    7.13 +
    7.14 +Goal "Restrict UNIV = id";
    7.15 +by (rtac ext 1);
    7.16 +by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
    7.17 +qed "Restrict_UNIV";
    7.18 +Addsimps [Restrict_UNIV];
    7.19 +
    7.20 +Goal "Restrict {} r = {}";
    7.21 +by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
    7.22 +qed "Restrict_empty";
    7.23 +Addsimps [Restrict_empty];
    7.24 +
    7.25 +Goalw [Restrict_def] "Restrict A (Restrict B r) = Restrict (A Int B) r";
    7.26 +by (Blast_tac 1);
    7.27 +qed "Restrict_Int";
    7.28 +Addsimps [Restrict_Int];
    7.29 +
    7.30 +Goalw [Restrict_def] "Domain r <= A ==> Restrict A r = r";
    7.31 +by Auto_tac;
    7.32 +qed "Restrict_triv";
    7.33 +
    7.34 +Goalw [Restrict_def] "Restrict A r <= r";
    7.35 +by Auto_tac;
    7.36 +qed "Restrict_subset";
    7.37 +
    7.38 +Goalw [Restrict_def]
    7.39 +     "[| A <= B;  Restrict B r = Restrict B s |] \
    7.40 +\     ==> Restrict A r = Restrict A s";
    7.41 +by (blast_tac (claset() addSEs [equalityE]) 1);
    7.42 +qed "Restrict_eq_mono";
    7.43 +
    7.44 +Goalw [Restrict_def, image_def]
    7.45 +     "[| s : RR;  Restrict A r = Restrict A s |] \
    7.46 +\     ==> Restrict A r : Restrict A `` RR";
    7.47 +by Auto_tac;
    7.48 +qed "Restrict_imageI";
    7.49 +
    7.50 +Goal "(Restrict A `` (Restrict A `` r - s)) = (Restrict A `` r - s)";
    7.51 +by Auto_tac;
    7.52 +by (rewrite_goals_tac [image_def, Restrict_def]);
    7.53 +by (Blast_tac 1);
    7.54 +qed "Restrict_image_Diff";
    7.55 +
    7.56 +(*Nothing to do with Restrict, but to specialized for Fun.ML?*)
    7.57 +Goal "f``(g``A - B) = (UN x: (A - g-`` B). {f(g(x))})";
    7.58 +by (Blast_tac 1);
    7.59 +qed "image_Diff_image_eq";
    7.60 +
    7.61 +
    7.62  (*** lessThan ***)
    7.63  
    7.64  Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
     8.1 --- a/src/HOL/UNITY/LessThan.thy	Mon Oct 18 15:17:35 1999 +0200
     8.2 +++ b/src/HOL/UNITY/LessThan.thy	Mon Oct 18 15:18:24 1999 +0200
     8.3 @@ -12,6 +12,10 @@
     8.4  
     8.5  constdefs
     8.6  
     8.7 +  (*MOVE TO RELATION.THY??*)
     8.8 +  Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
     8.9 +    "Restrict A r == r Int (A Times UNIV)"
    8.10 +
    8.11    lessThan   :: "nat => nat set"
    8.12       "lessThan n == {i. i<n}"
    8.13  
     9.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Oct 18 15:17:35 1999 +0200
     9.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Mon Oct 18 15:18:24 1999 +0200
     9.3 @@ -54,13 +54,8 @@
     9.4  qed "lift_act_eq";
     9.5  AddIffs [lift_act_eq];
     9.6  
     9.7 -Goalw [drop_act_def]
     9.8 -     "[| (s, s') : act;  s : C |] ==> (s i, s' i) : drop_act C i act";
     9.9 -by Auto_tac;
    9.10 -qed "drop_act_I";
    9.11 -
    9.12  Goalw [drop_set_def, drop_act_def]
    9.13 -     "UNIV <= drop_set i C ==> drop_act C i Id = Id";
    9.14 +     "UNIV <= drop_set i C ==> drop_act i (Restrict C Id) = Id";
    9.15  by (Blast_tac 1);
    9.16  qed "drop_act_Id";
    9.17  Addsimps [drop_act_Id];
    9.18 @@ -82,7 +77,7 @@
    9.19  qed "Init_drop_prog";
    9.20  Addsimps [Init_drop_prog];
    9.21  
    9.22 -Goal "Acts (drop_prog C i F) = insert Id (drop_act C i `` Acts F)";
    9.23 +Goal "Acts (drop_prog C i F) = insert Id (drop_act i `` Restrict C `` Acts F)";
    9.24  by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], 
    9.25  	      simpset() addsimps [drop_prog_def]));
    9.26  qed "Acts_drop_prog";
    9.27 @@ -169,7 +164,7 @@
    9.28  by (auto_tac (claset() addSIs [exI], simpset()));
    9.29  qed "lift_act_correct";
    9.30  
    9.31 -Goal "drop_act C i = project_act C (lift_map i)";
    9.32 +Goal "drop_act i = project_act (lift_map i)";
    9.33  by (rtac ext 1);
    9.34  by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
    9.35  by Auto_tac;
    9.36 @@ -230,12 +225,14 @@
    9.37  qed "lift_set_UNIV_eq";
    9.38  Addsimps [lift_set_UNIV_eq];
    9.39  
    9.40 -Goal "Domain act <= drop_set i C ==> drop_act C i (lift_act i act) = act";
    9.41 +(*
    9.42 +Goal "Domain act <= drop_set i C ==> drop_act i (Restrict C (lift_act i act)) = act";
    9.43  by (asm_full_simp_tac
    9.44      (simpset() addsimps [drop_set_correct, drop_act_correct, 
    9.45  			 lift_act_correct, lift_export extend_act_inverse]) 1);
    9.46  qed "lift_act_inverse";
    9.47  Addsimps [lift_act_inverse];
    9.48 +*)
    9.49  
    9.50  Goal "UNIV <= drop_set i C ==> drop_prog C i (lift_prog i F) = F";
    9.51  by (asm_full_simp_tac
    9.52 @@ -314,9 +311,8 @@
    9.53  
    9.54  (*** Diff, needed for localTo ***)
    9.55  
    9.56 -Goal "[| (UN act:acts. Domain act) <= drop_set i C; \
    9.57 -\        Diff G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |]  \
    9.58 -\     ==> Diff (drop_prog C i G) acts : A co B";
    9.59 +Goal "[| Diff C G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |] \
    9.60 +\     ==> Diff (drop_set i C) (drop_prog C i G) acts : A co B";
    9.61  by (asm_full_simp_tac
    9.62      (simpset() addsimps [drop_set_correct, drop_prog_correct, 
    9.63  			 lift_set_correct, lift_act_correct, 
    9.64 @@ -324,27 +320,11 @@
    9.65  qed "Diff_drop_prog_constrains";
    9.66  
    9.67  Goalw [stable_def]
    9.68 -     "[| (UN act:acts. Domain act) <= drop_set i C; \
    9.69 -\        Diff G (lift_act i `` acts) : stable (lift_set i A) |]  \
    9.70 -\     ==> Diff (drop_prog C i G) acts : stable A";
    9.71 -by (etac Diff_drop_prog_constrains 1);
    9.72 -by (assume_tac 1);
    9.73 +     "[| Diff C G (lift_act i `` acts) : stable (lift_set i A) |]  \
    9.74 +\     ==> Diff (drop_set i C) (drop_prog C i G) acts : stable A";
    9.75 +by (blast_tac (claset() addIs [Diff_drop_prog_constrains]) 1);
    9.76  qed "Diff_drop_prog_stable";
    9.77  
    9.78 -Goalw [constrains_def, Diff_def]
    9.79 -     "Diff G acts : A co B  \
    9.80 -\     ==> Diff (lift_prog i G) (lift_act i `` acts) \
    9.81 -\         : (lift_set i A) co (lift_set i B)";
    9.82 -by Auto_tac;
    9.83 -by (Blast_tac 1);
    9.84 -qed "Diff_lift_prog_co";
    9.85 -
    9.86 -Goalw [stable_def]
    9.87 -     "Diff G acts : stable A  \
    9.88 -\     ==> Diff (lift_prog i G) (lift_act i `` acts) : stable (lift_set i A)";
    9.89 -by (etac Diff_lift_prog_co 1);
    9.90 -qed "Diff_lift_prog_stable";
    9.91 -
    9.92  
    9.93  (*** Weak safety primitives: Co, Stable ***)
    9.94  
    9.95 @@ -466,19 +446,19 @@
    9.96  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
    9.97  qed "lift_prog_guar_Increasing";
    9.98  
    9.99 -Goal "F : (v localTo G) guarantees increasing func  \
   9.100 -\     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
   9.101 +Goal "F : (v localTo[UNIV] G) guarantees increasing func  \
   9.102 +\     ==> lift_prog i F : (v o sub i) localTo[UNIV] (lift_prog i G)  \
   9.103  \                         guarantees increasing (func o sub i)";
   9.104  by (dtac (lift_export extend_localTo_guar_increasing) 1);
   9.105  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   9.106  qed "lift_prog_localTo_guar_increasing";
   9.107  
   9.108 -Goal "F : (v localTo G) guarantees Increasing func  \
   9.109 -\     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
   9.110 +Goal "F : (v LocalTo G) guarantees Increasing func  \
   9.111 +\     ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i G)  \
   9.112  \                         guarantees Increasing (func o sub i)";
   9.113 -by (dtac (lift_export extend_localTo_guar_Increasing) 1);
   9.114 +by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
   9.115  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   9.116 -qed "lift_prog_localTo_guar_Increasing";
   9.117 +qed "lift_prog_LocalTo_guar_Increasing";
   9.118  
   9.119  Goal "F : Always A guarantees Always B \
   9.120  \ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
    10.1 --- a/src/HOL/UNITY/Lift_prog.thy	Mon Oct 18 15:17:35 1999 +0200
    10.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Mon Oct 18 15:18:24 1999 +0200
    10.3 @@ -22,19 +22,19 @@
    10.4    lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
    10.5      "lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}"
    10.6  
    10.7 -  (*Argument C allows weak safety laws to be projected*)
    10.8 -  drop_act :: "[('a=>'b) set, 'a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
    10.9 -    "drop_act C i act == {(f i, f' i) | f f'. (f,f'): act & f: C}"
   10.10 +  drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
   10.11 +    "drop_act i act == {(f i, f' i) | f f'. (f,f'): act}"
   10.12  
   10.13    lift_prog :: "['a, 'b program] => ('a => 'b) program"
   10.14      "lift_prog i F ==
   10.15         mk_program (lift_set i (Init F),
   10.16  		   lift_act i `` Acts F)"
   10.17  
   10.18 +  (*Argument C allows weak safety laws to be projected*)
   10.19    drop_prog :: "[('a=>'b) set, 'a, ('a=>'b) program] => 'b program"
   10.20      "drop_prog C i F ==
   10.21         mk_program (drop_set i (Init F),
   10.22 -		   drop_act C i `` (Acts F))"
   10.23 +		   drop_act i `` Restrict C `` (Acts F))"
   10.24  
   10.25    (*simplifies the expression of specifications*)
   10.26    constdefs
    11.1 --- a/src/HOL/UNITY/Project.ML	Mon Oct 18 15:17:35 1999 +0200
    11.2 +++ b/src/HOL/UNITY/Project.ML	Mon Oct 18 15:18:24 1999 +0200
    11.3 @@ -12,7 +12,7 @@
    11.4  
    11.5  (** projection: monotonicity for safety **)
    11.6  
    11.7 -Goal "D <= C ==> project_act D h act <= project_act C h act";
    11.8 +Goal "D <= C ==> project_act h (Restrict D act) <= project_act h (Restrict C act)";
    11.9  by (auto_tac (claset(), simpset() addsimps [project_act_def]));
   11.10  qed "project_act_mono";
   11.11  
   11.12 @@ -35,8 +35,8 @@
   11.13  Goal "UNIV <= project_set h C \
   11.14  \     ==> project C h ((extend h F) Join G) = F Join (project C h G)";
   11.15  by (rtac program_equalityI 1);
   11.16 -by (asm_simp_tac (simpset() addsimps [image_Un, image_image,
   11.17 -			subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
   11.18 +by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN, image_UN,
   11.19 +			subset_UNIV RS subset_trans RS Restrict_triv]) 2);
   11.20  by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
   11.21  qed "project_extend_Join";
   11.22  
   11.23 @@ -231,61 +231,106 @@
   11.24  (*Opposite direction fails because Diff in the extended state may remove
   11.25    fewer actions, i.e. those that affect other state variables.*)
   11.26  
   11.27 -Goal "Diff (project C h G) (project_act C h `` acts) <= \
   11.28 -\         project C h (Diff G acts)";
   11.29 -by (auto_tac (claset(), simpset() addsimps [component_eq_subset, Diff_def,
   11.30 -					    UN_subset_iff]));
   11.31 +Goalw [project_set_def, project_act_def]
   11.32 +     "Restrict (project_set h C) (project_act h (Restrict C act)) = \
   11.33 +\     project_act h (Restrict C act)";
   11.34 +by (Blast_tac 1);
   11.35 +qed "Restrict_project_act";
   11.36 +
   11.37 +Goalw [project_set_def, project_act_def]
   11.38 +     "project_act h (Restrict C Id) = Restrict (project_set h C) Id";
   11.39 +by (Blast_tac 1);
   11.40 +qed "project_act_Restrict_Id";
   11.41 +
   11.42 +Goal
   11.43 +  "Diff(project_set h C)(project C h G)(project_act h `` Restrict C `` acts) \
   11.44 +\  <= project C h (Diff C G acts)";
   11.45 +by (simp_tac 
   11.46 +    (simpset() addsimps [component_eq_subset, Diff_def,
   11.47 +			 Restrict_project_act, project_act_Restrict_Id, 
   11.48 +			 image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
   11.49 +by (Force_tac 1);
   11.50  qed "Diff_project_project_component_project_Diff";
   11.51  
   11.52 -Goal "(UN act:acts. Domain act) <= project_set h C \
   11.53 -\     ==> Diff (project C h G) acts <= \
   11.54 -\         project C h (Diff G (extend_act h `` acts))";
   11.55 -by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def,
   11.56 -					   UN_subset_iff]) 1);
   11.57 -by (force_tac (claset() addSIs [image_diff_subset RS subsetD], 
   11.58 -	       simpset() addsimps [image_image_eq_UN]) 1);
   11.59 +Goal "Diff (project_set h C) (project C h G) acts <= \
   11.60 +\         project C h (Diff C G (extend_act h `` acts))";
   11.61 +by (rtac component_trans 1);
   11.62 +by (rtac Diff_project_project_component_project_Diff 2);
   11.63 +by (simp_tac 
   11.64 +    (simpset() addsimps [component_eq_subset, Diff_def,
   11.65 +			 Restrict_project_act, project_act_Restrict_Id, 
   11.66 +			 image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
   11.67 +by (Blast_tac 1);
   11.68  qed "Diff_project_component_project_Diff";
   11.69  
   11.70 -Goal
   11.71 -   "[| (UN act:acts. Domain act) <= project_set h C; \
   11.72 -\      Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) |]\
   11.73 -\   ==> Diff (project C h G) acts : A co B";
   11.74 -by (etac (Diff_project_component_project_Diff RS component_constrains) 1);
   11.75 +Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
   11.76 +\     ==> Diff (project_set h C) (project C h G) acts : A co B";
   11.77 +by (rtac (Diff_project_component_project_Diff RS component_constrains) 1);
   11.78  by (rtac (project_constrains RS iffD2) 1);
   11.79  by (ftac constrains_imp_subset 1);
   11.80 -by (Asm_full_simp_tac 1);
   11.81  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   11.82  qed "Diff_project_constrains";
   11.83  
   11.84  Goalw [stable_def]
   11.85 -     "[| (UN act:acts. Domain act) <= project_set h C; \
   11.86 -\        Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
   11.87 -\     ==> Diff (project C h G) acts : stable A";
   11.88 +     "Diff C G (extend_act h `` acts) : stable (extend_set h A) \
   11.89 +\     ==> Diff (project_set h C) (project C h G) acts : stable A";
   11.90  by (etac Diff_project_constrains 1);
   11.91 -by (assume_tac 1);
   11.92  qed "Diff_project_stable";
   11.93  
   11.94 +(** Some results for Diff, extend and project_set **)
   11.95 +
   11.96 +Goal "Diff C (extend h G) (extend_act h `` acts) \
   11.97 +\         : (extend_set h A) co (extend_set h B) \
   11.98 +\     ==> Diff (project_set h C) G acts : A co B";
   11.99 +br (Diff_project_set_component RS component_constrains) 1;
  11.100 +by (forward_tac [constrains_imp_subset] 1);
  11.101 +by (asm_full_simp_tac
  11.102 +    (simpset() addsimps [project_constrains, extend_set_strict_mono]) 1);
  11.103 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
  11.104 +qed "Diff_project_set_constrains_I";
  11.105 +
  11.106 +Goalw [stable_def]
  11.107 +     "Diff C (extend h G) (extend_act h `` acts) : stable (extend_set h A) \
  11.108 +\     ==> Diff (project_set h C) G acts : stable A";
  11.109 +by (asm_simp_tac (simpset() addsimps [Diff_project_set_constrains_I]) 1);
  11.110 +qed "Diff_project_set_stable_I";
  11.111 +
  11.112 +Goalw [LOCALTO_def]
  11.113 +     "extend h F : (v o f) localTo[C] extend h H \
  11.114 +\     ==> F : v localTo[project_set h C] H";
  11.115 +by Auto_tac;
  11.116 +br Diff_project_set_stable_I 1;
  11.117 +by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym]) 1);
  11.118 +qed "localTo_project_set_I";
  11.119 +
  11.120  (*Converse fails: even if the conclusion holds, H could modify (v o f) 
  11.121    simultaneously with other variables, and this action would not be 
  11.122    superseded by anything in (extend h G) *)
  11.123 -Goal "[| UNIV <= project_set h C;  H : (func o f) localTo extend h G |] \
  11.124 -\     ==> project C h H : func localTo G";
  11.125 +Goal "H : (v o f) localTo[C] extend h G \
  11.126 +\     ==> project C h H : v localTo[project_set h C] G";
  11.127  by (asm_full_simp_tac 
  11.128 -    (simpset() addsimps [localTo_def, 
  11.129 +    (simpset() addsimps [LOCALTO_def, 
  11.130  			 project_extend_Join RS sym,
  11.131 -			 subset_UNIV RS subset_trans RS Diff_project_stable,
  11.132 +			 Diff_project_stable,
  11.133  			 Collect_eq_extend_set RS sym]) 1);
  11.134  qed "project_localTo_lemma";
  11.135  
  11.136 -Goal "extend h F Join G : (v o f) localTo extend h H \
  11.137 -\     ==> F Join project UNIV h G : v localTo H";
  11.138 -by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
  11.139 -by (asm_simp_tac 
  11.140 -    (simpset() addsimps [project_set_UNIV RS project_localTo_lemma]) 1);
  11.141 +Goal "extend h F Join G : (v o f) localTo[C] extend h H \
  11.142 +\     ==> F Join project C h G : v localTo[project_set h C] H";
  11.143 +by (asm_full_simp_tac 
  11.144 +    (simpset() addsimps [Join_localTo, localTo_project_set_I,
  11.145 +			 project_localTo_lemma]) 1);
  11.146 +qed "gen_project_localTo_I";
  11.147 +
  11.148 +Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \
  11.149 +\     ==> F Join project UNIV h G : v localTo[UNIV] H";
  11.150 +bd gen_project_localTo_I 1;
  11.151 +by (Asm_full_simp_tac 1);
  11.152  qed "project_localTo_I";
  11.153  
  11.154  Goalw [projecting_def]
  11.155 -     "projecting (%G. UNIV) h F ((v o f) localTo extend h H) (v localTo H)";
  11.156 +     "projecting (%G. UNIV) h F \
  11.157 +\         ((v o f) localTo[UNIV] extend h H)  (v localTo[UNIV] H)";
  11.158  by (blast_tac (claset() addIs [project_localTo_I]) 1);
  11.159  qed "projecting_localTo";
  11.160  
  11.161 @@ -428,6 +473,13 @@
  11.162  				      Collect_eq_extend_set RS sym]) 1);
  11.163  qed "project_Increasing";
  11.164  
  11.165 +Goal "extend h F Join G : (v o f) LocalTo extend h H \
  11.166 +\     ==> F Join project (reachable (extend h F Join G)) h G : v LocalTo H";
  11.167 +by (asm_full_simp_tac 
  11.168 +    (simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
  11.169 +			 gen_project_localTo_I]) 1);
  11.170 +qed "project_LocalTo_I";
  11.171 +
  11.172  (** A lot of redundant theorems: all are proved to facilitate reasoning
  11.173      about guarantees. **)
  11.174  
  11.175 @@ -455,6 +507,12 @@
  11.176  by (blast_tac (claset() addIs [project_Increasing_I]) 1);
  11.177  qed "projecting_Increasing";
  11.178  
  11.179 +Goalw [projecting_def]
  11.180 +     "projecting (%G. reachable (extend h F Join G)) h F \
  11.181 +\         ((v o f) LocalTo extend h H)  (v LocalTo H)";
  11.182 +by (blast_tac (claset() addIs [project_LocalTo_I]) 1);
  11.183 +qed "projecting_LocalTo";
  11.184 +
  11.185  Goalw [extending_def]
  11.186       "extending (%G. reachable (extend h F Join G)) h F X' \
  11.187  \               (extend_set h A Co extend_set h B) (A Co B)";
  11.188 @@ -510,7 +568,7 @@
  11.189    being enabled for all possible values of the new variables.*)
  11.190  Goalw [transient_def]
  11.191       "[| project C h F : transient A;  \
  11.192 -\        ALL act: Acts F. project_act C h act ^^ A <= - A --> \
  11.193 +\        ALL act: Acts F. project_act h (Restrict C act) ^^ A <= - A --> \
  11.194  \                         Domain act <= C \
  11.195  \             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
  11.196  \     ==> F : transient (extend_set h A)";
  11.197 @@ -622,7 +680,8 @@
  11.198  \     extend h F : (extend h `` X) guarantees (extend h `` Y)";
  11.199  by (rtac guaranteesI 1);
  11.200  by Auto_tac;
  11.201 -by (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D, 
  11.202 +by (blast_tac (claset() addDs [project_set_UNIV RS equalityD2 RS 
  11.203 +			         extend_Join_eq_extend_D, 
  11.204  			       guaranteesD]) 1);
  11.205  qed "guarantees_imp_extend_guarantees";
  11.206  
  11.207 @@ -650,7 +709,7 @@
  11.208  Goal "[| F : X guarantees Y;  \
  11.209  \        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
  11.210  \        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
  11.211 -\                Disjoint (extend h F) G |] \
  11.212 +\                Disjoint UNIV (extend h F) G |] \
  11.213  \             ==> extend h F Join G : Y' |] \
  11.214  \     ==> extend h F : X' guarantees Y'";
  11.215  by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
  11.216 @@ -689,22 +748,22 @@
  11.217  by Auto_tac;
  11.218  qed "extend_guar_Increasing";
  11.219  
  11.220 -Goal "F : (v localTo G) guarantees increasing func  \
  11.221 -\     ==> extend h F : (v o f) localTo (extend h G)  \
  11.222 +Goal "F : (v localTo[UNIV] G) guarantees increasing func  \
  11.223 +\     ==> extend h F : (v o f) localTo[UNIV] (extend h G)  \
  11.224  \                      guarantees increasing (func o f)";
  11.225  by (etac project_guarantees 1);
  11.226  by (rtac extending_increasing 2);
  11.227  by (rtac projecting_localTo 1);
  11.228  qed "extend_localTo_guar_increasing";
  11.229  
  11.230 -Goal "F : (v localTo G) guarantees Increasing func  \
  11.231 -\     ==> extend h F : (v o f) localTo (extend h G)  \
  11.232 +Goal "F : (v LocalTo G) guarantees Increasing func  \
  11.233 +\     ==> extend h F : (v o f) LocalTo (extend h G)  \
  11.234  \                      guarantees Increasing (func o f)";
  11.235  by (etac project_guarantees 1);
  11.236  by (rtac extending_Increasing 2);
  11.237 -by (rtac projecting_localTo 1);
  11.238 +by (rtac projecting_LocalTo 1);
  11.239  by Auto_tac;
  11.240 -qed "extend_localTo_guar_Increasing";
  11.241 +qed "extend_LocalTo_guar_Increasing";
  11.242  
  11.243  Goal "F : Always A guarantees Always B \
  11.244  \ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
  11.245 @@ -729,8 +788,15 @@
  11.246  but it can fail if C removes some parts of an action of G.*)
  11.247  
  11.248  
  11.249 -Goal "[| G : f localTo extend h F; \
  11.250 -\        Disjoint (extend h F) G |] ==> project C h G : stable {x}";
  11.251 +Goal "[| G : v localTo[UNIV] F;  Disjoint UNIV F G |] ==> G : stable {s. v s = z}";
  11.252 +by (asm_full_simp_tac 
  11.253 +    (simpset() addsimps [LOCALTO_def, Diff_def, Disjoint_def,
  11.254 +			 stable_def, constrains_def]) 1);
  11.255 +by (Blast_tac 1);
  11.256 +qed "localTo_imp_stable";
  11.257 +
  11.258 +Goal "[| G : f localTo[UNIV] extend h F; \
  11.259 +\        Disjoint UNIV (extend h F) G |] ==> project C h G : stable {x}";
  11.260  by (asm_full_simp_tac
  11.261      (simpset() addsimps [localTo_imp_stable,
  11.262  			 extend_set_sing, project_stable_I]) 1);
  11.263 @@ -742,14 +808,9 @@
  11.264  				  stable_def, constrains_def]));
  11.265  qed "stable_sing_imp_not_transient";
  11.266  
  11.267 -by (auto_tac (claset(), 
  11.268 -	      simpset() addsimps [FP_def, transient_def,
  11.269 -				  stable_def, constrains_def]));
  11.270 -qed "stable_sing_imp_not_transient";
  11.271 -
  11.272  Goal "[| F Join project UNIV h G : A leadsTo B;    \
  11.273 -\        G : f localTo extend h F; \
  11.274 -\        Disjoint (extend h F) G |]  \
  11.275 +\        G : f localTo[UNIV] extend h F; \
  11.276 +\        Disjoint UNIV (extend h F) G |]  \
  11.277  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
  11.278  by (rtac project_UNIV_leadsTo_lemma 1);
  11.279  by (Clarify_tac 1);
  11.280 @@ -760,8 +821,8 @@
  11.281  qed "project_leadsTo_D";
  11.282  
  11.283  Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
  11.284 -\         G : f localTo extend h F; \
  11.285 -\         Disjoint (extend h F) G |]  \
  11.286 +\         G : f localTo[UNIV] extend h F; \
  11.287 +\         Disjoint UNIV (extend h F) G |]  \
  11.288  \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
  11.289  by (rtac (refl RS Join_project_LeadsTo) 1);
  11.290  by (Clarify_tac 1);
  11.291 @@ -773,7 +834,7 @@
  11.292  
  11.293  Goalw [extending_def]
  11.294       "extending (%G. UNIV) h F \
  11.295 -\                (f localTo extend h F) \
  11.296 +\                (f localTo[UNIV] extend h F) \
  11.297  \                (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
  11.298  by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
  11.299  			addIs [project_leadsTo_D]) 1);
  11.300 @@ -781,7 +842,7 @@
  11.301  
  11.302  Goalw [extending_def]
  11.303       "extending (%G. reachable (extend h F Join G)) h F \
  11.304 -\               (f localTo extend h F) \
  11.305 +\               (f localTo[UNIV] extend h F) \
  11.306  \               (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
  11.307  by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
  11.308  			addIs [project_LeadsTo_D]) 1);
  11.309 @@ -790,7 +851,7 @@
  11.310  (*STRONG precondition and postcondition*)
  11.311  Goal "F : (A co A') guarantees (B leadsTo B')  \
  11.312  \ ==> extend h F : ((extend_set h A) co (extend_set h A'))  \
  11.313 -\                   Int (f localTo (extend h F)) \
  11.314 +\                   Int (f localTo[UNIV] (extend h F)) \
  11.315  \                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
  11.316  by (etac project_guarantees 1);
  11.317  by (rtac (extending_leadsTo RS extending_weaken) 2);
  11.318 @@ -801,7 +862,7 @@
  11.319  (*WEAK precondition and postcondition*)
  11.320  Goal "F : (A Co A') guarantees (B LeadsTo B')  \
  11.321  \ ==> extend h F : ((extend_set h A) Co (extend_set h A'))  \
  11.322 -\                   Int (f localTo (extend h F)) \
  11.323 +\                   Int (f localTo[UNIV] (extend h F)) \
  11.324  \                  guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
  11.325  by (etac project_guarantees 1);
  11.326  by (rtac (extending_LeadsTo RS extending_weaken) 2);
    12.1 --- a/src/HOL/UNITY/Project.thy	Mon Oct 18 15:17:35 1999 +0200
    12.2 +++ b/src/HOL/UNITY/Project.thy	Mon Oct 18 15:18:24 1999 +0200
    12.3 @@ -20,7 +20,7 @@
    12.4  		 'c program set, 'c program set, 'a program set] => bool"
    12.5    "extending C h F X' Y' Y ==
    12.6       ALL G. F Join project (C G) h G : Y & extend h F Join G : X' &
    12.7 -            Disjoint (extend h F) G
    12.8 +            Disjoint UNIV (extend h F) G
    12.9              --> extend h F Join G : Y'"
   12.10  
   12.11  end
    13.1 --- a/src/HOL/UNITY/Union.ML	Mon Oct 18 15:17:35 1999 +0200
    13.2 +++ b/src/HOL/UNITY/Union.ML	Mon Oct 18 15:18:24 1999 +0200
    13.3 @@ -288,98 +288,122 @@
    13.4  
    13.5  (** Diff and localTo **)
    13.6  
    13.7 -Goalw [Diff_def] "F Join (Diff G (Acts F)) = F Join G";
    13.8 +Goalw [Diff_def] "F Join (Diff UNIV G (Acts F)) = F Join G";
    13.9  by (rtac program_equalityI 1);
   13.10  by Auto_tac;
   13.11  qed "Join_Diff2";
   13.12  
   13.13  Goalw [Diff_def]
   13.14 -     "Diff (F Join G) (Acts H) = (Diff F (Acts H)) Join (Diff G (Acts H))";
   13.15 +   "Diff C (F Join G) (Acts H) = (Diff C F (Acts H)) Join (Diff C G (Acts H))";
   13.16  by (rtac program_equalityI 1);
   13.17  by Auto_tac;
   13.18  qed "Diff_Join_distrib";
   13.19  
   13.20 -Goalw [Diff_def, constrains_def] "(Diff F (Acts F) : A co B) = (A <= B)";
   13.21 +Goalw [Diff_def] "Diff C F (Acts F) = mk_program(Init F, {})";
   13.22  by Auto_tac;
   13.23 -qed "Diff_self_constrains";
   13.24 +qed "Diff_self_eq";
   13.25  
   13.26 -Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
   13.27 -by Auto_tac;
   13.28 +Goalw [Diff_def, Disjoint_def] "Disjoint C F (Diff C G (Acts F))";
   13.29 +by (force_tac (claset(), 
   13.30 +	       simpset() addsimps [Restrict_imageI, 
   13.31 +				   sym RSN (2,Restrict_imageI)]) 1);
   13.32  qed "Diff_Disjoint";
   13.33  
   13.34 -Goal "[| G : v localTo F;  Disjoint F G |] ==> G : stable {s. v s = z}";
   13.35 -by (asm_full_simp_tac 
   13.36 -    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
   13.37 -			 stable_def, constrains_def]) 1);
   13.38 -by (Blast_tac 1);
   13.39 -qed "localTo_imp_stable";
   13.40 +Goalw [Disjoint_def]
   13.41 +     "[| A <= B; Disjoint A F G |] ==> Disjoint B F G";
   13.42 +by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
   13.43 +qed "Disjoint_mono";
   13.44 +
   13.45 +(*** localTo ***)
   13.46  
   13.47 -Goalw [localTo_def, stable_def, constrains_def]
   13.48 -     "v localTo F <= (f o v) localTo F";
   13.49 +Goalw [LOCALTO_def, Diff_def, stable_def, constrains_def]
   13.50 +     "A <= B ==> v localTo[B] F <= v localTo[A] F";
   13.51 +by Auto_tac;
   13.52 +by (dres_inst_tac [("x", "v xc")] spec 1);
   13.53 +by (dres_inst_tac [("x", "Restrict B xa")] bspec 1);
   13.54 +by Auto_tac;
   13.55 +by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
   13.56 +qed "localTo_anti_mono";
   13.57 +
   13.58 +Goalw [LocalTo_def]
   13.59 +     "G : v localTo[UNIV] F ==> G : v LocalTo F";
   13.60 +by (blast_tac (claset() addDs [impOfSubs localTo_anti_mono]) 1);
   13.61 +qed "localTo_imp_LocalTo";
   13.62 +
   13.63 +Goalw [LOCALTO_def, stable_def, constrains_def]
   13.64 +     "v localTo[C] F <= (f o v) localTo[C] F";
   13.65  by (Clarify_tac 1);
   13.66  by (force_tac (claset() addSEs [allE, ballE], simpset()) 1);
   13.67  qed "localTo_imp_o_localTo";
   13.68  
   13.69 -Goalw [localTo_def, stable_def, constrains_def]
   13.70 -     "(%s. x) localTo F = UNIV";
   13.71 +Goalw [LOCALTO_def, stable_def, constrains_def]
   13.72 +     "(%s. x) localTo[C] F = UNIV";
   13.73  by (Blast_tac 1);
   13.74  qed "triv_localTo_eq_UNIV";
   13.75  
   13.76 -Goal "(F Join G : v localTo H) = (F : v localTo H  &  G : v localTo H)";
   13.77 +Goal "(F Join G : v localTo[C] H) = (F : v localTo[C] H  &  G : v localTo[C] H)";
   13.78  by (asm_full_simp_tac 
   13.79 -    (simpset() addsimps [localTo_def, Diff_Join_distrib,
   13.80 +    (simpset() addsimps [LOCALTO_def, Diff_Join_distrib,
   13.81  			 stable_def, Join_constrains]) 1);
   13.82  by (Blast_tac 1);
   13.83  qed "Join_localTo";
   13.84  
   13.85 -Goal "F : v localTo F";
   13.86 +Goal "F : v localTo[C] F";
   13.87  by (simp_tac 
   13.88 -    (simpset() addsimps [localTo_def, stable_def, Diff_self_constrains]) 1);
   13.89 +    (simpset() addsimps [LOCALTO_def, stable_def, constrains_def, 
   13.90 +			 Diff_self_eq]) 1);
   13.91  qed "self_localTo";
   13.92  
   13.93  
   13.94  
   13.95  (*** Higher-level rules involving localTo and Join ***)
   13.96  
   13.97 -Goal "[| F : {s. P (v s)} co {s. P' (v s)};  G : v localTo F |]  \
   13.98 -\     ==> F Join G : {s. P (v s)} co {s. P' (v s)}";
   13.99 -by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
  13.100 +Goal "[| F : {s. P (v s)} co {s. P' (v s)};  G : v localTo[C] F |]  \
  13.101 +\     ==> G : C Int {s. P (v s)} co {s. P' (v s)}";
  13.102 +by (ftac constrains_imp_subset 1);
  13.103  by (auto_tac (claset(), 
  13.104 -	      simpset() addsimps [localTo_def, stable_def, constrains_def,
  13.105 +	      simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
  13.106  				  Diff_def]));
  13.107 -by (case_tac "act: Acts F" 1);
  13.108 -by (Blast_tac 1);
  13.109 -by (dtac bspec 1 THEN rtac Id_in_Acts 1);
  13.110 +by (case_tac "Restrict C act: Restrict C `` Acts F" 1);
  13.111 +by (blast_tac (claset() addSEs [equalityE]) 1);
  13.112  by (subgoal_tac "v x = v xa" 1);
  13.113 +by (Force_tac 1);
  13.114 +by (thin_tac "ALL act: ?A. ?P act" 1);
  13.115 +by (dtac spec 1);
  13.116 +by (dres_inst_tac [("x", "Restrict C act")] bspec 1);
  13.117  by Auto_tac;
  13.118  qed "constrains_localTo_constrains";
  13.119  
  13.120 -Goalw [localTo_def, stable_def, constrains_def, Diff_def]
  13.121 -     "[| G : v localTo F;  G : w localTo F |]  \
  13.122 -\     ==> G : (%s. (v s, w s)) localTo F";
  13.123 +Goalw [LOCALTO_def, stable_def, constrains_def, Diff_def]
  13.124 +     "[| G : v localTo[C] F;  G : w localTo[C] F |]  \
  13.125 +\     ==> G : (%s. (v s, w s)) localTo[C] F";
  13.126  by (Blast_tac 1);
  13.127  qed "localTo_pairfun";
  13.128  
  13.129  Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)};   \
  13.130 -\        G : v localTo F;       \
  13.131 -\        G : w localTo F |]               \
  13.132 -\     ==> F Join G : {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
  13.133 -by (res_inst_tac [("A", "{s. (%(x,y). P x y) (v s, w s)}"),
  13.134 +\        G : v localTo[C] F;       \
  13.135 +\        G : w localTo[C] F |]               \
  13.136 +\     ==> G : C Int {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
  13.137 +by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}"),
  13.138  		  ("A'", "{s. (%(x,y). P' x y) (v s, w s)}")] 
  13.139      constrains_weaken 1);
  13.140  by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
  13.141  by Auto_tac;
  13.142  qed "constrains_localTo_constrains2";
  13.143  
  13.144 +(*Used just once, in Client.ML.  Having F in the conclusion is silly.*)
  13.145  Goalw [stable_def]
  13.146       "[| F : stable {s. P (v s) (w s)};   \
  13.147 -\        G : v localTo F;  G : w localTo F |]               \
  13.148 +\        G : v localTo[UNIV] F;  G : w localTo[UNIV] F |]               \
  13.149  \     ==> F Join G : stable {s. P (v s) (w s)}";
  13.150 -by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1);
  13.151 +by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
  13.152 +by (blast_tac (claset() addIs [constrains_localTo_constrains2 RS 
  13.153 +			       constrains_weaken]) 1);
  13.154  qed "stable_localTo_stable2";
  13.155  
  13.156 +(*Used just in Client.ML.  Generalize to arbitrary C?*)
  13.157  Goal "[| F : stable {s. v s <= w s};   \
  13.158 -\        G : v localTo F;       \
  13.159 +\        G : v localTo[UNIV] F;       \
  13.160  \        F Join G : Increasing w |]               \
  13.161  \     ==> F Join G : Stable {s. v s <= w s}";
  13.162  by (auto_tac (claset(), 
  13.163 @@ -388,8 +412,8 @@
  13.164  by (blast_tac (claset() addIs [constrains_weaken]) 1);
  13.165  (*The G case remains; proved like constrains_localTo_constrains*)
  13.166  by (auto_tac (claset(), 
  13.167 -	      simpset() addsimps [localTo_def, stable_def, constrains_def,
  13.168 -				  Diff_def]));
  13.169 +              simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
  13.170 +                                  Diff_def]));
  13.171  by (case_tac "act: Acts F" 1);
  13.172  by (Blast_tac 1);
  13.173  by (thin_tac "ALL act:Acts F. ?P act" 1);
    14.1 --- a/src/HOL/UNITY/Union.thy	Mon Oct 18 15:17:35 1999 +0200
    14.2 +++ b/src/HOL/UNITY/Union.thy	Mon Oct 18 15:18:24 1999 +0200
    14.3 @@ -22,17 +22,25 @@
    14.4    SKIP :: 'a program
    14.5      "SKIP == mk_program (UNIV, {})"
    14.6  
    14.7 -  Diff :: "['a program, ('a * 'a)set set] => 'a program"
    14.8 -    "Diff F acts == mk_program (Init F, Acts F - acts)"
    14.9 +  Diff :: "['a set, 'a program, ('a * 'a)set set] => 'a program"
   14.10 +    "Diff C G acts ==
   14.11 +       mk_program (Init G, (Restrict C `` Acts G) - (Restrict C `` acts))"
   14.12  
   14.13    (*The set of systems that regard "v" as local to F*)
   14.14 -  localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
   14.15 -    "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
   14.16 +  LOCALTO :: ['a => 'b, 'a set, 'a program] => 'a program set
   14.17 +                                           ("(_/ localTo[_]/ _)" [80,0,80] 80)
   14.18 +    "v localTo[C] F == {G. ALL z. Diff C G (Acts F) : stable {s. v s = z}}"
   14.19 +
   14.20 +  (*The weak version of localTo, considering only G's reachable states*)
   14.21 +  LocalTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
   14.22 +    "v LocalTo F == {G. G : v localTo[reachable G] F}"
   14.23  
   14.24    (*Two programs with disjoint actions, except for identity actions.
   14.25      It's a weak property but still useful.*)
   14.26 -  Disjoint :: ['a program, 'a program] => bool
   14.27 -    "Disjoint F G == Acts F Int Acts G <= {Id}"
   14.28 +  Disjoint :: ['a set, 'a program, 'a program] => bool
   14.29 +    "Disjoint C F G ==
   14.30 +       (Restrict C `` (Acts F - {Id})) Int (Restrict C `` (Acts G - {Id}))
   14.31 +       <= {}"
   14.32  
   14.33  syntax
   14.34    "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)