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