renamed le_0 to le_0_eq, to avoid confusion with le0,
authoroheimb
Fri May 31 19:34:40 1996 +0200 (1996-05-31)
changeset 177747c47b7d7aa8
parent 1776 d7e77cb8ce5c
child 1778 6c942cf3bf68
renamed le_0 to le_0_eq, to avoid confusion with le0,
supplied an experimental thm Suc_le_eq, but commented it out
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Nat.ML	Fri May 31 19:12:00 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Fri May 31 19:34:40 1996 +0200
     1.3 @@ -338,15 +338,6 @@
     1.4  qed "Suc_mono";
     1.5  
     1.6  
     1.7 -(*
     1.8 -goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)";
     1.9 -
    1.10 -
    1.11 -goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
    1.12 -by(stac less_Suc_eq 1);
    1.13 -by(rtac 
    1.14 -*)
    1.15 -
    1.16  goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
    1.17  by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
    1.18  qed "Suc_less_eq";
    1.19 @@ -411,14 +402,24 @@
    1.20  goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
    1.21  by (nat_ind_tac "i" 1);
    1.22  by (ALLGOALS Asm_simp_tac);
    1.23 -qed "le_0";
    1.24 +qed "le_0_eq";
    1.25  
    1.26  Addsimps [less_not_refl,
    1.27 -          (*less_Suc_eq,*) le0, le_0,
    1.28 +          (*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
    1.29            Suc_Suc_eq, Suc_n_not_le_n,
    1.30            n_not_Suc_n, Suc_n_not_n,
    1.31            nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
    1.32  
    1.33 +(*
    1.34 +goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)";
    1.35 +by(stac (less_Suc_eq RS sym) 1);
    1.36 +by(rtac Suc_less_eq 1);
    1.37 +qed "Suc_le_eq";
    1.38 +
    1.39 +this could make the simpset (with less_Suc_eq added again) more confluent,
    1.40 +but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...)
    1.41 +*)
    1.42 +
    1.43  (*Prevents simplification of f and g: much faster*)
    1.44  qed_goal "nat_case_weak_cong" Nat.thy
    1.45    "m=n ==> nat_case a f m = nat_case a f n"