more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code
authorhaftmann
Sun Sep 27 10:11:14 2015 +0200 (2015-09-27)
changeset 612740261eec37233
parent 61273 542a4d9bac96
child 61275 053ec04ea866
more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code
src/HOL/Code_Numeral.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Sep 28 17:29:01 2015 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Sep 27 10:11:14 2015 +0200
     1.3 @@ -244,12 +244,18 @@
     1.4  
     1.5  definition Pos :: "num \<Rightarrow> integer"
     1.6  where
     1.7 -  [simp, code_abbrev]: "Pos = numeral"
     1.8 +  [simp, code_post]: "Pos = numeral"
     1.9  
    1.10  lemma [transfer_rule]:
    1.11    "rel_fun HOL.eq pcr_integer numeral Pos"
    1.12    by simp transfer_prover
    1.13  
    1.14 +lemma Pos_fold [code_unfold]:
    1.15 +  "numeral Num.One = Pos Num.One"
    1.16 +  "numeral (Num.Bit0 k) = Pos (Num.Bit0 k)"
    1.17 +  "numeral (Num.Bit1 k) = Pos (Num.Bit1 k)"
    1.18 +  by simp_all
    1.19 +
    1.20  definition Neg :: "num \<Rightarrow> integer"
    1.21  where
    1.22    [simp, code_abbrev]: "Neg n = - Pos n"