src/HOL/Num.thy
changeset 47216 4d0878d54ca5
parent 47211 e1b0c8236ae4
child 47218 2b652cbadde1
     1.1 --- a/src/HOL/Num.thy	Fri Mar 30 09:55:03 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 30 10:41:27 2012 +0200
     1.3 @@ -935,6 +935,26 @@
     1.4    "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
     1.5    by (simp add: numeral_eq_Suc)
     1.6  
     1.7 +text {* For @{term nat_case} and @{term nat_rec}. *}
     1.8 +
     1.9 +lemma nat_case_numeral [simp]:
    1.10 +  "nat_case a f (numeral v) = (let pv = pred_numeral v in f pv)"
    1.11 +  by (simp add: numeral_eq_Suc)
    1.12 +
    1.13 +lemma nat_case_add_eq_if [simp]:
    1.14 +  "nat_case a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
    1.15 +  by (simp add: numeral_eq_Suc)
    1.16 +
    1.17 +lemma nat_rec_numeral [simp]:
    1.18 +  "nat_rec a f (numeral v) =
    1.19 +    (let pv = pred_numeral v in f pv (nat_rec a f pv))"
    1.20 +  by (simp add: numeral_eq_Suc Let_def)
    1.21 +
    1.22 +lemma nat_rec_add_eq_if [simp]:
    1.23 +  "nat_rec a f (numeral v + n) =
    1.24 +    (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))"
    1.25 +  by (simp add: numeral_eq_Suc Let_def)
    1.26 +
    1.27  
    1.28  subsection {* Numeral equations as default simplification rules *}
    1.29