| author | wenzelm |
| Wed, 02 Aug 2000 19:40:14 +0200 | |
| changeset 9502 | 50ec59aff389 |
| parent 9114 | de99e37effda |
| child 9622 | d9aa8ca06bc2 |
| permissions | -rw-r--r-- |
|
9114
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Lambda/Type.thy |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
3 |
Author: Stefan Berghofer |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
4 |
Copyright 2000 TU Muenchen |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
5 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
6 |
Simply-typed lambda terms. |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
7 |
*) |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
8 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
9 |
Type = InductTermi + |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
10 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
11 |
datatype typ = Atom nat |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
12 |
| Fun typ typ (infixr "=>" 200) |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
13 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
14 |
consts |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
15 |
typing :: "((nat => typ) * dB * typ) set" |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
16 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
17 |
syntax |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
18 |
"@type" :: "[nat => typ, dB, typ] => bool" ("_ |- _ : _" [50,50,50] 50)
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
19 |
"=>>" :: "[typ list, typ] => typ" (infixl 150) |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
20 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
21 |
translations |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
22 |
"env |- t : T" == "(env, t, T) : typing" |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
23 |
"Ts =>> T" == "foldr Fun Ts T" |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
24 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
25 |
inductive typing |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
26 |
intrs |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
27 |
VAR "env x = T ==> env |- Var x : T" |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
28 |
ABS "(nat_case T env) |- t : U ==> env |- (Abs t) : (T => U)" |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
29 |
APP "[| env |- s : T => U; env |- t : T |] ==> env |- (s $ t) : U" |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
30 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
31 |
consts |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
32 |
"types" :: "[nat => typ, dB list, typ list] => bool" |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
33 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
34 |
primrec |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
35 |
"types e [] Ts = (Ts = [])" |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
36 |
"types e (t # ts) Ts = (case Ts of |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
37 |
[] => False |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
38 |
| T # Ts => e |- t : T & types e ts Ts)" |
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
39 |
|
|
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
40 |
end |