abolition of localTo: instead "guarantees" has local vars as extra argument
authorpaulson
Wed Dec 08 13:53:29 1999 +0100 (1999-12-08)
changeset 8055bb15396278fb
parent 8054 2ce57ef2a4aa
child 8056 3c587e7b8fe5
abolition of localTo: instead "guarantees" has local vars as extra argument
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Alloc.thy
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/ELT.ML
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/Lift_prog.ML
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 Dec 08 13:52:36 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Wed Dec 08 13:53:29 1999 +0100
     1.3 @@ -123,19 +123,20 @@
     1.4      rewrite_rule [client_spec_def, client_increasing_def,
     1.5  		  client_bounded_def, client_progress_def] Client;
     1.6  
     1.7 -Goal "Client : UNIV guarantees Increasing ask";
     1.8 +Goal "Client : UNIV guarantees[funPair rel ask] Increasing ask";
     1.9  by (cut_facts_tac [Client_Spec] 1);
    1.10  by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
    1.11  qed "Client_Increasing_ask";
    1.12  
    1.13 -Goal "Client : UNIV guarantees Increasing rel";
    1.14 +Goal "Client : UNIV guarantees[funPair rel ask] Increasing rel";
    1.15  by (cut_facts_tac [Client_Spec] 1);
    1.16  by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
    1.17  qed "Client_Increasing_rel";
    1.18  
    1.19  AddIffs [Client_Increasing_ask, Client_Increasing_rel];
    1.20  
    1.21 -Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
    1.22 +Goal "Client : UNIV guarantees[ask] \
    1.23 +\              Always {s. ALL elt : set (ask s). elt <= NbT}";
    1.24  by (cut_facts_tac [Client_Spec] 1);
    1.25  by Auto_tac;
    1.26  qed "Client_Bounded";
    1.27 @@ -161,7 +162,8 @@
    1.28      rewrite_rule [alloc_spec_def, alloc_increasing_def,
    1.29  		  alloc_safety_def, alloc_progress_def] Alloc;
    1.30  
    1.31 -Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
    1.32 +Goal "i < Nclients \
    1.33 +\     ==> Alloc : UNIV guarantees[allocGiv] Increasing (sub i o allocGiv)";
    1.34  by (cut_facts_tac [Alloc_Spec] 1);
    1.35  by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
    1.36  qed "Alloc_Increasing";
    1.37 @@ -192,7 +194,8 @@
    1.38  
    1.39  (*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
    1.40  Goal "i < Nclients \
    1.41 -\ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
    1.42 +\     ==> extend sysOfAlloc Alloc : \
    1.43 +\           UNIV guarantees[allocGiv] Increasing (sub i o allocGiv)";
    1.44  by (dtac (Alloc_Increasing RS alloc_export extend_guar_Increasing) 1);
    1.45  by (auto_tac (claset(), simpset() addsimps [o_def]));
    1.46  qed "extend_Alloc_Increasing_allocGiv";
    1.47 @@ -324,7 +327,6 @@
    1.48  (** Lemmas about localTo **)
    1.49  
    1.50  Goal "extend sysOfAlloc F : client localTo[C] extend sysOfClient G";
    1.51 -by (rtac localTo_UNIV_imp_localTo 1);
    1.52  by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def, 
    1.53  				  stable_def, constrains_def,
    1.54  				  image_eq_UN, extend_act_def,
    1.55 @@ -332,12 +334,11 @@
    1.56  by (Force_tac 1);
    1.57  qed "sysOfAlloc_in_client_localTo_xl_Client";
    1.58  
    1.59 -Goal "extend sysOfClient (plam i:I. F) :  \
    1.60 +??Goal "extend sysOfClient (plam i:I. F) :  \
    1.61  \      (sub i o client) localTo[C] extend sysOfClient (lift_prog i F)";
    1.62 -by (rtac localTo_UNIV_imp_localTo 1);
    1.63  by (rtac (client_export (extend_set_UNIV_eq RS equalityD2 RSN
    1.64  			 (2, extend_localTo_extend_I))) 1);
    1.65 -by (rtac PLam_sub_localTo 1);
    1.66 +by (rtac ??PLam_sub_localTo 1);
    1.67  qed "sysOfClient_in_client_localTo_xl_Client";
    1.68  
    1.69  
    1.70 @@ -398,7 +399,7 @@
    1.71  (*Lemma (?).  A LOT of work just to lift "Client_Progress" to the array*)
    1.72  Goal "lift_prog i Client \
    1.73  \        :  Increasing (giv o sub i) Int \
    1.74 -\           ((funPair rel ask o sub i) LocalTo (lift_prog i Client)) \
    1.75 +\           ((funPair rel ask o sub i) localTo (lift_prog i Client)) \
    1.76  \          guarantees \
    1.77  \          (INT h. {s. h <=  (giv o sub i) s & \
    1.78  \                             h pfixGe (ask o sub i) s}  \
    1.79 @@ -421,7 +422,7 @@
    1.80       "(plam x:lessThan Nclients. Client) \
    1.81  \        : (INT i : lessThan Nclients. \
    1.82  \             Increasing (giv o sub i) Int \
    1.83 -\             ((funPair rel ask o sub i) LocalTo (lift_prog i Client))) \
    1.84 +\             ((funPair rel ask o sub i) localTo (lift_prog i Client))) \
    1.85  \          guarantees \
    1.86  \          (INT i : lessThan Nclients. \
    1.87  \               INT h. {s. h <=  (giv o sub i) s & \
    1.88 @@ -432,23 +433,39 @@
    1.89  by (rtac Client_i_Progress 1);
    1.90  qed "PLam_Client_Progress";
    1.91  
    1.92 +(*because it IS NOT CLEAR that localTo is good for anything: no laws*)
    1.93 +Goal "(plam x:lessThan Nclients. Client) \
    1.94 +\        : (INT i : lessThan Nclients. \
    1.95 +\             Increasing (giv o sub i) Int \
    1.96 +\             ((funPair rel ask o sub i) localTo[UNIV] (lift_prog i Client))) \
    1.97 +\          guarantees \
    1.98 +\          (INT i : lessThan Nclients. \
    1.99 +\               INT h. {s. h <=  (giv o sub i) s & \
   1.100 +\                             h pfixGe (ask o sub i) s}  \
   1.101 +\                  LeadsTo[givenBy (funPair rel ask o sub i)] \
   1.102 +\                    {s. tokens h <= (tokens o rel o sub i) s})";
   1.103 +by (blast_tac (claset() addIs [PLam_Client_Progress RS guarantees_weaken,
   1.104 +			       localTo_imp_localTo]) 1);
   1.105 +qed "PLam_Client_Progress_localTo";
   1.106 +
   1.107  (*progress (2), step 7*)
   1.108  
   1.109  
   1.110 +xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
   1.111  
   1.112         [| ALL i:lessThan Nclients.
   1.113 -             G : (sub i o client) LocalTo
   1.114 +             G : (sub i o client) localTo
   1.115                   extend sysOfClient (lift_prog i Client) |]
   1.116 -       ==> G : client LocalTo
   1.117 +       ==> G : client localTo
   1.118                 extend sysOfClient (plam i:lessThan Nclients. Client)
   1.119  
   1.120     
   1.121     
   1.122     
   1.123     [| ALL i: I.
   1.124 -	 G : (sub i o client) LocalTo
   1.125 +	 G : (sub i o client) localTo
   1.126  	     extend sysOfClient (lift_prog i Client) |]
   1.127 -   ==> G : client LocalTo
   1.128 +   ==> G : client localTo
   1.129  	   extend sysOfClient (plam x: I. Client)
   1.130  
   1.131  
   1.132 @@ -463,16 +480,31 @@
   1.133  
   1.134  
   1.135  
   1.136 - G : (sub i o client) LocalTo extend sysOfClient (plam x: I. Client)
   1.137 + G : (sub i o client) localTo extend sysOfClient (plam x: I. Client)
   1.138  
   1.139  
   1.140  xxxxxxxxxxxxxxxx;
   1.141  
   1.142 -THIS PROOF requires an extra locality specification for Network:
   1.143 -    Network : rel o sub i o client localTo[C] 
   1.144 -                     extend sysOfClient (lift_prog i Client)
   1.145 -and similarly for ask o sub i o client.
   1.146 +NEW AXIOM NEEDED??
   1.147 +i < Nclients
   1.148 +         ==> System
   1.149 +             : (funPair rel ask o sub i o client) localTo
   1.150 +               extend sysOfClient (lift_prog i Client)
   1.151 +
   1.152  
   1.153 +Goal "[| G : v localTo[C] (lift_prog i (F i));  i: I |]  \
   1.154 +\     ==> G : v localTo[C] (PLam I F)";
   1.155 +by (auto_tac (claset() addIs [Diff_anti_mono RS component_constrains], 
   1.156 +	      simpset()));
   1.157 +qed "localTo_component";
   1.158 +
   1.159 +Goalw [LOCALTO_def, localTo_def, stable_def]
   1.160 +     "[| G : v localTo (lift_prog i (F i));  i: I |]  \
   1.161 +\     ==> G : v localTo (PLam I F)";
   1.162 +by (subgoal_tac "reachable ((PLam I F) Join G) <= reachable ((lift_prog i (F i)) Join G)" 1);
   1.163 +by (auto_tac (claset() addIs [Diff_anti_mono RS component_constrains], 
   1.164 +	      simpset()));
   1.165 +qed "localTo_component";
   1.166  
   1.167  
   1.168  Goalw [System_def]
   1.169 @@ -483,31 +515,41 @@
   1.170  \                  {s. tokens h <= (tokens o rel o sub i o client) s})";
   1.171  by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
   1.172  by (rtac (PLam_Client_Progress RS project_guarantees) 1);
   1.173 -br extending_INT 2;
   1.174 +by (rtac extending_INT 2);
   1.175  by (rtac (client_export extending_LeadsETo RS extending_weaken RS extending_INT) 2);
   1.176  by (rtac subset_refl 4);
   1.177  by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
   1.178 +
   1.179 +by (rtac projecting_INT 1);
   1.180 +by (rtac projecting_Int 1);
   1.181 +by (rtac (client_export projecting_Increasing) 1);
   1.182 +
   1.183  by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
   1.184  			      client_export projecting_Increasing,
   1.185  			      component_PLam,
   1.186 -			      client_export projecting_LocalTo]) 1);
   1.187 -auto();
   1.188 +			      client_export projecting_localTo]) 1);
   1.189 +by Auto_tac;
   1.190 +by (fold_tac [System_def]);
   1.191 +by (etac System_Increasing_giv 2);
   1.192 +
   1.193  
   1.194 -be INT_lower 2;
   1.195 +by (rtac localTo_component 1);
   1.196  
   1.197 -br projecting_INT 1;
   1.198 -br projecting_Int 1;
   1.199 +by (etac INT_lower 2);
   1.200 +
   1.201 +by (rtac projecting_INT 1);
   1.202 +by (rtac projecting_Int 1);
   1.203  
   1.204  (*The next step goes wrong: it makes an impossible localTo subgoal*)
   1.205  (*blast_tac doesn't use HO unification*)
   1.206  by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
   1.207  			      client_export projecting_Increasing,
   1.208  			      component_PLam,
   1.209 -			      client_export projecting_LocalTo]) 1);
   1.210 +			      client_export projecting_localTo]) 1);
   1.211  by (Clarify_tac 2);
   1.212  by (asm_simp_tac
   1.213      (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
   1.214 -			 LocalTo_def, Join_localTo,
   1.215 +			 localTo_def, Join_localTo,
   1.216  			 sysOfClient_in_client_localTo_xl_Client,
   1.217  			 sysOfAlloc_in_client_localTo_xl_Client 
   1.218  			  RS localTo_imp_o_localTo,
   1.219 @@ -516,6 +558,7 @@
   1.220  
   1.221  
   1.222  
   1.223 +
   1.224  OLD PROOF;
   1.225  by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
   1.226  by (rtac (guarantees_PLam_I RS project_guarantees) 1);
   1.227 @@ -529,10 +572,10 @@
   1.228  by (fast_tac (claset() addIs [projecting_Int,
   1.229  			      client_export projecting_Increasing,
   1.230  			      component_PLam,
   1.231 -			      client_export projecting_LocalTo]) 1);
   1.232 +			      client_export projecting_localTo]) 1);
   1.233  by (asm_simp_tac
   1.234      (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
   1.235 -			 LocalTo_def, Join_localTo,
   1.236 +			 localTo_def, Join_localTo,
   1.237  			 sysOfClient_in_client_localTo_xl_Client,
   1.238  			 sysOfAlloc_in_client_localTo_xl_Client]) 2);
   1.239  by Auto_tac;
     2.1 --- a/src/HOL/UNITY/Alloc.thy	Wed Dec 08 13:52:36 1999 +0100
     2.2 +++ b/src/HOL/UNITY/Alloc.thy	Wed Dec 08 13:53:29 1999 +0100
     2.3 @@ -32,15 +32,17 @@
     2.4    Nclients :: nat       (*Number of clients*)
     2.5  
     2.6  
     2.7 +(** State definitions.  OUTPUT variables are locals **)
     2.8 +
     2.9  record clientState =
    2.10    giv :: nat list   (*client's INPUT history:  tokens GRANTED*)
    2.11    ask :: nat list   (*client's OUTPUT history: tokens REQUESTED*)
    2.12    rel :: nat list   (*client's OUTPUT history: tokens RELEASED*)
    2.13  
    2.14  record allocState =
    2.15 -  allocGiv :: nat => nat list   (*allocator's local copy of "giv" for i*)
    2.16 -  allocAsk :: nat => nat list   (*allocator's local copy of "ask" for i*)
    2.17 -  allocRel :: nat => nat list   (*allocator's local copy of "rel" for i*)
    2.18 +  allocGiv :: nat => nat list   (*OUTPUT history: source of "giv" for i*)
    2.19 +  allocAsk :: nat => nat list   (*INPUT: allocator's copy of "ask" for i*)
    2.20 +  allocRel :: nat => nat list   (*INPUT: allocator's copy of "rel" for i*)
    2.21  
    2.22  record systemState = allocState +
    2.23    client :: nat => clientState  (*states of all clients*)
    2.24 @@ -68,21 +70,23 @@
    2.25  
    2.26  (** Client specification (required) ***)
    2.27  
    2.28 -  (*spec (3) PROBABLY REQUIRES A LOCALTO PRECONDITION*)
    2.29 +  (*spec (3)*)
    2.30    client_increasing :: clientState program set
    2.31      "client_increasing ==
    2.32 -         UNIV guarantees Increasing ask Int Increasing rel"
    2.33 +         UNIV guarantees[funPair rel ask]
    2.34 +         Increasing ask Int Increasing rel"
    2.35  
    2.36    (*spec (4)*)
    2.37    client_bounded :: clientState program set
    2.38      "client_bounded ==
    2.39 -         UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
    2.40 +         UNIV guarantees[ask]
    2.41 +         Always {s. ALL elt : set (ask s). elt <= NbT}"
    2.42  
    2.43    (*spec (5)*)
    2.44    client_progress :: clientState program set
    2.45      "client_progress ==
    2.46  	 Increasing giv
    2.47 -	 guarantees
    2.48 +	 guarantees[funPair rel ask]
    2.49  	 (INT h. {s. h <= giv s & h pfixGe ask s}
    2.50  		 LeadsTo[givenBy (funPair rel ask)]
    2.51  		 {s. tokens h <= (tokens o rel) s})"
    2.52 @@ -92,18 +96,18 @@
    2.53  
    2.54  (** Allocator specification (required) ***)
    2.55  
    2.56 -  (*spec (6)  PROBABLY REQUIRES A LOCALTO PRECONDITION*)
    2.57 +  (*spec (6)*)
    2.58    alloc_increasing :: allocState program set
    2.59      "alloc_increasing ==
    2.60  	 UNIV
    2.61 -         guarantees
    2.62 +         guarantees[allocGiv]
    2.63  	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
    2.64  
    2.65    (*spec (7)*)
    2.66    alloc_safety :: allocState program set
    2.67      "alloc_safety ==
    2.68  	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
    2.69 -         guarantees
    2.70 +         guarantees[allocGiv]
    2.71  	 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients
    2.72  	         <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
    2.73  
    2.74 @@ -120,7 +124,7 @@
    2.75           (INT i : lessThan Nclients. 
    2.76  	  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
    2.77  		  LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})
    2.78 -         guarantees
    2.79 +         guarantees[allocGiv]
    2.80  	     (INT i : lessThan Nclients.
    2.81  	      INT h. {s. h <= (sub i o allocAsk) s} LeadsTo
    2.82  	             {s. h pfixLe (sub i o allocGiv) s})"
    2.83 @@ -134,21 +138,21 @@
    2.84    network_ask :: systemState program set
    2.85      "network_ask == INT i : lessThan Nclients.
    2.86                      Increasing (ask o sub i o client)
    2.87 -                    guarantees
    2.88 +                    guarantees[allocAsk]
    2.89                      ((sub i o allocAsk) Fols (ask o sub i o client))"
    2.90  
    2.91    (*spec (9.2)*)
    2.92    network_giv :: systemState program set
    2.93      "network_giv == INT i : lessThan Nclients.
    2.94                      Increasing (sub i o allocGiv)
    2.95 -                    guarantees
    2.96 +                    guarantees[giv o sub i o client]
    2.97                      ((giv o sub i o client) Fols (sub i o allocGiv))"
    2.98  
    2.99    (*spec (9.3)*)
   2.100    network_rel :: systemState program set
   2.101      "network_rel == INT i : lessThan Nclients.
   2.102                      Increasing (rel o sub i o client)
   2.103 -                    guarantees
   2.104 +                    guarantees[allocRel]
   2.105                      ((sub i o allocRel) Fols (rel o sub i o client))"
   2.106  
   2.107    network_spec :: systemState program set
     3.1 --- a/src/HOL/UNITY/Client.ML	Wed Dec 08 13:52:36 1999 +0100
     3.2 +++ b/src/HOL/UNITY/Client.ML	Wed Dec 08 13:53:29 1999 +0100
     3.3 @@ -73,13 +73,11 @@
     3.4  program_defs_ref := [];
     3.5  
     3.6  (*Safety property 2: clients return the right number of tokens*)
     3.7 -Goal "Cli_prg : (Increasing giv Int (rel localTo[UNIV] Cli_prg))  \
     3.8 -\               guarantees Always {s. rel s <= giv s}";
     3.9 +Goal "Cli_prg : Increasing giv  guarantees[rel]  Always {s. rel s <= giv s}";
    3.10  by (rtac guaranteesI 1);
    3.11  by (rtac AlwaysI 1);
    3.12  by (Force_tac 1);
    3.13 -by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
    3.14 -by (blast_tac (claset() addIs [Increasing_localTo_Stable, 
    3.15 +by (blast_tac (claset() addIs [Increasing_preserves_Stable, 
    3.16  			       stable_rel_le_giv]) 1);
    3.17  qed "ok_guar_rel_prefix_giv";
    3.18  
    3.19 @@ -101,30 +99,29 @@
    3.20  val Increasing_length = mono_length RS mono_Increasing_o;
    3.21  
    3.22  Goal "Cli_prg : \
    3.23 -\      (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg)) \
    3.24 -\      guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
    3.25 -\                            {s. size (rel s) <= size (giv s)})";
    3.26 +\      Increasing giv  guarantees[funPair rel ask] \
    3.27 +\      Always ({s. size (ask s) <= Suc (size (rel s))} Int \
    3.28 +\              {s. size (rel s) <= size (giv s)})";
    3.29  by (rtac guaranteesI 1);
    3.30 -by (Clarify_tac 1);
    3.31  by (dtac (impOfSubs (rewrite_o Increasing_length)) 1);
    3.32  by (rtac AlwaysI 1);
    3.33  by (Force_tac 1);
    3.34  by (rtac Stable_Int 1);
    3.35 -by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 2);
    3.36 -by (fast_tac (claset() addEs [rewrite_o localTo_imp_o_localTo]
    3.37 -	               addIs [Increasing_localTo_Stable, 
    3.38 +by (fast_tac (claset() addEs [rewrite_o (impOfSubs subset_preserves_o)]
    3.39 +	               addIs [Increasing_preserves_Stable, 
    3.40  			      stable_size_rel_le_giv]) 2);
    3.41 -by (full_simp_tac (simpset() addsimps [Join_localTo]) 1);
    3.42 -by (fast_tac (claset() addEs [rewrite_o localTo_imp_o_localTo]
    3.43 -	               addIs [stable_localTo_stable2 RS stable_imp_Stable,
    3.44 -			      stable_size_ask_le_rel]) 1);
    3.45 +by (res_inst_tac [("v1", "ask"), ("w1", "rel")]  
    3.46 +    (stable_localTo_stable2 RS stable_imp_Stable) 1);
    3.47 +by (ALLGOALS 
    3.48 +    (fast_tac (claset() addEs [rewrite_o (impOfSubs subset_preserves_o)]
    3.49 +	                addIs [stable_size_ask_le_rel])));
    3.50  val lemma1 = result();
    3.51  
    3.52  
    3.53  Goal "Cli_prg : \
    3.54 -\      (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg) \
    3.55 -\                 Int Always giv_meets_ask) \
    3.56 -\      guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
    3.57 +\      Increasing giv Int Always giv_meets_ask \
    3.58 +\      guarantees[funPair rel ask]  \
    3.59 +\        ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
    3.60  by (rtac guaranteesI 1);
    3.61  by (Clarify_tac 1);
    3.62  by (rtac Stable_transient_Always_LeadsTo 1);
    3.63 @@ -133,7 +130,7 @@
    3.64  			       impOfSubs Increasing_Stable_less],
    3.65  	       simpset()) 1);
    3.66  by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
    3.67 -by (Blast_tac 1);
    3.68 +by Auto_tac;
    3.69  by (force_tac (claset(), 
    3.70  	       simpset() addsimps [Always_eq_includes_reachable, 
    3.71  				  giv_meets_ask_def]) 1);
     4.1 --- a/src/HOL/UNITY/Comp.ML	Wed Dec 08 13:52:36 1999 +0100
     4.2 +++ b/src/HOL/UNITY/Comp.ML	Wed Dec 08 13:53:29 1999 +0100
     4.3 @@ -74,11 +74,6 @@
     4.4  by (blast_tac (claset() addSIs [program_equalityI]) 1);
     4.5  qed "component_antisym";
     4.6  
     4.7 -Goalw [component_def]
     4.8 -      "F <= H = (EX G. F Join G = H & Disjoint UNIV F G)";
     4.9 -by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
    4.10 -qed "component_eq";
    4.11 -
    4.12  Goal "((F Join G) <= H) = (F <= H & G <= H)";
    4.13  by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
    4.14  by (Blast_tac 1);
    4.15 @@ -92,16 +87,86 @@
    4.16  (*Used in Guar.thy to show that programs are partially ordered*)
    4.17  bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
    4.18  
    4.19 -Goal "F' <= F ==> Diff C G (Acts F) <= Diff C G (Acts F')";
    4.20 -by (auto_tac (claset(), simpset() addsimps [Diff_def, component_eq_subset]));
    4.21 -qed "Diff_anti_mono";
    4.22 +
    4.23 +(*** preserves ***)
    4.24 +
    4.25 +Goal "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
    4.26 +by (simp_tac (simpset() addsimps [Join_stable, preserves_def]) 1);
    4.27 +by (Blast_tac 1);
    4.28 +qed "Join_preserves";
    4.29 +
    4.30 +Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)";
    4.31 +by (simp_tac (simpset() addsimps [JN_stable, preserves_def]) 1);
    4.32 +by (Blast_tac 1);
    4.33 +qed "JN_preserves";
    4.34 +
    4.35 +Goal "preserves (funPair v w) = preserves v Int preserves w";
    4.36 +by (auto_tac (claset(),
    4.37 +	      simpset() addsimps [funPair_def, preserves_def, 
    4.38 +				  stable_def, constrains_def]));
    4.39 +by (Blast_tac 1);
    4.40 +qed "preserves_funPair";
    4.41 +
    4.42 +(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
    4.43 +AddIffs [preserves_funPair RS eqset_imp_iff];
    4.44 +
    4.45 +
    4.46 +Goal "(funPair f g) o h = funPair (f o h) (g o h)";
    4.47 +by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
    4.48 +qed "funPair_o_distrib";
    4.49 +
    4.50 +Goal "preserves v <= preserves (w o v)";
    4.51 +by (force_tac (claset(),
    4.52 +	       simpset() addsimps [preserves_def, 
    4.53 +				   stable_def, constrains_def]) 1);
    4.54 +qed "subset_preserves_o";
    4.55  
    4.56 -(*The LocalTo analogue fails unless 
    4.57 -    reachable (F Join G) <= reachable (F' Join G),
    4.58 -  e.g. if the initial condition of F is stronger than that of F'*)
    4.59 -Goalw [LOCALTO_def, stable_def]
    4.60 -     "[| G : v localTo[C] F';  F' <= F |] ==> G : v localTo[C] F";
    4.61 -by (auto_tac (claset() addIs [Diff_anti_mono RS component_constrains], 
    4.62 -	      simpset()));
    4.63 -qed "localTo_component";
    4.64 +Goal "preserves v <= stable {s. P (v s)}";
    4.65 +by (auto_tac (claset(),
    4.66 +	      simpset() addsimps [preserves_def, 
    4.67 +				  stable_def, constrains_def]));
    4.68 +by (rename_tac "s' s" 1);
    4.69 +by (subgoal_tac "v s = v s'" 1);
    4.70 +by (ALLGOALS Force_tac);
    4.71 +qed "preserves_subset_stable";
    4.72 +
    4.73 +Goal "preserves id <= stable A";
    4.74 +by (force_tac (claset(), 
    4.75 +	   simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
    4.76 +qed "preserves_id_subset_stable";
    4.77 +
    4.78 +
    4.79 +(** Some lemmas used only in Client.ML **)
    4.80  
    4.81 +Goal "[| F : stable {s. P (v s) (w s)};   \
    4.82 +\        G : preserves v;  G : preserves w |]               \
    4.83 +\     ==> F Join G : stable {s. P (v s) (w s)}";
    4.84 +by (asm_simp_tac (simpset() addsimps [Join_stable]) 1);
    4.85 +by (subgoal_tac "G: preserves (funPair v w)" 1);
    4.86 +by (Asm_simp_tac 2);
    4.87 +by (dres_inst_tac [("P1", "split ?Q")]  
    4.88 +    (impOfSubs preserves_subset_stable) 1);
    4.89 +by (auto_tac (claset(), simpset() addsimps [funPair_def]));
    4.90 +qed "stable_localTo_stable2";
    4.91 +
    4.92 +Goal "[| F : stable {s. v s <= w s};  G : preserves v;       \
    4.93 +\        F Join G : Increasing w |]               \
    4.94 +\     ==> F Join G : Stable {s. v s <= w s}";
    4.95 +by (auto_tac (claset(), 
    4.96 +	      simpset() addsimps [stable_def, Stable_def, Increasing_def, 
    4.97 +		    Constrains_def, Join_constrains, all_conj_distrib]));
    4.98 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
    4.99 +(*The G case remains*)
   4.100 +by (auto_tac (claset(), 
   4.101 +              simpset() addsimps [preserves_def, stable_def, constrains_def]));
   4.102 +by (case_tac "act: Acts F" 1);
   4.103 +by (Blast_tac 1);
   4.104 +(*We have a G-action, so delete assumptions about F-actions*)
   4.105 +by (thin_tac "ALL act:Acts F. ?P act" 1);
   4.106 +by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1);
   4.107 +by (subgoal_tac "v x = v xa" 1);
   4.108 +by (Blast_tac 2);
   4.109 +by Auto_tac;
   4.110 +by (etac order_trans 1);
   4.111 +by (Blast_tac 1);
   4.112 +qed "Increasing_preserves_Stable";
     5.1 --- a/src/HOL/UNITY/Comp.thy	Wed Dec 08 13:52:36 1999 +0100
     5.2 +++ b/src/HOL/UNITY/Comp.thy	Wed Dec 08 13:53:29 1999 +0100
     5.3 @@ -19,4 +19,11 @@
     5.4  
     5.5    strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
     5.6  
     5.7 +constdefs
     5.8 +  preserves :: "('a=>'b) => 'a program set"
     5.9 +    "preserves v == INT z. stable {s. v s = z}"
    5.10 +
    5.11 +  funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
    5.12 +    "funPair f g == %x. (f x, g x)"
    5.13 +
    5.14  end
     6.1 --- a/src/HOL/UNITY/ELT.ML	Wed Dec 08 13:52:36 1999 +0100
     6.2 +++ b/src/HOL/UNITY/ELT.ML	Wed Dec 08 13:53:29 1999 +0100
     6.3 @@ -6,6 +6,11 @@
     6.4  leadsTo strengthened with a specification of the allowable sets transient parts
     6.5  *)
     6.6  
     6.7 +Goalw [givenBy_def] "givenBy id = UNIV";
     6.8 +by Auto_tac;
     6.9 +qed "givenBy_id";
    6.10 +Addsimps [givenBy_id];
    6.11 +
    6.12  Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
    6.13  by Safe_tac;
    6.14  by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
    6.15 @@ -51,9 +56,12 @@
    6.16  			       givenBy_imp_eq_Collect]) 1);
    6.17  qed "givenBy_eq_eq_Collect";
    6.18  
    6.19 -Goal "(funPair f g) o h = funPair (f o h) (g o h)";
    6.20 -by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
    6.21 -qed "funPair_o_distrib";
    6.22 +(*preserving v preserves properties given by v*)
    6.23 +Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
    6.24 +by (force_tac (claset(), 
    6.25 +	       simpset() addsimps [impOfSubs preserves_subset_stable, 
    6.26 +				   givenBy_eq_Collect]) 1);
    6.27 +qed "preserves_givenBy_imp_stable";
    6.28  
    6.29  
    6.30  (** Standard leadsTo rules **)
    6.31 @@ -301,7 +309,7 @@
    6.32  (*** Special properties involving the parameter [CC] ***)
    6.33  
    6.34  (*??IS THIS NEEDED?? or is it just an example of what's provable??*)
    6.35 -Goal "[| F: (A leadsTo[givenBy v] B);  F Join G : v localTo[C] F;  \
    6.36 +Goal "[| F: (A leadsTo[givenBy v] B);  G : preserves v;  \
    6.37  \        F Join G : stable C |] \
    6.38  \     ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) `` givenBy v] B)";
    6.39  by (etac leadsETo_induct 1);
    6.40 @@ -311,30 +319,17 @@
    6.41  			       leadsETo_Trans]) 2);
    6.42  by (rtac leadsETo_Basis 1);
    6.43  by (auto_tac (claset(),
    6.44 -	      simpset() addsimps [Int_Diff, ensures_def, stable_def,
    6.45 -				  givenBy_eq_Collect,
    6.46 -				  Join_localTo, 
    6.47 +	      simpset() addsimps [Int_Diff, ensures_def,
    6.48 +				  givenBy_eq_Collect, Join_stable,
    6.49  				  Join_constrains, Join_transient]));
    6.50  by (blast_tac (claset() addIs [transient_strengthen]) 3);
    6.51 -by (blast_tac (claset() addDs [constrains_localTo_constrains]
    6.52 +by (ALLGOALS (dres_inst_tac [("P1","P")] (impOfSubs preserves_subset_stable)));
    6.53 +by (rewtac stable_def);
    6.54 +by (blast_tac (claset() addSEs [equalityE]
    6.55  			addIs [constrains_Int RS constrains_weaken]) 2);
    6.56 -by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
    6.57 -qed "gen_leadsETo_localTo_imp_Join_leadsETo";
    6.58 -
    6.59 -(*USED???
    6.60 -  Could replace this proof by instantiation of the one above with C=UNIV*)
    6.61 -Goal "[| F: (A leadsTo[givenBy v] B);  F Join G : v localTo[UNIV] F |] \
    6.62 -\     ==> F Join G : (A leadsTo[givenBy v] B)";
    6.63 -by (etac leadsETo_induct 1);
    6.64 -by (blast_tac (claset() addIs [leadsETo_Union]) 3);
    6.65 -by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
    6.66 -by (rtac leadsETo_Basis 1);
    6.67 -by (auto_tac (claset(),
    6.68 -	      simpset() addsimps [ensures_def, givenBy_eq_Collect,
    6.69 -				  Join_localTo, 
    6.70 -				  Join_constrains, Join_transient]));
    6.71 -by (force_tac (claset() addDs [constrains_localTo_constrains], simpset()) 1);
    6.72 -qed "leadsETo_localTo_imp_Join_leadsETo";
    6.73 +by (blast_tac (claset() addSEs [equalityE]
    6.74 +			addIs [constrains_Int RS constrains_weaken]) 1);
    6.75 +qed "gen_leadsETo_imp_Join_leadsETo";
    6.76  
    6.77  (*useful??*)
    6.78  Goal "[| F Join G : (A leadsTo[CC] B);  ALL C:CC. G : stable C |] \
    6.79 @@ -382,85 +377,54 @@
    6.80  				      extend_set_Diff_distrib RS sym]) 1);
    6.81  qed "leadsETo_imp_extend_leadsETo";
    6.82  
    6.83 -(*NOW OBSOLETE: SEE BELOW !! Generalizes the version proved in Project.ML*)
    6.84 -Goalw [LOCALTO_def, transient_def, Diff_def]
    6.85 -     "[| G : (v o f) localTo[C] extend h F;  project h C G : transient D;  \
    6.86 -\        D : givenBy v |]    \
    6.87 -\     ==> F : transient D";
    6.88 -by (auto_tac (claset(), 
    6.89 -	      simpset() addsimps [givenBy_eq_Collect]));
    6.90 -by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
    6.91 -by Auto_tac; 
    6.92 -by (rtac bexI 1);
    6.93 -by (assume_tac 2);
    6.94 -by (Blast_tac 1);
    6.95 -by (case_tac "{s. P (v s)} = {}" 1);
    6.96 -by (auto_tac (claset(),
    6.97 -	      simpset() addsimps [stable_def, constrains_def]));
    6.98 -by (subgoal_tac
    6.99 -    "ALL z. Restrict C act ^^ {s. v (f s) = z} <= {s. v (f s) = z}" 1);
   6.100 -by (blast_tac (claset() addSDs [bspec]) 2);
   6.101 -by (thin_tac "ALL z. ?P z" 1);
   6.102 -by (subgoal_tac "project_act h (Restrict C act) ^^ {s. P (v s)} <= {s. P (v s)}" 1);
   6.103 -by (Clarify_tac 2);
   6.104 -by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
   6.105 -by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 2);
   6.106 -by (blast_tac (claset() addSDs [subsetD]) 1);
   6.107 -qed "localTo_project_transient_transient";
   6.108 -
   6.109 -
   6.110 +(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
   6.111  Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
   6.112  by (auto_tac (claset() addIs [project_set_I], 
   6.113  	      simpset()));
   6.114  qed "Int_extend_set_lemma";
   6.115  
   6.116 +(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
   6.117  Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
   6.118  by (full_simp_tac (simpset() addsimps [constrains_def, project_def, 
   6.119  				       project_act_def, project_set_def]) 1);
   6.120  by (Blast_tac 1);
   6.121  qed "project_constrains_project_set";
   6.122  
   6.123 +(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
   6.124  Goal "G : stable C ==> project h C G : stable (project_set h C)";
   6.125  by (asm_full_simp_tac (simpset() addsimps [stable_def, 
   6.126  					   project_constrains_project_set]) 1);
   6.127  qed "project_stable_project_set";
   6.128  
   6.129 -(*!! Generalizes the version proved in Project.ML*)
   6.130 -Goalw [LOCALTO_def, transient_def, Diff_def]
   6.131 -     "[| G : (v o f) localTo[C] extend h F;  \
   6.132 -\        project h C G : transient (C' Int D);  \
   6.133 -\        project h C G : stable C';  \
   6.134 -\        D : givenBy v;  (C' Int D) <= D |]    \
   6.135 -\     ==> F : transient (C' Int D)";
   6.136 -by (auto_tac (claset(), 
   6.137 -	      simpset() addsimps [givenBy_eq_Collect]));
   6.138 -by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
   6.139 -by Auto_tac; 
   6.140 -by (rtac bexI 1);
   6.141 +
   6.142 +
   6.143 +(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
   6.144 +Goal "[| G : preserves (v o f);  project h C G : transient D;  \
   6.145 +\        D : givenBy v |] ==> D={}";
   6.146 +by (rtac stable_transient_empty 1);
   6.147  by (assume_tac 2);
   6.148 -by (Blast_tac 1);
   6.149 -by (case_tac "(C' Int {s. P (v s)}) = {}" 1);
   6.150 -by (auto_tac (claset(),
   6.151 -	      simpset() addsimps [stable_def, constrains_def]));
   6.152 -by (subgoal_tac
   6.153 -    "ALL z. Restrict C act ^^ {s. v (f s) = z} <= {s. v (f s) = z}" 1);
   6.154 -by (blast_tac (claset() addSDs [bspec]) 2);
   6.155 -by (thin_tac "ALL z. ?P z" 1);
   6.156 -by (subgoal_tac "project_act h (Restrict C act) ^^ (C' Int {s. P (v s)}) <= (C' Int {s. P (v s)})" 1);
   6.157 -by (Clarify_tac 2);
   6.158 -by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
   6.159 -by (thin_tac "(C' Int {s. P (v s)}) <= Domain ?A" 2);
   6.160 -by (thin_tac "?A <= -C' Un ?B" 2);
   6.161 -by (rtac conjI 2);
   6.162 -by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 3);
   6.163 -by (Blast_tac 2);
   6.164 -by (blast_tac (claset() addSDs [subsetD]) 1);
   6.165 -qed "localTo_project_transient_transient";
   6.166 +(*If addIs then PROOF FAILED at depth 2*)
   6.167 +by (blast_tac (claset() addSIs [preserves_givenBy_imp_stable,
   6.168 +				project_preserves_I]) 1);
   6.169 +result();
   6.170 +
   6.171 +(*Generalizes the version proved in Project.ML*)
   6.172 +Goal "[| G : preserves (v o f);  \
   6.173 +\        project h C G : transient (C' Int D);  \
   6.174 +\        project h C G : stable C';  D : givenBy v |]    \
   6.175 +\     ==> C' Int D = {}";
   6.176 +by (rtac stable_transient_empty 1);
   6.177 +by (assume_tac 2);
   6.178 +(*If addIs then PROOF FAILED at depth 3*)
   6.179 +by (blast_tac (claset() addSIs [stable_Int, preserves_givenBy_imp_stable,
   6.180 +				project_preserves_I]) 1);
   6.181 +qed "preserves_o_project_transient_empty";
   6.182 +
   6.183  
   6.184  (*This version's stronger in the "ensures" precondition
   6.185    BUT there's no ensures_weaken_L*)
   6.186 -Goal "[| project h C G : transient (project_set h C Int (A-B)) --> \
   6.187 -\          F : transient (project_set h C Int (A-B));  \
   6.188 +Goal "[| project h C G ~: transient (project_set h C Int (A-B)) | \
   6.189 +\          project_set h C Int (A - B) = {};  \
   6.190  \        extend h F Join G : stable C;  \
   6.191  \        F Join project h C G : (project_set h C Int A) ensures B |] \
   6.192  \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
   6.193 @@ -470,8 +434,8 @@
   6.194  qed "Join_project_ensures_strong";
   6.195  
   6.196  Goal "[| extend h F Join G : stable C;  \
   6.197 -\        F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
   6.198 -\        G : (v o f) localTo[C] extend h F |] \
   6.199 +\        F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B;  \
   6.200 +\        G : preserves (v o f) |] \
   6.201  \     ==> extend h F Join G : \
   6.202  \           (C Int extend_set h (project_set h C Int A)) \
   6.203  \           leadsTo[(%D. C Int extend_set h D)``givenBy v]  (extend_set h B)";
   6.204 @@ -486,8 +450,8 @@
   6.205  by (asm_simp_tac (simpset() addsimps [Int_Diff, Int_extend_set_lemma,
   6.206  				      extend_set_Diff_distrib RS sym]) 2);
   6.207  by (rtac Join_project_ensures_strong 1);
   6.208 -by (auto_tac (claset() addIs [localTo_project_transient_transient,
   6.209 -			      project_stable_project_set], 
   6.210 +by (auto_tac (claset() addDs [preserves_o_project_transient_empty]
   6.211 +		       addIs [project_stable_project_set], 
   6.212  	      simpset() addsimps [Int_left_absorb, Join_stable]));
   6.213  by (asm_simp_tac
   6.214      (simpset() addsimps [stable_ensures_Int RS ensures_weaken_R,
   6.215 @@ -496,33 +460,36 @@
   6.216  val lemma = result();
   6.217  
   6.218  Goal "[| extend h F Join G : stable C;  \
   6.219 -\        F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
   6.220 -\        G : (v o f) localTo[C] extend h F |] \
   6.221 +\        F Join project h C G : \
   6.222 +\            (project_set h C Int A) \
   6.223 +\            leadsTo[(%D. project_set h C Int D)``givenBy v] B;  \
   6.224 +\        G : preserves (v o f) |] \
   6.225  \     ==> extend h F Join G : (C Int extend_set h A) \
   6.226  \           leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
   6.227  by (rtac (lemma RS leadsETo_weaken) 1);
   6.228  by (auto_tac (claset() addIs [project_set_I], simpset()));
   6.229  qed "project_leadsETo_lemma";
   6.230  
   6.231 -Goal "[| F Join project h UNIV G : A leadsTo[givenBy v] B;    \
   6.232 -\        G : (v o f) localTo[UNIV] extend h F |]  \
   6.233 +Goal "[| F Join project h UNIV G : A leadsTo[givenBy v] B;  \
   6.234 +\        G : preserves (v o f) |]  \
   6.235  \     ==> extend h F Join G : (extend_set h A) \
   6.236  \           leadsTo[givenBy (v o f)] (extend_set h B)";
   6.237  by (rtac (make_elim project_leadsETo_lemma) 1);
   6.238 +by (stac stable_UNIV 1);
   6.239  by Auto_tac;
   6.240  by (etac leadsETo_givenBy 1);
   6.241  by (rtac extend_set_givenBy_subset 1);
   6.242  qed "project_leadsETo_D";
   6.243  
   6.244  Goal "[| F Join project h (reachable (extend h F Join G)) G \
   6.245 -\            : A LeadsTo[givenBy v] B;    \
   6.246 -\        G : (v o f) LocalTo extend h F |] \
   6.247 +\            : A LeadsTo[givenBy v] B;  \
   6.248 +\        G : preserves (v o f) |] \
   6.249  \     ==> extend h F Join G : \
   6.250  \           (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)";
   6.251  by (rtac (make_elim (subset_refl RS stable_reachable RS 
   6.252  		     project_leadsETo_lemma)) 1);
   6.253  by (auto_tac (claset(), 
   6.254 -	      simpset() addsimps [LeadsETo_def, LocalTo_def]));
   6.255 +	      simpset() addsimps [LeadsETo_def]));
   6.256  by (asm_full_simp_tac 
   6.257      (simpset() addsimps [project_set_reachable_extend_eq RS sym]) 1);
   6.258  by (etac (impOfSubs leadsETo_mono) 1);
   6.259 @@ -530,24 +497,18 @@
   6.260  qed "project_LeadsETo_D";
   6.261  
   6.262  Goalw [extending_def]
   6.263 -     "extending (%G. UNIV) h F \
   6.264 -\               ((v o f) localTo[UNIV] extend h F) \
   6.265 +     "extending (v o f) (%G. UNIV) h F \
   6.266  \               (extend_set h A leadsTo[givenBy (v o f)] extend_set h B) \
   6.267  \               (A leadsTo[givenBy v] B)";
   6.268 -by (auto_tac (claset(), 
   6.269 -	      simpset() addsimps [project_leadsETo_D, Join_localTo]));
   6.270 +by (auto_tac (claset(), simpset() addsimps [project_leadsETo_D]));
   6.271  qed "extending_leadsETo";
   6.272  
   6.273  
   6.274  Goalw [extending_def]
   6.275 -     "extending (%G. reachable (extend h F Join G)) h F \
   6.276 -\               ((v o f) LocalTo extend h F) \
   6.277 +     "extending (v o f) (%G. reachable (extend h F Join G)) h F \
   6.278  \               (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B) \
   6.279  \               (A LeadsTo[givenBy v]  B)";
   6.280 -
   6.281 -by (force_tac (claset() addIs [project_LeadsETo_D],
   6.282 -	       simpset()addsimps [LocalTo_def, Join_assoc RS sym, 
   6.283 -				  Join_localTo]) 1);
   6.284 +by (blast_tac (claset() addIs [project_LeadsETo_D]) 1);
   6.285  qed "extending_LeadsETo";
   6.286  
   6.287  
     7.1 --- a/src/HOL/UNITY/ELT.thy	Wed Dec 08 13:52:36 1999 +0100
     7.2 +++ b/src/HOL/UNITY/ELT.thy	Wed Dec 08 13:53:29 1999 +0100
     7.3 @@ -32,9 +32,6 @@
     7.4    givenBy :: "['a => 'b] => 'a set set"
     7.5      "givenBy f == range (%B. f-`` B)"
     7.6  
     7.7 -  funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
     7.8 -    "funPair f g == %x. (f x, g x)"
     7.9 -
    7.10    (*visible version of the LEADS-TO relation*)
    7.11    leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
    7.12                                          ("(3_/ leadsTo[_]/ _)" [80,0,80] 80)
     8.1 --- a/src/HOL/UNITY/Extend.ML	Wed Dec 08 13:52:36 1999 +0100
     8.2 +++ b/src/HOL/UNITY/Extend.ML	Wed Dec 08 13:53:29 1999 +0100
     8.3 @@ -159,7 +159,7 @@
     8.4  (*** More laws ***)
     8.5  
     8.6  (*Because A and B could differ on the "other" part of the state, 
     8.7 -   cannot generalize result to 
     8.8 +   cannot generalize to 
     8.9        project_set h (A Int B) = project_set h A Int project_set h B
    8.10  *)
    8.11  Goalw [project_set_def]
    8.12 @@ -167,6 +167,11 @@
    8.13  by Auto_tac;
    8.14  qed "project_set_extend_set_Int";
    8.15  
    8.16 +Goalw [project_set_def]
    8.17 +     "project_set h (A Int B) <= (project_set h A) Int (project_set h B)";
    8.18 +by Auto_tac;
    8.19 +qed "project_set_Int_subset";
    8.20 +
    8.21  Goal "extend_set h (A Un B) = extend_set h A Un extend_set h B";
    8.22  by Auto_tac;
    8.23  qed "extend_set_Un_distrib";
    8.24 @@ -207,6 +212,11 @@
    8.25  qed "extend_act_D";
    8.26  
    8.27  Goalw [extend_act_def, project_act_def, project_set_def]
    8.28 +     "project_act h (extend_act h act) = act";
    8.29 +by (Blast_tac 1);
    8.30 +qed "project_act_extend_act";
    8.31 +
    8.32 +Goalw [extend_act_def, project_act_def, project_set_def]
    8.33       "project_act h (Restrict C (extend_act h act)) = \
    8.34  \     Restrict (project_set h C) act";
    8.35  by (Blast_tac 1);
    8.36 @@ -405,97 +415,6 @@
    8.37  qed "extend_stable_project_set";
    8.38  
    8.39  
    8.40 -(*** Diff, needed for localTo ***)
    8.41 -
    8.42 -Goal "Restrict (extend_set h C) (extend_act h act) = \
    8.43 -\     extend_act h (Restrict C act)";
    8.44 -by (auto_tac (claset(), 
    8.45 -              simpset() addsimps [split_extended_all]));
    8.46 -by (auto_tac (claset(), 
    8.47 -              simpset() addsimps [extend_act_def]));
    8.48 -qed "Restrict_extend_set";
    8.49 -
    8.50 -Goalw [Diff_def]
    8.51 -     "(Diff (extend_set h C) (extend h G) (extend_act h `` acts)) = \
    8.52 -\     extend h (Diff C G acts)";
    8.53 -by (rtac program_equalityI 1);
    8.54 -by (Simp_tac 1);
    8.55 -by (simp_tac (simpset() addsimps [inj_extend_act RS image_set_diff]) 1);
    8.56 -by (simp_tac (simpset() addsimps [image_eq_UN,
    8.57 -				  Restrict_extend_set]) 1);
    8.58 -qed "Diff_extend_eq";
    8.59 -
    8.60 -(*Opposite inclusion fails; this inclusion's more general than that of
    8.61 -  Diff_extend_eq*)     
    8.62 -Goal "Diff (project_set h C) G acts \
    8.63 -\     <= project h C (Diff C (extend h G) (extend_act h `` acts))";
    8.64 -by (simp_tac
    8.65 -    (simpset() addsimps [component_eq_subset, Diff_def,image_UN,
    8.66 -			 image_image, image_Diff_image_eq,
    8.67 -			 Restrict_extend_act_eq_Restrict_project_act,
    8.68 -			 vimage_image_eq]) 1);
    8.69 -by  (blast_tac (claset() addSEs [equalityE])1);
    8.70 -qed "Diff_project_set_component";
    8.71 -
    8.72 -Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
    8.73 -\         : (extend_set h A) co (extend_set h B)) \
    8.74 -\     = (Diff C G acts : A co B)";
    8.75 -by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
    8.76 -qed "Diff_extend_constrains";
    8.77 -
    8.78 -Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
    8.79 -\       : stable (extend_set h A)) \
    8.80 -\     = (Diff C G acts : stable A)";
    8.81 -by (simp_tac (simpset() addsimps [Diff_extend_constrains, stable_def]) 1);
    8.82 -qed "Diff_extend_stable";
    8.83 -
    8.84 -(*UNUSED!!*)
    8.85 -Goal "Diff (extend_set h C) (extend h G) (extend_act h `` acts) : A co B \
    8.86 -\     ==> Diff C G acts : (project_set h A) co (project_set h B)";
    8.87 -by (asm_full_simp_tac (simpset() addsimps [Diff_extend_eq, 
    8.88 -					   extend_constrains_project_set]) 1);
    8.89 -qed "Diff_extend_constrains_project_set";
    8.90 -
    8.91 -Goalw [LOCALTO_def]
    8.92 -     "(extend h F : (v o f) localTo[extend_set h C] extend h H) = \
    8.93 -\     (F : v localTo[C] H)";
    8.94 -by (Simp_tac 1);
    8.95 -(*A trick to strip both quantifiers*)
    8.96 -by (res_inst_tac [("f", "All")] (ext RS arg_cong) 1);
    8.97 -by (stac Collect_eq_extend_set 1);
    8.98 -by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
    8.99 -qed "extend_localTo_extend_eq";
   8.100 -
   8.101 -Goal "[| F : v localTo[C] H;  C' <= extend_set h C |] \
   8.102 -\     ==> extend h F : (v o f) localTo[C'] extend h H";
   8.103 -by (blast_tac (claset() addDs [extend_localTo_extend_eq RS iffD2,
   8.104 -			       impOfSubs localTo_anti_mono]) 1);
   8.105 -qed "extend_localTo_extend_I";
   8.106 -
   8.107 -(*USED?? opposite inclusion fails*)
   8.108 -Goal "Restrict C (extend_act h act) <= \
   8.109 -\     extend_act h (Restrict (project_set h C) act)";
   8.110 -by (auto_tac (claset(), 
   8.111 -              simpset() addsimps [split_extended_all]));
   8.112 -by (auto_tac (claset(), 
   8.113 -              simpset() addsimps [extend_act_def, project_set_def]));
   8.114 -qed "Restrict_extend_set_subset";
   8.115 -
   8.116 -
   8.117 -Goal "(extend_act h `` Acts F) - {Id} = extend_act h `` (Acts F - {Id})";
   8.118 -by (stac (extend_act_Id RS sym) 1);
   8.119 -by (simp_tac (simpset() addsimps [inj_extend_act RS image_set_diff]) 1);
   8.120 -qed "extend_act_image_Id_eq";
   8.121 -
   8.122 -Goal "Disjoint C (extend h F) (extend h G) = Disjoint (project_set h C) F G";
   8.123 -by (simp_tac
   8.124 -    (simpset() addsimps [Disjoint_def, disjoint_iff_not_equal,
   8.125 -			 image_Diff_image_eq,
   8.126 -			 Restrict_extend_act_eq_Restrict_project_act,
   8.127 -			 extend_act_Id_iff, vimage_def]) 1);
   8.128 -qed "Disjoint_extend_eq";
   8.129 -Addsimps [Disjoint_extend_eq];
   8.130 -
   8.131  (*** Weak safety primitives: Co, Stable ***)
   8.132  
   8.133  Goal "p : reachable (extend h F) ==> f p : reachable F";
     9.1 --- a/src/HOL/UNITY/Guar.ML	Wed Dec 08 13:52:36 1999 +0100
     9.2 +++ b/src/HOL/UNITY/Guar.ML	Wed Dec 08 13:53:29 1999 +0100
     9.3 @@ -65,82 +65,79 @@
     9.4  (*** guarantees ***)
     9.5  
     9.6  val prems = Goal
     9.7 -     "(!!G. [| F Join G : X;  Disjoint UNIV F G |] ==> F Join G : Y) \
     9.8 -\     ==> F : X guarantees Y";
     9.9 -by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
    9.10 +     "(!!G. [| G : preserves v; F Join G : X |] ==> F Join G : Y) \
    9.11 +\     ==> F : X guarantees[v] Y";
    9.12 +by (simp_tac (simpset() addsimps [guar_def, component_def]) 1);
    9.13  by (blast_tac (claset() addIs prems) 1);
    9.14  qed "guaranteesI";
    9.15  
    9.16  Goalw [guar_def, component_def]
    9.17 -     "[| F : X guarantees Y;  F Join G : X |] ==> F Join G : Y";
    9.18 +     "[| F : X guarantees[v] Y;  G : preserves v;  F Join G : X |] \
    9.19 +\     ==> F Join G : Y";
    9.20  by (Blast_tac 1);
    9.21  qed "guaranteesD";
    9.22  
    9.23  (*This version of guaranteesD matches more easily in the conclusion*)
    9.24  Goalw [guar_def]
    9.25 -     "[| F : X guarantees Y;  H : X;  F <= H |] ==> H : Y";
    9.26 +     "[| F : X guarantees[v] Y;  H : X;  H = F Join G;  G : preserves v |] \
    9.27 +\     ==> H : Y";
    9.28  by (Blast_tac 1);
    9.29  qed "component_guaranteesD";
    9.30  
    9.31 -(*This equation is more intuitive than the official definition*)
    9.32 -Goal "(F : X guarantees Y) = \
    9.33 -\     (ALL G. F Join G : X & Disjoint UNIV F G --> F Join G : Y)";
    9.34 -by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
    9.35 -by (Blast_tac 1);
    9.36 -qed "guarantees_eq";
    9.37 -
    9.38  Goalw [guar_def]
    9.39 -     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
    9.40 +     "[| F: X guarantees[v] X'; Y <= X; X' <= Y' |] ==> F: Y guarantees[v] Y'";
    9.41  by (Blast_tac 1);
    9.42  qed "guarantees_weaken";
    9.43  
    9.44  Goalw [guar_def]
    9.45 -     "[| F: X guarantees Y; F <= F' |] ==> F': X guarantees Y";
    9.46 -by (blast_tac (claset() addIs [component_trans]) 1);
    9.47 -qed "guarantees_weaken_prog";
    9.48 +     "[| F: X guarantees[v] Y;  preserves w <= preserves v |] \
    9.49 +\     ==> F: X guarantees[w] Y";
    9.50 +by (Blast_tac 1);
    9.51 +qed "guarantees_weaken_var";
    9.52  
    9.53 -Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
    9.54 +Goalw [guar_def] "X <= Y ==> X guarantees[v] Y = UNIV";
    9.55  by (Blast_tac 1);
    9.56  qed "subset_imp_guarantees_UNIV";
    9.57  
    9.58  (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
    9.59 -Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
    9.60 +Goalw [guar_def] "X <= Y ==> F : X guarantees[v] Y";
    9.61  by (Blast_tac 1);
    9.62  qed "subset_imp_guarantees";
    9.63  
    9.64 -(*Remark at end of section 4.1*)
    9.65 -Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
    9.66 +(*Remark at end of section 4.1
    9.67 +Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees[v] Y)";
    9.68  by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
    9.69  by (blast_tac (claset() addEs [equalityE]) 1);
    9.70  qed "ex_prop_equiv2";
    9.71 +*)
    9.72  
    9.73  (** Distributive laws.  Re-orient to perform miniscoping **)
    9.74  
    9.75  Goalw [guar_def]
    9.76 -     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
    9.77 +     "(UN i:I. X i) guarantees[v] Y = (INT i:I. X i guarantees[v] Y)";
    9.78  by (Blast_tac 1);
    9.79  qed "guarantees_UN_left";
    9.80  
    9.81  Goalw [guar_def]
    9.82 -    "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
    9.83 +    "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
    9.84  by (Blast_tac 1);
    9.85  qed "guarantees_Un_left";
    9.86  
    9.87  Goalw [guar_def]
    9.88 -     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
    9.89 +     "X guarantees[v] (INT i:I. Y i) = (INT i:I. X guarantees[v] Y i)";
    9.90  by (Blast_tac 1);
    9.91  qed "guarantees_INT_right";
    9.92  
    9.93  Goalw [guar_def]
    9.94 -    "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
    9.95 +    "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
    9.96  by (Blast_tac 1);
    9.97  qed "guarantees_Int_right";
    9.98  
    9.99 -Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
   9.100 +Goalw [guar_def] "(X guarantees[v] Y) = (UNIV guarantees[v] (-X Un Y))";
   9.101  by (Blast_tac 1);
   9.102  qed "shunting";
   9.103  
   9.104 -Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
   9.105 +Goalw [guar_def] "(X guarantees[v] Y) = -Y guarantees[v] -X";
   9.106  by (Blast_tac 1);
   9.107  qed "contrapositive";
   9.108  
   9.109 @@ -149,78 +146,108 @@
   9.110  **)
   9.111  
   9.112  Goalw [guar_def]
   9.113 -    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
   9.114 -\    ==> F : (V Int Y) guarantees Z";
   9.115 +    "[| F : V guarantees[v] X;  F : (X Int Y) guarantees[v] Z |]\
   9.116 +\    ==> F : (V Int Y) guarantees[v] Z";
   9.117  by (Blast_tac 1);
   9.118  qed "combining1";
   9.119  
   9.120  Goalw [guar_def]
   9.121 -    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
   9.122 -\    ==> F : V guarantees (X Un Z)";
   9.123 +    "[| F : V guarantees[v] (X Un Y);  F : Y guarantees[v] Z |]\
   9.124 +\    ==> F : V guarantees[v] (X Un Z)";
   9.125  by (Blast_tac 1);
   9.126  qed "combining2";
   9.127  
   9.128  (** The following two follow Chandy-Sanders, but the use of object-quantifiers
   9.129      does not suit Isabelle... **)
   9.130  
   9.131 -(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
   9.132 +(*Premise should be (!!i. i: I ==> F: X guarantees[v] Y i) *)
   9.133  Goalw [guar_def]
   9.134 -     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
   9.135 +     "ALL i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (INT i:I. Y i)";
   9.136  by (Blast_tac 1);
   9.137  qed "all_guarantees";
   9.138  
   9.139 -(*Premises should be [| F: X guarantees Y i; i: I |] *)
   9.140 +(*Premises should be [| F: X guarantees[v] Y i; i: I |] *)
   9.141  Goalw [guar_def]
   9.142 -     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
   9.143 +     "EX i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (UN i:I. Y i)";
   9.144  by (Blast_tac 1);
   9.145  qed "ex_guarantees";
   9.146  
   9.147  (*** Additional guarantees laws, by lcp ***)
   9.148  
   9.149  Goalw [guar_def]
   9.150 -    "[| F: U guarantees V;  G: X guarantees Y |] \
   9.151 -\    ==> F Join G: (U Int X) guarantees (V Int Y)";
   9.152 -by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
   9.153 -by (Blast_tac 1);
   9.154 +    "[| F: U guarantees[v] V;  G: X guarantees[v] Y; \
   9.155 +\       F : preserves v;  G : preserves v |] \
   9.156 +\    ==> F Join G: (U Int X) guarantees[v] (V Int Y)";
   9.157 +by (Simp_tac 1);
   9.158 +by Safe_tac;
   9.159 +by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1);
   9.160 +by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
   9.161 +by (asm_full_simp_tac (simpset() addsimps [Join_preserves]) 1);
   9.162 +by (asm_simp_tac (simpset() addsimps Join_ac) 1);
   9.163  qed "guarantees_Join_Int";
   9.164  
   9.165  Goalw [guar_def]
   9.166 -    "[| F: U guarantees V;  G: X guarantees Y |]  \
   9.167 -\    ==> F Join G: (U Un X) guarantees (V Un Y)";
   9.168 -by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
   9.169 -by (Blast_tac 1);
   9.170 +    "[| F: U guarantees[v] V;  G: X guarantees[v] Y; \
   9.171 +\       F : preserves v;  G : preserves v |]  \
   9.172 +\    ==> F Join G: (U Un X) guarantees[v] (V Un Y)";
   9.173 +by (Simp_tac 1);
   9.174 +by Safe_tac;
   9.175 +by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1);
   9.176 +by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
   9.177 +by (asm_full_simp_tac (simpset() addsimps [Join_preserves]) 1);
   9.178 +by (asm_simp_tac (simpset() addsimps Join_ac) 1);
   9.179  qed "guarantees_Join_Un";
   9.180  
   9.181  Goalw [guar_def]
   9.182 -    "[| ALL i:I. F i : X i guarantees Y i |] \
   9.183 -\    ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
   9.184 -by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
   9.185 -by (Blast_tac 1);
   9.186 -bind_thm ("guarantees_JN_INT", ballI RS result());
   9.187 +    "[| ALL i:I. F i : X i guarantees[v] Y i;  \
   9.188 +\       ALL i:I. F i : preserves v |] \
   9.189 +\    ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)";
   9.190 +by Auto_tac;
   9.191 +by (ball_tac 1);
   9.192 +by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1);
   9.193 +by (asm_full_simp_tac (simpset() addsimps [Join_assoc RS sym, JN_absorb, 
   9.194 +					   Join_preserves, JN_preserves]) 1);
   9.195 +qed "guarantees_JN_INT";
   9.196  
   9.197  Goalw [guar_def]
   9.198 -    "[| ALL i:I. F i : X i guarantees Y i |] \
   9.199 -\    ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
   9.200 -by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
   9.201 -by (Blast_tac 1);
   9.202 -bind_thm ("guarantees_JN_UN", ballI RS result());
   9.203 +    "[| ALL i:I. F i : X i guarantees[v] Y i;  \
   9.204 +\       ALL i:I. F i : preserves v |] \
   9.205 +\    ==> (JOIN I F) : (UNION I X) guarantees[v] (UNION I Y)";
   9.206 +by Auto_tac;
   9.207 +by (ball_tac 1);
   9.208 +by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1);
   9.209 +by (auto_tac
   9.210 +    (claset(),
   9.211 +     simpset() addsimps [Join_assoc RS sym, JN_absorb, 
   9.212 +			 Join_preserves, JN_preserves]));
   9.213 +qed "guarantees_JN_UN";
   9.214  
   9.215  
   9.216 -(*** guarantees laws for breaking down the program, by lcp ***)
   9.217 +(*** guarantees[v] laws for breaking down the program, by lcp ***)
   9.218  
   9.219  Goalw [guar_def]
   9.220 -    "F: X guarantees Y | G: X guarantees Y ==> F Join G: X guarantees Y";
   9.221 -by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
   9.222 -by (Blast_tac 1);
   9.223 -qed "guarantees_Join_I";
   9.224 +     "[| F: X guarantees[v] Y;  G: preserves v |] \
   9.225 +\     ==> F Join G: X guarantees[v] Y";
   9.226 +by (Simp_tac 1);
   9.227 +by Safe_tac;
   9.228 +by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1);
   9.229 +qed "guarantees_Join_I1";
   9.230  
   9.231 -bind_thm ("guarantees_Join_I1", disjI1 RS guarantees_Join_I);
   9.232 -bind_thm ("guarantees_Join_I2", disjI2 RS guarantees_Join_I);
   9.233 +Goal "[| G: X guarantees[v] Y;  F: preserves v |] \
   9.234 +\    ==> F Join G: X guarantees[v] Y";
   9.235 +by (stac Join_commute 1);
   9.236 +by (blast_tac (claset() addIs [guarantees_Join_I1]) 1);
   9.237 +qed "guarantees_Join_I2";
   9.238  
   9.239  Goalw [guar_def]
   9.240 -     "[| i : I;  F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y";
   9.241 -by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
   9.242 -by (Blast_tac 1);
   9.243 +     "[| i : I;  F i: X guarantees[v] Y;  \
   9.244 +\        ALL j:I. i~=j --> F j : preserves v |] \
   9.245 +\     ==> (JN i:I. (F i)) : X guarantees[v] Y";
   9.246 +by (Clarify_tac 1);
   9.247 +by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
   9.248 +by (auto_tac (claset(),
   9.249 +	      simpset() addsimps [JN_Join_diff, Join_assoc RS sym, 
   9.250 +				  Join_preserves, JN_preserves]));
   9.251  qed "guarantees_JN_I";
   9.252  
   9.253  
    10.1 --- a/src/HOL/UNITY/Guar.thy	Wed Dec 08 13:52:36 1999 +0100
    10.2 +++ b/src/HOL/UNITY/Guar.thy	Wed Dec 08 13:53:29 1999 +0100
    10.3 @@ -35,9 +35,11 @@
    10.4    welldef :: 'a program set  
    10.5     "welldef == {F. Init F ~= {}}"
    10.6  
    10.7 -  guar :: ['a program set, 'a program set] => 'a program set
    10.8 -   (infixl "guarantees" 55)    (*higher than membership, lower than Co*)
    10.9 -   "X guarantees Y == {F. ALL H. F <= H --> H:X --> H:Y}"
   10.10 +  guar :: ['a program set, 'a=>'b, 'a program set] => 'a program set
   10.11 +   ("(_/ guarantees[_]/ _)" [55,0,55] 55)
   10.12 +                              (*higher than membership, lower than Co*)
   10.13 +   "X guarantees[v] Y == {F. ALL G. G : preserves v --> F Join G : X -->
   10.14 +		       F Join G : Y}"
   10.15  
   10.16    refines :: ['a program, 'a program, 'a program set] => bool
   10.17  			("(3_ refines _ wrt _)" [10,10,10] 10)
    11.1 --- a/src/HOL/UNITY/Lift_prog.ML	Wed Dec 08 13:52:36 1999 +0100
    11.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Wed Dec 08 13:53:29 1999 +0100
    11.3 @@ -85,6 +85,11 @@
    11.4  qed "sub_vimage";
    11.5  Addsimps [sub_vimage];
    11.6  
    11.7 +(*For tidying the result of "export"*)
    11.8 +Goal "v o (%z. z i) = v o sub i";
    11.9 +by (simp_tac (simpset() addsimps [sub_def]) 1);
   11.10 +qed "fold_o_sub";
   11.11 +
   11.12  
   11.13  
   11.14  (*** lift_prog and the lattice operations ***)
   11.15 @@ -115,7 +120,9 @@
   11.16  by Auto_tac;
   11.17  qed "good_map_lift_map";
   11.18  
   11.19 -fun lift_export th = good_map_lift_map RS export th;
   11.20 +fun lift_export th = 
   11.21 +    good_map_lift_map RS export th 
   11.22 +       |> simplify (simpset() addsimps [fold_o_sub]);;
   11.23  
   11.24  Goal "fst (inv (lift_map i) g) = g i";
   11.25  by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1);
   11.26 @@ -293,23 +300,6 @@
   11.27  qed "drop_prog_stable";
   11.28  
   11.29  
   11.30 -(*** Diff, needed for localTo ***)
   11.31 -
   11.32 -Goal "[| Diff C G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |] \
   11.33 -\     ==> Diff (drop_set i C) (drop_prog i C G) acts : A co B";
   11.34 -by (asm_full_simp_tac
   11.35 -    (simpset() addsimps [drop_set_correct, drop_prog_correct, 
   11.36 -			 lift_set_correct, lift_act_correct, 
   11.37 -			 lift_export Diff_project_constrains]) 1);
   11.38 -qed "Diff_drop_prog_constrains";
   11.39 -
   11.40 -Goalw [stable_def]
   11.41 -     "[| Diff C G (lift_act i `` acts) : stable (lift_set i A) |]  \
   11.42 -\     ==> Diff (drop_set i C) (drop_prog i C G) acts : stable A";
   11.43 -by (blast_tac (claset() addIs [Diff_drop_prog_constrains]) 1);
   11.44 -qed "Diff_drop_prog_stable";
   11.45 -
   11.46 -
   11.47  (*** Weak safety primitives: Co, Stable ***)
   11.48  
   11.49  (** Reachability **)
   11.50 @@ -391,24 +381,33 @@
   11.51  
   11.52  (*** guarantees properties ***)
   11.53  
   11.54 +Goal "G : preserves (v o sub i) ==> drop_prog i C G : preserves v";
   11.55 +by (asm_simp_tac
   11.56 +    (simpset() addsimps [drop_prog_correct, fold_o_sub,
   11.57 +			 lift_export project_preserves_I]) 1);
   11.58 +qed "drop_prog_preserves_I";
   11.59 +
   11.60  (*The raw version*)
   11.61  val [xguary,drop_prog,lift_prog] =
   11.62 -Goal "[| F : X guarantees Y;  \
   11.63 -\        !!G. lift_prog i F Join G : X' ==> F Join proj G i G : X;  \
   11.64 -\        !!G. [| F Join proj G i G : Y; lift_prog i F Join G : X' |] \
   11.65 +Goal "[| F : X guarantees[v] Y;  \
   11.66 +\        !!G. lift_prog i F Join G : X' ==> F Join drop_prog i C G : X;  \
   11.67 +\        !!G. [| F Join drop_prog i C G : Y; lift_prog i F Join G : X' |] \
   11.68  \             ==> lift_prog i F Join G : Y' |] \
   11.69 -\     ==> lift_prog i F : X' guarantees Y'";
   11.70 +\     ==> lift_prog i F : X' guarantees[v o sub i] Y'";
   11.71  by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
   11.72 +by (etac drop_prog_preserves_I 1);
   11.73  by (etac drop_prog 1);
   11.74  by (assume_tac 1);
   11.75  qed "drop_prog_guarantees_raw";
   11.76  
   11.77 -Goal "[| F : X guarantees Y;  \
   11.78 -\        projecting C (lift_map i) F X' X;  \
   11.79 -\        extending  C (lift_map i) F X' Y' Y |] \
   11.80 -\     ==> lift_prog i F : X' guarantees Y'";
   11.81 -by (asm_simp_tac 
   11.82 -    (simpset() addsimps [lift_prog_correct, project_guarantees]) 1);
   11.83 +Goal "[| F : X guarantees[v] Y;  \
   11.84 +\        projecting  C (lift_map i) F X' X;  \
   11.85 +\        extending w C (lift_map i) F Y' Y; \
   11.86 +\        preserves w <= preserves (v o sub i) |] \
   11.87 +\     ==> lift_prog i F : X' guarantees[w] Y'";
   11.88 +by (asm_simp_tac
   11.89 +    (simpset() addsimps [lift_prog_correct, fold_o_sub,
   11.90 +			 lift_export project_guarantees]) 1);
   11.91  qed "drop_prog_guarantees";
   11.92  
   11.93  
   11.94 @@ -431,35 +430,21 @@
   11.95  
   11.96  (*** guarantees corollaries ***)
   11.97  
   11.98 -Goal "F : UNIV guarantees increasing f \
   11.99 -\     ==> lift_prog i F : UNIV guarantees increasing (f o sub i)";
  11.100 +Goal "F : UNIV guarantees[v] increasing func \
  11.101 +\   ==> lift_prog i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
  11.102  by (dtac (lift_export extend_guar_increasing) 1);
  11.103  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
  11.104  qed "lift_prog_guar_increasing";
  11.105  
  11.106 -Goal "F : UNIV guarantees Increasing f \
  11.107 -\     ==> lift_prog i F : UNIV guarantees Increasing (f o sub i)";
  11.108 +Goal "F : UNIV guarantees[v] Increasing func \
  11.109 +\   ==> lift_prog i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
  11.110  by (dtac (lift_export extend_guar_Increasing) 1);
  11.111  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
  11.112  qed "lift_prog_guar_Increasing";
  11.113  
  11.114 -Goal "F : (v localTo[UNIV] G) guarantees increasing func  \
  11.115 -\     ==> lift_prog i F : (v o sub i) localTo[UNIV] (lift_prog i G)  \
  11.116 -\                         guarantees increasing (func o sub i)";
  11.117 -by (dtac (lift_export extend_localTo_guar_increasing) 1);
  11.118 -by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
  11.119 -qed "lift_prog_localTo_guar_increasing";
  11.120 -
  11.121 -Goal "[| F : (v LocalTo H) guarantees Increasing func;  H <= F |]  \
  11.122 -\     ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i H)  \
  11.123 -\                         guarantees Increasing (func o sub i)";
  11.124 -by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
  11.125 -by (auto_tac (claset(),
  11.126 -	      simpset() addsimps [lift_prog_correct, o_def]));
  11.127 -qed "lift_prog_LocalTo_guar_Increasing";
  11.128 -
  11.129 -Goal "F : Always A guarantees Always B \
  11.130 -\ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
  11.131 +Goal "F : Always A guarantees[v] Always B \
  11.132 +\ ==> lift_prog i F : \
  11.133 +\       Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)";
  11.134  by (asm_simp_tac
  11.135      (simpset() addsimps [lift_set_correct, lift_prog_correct, 
  11.136  			 lift_export extend_guar_Always]) 1);
    12.1 --- a/src/HOL/UNITY/PPROD.ML	Wed Dec 08 13:52:36 1999 +0100
    12.2 +++ b/src/HOL/UNITY/PPROD.ML	Wed Dec 08 13:53:29 1999 +0100
    12.3 @@ -126,15 +126,6 @@
    12.4  qed "const_PLam_invariant";
    12.5  
    12.6  
    12.7 -(** localTo **)
    12.8 -
    12.9 -Goal "(PLam I F) : (sub i) localTo[C] lift_prog i (F i)";
   12.10 -by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def, 
   12.11 -				  stable_def, constrains_def]) 1);
   12.12 -by (Force_tac 1);
   12.13 -qed "PLam_sub_localTo";
   12.14 -
   12.15 -
   12.16  (** Reachability **)
   12.17  
   12.18  Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)";
   12.19 @@ -286,7 +277,8 @@
   12.20  (*** guarantees properties ***)
   12.21  
   12.22  Goalw [PLam_def]
   12.23 -    "[| lift_prog i (F i): X guarantees Y;  i : I |]  \
   12.24 -\    ==> (PLam I F) : X guarantees Y";
   12.25 +    "[| lift_prog i (F i): X guarantees[v] Y;  i : I;  \
   12.26 +\        ALL j:I. i~=j --> lift_prog j (F j) : preserves v |]  \
   12.27 +\    ==> (PLam I F) : X guarantees[v] Y";
   12.28  by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
   12.29  qed "guarantees_PLam_I";
    13.1 --- a/src/HOL/UNITY/Project.ML	Wed Dec 08 13:52:36 1999 +0100
    13.2 +++ b/src/HOL/UNITY/Project.ML	Wed Dec 08 13:53:29 1999 +0100
    13.3 @@ -6,6 +6,8 @@
    13.4  Projections of state sets (also of actions and programs)
    13.5  
    13.6  Inheritance of GUARANTEES properties under extension
    13.7 +
    13.8 +POSSIBLY CAN DELETE Restrict_image_Diff
    13.9  *)
   13.10  
   13.11  Open_locale "Extend";
   13.12 @@ -157,34 +159,31 @@
   13.13  qed "projecting_weaken";
   13.14  
   13.15  Goalw [extending_def]
   13.16 -     "[| extending C h F X' YA' YA;  extending C h F X' YB' YB |] \
   13.17 -\     ==> extending C h F X' (YA' Int YB') (YA Int YB)";
   13.18 +     "[| extending v C h F YA' YA;  extending v C h F YB' YB |] \
   13.19 +\     ==> extending v C h F (YA' Int YB') (YA Int YB)";
   13.20  by (Blast_tac 1);
   13.21  qed "extending_Int";
   13.22  
   13.23  Goalw [extending_def]
   13.24 -     "[| extending C h F X' YA' YA;  extending C h F X' YB' YB |] \
   13.25 -\     ==> extending C h F X' (YA' Un YB') (YA Un YB)";
   13.26 +     "[| extending v C h F YA' YA;  extending v C h F YB' YB |] \
   13.27 +\     ==> extending v C h F (YA' Un YB') (YA Un YB)";
   13.28  by (Blast_tac 1);
   13.29  qed "extending_Un";
   13.30  
   13.31 -(*This is the right way to handle the X' argument.  Having (INT i:I. X' i)
   13.32 -  would strengthen the premise.*)
   13.33  val [prem] = Goalw [extending_def]
   13.34 -     "[| !!i. i:I ==> extending C h F X' (Y' i) (Y i) |] \
   13.35 -\     ==> extending C h F X' (INT i:I. Y' i) (INT i:I. Y i)";
   13.36 +     "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
   13.37 +\     ==> extending v C h F (INT i:I. Y' i) (INT i:I. Y i)";
   13.38  by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
   13.39  qed "extending_INT";
   13.40  
   13.41  val [prem] = Goalw [extending_def]
   13.42 -     "[| !!i. i:I ==> extending C h F X' (Y' i) (Y i) |] \
   13.43 -\     ==> extending C h F X' (UN i:I. Y' i) (UN i:I. Y i)";
   13.44 +     "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
   13.45 +\     ==> extending v C h F (UN i:I. Y' i) (UN i:I. Y i)";
   13.46  by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
   13.47  qed "extending_UN";
   13.48  
   13.49  Goalw [extending_def]
   13.50 -     "[| extending C h F X' Y' Y;  U'<= X';  Y'<=V';  V<=Y |] \
   13.51 -\     ==> extending C h F U' V' V";
   13.52 +     "[| extending v C h F Y' Y;  Y'<=V';  V<=Y |] ==> extending v C h F V' V";
   13.53  by Auto_tac;
   13.54  qed "extending_weaken";
   13.55  
   13.56 @@ -207,133 +206,38 @@
   13.57  by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
   13.58  qed "projecting_increasing";
   13.59  
   13.60 -Goal "extending C h F X' UNIV Y";
   13.61 +Goal "extending v C h F UNIV Y";
   13.62  by (simp_tac (simpset() addsimps [extending_def]) 1);
   13.63  qed "extending_UNIV";
   13.64  
   13.65  Goalw [extending_def]
   13.66 -     "extending (%G. UNIV) h F X' (extend_set h A co extend_set h B) (A co B)";
   13.67 +     "extending v (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)";
   13.68  by (blast_tac (claset() addIs [project_constrains_D]) 1);
   13.69  qed "extending_constrains";
   13.70  
   13.71  Goalw [stable_def]
   13.72 -     "extending (%G. UNIV) h F X' (stable (extend_set h A)) (stable A)";
   13.73 +     "extending v (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
   13.74  by (rtac extending_constrains 1);
   13.75  qed "extending_stable";
   13.76  
   13.77  Goalw [extending_def]
   13.78 -     "extending (%G. UNIV) h F X' (increasing (func o f)) (increasing func)";
   13.79 +     "extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
   13.80  by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
   13.81  qed "extending_increasing";
   13.82  
   13.83 -
   13.84 -(*** Diff, needed for localTo ***)
   13.85 -
   13.86 -(*Opposite direction fails because Diff in the extended state may remove
   13.87 -  fewer actions, i.e. those that affect other state variables.*)
   13.88 -
   13.89 +(*UNUSED*)
   13.90  Goalw [project_set_def, project_act_def]
   13.91       "Restrict (project_set h C) (project_act h (Restrict C act)) = \
   13.92  \     project_act h (Restrict C act)";
   13.93  by (Blast_tac 1);
   13.94  qed "Restrict_project_act";
   13.95  
   13.96 +(*UNUSED*)
   13.97  Goalw [project_set_def, project_act_def]
   13.98       "project_act h (Restrict C Id) = Restrict (project_set h C) Id";
   13.99  by (Blast_tac 1);
  13.100  qed "project_act_Restrict_Id";
  13.101  
  13.102 -Goal
  13.103 -  "Diff(project_set h C)(project h C G)(project_act h `` Restrict C `` acts) \
  13.104 -\  <= project h C (Diff C G acts)";
  13.105 -by (simp_tac 
  13.106 -    (simpset() addsimps [component_eq_subset, Diff_def,
  13.107 -			 project_act_Restrict_Id, Restrict_image_Diff]) 1);
  13.108 -by (force_tac (claset() delrules [equalityI], 
  13.109 -	       simpset() addsimps [Restrict_project_act, image_eq_UN]) 1);
  13.110 -qed "Diff_project_project_component_project_Diff";
  13.111 -
  13.112 -Goal "Diff (project_set h C) (project h C G) acts <= \
  13.113 -\         project h C (Diff C G (extend_act h `` acts))";
  13.114 -by (rtac component_trans 1);
  13.115 -by (rtac Diff_project_project_component_project_Diff 2);
  13.116 -by (simp_tac 
  13.117 -    (simpset() addsimps [component_eq_subset, Diff_def,
  13.118 -			 Restrict_project_act, project_act_Restrict_Id, 
  13.119 -			 image_eq_UN, Restrict_image_Diff]) 1);
  13.120 -qed "Diff_project_component_project_Diff";
  13.121 -
  13.122 -Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
  13.123 -\     ==> Diff (project_set h C) (project h C G) acts : A co B";
  13.124 -by (rtac (Diff_project_component_project_Diff RS component_constrains) 1);
  13.125 -by (rtac (project_constrains RS iffD2) 1);
  13.126 -by (ftac constrains_imp_subset 1);
  13.127 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
  13.128 -qed "Diff_project_constrains";
  13.129 -
  13.130 -Goalw [stable_def]
  13.131 -     "Diff C G (extend_act h `` acts) : stable (extend_set h A) \
  13.132 -\     ==> Diff (project_set h C) (project h C G) acts : stable A";
  13.133 -by (etac Diff_project_constrains 1);
  13.134 -qed "Diff_project_stable";
  13.135 -
  13.136 -(** Some results for Diff, extend and project_set **)
  13.137 -
  13.138 -Goal "Diff C (extend h G) (extend_act h `` acts) \
  13.139 -\         : (extend_set h A) co (extend_set h B) \
  13.140 -\     ==> Diff (project_set h C) G acts : A co B";
  13.141 -by (rtac (Diff_project_set_component RS component_constrains) 1);
  13.142 -by (ftac constrains_imp_subset 1);
  13.143 -by (asm_full_simp_tac
  13.144 -    (simpset() addsimps [project_constrains, extend_set_strict_mono]) 1);
  13.145 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
  13.146 -qed "Diff_project_set_constrains_I";
  13.147 -
  13.148 -Goalw [stable_def]
  13.149 -     "Diff C (extend h G) (extend_act h `` acts) : stable (extend_set h A) \
  13.150 -\     ==> Diff (project_set h C) G acts : stable A";
  13.151 -by (asm_simp_tac (simpset() addsimps [Diff_project_set_constrains_I]) 1);
  13.152 -qed "Diff_project_set_stable_I";
  13.153 -
  13.154 -Goalw [LOCALTO_def]
  13.155 -     "extend h F : (v o f) localTo[C] extend h H \
  13.156 -\     ==> F : v localTo[project_set h C] H";
  13.157 -by Auto_tac;
  13.158 -by (rtac Diff_project_set_stable_I 1);
  13.159 -by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym]) 1);
  13.160 -qed "localTo_project_set_I";
  13.161 -
  13.162 -(*Converse fails: even if the conclusion holds, H could modify (v o f) 
  13.163 -  simultaneously with other variables, and this action would not be 
  13.164 -  superseded by anything in (extend h G) *)
  13.165 -Goal "H : (v o f) localTo[C] extend h G \
  13.166 -\     ==> project h C H : v localTo[project_set h C] G";
  13.167 -by (asm_full_simp_tac 
  13.168 -    (simpset() addsimps [LOCALTO_def, 
  13.169 -			 project_extend_Join RS sym,
  13.170 -			 Diff_project_stable,
  13.171 -			 Collect_eq_extend_set RS sym]) 1);
  13.172 -qed "project_localTo_lemma";
  13.173 -
  13.174 -Goal "extend h F Join G : (v o f) localTo[C] extend h H \
  13.175 -\     ==> F Join project h C G : v localTo[project_set h C] H";
  13.176 -by (asm_full_simp_tac 
  13.177 -    (simpset() addsimps [Join_localTo, localTo_project_set_I,
  13.178 -			 project_localTo_lemma]) 1);
  13.179 -qed "gen_project_localTo_I";
  13.180 -
  13.181 -Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \
  13.182 -\     ==> F Join project h UNIV G : v localTo[UNIV] H";
  13.183 -by (dtac gen_project_localTo_I 1);
  13.184 -by (Asm_full_simp_tac 1);
  13.185 -qed "project_localTo_I";
  13.186 -
  13.187 -Goalw [projecting_def]
  13.188 -     "projecting (%G. UNIV) h F \
  13.189 -\         ((v o f) localTo[UNIV] extend h H)  (v localTo[UNIV] H)";
  13.190 -by (blast_tac (claset() addIs [project_localTo_I]) 1);
  13.191 -qed "projecting_localTo";
  13.192 -
  13.193  
  13.194  (** Reachability and project **)
  13.195  
  13.196 @@ -352,7 +256,8 @@
  13.197  qed "reachable_imp_reachable_project";
  13.198  
  13.199  (*The extra generality in the first premise allows guarantees with STRONG
  13.200 -  preconditions (localTo) and WEAK postconditions.*)
  13.201 +  preconditions (localT) and WEAK postconditions.*)
  13.202 +(*LOCALTO NO LONGER EXISTS: replace C by reachable...??*)
  13.203  Goalw [Constrains_def]
  13.204       "[| reachable (extend h F Join G) <= C;    \
  13.205  \        F Join project h C G : A Co B |] \
  13.206 @@ -479,15 +384,6 @@
  13.207  				      Collect_eq_extend_set RS sym]) 1);
  13.208  qed "project_Increasing";
  13.209  
  13.210 -Goal "[| H <= F;  extend h F Join G : (v o f) LocalTo extend h H |] \
  13.211 -\     ==> F Join project h (reachable (extend h F Join G)) G : v LocalTo H";
  13.212 -by (asm_full_simp_tac 
  13.213 -    (simpset() delsimps [extend_Join]
  13.214 -	       addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
  13.215 -			 gen_project_localTo_I, extend_Join RS sym, 
  13.216 -			 Join_assoc RS sym, Join_absorb1]) 1);
  13.217 -qed "project_LocalTo_I";
  13.218 -
  13.219  (** A lot of redundant theorems: all are proved to facilitate reasoning
  13.220      about guarantees. **)
  13.221  
  13.222 @@ -515,35 +411,28 @@
  13.223  by (blast_tac (claset() addIs [project_Increasing_I]) 1);
  13.224  qed "projecting_Increasing";
  13.225  
  13.226 -Goalw [projecting_def]
  13.227 -     "H <= F ==> projecting (%G. reachable (extend h F Join G)) h F \
  13.228 -\                           ((v o f) LocalTo extend h H) (v LocalTo H)";
  13.229 -by (blast_tac (claset() addIs [project_LocalTo_I]) 1);
  13.230 -qed "projecting_LocalTo";
  13.231 -
  13.232  Goalw [extending_def]
  13.233 -     "extending (%G. reachable (extend h F Join G)) h F X' \
  13.234 -\               (extend_set h A Co extend_set h B) (A Co B)";
  13.235 +     "extending v (%G. reachable (extend h F Join G)) h F \
  13.236 +\                 (extend_set h A Co extend_set h B) (A Co B)";
  13.237  by (blast_tac (claset() addIs [project_Constrains_D]) 1);
  13.238  qed "extending_Constrains";
  13.239  
  13.240  Goalw [extending_def]
  13.241 -     "extending (%G. reachable (extend h F Join G)) h F X' \
  13.242 -\               (Stable (extend_set h A)) (Stable A)";
  13.243 +     "extending v (%G. reachable (extend h F Join G)) h F \
  13.244 +\                 (Stable (extend_set h A)) (Stable A)";
  13.245  by (blast_tac (claset() addIs [project_Stable_D]) 1);
  13.246  qed "extending_Stable";
  13.247  
  13.248  Goalw [extending_def]
  13.249 -     "extending (%G. reachable (extend h F Join G)) h F X' \
  13.250 -\               (Always (extend_set h A)) (Always A)";
  13.251 +     "extending v (%G. reachable (extend h F Join G)) h F \
  13.252 +\                 (Always (extend_set h A)) (Always A)";
  13.253  by (blast_tac (claset() addIs [project_Always_D]) 1);
  13.254  qed "extending_Always";
  13.255  
  13.256  val [prem] = 
  13.257  Goalw [extending_def]
  13.258       "(!!G. reachable (extend h F Join G) <= C G)  \
  13.259 -\     ==> extending C h F X' \
  13.260 -\                   (Increasing (func o f)) (Increasing func)";
  13.261 +\     ==> extending v C h F (Increasing (func o f)) (Increasing func)";
  13.262  by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
  13.263  qed "extending_Increasing";
  13.264  
  13.265 @@ -585,10 +474,12 @@
  13.266  by (Blast_tac 1);
  13.267  qed "ensures_extend_set_imp_project_ensures";
  13.268  
  13.269 -Goal "[| project h C G : transient (A-B) --> F : transient (A-B);  \
  13.270 +Goal "[| project h C G ~: transient (A-B) | A<=B;  \
  13.271  \        extend h F Join G : stable C;  \
  13.272  \        F Join project h C G : A ensures B |] \
  13.273  \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
  13.274 +by (etac disjE 1);
  13.275 +by (blast_tac (claset() addIs [subset_imp_ensures]) 2);
  13.276  by (auto_tac (claset() addDs [extend_transient RS iffD2] 
  13.277                         addIs [transient_strengthen, project_set_I,
  13.278  			      project_unless RS unlessD, unlessI, 
  13.279 @@ -601,7 +492,7 @@
  13.280  
  13.281  (*The strange induction formula allows induction over the leadsTo
  13.282    assumption's non-atomic precondition*)
  13.283 -Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
  13.284 +Goal "[| ALL D. project h C G : transient D --> D={};  \
  13.285  \        extend h F Join G : stable C;  \
  13.286  \        F Join project h C G : (project_set h C Int A) leadsTo B |] \
  13.287  \     ==> extend h F Join G : \
  13.288 @@ -614,7 +505,7 @@
  13.289  by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
  13.290  val lemma = result();
  13.291  
  13.292 -Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
  13.293 +Goal "[| ALL D. project h C G : transient D --> D={};  \
  13.294  \        extend h F Join G : stable C;  \
  13.295  \        F Join project h C G : (project_set h C Int A) leadsTo B |] \
  13.296  \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
  13.297 @@ -623,7 +514,7 @@
  13.298  qed "project_leadsTo_lemma";
  13.299  
  13.300  Goal "[| C = (reachable (extend h F Join G)); \
  13.301 -\        ALL D. project h C G : transient D --> F : transient D;  \
  13.302 +\        ALL D. project h C G : transient D --> D={};  \
  13.303  \        F Join project h C G : A LeadsTo B |] \
  13.304  \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
  13.305  by (asm_full_simp_tac 
  13.306 @@ -632,30 +523,52 @@
  13.307  qed "Join_project_LeadsTo";
  13.308  
  13.309  
  13.310 +
  13.311  (*** GUARANTEES and EXTEND ***)
  13.312  
  13.313 +(** preserves **)
  13.314 +
  13.315 +Goal "G : preserves (v o f) ==> project h C G : preserves v";
  13.316 +by (auto_tac (claset(),
  13.317 +	      simpset() addsimps [preserves_def, project_stable_I,
  13.318 +				  Collect_eq_extend_set RS sym]));
  13.319 +qed "project_preserves_I";
  13.320 +
  13.321 +(*to preserve f is to preserve the whole original state*)
  13.322 +Goal "G : preserves f ==> project h C G : preserves id";
  13.323 +by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
  13.324 +qed "project_preserves_id_I";
  13.325 +
  13.326 +Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
  13.327 +by (auto_tac (claset(),
  13.328 +	      simpset() addsimps [preserves_def, extend_stable RS sym,
  13.329 +				  Collect_eq_extend_set RS sym]));
  13.330 +qed "extend_preserves";
  13.331 +
  13.332  (** Strong precondition and postcondition; doesn't seem very useful. **)
  13.333  
  13.334 -Goal "F : X guarantees Y ==> \
  13.335 -\     extend h F : (extend h `` X) guarantees (extend h `` Y)";
  13.336 +Goal "F : X guarantees[v] Y ==> \
  13.337 +\     extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
  13.338  by (rtac guaranteesI 1);
  13.339  by Auto_tac;
  13.340 -by (blast_tac (claset() addDs [project_set_UNIV RS equalityD2 RS 
  13.341 -			         extend_Join_eq_extend_D, 
  13.342 +by (blast_tac (claset() addIs [project_preserves_I]
  13.343 +			addDs [project_set_UNIV RS equalityD2 RS 
  13.344 +			       extend_Join_eq_extend_D, 
  13.345  			       guaranteesD]) 1);
  13.346  qed "guarantees_imp_extend_guarantees";
  13.347  
  13.348 -Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
  13.349 -\    ==> F : X guarantees Y";
  13.350 -by (auto_tac (claset(), simpset() addsimps [guarantees_eq]));
  13.351 +Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
  13.352 +\     ==> F : X guarantees[v] Y";
  13.353 +by (auto_tac (claset(), simpset() addsimps [guar_def]));
  13.354  by (dres_inst_tac [("x", "extend h G")] spec 1);
  13.355  by (asm_full_simp_tac 
  13.356      (simpset() delsimps [extend_Join] 
  13.357 -           addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 1);
  13.358 +           addsimps [extend_Join RS sym, extend_preserves,
  13.359 +		     inj_extend RS inj_image_mem_iff]) 1);
  13.360  qed "extend_guarantees_imp_guarantees";
  13.361  
  13.362 -Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
  13.363 -\    (F : X guarantees Y)";
  13.364 +Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
  13.365 +\    (F : X guarantees[v] Y)";
  13.366  by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
  13.367  			       extend_guarantees_imp_guarantees]) 1);
  13.368  qed "extend_guarantees_eq";
  13.369 @@ -666,151 +579,116 @@
  13.370  
  13.371  (*The raw version*)
  13.372  val [xguary,project,extend] =
  13.373 -Goal "[| F : X guarantees Y;  \
  13.374 -\        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
  13.375 -\        !!G. [| F Join proj G h G : Y; extend h F Join G : X' |] \
  13.376 +Goal "[| F : X guarantees[v] Y;  \
  13.377 +\        !!G. extend h F Join G : X' ==> F Join project h C G : X;  \
  13.378 +\        !!G. [| F Join project h C G : Y; extend h F Join G : X' |] \
  13.379  \             ==> extend h F Join G : Y' |] \
  13.380 -\     ==> extend h F : X' guarantees Y'";
  13.381 +\     ==> extend h F : X' guarantees[v o f] Y'";
  13.382  by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
  13.383 +by (etac project_preserves_I 1);
  13.384  by (etac project 1);
  13.385  by (assume_tac 1);
  13.386  qed "project_guarantees_raw";
  13.387  
  13.388 -Goal "[| F : X guarantees Y;  \
  13.389 -\        projecting C h F X' X;  extending C h F X' Y' Y |] \
  13.390 -\     ==> extend h F : X' guarantees Y'";
  13.391 +Goal "[| F : X guarantees[v] Y;  \
  13.392 +\        projecting C h F X' X;  extending w C h F Y' Y; \
  13.393 +\        preserves w <= preserves (v o f) |] \
  13.394 +\     ==> extend h F : X' guarantees[w] Y'";
  13.395  by (rtac guaranteesI 1);
  13.396  by (auto_tac (claset(), 
  13.397 -        simpset() addsimps [guaranteesD, projecting_def, extending_def]));
  13.398 +        simpset() addsimps [project_preserves_I, guaranteesD, projecting_def,
  13.399 +			    extending_def]));
  13.400  qed "project_guarantees";
  13.401  
  13.402 +
  13.403  (*It seems that neither "guarantees" law can be proved from the other.*)
  13.404  
  13.405  
  13.406  (*** guarantees corollaries ***)
  13.407  
  13.408 -(** Most could be deleted: the required versions are easy to prove **)
  13.409 +(** Some could be deleted: the required versions are easy to prove **)
  13.410  
  13.411 -Goal "F : UNIV guarantees increasing func \
  13.412 -\     ==> extend h F : X' guarantees increasing (func o f)";
  13.413 +Goal "F : UNIV guarantees[v] increasing func \
  13.414 +\     ==> extend h F : X' guarantees[v o f] increasing (func o f)";
  13.415  by (etac project_guarantees 1);
  13.416  by (rtac extending_increasing 2);
  13.417  by (rtac projecting_UNIV 1);
  13.418 +by Auto_tac;
  13.419  qed "extend_guar_increasing";
  13.420  
  13.421 -Goal "F : UNIV guarantees Increasing func \
  13.422 -\     ==> extend h F : X' guarantees Increasing (func o f)";
  13.423 +Goal "F : UNIV guarantees[v] Increasing func \
  13.424 +\     ==> extend h F : X' guarantees[v o f] Increasing (func o f)";
  13.425  by (etac project_guarantees 1);
  13.426  by (rtac extending_Increasing 2);
  13.427  by (rtac projecting_UNIV 1);
  13.428  by Auto_tac;
  13.429  qed "extend_guar_Increasing";
  13.430  
  13.431 -Goal "F : (v localTo[UNIV] G) guarantees increasing func  \
  13.432 -\     ==> extend h F : (v o f) localTo[UNIV] (extend h G)  \
  13.433 -\                      guarantees increasing (func o f)";
  13.434 -by (etac project_guarantees 1);
  13.435 -by (rtac extending_increasing 2);
  13.436 -by (rtac projecting_localTo 1);
  13.437 -qed "extend_localTo_guar_increasing";
  13.438 -
  13.439 -Goal "[| F : (v LocalTo H) guarantees Increasing func;  H <= F |]  \
  13.440 -\     ==> extend h F : (v o f) LocalTo (extend h H)  \
  13.441 -\                      guarantees Increasing (func o f)";
  13.442 -by (etac project_guarantees 1);
  13.443 -by (rtac extending_Increasing 2);
  13.444 -by (rtac projecting_LocalTo 1);
  13.445 -by Auto_tac;
  13.446 -qed "extend_LocalTo_guar_Increasing";
  13.447 -
  13.448 -Goal "F : Always A guarantees Always B \
  13.449 -\ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
  13.450 +Goal "F : Always A guarantees[v] Always B \
  13.451 +\     ==> extend h F : Always(extend_set h A) guarantees[v o f] \
  13.452 +\                      Always(extend_set h B)";
  13.453  by (etac project_guarantees 1);
  13.454  by (rtac extending_Always 2);
  13.455  by (rtac projecting_Always 1);
  13.456 +by Auto_tac;
  13.457  qed "extend_guar_Always";
  13.458  
  13.459 +Goal "[| G : preserves f;  project h C G : transient D |] ==> D={}";
  13.460 +by (rtac stable_transient_empty 1);
  13.461 +by (assume_tac 2);
  13.462 +by (blast_tac (claset() addIs [project_preserves_id_I,
  13.463 +			 impOfSubs preserves_id_subset_stable]) 1);
  13.464 +qed "preserves_project_transient_empty";
  13.465 +
  13.466  
  13.467  (** Guarantees with a leadsTo postcondition **)
  13.468  
  13.469 -Goalw [LOCALTO_def, transient_def, Diff_def]
  13.470 -     "[| G : f localTo[C] extend h F;  project h C G : transient D |]    \
  13.471 -\     ==> F : transient D";
  13.472 -by Auto_tac;
  13.473 -by (case_tac "Restrict C act : Restrict C ``extend_act h `` Acts F" 1);
  13.474 -by Auto_tac; 
  13.475 -by (rtac bexI 1);
  13.476 -by (assume_tac 2);
  13.477 -by (Blast_tac 1);
  13.478 -by (case_tac "D={}" 1);
  13.479 -by (Blast_tac 1);
  13.480 -by (auto_tac (claset(),
  13.481 -	      simpset() addsimps [stable_def, constrains_def]));
  13.482 -by (subgoal_tac "ALL z. Restrict C act ^^ {s. f s = z} <= {s. f s = z}" 1);
  13.483 -by (blast_tac (claset() addSDs [bspec]) 2);
  13.484 -by (thin_tac "ALL z. ?P z" 1);
  13.485 -by (subgoal_tac "project_act h (Restrict C act) ^^ D <= D" 1);
  13.486 -by (Clarify_tac 2);
  13.487 -by (asm_full_simp_tac (simpset() addsimps [project_act_def]) 2);
  13.488 -by (force_tac (claset() addSDs [spec, ImageI RSN (2, subsetD)], simpset()) 2);
  13.489 -by (blast_tac (claset() addSDs [subsetD]) 1);
  13.490 -qed "localTo_project_transient_transient";
  13.491 -
  13.492  Goal "[| F Join project h UNIV G : A leadsTo B;    \
  13.493 -\        G : f localTo[UNIV] extend h F |]  \
  13.494 +\        G : preserves f |]  \
  13.495  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
  13.496  by (res_inst_tac [("C1", "UNIV")] (project_leadsTo_lemma RS leadsTo_weaken) 1);
  13.497 -by (auto_tac (claset(), 
  13.498 -         simpset() addsimps [localTo_UNIV_imp_localTo RS
  13.499 -			     localTo_project_transient_transient]));
  13.500 +by (auto_tac (claset() addDs [preserves_project_transient_empty], 
  13.501 +	      simpset()));
  13.502  qed "project_leadsTo_D";
  13.503  
  13.504  Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
  13.505 -\         G : f LocalTo extend h F |]  \
  13.506 +\         G : preserves f |]  \
  13.507  \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
  13.508  by (rtac (refl RS Join_project_LeadsTo) 1);
  13.509 -by (auto_tac (claset(), 
  13.510 -	      simpset() addsimps [LocalTo_def,
  13.511 -				  localTo_project_transient_transient]));
  13.512 +by (auto_tac (claset() addDs [preserves_project_transient_empty], 
  13.513 +	      simpset()));
  13.514  qed "project_LeadsTo_D";
  13.515  
  13.516  Goalw [extending_def]
  13.517 -     "extending (%G. UNIV) h F \
  13.518 -\                (f localTo[UNIV] extend h F) \
  13.519 -\                (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
  13.520 -by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
  13.521 -			addIs [project_leadsTo_D]) 1);
  13.522 +     "extending f (%G. UNIV) h F \
  13.523 +\                 (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
  13.524 +by (blast_tac (claset() addIs [project_leadsTo_D]) 1);
  13.525  qed "extending_leadsTo";
  13.526  
  13.527  Goalw [extending_def]
  13.528 -     "extending (%G. reachable (extend h F Join G)) h F \
  13.529 -\               (f LocalTo extend h F) \
  13.530 -\               (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
  13.531 -by (force_tac (claset() addIs [project_LeadsTo_D],
  13.532 -	       simpset()addsimps [LocalTo_def, Join_assoc RS sym, 
  13.533 -				  Join_localTo]) 1);
  13.534 +     "extending f (%G. reachable (extend h F Join G)) h F \
  13.535 +\                 (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
  13.536 +by (blast_tac (claset() addIs [project_LeadsTo_D]) 1);
  13.537  qed "extending_LeadsTo";
  13.538  
  13.539  (*STRONG precondition and postcondition*)
  13.540 -Goal "F : (A co A') guarantees (B leadsTo B')  \
  13.541 -\ ==> extend h F : ((extend_set h A) co (extend_set h A'))  \
  13.542 -\                   Int (f localTo[UNIV] (extend h F)) \
  13.543 -\                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
  13.544 +Goal "F : (A co A') guarantees[v] (B leadsTo B')  \
  13.545 +\ ==> extend h F : (extend_set h A co extend_set h A') \
  13.546 +\                  guarantees[f] (extend_set h B leadsTo extend_set h B')";
  13.547  by (etac project_guarantees 1);
  13.548 -by (rtac (extending_leadsTo RS extending_weaken) 2);
  13.549 -by (rtac (projecting_constrains RS projecting_weaken) 1);
  13.550 -by Auto_tac;
  13.551 +by (rtac subset_preserves_o 3);
  13.552 +by (rtac extending_leadsTo 2);
  13.553 +by (rtac projecting_constrains 1);
  13.554  qed "extend_co_guar_leadsTo";
  13.555  
  13.556  (*WEAK precondition and postcondition*)
  13.557 -Goal "F : (A Co A') guarantees (B LeadsTo B')  \
  13.558 -\ ==> extend h F : ((extend_set h A) Co (extend_set h A'))  \
  13.559 -\                   Int (f LocalTo (extend h F)) \
  13.560 -\                  guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
  13.561 +Goal "F : (A Co A') guarantees[v] (B LeadsTo B')  \
  13.562 +\ ==> extend h F : (extend_set h A Co extend_set h A') \
  13.563 +\                  guarantees[f] (extend_set h B LeadsTo extend_set h B')";
  13.564  by (etac project_guarantees 1);
  13.565 -by (rtac (extending_LeadsTo RS extending_weaken) 2);
  13.566 -by (rtac (projecting_Constrains RS projecting_weaken) 1);
  13.567 -by Auto_tac;
  13.568 +by (rtac subset_preserves_o 3);
  13.569 +by (rtac extending_LeadsTo 2);
  13.570 +by (rtac projecting_Constrains 1);
  13.571  qed "extend_Co_guar_LeadsTo";
  13.572  
  13.573  Close_locale "Extend";
    14.1 --- a/src/HOL/UNITY/Project.thy	Wed Dec 08 13:52:36 1999 +0100
    14.2 +++ b/src/HOL/UNITY/Project.thy	Wed Dec 08 13:53:29 1999 +0100
    14.3 @@ -16,10 +16,10 @@
    14.4    "projecting C h F X' X ==
    14.5       ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
    14.6  
    14.7 -  extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
    14.8 -		 'c program set, 'c program set, 'a program set] => bool"
    14.9 -  "extending C h F X' Y' Y ==
   14.10 -     ALL G. F Join project h (C G) G : Y & extend h F Join G : X'
   14.11 +  extending :: "['c=>'d, 'c program => 'c set, 'a*'b => 'c, 'a program, 
   14.12 +		 'c program set, 'a program set] => bool"
   14.13 +  "extending v C h F Y' Y ==
   14.14 +     ALL G. G : preserves v --> F Join project h (C G) G : Y
   14.15              --> extend h F Join G : Y'"
   14.16  
   14.17  end
    15.1 --- a/src/HOL/UNITY/Union.ML	Wed Dec 08 13:52:36 1999 +0100
    15.2 +++ b/src/HOL/UNITY/Union.ML	Wed Dec 08 13:53:29 1999 +0100
    15.3 @@ -159,6 +159,12 @@
    15.4  by Auto_tac;
    15.5  qed "JN_Join_miniscope";
    15.6  
    15.7 +(*Used to prove guarantees_JN_I*)
    15.8 +Goalw  [JOIN_def, Join_def] "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F";
    15.9 +by (rtac program_equalityI 1);
   15.10 +by Auto_tac;
   15.11 +qed "JN_Join_diff";
   15.12 +
   15.13  
   15.14  (*** Safety: co, stable, FP ***)
   15.15  
   15.16 @@ -192,9 +198,9 @@
   15.17  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   15.18  qed "JN_constrains_weaken";
   15.19  
   15.20 -Goal "i : I ==> \
   15.21 -\     (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
   15.22 -by (asm_simp_tac (simpset() addsimps [stable_def, JN_constrains]) 1);
   15.23 +Goal "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
   15.24 +by (asm_simp_tac 
   15.25 +    (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1);
   15.26  qed "JN_stable";
   15.27  
   15.28  Goal "[| ALL i:I. F i : invariant A;  i : I |]  \
   15.29 @@ -220,7 +226,7 @@
   15.30  by (Blast_tac 1);
   15.31  qed "invariant_JoinI";
   15.32  
   15.33 -Goal "i : I ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
   15.34 +Goal "FP (JN i:I. F i) = (INT i:I. FP (F i))";
   15.35  by (asm_simp_tac (simpset() addsimps [FP_def, JN_stable, INTER_def]) 1);
   15.36  qed "FP_JN";
   15.37  
   15.38 @@ -286,156 +292,3 @@
   15.39  qed "stable_Join_ensures2";
   15.40  
   15.41  
   15.42 -(** Diff and localTo **)
   15.43 -
   15.44 -Goalw [Diff_def] "F Join (Diff UNIV G (Acts F)) = F Join G";
   15.45 -by (rtac program_equalityI 1);
   15.46 -by Auto_tac;
   15.47 -qed "Join_Diff2";
   15.48 -
   15.49 -Goalw [Diff_def]
   15.50 -   "Diff C (F Join G) (Acts H) = (Diff C F (Acts H)) Join (Diff C G (Acts H))";
   15.51 -by (rtac program_equalityI 1);
   15.52 -by Auto_tac;
   15.53 -qed "Diff_Join_distrib";
   15.54 -
   15.55 -Goalw [Diff_def] "Diff C F (Acts F) = mk_program(Init F, {})";
   15.56 -by Auto_tac;
   15.57 -qed "Diff_self_eq";
   15.58 -
   15.59 -Goalw [Diff_def, Disjoint_def] "Disjoint C F (Diff C G (Acts F))";
   15.60 -by (force_tac (claset(), 
   15.61 -	       simpset() addsimps [Restrict_imageI, 
   15.62 -				   sym RSN (2,Restrict_imageI)]) 1);
   15.63 -qed "Diff_Disjoint";
   15.64 -
   15.65 -Goalw [Disjoint_def]
   15.66 -     "[| A <= B; Disjoint A F G |] ==> Disjoint B F G";
   15.67 -by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
   15.68 -qed "Disjoint_mono";
   15.69 -
   15.70 -(*** localTo ***)
   15.71 -
   15.72 -Goalw [LOCALTO_def, Diff_def, stable_def, constrains_def]
   15.73 -     "A <= B ==> v localTo[B] F <= v localTo[A] F";
   15.74 -by Auto_tac;
   15.75 -by (dres_inst_tac [("x", "v xc")] spec 1);
   15.76 -by (dres_inst_tac [("x", "Restrict B xa")] bspec 1);
   15.77 -by Auto_tac;
   15.78 -by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
   15.79 -qed "localTo_anti_mono";
   15.80 -
   15.81 -bind_thm ("localTo_UNIV_imp_localTo", 
   15.82 -	  impOfSubs (subset_UNIV RS localTo_anti_mono));
   15.83 -
   15.84 -Goalw [LocalTo_def]
   15.85 -     "G : v localTo[UNIV] F ==> G : v LocalTo F";
   15.86 -by (blast_tac (claset() addDs [impOfSubs localTo_anti_mono]) 1);
   15.87 -qed "localTo_imp_LocalTo";
   15.88 -
   15.89 -Goalw [LOCALTO_def, stable_def, constrains_def]
   15.90 -     "G : v localTo[C] F ==> G : (f o v) localTo[C] F";
   15.91 -by (Force_tac 1);
   15.92 -qed "localTo_imp_o_localTo";
   15.93 -
   15.94 -Goal "G : v LocalTo F ==> G : (f o v) LocalTo F";
   15.95 -by (asm_full_simp_tac
   15.96 -    (simpset() addsimps [LocalTo_def, localTo_imp_o_localTo]) 1);
   15.97 -qed "LocalTo_imp_o_LocalTo";
   15.98 -
   15.99 -(*NOT USED*)
  15.100 -Goalw [LOCALTO_def, stable_def, constrains_def]
  15.101 -     "(%s. x) localTo[C] F = UNIV";
  15.102 -by (Blast_tac 1);
  15.103 -qed "triv_localTo_eq_UNIV";
  15.104 -
  15.105 -Goal "(F Join G : v localTo[C] H) = \
  15.106 -\     (F : v localTo[C] H  &  G : v localTo[C] H)";
  15.107 -by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_Join_distrib,
  15.108 -				  stable_def, Join_constrains]) 1);
  15.109 -by (Blast_tac 1);
  15.110 -qed "Join_localTo";
  15.111 -
  15.112 -Goal "F : v localTo[C] F";
  15.113 -by (simp_tac 
  15.114 -    (simpset() addsimps [LOCALTO_def, stable_def, constrains_def, 
  15.115 -			 Diff_self_eq]) 1);
  15.116 -qed "self_localTo";
  15.117 -
  15.118 -Goal "(F Join G : v localTo[C] F) = (G : v localTo[C] F)";
  15.119 -by (simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
  15.120 -qed "self_Join_localTo";
  15.121 -
  15.122 -Goal "(F Join G : v LocalTo F) = (G : v LocalTo F)";
  15.123 -by (simp_tac (simpset() addsimps [self_Join_localTo, LocalTo_def,
  15.124 -				  Join_left_absorb]) 1);
  15.125 -qed "self_Join_LocalTo";
  15.126 -
  15.127 -
  15.128 -(*** Higher-level rules involving localTo and Join ***)
  15.129 -
  15.130 -Goal "[| F : {s. P (v s)} co B;  G : v localTo[C] F |]  \
  15.131 -\     ==> G : C Int {s. P (v s)} co B";
  15.132 -by (ftac constrains_imp_subset 1);
  15.133 -by (auto_tac (claset(), 
  15.134 -	      simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
  15.135 -				  Diff_def]));
  15.136 -by (case_tac "Restrict C act: Restrict C `` Acts F" 1);
  15.137 -by (blast_tac (claset() addSEs [equalityE]) 1);
  15.138 -by (subgoal_tac "v x = v xa" 1);
  15.139 -by (Force_tac 1);
  15.140 -by (thin_tac "ALL act: ?A. ?P act" 1);
  15.141 -by (dtac spec 1);
  15.142 -by (dres_inst_tac [("x", "Restrict C act")] bspec 1);
  15.143 -by Auto_tac;
  15.144 -qed "constrains_localTo_constrains";
  15.145 -
  15.146 -Goalw [LOCALTO_def, stable_def, constrains_def, Diff_def]
  15.147 -     "[| G : v localTo[C] F;  G : w localTo[C] F |]  \
  15.148 -\     ==> G : (%s. (v s, w s)) localTo[C] F";
  15.149 -by (Blast_tac 1);
  15.150 -qed "localTo_pairfun";
  15.151 -
  15.152 -Goal "[| F : {s. P (v s) (w s)} co B;   \
  15.153 -\        G : v localTo[C] F;       \
  15.154 -\        G : w localTo[C] F |]               \
  15.155 -\     ==> G : C Int {s. P (v s) (w s)} co B";
  15.156 -by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}")] 
  15.157 -    constrains_weaken 1);
  15.158 -by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
  15.159 -by Auto_tac;
  15.160 -qed "constrains_localTo_constrains2";
  15.161 -
  15.162 -(*Used just once, in Client.ML.  Having F in the conclusion is silly.*)
  15.163 -Goalw [stable_def]
  15.164 -     "[| F : stable {s. P (v s) (w s)};   \
  15.165 -\        G : v localTo[UNIV] F;  G : w localTo[UNIV] F |]               \
  15.166 -\     ==> F Join G : stable {s. P (v s) (w s)}";
  15.167 -by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
  15.168 -by (blast_tac (claset() addIs [constrains_localTo_constrains2 RS 
  15.169 -			       constrains_weaken]) 1);
  15.170 -qed "stable_localTo_stable2";
  15.171 -
  15.172 -(*Used just in Client.ML.  Generalize to arbitrary C?*)
  15.173 -Goal "[| F : stable {s. v s <= w s};   \
  15.174 -\        G : v localTo[UNIV] F;       \
  15.175 -\        F Join G : Increasing w |]               \
  15.176 -\     ==> F Join G : Stable {s. v s <= w s}";
  15.177 -by (auto_tac (claset(), 
  15.178 -	      simpset() addsimps [stable_def, Stable_def, Increasing_def, 
  15.179 -		    Constrains_def, Join_constrains, all_conj_distrib]));
  15.180 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
  15.181 -(*The G case remains; proved like constrains_localTo_constrains*)
  15.182 -by (auto_tac (claset(), 
  15.183 -              simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
  15.184 -                                  Diff_def]));
  15.185 -by (case_tac "act: Acts F" 1);
  15.186 -by (Blast_tac 1);
  15.187 -by (thin_tac "ALL act:Acts F. ?P act" 1);
  15.188 -by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1);
  15.189 -by (dres_inst_tac [("x", "v xa")] spec 1 THEN dtac bspec 1 THEN rtac DiffI 1);
  15.190 -by (assume_tac 1);
  15.191 -by (Blast_tac 1);
  15.192 -by (subgoal_tac "v x = v xa" 1);
  15.193 -by Auto_tac;
  15.194 -qed "Increasing_localTo_Stable";
    16.1 --- a/src/HOL/UNITY/Union.thy	Wed Dec 08 13:52:36 1999 +0100
    16.2 +++ b/src/HOL/UNITY/Union.thy	Wed Dec 08 13:53:29 1999 +0100
    16.3 @@ -6,10 +6,6 @@
    16.4  Unions of programs
    16.5  
    16.6  Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
    16.7 -
    16.8 -Do we need a Meet operator?  (Aka Intersection)
    16.9 -
   16.10 -CAN PROBABLY DELETE the "Disjoint" predicate
   16.11  *)
   16.12  
   16.13  Union = SubstAx + FP +
   16.14 @@ -24,26 +20,6 @@
   16.15    SKIP :: 'a program
   16.16      "SKIP == mk_program (UNIV, {})"
   16.17  
   16.18 -  Diff :: "['a set, 'a program, ('a * 'a)set set] => 'a program"
   16.19 -    "Diff C G acts ==
   16.20 -       mk_program (Init G, (Restrict C `` Acts G) - (Restrict C `` acts))"
   16.21 -
   16.22 -  (*The set of systems that regard "v" as local to F*)
   16.23 -  LOCALTO :: ['a => 'b, 'a set, 'a program] => 'a program set
   16.24 -                                           ("(_/ localTo[_]/ _)" [80,0,80] 80)
   16.25 -    "v localTo[C] F == {G. ALL z. Diff C G (Acts F) : stable {s. v s = z}}"
   16.26 -
   16.27 -  (*The weak version of localTo, considering only G's reachable states*)
   16.28 -  LocalTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
   16.29 -    "v LocalTo F == {G. G : v localTo[reachable (F Join G)] F}"
   16.30 -
   16.31 -  (*Two programs with disjoint actions, except for identity actions.
   16.32 -    It's a weak property but still useful.*)
   16.33 -  Disjoint :: ['a set, 'a program, 'a program] => bool
   16.34 -    "Disjoint C F G ==
   16.35 -       (Restrict C `` (Acts F - {Id})) Int (Restrict C `` (Acts G - {Id}))
   16.36 -       <= {}"
   16.37 -
   16.38  syntax
   16.39    "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)
   16.40    "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)