src/HOL/Num.thy
changeset 51143 0a2371e7ced3
parent 50817 652731d92061
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/Num.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Num.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -545,7 +545,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma nat_of_num_numeral: "nat_of_num = numeral"
     1.8 +lemma nat_of_num_numeral [code_abbrev]:
     1.9 +  "nat_of_num = numeral"
    1.10  proof
    1.11    fix n
    1.12    have "numeral n = nat_of_num n"
    1.13 @@ -553,6 +554,12 @@
    1.14    then show "nat_of_num n = numeral n" by simp
    1.15  qed
    1.16  
    1.17 +lemma nat_of_num_code [code]:
    1.18 +  "nat_of_num One = 1"
    1.19 +  "nat_of_num (Bit0 n) = (let m = nat_of_num n in m + m)"
    1.20 +  "nat_of_num (Bit1 n) = (let m = nat_of_num n in Suc (m + m))"
    1.21 +  by (simp_all add: Let_def)
    1.22 +
    1.23  subsubsection {*
    1.24    Equality: class @{text semiring_char_0}
    1.25  *}
    1.26 @@ -1097,6 +1104,7 @@
    1.27  
    1.28  hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
    1.29  
    1.30 +
    1.31  subsection {* code module namespace *}
    1.32  
    1.33  code_modulename SML
    1.34 @@ -1110,3 +1118,4 @@
    1.35  
    1.36  end
    1.37  
    1.38 +