1section \<open>Lambda Cube Examples\<close>
2
3theory Example
4imports Cube
5begin
6
7text \<open>Examples taken from:
8
9  H. Barendregt. Introduction to Generalised Type Systems.
10  J. Functional Programming.\<close>
11
12method_setup depth_solve =
13  \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
14    (DEPTH_SOLVE (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
15
16method_setup depth_solve1 =
17  \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
18    (DEPTH_SOLVE_1 (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
19
20method_setup strip_asms =
21  \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
22    REPEAT (resolve_tac ctxt @{thms strip_b strip_s} 1 THEN
23    DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close>
24
25
26subsection \<open>Simple types\<close>
27
28schematic_goal "A:* \<turnstile> A\<rightarrow>A : ?T"
29  by (depth_solve rules)
30
31schematic_goal "A:* \<turnstile> \<^bold>\<lambda>a:A. a : ?T"
32  by (depth_solve rules)
33
34schematic_goal "A:* B:* b:B \<turnstile> \<^bold>\<lambda>x:A. b : ?T"
35  by (depth_solve rules)
36
37schematic_goal "A:* b:A \<turnstile> (\<^bold>\<lambda>a:A. a)\<cdot>b: ?T"
38  by (depth_solve rules)
39
40schematic_goal "A:* B:* c:A b:B \<turnstile> (\<^bold>\<lambda>x:A. b)\<cdot> c: ?T"
41  by (depth_solve rules)
42
43schematic_goal "A:* B:* \<turnstile> \<^bold>\<lambda>a:A. \<^bold>\<lambda>b:B. a : ?T"
44  by (depth_solve rules)
45
46
47subsection \<open>Second-order types\<close>
48
49schematic_goal (in L2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>a:A. a : ?T"
50  by (depth_solve rules)
51
52schematic_goal (in L2) "A:* \<turnstile> (\<^bold>\<lambda>B:*. \<^bold>\<lambda>b:B. b)\<cdot>A : ?T"
53  by (depth_solve rules)
54
55schematic_goal (in L2) "A:* b:A \<turnstile> (\<^bold>\<lambda>B:*. \<^bold>\<lambda>b:B. b) \<cdot> A \<cdot> b: ?T"
56  by (depth_solve rules)
57
58schematic_goal (in L2) "\<turnstile> \<^bold>\<lambda>B:*. \<^bold>\<lambda>a:(\<Prod>A:*.A).a \<cdot> ((\<Prod>A:*.A)\<rightarrow>B) \<cdot> a: ?T"
59  by (depth_solve rules)
60
61
62subsection \<open>Weakly higher-order propositional logic\<close>
63
64schematic_goal (in Lomega) "\<turnstile> \<^bold>\<lambda>A:*.A\<rightarrow>A : ?T"
65  by (depth_solve rules)
66
67schematic_goal (in Lomega) "B:* \<turnstile> (\<^bold>\<lambda>A:*.A\<rightarrow>A) \<cdot> B : ?T"
68  by (depth_solve rules)
69
70schematic_goal (in Lomega) "B:* b:B \<turnstile> (\<^bold>\<lambda>y:B. b): ?T"
71  by (depth_solve rules)
72
73schematic_goal (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F\<cdot>(F\<cdot>A): ?T"
74  by (depth_solve rules)
75
76schematic_goal (in Lomega) "A:* \<turnstile> \<^bold>\<lambda>F:*\<rightarrow>*.F\<cdot>(F\<cdot>A): ?T"
77  by (depth_solve rules)
78
79
80subsection \<open>LP\<close>
81
82schematic_goal (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T"
83  by (depth_solve rules)
84
85schematic_goal (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P\<cdot>a: ?T"
86  by (depth_solve rules)
87
88schematic_goal (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Prod>a:A. P\<cdot>a\<cdot>a: ?T"
89  by (depth_solve rules)
90
91schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Prod>a:A. P\<cdot>a \<rightarrow> Q\<cdot>a: ?T"
92  by (depth_solve rules)
93
94schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Prod>a:A. P\<cdot>a \<rightarrow> P\<cdot>a: ?T"
95  by (depth_solve rules)
96
97schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<^bold>\<lambda>a:A. \<^bold>\<lambda>x:P\<cdot>a. x: ?T"
98  by (depth_solve rules)
99
100schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* \<turnstile> (\<Prod>a:A. P\<cdot>a\<rightarrow>Q) \<rightarrow> (\<Prod>a:A. P\<cdot>a) \<rightarrow> Q : ?T"
101  by (depth_solve rules)
102
103schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile>
104        \<^bold>\<lambda>x:\<Prod>a:A. P\<cdot>a\<rightarrow>Q. \<^bold>\<lambda>y:\<Prod>a:A. P\<cdot>a. x\<cdot>a0\<cdot>(y\<cdot>a0): ?T"
105  by (depth_solve rules)
106
107
108subsection \<open>Omega-order types\<close>
109
110schematic_goal (in L2) "A:* B:* \<turnstile> \<Prod>C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
111  by (depth_solve rules)
112
113schematic_goal (in Lomega2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>B:*.\<Prod>C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
114  by (depth_solve rules)
115
116schematic_goal (in Lomega2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>B:*. \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : ?T"
117  by (depth_solve rules)
118
119schematic_goal (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Prod>P:*.P)\<rightarrow>(A\<rightarrow>\<Prod>P:*.P))"
120  apply (strip_asms rules)
121  apply (rule lam_ss)
122    apply (depth_solve1 rules)
123   prefer 2
124   apply (depth_solve1 rules)
125  apply (rule lam_ss)
126    apply (depth_solve1 rules)
127   prefer 2
128   apply (depth_solve1 rules)
129  apply (rule lam_ss)
130    apply assumption
131   prefer 2
132   apply (depth_solve1 rules)
133  apply (erule pi_elim)
134   apply assumption
135  apply (erule pi_elim)
136   apply assumption
137  apply assumption
138  done
139
140
141subsection \<open>Second-order Predicate Logic\<close>
142
143schematic_goal (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<^bold>\<lambda>a:A. P\<cdot>a\<rightarrow>(\<Prod>A:*.A) : ?T"
144  by (depth_solve rules)
145
146schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
147    (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P : ?T"
148  by (depth_solve rules)
149
150schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
151    ?p: (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P"
152  \<comment> \<open>Antisymmetry implies irreflexivity:\<close>
153  apply (strip_asms rules)
154  apply (rule lam_ss)
155    apply (depth_solve1 rules)
156   prefer 2
157   apply (depth_solve1 rules)
158  apply (rule lam_ss)
159    apply assumption
160   prefer 2
161   apply (depth_solve1 rules)
162  apply (rule lam_ss)
163    apply (depth_solve1 rules)
164   prefer 2
165   apply (depth_solve1 rules)
166  apply (erule pi_elim, assumption, assumption?)+
167  done
168
169
170subsection \<open>LPomega\<close>
171
172schematic_goal (in LPomega) "A:* \<turnstile> \<^bold>\<lambda>P:A\<rightarrow>A\<rightarrow>*. \<^bold>\<lambda>a:A. P\<cdot>a\<cdot>a : ?T"
173  by (depth_solve rules)
174
175schematic_goal (in LPomega) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>P:A\<rightarrow>A\<rightarrow>*. \<^bold>\<lambda>a:A. P\<cdot>a\<cdot>a : ?T"
176  by (depth_solve rules)
177
178
179subsection \<open>Constructions\<close>
180
181schematic_goal (in CC) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>P:A\<rightarrow>*. \<^bold>\<lambda>a:A. P\<cdot>a\<rightarrow>\<Prod>P:*.P: ?T"
182  by (depth_solve rules)
183
184schematic_goal (in CC) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>P:A\<rightarrow>*.\<Prod>a:A. P\<cdot>a: ?T"
185  by (depth_solve rules)
186
187schematic_goal (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Prod>a:A. P\<cdot>a)\<rightarrow>P\<cdot>a"
188  apply (strip_asms rules)
189  apply (rule lam_ss)
190    apply (depth_solve1 rules)
191   prefer 2
192   apply (depth_solve1 rules)
193  apply (erule pi_elim, assumption, assumption)
194  done
195
196
197subsection \<open>Some random examples\<close>
198
199schematic_goal (in LP2) "A:* c:A f:A\<rightarrow>A \<turnstile>
200    \<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>a : ?T"
201  by (depth_solve rules)
202
203schematic_goal (in CC) "\<^bold>\<lambda>A:*. \<^bold>\<lambda>c:A. \<^bold>\<lambda>f:A\<rightarrow>A.
204    \<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>a : ?T"
205  by (depth_solve rules)
206
207schematic_goal (in LP2)
208  "A:* a:A b:A \<turnstile> ?p: (\<Prod>P:A\<rightarrow>*.P\<cdot>a\<rightarrow>P\<cdot>b) \<rightarrow> (\<Prod>P:A\<rightarrow>*.P\<cdot>b\<rightarrow>P\<cdot>a)"
209  \<comment> \<open>Symmetry of Leibnitz equality\<close>
210  apply (strip_asms rules)
211  apply (rule lam_ss)
212    apply (depth_solve1 rules)
213   prefer 2
214   apply (depth_solve1 rules)
215  apply (erule_tac a = "\<^bold>\<lambda>x:A. \<Prod>Q:A\<rightarrow>*.Q\<cdot>x\<rightarrow>Q\<cdot>a" in pi_elim)
216   apply (depth_solve1 rules)
217  apply (unfold beta)
218  apply (erule imp_elim)
219   apply (rule lam_bs)
220     apply (depth_solve1 rules)
221    prefer 2
222    apply (depth_solve1 rules)
223   apply (rule lam_ss)
224     apply (depth_solve1 rules)
225    prefer 2
226    apply (depth_solve1 rules)
227   apply assumption
228  apply assumption
229  done
230
231end
232