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