equal
deleted
inserted
replaced
1 (* Title: Cube/Cube.thy |
1 (* Title: Cube/Cube.thy |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 *) |
3 *) |
4 |
4 |
5 header {* Barendregt's Lambda-Cube *} |
5 header \<open>Barendregt's Lambda-Cube\<close> |
6 |
6 |
7 theory Cube |
7 theory Cube |
8 imports Pure |
8 imports Pure |
9 begin |
9 begin |
10 |
10 |
52 "A \<rightarrow> B" => "CONST Prod(A, %_. B)" |
52 "A \<rightarrow> B" => "CONST Prod(A, %_. B)" |
53 |
53 |
54 syntax (xsymbols) |
54 syntax (xsymbols) |
55 "_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10) |
55 "_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10) |
56 |
56 |
57 print_translation {* |
57 print_translation \<open> |
58 [(@{const_syntax Prod}, |
58 [(@{const_syntax Prod}, |
59 fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] |
59 fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] |
60 *} |
60 \<close> |
61 |
61 |
62 axiomatization where |
62 axiomatization where |
63 s_b: "*: \<box>" and |
63 s_b: "*: \<box>" and |
64 |
64 |
65 strip_s: "[| A:*; a:A ==> G \<turnstile> x:X |] ==> a:A G \<turnstile> x:X" and |
65 strip_s: "[| A:*; a:A ==> G \<turnstile> x:X |] ==> a:A G \<turnstile> x:X" and |