author | kleing |
Fri, 27 May 2005 01:09:44 +0200 | |
changeset 16095 | f6af6b265d20 |
parent 14854 | 61bdf2ae4dc5 |
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 |
|
14773
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
12 |
term |
4583 | 13 |
|
14773
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
14 |
types |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
15 |
context typing |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
16 |
nonterminals |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
17 |
context_ typing_ |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
18 |
|
4583 | 19 |
consts |
20 |
Abs, Prod :: "[term, term => term] => term" |
|
14773
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
21 |
Trueprop :: "[context, typing] => prop" |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
22 |
MT_context :: "context" |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
23 |
Context :: "[typing, context] => context" |
4583 | 24 |
star :: "term" ("*") |
25 |
box :: "term" ("[]") |
|
26 |
"^" :: "[term, term] => term" (infixl 20) |
|
14773
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
27 |
Has_type :: "[term, term] => typing" |
4583 | 28 |
|
29 |
syntax |
|
14773
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
30 |
Trueprop :: "[context_, typing_] => prop" ("(_/ |- _)") |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
31 |
Trueprop1 :: "typing_ => prop" ("(_)") |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
32 |
"" :: "id => context_" ("_") |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
33 |
"" :: "var => context_" ("_") |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
34 |
MT_context :: "context_" ("") |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
35 |
Context :: "[typing_, context_] => context_" ("_ _") |
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
36 |
Has_type :: "[term, term] => typing_" ("(_:/ _)" [0, 0] 5) |
4583 | 37 |
Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10) |
38 |
Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10) |
|
39 |
"->" :: "[term, term] => term" (infixr 10) |
|
40 |
||
41 |
translations |
|
42 |
(prop) "x:X" == (prop) "|- x:X" |
|
43 |
"Lam x:A. B" == "Abs(A, %x. B)" |
|
44 |
"Pi x:A. B" => "Prod(A, %x. B)" |
|
45 |
"A -> B" => "Prod(A, _K(B))" |
|
46 |
||
12110
f8b4b11cd79d
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
4584
diff
changeset
|
47 |
syntax (xsymbols) |
14773
556d9cc73711
adapted syntax to cope with lack of non-logical types;
wenzelm
parents:
12110
diff
changeset
|
48 |
Trueprop :: "[context_, typing_] => prop" ("(_/ \\<turnstile> _)") |
4584 | 49 |
box :: "term" ("\\<box>") |
50 |
Lam :: "[idt, term, term] => term" ("(3\\<Lambda>_:_./ _)" [0, 0, 0] 10) |
|
51 |
Pi :: "[idt, term, term] => term" ("(3\\<Pi>_:_./ _)" [0, 0] 10) |
|
52 |
"op ->" :: "[term, term] => term" (infixr "\\<rightarrow>" 10) |
|
53 |
||
54 |
||
4583 | 55 |
rules |
56 |
s_b "*: []" |
|
57 |
||
58 |
strip_s "[| A:*; a:A ==> G |- x:X |] ==> a:A G |- x:X" |
|
59 |
strip_b "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X" |
|
60 |
||
61 |
app "[| F:Prod(A, B); C:A |] ==> F^C: B(C)" |
|
62 |
||
63 |
pi_ss "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*" |
|
64 |
||
65 |
lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] |
|
66 |
==> Abs(A, f) : Prod(A, B)" |
|
67 |
||
68 |
beta "Abs(A, f)^a == f(a)" |
|
69 |
||
70 |
end |
|
71 |
||
72 |
||
73 |
ML |
|
74 |
||
75 |
val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))]; |
|
76 |