src/HOL/Code_Evaluation.thy
changeset 51144 0ede9e2266a8
parent 51143 0a2371e7ced3
child 51160 599ff65b85e2
--- a/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:31 2013 +0100
+++ b/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:31 2013 +0100
@@ -133,50 +133,15 @@
   (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))"
      and "Term.Free/ ((_), (_))")
 
+code_const "term_of \<Colon> integer \<Rightarrow> term"
+  (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT")
+  
 code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   (Eval "HOLogic.mk'_literal")
 
 code_reserved Eval HOLogic
 
 
-subsubsection {* Numeric types *}
-
-definition term_of_num_semiring :: "'a\<Colon>semiring_div \<Rightarrow> 'a \<Rightarrow> term" where
-  "term_of_num_semiring two = (\<lambda>_. dummy_term)"
-
-lemma (in term_syntax) term_of_num_semiring_code [code]:
-  "term_of_num_semiring two k = (
-    if k = 1 then termify Num.One
-    else (if k mod two = 0
-      then termify Num.Bit0 <\<cdot>> term_of_num_semiring two (k div two)
-      else termify Num.Bit1 <\<cdot>> term_of_num_semiring two (k div two)))"
-  by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def)
-
-lemma (in term_syntax) term_of_nat_code [code]:
-  "term_of (n::nat) = (
-    if n = 0 then termify (0 :: nat)
-    else termify (numeral :: num \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n)"
-  by (simp only: term_of_anything)
-
-lemma (in term_syntax) term_of_natural_code [code]:
-  "term_of (k::natural) = (
-    if k = 0 then termify (0 :: natural)
-    else termify (numeral :: num \<Rightarrow> natural) <\<cdot>> term_of_num_semiring (2::natural) k)"
-  by (simp only: term_of_anything)
-
-lemma (in term_syntax) term_of_integer_code [code]:
-  "term_of (k::integer) = (if k = 0 then termify (0 :: integer)
-    else if k < 0 then termify (neg_numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) (- k)
-    else termify (numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) k)"
-  by (simp only: term_of_anything)
-
-lemma (in term_syntax) term_of_int_code [code]:
-  "term_of (k::int) = (if k = 0 then termify (0 :: int)
-    else if k < 0 then termify (neg_numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) (- k)
-    else termify (numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) k)"
-  by (simp only: term_of_anything)
-
-
 subsubsection {* Obfuscation *}
 
 print_translation {*
@@ -202,7 +167,7 @@
 
 
 hide_const dummy_term valapp
-hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring tracing
+hide_const (open) Const App Abs Free termify valtermify term_of tracing
 
 end