| author | wenzelm |
| Mon, 07 Jan 2002 18:30:43 +0100 | |
| changeset 12653 | a55c066624eb |
| parent 12110 | f8b4b11cd79d |
| child 14773 | 556d9cc73711 |
| permissions | -rw-r--r-- |
| 4583 | 1 |
(* Title: Cube/Base.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Barendregt's Lambda-Cube. |
|
7 |
*) |
|
8 |
||
9 |
Base = Pure + |
|
10 |
||
11 |
types |
|
12 |
term context typing |
|
13 |
||
14 |
arities |
|
15 |
term :: logic |
|
16 |
||
17 |
consts |
|
18 |
Abs, Prod :: "[term, term => term] => term" |
|
19 |
Trueprop :: "[context, typing] => prop" ("(_/ |- _)")
|
|
20 |
MT_context :: "context" ("")
|
|
21 |
Context :: "[typing, context] => context" ("_ _")
|
|
22 |
star :: "term" ("*")
|
|
23 |
box :: "term" ("[]")
|
|
24 |
"^" :: "[term, term] => term" (infixl 20) |
|
25 |
Has_type :: "[term, term] => typing" ("(_:/ _)" [0, 0] 5)
|
|
26 |
||
27 |
syntax |
|
28 |
Trueprop1 :: "typing => prop" ("(_)")
|
|
29 |
"" :: "id => context" ("_ ")
|
|
30 |
"" :: "var => context" ("_ ")
|
|
31 |
Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
|
|
32 |
Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
|
|
33 |
"->" :: "[term, term] => term" (infixr 10) |
|
34 |
||
35 |
translations |
|
36 |
(prop) "x:X" == (prop) "|- x:X" |
|
37 |
"Lam x:A. B" == "Abs(A, %x. B)" |
|
38 |
"Pi x:A. B" => "Prod(A, %x. B)" |
|
39 |
"A -> B" => "Prod(A, _K(B))" |
|
40 |
||
|
12110
f8b4b11cd79d
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
4584
diff
changeset
|
41 |
syntax (xsymbols) |
| 4584 | 42 |
Trueprop :: "[context, typing] => prop" ("(_/ \\<turnstile> _)")
|
43 |
box :: "term" ("\\<box>")
|
|
44 |
Lam :: "[idt, term, term] => term" ("(3\\<Lambda>_:_./ _)" [0, 0, 0] 10)
|
|
45 |
Pi :: "[idt, term, term] => term" ("(3\\<Pi>_:_./ _)" [0, 0] 10)
|
|
46 |
"op ->" :: "[term, term] => term" (infixr "\\<rightarrow>" 10) |
|
47 |
||
48 |
||
| 4583 | 49 |
rules |
50 |
s_b "*: []" |
|
51 |
||
52 |
strip_s "[| A:*; a:A ==> G |- x:X |] ==> a:A G |- x:X" |
|
53 |
strip_b "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X" |
|
54 |
||
55 |
app "[| F:Prod(A, B); C:A |] ==> F^C: B(C)" |
|
56 |
||
57 |
pi_ss "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*" |
|
58 |
||
59 |
lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] |
|
60 |
==> Abs(A, f) : Prod(A, B)" |
|
61 |
||
62 |
beta "Abs(A, f)^a == f(a)" |
|
63 |
||
64 |
end |
|
65 |
||
66 |
||
67 |
ML |
|
68 |
||
69 |
val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
|
|
70 |