1.1 --- a/src/HOL/UNITY/Lift.ML Thu Aug 20 16:58:28 1998 +0200
1.2 +++ b/src/HOL/UNITY/Lift.ML Thu Aug 20 17:43:01 1998 +0200
1.3 @@ -6,19 +6,21 @@
1.4 The Lift-Control Example
1.5 *)
1.6
1.7 -(*ARITH.ML??*)
1.8 -Goal "m-1 < n ==> m <= n";
1.9 -by (exhaust_tac "m" 1);
1.10 -by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
1.11 -qed "pred_less_imp_le";
1.12
1.13 +(*To move 0 < metric n s out of the assumptions for case splitting*)
1.14 +val rev_mp' = read_instantiate_sg (sign_of thy)
1.15 + [("P", "0 < metric ?n ?s")] rev_mp;
1.16 +
1.17 +val Suc_lessD_contra = Suc_lessD COMP rev_contrapos;
1.18 +val Suc_lessD_contra' = less_not_sym RS Suc_lessD_contra;
1.19
1.20 val always_defs = [above_def, below_def, queueing_def,
1.21 goingup_def, goingdown_def, ready_def];
1.22
1.23 val cmd_defs = [Lprg_def,
1.24 request_act_def, open_act_def, close_act_def,
1.25 - req_up_act_def, req_down_act_def, move_up_def, move_down_def];
1.26 + req_up_def, req_down_def, move_up_def, move_down_def,
1.27 + button_press_def];
1.28
1.29 Goalw [Lprg_def] "id : Acts Lprg";
1.30 by (Simp_tac 1);
1.31 @@ -26,6 +28,19 @@
1.32 AddIffs [id_in_Acts];
1.33
1.34
1.35 +val LeadsTo_Un_post' = id_in_Acts RS LeadsTo_Un_post
1.36 +and LeadsTo_Trans_Un' = rotate_prems 1 (id_in_Acts RS LeadsTo_Trans_Un);
1.37 +(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
1.38 +
1.39 +
1.40 +val metric_simps =
1.41 + [metric_def, vimage_def,
1.42 + not_less_less_Suc_eq, less_not_sym RS not_less_less_Suc_eq,
1.43 + Suc_lessD_contra, Suc_lessD_contra',
1.44 + less_not_refl2, less_not_refl3];
1.45 +
1.46 +
1.47 +
1.48 (*split_all_tac causes a big blow-up*)
1.49 claset_ref() := claset() delSWrapper "split_all_tac";
1.50
1.51 @@ -37,7 +52,7 @@
1.52 Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
1.53 moving_up_def, moving_down_def];
1.54
1.55 -AddIffs [min_le_max];
1.56 +AddIffs [Min_le_Max];
1.57
1.58
1.59 val nat_exhaust_le_pred =
1.60 @@ -60,7 +75,6 @@
1.61 by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
1.62 qed "less_imp_le_pred";
1.63
1.64 -
1.65 Goalw [Lprg_def] "Invariant Lprg open_stop";
1.66 by (rtac InvariantI 1);
1.67 by (Force_tac 1);
1.68 @@ -123,35 +137,53 @@
1.69
1.70 (** The HUG'93 paper mistakenly omits the Req n from these! **)
1.71
1.72 +(** Lift_1 **)
1.73 +
1.74 +(*lem_lift_1_5*)
1.75 Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
1.76 by (cut_facts_tac [stop_floor] 1);
1.77 by (ensures_tac defs "open_act" 1);
1.78 qed "E_thm01";
1.79
1.80 +(*lem_lift_1_1*)
1.81 Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
1.82 \ (Req n Int opened - atFloor n)";
1.83 by (cut_facts_tac [stop_floor] 1);
1.84 by (ensures_tac defs "open_act" 1);
1.85 qed "E_thm02";
1.86
1.87 +(*lem_lift_1_2*)
1.88 Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
1.89 \ (Req n Int closed - (atFloor n - queueing))";
1.90 by (ensures_tac defs "close_act" 1);
1.91 qed "E_thm03";
1.92
1.93 +
1.94 +(*lem_lift_1_7*)
1.95 Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
1.96 \ (opened Int atFloor n)";
1.97 by (ensures_tac defs "open_act" 1);
1.98 qed "E_thm04";
1.99
1.100
1.101 -(** Theorem 5. Statements of thm05a and thm05b were wrong! **)
1.102 +(** Lift 2. Statements of thm05a and thm05b were wrong! **)
1.103
1.104 Open_locale "floor";
1.105
1.106 -AddIffs [thm "min_le_n", thm "n_le_max"];
1.107 +val Min_le_n = thm "Min_le_n";
1.108 +val n_le_Max = thm "n_le_Max";
1.109
1.110 -(*NOT an ensures property, but a mere inclusion*)
1.111 +AddIffs [Min_le_n, n_le_Max];
1.112 +
1.113 +val le_MinD = Min_le_n RS le_anti_sym;
1.114 +val Max_leD = n_le_Max RSN (2,le_anti_sym);
1.115 +
1.116 +AddSDs [le_MinD, leI RS le_MinD,
1.117 + Max_leD, leI RS Max_leD];
1.118 +
1.119 +(*lem_lift_2_0
1.120 + NOT an ensures property, but a mere inclusion;
1.121 + don't know why script lift_2.uni says ENSURES*)
1.122 Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
1.123 \ ((closed Int goingup Int Req n) Un \
1.124 \ (closed Int goingdown Int Req n))";
1.125 @@ -159,21 +191,248 @@
1.126 by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs));
1.127 qed "E_thm05c";
1.128
1.129 +(*lift_2*)
1.130 Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
1.131 \ (moving Int Req n)";
1.132 br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
1.133 -by (ensures_tac defs "req_down_act" 2);
1.134 -by (ensures_tac defs "req_up_act" 1);
1.135 +by (ensures_tac defs "req_down" 2);
1.136 +by (ensures_tac defs "req_up" 1);
1.137 qed "lift_2";
1.138
1.139
1.140 +(** Towards lift_4 ***)
1.141
1.142 -val LeadsTo_Un_post' = id_in_Acts RS LeadsTo_Un_post
1.143 -and LeadsTo_Trans_Un' = rotate_prems 1 (id_in_Acts RS LeadsTo_Trans_Un);
1.144 -(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
1.145 +Goal "[| x ~: A; y : A |] ==> x ~= y";
1.146 +by (Blast_tac 1);
1.147 +qed "not_mem_distinct";
1.148
1.149 -val [lift_3] =
1.150 -goal thy "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n) ==> LeadsTo Lprg (Req n) (opened Int atFloor n)";
1.151 +fun distinct_tac i =
1.152 + dtac le_neq_implies_less i THEN
1.153 + eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN
1.154 + assume_tac i;
1.155 +
1.156 +
1.157 +(*lem_lift_4_1 *)
1.158 +Goal "0 < N ==> \
1.159 +\ LeadsTo Lprg \
1.160 +\ (moving Int Req n Int (metric n -`` {N}) Int \
1.161 +\ {s. floor s ~: req s} Int {s. up s}) \
1.162 +\ (moving Int Req n Int (metric n -`` lessThan N))";
1.163 +by (cut_facts_tac [moving_up] 1);
1.164 +by (ensures_tac defs "move_up" 1);
1.165 +(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
1.166 +be (leI RS le_anti_sym RS sym) 1;
1.167 +by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
1.168 +by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
1.169 +by (REPEAT_FIRST (etac rev_mp'));
1.170 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
1.171 +by (distinct_tac 1);
1.172 +by (auto_tac
1.173 + (claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)]
1.174 + addIs [diff_Suc_less_diff],
1.175 + simpset()));
1.176 +qed "E_thm12a";
1.177 +
1.178 +
1.179 +(*This rule helps eliminate occurrences of (floor s - 1) *)
1.180 +val less_floor_imp = read_instantiate_sg (sign_of thy)
1.181 + [("n", "floor ?s")] less_eq_Suc_add RS exE;
1.182 +
1.183 +(*lem_lift_4_3 *)
1.184 +Goal "0 < N ==> \
1.185 +\ LeadsTo Lprg \
1.186 +\ (moving Int Req n Int (metric n -`` {N}) Int \
1.187 +\ {s. floor s ~: req s} - {s. up s}) \
1.188 +\ (moving Int Req n Int (metric n -`` lessThan N))";
1.189 +by (cut_facts_tac [moving_down] 1);
1.190 +by (ensures_tac defs "move_down" 1);
1.191 +by (ALLGOALS distinct_tac);
1.192 +by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
1.193 +(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
1.194 +be (leI RS le_anti_sym RS sym) 1;
1.195 +by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
1.196 +by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
1.197 +by (REPEAT_FIRST (etac rev_mp'));
1.198 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
1.199 +by (auto_tac
1.200 + (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)]
1.201 + addIs [diff_le_Suc_diff, diff_less_Suc_diff],
1.202 + simpset() addsimps [trans_le_add1]));
1.203 +qed "E_thm12b";
1.204 +
1.205 +
1.206 +(*lift_4*)
1.207 +Goal "0<N ==> LeadsTo Lprg (moving Int Req n Int (metric n -`` {N}) Int \
1.208 +\ {s. floor s ~: req s}) \
1.209 +\ (moving Int Req n Int (metric n -`` lessThan N))";
1.210 +br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
1.211 +by (etac E_thm12b 4);
1.212 +by (etac E_thm12a 3);
1.213 +by (rtac id_in_Acts 2);
1.214 +by (Blast_tac 1);
1.215 +qed "lift_4";
1.216 +
1.217 +
1.218 +(** towards lift_5 **)
1.219 +
1.220 +(*lem_lift_5_3*)
1.221 +Goal "0<N \
1.222 +\ ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingup) \
1.223 +\ (moving Int Req n Int (metric n -`` lessThan N))";
1.224 +by (cut_facts_tac [bounded] 1);
1.225 +by (ensures_tac defs "req_up" 1);
1.226 +by (REPEAT_FIRST (etac rev_mp'));
1.227 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
1.228 +by (auto_tac (claset() addIs [diff_Suc_less_diff],
1.229 + simpset() addsimps [arith1, arith2]));
1.230 +qed "E_thm16a";
1.231 +
1.232 + (*arith1 comes from
1.233 + 1. !!s i.
1.234 + [| n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
1.235 + i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
1.236 + ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
1.237 + Suc (floor s) < n; 0 < floor s - Min |]
1.238 + ==> n - Suc (floor s) < floor s - Min + (n - Min)
1.239 + *)
1.240 +
1.241 + (*arith2 comes from
1.242 + 2. !!s i.
1.243 + [| Min <= floor s; ...
1.244 + n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
1.245 + i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
1.246 + ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
1.247 + Suc (floor s) < n; Min < n |]
1.248 + ==> n - Suc (floor s) < floor s - Min + (n - Min)
1.249 + *)
1.250 +
1.251 +(*lem_lift_5_1 has ~goingup instead of goingdown*)
1.252 +Goal "0<N ==> \
1.253 +\ LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingdown) \
1.254 +\ (moving Int Req n Int (metric n -`` lessThan N))";
1.255 +by (cut_facts_tac [bounded] 1);
1.256 +by (ensures_tac defs "req_down" 1);
1.257 +by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
1.258 +by (REPEAT_FIRST (etac rev_mp'));
1.259 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
1.260 +by (auto_tac (claset() addIs [diff_Suc_less_diff, diff_less_Suc_diff],
1.261 + simpset() addsimps [trans_le_add1, arith3, arith4]));
1.262 +qed "E_thm16b";
1.263 +
1.264 + (*arith3 comes from
1.265 + 1. !!s i x.
1.266 + [| floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max;
1.267 + ~ open s; n : req s; move s; Min <= i; i : req s;
1.268 + ALL ia. ia <= Max --> Suc (i + x) < ia --> ia ~: req s;
1.269 + ~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x;
1.270 + Suc (i + x) < Max |]
1.271 + ==> i + x - n < Max - Suc (i + x) + (Max - n)
1.272 + *)
1.273 +
1.274 + (*arith4 comes from
1.275 + 2. !!s i x.
1.276 + [| floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max;
1.277 + ~ open s; n : req s; move s; Min <= i; i : req s;
1.278 + ALL ia. ia <= Max --> Suc (i + x) < ia --> ia ~: req s;
1.279 + ~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x;
1.280 + n < Max |]
1.281 + ==> i + x - n < Max - Suc (i + x) + (Max - n)
1.282 + *)
1.283 +
1.284 +
1.285 +
1.286 +(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
1.287 + i.e. the trivial disjunction, leading to an asymmetrical proof.*)
1.288 +Goal "0<N ==> Req n Int (metric n -``{N}) <= goingup Un goingdown";
1.289 +by (asm_simp_tac (simpset() addsimps (defs@metric_simps)) 1);
1.290 +by (Blast_tac 1);
1.291 +qed "E_thm16c";
1.292 +
1.293 +
1.294 +(*lift_5*)
1.295 +Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N})) \
1.296 +\ (moving Int Req n Int (metric n -`` lessThan N))";
1.297 +br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
1.298 +by (etac E_thm16b 4);
1.299 +by (etac E_thm16a 3);
1.300 +by (rtac id_in_Acts 2);
1.301 +bd E_thm16c 1;
1.302 +by (Blast_tac 1);
1.303 +qed "lift_5";
1.304 +
1.305 +
1.306 +(** towards lift_3 **)
1.307 +
1.308 +(*lemma used to prove lem_lift_3_1*)
1.309 +Goal "[| metric n s = 0; Min <= floor s; floor s <= Max |] ==> floor s = n";
1.310 +be rev_mp 1;
1.311 +by (asm_simp_tac (simpset() addsimps metric_simps) 1);
1.312 +auto();
1.313 +qed "metric_eq_0D";
1.314 +
1.315 +AddDs [metric_eq_0D];
1.316 +
1.317 +
1.318 +(*lem_lift_3_1*)
1.319 +Goal "LeadsTo Lprg (moving Int Req n Int (metric n -`` {0})) \
1.320 +\ (stopped Int atFloor n)";
1.321 +by (cut_facts_tac [bounded] 1);
1.322 +by (ensures_tac defs "request_act" 1);
1.323 +qed "E_thm11";
1.324 +
1.325 +(*lem_lift_3_5*)
1.326 +Goal "LeadsTo Lprg \
1.327 +\ (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
1.328 +\ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})";
1.329 +by (ensures_tac defs "request_act" 1);
1.330 +by (asm_simp_tac (simpset() addsimps metric_simps) 1);
1.331 +qed "E_thm13";
1.332 +
1.333 +(*lem_lift_3_6*)
1.334 +Goal "0 < N ==> \
1.335 +\ LeadsTo Lprg \
1.336 +\ (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
1.337 +\ (opened Int Req n Int (metric n -`` {N}))";
1.338 +by (ensures_tac defs "open_act" 1);
1.339 +by (REPEAT_FIRST (etac rev_mp'));
1.340 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
1.341 +qed "E_thm14";
1.342 +
1.343 +(*lem_lift_3_7*)
1.344 +Goal "LeadsTo Lprg \
1.345 +\ (opened Int Req n Int (metric n -`` {N})) \
1.346 +\ (closed Int Req n Int (metric n -`` {N}))";
1.347 +by (ensures_tac defs "close_act" 1);
1.348 +by (asm_simp_tac (simpset() addsimps metric_simps) 1);
1.349 +qed "E_thm15";
1.350 +
1.351 +
1.352 +(** the final steps **)
1.353 +
1.354 +Goal "0 < N ==> \
1.355 +\ LeadsTo Lprg \
1.356 +\ (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
1.357 +\ (moving Int Req n Int (metric n -`` lessThan N))";
1.358 +(*Blast_tac: PROOF FAILED*)
1.359 +by (best_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
1.360 + addIs [LeadsTo_Trans]) 1);
1.361 +qed "lift_3_Req";
1.362 +
1.363 +
1.364 +Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
1.365 +br (allI RS LessThan_induct) 1;
1.366 +by (exhaust_tac "m" 1);
1.367 +auto();
1.368 +br E_thm11 1;
1.369 +br ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1;
1.370 +br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
1.371 +br lift_3_Req 4;
1.372 +br lift_4 3;
1.373 +auto();
1.374 +qed "lift_3";
1.375 +
1.376 +
1.377 +Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)";
1.378 br LeadsTo_Trans 1;
1.379 br (E_thm04 RS LeadsTo_Un) 2;
1.380 br LeadsTo_Un_post' 2;
1.381 @@ -189,230 +448,10 @@
1.382 bws defs;
1.383 by (Clarify_tac 1);
1.384 (*stops simplification from looping*)
1.385 -by (asm_full_simp_tac (simpset() setsubgoaler simp_tac) 1);
1.386 +by (Full_simp_tac 1);
1.387 by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1));
1.388 qed "lift_1";
1.389
1.390 +Close_locale;
1.391
1.392 -val rev_mp' = read_instantiate_sg (sign_of thy)
1.393 - [("P", "0 < metric ?n ?s")] rev_mp;
1.394
1.395 -
1.396 -Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
1.397 -\ (moving Int Req n Int {s. metric n s < N})";
1.398 -by (ensures_tac defs "req_up_act" 1);
1.399 -by (REPEAT_FIRST (etac rev_mp'));
1.400 -by (auto_tac (claset() addIs [diff_Suc_less_diff],
1.401 - simpset() addsimps [arith1, arith2, metric_def]));
1.402 -qed "E_thm16a";
1.403 -
1.404 -
1.405 -(*arith1 comes from
1.406 - 1. !!s i.
1.407 - [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
1.408 - i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
1.409 - ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
1.410 - Suc (floor s) < n; 0 < floor s - min |]
1.411 - ==> n - Suc (floor s) < floor s - min + (n - min)
1.412 -*)
1.413 -
1.414 -(*arith2 comes from
1.415 - 2. !!s i.
1.416 - [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
1.417 - i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
1.418 - ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
1.419 - Suc (floor s) < n; min < n |]
1.420 - ==> n - Suc (floor s) < floor s - min + (n - min)
1.421 -*)
1.422 -
1.423 -
1.424 -xxxxxxxxxxxxxxxx;
1.425 -
1.426 -Goal "j<=i ==> i - j < Suc i - j";
1.427 -by (REPEAT (etac rev_mp 1));
1.428 -by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
1.429 -by Auto_tac;
1.430 -qed "diff_less_Suc_diff";
1.431 -
1.432 -
1.433 -Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
1.434 -\ (moving Int Req n Int {s. metric n s < N})";
1.435 -by (ensures_tac defs "req_down_act" 1);
1.436 -be rev_mp 2;
1.437 -be rev_mp 1;
1.438 -by (dtac less_eq_Suc_add 2);
1.439 -by (Clarify_tac 2);
1.440 -by (Asm_full_simp_tac 2);
1.441 -by (dtac less_eq_Suc_add 1);
1.442 -by (Clarify_tac 1);
1.443 -by (Asm_full_simp_tac 1);
1.444 -
1.445 -by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
1.446 -by (REPEAT (Safe_step_tac 1));
1.447 -by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
1.448 -by (REPEAT (Safe_step_tac 1));
1.449 -by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
1.450 -by (REPEAT (Safe_step_tac 1));
1.451 -
1.452 -
1.453 -
1.454 -
1.455 -
1.456 -
1.457 -
1.458 -Goal "[| i + k < n; Suc (i + k) < n |] ==> i + k - m < Suc (i + k) - m";
1.459 -by (REPEAT (etac rev_mp 1));
1.460 -by (arith_oracle_tac 1);
1.461 -
1.462 -
1.463 -by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
1.464 -by (REPEAT (Safe_step_tac 2));
1.465 -by(Blast_tac 2);
1.466 -by(Blast_tac 2);
1.467 -by(Blast_tac 2);
1.468 -by (REPEAT (Safe_step_tac 2));
1.469 -by(Blast_tac 2);
1.470 -by(blast_tac (claset() addEs [less_asym]) 2);
1.471 -by (REPEAT (Safe_step_tac 2));
1.472 -by(blast_tac (claset() addEs [less_asym]) 2);
1.473 -by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
1.474 -by (REPEAT (Safe_step_tac 2));
1.475 -by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
1.476 -
1.477 -
1.478 -by (asm_simp_tac (simpset() addsimps [less_not_sym] setsubgoaler simp_tac) 1);
1.479 -
1.480 -
1.481 -by (REPEAT (Safe_step_tac 2));
1.482 -by (REPEAT (Safe_step_tac 2 THEN Blast_tac 2));
1.483 -
1.484 -by (auto_tac (claset() addIs [diff_Suc_less_diff],
1.485 - simpset() addsimps [metric_def]));
1.486 -qed "E_thm16b";
1.487 -
1.488 -
1.489 -
1.490 -Goal "[| m <= i; i < fl; ~ fl < n; fl - 1 < n |] ==> ~ n < fl - 1 --> n < fl --> fl - 1 - m + (n - m) < fl - n";
1.491 -
1.492 -
1.493 -not_less_iff_le
1.494 -
1.495 -Goal "[| ~ m < n; m - 1 < n |] ==> n = m";
1.496 -by (cut_facts_tac [less_linear] 1);
1.497 -by (blast_tac (claset() addSEs [less_irrefl]) 1);
1.498 - by (REPEAT (etac rev_mp 1));
1.499 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
1.500 -by (arith_oracle_tac 1);
1.501 -
1.502 -
1.503 -
1.504 -
1.505 -
1.506 -
1.507 -
1.508 -(**in the postscript file, but too horrible**)
1.509 -
1.510 -Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} - goingup) \
1.511 -\ (moving Int Req n Int {s. metric n s < N})";
1.512 -by (ensures_tac defs "req_down_act" 1);
1.513 -by (REPEAT_FIRST (etac rev_mp'));
1.514 -
1.515 -by (dtac less_eq_Suc_add 2);
1.516 -by (Clarify_tac 2);
1.517 -by (Asm_full_simp_tac 2);
1.518 -by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
1.519 -
1.520 -
1.521 -yyyyyyyyyyyyyyyy;
1.522 -
1.523 -by (REPEAT (Safe_step_tac 2));
1.524 -by(blast_tac (claset() addEs [less_asym]) 2);
1.525 -by (REPEAT (Safe_step_tac 2));
1.526 -by(Blast_tac 2);
1.527 -by(Blast_tac 2);
1.528 -by (REPEAT (Safe_step_tac 2));
1.529 -by(Blast_tac 2);
1.530 -by(Blast_tac 2);
1.531 -by (REPEAT (Safe_step_tac 2));
1.532 -by(blast_tac (claset() addEs [less_asym]) 2);
1.533 -by(blast_tac (claset() addDs [le_anti_sym]
1.534 - addSDs [leI, pred_less_imp_le]) 2);
1.535 -by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
1.536 -
1.537 -
1.538 -by(Blast_tac 3);
1.539 -
1.540 -
1.541 -
1.542 -
1.543 -
1.544 -
1.545 -
1.546 -Goal "m < fl ==> n - Suc (fl) < fl - m + (n - m)";
1.547 -fe rev_mp;
1.548 -by (res_inst_tac [("m","MIN"),("n","fl")] diff_induct 1);
1.549 - by (ALLGOALS Asm_simp_tac);
1.550 -
1.551 -by (arith_oracle_tac 1);
1.552 -
1.553 -
1.554 -Goal "[| Suc (fl) < n; m < n |] ==> n - Suc (fl) < fl - m + (n - m)";
1.555 -by (REPEAT (etac rev_mp 1));
1.556 -by (arith_oracle_tac 1);
1.557 -
1.558 -
1.559 -
1.560 -
1.561 -
1.562 -
1.563 -
1.564 -infixr TRANS;
1.565 -fun th1 TRANS th2 = [th1, th2] MRS LeadsTo_Trans_Un';
1.566 -
1.567 -E_thm02 TRANS E_thm03 TRANS (lift_2 RS LeadsTo_Un_post');
1.568 -
1.569 -
1.570 -
1.571 -[E_thm02,
1.572 - E_thm03 RS LeadsTo_Un_post'] MRS LeadsTo_Trans_Un';
1.573 -
1.574 -
1.575 -val sact = "open_act";
1.576 -val sact = "move_up_act";
1.577 -
1.578 -val (main_def::CDEFS) = defs;
1.579 -
1.580 -by (REPEAT (Invariant_Int_tac 1));
1.581 -
1.582 -by (etac Invariant_LeadsTo_Basis 1
1.583 - ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
1.584 - REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1));
1.585 -
1.586 -by (res_inst_tac [("act", sact)] transient_mem 2);
1.587 -by (simp_tac (simpset() addsimps (Domain_partial_func::CDEFS)) 3);
1.588 -by (force_tac (claset(), simpset() addsimps [main_def]) 2);
1.589 -by (constrains_tac (main_def::CDEFS) 1);
1.590 -by (rewrite_goals_tac CDEFS);
1.591 -by (ALLGOALS Clarify_tac);
1.592 -by (Auto_tac);
1.593 -
1.594 -by(Force_tac 2);
1.595 -
1.596 -
1.597 -
1.598 -yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
1.599 -
1.600 -
1.601 -
1.602 -Goalw [transient_def]
1.603 - "transient acts A = (EX act:acts. A <= act^-1 ^^ (Compl A))";
1.604 -by Safe_tac;
1.605 -by (ALLGOALS (rtac bexI));
1.606 -by (TRYALL assume_tac);
1.607 -by (Blast_tac 1);
1.608 -br conjI 1;
1.609 -by (Blast_tac 1);
1.610 -(*remains to show
1.611 - [| act : acts; A <= act^-1 ^^ Compl A |] ==> act ^^ A <= Compl A
1.612 -*)
1.613 -
2.1 --- a/src/HOL/UNITY/Lift.thy Thu Aug 20 16:58:28 1998 +0200
2.2 +++ b/src/HOL/UNITY/Lift.thy Thu Aug 20 17:43:01 1998 +0200
2.3 @@ -19,25 +19,26 @@
2.4 move :: bool (*whether moving takes precedence over opening*)
2.5
2.6 consts
2.7 - min, max :: nat (*least and greatest floors*)
2.8 + Min, Max :: nat (*least and greatest floors*)
2.9
2.10 rules
2.11 - min_le_max "min <= max"
2.12 + Min_le_Max "Min <= Max"
2.13
2.14 (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
2.15 arith1 "m < fl ==> n - Suc fl < fl - m + (n - m)"
2.16 - arith2 "[| Suc fl < n; m < n |] ==> n - Suc fl < fl - m + (n - m)"
2.17 -
2.18 + arith2 "[| m<n; m <= fl |] ==> n - Suc fl < fl - m + (n - m)"
2.19 + arith3 "[| Suc ix < m |] ==> ix - n < m - Suc ix + (m - n)"
2.20 + arith4 "[| ix < m; n < ix |] ==> ix - n < m - Suc (ix) + (m - n)"
2.21
2.22 constdefs
2.23
2.24 (** Abbreviations: the "always" part **)
2.25
2.26 above :: state set
2.27 - "above == {s. EX i. floor s < i & i <= max & i : req s}"
2.28 + "above == {s. EX i. floor s < i & i <= Max & i : req s}"
2.29
2.30 below :: state set
2.31 - "below == {s. EX i. min <= i & i < floor s & i : req s}"
2.32 + "below == {s. EX i. Min <= i & i < floor s & i : req s}"
2.33
2.34 queueing :: state set
2.35 "queueing == above Un below"
2.36 @@ -91,15 +92,15 @@
2.37 close_act :: "(state*state) set"
2.38 "close_act == {(s,s'). s' = s (|open := False|) & open s}"
2.39
2.40 - req_up_act :: "(state*state) set"
2.41 - "req_up_act ==
2.42 + req_up :: "(state*state) set"
2.43 + "req_up ==
2.44 {(s,s'). s' = s (|stop :=False,
2.45 floor := Suc (floor s),
2.46 up := True|)
2.47 & s : (ready Int goingup)}"
2.48
2.49 - req_down_act :: "(state*state) set"
2.50 - "req_down_act ==
2.51 + req_down :: "(state*state) set"
2.52 + "req_down ==
2.53 {(s,s'). s' = s (|stop :=False,
2.54 floor := floor s - 1,
2.55 up := False|)
2.56 @@ -115,17 +116,24 @@
2.57 {(s,s'). s' = s (|floor := floor s - 1|)
2.58 & ~ stop s & ~ up s & floor s ~: req s}"
2.59
2.60 + button_press :: "(state*state) set"
2.61 + "button_press ==
2.62 + {(s,s'). EX n. s' = s (|req := insert n (req s)|)
2.63 + & Min <= n & n <= Max}"
2.64 +
2.65 +
2.66 Lprg :: state program
2.67 - "Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s &
2.68 + (*for the moment, we OMIT button_press*)
2.69 + "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
2.70 ~ open s & req s = {}},
2.71 Acts = {id, request_act, open_act, close_act,
2.72 - req_up_act, req_down_act, move_up, move_down}|)"
2.73 + req_up, req_down, move_up, move_down}|)"
2.74
2.75
2.76 (** Invariants **)
2.77
2.78 bounded :: state set
2.79 - "bounded == {s. min <= floor s & floor s <= max}"
2.80 + "bounded == {s. Min <= floor s & floor s <= Max}"
2.81
2.82 open_stop :: state set
2.83 "open_stop == {s. open s --> stop s}"
2.84 @@ -138,25 +146,26 @@
2.85
2.86 moving_up :: state set
2.87 "moving_up == {s. ~ stop s & up s -->
2.88 - (EX f. floor s <= f & f <= max & f : req s)}"
2.89 + (EX f. floor s <= f & f <= Max & f : req s)}"
2.90
2.91 moving_down :: state set
2.92 "moving_down == {s. ~ stop s & ~ up s -->
2.93 - (EX f. min <= f & f <= floor s & f : req s)}"
2.94 + (EX f. Min <= f & f <= floor s & f : req s)}"
2.95
2.96 metric :: [nat,state] => nat
2.97 - "metric n s == if up s & floor s < n then n - floor s
2.98 - else if ~ up s & n < floor s then floor s - n
2.99 - else if up s & n < floor s then (max - floor s) + (max-n)
2.100 - else if ~ up s & floor s < n then (floor s - min) + (n-min)
2.101 - else 0"
2.102 + "metric ==
2.103 + %n s. if up s & floor s < n then n - floor s
2.104 + else if ~ up s & n < floor s then floor s - n
2.105 + else if up s & n < floor s then (Max - floor s) + (Max-n)
2.106 + else if ~ up s & floor s < n then (floor s - Min) + (n-Min)
2.107 + else 0"
2.108
2.109 locale floor =
2.110 fixes
2.111 n :: nat
2.112 assumes
2.113 - min_le_n "min <= n"
2.114 - n_le_max "n <= max"
2.115 + Min_le_n "Min <= n"
2.116 + n_le_Max "n <= Max"
2.117 defines
2.118
2.119 end
3.1 --- a/src/HOL/UNITY/ROOT.ML Thu Aug 20 16:58:28 1998 +0200
3.2 +++ b/src/HOL/UNITY/ROOT.ML Thu Aug 20 17:43:01 1998 +0200
3.3 @@ -20,3 +20,4 @@
3.4 time_use_thy "FP";
3.5 time_use_thy "Reach";
3.6 time_use_thy "Handshake";
3.7 +time_use_thy "Lift";