src/HOL/Library/Pure_term.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 23063 b4ee6ec4f9c6
child 23854 688a8a7bcd4e
permissions -rw-r--r--
tuned Proof
     1 (*  Title:      HOL/Library/Pure_term.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 header {* Embedding (a subset of) the Pure term algebra in HOL *}
     7 
     8 theory Pure_term
     9 imports MLString
    10 begin
    11 
    12 subsection {* Definitions *}
    13 
    14 types vname = ml_string;
    15 types "class" = ml_string;
    16 types sort = "class list"
    17 
    18 datatype "typ" =
    19     Type ml_string "typ list" (infix "{\<struct>}" 120)
    20   | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
    21 
    22 abbreviation
    23   Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) where
    24   "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
    25 abbreviation
    26   Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) where
    27   "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
    28 
    29 datatype "term" =
    30     Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112)
    31   | Fix   vname "typ" (infix ":\<epsilon>" 112)
    32   | App   "term" "term" (infixl "\<bullet>" 110)
    33   | Abs   "vname \<times> typ" "term" (infixr "\<mapsto>" 111)
    34   | Bnd   nat
    35 
    36 abbreviation
    37   Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where
    38   "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
    39 abbreviation
    40   Abss :: "(vname \<times> typ) list \<Rightarrow> term \<Rightarrow> term" (infixr "{\<mapsto>}" 111) where
    41   "vs {\<mapsto>} t \<equiv> foldr (op \<mapsto>) vs t"
    42 
    43 
    44 subsection {* ML interface *}
    45 
    46 ML {*
    47 structure Pure_term =
    48 struct
    49 
    50 val mk_sort = HOLogic.mk_list @{typ class} o map MLString.mk;
    51 
    52 fun mk_typ f (Type (tyco, tys)) =
    53       @{term Type} $ MLString.mk tyco
    54         $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
    55   | mk_typ f (TFree v) =
    56       f v;
    57 
    58 fun mk_term f g (Const (c, ty)) =
    59       @{term Const} $ MLString.mk c $ g ty
    60   | mk_term f g (t1 $ t2) =
    61       @{term App} $ mk_term f g t1 $ mk_term f g t2
    62   | mk_term f g (Free v) = f v;
    63 
    64 end;
    65 *}
    66 
    67 
    68 subsection {* Code generator setup *}
    69 
    70 lemma [code func]:
    71   "tyco1 {\<struct>} tys1 = tyco2 {\<struct>} tys2 \<longleftrightarrow> tyco1 = tyco2
    72      \<and> list_all2 (op =) tys1 tys2"
    73   by (auto simp add: list_all2_eq [symmetric])
    74 
    75 code_datatype Const App Fix
    76 
    77 lemmas [code func del] = term.recs term.cases term.size
    78 lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
    79 
    80 code_type "typ" and "term"
    81   (SML "Term.typ" and "Term.term")
    82 
    83 code_const Type and TFix
    84   (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)")
    85 
    86 code_const Const and App and Fix
    87   (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)")
    88  
    89 code_reserved SML Term
    90 
    91 end