X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fnatural_deduction.ma;h=078c7fb00fe0489c74a9028d878198cdb386225d;hb=026c6c5b0e094b2e6e8244909bc5ac3d88b70b9c;hp=1bc9717fd5ec7966d41efcf09d674705955e012d;hpb=2030cae5f1a588fa6bbea50927030f83a2156d67;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 1bc9717fd..078c7fb00 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -100,6 +100,41 @@ 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.
+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*)
 
 include "didactic/support/natural_deduction.ma".