ALMOST working version: LocalTo results commented out
authorpaulson
Fri Oct 22 18:35:20 1999 +0200 (1999-10-22)
changeset 7915c7fd7eb3b0ef
parent 7914 5bfde29f1dbb
child 7916 3cb310f40a3a
ALMOST working version: LocalTo results commented out
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/LessThan.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Project.ML
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Fri Oct 22 18:33:39 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Fri Oct 22 18:35:20 1999 +0200
     1.3 @@ -388,7 +388,7 @@
     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[UNIV] (lift_prog i Client)) \
     1.8 +\  : Increasing (giv o sub i) Int ((%z. z i) LocalTo (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}  \
     2.1 --- a/src/HOL/UNITY/Comp.ML	Fri Oct 22 18:33:39 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Comp.ML	Fri Oct 22 18:35:20 1999 +0200
     2.3 @@ -48,6 +48,14 @@
     2.4  by (Blast_tac 1);
     2.5  qed "component_Join2";
     2.6  
     2.7 +Goal "F<=G ==> F Join G = G";
     2.8 +by (auto_tac (claset(), simpset() addsimps [component_def, Join_left_absorb]));
     2.9 +qed "Join_absorb1";
    2.10 +
    2.11 +Goal "G<=F ==> F Join G = F";
    2.12 +by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
    2.13 +qed "Join_absorb2";
    2.14 +
    2.15  Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
    2.16  by (blast_tac (claset() addIs [JN_absorb]) 1);
    2.17  qed "component_JN";
     3.1 --- a/src/HOL/UNITY/Extend.ML	Fri Oct 22 18:33:39 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Extend.ML	Fri Oct 22 18:35:20 1999 +0200
     3.3 @@ -8,17 +8,6 @@
     3.4    function g (forgotten) maps the extended state to the "extending part"
     3.5  *)
     3.6  
     3.7 -
     3.8 -
     3.9 -		Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
    3.10 -		by  (Blast_tac 1);
    3.11 -		qed "disjoint_iff_not_equal";
    3.12 -
    3.13 -		Goal "ff -`` (ff `` A) = {y. EX x:A. ff x = ff y}";
    3.14 -		by (blast_tac (claset() addIs [sym]) 1);
    3.15 -		qed "vimage_image_eq";
    3.16 -
    3.17 -
    3.18  (** These we prove OUTSIDE the locale. **)
    3.19  
    3.20  (*Possibly easier than reasoning about "inv h"*)
    3.21 @@ -277,7 +266,7 @@
    3.22  qed "project_act_Id";
    3.23  
    3.24  Goalw [project_set_def, project_act_def]
    3.25 -  "Domain (project_act h (Restrict C act)) = project_set h (Domain act Int C)";
    3.26 +  "Domain (project_act h act) = project_set h (Domain act)";
    3.27  by (force_tac (claset(), 
    3.28                simpset() addsimps [split_extended_all]) 1);
    3.29  qed "Domain_project_act";
    3.30 @@ -330,14 +319,19 @@
    3.31  qed "project_set_UNIV";
    3.32  Addsimps [project_set_UNIV];
    3.33  
    3.34 +Goal "project h C (extend h F) = \
    3.35 +\     mk_program (Init F, Restrict (project_set h C) `` Acts F)";
    3.36 +by (rtac program_equalityI 1);
    3.37 +by (asm_simp_tac (simpset() addsimps [image_eq_UN, 
    3.38 +                   project_act_extend_act_restrict]) 2);
    3.39 +by (Simp_tac 1);
    3.40 +qed "project_extend_eq";
    3.41 +
    3.42  (*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
    3.43  Goal "UNIV <= project_set h C \
    3.44  \     ==> project h C (extend h F) = F";
    3.45 -by (simp_tac (simpset() addsimps [extend_def, project_def]) 1);
    3.46 -by (rtac program_equalityI 1);
    3.47 -by (asm_simp_tac (simpset() addsimps [image_image_eq_UN, image_UN, 
    3.48 -                   subset_UNIV RS subset_trans RS Restrict_triv]) 2);
    3.49 -by (Simp_tac 1);
    3.50 +by (asm_simp_tac (simpset() addsimps [project_extend_eq, image_eq_UN, 
    3.51 +                   subset_UNIV RS subset_trans RS Restrict_triv]) 1);
    3.52  qed "extend_inverse";
    3.53  Addsimps [extend_inverse];
    3.54  
    3.55 @@ -409,12 +403,14 @@
    3.56                simpset() addsimps [extend_act_def]));
    3.57  qed "Restrict_extend_set";
    3.58  
    3.59 -Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts)) = \
    3.60 +Goalw [Diff_def]
    3.61 +     "(Diff (extend_set h C) (extend h G) (extend_act h `` acts)) = \
    3.62  \     extend h (Diff C G acts)";
    3.63 -by (auto_tac (claset() addSIs [program_equalityI],
    3.64 -	      simpset() addsimps [Diff_def, image_image_eq_UN,
    3.65 -				  Restrict_extend_set,
    3.66 -				  inj_extend_act RS image_set_diff]));
    3.67 +by (rtac program_equalityI 1);
    3.68 +by (Simp_tac 1);
    3.69 +by (simp_tac (simpset() addsimps [inj_extend_act RS image_set_diff]) 1);
    3.70 +by (simp_tac (simpset() addsimps [image_eq_UN,
    3.71 +				  Restrict_extend_set]) 1);
    3.72  qed "Diff_extend_eq";
    3.73  
    3.74  (*Opposite inclusion fails; this inclusion's more general than that of
     4.1 --- a/src/HOL/UNITY/LessThan.ML	Fri Oct 22 18:33:39 1999 +0200
     4.2 +++ b/src/HOL/UNITY/LessThan.ML	Fri Oct 22 18:35:20 1999 +0200
     4.3 @@ -61,6 +61,17 @@
     4.4  by (Blast_tac 1);
     4.5  qed "image_Diff_image_eq";
     4.6  
     4.7 +Goal "Domain (Restrict A r) = A Int Domain r";
     4.8 +by (Blast_tac 1);
     4.9 +qed "Domain_Restrict";
    4.10 +
    4.11 +Goal "(Restrict A r) ^^ B = r ^^ (A Int B)";
    4.12 +by (Blast_tac 1);
    4.13 +qed "Image_Restrict";
    4.14 +
    4.15 +Addsimps [Domain_Restrict, Image_Restrict];
    4.16 +
    4.17 +
    4.18  
    4.19  (*** lessThan ***)
    4.20  
     5.1 --- a/src/HOL/UNITY/Lift_prog.ML	Fri Oct 22 18:33:39 1999 +0200
     5.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Fri Oct 22 18:35:20 1999 +0200
     5.3 @@ -453,12 +453,14 @@
     5.4  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
     5.5  qed "lift_prog_localTo_guar_increasing";
     5.6  
     5.7 +(***
     5.8  Goal "F : (v LocalTo G) guarantees Increasing func  \
     5.9  \     ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i G)  \
    5.10  \                         guarantees Increasing (func o sub i)";
    5.11  by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
    5.12  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
    5.13  qed "lift_prog_LocalTo_guar_Increasing";
    5.14 +***)
    5.15  
    5.16  Goal "F : Always A guarantees Always B \
    5.17  \ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
     6.1 --- a/src/HOL/UNITY/Project.ML	Fri Oct 22 18:33:39 1999 +0200
     6.2 +++ b/src/HOL/UNITY/Project.ML	Fri Oct 22 18:35:20 1999 +0200
     6.3 @@ -35,7 +35,7 @@
     6.4  Goal "UNIV <= project_set h C \
     6.5  \     ==> project h C ((extend h F) Join G) = F Join (project h C G)";
     6.6  by (rtac program_equalityI 1);
     6.7 -by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN, image_UN,
     6.8 +by (asm_simp_tac (simpset() addsimps [image_eq_UN, UN_Un,
     6.9  			subset_UNIV RS subset_trans RS Restrict_triv]) 2);
    6.10  by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
    6.11  qed "project_extend_Join";
    6.12 @@ -247,9 +247,9 @@
    6.13  \  <= project h C (Diff C G acts)";
    6.14  by (simp_tac 
    6.15      (simpset() addsimps [component_eq_subset, Diff_def,
    6.16 -			 Restrict_project_act, project_act_Restrict_Id, 
    6.17 -			 image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
    6.18 -by (Force_tac 1);
    6.19 +			 project_act_Restrict_Id, Restrict_image_Diff]) 1);
    6.20 +by (force_tac (claset() delrules [equalityI], 
    6.21 +	       simpset() addsimps [Restrict_project_act, image_eq_UN]) 1);
    6.22  qed "Diff_project_project_component_project_Diff";
    6.23  
    6.24  Goal "Diff (project_set h C) (project h C G) acts <= \
    6.25 @@ -259,8 +259,7 @@
    6.26  by (simp_tac 
    6.27      (simpset() addsimps [component_eq_subset, Diff_def,
    6.28  			 Restrict_project_act, project_act_Restrict_Id, 
    6.29 -			 image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
    6.30 -by (Blast_tac 1);
    6.31 +			 image_eq_UN, Restrict_image_Diff]) 1);
    6.32  qed "Diff_project_component_project_Diff";
    6.33  
    6.34  Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
    6.35 @@ -282,8 +281,8 @@
    6.36  Goal "Diff C (extend h G) (extend_act h `` acts) \
    6.37  \         : (extend_set h A) co (extend_set h B) \
    6.38  \     ==> Diff (project_set h C) G acts : A co B";
    6.39 -br (Diff_project_set_component RS component_constrains) 1;
    6.40 -by (forward_tac [constrains_imp_subset] 1);
    6.41 +by (rtac (Diff_project_set_component RS component_constrains) 1);
    6.42 +by (ftac constrains_imp_subset 1);
    6.43  by (asm_full_simp_tac
    6.44      (simpset() addsimps [project_constrains, extend_set_strict_mono]) 1);
    6.45  by (blast_tac (claset() addIs [constrains_weaken]) 1);
    6.46 @@ -299,7 +298,7 @@
    6.47       "extend h F : (v o f) localTo[C] extend h H \
    6.48  \     ==> F : v localTo[project_set h C] H";
    6.49  by Auto_tac;
    6.50 -br Diff_project_set_stable_I 1;
    6.51 +by (rtac Diff_project_set_stable_I 1);
    6.52  by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym]) 1);
    6.53  qed "localTo_project_set_I";
    6.54  
    6.55 @@ -324,7 +323,7 @@
    6.56  
    6.57  Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \
    6.58  \     ==> F Join project h UNIV G : v localTo[UNIV] H";
    6.59 -bd gen_project_localTo_I 1;
    6.60 +by (dtac gen_project_localTo_I 1);
    6.61  by (Asm_full_simp_tac 1);
    6.62  qed "project_localTo_I";
    6.63  
    6.64 @@ -473,12 +472,16 @@
    6.65  				      Collect_eq_extend_set RS sym]) 1);
    6.66  qed "project_Increasing";
    6.67  
    6.68 +(**
    6.69  Goal "extend h F Join G : (v o f) LocalTo extend h H \
    6.70  \     ==> F Join project h (reachable (extend h F Join G)) G : v LocalTo H";
    6.71  by (asm_full_simp_tac 
    6.72      (simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
    6.73 -			 gen_project_localTo_I]) 1);
    6.74 +			 gen_project_localTo_I,
    6.75 +			 Join_assoc RS sym]) 1);
    6.76 +
    6.77  qed "project_LocalTo_I";
    6.78 +**)
    6.79  
    6.80  (** A lot of redundant theorems: all are proved to facilitate reasoning
    6.81      about guarantees. **)
    6.82 @@ -507,11 +510,13 @@
    6.83  by (blast_tac (claset() addIs [project_Increasing_I]) 1);
    6.84  qed "projecting_Increasing";
    6.85  
    6.86 +(**
    6.87  Goalw [projecting_def]
    6.88       "projecting (%G. reachable (extend h F Join G)) h F \
    6.89 -\         ((v o f) LocalTo extend h H)  (v LocalTo H)";
    6.90 +\                ((v o f) LocalTo extend h H) (v LocalTo H)";
    6.91  by (blast_tac (claset() addIs [project_LocalTo_I]) 1);
    6.92  qed "projecting_LocalTo";
    6.93 +**)
    6.94  
    6.95  Goalw [extending_def]
    6.96       "extending (%G. reachable (extend h F Join G)) h F X' \
    6.97 @@ -554,7 +559,7 @@
    6.98  \        F : transient (extend_set h A) |] \
    6.99  \     ==> project h C F : transient A";
   6.100  by (auto_tac (claset() delrules [ballE],
   6.101 -              simpset() addsimps [Domain_project_act, Int_absorb2]));
   6.102 +              simpset() addsimps [Domain_project_act, Int_absorb1]));
   6.103  by (REPEAT (ball_tac 1));
   6.104  by (auto_tac (claset(),
   6.105                simpset() addsimps [extend_set_def, project_set_def, 
   6.106 @@ -579,7 +584,7 @@
   6.107  by (assume_tac 2);
   6.108  by Auto_tac;
   6.109  by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1);
   6.110 -by (force_tac (claset(), simpset() addsimps [Int_absorb2]) 1);
   6.111 +by (force_tac (claset(), simpset() addsimps [Int_absorb1]) 1);
   6.112  (*The Domain requirement's proved; must prove the Image requirement*)
   6.113  by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
   6.114  by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
   6.115 @@ -756,6 +761,7 @@
   6.116  by (rtac projecting_localTo 1);
   6.117  qed "extend_localTo_guar_increasing";
   6.118  
   6.119 +(**
   6.120  Goal "F : (v LocalTo G) guarantees Increasing func  \
   6.121  \     ==> extend h F : (v o f) LocalTo (extend h G)  \
   6.122  \                      guarantees Increasing (func o f)";
   6.123 @@ -764,6 +770,7 @@
   6.124  by (rtac projecting_LocalTo 1);
   6.125  by Auto_tac;
   6.126  qed "extend_LocalTo_guar_Increasing";
   6.127 +**)
   6.128  
   6.129  Goal "F : Always A guarantees Always B \
   6.130  \ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
   6.131 @@ -775,61 +782,45 @@
   6.132  
   6.133  (** Guarantees with a leadsTo postcondition **)
   6.134  
   6.135 -(*Bridges the gap between the "old" and "new" condition of the leadsTo rules*)
   6.136 -Goal "[| ALL x. project h C G ~: transient {x}; project h C G: transient D |] \
   6.137 +Goalw [LOCALTO_def, transient_def, Diff_def]
   6.138 +     "[| G : f localTo[C] extend h F;  project h C G : transient D |]    \
   6.139  \     ==> F : transient D";
   6.140 +by Auto_tac;
   6.141 +by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
   6.142 +by Auto_tac; 
   6.143 +by (rtac bexI 1);
   6.144 +by (assume_tac 2);
   6.145 +by (Blast_tac 1);
   6.146  by (case_tac "D={}" 1);
   6.147 -by (auto_tac (claset() addIs [transient_strengthen], simpset()));
   6.148 -qed "transient_lemma";
   6.149 -
   6.150 -
   6.151 -(*Previously tried to prove
   6.152 -[| G : f localTo extend h F; project h C G : transient D |] ==> F : transient D
   6.153 -but it can fail if C removes some parts of an action of G.*)
   6.154 -
   6.155 -
   6.156 -Goal "[| G : v localTo[UNIV] F;  Disjoint UNIV F G |] ==> G : stable {s. v s = z}";
   6.157 -by (asm_full_simp_tac 
   6.158 -    (simpset() addsimps [LOCALTO_def, Diff_def, Disjoint_def,
   6.159 -			 stable_def, constrains_def]) 1);
   6.160  by (Blast_tac 1);
   6.161 -qed "localTo_imp_stable";
   6.162 -
   6.163 -Goal "[| G : f localTo[UNIV] extend h F; \
   6.164 -\        Disjoint UNIV (extend h F) G |] ==> project h C G : stable {x}";
   6.165 -by (asm_full_simp_tac
   6.166 -    (simpset() addsimps [localTo_imp_stable,
   6.167 -			 extend_set_sing, project_stable_I]) 1);
   6.168 -qed "localTo_imp_project_stable";
   6.169 -
   6.170 -Goal "F : stable{s} ==> F ~: transient {s}";
   6.171 -by (auto_tac (claset(), 
   6.172 -	      simpset() addsimps [FP_def, transient_def,
   6.173 -				  stable_def, constrains_def]));
   6.174 -qed "stable_sing_imp_not_transient";
   6.175 +by (auto_tac (claset(),
   6.176 +	      simpset() addsimps [stable_def, constrains_def]));
   6.177 +by (subgoal_tac "ALL z. Restrict C act ^^ {s. f s = z} <= {s. f s = z}" 1);
   6.178 +by (blast_tac (claset() addSDs [bspec]) 2);
   6.179 +by (thin_tac "ALL z. ?P z" 1);
   6.180 +by (subgoal_tac "project_act h (Restrict C act) ^^ D <= D" 1);
   6.181 +by (Clarify_tac 2);
   6.182 +by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
   6.183 +by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 2);
   6.184 +by (blast_tac (claset() addSDs [subsetD]) 1);
   6.185 +qed "localTo_project_transient_transient";
   6.186  
   6.187  Goal "[| F Join project h UNIV G : A leadsTo B;    \
   6.188 -\        G : f localTo[UNIV] extend h F; \
   6.189 -\        Disjoint UNIV (extend h F) G |]  \
   6.190 +\        G : f localTo[UNIV] extend h F |]  \
   6.191  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   6.192  by (rtac project_UNIV_leadsTo_lemma 1);
   6.193 -by (Clarify_tac 1);
   6.194 -by (rtac transient_lemma 1);
   6.195  by (auto_tac (claset(), 
   6.196 -	      simpset() addsimps [localTo_imp_project_stable, 
   6.197 -				  stable_sing_imp_not_transient]));
   6.198 +         simpset() addsimps [impOfSubs (subset_UNIV RS localTo_anti_mono) RS
   6.199 +			     localTo_project_transient_transient]));
   6.200  qed "project_leadsTo_D";
   6.201  
   6.202  Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
   6.203 -\         G : f localTo[UNIV] extend h F; \
   6.204 -\         Disjoint UNIV (extend h F) G |]  \
   6.205 +\         G : f LocalTo extend h F |]  \
   6.206  \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
   6.207  by (rtac (refl RS Join_project_LeadsTo) 1);
   6.208 -by (Clarify_tac 1);
   6.209 -by (rtac transient_lemma 1);
   6.210  by (auto_tac (claset(), 
   6.211 -	      simpset() addsimps [localTo_imp_project_stable, 
   6.212 -				  stable_sing_imp_not_transient]));
   6.213 +	      simpset() addsimps [LocalTo_def,
   6.214 +				  localTo_project_transient_transient]));
   6.215  qed "project_LeadsTo_D";
   6.216  
   6.217  Goalw [extending_def]
   6.218 @@ -842,10 +833,11 @@
   6.219  
   6.220  Goalw [extending_def]
   6.221       "extending (%G. reachable (extend h F Join G)) h F \
   6.222 -\               (f localTo[UNIV] extend h F) \
   6.223 +\               (f LocalTo extend h F) \
   6.224  \               (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
   6.225 -by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
   6.226 -			addIs [project_LeadsTo_D]) 1);
   6.227 +by (force_tac (claset() addIs [project_LeadsTo_D],
   6.228 +	       simpset()addsimps [LocalTo_def, Join_assoc RS sym, 
   6.229 +				  Join_localTo]) 1);
   6.230  qed "extending_LeadsTo";
   6.231  
   6.232  (*STRONG precondition and postcondition*)
   6.233 @@ -862,7 +854,7 @@
   6.234  (*WEAK precondition and postcondition*)
   6.235  Goal "F : (A Co A') guarantees (B LeadsTo B')  \
   6.236  \ ==> extend h F : ((extend_set h A) Co (extend_set h A'))  \
   6.237 -\                   Int (f localTo[UNIV] (extend h F)) \
   6.238 +\                   Int (f LocalTo (extend h F)) \
   6.239  \                  guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
   6.240  by (etac project_guarantees 1);
   6.241  by (rtac (extending_LeadsTo RS extending_weaken) 2);
     7.1 --- a/src/HOL/UNITY/UNITY.ML	Fri Oct 22 18:33:39 1999 +0200
     7.2 +++ b/src/HOL/UNITY/UNITY.ML	Fri Oct 22 18:35:20 1999 +0200
     7.3 @@ -62,14 +62,17 @@
     7.4  
     7.5  (** The notation of equality for type "program" **)
     7.6  
     7.7 -Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
     7.8 -by (subgoals_tac ["EX x. Rep_Program F = x",
     7.9 -		  "EX x. Rep_Program G = x"] 1);
    7.10 -by (REPEAT (Blast_tac 2));
    7.11 -by (Clarify_tac 1);
    7.12 +
    7.13 +Goal "mk_program (Init F, Acts F) = F";
    7.14 +by (cut_inst_tac [("x", "F")] Rep_Program 1);
    7.15  by (auto_tac (claset(), rep_ss));
    7.16  by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
    7.17 -by (asm_full_simp_tac rep_ss 1);
    7.18 +by (asm_full_simp_tac (rep_ss addsimps [insert_absorb]) 1);
    7.19 +qed "surjective_mk_program";
    7.20 +
    7.21 +Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
    7.22 +by (stac (surjective_mk_program RS sym) 1);
    7.23 +by (stac (surjective_mk_program RS sym) 1 THEN Force_tac 1);
    7.24  qed "program_equalityI";
    7.25  
    7.26  val [major,minor] =
    7.27 @@ -78,6 +81,8 @@
    7.28  by (auto_tac (claset(), simpset() addsimps [major]));
    7.29  qed "program_equalityE";
    7.30  
    7.31 +Addsimps [surjective_mk_program];
    7.32 +
    7.33  
    7.34  (*** These rules allow "lazy" definition expansion 
    7.35       They avoid expanding the full program, which is a large expression
     8.1 --- a/src/HOL/UNITY/Union.ML	Fri Oct 22 18:33:39 1999 +0200
     8.2 +++ b/src/HOL/UNITY/Union.ML	Fri Oct 22 18:35:20 1999 +0200
     8.3 @@ -126,7 +126,7 @@
     8.4  
     8.5  Addsimps [Join_absorb];
     8.6  
     8.7 -Goalw [Join_def] "A Join (A Join B) = A Join B";
     8.8 +Goalw [Join_def] "F Join (F Join G) = F Join G";
     8.9  by (rtac program_equalityI 1);
    8.10  by Auto_tac;
    8.11  qed "Join_left_absorb";
    8.12 @@ -336,15 +336,16 @@
    8.13  by (force_tac (claset() addSEs [allE, ballE], simpset()) 1);
    8.14  qed "localTo_imp_o_localTo";
    8.15  
    8.16 +(*NOT USED*)
    8.17  Goalw [LOCALTO_def, stable_def, constrains_def]
    8.18       "(%s. x) localTo[C] F = UNIV";
    8.19  by (Blast_tac 1);
    8.20  qed "triv_localTo_eq_UNIV";
    8.21  
    8.22 -Goal "(F Join G : v localTo[C] H) = (F : v localTo[C] H  &  G : v localTo[C] H)";
    8.23 -by (asm_full_simp_tac 
    8.24 -    (simpset() addsimps [LOCALTO_def, Diff_Join_distrib,
    8.25 -			 stable_def, Join_constrains]) 1);
    8.26 +Goal "(F Join G : v localTo[C] H) = \
    8.27 +\     (F : v localTo[C] H  &  G : v localTo[C] H)";
    8.28 +by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_Join_distrib,
    8.29 +				  stable_def, Join_constrains]) 1);
    8.30  by (Blast_tac 1);
    8.31  qed "Join_localTo";
    8.32  
     9.1 --- a/src/HOL/UNITY/Union.thy	Fri Oct 22 18:33:39 1999 +0200
     9.2 +++ b/src/HOL/UNITY/Union.thy	Fri Oct 22 18:35:20 1999 +0200
     9.3 @@ -33,7 +33,7 @@
     9.4  
     9.5    (*The weak version of localTo, considering only G's reachable states*)
     9.6    LocalTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
     9.7 -    "v LocalTo F == {G. G : v localTo[reachable G] F}"
     9.8 +    "v LocalTo F == {G. G : v localTo[reachable (F Join G)] F}"
     9.9  
    9.10    (*Two programs with disjoint actions, except for identity actions.
    9.11      It's a weak property but still useful.*)