src/HOL/Nat.ML
changeset 1301 42782316d510
parent 1264 3eb91524b938
child 1327 6c29cfab679c
     1.1 --- a/src/HOL/Nat.ML	Wed Oct 25 09:46:46 1995 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Oct 25 09:48:29 1995 +0100
     1.3 @@ -97,6 +97,8 @@
     1.4  
     1.5  bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym));
     1.6  
     1.7 +Addsimps [Suc_not_Zero,Zero_not_Suc];
     1.8 +
     1.9  bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
    1.10  val Zero_neq_Suc = sym RS Suc_neq_Zero;
    1.11  
    1.12 @@ -118,7 +120,7 @@
    1.13  
    1.14  goal Nat.thy "n ~= Suc(n)";
    1.15  by (nat_ind_tac "n" 1);
    1.16 -by (ALLGOALS(asm_simp_tac (!simpset addsimps [Zero_not_Suc,Suc_Suc_eq])));
    1.17 +by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq])));
    1.18  qed "n_not_Suc_n";
    1.19  
    1.20  val Suc_n_not_n = n_not_Suc_n RS not_sym;
    1.21 @@ -203,6 +205,7 @@
    1.22  goalw Nat.thy [less_def] "n < Suc(n)";
    1.23  by (rtac (pred_natI RS r_into_trancl) 1);
    1.24  qed "lessI";
    1.25 +Addsimps [lessI];
    1.26  
    1.27  (* i(j ==> i(Suc(j) *)
    1.28  val less_SucI = lessI RSN (2, less_trans);
    1.29 @@ -213,6 +216,7 @@
    1.30  by (etac less_trans 1);
    1.31  by (rtac lessI 1);
    1.32  qed "zero_less_Suc";
    1.33 +Addsimps [zero_less_Suc];
    1.34  
    1.35  (** Elimination properties **)
    1.36  
    1.37 @@ -251,6 +255,7 @@
    1.38  by (etac Zero_neq_Suc 1);
    1.39  by (etac Zero_neq_Suc 1);
    1.40  qed "not_less0";
    1.41 +Addsimps [not_less0];
    1.42  
    1.43  (* n<0 ==> R *)
    1.44  bind_thm ("less_zeroE", (not_less0 RS notE));
    1.45 @@ -269,6 +274,12 @@
    1.46  		     addEs  [less_trans, less_SucE]) 1);
    1.47  qed "less_Suc_eq";
    1.48  
    1.49 +val prems = goal Nat.thy "m<n ==> n ~= 0";
    1.50 +by(res_inst_tac [("n","n")] natE 1);
    1.51 +by(cut_facts_tac prems 1);
    1.52 +by(ALLGOALS Asm_full_simp_tac);
    1.53 +qed "gr_implies_not0";
    1.54 +Addsimps [gr_implies_not0];
    1.55  
    1.56  (** Inductive (?) properties **)
    1.57  
    1.58 @@ -311,10 +322,18 @@
    1.59  goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
    1.60  by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
    1.61  qed "Suc_less_eq";
    1.62 +Addsimps [Suc_less_eq];
    1.63  
    1.64  goal Nat.thy "~(Suc(n) < n)";
    1.65  by(fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
    1.66  qed "not_Suc_n_less_n";
    1.67 +Addsimps [not_Suc_n_less_n];
    1.68 +
    1.69 +goal Nat.thy "!!i. i<j ==> j<k --> Suc i < k";
    1.70 +by(nat_ind_tac "k" 1);
    1.71 +by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
    1.72 +by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    1.73 +bind_thm("less_trans_Suc",result() RS mp);
    1.74  
    1.75  (*"Less than" is a linear ordering*)
    1.76  goal Nat.thy "m<n | m=n | n<(m::nat)";
    1.77 @@ -328,8 +347,7 @@
    1.78  (*Can be used with less_Suc_eq to get n=m | n<m *)
    1.79  goal Nat.thy "(~ m < n) = (n < Suc(m))";
    1.80  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.81 -by(ALLGOALS(asm_simp_tac (!simpset addsimps
    1.82 -                          [not_less0,zero_less_Suc,Suc_less_eq])));
    1.83 +by(ALLGOALS Asm_simp_tac);
    1.84  qed "not_less_eq";
    1.85  
    1.86  (*Complete induction, aka course-of-values induction*)
    1.87 @@ -346,9 +364,18 @@
    1.88  by (rtac not_less0 1);
    1.89  qed "le0";
    1.90  
    1.91 -Addsimps [not_less0, less_not_refl, zero_less_Suc, lessI, 
    1.92 -          Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
    1.93 -          Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
    1.94 +goalw Nat.thy [le_def] "~ Suc n <= n";
    1.95 +by(Simp_tac 1);
    1.96 +qed "Suc_n_not_le_n";
    1.97 +
    1.98 +goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
    1.99 +by(nat_ind_tac "i" 1);
   1.100 +by(ALLGOALS Asm_simp_tac);
   1.101 +qed "le_0";
   1.102 +
   1.103 +Addsimps [less_not_refl,
   1.104 +          less_Suc_eq, le0, le_0,
   1.105 +          Suc_Suc_eq, Suc_n_not_le_n,
   1.106            n_not_Suc_n, Suc_n_not_n,
   1.107            nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
   1.108