1.1 --- a/src/HOL/Code_Eval.thy	Mon May 18 09:49:37 2009 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Mon May 18 15:45:32 2009 +0200
     1.3 @@ -28,13 +28,13 @@
     1.4  lemma term_of_anything: "term_of x \<equiv> t"
     1.5    by (rule eq_reflection) (cases "term_of x", cases t, simp)
     1.6  
     1.7 -definition app :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
     1.8 +definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
     1.9    \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
    1.10 -  "app f x = (fst f (fst x), \<lambda>u. Code_Eval.App (snd f ()) (snd x ()))"
    1.11 +  "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
    1.12  
    1.13 -lemma app_code [code, code inline]:
    1.14 -  "app (f, tf) (x, tx) = (f x, \<lambda>u. Code_Eval.App (tf ()) (tx ()))"
    1.15 -  by (simp only: app_def fst_conv snd_conv)
    1.16 +lemma valapp_code [code, code inline]:
    1.17 +  "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
    1.18 +  by (simp only: valapp_def fst_conv snd_conv)
    1.19  
    1.20  
    1.21  subsubsection {* @{text term_of} instances *}
    1.22 @@ -145,8 +145,11 @@
    1.23  
    1.24  subsubsection {* Syntax *}
    1.25  
    1.26 -definition termify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
    1.27 -  [code del]: "termify x = (x, \<lambda>u. dummy_term)"
    1.28 +definition termify :: "'a \<Rightarrow> term" where
    1.29 +  [code del]: "termify x = dummy_term"
    1.30 +
    1.31 +abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
    1.32 +  "valtermify x \<equiv> (x, \<lambda>u. termify x)"
    1.33  
    1.34  setup {*
    1.35  let
    1.36 @@ -159,8 +162,7 @@
    1.37    fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
    1.38          if not (Term.has_abs t)
    1.39          then if fold_aterms (fn Const _ => I | _ => K false) t true
    1.40 -          then SOME (HOLogic.mk_prod
    1.41 -            (t, Abs ("u", HOLogic.unitT, HOLogic.reflect_term t)))
    1.42 +          then SOME (HOLogic.reflect_term t)
    1.43            else error "Cannot termify expression containing variables"
    1.44          else error "Cannot termify expression containing abstraction"
    1.45      | subst_termify_app (t, ts) = case map_default subst_termify ts
    1.46 @@ -180,13 +182,41 @@
    1.47  locale term_syntax
    1.48  begin
    1.49  
    1.50 -notation app (infixl "<\<cdot>>" 70) and termify ("termify")
    1.51 +notation App (infixl "<\<cdot>>" 70)
    1.52 +  and valapp (infixl "{\<cdot>}" 70)
    1.53  
    1.54  end
    1.55  
    1.56  interpretation term_syntax .
    1.57  
    1.58 -no_notation app (infixl "<\<cdot>>" 70) and termify ("termify")
    1.59 +no_notation App (infixl "<\<cdot>>" 70)
    1.60 +  and valapp (infixl "{\<cdot>}" 70)
    1.61 +
    1.62 +
    1.63 +subsection {* Numeric types *}
    1.64 +
    1.65 +definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
    1.66 +  "term_of_num two = (\<lambda>_. dummy_term)"
    1.67 +
    1.68 +lemma (in term_syntax) term_of_num_code [code]:
    1.69 +  "term_of_num two k = (if k = 0 then termify Int.Pls
    1.70 +    else (if k mod two = 0
    1.71 +      then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
    1.72 +      else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
    1.73 +  by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
    1.74 +
    1.75 +lemma (in term_syntax) term_of_nat_code [code]:
    1.76 +  "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
    1.77 +  by (simp only: term_of_anything)
    1.78 +
    1.79 +lemma (in term_syntax) term_of_int_code [code]:
    1.80 +  "term_of (k::int) = (if k = 0 then termify (0 :: int)
    1.81 +    else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
    1.82 +      else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
    1.83 +  by (simp only: term_of_anything)
    1.84 +
    1.85 +
    1.86 +subsection {* Obfuscate *}
    1.87  
    1.88  print_translation {*
    1.89  let
    1.90 @@ -200,9 +230,8 @@
    1.91  end
    1.92  *}
    1.93  
    1.94 -hide const dummy_term termify app
    1.95 -hide (open) const Const App term_of
    1.96 -
    1.97 +hide const dummy_term App valapp
    1.98 +hide (open) const Const termify valtermify term_of term_of_num
    1.99  
   1.100  
   1.101  subsection {* Evaluation setup *}