working again; new treatment of LocalTo
authorpaulson
Wed Oct 27 13:03:32 1999 +0200 (1999-10-27)
changeset 7947b999c1ab9327
parent 7946 95e1de322e82
child 7948 61102e8cbe3c
working again; new treatment of LocalTo
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/PPROD.ML
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	Wed Oct 27 13:02:23 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Wed Oct 27 13:03:32 1999 +0200
     1.3 @@ -402,8 +402,35 @@
     1.4  by (auto_tac (claset(), simpset() addsimps [o_def]));
     1.5  qed "Client_i_Progress";
     1.6  
     1.7 +Goal "extend sysOfAlloc F \
     1.8 +\       : (v o client) localTo[C] extend sysOfClient (lift_prog i Client)";
     1.9 +br localTo_UNIV_imp_localTo 1;
    1.10 +by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def, 
    1.11 +				  stable_def, constrains_def,
    1.12 +				  image_eq_UN, extend_act_def,
    1.13 +				  sysOfAlloc_def, sysOfClient_def]) 1);
    1.14 +by (Force_tac 1);
    1.15 +qed "sysOfAlloc_in_client_localTo_xl_Client";
    1.16 +
    1.17 +Goal "extend sysOfClient (plam x: I. Client) : ((%z. z i) o client) \
    1.18 +\     localTo[C] extend sysOfClient (lift_prog i Client)";
    1.19 +br localTo_UNIV_imp_localTo 1;
    1.20 +by (rtac (client_export (extend_set_UNIV_eq RS equalityD2 RSN
    1.21 +			 (2, extend_localTo_extend_I))) 1);
    1.22 +br (rewrite_rule [sub_def] PLam_sub_localTo) 1;
    1.23 +qed "sysOfClient_in_client_localTo_xl_Client";
    1.24 +
    1.25  xxxxxxxxxxxxxxxx;
    1.26  
    1.27 +THIS PROOF requires an extra locality specification for Network:
    1.28 +    Network : rel o sub i o client localTo[C] 
    1.29 +                     extend sysOfClient (lift_prog i Client)
    1.30 +and similarly for ask o sub i o client.
    1.31 +
    1.32 +The LeadsTo rule must be refined so as not to require the whole of client to
    1.33 +be local, since giv is written by the Network.
    1.34 +
    1.35 +
    1.36  Goalw [System_def]
    1.37       "i < Nclients \
    1.38  \ ==> System : (INT h. {s. h <=  (giv o sub i o client) s & \
    1.39 @@ -411,17 +438,23 @@
    1.40  \            LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
    1.41  by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
    1.42  by (rtac (guarantees_PLam_I RS project_guarantees) 1);
    1.43 -by (rtac Client_i_Progress  1);
    1.44 +by (rtac Client_i_Progress 1);
    1.45  by (Force_tac 1);
    1.46  by (rtac (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
    1.47  by (rtac subset_refl 4);
    1.48  by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
    1.49 -by (rtac projecting_Int 1);
    1.50 -by (rtac (client_export projecting_Increasing) 1);
    1.51 -by (rtac (client_export projecting_localTo) 1);
    1.52 +(*The next step goes wrong: it makes an impossible localTo subgoal*)
    1.53 +(*blast_tac doesn't use HO unification*)
    1.54 +by (fast_tac (claset() addIs [projecting_Int,
    1.55 +			      client_export projecting_Increasing,
    1.56 +			      component_PLam,
    1.57 +			      client_export projecting_LocalTo]) 1);
    1.58 +by (asm_simp_tac
    1.59 +    (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
    1.60 +			 LocalTo_def, Join_localTo,
    1.61 +			 sysOfClient_in_client_localTo_xl_Client,
    1.62 +			 sysOfAlloc_in_client_localTo_xl_Client]) 2);
    1.63 +auto();
    1.64  
    1.65 -by (simp_tac (simpset()addsimps [lift_prog_correct]) 1);
    1.66  
    1.67 -by (rtac (client_export ) 1);
    1.68  
    1.69 -Client_Progress;
     2.1 --- a/src/HOL/UNITY/Comp.ML	Wed Oct 27 13:02:23 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Comp.ML	Wed Oct 27 13:03:32 1999 +0200
     2.3 @@ -56,6 +56,11 @@
     2.4  by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
     2.5  qed "Join_absorb2";
     2.6  
     2.7 +Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
     2.8 +by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
     2.9 +by (Blast_tac 1);
    2.10 +qed "JN_component_iff";
    2.11 +
    2.12  Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
    2.13  by (blast_tac (claset() addIs [JN_absorb]) 1);
    2.14  qed "component_JN";
    2.15 @@ -84,4 +89,19 @@
    2.16  	      simpset() addsimps [constrains_def, component_eq_subset]));
    2.17  qed "component_constrains";
    2.18  
    2.19 +(*Used in Guar.thy to show that programs are partially ordered*)
    2.20  bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
    2.21 +
    2.22 +Goal "F' <= F ==> Diff C G (Acts F) <= Diff C G (Acts F')";
    2.23 +by (auto_tac (claset(), simpset() addsimps [Diff_def, component_eq_subset]));
    2.24 +qed "Diff_anti_mono";
    2.25 +
    2.26 +(*The LocalTo analogue fails unless 
    2.27 +    reachable (F Join G) <= reachable (F' Join G),
    2.28 +  e.g. if the initial condition of F is stronger than that of F'*)
    2.29 +Goalw [LOCALTO_def, stable_def]
    2.30 +     "[| G : v localTo[C] F';  F' <= F |] ==> G : v localTo[C] F";
    2.31 +by (auto_tac (claset() addIs [Diff_anti_mono RS component_constrains], 
    2.32 +	      simpset()));
    2.33 +qed "localTo_component";
    2.34 +
     3.1 --- a/src/HOL/UNITY/Extend.ML	Wed Oct 27 13:02:23 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Extend.ML	Wed Oct 27 13:03:32 1999 +0200
     3.3 @@ -123,6 +123,13 @@
     3.4  qed "extend_set_inverse";
     3.5  Addsimps [extend_set_inverse];
     3.6  
     3.7 +Goalw [extend_set_def, project_set_def]
     3.8 +     "C <= extend_set h (project_set h C)";
     3.9 +by (auto_tac (claset(), 
    3.10 +	      simpset() addsimps [split_extended_all]));
    3.11 +by (Blast_tac 1);
    3.12 +qed "extend_set_project_set";
    3.13 +
    3.14  Goal "inj (extend_set h)";
    3.15  by (rtac inj_on_inverseI 1);
    3.16  by (rtac extend_set_inverse 1);
    3.17 @@ -454,6 +461,12 @@
    3.18  by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
    3.19  qed "extend_localTo_extend_eq";
    3.20  
    3.21 +Goal "[| F : v localTo[C] H;  C' <= extend_set h C |] \
    3.22 +\     ==> extend h F : (v o f) localTo[C'] extend h H";
    3.23 +by (blast_tac (claset() addDs [extend_localTo_extend_eq RS iffD2,
    3.24 +			       impOfSubs localTo_anti_mono]) 1);
    3.25 +qed "extend_localTo_extend_I";
    3.26 +
    3.27  (*USED?? opposite inclusion fails*)
    3.28  Goal "Restrict C (extend_act h act) <= \
    3.29  \     extend_act h (Restrict (project_set h C) act)";
     4.1 --- a/src/HOL/UNITY/Guar.ML	Wed Oct 27 13:02:23 1999 +0200
     4.2 +++ b/src/HOL/UNITY/Guar.ML	Wed Oct 27 13:03:32 1999 +0200
     4.3 @@ -191,11 +191,6 @@
     4.4  by (Blast_tac 1);
     4.5  qed "guarantees_Join_Un";
     4.6  
     4.7 -Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
     4.8 -by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
     4.9 -by (Blast_tac 1);
    4.10 -qed "JN_component_iff";
    4.11 -
    4.12  Goalw [guar_def]
    4.13      "[| ALL i:I. F i : X i guarantees Y i |] \
    4.14  \    ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
     5.1 --- a/src/HOL/UNITY/Lift_prog.ML	Wed Oct 27 13:02:23 1999 +0200
     5.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Wed Oct 27 13:03:32 1999 +0200
     5.3 @@ -30,21 +30,8 @@
     5.4  
     5.5  Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set];
     5.6  
     5.7 -(*Converse fails*)
     5.8 -Goalw [drop_set_def] "f : A ==> f i : drop_set i A";
     5.9 -by Auto_tac;
    5.10 -qed "drop_set_I";
    5.11 -
    5.12  (** lift_act and drop_act **)
    5.13  
    5.14 -Goalw [lift_act_def] "lift_act i Id = Id";
    5.15 -by Auto_tac;
    5.16 -by (etac rev_mp 1);
    5.17 -by (dtac sym 1);
    5.18 -by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
    5.19 -qed "lift_act_Id";
    5.20 -Addsimps [lift_act_Id];
    5.21 -
    5.22  (*For compatibility with the original definition and perhaps simpler proofs*)
    5.23  Goalw [lift_act_def]
    5.24      "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
    5.25 @@ -54,12 +41,6 @@
    5.26  qed "lift_act_eq";
    5.27  AddIffs [lift_act_eq];
    5.28  
    5.29 -Goalw [drop_set_def, drop_act_def]
    5.30 -     "UNIV <= drop_set i C ==> drop_act i (Restrict C Id) = Id";
    5.31 -by (Blast_tac 1);
    5.32 -qed "drop_act_Id";
    5.33 -Addsimps [drop_act_Id];
    5.34 -
    5.35  (** lift_prog and drop_prog **)
    5.36  
    5.37  Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
    5.38 @@ -86,7 +67,10 @@
    5.39  
    5.40  (*** sub ***)
    5.41  
    5.42 -Addsimps [sub_def];
    5.43 +Goal "sub i f = f i";
    5.44 +by (simp_tac (simpset() addsimps [sub_def]) 1);
    5.45 +qed "sub_apply";
    5.46 +Addsimps [sub_apply];
    5.47  
    5.48  Goal "lift_set i {s. P s} = {s. P (sub i s)}";
    5.49  by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
    5.50 @@ -338,8 +322,9 @@
    5.51  
    5.52  Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
    5.53  \     (F : A Co B)";
    5.54 -by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog,
    5.55 -				  lift_prog_constrains]) 1);
    5.56 +by (simp_tac
    5.57 +    (simpset() addsimps [lift_prog_correct, lift_set_correct, 
    5.58 +			 lift_export extend_Constrains]) 1);
    5.59  qed "lift_prog_Constrains";
    5.60  
    5.61  Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
    5.62 @@ -453,14 +438,13 @@
    5.63  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
    5.64  qed "lift_prog_localTo_guar_increasing";
    5.65  
    5.66 -(***
    5.67 -Goal "F : (v LocalTo G) guarantees Increasing func  \
    5.68 -\     ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i G)  \
    5.69 +Goal "[| F : (v LocalTo H) guarantees Increasing func;  H <= F |]  \
    5.70 +\     ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i H)  \
    5.71  \                         guarantees Increasing (func o sub i)";
    5.72  by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
    5.73 -by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
    5.74 +by (auto_tac (claset(),
    5.75 +	      simpset() addsimps [lift_prog_correct, o_def]));
    5.76  qed "lift_prog_LocalTo_guar_Increasing";
    5.77 -***)
    5.78  
    5.79  Goal "F : Always A guarantees Always B \
    5.80  \ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
     6.1 --- a/src/HOL/UNITY/Lift_prog.thy	Wed Oct 27 13:02:23 1999 +0200
     6.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Wed Oct 27 13:03:32 1999 +0200
     6.3 @@ -39,7 +39,7 @@
     6.4    (*simplifies the expression of specifications*)
     6.5    constdefs
     6.6      sub :: ['a, 'a=>'b] => 'b
     6.7 -      "sub i f == f i"
     6.8 +      "sub == %i f. f i"
     6.9  
    6.10  
    6.11  end
     7.1 --- a/src/HOL/UNITY/PPROD.ML	Wed Oct 27 13:02:23 1999 +0200
     7.2 +++ b/src/HOL/UNITY/PPROD.ML	Wed Oct 27 13:03:32 1999 +0200
     7.3 @@ -18,13 +18,14 @@
     7.4  Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
     7.5  by Auto_tac;
     7.6  qed "Init_PLam";
     7.7 -Addsimps [Init_PLam];
     7.8  
     7.9  Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
    7.10  by (auto_tac (claset(),
    7.11  	      simpset() addsimps [PLam_def]));
    7.12  qed "Acts_PLam";
    7.13  
    7.14 +Addsimps [Init_PLam, Acts_PLam];
    7.15 +
    7.16  Goal "PLam {} F = SKIP";
    7.17  by (simp_tac (simpset() addsimps [PLam_def]) 1);
    7.18  qed "PLam_empty";
    7.19 @@ -40,6 +41,10 @@
    7.20  by Auto_tac;
    7.21  qed "PLam_insert";
    7.22  
    7.23 +Goal "((PLam I F) <= H) = (ALL i: I. lift_prog i (F i) <= H)";
    7.24 +by (simp_tac (simpset() addsimps [PLam_def, JN_component_iff]) 1);
    7.25 +qed "PLam_component_iff";
    7.26 +
    7.27  Goalw [PLam_def] "i : I ==> lift_prog i (F i) <= (PLam I F)";
    7.28  (*blast_tac doesn't use HO unification*)
    7.29  by (fast_tac (claset() addIs [component_JN]) 1);
    7.30 @@ -121,13 +126,20 @@
    7.31  qed "const_PLam_invariant";
    7.32  
    7.33  
    7.34 +(** localTo **)
    7.35 +
    7.36 +Goal "(PLam I F) : (sub i) localTo[C] lift_prog i (F i)";
    7.37 +by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def, 
    7.38 +				  stable_def, constrains_def]) 1);
    7.39 +by (Force_tac 1);
    7.40 +qed "PLam_sub_localTo";
    7.41 +
    7.42 +
    7.43  (** Reachability **)
    7.44  
    7.45  Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)";
    7.46  by (etac reachable.induct 1);
    7.47 -by (auto_tac
    7.48 -    (claset() addIs reachable.intrs,
    7.49 -     simpset() addsimps [Acts_PLam]));
    7.50 +by (auto_tac (claset() addIs reachable.intrs, simpset()));
    7.51  qed "reachable_PLam";
    7.52  
    7.53  (*Result to justify a re-organization of this file*)
    7.54 @@ -149,10 +161,10 @@
    7.55  (*Init, Init case*)
    7.56  by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
    7.57  (*Init of F, action of PLam F case*)
    7.58 -by (rtac reachable.Acts 1);
    7.59 +by (res_inst_tac [("act","act")] reachable.Acts 1);
    7.60  by (Force_tac 1);
    7.61  by (assume_tac 1);
    7.62 -by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1);
    7.63 +by (force_tac (claset() addIs [ext], simpset()) 1);
    7.64  (*induction over the 2nd "reachable" assumption*)
    7.65  by (eres_inst_tac [("xa","f")] reachable.induct 1);
    7.66  (*Init of PLam F, action of F case*)
    7.67 @@ -161,10 +173,10 @@
    7.68  by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
    7.69  by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
    7.70  (*last case: an action of PLam I F*)
    7.71 -by (rtac reachable.Acts 1);
    7.72 +by (res_inst_tac [("act","acta")] reachable.Acts 1);
    7.73  by (Force_tac 1);
    7.74  by (assume_tac 1);
    7.75 -by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1);
    7.76 +by (force_tac (claset() addIs [ext], simpset()) 1);
    7.77  qed_spec_mp "reachable_lift_Join_PLam";
    7.78  
    7.79  
     8.1 --- a/src/HOL/UNITY/Project.ML	Wed Oct 27 13:02:23 1999 +0200
     8.2 +++ b/src/HOL/UNITY/Project.ML	Wed Oct 27 13:03:32 1999 +0200
     8.3 @@ -402,7 +402,6 @@
     8.4  	       simpset() addsimps [project_set_def]) 1);
     8.5  qed "reachable_project_imp_reachable";
     8.6  
     8.7 -
     8.8  Goal "project_set h (reachable (extend h F Join G)) = \
     8.9  \     reachable (F Join project h (reachable (extend h F Join G)) G)";
    8.10  by (auto_tac (claset() addDs [subset_refl RS reachable_imp_reachable_project,
    8.11 @@ -410,6 +409,13 @@
    8.12  	      simpset() addsimps [project_set_def]));
    8.13  qed "project_set_reachable_extend_eq";
    8.14  
    8.15 +Goal "reachable (extend h F Join G) <= C  \
    8.16 +\     ==> reachable (extend h F Join G) <= \
    8.17 +\         extend_set h (reachable (F Join project h C G))";
    8.18 +by (auto_tac (claset() addDs [reachable_imp_reachable_project], 
    8.19 +	      simpset()));
    8.20 +qed "reachable_extend_Join_subset";
    8.21 +
    8.22  (*Perhaps should replace C by reachable...*)
    8.23  Goalw [Constrains_def]
    8.24       "[| C <= reachable (extend h F Join G);  \
    8.25 @@ -472,16 +478,14 @@
    8.26  				      Collect_eq_extend_set RS sym]) 1);
    8.27  qed "project_Increasing";
    8.28  
    8.29 -(**
    8.30 -Goal "extend h F Join G : (v o f) LocalTo extend h H \
    8.31 +Goal "[| H <= F;  extend h F Join G : (v o f) LocalTo extend h H |] \
    8.32  \     ==> F Join project h (reachable (extend h F Join G)) G : v LocalTo H";
    8.33  by (asm_full_simp_tac 
    8.34 -    (simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
    8.35 -			 gen_project_localTo_I,
    8.36 -			 Join_assoc RS sym]) 1);
    8.37 -
    8.38 +    (simpset() delsimps [extend_Join]
    8.39 +	       addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
    8.40 +			 gen_project_localTo_I, extend_Join RS sym, 
    8.41 +			 Join_assoc RS sym, Join_absorb1]) 1);
    8.42  qed "project_LocalTo_I";
    8.43 -**)
    8.44  
    8.45  (** A lot of redundant theorems: all are proved to facilitate reasoning
    8.46      about guarantees. **)
    8.47 @@ -510,13 +514,11 @@
    8.48  by (blast_tac (claset() addIs [project_Increasing_I]) 1);
    8.49  qed "projecting_Increasing";
    8.50  
    8.51 -(**
    8.52  Goalw [projecting_def]
    8.53 -     "projecting (%G. reachable (extend h F Join G)) h F \
    8.54 -\                ((v o f) LocalTo extend h H) (v LocalTo H)";
    8.55 +     "H <= F ==> projecting (%G. reachable (extend h F Join G)) h F \
    8.56 +\                           ((v o f) LocalTo extend h H) (v LocalTo H)";
    8.57  by (blast_tac (claset() addIs [project_LocalTo_I]) 1);
    8.58  qed "projecting_LocalTo";
    8.59 -**)
    8.60  
    8.61  Goalw [extending_def]
    8.62       "extending (%G. reachable (extend h F Join G)) h F X' \
    8.63 @@ -625,32 +627,15 @@
    8.64  		       simpset()) 1));
    8.65  qed_spec_mp "Join_project_ensures";
    8.66  
    8.67 -Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
    8.68 -\        extend h F Join G : stable C;  \
    8.69 -\        F Join project h C G : A leadsTo B |] \
    8.70 -\     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
    8.71 -by (etac leadsTo_induct 1);
    8.72 -by (asm_simp_tac (simpset() delsimps UN_simps
    8.73 -		  addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
    8.74 -by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, 
    8.75 -			       leadsTo_Trans]) 2);
    8.76 -by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
    8.77 -qed "project_leadsTo_lemma";
    8.78 +(** Lemma useful for both STRONG and WEAK progress*)
    8.79  
    8.80 -(*Instance of the previous theorem for STRONG progress*)
    8.81 -Goal "[| ALL D. project h UNIV G : transient D --> F : transient D;  \
    8.82 -\        F Join project h UNIV G : A leadsTo B |] \
    8.83 -\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
    8.84 -by (dtac project_leadsTo_lemma 1);
    8.85 -by Auto_tac;
    8.86 -qed "project_UNIV_leadsTo_lemma";
    8.87 -
    8.88 -(** Towards the analogous theorem for WEAK progress*)
    8.89 -
    8.90 +(*The strange induction formula allows induction over the leadsTo
    8.91 +  assumption's non-atomic precondition*)
    8.92  Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
    8.93  \        extend h F Join G : stable C;  \
    8.94  \        F Join project h C G : (project_set h C Int A) leadsTo B |] \
    8.95 -\     ==> extend h F Join G : C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
    8.96 +\     ==> extend h F Join G : \
    8.97 +\         C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
    8.98  by (etac leadsTo_induct 1);
    8.99  by (asm_simp_tac (simpset() delsimps UN_simps
   8.100  		  addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
   8.101 @@ -665,14 +650,14 @@
   8.102  \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
   8.103  by (rtac (lemma RS leadsTo_weaken) 1);
   8.104  by (auto_tac (claset() addIs [project_set_I], simpset()));
   8.105 -val lemma2 = result();
   8.106 +qed "project_leadsTo_lemma";
   8.107  
   8.108  Goal "[| C = (reachable (extend h F Join G)); \
   8.109  \        ALL D. project h C G : transient D --> F : transient D;  \
   8.110  \        F Join project h C G : A LeadsTo B |] \
   8.111  \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
   8.112  by (asm_full_simp_tac 
   8.113 -    (simpset() addsimps [LeadsTo_def, lemma2, stable_reachable, 
   8.114 +    (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma, stable_reachable, 
   8.115  			 project_set_reachable_extend_eq]) 1);
   8.116  qed "Join_project_LeadsTo";
   8.117  
   8.118 @@ -713,14 +698,12 @@
   8.119  val [xguary,project,extend] =
   8.120  Goal "[| F : X guarantees Y;  \
   8.121  \        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
   8.122 -\        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
   8.123 -\                Disjoint UNIV (extend h F) G |] \
   8.124 +\        !!G. [| F Join proj G h G : Y; extend h F Join G : X' |] \
   8.125  \             ==> extend h F Join G : Y' |] \
   8.126  \     ==> extend h F : X' guarantees Y'";
   8.127  by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
   8.128  by (etac project 1);
   8.129  by (assume_tac 1);
   8.130 -by (assume_tac 1);
   8.131  qed "project_guarantees_lemma";
   8.132  
   8.133  Goal "[| F : X guarantees Y;  \
   8.134 @@ -761,16 +744,14 @@
   8.135  by (rtac projecting_localTo 1);
   8.136  qed "extend_localTo_guar_increasing";
   8.137  
   8.138 -(**
   8.139 -Goal "F : (v LocalTo G) guarantees Increasing func  \
   8.140 -\     ==> extend h F : (v o f) LocalTo (extend h G)  \
   8.141 +Goal "[| F : (v LocalTo H) guarantees Increasing func;  H <= F |]  \
   8.142 +\     ==> extend h F : (v o f) LocalTo (extend h H)  \
   8.143  \                      guarantees Increasing (func o f)";
   8.144  by (etac project_guarantees 1);
   8.145  by (rtac extending_Increasing 2);
   8.146  by (rtac projecting_LocalTo 1);
   8.147  by Auto_tac;
   8.148  qed "extend_LocalTo_guar_Increasing";
   8.149 -**)
   8.150  
   8.151  Goal "F : Always A guarantees Always B \
   8.152  \ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
   8.153 @@ -808,9 +789,9 @@
   8.154  Goal "[| F Join project h UNIV G : A leadsTo B;    \
   8.155  \        G : f localTo[UNIV] extend h F |]  \
   8.156  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   8.157 -by (rtac project_UNIV_leadsTo_lemma 1);
   8.158 +by (res_inst_tac [("C1", "UNIV")] (project_leadsTo_lemma RS leadsTo_weaken) 1);
   8.159  by (auto_tac (claset(), 
   8.160 -         simpset() addsimps [impOfSubs (subset_UNIV RS localTo_anti_mono) RS
   8.161 +         simpset() addsimps [localTo_UNIV_imp_localTo RS
   8.162  			     localTo_project_transient_transient]));
   8.163  qed "project_leadsTo_D";
   8.164  
     9.1 --- a/src/HOL/UNITY/Project.thy	Wed Oct 27 13:02:23 1999 +0200
     9.2 +++ b/src/HOL/UNITY/Project.thy	Wed Oct 27 13:03:32 1999 +0200
     9.3 @@ -19,8 +19,7 @@
     9.4    extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
     9.5  		 'c program set, 'c program set, 'a program set] => bool"
     9.6    "extending C h F X' Y' Y ==
     9.7 -     ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
     9.8 -            Disjoint UNIV (extend h F) G
     9.9 +     ALL G. F Join project h (C G) G : Y & extend h F Join G : X'
    9.10              --> extend h F Join G : Y'"
    9.11  
    9.12  end
    10.1 --- a/src/HOL/UNITY/Union.ML	Wed Oct 27 13:02:23 1999 +0200
    10.2 +++ b/src/HOL/UNITY/Union.ML	Wed Oct 27 13:03:32 1999 +0200
    10.3 @@ -325,6 +325,9 @@
    10.4  by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
    10.5  qed "localTo_anti_mono";
    10.6  
    10.7 +bind_thm ("localTo_UNIV_imp_localTo", 
    10.8 +	  impOfSubs (subset_UNIV RS localTo_anti_mono));
    10.9 +
   10.10  Goalw [LocalTo_def]
   10.11       "G : v localTo[UNIV] F ==> G : v LocalTo F";
   10.12  by (blast_tac (claset() addDs [impOfSubs localTo_anti_mono]) 1);
   10.13 @@ -355,6 +358,15 @@
   10.14  			 Diff_self_eq]) 1);
   10.15  qed "self_localTo";
   10.16  
   10.17 +Goal "(F Join G : v localTo[C] F) = (G : v localTo[C] F)";
   10.18 +by (simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
   10.19 +qed "self_Join_localTo";
   10.20 +
   10.21 +Goal "(F Join G : v LocalTo F) = (G : v LocalTo F)";
   10.22 +by (simp_tac (simpset() addsimps [self_Join_localTo, LocalTo_def,
   10.23 +				  Join_left_absorb]) 1);
   10.24 +qed "self_Join_LocalTo";
   10.25 +
   10.26  
   10.27  
   10.28  (*** Higher-level rules involving localTo and Join ***)
    11.1 --- a/src/HOL/UNITY/Union.thy	Wed Oct 27 13:02:23 1999 +0200
    11.2 +++ b/src/HOL/UNITY/Union.thy	Wed Oct 27 13:03:32 1999 +0200
    11.3 @@ -8,6 +8,8 @@
    11.4  Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
    11.5  
    11.6  Do we need a Meet operator?  (Aka Intersection)
    11.7 +
    11.8 +CAN PROBABLY DELETE the "Disjoint" predicate
    11.9  *)
   11.10  
   11.11  Union = SubstAx + FP +