(* Title: Cube/Cube.thy
Author: Tobias Nipkow
*)
section \<open>Barendregt's Lambda-Cube\<close>
theory Cube
imports Pure
begin
setup Pure_Thy.old_appl_syntax_setup
named_theorems rules "Cube inference rules"
typedecl "term"
typedecl "context"
typedecl typing
axiomatization
Abs :: "[term, term \ term] \ term" and
Prod :: "[term, term \ term] \ term" and
Trueprop :: "[context, typing] \ prop" and
MT_context :: "context" and
Context :: "[typing, context] \ context" and
star :: "term" ("*") and
box :: "term" ("\") and
app :: "[term, term] \ term" (infixl "\" 20) and
Has_type :: "[term, term] \ typing"
nonterminal context' and typing'
syntax
"_Trueprop" :: "[context', typing'] \ prop" ("(_/ \ _)")
"_Trueprop1" :: "typing' \ prop" ("(_)")
"" :: "id \ context'" ("_")
"" :: "var \ context'" ("_")
"_MT_context" :: "context'" ("")
"_Context" :: "[typing', context'] \ context'" ("_ _")
"_Has_type" :: "[term, term] \ typing'" ("(_:/ _)" [0, 0] 5)
"_Lam" :: "[idt, term, term] \ term" ("(3\<^bold>\_:_./ _)" [0, 0, 0] 10)
"_Pi" :: "[idt, term, term] \ term" ("(3\_:_./ _)" [0, 0] 10)
"_arrow" :: "[term, term] \ term" (infixr "\" 10)
translations
"_Trueprop(G, t)" \<rightleftharpoons> "CONST Trueprop(G, t)"
("prop") "x:X" \<rightleftharpoons> ("prop") "\<turnstile> x:X"
"_MT_context" \<rightleftharpoons> "CONST MT_context"
"_Context" \<rightleftharpoons> "CONST Context"
"_Has_type" \<rightleftharpoons> "CONST Has_type"
"\<^bold>\x:A. B" \ "CONST Abs(A, \x. B)"
"\x:A. B" \ "CONST Prod(A, \x. B)"
"A \ B" \ "CONST Prod(A, \_. B)"
print_translation \<open>
[(\<^const_syntax>\<open>Prod\<close>,
fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\_Pi\, \<^syntax_const>\_arrow\))]
\<close>
axiomatization where
s_b: "*: \" and
strip_s: "\A:*; a:A \ G \ x:X\ \ a:A G \ x:X" and
strip_b: "\A:\; a:A \ G \ x:X\ \ a:A G \ x:X" and
app: "\F:Prod(A, B); C:A\ \ F\C: B(C)" and
pi_ss: "\A:*; \x. x:A \ B(x):*\ \ Prod(A, B):*" and
lam_ss: "\A:*; \x. x:A \ f(x):B(x); \x. x:A \ B(x):* \
\<Longrightarrow> Abs(A, f) : Prod(A, B)" and
beta: "Abs(A, f)\a \ f(a)"
lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss
lemma imp_elim:
assumes "f:A\B" and "a:A" and "f\a:B \ PROP P"
shows "PROP P" by (rule app assms)+
lemma pi_elim:
assumes "F:Prod(A,B)" and "a:A" and "F\a:B(a) \ PROP P"
shows "PROP P" by (rule app assms)+
locale L2 =
assumes pi_bs: "\A:\; \x. x:A \ B(x):*\ \ Prod(A,B):*"
and lam_bs: "\A:\; \x. x:A \ f(x):B(x); \x. x:A \ B(x):*\
\<Longrightarrow> Abs(A,f) : Prod(A,B)"
begin
lemmas [rules] = lam_bs pi_bs
end
locale Lomega =
assumes
pi_bb: "\A:\; \x. x:A \ B(x):\\ \ Prod(A,B):\"
and lam_bb: "\A:\; \x. x:A \ f(x):B(x); \x. x:A \ B(x):\\
\<Longrightarrow> Abs(A,f) : Prod(A,B)"
begin
lemmas [rules] = lam_bb pi_bb
end
locale LP =
assumes pi_sb: "\A:*; \x. x:A \ B(x):\\ \ Prod(A,B):\"
and lam_sb: "\A:*; \x. x:A \ f(x):B(x); \x. x:A \ B(x):\\
\<Longrightarrow> Abs(A,f) : Prod(A,B)"
begin
lemmas [rules] = lam_sb pi_sb
end
locale LP2 = LP + L2
begin
lemmas [rules] = lam_bs pi_bs lam_sb pi_sb
end
locale Lomega2 = L2 + Lomega
begin
lemmas [rules] = lam_bs pi_bs lam_bb pi_bb
end
locale LPomega = LP + Lomega
begin
lemmas [rules] = lam_bb pi_bb lam_sb pi_sb
end
locale CC = L2 + LP + Lomega
begin
lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
end
end
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
