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