src/HOL/MiniML/MiniML.thy
author nipkow
Mon, 11 Dec 1995 11:24:51 +0100
changeset 1402 b72ccd1cff02
parent 1400 5d909faf0e04
child 1476 608483c2122a
permissions -rw-r--r--
layout
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/MiniML.thy
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     2
   ID:        $Id$
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     3
   Author:    Dieter Nazareth and Tobias Nipkow
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     4
   Copyright  1995 TU Muenchen
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     5
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     6
Mini_ML with type inference rules.
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     7
*)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     8
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     9
MiniML = Type + 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    10
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    11
(* expressions *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    12
datatype
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    13
	expr = Var nat | Abs expr | App expr expr
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    14
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    15
(* type inference rules *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    16
consts
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    17
	has_type :: "(typ list * expr * typ)set"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    18
syntax
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    19
        "@has_type" :: [typ list, expr, typ] => bool
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    20
                       ("((_) |-/ (_) :: (_))" 60)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    21
translations 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    22
        "a |- e :: t" == "(a,e,t):has_type"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    23
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    24
inductive "has_type"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    25
intrs
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    26
	VarI "[| n < length a |] ==> a |- Var n :: nth n a"
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    27
	AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    28
	AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    29
     	      ==> a |- App e1 e2 :: t1"
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    30
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    31
end
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    32