1300

1 
(* Title: HOL/MiniML/MiniML.thy


2 
ID: $Id$

2525

3 
Author: Wolfgang Naraschewski and Tobias Nipkow


4 
Copyright 1996 TU Muenchen

1300

5 


6 
Mini_ML with type inference rules.


7 
*)


8 

2525

9 
MiniML = Generalize +

1300

10 


11 
(* expressions *)


12 
datatype

2525

13 
expr = Var nat  Abs expr  App expr expr  LET expr expr

1300

14 


15 
(* type inference rules *)


16 
consts

2525

17 
has_type :: "(ctxt * expr * typ)set"

1300

18 
syntax

2525

19 
"@has_type" :: [ctxt, expr, typ] => bool

1525

20 
("((_) / (_) :: (_))" [60,0,60] 60)

1300

21 
translations

2525

22 
"A  e :: t" == "(A,e,t):has_type"

1300

23 

1790

24 
inductive has_type

1300

25 
intrs

2525

26 
VarI "[ n < length A; t < (nth n A) ] ==> A  Var n :: t"


27 
AbsI "[ (mk_scheme t1)#A  e :: t2 ] ==> A  Abs e :: t1 > t2"


28 
AppI "[ A  e1 :: t2 > t1; A  e2 :: t2 ]


29 
==> A  App e1 e2 :: t1"


30 
LETI "[ A  e1 :: t1; (gen A t1)#A  e2 :: t ] ==> A  LET e1 e2 :: t"

1300

31 


32 
end
