author  wenzelm 
Tue, 10 Feb 2015 16:46:21 +0100  
changeset 59499  14095f771781 
parent 59498  50b60f501b05 
child 61337  4645502c3c64 
permissions  rwrr 
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>Secondorder 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 higherorder 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>Omegaorder 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>Secondorder 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 