Now uses integers instead of naturals
authorpaulson
Fri Sep 25 13:58:24 1998 +0200 (1998-09-25)
changeset 5563228b92552d1f
parent 5562 02261e6880d1
child 5564 f16de69b7c0c
Now uses integers instead of naturals
src/HOL/UNITY/Lift.ML
src/HOL/UNITY/Lift.thy
     1.1 --- a/src/HOL/UNITY/Lift.ML	Fri Sep 25 13:57:01 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Lift.ML	Fri Sep 25 13:58:24 1998 +0200
     1.3 @@ -7,9 +7,25 @@
     1.4  *)
     1.5  
     1.6  
     1.7 +Goal "~ z < w ==> (z < w + #1) = (z = w)";
     1.8 +by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1);
     1.9 +qed "not_zless_zless1_eq";
    1.10 +
    1.11 +
    1.12  (*split_all_tac causes a big blow-up*)
    1.13  claset_ref() := claset() delSWrapper "split_all_tac";
    1.14  
    1.15 +Delsimps [split_paired_All];
    1.16 +
    1.17 +Goal "[| x ~: A;  y : A |] ==> x ~= y";
    1.18 +by (Blast_tac 1);
    1.19 +qed "not_mem_distinct";
    1.20 +
    1.21 +fun distinct_tac i =
    1.22 +    dtac zle_neq_implies_zless i THEN
    1.23 +    eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN
    1.24 +    assume_tac i;
    1.25 +
    1.26  
    1.27  (** Rules to move "metric n s" out of the assumptions, for case splitting **)
    1.28  val mov_metric1 = read_instantiate_sg (sign_of thy) 
    1.29 @@ -21,12 +37,24 @@
    1.30  val mov_metric3 = read_instantiate_sg (sign_of thy) 
    1.31                   [("P", "~ (?x < metric ?n ?s)")] rev_mp;
    1.32  
    1.33 +val mov_metric4 = read_instantiate_sg (sign_of thy) 
    1.34 +                 [("P", "(?x <= metric ?n ?s)")] rev_mp;
    1.35 +
    1.36  (*The order in which they are applied seems to be critical...*)
    1.37 -val mov_metrics = [mov_metric2, mov_metric3, mov_metric1];
    1.38 +val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
    1.39  
    1.40  
    1.41 -val Suc_lessD_contra = Suc_lessD COMP rev_contrapos;
    1.42 -val Suc_lessD_contra' = less_not_sym RS Suc_lessD_contra;
    1.43 +val zless_zadd1_contra = zless_zadd1_imp_zless COMP rev_contrapos;
    1.44 +val zless_zadd1_contra' = zless_not_sym RS zless_zadd1_contra;
    1.45 +
    1.46 +
    1.47 +val metric_simps =
    1.48 +    [metric_def, vimage_def, order_less_imp_not_less, order_less_imp_triv, 
    1.49 +     order_less_imp_not_eq, order_less_imp_not_eq2,
    1.50 +     not_zless_zless1_eq, zless_not_sym RS not_zless_zless1_eq,
    1.51 +     zless_zadd1_contra, zless_zadd1_contra',
    1.52 +     zless_not_refl2, zless_not_refl3];
    1.53 +
    1.54  
    1.55  Addsimps [Lprg_def RS def_prg_simps];
    1.56  
    1.57 @@ -51,26 +79,9 @@
    1.58  (* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
    1.59  
    1.60  
    1.61 -val metric_simps =
    1.62 -    [metric_def, vimage_def, 
    1.63 -     not_less_less_Suc_eq, less_not_sym RS not_less_less_Suc_eq,
    1.64 -     Suc_lessD_contra, Suc_lessD_contra',
    1.65 -     less_not_refl2, less_not_refl3];
    1.66 -
    1.67 -
    1.68 -(*Hoping to be faster than
    1.69 -    asm_simp_tac (simpset() addsimps metric_simps
    1.70 -  but sometimes it's slower*)
    1.71 -val metric_simp_tac = 
    1.72 -    asm_simp_tac (simpset() addsimps [metric_def, vimage_def]) THEN'
    1.73 -    asm_simp_tac (simpset() addsimps metric_simps);
    1.74 -
    1.75 -
    1.76  (*Simplification for records*)
    1.77  Addsimps (thms"state.update_defs");
    1.78  
    1.79 -Addsimps [Suc_le_eq];
    1.80 -
    1.81  Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
    1.82  	  moving_up_def, moving_down_def];
    1.83  
    1.84 @@ -83,10 +94,6 @@
    1.85  val nat_exhaust_pred_le = 
    1.86      read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
    1.87  
    1.88 -Goal "m < n ==> m <= n-1";
    1.89 -by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
    1.90 -qed "less_imp_le_pred";
    1.91 -
    1.92  Goal "Invariant Lprg open_stop";
    1.93  by (rtac InvariantI 1);
    1.94  by (Force_tac 1);
    1.95 @@ -111,17 +118,14 @@
    1.96  by (rtac InvariantI 1);
    1.97  by (Force_tac 1);
    1.98  by (constrains_tac 1);
    1.99 -by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
   1.100 +by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
   1.101  qed "moving_up";
   1.102  
   1.103  Goal "Invariant Lprg moving_down";
   1.104  by (rtac InvariantI 1);
   1.105  by (Force_tac 1);
   1.106  by (constrains_tac 1);
   1.107 -by Safe_tac;
   1.108 -by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
   1.109 -by (auto_tac (claset(),
   1.110 -	      simpset() addsimps [gr_implies_gr0 RS le_pred_eq]));
   1.111 +by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
   1.112  qed "moving_down";
   1.113  
   1.114  Goal "Invariant Lprg bounded";
   1.115 @@ -129,10 +133,13 @@
   1.116  by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
   1.117  by (Force_tac 1);
   1.118  by (constrains_tac 1);
   1.119 -by Safe_tac;
   1.120 -by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le]));
   1.121 -by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
   1.122 -by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]));
   1.123 +by (ALLGOALS Clarify_tac);
   1.124 +by (REPEAT_FIRST distinct_tac);
   1.125 +by (ALLGOALS 
   1.126 +    (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]@zcompare_rls)));
   1.127 +by (ALLGOALS 
   1.128 +    (blast_tac (claset() addDs [zle_imp_zless_or_eq] 
   1.129 +                         addIs [zless_trans])));
   1.130  qed "bounded";
   1.131  
   1.132  
   1.133 @@ -181,11 +188,11 @@
   1.134  
   1.135  AddIffs [Min_le_n, n_le_Max];
   1.136  
   1.137 -val le_MinD = Min_le_n RS le_anti_sym;
   1.138 -val Max_leD = n_le_Max RSN (2,le_anti_sym);
   1.139 +val le_MinD = Min_le_n RS zle_anti_sym;
   1.140 +val Max_leD = n_le_Max RSN (2,zle_anti_sym);
   1.141  
   1.142 -AddSDs [le_MinD, leI RS le_MinD,
   1.143 -	Max_leD, leI RS Max_leD];
   1.144 +AddSDs [le_MinD, zleI RS le_MinD,
   1.145 +	Max_leD, zleI RS Max_leD];
   1.146  
   1.147  (*lem_lift_2_0 
   1.148    NOT an ensures property, but a mere inclusion;
   1.149 @@ -194,7 +201,7 @@
   1.150  \                  ((closed Int goingup Int Req n)  Un \
   1.151  \                   (closed Int goingdown Int Req n))";
   1.152  by (rtac subset_imp_LeadsTo 1);
   1.153 -by (auto_tac (claset() addSEs [nat_neqE], simpset()));
   1.154 +by (auto_tac (claset() addSEs [int_neqE], simpset()));
   1.155  qed "E_thm05c";
   1.156  
   1.157  (*lift_2*)
   1.158 @@ -208,68 +215,52 @@
   1.159  
   1.160  
   1.161  (** Towards lift_4 ***)
   1.162 -
   1.163 -Goal "[| x ~: A;  y : A |] ==> x ~= y";
   1.164 -by (Blast_tac 1);
   1.165 -qed "not_mem_distinct";
   1.166 -
   1.167 -fun distinct_tac i =
   1.168 -    dtac le_neq_implies_less i THEN
   1.169 -    eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN
   1.170 -    assume_tac i;
   1.171 -
   1.172 + 
   1.173  
   1.174  (*lem_lift_4_1 *)
   1.175 -Goal "0 < N ==> \
   1.176 +Goal "#0 < N ==> \
   1.177  \     LeadsTo Lprg \
   1.178 -\       (moving Int Req n Int (metric n -`` {N}) Int \
   1.179 +\       (moving Int Req n Int {s. metric n s = N} Int \
   1.180  \         {s. floor s ~: req s} Int {s. up s})   \
   1.181 -\       (moving Int Req n Int (metric n -`` lessThan N))";
   1.182 +\       (moving Int Req n Int {s. metric n s < N})";
   1.183  by (cut_facts_tac [moving_up] 1);
   1.184  by (ensures_tac "move_up" 1);
   1.185  by Safe_tac;
   1.186  (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   1.187 -by (etac (leI RS le_anti_sym RS sym) 1);
   1.188 +by (etac (zleI RS zle_anti_sym RS sym) 1);
   1.189  by (REPEAT_FIRST (eresolve_tac mov_metrics));
   1.190  by (REPEAT_FIRST distinct_tac);
   1.191 -by (ALLGOALS metric_simp_tac);
   1.192 -by (auto_tac
   1.193 -    (claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)]
   1.194 -	      addIs [diff_Suc_less_diff], 
   1.195 -     simpset()));
   1.196 +(** LEVEL 6 **)
   1.197 +by (ALLGOALS
   1.198 +   (asm_simp_tac (simpset() addsimps [zle_def]@ metric_simps @ zcompare_rls)));
   1.199  qed "E_thm12a";
   1.200  
   1.201  
   1.202 -(*This rule helps eliminate occurrences of  (floor s - 1) *)
   1.203 -val less_floor_imp = read_instantiate_sg (sign_of thy) 
   1.204 -                 [("n", "floor ?s")] less_eq_Suc_add RS exE;
   1.205  
   1.206  (*lem_lift_4_3 *)
   1.207 -Goal "0 < N ==> \
   1.208 +Goal "#0 < N ==> \
   1.209  \     LeadsTo Lprg \
   1.210 -\       (moving Int Req n Int (metric n -`` {N}) Int \
   1.211 +\       (moving Int Req n Int {s. metric n s = N} Int \
   1.212  \        {s. floor s ~: req s} - {s. up s})   \
   1.213 -\       (moving Int Req n Int (metric n -`` lessThan N))";
   1.214 +\       (moving Int Req n Int {s. metric n s < N})";
   1.215  by (cut_facts_tac [moving_down] 1);
   1.216  by (ensures_tac "move_down" 1);
   1.217  by Safe_tac;
   1.218 -by (ALLGOALS distinct_tac);
   1.219 -by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
   1.220  (*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
   1.221 -by (etac (leI RS le_anti_sym RS sym) 1);
   1.222 +by (etac (zleI RS zle_anti_sym RS sym) 1);
   1.223  by (REPEAT_FIRST (eresolve_tac mov_metrics));
   1.224 -by (ALLGOALS metric_simp_tac);
   1.225 -by (auto_tac
   1.226 -    (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)]
   1.227 -              addIs [diff_le_Suc_diff, diff_less_Suc_diff],
   1.228 -	      simpset() addsimps [trans_le_add1]));
   1.229 +by (REPEAT_FIRST distinct_tac);
   1.230 +(** LEVEL 6 **)
   1.231 +by (ALLGOALS
   1.232 +   (asm_simp_tac (simpset() addsimps [zle_def] @
   1.233 +				       metric_simps @ zcompare_rls)));
   1.234 +by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls)));
   1.235  qed "E_thm12b";
   1.236  
   1.237 -
   1.238  (*lift_4*)
   1.239 -Goal "0<N ==> LeadsTo Lprg (moving Int Req n Int (metric n -`` {N}) Int \
   1.240 +Goal "#0<N ==> LeadsTo Lprg (moving Int Req n Int {s. metric n s = N} Int \
   1.241  \                           {s. floor s ~: req s})     \
   1.242 -\                          (moving Int Req n Int (metric n -`` lessThan N))";
   1.243 +\                          (moving Int Req n Int {s. metric n s < N})";
   1.244  by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
   1.245  by (etac E_thm12b 4);
   1.246  by (etac E_thm12a 3);
   1.247 @@ -281,87 +272,54 @@
   1.248  (** towards lift_5 **)
   1.249  
   1.250  (*lem_lift_5_3*)
   1.251 -Goal "0<N   \
   1.252 -\     ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingup) \
   1.253 -\                      (moving Int Req n Int (metric n -`` lessThan N))";
   1.254 +Goal "#0<N   \
   1.255 +\     ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
   1.256 +\                      (moving Int Req n Int {s. metric n s < N})";
   1.257  by (cut_facts_tac [bounded] 1);
   1.258  by (ensures_tac "req_up" 1);
   1.259  by Auto_tac;
   1.260  by (REPEAT_FIRST (eresolve_tac mov_metrics));
   1.261 -by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
   1.262 -     (*faster than metric_simp_tac or than using just metric_def*)
   1.263 -by (auto_tac (claset() addIs [diff_Suc_less_diff], 
   1.264 -	      simpset() addsimps [arith1, arith2]));
   1.265 +by (ALLGOALS
   1.266 +    (asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
   1.267 +(** LEVEL 5 **)
   1.268 +by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
   1.269 +by Auto_tac;
   1.270 +by (asm_simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls) 1);
   1.271 +by (full_simp_tac (no_neg_ss addsimps [add_nat, integ_of_Min]) 1);
   1.272  qed "E_thm16a";
   1.273  
   1.274 -    (*arith1 comes from
   1.275 -     1. !!s i.
   1.276 -	   [| n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
   1.277 -	      i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
   1.278 -	      ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
   1.279 -	      Suc (floor s) < n; 0 < floor s - Min |]
   1.280 -	   ==> n - Suc (floor s) < floor s - Min + (n - Min)
   1.281 -    *)
   1.282 -
   1.283 -    (*arith2 comes from
   1.284 -     2. !!s i.
   1.285 -	   [| Min <= floor s; ...
   1.286 -	      n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
   1.287 -	      i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
   1.288 -	      ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
   1.289 -	      Suc (floor s) < n; Min < n |]
   1.290 -	   ==> n - Suc (floor s) < floor s - Min + (n - Min)
   1.291 -    *)
   1.292 -
   1.293  (*lem_lift_5_1 has ~goingup instead of goingdown*)
   1.294 -Goal "0<N ==>   \
   1.295 -\     LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingdown) \
   1.296 -\                  (moving Int Req n Int (metric n -`` lessThan N))";
   1.297 +Goal "#0<N ==>   \
   1.298 +\     LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
   1.299 +\                  (moving Int Req n Int {s. metric n s < N})";
   1.300  by (cut_facts_tac [bounded] 1);
   1.301  by (ensures_tac "req_down" 1);
   1.302  by Auto_tac;
   1.303 -by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
   1.304  by (REPEAT_FIRST (eresolve_tac mov_metrics));
   1.305 -by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
   1.306 -     (*faster and better than metric_simp_tac *)
   1.307 -by (auto_tac (claset() addIs [diff_Suc_less_diff, diff_less_Suc_diff], 
   1.308 -	      simpset() addsimps [trans_le_add1, arith3, arith4]));
   1.309 +by (ALLGOALS
   1.310 +    (asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
   1.311 +(** LEVEL 5 **)
   1.312 +by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 2);
   1.313 +by (etac exE 2);  
   1.314 +by (etac ssubst 2);
   1.315 +by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls)));
   1.316 +by (auto_tac (claset(), no_neg_ss addsimps [add_nat, integ_of_Min]));
   1.317  qed "E_thm16b";
   1.318  
   1.319 -    (*arith3 comes from
   1.320 -     1. !!s i x.
   1.321 -	   [| floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max;
   1.322 -	      ~ open s; n : req s; move s; Min <= i; i : req s;
   1.323 -	      ALL ia. ia <= Max --> Suc (i + x) < ia --> ia ~: req s;
   1.324 -	      ~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x;
   1.325 -	      Suc (i + x) < Max |]
   1.326 -	   ==> i + x - n < Max - Suc (i + x) + (Max - n)
   1.327 -    *)
   1.328 -
   1.329 -    (*arith4 comes from
   1.330 -     2. !!s i x.
   1.331 -	   [| floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max;
   1.332 -	      ~ open s; n : req s; move s; Min <= i; i : req s;
   1.333 -	      ALL ia. ia <= Max --> Suc (i + x) < ia --> ia ~: req s;
   1.334 -	      ~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x;
   1.335 -	      n < Max |]
   1.336 -	   ==> i + x - n < Max - Suc (i + x) + (Max - n)
   1.337 -    *)
   1.338 -
   1.339  
   1.340  
   1.341  (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
   1.342    i.e. the trivial disjunction, leading to an asymmetrical proof.*)
   1.343 -Goal "0<N ==> Req n Int (metric n -``{N}) <= goingup Un goingdown";
   1.344 -by (asm_simp_tac
   1.345 -    (simpset() addsimps (always_defs@abbrev_defs@[metric_def,vimage_def])) 1);
   1.346 -by (auto_tac (claset(), simpset() addsimps metric_simps));
   1.347 +Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
   1.348 +by (asm_simp_tac (simpset() addsimps metric_simps) 1);
   1.349 +by (auto_tac (claset() delrules [impCE] addEs [impCE], 
   1.350 +	      simpset() addsimps conj_comms));
   1.351  qed "E_thm16c";
   1.352  
   1.353  
   1.354  (*lift_5*)
   1.355 -Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}))   \
   1.356 -\                          (moving Int Req n Int (metric n -`` lessThan N))";
   1.357 +Goal "#0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N})   \
   1.358 +\                          (moving Int Req n Int {s. metric n s < N})";
   1.359  by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
   1.360  by (etac E_thm16b 4);
   1.361  by (etac E_thm16a 3);
   1.362 @@ -374,18 +332,27 @@
   1.363  (** towards lift_3 **)
   1.364  
   1.365  (*lemma used to prove lem_lift_3_1*)
   1.366 -Goal "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
   1.367 +Goal "[| metric n s = #0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
   1.368  by (etac rev_mp 1);
   1.369 -  (*MUCH faster than metric_simps*)
   1.370 -by (asm_simp_tac (simpset() addsimps [metric_def]) 1);
   1.371 -by (auto_tac (claset(), simpset() addsimps metric_simps));
   1.372 +(*force simplification of "metric..." while in conclusion part*)
   1.373 +by (asm_simp_tac (simpset() addsimps metric_simps) 1);
   1.374 +by (auto_tac (claset() addIs [zleI, zle_anti_sym], 
   1.375 +	      simpset() addsimps zcompare_rls@[add_nat, integ_of_Min]));
   1.376 +(*trans_tac (or decision procedures) could do the rest*)
   1.377 +by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 2);
   1.378 +by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
   1.379 +by (ALLGOALS (clarify_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1])));
   1.380 +by (REPEAT_FIRST (eres_inst_tac [("P", "?x+?y = ?z")] rev_mp));
   1.381 +by (REPEAT_FIRST (etac ssubst));
   1.382 +by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls)));
   1.383 +by (auto_tac (claset(), no_neg_ss addsimps [add_nat]));
   1.384  qed "metric_eq_0D";
   1.385  
   1.386  AddDs [metric_eq_0D];
   1.387  
   1.388  
   1.389  (*lem_lift_3_1*)
   1.390 -Goal "LeadsTo Lprg (moving Int Req n Int (metric n -`` {0}))   \
   1.391 +Goal "LeadsTo Lprg (moving Int Req n Int {s. metric n s = #0})   \
   1.392  \                  (stopped Int atFloor n)";
   1.393  by (cut_facts_tac [bounded] 1);
   1.394  by (ensures_tac "request_act" 1);
   1.395 @@ -394,17 +361,17 @@
   1.396  
   1.397  (*lem_lift_3_5*)
   1.398  Goal "LeadsTo Lprg \
   1.399 -\       (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})   \
   1.400 -\       (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})";
   1.401 +\       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
   1.402 +\       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
   1.403  by (ensures_tac "request_act" 1);
   1.404  by (auto_tac (claset(), simpset() addsimps metric_simps));
   1.405  qed "E_thm13";
   1.406  
   1.407  (*lem_lift_3_6*)
   1.408 -Goal "0 < N ==> \
   1.409 +Goal "#0 < N ==> \
   1.410  \     LeadsTo Lprg \
   1.411 -\       (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
   1.412 -\       (opened Int Req n Int (metric n -`` {N}))";
   1.413 +\       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
   1.414 +\       (opened Int Req n Int {s. metric n s = N})";
   1.415  by (ensures_tac "open_act" 1);
   1.416  by (REPEAT_FIRST (eresolve_tac mov_metrics));
   1.417  by (auto_tac (claset(), simpset() addsimps metric_simps));
   1.418 @@ -412,8 +379,8 @@
   1.419  
   1.420  (*lem_lift_3_7*)
   1.421  Goal "LeadsTo Lprg \
   1.422 -\       (opened Int Req n Int (metric n -`` {N}))  \
   1.423 -\       (closed Int Req n Int (metric n -`` {N}))";
   1.424 +\       (opened Int Req n Int {s. metric n s = N})  \
   1.425 +\       (closed Int Req n Int {s. metric n s = N})";
   1.426  by (ensures_tac "close_act" 1);
   1.427  by (auto_tac (claset(), simpset() addsimps metric_simps));
   1.428  qed "E_thm15";
   1.429 @@ -421,20 +388,37 @@
   1.430  
   1.431  (** the final steps **)
   1.432  
   1.433 -Goal "0 < N ==> \
   1.434 +Goal "#0 < N ==> \
   1.435  \     LeadsTo Lprg \
   1.436 -\       (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})   \
   1.437 -\       (moving Int Req n Int (metric n -`` lessThan N))";
   1.438 +\       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
   1.439 +\       (moving Int Req n Int {s. metric n s < N})";
   1.440  by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
   1.441  	                addIs [LeadsTo_Trans]) 1);
   1.442  qed "lift_3_Req";
   1.443  
   1.444  
   1.445 +
   1.446 +(*Now we observe that our integer metric is really a natural number*)
   1.447 +Goal "reachable Lprg <= {s. #0 <= metric n s}";
   1.448 +by (rtac (bounded RS Invariant_includes_reachable RS subset_trans) 1);
   1.449 +by (simp_tac (simpset() addsimps metric_simps @ zcompare_rls) 1);
   1.450 +by (auto_tac (claset(),
   1.451 +	      simpset() addsimps [zless_iff_Suc_zadd, zle_iff_zadd]));
   1.452 +by (REPEAT_FIRST (etac ssubst));
   1.453 +by (auto_tac (claset(),
   1.454 +	      simpset() addsimps zadd_ac@zcompare_0_rls));
   1.455 +by (auto_tac (claset(),
   1.456 +	      no_neg_ss addsimps [add_nat]));
   1.457 +qed "reach_nonneg";
   1.458 +
   1.459 +val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
   1.460 +
   1.461  Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
   1.462 -by (rtac (allI RS LessThan_induct) 1);
   1.463 -by (exhaust_tac "m" 1);
   1.464 -by Auto_tac;
   1.465 -by (rtac E_thm11 1);
   1.466 +by (rtac (reach_nonneg RS integ_0_le_induct) 1);
   1.467 +by (case_tac "#0 < z" 1);
   1.468 +(*If z <= #0 then actually z = #0*)
   1.469 +by (fold_tac [zle_def]);
   1.470 +by (force_tac (claset() addIs [R_thm11, zle_anti_sym], simpset()) 2);
   1.471  by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
   1.472  by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
   1.473  by (rtac lift_3_Req 4);
     2.1 --- a/src/HOL/UNITY/Lift.thy	Fri Sep 25 13:57:01 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Lift.thy	Fri Sep 25 13:58:24 1998 +0200
     2.3 @@ -9,25 +9,19 @@
     2.4  Lift = SubstAx +
     2.5  
     2.6  record state =
     2.7 -  floor :: nat		(*current position of the lift*)
     2.8 +  floor :: int		(*current position of the lift*)
     2.9    open  :: bool		(*whether the door is open at floor*)
    2.10    stop  :: bool		(*whether the lift is stopped at floor*)
    2.11 -  req   :: nat set	(*for each floor, whether the lift is requested*)
    2.12 +  req   :: int set	(*for each floor, whether the lift is requested*)
    2.13    up    :: bool		(*current direction of movement*)
    2.14    move  :: bool		(*whether moving takes precedence over opening*)
    2.15  
    2.16  consts
    2.17 -  Min, Max :: nat       (*least and greatest floors*)
    2.18 +  Min, Max :: int       (*least and greatest floors*)
    2.19  
    2.20  rules
    2.21    Min_le_Max  "Min <= Max"
    2.22    
    2.23 -  (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
    2.24 -  arith1      "m < fl ==> n - Suc fl < fl - m + (n - m)"
    2.25 -  arith2      "[| m<n;  m <= fl |] ==> n - Suc fl < fl - m + (n - m)"
    2.26 -  arith3      "[| Suc ix < m |] ==> ix - n < m - Suc ix + (m - n)"
    2.27 -  arith4      "[| ix < m;  n < ix |] ==> ix - n < m - Suc (ix) + (m - n)"
    2.28 -
    2.29  constdefs
    2.30    
    2.31    (** Abbreviations: the "always" part **)
    2.32 @@ -65,10 +59,10 @@
    2.33    closed :: state set  (*but this is the same as ready!!*)
    2.34      "closed ==  {s. stop s  & ~ open s &  move s}"
    2.35  
    2.36 -  atFloor :: nat => state set
    2.37 +  atFloor :: int => state set
    2.38      "atFloor n ==  {s. floor s = n}"
    2.39  
    2.40 -  Req :: nat => state set
    2.41 +  Req :: int => state set
    2.42      "Req n ==  {s. n : req s}"
    2.43  
    2.44  
    2.45 @@ -93,25 +87,25 @@
    2.46    req_up :: "(state*state) set"
    2.47      "req_up ==
    2.48           {(s,s'). s' = s (|stop  :=False,
    2.49 -			   floor := Suc (floor s),
    2.50 +			   floor := floor s + #1,
    2.51  			   up    := True|)
    2.52  		       & s : (ready Int goingup)}"
    2.53  
    2.54    req_down :: "(state*state) set"
    2.55      "req_down ==
    2.56           {(s,s'). s' = s (|stop  :=False,
    2.57 -			   floor := floor s - 1,
    2.58 +			   floor := floor s - #1,
    2.59  			   up    := False|)
    2.60  		       & s : (ready Int goingdown)}"
    2.61  
    2.62    move_up :: "(state*state) set"
    2.63      "move_up ==
    2.64 -         {(s,s'). s' = s (|floor := Suc (floor s)|)
    2.65 +         {(s,s'). s' = s (|floor := floor s + #1|)
    2.66  		       & ~ stop s & up s & floor s ~: req s}"
    2.67  
    2.68    move_down :: "(state*state) set"
    2.69      "move_down ==
    2.70 -         {(s,s'). s' = s (|floor := floor s - 1|)
    2.71 +         {(s,s'). s' = s (|floor := floor s - #1|)
    2.72  		       & ~ stop s & ~ up s & floor s ~: req s}"
    2.73  
    2.74    button_press  :: "(state*state) set"
    2.75 @@ -150,17 +144,18 @@
    2.76      "moving_down == {s. ~ stop s & ~ up s -->
    2.77                       (EX f. Min <= f & f <= floor s & f : req s)}"
    2.78    
    2.79 -  metric :: [nat,state] => nat
    2.80 +  metric :: [int,state] => int
    2.81      "metric ==
    2.82 -       %n s. if up s & floor s < n then n - floor s
    2.83 -	     else if ~ up s & n < floor s then floor s - n
    2.84 -	     else if up s & n < floor s then (Max - floor s) + (Max-n)
    2.85 -	     else if ~ up s & floor s < n then (floor s - Min) + (n-Min)
    2.86 -	     else 0"
    2.87 +       %n s. if floor s < n then (if up s then n - floor s
    2.88 +			          else (floor s - Min) + (n-Min))
    2.89 +             else
    2.90 +             if n < floor s then (if up s then (Max - floor s) + (Max-n)
    2.91 +		                  else floor s - n)
    2.92 +             else #0"
    2.93  
    2.94  locale floor =
    2.95    fixes 
    2.96 -    n	:: nat
    2.97 +    n	:: int
    2.98    assumes
    2.99      Min_le_n    "Min <= n"
   2.100      n_le_Max    "n <= Max"