+(**************************************************************************)
+(* ___ *)
+(* ||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
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".
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));
(*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]);
(*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]);
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]);
]
]
(*END*)
-qed.
+qed.