move lemmas from Nat_Numeral.thy to Nat.thy
authorhuffman
Fri Mar 30 08:11:52 2012 +0200 (2012-03-30)
changeset 472089a91b163bb71
parent 47207 9368aa814518
child 47209 4893907fe872
move lemmas from Nat_Numeral.thy to Nat.thy
src/HOL/Nat.thy
src/HOL/Nat_Numeral.thy
     1.1 --- a/src/HOL/Nat.thy	Fri Mar 30 08:10:28 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Mar 30 08:11:52 2012 +0200
     1.3 @@ -252,6 +252,12 @@
     1.4    apply (simp add:o_def)
     1.5    done
     1.6  
     1.7 +lemma Suc_eq_plus1: "Suc n = n + 1"
     1.8 +  unfolding One_nat_def by simp
     1.9 +
    1.10 +lemma Suc_eq_plus1_left: "Suc n = 1 + n"
    1.11 +  unfolding One_nat_def by simp
    1.12 +
    1.13  
    1.14  subsubsection {* Difference *}
    1.15  
     2.1 --- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 08:10:28 2012 +0200
     2.2 +++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 08:11:52 2012 +0200
     2.3 @@ -31,12 +31,6 @@
     2.4  
     2.5  subsubsection{*Arith *}
     2.6  
     2.7 -lemma Suc_eq_plus1: "Suc n = n + 1"
     2.8 -  unfolding One_nat_def by simp
     2.9 -
    2.10 -lemma Suc_eq_plus1_left: "Suc n = 1 + n"
    2.11 -  unfolding One_nat_def by simp
    2.12 -
    2.13  (* These two can be useful when m = numeral... *)
    2.14  
    2.15  lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"