1.1 --- a/src/HOL/UNITY/Simple/Lift.ML	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/UNITY/Simple/Lift.ML	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -142,7 +142,7 @@
     1.4  
     1.5  
     1.6  (*lem_lift_4_1 *)
     1.7 -Goal "Numeral0 < N ==> \
     1.8 +Goal "0 < N ==> \
     1.9  \     Lift : (moving Int Req n Int {s. metric n s = N} Int \
    1.10  \             {s. floor s ~: req s} Int {s. up s})   \
    1.11  \            LeadsTo \
    1.12 @@ -157,7 +157,7 @@
    1.13  
    1.14  
    1.15  (*lem_lift_4_3 *)
    1.16 -Goal "Numeral0 < N ==> \
    1.17 +Goal "0 < N ==> \
    1.18  \     Lift : (moving Int Req n Int {s. metric n s = N} Int \
    1.19  \             {s. floor s ~: req s} - {s. up s})   \
    1.20  \            LeadsTo (moving Int Req n Int {s. metric n s < N})";
    1.21 @@ -170,7 +170,7 @@
    1.22  qed "E_thm12b";
    1.23  
    1.24  (*lift_4*)
    1.25 -Goal "Numeral0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \
    1.26 +Goal "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \
    1.27  \                           {s. floor s ~: req s}) LeadsTo     \
    1.28  \                          (moving Int Req n Int {s. metric n s < N})";
    1.29  by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un] 
    1.30 @@ -182,7 +182,7 @@
    1.31  (** towards lift_5 **)
    1.32  
    1.33  (*lem_lift_5_3*)
    1.34 -Goal "Numeral0<N   \
    1.35 +Goal "0<N   \
    1.36  \ ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \
    1.37  \            (moving Int Req n Int {s. metric n s < N})";
    1.38  by (cut_facts_tac [bounded] 1);
    1.39 @@ -192,7 +192,7 @@
    1.40  
    1.41  
    1.42  (*lem_lift_5_1 has ~goingup instead of goingdown*)
    1.43 -Goal "Numeral0<N ==>   \
    1.44 +Goal "0<N ==>   \
    1.45  \     Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
    1.46  \                  (moving Int Req n Int {s. metric n s < N})";
    1.47  by (cut_facts_tac [bounded] 1);
    1.48 @@ -203,14 +203,14 @@
    1.49  
    1.50  (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
    1.51    i.e. the trivial disjunction, leading to an asymmetrical proof.*)
    1.52 -Goal "Numeral0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
    1.53 +Goal "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
    1.54  by (Clarify_tac 1);
    1.55  by (auto_tac (claset(), metric_ss));
    1.56  qed "E_thm16c";
    1.57  
    1.58  
    1.59  (*lift_5*)
    1.60 -Goal "Numeral0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo   \
    1.61 +Goal "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo   \
    1.62  \                          (moving Int Req n Int {s. metric n s < N})";
    1.63  by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un] 
    1.64  	  MRS LeadsTo_Trans) 1);
    1.65 @@ -222,7 +222,7 @@
    1.66  (** towards lift_3 **)
    1.67  
    1.68  (*lemma used to prove lem_lift_3_1*)
    1.69 -Goal "[| metric n s = Numeral0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
    1.70 +Goal "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
    1.71  by (auto_tac (claset(), metric_ss));
    1.72  qed "metric_eq_0D";
    1.73  
    1.74 @@ -230,7 +230,7 @@
    1.75  
    1.76  
    1.77  (*lem_lift_3_1*)
    1.78 -Goal "Lift : (moving Int Req n Int {s. metric n s = Numeral0}) LeadsTo   \
    1.79 +Goal "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo   \
    1.80  \                  (stopped Int atFloor n)";
    1.81  by (cut_facts_tac [bounded] 1);
    1.82  by (ensures_tac "request_act" 1);
    1.83 @@ -246,7 +246,7 @@
    1.84  qed "E_thm13";
    1.85  
    1.86  (*lem_lift_3_6*)
    1.87 -Goal "Numeral0 < N ==> \
    1.88 +Goal "0 < N ==> \
    1.89  \     Lift : \
    1.90  \       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
    1.91  \       LeadsTo (opened Int Req n Int {s. metric n s = N})";
    1.92 @@ -264,7 +264,7 @@
    1.93  
    1.94  (** the final steps **)
    1.95  
    1.96 -Goal "Numeral0 < N ==> \
    1.97 +Goal "0 < N ==> \
    1.98  \     Lift : \
    1.99  \       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
   1.100  \       LeadsTo (moving Int Req n Int {s. metric n s < N})";
   1.101 @@ -274,7 +274,7 @@
   1.102  
   1.103  
   1.104  (*Now we observe that our integer metric is really a natural number*)
   1.105 -Goal "Lift : Always {s. Numeral0 <= metric n s}";
   1.106 +Goal "Lift : Always {s. 0 <= metric n s}";
   1.107  by (rtac (bounded RS Always_weaken) 1);
   1.108  by (auto_tac (claset(), metric_ss));
   1.109  qed "Always_nonneg";
   1.110 @@ -283,8 +283,8 @@
   1.111  
   1.112  Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
   1.113  by (rtac (Always_nonneg RS integ_0_le_induct) 1);
   1.114 -by (case_tac "Numeral0 < z" 1);
   1.115 -(*If z <= Numeral0 then actually z = Numeral0*)
   1.116 +by (case_tac "0 < z" 1);
   1.117 +(*If z <= 0 then actually z = 0*)
   1.118  by (force_tac (claset() addIs [R_thm11, order_antisym], 
   1.119  	       simpset() addsimps [linorder_not_less]) 2);
   1.120  by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);