1(* Title: Cube/Cube.thy 2 Author: Tobias Nipkow 3*) 4 5section \<open>Barendregt's Lambda-Cube\<close> 6 7theory Cube 8imports Pure 9begin 10 11setup Pure_Thy.old_appl_syntax_setup 12 13named_theorems rules "Cube inference rules" 14 15typedecl "term" 16typedecl "context" 17typedecl typing 18 19axiomatization 20 Abs :: "[term, term \<Rightarrow> term] \<Rightarrow> term" and 21 Prod :: "[term, term \<Rightarrow> term] \<Rightarrow> term" and 22 Trueprop :: "[context, typing] \<Rightarrow> prop" and 23 MT_context :: "context" and 24 Context :: "[typing, context] \<Rightarrow> context" and 25 star :: "term" ("*") and 26 box :: "term" ("\<box>") and 27 app :: "[term, term] \<Rightarrow> term" (infixl "\<cdot>" 20) and 28 Has_type :: "[term, term] \<Rightarrow> typing" 29 30nonterminal context' and typing' 31syntax 32 "_Trueprop" :: "[context', typing'] \<Rightarrow> prop" ("(_/ \<turnstile> _)") 33 "_Trueprop1" :: "typing' \<Rightarrow> prop" ("(_)") 34 "" :: "id \<Rightarrow> context'" ("_") 35 "" :: "var \<Rightarrow> context'" ("_") 36 "_MT_context" :: "context'" ("") 37 "_Context" :: "[typing', context'] \<Rightarrow> context'" ("_ _") 38 "_Has_type" :: "[term, term] \<Rightarrow> typing'" ("(_:/ _)" [0, 0] 5) 39 "_Lam" :: "[idt, term, term] \<Rightarrow> term" ("(3\<^bold>\<lambda>_:_./ _)" [0, 0, 0] 10) 40 "_Pi" :: "[idt, term, term] \<Rightarrow> term" ("(3\<Prod>_:_./ _)" [0, 0] 10) 41 "_arrow" :: "[term, term] \<Rightarrow> term" (infixr "\<rightarrow>" 10) 42translations 43 "_Trueprop(G, t)" \<rightleftharpoons> "CONST Trueprop(G, t)" 44 ("prop") "x:X" \<rightleftharpoons> ("prop") "\<turnstile> x:X" 45 "_MT_context" \<rightleftharpoons> "CONST MT_context" 46 "_Context" \<rightleftharpoons> "CONST Context" 47 "_Has_type" \<rightleftharpoons> "CONST Has_type" 48 "\<^bold>\<lambda>x:A. B" \<rightleftharpoons> "CONST Abs(A, \<lambda>x. B)" 49 "\<Prod>x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)" 50 "A \<rightarrow> B" \<rightharpoonup> "CONST Prod(A, \<lambda>_. B)" 51print_translation \<open> 52 [(\<^const_syntax>\<open>Prod\<close>, 53 fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\<open>_Pi\<close>, \<^syntax_const>\<open>_arrow\<close>))] 54\<close> 55 56axiomatization where 57 s_b: "*: \<box>" and 58 59 strip_s: "\<lbrakk>A:*; a:A \<Longrightarrow> G \<turnstile> x:X\<rbrakk> \<Longrightarrow> a:A G \<turnstile> x:X" and 60 strip_b: "\<lbrakk>A:\<box>; a:A \<Longrightarrow> G \<turnstile> x:X\<rbrakk> \<Longrightarrow> a:A G \<turnstile> x:X" and 61 62 app: "\<lbrakk>F:Prod(A, B); C:A\<rbrakk> \<Longrightarrow> F\<cdot>C: B(C)" and 63 64 pi_ss: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk> \<Longrightarrow> Prod(A, B):*" and 65 66 lam_ss: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):* \<rbrakk> 67 \<Longrightarrow> Abs(A, f) : Prod(A, B)" and 68 69 beta: "Abs(A, f)\<cdot>a \<equiv> f(a)" 70 71lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss 72 73lemma imp_elim: 74 assumes "f:A\<rightarrow>B" and "a:A" and "f\<cdot>a:B \<Longrightarrow> PROP P" 75 shows "PROP P" by (rule app assms)+ 76 77lemma pi_elim: 78 assumes "F:Prod(A,B)" and "a:A" and "F\<cdot>a:B(a) \<Longrightarrow> PROP P" 79 shows "PROP P" by (rule app assms)+ 80 81 82locale L2 = 83 assumes pi_bs: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk> \<Longrightarrow> Prod(A,B):*" 84 and lam_bs: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk> 85 \<Longrightarrow> Abs(A,f) : Prod(A,B)" 86begin 87 88lemmas [rules] = lam_bs pi_bs 89 90end 91 92 93locale Lomega = 94 assumes 95 pi_bb: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk> \<Longrightarrow> Prod(A,B):\<box>" 96 and lam_bb: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk> 97 \<Longrightarrow> Abs(A,f) : Prod(A,B)" 98begin 99 100lemmas [rules] = lam_bb pi_bb 101 102end 103 104 105locale LP = 106 assumes pi_sb: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk> \<Longrightarrow> Prod(A,B):\<box>" 107 and lam_sb: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk> 108 \<Longrightarrow> Abs(A,f) : Prod(A,B)" 109begin 110 111lemmas [rules] = lam_sb pi_sb 112 113end 114 115 116locale LP2 = LP + L2 117begin 118 119lemmas [rules] = lam_bs pi_bs lam_sb pi_sb 120 121end 122 123 124locale Lomega2 = L2 + Lomega 125begin 126 127lemmas [rules] = lam_bs pi_bs lam_bb pi_bb 128 129end 130 131 132locale LPomega = LP + Lomega 133begin 134 135lemmas [rules] = lam_bb pi_bb lam_sb pi_sb 136 137end 138 139 140locale CC = L2 + LP + Lomega 141begin 142 143lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb 144 145end 146 147end 148