better doc

[helm.git] / helm / software / matita / library / didactic / exercises / natural_deduction.ma

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 7f941c1189ed34d408ace19df731848b1007f895..3a5bca154955900e112ae9f7828e0f078c3cd129 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -100,6 +100,39 @@ alto a sinistra.
 Applicazioni di regole errate vengono contrassegnate con
 il colore rosso.
 
+Usare i lemmi dimostrati in precedenza
+======================================
+
+Una volta dimostrati alcuni utili lemmi come `A ∨ ¬A` è possibile
+riutilizzarli in altre dimostrazioni utilizzando la "regola" `lem`.
+
+La "regola" `lem` prende come argomenti:
+
+- Il numero delle ipotesi del lemma che si vuole utilizzare, nel
+  caso del terzo escluso `0`, nel caso di `¬¬A⇒A` le ipotesi sono `1`.
+
+- Dopo il numero di ipotesi, è necessario digitare il nome del lemma.
+
+- Infine, le formule che devono essere scritte come premesse per la 
+  "regola".
+
+Ad esempio, per usare il lemma EM (terzo escluso) basta digitare
+`lem 0 EM`, mentre per usare il lemma NNAA (`¬¬A⇒A`) bisogna digitare
+`lem 1 NNAA (¬¬A)`. Ai lemmi con più di una premessa è necessario 
+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)` ...
+
 DOCEND*)
 
 include "didactic/support/natural_deduction.ma".
@@ -173,7 +206,7 @@ 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 EM);
+       [ apply rule (lem 0 EM);
        | apply rule (⇒_e (B∧D⇒C) (B∧D));
            [ apply rule (discharge [h2]);
        | apply rule (∧_i (B) (D));
@@ -234,9 +267,9 @@ 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 (lem EM);
+       [ apply rule (lem 0 EM);
        | apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
-           [ apply rule (lem EM);
+           [ apply rule (lem 0 EM);
            | apply rule (⊥_e (⊥));
              apply rule (¬_e (¬(A∧B)) (A∧B));
                [ apply rule (discharge [h1]);
@@ -259,7 +292,7 @@ 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 (lem EM);
+       [ apply rule (lem 0 EM);
        | apply rule (⊥_e (⊥));
     apply rule (¬_e (¬(A∨B)) (A∨B));
            [ apply rule (discharge [h1]);
@@ -267,7 +300,7 @@ apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
         apply rule (discharge [h2]);
            ]
        | apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
-           [ apply rule (lem EM);
+           [ apply rule (lem 0 EM);
            | apply rule (⊥_e (⊥));
         apply rule (¬_e (¬(A∨B)) (A∨B));
                [ apply rule (discharge [h1]);
@@ -318,5 +351,5 @@ apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
            ]
        ]
 (*END*)
-qed. 
+qed.