(* Title: Cube/Cube.thy Author: Tobias Nipkow *) section \Barendregt's Lambda-Cube\ 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)" \ "CONST Trueprop(G, t)" ("prop") "x:X" \ ("prop") "\ x:X" "_MT_context" \ "CONST MT_context" "_Context" \ "CONST Context" "_Has_type" \ "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)" syntax "_Pi" :: "[idt, term, term] \ term" ("(3\_:_./ _)" [0, 0] 10) print_translation \ [(@{const_syntax Prod}, fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] \ 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):* \ \ 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):*\ \ 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):\\ \ 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):\\ \ 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