--- a/src/HOL/Integ/NatBin.thy Wed Jun 14 12:12:01 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy Wed Jun 14 12:12:37 2006 +0200
@@ -781,13 +781,6 @@
subsection {* code generator setup *}
-lemma number_of_eval [code fun]:
- "number_of Numeral.Pls = (0::int)"
- and "number_of Numeral.Min = uminus (1::int)"
- and "number_of (n BIT bit.B0) = (2::int) * number_of n"
- and "number_of (n BIT bit.B1) = (2::int) * number_of n + 1"
- by simp_all
-
lemma elim_nat [code unfolt]:
"(number_of n :: nat) = nat (number_of n)"
by simp
@@ -800,6 +793,10 @@
"(1::int) = number_of (Numeral.Pls BIT bit.B1)"
by simp
+lemma elim_one_nat [code unfolt]:
+ "1 = Suc 0"
+ by simp
+
lemmas [code unfolt] =
bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0