src/HOL/Code_Evaluation.thy
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 51144 0ede9e2266a8
     1.1 --- a/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -158,10 +158,16 @@
     1.4      else termify (numeral :: num \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n)"
     1.5    by (simp only: term_of_anything)
     1.6  
     1.7 -lemma (in term_syntax) term_of_code_numeral_code [code]:
     1.8 -  "term_of (k::code_numeral) = (
     1.9 -    if k = 0 then termify (0 :: code_numeral)
    1.10 -    else termify (numeral :: num \<Rightarrow> code_numeral) <\<cdot>> term_of_num_semiring (2::code_numeral) k)"
    1.11 +lemma (in term_syntax) term_of_natural_code [code]:
    1.12 +  "term_of (k::natural) = (
    1.13 +    if k = 0 then termify (0 :: natural)
    1.14 +    else termify (numeral :: num \<Rightarrow> natural) <\<cdot>> term_of_num_semiring (2::natural) k)"
    1.15 +  by (simp only: term_of_anything)
    1.16 +
    1.17 +lemma (in term_syntax) term_of_integer_code [code]:
    1.18 +  "term_of (k::integer) = (if k = 0 then termify (0 :: integer)
    1.19 +    else if k < 0 then termify (neg_numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) (- k)
    1.20 +    else termify (numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) k)"
    1.21    by (simp only: term_of_anything)
    1.22  
    1.23  lemma (in term_syntax) term_of_int_code [code]:
    1.24 @@ -199,3 +205,4 @@
    1.25  hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring tracing
    1.26  
    1.27  end
    1.28 +