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 {s. ~ PP s & MM s = 2} {s. MM s = 3}";
3.69 -by (cut_facts_tac [invariantUV] 1);
3.70 -by (rewtac Lprg_def);
3.71 -by (ensures_tac defs "cmd2U" 1);
3.72 -qed "U_F2";
3.73 +Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
3.74 +\ (Req n Int opened - atFloor n)";
3.75 +by (cut_facts_tac [stop_floor] 1);
3.76 +by (ensures_tac defs "open_act" 1);
3.77 +qed "E_thm02";
3.78
3.79 -Goal "LeadsTo Lprg {s. MM s = 3} {s. PP s}";
3.80 -by (rtac leadsTo_imp_LeadsTo 1);
3.81 -by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
3.82 -by (ensures_tac defs "cmd4U" 2);
3.83 -by (ensures_tac defs "cmd3U" 1);
3.84 -qed "U_F3";
3.85 +Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
3.86 +\ (Req n Int closed - (atFloor n - queueing))";
3.87 +by (ensures_tac defs "close_act" 1);
3.88 +qed "E_thm03";
3.89
3.90 -Goal "LeadsTo Lprg {s. MM s = 2} {s. PP s}";
3.91 -by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo]
3.92 - MRS LeadsTo_Diff) 1);
3.93 -by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
3.94 -by (auto_tac (claset() addSEs [less_SucE], simpset()));
3.95 -val U_lemma2 = result();
3.96 +Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
3.97 +\ (opened Int atFloor n)";
3.98 +by (ensures_tac defs "open_act" 1);
3.99 +qed "E_thm04";
3.100
3.101 -***)
3.102 +
3.103 +(** Theorem 5. Statements of thm05a and thm05b were wrong! **)
3.104 +
3.105 +Open_locale "floor";
3.106 +
3.107 +AddIffs [thm "min_le_n", thm "n_le_max"];
3.108 +
3.109 +(*NOT an ensures property, but a mere inclusion*)
3.110 +Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
3.111 +\ ((closed Int goingup Int Req n) Un \
3.112 +\ (closed Int goingdown Int Req n))";
3.113 +br subset_imp_LeadsTo 1;
3.114 +by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs));
3.115 +qed "E_thm05c";
3.116 +
3.117 +Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
3.118 +\ (moving Int Req n)";
3.119 +br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
3.120 +by (ensures_tac defs "req_down_act" 2);
3.121 +by (ensures_tac defs "req_up_act" 1);
3.122 +qed "lift_2";
3.123 +
3.124 +
3.125 +
3.126 +val LeadsTo_Un_post' = id_in_Acts RS LeadsTo_Un_post
3.127 +and LeadsTo_Trans_Un' = rotate_prems 1 (id_in_Acts RS LeadsTo_Trans_Un);
3.128 +(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
3.129 +
3.130 +val [lift_3] =
3.131 +goal thy "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n) ==> LeadsTo Lprg (Req n) (opened Int atFloor n)";
3.132 +br LeadsTo_Trans 1;
3.133 +br (E_thm04 RS LeadsTo_Un) 2;
3.134 +br LeadsTo_Un_post' 2;
3.135 +br (E_thm01 RS LeadsTo_Trans_Un') 2;
3.136 +br (lift_3 RS LeadsTo_Trans_Un') 2;
3.137 +br (lift_2 RS LeadsTo_Trans_Un') 2;
3.138 +br (E_thm03 RS LeadsTo_Trans_Un') 2;
3.139 +br E_thm02 2;
3.140 +br (open_move RS Invariant_LeadsToI) 1;
3.141 +br (open_stop RS Invariant_LeadsToI) 1;
3.142 +br subset_imp_LeadsTo 1;
3.143 +by (rtac id_in_Acts 2);
3.144 +bws defs;
3.145 +by (Clarify_tac 1);
3.146 + (*stops simplification from looping*)
3.147 +by (asm_full_simp_tac (simpset() setsubgoaler simp_tac) 1);
3.148 +by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1));
3.149 +qed "lift_1";
3.150 +
3.151 +
3.152 +val rev_mp' = read_instantiate_sg (sign_of thy)
3.153 + [("P", "0 < metric ?n ?s")] rev_mp;
3.154 +
3.155 +
3.156 +Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
3.157 +\ (moving Int Req n Int {s. metric n s < N})";
3.158 +by (ensures_tac defs "req_up_act" 1);
3.159 +by (REPEAT_FIRST (etac rev_mp'));
3.160 +by (auto_tac (claset() addIs [diff_Suc_less_diff],
3.161 + simpset() addsimps [arith1, arith2, metric_def]));
3.162 +qed "E_thm16a";
3.163 +
3.164 +
3.165 +(*arith1 comes from
3.166 + 1. !!s i.
3.167 + [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
3.168 + i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
3.169 + ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
3.170 + Suc (floor s) < n; 0 < floor s - min |]
3.171 + ==> n - Suc (floor s) < floor s - min + (n - min)
3.172 +*)
3.173 +
3.174 +(*arith2 comes from
3.175 + 2. !!s i.
3.176 + [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
3.177 + i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
3.178 + ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
3.179 + Suc (floor s) < n; min < n |]
3.180 + ==> n - Suc (floor s) < floor s - min + (n - min)
3.181 +*)
3.182 +
3.183 +
3.184 +xxxxxxxxxxxxxxxx;
3.185 +
3.186 +Goal "j<=i ==> i - j < Suc i - j";
3.187 +by (REPEAT (etac rev_mp 1));
3.188 +by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
3.189 +by Auto_tac;
3.190 +qed "diff_less_Suc_diff";
3.191 +
3.192 +
3.193 +Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
3.194 +\ (moving Int Req n Int {s. metric n s < N})";
3.195 +by (ensures_tac defs "req_down_act" 1);
3.196 +be rev_mp 2;
3.197 +be rev_mp 1;
3.198 +by (dtac less_eq_Suc_add 2);
3.199 +by (Clarify_tac 2);
3.200 +by (Asm_full_simp_tac 2);
3.201 +by (dtac less_eq_Suc_add 1);
3.202 +by (Clarify_tac 1);
3.203 +by (Asm_full_simp_tac 1);
3.204 +
3.205 +by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
3.206 +by (REPEAT (Safe_step_tac 1));
3.207 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
3.208 +by (REPEAT (Safe_step_tac 1));
3.209 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
3.210 +by (REPEAT (Safe_step_tac 1));
3.211 +
3.212 +
3.213 +
3.214 +
3.215 +
3.216 +
3.217 +
3.218 +Goal "[| i + k < n; Suc (i + k) < n |] ==> i + k - m < Suc (i + k) - m";
3.219 +by (REPEAT (etac rev_mp 1));
3.220 +by (arith_oracle_tac 1);
3.221 +
3.222 +
3.223 +by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
3.224 +by (REPEAT (Safe_step_tac 2));
3.225 +by(Blast_tac 2);
3.226 +by(Blast_tac 2);
3.227 +by(Blast_tac 2);
3.228 +by (REPEAT (Safe_step_tac 2));
3.229 +by(Blast_tac 2);
3.230 +by(blast_tac (claset() addEs [less_asym]) 2);
3.231 +by (REPEAT (Safe_step_tac 2));
3.232 +by(blast_tac (claset() addEs [less_asym]) 2);
3.233 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
3.234 +by (REPEAT (Safe_step_tac 2));
3.235 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
3.236 +
3.237 +
3.238 +by (asm_simp_tac (simpset() addsimps [less_not_sym] setsubgoaler simp_tac) 1);
3.239 +
3.240 +
3.241 +by (REPEAT (Safe_step_tac 2));
3.242 +by (REPEAT (Safe_step_tac 2 THEN Blast_tac 2));
3.243 +
3.244 +by (auto_tac (claset() addIs [diff_Suc_less_diff],
3.245 + simpset() addsimps [metric_def]));
3.246 +qed "E_thm16b";
3.247 +
3.248 +
3.249 +
3.250 +Goal "[| m <= i; i < fl; ~ fl < n; fl - 1 < n |] ==> ~ n < fl - 1 --> n < fl --> fl - 1 - m + (n - m) < fl - n";
3.251 +
3.252 +
3.253 +not_less_iff_le
3.254 +
3.255 +Goal "[| ~ m < n; m - 1 < n |] ==> n = m";
3.256 +by (cut_facts_tac [less_linear] 1);
3.257 +by (blast_tac (claset() addSEs [less_irrefl]) 1);
3.258 + by (REPEAT (etac rev_mp 1));
3.259 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
3.260 +by (arith_oracle_tac 1);
3.261 +
3.262 +
3.263 +
3.264 +
3.265 +
3.266 +
3.267 +
3.268 +(**in the postscript file, but too horrible**)
3.269 +
3.270 +Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} - goingup) \
3.271 +\ (moving Int Req n Int {s. metric n s < N})";
3.272 +by (ensures_tac defs "req_down_act" 1);
3.273 +by (REPEAT_FIRST (etac rev_mp'));
3.274 +
3.275 +by (dtac less_eq_Suc_add 2);
3.276 +by (Clarify_tac 2);
3.277 +by (Asm_full_simp_tac 2);
3.278 +by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
3.279 +
3.280 +
3.281 +yyyyyyyyyyyyyyyy;
3.282 +
3.283 +by (REPEAT (Safe_step_tac 2));
3.284 +by(blast_tac (claset() addEs [less_asym]) 2);
3.285 +by (REPEAT (Safe_step_tac 2));
3.286 +by(Blast_tac 2);
3.287 +by(Blast_tac 2);
3.288 +by (REPEAT (Safe_step_tac 2));
3.289 +by(Blast_tac 2);
3.290 +by(Blast_tac 2);
3.291 +by (REPEAT (Safe_step_tac 2));
3.292 +by(blast_tac (claset() addEs [less_asym]) 2);
3.293 +by(blast_tac (claset() addDs [le_anti_sym]
3.294 + addSDs [leI, pred_less_imp_le]) 2);
3.295 +by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
3.296 +
3.297 +
3.298 +by(Blast_tac 3);
3.299 +
3.300 +
3.301 +
3.302 +
3.303 +
3.304 +
3.305 +
3.306 +Goal "m < fl ==> n - Suc (fl) < fl - m + (n - m)";
3.307 +fe rev_mp;
3.308 +by (res_inst_tac [("m","MIN"),("n","fl")] diff_induct 1);
3.309 + by (ALLGOALS Asm_simp_tac);
3.310 +
3.311 +by (arith_oracle_tac 1);
3.312 +
3.313 +
3.314 +Goal "[| Suc (fl) < n; m < n |] ==> n - Suc (fl) < fl - m + (n - m)";
3.315 +by (REPEAT (etac rev_mp 1));
3.316 +by (arith_oracle_tac 1);
3.317 +
3.318 +
3.319 +
3.320 +
3.321 +
3.322 +
3.323 +
3.324 +infixr TRANS;
3.325 +fun th1 TRANS th2 = [th1, th2] MRS LeadsTo_Trans_Un';
3.326 +
3.327 +E_thm02 TRANS E_thm03 TRANS (lift_2 RS LeadsTo_Un_post');
3.328 +
3.329 +
3.330 +
3.331 +[E_thm02,
3.332 + E_thm03 RS LeadsTo_Un_post'] MRS LeadsTo_Trans_Un';
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