| author | oheimb |
| Fri, 02 Jun 2000 17:46:32 +0200 | |
| changeset 9020 | 1056cbbaeb29 |
| 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 |