# HG changeset patch
# User huffman
# Date 1235502605 28800
# Node ID 46b9c8ae3897e1157f4a341cc836cc37ad68e7ad
# Parent  4cf42465b3daefdbb4cc8eebee52ec7b630a356c
add simp rules for numerals with 1::nat

diff -r 4cf42465b3da -r 46b9c8ae3897 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Tue Feb 24 08:20:14 2009 -0800
+++ b/src/HOL/NatBin.thy	Tue Feb 24 11:10:05 2009 -0800
@@ -159,6 +159,21 @@
   unfolding nat_number_of_def number_of_is_id numeral_simps
   by (simp add: nat_add_distrib)
 
+lemma nat_number_of_add_1 [simp]:
+  "number_of v + (1::nat) =
+    (if v < Int.Pls then 1 else number_of (Int.succ v))"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
+  by (simp add: nat_add_distrib)
+
+lemma nat_1_add_number_of [simp]:
+  "(1::nat) + number_of v =
+    (if v < Int.Pls then 1 else number_of (Int.succ v))"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
+  by (simp add: nat_add_distrib)
+
+lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
+  by (rule int_int_eq [THEN iffD1]) simp
+
 
 subsubsection{*Subtraction *}
 
@@ -178,6 +193,12 @@
   unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
   by auto
 
+lemma nat_number_of_diff_1 [simp]:
+  "number_of v - (1::nat) =
+    (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
+  by auto
+
 
 subsubsection{*Multiplication *}