]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/compose.ma
Added null character.
[helm.git] / matita / matita / tests / compose.ma
1
2 include "logic/equality.ma".
3
4 theorem an_1:
5 ∀ Univ:Set.
6 ∀ a:Univ.
7 ∀ is_a_theorem:Univ → Prop.
8 ∀ not:Univ → Univ.
9 ∀ or:Univ → Univ → Univ.
10 ∀ H0:∀ U:Univ.∀ V:Univ.∀ X:Univ.∀ Y:Univ.∀ Z:Univ.
11   is_a_theorem 
12     (or (not (or (not (or (not X) Y)) (or Z (or U V)))) 
13         (or (not (or (not U) X)) (or Z (or V X)))).
14 ∀ H1:∀ X:Univ.∀ Y:Univ.
15   is_a_theorem (or (not X) Y) → is_a_theorem X → is_a_theorem Y.
16 ∀ ABS:∀ X.is_a_theorem X.
17 True.
18 .
19 intros 5.
20 intros (H H1 ABS).
21
22 (* H1 o H *)
23 compose (H) with (H1) (primo secondo).
24 letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H ? ? ? ? ?)); 
25 try assumption; [1,2: apply ABS]
26 letin verifica_secondo ≝ (secondo ? ? ? ? ? ? ? = H1 ? ? (H ? ? ? ? ?) ?);
27 try assumption; [1,2: apply ABS]
28 clear verifica_primo verifica_secondo.
29 compose (H) with (primo) (terzo).
30 compose (H) with (secondo) (quarto).
31 letin verifica_terzo_quarto ≝ (terzo ? ? ? ? ? = quarto ? ? ? ? ?);
32 try assumption.
33 clear verifica_terzo_quarto.
34 clear primo secondo terzo quarto.
35
36 (* H1 o H1 *)
37 compose (H1) with (H1) (primo secondo).
38 letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H1 ? ? ? ?));
39 try assumption; [1,2,3,4,5,6: apply ABS]
40 letin verifica_secondo ≝ (secondo ? ? ? ? ? ? = H1 ? ? (H1 ? ? ? ?) ?);
41 try assumption; [1,2,3,4,5,6: apply ABS]
42 clear verifica_primo verifica_secondo.
43 clear primo secondo.
44
45 (* close H1 o H1 with H *)
46 compose H1 with H1 0. 
47 (* 
48 leaving the result under the sequent line and calling compose without 
49 the with parameter, will compose H with all the stuff under the sequent line
50 *)
51 compose 3 (H) (i1 i2 p1 p2 p3 p4 p5 p6 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12).
52 exact I.
53 qed.