--- 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