removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
authorwenzelm
Tue Mar 18 20:33:29 2008 +0100 (2008-03-18)
changeset 26315cb3badaa192e
parent 26314 9c39fc898fff
child 26316 9e9e67e33557
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
renamed less_imp_le to less_imp_le_nat;
NEWS
src/HOL/Nat.thy
     1.1 --- a/NEWS	Tue Mar 18 20:33:28 2008 +0100
     1.2 +++ b/NEWS	Tue Mar 18 20:33:29 2008 +0100
     1.3 @@ -40,6 +40,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Nat: renamed less_imp_le to less_imp_le_nat; removed
     1.8 +redundant lemmas less_trans, less_linear, le_imp_less_or_eq,
     1.9 +le_less_trans, less_le_trans, which merely duplicate lemmas of the
    1.10 +same name in theory Orderings.  Potential INCOMPATIBILITY due to more
    1.11 +general and different variable names.
    1.12 +
    1.13  * Library/Option_ord.thy: Canonical order on option type.
    1.14  
    1.15  * Library/RBT.thy: New theory of red-black trees, an efficient
     2.1 --- a/src/HOL/Nat.thy	Tue Mar 18 20:33:28 2008 +0100
     2.2 +++ b/src/HOL/Nat.thy	Tue Mar 18 20:33:29 2008 +0100
     2.3 @@ -386,7 +386,8 @@
     2.4  lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n"
     2.5    by (simp add: less_eq_Suc_le) (erule Suc_leD)
     2.6  
     2.7 -instance proof
     2.8 +instance
     2.9 +proof
    2.10    fix n m :: nat
    2.11    have less_imp_le: "n < m \<Longrightarrow> n \<le> m"
    2.12      unfolding less_eq_Suc_le by (erule Suc_leD)
    2.13 @@ -435,8 +436,6 @@
    2.14  lemma zero_less_Suc [iff]: "0 < Suc n"
    2.15    by (simp add: less_Suc_eq_le)
    2.16  
    2.17 -lemma less_trans: "i < j ==> j < k ==> i < (k::nat)"
    2.18 -  by (rule order_less_trans)
    2.19  
    2.20  subsubsection {* Elimination properties *}
    2.21  
    2.22 @@ -478,9 +477,6 @@
    2.23  lemma Suc_mono: "m < n ==> Suc m < Suc n"
    2.24    by simp
    2.25  
    2.26 -lemma less_linear: "m < n | m = n | n < (m::nat)"
    2.27 -  by (rule less_linear)
    2.28 -
    2.29  text {* "Less than" is antisymmetric, sort of *}
    2.30  lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
    2.31    unfolding not_less less_Suc_eq_le by (rule antisym)
    2.32 @@ -569,18 +565,15 @@
    2.33  lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
    2.34    unfolding Suc_le_eq .
    2.35  
    2.36 -lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
    2.37 +lemma less_imp_le_nat: "m < n ==> m \<le> (n::nat)"
    2.38    unfolding less_eq_Suc_le by (rule Suc_leD)
    2.39  
    2.40  text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
    2.41 -lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
    2.42 +lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
    2.43  
    2.44  
    2.45  text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}
    2.46  
    2.47 -lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)"
    2.48 -  unfolding le_less .
    2.49 -
    2.50  lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
    2.51    unfolding le_less .
    2.52  
    2.53 @@ -594,12 +587,6 @@
    2.54  lemma le_refl: "n \<le> (n::nat)"
    2.55    by simp
    2.56  
    2.57 -lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
    2.58 -  by (rule order_le_less_trans)
    2.59 -
    2.60 -lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
    2.61 -  by (rule order_less_le_trans)
    2.62 -
    2.63  lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
    2.64    by (rule order_trans)
    2.65