(* Title: Cube/Cube.thy Author: Tobias Nipkow \<open>Barendregt's Lambda-Cube\<close> theory Cubeimports Purebegin setup Pure_Thy.old_appl_syntax_setup"Cube inference rules" typedecl "term" typedecl "context" typedecl typingaxiomatization "[term, term \ term] \ term" and "[term, term \ term] \ term" and "[context, typing] \ prop" and "context" and Context :: "[typing, context] \ context" and "term" (\<open>*\<close>) and "term" (\<open>\<box>\<close>) and "[term, term] \ term" (infixl \\\ 20) and "[term, term] \ typing" context ' and typing' syntax "_Trueprop" :: "[context', typing'] \ prop" (\(\notation=judgment\_/ \ _)\) "_Trueprop1" :: "typing' \ prop" (\(\notation=judgment\_)\) "" :: "id \ context'" (\_\) "" :: "var \ context'" (\_\) "_MT_context" :: "context'" (\<open>\<close>) "_Context" :: "[typing', context'] \ context'" (\_ _\) "_Has_type" :: "[term, term] \ typing'" (\(\notation=\infix Has_Type\\_:/ _)\ [0, 0] 5) "_Lam" :: "[idt, term, term] \ term" (\(\indent=3 notation=\binder \<^bold>\\\\<^bold>\_:_./ _)\ [0, 0, 0] 10) "_Pi" :: "[idt, term, term] \ term" (\(\indent=3 notation=\binder \\\\_:_./ _)\ [0, 0] 10) "_arrow" :: "[term, term] \ term" (infixr \\\ 10) "_Trueprop" \<rightleftharpoons> Trueprop and "_MT_context" \<rightleftharpoons> MT_context and "_Context" \<rightleftharpoons> Context and "_Has_type" \<rightleftharpoons> Has_type and "_Lam" \<rightleftharpoons> Abs and "_Pi" "_arrow" \<rightleftharpoons> Prod 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>, ' (\<^syntax_const>\_Pi\, \<^syntax_const>\_arrow\))] \<close> axiomatization where "*: \" and "\A:*; a:A \ G \ x:X\ \ a:A G \ x:X" and "\A:\; a:A \ G \ x:X\ \ a:A G \ x:X" and "\F:Prod(A, B); C:A\ \ F\C: B(C)" and "\A:*; \x. x:A \ B(x):*\ \ Prod(A, B):*" and "\A:*; \x. x:A \ f(x):B(x); \x. x:A \ B(x):* \ \<Longrightarrow> Abs(A, f) : Prod(A, B)" and "Abs(A, f)\a \ f(a)" lemmas [rules] = s_b strip_s strip_b app lam_ss pi_sslemma 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_bsend locale Lomega =assumes "\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_bbend 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_sbend locale LP2 = LP + L2begin lemmas [rules] = lam_bs pi_bs lam_sb pi_sbend locale Lomega2 = L2 + Lomegabegin lemmas [rules] = lam_bs pi_bs lam_bb pi_bbend locale LPomega = LP + Lomegabegin lemmas [rules] = lam_bb pi_bb lam_sb pi_sbend locale CC = L2 + LP + Lomegabegin lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sbend end quality 96%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
