author | wenzelm |
Thu, 25 Jun 2015 21:45:00 +0200 | |
changeset 60578 | c708dafe2220 |
parent 59499 | 14095f771781 |
child 61337 | 4645502c3c64 |
permissions | -rw-r--r-- |
58889 | 1 |
section \<open>Lambda Cube Examples\<close> |
17453 | 2 |
|
3 |
theory Example |
|
4 |
imports Cube |
|
5 |
begin |
|
6 |
||
58617 | 7 |
text \<open>Examples taken from: |
17453 | 8 |
|
9 |
H. Barendregt. Introduction to Generalised Type Systems. |
|
58617 | 10 |
J. Functional Programming.\<close> |
17453 | 11 |
|
58617 | 12 |
method_setup depth_solve = |
59499 | 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> |
|
17453 | 15 |
|
58617 | 16 |
method_setup depth_solve1 = |
59499 | 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> |
|
17453 | 19 |
|
58617 | 20 |
method_setup strip_asms = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
21 |
\<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts => |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
22 |
REPEAT (resolve_tac ctxt [@{thm strip_b}, @{thm strip_s}] 1 THEN |
59499 | 23 |
DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close> |
17453 | 24 |
|
25 |
||
58617 | 26 |
subsection \<open>Simple types\<close> |
17453 | 27 |
|
45242 | 28 |
schematic_lemma "A:* \<turnstile> A\<rightarrow>A : ?T" |
17453 | 29 |
by (depth_solve rules) |
30 |
||
45242 | 31 |
schematic_lemma "A:* \<turnstile> \<Lambda> a:A. a : ?T" |
17453 | 32 |
by (depth_solve rules) |
33 |
||
45242 | 34 |
schematic_lemma "A:* B:* b:B \<turnstile> \<Lambda> x:A. b : ?T" |
17453 | 35 |
by (depth_solve rules) |
36 |
||
45242 | 37 |
schematic_lemma "A:* b:A \<turnstile> (\<Lambda> a:A. a)^b: ?T" |
17453 | 38 |
by (depth_solve rules) |
39 |
||
45242 | 40 |
schematic_lemma "A:* B:* c:A b:B \<turnstile> (\<Lambda> x:A. b)^ c: ?T" |
17453 | 41 |
by (depth_solve rules) |
42 |
||
45242 | 43 |
schematic_lemma "A:* B:* \<turnstile> \<Lambda> a:A. \<Lambda> b:B. a : ?T" |
17453 | 44 |
by (depth_solve rules) |
45 |
||
46 |
||
58617 | 47 |
subsection \<open>Second-order types\<close> |
17453 | 48 |
|
45242 | 49 |
schematic_lemma (in L2) "\<turnstile> \<Lambda> A:*. \<Lambda> a:A. a : ?T" |
17453 | 50 |
by (depth_solve rules) |
51 |
||
45242 | 52 |
schematic_lemma (in L2) "A:* \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b)^A : ?T" |
17453 | 53 |
by (depth_solve rules) |
54 |
||
45242 | 55 |
schematic_lemma (in L2) "A:* b:A \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b) ^ A ^ b: ?T" |
17453 | 56 |
by (depth_solve rules) |
57 |
||
45242 | 58 |
schematic_lemma (in L2) "\<turnstile> \<Lambda> B:*.\<Lambda> a:(\<Pi> A:*.A).a ^ ((\<Pi> A:*.A)\<rightarrow>B) ^ a: ?T" |
17453 | 59 |
by (depth_solve rules) |
60 |
||
61 |
||
58617 | 62 |
subsection \<open>Weakly higher-order propositional logic\<close> |
17453 | 63 |
|
45242 | 64 |
schematic_lemma (in Lomega) "\<turnstile> \<Lambda> A:*.A\<rightarrow>A : ?T" |
17453 | 65 |
by (depth_solve rules) |
66 |
||
45242 | 67 |
schematic_lemma (in Lomega) "B:* \<turnstile> (\<Lambda> A:*.A\<rightarrow>A) ^ B : ?T" |
17453 | 68 |
by (depth_solve rules) |
69 |
||
45242 | 70 |
schematic_lemma (in Lomega) "B:* b:B \<turnstile> (\<Lambda> y:B. b): ?T" |
17453 | 71 |
by (depth_solve rules) |
72 |
||
45242 | 73 |
schematic_lemma (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F^(F^A): ?T" |
17453 | 74 |
by (depth_solve rules) |
75 |
||
45242 | 76 |
schematic_lemma (in Lomega) "A:* \<turnstile> \<Lambda> F:*\<rightarrow>*.F^(F^A): ?T" |
17453 | 77 |
by (depth_solve rules) |
78 |
||
79 |
||
58617 | 80 |
subsection \<open>LP\<close> |
17453 | 81 |
|
45242 | 82 |
schematic_lemma (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T" |
17453 | 83 |
by (depth_solve rules) |
84 |
||
45242 | 85 |
schematic_lemma (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P^a: ?T" |
17453 | 86 |
by (depth_solve rules) |
87 |
||
45242 | 88 |
schematic_lemma (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Pi> a:A. P^a^a: ?T" |
17453 | 89 |
by (depth_solve rules) |
90 |
||
45242 | 91 |
schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> Q^a: ?T" |
17453 | 92 |
by (depth_solve rules) |
93 |
||
45242 | 94 |
schematic_lemma (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> P^a: ?T" |
17453 | 95 |
by (depth_solve rules) |
96 |
||
45242 | 97 |
schematic_lemma (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. \<Lambda> x:P^a. x: ?T" |
17453 | 98 |
by (depth_solve rules) |
99 |
||
45242 | 100 |
schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:* \<turnstile> (\<Pi> a:A. P^a\<rightarrow>Q) \<rightarrow> (\<Pi> a:A. P^a) \<rightarrow> Q : ?T" |
17453 | 101 |
by (depth_solve rules) |
102 |
||
45242 | 103 |
schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile> |
104 |
\<Lambda> x:\<Pi> a:A. P^a\<rightarrow>Q. \<Lambda> y:\<Pi> a:A. P^a. x^a0^(y^a0): ?T" |
|
17453 | 105 |
by (depth_solve rules) |
106 |
||
107 |
||
58617 | 108 |
subsection \<open>Omega-order types\<close> |
17453 | 109 |
|
45242 | 110 |
schematic_lemma (in L2) "A:* B:* \<turnstile> \<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" |
17453 | 111 |
by (depth_solve rules) |
112 |
||
45242 | 113 |
schematic_lemma (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" |
17453 | 114 |
by (depth_solve rules) |
115 |
||
45242 | 116 |
schematic_lemma (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Lambda> x:A. \<Lambda> y:B. x : ?T" |
17453 | 117 |
by (depth_solve rules) |
118 |
||
45242 | 119 |
schematic_lemma (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Pi> P:*.P)\<rightarrow>(A\<rightarrow>\<Pi> P:*.P))" |
17453 | 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 |
||
58617 | 141 |
subsection \<open>Second-order Predicate Logic\<close> |
17453 | 142 |
|
45242 | 143 |
schematic_lemma (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. P^a\<rightarrow>(\<Pi> A:*.A) : ?T" |
17453 | 144 |
by (depth_solve rules) |
145 |
||
45242 | 146 |
schematic_lemma (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile> |
147 |
(\<Pi> a:A. \<Pi> b:A. P^a^b\<rightarrow>P^b^a\<rightarrow>\<Pi> P:*.P) \<rightarrow> \<Pi> a:A. P^a^a\<rightarrow>\<Pi> P:*.P : ?T" |
|
17453 | 148 |
by (depth_solve rules) |
149 |
||
45242 | 150 |
schematic_lemma (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile> |
151 |
?p: (\<Pi> a:A. \<Pi> b:A. P^a^b\<rightarrow>P^b^a\<rightarrow>\<Pi> P:*.P) \<rightarrow> \<Pi> a:A. P^a^a\<rightarrow>\<Pi> P:*.P" |
|
58617 | 152 |
-- \<open>Antisymmetry implies irreflexivity:\<close> |
17453 | 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 |
||
58617 | 170 |
subsection \<open>LPomega\<close> |
17453 | 171 |
|
45242 | 172 |
schematic_lemma (in LPomega) "A:* \<turnstile> \<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T" |
17453 | 173 |
by (depth_solve rules) |
174 |
||
45242 | 175 |
schematic_lemma (in LPomega) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T" |
17453 | 176 |
by (depth_solve rules) |
177 |
||
178 |
||
58617 | 179 |
subsection \<open>Constructions\<close> |
17453 | 180 |
|
45242 | 181 |
schematic_lemma (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Lambda> a:A. P^a\<rightarrow>\<Pi> P:*.P: ?T" |
17453 | 182 |
by (depth_solve rules) |
183 |
||
45242 | 184 |
schematic_lemma (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Pi> a:A. P^a: ?T" |
17453 | 185 |
by (depth_solve rules) |
186 |
||
45242 | 187 |
schematic_lemma (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Pi> a:A. P^a)\<rightarrow>P^a" |
17453 | 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 |
||
58617 | 197 |
subsection \<open>Some random examples\<close> |
17453 | 198 |
|
45242 | 199 |
schematic_lemma (in LP2) "A:* c:A f:A\<rightarrow>A \<turnstile> |
200 |
\<Lambda> a:A. \<Pi> P:A\<rightarrow>*.P^c \<rightarrow> (\<Pi> x:A. P^x\<rightarrow>P^(f^x)) \<rightarrow> P^a : ?T" |
|
17453 | 201 |
by (depth_solve rules) |
202 |
||
45242 | 203 |
schematic_lemma (in CC) "\<Lambda> A:*.\<Lambda> c:A. \<Lambda> f:A\<rightarrow>A. |
204 |
\<Lambda> a:A. \<Pi> P:A\<rightarrow>*.P^c \<rightarrow> (\<Pi> x:A. P^x\<rightarrow>P^(f^x)) \<rightarrow> P^a : ?T" |
|
17453 | 205 |
by (depth_solve rules) |
206 |
||
36319 | 207 |
schematic_lemma (in LP2) |
45242 | 208 |
"A:* a:A b:A \<turnstile> ?p: (\<Pi> P:A\<rightarrow>*.P^a\<rightarrow>P^b) \<rightarrow> (\<Pi> P:A\<rightarrow>*.P^b\<rightarrow>P^a)" |
58617 | 209 |
-- \<open>Symmetry of Leibnitz equality\<close> |
17453 | 210 |
apply (strip_asms rules) |
211 |
apply (rule lam_ss) |
|
212 |
apply (depth_solve1 rules) |
|
213 |
prefer 2 |
|
214 |
apply (depth_solve1 rules) |
|
45242 | 215 |
apply (erule_tac a = "\<Lambda> x:A. \<Pi> Q:A\<rightarrow>*.Q^x\<rightarrow>Q^a" in pi_elim) |
17453 | 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 |
||
231 |
end |