--- a/src/HOL/Nat_Numeral.thy Fri Mar 30 11:16:35 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy Fri Mar 30 11:52:26 2012 +0200
@@ -101,11 +101,6 @@
lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - Numeral1)"
by (simp split: nat_diff_split)
-text{*No longer required as a simprule because of the @{text inverse_fold}
- simproc*}
-lemma Suc_diff_numeral: "Suc m - (numeral v) = m - (numeral v - 1)"
- by (subst expand_Suc, simp only: diff_Suc_Suc)
-
lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
by (simp split: nat_diff_split)
--- a/src/HOL/Num.thy Fri Mar 30 11:16:35 2012 +0200
+++ b/src/HOL/Num.thy Fri Mar 30 11:52:26 2012 +0200
@@ -919,6 +919,12 @@
lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
by (simp add: numeral_eq_Suc)
+lemma diff_Suc_numeral [simp]: "Suc n - numeral k = n - pred_numeral k"
+ by (simp add: numeral_eq_Suc)
+
+lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n"
+ by (simp add: numeral_eq_Suc)
+
lemma max_Suc_numeral [simp]:
"max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
by (simp add: numeral_eq_Suc)