src/HOL/MiniML/MiniML.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 4502 337c073de95e
child 14422 b8da5f258b04
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
nipkow@1300
     1
(* Title:     HOL/MiniML/MiniML.thy
nipkow@1300
     2
   ID:        $Id$
nipkow@2525
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
nipkow@2525
     4
   Copyright  1996 TU Muenchen
nipkow@1300
     5
nipkow@1300
     6
Mini_ML with type inference rules.
nipkow@1300
     7
*)
nipkow@1300
     8
nipkow@2525
     9
MiniML = Generalize + 
nipkow@1300
    10
nipkow@1300
    11
(* expressions *)
nipkow@1300
    12
datatype
nipkow@2525
    13
        expr = Var nat | Abs expr | App expr expr | LET expr expr
nipkow@1300
    14
nipkow@1300
    15
(* type inference rules *)
nipkow@1300
    16
consts
nipkow@2525
    17
        has_type :: "(ctxt * expr * typ)set"
nipkow@1300
    18
syntax
nipkow@2525
    19
        "@has_type" :: [ctxt, expr, typ] => bool
nipkow@1525
    20
                       ("((_) |-/ (_) :: (_))" [60,0,60] 60)
nipkow@1300
    21
translations 
nipkow@2525
    22
        "A |- e :: t" == "(A,e,t):has_type"
nipkow@1300
    23
paulson@1790
    24
inductive has_type
nipkow@1300
    25
intrs
nipkow@4502
    26
        VarI "[| n < length A; t <| A!n |] ==> A |- Var n :: t"
nipkow@2525
    27
        AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2"
nipkow@2525
    28
        AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] 
nipkow@2525
    29
              ==> A |- App e1 e2 :: t1"
nipkow@2525
    30
        LETI "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t"
nipkow@1300
    31
nipkow@1300
    32
end