removed redundant Nat.less_not_sym, Nat.less_asym;
authorwenzelm
Wed Mar 19 18:15:25 2008 +0100 (2008-03-19)
changeset 26335961bbcc9d85b
parent 26334 80ec6cf82d95
child 26336 a0e2b706ce73
removed redundant Nat.less_not_sym, Nat.less_asym;
renamed Nat.less_irrefl to less_irrefl_nat, no longer declared elim;
NEWS
src/HOL/Nat.thy
     1.1 --- a/NEWS	Wed Mar 19 18:15:13 2008 +0100
     1.2 +++ b/NEWS	Wed Mar 19 18:15:25 2008 +0100
     1.3 @@ -44,11 +44,20 @@
     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 types and different variable names.
    1.12 +* Theory Nat: removed redundant lemmas that merely duplicate lemmas of
    1.13 +the same name in theory Orderings:
    1.14 +
    1.15 +  less_trans
    1.16 +  less_linear
    1.17 +  le_imp_less_or_eq
    1.18 +  le_less_trans
    1.19 +  less_le_trans
    1.20 +  less_not_sym
    1.21 +  less_asym
    1.22 +
    1.23 +Renamed less_imp_le to less_imp_le_nat, and less_irrefl to
    1.24 +less_irrefl_nat.  Potential INCOMPATIBILITY due to more general types
    1.25 +and different variable names.
    1.26  
    1.27  * Library/Option_ord.thy: Canonical order on option type.
    1.28  
     2.1 --- a/src/HOL/Nat.thy	Wed Mar 19 18:15:13 2008 +0100
     2.2 +++ b/src/HOL/Nat.thy	Wed Mar 19 18:15:25 2008 +0100
     2.3 @@ -439,28 +439,17 @@
     2.4  
     2.5  subsubsection {* Elimination properties *}
     2.6  
     2.7 -lemma less_not_sym: "n < m ==> ~ m < (n::nat)"
     2.8 -  by (rule order_less_not_sym)
     2.9 -
    2.10 -lemma less_asym:
    2.11 -  assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P
    2.12 -  apply (rule contrapos_np)
    2.13 -  apply (rule less_not_sym)
    2.14 -  apply (rule h1)
    2.15 -  apply (erule h2)
    2.16 -  done
    2.17 -
    2.18  lemma less_not_refl: "~ n < (n::nat)"
    2.19    by (rule order_less_irrefl)
    2.20  
    2.21 -lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
    2.22 -  by (rule notE, rule less_not_refl)
    2.23 +lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
    2.24 +  by (rule not_sym) (rule less_imp_neq) 
    2.25  
    2.26  lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
    2.27    by (rule less_imp_neq)
    2.28  
    2.29 -lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
    2.30 -  by (rule not_sym) (rule less_imp_neq) 
    2.31 +lemma less_irrefl_nat: "(n::nat) < n ==> R"
    2.32 +  by (rule notE, rule less_not_refl)
    2.33  
    2.34  lemma less_zeroE: "(n::nat) < 0 ==> R"
    2.35    by (rule notE) (rule not_less0)
    2.36 @@ -815,7 +804,8 @@
    2.37  
    2.38  lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
    2.39  apply (rule notI)
    2.40 -apply (erule add_lessD1 [THEN less_irrefl])
    2.41 +apply (drule add_lessD1)
    2.42 +apply (erule less_irrefl [THEN notE])
    2.43  done
    2.44  
    2.45  lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"