New theory Lift
authorpaulson
Thu Aug 20 17:43:01 1998 +0200 (1998-08-20)
changeset 53576efb2b87610c
parent 5356 6ef114ba5b55
child 5358 7e046ef59fe2
New theory Lift
src/HOL/UNITY/Lift.ML
src/HOL/UNITY/Lift.thy
src/HOL/UNITY/ROOT.ML
     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 +AddIffs [Min_le_n, n_le_Max];
   1.111  
   1.112 -(*NOT an ensures property, but a mere inclusion*)
   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 +fun distinct_tac i =
   1.150 +    dtac le_neq_implies_less i THEN
   1.151 +    eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN
   1.152 +    assume_tac i;
   1.153 +
   1.154 +
   1.155 +(*lem_lift_4_1 *)
   1.156 +Goal "0 < N ==> \
   1.157 +\     LeadsTo Lprg \
   1.158 +\       (moving Int Req n Int (metric n -`` {N}) Int \
   1.159 +\        {s. floor s ~: req s} Int {s. up s})   \
   1.160 +\       (moving Int Req n Int (metric n -`` lessThan N))";
   1.161 +by (cut_facts_tac [moving_up] 1);
   1.162 +by (ensures_tac defs "move_up" 1);
   1.163 +(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   1.164 +be (leI RS le_anti_sym RS sym) 1;
   1.165 +by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
   1.166 +by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
   1.167 +by (REPEAT_FIRST (etac rev_mp'));
   1.168 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
   1.169 +by (distinct_tac 1);
   1.170 +by (auto_tac
   1.171 +    (claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)]
   1.172 +	      addIs [diff_Suc_less_diff], 
   1.173 +     simpset()));
   1.174 +qed "E_thm12a";
   1.175 +
   1.176 +
   1.177 +(*This rule helps eliminate occurrences of  (floor s - 1) *)
   1.178 +val less_floor_imp = read_instantiate_sg (sign_of thy) 
   1.179 +                 [("n", "floor ?s")] less_eq_Suc_add RS exE;
   1.180 +
   1.181 +(*lem_lift_4_3 *)
   1.182 +Goal "0 < N ==> \
   1.183 +\     LeadsTo Lprg \
   1.184 +\       (moving Int Req n Int (metric n -`` {N}) Int \
   1.185 +\        {s. floor s ~: req s} - {s. up s})   \
   1.186 +\       (moving Int Req n Int (metric n -`` lessThan N))";
   1.187 +by (cut_facts_tac [moving_down] 1);
   1.188 +by (ensures_tac defs "move_down" 1);
   1.189 +by (ALLGOALS distinct_tac);
   1.190 +by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
   1.191 +(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   1.192 +be (leI RS le_anti_sym RS sym) 1;
   1.193 +by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
   1.194 +by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
   1.195 +by (REPEAT_FIRST (etac rev_mp'));
   1.196 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
   1.197 +by (auto_tac
   1.198 +    (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)]
   1.199 +              addIs [diff_le_Suc_diff, diff_less_Suc_diff],
   1.200 +	      simpset() addsimps [trans_le_add1]));
   1.201 +qed "E_thm12b";
   1.202 +
   1.203 +
   1.204 +(*lift_4*)
   1.205 +Goal "0<N ==> LeadsTo Lprg (moving Int Req n Int (metric n -`` {N}) Int \
   1.206 +\                           {s. floor s ~: req s})     \
   1.207 +\                          (moving Int Req n Int (metric n -`` lessThan N))";
   1.208 +br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
   1.209 +by (etac E_thm12b 4);
   1.210 +by (etac E_thm12a 3);
   1.211 +by (rtac id_in_Acts 2);
   1.212 +by (Blast_tac 1);
   1.213 +qed "lift_4";
   1.214 +
   1.215 +
   1.216 +(** towards lift_5 **)
   1.217 +
   1.218 +(*lem_lift_5_3*)
   1.219 +Goal "0<N   \
   1.220 +\     ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingup) \
   1.221 +\                      (moving Int Req n Int (metric n -`` lessThan N))";
   1.222 +by (cut_facts_tac [bounded] 1);
   1.223 +by (ensures_tac defs "req_up" 1);
   1.224 +by (REPEAT_FIRST (etac rev_mp'));
   1.225 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
   1.226 +by (auto_tac (claset() addIs [diff_Suc_less_diff], 
   1.227 +	      simpset() addsimps [arith1, arith2]));
   1.228 +qed "E_thm16a";
   1.229 +
   1.230 +    (*arith1 comes from
   1.231 +     1. !!s i.
   1.232 +	   [| n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
   1.233 +	      i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
   1.234 +	      ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
   1.235 +	      Suc (floor s) < n; 0 < floor s - Min |]
   1.236 +	   ==> n - Suc (floor s) < floor s - Min + (n - Min)
   1.237 +    *)
   1.238 +
   1.239 +    (*arith2 comes from
   1.240 +     2. !!s i.
   1.241 +	   [| Min <= floor s; ...
   1.242 +	      n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
   1.243 +	      i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
   1.244 +	      ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
   1.245 +	      Suc (floor s) < n; Min < n |]
   1.246 +	   ==> n - Suc (floor s) < floor s - Min + (n - Min)
   1.247 +    *)
   1.248  
   1.249 -val [lift_3] = 
   1.250 -goal thy "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n) ==> LeadsTo Lprg (Req n) (opened Int atFloor n)";
   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 -
   1.391 -val rev_mp' = read_instantiate_sg (sign_of thy) 
   1.392 -                 [("P", "0 < metric ?n ?s")] rev_mp;
   1.393 -
   1.394 -
   1.395 -Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
   1.396 -\                  (moving Int Req n Int {s. metric n s < N})";
   1.397 -by (ensures_tac defs "req_up_act" 1);
   1.398 -by (REPEAT_FIRST (etac rev_mp'));
   1.399 -by (auto_tac (claset() addIs [diff_Suc_less_diff], 
   1.400 -	      simpset() addsimps [arith1, arith2, metric_def]));
   1.401 -qed "E_thm16a";
   1.402 -
   1.403 -
   1.404 -(*arith1 comes from
   1.405 - 1. !!s i.
   1.406 -       [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
   1.407 -          i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
   1.408 -          ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
   1.409 -          Suc (floor s) < n; 0 < floor s - min |]
   1.410 -       ==> n - Suc (floor s) < floor s - min + (n - min)
   1.411 -*)
   1.412 -
   1.413 -(*arith2 comes from
   1.414 - 2. !!s i.
   1.415 -       [| n : req s; stop s; ~ open s; move s; floor s < i; i <= max;
   1.416 -          i : req s; ALL i. i < floor s --> min <= i --> i ~: req s;
   1.417 -          ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
   1.418 -          Suc (floor s) < n; min < n |]
   1.419 -       ==> n - Suc (floor s) < floor s - min + (n - min)
   1.420 -*)
   1.421 -
   1.422 -
   1.423 -xxxxxxxxxxxxxxxx;
   1.424 -
   1.425 -Goal "j<=i ==> i - j < Suc i - j";
   1.426 -by (REPEAT (etac rev_mp 1));
   1.427 -by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   1.428 -by Auto_tac;
   1.429 -qed "diff_less_Suc_diff";
   1.430 -
   1.431 -
   1.432 -Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
   1.433 -\                  (moving Int Req n Int {s. metric n s < N})";
   1.434 -by (ensures_tac defs "req_down_act" 1);
   1.435 -be rev_mp 2;
   1.436 -be rev_mp 1;
   1.437 -by (dtac less_eq_Suc_add 2);
   1.438 -by (Clarify_tac 2);
   1.439 -by (Asm_full_simp_tac 2);
   1.440 -by (dtac less_eq_Suc_add 1);
   1.441 -by (Clarify_tac 1);
   1.442 -by (Asm_full_simp_tac 1);
   1.443 -
   1.444 -by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
   1.445 -by (REPEAT (Safe_step_tac 1));
   1.446 -by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
   1.447 -by (REPEAT (Safe_step_tac 1));
   1.448 -by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 1);
   1.449 -by (REPEAT (Safe_step_tac 1));
   1.450 -
   1.451 -
   1.452 -
   1.453 -
   1.454 -
   1.455 -
   1.456 -
   1.457 -Goal "[| i + k < n;  Suc (i + k) < n |] ==> i + k - m < Suc (i + k) - m";
   1.458 -by (REPEAT (etac rev_mp 1));
   1.459 -by (arith_oracle_tac 1);
   1.460 -
   1.461 -
   1.462 -by (asm_simp_tac (simpset() addsimps [metric_def]) 2);
   1.463 -by (REPEAT (Safe_step_tac 2));
   1.464 -by(Blast_tac 2);
   1.465 -by(Blast_tac 2);
   1.466 -by(Blast_tac 2);
   1.467 -by (REPEAT (Safe_step_tac 2));
   1.468 -by(Blast_tac 2);
   1.469 -by(blast_tac (claset() addEs [less_asym]) 2);
   1.470 -by (REPEAT (Safe_step_tac 2));
   1.471 -by(blast_tac (claset() addEs [less_asym]) 2);
   1.472 -by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
   1.473 -by (REPEAT (Safe_step_tac 2));
   1.474 -by(blast_tac (claset() addEs [less_asym, less_irrefl, less_SucE]) 2);
   1.475 -
   1.476 -
   1.477 -by (asm_simp_tac (simpset() addsimps [less_not_sym] setsubgoaler simp_tac) 1);
   1.478 -
   1.479 -
   1.480 -by (REPEAT (Safe_step_tac 2));
   1.481 -by (REPEAT (Safe_step_tac 2 THEN Blast_tac 2));
   1.482 -
   1.483 -by (auto_tac (claset() addIs [diff_Suc_less_diff], 
   1.484 -	      simpset() addsimps [metric_def]));
   1.485 -qed "E_thm16b";
   1.486 -
   1.487 -
   1.488 -
   1.489 -Goal "[|  m <= i; i < fl; ~ fl < n; fl - 1 < n |] ==> ~ n < fl - 1 --> n < fl --> fl - 1 - m + (n - m) < fl - n";
   1.490 -
   1.491 -
   1.492 -not_less_iff_le
   1.493 -
   1.494 -Goal "[|  ~ m < n; m - 1 < n |] ==> n = m";
   1.495 -by (cut_facts_tac [less_linear] 1);
   1.496 -by (blast_tac (claset() addSEs [less_irrefl]) 1);
   1.497 - by (REPEAT (etac rev_mp 1));
   1.498 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.499 -by (arith_oracle_tac 1);
   1.500 +Close_locale;
   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";