# HG changeset patch # User haftmann # Date 1197910668 -3600 # Node ID f46ed5b333fd72a89f38fd88e6d527d648245e15 # Parent faabc08af8822004049b8999e0a78577cf412da8 improved term syntax diff -r faabc08af882 -r f46ed5b333fd src/HOL/Library/Eval.thy --- 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\prop itself) = STR ''prop'' {\} []" +definition + "typ_of (T\prop itself) = Type (STR ''prop'') []" instance .. @@ -64,7 +64,7 @@ begin definition - "typ_of (T\'a itself itself) = STR ''itself'' {\} [typ_of TYPE('a\typ_of)]" + "typ_of (T\'a itself itself) = Type (STR ''itself'') [typ_of TYPE('a\typ_of)]" instance .. @@ -74,7 +74,7 @@ begin definition - "typ_of (T\'a set itself) = STR ''set'' {\} [typ_of TYPE('a\typ_of)]" + "typ_of (T\'a set itself) = Type (STR ''set'') [typ_of TYPE('a\typ_of)]" instance .. @@ -172,17 +172,17 @@ in DatatypePackage.interpretation interpretator end *} -abbreviation +abbreviation (in pure_term_syntax) (input) intT :: "typ" where - "intT \ STR ''IntDef.int'' {\} []" + "intT \ Type (STR ''IntDef.int'') []" -abbreviation +abbreviation (in pure_term_syntax) (input) bitT :: "typ" where - "bitT \ STR ''Numeral.bit'' {\} []" + "bitT \ Type (STR ''Numeral.bit'') []" -function +function (in pure_term_syntax) mk_int :: "int \ term" where "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \\ intT @@ -191,13 +191,21 @@ in STR ''Numeral.Bit'' \\ intT \ bitT \ intT \ mk_int l \ (if m = 0 then STR ''Numeral.bit.B0'' \\ bitT else STR ''Numeral.bit.B1'' \\ 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'' \\ intT \ intT \ 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'' \\ intT \ intT \ mk_int k" + "term_of = pure_term_syntax.term_of_int_aux" instance .. diff -r faabc08af882 -r f46ed5b333fd src/HOL/Library/Pure_term.thy --- 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 "{\}" 120) - | TFix vname sort (infix "\\" 117) + Type message_string "typ list" + | TFree vname sort abbreviation - Fun :: "typ \ typ \ typ" (infixr "\" 115) where - "ty1 \ ty2 \ Type (STR ''fun'') [ty1, ty2]" -abbreviation - Funs :: "typ list \ typ \ typ" (infixr "{\}" 115) where - "tys {\} ty \ foldr (op \) tys ty" + Fun :: "typ \ typ \ typ" where + "Fun ty1 ty2 \ Type (STR ''fun'') [ty1, ty2]" + +locale (open) pure_term_syntax = + fixes pure_term_Type :: "message_string \ typ list \ typ" (infixl "{\}" 120) + and pure_term_TFree :: "vname \ sort \ typ" ("\_\_\" [118, 118] 117) + and pure_term_Fun :: "typ \ typ \ typ" (infixr "\" 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 "{\}" 120) +and + TFree ("\_\_\" [118, 118] 117) +and + Fun (infixr "\" 114) datatype "term" = Const message_string "typ" (infix "\\" 112) @@ -68,7 +92,8 @@ subsection {* Code generator setup *} lemma [code func]: - "tyco1 {\} tys1 = tyco2 {\} tys2 \ tyco1 = tyco2 + includes pure_term_syntax + shows "tyco1 {\} tys1 = tyco2 {\} tys2 \ tyco1 = tyco2 \ 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