--- a/src/HOL/Nat_Numeral.thy Fri Mar 30 09:55:03 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy Fri Mar 30 10:41:27 2012 +0200
@@ -110,26 +110,6 @@
by (simp split: nat_diff_split)
-subsubsection{*For @{term nat_case} and @{term nat_rec}*}
-
-lemma nat_case_numeral [simp]:
- "nat_case a f (numeral v) = (let pv = nat (numeral v - 1) in f pv)"
- by (subst expand_Suc, simp only: nat.cases nat_numeral_diff_1 Let_def)
-
-lemma nat_case_add_eq_if [simp]:
- "nat_case a f ((numeral v) + n) = (let pv = nat (numeral v - 1) in f (pv + n))"
- by (subst expand_Suc, simp only: nat.cases nat_numeral_diff_1 Let_def add_Suc)
-
-lemma nat_rec_numeral [simp]:
- "nat_rec a f (numeral v) = (let pv = nat (numeral v - 1) in f pv (nat_rec a f pv))"
- by (subst expand_Suc, simp only: nat_rec_Suc nat_numeral_diff_1 Let_def)
-
-lemma nat_rec_add_eq_if [simp]:
- "nat_rec a f (numeral v + n) =
- (let pv = nat (numeral v - 1) in f (pv + n) (nat_rec a f (pv + n)))"
- by (subst expand_Suc, simp only: nat_rec_Suc nat_numeral_diff_1 Let_def add_Suc)
-
-
subsubsection{*Various Other Lemmas*}
text {*Evens and Odds, for Mutilated Chess Board*}
--- a/src/HOL/Num.thy Fri Mar 30 09:55:03 2012 +0200
+++ b/src/HOL/Num.thy Fri Mar 30 10:41:27 2012 +0200
@@ -935,6 +935,26 @@
"min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
by (simp add: numeral_eq_Suc)
+text {* For @{term nat_case} and @{term nat_rec}. *}
+
+lemma nat_case_numeral [simp]:
+ "nat_case a f (numeral v) = (let pv = pred_numeral v in f pv)"
+ by (simp add: numeral_eq_Suc)
+
+lemma nat_case_add_eq_if [simp]:
+ "nat_case a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
+ by (simp add: numeral_eq_Suc)
+
+lemma nat_rec_numeral [simp]:
+ "nat_rec a f (numeral v) =
+ (let pv = pred_numeral v in f pv (nat_rec a f pv))"
+ by (simp add: numeral_eq_Suc Let_def)
+
+lemma nat_rec_add_eq_if [simp]:
+ "nat_rec a f (numeral v + n) =
+ (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))"
+ by (simp add: numeral_eq_Suc Let_def)
+
subsection {* Numeral equations as default simplification rules *}