src/HOL/Code_Evaluation.thy
changeset 51144 0ede9e2266a8
parent 51143 0a2371e7ced3
child 51160 599ff65b85e2
     1.1 --- a/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:31 2013 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -133,50 +133,15 @@
     1.4    (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))"
     1.5       and "Term.Free/ ((_), (_))")
     1.6  
     1.7 +code_const "term_of \<Colon> integer \<Rightarrow> term"
     1.8 +  (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT")
     1.9 +  
    1.10  code_const "term_of \<Colon> String.literal \<Rightarrow> term"
    1.11    (Eval "HOLogic.mk'_literal")
    1.12  
    1.13  code_reserved Eval HOLogic
    1.14  
    1.15  
    1.16 -subsubsection {* Numeric types *}
    1.17 -
    1.18 -definition term_of_num_semiring :: "'a\<Colon>semiring_div \<Rightarrow> 'a \<Rightarrow> term" where
    1.19 -  "term_of_num_semiring two = (\<lambda>_. dummy_term)"
    1.20 -
    1.21 -lemma (in term_syntax) term_of_num_semiring_code [code]:
    1.22 -  "term_of_num_semiring two k = (
    1.23 -    if k = 1 then termify Num.One
    1.24 -    else (if k mod two = 0
    1.25 -      then termify Num.Bit0 <\<cdot>> term_of_num_semiring two (k div two)
    1.26 -      else termify Num.Bit1 <\<cdot>> term_of_num_semiring two (k div two)))"
    1.27 -  by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def)
    1.28 -
    1.29 -lemma (in term_syntax) term_of_nat_code [code]:
    1.30 -  "term_of (n::nat) = (
    1.31 -    if n = 0 then termify (0 :: nat)
    1.32 -    else termify (numeral :: num \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n)"
    1.33 -  by (simp only: term_of_anything)
    1.34 -
    1.35 -lemma (in term_syntax) term_of_natural_code [code]:
    1.36 -  "term_of (k::natural) = (
    1.37 -    if k = 0 then termify (0 :: natural)
    1.38 -    else termify (numeral :: num \<Rightarrow> natural) <\<cdot>> term_of_num_semiring (2::natural) k)"
    1.39 -  by (simp only: term_of_anything)
    1.40 -
    1.41 -lemma (in term_syntax) term_of_integer_code [code]:
    1.42 -  "term_of (k::integer) = (if k = 0 then termify (0 :: integer)
    1.43 -    else if k < 0 then termify (neg_numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) (- k)
    1.44 -    else termify (numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) k)"
    1.45 -  by (simp only: term_of_anything)
    1.46 -
    1.47 -lemma (in term_syntax) term_of_int_code [code]:
    1.48 -  "term_of (k::int) = (if k = 0 then termify (0 :: int)
    1.49 -    else if k < 0 then termify (neg_numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) (- k)
    1.50 -    else termify (numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) k)"
    1.51 -  by (simp only: term_of_anything)
    1.52 -
    1.53 -
    1.54  subsubsection {* Obfuscation *}
    1.55  
    1.56  print_translation {*
    1.57 @@ -202,7 +167,7 @@
    1.58  
    1.59  
    1.60  hide_const dummy_term valapp
    1.61 -hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring tracing
    1.62 +hide_const (open) Const App Abs Free termify valtermify term_of tracing
    1.63  
    1.64  end
    1.65