23 DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close> |
23 DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close> |
24 |
24 |
25 |
25 |
26 subsection \<open>Simple types\<close> |
26 subsection \<open>Simple types\<close> |
27 |
27 |
28 schematic_lemma "A:* \<turnstile> A\<rightarrow>A : ?T" |
28 schematic_goal "A:* \<turnstile> A\<rightarrow>A : ?T" |
29 by (depth_solve rules) |
29 by (depth_solve rules) |
30 |
30 |
31 schematic_lemma "A:* \<turnstile> \<Lambda> a:A. a : ?T" |
31 schematic_goal "A:* \<turnstile> \<Lambda> a:A. a : ?T" |
32 by (depth_solve rules) |
32 by (depth_solve rules) |
33 |
33 |
34 schematic_lemma "A:* B:* b:B \<turnstile> \<Lambda> x:A. b : ?T" |
34 schematic_goal "A:* B:* b:B \<turnstile> \<Lambda> x:A. b : ?T" |
35 by (depth_solve rules) |
35 by (depth_solve rules) |
36 |
36 |
37 schematic_lemma "A:* b:A \<turnstile> (\<Lambda> a:A. a)^b: ?T" |
37 schematic_goal "A:* b:A \<turnstile> (\<Lambda> a:A. a)^b: ?T" |
38 by (depth_solve rules) |
38 by (depth_solve rules) |
39 |
39 |
40 schematic_lemma "A:* B:* c:A b:B \<turnstile> (\<Lambda> x:A. b)^ c: ?T" |
40 schematic_goal "A:* B:* c:A b:B \<turnstile> (\<Lambda> x:A. b)^ c: ?T" |
41 by (depth_solve rules) |
41 by (depth_solve rules) |
42 |
42 |
43 schematic_lemma "A:* B:* \<turnstile> \<Lambda> a:A. \<Lambda> b:B. a : ?T" |
43 schematic_goal "A:* B:* \<turnstile> \<Lambda> a:A. \<Lambda> b:B. a : ?T" |
44 by (depth_solve rules) |
44 by (depth_solve rules) |
45 |
45 |
46 |
46 |
47 subsection \<open>Second-order types\<close> |
47 subsection \<open>Second-order types\<close> |
48 |
48 |
49 schematic_lemma (in L2) "\<turnstile> \<Lambda> A:*. \<Lambda> a:A. a : ?T" |
49 schematic_goal (in L2) "\<turnstile> \<Lambda> A:*. \<Lambda> a:A. a : ?T" |
50 by (depth_solve rules) |
50 by (depth_solve rules) |
51 |
51 |
52 schematic_lemma (in L2) "A:* \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b)^A : ?T" |
52 schematic_goal (in L2) "A:* \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b)^A : ?T" |
53 by (depth_solve rules) |
53 by (depth_solve rules) |
54 |
54 |
55 schematic_lemma (in L2) "A:* b:A \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b) ^ A ^ b: ?T" |
55 schematic_goal (in L2) "A:* b:A \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b) ^ A ^ b: ?T" |
56 by (depth_solve rules) |
56 by (depth_solve rules) |
57 |
57 |
58 schematic_lemma (in L2) "\<turnstile> \<Lambda> B:*.\<Lambda> a:(\<Pi> A:*.A).a ^ ((\<Pi> A:*.A)\<rightarrow>B) ^ a: ?T" |
58 schematic_goal (in L2) "\<turnstile> \<Lambda> B:*.\<Lambda> a:(\<Pi> A:*.A).a ^ ((\<Pi> A:*.A)\<rightarrow>B) ^ a: ?T" |
59 by (depth_solve rules) |
59 by (depth_solve rules) |
60 |
60 |
61 |
61 |
62 subsection \<open>Weakly higher-order propositional logic\<close> |
62 subsection \<open>Weakly higher-order propositional logic\<close> |
63 |
63 |
64 schematic_lemma (in Lomega) "\<turnstile> \<Lambda> A:*.A\<rightarrow>A : ?T" |
64 schematic_goal (in Lomega) "\<turnstile> \<Lambda> A:*.A\<rightarrow>A : ?T" |
65 by (depth_solve rules) |
65 by (depth_solve rules) |
66 |
66 |
67 schematic_lemma (in Lomega) "B:* \<turnstile> (\<Lambda> A:*.A\<rightarrow>A) ^ B : ?T" |
67 schematic_goal (in Lomega) "B:* \<turnstile> (\<Lambda> A:*.A\<rightarrow>A) ^ B : ?T" |
68 by (depth_solve rules) |
68 by (depth_solve rules) |
69 |
69 |
70 schematic_lemma (in Lomega) "B:* b:B \<turnstile> (\<Lambda> y:B. b): ?T" |
70 schematic_goal (in Lomega) "B:* b:B \<turnstile> (\<Lambda> y:B. b): ?T" |
71 by (depth_solve rules) |
71 by (depth_solve rules) |
72 |
72 |
73 schematic_lemma (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F^(F^A): ?T" |
73 schematic_goal (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F^(F^A): ?T" |
74 by (depth_solve rules) |
74 by (depth_solve rules) |
75 |
75 |
76 schematic_lemma (in Lomega) "A:* \<turnstile> \<Lambda> F:*\<rightarrow>*.F^(F^A): ?T" |
76 schematic_goal (in Lomega) "A:* \<turnstile> \<Lambda> F:*\<rightarrow>*.F^(F^A): ?T" |
77 by (depth_solve rules) |
77 by (depth_solve rules) |
78 |
78 |
79 |
79 |
80 subsection \<open>LP\<close> |
80 subsection \<open>LP\<close> |
81 |
81 |
82 schematic_lemma (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T" |
82 schematic_goal (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T" |
83 by (depth_solve rules) |
83 by (depth_solve rules) |
84 |
84 |
85 schematic_lemma (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P^a: ?T" |
85 schematic_goal (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P^a: ?T" |
86 by (depth_solve rules) |
86 by (depth_solve rules) |
87 |
87 |
88 schematic_lemma (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Pi> a:A. P^a^a: ?T" |
88 schematic_goal (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Pi> a:A. P^a^a: ?T" |
89 by (depth_solve rules) |
89 by (depth_solve rules) |
90 |
90 |
91 schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> Q^a: ?T" |
91 schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> Q^a: ?T" |
92 by (depth_solve rules) |
92 by (depth_solve rules) |
93 |
93 |
94 schematic_lemma (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> P^a: ?T" |
94 schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> P^a: ?T" |
95 by (depth_solve rules) |
95 by (depth_solve rules) |
96 |
96 |
97 schematic_lemma (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. \<Lambda> x:P^a. x: ?T" |
97 schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. \<Lambda> x:P^a. x: ?T" |
98 by (depth_solve rules) |
98 by (depth_solve rules) |
99 |
99 |
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" |
100 schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* \<turnstile> (\<Pi> a:A. P^a\<rightarrow>Q) \<rightarrow> (\<Pi> a:A. P^a) \<rightarrow> Q : ?T" |
101 by (depth_solve rules) |
101 by (depth_solve rules) |
102 |
102 |
103 schematic_lemma (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile> |
103 schematic_goal (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" |
104 \<Lambda> x:\<Pi> a:A. P^a\<rightarrow>Q. \<Lambda> y:\<Pi> a:A. P^a. x^a0^(y^a0): ?T" |
105 by (depth_solve rules) |
105 by (depth_solve rules) |
106 |
106 |
107 |
107 |
108 subsection \<open>Omega-order types\<close> |
108 subsection \<open>Omega-order types\<close> |
109 |
109 |
110 schematic_lemma (in L2) "A:* B:* \<turnstile> \<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" |
110 schematic_goal (in L2) "A:* B:* \<turnstile> \<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" |
111 by (depth_solve rules) |
111 by (depth_solve rules) |
112 |
112 |
113 schematic_lemma (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" |
113 schematic_goal (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T" |
114 by (depth_solve rules) |
114 by (depth_solve rules) |
115 |
115 |
116 schematic_lemma (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Lambda> x:A. \<Lambda> y:B. x : ?T" |
116 schematic_goal (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Lambda> x:A. \<Lambda> y:B. x : ?T" |
117 by (depth_solve rules) |
117 by (depth_solve rules) |
118 |
118 |
119 schematic_lemma (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Pi> P:*.P)\<rightarrow>(A\<rightarrow>\<Pi> P:*.P))" |
119 schematic_goal (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Pi> P:*.P)\<rightarrow>(A\<rightarrow>\<Pi> P:*.P))" |
120 apply (strip_asms rules) |
120 apply (strip_asms rules) |
121 apply (rule lam_ss) |
121 apply (rule lam_ss) |
122 apply (depth_solve1 rules) |
122 apply (depth_solve1 rules) |
123 prefer 2 |
123 prefer 2 |
124 apply (depth_solve1 rules) |
124 apply (depth_solve1 rules) |
167 done |
167 done |
168 |
168 |
169 |
169 |
170 subsection \<open>LPomega\<close> |
170 subsection \<open>LPomega\<close> |
171 |
171 |
172 schematic_lemma (in LPomega) "A:* \<turnstile> \<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T" |
172 schematic_goal (in LPomega) "A:* \<turnstile> \<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T" |
173 by (depth_solve rules) |
173 by (depth_solve rules) |
174 |
174 |
175 schematic_lemma (in LPomega) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T" |
175 schematic_goal (in LPomega) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T" |
176 by (depth_solve rules) |
176 by (depth_solve rules) |
177 |
177 |
178 |
178 |
179 subsection \<open>Constructions\<close> |
179 subsection \<open>Constructions\<close> |
180 |
180 |
181 schematic_lemma (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Lambda> a:A. P^a\<rightarrow>\<Pi> P:*.P: ?T" |
181 schematic_goal (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Lambda> a:A. P^a\<rightarrow>\<Pi> P:*.P: ?T" |
182 by (depth_solve rules) |
182 by (depth_solve rules) |
183 |
183 |
184 schematic_lemma (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Pi> a:A. P^a: ?T" |
184 schematic_goal (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Pi> a:A. P^a: ?T" |
185 by (depth_solve rules) |
185 by (depth_solve rules) |
186 |
186 |
187 schematic_lemma (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Pi> a:A. P^a)\<rightarrow>P^a" |
187 schematic_goal (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Pi> a:A. P^a)\<rightarrow>P^a" |
188 apply (strip_asms rules) |
188 apply (strip_asms rules) |
189 apply (rule lam_ss) |
189 apply (rule lam_ss) |
190 apply (depth_solve1 rules) |
190 apply (depth_solve1 rules) |
191 prefer 2 |
191 prefer 2 |
192 apply (depth_solve1 rules) |
192 apply (depth_solve1 rules) |