A new approach, using simp_of_act and simp_of_set to activate definitions when
authorpaulson
Thu Sep 03 16:40:02 1998 +0200 (1998-09-03)
changeset 5426566f47250bd0
parent 5425 157c6663dedd
child 5427 26c9a7c0b36b
A new approach, using simp_of_act and simp_of_set to activate definitions when
necessary
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Handshake.ML
src/HOL/UNITY/Lift.ML
src/HOL/UNITY/Lift.thy
src/HOL/UNITY/Mutex.ML
src/HOL/UNITY/Reach.ML
src/HOL/UNITY/Reach.thy
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/Traces.ML
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/UNITY/Constrains.ML	Wed Sep 02 16:52:06 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.ML	Thu Sep 03 16:40:02 1998 +0200
     1.3 @@ -252,19 +252,15 @@
     1.4  val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
     1.5  
     1.6  
     1.7 -(** main_def defines the main program as a set;
     1.8 -    cmd_defs defines the separate commands
     1.9 -**)
    1.10 -
    1.11  (*proves "constrains" properties when the program is specified*)
    1.12 -fun constrains_tac (main_def::cmd_defs) = 
    1.13 +val constrains_tac = 
    1.14     SELECT_GOAL
    1.15        (EVERY [REPEAT (resolve_tac [StableI, stableI,
    1.16  				   constrains_imp_Constrains] 1),
    1.17  	      rtac constrainsI 1,
    1.18 -	      full_simp_tac (simpset() addsimps [main_def]) 1,
    1.19 +	      Full_simp_tac 1,
    1.20  	      REPEAT_FIRST (etac disjE),
    1.21  	      ALLGOALS Clarify_tac,
    1.22 -	      ALLGOALS (asm_full_simp_tac (simpset() addsimps cmd_defs))]);
    1.23 +	      ALLGOALS Asm_full_simp_tac]);
    1.24  
    1.25  
     2.1 --- a/src/HOL/UNITY/Handshake.ML	Wed Sep 02 16:52:06 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Handshake.ML	Thu Sep 03 16:40:02 1998 +0200
     2.3 @@ -11,38 +11,41 @@
     2.4  (*split_all_tac causes a big blow-up*)
     2.5  claset_ref() := claset() delSWrapper "split_all_tac";
     2.6  
     2.7 +Addsimps [prgF_def RS def_prg_simps];
     2.8 +Addsimps [prgG_def RS def_prg_simps];
     2.9 +Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
    2.10 +
    2.11  (*Simplification for records*)
    2.12  Addsimps (thms"state.update_defs");
    2.13 -Addsimps [invFG_def];
    2.14 +Addsimps [simp_of_set invFG_def];
    2.15  
    2.16  
    2.17 -Goalw [prgF_def, Join_def] "id : Acts (Join prgF prgG) ";
    2.18 +Goalw [Join_def] "id : Acts (Join prgF prgG) ";
    2.19  by (Simp_tac 1);
    2.20  qed "id_in_Acts";
    2.21  AddIffs [id_in_Acts];
    2.22  
    2.23 -
    2.24 -Goalw [prgF_def, prgG_def] "Invariant (Join prgF prgG) invFG";
    2.25 +Goal "Invariant (Join prgF prgG) invFG";
    2.26  by (rtac InvariantI 1);
    2.27  by (Force_tac 1);
    2.28  by (rtac (constrains_imp_Constrains RS StableI) 1);
    2.29  by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
    2.30 -by (constrains_tac [prgG_def,cmdG_def] 2);
    2.31 +by (constrains_tac 2);
    2.32  by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
    2.33 -by (constrains_tac [prgF_def,cmdF_def] 1);
    2.34 +by (constrains_tac 1);
    2.35  qed "invFG";
    2.36  
    2.37  Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} - {s. BB s}) \
    2.38  \                              ({s. NF s = k} Int {s. BB s})";
    2.39  by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    2.40 -by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
    2.41 -by (constrains_tac [prgF_def,cmdF_def] 1);
    2.42 +by (ensures_tac "cmdG" 2);
    2.43 +by (constrains_tac 1);
    2.44  qed "lemma2_1";
    2.45  
    2.46  Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
    2.47  by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    2.48 -by (constrains_tac [prgG_def,cmdG_def] 2);
    2.49 -by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
    2.50 +by (constrains_tac 2);
    2.51 +by (ensures_tac "cmdF" 1);
    2.52  qed "lemma2_2";
    2.53  
    2.54  
     3.1 --- a/src/HOL/UNITY/Lift.ML	Wed Sep 02 16:52:06 1998 +0200
     3.2 +++ b/src/HOL/UNITY/Lift.ML	Thu Sep 03 16:40:02 1998 +0200
     3.3 @@ -7,20 +7,38 @@
     3.4  *)
     3.5  
     3.6  
     3.7 -(*To move  0 < metric n s  out of the assumptions for case splitting*)
     3.8 -val rev_mp' = read_instantiate_sg (sign_of thy) 
     3.9 -                 [("P", "0 < metric ?n ?s")] rev_mp;
    3.10 +(*split_all_tac causes a big blow-up*)
    3.11 +claset_ref() := claset() delSWrapper "split_all_tac";
    3.12 +
    3.13 +
    3.14 +(** Rules to move "metric n s" out of the assumptions, for case splitting **)
    3.15 +val mov_metric1 = read_instantiate_sg (sign_of thy) 
    3.16 +                 [("P", "?x < metric ?n ?s")] rev_mp;
    3.17 +
    3.18 +val mov_metric2 = read_instantiate_sg (sign_of thy) 
    3.19 +                 [("P", "?x = metric ?n ?s")] rev_mp;
    3.20 +
    3.21 +val mov_metric3 = read_instantiate_sg (sign_of thy) 
    3.22 +                 [("P", "~ (?x < metric ?n ?s)")] rev_mp;
    3.23 +
    3.24 +(*The order in which they are applied seems to be critical...*)
    3.25 +val mov_metrics = [mov_metric2, mov_metric3, mov_metric1];
    3.26 +
    3.27  
    3.28  val Suc_lessD_contra = Suc_lessD COMP rev_contrapos;
    3.29  val Suc_lessD_contra' = less_not_sym RS Suc_lessD_contra;
    3.30  
    3.31 +Addsimps [Lprg_def RS def_prg_simps];
    3.32 +
    3.33 +Addsimps (map simp_of_act
    3.34 +	  [request_act_def, open_act_def, close_act_def,
    3.35 +	   req_up_def, req_down_def, move_up_def, move_down_def,
    3.36 +	   button_press_def]);
    3.37 +
    3.38  val always_defs = [above_def, below_def, queueing_def, 
    3.39  		   goingup_def, goingdown_def, ready_def];
    3.40  
    3.41 -val cmd_defs = [Lprg_def, 
    3.42 -		request_act_def, open_act_def, close_act_def,
    3.43 -		req_up_def, req_down_def, move_up_def, move_down_def,
    3.44 -		button_press_def];
    3.45 +Addsimps (map simp_of_set always_defs);
    3.46  
    3.47  Goalw [Lprg_def] "id : Acts Lprg";
    3.48  by (Simp_tac 1);
    3.49 @@ -40,9 +58,13 @@
    3.50       less_not_refl2, less_not_refl3];
    3.51  
    3.52  
    3.53 +(*Hoping to be faster than
    3.54 +    asm_simp_tac (simpset() addsimps metric_simps
    3.55 +  but sometimes it's slower*)
    3.56 +val metric_simp_tac = 
    3.57 +    asm_simp_tac (simpset() addsimps [metric_def, vimage_def]) THEN'
    3.58 +    asm_simp_tac (simpset() addsimps metric_simps);
    3.59  
    3.60 -(*split_all_tac causes a big blow-up*)
    3.61 -claset_ref() := claset() delSWrapper "split_all_tac";
    3.62  
    3.63  (*Simplification for records*)
    3.64  Addsimps (thms"state.update_defs");
    3.65 @@ -65,38 +87,37 @@
    3.66  by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
    3.67  qed "less_imp_le_pred";
    3.68  
    3.69 -Goalw [Lprg_def] "Invariant Lprg open_stop";
    3.70 +Goal "Invariant Lprg open_stop";
    3.71  by (rtac InvariantI 1);
    3.72  by (Force_tac 1);
    3.73 -by (constrains_tac (cmd_defs@always_defs) 1);
    3.74 +by (constrains_tac 1);
    3.75  qed "open_stop";
    3.76  
    3.77 -Goalw [Lprg_def] "Invariant Lprg stop_floor";
    3.78 +Goal "Invariant Lprg stop_floor";
    3.79  by (rtac InvariantI 1);
    3.80  by (Force_tac 1);
    3.81 -by (constrains_tac (cmd_defs@always_defs) 1);
    3.82 +by (constrains_tac 1);
    3.83  qed "stop_floor";
    3.84  
    3.85  (*This one needs open_stop, which was proved above*)
    3.86  Goal "Invariant Lprg open_move";
    3.87  by (rtac InvariantI 1);
    3.88 -br (open_stop RS Invariant_ConstrainsI RS StableI) 2;
    3.89 -bw Lprg_def;
    3.90 +by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2);
    3.91  by (Force_tac 1);
    3.92 -by (constrains_tac (cmd_defs@always_defs) 1);
    3.93 +by (constrains_tac 1);
    3.94  qed "open_move";
    3.95  
    3.96 -Goalw [Lprg_def] "Invariant Lprg moving_up";
    3.97 +Goal "Invariant Lprg moving_up";
    3.98  by (rtac InvariantI 1);
    3.99  by (Force_tac 1);
   3.100 -by (constrains_tac (cmd_defs@always_defs) 1);
   3.101 +by (constrains_tac 1);
   3.102  by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
   3.103  qed "moving_up";
   3.104  
   3.105 -Goalw [Lprg_def] "Invariant Lprg moving_down";
   3.106 +Goal "Invariant Lprg moving_down";
   3.107  by (rtac InvariantI 1);
   3.108  by (Force_tac 1);
   3.109 -by (constrains_tac (cmd_defs@always_defs) 1);
   3.110 +by (constrains_tac 1);
   3.111  by Safe_tac;
   3.112  by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
   3.113  by (auto_tac (claset(),
   3.114 @@ -105,10 +126,9 @@
   3.115  
   3.116  Goal "Invariant Lprg bounded";
   3.117  by (rtac InvariantI 1);
   3.118 -br (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2;
   3.119 -bw Lprg_def;
   3.120 +by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
   3.121  by (Force_tac 1);
   3.122 -by (constrains_tac (cmd_defs@always_defs) 1);
   3.123 +by (constrains_tac 1);
   3.124  by Safe_tac;
   3.125  by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le]));
   3.126  by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
   3.127 @@ -123,42 +143,33 @@
   3.128  val abbrev_defs = [moving_def, stopped_def, 
   3.129  		   opened_def, closed_def, atFloor_def, Req_def];
   3.130  
   3.131 -val defs = cmd_defs@always_defs@abbrev_defs;
   3.132 +Addsimps (map simp_of_set abbrev_defs);
   3.133  
   3.134  
   3.135  (** The HUG'93 paper mistakenly omits the Req n from these! **)
   3.136  
   3.137  (** Lift_1 **)
   3.138  
   3.139 -(*lem_lift_1_5*)
   3.140  Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
   3.141  by (cut_facts_tac [stop_floor] 1);
   3.142 -by (ensures_tac defs "open_act" 1);
   3.143 -by Auto_tac;
   3.144 -qed "E_thm01";
   3.145 +by (ensures_tac "open_act" 1);
   3.146 +qed "E_thm01";  (*lem_lift_1_5*)
   3.147  
   3.148 -(*lem_lift_1_1*)
   3.149  Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
   3.150  \                  (Req n Int opened - atFloor n)";
   3.151  by (cut_facts_tac [stop_floor] 1);
   3.152 -by (ensures_tac defs "open_act" 1);
   3.153 -by Auto_tac;
   3.154 -qed "E_thm02";
   3.155 +by (ensures_tac "open_act" 1);
   3.156 +qed "E_thm02";  (*lem_lift_1_1*)
   3.157  
   3.158 -(*lem_lift_1_2*)
   3.159  Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
   3.160  \                  (Req n Int closed - (atFloor n - queueing))";
   3.161 -by (ensures_tac defs "close_act" 1);
   3.162 -by Auto_tac;
   3.163 -qed "E_thm03";
   3.164 +by (ensures_tac "close_act" 1);
   3.165 +qed "E_thm03";  (*lem_lift_1_2*)
   3.166  
   3.167 -
   3.168 -(*lem_lift_1_7*)
   3.169  Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
   3.170  \                  (opened Int atFloor n)";
   3.171 -by (ensures_tac defs "open_act" 1);
   3.172 -by Auto_tac;
   3.173 -qed "E_thm04";
   3.174 +by (ensures_tac "open_act" 1);
   3.175 +qed "E_thm04";  (*lem_lift_1_7*)
   3.176  
   3.177  
   3.178  (** Lift 2.  Statements of thm05a and thm05b were wrong! **)
   3.179 @@ -182,16 +193,16 @@
   3.180  Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
   3.181  \                  ((closed Int goingup Int Req n)  Un \
   3.182  \                   (closed Int goingdown Int Req n))";
   3.183 -br subset_imp_LeadsTo 1;
   3.184 -by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs));
   3.185 +by (rtac subset_imp_LeadsTo 1);
   3.186 +by (auto_tac (claset() addSEs [nat_neqE], simpset()));
   3.187  qed "E_thm05c";
   3.188  
   3.189  (*lift_2*)
   3.190  Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
   3.191  \                  (moving Int Req n)";
   3.192 -br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
   3.193 -by (ensures_tac defs "req_down" 2);
   3.194 -by (ensures_tac defs "req_up" 1);
   3.195 +by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
   3.196 +by (ensures_tac "req_down" 2);
   3.197 +by (ensures_tac "req_up" 1);
   3.198  by Auto_tac;
   3.199  qed "lift_2";
   3.200  
   3.201 @@ -212,18 +223,16 @@
   3.202  Goal "0 < N ==> \
   3.203  \     LeadsTo Lprg \
   3.204  \       (moving Int Req n Int (metric n -`` {N}) Int \
   3.205 -\        {s. floor s ~: req s} Int {s. up s})   \
   3.206 +\         {s. floor s ~: req s} Int {s. up s})   \
   3.207  \       (moving Int Req n Int (metric n -`` lessThan N))";
   3.208  by (cut_facts_tac [moving_up] 1);
   3.209 -by (ensures_tac defs "move_up" 1);
   3.210 -by Auto_tac;
   3.211 +by (ensures_tac "move_up" 1);
   3.212 +by Safe_tac;
   3.213  (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   3.214 -be (leI RS le_anti_sym RS sym) 1;
   3.215 -by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
   3.216 -by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
   3.217 -by (REPEAT_FIRST (etac rev_mp'));
   3.218 -by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
   3.219 -by (distinct_tac 1);
   3.220 +by (etac (leI RS le_anti_sym RS sym) 1);
   3.221 +by (REPEAT_FIRST (eresolve_tac mov_metrics));
   3.222 +by (REPEAT_FIRST distinct_tac);
   3.223 +by (ALLGOALS metric_simp_tac);
   3.224  by (auto_tac
   3.225      (claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)]
   3.226  	      addIs [diff_Suc_less_diff], 
   3.227 @@ -242,16 +251,14 @@
   3.228  \        {s. floor s ~: req s} - {s. up s})   \
   3.229  \       (moving Int Req n Int (metric n -`` lessThan N))";
   3.230  by (cut_facts_tac [moving_down] 1);
   3.231 -by (ensures_tac defs "move_down" 1);
   3.232 -by Auto_tac;
   3.233 +by (ensures_tac "move_down" 1);
   3.234 +by Safe_tac;
   3.235  by (ALLGOALS distinct_tac);
   3.236  by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
   3.237  (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   3.238 -be (leI RS le_anti_sym RS sym) 1;
   3.239 -by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
   3.240 -by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
   3.241 -by (REPEAT_FIRST (etac rev_mp'));
   3.242 -by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
   3.243 +by (etac (leI RS le_anti_sym RS sym) 1);
   3.244 +by (REPEAT_FIRST (eresolve_tac mov_metrics));
   3.245 +by (ALLGOALS metric_simp_tac);
   3.246  by (auto_tac
   3.247      (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)]
   3.248                addIs [diff_le_Suc_diff, diff_less_Suc_diff],
   3.249 @@ -263,7 +270,7 @@
   3.250  Goal "0<N ==> LeadsTo Lprg (moving Int Req n Int (metric n -`` {N}) Int \
   3.251  \                           {s. floor s ~: req s})     \
   3.252  \                          (moving Int Req n Int (metric n -`` lessThan N))";
   3.253 -br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
   3.254 +by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
   3.255  by (etac E_thm12b 4);
   3.256  by (etac E_thm12a 3);
   3.257  by (rtac id_in_Acts 2);
   3.258 @@ -278,11 +285,11 @@
   3.259  \     ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingup) \
   3.260  \                      (moving Int Req n Int (metric n -`` lessThan N))";
   3.261  by (cut_facts_tac [bounded] 1);
   3.262 -by (ensures_tac defs "req_up" 1);
   3.263 +by (ensures_tac "req_up" 1);
   3.264  by Auto_tac;
   3.265 -by (ALLGOALS (eres_inst_tac [("P", "?x < metric n s")] notE));
   3.266 -by (REPEAT_FIRST (etac rev_mp'));
   3.267 +by (REPEAT_FIRST (eresolve_tac mov_metrics));
   3.268  by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
   3.269 +     (*faster than metric_simp_tac or than using just metric_def*)
   3.270  by (auto_tac (claset() addIs [diff_Suc_less_diff], 
   3.271  	      simpset() addsimps [arith1, arith2]));
   3.272  qed "E_thm16a";
   3.273 @@ -311,12 +318,12 @@
   3.274  \     LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingdown) \
   3.275  \                  (moving Int Req n Int (metric n -`` lessThan N))";
   3.276  by (cut_facts_tac [bounded] 1);
   3.277 -by (ensures_tac defs "req_down" 1);
   3.278 +by (ensures_tac "req_down" 1);
   3.279  by Auto_tac;
   3.280 -by (ALLGOALS (eres_inst_tac [("P", "?x < metric n s")] notE));
   3.281  by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
   3.282 -by (REPEAT_FIRST (etac rev_mp'));
   3.283 +by (REPEAT_FIRST (eresolve_tac mov_metrics));
   3.284  by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
   3.285 +     (*faster and better than metric_simp_tac *)
   3.286  by (auto_tac (claset() addIs [diff_Suc_less_diff, diff_less_Suc_diff], 
   3.287  	      simpset() addsimps [trans_le_add1, arith3, arith4]));
   3.288  qed "E_thm16b";
   3.289 @@ -346,19 +353,20 @@
   3.290  (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
   3.291    i.e. the trivial disjunction, leading to an asymmetrical proof.*)
   3.292  Goal "0<N ==> Req n Int (metric n -``{N}) <= goingup Un goingdown";
   3.293 -by (asm_simp_tac (simpset() addsimps (defs@metric_simps)) 1);
   3.294 -by (Blast_tac 1);
   3.295 +by (asm_simp_tac
   3.296 +    (simpset() addsimps (always_defs@abbrev_defs@[metric_def,vimage_def])) 1);
   3.297 +by (auto_tac (claset(), simpset() addsimps metric_simps));
   3.298  qed "E_thm16c";
   3.299  
   3.300  
   3.301  (*lift_5*)
   3.302  Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}))   \
   3.303  \                          (moving Int Req n Int (metric n -`` lessThan N))";
   3.304 -br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
   3.305 +by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
   3.306  by (etac E_thm16b 4);
   3.307  by (etac E_thm16a 3);
   3.308  by (rtac id_in_Acts 2);
   3.309 -bd E_thm16c 1;
   3.310 +by (dtac E_thm16c 1);
   3.311  by (Blast_tac 1);
   3.312  qed "lift_5";
   3.313  
   3.314 @@ -367,9 +375,10 @@
   3.315  
   3.316  (*lemma used to prove lem_lift_3_1*)
   3.317  Goal "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
   3.318 -be rev_mp 1;
   3.319 -by (asm_simp_tac (simpset() addsimps metric_simps) 1);
   3.320 -by Auto_tac;
   3.321 +by (etac rev_mp 1);
   3.322 +  (*MUCH faster than metric_simps*)
   3.323 +by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
   3.324 +by (auto_tac (claset(), simpset() addsimps metric_simps));
   3.325  qed "metric_eq_0D";
   3.326  
   3.327  AddDs [metric_eq_0D];
   3.328 @@ -379,7 +388,7 @@
   3.329  Goal "LeadsTo Lprg (moving Int Req n Int (metric n -`` {0}))   \
   3.330  \                  (stopped Int atFloor n)";
   3.331  by (cut_facts_tac [bounded] 1);
   3.332 -by (ensures_tac defs "request_act" 1);
   3.333 +by (ensures_tac "request_act" 1);
   3.334  by Auto_tac;
   3.335  qed "E_thm11";
   3.336  
   3.337 @@ -387,7 +396,7 @@
   3.338  Goal "LeadsTo Lprg \
   3.339  \       (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})   \
   3.340  \       (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})";
   3.341 -by (ensures_tac defs "request_act" 1);
   3.342 +by (ensures_tac "request_act" 1);
   3.343  by (auto_tac (claset(), simpset() addsimps metric_simps));
   3.344  qed "E_thm13";
   3.345  
   3.346 @@ -396,8 +405,8 @@
   3.347  \     LeadsTo Lprg \
   3.348  \       (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
   3.349  \       (opened Int Req n Int (metric n -`` {N}))";
   3.350 -by (ensures_tac defs "open_act" 1);
   3.351 -by (REPEAT_FIRST (etac rev_mp'));
   3.352 +by (ensures_tac "open_act" 1);
   3.353 +by (REPEAT_FIRST (eresolve_tac mov_metrics));
   3.354  by (auto_tac (claset(), simpset() addsimps metric_simps));
   3.355  qed "E_thm14";
   3.356  
   3.357 @@ -405,7 +414,7 @@
   3.358  Goal "LeadsTo Lprg \
   3.359  \       (opened Int Req n Int (metric n -`` {N}))  \
   3.360  \       (closed Int Req n Int (metric n -`` {N}))";
   3.361 -by (ensures_tac defs "close_act" 1);
   3.362 +by (ensures_tac "close_act" 1);
   3.363  by (auto_tac (claset(), simpset() addsimps metric_simps));
   3.364  qed "E_thm15";
   3.365  
   3.366 @@ -423,36 +432,35 @@
   3.367  
   3.368  
   3.369  Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
   3.370 -br (allI RS LessThan_induct) 1;
   3.371 +by (rtac (allI RS LessThan_induct) 1);
   3.372  by (exhaust_tac "m" 1);
   3.373 -auto();
   3.374 -br E_thm11 1;
   3.375 -br ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1;
   3.376 -br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
   3.377 -br lift_3_Req 4;
   3.378 -br lift_4 3;
   3.379 -auto();
   3.380 +by Auto_tac;
   3.381 +by (rtac E_thm11 1);
   3.382 +by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
   3.383 +by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
   3.384 +by (rtac lift_3_Req 4);
   3.385 +by (rtac lift_4 3);
   3.386 +by Auto_tac;
   3.387  qed "lift_3";
   3.388  
   3.389  
   3.390  Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)";
   3.391 -br LeadsTo_Trans 1;
   3.392 -br (E_thm04 RS LeadsTo_Un) 2;
   3.393 -br LeadsTo_Un_post' 2;
   3.394 -br (E_thm01 RS LeadsTo_Trans_Un') 2;
   3.395 -br (lift_3 RS LeadsTo_Trans_Un') 2;
   3.396 -br (lift_2 RS LeadsTo_Trans_Un') 2;
   3.397 -br (E_thm03 RS LeadsTo_Trans_Un') 2;
   3.398 -br E_thm02 2;
   3.399 -br (open_move RS Invariant_LeadsToI) 1;
   3.400 -br (open_stop RS Invariant_LeadsToI) 1;
   3.401 -br subset_imp_LeadsTo 1;
   3.402 +by (rtac LeadsTo_Trans 1);
   3.403 +by (rtac (E_thm04 RS LeadsTo_Un) 2);
   3.404 +by (rtac LeadsTo_Un_post' 2);
   3.405 +by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
   3.406 +by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
   3.407 +by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
   3.408 +by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2);
   3.409 +by (rtac E_thm02 2);
   3.410 +by (rtac (open_move RS Invariant_LeadsToI) 1);
   3.411 +by (rtac (open_stop RS Invariant_LeadsToI) 1);
   3.412 +by (rtac subset_imp_LeadsTo 1);
   3.413  by (rtac id_in_Acts 2);
   3.414 -bws defs;
   3.415  by (Clarify_tac 1);
   3.416  	(*stops simplification from looping*)
   3.417  by (Full_simp_tac 1);
   3.418 -by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1));
   3.419 +by (Blast_tac 1);
   3.420  qed "lift_1";
   3.421  
   3.422  Close_locale;
     4.1 --- a/src/HOL/UNITY/Lift.thy	Wed Sep 02 16:52:06 1998 +0200
     4.2 +++ b/src/HOL/UNITY/Lift.thy	Thu Sep 03 16:40:02 1998 +0200
     4.3 @@ -4,8 +4,6 @@
     4.4      Copyright   1998  University of Cambridge
     4.5  
     4.6  The Lift-Control Example
     4.7 -
     4.8 -
     4.9  *)
    4.10  
    4.11  Lift = SubstAx +
     5.1 --- a/src/HOL/UNITY/Mutex.ML	Wed Sep 02 16:52:06 1998 +0200
     5.2 +++ b/src/HOL/UNITY/Mutex.ML	Thu Sep 03 16:40:02 1998 +0200
     5.3 @@ -9,35 +9,27 @@
     5.4  (*split_all_tac causes a big blow-up*)
     5.5  claset_ref() := claset() delSWrapper "split_all_tac";
     5.6  
     5.7 -val cmd_defs = [Mprg_def, 
     5.8 -		cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, 
     5.9 -		cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def];
    5.10 +Addsimps [Mprg_def RS def_prg_simps];
    5.11  
    5.12 -Goalw [Mprg_def] "id : Acts Mprg";
    5.13 -by (Simp_tac 1);
    5.14 -qed "id_in_Acts";
    5.15 -AddIffs [id_in_Acts];
    5.16 +Addsimps (map simp_of_act
    5.17 +	  [cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, 
    5.18 +	   cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def]);
    5.19  
    5.20 +Addsimps (map simp_of_set
    5.21 +	  [invariantU_def, invariantV_def, bad_invariantU_def]);
    5.22  
    5.23  (*Simplification for records*)
    5.24 -val select_defs = thms"state.select_defs"
    5.25 -and update_defs = thms"state.update_defs"
    5.26 -and dest_defs   = thms"state.dest_defs";
    5.27 -
    5.28 -Addsimps update_defs;
    5.29 +Addsimps (thms"state.update_defs");
    5.30  
    5.31 -Addsimps [invariantU_def, invariantV_def];
    5.32 -
    5.33 -
    5.34 -Goalw [Mprg_def] "Invariant Mprg invariantU";
    5.35 +Goal "Invariant Mprg invariantU";
    5.36  by (rtac InvariantI 1);
    5.37 -by (constrains_tac cmd_defs 2);
    5.38 +by (constrains_tac 2);
    5.39  by Auto_tac;
    5.40  qed "invariantU";
    5.41  
    5.42 -Goalw [Mprg_def] "Invariant Mprg invariantV";
    5.43 +Goal "Invariant Mprg invariantV";
    5.44  by (rtac InvariantI 1);
    5.45 -by (constrains_tac cmd_defs 2);
    5.46 +by (constrains_tac 2);
    5.47  by Auto_tac;
    5.48  qed "invariantV";
    5.49  
    5.50 @@ -52,12 +44,10 @@
    5.51  
    5.52  
    5.53  (*The bad invariant FAILS in cmd1V*)
    5.54 -Goalw [Mprg_def, bad_invariantU_def] "Invariant Mprg bad_invariantU";
    5.55 +Goal "Invariant Mprg bad_invariantU";
    5.56  by (rtac InvariantI 1);
    5.57 -by (Force_tac 1);
    5.58 -by (constrains_tac cmd_defs 1);
    5.59 -by Auto_tac;
    5.60 -by (safe_tac (claset() addSEs [le_SucE]));
    5.61 +by (constrains_tac 2);
    5.62 +by (auto_tac (claset() addSEs [le_SucE], simpset()));
    5.63  by (Asm_full_simp_tac 1);
    5.64  (*Resulting state: n=1, p=false, m=4, u=false.  
    5.65    Execution of cmd1V (the command of process v guarded by n=1) sets p:=true,
    5.66 @@ -69,26 +59,22 @@
    5.67  (*** Progress for U ***)
    5.68  
    5.69  Goalw [Unless_def] "Unless Mprg {s. MM s=2} {s. MM s=3}";
    5.70 -by (constrains_tac cmd_defs 1);
    5.71 +by (constrains_tac 1);
    5.72  qed "U_F0";
    5.73  
    5.74  Goal "LeadsTo Mprg {s. MM s=1} {s. PP s = VV s & MM s = 2}";
    5.75 -by (ensures_tac cmd_defs "cmd1U" 1);
    5.76 -by Auto_tac;
    5.77 +by (ensures_tac "cmd1U" 1);
    5.78  qed "U_F1";
    5.79  
    5.80  Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
    5.81  by (cut_facts_tac [invariantU] 1);
    5.82 -by (rewtac Mprg_def);
    5.83 -by (ensures_tac cmd_defs "cmd2U" 1);
    5.84 -by Auto_tac;
    5.85 +by (ensures_tac "cmd2U" 1);
    5.86  qed "U_F2";
    5.87  
    5.88  Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}";
    5.89  by (res_inst_tac [("B", "{s. MM s = 4}")] LeadsTo_Trans 1);
    5.90 -by (ensures_tac cmd_defs "cmd4U" 2);
    5.91 -by (ensures_tac cmd_defs "cmd3U" 1);
    5.92 -by Auto_tac;
    5.93 +by (ensures_tac "cmd4U" 2);
    5.94 +by (ensures_tac "cmd3U" 1);
    5.95  qed "U_F3";
    5.96  
    5.97  Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}";
    5.98 @@ -121,25 +107,22 @@
    5.99  
   5.100  
   5.101  Goalw [Unless_def] "Unless Mprg {s. NN s=2} {s. NN s=3}";
   5.102 -by (constrains_tac cmd_defs 1);
   5.103 +by (constrains_tac 1);
   5.104  qed "V_F0";
   5.105  
   5.106  Goal "LeadsTo Mprg {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}";
   5.107 -by (ensures_tac cmd_defs "cmd1V" 1);
   5.108 -by Auto_tac;
   5.109 +by (ensures_tac "cmd1V" 1);
   5.110  qed "V_F1";
   5.111  
   5.112  Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}";
   5.113  by (cut_facts_tac [invariantV] 1);
   5.114 -by (ensures_tac cmd_defs "cmd2V" 1);
   5.115 -by Auto_tac;
   5.116 +by (ensures_tac "cmd2V" 1);
   5.117  qed "V_F2";
   5.118  
   5.119  Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}";
   5.120  by (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1);
   5.121 -by (ensures_tac cmd_defs "cmd4V" 2);
   5.122 -by (ensures_tac cmd_defs "cmd3V" 1);
   5.123 -by Auto_tac;
   5.124 +by (ensures_tac "cmd4V" 2);
   5.125 +by (ensures_tac "cmd3V" 1);
   5.126  qed "V_F3";
   5.127  
   5.128  Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}";
     6.1 --- a/src/HOL/UNITY/Reach.ML	Wed Sep 02 16:52:06 1998 +0200
     6.2 +++ b/src/HOL/UNITY/Reach.ML	Thu Sep 03 16:40:02 1998 +0200
     6.3 @@ -19,22 +19,19 @@
     6.4  AddSEs [ifE];
     6.5  
     6.6  
     6.7 -val cmd_defs = [Rprg_def, asgt_def, fun_upd_def];
     6.8 +Addsimps [Rprg_def RS def_prg_simps];
     6.9  
    6.10 -Goalw [Rprg_def] "id : (Acts Rprg)";
    6.11 -by (Simp_tac 1);
    6.12 -qed "id_in_Acts";
    6.13 -AddIffs [id_in_Acts];
    6.14 +Addsimps [simp_of_act asgt_def];
    6.15  
    6.16  (*All vertex sets are finite*)
    6.17  AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
    6.18  
    6.19 -Addsimps [reach_invariant_def];
    6.20 +Addsimps [simp_of_set reach_invariant_def];
    6.21  
    6.22 -Goalw [Rprg_def] "Invariant Rprg reach_invariant";
    6.23 +Goal "Invariant Rprg reach_invariant";
    6.24  by (rtac InvariantI 1);
    6.25  by Auto_tac;  (*for the initial state; proof of stability remains*)
    6.26 -by (constrains_tac [Rprg_def, asgt_def] 1);
    6.27 +by (constrains_tac 1);
    6.28  by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
    6.29  qed "reach_invariant";
    6.30  
    6.31 @@ -42,28 +39,27 @@
    6.32  (*** Fixedpoint ***)
    6.33  
    6.34  (*If it reaches a fixedpoint, it has found a solution*)
    6.35 -Goalw [fixedpoint_def, reach_invariant_def]
    6.36 -    "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
    6.37 +Goalw [fixedpoint_def]
    6.38 +     "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
    6.39  by (rtac equalityI 1);
    6.40 +by (auto_tac (claset() addSIs [ext], simpset()));
    6.41  by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
    6.42 -by (auto_tac (claset() addSIs [ext], simpset()));
    6.43  by (etac rtrancl_induct 1);
    6.44  by Auto_tac;
    6.45  qed "fixedpoint_invariant_correct";
    6.46  
    6.47 -Goalw (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
    6.48 -    "FP (Acts Rprg) <= fixedpoint";
    6.49 +Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
    6.50 +     "FP (Acts Rprg) <= fixedpoint";
    6.51  by Auto_tac;
    6.52 -by (dtac bspec 1); 
    6.53 -by (Blast_tac 1);
    6.54 +by (dtac bspec 1 THEN Blast_tac 1);
    6.55  by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
    6.56  by (dtac fun_cong 1);
    6.57  by Auto_tac;
    6.58  val lemma1 = result();
    6.59  
    6.60 -Goalw (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
    6.61 -    "fixedpoint <= FP (Acts Rprg)";
    6.62 -by (auto_tac (claset() addIs [ext], simpset()));
    6.63 +Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
    6.64 +     "fixedpoint <= FP (Acts Rprg)";
    6.65 +by (auto_tac (claset() addSIs [ext], simpset()));
    6.66  val lemma2 = result();
    6.67  
    6.68  Goal "FP (Acts Rprg) = fixedpoint";
    6.69 @@ -79,9 +75,8 @@
    6.70  
    6.71  Goal "Compl fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
    6.72  by (simp_tac (simpset() addsimps
    6.73 -	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, 
    6.74 -		Rprg_def, asgt_def])) 1);
    6.75 -by Safe_tac;
    6.76 +	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym])) 1);
    6.77 +by Auto_tac;
    6.78  by (rtac fun_upd_idem 1);
    6.79  by (Blast_tac 1);
    6.80  by (Full_simp_tac 1);
    6.81 @@ -121,7 +116,7 @@
    6.82  by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
    6.83  by (rtac LeadsTo_UN 1);
    6.84  by Auto_tac;
    6.85 -by (ensures_tac [Rprg_def, asgt_def] "asgt a b" 1);
    6.86 +by (ensures_tac "asgt a b" 1);
    6.87  by (Blast_tac 2);
    6.88  by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
    6.89  bd (metric_le RS le_anti_sym) 1;
    6.90 @@ -130,8 +125,9 @@
    6.91  qed "LeadsTo_Diff_fixedpoint";
    6.92  
    6.93  Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
    6.94 -by (rtac (LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R RS LeadsTo_Diff) 1);
    6.95 -by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
    6.96 +by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
    6.97 +	   subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
    6.98 +by Auto_tac;
    6.99  qed "LeadsTo_Un_fixedpoint";
   6.100  
   6.101  
     7.1 --- a/src/HOL/UNITY/Reach.thy	Wed Sep 02 16:52:06 1998 +0200
     7.2 +++ b/src/HOL/UNITY/Reach.thy	Thu Sep 03 16:40:02 1998 +0200
     7.3 @@ -34,7 +34,7 @@
     7.4      "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
     7.5  
     7.6    metric :: state => nat
     7.7 -    "metric == (%s. card {v. ~ s v})"
     7.8 +    "metric s == card {v. ~ s v}"
     7.9  
    7.10  rules
    7.11  
     8.1 --- a/src/HOL/UNITY/SubstAx.ML	Wed Sep 02 16:52:06 1998 +0200
     8.2 +++ b/src/HOL/UNITY/SubstAx.ML	Thu Sep 03 16:40:02 1998 +0200
     8.3 @@ -401,12 +401,8 @@
     8.4  qed "Finite_completion";
     8.5  
     8.6  
     8.7 -(** main_def defines the main program as a set;
     8.8 -    cmd_defs defines the separate commands
     8.9 -**)
    8.10 -
    8.11  (*proves "ensures/leadsTo" properties when the program is specified*)
    8.12 -fun ensures_tac (main_def::cmd_defs) sact = 
    8.13 +fun ensures_tac sact = 
    8.14      SELECT_GOAL
    8.15        (EVERY [REPEAT (Invariant_Int_tac 1),
    8.16  	      etac Invariant_LeadsTo_Basis 1 
    8.17 @@ -414,11 +410,8 @@
    8.18  		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
    8.19  	      res_inst_tac [("act", sact)] transient_mem 2,
    8.20                   (*simplify the command's domain*)
    8.21 -	      simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
    8.22 -	         (*INSIST that the command belongs to the program*)
    8.23 -	      force_tac (claset(), simpset() addsimps [main_def]) 2,
    8.24 -	      constrains_tac (main_def::cmd_defs) 1,
    8.25 -	      rewrite_goals_tac cmd_defs,
    8.26 +	      simp_tac (simpset() addsimps [Domain_def]) 3,
    8.27 +	      constrains_tac 1,
    8.28  	      ALLGOALS Clarify_tac,
    8.29  	      ALLGOALS Asm_full_simp_tac]);
    8.30  
     9.1 --- a/src/HOL/UNITY/Traces.ML	Wed Sep 02 16:52:06 1998 +0200
     9.2 +++ b/src/HOL/UNITY/Traces.ML	Thu Sep 03 16:40:02 1998 +0200
     9.3 @@ -12,7 +12,7 @@
     9.4  Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
     9.5  by Safe_tac;
     9.6  by (etac traces.induct 2);
     9.7 -be reachable.induct 1;
     9.8 +by (etac reachable.induct 1);
     9.9  by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
    9.10  qed "reachable_equiv_traces";
    9.11  
    9.12 @@ -21,11 +21,38 @@
    9.13  qed "stable_reachable";
    9.14  
    9.15  Goal "(act : Acts(|Init=init, Acts=acts|)) = (act:acts)";
    9.16 -auto();
    9.17 +by Auto_tac;
    9.18  qed "Acts_eq";
    9.19  
    9.20  Goal "(s : Init(|Init=init, Acts=acts|)) = (s:init)";
    9.21 -auto();
    9.22 +by Auto_tac;
    9.23  qed "Init_eq";
    9.24  
    9.25  AddIffs [Acts_eq, Init_eq];
    9.26 +
    9.27 +
    9.28 +(*** These three rules allow "lazy" definition expansion ***)
    9.29 +
    9.30 +val [rew] = goal thy
    9.31 +    "[| prg == (|Init=init, Acts=acts|) |] \
    9.32 +\    ==> Init prg = init & Acts prg = acts";
    9.33 +by (rewtac rew);
    9.34 +by Auto_tac;
    9.35 +qed "def_prg_simps";
    9.36 +
    9.37 +val [rew] = goal thy
    9.38 +    "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
    9.39 +by (rewtac rew);
    9.40 +by Auto_tac;
    9.41 +qed "def_act_simp";
    9.42 +
    9.43 +fun simp_of_act def = def RS def_act_simp;
    9.44 +
    9.45 +val [rew] = goal thy
    9.46 +    "[| A == B |] ==> (x : A) = (x : B)";
    9.47 +by (rewtac rew);
    9.48 +by Auto_tac;
    9.49 +qed "def_set_simp";
    9.50 +
    9.51 +fun simp_of_set def = def RS def_set_simp;
    9.52 +
    10.1 --- a/src/HOL/UNITY/Union.ML	Wed Sep 02 16:52:06 1998 +0200
    10.2 +++ b/src/HOL/UNITY/Union.ML	Thu Sep 03 16:40:02 1998 +0200
    10.3 @@ -6,9 +6,6 @@
    10.4  Unions of programs
    10.5  
    10.6  From Misra's Chapter 5: Asynchronous Compositions of Programs
    10.7 -
    10.8 -NOT CLEAR WHETHER ALL THESE FORMS ARE NEEDED: 
    10.9 -    Maybe Join instead of Un, and JOIN for UNION
   10.10  *)
   10.11  
   10.12