author | paulson |
Tue, 20 Jun 2000 11:52:38 +0200 | |
changeset 9091 | 8ae7a2e5119b |
parent 4502 | 337c073de95e |
permissions | -rw-r--r-- |
2520 | 1 |
(* Title: HOL/W0/MiniML.thy |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
3 |
Author: Dieter Nazareth and Tobias Nipkow |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
4 |
Copyright 1995 TU Muenchen |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
5 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
6 |
Mini_ML with type inference rules. |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
7 |
*) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
8 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
9 |
MiniML = Type + |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
10 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
11 |
(* expressions *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
12 |
datatype |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
13 |
expr = Var nat | Abs expr | App expr expr |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
14 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
15 |
(* type inference rules *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
16 |
consts |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
17 |
has_type :: "(typ list * expr * typ)set" |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
18 |
syntax |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
19 |
"@has_type" :: [typ list, expr, typ] => bool |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
20 |
("((_) |-/ (_) :: (_))" [60,0,60] 60) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
21 |
translations |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
22 |
"a |- e :: t" == "(a,e,t):has_type" |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
23 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
24 |
inductive has_type |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
25 |
intrs |
4502 | 26 |
VarI "[| n < length a |] ==> a |- Var n :: a!n" |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
27 |
AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2" |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
28 |
AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
29 |
==> a |- App e1 e2 :: t1" |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
30 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
31 |
end |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
32 |