use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
authorAndreas Lochbihler
Wed Aug 14 17:45:16 2013 +0200 (2013-08-14)
changeset 530271774d569b604
parent 53026 e1a548c11845
child 53030 1b18e3ce776f
use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
src/HOL/Library/Code_Target_Nat.thy
     1.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Tue Aug 13 18:22:55 2013 +0200
     1.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Wed Aug 14 17:45:16 2013 +0200
     1.3 @@ -123,9 +123,27 @@
     1.4    "integer_of_nat (nat k) = max 0 (integer_of_int k)"
     1.5    by transfer auto
     1.6  
     1.7 +lemma term_of_nat_code [code]:
     1.8 +  -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
     1.9 +        instead of @{term Code_Target_Nat.Nat} such that reconstructed
    1.10 +        terms can be fed back to the code generator *}
    1.11 +  "term_of_class.term_of n =
    1.12 +   Code_Evaluation.App
    1.13 +     (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
    1.14 +        (typerep.Typerep (STR ''fun'')
    1.15 +           [typerep.Typerep (STR ''Code_Numeral.integer'') [],
    1.16 +         typerep.Typerep (STR ''Nat.nat'') []]))
    1.17 +     (term_of_class.term_of (integer_of_nat n))"
    1.18 +by(simp add: term_of_anything)
    1.19 +
    1.20 +lemma nat_of_integer_code_post [code_post]:
    1.21 +  "nat_of_integer 0 = 0"
    1.22 +  "nat_of_integer 1 = 1"
    1.23 +  "nat_of_integer (numeral k) = numeral k"
    1.24 +by(transfer, simp)+
    1.25 +
    1.26  code_identifier
    1.27    code_module Code_Target_Nat \<rightharpoonup>
    1.28      (SML) Arith and (OCaml) Arith and (Haskell) Arith
    1.29  
    1.30  end
    1.31 -