sharing of recursive results on evaluation
authorhaftmann
Fri Jan 11 08:17:39 2013 +0100 (2013-01-11)
changeset 50817652731d92061
parent 50816 2c366a03c888
child 50818 5d4852f1b952
sharing of recursive results on evaluation
src/HOL/Num.thy
     1.1 --- a/src/HOL/Num.thy	Thu Jan 10 23:48:01 2013 +0100
     1.2 +++ b/src/HOL/Num.thy	Fri Jan 11 08:17:39 2013 +0100
     1.3 @@ -245,6 +245,12 @@
     1.4    numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n" |
     1.5    numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1"
     1.6  
     1.7 +lemma numeral_code [code]:
     1.8 +  "numeral One = 1"
     1.9 +  "numeral (Bit0 n) = (let m = numeral n in m + m)"
    1.10 +  "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"
    1.11 +  by (simp_all add: Let_def)
    1.12 +  
    1.13  lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1"
    1.14    apply (induct x)
    1.15    apply simp
    1.16 @@ -1103,3 +1109,4 @@
    1.17    Num Arith
    1.18  
    1.19  end
    1.20 +