src/HOL/Nat.ML
changeset 1618 372880456b5b
parent 1552 6f71b5d46700
child 1660 8cb42cd97579
     1.1 --- a/src/HOL/Nat.ML	Tue Mar 26 17:15:54 1996 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Mar 27 18:45:17 1996 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4  by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq])));
     1.5  qed "n_not_Suc_n";
     1.6  
     1.7 -val Suc_n_not_n = n_not_Suc_n RS not_sym;
     1.8 +bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
     1.9  
    1.10  (*** nat_case -- the selection operator for nat ***)
    1.11  
    1.12 @@ -217,7 +217,7 @@
    1.13  qed "lessI";
    1.14  Addsimps [lessI];
    1.15  
    1.16 -(* i(j ==> i(Suc(j) *)
    1.17 +(* i<j ==> i<Suc(j) *)
    1.18  val less_SucI = lessI RSN (2, less_trans);
    1.19  
    1.20  goal Nat.thy "0 < Suc(n)";
    1.21 @@ -239,14 +239,14 @@
    1.22  
    1.23  goalw Nat.thy [less_def] "~ n<(n::nat)";
    1.24  by (rtac notI 1);
    1.25 -by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1);
    1.26 +by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1);
    1.27  qed "less_not_refl";
    1.28  
    1.29  (* n(n ==> R *)
    1.30 -bind_thm ("less_anti_refl", (less_not_refl RS notE));
    1.31 +bind_thm ("less_irrefl", (less_not_refl RS notE));
    1.32  
    1.33  goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
    1.34 -by (fast_tac (HOL_cs addEs [less_anti_refl]) 1);
    1.35 +by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
    1.36  qed "less_not_refl2";
    1.37  
    1.38  
    1.39 @@ -335,7 +335,7 @@
    1.40  Addsimps [Suc_less_eq];
    1.41  
    1.42  goal Nat.thy "~(Suc(n) < n)";
    1.43 -by (fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
    1.44 +by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);
    1.45  qed "not_Suc_n_less_n";
    1.46  Addsimps [not_Suc_n_less_n];
    1.47  
    1.48 @@ -398,23 +398,27 @@
    1.49    "m=n ==> nat_rec m a f = nat_rec n a f"
    1.50    (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.51  
    1.52 -val prems = goalw Nat.thy [le_def] "~(n<m) ==> m<=(n::nat)";
    1.53 +val prems = goalw Nat.thy [le_def] "~n<m ==> m<=(n::nat)";
    1.54  by (resolve_tac prems 1);
    1.55  qed "leI";
    1.56  
    1.57 -val prems = goalw Nat.thy [le_def] "m<=n ==> ~(n<(m::nat))";
    1.58 +val prems = goalw Nat.thy [le_def] "m<=n ==> ~ n < (m::nat)";
    1.59  by (resolve_tac prems 1);
    1.60  qed "leD";
    1.61  
    1.62  val leE = make_elim leD;
    1.63  
    1.64 +goal Nat.thy "(~n<m) = (m<=(n::nat))";
    1.65 +by (fast_tac (HOL_cs addIs [leI] addEs [leE]) 1);
    1.66 +qed "not_less_iff_le";
    1.67 +
    1.68  goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
    1.69  by (fast_tac HOL_cs 1);
    1.70  qed "not_leE";
    1.71  
    1.72  goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
    1.73  by (Simp_tac 1);
    1.74 -by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
    1.75 +by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
    1.76  qed "lessD";
    1.77  
    1.78  goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
    1.79 @@ -433,12 +437,12 @@
    1.80  
    1.81  goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
    1.82  by (cut_facts_tac [less_linear] 1);
    1.83 -by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
    1.84 +by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
    1.85  qed "le_imp_less_or_eq";
    1.86  
    1.87  goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
    1.88  by (cut_facts_tac [less_linear] 1);
    1.89 -by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
    1.90 +by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
    1.91  by (flexflex_tac);
    1.92  qed "less_or_eq_imp_le";
    1.93  
    1.94 @@ -467,7 +471,7 @@
    1.95  
    1.96  val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
    1.97  by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
    1.98 -          fast_tac (HOL_cs addEs [less_anti_refl,less_asym])]);
    1.99 +          fast_tac (HOL_cs addEs [less_irrefl,less_asym])]);
   1.100  qed "le_anti_sym";
   1.101  
   1.102  goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)";