1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
17 include "basics/pts.ma".
18 include "hints_declaration.ma".
20 inductive Imply (A,B:Prop) : Prop ≝
21 | Imply_intro: (A → B) → Imply A B.
23 definition Imply_elim ≝ λA,B:Prop.λf:Imply A B. λa:A.
24 match f with [ Imply_intro g ⇒ g a].
26 inductive And (A,B:Prop) : Prop ≝
27 | And_intro: A → B → And A B.
29 definition And_elim_l ≝ λA,B.λc:And A B.
30 match c with [ And_intro a b ⇒ a ].
32 definition And_elim_r ≝ λA,B.λc:And A B.
33 match c with [ And_intro a b ⇒ b ].
35 inductive Or (A,B:Prop) : Prop ≝
36 | Or_intro_l: A → Or A B
37 | Or_intro_r: B → Or A B.
39 definition Or_elim ≝ λA,B,C:Prop.λc:Or A B.λfa: A → C.λfb: B → C.
42 | Or_intro_r b ⇒ fb b].
44 inductive Top : Prop :=
47 inductive Bot : Prop := .
49 definition Bot_elim ≝ λP:Prop.λx:Bot.
50 match x in Bot return λx.P with [].
52 definition Not := λA:Prop.Imply A Bot.
54 definition Not_intro : ∀A.(A → Bot) → Not A ≝ λA.
57 definition Not_elim : ∀A.Not A → A → Bot ≝ λA.
60 definition Discharge := λA:Prop.λa:A.
63 axiom Raa : ∀A.(Not A → Bot) → A.
67 inductive Exists (A:Type[0]) (P:A→Prop) : Prop ≝
68 Exists_intro: ∀w:A. P w → Exists A P.
70 definition Exists_elim ≝
71 λA:Type[0].λP:A→Prop.λC:Prop.λc:Exists A P.λH:(Πx.P x → C).
72 match c with [ Exists_intro w p ⇒ H w p ].
74 inductive Forall (A:Type[0]) (P:A→Prop) : Prop ≝
75 Forall_intro: (∀n:A. P n) → Forall A P.
77 definition Forall_elim ≝
78 λA:Type[0].λP:A→Prop.λn:A.λf:Forall A P.match f with [ Forall_intro g ⇒ g n ].
80 (* Dummy proposition *)
84 notation "hbox(a break ⇒ b)" right associative with precedence 20
85 for @{ 'Imply $a $b }.
86 interpretation "Imply" 'Imply a b = (Imply a b).
87 interpretation "constructive or" 'or x y = (Or x y).
88 interpretation "constructive and" 'and x y = (And x y).
89 notation "⊤" non associative with precedence 90 for @{'Top}.
90 interpretation "Top" 'Top = Top.
91 notation "⊥" non associative with precedence 90 for @{'Bot}.
92 interpretation "Bot" 'Bot = Bot.
93 interpretation "Not" 'not a = (Not a).
94 notation "✶" non associative with precedence 90 for @{'unit}.
95 interpretation "dummy prop" 'unit = unit.
96 notation > "\exists list1 ident x sep , . term 19 Px" with precedence 20
97 for ${ fold right @{$Px} rec acc @{'myexists (λ${ident x}.$acc)} }.
98 notation < "hvbox(\exists ident i break . p)" with precedence 20
99 for @{ 'myexists (\lambda ${ident i} : $ty. $p) }.
100 interpretation "constructive ex" 'myexists \eta.x = (Exists sort x).
101 notation > "\forall ident x.break term 19 Px" with precedence 20
102 for @{ 'Forall (λ${ident x}.$Px) }.
103 notation < "\forall ident x.break term 19 Px" with precedence 20
104 for @{ 'Forall (λ${ident x}:$tx.$Px) }.
105 interpretation "Forall" 'Forall \eta.Px = (Forall ? Px).
128 (* Every formula user provided annotates its proof:
129 `A` becomes `(show A ?)` *)
130 definition show : ΠA.A→A ≝ λA:Prop.λa:A.a.
132 (* When something does not fit, this daemon is used *)
133 axiom cast: ΠA,B:Prop.B → A.
135 (* begin a proof: draws the root *)
136 notation > "'prove' p" non associative with precedence 19
138 interpretation "prove KO" 'prove p = (cast ? ? (show p ?)).
139 interpretation "prove OK" 'prove p = (show p ?).
142 notation < "\infrule (t\atop ⋮) a ?" with precedence 19
143 for @{ 'leaf_ok $a $t }.
144 interpretation "leaf OK" 'leaf_ok a t = (show a t).
145 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19
146 for @{ 'leaf_ko $a $t }.
147 interpretation "leaf KO" 'leaf_ko a t = (cast ? ? (show a t)).
150 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19
151 for @{ 'discharge_ko_1 $a $H }.
152 interpretation "discharge_ko_1" 'discharge_ko_1 a H =
153 (show a (cast ? ? (Discharge ? H))).
154 notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19
155 for @{ 'discharge_ko_2 $a $H }.
156 interpretation "discharge_ko_2" 'discharge_ko_2 a H =
157 (cast ? ? (show a (cast ? ? (Discharge ? H)))).
159 notation < "[ a ] \sup H" with precedence 19
160 for @{ 'discharge_ok_1 $a $H }.
161 interpretation "discharge_ok_1" 'discharge_ok_1 a H =
162 (show a (Discharge ? H)).
163 notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19
164 for @{ 'discharge_ok_2 $a $H }.
165 interpretation "discharge_ok_2" 'discharge_ok_2 a H =
166 (cast ? ? (show a (Discharge ? H))).
168 notation > "'discharge' [H]" with precedence 19
169 for @{ 'discharge $H }.
170 interpretation "discharge KO" 'discharge H = (cast ? ? (Discharge ? H)).
171 interpretation "discharge OK" 'discharge H = (Discharge ? H).
174 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
175 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
176 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b =
177 (show ab (cast ? ? (Imply_intro ? ? b))).
179 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
180 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
181 interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b =
182 (cast ? ? (show ab (cast ? ? (Imply_intro ? ? b)))).
184 notation < "maction (\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) ) (\vdots)" with precedence 19
185 for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
186 interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b =
187 (show ab (Imply_intro ? ? b)).
189 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19
190 for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
191 interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b =
192 (cast ? ? (show ab (Imply_intro ? ? b))).
194 notation > "⇒#'i' [ident H] term 90 b" with precedence 19
195 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
197 interpretation "Imply_intro KO" 'Imply_intro b pb =
198 (cast ? (Imply unit b) (Imply_intro ? b pb)).
199 interpretation "Imply_intro OK" 'Imply_intro b pb =
200 (Imply_intro ? b pb).
203 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
204 for @{ 'Imply_elim_ko_1 $ab $a $b }.
205 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b =
206 (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a)))).
208 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19
209 for @{ 'Imply_elim_ko_2 $ab $a $b }.
210 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b =
211 (cast ? ? (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a))))).
213 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19
214 for @{ 'Imply_elim_ok_1 $ab $a $b }.
215 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b =
216 (show b (Imply_elim ? ? ab a)).
218 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19
219 for @{ 'Imply_elim_ok_2 $ab $a $b }.
220 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b =
221 (cast ? ? (show b (Imply_elim ? ? ab a))).
223 notation > "⇒#'e' term 90 ab term 90 a" with precedence 19
224 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
225 interpretation "Imply_elim KO" 'Imply_elim ab a =
226 (cast ? ? (Imply_elim ? ? (cast (Imply unit unit) ? ab) (cast unit ? a))).
227 interpretation "Imply_elim OK" 'Imply_elim ab a =
228 (Imply_elim ? ? ab a).
231 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19
232 for @{ 'And_intro_ko_1 $a $b $ab }.
233 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab =
234 (show ab (cast ? ? (And_intro ? ? a b))).
236 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19
237 for @{ 'And_intro_ko_2 $a $b $ab }.
238 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab =
239 (cast ? ? (show ab (cast ? ? (And_intro ? ? a b)))).
241 notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19
242 for @{ 'And_intro_ok_1 $a $b $ab }.
243 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab =
244 (show ab (And_intro ? ? a b)).
246 notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19
247 for @{ 'And_intro_ok_2 $a $b $ab }.
248 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab =
249 (cast ? ? (show ab (And_intro ? ? a b))).
251 notation > "∧#'i' term 90 a term 90 b" with precedence 19
252 for @{ 'And_intro (show $a ?) (show $b ?) }.
253 interpretation "And_intro KO" 'And_intro a b = (cast ? ? (And_intro ? ? a b)).
254 interpretation "And_intro OK" 'And_intro a b = (And_intro ? ? a b).
257 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
258 for @{ 'And_elim_l_ko_1 $ab $a }.
259 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a =
260 (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab)))).
262 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19
263 for @{ 'And_elim_l_ko_2 $ab $a }.
264 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a =
265 (cast ? ? (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab))))).
267 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19
268 for @{ 'And_elim_l_ok_1 $ab $a }.
269 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a =
270 (show a (And_elim_l ? ? ab)).
272 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19
273 for @{ 'And_elim_l_ok_2 $ab $a }.
274 interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a =
275 (cast ? ? (show a (And_elim_l ? ? ab))).
277 notation > "∧#'e_l' term 90 ab" with precedence 19
278 for @{ 'And_elim_l (show $ab ?) }.
279 interpretation "And_elim_l KO" 'And_elim_l a = (cast ? ? (And_elim_l ? ? (cast (And unit unit) ? a))).
280 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l ? ? a).
282 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
283 for @{ 'And_elim_r_ko_1 $ab $a }.
284 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a =
285 (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab)))).
287 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19
288 for @{ 'And_elim_r_ko_2 $ab $a }.
289 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a =
290 (cast ? ? (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab))))).
292 notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19
293 for @{ 'And_elim_r_ok_1 $ab $a }.
294 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a =
295 (show a (And_elim_r ? ? ab)).
297 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19
298 for @{ 'And_elim_r_ok_2 $ab $a }.
299 interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a =
300 (cast ? ? (show a (And_elim_r ? ? ab))).
302 notation > "∧#'e_r' term 90 ab" with precedence 19
303 for @{ 'And_elim_r (show $ab ?) }.
304 interpretation "And_elim_r KO" 'And_elim_r a = (cast ? ? (And_elim_r ? ? (cast (And unit unit) ? a))).
305 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r ? ? a).
308 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
309 for @{ 'Or_intro_l_ko_1 $a $ab }.
310 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab =
311 (show ab (cast ? ? (Or_intro_l ? ? a))).
313 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19
314 for @{ 'Or_intro_l_ko_2 $a $ab }.
315 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab =
316 (cast ? ? (show ab (cast ? ? (Or_intro_l ? ? a)))).
318 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19
319 for @{ 'Or_intro_l_ok_1 $a $ab }.
320 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
321 (show ab (Or_intro_l ? ? a)).
323 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19
324 for @{ 'Or_intro_l_ok_2 $a $ab }.
325 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab =
326 (cast ? ? (show ab (Or_intro_l ? ? a))).
328 notation > "∨#'i_l' term 90 a" with precedence 19
329 for @{ 'Or_intro_l (show $a ?) }.
330 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast ? (Or ? unit) (Or_intro_l ? ? a)).
331 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l ? ? a).
333 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
334 for @{ 'Or_intro_r_ko_1 $a $ab }.
335 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab =
336 (show ab (cast ? ? (Or_intro_r ? ? a))).
338 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19
339 for @{ 'Or_intro_r_ko_2 $a $ab }.
340 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab =
341 (cast ? ? (show ab (cast ? ? (Or_intro_r ? ? a)))).
343 notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19
344 for @{ 'Or_intro_r_ok_1 $a $ab }.
345 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab =
346 (show ab (Or_intro_r ? ? a)).
348 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19
349 for @{ 'Or_intro_r_ok_2 $a $ab }.
350 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab =
351 (cast ? ? (show ab (Or_intro_r ? ? a))).
353 notation > "∨#'i_r' term 90 a" with precedence 19
354 for @{ 'Or_intro_r (show $a ?) }.
355 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast ? (Or unit ?) (Or_intro_r ? ? a)).
356 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r ? ? a).
359 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19
360 for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
361 interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc =
362 (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc)))).
364 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19
365 for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
366 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c =
367 (cast ? ? (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc))))).
369 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)) (\vdots)" with precedence 19
370 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
371 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c =
372 (show c (Or_elim ? ? ? ab ac bc)).
374 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
375 for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
376 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c =
377 (cast ? ? (show c (Or_elim ? ? ? ab ac bc))).
379 definition unit_to ≝ λx:Prop.unit → x.
381 notation > "∨#'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
382 for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
383 interpretation "Or_elim KO" 'Or_elim ab ac bc =
384 (cast ? ? (Or_elim ? ? ?
385 (cast (Or unit unit) ? ab)
386 (cast (unit_to unit) (unit_to ?) ac)
387 (cast (unit_to unit) (unit_to ?) bc))).
388 interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim ? ? ? ab ac bc).
391 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19
392 for @{'Top_intro_ko_1}.
393 interpretation "Top_intro_ko_1" 'Top_intro_ko_1 =
394 (show ? (cast ? ? Top_intro)).
396 notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19
397 for @{'Top_intro_ko_2}.
398 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 =
399 (cast ? ? (show ? (cast ? ? Top_intro))).
401 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
402 for @{'Top_intro_ok_1}.
403 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show ? Top_intro).
405 notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19
406 for @{'Top_intro_ok_2 }.
407 interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast ? ? (show ? Top_intro)).
409 notation > "⊤#'i'" with precedence 19 for @{ 'Top_intro }.
410 interpretation "Top_intro KO" 'Top_intro = (cast ? ? Top_intro).
411 interpretation "Top_intro OK" 'Top_intro = Top_intro.
414 notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19
415 for @{'Bot_elim_ko_1 $a $b}.
416 interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b =
417 (show a (Bot_elim ? (cast ? ? b))).
419 notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19
420 for @{'Bot_elim_ko_2 $a $b}.
421 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b =
422 (cast ? ? (show a (Bot_elim ? (cast ? ? b)))).
424 notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19
425 for @{'Bot_elim_ok_1 $a $b}.
426 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b =
427 (show a (Bot_elim ? b)).
429 notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19
430 for @{'Bot_elim_ok_2 $a $b}.
431 interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b =
432 (cast ? ? (show a (Bot_elim ? b))).
434 notation > "⊥#'e' term 90 b" with precedence 19
435 for @{ 'Bot_elim (show $b ?) }.
436 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim ? (cast ? ? a)).
437 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim ? a).
440 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
441 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
442 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b =
443 (show ab (cast ? ? (Not_intro ? (cast ? ? b)))).
445 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19
446 for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
447 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b =
448 (cast ? ? (show ab (cast ? ? (Not_intro ? (cast ? ? b))))).
450 notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19
451 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
452 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b =
453 (show ab (Not_intro ? b)).
455 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
456 for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
457 interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b =
458 (cast ? ? (show ab (Not_intro ? b))).
460 notation > "¬#'i' [ident H] term 90 b" with precedence 19
461 for @{ 'Not_intro (λ${ident H}.show $b ?) }.
462 interpretation "Not_intro KO" 'Not_intro a = (cast ? ? (Not_intro ? (cast ? ? a))).
463 interpretation "Not_intro OK" 'Not_intro a = (Not_intro ? a).
466 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
467 for @{ 'Not_elim_ko_1 $ab $a $b }.
468 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b =
469 (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a)))).
471 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19
472 for @{ 'Not_elim_ko_2 $ab $a $b }.
473 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b =
474 (cast ? ? (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a))))).
476 notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19
477 for @{ 'Not_elim_ok_1 $ab $a $b }.
478 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b =
479 (show b (Not_elim ? ab a)).
481 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19
482 for @{ 'Not_elim_ok_2 $ab $a $b }.
483 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
484 (cast ? ? (show b (Not_elim ? ab a))).
486 notation > "¬#'e' term 90 ab term 90 a" with precedence 19
487 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
488 interpretation "Not_elim KO" 'Not_elim ab a =
489 (cast ? ? (Not_elim unit (cast ? ? ab) (cast ? ? a))).
490 interpretation "Not_elim OK" 'Not_elim ab a =
494 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
495 for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
496 interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn =
497 (show Pn (cast ? ? (Raa ? (cast ? ? Px)))).
499 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
500 for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
501 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn =
502 (cast ? ? (show Pn (cast ? ? (Raa ? (cast ? ? Px))))).
504 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19
505 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
506 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn =
507 (show Pn (Raa ? Px)).
509 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
510 for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
511 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn =
512 (cast ? ? (show Pn (Raa ? Px))).
514 notation > "'RAA' [ident H] term 90 b" with precedence 19
515 for @{ 'Raa (λ${ident H}.show $b ?) }.
516 interpretation "RAA KO" 'Raa p = (cast ? unit (Raa ? (cast ? (unit_to ?) p))).
517 interpretation "RAA OK" 'Raa p = (Raa ? p).
520 notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19
521 for @{ 'Exists_intro_ko_1 $Pn $Px }.
522 interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px =
523 (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn)))).
525 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19
526 for @{ 'Exists_intro_ko_2 $Pn $Px }.
527 interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px =
528 (cast ? ? (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn))))).
530 notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19
531 for @{ 'Exists_intro_ok_1 $Pn $Px }.
532 interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px =
533 (show Px (Exists_intro ? ? ? Pn)).
535 notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19
536 for @{ 'Exists_intro_ok_2 $Pn $Px }.
537 interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px =
538 (cast ? ? (show Px (Exists_intro ? ? ? Pn))).
540 notation >"∃#'i' {term 90 t} term 90 Pt" non associative with precedence 19
541 for @{'Exists_intro $t (λw.? w) (show $Pt ?)}.
542 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
543 (cast ? ? (Exists_intro sort P t (cast ? ? Pt))).
544 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
545 (Exists_intro sort P t Pt).
548 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19
549 for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
550 interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c =
551 (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc)))).
553 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19
554 for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
555 interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
556 (cast ? ? (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc))))).
558 notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19
559 for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
560 interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
561 (show c (Exists_elim ? ? ? ExPx Pc)).
563 notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
564 for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
565 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
566 (cast ? ? (show c (Exists_elim ? ? ? ExPx Pc))).
568 definition ex_concl := λx:sort → Prop.Πy:sort.unit → x y.
569 definition ex_concl_dummy := Πy:sort.unit → unit.
570 definition fake_pred := λx:sort.unit.
572 notation >"∃#'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
573 for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}.
574 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
575 (cast ? ? (Exists_elim sort P ?
576 (cast (Exists ? P) ? ExPt)
577 (cast ex_concl_dummy (ex_concl ?) c))).
578 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
579 (Exists_elim sort P ? ExPt c).
583 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
584 for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
585 interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn =
586 (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px)))).
588 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19
589 for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
590 interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn =
591 (cast ? ? (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px))))).
593 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19
594 for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
595 interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn =
596 (show Pn (Forall_intro ? ? Px)).
598 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19
599 for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
600 interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn =
601 (cast ? ? (show Pn (Forall_intro ? ? Px))).
603 notation > "∀#'i' {ident y} term 90 Px" non associative with precedence 19
604 for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }.
605 interpretation "Forall_intro KO" 'Forall_intro P Px =
606 (cast ? ? (Forall_intro sort P (cast ? ? Px))).
607 interpretation "Forall_intro OK" 'Forall_intro P Px =
608 (Forall_intro sort P Px).
611 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19
612 for @{ 'Forall_elim_ko_1 $Px $Pn }.
613 interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn =
614 (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px)))).
616 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19
617 for @{ 'Forall_elim_ko_2 $Px $Pn }.
618 interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn =
619 (cast ? ? (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px))))).
621 notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19
622 for @{ 'Forall_elim_ok_1 $Px $Pn }.
623 interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn =
624 (show Pn (Forall_elim ? ? ? Px)).
626 notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19
627 for @{ 'Forall_elim_ok_2 $Px $Pn }.
628 interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn =
629 (cast ? ? (show Pn (Forall_elim ? ? ? Px))).
631 notation > "∀#'e' {term 90 t} term 90 Pn" non associative with precedence 19
632 for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }.
633 interpretation "Forall_elim KO" 'Forall_elim P t Px =
634 (cast ? unit (Forall_elim sort P t (cast ? ? Px))).
635 interpretation "Forall_elim OK" 'Forall_elim P t Px =
636 (Forall_elim sort P t Px).
638 (* already proved lemma *)
639 definition hide_args : ΠA:Type[0].A→A := λA:Type[0].λa:A.a.
640 notation < "t" non associative with precedence 90 for @{'hide_args $t}.
641 interpretation "hide 0 args" 'hide_args t = (hide_args ? t).
642 interpretation "hide 1 args" 'hide_args t = (hide_args ? t ?).
643 interpretation "hide 2 args" 'hide_args t = (hide_args ? t ? ?).
644 interpretation "hide 3 args" 'hide_args t = (hide_args ? t ? ? ?).
645 interpretation "hide 4 args" 'hide_args t = (hide_args ? t ? ? ? ?).
646 interpretation "hide 5 args" 'hide_args t = (hide_args ? t ? ? ? ? ?).
647 interpretation "hide 6 args" 'hide_args t = (hide_args ? t ? ? ? ? ? ?).
648 interpretation "hide 7 args" 'hide_args t = (hide_args ? t ? ? ? ? ? ? ?).
650 (* more args crashes the pattern matcher *)
652 (* already proved lemma, 0 assumptions *)
653 definition Lemma : ΠA.A→A ≝ λA:Prop.λa:A.a.
658 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
660 non associative with precedence 19
661 for @{ 'lemma_ko_1 $p ($H : $_) }.
662 interpretation "lemma_ko_1" 'lemma_ko_1 p H =
663 (show p (cast ? ? (Lemma ? (cast ? ? H)))).
668 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
669 mstyle color #ff0000 (p) \nbsp"
670 non associative with precedence 19
671 for @{ 'lemma_ko_2 $p ($H : $_) }.
672 interpretation "lemma_ko_2" 'lemma_ko_2 p H =
673 (cast ? ? (show p (cast ? ?
674 (Lemma ? (cast ? ? H))))).
680 (╲ mstyle mathsize normal (H) ╱) \nbsp)
682 non associative with precedence 19
683 for @{ 'lemma_ok_1 $p ($H : $_) }.
684 interpretation "lemma_ok_1" 'lemma_ok_1 p H =
685 (show p (Lemma ? H)).
690 (╲ mstyle mathsize normal (H) ╱) \nbsp)
691 mstyle color #ff0000 (p) \nbsp"
692 non associative with precedence 19
693 for @{ 'lemma_ok_2 $p ($H : $_) }.
694 interpretation "lemma_ok_2" 'lemma_ok_2 p H =
695 (cast ? ? (show p (Lemma ? H))).
697 notation > "'lem' 0 term 90 l" non associative with precedence 19
698 for @{ 'Lemma (hide_args ? $l : ?) }.
699 interpretation "lemma KO" 'Lemma l =
700 (cast ? ? (Lemma unit (cast unit ? l))).
701 interpretation "lemma OK" 'Lemma l = (Lemma ? l).
704 (* already proved lemma, 1 assumption *)
705 definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝
706 λA,B:Prop.λf:A⇒B.λa:A.
712 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
714 non associative with precedence 19
715 for @{ 'lemma1_ko_1 $a $p ($H : $_) }.
716 interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H =
717 (show p (cast ? ? (Lemma1 ? ? (cast ? ? H) (cast ? ? a)))).
722 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
723 mstyle color #ff0000 (p) \nbsp"
724 non associative with precedence 19
725 for @{ 'lemma1_ko_2 $a $p ($H : $_) }.
726 interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H =
727 (cast ? ? (show p (cast ? ?
728 (Lemma1 ? ? (cast ? ? H) (cast ? ? a))))).
734 (╲ mstyle mathsize normal (H) ╱) \nbsp)
736 non associative with precedence 19
737 for @{ 'lemma1_ok_1 $a $p ($H : $_) }.
738 interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H =
739 (show p (Lemma1 ? ? H a)).
744 (╲ mstyle mathsize normal (H) ╱) \nbsp)
745 mstyle color #ff0000 (p) \nbsp"
746 non associative with precedence 19
747 for @{ 'lemma1_ok_2 $a $p ($H : $_) }.
748 interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H =
749 (cast ? ? (show p (Lemma1 ? ? H a))).
752 notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19
753 for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }.
754 interpretation "lemma 1 KO" 'Lemma1 l p =
755 (cast ? ? (Lemma1 unit unit (cast (Imply unit unit) ? l) (cast unit ? p))).
756 interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 ? ? l p).
758 (* already proved lemma, 2 assumptions *)
759 definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝
760 λA,B,C:Prop.λf:A⇒B⇒C.λa:A.λb:B.
761 Imply_elim B C (Imply_elim A (B⇒C) f a) b.
765 (\emsp a \emsp\emsp\emsp b \emsp)
766 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
768 non associative with precedence 19
769 for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }.
770 interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H =
771 (show p (cast ? ? (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b)))).
775 (\emsp a \emsp\emsp\emsp b \emsp)
776 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
777 mstyle color #ff0000 (p) \nbsp"
778 non associative with precedence 19
779 for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }.
780 interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H =
781 (cast ? ? (show p (cast ? ?
782 (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b))))).
787 (\emsp a \emsp\emsp\emsp b \emsp)
788 (╲ mstyle mathsize normal (H) ╱) \nbsp)
790 non associative with precedence 19
791 for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }.
792 interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H =
793 (show p (Lemma2 ? ? ? H a b)).
797 (\emsp a \emsp\emsp\emsp b \emsp)
798 (╲ mstyle mathsize normal (H) ╱) \nbsp)
799 mstyle color #ff0000 (p) \nbsp"
800 non associative with precedence 19
801 for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }.
802 interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H =
803 (cast ? ? (show p (Lemma2 ? ? ? H a b))).
805 notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19
806 for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }.
807 interpretation "lemma 2 KO" 'Lemma2 l p q =
808 (cast ? ? (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) ? l) (cast unit ? p) (cast unit ? q))).
809 interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 ? ? ? l p q).
811 (* already proved lemma, 3 assumptions *)
812 definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝
813 λA,B,C,D:Prop.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C.
814 Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c.
818 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
819 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
821 non associative with precedence 19
822 for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }.
823 interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H =
825 (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c)))).
829 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
830 (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp)
831 mstyle color #ff0000 (p) \nbsp"
832 non associative with precedence 19
833 for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }.
834 interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H =
835 (cast ? ? (show p (cast ? ?
836 (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c))))).
841 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
842 (╲ mstyle mathsize normal (H) ╱) \nbsp)
844 non associative with precedence 19
845 for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }.
846 interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H =
847 (show p (Lemma3 ? ? ? ? H a b c)).
851 (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp)
852 (╲ mstyle mathsize normal (H) ╱) \nbsp)
853 mstyle color #ff0000 (p) \nbsp"
854 non associative with precedence 19
855 for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }.
856 interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H =
857 (cast ? ? (show p (Lemma3 ? ? ? ? H a b c))).
859 notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19
860 for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }.
861 interpretation "lemma 3 KO" 'Lemma3 l p q r =
862 (cast ? ? (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) ? l) (cast unit ? p) (cast unit ? q) (cast unit ? r))).
863 interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 ? ? ? ? l p q r).