From: Enrico Tassi Date: Mon, 1 Dec 2008 09:29:23 +0000 (+0000) Subject: better doc X-Git-Tag: make_still_working~4472 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5755ebe4016316a474ad8ab8d33b1a1a9187cc9e;p=helm.git better doc --- diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma index 1bc9717fd..3a5bca154 100644 --- 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".