added compatibility relation: AllowedActs, Allowed, ok,
authorpaulson
Sat Sep 23 16:02:01 2000 +0200 (2000-09-23)
changeset 100641a77667b21ef
parent 10063 947ee8608b90
child 10065 ddb3a014f721
added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Alloc.thy
src/HOL/UNITY/AllocImpl.ML
src/HOL/UNITY/AllocImpl.thy
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Client.thy
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Common.thy
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/ELT.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/Handshake.thy
src/HOL/UNITY/Lift.thy
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Mutex.thy
src/HOL/UNITY/NSP_Bad.thy
src/HOL/UNITY/PPROD.ML
src/HOL/UNITY/Project.ML
src/HOL/UNITY/Project.thy
src/HOL/UNITY/Reach.thy
src/HOL/UNITY/Rename.ML
src/HOL/UNITY/TimerArray.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Fri Sep 22 17:25:09 2000 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Sat Sep 23 16:02:01 2000 +0200
     1.3 @@ -9,7 +9,8 @@
     1.4  (*Perhaps equalities.ML shouldn't add this in the first place!*)
     1.5  Delsimps [image_Collect];
     1.6  
     1.7 -AddIs [impOfSubs subset_preserves_o];
     1.8 +AddIs    [impOfSubs subset_preserves_o];
     1.9 +Addsimps [impOfSubs subset_preserves_o];
    1.10  Addsimps [funPair_o_distrib];
    1.11  Addsimps [Always_INT_distrib];
    1.12  Delsimps [o_apply];
    1.13 @@ -23,7 +24,7 @@
    1.14  	  rename_image_Constrains, rename_image_Stable,
    1.15  	  rename_image_Increasing, rename_image_Always,
    1.16  	  rename_image_leadsTo, rename_image_LeadsTo,
    1.17 -	  rename_preserves,
    1.18 +	  rename_preserves, rename_image_preserves, lift_image_preserves,
    1.19  	  bij_image_INT, bij_is_inj RS image_Int, bij_image_Collect_eq];
    1.20  
    1.21  (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
    1.22 @@ -31,6 +32,7 @@
    1.23      (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
    1.24      handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
    1.25      handle THM _ => (list_of_Int (th RS INT_D))
    1.26 +    handle THM _ => (list_of_Int (th RS bspec))
    1.27      handle THM _ => [th];
    1.28  
    1.29  (*Used just once, for Alloc_Increasing*)
    1.30 @@ -196,7 +198,32 @@
    1.31  qed "allocRel_o_sysOfClient_eq";
    1.32  Addsimps (make_o_equivs allocRel_o_sysOfClient_eq);
    1.33  
    1.34 +Goal "allocGiv o inv sysOfAlloc = allocGiv";
    1.35 +by (simp_tac (simpset() addsimps [o_def]) 1); 
    1.36 +qed "allocGiv_o_inv_sysOfAlloc_eq";
    1.37 +Addsimps (make_o_equivs allocGiv_o_inv_sysOfAlloc_eq);
    1.38  
    1.39 +Goal "allocAsk o inv sysOfAlloc = allocAsk";
    1.40 +by (simp_tac (simpset() addsimps [o_def]) 1); 
    1.41 +qed "allocAsk_o_inv_sysOfAlloc_eq";
    1.42 +Addsimps (make_o_equivs allocAsk_o_inv_sysOfAlloc_eq);
    1.43 +
    1.44 +Goal "allocRel o inv sysOfAlloc = allocRel";
    1.45 +by (simp_tac (simpset() addsimps [o_def]) 1); 
    1.46 +qed "allocRel_o_inv_sysOfAlloc_eq";
    1.47 +Addsimps (make_o_equivs allocRel_o_inv_sysOfAlloc_eq);
    1.48 +
    1.49 +Goal "(rel o inv client_map o drop_map i o inv sysOfClient) = \
    1.50 +\     rel o sub i o client";
    1.51 +by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1); 
    1.52 +qed "rel_inv_client_map_drop_map";
    1.53 +Addsimps (make_o_equivs rel_inv_client_map_drop_map);
    1.54 +
    1.55 +Goal "(ask o inv client_map o drop_map i o inv sysOfClient) = \
    1.56 +\     ask o sub i o client";
    1.57 +by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1); 
    1.58 +qed "ask_inv_client_map_drop_map";
    1.59 +Addsimps (make_o_equivs ask_inv_client_map_drop_map);
    1.60  
    1.61  (**
    1.62  Open_locale "System";
    1.63 @@ -206,55 +233,63 @@
    1.64  val Network = thm "Network";
    1.65  val System_def = thm "System_def";
    1.66  
    1.67 -(*CANNOT use bind_thm: it puts the theorem into standard form, in effect
    1.68 -  exporting it from the locale*)
    1.69 +CANNOT use bind_thm: it puts the theorem into standard form, in effect
    1.70 +  exporting it from the locale
    1.71  **)
    1.72  
    1.73  AddIffs [finite_lessThan];
    1.74  
    1.75  (*Client : <unfolded specification> *)
    1.76 -val Client_Spec =
    1.77 -    rewrite_rule [client_spec_def, client_increasing_def,
    1.78 -		  client_bounded_def, client_progress_def,
    1.79 -		  client_preserves_def] Client;
    1.80 +val client_spec_simps = 
    1.81 +    [client_spec_def, client_increasing_def, client_bounded_def, 
    1.82 +     client_progress_def, client_allowed_acts_def, client_preserves_def, 
    1.83 +     guarantees_Int_right];
    1.84  
    1.85  val [Client_Increasing_ask, Client_Increasing_rel,
    1.86 -     Client_Bounded, Client_Progress, Client_preserves_giv,
    1.87 -     Client_preserves_dummy] =
    1.88 -        Client_Spec 
    1.89 -          |> simplify (simpset() addsimps [guarantees_Int_right]) 
    1.90 -          |> list_of_Int;
    1.91 +     Client_Bounded, Client_Progress, Client_AllowedActs, 
    1.92 +     Client_preserves_giv, Client_preserves_dummy] =
    1.93 +        Client |> simplify (simpset() addsimps client_spec_simps) 
    1.94 +               |> list_of_Int;
    1.95  
    1.96  AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded,
    1.97  	 Client_preserves_giv, Client_preserves_dummy];
    1.98  
    1.99  
   1.100  (*Network : <unfolded specification> *)
   1.101 -val Network_Spec =
   1.102 -    rewrite_rule [network_spec_def, network_ask_def, network_giv_def, 
   1.103 -		  network_rel_def, network_preserves_def] Network;
   1.104 +val network_spec_simps = 
   1.105 +    [network_spec_def, network_ask_def, network_giv_def, 
   1.106 +     network_rel_def, network_allowed_acts_def, network_preserves_def, 
   1.107 +     ball_conj_distrib];
   1.108  
   1.109 -val [Network_Ask, Network_Giv, Network_Rel, 
   1.110 -     Network_preserves_allocGiv, Network_preserves_rel_ask] = 
   1.111 -    list_of_Int Network_Spec;
   1.112 +val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
   1.113 +     Network_preserves_allocGiv, Network_preserves_rel, 
   1.114 +     Network_preserves_ask]  =  
   1.115 +        Network |> simplify (simpset() addsimps network_spec_simps) 
   1.116 +                |> list_of_Int;
   1.117  
   1.118  AddIffs  [Network_preserves_allocGiv];
   1.119  
   1.120 -Addsimps (Network_preserves_rel_ask |> simplify (simpset()) |> list_of_Int);
   1.121 +Addsimps [Network_preserves_rel, Network_preserves_ask];
   1.122 +Addsimps [o_simp Network_preserves_rel, o_simp Network_preserves_ask];
   1.123  
   1.124  
   1.125  (*Alloc : <unfolded specification> *)
   1.126 -val Alloc_Spec =
   1.127 -    rewrite_rule [alloc_spec_def, alloc_increasing_def, alloc_safety_def, 
   1.128 -		  alloc_progress_def, alloc_preserves_def] Alloc;
   1.129 +val alloc_spec_simps = 
   1.130 +    [alloc_spec_def, alloc_increasing_def, alloc_safety_def, 
   1.131 +		  alloc_progress_def, alloc_allowed_acts_def, 
   1.132 +                  alloc_preserves_def];
   1.133  
   1.134 -val [Alloc_Increasing_0, Alloc_Safety, 
   1.135 -     Alloc_Progress, Alloc_preserves] = list_of_Int Alloc_Spec;
   1.136 +val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
   1.137 +     Alloc_preserves_allocRel, Alloc_preserves_allocAsk, 
   1.138 +     Alloc_preserves_dummy] = 
   1.139 +        Alloc |> simplify (simpset() addsimps alloc_spec_simps) 
   1.140 +              |> list_of_Int;
   1.141  
   1.142  (*Strip off the INT in the guarantees postcondition*)
   1.143  val Alloc_Increasing = normalize Alloc_Increasing_0;
   1.144  
   1.145 -AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int);
   1.146 +AddIffs [Alloc_preserves_allocRel, Alloc_preserves_allocAsk, 
   1.147 +         Alloc_preserves_dummy];
   1.148  
   1.149  (** Components lemmas [MUST BE AUTOMATED] **)
   1.150  
   1.151 @@ -283,9 +318,37 @@
   1.152  
   1.153  (** These preservation laws should be generated automatically **)
   1.154  
   1.155 -AddIs    [impOfSubs subset_preserves_o];
   1.156 -Addsimps [impOfSubs subset_preserves_o];
   1.157 +Goal "Allowed Client = preserves rel Int preserves ask";
   1.158 +by (auto_tac (claset(), 
   1.159 +              simpset() addsimps [Allowed_def, Client_AllowedActs, 
   1.160 +                                  safety_prop_Acts_iff]));  
   1.161 +qed "Client_Allowed";
   1.162 +Addsimps [Client_Allowed];
   1.163 +
   1.164 +Goal "Allowed Network =        \
   1.165 +\       preserves allocRel Int \
   1.166 +\       (INT i: lessThan Nclients. preserves(giv o sub i o client))";
   1.167 +by (auto_tac (claset(), 
   1.168 +              simpset() addsimps [Allowed_def, Network_AllowedActs, 
   1.169 +                                  safety_prop_Acts_iff]));  
   1.170 +qed "Network_Allowed";
   1.171 +Addsimps [Network_Allowed];
   1.172  
   1.173 +Goal "Allowed Alloc = preserves allocGiv";
   1.174 +by (auto_tac (claset(), 
   1.175 +              simpset() addsimps [Allowed_def, Alloc_AllowedActs, 
   1.176 +                                  safety_prop_Acts_iff]));  
   1.177 +qed "Alloc_Allowed";
   1.178 +Addsimps [Alloc_Allowed];
   1.179 +
   1.180 +Goal "OK I (%i. lift i (rename client_map Client))";
   1.181 +by (rtac OK_lift_I 1); 
   1.182 +by Auto_tac;  
   1.183 +by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
   1.184 +by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
   1.185 +by (auto_tac (claset(), simpset() addsimps [o_def, split_def]));  
   1.186 +qed "OK_lift_rename_Client";
   1.187 +Addsimps [OK_lift_rename_Client]; (*needed in rename_client_map_tac*
   1.188  
   1.189  (*The proofs of rename_Client_Increasing, rename_Client_Bounded and
   1.190    rename_Client_Progress are similar.  All require copying out the original
   1.191 @@ -321,23 +384,62 @@
   1.192      asm_simp_tac
   1.193          (simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1];
   1.194  
   1.195 -
   1.196 +						     
   1.197  (*Lifting Client_Increasing to systemState*)
   1.198  Goal "i : I \
   1.199  \     ==> rename sysOfClient (plam x: I. rename client_map Client) : \
   1.200 -\           UNIV \
   1.201 -\           guarantees[(funPair rel ask) o sub i o client]  \
   1.202 -\             Increasing (ask o sub i o client) Int \
   1.203 -\             Increasing (rel o sub i o client)";
   1.204 +\           UNIV  guarantees  \
   1.205 +\           Increasing (ask o sub i o client) Int \
   1.206 +\           Increasing (rel o sub i o client)";
   1.207  by rename_client_map_tac;
   1.208  qed "rename_Client_Increasing";
   1.209  
   1.210 +Goal "[| F : preserves w; i ~= j |] \
   1.211 +\     ==> F : preserves (sub i o fst o lift_map j o funPair v w)";
   1.212 +by (auto_tac (claset(), 
   1.213 +       simpset() addsimps [lift_map_def, split_def, linorder_neq_iff, o_def]));
   1.214 +by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
   1.215 +by (auto_tac (claset(), simpset() addsimps [o_def]));  
   1.216 +qed "preserves_sub_fst_lift_map";
   1.217 +
   1.218 +Goal "[| i < Nclients; j < Nclients |] \
   1.219 +\     ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)";
   1.220 +by (case_tac "i=j" 1);
   1.221 +by (asm_full_simp_tac (simpset() addsimps [o_def, non_dummy_def]) 1);
   1.222 +by (dtac (Client_preserves_dummy RS preserves_sub_fst_lift_map) 1);
   1.223 +by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
   1.224 +by (asm_full_simp_tac (simpset() addsimps [o_def, client_map_def]) 1);  
   1.225 +qed "client_preserves_giv_oo_client_map";
   1.226 +
   1.227 +Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
   1.228 +\     ok Network";
   1.229 +by (auto_tac (claset(), simpset() addsimps [ok_iff_Allowed,
   1.230 +        client_preserves_giv_oo_client_map]));  
   1.231 +qed "rename_sysOfClient_ok_Network";
   1.232 +
   1.233 +Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
   1.234 +\     ok rename sysOfAlloc Alloc";
   1.235 +by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
   1.236 +qed "rename_sysOfClient_ok_Alloc";
   1.237 +
   1.238 +Goal "rename sysOfAlloc Alloc ok Network";
   1.239 +by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
   1.240 +qed "rename_sysOfAlloc_ok_Network";
   1.241 +
   1.242 +AddIffs [rename_sysOfClient_ok_Network, rename_sysOfClient_ok_Alloc,
   1.243 +         rename_sysOfAlloc_ok_Network];
   1.244 +
   1.245 +(*The "ok" laws, re-oriented*)
   1.246 +AddIffs [rename_sysOfClient_ok_Network RS ok_sym,
   1.247 +         rename_sysOfClient_ok_Alloc RS ok_sym,
   1.248 +         rename_sysOfAlloc_ok_Network RS ok_sym];
   1.249 +
   1.250  Goal "i < Nclients \
   1.251  \     ==> System : Increasing (ask o sub i o client) Int \
   1.252  \                  Increasing (rel o sub i o client)";
   1.253  by (rtac ([rename_Client_Increasing,
   1.254  	   Client_component_System] MRS component_guaranteesD) 1);
   1.255 -by Auto_tac;
   1.256 +by Auto_tac;  
   1.257  qed "System_Increasing";
   1.258  
   1.259  bind_thm ("rename_guarantees_sysOfAlloc_I",
   1.260 @@ -476,9 +578,8 @@
   1.261  (*progress (2), step 3: lifting "Client_Bounded" to systemState*)
   1.262  Goal "i : I \
   1.263  \   ==> rename sysOfClient (plam x: I. rename client_map Client) : \
   1.264 -\         UNIV \
   1.265 -\         guarantees[ask o sub i o client]  \
   1.266 -\           Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
   1.267 +\         UNIV  guarantees  \
   1.268 +\         Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
   1.269  by rename_client_map_tac;
   1.270  qed "rename_Client_Bounded";
   1.271  
   1.272 @@ -514,7 +615,7 @@
   1.273  Goal "i: I \
   1.274  \  ==> rename sysOfClient (plam x: I. rename client_map Client) \
   1.275  \       : Increasing (giv o sub i o client)  \
   1.276 -\         guarantees[funPair rel ask o sub i o client] \
   1.277 +\         guarantees \
   1.278  \         (INT h. {s. h <= (giv o sub i o client) s & \
   1.279  \                           h pfixGe (ask o sub i o client) s}  \
   1.280  \                 LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
   1.281 @@ -616,3 +717,28 @@
   1.282  qed "System_correct";
   1.283  
   1.284  
   1.285 +(** Some lemmas no longer used **)
   1.286 +
   1.287 +Goal "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o \
   1.288 +\                             (funPair giv (funPair ask rel))";
   1.289 +by (rtac ext 1); 
   1.290 +by (auto_tac (claset(), simpset() addsimps [o_def, non_dummy_def]));  
   1.291 +qed "non_dummy_eq_o_funPair";
   1.292 +
   1.293 +Goal "(preserves non_dummy) = \
   1.294 +\     (preserves rel Int preserves ask Int preserves giv)";
   1.295 +by (simp_tac (simpset() addsimps [non_dummy_eq_o_funPair]) 1); 
   1.296 +by Auto_tac;  
   1.297 +by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
   1.298 +by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
   1.299 +by (dres_inst_tac [("w1", "giv")] (impOfSubs subset_preserves_o) 3);
   1.300 +by (auto_tac (claset(), simpset() addsimps [o_def]));  
   1.301 +qed "preserves_non_dummy_eq";
   1.302 +
   1.303 +(*Could go to Extend.ML*)
   1.304 +Goal "bij f ==> fst (inv (%(x, u). inv f x) z) = f z";
   1.305 +by (rtac fst_inv_equalityI 1); 
   1.306 +by (res_inst_tac [("f","%z. (f z, ?h z)")] surjI 1); 
   1.307 +by (asm_full_simp_tac (simpset() addsimps [bij_is_inj, inv_f_f]) 1); 
   1.308 +by (asm_full_simp_tac (simpset() addsimps [bij_is_surj, surj_f_inv_f]) 1); 
   1.309 +qed "bij_fst_inv_inv_eq";
     2.1 --- a/src/HOL/UNITY/Alloc.thy	Fri Sep 22 17:25:09 2000 +0200
     2.2 +++ b/src/HOL/UNITY/Alloc.thy	Sat Sep 23 16:02:01 2000 +0200
     2.3 @@ -70,45 +70,47 @@
     2.4    (*spec (3)*)
     2.5    client_increasing :: 'a clientState_d program set
     2.6      "client_increasing ==
     2.7 -         UNIV guarantees[funPair rel ask]
     2.8 -         Increasing ask Int Increasing rel"
     2.9 +         UNIV guarantees  Increasing ask Int Increasing rel"
    2.10  
    2.11    (*spec (4)*)
    2.12    client_bounded :: 'a clientState_d program set
    2.13      "client_bounded ==
    2.14 -         UNIV guarantees[ask]
    2.15 -         Always {s. ALL elt : set (ask s). elt <= NbT}"
    2.16 +         UNIV guarantees  Always {s. ALL elt : set (ask s). elt <= NbT}"
    2.17  
    2.18    (*spec (5)*)
    2.19    client_progress :: 'a clientState_d program set
    2.20      "client_progress ==
    2.21 -	 Increasing giv
    2.22 -	 guarantees[funPair rel ask]
    2.23 +	 Increasing giv  guarantees
    2.24  	 (INT h. {s. h <= giv s & h pfixGe ask s}
    2.25  		 LeadsTo {s. tokens h <= (tokens o rel) s})"
    2.26  
    2.27    (*spec: preserves part*)
    2.28 -    client_preserves :: 'a clientState_d program set
    2.29 -    "client_preserves == preserves (funPair giv clientState_d.dummy)"
    2.30 +  client_preserves :: 'a clientState_d program set
    2.31 +    "client_preserves == preserves giv Int preserves clientState_d.dummy"
    2.32 +
    2.33 +  (*environmental constraints*)
    2.34 +  client_allowed_acts :: 'a clientState_d program set
    2.35 +    "client_allowed_acts ==
    2.36 +       {F. AllowedActs F =
    2.37 +	    insert Id (UNION (preserves (funPair rel ask)) Acts)}"
    2.38  
    2.39    client_spec :: 'a clientState_d program set
    2.40      "client_spec == client_increasing Int client_bounded Int client_progress
    2.41 -                    Int client_preserves"
    2.42 +                    Int client_allowed_acts Int client_preserves"
    2.43  
    2.44  (** Allocator specification (required) ***)
    2.45  
    2.46    (*spec (6)*)
    2.47    alloc_increasing :: 'a allocState_d program set
    2.48      "alloc_increasing ==
    2.49 -	 UNIV
    2.50 -         guarantees[allocGiv]
    2.51 +	 UNIV  guarantees
    2.52  	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
    2.53  
    2.54    (*spec (7)*)
    2.55    alloc_safety :: 'a allocState_d program set
    2.56      "alloc_safety ==
    2.57  	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
    2.58 -         guarantees[allocGiv]
    2.59 +         guarantees
    2.60  	 Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
    2.61           <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
    2.62  
    2.63 @@ -125,7 +127,7 @@
    2.64  	  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
    2.65  		 LeadsTo
    2.66  	         {s. tokens h <= (tokens o sub i o allocRel)s})
    2.67 -         guarantees[allocGiv]
    2.68 +         guarantees
    2.69  	     (INT i : lessThan Nclients.
    2.70  	      INT h. {s. h <= (sub i o allocAsk) s}
    2.71  	             LeadsTo
    2.72 @@ -139,46 +141,62 @@
    2.73      looked at.*)
    2.74  
    2.75    (*spec: preserves part*)
    2.76 -    alloc_preserves :: 'a allocState_d program set
    2.77 -    "alloc_preserves == preserves (funPair allocRel
    2.78 -				   (funPair allocAsk allocState_d.dummy))"
    2.79 +  alloc_preserves :: 'a allocState_d program set
    2.80 +    "alloc_preserves == preserves allocRel Int preserves allocAsk Int
    2.81 +                        preserves allocState_d.dummy"
    2.82    
    2.83 +  (*environmental constraints*)
    2.84 +  alloc_allowed_acts :: 'a allocState_d program set
    2.85 +    "alloc_allowed_acts ==
    2.86 +       {F. AllowedActs F =
    2.87 +	    insert Id (UNION (preserves allocGiv) Acts)}"
    2.88 +
    2.89    alloc_spec :: 'a allocState_d program set
    2.90      "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
    2.91 -                   alloc_preserves"
    2.92 +                   alloc_allowed_acts Int alloc_preserves"
    2.93  
    2.94  (** Network specification ***)
    2.95  
    2.96    (*spec (9.1)*)
    2.97    network_ask :: 'a systemState program set
    2.98      "network_ask == INT i : lessThan Nclients.
    2.99 -			Increasing (ask o sub i o client)
   2.100 -			guarantees[allocAsk]
   2.101 +			Increasing (ask o sub i o client)  guarantees
   2.102  			((sub i o allocAsk) Fols (ask o sub i o client))"
   2.103  
   2.104    (*spec (9.2)*)
   2.105    network_giv :: 'a systemState program set
   2.106      "network_giv == INT i : lessThan Nclients.
   2.107  			Increasing (sub i o allocGiv)
   2.108 -			guarantees[giv o sub i o client]
   2.109 +			guarantees
   2.110  			((giv o sub i o client) Fols (sub i o allocGiv))"
   2.111  
   2.112    (*spec (9.3)*)
   2.113    network_rel :: 'a systemState program set
   2.114      "network_rel == INT i : lessThan Nclients.
   2.115  			Increasing (rel o sub i o client)
   2.116 -			guarantees[allocRel]
   2.117 +			guarantees
   2.118  			((sub i o allocRel) Fols (rel o sub i o client))"
   2.119  
   2.120    (*spec: preserves part*)
   2.121 -    network_preserves :: 'a systemState program set
   2.122 -    "network_preserves == preserves allocGiv  Int
   2.123 -                          (INT i : lessThan Nclients.
   2.124 -                           preserves (funPair rel ask o sub i o client))"
   2.125 +  network_preserves :: 'a systemState program set
   2.126 +    "network_preserves ==
   2.127 +       preserves allocGiv  Int
   2.128 +       (INT i : lessThan Nclients. preserves (rel o sub i o client)  Int
   2.129 +                                   preserves (ask o sub i o client))"
   2.130    
   2.131 +  (*environmental constraints*)
   2.132 +  network_allowed_acts :: 'a systemState program set
   2.133 +    "network_allowed_acts ==
   2.134 +       {F. AllowedActs F =
   2.135 +           insert Id
   2.136 +	    (UNION (preserves allocRel Int
   2.137 +		    (INT i: lessThan Nclients. preserves(giv o sub i o client)))
   2.138 +		  Acts)}"
   2.139 +
   2.140    network_spec :: 'a systemState program set
   2.141      "network_spec == network_ask Int network_giv Int
   2.142 -                     network_rel Int network_preserves"
   2.143 +                     network_rel Int network_allowed_acts Int
   2.144 +                     network_preserves"
   2.145  
   2.146  
   2.147  (** State mappings **)
     3.1 --- a/src/HOL/UNITY/AllocImpl.ML	Fri Sep 22 17:25:09 2000 +0200
     3.2 +++ b/src/HOL/UNITY/AllocImpl.ML	Sat Sep 23 16:02:01 2000 +0200
     3.3 @@ -11,21 +11,38 @@
     3.4  Addsimps [Always_INT_distrib];
     3.5  Delsimps [o_apply];
     3.6  
     3.7 -(*Make a locale for M: merge_spec and G: preserves (funPair merge.Out iOut)?*)
     3.8 +Open_locale "Merge";
     3.9 +
    3.10 +val Merge = thm "Merge_spec";
    3.11 +
    3.12 +Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)";
    3.13 +by (cut_facts_tac [Merge] 1);
    3.14 +by (auto_tac (claset(), 
    3.15 +              simpset() addsimps [merge_spec_def, merge_allowed_acts_def, 
    3.16 +                                  Allowed_def, safety_prop_Acts_iff]));  
    3.17 +qed "Merge_Allowed";
    3.18  
    3.19 -Goalw [merge_spec_def,merge_eqOut_def]
    3.20 -     "[| M: merge_spec; G: preserves merge.Out; G: preserves merge.iOut |] \
    3.21 -\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";  
    3.22 -by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
    3.23 +Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \
    3.24 +\                    M : Allowed G)";
    3.25 +by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed]));  
    3.26 +qed "M_ok_iff";
    3.27 +AddIffs [M_ok_iff];
    3.28 +
    3.29 +Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \
    3.30 +\     ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
    3.31 +by (cut_facts_tac [Merge] 1);
    3.32 +by (force_tac (claset() addDs [guaranteesD], 
    3.33 +               simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1); 
    3.34  qed "Merge_Always_Out_eq_iOut";
    3.35  
    3.36 -Goalw [merge_spec_def,merge_bounded_def]
    3.37 -     "[| M: merge_spec; G: preserves merge.iOut |] \
    3.38 -\ ==> M Join G : Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";  
    3.39 -by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
    3.40 +Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
    3.41 +\     ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
    3.42 +by (cut_facts_tac [Merge] 1);
    3.43 +by (force_tac (claset() addDs [guaranteesD], 
    3.44 +               simpset() addsimps [merge_spec_def, merge_bounded_def]) 1); 
    3.45  qed "Merge_Bounded";
    3.46  
    3.47 -Goal "[| M : merge_spec;  G : preserves (funPair merge.Out iOut) |] \
    3.48 +Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
    3.49  \ ==> M Join G : Always \
    3.50  \         {s. setsum (%i. bag_of (sublist (merge.Out s) \
    3.51  \                                 {k. k < length (iOut s) & iOut s ! k = i})) \
    3.52 @@ -45,35 +62,44 @@
    3.53  by (asm_simp_tac (simpset() addsimps [o_def]) 1); 
    3.54  qed "Merge_Bag_Follows_lemma";
    3.55  
    3.56 -Goal "M : merge_spec \
    3.57 -\ ==> M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
    3.58 -\             guarantees[funPair merge.Out merge.iOut]  \
    3.59 -\                (bag_of o merge.Out) Fols \
    3.60 -\                (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
    3.61 -\                            (lessThan Nclients))";
    3.62 +Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
    3.63 +\         guarantees  \
    3.64 +\            (bag_of o merge.Out) Fols \
    3.65 +\            (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
    3.66 +\                        (lessThan Nclients))";
    3.67  by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
    3.68 -by Auto_tac;
    3.69 +by Auto_tac;  
    3.70  by (rtac Follows_setsum 1);
    3.71 +by (cut_facts_tac [Merge] 1);
    3.72  by (auto_tac (claset(), 
    3.73 -              simpset() addsimps [merge_spec_def,merge_follows_def, o_def]));
    3.74 -by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]
    3.75 -                       addDs [guaranteesD]) 1);
    3.76 +              simpset() addsimps [merge_spec_def, merge_follows_def, o_def]));
    3.77 +by (dtac guaranteesD 1); 
    3.78 +by (best_tac
    3.79 +    (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
    3.80 +by Auto_tac;  
    3.81  qed "Merge_Bag_Follows";
    3.82  
    3.83 +Close_locale "Merge";
    3.84 +
    3.85  
    3.86  (** Distributor **)
    3.87 -	 
    3.88 -Goalw [distr_follows_def]
    3.89 -     "D : distr_follows \
    3.90 -\ ==> D : Increasing distr.In Int Increasing distr.iIn Int \
    3.91 -\        Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
    3.92 -\        guarantees[distr.Out] \
    3.93 -\        (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
    3.94 +
    3.95 +Open_locale "Distrib";
    3.96 +
    3.97 +val Distrib = thm "Distrib_spec";
    3.98 +  
    3.99 +
   3.100 +Goal "D : Increasing distr.In Int Increasing distr.iIn Int \
   3.101 +\         Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
   3.102 +\         guarantees \
   3.103 +\         (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
   3.104 +by (cut_facts_tac [Distrib] 1);
   3.105 +by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
   3.106 +by (Clarify_tac 1); 
   3.107  by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1]
   3.108                          addDs [guaranteesD]) 1);
   3.109  qed "Distr_Increasing_Out";
   3.110  
   3.111 -
   3.112  Goal "[| G : preserves distr.Out; \
   3.113  \        D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
   3.114  \ ==> D Join G : Always \
   3.115 @@ -94,26 +120,37 @@
   3.116  by (Asm_simp_tac 1); 
   3.117  qed "Distr_Bag_Follows_lemma";
   3.118  
   3.119 +Goal "D ok G = (G: preserves distr.Out & D : Allowed G)";
   3.120 +by (cut_facts_tac [Distrib] 1);
   3.121 +by (auto_tac (claset(), 
   3.122 +     simpset() addsimps [distr_spec_def, distr_allowed_acts_def, 
   3.123 +                         Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed]));
   3.124 +qed "D_ok_iff";
   3.125 +AddIffs [D_ok_iff];
   3.126  
   3.127 -Goal "D : distr_follows \
   3.128 -\ ==> D : Increasing distr.In Int Increasing distr.iIn Int \
   3.129 +Goal
   3.130 + "D : Increasing distr.In Int Increasing distr.iIn Int \
   3.131  \     Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
   3.132 -\     guarantees[distr.Out] \
   3.133 +\     guarantees  \
   3.134  \      (INT i : lessThan Nclients. \
   3.135  \       (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \
   3.136  \       Fols \
   3.137  \       (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
   3.138  by (rtac guaranteesI 1);
   3.139 -by (Clarify_tac 1);
   3.140 +by (Clarify_tac 1); 
   3.141  by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1);
   3.142 -by Auto_tac;
   3.143 +by Auto_tac;  
   3.144  by (rtac Follows_setsum 1);
   3.145 +by (cut_facts_tac [Distrib] 1);
   3.146  by (auto_tac (claset(), 
   3.147 -              simpset() addsimps [distr_follows_def, o_def]));
   3.148 -by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]
   3.149 -                       addDs [guaranteesD]) 1);
   3.150 +              simpset() addsimps [distr_spec_def, distr_follows_def, o_def]));
   3.151 +by (dtac guaranteesD 1); 
   3.152 +by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
   3.153 +by Auto_tac;  
   3.154  qed "Distr_Bag_Follows";
   3.155  
   3.156 +Close_locale "Distrib";
   3.157 +
   3.158  
   3.159  Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s})  \
   3.160  \     <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}";
     4.1 --- a/src/HOL/UNITY/AllocImpl.thy	Fri Sep 22 17:25:09 2000 +0200
     4.2 +++ b/src/HOL/UNITY/AllocImpl.thy	Sat Sep 23 16:02:01 2000 +0200
     4.3 @@ -58,38 +58,43 @@
     4.4    (*spec (10)*)
     4.5    merge_increasing :: ('a,'b) merge_d program set
     4.6      "merge_increasing ==
     4.7 -         UNIV guarantees[funPair merge.Out merge.iOut]
     4.8 -         (Increasing merge.Out) Int (Increasing merge.iOut)"
     4.9 +         UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
    4.10  
    4.11    (*spec (11)*)
    4.12    merge_eqOut :: ('a,'b) merge_d program set
    4.13      "merge_eqOut ==
    4.14 -         UNIV guarantees[funPair merge.Out merge.iOut]
    4.15 +         UNIV guarantees
    4.16           Always {s. length (merge.Out s) = length (merge.iOut s)}"
    4.17  
    4.18    (*spec (12)*)
    4.19    merge_bounded :: ('a,'b) merge_d program set
    4.20      "merge_bounded ==
    4.21 -         UNIV guarantees[merge.iOut]
    4.22 +         UNIV guarantees
    4.23           Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
    4.24  
    4.25    (*spec (13)*)
    4.26    merge_follows :: ('a,'b) merge_d program set
    4.27      "merge_follows ==
    4.28  	 (INT i : lessThan Nclients. Increasing (sub i o merge.In))
    4.29 -	 guarantees[funPair merge.Out merge.iOut]
    4.30 +	 guarantees
    4.31  	 (INT i : lessThan Nclients. 
    4.32  	  (%s. sublist (merge.Out s) 
    4.33                         {k. k < size(merge.iOut s) & merge.iOut s! k = i})
    4.34  	  Fols (sub i o merge.In))"
    4.35  
    4.36    (*spec: preserves part*)
    4.37 -    merge_preserves :: ('a,'b) merge_d program set
    4.38 -    "merge_preserves == preserves (funPair merge.In merge_d.dummy)"
    4.39 +  merge_preserves :: ('a,'b) merge_d program set
    4.40 +    "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
    4.41 +
    4.42 +  (*environmental constraints*)
    4.43 +  merge_allowed_acts :: ('a,'b) merge_d program set
    4.44 +    "merge_allowed_acts ==
    4.45 +       {F. AllowedActs F =
    4.46 +	    insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
    4.47  
    4.48    merge_spec :: ('a,'b) merge_d program set
    4.49      "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
    4.50 -                   merge_follows Int merge_preserves"
    4.51 +                   merge_follows Int merge_allowed_acts Int merge_preserves"
    4.52  
    4.53  (** Distributor specification (the number of outputs is Nclients) ***)
    4.54  
    4.55 @@ -98,24 +103,30 @@
    4.56      "distr_follows ==
    4.57  	 Increasing distr.In Int Increasing distr.iIn Int
    4.58  	 Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
    4.59 -	 guarantees[distr.Out]
    4.60 +	 guarantees
    4.61  	 (INT i : lessThan Nclients. 
    4.62  	  (sub i o distr.Out) Fols
    4.63  	  (%s. sublist (distr.In s) 
    4.64                         {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
    4.65  
    4.66 +  distr_allowed_acts :: ('a,'b) distr_d program set
    4.67 +    "distr_allowed_acts ==
    4.68 +       {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
    4.69 +
    4.70 +  distr_spec :: ('a,'b) distr_d program set
    4.71 +    "distr_spec == distr_follows Int distr_allowed_acts"
    4.72  
    4.73  (** Single-client allocator specification (required) ***)
    4.74  
    4.75    (*spec (18)*)
    4.76    alloc_increasing :: 'a allocState_d program set
    4.77 -    "alloc_increasing == UNIV guarantees[giv] Increasing giv"
    4.78 +    "alloc_increasing == UNIV  guarantees  Increasing giv"
    4.79  
    4.80    (*spec (19)*)
    4.81    alloc_safety :: 'a allocState_d program set
    4.82      "alloc_safety ==
    4.83  	 Increasing rel
    4.84 -         guarantees[giv] Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
    4.85 +         guarantees  Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
    4.86  
    4.87    (*spec (20)*)
    4.88    alloc_progress :: 'a allocState_d program set
    4.89 @@ -126,86 +137,88 @@
    4.90           (INT h. {s. h <= giv s & h pfixGe (ask s)}
    4.91  		 LeadsTo
    4.92  	         {s. tokens h <= tokens (rel s)})
    4.93 -         guarantees[giv]
    4.94 -	     (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
    4.95 +         guarantees  (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
    4.96  
    4.97    (*spec: preserves part*)
    4.98 -    alloc_preserves :: 'a allocState_d program set
    4.99 -    "alloc_preserves == preserves (funPair rel
   4.100 -				   (funPair ask allocState_d.dummy))"
   4.101 +  alloc_preserves :: 'a allocState_d program set
   4.102 +    "alloc_preserves == preserves rel Int
   4.103 +                        preserves ask Int
   4.104 +                        preserves allocState_d.dummy"
   4.105    
   4.106 +
   4.107 +  (*environmental constraints*)
   4.108 +  alloc_allowed_acts :: 'a allocState_d program set
   4.109 +    "alloc_allowed_acts ==
   4.110 +       {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
   4.111 +
   4.112    alloc_spec :: 'a allocState_d program set
   4.113      "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
   4.114 -                   alloc_preserves"
   4.115 +                   alloc_allowed_acts Int alloc_preserves"
   4.116 +
   4.117 +locale Merge =
   4.118 +  fixes 
   4.119 +    M   :: ('a,'b::order) merge_d program
   4.120 +  assumes
   4.121 +    Merge_spec  "M  : merge_spec"
   4.122 +
   4.123 +locale Distrib =
   4.124 +  fixes 
   4.125 +    D   :: ('a,'b::order) distr_d program
   4.126 +  assumes
   4.127 +    Distrib_spec  "D : distr_spec"
   4.128 +
   4.129  
   4.130  (****
   4.131 -    (** Network specification ***)
   4.132 +#  (** Network specification ***)
   4.133  
   4.134 -      (*spec (9.1)*)
   4.135 -      network_ask :: 'a systemState program set
   4.136 -	"network_ask == INT i : lessThan Nclients.
   4.137 -			    Increasing (ask o sub i o client)
   4.138 -			    guarantees[ask]
   4.139 -			    (ask  Fols (ask o sub i o client))"
   4.140 +#    (*spec (9.1)*)
   4.141 +#    network_ask :: 'a systemState program set
   4.142 +#	"network_ask == INT i : lessThan Nclients.
   4.143 +#			    Increasing (ask o sub i o client)
   4.144 +#			    guarantees[ask]
   4.145 +#			    (ask  Fols (ask o sub i o client))"
   4.146  
   4.147 -      (*spec (9.2)*)
   4.148 -      network_giv :: 'a systemState program set
   4.149 -	"network_giv == INT i : lessThan Nclients.
   4.150 -			    Increasing giv 
   4.151 -			    guarantees[giv o sub i o client]
   4.152 -			    ((giv o sub i o client) Fols giv )"
   4.153 +#    (*spec (9.2)*)
   4.154 +#    network_giv :: 'a systemState program set
   4.155 +#	"network_giv == INT i : lessThan Nclients.
   4.156 +#			    Increasing giv 
   4.157 +#			    guarantees[giv o sub i o client]
   4.158 +#			    ((giv o sub i o client) Fols giv )"
   4.159  
   4.160 -      (*spec (9.3)*)
   4.161 -      network_rel :: 'a systemState program set
   4.162 -	"network_rel == INT i : lessThan Nclients.
   4.163 -			    Increasing (rel o sub i o client)
   4.164 -			    guarantees[rel]
   4.165 -			    (rel  Fols (rel o sub i o client))"
   4.166 +#    (*spec (9.3)*)
   4.167 +#    network_rel :: 'a systemState program set
   4.168 +#	"network_rel == INT i : lessThan Nclients.
   4.169 +#			    Increasing (rel o sub i o client)
   4.170 +#			    guarantees[rel]
   4.171 +#			    (rel  Fols (rel o sub i o client))"
   4.172  
   4.173 -      (*spec: preserves part*)
   4.174 -	network_preserves :: 'a systemState program set
   4.175 -	"network_preserves == preserves giv  Int
   4.176 -			      (INT i : lessThan Nclients.
   4.177 -			       preserves (funPair rel ask o sub i o client))"
   4.178 +#    (*spec: preserves part*)
   4.179 +#	network_preserves :: 'a systemState program set
   4.180 +#	"network_preserves == preserves giv  Int
   4.181 +#			      (INT i : lessThan Nclients.
   4.182 +#			       preserves (funPair rel ask o sub i o client))"
   4.183  
   4.184 -      network_spec :: 'a systemState program set
   4.185 -	"network_spec == network_ask Int network_giv Int
   4.186 -			 network_rel Int network_preserves"
   4.187 +#    network_spec :: 'a systemState program set
   4.188 +#	"network_spec == network_ask Int network_giv Int
   4.189 +#			 network_rel Int network_preserves"
   4.190  
   4.191  
   4.192 -    (** State mappings **)
   4.193 -      sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
   4.194 -	"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
   4.195 -			   in (| giv = giv s,
   4.196 -				 ask = ask s,
   4.197 -				 rel = rel s,
   4.198 -				 client   = cl,
   4.199 -				 dummy    = xtr|)"
   4.200 +#  (** State mappings **)
   4.201 +#    sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
   4.202 +#	"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
   4.203 +#			   in (| giv = giv s,
   4.204 +#				 ask = ask s,
   4.205 +#				 rel = rel s,
   4.206 +#				 client   = cl,
   4.207 +#				 dummy    = xtr|)"
   4.208  
   4.209  
   4.210 -      sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
   4.211 -	"sysOfClient == %(cl,al). (| giv = giv al,
   4.212 -				     ask = ask al,
   4.213 -				     rel = rel al,
   4.214 -				     client   = cl,
   4.215 -				     systemState.dummy = allocState_d.dummy al|)"
   4.216 +#    sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
   4.217 +#	"sysOfClient == %(cl,al). (| giv = giv al,
   4.218 +#				     ask = ask al,
   4.219 +#				     rel = rel al,
   4.220 +#				     client   = cl,
   4.221 +#				     systemState.dummy = allocState_d.dummy al|)"
   4.222  ****)
   4.223  
   4.224 -consts 
   4.225 -    Alloc  :: 'a allocState_d program
   4.226 -    Merge  :: ('a,'b) merge_d program
   4.227 -
   4.228 -(*    
   4.229 -    Network :: 'a systemState program
   4.230 -    System  :: 'a systemState program
   4.231 -  *)
   4.232 -  
   4.233 -rules
   4.234 -    Alloc   "Alloc   : alloc_spec"
   4.235 -    Merge  "Merge  : merge_spec"
   4.236 -
   4.237 -(**    Network "Network : network_spec"**)
   4.238 -
   4.239 -
   4.240 -
   4.241  end
     5.1 --- a/src/HOL/UNITY/Client.ML	Fri Sep 22 17:25:09 2000 +0200
     5.2 +++ b/src/HOL/UNITY/Client.ML	Sat Sep 23 16:02:01 2000 +0200
     5.3 @@ -6,15 +6,23 @@
     5.4  Distributed Resource Management System: the Client
     5.5  *)
     5.6  
     5.7 -Addsimps [Client_def RS def_prg_Init];
     5.8 +Addsimps [Client_def RS def_prg_Init, 
     5.9 +          Client_def RS def_prg_AllowedActs];
    5.10  program_defs_ref := [Client_def];
    5.11  
    5.12  Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
    5.13  
    5.14 +Goal "(Client ok G) = \
    5.15 +\     (G : preserves rel & G : preserves ask & G : preserves tok &\
    5.16 +\      Client : Allowed G)";
    5.17 +by (auto_tac (claset(), 
    5.18 +      simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed]));  
    5.19 +qed "Client_ok_iff";
    5.20 +AddIffs [Client_ok_iff];
    5.21 +
    5.22  
    5.23  (*Safety property 1: ask, rel are increasing*)
    5.24 -Goal "Client: UNIV guarantees[funPair rel ask] \
    5.25 -\             Increasing ask Int Increasing rel";
    5.26 +Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
    5.27  by (auto_tac
    5.28      (claset() addSIs [increasing_imp_Increasing],
    5.29       simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
    5.30 @@ -23,7 +31,6 @@
    5.31  by Auto_tac;
    5.32  qed "increasing_ask_rel";
    5.33  
    5.34 -
    5.35  Addsimps [nth_append, append_one_prefix];
    5.36  
    5.37  
    5.38 @@ -31,10 +38,11 @@
    5.39        With no Substitution Axiom, we must prove the two invariants 
    5.40    simultaneously.
    5.41  *)
    5.42 -Goal "G : preserves (funPair ask tok)  \
    5.43 +Goal "Client ok G  \
    5.44  \     ==> Client Join G :  \
    5.45  \             Always ({s. tok s <= NbT}  Int  \
    5.46  \                     {s. ALL elt : set (ask s). elt <= NbT})";
    5.47 +by Auto_tac;  
    5.48  by (rtac (invariantI RS stable_Join_Always2) 1);
    5.49  by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
    5.50  		       addSIs [stable_Int]) 3);
    5.51 @@ -45,8 +53,7 @@
    5.52  
    5.53  (*export version, with no mention of tok in the postcondition, but
    5.54    unfortunately tok must be declared local.*)
    5.55 -Goal "Client: UNIV guarantees[funPair ask tok] \
    5.56 -\             Always {s. ALL elt : set (ask s). elt <= NbT}";
    5.57 +Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
    5.58  by (rtac guaranteesI 1);
    5.59  by (etac (ask_bounded_lemma RS Always_weaken) 1);
    5.60  by (rtac Int_lower2 1);
    5.61 @@ -83,7 +90,7 @@
    5.62  qed "transient_lemma";
    5.63  
    5.64  
    5.65 -Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
    5.66 +Goal "[| Client Join G : Increasing giv;  Client ok G |] \
    5.67  \ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}  \
    5.68  \                     LeadsTo {s. k < rel s & rel s <= giv s & \
    5.69  \                                 h <= giv s & h pfixGe ask s}";
    5.70 @@ -105,7 +112,7 @@
    5.71  qed "induct_lemma";
    5.72  
    5.73  
    5.74 -Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
    5.75 +Goal "[| Client Join G : Increasing giv;  Client ok G |] \
    5.76  \ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s}  \
    5.77  \                     LeadsTo {s. h <= rel s}";
    5.78  by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
    5.79 @@ -120,7 +127,7 @@
    5.80  qed "rel_progress_lemma";
    5.81  
    5.82  
    5.83 -Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
    5.84 +Goal "[| Client Join G : Increasing giv;  Client ok G |] \
    5.85  \ ==> Client Join G : {s. h <= giv s & h pfixGe ask s}  \
    5.86  \                     LeadsTo {s. h <= rel s}";
    5.87  by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
    5.88 @@ -133,7 +140,7 @@
    5.89  
    5.90  (*Progress property: all tokens that are given will be released*)
    5.91  Goal "Client : \
    5.92 -\      Increasing giv  guarantees[funPair rel ask]  \
    5.93 +\      Increasing giv  guarantees  \
    5.94  \      (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
    5.95  by (rtac guaranteesI 1);
    5.96  by (Clarify_tac 1);
    5.97 @@ -158,7 +165,7 @@
    5.98  qed "stable_size_rel_le_giv";
    5.99  
   5.100  (*clients return the right number of tokens*)
   5.101 -Goal "Client : Increasing giv  guarantees[rel]  Always {s. rel s <= giv s}";
   5.102 +Goal "Client : Increasing giv  guarantees  Always {s. rel s <= giv s}";
   5.103  by (rtac guaranteesI 1);
   5.104  by (rtac AlwaysI 1);
   5.105  by (Force_tac 1);
     6.1 --- a/src/HOL/UNITY/Client.thy	Fri Sep 22 17:25:09 2000 +0200
     6.2 +++ b/src/HOL/UNITY/Client.thy	Sat Sep 23 16:02:01 2000 +0200
     6.3 @@ -48,9 +48,12 @@
     6.4  		         (s' = s (|ask := ask s @ [tok s]|))}"
     6.5  
     6.6    Client :: 'a state_d program
     6.7 -    "Client == mk_program ({s. tok s : atMost NbT &
     6.8 -		               giv s = [] & ask s = [] & rel s = []},
     6.9 -			   {rel_act, tok_act, ask_act})"
    6.10 +    "Client ==
    6.11 +       mk_program ({s. tok s : atMost NbT &
    6.12 +		    giv s = [] & ask s = [] & rel s = []},
    6.13 +		   {rel_act, tok_act, ask_act},
    6.14 +		   UN G: preserves rel Int preserves ask Int preserves tok.
    6.15 +		   Acts G)"
    6.16  
    6.17    (*Maybe want a special theory section to declare such maps*)
    6.18    non_dummy :: 'a state_d => state
     7.1 --- a/src/HOL/UNITY/Common.ML	Fri Sep 22 17:25:09 2000 +0200
     7.2 +++ b/src/HOL/UNITY/Common.ML	Sat Sep 23 16:02:01 2000 +0200
     7.3 @@ -36,21 +36,22 @@
     7.4  result();
     7.5  
     7.6  (*This one is  t := ftime t || t := gtime t*)
     7.7 -Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
     7.8 +Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \
     7.9  \      : {m} co (maxfg m)";
    7.10  by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
    7.11  				  le_max_iff_disj, fasc]) 1);
    7.12  result();
    7.13  
    7.14  (*This one is  t := max (ftime t) (gtime t)*)
    7.15 -Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
    7.16 +Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \
    7.17  \      : {m} co (maxfg m)";
    7.18  by (simp_tac 
    7.19      (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
    7.20  result();
    7.21  
    7.22  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    7.23 -Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
    7.24 +Goal "mk_program  \
    7.25 +\         (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)  \
    7.26  \      : {m} co (maxfg m)";
    7.27  by (simp_tac 
    7.28      (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
     8.1 --- a/src/HOL/UNITY/Common.thy	Fri Sep 22 17:25:09 2000 +0200
     8.2 +++ b/src/HOL/UNITY/Common.thy	Sat Sep 23 16:02:01 2000 +0200
     8.3 @@ -10,7 +10,7 @@
     8.4  From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
     8.5  *)
     8.6  
     8.7 -Common = Union + 
     8.8 +Common = SubstAx + 
     8.9  
    8.10  consts
    8.11    ftime,gtime :: nat=>nat
     9.1 --- a/src/HOL/UNITY/Comp.ML	Fri Sep 22 17:25:09 2000 +0200
     9.2 +++ b/src/HOL/UNITY/Comp.ML	Sat Sep 23 16:02:01 2000 +0200
     9.3 @@ -19,7 +19,8 @@
     9.4  qed "componentI";
     9.5  
     9.6  Goalw [component_def]
     9.7 -     "(F <= G) = (Init G <= Init F & Acts F <= Acts G)";
     9.8 +     "(F <= G) = \
     9.9 +\     (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)";
    9.10  by (force_tac (claset() addSIs [exI, program_equalityI], 
    9.11  	       simpset()) 1);
    9.12  qed "component_eq_subset";
    9.13 @@ -110,7 +111,11 @@
    9.14  by (Blast_tac 1);
    9.15  qed "JN_preserves";
    9.16  
    9.17 -AddIffs [Join_preserves, JN_preserves];
    9.18 +Goal "SKIP : preserves v";
    9.19 +by (auto_tac (claset(), simpset() addsimps [preserves_def]));
    9.20 +qed "SKIP_preserves";
    9.21 +
    9.22 +AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
    9.23  
    9.24  Goalw [funPair_def] "(funPair f g) x = (f x, g x)";
    9.25  by (Simp_tac 1);
    9.26 @@ -131,7 +136,6 @@
    9.27  by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
    9.28  qed "funPair_o_distrib";
    9.29  
    9.30 -
    9.31  Goal "fst o (funPair f g) = f";
    9.32  by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
    9.33  qed "fst_o_funPair";
    9.34 @@ -141,11 +145,9 @@
    9.35  qed "snd_o_funPair";
    9.36  Addsimps [fst_o_funPair, snd_o_funPair];
    9.37  
    9.38 -
    9.39  Goal "preserves v <= preserves (w o v)";
    9.40  by (force_tac (claset(),
    9.41 -	       simpset() addsimps [preserves_def, 
    9.42 -				   stable_def, constrains_def]) 1);
    9.43 +      simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
    9.44  qed "subset_preserves_o";
    9.45  
    9.46  Goal "preserves v <= stable {s. P (v s)}";
    9.47 @@ -168,6 +170,15 @@
    9.48  qed "preserves_id_subset_stable";
    9.49  
    9.50  
    9.51 +(** For use with def_UNION_ok_iff **)
    9.52 +
    9.53 +Goal "safety_prop (preserves v)";
    9.54 +by (auto_tac (claset() addIs [safety_prop_INTER1], 
    9.55 +              simpset() addsimps [preserves_def]));
    9.56 +qed "safety_prop_preserves";
    9.57 +AddIffs [safety_prop_preserves];
    9.58 +
    9.59 +
    9.60  (** Some lemmas used only in Client.ML **)
    9.61  
    9.62  Goal "[| F : stable {s. P (v s) (w s)};   \
    10.1 --- a/src/HOL/UNITY/ELT.ML	Fri Sep 22 17:25:09 2000 +0200
    10.2 +++ b/src/HOL/UNITY/ELT.ML	Sat Sep 23 16:02:01 2000 +0200
    10.3 @@ -76,6 +76,7 @@
    10.4       "[| F: A ensures B;  A-B: insert {} CC |] ==> F : A leadsTo[CC] B";
    10.5  by (blast_tac (claset() addIs [elt.Basis]) 1);
    10.6  qed "leadsETo_Basis";
    10.7 +AddIs [leadsETo_Basis];
    10.8  
    10.9  Goalw [leadsETo_def]
   10.10       "[| F : A leadsTo[CC] B;  F : B leadsTo[CC] C |] ==> F : A leadsTo[CC] C";
   10.11 @@ -350,7 +351,7 @@
   10.12  by (etac leadsETo_induct 1);
   10.13  by (blast_tac (claset() addIs [leadsTo_Union]) 3);
   10.14  by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
   10.15 -by (blast_tac (claset() addIs [leadsTo_Basis]) 1);
   10.16 +by (Blast_tac 1);
   10.17  qed "leadsETo_subset_leadsTo";
   10.18  
   10.19  Goal "(A leadsTo[UNIV] B) = (A leadsTo B)";
   10.20 @@ -360,7 +361,7 @@
   10.21  by (etac leadsTo_induct 1);
   10.22  by (blast_tac (claset() addIs [leadsETo_Union]) 3);
   10.23  by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
   10.24 -by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
   10.25 +by (Blast_tac 1);
   10.26  qed "leadsETo_UNIV_eq_leadsTo";
   10.27  
   10.28  (**** weak ****)
   10.29 @@ -595,7 +596,8 @@
   10.30  qed "project_LeadsETo_D";
   10.31  
   10.32  Goalw [extending_def]
   10.33 -     "extending (v o f) (%G. UNIV) h F \
   10.34 +     "(ALL G. extend h F ok G --> G : preserves (v o f)) \
   10.35 +\     ==> extending (%G. UNIV) h F \
   10.36  \               (extend_set h A leadsTo[givenBy (v o f)] extend_set h B) \
   10.37  \               (A leadsTo[givenBy v] B)";
   10.38  by (auto_tac (claset(), simpset() addsimps [project_leadsETo_D]));
   10.39 @@ -603,7 +605,8 @@
   10.40  
   10.41  
   10.42  Goalw [extending_def]
   10.43 -     "extending (v o f) (%G. reachable (extend h F Join G)) h F \
   10.44 +     "(ALL G. extend h F ok G --> G : preserves (v o f)) \
   10.45 +\     ==> extending (%G. reachable (extend h F Join G)) h F \
   10.46  \               (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B) \
   10.47  \               (A LeadsTo[givenBy v]  B)";
   10.48  by (blast_tac (claset() addIs [project_LeadsETo_D]) 1);
   10.49 @@ -637,8 +640,7 @@
   10.50  by (asm_full_simp_tac 
   10.51      (simpset() addsimps [givenBy_eq_extend_set]) 1);
   10.52  by (rtac leadsTo_Basis 1);
   10.53 -by (blast_tac (claset() addIs [leadsTo_Basis,
   10.54 -			       ensures_extend_set_imp_project_ensures]) 1);
   10.55 +by (blast_tac (claset() addIs [ensures_extend_set_imp_project_ensures]) 1);
   10.56  
   10.57  qed "project_leadsETo_I_lemma";
   10.58  
    11.1 --- a/src/HOL/UNITY/Extend.ML	Fri Sep 22 17:25:09 2000 +0200
    11.2 +++ b/src/HOL/UNITY/Extend.ML	Sat Sep 23 16:02:01 2000 +0200
    11.3 @@ -288,6 +288,7 @@
    11.4       "project_act h (extend_act h act) = act";
    11.5  by (Blast_tac 1);
    11.6  qed "extend_act_inverse";
    11.7 +Addsimps [extend_act_inverse];
    11.8  
    11.9  Goalw [extend_act_def, project_act_def]
   11.10       "project_act h (Restrict C (extend_act h act)) = \
   11.11 @@ -345,7 +346,7 @@
   11.12                simpset() addsimps [split_extended_all]) 1);
   11.13  qed "Domain_project_act";
   11.14  
   11.15 -Addsimps [extend_act_Id];
   11.16 +Addsimps [extend_act_Id, project_act_Id];
   11.17  
   11.18  
   11.19  (**** extend ****)
   11.20 @@ -355,21 +356,43 @@
   11.21  Goalw [extend_def] "Init (extend h F) = extend_set h (Init F)";
   11.22  by Auto_tac;
   11.23  qed "Init_extend";
   11.24 +Addsimps [Init_extend];
   11.25  
   11.26  Goalw [project_def] "Init (project h C F) = project_set h (Init F)";
   11.27  by Auto_tac;
   11.28  qed "Init_project";
   11.29 +Addsimps [Init_project];
   11.30  
   11.31  Goal "Acts (extend h F) = (extend_act h `` Acts F)";
   11.32  by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1);
   11.33  qed "Acts_extend";
   11.34 +Addsimps [Acts_extend];
   11.35 +
   11.36 +Goal "AllowedActs (extend h F) = project_act h -`` AllowedActs F";
   11.37 +by (simp_tac (simpset() addsimps [extend_def, insert_absorb]) 1);
   11.38 +qed "AllowedActs_extend";
   11.39 +Addsimps [AllowedActs_extend];
   11.40  
   11.41  Goal "Acts(project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
   11.42  by (auto_tac (claset(), 
   11.43  	      simpset() addsimps [project_def, image_iff]));
   11.44  qed "Acts_project";
   11.45 +Addsimps [Acts_project];
   11.46  
   11.47 -Addsimps [Init_extend, Init_project, Acts_extend, Acts_project];
   11.48 +Goal "AllowedActs(project h C F) = \
   11.49 +\       {act. Restrict (project_set h C) act \
   11.50 +\              : project_act h `` Restrict C `` AllowedActs F}";
   11.51 +by (simp_tac (simpset() addsimps [project_def, image_iff]) 1);
   11.52 +by (stac insert_absorb 1);
   11.53 +by (auto_tac (claset() addSIs [inst "x" "Id" bexI], 
   11.54 +                 simpset() addsimps [project_act_def]));  
   11.55 +qed "AllowedActs_project";
   11.56 +Addsimps [AllowedActs_project];
   11.57 +
   11.58 +Goal "Allowed (extend h F) = project h UNIV -`` Allowed F";
   11.59 +by (simp_tac (simpset() addsimps [AllowedActs_extend, Allowed_def]) 1);
   11.60 +by (Blast_tac 1); 
   11.61 +qed "Allowed_extend";
   11.62  
   11.63  Goalw [SKIP_def] "extend h SKIP = SKIP";
   11.64  by (rtac program_equalityI 1);
   11.65 @@ -386,31 +409,51 @@
   11.66  by (Blast_tac 1);
   11.67  qed "project_set_Union";
   11.68  
   11.69 +(*Converse FAILS: the extended state contributing to project_set h C
   11.70 +  may not coincide with the one contributing to project_act h act*)
   11.71 +Goal "project_act h (Restrict C act) <= \
   11.72 +\     Restrict (project_set h C) (project_act h act)";
   11.73 +by (auto_tac (claset(), simpset() addsimps [project_act_def]));  
   11.74 +qed "project_act_Restrict_subset";
   11.75 +
   11.76 +
   11.77 +Goal "project_act h (Restrict C Id) = Restrict (project_set h C) Id";
   11.78 +by (auto_tac (claset(), simpset() addsimps [project_act_def]));  
   11.79 +qed "project_act_Restrict_Id_eq";
   11.80 +
   11.81  Goal "project h C (extend h F) = \
   11.82 -\     mk_program (Init F, Restrict (project_set h C) `` Acts F)";
   11.83 +\     mk_program (Init F, Restrict (project_set h C) `` Acts F, \
   11.84 +\                 {act. Restrict (project_set h C) act : project_act h `` Restrict C `` (project_act h -`` AllowedActs F)})";
   11.85  by (rtac program_equalityI 1);
   11.86  by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 2);
   11.87  by (Simp_tac 1);
   11.88 +by (simp_tac (simpset() addsimps [project_def]) 1);
   11.89  qed "project_extend_eq";
   11.90  
   11.91 -(*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
   11.92 -Goal "UNIV <= project_set h C \
   11.93 -\     ==> project h C (extend h F) = F";
   11.94 +Goal "project h UNIV (extend h F) = F";
   11.95  by (asm_simp_tac (simpset() addsimps [project_extend_eq, image_eq_UN, 
   11.96                     subset_UNIV RS subset_trans RS Restrict_triv]) 1);
   11.97 +by (rtac program_equalityI 1);
   11.98 +by (ALLGOALS Simp_tac);
   11.99 +by (stac insert_absorb 1);
  11.100 +by (simp_tac (simpset() addsimps [inst "x" "Id" bexI]) 1); 
  11.101 +by Auto_tac;  
  11.102 +by (rename_tac "act" 1);
  11.103 +by (res_inst_tac [("x","extend_act h act")] bexI 1);
  11.104 +by Auto_tac;  
  11.105  qed "extend_inverse";
  11.106  Addsimps [extend_inverse];
  11.107  
  11.108  Goal "inj (extend h)";
  11.109  by (rtac inj_on_inverseI 1);
  11.110  by (rtac extend_inverse 1);
  11.111 -by (Force_tac 1);
  11.112  qed "inj_extend";
  11.113  
  11.114  Goal "extend h (F Join G) = extend h F Join extend h G";
  11.115  by (rtac program_equalityI 1);
  11.116  by (simp_tac (simpset() addsimps [image_Un]) 2);
  11.117  by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1);
  11.118 +by Auto_tac;  
  11.119  qed "extend_Join";
  11.120  Addsimps [extend_Join];
  11.121  
  11.122 @@ -418,6 +461,7 @@
  11.123  by (rtac program_equalityI 1);
  11.124  by (simp_tac (simpset() addsimps [image_UN]) 2);
  11.125  by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1);
  11.126 +by Auto_tac;  
  11.127  qed "extend_JN";
  11.128  Addsimps [extend_JN];
  11.129  
  11.130 @@ -430,7 +474,7 @@
  11.131  
  11.132  Goal "F <= G ==> project h C F <= project h C G";
  11.133  by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
  11.134 -by Auto_tac;
  11.135 +by (Blast_tac 1); 
  11.136  qed "project_mono";
  11.137  
  11.138  
  11.139 @@ -685,9 +729,9 @@
  11.140  
  11.141  Goal "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)";
  11.142  by (rtac program_equalityI 1);
  11.143 -by (asm_simp_tac
  11.144 -    (simpset() addsimps [image_eq_UN, UN_Un, extend_act_inverse]) 2);
  11.145 +by (simp_tac (simpset() addsimps [image_eq_UN, UN_Un]) 2);
  11.146  by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
  11.147 +by Auto_tac;  
  11.148  qed "project_extend_Join";
  11.149  
  11.150  Goal "(extend h F) Join G = extend h H ==> H = F Join (project h UNIV G)";
  11.151 @@ -698,26 +742,44 @@
  11.152  (** Strong precondition and postcondition; only useful when
  11.153      the old and new state sets are in bijection **)
  11.154  
  11.155 -Goal "F : X guarantees[v] Y ==> \
  11.156 -\     extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
  11.157 +
  11.158 +Goal "extend h F ok G ==> F ok project h UNIV G";
  11.159 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
  11.160 +by (dtac subsetD 1);   
  11.161 +by (auto_tac (claset() addSIs [rev_image_eqI], simpset()));  
  11.162 +qed "ok_extend_imp_ok_project";
  11.163 +
  11.164 +Goal "(extend h F ok extend h G) = (F ok G)";
  11.165 +by (auto_tac (claset(), simpset() addsimps [ok_def]));  
  11.166 +qed "ok_extend_iff";
  11.167 +
  11.168 +Goal "OK I (%i. extend h (F i)) = (OK I F)";
  11.169 +by (auto_tac (claset(), simpset() addsimps [OK_def]));  
  11.170 +by (dres_inst_tac [("x","i")] bspec 1); 
  11.171 +by (dres_inst_tac [("x","j")] bspec 2); 
  11.172 +by Auto_tac;  
  11.173 +qed "OK_extend_iff";
  11.174 +
  11.175 +Goal "F : X guarantees Y ==> \
  11.176 +\     extend h F : (extend h `` X) guarantees (extend h `` Y)";
  11.177  by (rtac guaranteesI 1);
  11.178 -by Auto_tac;
  11.179 -by (blast_tac (claset() addIs [project_preserves_I]
  11.180 -			addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
  11.181 +by (Clarify_tac 1);
  11.182 +by (blast_tac (claset() addDs [ok_extend_imp_ok_project, 
  11.183 +                               extend_Join_eq_extend_D, guaranteesD]) 1);
  11.184  qed "guarantees_imp_extend_guarantees";
  11.185  
  11.186 -Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
  11.187 -\     ==> F : X guarantees[v] Y";
  11.188 +Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
  11.189 +\     ==> F : X guarantees Y";
  11.190  by (auto_tac (claset(), simpset() addsimps [guar_def]));
  11.191 -by (dres_inst_tac [("x", "extend h G")] bspec 1);
  11.192 +by (dres_inst_tac [("x", "extend h G")] spec 1);
  11.193  by (asm_full_simp_tac 
  11.194      (simpset() delsimps [extend_Join] 
  11.195 -           addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 2);
  11.196 -by (asm_simp_tac (simpset() addsimps [extend_preserves]) 1);
  11.197 +               addsimps [extend_Join RS sym, ok_extend_iff, 
  11.198 +                         inj_extend RS inj_image_mem_iff]) 1);
  11.199  qed "extend_guarantees_imp_guarantees";
  11.200  
  11.201 -Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
  11.202 -\    (F : X guarantees[v] Y)";
  11.203 +Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
  11.204 +\    (F : X guarantees Y)";
  11.205  by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
  11.206  			       extend_guarantees_imp_guarantees]) 1);
  11.207  qed "extend_guarantees_eq";
    12.1 --- a/src/HOL/UNITY/Extend.thy	Fri Sep 22 17:25:09 2000 +0200
    12.2 +++ b/src/HOL/UNITY/Extend.thy	Sat Sep 23 16:02:01 2000 +0200
    12.3 @@ -34,12 +34,16 @@
    12.4  
    12.5    extend :: "['a*'b => 'c, 'a program] => 'c program"
    12.6      "extend h F == mk_program (extend_set h (Init F),
    12.7 -			       extend_act h `` Acts F)"
    12.8 +			       extend_act h `` Acts F,
    12.9 +			       project_act h -`` AllowedActs F)"
   12.10  
   12.11    (*Argument C allows weak safety laws to be projected*)
   12.12    project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
   12.13 -    "project h C F == mk_program (project_set h (Init F),
   12.14 -		  	          project_act h `` Restrict C `` Acts F)"
   12.15 +    "project h C F ==
   12.16 +       mk_program (project_set h (Init F),
   12.17 +		   project_act h `` Restrict C `` Acts F,
   12.18 +		   {act. Restrict (project_set h C) act :
   12.19 +		         project_act h `` Restrict C `` AllowedActs F})"
   12.20  
   12.21  locale Extend =
   12.22    fixes 
    13.1 --- a/src/HOL/UNITY/Guar.ML	Fri Sep 22 17:25:09 2000 +0200
    13.2 +++ b/src/HOL/UNITY/Guar.ML	Sat Sep 23 16:02:01 2000 +0200
    13.3 @@ -65,14 +65,14 @@
    13.4  (*** guarantees ***)
    13.5  
    13.6  val prems = Goal
    13.7 -     "(!!G. [| G : preserves v; F Join G : X |] ==> F Join G : Y) \
    13.8 -\     ==> F : X guarantees[v] Y";
    13.9 +     "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) \
   13.10 +\     ==> F : X guarantees Y";
   13.11  by (simp_tac (simpset() addsimps [guar_def, component_def]) 1);
   13.12  by (blast_tac (claset() addIs prems) 1);
   13.13  qed "guaranteesI";
   13.14  
   13.15  Goalw [guar_def, component_def]
   13.16 -     "[| F : X guarantees[v] Y;  G : preserves v;  F Join G : X |] \
   13.17 +     "[| F : X guarantees Y;  F ok G;  F Join G : X |] \
   13.18  \     ==> F Join G : Y";
   13.19  by (Blast_tac 1);
   13.20  qed "guaranteesD";
   13.21 @@ -80,33 +80,27 @@
   13.22  (*This version of guaranteesD matches more easily in the conclusion
   13.23    The major premise can no longer be  F<=H since we need to reason about G*)
   13.24  Goalw [guar_def]
   13.25 -     "[| F : X guarantees[v] Y;  F Join G = H;  H : X;  G : preserves v |] \
   13.26 +     "[| F : X guarantees Y;  F Join G = H;  H : X;  F ok G |] \
   13.27  \     ==> H : Y";
   13.28  by (Blast_tac 1);
   13.29  qed "component_guaranteesD";
   13.30  
   13.31  Goalw [guar_def]
   13.32 -     "[| F: X guarantees[v] X'; Y <= X; X' <= Y' |] ==> F: Y guarantees[v] Y'";
   13.33 +     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
   13.34  by (Blast_tac 1);
   13.35  qed "guarantees_weaken";
   13.36  
   13.37 -Goalw [guar_def]
   13.38 -     "[| F: X guarantees[v] Y;  preserves w <= preserves v |] \
   13.39 -\     ==> F: X guarantees[w] Y";
   13.40 -by (Blast_tac 1);
   13.41 -qed "guarantees_weaken_var";
   13.42 -
   13.43 -Goalw [guar_def] "X <= Y ==> X guarantees[v] Y = UNIV";
   13.44 +Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
   13.45  by (Blast_tac 1);
   13.46  qed "subset_imp_guarantees_UNIV";
   13.47  
   13.48  (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
   13.49 -Goalw [guar_def] "X <= Y ==> F : X guarantees[v] Y";
   13.50 +Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
   13.51  by (Blast_tac 1);
   13.52  qed "subset_imp_guarantees";
   13.53  
   13.54  (*Remark at end of section 4.1
   13.55 -Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees[v] Y)";
   13.56 +Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
   13.57  by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   13.58  by (blast_tac (claset() addEs [equalityE]) 1);
   13.59  qed "ex_prop_equiv2";
   13.60 @@ -115,40 +109,40 @@
   13.61  (** Distributive laws.  Re-orient to perform miniscoping **)
   13.62  
   13.63  Goalw [guar_def]
   13.64 -     "(UN i:I. X i) guarantees[v] Y = (INT i:I. X i guarantees[v] Y)";
   13.65 +     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
   13.66  by (Blast_tac 1);
   13.67  qed "guarantees_UN_left";
   13.68  
   13.69  Goalw [guar_def]
   13.70 -     "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
   13.71 +     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
   13.72  by (Blast_tac 1);
   13.73  qed "guarantees_Un_left";
   13.74  
   13.75  Goalw [guar_def]
   13.76 -     "X guarantees[v] (INT i:I. Y i) = (INT i:I. X guarantees[v] Y i)";
   13.77 +     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
   13.78  by (Blast_tac 1);
   13.79  qed "guarantees_INT_right";
   13.80  
   13.81  Goalw [guar_def]
   13.82 -     "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
   13.83 +     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
   13.84  by (Blast_tac 1);
   13.85  qed "guarantees_Int_right";
   13.86  
   13.87 -Goal "[| F : Z guarantees[v] X;  F : Z guarantees[v] Y |] \
   13.88 -\    ==> F : Z guarantees[v] (X Int Y)";
   13.89 +Goal "[| F : Z guarantees X;  F : Z guarantees Y |] \
   13.90 +\    ==> F : Z guarantees (X Int Y)";
   13.91  by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
   13.92  qed "guarantees_Int_right_I";
   13.93  
   13.94 -Goal "(F : X guarantees[v] (INTER I Y)) = \
   13.95 -\     (ALL i:I. F : X guarantees[v] (Y i))";
   13.96 +Goal "(F : X guarantees (INTER I Y)) = \
   13.97 +\     (ALL i:I. F : X guarantees (Y i))";
   13.98  by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
   13.99  qed "guarantees_INT_right_iff";
  13.100  
  13.101 -Goalw [guar_def] "(X guarantees[v] Y) = (UNIV guarantees[v] (-X Un Y))";
  13.102 +Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
  13.103  by (Blast_tac 1);
  13.104  qed "shunting";
  13.105  
  13.106 -Goalw [guar_def] "(X guarantees[v] Y) = -Y guarantees[v] -X";
  13.107 +Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
  13.108  by (Blast_tac 1);
  13.109  qed "contrapositive";
  13.110  
  13.111 @@ -157,119 +151,115 @@
  13.112  **)
  13.113  
  13.114  Goalw [guar_def]
  13.115 -    "[| F : V guarantees[v] X;  F : (X Int Y) guarantees[v] Z |]\
  13.116 -\    ==> F : (V Int Y) guarantees[v] Z";
  13.117 +    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
  13.118 +\    ==> F : (V Int Y) guarantees Z";
  13.119  by (Blast_tac 1);
  13.120  qed "combining1";
  13.121  
  13.122  Goalw [guar_def]
  13.123 -    "[| F : V guarantees[v] (X Un Y);  F : Y guarantees[v] Z |]\
  13.124 -\    ==> F : V guarantees[v] (X Un Z)";
  13.125 +    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
  13.126 +\    ==> F : V guarantees (X Un Z)";
  13.127  by (Blast_tac 1);
  13.128  qed "combining2";
  13.129  
  13.130  (** The following two follow Chandy-Sanders, but the use of object-quantifiers
  13.131      does not suit Isabelle... **)
  13.132  
  13.133 -(*Premise should be (!!i. i: I ==> F: X guarantees[v] Y i) *)
  13.134 +(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
  13.135  Goalw [guar_def]
  13.136 -     "ALL i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (INT i:I. Y i)";
  13.137 +     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
  13.138  by (Blast_tac 1);
  13.139  qed "all_guarantees";
  13.140  
  13.141 -(*Premises should be [| F: X guarantees[v] Y i; i: I |] *)
  13.142 +(*Premises should be [| F: X guarantees Y i; i: I |] *)
  13.143  Goalw [guar_def]
  13.144 -     "EX i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (UN i:I. Y i)";
  13.145 +     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
  13.146  by (Blast_tac 1);
  13.147  qed "ex_guarantees";
  13.148  
  13.149  (*** Additional guarantees laws, by lcp ***)
  13.150  
  13.151  Goalw [guar_def]
  13.152 -    "[| F: U guarantees[v] V;  G: X guarantees[v] Y; \
  13.153 -\       F : preserves v;  G : preserves v |] \
  13.154 -\    ==> F Join G: (U Int X) guarantees[v] (V Int Y)";
  13.155 +    "[| F: U guarantees V;  G: X guarantees Y; F ok G |] \
  13.156 +\    ==> F Join G: (U Int X) guarantees (V Int Y)"; 
  13.157  by (Simp_tac 1);
  13.158  by Safe_tac;
  13.159  by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
  13.160  by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
  13.161 -by (Asm_full_simp_tac 1);
  13.162 +by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); 
  13.163  by (asm_simp_tac (simpset() addsimps Join_ac) 1);
  13.164  qed "guarantees_Join_Int";
  13.165  
  13.166  Goalw [guar_def]
  13.167 -    "[| F: U guarantees[v] V;  G: X guarantees[v] Y; \
  13.168 -\       F : preserves v;  G : preserves v |]  \
  13.169 -\    ==> F Join G: (U Un X) guarantees[v] (V Un Y)";
  13.170 +    "[| F: U guarantees V;  G: X guarantees Y; F ok G |]  \
  13.171 +\    ==> F Join G: (U Un X) guarantees (V Un Y)";
  13.172  by (Simp_tac 1);
  13.173  by Safe_tac;
  13.174  by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
  13.175  by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
  13.176 -by (Asm_full_simp_tac 1);
  13.177 +by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1);
  13.178  by (asm_simp_tac (simpset() addsimps Join_ac) 1);
  13.179  qed "guarantees_Join_Un";
  13.180  
  13.181  Goalw [guar_def]
  13.182 -     "[| ALL i:I. F i : X i guarantees[v] Y i;  \
  13.183 -\        ALL i:I. F i : preserves v |] \
  13.184 -\     ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)";
  13.185 +     "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
  13.186 +\     ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
  13.187  by Auto_tac;
  13.188  by (ball_tac 1);
  13.189 -by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
  13.190 +by (rename_tac "i" 1);
  13.191 +by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
  13.192  by (auto_tac
  13.193 -    (claset(),
  13.194 -     simpset() addsimps [Join_assoc RS sym, JN_absorb]));
  13.195 +    (claset() addIs [OK_imp_ok],
  13.196 +     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
  13.197  qed "guarantees_JN_INT";
  13.198  
  13.199  Goalw [guar_def]
  13.200 -    "[| ALL i:I. F i : X i guarantees[v] Y i;  \
  13.201 -\       ALL i:I. F i : preserves v |] \
  13.202 -\    ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)";
  13.203 +    "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
  13.204 +\    ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
  13.205  by Auto_tac;
  13.206  by (ball_tac 1);
  13.207 -by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
  13.208 +by (rename_tac "i" 1);
  13.209 +by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
  13.210  by (auto_tac
  13.211 -    (claset(),
  13.212 -     simpset() addsimps [Join_assoc RS sym, JN_absorb]));
  13.213 +    (claset() addIs [OK_imp_ok],
  13.214 +     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
  13.215  qed "guarantees_JN_INT";
  13.216  
  13.217  Goalw [guar_def]
  13.218 -    "[| ALL i:I. F i : X i guarantees[v] Y i;  \
  13.219 -\       ALL i:I. F i : preserves v |] \
  13.220 -\    ==> (JOIN I F) : (UNION I X) guarantees[v] (UNION I Y)";
  13.221 +    "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
  13.222 +\    ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
  13.223  by Auto_tac;
  13.224  by (ball_tac 1);
  13.225 -by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
  13.226 +by (rename_tac "i" 1);
  13.227 +by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
  13.228  by (auto_tac
  13.229 -    (claset(),
  13.230 -     simpset() addsimps [Join_assoc RS sym, JN_absorb]));
  13.231 +    (claset() addIs [OK_imp_ok],
  13.232 +     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
  13.233  qed "guarantees_JN_UN";
  13.234  
  13.235  
  13.236 -(*** guarantees[v] laws for breaking down the program, by lcp ***)
  13.237 +(*** guarantees laws for breaking down the program, by lcp ***)
  13.238  
  13.239  Goalw [guar_def]
  13.240 -     "[| F: X guarantees[v] Y;  G: preserves v |] \
  13.241 -\     ==> F Join G: X guarantees[v] Y";
  13.242 +     "[| F: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y";
  13.243  by (Simp_tac 1);
  13.244  by Safe_tac;
  13.245  by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
  13.246  qed "guarantees_Join_I1";
  13.247  
  13.248 -Goal "[| G: X guarantees[v] Y;  F: preserves v |] \
  13.249 -\    ==> F Join G: X guarantees[v] Y";
  13.250 -by (stac Join_commute 1);
  13.251 +Goal "[| G: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y";
  13.252 +by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute, 
  13.253 +                                           inst "G" "G" ok_commute]) 1);
  13.254  by (blast_tac (claset() addIs [guarantees_Join_I1]) 1);
  13.255  qed "guarantees_Join_I2";
  13.256  
  13.257  Goalw [guar_def]
  13.258 -     "[| i : I;  F i: X guarantees[v] Y;  \
  13.259 -\        ALL j:I. i~=j --> F j : preserves v |] \
  13.260 -\     ==> (JN i:I. (F i)) : X guarantees[v] Y";
  13.261 +     "[| i : I;  F i: X guarantees Y;  OK I F |] \
  13.262 +\     ==> (JN i:I. (F i)) : X guarantees Y";
  13.263  by (Clarify_tac 1);
  13.264 -by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] bspec 1);
  13.265 -by (auto_tac (claset(),
  13.266 -	      simpset() addsimps [JN_Join_diff, Join_assoc RS sym]));
  13.267 +by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
  13.268 +by (auto_tac (claset() addIs [OK_imp_ok],
  13.269 +	      simpset() addsimps [JN_Join_diff, JN_Join_diff, Join_assoc RS sym]));
  13.270  qed "guarantees_JN_I";
  13.271  
  13.272  
    14.1 --- a/src/HOL/UNITY/Guar.thy	Fri Sep 22 17:25:09 2000 +0200
    14.2 +++ b/src/HOL/UNITY/Guar.thy	Sat Sep 23 16:02:01 2000 +0200
    14.3 @@ -35,11 +35,9 @@
    14.4    welldef :: 'a program set  
    14.5     "welldef == {F. Init F ~= {}}"
    14.6  
    14.7 -  guar :: ['a program set, 'a=>'b, 'a program set] => 'a program set
    14.8 -   ("(_/ guarantees[_]/ _)" [55,0,55] 55)
    14.9 -                              (*higher than membership, lower than Co*)
   14.10 -   "X guarantees[v] Y == {F. ALL G : preserves v. 
   14.11 -                               F Join G : X --> F Join G : Y}"
   14.12 +  guar :: ['a program set, 'a program set] => 'a program set
   14.13 +          (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
   14.14 +   "X guarantees Y == {F. ALL G. F ok G --> F Join G : X --> F Join G : Y}"
   14.15  
   14.16    refines :: ['a program, 'a program, 'a program set] => bool
   14.17  			("(3_ refines _ wrt _)" [10,10,10] 10)
    15.1 --- a/src/HOL/UNITY/Handshake.thy	Fri Sep 22 17:25:09 2000 +0200
    15.2 +++ b/src/HOL/UNITY/Handshake.thy	Sat Sep 23 16:02:01 2000 +0200
    15.3 @@ -21,14 +21,14 @@
    15.4      "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
    15.5  
    15.6    F :: "state program"
    15.7 -    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
    15.8 +    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
    15.9  
   15.10    (*G's program*)
   15.11    cmdG :: "(state*state) set"
   15.12      "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
   15.13  
   15.14    G :: "state program"
   15.15 -    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
   15.16 +    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
   15.17  
   15.18    (*the joint invariant*)
   15.19    invFG :: "state set"
    16.1 --- a/src/HOL/UNITY/Lift.thy	Fri Sep 22 17:25:09 2000 +0200
    16.2 +++ b/src/HOL/UNITY/Lift.thy	Sat Sep 23 16:02:01 2000 +0200
    16.3 @@ -108,6 +108,10 @@
    16.4           {(s,s'). s' = s (|floor := floor s - #1|)
    16.5  		       & ~ stop s & ~ up s & floor s ~: req s}"
    16.6  
    16.7 +  (*This action is omitted from prior treatments, which therefore are
    16.8 +    unrealistic: nobody asks the lift to do anything!  But adding this
    16.9 +    action invalidates many of the existing progress arguments: various
   16.10 +    "ensures" properties fail.*)
   16.11    button_press  :: "(state*state) set"
   16.12      "button_press ==
   16.13           {(s,s'). EX n. s' = s (|req := insert n (req s)|)
   16.14 @@ -119,7 +123,8 @@
   16.15      "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
   16.16  		          ~ open s & req s = {}},
   16.17  			 {request_act, open_act, close_act,
   16.18 -			  req_up, req_down, move_up, move_down})"
   16.19 +			  req_up, req_down, move_up, move_down},
   16.20 +			 UNIV)"
   16.21  
   16.22  
   16.23    (** Invariants **)
    17.1 --- a/src/HOL/UNITY/Lift_prog.ML	Fri Sep 22 17:25:09 2000 +0200
    17.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Sat Sep 23 16:02:01 2000 +0200
    17.3 @@ -133,6 +133,11 @@
    17.4  
    17.5  (*** the lattice operations ***)
    17.6  
    17.7 +Goal "bij (lift i)";
    17.8 +by (simp_tac (simpset() addsimps [lift_def]) 1);
    17.9 +qed "bij_lift";
   17.10 +AddIffs [bij_lift];
   17.11 +
   17.12  Goalw [lift_def] "lift i SKIP = SKIP";
   17.13  by (Asm_simp_tac 1);
   17.14  qed "lift_SKIP";
   17.15 @@ -209,15 +214,14 @@
   17.16  (** guarantees **)
   17.17  
   17.18  Goalw [lift_def]
   17.19 -     "(lift i F : (lift i `` X) guarantees[v o drop_map i] (lift i `` Y)) = \
   17.20 -\     (F : X guarantees[v] Y)";
   17.21 +     "(lift i F : (lift i `` X) guarantees (lift i `` Y)) = \
   17.22 +\     (F : X guarantees Y)";
   17.23  by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1);
   17.24  by (asm_simp_tac (simpset() addsimps [o_def]) 1);
   17.25  qed "lift_lift_guarantees_eq";
   17.26  
   17.27 -Goal "(lift i F : X guarantees[v] Y) = \
   17.28 -\     (F : (rename (drop_map i) `` X) guarantees[v o lift_map i] \
   17.29 -\          (rename (drop_map i) `` Y))";
   17.30 +Goal "(lift i F : X guarantees Y) = \
   17.31 +\     (F : (rename (drop_map i) `` X) guarantees (rename (drop_map i) `` Y))";
   17.32  by (asm_simp_tac 
   17.33      (simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv,
   17.34  			 lift_def]) 1);
   17.35 @@ -409,4 +413,74 @@
   17.36  Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);
   17.37  
   17.38  
   17.39 +(*** More lemmas about extend and project 
   17.40 +     They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
   17.41  
   17.42 +Goal "extend_act h' (extend_act h act) = \
   17.43 +\     extend_act (%(x,(y,y')). h'(h(x,y),y')) act";
   17.44 +by (auto_tac (claset() addSEs [rev_bexI], 
   17.45 +              simpset() addsimps [extend_act_def]));
   17.46 +by (ALLGOALS Blast_tac);
   17.47 +qed "extend_act_extend_act";
   17.48 +
   17.49 +Goal "project_act h (project_act h' act) = \
   17.50 +\     project_act (%(x,(y,y')). h'(h(x,y),y')) act";
   17.51 +by (auto_tac (claset() addSEs [rev_bexI], 
   17.52 +              simpset() addsimps [project_act_def]));    
   17.53 +qed "project_act_project_act";
   17.54 +
   17.55 +Goal "project_act h (extend_act h' act) = \
   17.56 +\       {(x,x'). EX s s' y y' z. (s,s') : act & \
   17.57 +\                h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}";
   17.58 +by (simp_tac (simpset() addsimps [extend_act_def, project_act_def]) 1); 
   17.59 +by (Blast_tac 1); 
   17.60 +qed "project_act_extend_act";
   17.61 +
   17.62 +
   17.63 +(*** OK and "lift" ***)
   17.64 +
   17.65 +Goal "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts";
   17.66 +by (res_inst_tac [("a","mk_program(UNIV,{act},UNIV)")] UN_I 1);
   17.67 +by (auto_tac (claset(),
   17.68 +              simpset() addsimps [preserves_def,stable_def,constrains_def]));  
   17.69 +qed "act_in_UNION_preserves_fst";
   17.70 +
   17.71 +Goal "[| ALL i:I. F i : preserves snd;  \
   17.72 +\        ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |] \
   17.73 +\     ==> OK I (%i. lift i (F i))";
   17.74 +by (auto_tac (claset(), 
   17.75 +      simpset() addsimps [OK_def, lift_def, rename_def, export Acts_extend,
   17.76 +                export AllowedActs_extend, project_act_extend_act]));
   17.77 +by (rename_tac "act" 1);
   17.78 +by (subgoal_tac
   17.79 +    "{(x, x'). EX s f u s' f' u'.   \
   17.80 +\                ((s, f, u), s', f', u') : act &   \
   17.81 +\                lift_map j x  = lift_map i (s, f, u) &   \
   17.82 +\                lift_map j x' = lift_map i (s', f', u')}   \
   17.83 +\    <= {(x,x'). fst x = fst x'}" 1);
   17.84 +by (blast_tac (claset() addIs [act_in_UNION_preserves_fst]) 1);
   17.85 +by (Clarify_tac 1); 
   17.86 +by (REPEAT (dres_inst_tac [("x","j")] fun_cong 1) );
   17.87 +by (dres_inst_tac [("x","i")] bspec 1); 
   17.88 +by (assume_tac 1); 
   17.89 +by (ftac preserves_imp_eq 1);
   17.90 +by Auto_tac;  
   17.91 +qed "UNION_OK_lift_I";
   17.92 +
   17.93 +Goal "[| ALL i:I. F i : preserves snd;  \
   17.94 +\        ALL i:I. preserves fst <= Allowed (F i) |] \
   17.95 +\     ==> OK I (%i. lift i (F i))";
   17.96 +by (asm_full_simp_tac 
   17.97 +    (simpset() addsimps [safety_prop_AllowedActs_iff_Allowed, 
   17.98 +                         UNION_OK_lift_I]) 1); 
   17.99 +qed "OK_lift_I";
  17.100 +
  17.101 +Goal "Allowed (lift i F) = lift i `` (Allowed F)";
  17.102 +by (simp_tac (simpset() addsimps [lift_def, Allowed_rename]) 1); 
  17.103 +qed "Allowed_lift"; 
  17.104 +Addsimps [Allowed_lift];
  17.105 +
  17.106 +Goal "lift i `` preserves v = preserves (v o drop_map i)";
  17.107 +by (simp_tac (simpset() addsimps [rename_image_preserves, lift_def, 
  17.108 +                                  inv_lift_map_eq]) 1); 
  17.109 +qed "lift_image_preserves";
    18.1 --- a/src/HOL/UNITY/Mutex.thy	Fri Sep 22 17:25:09 2000 +0200
    18.2 +++ b/src/HOL/UNITY/Mutex.thy	Sat Sep 23 16:02:01 2000 +0200
    18.3 @@ -55,7 +55,8 @@
    18.4  
    18.5    Mutex :: state program
    18.6      "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
    18.7 -		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4})"
    18.8 +		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
    18.9 +			  UNIV)"
   18.10  
   18.11  
   18.12    (** The correct invariants **)
    19.1 --- a/src/HOL/UNITY/NSP_Bad.thy	Fri Sep 22 17:25:09 2000 +0200
    19.2 +++ b/src/HOL/UNITY/NSP_Bad.thy	Sat Sep 23 16:02:01 2000 +0200
    19.3 @@ -54,6 +54,6 @@
    19.4  constdefs
    19.5    Nprg :: state program
    19.6      (*Initial trace is empty*)
    19.7 -    "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})"
    19.8 +    "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
    19.9  
   19.10  end
    20.1 --- a/src/HOL/UNITY/PPROD.ML	Fri Sep 22 17:25:09 2000 +0200
    20.2 +++ b/src/HOL/UNITY/PPROD.ML	Sat Sep 23 16:02:01 2000 +0200
    20.3 @@ -121,12 +121,21 @@
    20.4    something like lift_preserves_sub to rewrite the third.  However there's
    20.5    no obvious way to alternative for the third premise.*)
    20.6  Goalw [PLam_def]
    20.7 -    "[| lift i (F i): X guarantees[v] Y;  i : I;  \
    20.8 -\        ALL j:I. i~=j --> lift j (F j) : preserves v |]  \
    20.9 -\    ==> (PLam I F) : X guarantees[v] Y";
   20.10 +    "[| lift i (F i): X guarantees Y;  i : I;  \
   20.11 +\       OK I (%i. lift i (F i)) |]  \
   20.12 +\    ==> (PLam I F) : X guarantees Y"; 
   20.13  by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
   20.14  qed "guarantees_PLam_I";
   20.15  
   20.16 +Goal "Allowed (PLam I F) = (INT i:I. lift i `` Allowed(F i))";
   20.17 +by (simp_tac (simpset() addsimps [PLam_def]) 1); 
   20.18 +qed "Allowed_PLam";
   20.19 +Addsimps [Allowed_PLam];
   20.20 +
   20.21 +Goal "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))";
   20.22 +by (simp_tac (simpset() addsimps [PLam_def, lift_def, rename_preserves]) 1); 
   20.23 +qed "PLam_preserves";
   20.24 +Addsimps [PLam_preserves];
   20.25  
   20.26  (**UNUSED
   20.27      (*The f0 premise ensures that the product is well-defined.*)
    21.1 --- a/src/HOL/UNITY/Project.ML	Fri Sep 22 17:25:09 2000 +0200
    21.2 +++ b/src/HOL/UNITY/Project.ML	Sat Sep 23 16:02:01 2000 +0200
    21.3 @@ -120,38 +120,36 @@
    21.4  qed "projecting_weaken_L";
    21.5  
    21.6  Goalw [extending_def]
    21.7 -     "[| extending v C h F YA' YA;  extending v C h F YB' YB |] \
    21.8 -\     ==> extending v C h F (YA' Int YB') (YA Int YB)";
    21.9 +     "[| extending C h F YA' YA;  extending C h F YB' YB |] \
   21.10 +\     ==> extending C h F (YA' Int YB') (YA Int YB)";
   21.11  by (Blast_tac 1);
   21.12  qed "extending_Int";
   21.13  
   21.14  Goalw [extending_def]
   21.15 -     "[| extending v C h F YA' YA;  extending v C h F YB' YB |] \
   21.16 -\     ==> extending v C h F (YA' Un YB') (YA Un YB)";
   21.17 +     "[| extending C h F YA' YA;  extending C h F YB' YB |] \
   21.18 +\     ==> extending C h F (YA' Un YB') (YA Un YB)";
   21.19  by (Blast_tac 1);
   21.20  qed "extending_Un";
   21.21  
   21.22  val [prem] = Goalw [extending_def]
   21.23 -     "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
   21.24 -\     ==> extending v C h F (INT i:I. Y' i) (INT i:I. Y i)";
   21.25 +     "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] \
   21.26 +\     ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)";
   21.27  by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
   21.28  qed "extending_INT";
   21.29  
   21.30  val [prem] = Goalw [extending_def]
   21.31 -     "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
   21.32 -\     ==> extending v C h F (UN i:I. Y' i) (UN i:I. Y i)";
   21.33 +     "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] \
   21.34 +\     ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)";
   21.35  by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
   21.36  qed "extending_UN";
   21.37  
   21.38  Goalw [extending_def]
   21.39 -     "[| extending v C h F Y' Y;  Y'<=V';  V<=Y; \
   21.40 -\        preserves w <= preserves v |] \
   21.41 -\     ==> extending w C h F V' V";
   21.42 +     "[| extending C h F Y' Y;  Y'<=V';  V<=Y |] ==> extending C h F V' V";
   21.43  by Auto_tac;
   21.44  qed "extending_weaken";
   21.45  
   21.46  Goalw [extending_def]
   21.47 -     "[| extending v C h F Y' Y;  Y'<=V' |] ==> extending v C h F V' Y";
   21.48 +     "[| extending C h F Y' Y;  Y'<=V' |] ==> extending C h F V' Y";
   21.49  by Auto_tac;
   21.50  qed "extending_weaken_L";
   21.51  
   21.52 @@ -174,22 +172,22 @@
   21.53  by (blast_tac (claset() addIs [project_increasing_I]) 1);
   21.54  qed "projecting_increasing";
   21.55  
   21.56 -Goal "extending v C h F UNIV Y";
   21.57 +Goal "extending C h F UNIV Y";
   21.58  by (simp_tac (simpset() addsimps [extending_def]) 1);
   21.59  qed "extending_UNIV";
   21.60  
   21.61  Goalw [extending_def]
   21.62 -     "extending v (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)";
   21.63 +     "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)";
   21.64  by (blast_tac (claset() addIs [project_constrains_D]) 1);
   21.65  qed "extending_constrains";
   21.66  
   21.67  Goalw [stable_def]
   21.68 -     "extending v (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
   21.69 +     "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
   21.70  by (rtac extending_constrains 1);
   21.71  qed "extending_stable";
   21.72  
   21.73  Goalw [extending_def]
   21.74 -     "extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
   21.75 +     "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)";
   21.76  by (simp_tac (HOL_ss addsimps [Join_project_increasing]) 1);
   21.77  qed "extending_increasing";
   21.78  
   21.79 @@ -354,25 +352,25 @@
   21.80  qed "projecting_Increasing";
   21.81  
   21.82  Goalw [extending_def]
   21.83 -     "extending v (%G. reachable (extend h F Join G)) h F \
   21.84 +     "extending (%G. reachable (extend h F Join G)) h F \
   21.85  \                 (extend_set h A Co extend_set h B) (A Co B)";
   21.86  by (blast_tac (claset() addIs [project_Constrains_D]) 1);
   21.87  qed "extending_Constrains";
   21.88  
   21.89  Goalw [extending_def]
   21.90 -     "extending v (%G. reachable (extend h F Join G)) h F \
   21.91 +     "extending (%G. reachable (extend h F Join G)) h F \
   21.92  \                 (Stable (extend_set h A)) (Stable A)";
   21.93  by (blast_tac (claset() addIs [project_Stable_D]) 1);
   21.94  qed "extending_Stable";
   21.95  
   21.96  Goalw [extending_def]
   21.97 -     "extending v (%G. reachable (extend h F Join G)) h F \
   21.98 +     "extending (%G. reachable (extend h F Join G)) h F \
   21.99  \                 (Always (extend_set h A)) (Always A)";
  21.100  by (blast_tac (claset() addIs [project_Always_D]) 1);
  21.101  qed "extending_Always";
  21.102  
  21.103  Goalw [extending_def]
  21.104 -     "extending v (%G. reachable (extend h F Join G)) h F \
  21.105 +     "extending (%G. reachable (extend h F Join G)) h F \
  21.106  \                 (Increasing (func o f)) (Increasing func)";
  21.107  by (blast_tac (claset() addIs [project_Increasing_D]) 1);
  21.108  qed "extending_Increasing";
  21.109 @@ -596,31 +594,46 @@
  21.110  
  21.111  (*** Guarantees ***)
  21.112  
  21.113 +Goal "project_act h (Restrict C act) <= project_act h act";
  21.114 +by (auto_tac (claset(), simpset() addsimps [project_act_def]));  
  21.115 +qed "project_act_Restrict_subset_project_act";
  21.116 +					   
  21.117 +							   
  21.118 +Goal "[| extend h F ok G; subset_closed (AllowedActs F) |] \
  21.119 +\     ==> F ok project h C G";
  21.120 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
  21.121 +by (dtac subsetD 1);   
  21.122 +by (Blast_tac 1); 
  21.123 +by (force_tac (claset() addSIs [rev_image_eqI], simpset()) 1);
  21.124 +by (cut_facts_tac [project_act_Restrict_subset_project_act] 1);
  21.125 +by (auto_tac (claset(), simpset() addsimps [subset_closed_def]));  
  21.126 +qed "subset_closed_ok_extend_imp_ok_project";
  21.127 +
  21.128 +
  21.129  (*Weak precondition and postcondition
  21.130    Not clear that it has a converse [or that we want one!]*)
  21.131  
  21.132  (*The raw version; 3rd premise could be weakened by adding the
  21.133    precondition extend h F Join G : X' *)
  21.134 -val [xguary,project,extend] =
  21.135 -Goal "[| F : X guarantees[v] Y;  \
  21.136 +val [xguary,closed,project,extend] =
  21.137 +Goal "[| F : X guarantees Y;  subset_closed (AllowedActs F);  \
  21.138  \        !!G. extend h F Join G : X' ==> F Join project h (C G) G : X;  \
  21.139 -\        !!G. [| F Join project h (C G) G : Y; G : preserves (v o f) |] \
  21.140 +\        !!G. [| F Join project h (C G) G : Y |] \
  21.141  \             ==> extend h F Join G : Y' |] \
  21.142 -\     ==> extend h F : X' guarantees[v o f] Y'";
  21.143 +\     ==> extend h F : X' guarantees Y'";
  21.144  by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
  21.145 -by (etac project_preserves_I 1);
  21.146 +by (blast_tac (claset() addIs [closed, 
  21.147 +          subset_closed_ok_extend_imp_ok_project]) 1); 
  21.148  by (etac project 1);
  21.149 -by Auto_tac;
  21.150  qed "project_guarantees_raw";
  21.151  
  21.152 -Goal "[| F : X guarantees[v] Y;  \
  21.153 -\        projecting C h F X' X;  extending w C h F Y' Y; \
  21.154 -\        preserves w <= preserves (v o f) |] \
  21.155 -\     ==> extend h F : X' guarantees[w] Y'";
  21.156 +Goal "[| F : X guarantees Y;  subset_closed (AllowedActs F); \
  21.157 +\        projecting C h F X' X;  extending C h F Y' Y |] \
  21.158 +\     ==> extend h F : X' guarantees Y'";
  21.159  by (rtac guaranteesI 1);
  21.160  by (auto_tac (claset(), 
  21.161 -        simpset() addsimps [project_preserves_I, guaranteesD, projecting_def,
  21.162 -			    extending_def]));
  21.163 +        simpset() addsimps [guaranteesD, projecting_def, 
  21.164 +                    extending_def, subset_closed_ok_extend_imp_ok_project]));
  21.165  qed "project_guarantees";
  21.166  
  21.167  
  21.168 @@ -631,28 +644,31 @@
  21.169  
  21.170  (** Some could be deleted: the required versions are easy to prove **)
  21.171  
  21.172 -Goal "F : UNIV guarantees[v] increasing func \
  21.173 -\     ==> extend h F : X' guarantees[v o f] increasing (func o f)";
  21.174 +Goal "[| F : UNIV guarantees increasing func;  \
  21.175 +\        subset_closed (AllowedActs F) |] \
  21.176 +\     ==> extend h F : X' guarantees increasing (func o f)";
  21.177  by (etac project_guarantees 1);
  21.178 -by (rtac extending_increasing 2);
  21.179 -by (rtac projecting_UNIV 1);
  21.180 +by (rtac extending_increasing 3);
  21.181 +by (rtac projecting_UNIV 2);
  21.182  by Auto_tac;
  21.183  qed "extend_guar_increasing";
  21.184  
  21.185 -Goal "F : UNIV guarantees[v] Increasing func \
  21.186 -\     ==> extend h F : X' guarantees[v o f] Increasing (func o f)";
  21.187 +Goal "[| F : UNIV guarantees Increasing func;  \
  21.188 +\        subset_closed (AllowedActs F) |] \
  21.189 +\     ==> extend h F : X' guarantees Increasing (func o f)";
  21.190  by (etac project_guarantees 1);
  21.191 -by (rtac extending_Increasing 2);
  21.192 -by (rtac projecting_UNIV 1);
  21.193 +by (rtac extending_Increasing 3);
  21.194 +by (rtac projecting_UNIV 2);
  21.195  by Auto_tac;
  21.196  qed "extend_guar_Increasing";
  21.197  
  21.198 -Goal "F : Always A guarantees[v] Always B \
  21.199 -\     ==> extend h F : Always(extend_set h A) guarantees[v o f] \
  21.200 -\                      Always(extend_set h B)";
  21.201 +Goal "[| F : Always A guarantees Always B;  \
  21.202 +\        subset_closed (AllowedActs F) |] \
  21.203 +\     ==> extend h F                   \
  21.204 +\           : Always(extend_set h A) guarantees Always(extend_set h B)";
  21.205  by (etac project_guarantees 1);
  21.206 -by (rtac extending_Always 2);
  21.207 -by (rtac projecting_Always 1);
  21.208 +by (rtac extending_Always 3);
  21.209 +by (rtac projecting_Always 2);
  21.210  by Auto_tac;
  21.211  qed "extend_guar_Always";
  21.212  
  21.213 @@ -676,8 +692,8 @@
  21.214  	      simpset()));
  21.215  qed "project_leadsTo_D";
  21.216  
  21.217 -Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
  21.218 -\         G : preserves f |]  \
  21.219 +Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B;    \
  21.220 +\        G : preserves f |]  \
  21.221  \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
  21.222  by (rtac (refl RS Join_project_LeadsTo) 1);
  21.223  by (auto_tac (claset() addDs [preserves_project_transient_empty], 
  21.224 @@ -685,35 +701,17 @@
  21.225  qed "project_LeadsTo_D";
  21.226  
  21.227  Goalw [extending_def]
  21.228 -     "extending f (%G. UNIV) h F \
  21.229 +     "(ALL G. extend h F ok G --> G : preserves f) \
  21.230 +\     ==> extending (%G. UNIV) h F \
  21.231  \                 (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
  21.232  by (blast_tac (claset() addIs [project_leadsTo_D]) 1);
  21.233  qed "extending_leadsTo";
  21.234  
  21.235  Goalw [extending_def]
  21.236 -     "extending f (%G. reachable (extend h F Join G)) h F \
  21.237 +     "(ALL G. extend h F ok G --> G : preserves f) \
  21.238 +\     ==> extending (%G. reachable (extend h F Join G)) h F \
  21.239  \                 (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
  21.240  by (blast_tac (claset() addIs [project_LeadsTo_D]) 1);
  21.241  qed "extending_LeadsTo";
  21.242  
  21.243 -(*STRONG precondition and postcondition*)
  21.244 -Goal "F : (A co A') guarantees[v] (B leadsTo B')  \
  21.245 -\ ==> extend h F : (extend_set h A co extend_set h A') \
  21.246 -\                  guarantees[f] (extend_set h B leadsTo extend_set h B')";
  21.247 -by (etac project_guarantees 1);
  21.248 -by (rtac subset_preserves_o 3);
  21.249 -by (rtac extending_leadsTo 2);
  21.250 -by (rtac projecting_constrains 1);
  21.251 -qed "extend_co_guar_leadsTo";
  21.252 -
  21.253 -(*WEAK precondition and postcondition*)
  21.254 -Goal "F : (A Co A') guarantees[v] (B LeadsTo B')  \
  21.255 -\ ==> extend h F : (extend_set h A Co extend_set h A') \
  21.256 -\                  guarantees[f] (extend_set h B LeadsTo extend_set h B')";
  21.257 -by (etac project_guarantees 1);
  21.258 -by (rtac subset_preserves_o 3);
  21.259 -by (rtac extending_LeadsTo 2);
  21.260 -by (rtac projecting_Constrains 1);
  21.261 -qed "extend_Co_guar_LeadsTo";
  21.262 -
  21.263  Close_locale "Extend";
    22.1 --- a/src/HOL/UNITY/Project.thy	Fri Sep 22 17:25:09 2000 +0200
    22.2 +++ b/src/HOL/UNITY/Project.thy	Sat Sep 23 16:02:01 2000 +0200
    22.3 @@ -13,13 +13,16 @@
    22.4  constdefs
    22.5    projecting :: "['c program => 'c set, 'a*'b => 'c, 
    22.6  		  'a program, 'c program set, 'a program set] => bool"
    22.7 -  "projecting C h F X' X ==
    22.8 -     ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
    22.9 +    "projecting C h F X' X ==
   22.10 +       ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
   22.11  
   22.12 -  extending :: "['c=>'d, 'c program => 'c set, 'a*'b => 'c, 'a program, 
   22.13 +  extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
   22.14  		 'c program set, 'a program set] => bool"
   22.15 -  "extending v C h F Y' Y ==
   22.16 -     ALL G. G : preserves v --> F Join project h (C G) G : Y
   22.17 -            --> extend h F Join G : Y'"
   22.18 +    "extending C h F Y' Y ==
   22.19 +       ALL G. extend h F  ok G --> F Join project h (C G) G : Y
   22.20 +	      --> extend h F Join G : Y'"
   22.21 +
   22.22 +  subset_closed :: "'a set set => bool"
   22.23 +    "subset_closed U == ALL A: U. Pow A <= U"  
   22.24  
   22.25  end
    23.1 --- a/src/HOL/UNITY/Reach.thy	Fri Sep 22 17:25:09 2000 +0200
    23.2 +++ b/src/HOL/UNITY/Reach.thy	Sat Sep 23 16:02:01 2000 +0200
    23.3 @@ -24,7 +24,7 @@
    23.4      "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
    23.5  
    23.6    Rprg :: state program
    23.7 -    "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})"
    23.8 +    "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)"
    23.9  
   23.10    reach_invariant :: state set
   23.11      "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
    24.1 --- a/src/HOL/UNITY/Rename.ML	Fri Sep 22 17:25:09 2000 +0200
    24.2 +++ b/src/HOL/UNITY/Rename.ML	Sat Sep 23 16:02:01 2000 +0200
    24.3 @@ -13,6 +13,7 @@
    24.4  by Auto_tac;
    24.5  qed "good_map_bij";
    24.6  Addsimps [good_map_bij];
    24.7 +AddIs    [good_map_bij];
    24.8  
    24.9  fun bij_export th = good_map_bij RS export th |> simplify (simpset());
   24.10  
   24.11 @@ -57,12 +58,35 @@
   24.12  (** for "rename" (programs) **)
   24.13  
   24.14  Goal "bij h \
   24.15 -\     ==> extend_act (%(x,u::'c). inv h x) = project_act (%(x,u::'c). h x)";
   24.16 +\     ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)";
   24.17  by (rtac ext 1);
   24.18  by (auto_tac (claset() addSIs [image_eqI], 
   24.19  	      simpset() addsimps [extend_act_def, project_act_def, bij_def,
   24.20  				  surj_f_inv_f]));
   24.21 -qed "extend_act_inv";
   24.22 +qed "bij_extend_act_eq_project_act";
   24.23 +
   24.24 +Goal "bij h ==> bij (extend_act (%(x,u::'c). h x))";
   24.25 +by (rtac bijI 1);
   24.26 +by (rtac (export inj_extend_act) 1);
   24.27 +by (auto_tac (claset(), simpset() addsimps [bij_extend_act_eq_project_act]));  
   24.28 +by (blast_tac (claset() addIs [bij_imp_bij_inv, surjI, 
   24.29 +                               export extend_act_inverse]) 1); 
   24.30 +qed "bij_extend_act";
   24.31 +
   24.32 +Goal "bij h ==> bij (project_act (%(x,u::'c). h x))";
   24.33 +by (ftac (bij_imp_bij_inv RS bij_extend_act) 1);
   24.34 +by (asm_full_simp_tac (simpset() addsimps [bij_extend_act_eq_project_act,
   24.35 +                                    bij_imp_bij_inv, inv_inv_eq]) 1);  
   24.36 +qed "bij_project_act";
   24.37 +
   24.38 +Goal "bij h ==> inv (project_act (%(x,u::'c). inv h x)) = \
   24.39 +\               project_act (%(x,u::'c). h x)";
   24.40 +by (asm_simp_tac
   24.41 +    (simpset() addsimps [bij_extend_act_eq_project_act RS sym]) 1); 
   24.42 +by (rtac surj_imp_inv_eq 1);
   24.43 +by (blast_tac (claset() addIs [bij_extend_act, bij_is_surj]) 1);  
   24.44 +by (asm_simp_tac (simpset() addsimps [export extend_act_inverse]) 1); 
   24.45 +qed "bij_inv_project_act_eq";
   24.46  
   24.47  Goal "bij h  \
   24.48  \     ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV";
   24.49 @@ -71,8 +95,14 @@
   24.50  by (rtac program_equalityI 1);
   24.51  by (asm_simp_tac
   24.52      (simpset() addsimps [export project_act_Id, export Acts_extend,
   24.53 -			 insert_Id_image_Acts, extend_act_inv]) 2);
   24.54 +			 insert_Id_image_Acts, bij_extend_act_eq_project_act, 
   24.55 +                         inv_inv_eq]) 2);
   24.56  by (asm_simp_tac (simpset() addsimps [extend_set_inv]) 1);
   24.57 +by (asm_simp_tac
   24.58 +    (simpset() addsimps [export AllowedActs_extend,
   24.59 +			 export AllowedActs_project,
   24.60 +			 bij_project_act, bij_vimage_eq_inv_image,
   24.61 +                         bij_inv_project_act_eq]) 1);
   24.62  qed "extend_inv";
   24.63  
   24.64  Goal "bij h ==> rename (inv h) (rename h F) = F";
   24.65 @@ -94,24 +124,45 @@
   24.66  
   24.67  (** (rename h) is bijective <=> h is bijective **)
   24.68  
   24.69 -Goal "bij h ==> inj (rename h)";
   24.70 -by (asm_simp_tac (simpset() addsimps [inj_iff, expand_fun_eq, o_def, 
   24.71 -				      rename_inv_eq RS sym]) 1);
   24.72 -qed "inj_rename";
   24.73 +Goal "bij h ==> bij (extend (%(x,u::'c). h x))";
   24.74 +by (rtac bijI 1);
   24.75 +by (blast_tac (claset() addIs [export inj_extend]) 1);
   24.76 +by (res_inst_tac [("f","extend (%(x,u). inv h x)")] surjI 1); 
   24.77 +by (stac ((inst "f" "h" inv_inv_eq) RS sym) 1
   24.78 +    THEN stac extend_inv 2 THEN stac (export extend_inverse) 3);
   24.79 +by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, inv_inv_eq]));
   24.80 +qed "bij_extend";
   24.81 +
   24.82 +Goal "bij h ==> bij (project (%(x,u::'c). h x) UNIV)";
   24.83 +by (stac (extend_inv RS sym) 1); 
   24.84 +by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, bij_extend]));
   24.85 +qed "bij_project";
   24.86  
   24.87 -Goal "bij h ==> surj (rename h)";
   24.88 -by (asm_simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def, 
   24.89 -				      rename_inv_eq RS sym]) 1);
   24.90 -qed "surj_rename";
   24.91 +Goal "bij h  \
   24.92 +\     ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)";
   24.93 +by (rtac inj_imp_inv_eq 1); 
   24.94 +by (etac (bij_project RS bij_is_inj) 1); 
   24.95 +by (asm_simp_tac (simpset() addsimps [export extend_inverse]) 1); 
   24.96 +qed "inv_project_eq";
   24.97 +
   24.98 +Goal "bij h ==> Allowed (rename h F) = rename h `` Allowed F";
   24.99 +by (asm_simp_tac (simpset() addsimps [rename_def, export Allowed_extend]) 1);
  24.100 +by (stac bij_vimage_eq_inv_image 1); 
  24.101 +by (rtac bij_project 1); 
  24.102 +by (Blast_tac 1); 
  24.103 +by (asm_simp_tac (simpset() addsimps [inv_project_eq]) 1);
  24.104 +qed "Allowed_rename"; 
  24.105 +Addsimps [Allowed_rename];
  24.106  
  24.107  Goal "bij h ==> bij (rename h)";
  24.108 -by (blast_tac (claset() addIs [bijI, inj_rename, surj_rename]) 1);
  24.109 +by (asm_simp_tac (simpset() addsimps [rename_def, bij_extend]) 1); 
  24.110  qed "bij_rename";
  24.111 +bind_thm ("surj_rename", bij_rename RS bij_is_surj);
  24.112  
  24.113  Goalw [inj_on_def] "inj (rename h) ==> inj h";
  24.114  by Auto_tac;
  24.115 -by (dres_inst_tac [("x", "mk_program ({x}, {})")] spec 1);
  24.116 -by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
  24.117 +by (dres_inst_tac [("x", "mk_program ({x}, {}, {})")] spec 1);
  24.118 +by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1);
  24.119  by (auto_tac (claset(), 
  24.120  	      simpset() addsimps [program_equality_iff, 
  24.121                                    rename_def, extend_def]));
  24.122 @@ -119,7 +170,7 @@
  24.123  
  24.124  Goalw [surj_def] "surj (rename h) ==> surj h";
  24.125  by Auto_tac;
  24.126 -by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
  24.127 +by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1);
  24.128  by (auto_tac (claset(), 
  24.129  	      simpset() addsimps [program_equality_iff, 
  24.130                                    rename_def, extend_def]));
  24.131 @@ -135,6 +186,7 @@
  24.132  qed "bij_rename_iff";
  24.133  AddIffs [bij_rename_iff];
  24.134  
  24.135 +
  24.136  (*** the lattice operations ***)
  24.137  
  24.138  Goalw [rename_def] "bij h ==> rename h SKIP = SKIP";
  24.139 @@ -236,16 +288,16 @@
  24.140  qed "rename_LeadsTo";
  24.141  
  24.142  Goalw [rename_def]
  24.143 -     "bij h ==> (rename h F : (rename h `` X) guarantees[v o inv h] \
  24.144 +     "bij h ==> (rename h F : (rename h `` X) guarantees \
  24.145  \                             (rename h `` Y)) = \
  24.146 -\               (F : X guarantees[v] Y)";
  24.147 +\               (F : X guarantees Y)";
  24.148  by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1);
  24.149  by (assume_tac 1);
  24.150  by (asm_simp_tac (simpset() addsimps [fst_o_inv_eq_inv, o_def]) 1);
  24.151  qed "rename_rename_guarantees_eq";
  24.152  
  24.153 -Goal "bij h ==> (rename h F : X guarantees[v] Y) = \
  24.154 -\               (F : (rename (inv h) `` X) guarantees[v o h] \
  24.155 +Goal "bij h ==> (rename h F : X guarantees Y) = \
  24.156 +\               (F : (rename (inv h) `` X) guarantees \
  24.157  \                    (rename (inv h) `` Y))";
  24.158  by (stac (rename_rename_guarantees_eq RS sym) 1);
  24.159  by (assume_tac 1);
  24.160 @@ -260,6 +312,16 @@
  24.161  				      bij_is_surj RS surj_f_inv_f]) 1);
  24.162  qed "rename_preserves";
  24.163  
  24.164 +Goal "bij h ==> (rename h F ok rename h G) = (F ok G)";
  24.165 +by (asm_simp_tac (simpset() addsimps [export ok_extend_iff, rename_def]) 1); 
  24.166 +qed "ok_rename_iff";
  24.167 +Addsimps [ok_rename_iff];
  24.168 +
  24.169 +Goal "bij h ==> OK I (%i. rename h (F i)) = (OK I F)";
  24.170 +by (asm_simp_tac (simpset() addsimps [export OK_extend_iff, rename_def]) 1); 
  24.171 +qed "OK_rename_iff";
  24.172 +Addsimps [OK_rename_iff];
  24.173 +
  24.174  
  24.175  (*** "image" versions of the rules, for lifting "guarantees" properties ***)
  24.176  
  24.177 @@ -294,6 +356,11 @@
  24.178  by (rename_image_tac [rename_Constrains]);
  24.179  qed "rename_image_Constrains";
  24.180  
  24.181 +Goal "bij h ==> rename h `` preserves v = preserves (v o inv h)";
  24.182 +by (asm_simp_tac (simpset() addsimps [o_def, rename_image_stable,
  24.183 +                    preserves_def, bij_image_INT, bij_image_Collect_eq]) 1); 
  24.184 +qed "rename_image_preserves";
  24.185 +
  24.186  Goal "bij h ==> rename h `` Stable A = Stable (h `` A)";
  24.187  by (rename_image_tac [rename_Stable]);
  24.188  qed "rename_image_Stable";
    25.1 --- a/src/HOL/UNITY/TimerArray.thy	Fri Sep 22 17:25:09 2000 +0200
    25.2 +++ b/src/HOL/UNITY/TimerArray.thy	Sat Sep 23 16:02:01 2000 +0200
    25.3 @@ -18,6 +18,6 @@
    25.4      "decr == UN n uu. {((Suc n, uu), (n,uu))}"
    25.5    
    25.6    Timer :: 'a state program
    25.7 -    "Timer == mk_program (UNIV, {decr})"
    25.8 +    "Timer == mk_program (UNIV, {decr}, UNIV)"
    25.9  
   25.10  end
    26.1 --- a/src/HOL/UNITY/UNITY.ML	Fri Sep 22 17:25:09 2000 +0200
    26.2 +++ b/src/HOL/UNITY/UNITY.ML	Sat Sep 23 16:02:01 2000 +0200
    26.3 @@ -8,16 +8,14 @@
    26.4  From Misra, "A Logic for Concurrent Programming", 1994
    26.5  *)
    26.6  
    26.7 -set timing;
    26.8 -
    26.9  (*Perhaps equalities.ML shouldn't add this in the first place!*)
   26.10  Delsimps [image_Collect];
   26.11  
   26.12 -
   26.13  (*** The abstract type of programs ***)
   26.14  
   26.15  val rep_ss = simpset() addsimps 
   26.16 -                [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, 
   26.17 +                [Init_def, Acts_def, AllowedActs_def, 
   26.18 +		 mk_program_def, Program_def, Rep_Program, 
   26.19  		 Rep_Program_inverse, Abs_Program_inverse];
   26.20  
   26.21  
   26.22 @@ -32,41 +30,59 @@
   26.23  qed "insert_Id_Acts";
   26.24  AddIffs [insert_Id_Acts];
   26.25  
   26.26 +Goal "Id : AllowedActs F";
   26.27 +by (cut_inst_tac [("x", "F")] Rep_Program 1);
   26.28 +by (auto_tac (claset(), rep_ss));
   26.29 +qed "Id_in_AllowedActs";
   26.30 +AddIffs [Id_in_AllowedActs];
   26.31 +
   26.32 +Goal "insert Id (AllowedActs F) = AllowedActs F";
   26.33 +by (simp_tac (simpset() addsimps [insert_absorb, Id_in_AllowedActs]) 1);
   26.34 +qed "insert_Id_AllowedActs";
   26.35 +AddIffs [insert_Id_AllowedActs];
   26.36 +
   26.37  (** Inspectors for type "program" **)
   26.38  
   26.39 -Goal "Init (mk_program (init,acts)) = init";
   26.40 +Goal "Init (mk_program (init,acts,allowed)) = init";
   26.41  by (auto_tac (claset(), rep_ss));
   26.42  qed "Init_eq";
   26.43  
   26.44 -Goal "Acts (mk_program (init,acts)) = insert Id acts";
   26.45 +Goal "Acts (mk_program (init,acts,allowed)) = insert Id acts";
   26.46  by (auto_tac (claset(), rep_ss));
   26.47  qed "Acts_eq";
   26.48  
   26.49 -Addsimps [Acts_eq, Init_eq];
   26.50 +Goal "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed";
   26.51 +by (auto_tac (claset(), rep_ss));
   26.52 +qed "AllowedActs_eq";
   26.53  
   26.54 +Addsimps [Init_eq, Acts_eq, AllowedActs_eq];
   26.55  
   26.56  (** Equality for UNITY programs **)
   26.57  
   26.58 -Goal "mk_program (Init F, Acts F) = F";
   26.59 +Goal "mk_program (Init F, Acts F, AllowedActs F) = F";
   26.60  by (cut_inst_tac [("x", "F")] Rep_Program 1);
   26.61  by (auto_tac (claset(), rep_ss));
   26.62  by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
   26.63  by (asm_full_simp_tac (rep_ss addsimps [insert_absorb]) 1);
   26.64  qed "surjective_mk_program";
   26.65  
   26.66 -Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
   26.67 +Goal "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] \
   26.68 +\     ==> F = G";
   26.69  by (res_inst_tac [("t", "F")] (surjective_mk_program RS subst) 1);
   26.70  by (res_inst_tac [("t", "G")] (surjective_mk_program RS subst) 1);
   26.71  by (Asm_simp_tac 1);
   26.72  qed "program_equalityI";
   26.73  
   26.74  val [major,minor] =
   26.75 -Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
   26.76 +Goal "[| F = G; \
   26.77 +\        [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]\
   26.78 +\        ==> P |] ==> P";
   26.79  by (rtac minor 1);
   26.80  by (auto_tac (claset(), simpset() addsimps [major]));
   26.81  qed "program_equalityE";
   26.82  
   26.83 -Goal "(F=G) = (Init F = Init G & Acts F = Acts G)";
   26.84 +Goal "(F=G) =  \
   26.85 +\     (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)";
   26.86  by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1);
   26.87  qed "program_equality_iff";
   26.88  
   26.89 @@ -77,13 +93,22 @@
   26.90       They avoid expanding the full program, which is a large expression
   26.91  ***)
   26.92  
   26.93 -Goal "F == mk_program (init,acts) ==> Init F = init";
   26.94 +Goal "F == mk_program (init,acts,allowed) ==> Init F = init";
   26.95  by Auto_tac;
   26.96  qed "def_prg_Init";
   26.97  
   26.98 +Goal "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts";
   26.99 +by Auto_tac;
  26.100 +qed "def_prg_Acts";
  26.101 +
  26.102 +Goal "F == mk_program (init,acts,allowed) \
  26.103 +\     ==> AllowedActs F = insert Id allowed";
  26.104 +by Auto_tac;
  26.105 +qed "def_prg_AllowedActs";
  26.106 +
  26.107  (*The program is not expanded, but its Init and Acts are*)
  26.108  val [rew] = goal thy
  26.109 -    "[| F == mk_program (init,acts) |] \
  26.110 +    "[| F == mk_program (init,acts,allowed) |] \
  26.111  \    ==> Init F = init & Acts F = insert Id acts";
  26.112  by (rewtac rew);
  26.113  by Auto_tac;
    27.1 --- a/src/HOL/UNITY/UNITY.thy	Fri Sep 22 17:25:09 2000 +0200
    27.2 +++ b/src/HOL/UNITY/UNITY.thy	Sat Sep 23 16:02:01 2000 +0200
    27.3 @@ -11,21 +11,30 @@
    27.4  UNITY = Main + 
    27.5  
    27.6  typedef (Program)
    27.7 -  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
    27.8 +  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
    27.9 +		  allowed :: ('a * 'a)set set). Id:acts & Id: allowed}"
   27.10  
   27.11  consts
   27.12    constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
   27.13    op_unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
   27.14  
   27.15  constdefs
   27.16 -    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
   27.17 -    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
   27.18 +    mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
   27.19 +		   => 'a program"
   27.20 +    "mk_program == %(init, acts, allowed).
   27.21 +                      Abs_Program (init, insert Id acts, insert Id allowed)"
   27.22  
   27.23    Init :: "'a program => 'a set"
   27.24 -    "Init F == (%(init, acts). init) (Rep_Program F)"
   27.25 +    "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
   27.26  
   27.27    Acts :: "'a program => ('a * 'a)set set"
   27.28 -    "Acts F == (%(init, acts). acts) (Rep_Program F)"
   27.29 +    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
   27.30 +
   27.31 +  AllowedActs :: "'a program => ('a * 'a)set set"
   27.32 +    "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
   27.33 +
   27.34 +  Allowed :: "'a program => 'a program set"
   27.35 +    "Allowed F == {G. Acts G <= AllowedActs F}"
   27.36  
   27.37    stable     :: "'a set => 'a program set"
   27.38      "stable A == A co A"
    28.1 --- a/src/HOL/UNITY/Union.ML	Fri Sep 22 17:25:09 2000 +0200
    28.2 +++ b/src/HOL/UNITY/Union.ML	Sat Sep 23 16:02:01 2000 +0200
    28.3 @@ -19,7 +19,11 @@
    28.4  by (simp_tac (simpset() addsimps [SKIP_def]) 1);
    28.5  qed "Acts_SKIP";
    28.6  
    28.7 -Addsimps [Init_SKIP, Acts_SKIP];
    28.8 +Goal "AllowedActs SKIP = UNIV";
    28.9 +by (auto_tac (claset(), simpset() addsimps [SKIP_def]));  
   28.10 +qed "AllowedActs_SKIP";
   28.11 +
   28.12 +Addsimps [Init_SKIP, Acts_SKIP, AllowedActs_SKIP];
   28.13  
   28.14  Goal "reachable SKIP = UNIV";
   28.15  by (force_tac (claset() addEs [reachable.induct]
   28.16 @@ -56,7 +60,11 @@
   28.17  by (auto_tac (claset(), simpset() addsimps [Join_def]));
   28.18  qed "Acts_Join";
   28.19  
   28.20 -Addsimps [Init_Join, Acts_Join];
   28.21 +Goal "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G";
   28.22 +by (auto_tac (claset(), simpset() addsimps [Join_def]));
   28.23 +qed "AllowedActs_Join";
   28.24 +
   28.25 +Addsimps [Init_Join, Acts_Join, AllowedActs_Join];
   28.26  
   28.27  
   28.28  (** JN **)
   28.29 @@ -68,7 +76,7 @@
   28.30  
   28.31  Goal "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)";
   28.32  by (rtac program_equalityI 1);
   28.33 -by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
   28.34 +by (auto_tac (claset(), simpset() addsimps [JOIN_def, Join_def]));  
   28.35  qed "JN_insert";
   28.36  Addsimps[JN_empty, JN_insert];
   28.37  
   28.38 @@ -80,7 +88,11 @@
   28.39  by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
   28.40  qed "Acts_JN";
   28.41  
   28.42 -Addsimps [Init_JN, Acts_JN];
   28.43 +Goal "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))";
   28.44 +by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
   28.45 +qed "AllowedActs_JN";
   28.46 +
   28.47 +Addsimps [Init_JN, Acts_JN, AllowedActs_JN];
   28.48  
   28.49  val prems = Goalw [JOIN_def]
   28.50      "[| I=J;  !!i. i:J ==> F i = G i |] ==> \
   28.51 @@ -97,12 +109,14 @@
   28.52  by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
   28.53  qed "Join_commute";
   28.54  
   28.55 +
   28.56  Goal "A Join (B Join C) = B Join (A Join C)";
   28.57 -by (simp_tac (simpset() addsimps Un_ac@Int_ac@[Join_def]) 1);
   28.58 +by (simp_tac (simpset() addsimps Un_ac@Int_ac@[Join_def, insert_absorb]) 1);
   28.59  qed "Join_left_commute";
   28.60  
   28.61 +
   28.62  Goal "(F Join G) Join H = F Join (G Join H)";
   28.63 -by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
   28.64 +by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc, insert_absorb]) 1);
   28.65  qed "Join_assoc";
   28.66   
   28.67  Goalw [Join_def, SKIP_def] "SKIP Join F = F";
   28.68 @@ -316,3 +330,142 @@
   28.69  qed "stable_Join_ensures2";
   28.70  
   28.71  
   28.72 +(*** the ok and OK relations ***)
   28.73 +
   28.74 +Goal "SKIP ok F";
   28.75 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
   28.76 +qed "ok_SKIP1";  
   28.77 +
   28.78 +Goal "F ok SKIP";
   28.79 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
   28.80 +qed "ok_SKIP2";
   28.81 +
   28.82 +AddIffs [ok_SKIP1, ok_SKIP2];  
   28.83 +
   28.84 +Goal "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))";
   28.85 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
   28.86 +qed "ok_Join_commute";
   28.87 +
   28.88 +Goal "(F ok G) = (G ok F)";
   28.89 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
   28.90 +qed "ok_commute";
   28.91 +
   28.92 +bind_thm ("ok_sym", ok_commute RS iffD1);
   28.93 +
   28.94 +Goal "OK {(0,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
   28.95 +by (asm_full_simp_tac
   28.96 +    (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, 
   28.97 +                   OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1); 
   28.98 +by (Blast_tac 1); 
   28.99 +qed "ok_iff_OK";
  28.100 +
  28.101 +Goal "F ok (G Join H) = (F ok G & F ok H)";
  28.102 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
  28.103 +qed "ok_Join_iff1";
  28.104 +
  28.105 +Goal "(G Join H) ok F = (G ok F & H ok F)";
  28.106 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
  28.107 +qed "ok_Join_iff2";
  28.108 +AddIffs [ok_Join_iff1, ok_Join_iff2];
  28.109 +
  28.110 +(*useful?  Not with the previous two around*)
  28.111 +Goal "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)";
  28.112 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
  28.113 +qed "ok_Join_commute_I";
  28.114 +
  28.115 +Goal "F ok (JOIN I G) = (ALL i:I. F ok G i)";
  28.116 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
  28.117 +qed "ok_JN_iff1";
  28.118 +
  28.119 +Goal "(JOIN I G) ok F =  (ALL i:I. G i ok F)";
  28.120 +by (auto_tac (claset(), simpset() addsimps [ok_def]));
  28.121 +qed "ok_JN_iff2";
  28.122 +AddIffs [ok_JN_iff1, ok_JN_iff2];
  28.123 +
  28.124 +Goal "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"; 
  28.125 +by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def]));  
  28.126 +qed "OK_iff_ok";
  28.127 +
  28.128 +Goal "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"; 
  28.129 +by (auto_tac (claset(), simpset() addsimps [OK_iff_ok]));  
  28.130 +qed "OK_imp_ok";
  28.131 +
  28.132 +
  28.133 +(*** Allowed ***)
  28.134 +
  28.135 +Goal "Allowed SKIP = UNIV";
  28.136 +by (auto_tac (claset(), simpset() addsimps [Allowed_def]));  
  28.137 +qed "Allowed_SKIP";
  28.138 +
  28.139 +Goal "Allowed (F Join G) = Allowed F Int Allowed G";
  28.140 +by (auto_tac (claset(), simpset() addsimps [Allowed_def]));  
  28.141 +qed "Allowed_Join";
  28.142 +
  28.143 +Goal "Allowed (JOIN I F) = (INT i:I. Allowed (F i))";
  28.144 +by (auto_tac (claset(), simpset() addsimps [Allowed_def]));  
  28.145 +qed "Allowed_JN";
  28.146 +
  28.147 +Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN];
  28.148 +
  28.149 +Goal "F ok G = (F : Allowed G & G : Allowed F)";
  28.150 +by (simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1);
  28.151 +qed "ok_iff_Allowed";
  28.152 +
  28.153 +Goal "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"; 
  28.154 +by (auto_tac (claset(), simpset() addsimps [OK_iff_ok, ok_iff_Allowed]));  
  28.155 +qed "OK_iff_Allowed";
  28.156 +
  28.157 +(*** safety_prop, for reasoning about given instances of "ok" ***)
  28.158 +
  28.159 +Goal "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)";
  28.160 +by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
  28.161 +qed "safety_prop_Acts_iff";
  28.162 +
  28.163 +Goal "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)";
  28.164 +by (auto_tac (claset(), 
  28.165 +      simpset() addsimps [Allowed_def, safety_prop_Acts_iff RS sym]));  
  28.166 +qed "safety_prop_AllowedActs_iff_Allowed";
  28.167 +
  28.168 +Goal "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X";
  28.169 +by (asm_simp_tac (simpset() addsimps [Allowed_def, safety_prop_Acts_iff]) 1); 
  28.170 +qed "Allowed_eq";
  28.171 +
  28.172 +Goal "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |] \
  28.173 +\     ==> Allowed F = X";
  28.174 +by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1); 
  28.175 +qed "def_prg_Allowed";
  28.176 +
  28.177 +(*For safety_prop to hold, the property must be satisfiable!*)
  28.178 +Goal "safety_prop (A co B) = (A <= B)";
  28.179 +by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1);
  28.180 +by (Blast_tac 1); 
  28.181 +qed "safety_prop_constrains";
  28.182 +AddIffs [safety_prop_constrains];
  28.183 +
  28.184 +Goal "safety_prop (stable A)";
  28.185 +by (simp_tac (simpset() addsimps [stable_def]) 1);
  28.186 +qed "safety_prop_stable";
  28.187 +AddIffs [safety_prop_stable];
  28.188 +
  28.189 +Goal "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)";
  28.190 +by (full_simp_tac (simpset() addsimps [safety_prop_def]) 1); 
  28.191 +by (Blast_tac 1); 
  28.192 +qed "safety_prop_Int";
  28.193 +Addsimps [safety_prop_Int];
  28.194 +
  28.195 +Goal "(ALL i. safety_prop (X i)) ==> safety_prop (INT i. X i)";
  28.196 +by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
  28.197 +by (Blast_tac 1); 
  28.198 +bind_thm ("safety_prop_INTER1", allI RS result());
  28.199 +Addsimps [safety_prop_INTER1];
  28.200 +							       
  28.201 +Goal "(ALL i:I. safety_prop (X i)) ==> safety_prop (INT i:I. X i)";
  28.202 +by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
  28.203 +by (Blast_tac 1); 
  28.204 +bind_thm ("safety_prop_INTER", ballI RS result());
  28.205 +Addsimps [safety_prop_INTER];
  28.206 +
  28.207 +Goal "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] \
  28.208 +\     ==> F ok G = (G : X & acts <= AllowedActs G)";
  28.209 +by (auto_tac (claset(), simpset() addsimps [ok_def, safety_prop_Acts_iff]));  
  28.210 +qed "def_UNION_ok_iff";
    29.1 --- a/src/HOL/UNITY/Union.thy	Fri Sep 22 17:25:09 2000 +0200
    29.2 +++ b/src/HOL/UNITY/Union.thy	Sat Sep 23 16:02:01 2000 +0200
    29.3 @@ -11,14 +11,30 @@
    29.4  Union = SubstAx + FP +
    29.5  
    29.6  constdefs
    29.7 +
    29.8 +  (*FIXME: conjoin Init F Int Init G ~= {} *) 
    29.9 +  ok :: ['a program, 'a program] => bool      (infixl 65)
   29.10 +    "F ok G == Acts F <= AllowedActs G &
   29.11 +               Acts G <= AllowedActs F"
   29.12 +
   29.13 +  (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) 
   29.14 +  OK  :: ['a set, 'a => 'b program] => bool
   29.15 +    "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
   29.16 +
   29.17    JOIN  :: ['a set, 'a => 'b program] => 'b program
   29.18 -    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
   29.19 +    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
   29.20 +			     INT i:I. AllowedActs (F i))"
   29.21  
   29.22    Join :: ['a program, 'a program] => 'a program      (infixl 65)
   29.23 -    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
   29.24 +    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
   29.25 +			     AllowedActs F Int AllowedActs G)"
   29.26  
   29.27    SKIP :: 'a program
   29.28 -    "SKIP == mk_program (UNIV, {})"
   29.29 +    "SKIP == mk_program (UNIV, {}, UNIV)"
   29.30 +
   29.31 +  (*Characterizes safety properties.  Used with specifying AllowedActs*)
   29.32 +  safety_prop :: "'a program set => bool"
   29.33 +    "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
   29.34  
   29.35  syntax
   29.36    "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)
    30.1 --- a/src/HOL/UNITY/WFair.ML	Fri Sep 22 17:25:09 2000 +0200
    30.2 +++ b/src/HOL/UNITY/WFair.ML	Sat Sep 23 16:02:01 2000 +0200
    30.3 @@ -237,7 +237,7 @@
    30.4  qed "leadsTo_weaken";
    30.5  
    30.6  
    30.7 -(*Set difference: maybe combine with leadsTo_weaken_L??*)
    30.8 +(*Set difference: maybe combine with leadsTo_weaken_L?*)
    30.9  Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C";
   30.10  by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
   30.11  qed "leadsTo_Diff";
   30.12 @@ -373,7 +373,7 @@
   30.13  val lemma = result();
   30.14  
   30.15  
   30.16 -(** Meta or object quantifier ????? **)
   30.17 +(** Meta or object quantifier ? **)
   30.18  Goal "[| wf r;     \
   30.19  \        ALL m. F : (A Int f-``{m}) leadsTo                     \
   30.20  \                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \