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