new lemmas for simplifying subtraction on nat numerals
authorhuffman
Fri Mar 30 11:52:26 2012 +0200 (2012-03-30)
changeset 472182b652cbadde1
parent 47217 501b9bbd0d6e
child 47219 172c031ad743
new lemmas for simplifying subtraction on nat numerals
src/HOL/Nat_Numeral.thy
src/HOL/Num.thy
     1.1 --- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 11:16:35 2012 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 11:52:26 2012 +0200
     1.3 @@ -101,11 +101,6 @@
     1.4  lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - Numeral1)"
     1.5  by (simp split: nat_diff_split)
     1.6  
     1.7 -text{*No longer required as a simprule because of the @{text inverse_fold}
     1.8 -   simproc*}
     1.9 -lemma Suc_diff_numeral: "Suc m - (numeral v) = m - (numeral v - 1)"
    1.10 -  by (subst expand_Suc, simp only: diff_Suc_Suc)
    1.11 -
    1.12  lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
    1.13  by (simp split: nat_diff_split)
    1.14  
     2.1 --- a/src/HOL/Num.thy	Fri Mar 30 11:16:35 2012 +0200
     2.2 +++ b/src/HOL/Num.thy	Fri Mar 30 11:52:26 2012 +0200
     2.3 @@ -919,6 +919,12 @@
     2.4  lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
     2.5    by (simp add: numeral_eq_Suc)
     2.6  
     2.7 +lemma diff_Suc_numeral [simp]: "Suc n - numeral k = n - pred_numeral k"
     2.8 +  by (simp add: numeral_eq_Suc)
     2.9 +
    2.10 +lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n"
    2.11 +  by (simp add: numeral_eq_Suc)
    2.12 +
    2.13  lemma max_Suc_numeral [simp]:
    2.14    "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
    2.15    by (simp add: numeral_eq_Suc)