src/HOL/Nat.thy
changeset 26315 cb3badaa192e
parent 26300 03def556e26e
child 26335 961bbcc9d85b
     1.1 --- a/src/HOL/Nat.thy	Tue Mar 18 20:33:28 2008 +0100
     1.2 +++ b/src/HOL/Nat.thy	Tue Mar 18 20:33:29 2008 +0100
     1.3 @@ -386,7 +386,8 @@
     1.4  lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n"
     1.5    by (simp add: less_eq_Suc_le) (erule Suc_leD)
     1.6  
     1.7 -instance proof
     1.8 +instance
     1.9 +proof
    1.10    fix n m :: nat
    1.11    have less_imp_le: "n < m \<Longrightarrow> n \<le> m"
    1.12      unfolding less_eq_Suc_le by (erule Suc_leD)
    1.13 @@ -435,8 +436,6 @@
    1.14  lemma zero_less_Suc [iff]: "0 < Suc n"
    1.15    by (simp add: less_Suc_eq_le)
    1.16  
    1.17 -lemma less_trans: "i < j ==> j < k ==> i < (k::nat)"
    1.18 -  by (rule order_less_trans)
    1.19  
    1.20  subsubsection {* Elimination properties *}
    1.21  
    1.22 @@ -478,9 +477,6 @@
    1.23  lemma Suc_mono: "m < n ==> Suc m < Suc n"
    1.24    by simp
    1.25  
    1.26 -lemma less_linear: "m < n | m = n | n < (m::nat)"
    1.27 -  by (rule less_linear)
    1.28 -
    1.29  text {* "Less than" is antisymmetric, sort of *}
    1.30  lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
    1.31    unfolding not_less less_Suc_eq_le by (rule antisym)
    1.32 @@ -569,18 +565,15 @@
    1.33  lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
    1.34    unfolding Suc_le_eq .
    1.35  
    1.36 -lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
    1.37 +lemma less_imp_le_nat: "m < n ==> m \<le> (n::nat)"
    1.38    unfolding less_eq_Suc_le by (rule Suc_leD)
    1.39  
    1.40  text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
    1.41 -lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
    1.42 +lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
    1.43  
    1.44  
    1.45  text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}
    1.46  
    1.47 -lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)"
    1.48 -  unfolding le_less .
    1.49 -
    1.50  lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
    1.51    unfolding le_less .
    1.52  
    1.53 @@ -594,12 +587,6 @@
    1.54  lemma le_refl: "n \<le> (n::nat)"
    1.55    by simp
    1.56  
    1.57 -lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
    1.58 -  by (rule order_le_less_trans)
    1.59 -
    1.60 -lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
    1.61 -  by (rule order_less_le_trans)
    1.62 -
    1.63  lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
    1.64    by (rule order_trans)
    1.65