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