author | ballarin |
Tue, 20 Jun 2006 15:53:44 +0200 | |
changeset 19931 | fb32b43e7f80 |
parent 17453 | eccff680177d |
child 19943 | 26b37721b357 |
permissions | -rw-r--r-- |
17453 | 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 => |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
17453
diff
changeset
|
19 |
(DEPTH_SOLVE (HEADGOAL (ares_tac (PolyML.print (facts @ thms))))))) |
17453 | 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 |