src/HOL/MiniML/MiniML.thy
changeset 2525 477c05586286
parent 1790 2f3694c50101
child 4502 337c073de95e
equal deleted inserted replaced
2524:dd0f298b024c 2525:477c05586286
     1 (* Title:     HOL/MiniML/MiniML.thy
     1 (* Title:     HOL/MiniML/MiniML.thy
     2    ID:        $Id$
     2    ID:        $Id$
     3    Author:    Dieter Nazareth and Tobias Nipkow
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1995 TU Muenchen
     4    Copyright  1996 TU Muenchen
     5 
     5 
     6 Mini_ML with type inference rules.
     6 Mini_ML with type inference rules.
     7 *)
     7 *)
     8 
     8 
     9 MiniML = Type + 
     9 MiniML = Generalize + 
    10 
    10 
    11 (* expressions *)
    11 (* expressions *)
    12 datatype
    12 datatype
    13         expr = Var nat | Abs expr | App expr expr
    13         expr = Var nat | Abs expr | App expr expr | LET expr expr
    14 
    14 
    15 (* type inference rules *)
    15 (* type inference rules *)
    16 consts
    16 consts
    17         has_type :: "(typ list * expr * typ)set"
    17         has_type :: "(ctxt * expr * typ)set"
    18 syntax
    18 syntax
    19         "@has_type" :: [typ list, expr, typ] => bool
    19         "@has_type" :: [ctxt, expr, typ] => bool
    20                        ("((_) |-/ (_) :: (_))" [60,0,60] 60)
    20                        ("((_) |-/ (_) :: (_))" [60,0,60] 60)
    21 translations 
    21 translations 
    22         "a |- e :: t" == "(a,e,t):has_type"
    22         "A |- e :: t" == "(A,e,t):has_type"
    23 
    23 
    24 inductive has_type
    24 inductive has_type
    25 intrs
    25 intrs
    26         VarI "[| n < length a |] ==> a |- Var n :: nth n a"
    26         VarI "[| n < length A; t <| (nth n A) |] ==> A |- Var n :: t"
    27         AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
    27         AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2"
    28         AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
    28         AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] 
    29               ==> a |- App e1 e2 :: t1"
    29               ==> A |- App e1 e2 :: t1"
       
    30         LETI "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t"
    30 
    31 
    31 end
    32 end
    32