| author | haftmann |
| Fri, 14 Oct 2011 18:55:29 +0200 | |
| changeset 45143 | aed8f14bf562 |
| parent 42284 | 326f57825e1a |
| child 45241 | 87950f752099 |
| permissions | -rw-r--r-- |
| 22809 | 1 |
(* Title: Cube/Cube.thy |
2 |
Author: Tobias Nipkow |
|
3 |
*) |
|
| 3773 | 4 |
|
| 17252 | 5 |
header {* Barendregt's Lambda-Cube *}
|
6 |
||
7 |
theory Cube |
|
8 |
imports Pure |
|
9 |
begin |
|
10 |
||
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
35256
diff
changeset
|
11 |
setup Pure_Thy.old_appl_syntax_setup |
|
26956
1309a6a0a29f
setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
wenzelm
parents:
24783
diff
changeset
|
12 |
|
| 17252 | 13 |
typedecl "term" |
14 |
typedecl "context" |
|
15 |
typedecl typing |
|
16 |
||
|
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
39557
diff
changeset
|
17 |
nonterminal context' and typing' |
| 17252 | 18 |
|
19 |
consts |
|
| 35256 | 20 |
Abs :: "[term, term => term] => term" |
21 |
Prod :: "[term, term => term] => term" |
|
22 |
Trueprop :: "[context, typing] => prop" |
|
23 |
MT_context :: "context" |
|
24 |
Context :: "[typing, context] => context" |
|
25 |
star :: "term" ("*")
|
|
26 |
box :: "term" ("[]")
|
|
27 |
app :: "[term, term] => term" (infixl "^" 20) |
|
28 |
Has_type :: "[term, term] => typing" |
|
| 17252 | 29 |
|
30 |
syntax |
|
| 35256 | 31 |
"\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ |- _)")
|
32 |
"_Trueprop1" :: "typing' => prop" ("(_)")
|
|
33 |
"" :: "id => context'" ("_")
|
|
34 |
"" :: "var => context'" ("_")
|
|
35 |
"\<^const>Cube.MT_context" :: "context'" ("")
|
|
36 |
"\<^const>Cube.Context" :: "[typing', context'] => context'" ("_ _")
|
|
37 |
"\<^const>Cube.Has_type" :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5)
|
|
38 |
"_Lam" :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
|
|
39 |
"_Pi" :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
|
|
40 |
"_arrow" :: "[term, term] => term" (infixr "->" 10) |
|
| 17252 | 41 |
|
42 |
translations |
|
| 17260 | 43 |
("prop") "x:X" == ("prop") "|- x:X"
|
| 35256 | 44 |
"Lam x:A. B" == "CONST Abs(A, %x. B)" |
45 |
"Pi x:A. B" => "CONST Prod(A, %x. B)" |
|
46 |
"A -> B" => "CONST Prod(A, %_. B)" |
|
| 17252 | 47 |
|
48 |
syntax (xsymbols) |
|
| 35256 | 49 |
"\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ \<turnstile> _)")
|
50 |
"\<^const>Cube.box" :: "term" ("\<box>")
|
|
51 |
"_Lam" :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
|
|
52 |
"_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
|
|
53 |
"_arrow" :: "[term, term] => term" (infixr "\<rightarrow>" 10) |
|
| 17252 | 54 |
|
| 35113 | 55 |
print_translation {*
|
| 42284 | 56 |
[(@{const_syntax Prod},
|
57 |
Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
|
|
| 35113 | 58 |
*} |
| 17252 | 59 |
|
60 |
axioms |
|
61 |
s_b: "*: []" |
|
62 |
||
63 |
strip_s: "[| A:*; a:A ==> G |- x:X |] ==> a:A G |- x:X" |
|
64 |
strip_b: "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X" |
|
65 |
||
66 |
app: "[| F:Prod(A, B); C:A |] ==> F^C: B(C)" |
|
| 0 | 67 |
|
| 17252 | 68 |
pi_ss: "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*" |
69 |
||
70 |
lam_ss: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] |
|
71 |
==> Abs(A, f) : Prod(A, B)" |
|
72 |
||
73 |
beta: "Abs(A, f)^a == f(a)" |
|
74 |
||
75 |
lemmas simple = s_b strip_s strip_b app lam_ss pi_ss |
|
76 |
lemmas rules = simple |
|
77 |
||
78 |
lemma imp_elim: |
|
79 |
assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P" |
|
| 41526 | 80 |
shows "PROP P" by (rule app assms)+ |
| 17252 | 81 |
|
82 |
lemma pi_elim: |
|
83 |
assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P" |
|
| 41526 | 84 |
shows "PROP P" by (rule app assms)+ |
| 17252 | 85 |
|
86 |
||
87 |
locale L2 = |
|
88 |
assumes pi_bs: "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*" |
|
89 |
and lam_bs: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] |
|
90 |
==> Abs(A,f) : Prod(A,B)" |
|
91 |
||
92 |
lemmas (in L2) rules = simple lam_bs pi_bs |
|
93 |
||
| 17260 | 94 |
|
| 17252 | 95 |
locale Lomega = |
96 |
assumes |
|
97 |
pi_bb: "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]" |
|
98 |
and lam_bb: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] |
|
99 |
==> Abs(A,f) : Prod(A,B)" |
|
100 |
||
101 |
lemmas (in Lomega) rules = simple lam_bb pi_bb |
|
102 |
||
103 |
||
104 |
locale LP = |
|
105 |
assumes pi_sb: "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]" |
|
106 |
and lam_sb: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] |
|
107 |
==> Abs(A,f) : Prod(A,B)" |
|
108 |
||
109 |
lemmas (in LP) rules = simple lam_sb pi_sb |
|
110 |
||
| 17260 | 111 |
|
| 17252 | 112 |
locale LP2 = LP + L2 |
113 |
||
114 |
lemmas (in LP2) rules = simple lam_bs pi_bs lam_sb pi_sb |
|
115 |
||
| 17260 | 116 |
|
| 17252 | 117 |
locale Lomega2 = L2 + Lomega |
118 |
||
119 |
lemmas (in Lomega2) rules = simple lam_bs pi_bs lam_bb pi_bb |
|
120 |
||
| 17260 | 121 |
|
| 17252 | 122 |
locale LPomega = LP + Lomega |
123 |
||
124 |
lemmas (in LPomega) rules = simple lam_bb pi_bb lam_sb pi_sb |
|
125 |
||
| 17260 | 126 |
|
| 17252 | 127 |
locale CC = L2 + LP + Lomega |
128 |
||
129 |
lemmas (in CC) rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb |
|
130 |
||
131 |
end |