author  wenzelm 
Mon, 24 Oct 2016 11:42:39 +0200  
changeset 64367  a424f2737646 
parent 62020  5d208fd2507d 
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 => 
61389  22 
REPEAT (resolve_tac ctxt @{thms strip_b 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 

61337  28 
schematic_goal "A:* \<turnstile> A\<rightarrow>A : ?T" 
17453  29 
by (depth_solve rules) 
30 

61388  31 
schematic_goal "A:* \<turnstile> \<^bold>\<lambda>a:A. a : ?T" 
17453  32 
by (depth_solve rules) 
33 

61388  34 
schematic_goal "A:* B:* b:B \<turnstile> \<^bold>\<lambda>x:A. b : ?T" 
17453  35 
by (depth_solve rules) 
36 

61388  37 
schematic_goal "A:* b:A \<turnstile> (\<^bold>\<lambda>a:A. a)\<cdot>b: ?T" 
17453  38 
by (depth_solve rules) 
39 

61388  40 
schematic_goal "A:* B:* c:A b:B \<turnstile> (\<^bold>\<lambda>x:A. b)\<cdot> c: ?T" 
17453  41 
by (depth_solve rules) 
42 

61388  43 
schematic_goal "A:* B:* \<turnstile> \<^bold>\<lambda>a:A. \<^bold>\<lambda>b:B. a : ?T" 
17453  44 
by (depth_solve rules) 
45 

46 

58617  47 
subsection \<open>Secondorder types\<close> 
17453  48 

61388  49 
schematic_goal (in L2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>a:A. a : ?T" 
17453  50 
by (depth_solve rules) 
51 

61390  52 
schematic_goal (in L2) "A:* \<turnstile> (\<^bold>\<lambda>B:*. \<^bold>\<lambda>b:B. b)\<cdot>A : ?T" 
17453  53 
by (depth_solve rules) 
54 

61390  55 
schematic_goal (in L2) "A:* b:A \<turnstile> (\<^bold>\<lambda>B:*. \<^bold>\<lambda>b:B. b) \<cdot> A \<cdot> b: ?T" 
17453  56 
by (depth_solve rules) 
57 

61390  58 
schematic_goal (in L2) "\<turnstile> \<^bold>\<lambda>B:*. \<^bold>\<lambda>a:(\<Prod>A:*.A).a \<cdot> ((\<Prod>A:*.A)\<rightarrow>B) \<cdot> a: ?T" 
17453  59 
by (depth_solve rules) 
60 

61 

58617  62 
subsection \<open>Weakly higherorder propositional logic\<close> 
17453  63 

61388  64 
schematic_goal (in Lomega) "\<turnstile> \<^bold>\<lambda>A:*.A\<rightarrow>A : ?T" 
17453  65 
by (depth_solve rules) 
66 

61388  67 
schematic_goal (in Lomega) "B:* \<turnstile> (\<^bold>\<lambda>A:*.A\<rightarrow>A) \<cdot> B : ?T" 
17453  68 
by (depth_solve rules) 
69 

61388  70 
schematic_goal (in Lomega) "B:* b:B \<turnstile> (\<^bold>\<lambda>y:B. b): ?T" 
17453  71 
by (depth_solve rules) 
72 

61388  73 
schematic_goal (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F\<cdot>(F\<cdot>A): ?T" 
17453  74 
by (depth_solve rules) 
75 

61388  76 
schematic_goal (in Lomega) "A:* \<turnstile> \<^bold>\<lambda>F:*\<rightarrow>*.F\<cdot>(F\<cdot>A): ?T" 
17453  77 
by (depth_solve rules) 
78 

79 

58617  80 
subsection \<open>LP\<close> 
17453  81 

61337  82 
schematic_goal (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T" 
17453  83 
by (depth_solve rules) 
84 

61388  85 
schematic_goal (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P\<cdot>a: ?T" 
17453  86 
by (depth_solve rules) 
87 

61388  88 
schematic_goal (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Prod>a:A. P\<cdot>a\<cdot>a: ?T" 
17453  89 
by (depth_solve rules) 
90 

61388  91 
schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Prod>a:A. P\<cdot>a \<rightarrow> Q\<cdot>a: ?T" 
17453  92 
by (depth_solve rules) 
93 

61388  94 
schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Prod>a:A. P\<cdot>a \<rightarrow> P\<cdot>a: ?T" 
17453  95 
by (depth_solve rules) 
96 

61388  97 
schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<^bold>\<lambda>a:A. \<^bold>\<lambda>x:P\<cdot>a. x: ?T" 
17453  98 
by (depth_solve rules) 
99 

61388  100 
schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* \<turnstile> (\<Prod>a:A. P\<cdot>a\<rightarrow>Q) \<rightarrow> (\<Prod>a:A. P\<cdot>a) \<rightarrow> Q : ?T" 
17453  101 
by (depth_solve rules) 
102 

61337  103 
schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile> 
61388  104 
\<^bold>\<lambda>x:\<Prod>a:A. P\<cdot>a\<rightarrow>Q. \<^bold>\<lambda>y:\<Prod>a:A. P\<cdot>a. x\<cdot>a0\<cdot>(y\<cdot>a0): ?T" 
17453  105 
by (depth_solve rules) 
106 

107 

58617  108 
subsection \<open>Omegaorder types\<close> 
17453  109 

61388  110 
schematic_goal (in L2) "A:* B:* \<turnstile> \<Prod>C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" 
17453  111 
by (depth_solve rules) 
112 

61390  113 
schematic_goal (in Lomega2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>B:*.\<Prod>C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" 
17453  114 
by (depth_solve rules) 
115 

61390  116 
schematic_goal (in Lomega2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>B:*. \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : ?T" 
17453  117 
by (depth_solve rules) 
118 

61388  119 
schematic_goal (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Prod>P:*.P)\<rightarrow>(A\<rightarrow>\<Prod>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 

61388  143 
schematic_goal (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<^bold>\<lambda>a:A. P\<cdot>a\<rightarrow>(\<Prod>A:*.A) : ?T" 
17453  144 
by (depth_solve rules) 
145 

61337  146 
schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile> 
61388  147 
(\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P : ?T" 
17453  148 
by (depth_solve rules) 
149 

61337  150 
schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile> 
61388  151 
?p: (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P" 
62020  152 
\<comment> \<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 

61390  172 
schematic_goal (in LPomega) "A:* \<turnstile> \<^bold>\<lambda>P:A\<rightarrow>A\<rightarrow>*. \<^bold>\<lambda>a:A. P\<cdot>a\<cdot>a : ?T" 
17453  173 
by (depth_solve rules) 
174 

61390  175 
schematic_goal (in LPomega) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>P:A\<rightarrow>A\<rightarrow>*. \<^bold>\<lambda>a:A. P\<cdot>a\<cdot>a : ?T" 
17453  176 
by (depth_solve rules) 
177 

178 

58617  179 
subsection \<open>Constructions\<close> 
17453  180 

61390  181 
schematic_goal (in CC) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>P:A\<rightarrow>*. \<^bold>\<lambda>a:A. P\<cdot>a\<rightarrow>\<Prod>P:*.P: ?T" 
17453  182 
by (depth_solve rules) 
183 

61390  184 
schematic_goal (in CC) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>P:A\<rightarrow>*.\<Prod>a:A. P\<cdot>a: ?T" 
17453  185 
by (depth_solve rules) 
186 

61388  187 
schematic_goal (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Prod>a:A. P\<cdot>a)\<rightarrow>P\<cdot>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 

61337  199 
schematic_goal (in LP2) "A:* c:A f:A\<rightarrow>A \<turnstile> 
61388  200 
\<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>a : ?T" 
17453  201 
by (depth_solve rules) 
202 

61390  203 
schematic_goal (in CC) "\<^bold>\<lambda>A:*. \<^bold>\<lambda>c:A. \<^bold>\<lambda>f:A\<rightarrow>A. 
61388  204 
\<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>a : ?T" 
17453  205 
by (depth_solve rules) 
206 

61337  207 
schematic_goal (in LP2) 
61388  208 
"A:* a:A b:A \<turnstile> ?p: (\<Prod>P:A\<rightarrow>*.P\<cdot>a\<rightarrow>P\<cdot>b) \<rightarrow> (\<Prod>P:A\<rightarrow>*.P\<cdot>b\<rightarrow>P\<cdot>a)" 
62020  209 
\<comment> \<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) 

61388  215 
apply (erule_tac a = "\<^bold>\<lambda>x:A. \<Prod>Q:A\<rightarrow>*.Q\<cdot>x\<rightarrow>Q\<cdot>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 