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