X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction.ma;h=47cb9e4ab2f74b5874ca15720908492528184e99;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=3a5bca154955900e112ae9f7828e0f078c3cd129;hpb=5755ebe4016316a474ad8ab8d33b1a1a9187cc9e;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 3a5bca154..47cb9e4ab 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -1,3 +1,17 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
 (* Istruzioni: 
 
      http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html 
@@ -65,7 +79,7 @@ L'albero si descrive partendo dalla radice. Le regole
 con premesse multiple sono seguite da `[`, `|` e `]`.
 Ad esempio: 
 
-        apply rule (∧_i (A∨B) ⊥);
+        apply rule (∧#i (A∨B) ⊥);
           [ …continua qui il sottoalbero per (A∨B)
           | …continua qui il sottoalbero per ⊥
           ] 
@@ -75,7 +89,7 @@ gli argomenti delle regole sono le formule che normalmente
 scrivete sopra la linea che rappresenta l'applicazione della
 regola stessa. Ad esempio:
 
-        aply rule (∨_e (A∨B) [h1] C [h2] C);
+        aply rule (∨#e (A∨B) [h1] C [h2] C);
           [ …prova di (A∨B)
           | …prova di C sotto l'ipotesi A (di nome h1)  
           | …prova di C sotto l'ipotesi B (di nome h2)
@@ -124,14 +138,16 @@ far seguire le parentesi quadre come spiegato in precedenza.
 Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
 per rappresentare l'albero di prova del lemma che si sta riutilizzando.
 
-Per motivi che saranno più chiari una volta studiate logiche del primo ordine
-o di ordine superiore, i lemmi che si intende riutilizzare è bene
-che siano dimostrati astratti sugli atomi, ovvero per ogni
-atomo `A`...`Z` che compare nella formula, è bene aggiungere
-una quantificazione all'inizio della formula stessa (es. `∀A:CProp.`)
-e iniziare la dimostrazione con il comando `assume`. In tale
-modo il lemma EM può essere utilizzato sia per dimostrare 
-`A ∨ ¬A` sia `B ∨ ¬B` sia `(A∨C) ∨ ¬(A∨C)` ...
+Per motivi che saranno più chiari una volta studiate logiche del 
+primo ordine o di ordine superiore, i lemmi che si intende 
+riutilizzare è bene che siano dimostrati astratti sugli atomi. 
+Ovvero per ogni atomo `A`...`Z` che compare nella formula, 
+è bene aggiungere una quantificazione all'inizio della formula stessa.
+Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
+La dimostrazione deve poi iniziare con il comando `assume`. 
+
+In tale modo il lemma EM può essere utilizzato sia per dimostrare 
+`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
 
 DOCEND*)
 
@@ -146,20 +162,20 @@ apply rule (prove (A ∨ ¬A));
 (* qui inizia l'albero, eseguite passo passo osservando come
    si modifica l'albero. *)
 apply rule (RAA [H] (⊥)).
-apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 	[ apply rule (discharge [H]).
-	| apply rule (⊥_e (⊥));
-	  apply rule (¬_e (¬¬A) (¬A));
-	   [ apply rule (¬_i [K] (⊥)).
-       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+	| apply rule (⊥#e (⊥));
+	  apply rule (¬#e (¬¬A) (¬A));
+	   [ apply rule (¬#i [K] (⊥)).
+       apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 	      [ (*BEGIN*)apply rule (discharge [H]).(*END*)
-	      | (*BEGIN*)apply rule (∨_i_r (¬A)).
+	      | (*BEGIN*)apply rule (∨#i_r (¬A)).
           apply rule (discharge [K]).(*END*)
 	      ]
-	   | (*BEGIN*)apply rule (¬_i [K] (⊥)).
-       apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+	   | (*BEGIN*)apply rule (¬#i [K] (⊥)).
+       apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
 	      [ apply rule (discharge [H]).
-	      | apply rule (∨_i_l (A)).
+	      | apply rule (∨#i_l (A)).
           apply rule (discharge [K]).
 	      ](*END*)
 	   ]
@@ -169,28 +185,28 @@ qed.
 theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
 apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
 (*BEGIN*)
-apply rule (⇒_i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
-apply rule (⇒_i [h2] (G ∨ L ⇒ ¬L ⇒ E));
-apply rule (⇒_i [h3] (¬L ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (G∨L) [h5] (E) [h6] (E));
+apply rule (⇒#i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒#i [h2] (G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒#i [h3] (¬L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨L) [h5] (E) [h6] (E));
 	[ apply rule (discharge [h3]);
-	| apply rule (∨_e (E∨C) [h6] (E) [h7] (E));
-	    [ apply rule (⇒_e (¬L ⇒ E∨C) (¬L));
+	| apply rule (∨#e (E∨C) [h6] (E) [h7] (E));
+	    [ apply rule (⇒#e (¬L ⇒ E∨C) (¬L));
 	        [ apply rule (discharge [h2]);
 	        | apply rule (discharge [h4]);
 	        ]
 	    | apply rule (discharge [h6]);
-	    | apply rule (⇒_e (C∧G ⇒ E) (C∧G));
+	    | apply rule (⇒#e (C∧G ⇒ E) (C∧G));
 	        [ apply rule (discharge [h1]);
-	        | apply rule (∧_i (C) (G));
+	        | apply rule (∧#i (C) (G));
 	            [ apply rule (discharge [h7]);
 	            | apply rule (discharge [h5]);
              	]
 	        ]
 	    ]
-	| apply rule (⊥_e (⊥));
-	  apply rule (¬_e (¬L) (L));
+	| apply rule (⊥#e (⊥));
+	  apply rule (¬#e (¬L) (L));
 	    [ apply rule (discharge [h4]);
 	    | apply rule (discharge [h6]);
 	    ]
@@ -201,23 +217,23 @@ qed.
 theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
 apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
 (*BEGIN*)
-apply rule (⇒_i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
-apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
-apply rule (⇒_i [h3] (D ⇒ C));
-apply rule (⇒_i [h4] (C));
-apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
+apply rule (⇒#i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
+apply rule (⇒#i [h2] ((D ⇒ A) ⇒ D ⇒ C));
+apply rule (⇒#i [h3] (D ⇒ C));
+apply rule (⇒#i [h4] (C));
+apply rule (∨#e (B∨¬B) [h5] (C) [h6] (C));
 	[ apply rule (lem 0 EM);
-	| apply rule (⇒_e (B∧D⇒C) (B∧D));
+	| apply rule (⇒#e (B∧D⇒C) (B∧D));
 	    [ apply rule (discharge [h2]);
-    	| apply rule (∧_i (B) (D));
+    	| apply rule (∧#i (B) (D));
 	        [ apply rule (discharge [h5]);
 	        | apply rule (discharge [h4]);
 	        ]
 	    ] 
-	| apply rule (⇒_e (A∧¬B⇒C) (A∧¬B));
+	| apply rule (⇒#e (A∧¬B⇒C) (A∧¬B));
 	    [ apply rule (discharge [h1]);
-	    | apply rule (∧_i (A) (¬B));
-	        [ apply rule (⇒_e (D⇒A) (D));
+	    | apply rule (∧#i (A) (¬B));
+	        [ apply rule (⇒#e (D⇒A) (D));
 	            [ apply rule (discharge [h3]);
 	            | apply rule (discharge [h4]);
 	            ]
@@ -233,25 +249,25 @@ qed.
 theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
 apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
 (*BEGIN*)
-apply rule (⇒_i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
-apply rule (⇒_i [h2] ((L⇒F) ⇒ L ⇒ E));
-apply rule (⇒_i [h3] (L ⇒ E));
-apply rule (⇒_i [h4] (E));
-apply rule (∨_e (G∨E) [h5] (E) [h6] (E));
-	[ apply rule (⇒_e (F ⇒ G∨E) (F));
+apply rule (⇒#i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
+apply rule (⇒#i [h2] ((L⇒F) ⇒ L ⇒ E));
+apply rule (⇒#i [h3] (L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨E) [h5] (E) [h6] (E));
+	[ apply rule (⇒#e (F ⇒ G∨E) (F));
 	    [ apply rule (discharge [h1]);
-	    | apply rule (⇒_e (L⇒F) (L));
+	    | apply rule (⇒#e (L⇒F) (L));
 	        [ apply rule (discharge [h3]);
 	        | apply rule (discharge [h4]);
 	        ]
 	    ]
-	|apply rule (∨_e (¬L∨E) [h7] (E) [h8] (E));
-	    [ apply rule (⇒_e (G⇒¬L∨E) (G));
+	|apply rule (∨#e (¬L∨E) [h7] (E) [h8] (E));
+	    [ apply rule (⇒#e (G⇒¬L∨E) (G));
 	        [ apply rule (discharge [h2]);
 	        | apply rule (discharge [h5]);
 	        ]
-	    | apply rule (⊥_e (⊥));
-        apply rule (¬_e (¬L) (L));
+	    | apply rule (⊥#e (⊥));
+        apply rule (¬#e (¬L) (L));
 	        [ apply rule (discharge [h7]);
 	        | apply rule (discharge [h4]);
 	        ]
@@ -265,23 +281,23 @@ qed.
 theorem ex4: ¬(A∧B) ⇒ ¬A∨¬B.
 apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 (*BEGIN*)
-apply rule (⇒_i [h1] (¬A∨¬B));
-apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
+apply rule (⇒#i [h1] (¬A∨¬B));
+apply rule (∨#e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
 	[ apply rule (lem 0 EM);
-	| apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
+	| apply rule (∨#e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
 	    [ apply rule (lem 0 EM);
-	    | apply rule (⊥_e (⊥));
-	      apply rule (¬_e (¬(A∧B)) (A∧B));
+	    | apply rule (⊥#e (⊥));
+	      apply rule (¬#e (¬(A∧B)) (A∧B));
 	        [ apply rule (discharge [h1]);
-	        | apply rule (∧_i (A) (B));
+	        | apply rule (∧#i (A) (B));
 	            [ apply rule (discharge [h2]);
 	            | apply rule (discharge [h4]);
 	            ]
 	        ]
-	    | apply rule (∨_i_r (¬B));
+	    | apply rule (∨#i_r (¬B));
         apply rule (discharge [h5]);
 	    ]
-	| apply rule (∨_i_l (¬A));
+	| apply rule (∨#i_l (¬A));
     apply rule (discharge [h3]);
 	]
 (*END*)
@@ -290,24 +306,24 @@ qed.
 theorem ex5: ¬(A∨B) ⇒ (¬A ∧ ¬B).
 apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 (*BEGIN*)
-apply rule (⇒_i [h1] (¬A ∧ ¬B));
-apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
+apply rule (⇒#i [h1] (¬A ∧ ¬B));
+apply rule (∨#e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
 	[ apply rule (lem 0 EM);
-	| apply rule (⊥_e (⊥));
-    apply rule (¬_e (¬(A∨B)) (A∨B));
+	| apply rule (⊥#e (⊥));
+    apply rule (¬#e (¬(A∨B)) (A∨B));
 	    [ apply rule (discharge [h1]);
-	    | apply rule (∨_i_l (A));
+	    | apply rule (∨#i_l (A));
         apply rule (discharge [h2]);
 	    ]
-	| apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
+	| apply rule (∨#e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
 	    [ apply rule (lem 0 EM);
-	    | apply rule (⊥_e (⊥));
-        apply rule (¬_e (¬(A∨B)) (A∨B));
+	    | apply rule (⊥#e (⊥));
+        apply rule (¬#e (¬(A∨B)) (A∨B));
 	        [ apply rule (discharge [h1]);
-	        | apply rule (∨_i_r (B));
+	        | apply rule (∨#i_r (B));
             apply rule (discharge [h10]);
 	        ] 
-	    | apply rule (∧_i (¬A) (¬B));
+	    | apply rule (∧#i (¬A) (¬B));
 	        [ apply rule (discharge [h3]);
 	        |apply rule (discharge [h11]);
 	        ]
@@ -319,17 +335,17 @@ qed.
 theorem ex6: ¬A ∧ ¬B ⇒ ¬(A∨B).
 apply rule (prove (¬A ∧ ¬B ⇒ ¬(A∨B)));
 (*BEGIN*)
-apply rule (⇒_i [h1] (¬(A∨B)));
-apply rule (¬_i [h2] (⊥));
-apply rule (∨_e (A∨B) [h3] (⊥) [h3] (⊥));
+apply rule (⇒#i [h1] (¬(A∨B)));
+apply rule (¬#i [h2] (⊥));
+apply rule (∨#e (A∨B) [h3] (⊥) [h3] (⊥));
 	[ apply rule (discharge [h2]);
-	| apply rule (¬_e (¬A) (A));
-	    [ apply rule (∧_e_l (¬A∧¬B));
+	| apply rule (¬#e (¬A) (A));
+	    [ apply rule (∧#e_l (¬A∧¬B));
         apply rule (discharge [h1]);
 	    | apply rule (discharge [h3]);
 	    ]
-	| apply rule (¬_e (¬B) (B));
-	    [ apply rule (∧_e_r (¬A∧¬B));
+	| apply rule (¬#e (¬B) (B));
+	    [ apply rule (∧#e_r (¬A∧¬B));
         apply rule (discharge [h1]);
 	    | apply rule (discharge [h3]);
 	    ]
@@ -340,12 +356,12 @@ qed.
 theorem ex7: ((A ⇒ ⊥) ⇒ ⊥) ⇒ A.
 apply rule (prove (((A ⇒ ⊥) ⇒ ⊥) ⇒ A));
 (*BEGIN*)
-apply rule (⇒_i [h1] (A));
+apply rule (⇒#i [h1] (A));
 apply rule (RAA [h2] (⊥));
-apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
+apply rule (⇒#e ((A⇒⊥)⇒⊥) (A⇒⊥));
 	[ apply rule (discharge [h1]);
-	| apply rule (⇒_i [h3] (⊥));
-	  apply rule (¬_e (¬A) (A));
+	| apply rule (⇒#i [h3] (⊥));
+	  apply rule (¬#e (¬A) (A));
 	    [ apply rule (discharge [h2]);
 	    | apply rule (discharge [h3]);
 	    ]