|
1 (* Title: Cube/cube.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Barendregt's Lambda-Cube |
|
7 *) |
|
8 |
|
9 Cube = Pure + |
|
10 |
|
11 types |
|
12 term, context, typing 0 |
|
13 |
|
14 arities |
|
15 term :: logic |
|
16 |
|
17 consts |
|
18 Abs, Prod :: "[term, term => term] => term" |
|
19 Trueprop :: "[context, typing] => prop" ("(_/ |- _)") |
|
20 Trueprop1 :: "typing => prop" ("(_)") |
|
21 MT_context :: "context" ("") |
|
22 "" :: "id => context" ("_ ") |
|
23 "" :: "var => context" ("_ ") |
|
24 Context :: "[typing, context] => context" ("_ _") |
|
25 star :: "term" ("*") |
|
26 box :: "term" ("[]") |
|
27 "^" :: "[term, term] => term" (infixl 20) |
|
28 Lam :: "[id, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10) |
|
29 Pi :: "[id, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10) |
|
30 "->" :: "[term, term] => term" (infixr 10) |
|
31 Has_type :: "[term, term] => typing" ("(_:/ _)" [0, 0] 5) |
|
32 |
|
33 translations |
|
34 (prop) "x:X" == (prop) "|- x:X" |
|
35 "Lam x:A. B" == "Abs(A, %x. B)" |
|
36 "Pi x:A. B" => "Prod(A, %x. B)" |
|
37 |
|
38 rules |
|
39 s_b "*: []" |
|
40 |
|
41 strip_s "[| A:*; a:A ==> G |- x:X |] ==> a:A G |- x:X" |
|
42 strip_b "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X" |
|
43 |
|
44 app "[| F:Prod(A, B); C:A |] ==> F^C: B(C)" |
|
45 |
|
46 pi_ss "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*" |
|
47 |
|
48 lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \ |
|
49 \ ==> Abs(A, f) : Prod(A, B)" |
|
50 |
|
51 beta "Abs(A, f)^a == f(a)" |
|
52 |
|
53 end |
|
54 |
|
55 |
|
56 ML |
|
57 |
|
58 val parse_translation = [("op ->", ndependent_tr "Prod")]; |
|
59 val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))]; |
|
60 |