# HG changeset patch
# User haftmann
# Date 1357888659 -3600
# Node ID 652731d920614d72b054f3682a69b015920b2b05
# Parent  2c366a03c888d3507741fa5a59973a41c00f4236
sharing of recursive results on evaluation

diff -r 2c366a03c888 -r 652731d92061 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Thu Jan 10 23:48:01 2013 +0100
+++ b/src/HOL/Num.thy	Fri Jan 11 08:17:39 2013 +0100
@@ -245,6 +245,12 @@
   numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n" |
   numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1"
 
+lemma numeral_code [code]:
+  "numeral One = 1"
+  "numeral (Bit0 n) = (let m = numeral n in m + m)"
+  "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"
+  by (simp_all add: Let_def)
+  
 lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1"
   apply (induct x)
   apply simp
@@ -1103,3 +1109,4 @@
   Num Arith
 
 end
+