src/HOL/Nat.thy
changeset 26335 961bbcc9d85b
parent 26315 cb3badaa192e
child 26748 4d51ddd6aa5c
     1.1 --- a/src/HOL/Nat.thy	Wed Mar 19 18:15:13 2008 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Mar 19 18:15:25 2008 +0100
     1.3 @@ -439,28 +439,17 @@
     1.4  
     1.5  subsubsection {* Elimination properties *}
     1.6  
     1.7 -lemma less_not_sym: "n < m ==> ~ m < (n::nat)"
     1.8 -  by (rule order_less_not_sym)
     1.9 -
    1.10 -lemma less_asym:
    1.11 -  assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P
    1.12 -  apply (rule contrapos_np)
    1.13 -  apply (rule less_not_sym)
    1.14 -  apply (rule h1)
    1.15 -  apply (erule h2)
    1.16 -  done
    1.17 -
    1.18  lemma less_not_refl: "~ n < (n::nat)"
    1.19    by (rule order_less_irrefl)
    1.20  
    1.21 -lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
    1.22 -  by (rule notE, rule less_not_refl)
    1.23 +lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
    1.24 +  by (rule not_sym) (rule less_imp_neq) 
    1.25  
    1.26  lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
    1.27    by (rule less_imp_neq)
    1.28  
    1.29 -lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
    1.30 -  by (rule not_sym) (rule less_imp_neq) 
    1.31 +lemma less_irrefl_nat: "(n::nat) < n ==> R"
    1.32 +  by (rule notE, rule less_not_refl)
    1.33  
    1.34  lemma less_zeroE: "(n::nat) < 0 ==> R"
    1.35    by (rule notE) (rule not_less0)
    1.36 @@ -815,7 +804,8 @@
    1.37  
    1.38  lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
    1.39  apply (rule notI)
    1.40 -apply (erule add_lessD1 [THEN less_irrefl])
    1.41 +apply (drule add_lessD1)
    1.42 +apply (erule less_irrefl [THEN notE])
    1.43  done
    1.44  
    1.45  lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"