# HG changeset patch
# User huffman
# Date 1333096887 -7200
# Node ID 4d0878d54ca5d688ea780428c0ca42fa5f3a9b0e
# Parent  c610b61c74a3dd75bc17bff23d7dbd5cd3c9197c
move more theorems from Nat_Numeral.thy to Num.thy

diff -r c610b61c74a3 -r 4d0878d54ca5 src/HOL/Nat_Numeral.thy
--- 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*}
diff -r c610b61c74a3 -r 4d0878d54ca5 src/HOL/Num.thy
--- 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 *}