improved term syntax

--- a/src/HOL/Library/Eval.thy	Mon Dec 17 17:01:54 2007 +0100
+++ b/src/HOL/Library/Eval.thy	Mon Dec 17 17:57:48 2007 +0100
@@ -53,8 +53,8 @@
 instantiation "prop" :: typ_of
 begin
 
-definition
-  "typ_of (T\<Colon>prop itself) = STR ''prop'' {\<struct>} []"
+definition 
+  "typ_of (T\<Colon>prop itself) = Type (STR ''prop'') []"
 
 instance ..
 
@@ -64,7 +64,7 @@
 begin
 
 definition
-  "typ_of (T\<Colon>'a itself itself) = STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]"
+  "typ_of (T\<Colon>'a itself itself) = Type (STR ''itself'') [typ_of TYPE('a\<Colon>typ_of)]"
 
 instance ..
 
@@ -74,7 +74,7 @@
 begin
  
 definition
-  "typ_of (T\<Colon>'a set itself) = STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]"
+  "typ_of (T\<Colon>'a set itself) = Type (STR ''set'') [typ_of TYPE('a\<Colon>typ_of)]"
 
 instance ..
 
@@ -172,17 +172,17 @@
   in DatatypePackage.interpretation interpretator end
 *}
 
-abbreviation
+abbreviation (in pure_term_syntax) (input)
   intT :: "typ"
 where
-  "intT \<equiv> STR ''IntDef.int'' {\<struct>} []"
+  "intT \<equiv> Type (STR ''IntDef.int'') []"
 
-abbreviation
+abbreviation (in pure_term_syntax) (input)
   bitT :: "typ"
 where
-  "bitT \<equiv> STR ''Numeral.bit'' {\<struct>} []"
+  "bitT \<equiv> Type (STR ''Numeral.bit'') []"
 
-function
+function (in pure_term_syntax)
   mk_int :: "int \<Rightarrow> term"
 where
   "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT
@@ -191,13 +191,21 @@
   in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
     (if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))"
 by pat_completeness auto
-termination by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
+termination (in pure_term_syntax)
+by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
+
+declare pure_term_syntax.mk_int.simps [code func]
+
+definition (in pure_term_syntax)
+  "term_of_int_aux k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
+
+declare pure_term_syntax.term_of_int_aux_def [code func]
 
 instantiation int :: term_of
 begin
 
 definition
-  "term_of k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
+  "term_of = pure_term_syntax.term_of_int_aux"
 
 instance ..
 

--- a/src/HOL/Library/Pure_term.thy	Mon Dec 17 17:01:54 2007 +0100
+++ b/src/HOL/Library/Pure_term.thy	Mon Dec 17 17:57:48 2007 +0100
@@ -3,28 +3,52 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Embedding (a subset of) the Pure term algebra in HOL *}
+header {* Partial reflection of the Pure term algebra in HOL *}
 
 theory Pure_term
 imports Code_Message
 begin
 
-subsection {* Definitions *}
+subsection {* Definitions and syntax *}
 
 types vname = message_string;
 types "class" = message_string;
 types sort = "class list"
 
 datatype "typ" =
-    Type message_string "typ list" (infix "{\<struct>}" 120)
-  | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
+    Type message_string "typ list"
+  | TFree vname sort  
 
 abbreviation
-  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) where
-  "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
-abbreviation
-  Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) where
-  "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
+  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" where
+  "Fun ty1 ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
+
+locale (open) pure_term_syntax =
+  fixes pure_term_Type :: "message_string \<Rightarrow> typ list \<Rightarrow> typ" (infixl "{\<struct>}" 120)
+    and pure_term_TFree :: "vname \<Rightarrow> sort \<Rightarrow> typ" ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
+    and pure_term_Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 114)
+
+parse_translation {*
+let
+  fun Type_tr [tyco, tys] = Lexicon.const @{const_syntax Type} $ tyco $ tys
+    | Type_tr ts = raise TERM ("Type_tr", ts);
+  fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort
+    | TFree_tr ts = raise TERM ("TFree_tr", ts);
+  fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2
+    | Fun_tr ts = raise TERM("Fun_tr", ts);
+in [
+  ("\\<^fixed>pure_term_Type", Type_tr),
+  ("\\<^fixed>pure_term_TFree", TFree_tr),
+  ("\\<^fixed>pure_term_Fun", Fun_tr)
+] end
+*}
+
+notation (output)
+  Type (infixl "{\<struct>}" 120)
+and
+  TFree ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117)
+and
+  Fun (infixr "\<rightarrow>" 114)
 
 datatype "term" =
     Const message_string "typ" (infix "\<Colon>\<subseteq>" 112)
@@ -68,7 +92,8 @@
 subsection {* Code generator setup *}
 
 lemma [code func]:
-  "tyco1 {\<struct>} tys1 = tyco2 {\<struct>} tys2 \<longleftrightarrow> tyco1 = tyco2
+  includes pure_term_syntax
+  shows "tyco1 {\<struct>} tys1 = tyco2 {\<struct>} tys2 \<longleftrightarrow> tyco1 = tyco2
      \<and> list_all2 (op =) tys1 tys2"
   by (auto simp add: list_all2_eq [symmetric])
 
@@ -80,7 +105,7 @@
 code_type "typ" and "term"
   (SML "Term.typ" and "Term.term")
 
-code_const Type and TFix
+code_const Type and TFree
   (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)")
 
 code_const Const and App and Fix