diff -r 732c0b059463 -r 78a64f3f7125 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed Mar 28 12:13:21 2018 -0700
+++ b/src/HOL/Num.thy	Tue Apr 03 15:36:51 2018 +0000
@@ -987,6 +987,10 @@
 
 subsubsection \<open>Natural numbers\<close>
 
+lemma numeral_num_of_nat:
+  "numeral (num_of_nat n) = n" if "n > 0"
+  using that nat_of_num_numeral num_of_nat_inverse by simp
+
 lemma Suc_1 [simp]: "Suc 1 = 2"
   unfolding Suc_eq_plus1 by (rule one_add_one)
 
@@ -994,7 +998,9 @@
   unfolding Suc_eq_plus1 by (rule numeral_plus_one)
 
 definition pred_numeral :: "num \<Rightarrow> nat"
-  where [code del]: "pred_numeral k = numeral k - 1"
+  where "pred_numeral k = numeral k - 1"
+
+declare [[code drop: pred_numeral]]
 
 lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
   by (simp add: pred_numeral_def)
@@ -1011,6 +1017,10 @@
   "pred_numeral (Bit1 k) = numeral (Bit0 k)"
   by (simp_all only: pred_numeral_def eval_nat_numeral diff_Suc_Suc diff_0)
 
+lemma pred_numeral_inc [simp]:
+  "pred_numeral (Num.inc k) = numeral k"
+  by (simp only: pred_numeral_def numeral_inc diff_add_inverse2)
+
 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
   by (simp add: eval_nat_numeral)