Misc changes
authorpaulson
Wed Aug 19 10:34:31 1998 +0200 (1998-08-19)
changeset 5340d75c03cf77b5
parent 5339 22c195854229
child 5341 eb105c6931a4
Misc changes
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/SubstAx.ML
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/WFair.ML
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/UNITY/Constrains.ML	Wed Aug 19 10:29:01 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.ML	Wed Aug 19 10:34:31 1998 +0200
     1.3 @@ -9,6 +9,10 @@
     1.4  
     1.5  (*** Constrains ***)
     1.6  
     1.7 +(*Map its type, ('a * 'a)set set, 'a set, 'a set] => bool, to just 'a*)
     1.8 +Blast.overloaded ("Constrains.Constrains", 
     1.9 +		  HOLogic.dest_setT o domain_type o range_type);
    1.10 +
    1.11  (*constrains (Acts prg) B B'
    1.12    ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
    1.13  bind_thm ("constrains_reachable_Int",
    1.14 @@ -80,7 +84,8 @@
    1.15      "[| ALL i:I. Constrains prg (A i) (A' i) |]   \
    1.16  \    ==> Constrains prg (INT i:I. A i) (INT i:I. A' i)";
    1.17  by (dtac ball_constrains_INT 1);
    1.18 -by (blast_tac (claset() addIs [constrains_reachable_Int, constrains_weaken]) 1);
    1.19 +by (dtac constrains_reachable_Int 1);
    1.20 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
    1.21  qed "ball_Constrains_INT";
    1.22  
    1.23  Goalw [Constrains_def]
     2.1 --- a/src/HOL/UNITY/Handshake.ML	Wed Aug 19 10:29:01 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Handshake.ML	Wed Aug 19 10:34:31 1998 +0200
     2.3 @@ -32,13 +32,14 @@
     2.4  by (constrains_tac [prgF_def,cmdF_def] 1);
     2.5  qed "invFG";
     2.6  
     2.7 -Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}";
     2.8 +Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} - {s. BB s}) \
     2.9 +\                              ({s. NF s = k} Int {s. BB s})";
    2.10  by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    2.11  by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
    2.12  by (constrains_tac [prgF_def,cmdF_def] 1);
    2.13  qed "lemma2_1";
    2.14  
    2.15 -Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}";
    2.16 +Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
    2.17  by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    2.18  by (constrains_tac [prgG_def,cmdG_def] 2);
    2.19  by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
    2.20 @@ -55,6 +56,6 @@
    2.21  by (rtac lemma2_2 2);
    2.22  by (rtac LeadsTo_Trans 1);
    2.23  by (rtac lemma2_2 2);
    2.24 -by (rtac (lemma2_1 RS LeadsTo_weaken_L) 1);
    2.25 +by (rtac (lemma2_1) 1);
    2.26  by Auto_tac;
    2.27  qed "progress";
     3.1 --- a/src/HOL/UNITY/Lift.ML	Wed Aug 19 10:29:01 1998 +0200
     3.2 +++ b/src/HOL/UNITY/Lift.ML	Wed Aug 19 10:34:31 1998 +0200
     3.3 @@ -6,6 +6,13 @@
     3.4  The Lift-Control Example
     3.5  *)
     3.6  
     3.7 +(*ARITH.ML??*)
     3.8 +Goal "m-1 < n ==> m <= n";
     3.9 +by (exhaust_tac "m" 1);
    3.10 +by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
    3.11 +qed "pred_less_imp_le";
    3.12 +
    3.13 +
    3.14  val always_defs = [above_def, below_def, queueing_def, 
    3.15  		   goingup_def, goingdown_def, ready_def];
    3.16  
    3.17 @@ -13,8 +20,6 @@
    3.18  		request_act_def, open_act_def, close_act_def,
    3.19  		req_up_act_def, req_down_act_def, move_up_def, move_down_def];
    3.20  
    3.21 -AddIffs [min_le_max];
    3.22 -
    3.23  Goalw [Lprg_def] "id : Acts Lprg";
    3.24  by (Simp_tac 1);
    3.25  qed "id_in_Acts";
    3.26 @@ -32,9 +37,8 @@
    3.27  Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
    3.28  	  moving_up_def, moving_down_def];
    3.29  
    3.30 +AddIffs [min_le_max];
    3.31  
    3.32 -val nat_exhaust_less_pred = 
    3.33 -    read_instantiate_sg (sign_of thy) [("P", "?m < ?y-1")] nat.exhaust;
    3.34  
    3.35  val nat_exhaust_le_pred = 
    3.36      read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
    3.37 @@ -47,6 +51,11 @@
    3.38  by Auto_tac;
    3.39  qed "le_pred_eq";
    3.40  
    3.41 +Goal "0 < n ==> (m-1 < n) = (m<=n)";
    3.42 +by (exhaust_tac "m" 1);
    3.43 +by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
    3.44 +qed "less_pred_eq";
    3.45 +
    3.46  Goal "m < n ==> m <= n-1";
    3.47  by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
    3.48  qed "less_imp_le_pred";
    3.49 @@ -107,34 +116,303 @@
    3.50  
    3.51  
    3.52  val abbrev_defs = [moving_def, stopped_def, 
    3.53 -		   opened_def, closed_def, atFloor_def];
    3.54 +		   opened_def, closed_def, atFloor_def, Req_def];
    3.55  
    3.56  val defs = cmd_defs@always_defs@abbrev_defs;
    3.57  
    3.58 -(***
    3.59 +
    3.60 +(** The HUG'93 paper mistakenly omits the Req n from these! **)
    3.61  
    3.62  Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
    3.63 +by (cut_facts_tac [stop_floor] 1);
    3.64  by (ensures_tac defs "open_act" 1);
    3.65 -qed "U_F1";
    3.66 +qed "E_thm01";
    3.67 +
    3.68 +Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
    3.69 +\                  (Req n Int opened - atFloor n)";
    3.70 +by (cut_facts_tac [stop_floor] 1);
    3.71 +by (ensures_tac defs "open_act" 1);
    3.72 +qed "E_thm02";
    3.73 +
    3.74 +Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
    3.75 +\                  (Req n Int closed - (atFloor n - queueing))";
    3.76 +by (ensures_tac defs "close_act" 1);
    3.77 +qed "E_thm03";
    3.78 +
    3.79 +Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
    3.80 +\                  (opened Int atFloor n)";
    3.81 +by (ensures_tac defs "open_act" 1);
    3.82 +qed "E_thm04";
    3.83 +
    3.84 +
    3.85 +(** Theorem 5.  Statements of thm05a and thm05b were wrong! **)
    3.86 +
    3.87 +Open_locale "floor"; 
    3.88 +
    3.89 +AddIffs [thm "min_le_n", thm "n_le_max"];
    3.90 +
    3.91 +(*NOT an ensures property, but a mere inclusion*)
    3.92 +Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
    3.93 +\                  ((closed Int goingup Int Req n)  Un \
    3.94 +\                   (closed Int goingdown Int Req n))";
    3.95 +br subset_imp_LeadsTo 1;
    3.96 +by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs));
    3.97 +qed "E_thm05c";
    3.98 +
    3.99 +Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
   3.100 +\                  (moving Int Req n)";
   3.101 +br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
   3.102 +by (ensures_tac defs "req_down_act" 2);
   3.103 +by (ensures_tac defs "req_up_act" 1);
   3.104 +qed "lift_2";
   3.105 +
   3.106 +
   3.107 +
   3.108 +val LeadsTo_Un_post' = id_in_Acts RS LeadsTo_Un_post
   3.109 +and LeadsTo_Trans_Un' = rotate_prems 1 (id_in_Acts RS LeadsTo_Trans_Un);
   3.110 +(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
   3.111 +
   3.112 +val [lift_3] = 
   3.113 +goal thy "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n) ==> LeadsTo Lprg (Req n) (opened Int atFloor n)";
   3.114 +br LeadsTo_Trans 1;
   3.115 +br (E_thm04 RS LeadsTo_Un) 2;
   3.116 +br LeadsTo_Un_post' 2;
   3.117 +br (E_thm01 RS LeadsTo_Trans_Un') 2;
   3.118 +br (lift_3 RS LeadsTo_Trans_Un') 2;
   3.119 +br (lift_2 RS LeadsTo_Trans_Un') 2;
   3.120 +br (E_thm03 RS LeadsTo_Trans_Un') 2;
   3.121 +br E_thm02 2;
   3.122 +br (open_move RS Invariant_LeadsToI) 1;
   3.123 +br (open_stop RS Invariant_LeadsToI) 1;
   3.124 +br subset_imp_LeadsTo 1;
   3.125 +by (rtac id_in_Acts 2);
   3.126 +bws defs;
   3.127 +by (Clarify_tac 1);
   3.128 +	(*stops simplification from looping*)
   3.129 +by (asm_full_simp_tac (simpset() setsubgoaler simp_tac) 1);
   3.130 +by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1));
   3.131 +qed "lift_1";
   3.132 +
   3.133  
   3.134 -Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
   3.135 -by (cut_facts_tac [invariantUV] 1);
   3.136 -by (rewtac Lprg_def);
   3.137 -by (ensures_tac defs "cmd2U" 1);
   3.138 -qed "U_F2";
   3.139 +val rev_mp' = read_instantiate_sg (sign_of thy) 
   3.140 +                 [("P", "0 < metric ?n ?s")] rev_mp;
   3.141 +
   3.142 +
   3.143 +Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
   3.144 +\                  (moving Int Req n Int {s. metric n s < N})";
   3.145 +by (ensures_tac defs "req_up_act" 1);
   3.146 +by (REPEAT_FIRST (etac rev_mp'));
   3.147 +by (auto_tac (claset() addIs [diff_Suc_less_diff], 
   3.148 +	      simpset() addsimps [arith1, arith2, metric_def]));
   3.149 +qed "E_thm16a";
   3.150 +
   3.151 +
   3.152 +(*arith1 comes from
   3.153 + 1. !!s i.
   3.154 +       [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
   3.155 +          i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
   3.156 +          ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
   3.157 +          Suc (floor s) < n; 0 < floor s - min |]
   3.158 +       ==> n - Suc (floor s) < floor s - min + (n - min)
   3.159 +*)
   3.160 +
   3.161 +(*arith2 comes from
   3.162 + 2. !!s i.
   3.163 +       [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
   3.164 +          i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
   3.165 +          ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
   3.166 +          Suc (floor s) < n; min < n |]
   3.167 +       ==> n - Suc (floor s) < floor s - min + (n - min)
   3.168 +*)
   3.169 +
   3.170 +
   3.171 +xxxxxxxxxxxxxxxx;
   3.172 +
   3.173 +Goal "j<=i ==> i - j < Suc i - j";
   3.174 +by (REPEAT (etac rev_mp 1));
   3.175 +by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   3.176 +by Auto_tac;
   3.177 +qed "diff_less_Suc_diff";
   3.178 +
   3.179 +
   3.180 +Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
   3.181 +\                  (moving Int Req n Int {s. metric n s < N})";
   3.182 +by (ensures_tac defs "req_down_act" 1);
   3.183 +be rev_mp 2;
   3.184 +be rev_mp 1;
   3.185 +by (dtac less_eq_Suc_add 2);
   3.186 +by (Clarify_tac 2);
   3.187 +by (Asm_full_simp_tac 2);
   3.188 +by (dtac less_eq_Suc_add 1);
   3.189 +by (Clarify_tac 1);
   3.190 +by (Asm_full_simp_tac 1);
   3.191 +
   3.192 +by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
   3.193 +by (REPEAT (Safe_step_tac 1));
   3.194 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
   3.195 +by (REPEAT (Safe_step_tac 1));
   3.196 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
   3.197 +by (REPEAT (Safe_step_tac 1));
   3.198 +
   3.199 +
   3.200 +
   3.201 +
   3.202 +
   3.203 +
   3.204 +
   3.205 +Goal "[| i + k < n;  Suc (i + k) < n |] ==> i + k - m < Suc (i + k) - m";
   3.206 +by (REPEAT (etac rev_mp 1));
   3.207 +by (arith_oracle_tac 1);
   3.208 +
   3.209  
   3.210 -Goal "LeadsTo Lprg {s. MM s = 3} {s. PP s}";
   3.211 -by (rtac leadsTo_imp_LeadsTo 1); 
   3.212 -by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
   3.213 -by (ensures_tac defs "cmd4U" 2);
   3.214 -by (ensures_tac defs "cmd3U" 1);
   3.215 -qed "U_F3";
   3.216 +by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
   3.217 +by (REPEAT (Safe_step_tac 2));
   3.218 +by(Blast_tac 2);
   3.219 +by(Blast_tac 2);
   3.220 +by(Blast_tac 2);
   3.221 +by (REPEAT (Safe_step_tac 2));
   3.222 +by(Blast_tac 2);
   3.223 +by(blast_tac (claset() addEs [less_asym]) 2);
   3.224 +by (REPEAT (Safe_step_tac 2));
   3.225 +by(blast_tac (claset() addEs [less_asym]) 2);
   3.226 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
   3.227 +by (REPEAT (Safe_step_tac 2));
   3.228 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
   3.229 +
   3.230 +
   3.231 +by (asm_simp_tac (simpset() addsimps [less_not_sym] setsubgoaler simp_tac) 1);
   3.232 +
   3.233 +
   3.234 +by (REPEAT (Safe_step_tac 2));
   3.235 +by (REPEAT (Safe_step_tac 2 THEN Blast_tac 2));
   3.236 +
   3.237 +by (auto_tac (claset() addIs [diff_Suc_less_diff], 
   3.238 +	      simpset() addsimps [metric_def]));
   3.239 +qed "E_thm16b";
   3.240 +
   3.241 +
   3.242 +
   3.243 +Goal "[|  m <= i; i < fl; ~ fl < n; fl - 1 < n |] ==> ~ n < fl - 1 --> n < fl --> fl - 1 - m + (n - m) < fl - n";
   3.244 +
   3.245 +
   3.246 +not_less_iff_le
   3.247 +
   3.248 +Goal "[|  ~ m < n; m - 1 < n |] ==> n = m";
   3.249 +by (cut_facts_tac [less_linear] 1);
   3.250 +by (blast_tac (claset() addSEs [less_irrefl]) 1);
   3.251 + by (REPEAT (etac rev_mp 1));
   3.252 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   3.253 +by (arith_oracle_tac 1);
   3.254 +
   3.255 +
   3.256 +
   3.257 +
   3.258 +
   3.259 +
   3.260 +
   3.261 +(**in the postscript file, but too horrible**)
   3.262 +
   3.263 +Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} - goingup) \
   3.264 +\                  (moving Int Req n Int {s. metric n s < N})";
   3.265 +by (ensures_tac defs "req_down_act" 1);
   3.266 +by (REPEAT_FIRST (etac rev_mp'));
   3.267 +
   3.268 +by (dtac less_eq_Suc_add 2);
   3.269 +by (Clarify_tac 2);
   3.270 +by (Asm_full_simp_tac 2);
   3.271 +by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
   3.272 +
   3.273 +
   3.274 +yyyyyyyyyyyyyyyy;
   3.275 +
   3.276 +by (REPEAT (Safe_step_tac 2));
   3.277 +by(blast_tac (claset() addEs [less_asym]) 2);
   3.278 +by (REPEAT (Safe_step_tac 2));
   3.279 +by(Blast_tac 2);
   3.280 +by(Blast_tac 2);
   3.281 +by (REPEAT (Safe_step_tac 2));
   3.282 +by(Blast_tac 2);
   3.283 +by(Blast_tac 2);
   3.284 +by (REPEAT (Safe_step_tac 2));
   3.285 +by(blast_tac (claset() addEs [less_asym]) 2);
   3.286 +by(blast_tac (claset() addDs [le_anti_sym]
   3.287 +		       addSDs [leI, pred_less_imp_le]) 2);
   3.288 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
   3.289 +
   3.290  
   3.291 -Goal "LeadsTo Lprg {s. MM s = 2} {s. PP s}";
   3.292 -by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
   3.293 -	  MRS LeadsTo_Diff) 1);
   3.294 -by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
   3.295 -by (auto_tac (claset() addSEs [less_SucE], simpset()));
   3.296 -val U_lemma2 = result();
   3.297 +by(Blast_tac 3);
   3.298 +
   3.299 +
   3.300 +
   3.301 +
   3.302 +
   3.303 +
   3.304 +
   3.305 +Goal "m < fl ==> n - Suc (fl) < fl - m + (n - m)";
   3.306 +fe rev_mp;
   3.307 +by (res_inst_tac [("m","MIN"),("n","fl")] diff_induct 1);
   3.308 +		by (ALLGOALS Asm_simp_tac);
   3.309 +
   3.310 +by (arith_oracle_tac 1);
   3.311 +
   3.312 +
   3.313 +Goal "[| Suc (fl) < n; m < n |] ==> n - Suc (fl) < fl - m + (n - m)";
   3.314 +by (REPEAT (etac rev_mp 1));
   3.315 +by (arith_oracle_tac 1);
   3.316 +
   3.317 +
   3.318 +
   3.319 +
   3.320 +
   3.321 +
   3.322 +
   3.323 +infixr TRANS;
   3.324 +fun th1 TRANS th2 = [th1, th2] MRS LeadsTo_Trans_Un';
   3.325 +
   3.326 +E_thm02 TRANS E_thm03 TRANS (lift_2 RS LeadsTo_Un_post');
   3.327 +
   3.328 +
   3.329 +
   3.330 +[E_thm02, 
   3.331 + E_thm03 RS LeadsTo_Un_post'] MRS LeadsTo_Trans_Un';
   3.332 +
   3.333  
   3.334 -***)
   3.335 +val sact = "open_act";
   3.336 +val sact = "move_up_act";
   3.337 +
   3.338 +val (main_def::CDEFS) = defs;
   3.339 +
   3.340 +by (REPEAT (Invariant_Int_tac 1));
   3.341 +
   3.342 +by (etac Invariant_LeadsTo_Basis 1 
   3.343 +	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   3.344 +		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1));
   3.345 +
   3.346 +by (res_inst_tac [("act", sact)] transient_mem 2);
   3.347 +by (simp_tac (simpset() addsimps (Domain_partial_func::CDEFS)) 3);
   3.348 +by (force_tac (claset(), simpset() addsimps [main_def]) 2);
   3.349 +by (constrains_tac (main_def::CDEFS) 1);
   3.350 +by (rewrite_goals_tac CDEFS);
   3.351 +by (ALLGOALS Clarify_tac);
   3.352 +by (Auto_tac);
   3.353 +
   3.354 +by(Force_tac 2);
   3.355 +
   3.356 +
   3.357 +
   3.358 +yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
   3.359 +
   3.360 +
   3.361 +
   3.362 +Goalw [transient_def]
   3.363 +     "transient acts A = (EX act:acts. A <= act^-1 ^^ (Compl A))";
   3.364 +by Safe_tac;
   3.365 +by (ALLGOALS (rtac bexI));
   3.366 +by (TRYALL assume_tac);
   3.367 +by (Blast_tac 1);
   3.368 +br conjI 1;
   3.369 +by (Blast_tac 1);
   3.370 +(*remains to show  
   3.371 +  [| act : acts; A <= act^-1 ^^ Compl A |] ==> act ^^ A <= Compl A
   3.372 +*)
   3.373 +
     4.1 --- a/src/HOL/UNITY/Lift.thy	Wed Aug 19 10:29:01 1998 +0200
     4.2 +++ b/src/HOL/UNITY/Lift.thy	Wed Aug 19 10:34:31 1998 +0200
     4.3 @@ -4,6 +4,8 @@
     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 +
    4.12 @@ -17,11 +19,15 @@
    4.13    move  :: bool		(*whether moving takes precedence over opening*)
    4.14  
    4.15  consts
    4.16 -  min, max :: nat	(*least and greatest floors*)
    4.17 +  min, max :: nat       (*least and greatest floors*)
    4.18  
    4.19  rules
    4.20    min_le_max  "min <= max"
    4.21    
    4.22 +  (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
    4.23 +  arith1      "m < fl ==> n - Suc fl < fl - m + (n - m)"
    4.24 +  arith2      "[| Suc fl < n; m < n |] ==> n - Suc fl < fl - m + (n - m)"
    4.25 +
    4.26  
    4.27  constdefs
    4.28    
    4.29 @@ -37,7 +43,7 @@
    4.30      "queueing == above Un below"
    4.31  
    4.32    goingup :: state set
    4.33 -    "goingup == above Int ({s. up s} Un Compl below)"
    4.34 +    "goingup   == above Int  ({s. up s}  Un Compl below)"
    4.35  
    4.36    goingdown :: state set
    4.37      "goingdown == below Int ({s. ~ up s} Un Compl above)"
    4.38 @@ -52,17 +58,20 @@
    4.39      "moving ==  {s. ~ stop s & ~ open s}"
    4.40  
    4.41    stopped :: state set
    4.42 -    "stopped == {s. stop s  & ~ open s &  move s}"
    4.43 +    "stopped == {s. stop s  & ~ open s & ~ move s}"
    4.44  
    4.45    opened :: state set
    4.46      "opened ==  {s. stop s  &  open s  &  move s}"
    4.47  
    4.48 -  closed :: state set
    4.49 +  closed :: state set  (*but this is the same as ready!!*)
    4.50      "closed ==  {s. stop s  & ~ open s &  move s}"
    4.51  
    4.52    atFloor :: nat => state set
    4.53      "atFloor n ==  {s. floor s = n}"
    4.54  
    4.55 +  Req :: nat => state set
    4.56 +    "Req n ==  {s. n : req s}"
    4.57 +
    4.58  
    4.59    
    4.60    (** The program **)
    4.61 @@ -125,7 +134,7 @@
    4.62      "open_move == {s. open s --> move s}"
    4.63    
    4.64    stop_floor :: state set
    4.65 -    "stop_floor == {s. open s & ~ move s --> floor s : req s}"
    4.66 +    "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
    4.67    
    4.68    moving_up :: state set
    4.69      "moving_up == {s. ~ stop s & up s -->
    4.70 @@ -135,8 +144,19 @@
    4.71      "moving_down == {s. ~ stop s & ~ up s -->
    4.72                       (EX f. min <= f & f <= floor s & f : req s)}"
    4.73    
    4.74 -  (*intersection of all invariants: NECESSARY??*)
    4.75 -  valid :: state set
    4.76 -    "valid == bounded Int open_stop Int open_move"
    4.77 +  metric :: [nat,state] => nat
    4.78 +    "metric n s == if up s & floor s < n then n - floor s
    4.79 +		   else if ~ up s & n < floor s then floor s - n
    4.80 +		   else if up s & n < floor s then (max - floor s) + (max-n)
    4.81 +		   else if ~ up s & floor s < n then (floor s - min) + (n-min)
    4.82 +		   else 0"
    4.83 +
    4.84 +locale floor =
    4.85 +  fixes 
    4.86 +    n	:: nat
    4.87 +  assumes
    4.88 +    min_le_n    "min <= n"
    4.89 +    n_le_max    "n <= max"
    4.90 +  defines
    4.91  
    4.92  end
     5.1 --- a/src/HOL/UNITY/Mutex.ML	Wed Aug 19 10:29:01 1998 +0200
     5.2 +++ b/src/HOL/UNITY/Mutex.ML	Wed Aug 19 10:34:31 1998 +0200
     5.3 @@ -76,7 +76,7 @@
     5.4  qed "U_F1";
     5.5  
     5.6  Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
     5.7 -by (cut_facts_tac [invariantUV] 1);
     5.8 +by (cut_facts_tac [invariantU] 1);
     5.9  by (rewtac Mprg_def);
    5.10  by (ensures_tac cmd_defs "cmd2U" 1);
    5.11  qed "U_F2";
    5.12 @@ -88,7 +88,7 @@
    5.13  qed "U_F3";
    5.14  
    5.15  Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}";
    5.16 -by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
    5.17 +by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
    5.18  	  MRS LeadsTo_Diff) 1);
    5.19  by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
    5.20  by (auto_tac (claset() addSEs [less_SucE], simpset()));
    5.21 @@ -125,7 +125,7 @@
    5.22  qed "V_F1";
    5.23  
    5.24  Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}";
    5.25 -by (cut_facts_tac [invariantUV] 1);
    5.26 +by (cut_facts_tac [invariantV] 1);
    5.27  by (ensures_tac cmd_defs "cmd2V" 1);
    5.28  qed "V_F2";
    5.29  
    5.30 @@ -136,7 +136,7 @@
    5.31  qed "V_F3";
    5.32  
    5.33  Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}";
    5.34 -by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
    5.35 +by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
    5.36  	  MRS LeadsTo_Diff) 1);
    5.37  by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
    5.38  by (auto_tac (claset() addSEs [less_SucE], simpset()));
     6.1 --- a/src/HOL/UNITY/SubstAx.ML	Wed Aug 19 10:29:01 1998 +0200
     6.2 +++ b/src/HOL/UNITY/SubstAx.ML	Wed Aug 19 10:34:31 1998 +0200
     6.3 @@ -6,6 +6,9 @@
     6.4  LeadsTo relation, restricted to the set of reachable states.
     6.5  *)
     6.6  
     6.7 +(*Map its type, ['a program, 'a set, 'a set] => bool, to just 'a*)
     6.8 +Blast.overloaded ("SubstAx.LeadsTo", 
     6.9 +		  HOLogic.dest_setT o domain_type o range_type);
    6.10  
    6.11  
    6.12  (*** Specialized laws for handling invariants ***)
    6.13 @@ -42,7 +45,7 @@
    6.14  by (Simp_tac 1);
    6.15  by (stac Int_Union 1);
    6.16  by (blast_tac (claset() addIs [leadsTo_UN,
    6.17 -			        simplify (simpset()) prem]) 1);
    6.18 +			       simplify (simpset()) prem]) 1);
    6.19  qed "LeadsTo_Union";
    6.20  
    6.21  
    6.22 @@ -88,15 +91,36 @@
    6.23  by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
    6.24  qed_spec_mp "LeadsTo_weaken_R";
    6.25  
    6.26 -
    6.27  Goal "[| LeadsTo prg A A';  B <= A; id: Acts prg |]  \
    6.28  \     ==> LeadsTo prg B A'";
    6.29  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
    6.30  by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
    6.31  qed_spec_mp "LeadsTo_weaken_L";
    6.32  
    6.33 +Goal "[| LeadsTo prg A A'; id: Acts prg;   \
    6.34 +\        B  <= A;   A' <= B' |] \
    6.35 +\     ==> LeadsTo prg B B'";
    6.36 +(*PROOF FAILED unless the Trans rule is last*)
    6.37 +by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
    6.38 +			       LeadsTo_Trans]) 1);
    6.39 +qed "LeadsTo_weaken";
    6.40  
    6.41 -(*Distributes over binary unions*)
    6.42 +
    6.43 +(** Two theorems for "proof lattices" **)
    6.44 +
    6.45 +Goal "[| id: Acts prg; LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
    6.46 +by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
    6.47 +qed "LeadsTo_Un_post";
    6.48 +
    6.49 +Goal "[| id: Acts prg;  LeadsTo prg A B;  LeadsTo prg B C |] \
    6.50 +\     ==> LeadsTo prg (A Un B) C";
    6.51 +by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, 
    6.52 +			       LeadsTo_weaken_L, LeadsTo_Trans]) 1);
    6.53 +qed "LeadsTo_Trans_Un";
    6.54 +
    6.55 +
    6.56 +(** Distributive laws **)
    6.57 +
    6.58  Goal "id: Acts prg ==> \
    6.59  \       LeadsTo prg (A Un B) C  =  \
    6.60  \       (LeadsTo prg A C & LeadsTo prg B C)";
    6.61 @@ -116,15 +140,6 @@
    6.62  qed "LeadsTo_Union_distrib";
    6.63  
    6.64  
    6.65 -Goal "[| LeadsTo prg A A'; id: Acts prg;   \
    6.66 -\        B  <= A;   A' <= B' |] \
    6.67 -\     ==> LeadsTo prg B B'";
    6.68 -(*PROOF FAILED*)
    6.69 -by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
    6.70 -			       LeadsTo_weaken_L]) 1);
    6.71 -qed "LeadsTo_weaken";
    6.72 -
    6.73 -
    6.74  (** More rules using the premise "Invariant prg" **)
    6.75  
    6.76  Goalw [LeadsTo_def, Constrains_def]
    6.77 @@ -160,12 +175,18 @@
    6.78  
    6.79  (*Set difference: maybe combine with leadsTo_weaken_L??
    6.80    This is the most useful form of the "disjunction" rule*)
    6.81 -Goal "[| LeadsTo prg (A-B) C; LeadsTo prg B C; id: Acts prg |] \
    6.82 +Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C; id: Acts prg |] \
    6.83  \     ==> LeadsTo prg A C";
    6.84 -by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
    6.85 +by (stac (Un_Diff_Int RS sym) 1 THEN rtac LeadsTo_Un 1);
    6.86 +by (REPEAT (assume_tac 1));
    6.87 +(*One step, but PROOF FAILED...
    6.88 +  by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
    6.89 +*)
    6.90  qed "LeadsTo_Diff";
    6.91  
    6.92  
    6.93 +
    6.94 +
    6.95  val prems = 
    6.96  Goal "(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \
    6.97  \     ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)";
    6.98 @@ -405,8 +426,10 @@
    6.99  	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   6.100  		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
   6.101  	      res_inst_tac [("act", sact)] transient_mem 2,
   6.102 +                 (*simplify the command's domain*)
   6.103  	      simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
   6.104 -	      simp_tac (simpset() addsimps [main_def]) 2,
   6.105 +	         (*INSIST that the command belongs to the program*)
   6.106 +	      force_tac (claset(), simpset() addsimps [main_def]) 2,
   6.107  	      constrains_tac (main_def::cmd_defs) 1,
   6.108  	      rewrite_goals_tac cmd_defs,
   6.109  	      ALLGOALS Clarify_tac,
     7.1 --- a/src/HOL/UNITY/UNITY.ML	Wed Aug 19 10:29:01 1998 +0200
     7.2 +++ b/src/HOL/UNITY/UNITY.ML	Wed Aug 19 10:34:31 1998 +0200
     7.3 @@ -14,6 +14,14 @@
     7.4  
     7.5  (*** constrains ***)
     7.6  
     7.7 +(*Map the type (anything => ('a set => anything) to just 'a*)
     7.8 +fun overload_2nd_set s =
     7.9 +    Blast.overloaded (s, HOLogic.dest_setT o domain_type o range_type);
    7.10 +
    7.11 +overload_2nd_set "UNITY.constrains";
    7.12 +overload_2nd_set "UNITY.stable";
    7.13 +overload_2nd_set "UNITY.unless";
    7.14 +
    7.15  val prems = Goalw [constrains_def]
    7.16      "(!!act s s'. [| act: acts;  (s,s') : act;  s: A |] ==> s': A') \
    7.17  \    ==> constrains acts A A'";
     8.1 --- a/src/HOL/UNITY/WFair.ML	Wed Aug 19 10:29:01 1998 +0200
     8.2 +++ b/src/HOL/UNITY/WFair.ML	Wed Aug 19 10:34:31 1998 +0200
     8.3 @@ -9,6 +9,14 @@
     8.4  *)
     8.5  
     8.6  
     8.7 +(*Map its type, [('a * 'a)set set] => ('a set * 'a set) set, to just 'a*)
     8.8 +Blast.overloaded ("WFair.leadsto", 
     8.9 +		  #1 o HOLogic.dest_prodT o 
    8.10 +		  HOLogic.dest_setT o HOLogic.dest_setT o domain_type);
    8.11 +
    8.12 +overload_2nd_set "WFair.transient";
    8.13 +overload_2nd_set "WFair.ensures";
    8.14 +
    8.15  (*** transient ***)
    8.16  
    8.17  Goalw [stable_def, constrains_def, transient_def]
    8.18 @@ -52,8 +60,7 @@
    8.19  
    8.20  Goalw [ensures_def, constrains_def, transient_def]
    8.21      "acts ~= {} ==> ensures acts A UNIV";
    8.22 -by (Asm_simp_tac 1);  (*omitting this causes PROOF FAILED, even with Safe_tac*)
    8.23 -by (Blast_tac 1);
    8.24 +by Auto_tac;
    8.25  qed "ensures_UNIV";
    8.26  
    8.27  Goalw [ensures_def]
    8.28 @@ -165,9 +172,9 @@
    8.29  
    8.30  Goal "[| leadsTo acts A A'; id: acts; B<=A; A'<=B' |] \
    8.31  \   ==> leadsTo acts B B'";
    8.32 -(*PROOF FAILED: why?*)
    8.33 -by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,
    8.34 -			       leadsTo_weaken_L]) 1);
    8.35 +(*PROOF FAILED unless leadsTo_Trans is last*)
    8.36 +by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
    8.37 +			       leadsTo_Trans]) 1);
    8.38  qed "leadsTo_weaken";
    8.39  
    8.40  
    8.41 @@ -468,7 +475,7 @@
    8.42  (*** Completion: Binary and General Finite versions ***)
    8.43  
    8.44  Goal "[| leadsTo acts A A';  stable acts A';   \
    8.45 -\      leadsTo acts B B';  stable acts B';  id: acts |] \
    8.46 +\        leadsTo acts B B';  stable acts B';  id: acts |] \
    8.47  \   ==> leadsTo acts (A Int B) (A' Int B')";
    8.48  by (subgoal_tac "stable acts (wlt acts B')" 1);
    8.49  by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
    8.50 @@ -483,8 +490,8 @@
    8.51  by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
    8.52  by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
    8.53  			       subset_imp_leadsTo]) 2);
    8.54 -(*Blast_tac gives PROOF FAILED*)
    8.55 -by (best_tac (claset() addIs [leadsTo_Trans]) 1);
    8.56 +(*addIs looks safer, but loops with PROOF FAILED*)
    8.57 +by (blast_tac (claset() addSIs [leadsTo_Trans]) 1);
    8.58  qed "stable_completion";
    8.59  
    8.60  
     9.1 --- a/src/HOL/UNITY/WFair.thy	Wed Aug 19 10:29:01 1998 +0200
     9.2 +++ b/src/HOL/UNITY/WFair.thy	Wed Aug 19 10:34:31 1998 +0200
     9.3 @@ -21,11 +21,12 @@
     9.4      "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)"
     9.5  			(*(unless acts A B) would be equivalent*)
     9.6  
     9.7 -consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
     9.8 -       leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
     9.9 +syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
    9.10 +consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
    9.11    
    9.12  translations
    9.13    "leadsTo acts A B" == "(A,B) : leadsto acts"
    9.14 +  "~ leadsTo acts A B" <= "(A,B) ~: leadsto acts"
    9.15  
    9.16  inductive "leadsto acts"
    9.17    intrs