https://www.glc.us.es/~jalonso/LMF2020/index.php?action=history&feed=atom&title=Rel_3 Rel 3 - Historial de revisiones 2026-07-20T11:40:38Z Historial de revisiones para esta página en el wiki MediaWiki 1.31.14 https://www.glc.us.es/~jalonso/LMF2020/index.php?title=Rel_3&diff=264&oldid=prev Mjoseh: Protegió «Rel 3» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido)) 2020-03-17T16:14:15Z <p>Protegió «<a href="/~jalonso/LMF2020/index.php/Rel_3" title="Rel 3">Rel 3</a>» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))</p> <table class="diff diff-contentalign-left" data-mw="interface"> <tr class="diff-title" lang="es"> <td colspan="1" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="1" style="background-color: #fff; color: #222; text-align: center;">Revisión del 16:14 17 mar 2020</td> </tr><tr><td colspan="2" class="diff-notice" lang="es"><div class="mw-diff-empty">(Sin diferencias)</div> </td></tr></table> Mjoseh https://www.glc.us.es/~jalonso/LMF2020/index.php?title=Rel_3&diff=263&oldid=prev Mjoseh: Página creada con «<source lang = "isabelle"> chapter ‹ R3: Deducción natural proposicional(II) › theory R3_sol imports Main begin text ‹--------------------------------------------…» 2020-03-17T16:14:00Z <p>Página creada con «&lt;source lang = &quot;isabelle&quot;&gt; chapter ‹ R3: Deducción natural proposicional(II) › theory R3_sol imports Main begin text ‹--------------------------------------------…»</p> <p><b>Página nueva</b></p><div>&lt;source lang = &quot;isabelle&quot;&gt;<br /> chapter ‹ R3: Deducción natural proposicional(II) ›<br /> <br /> theory R3_sol<br /> imports Main <br /> begin<br /> <br /> text ‹------------------------------------------------------------------ <br /> El objetivo de esta relación es demostrar cada uno de los ejercicios<br /> usando sólo las reglas básicas de deducción natural de la lógica<br /> proposicional (sin usar los método simp ni auto).<br /> <br /> Para cada ejercicio dar una demostración estructurada y otra<br /> aplicativa.<br /> <br /> Las reglas básicas de la deducción natural son las siguientes:<br /> · conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br /> · conjunct1: P ∧ Q ⟹ P<br /> · conjunct2: P ∧ Q ⟹ Q <br /> · notnotD: ¬¬ P ⟹ P<br /> · notnotI: P ⟹ ¬¬ P<br /> · mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br /> · mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br /> · impI: (P ⟹ Q) ⟹ P ⟶ Q<br /> · disjI1: P ⟹ P ∨ Q<br /> · disjI2: Q ⟹ P ∨ Q<br /> · disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br /> · FalseE: False ⟹ P<br /> · notE: ⟦¬P; P⟧ ⟹ R<br /> · notI: (P ⟹ False) ⟹ ¬P<br /> · iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br /> · iffD1: ⟦Q = P; Q⟧ ⟹ P <br /> · iffD2: ⟦P = Q; Q⟧ ⟹ P<br /> · ccontr: (¬P ⟹ False) ⟹ P<br /> ---------------------------------------------------------------------›<br /> <br /> text ‹Se usarán las reglas notnotI y mt que demostramos a continuación.›<br /> <br /> lemma notnotI: &quot;P ⟹ ¬¬ P&quot;<br /> by auto<br /> <br /> lemma mt: &quot;⟦F ⟶ G; ¬G⟧ ⟹ ¬F&quot;<br /> by auto<br /> <br /> section ‹ Disyunciones ›<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 25. Demostrar<br /> p ⊢ p ∨ q<br /> ------------------------------------------------------------------ ›<br /> lemma ejercicio_25:<br /> assumes &quot;p&quot;<br /> shows &quot;p ∨ q&quot;<br /> proof -<br /> show &quot;p∨q&quot; using assms by (rule disjI1)<br /> qed<br /> <br /> lemma ej25: &quot;p ⟹ p ∨ q&quot;<br /> apply (erule disjI1)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 26. Demostrar<br /> q ⊢ p ∨ q<br /> ------------------------------------------------------------------ ›<br /> lemma ejercicio_26:<br /> assumes &quot;q&quot;<br /> shows &quot;p ∨ q&quot;<br /> proof -<br /> show &quot;p∨q&quot; using assms by (rule disjI2)<br /> qed<br /> <br /> lemma ej26: &quot;q ⟹ p ∨ q&quot;<br /> apply (erule disjI2)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 27. Demostrar<br /> p ∨ q ⊢ q ∨ p<br /> ------------------------------------------------------------------ ›<br /> lemma ejercicio_27a:<br /> assumes &quot;p ∨ q&quot;<br /> shows &quot;q ∨ p&quot;<br /> proof - <br /> have &quot;p ∨ q&quot; using assms by this<br /> moreover<br /> { assume 2: &quot;p&quot;<br /> have &quot;q ∨ p&quot; using 2 by (rule disjI2) }<br /> moreover<br /> { assume 3: &quot;q&quot;<br /> have &quot;q ∨ p&quot; using 3 by (rule disjI1) }<br /> ultimately show &quot;q ∨ p&quot; by (rule disjE) <br /> qed <br /> <br /> lemma ejercicio_27b:<br /> assumes &quot;p ∨ q&quot;<br /> shows &quot;q ∨ p&quot;<br /> proof - <br /> note `p ∨ q`<br /> moreover<br /> { assume &quot;p&quot;<br /> then have &quot;q ∨ p&quot; ..}<br /> moreover<br /> { assume &quot;q&quot;<br /> then have &quot;q ∨ p&quot; .. }<br /> ultimately show &quot;q ∨ p&quot; .. <br /> qed <br /> <br /> <br /> lemma ejercicio_27c:<br /> assumes &quot;p ∨ q&quot;<br /> shows &quot;q ∨ p&quot;<br /> using assms<br /> proof (rule disjE)<br /> assume &quot;p&quot;<br /> then show &quot;q ∨ p&quot; ..<br /> next<br /> assume &quot;q&quot;<br /> then show &quot;q ∨ p&quot; ..<br /> qed<br /> <br /> lemma ejercicio_27d:<br /> assumes &quot;p ∨ q&quot;<br /> shows &quot;q ∨ p&quot;<br /> using assms by auto<br /> <br /> lemma ej27: &quot;p ∨ q ⟹ q ∨ p&quot;<br /> apply (erule disjE)<br /> apply (erule disjI2)<br /> apply (erule disjI1)<br /> done<br /> <br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 28. Demostrar<br /> q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_28b:<br /> assumes &quot;q ⟶ r&quot; <br /> shows &quot;p ∨ q ⟶ p ∨ r&quot;<br /> proof (rule impI)<br /> assume &quot;p ∨ q&quot;<br /> show &quot;p ∨ r&quot;<br /> using `p ∨ q`<br /> proof (rule disjE)<br /> assume &quot;p&quot;<br /> then show &quot;p ∨ r&quot; ..<br /> next<br /> assume &quot;q&quot;<br /> with assms(1) have &quot;r&quot; ..<br /> then show &quot;p ∨ r&quot; ..<br /> qed<br /> qed<br /> <br /> lemma ejercicio_28c:<br /> assumes &quot;q ⟶ r&quot; <br /> shows &quot;p ∨ q ⟶ p ∨ r&quot;<br /> using assms by auto<br /> <br /> lemma ej28: &quot;q ⟶ r ⟹ p ∨ q ⟶ p ∨ r&quot;<br /> apply (rule impI)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (drule mp)<br /> apply assumption<br /> apply (erule disjI2)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 29. Demostrar<br /> p ∨ p ⊢ p<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_29b:<br /> assumes &quot;p ∨ p&quot;<br /> shows &quot;p&quot;<br /> using assms<br /> proof (rule disjE)<br /> assume &quot;p&quot;<br /> then show &quot;p&quot; .<br /> next<br /> assume &quot;p&quot;<br /> then show &quot;p&quot; .<br /> qed<br /> <br /> lemma ejercicio_29c:<br /> assumes &quot;p ∨ p&quot;<br /> shows &quot;p&quot;<br /> using assms by auto<br /> <br /> lemma ej29: &quot;p ∨ p ⟹ p&quot;<br /> apply (erule disjE)<br /> apply assumption+<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 30. Demostrar<br /> p ⊢ p ∨ p<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_30a:<br /> assumes &quot;p&quot; <br /> shows &quot;p ∨ p&quot;<br /> using assms<br /> proof (rule disjI1)<br /> qed<br /> <br /> lemma ejercicio_30b:<br /> assumes &quot;p&quot; <br /> shows &quot;p ∨ p&quot;<br /> using assms by auto<br /> <br /> lemma ej30: &quot;p ⟹ p ∨ p&quot;<br /> apply (erule disjI1)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 31. Demostrar<br /> p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_31a:<br /> assumes &quot;p ∨ (q ∨ r)&quot; <br /> shows &quot;(p ∨ q) ∨ r&quot;<br /> using assms<br /> proof (rule disjE)<br /> assume &quot;p&quot;<br /> then have &quot;p ∨ q&quot; by (rule disjI1)<br /> then show &quot;(p ∨ q) ∨ r&quot; by (rule disjI1)<br /> next<br /> assume &quot;q ∨ r&quot; <br /> then show &quot;(p ∨ q) ∨ r&quot;<br /> proof (rule disjE)<br /> assume &quot;q&quot;<br /> then have &quot;p ∨ q&quot; by (rule disjI2)<br /> then show &quot;(p ∨ q) ∨ r&quot; by (rule disjI1)<br /> next<br /> assume &quot;r&quot;<br /> then show &quot;(p ∨ q) ∨ r&quot; by (rule disjI2)<br /> qed<br /> qed<br /> <br /> lemma ejercicio_31b:<br /> assumes &quot;p ∨ (q ∨ r)&quot; <br /> shows &quot;(p ∨ q) ∨ r&quot;<br /> using assms by auto<br /> <br /> lemma ej31: &quot;p ∨ (q ∨ r) ⟹ (p ∨ q) ∨ r&quot;<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (erule disjI1)<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (erule disjI2)<br /> apply (erule disjI2)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 32. Demostrar<br /> (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_32:<br /> assumes &quot;(p ∨ q) ∨ r&quot; <br /> shows &quot;p ∨ (q ∨ r)&quot;<br /> oops<br /> <br /> lemma ejercicio_32b:<br /> assumes &quot;(p ∨ q) ∨ r&quot; <br /> shows &quot;p ∨ (q ∨ r)&quot;<br /> using ‹(p ∨ q) ∨ r›<br /> proof (rule disjE)<br /> assume &quot;p ∨ q&quot; <br /> then show &quot;p ∨ (q ∨ r)&quot;<br /> proof (rule disjE)<br /> assume &quot;p&quot; <br /> then show &quot;p ∨ (q ∨ r)&quot; by (rule disjI1)<br /> next<br /> assume &quot;q&quot; <br /> then have &quot;q ∨ r&quot; by (rule disjI1)<br /> then show &quot;p ∨ (q ∨ r)&quot; by (rule disjI2)<br /> qed<br /> next<br /> assume &quot;r&quot; <br /> then have &quot;q ∨ r&quot; by (rule disjI2)<br /> then show &quot;p ∨ (q ∨ r)&quot; by (rule disjI2)<br /> qed<br /> <br /> lemma ej32: &quot;(p ∨ q) ∨ r ⟹ p ∨ (q ∨ r)&quot;<br /> apply (erule disjE)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (rule disjI2)<br /> apply (erule disjI1)<br /> apply (rule disjI2)<br /> apply (erule disjI2)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 33. Demostrar<br /> p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_33:<br /> assumes &quot;p ∧ (q ∨ r)&quot; <br /> shows &quot;(p ∧ q) ∨ (p ∧ r)&quot;<br /> oops<br /> <br /> lemma ejercicio_33b:<br /> assumes &quot;p ∧ (q ∨ r)&quot; <br /> shows &quot;(p ∧ q) ∨ (p ∧ r)&quot;<br /> proof-<br /> have &quot;p&quot; using ‹p ∧ (q ∨ r)› by (rule conjunct1)<br /> show &quot;(p ∧ q) ∨ (p ∧ r)&quot;<br /> proof (rule disjE)<br /> assume &quot;q&quot; <br /> have &quot;p ∧ q&quot; using ‹p› ‹q› by (rule conjI)<br /> then show &quot;(p ∧ q) ∨ (p ∧ r)&quot; by (rule disjI1)<br /> next<br /> assume &quot;r&quot; <br /> have &quot;p ∧ r&quot; using ‹p› ‹r› by (rule conjI)<br /> then show &quot;(p ∧ q) ∨ (p ∧ r)&quot; by (rule disjI2)<br /> next<br /> show &quot;q ∨ r&quot; using ‹p ∧ (q ∨ r)› by (rule conjunct2)<br /> qed<br /> qed<br /> <br /> <br /> lemma ej33: &quot;p ∧ (q ∨ r) ⟹ (p ∧ q) ∨ (p ∧ r)&quot;<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (rule conjI)<br /> apply assumption<br /> apply assumption<br /> apply (rule disjI2)<br /> apply (rule conjI)<br /> apply assumption<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 34. Demostrar<br /> (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_34a:<br /> assumes &quot;(p ∧ q) ∨ (p ∧ r)&quot; <br /> shows &quot;p ∧ (q ∨ r)&quot;<br /> using assms<br /> proof <br /> assume &quot;p∧q&quot;<br /> show &quot;p ∧ (q ∨ r)&quot;<br /> proof (rule conjI)<br /> show &quot;p&quot; using `p∧q` ..<br /> next<br /> have &quot;q&quot; using `p∧q` ..<br /> then show &quot;q∨r&quot; by (rule disjI1)<br /> qed<br /> next<br /> assume &quot;p∧r&quot;<br /> show &quot;p ∧ (q ∨ r)&quot;<br /> proof (rule conjI)<br /> show &quot;p&quot; using `p∧r` ..<br /> next<br /> have &quot;r&quot; using `p∧r` ..<br /> then show &quot;q∨r&quot; by (rule disjI2)<br /> qed<br /> qed<br /> <br /> lemma ejercicio_34b:<br /> assumes &quot;(p ∧ q) ∨ (p ∧ r)&quot; <br /> shows &quot;p ∧ (q ∨ r)&quot;<br /> using assms by auto<br /> <br /> lemma ej34: &quot;(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)&quot;<br /> apply (rule conjI)<br /> apply (erule disjE)<br /> apply (erule conjunct1)<br /> apply (erule conjunct1)<br /> apply (erule disjE)<br /> apply (erule conjE)<br /> apply (rule disjI1)<br /> apply assumption<br /> apply (erule conjE)<br /> apply (erule disjI2)<br /> done<br /> <br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 35. Demostrar<br /> p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_35:<br /> assumes &quot;p ∨ (q ∧ r)&quot; <br /> shows &quot;(p ∨ q) ∧ (p ∨ r)&quot;<br /> oops<br /> <br /> lemma ejercicio_35b:<br /> assumes &quot;p ∨ (q ∧ r)&quot; <br /> shows &quot;(p ∨ q) ∧ (p ∨ r)&quot;<br /> using ‹p ∨ (q ∧ r)› <br /> proof (rule disjE)<br /> assume &quot;p&quot; <br /> then have &quot;p ∨ r&quot; by (rule disjI1)<br /> have &quot;p ∨ q&quot; using ‹p› by (rule disjI1)<br /> then show &quot;(p ∨ q) ∧ (p ∨ r)&quot; using ‹p ∨ r› by (rule conjI)<br /> next<br /> assume &quot;q ∧ r&quot;<br /> then have &quot;r&quot; by (rule conjunct2)<br /> then have &quot;p ∨ r&quot; by (rule disjI2)<br /> have &quot;q&quot; using ‹q ∧ r› by (rule conjunct1)<br /> then have &quot;p ∨ q&quot; by (rule disjI2)<br /> then show &quot;(p ∨ q) ∧ (p ∨ r)&quot; using ‹p ∨ r› by (rule conjI)<br /> qed<br /> <br /> lemma ej35: &quot;p ∨ (q ∧ r) ⟹ (p ∨ q) ∧ (p ∨ r)&quot;<br /> apply (erule disjE)<br /> apply (rule conjI)<br /> apply (erule disjI1)<br /> apply (erule disjI1)<br /> apply (erule conjE)<br /> apply (rule conjI)<br /> apply (erule disjI2)<br /> apply (erule disjI2)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 36. Demostrar<br /> (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_36a:<br /> assumes &quot;(p ∨ q) ∧ (p ∨ r)&quot;<br /> shows &quot;p ∨ (q ∧ r)&quot;<br /> proof -<br /> have &quot;p ∨ q&quot; using assms ..<br /> then show &quot;p ∨ (q ∧ r)&quot;<br /> proof<br /> assume &quot;p&quot;<br /> then show &quot;p ∨ (q ∧ r)&quot; by (rule disjI1)<br /> next <br /> assume &quot;q&quot;<br /> have &quot;p ∨ r&quot; using assms ..<br /> then show &quot;p ∨ (q ∧ r)&quot;<br /> proof<br /> assume &quot;p&quot;<br /> then show &quot;p ∨ (q∧r)&quot; by (rule disjI1)<br /> next<br /> assume &quot;r&quot;<br /> with `q` have &quot;q ∧ r&quot; ..<br /> then show &quot;p ∨ (q ∧ r)&quot; by (rule disjI2)<br /> qed<br /> qed<br /> qed<br /> <br /> lemma ejercicio_36b:<br /> assumes &quot;(p ∨ q) ∧ (p ∨ r)&quot;<br /> shows &quot;p ∨ (q ∧ r)&quot;<br /> using assms by auto<br /> <br /> lemma ej36: &quot;(p ∨ q) ∧ (p ∨ r) ⟹ p ∨ (q ∧ r)&quot;<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (rule disjI2)<br /> apply (rule conjI)<br /> apply assumption+<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 37. Demostrar<br /> (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_37:<br /> assumes &quot;(p ⟶ r) ∧ (q ⟶ r)&quot; <br /> shows &quot;p ∨ q ⟶ r&quot;<br /> proof (rule impI)<br /> assume &quot;p ∨ q&quot;<br /> then show &quot;r&quot;<br /> proof<br /> assume &quot;p&quot;<br /> have &quot;p ⟶ r&quot; using assms by (rule conjunct1)<br /> then show &quot;r&quot; using `p` ..<br /> next<br /> assume &quot;q&quot;<br /> have &quot;q ⟶ r&quot; using assms by (rule conjunct2)<br /> then show &quot;r&quot; using `q` ..<br /> qed<br /> qed<br /> <br /> lemma ejercicio_37b:<br /> assumes &quot;(p ⟶ r) ∧ (q ⟶ r)&quot; <br /> shows &quot;p ∨ q ⟶ r&quot;<br /> using assms by auto<br /> <br /> lemma ej37: &quot;(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r&quot;<br /> apply (rule impI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (drule mp, assumption+)+<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 38. Demostrar<br /> p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_38a:<br /> assumes &quot;p ∨ q ⟶ r&quot; <br /> shows &quot;(p ⟶ r) ∧ (q ⟶ r)&quot;<br /> proof (rule conjI)<br /> show &quot;p ⟶ r&quot;<br /> proof (rule impI)<br /> assume &quot;p&quot;<br /> then have &quot;p ∨ q&quot; ..<br /> with assms show &quot;r&quot; by (rule mp)<br /> qed<br /> next<br /> show &quot;q ⟶ r&quot;<br /> proof (rule impI)<br /> assume &quot;q&quot;<br /> then have &quot;p ∨ q&quot; ..<br /> with assms show &quot;r&quot; by (rule mp)<br /> qed<br /> qed<br /> <br /> lemma ejercicio_38b:<br /> assumes &quot;p ∨ q ⟶ r&quot; <br /> shows &quot;(p ⟶ r) ∧ (q ⟶ r)&quot;<br /> using assms by auto<br /> <br /> lemma ej38: &quot;p ∨ q ⟶ r ⟹ (p ⟶ r) ∧ (q ⟶ r)&quot;<br /> apply (rule conjI)<br /> apply (rule impI)<br /> apply (drule mp)<br /> apply (erule disjI1)<br /> apply assumption<br /> apply (rule impI)<br /> apply (drule mp)<br /> apply (erule disjI2)<br /> apply assumption<br /> done<br /> <br /> section ‹ Negaciones ›<br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 39. Demostrar<br /> p ⊢ ¬¬p<br /> ------------------------------------------------------------------ ›<br /> lemma ejercicio_39:<br /> assumes &quot;p&quot;<br /> shows &quot;¬¬p&quot;<br /> proof -<br /> show &quot;¬¬p&quot; using assms by (rule notnotI)<br /> qed<br /> <br /> lemma ej39: &quot;p ⟹ ¬¬p&quot;<br /> apply (rule notI)<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 40. Demostrar<br /> ¬p ⊢ p ⟶ q<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_40a:<br /> assumes &quot;¬p&quot; <br /> shows &quot;p ⟶ q&quot;<br /> proof<br /> assume &quot;p&quot;<br /> with assms show &quot;q&quot; by (rule notE)<br /> qed<br /> <br /> lemma ejercicio_40b:<br /> assumes &quot;¬p&quot; <br /> shows &quot;p ⟶ q&quot;<br /> using assms by auto<br /> <br /> lemma ej40: &quot;¬p ⟹ p ⟶ q&quot;<br /> apply (rule impI)<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 41. Demostrar<br /> p ⟶ q ⊢ ¬q ⟶ ¬p<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_41:<br /> assumes &quot;p ⟶ q&quot;<br /> shows &quot;¬q ⟶ ¬p&quot;<br /> proof<br /> assume &quot;¬q&quot;<br /> with assms show &quot;¬p&quot; by (rule mt)<br /> qed<br /> <br /> lemma ejercicio_41b:<br /> assumes &quot;p ⟶ q&quot;<br /> shows &quot;¬q ⟶ ¬p&quot;<br /> using assms by auto<br /> <br /> <br /> lemma ej41: &quot;p ⟶ q ⟹ ¬q ⟶ ¬p&quot;<br /> apply (rule impI)<br /> apply (rule notI)<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 42. Demostrar<br /> p∨q, ¬q ⊢ p<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_42a:<br /> assumes &quot;p∨q&quot;<br /> &quot;¬q&quot; <br /> shows &quot;p&quot;<br /> using assms(1)<br /> proof <br /> assume &quot;p&quot; then show &quot;p&quot; .<br /> next<br /> assume &quot;q&quot; <br /> with assms(2) show &quot;p&quot; by (rule notE)<br /> qed<br /> <br /> lemma ejercicio_42b:<br /> assumes &quot;p∨q&quot;<br /> &quot;¬q&quot; <br /> shows &quot;p&quot;<br /> using assms by auto<br /> <br /> lemma ej42: &quot;⟦p ∨ q; ¬q⟧ ⟹ p&quot;<br /> apply (erule disjE)<br /> apply assumption<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 43. Demostrar<br /> p ∨ q, ¬p ⊢ q<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_43a:<br /> assumes &quot;p ∨ q&quot;<br /> &quot;¬p&quot; <br /> shows &quot;q&quot;<br /> using assms(1)<br /> proof<br /> assume &quot;p&quot;<br /> with assms(2) show &quot;q&quot; by (rule notE)<br /> next<br /> assume &quot;q&quot; then show q .<br /> qed<br /> <br /> <br /> lemma ejercicio_43b:<br /> assumes &quot;p ∨ q&quot;<br /> &quot;¬p&quot; <br /> shows &quot;q&quot;<br /> using assms by auto<br /> <br /> lemma ej43: &quot;⟦p ∨ q; ¬p⟧ ⟹ q&quot;<br /> apply (erule disjE)<br /> apply (erule notE)<br /> apply assumption<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 44. Demostrar<br /> p ∨ q ⊢ ¬(¬p ∧ ¬q)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_44a:<br /> assumes &quot;p ∨ q&quot; <br /> shows &quot;¬(¬p ∧ ¬q)&quot;<br /> using assms<br /> proof <br /> assume &quot;p&quot;<br /> show &quot;¬(¬p ∧ ¬q)&quot;<br /> proof (rule notI)<br /> assume &quot;¬p ∧ ¬q&quot;<br /> then have &quot;¬p&quot; by (rule conjunct1)<br /> then show False using `p` by (rule notE)<br /> qed<br /> next<br /> assume &quot;q&quot;<br /> show &quot;¬(¬p ∧ ¬q)&quot;<br /> proof (rule notI)<br /> assume &quot;¬p ∧ ¬q&quot;<br /> then have &quot;¬q&quot; by (rule conjunct2)<br /> then show False using `q` by (rule notE)<br /> qed<br /> qed<br /> <br /> <br /> lemma ejercicio_44b:<br /> assumes &quot;p ∨ q&quot; <br /> shows &quot;¬(¬p ∧ ¬q)&quot;<br /> proof (rule notI)<br /> assume &quot;¬p ∧ ¬q&quot;<br /> show False using assms <br /> proof (rule disjE)<br /> assume &quot;p&quot;<br /> have &quot;¬p&quot; using `¬p ∧ ¬q` by (rule conjunct1)<br /> then show False using `p` by (rule notE)<br /> next<br /> assume &quot;q&quot;<br /> have &quot;¬q&quot; using `¬p ∧ ¬q` by (rule conjunct2)<br /> then show False using `q` by (rule notE)<br /> qed<br /> qed<br /> <br /> lemma ejercicio_44c:<br /> assumes &quot;p ∨ q&quot; <br /> shows &quot;¬(¬p ∧ ¬q)&quot;<br /> using assms by auto<br /> <br /> lemma ej44: &quot;p ∨ q ⟹ ¬(¬p ∧ ¬q)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule notE, assumption)+<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 45. Demostrar<br /> p ∧ q ⊢ ¬(¬p ∨ ¬q)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_45a:<br /> assumes &quot;p ∧ q&quot; <br /> shows &quot;¬(¬p ∨ ¬q)&quot;<br /> proof<br /> assume &quot;¬p ∨ ¬q&quot;<br /> then show False<br /> proof (rule disjE)<br /> assume &quot;¬p&quot;<br /> have &quot;p&quot; using assms ..<br /> with `¬ p` show False ..<br /> next<br /> assume &quot;¬q&quot;<br /> have &quot;q&quot; using assms by (rule conjunct2)<br /> with `¬ q` show False by (rule notE)<br /> qed<br /> qed<br /> <br /> <br /> lemma ejercicio_45c:<br /> assumes &quot;p ∧ q&quot; <br /> shows &quot;¬(¬p ∨ ¬q)&quot;<br /> using assms by auto<br /> <br /> lemma ej45: &quot;p ∧ q ⟹ ¬(¬p ∨ ¬q)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule notE, assumption)+<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 46. Demostrar<br /> ¬(p ∨ q) ⊢ ¬p ∧ ¬q<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_46a:<br /> assumes &quot;¬(p ∨ q)&quot; <br /> shows &quot;¬p ∧ ¬q&quot;<br /> proof<br /> show &quot;¬p&quot;<br /> proof<br /> assume &quot;p&quot;<br /> then have &quot;p ∨ q&quot; by (rule disjI1)<br /> with assms show False by (rule notE)<br /> qed<br /> next<br /> show &quot;¬q&quot;<br /> proof<br /> assume &quot;q&quot;<br /> then have &quot;p ∨ q&quot; ..<br /> with assms show False ..<br /> qed<br /> qed<br /> <br /> lemma ejercicio_46c:<br /> assumes &quot;¬(p ∨ q)&quot; <br /> shows &quot;¬p ∧ ¬q&quot;<br /> using assms by auto<br /> <br /> lemma ej46: &quot;¬(p ∨ q) ⟹ ¬p ∧ ¬q&quot;<br /> apply (rule conjI)<br /> apply (rule notI)<br /> apply (erule notE)<br /> apply (erule disjI1)<br /> apply (rule notI)<br /> apply (erule notE)<br /> apply (erule disjI2)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 47. Demostrar<br /> ¬p ∧ ¬q ⊢ ¬(p ∨ q)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_47a:<br /> assumes &quot;¬p ∧ ¬q&quot; <br /> shows &quot;¬(p ∨ q)&quot;<br /> proof<br /> assume &quot;p ∨ q&quot;<br /> then show False<br /> proof<br /> assume &quot;p&quot;<br /> have &quot;¬p&quot; using assms by (rule conjunct1)<br /> then show False using `p` by (rule notE)<br /> next<br /> assume &quot;q&quot;<br /> have &quot;¬q&quot; using assms by (rule conjunct2)<br /> then show False using `q` by (rule notE)<br /> qed<br /> qed<br /> <br /> <br /> lemma ejercicio_47c:<br /> assumes &quot;¬p ∧ ¬q&quot; <br /> shows &quot;¬(p ∨ q)&quot;<br /> using assms by auto<br /> <br /> lemma ej47: &quot;¬p ∧ ¬q ⟹ ¬(p ∨ q)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule notE, assumption)+<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 48. Demostrar<br /> ¬p ∨ ¬q ⊢ ¬(p ∧ q)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_48a:<br /> assumes &quot;¬p ∨ ¬q&quot;<br /> shows &quot;¬(p ∧ q)&quot;<br /> using assms<br /> proof<br /> assume &quot;¬p&quot;<br /> show &quot;¬(p ∧ q)&quot;<br /> proof<br /> assume &quot;p ∧ q&quot;<br /> then have &quot;p&quot; by (rule conjunct1)<br /> with `¬p` show False by (rule notE)<br /> qed<br /> next<br /> assume &quot;¬q&quot;<br /> show &quot;¬(p ∧ q)&quot;<br /> proof<br /> assume &quot;p ∧ q&quot;<br /> then have &quot;q&quot; ..<br /> with `¬q` show False ..<br /> qed<br /> qed<br /> <br /> <br /> lemma ejercicio_48b:<br /> assumes &quot;¬p ∨ ¬q&quot;<br /> shows &quot;¬(p ∧ q)&quot;<br /> proof<br /> assume &quot;p ∧ q&quot;<br /> show False<br /> using assms<br /> proof<br /> assume &quot;¬p&quot;<br /> have &quot;p&quot; using `p ∧ q` ..<br /> with `¬p` show False ..<br /> next<br /> assume &quot;¬q&quot;<br /> have &quot;q&quot; using `p ∧ q` ..<br /> with `¬q` show False ..<br /> qed<br /> qed<br /> <br /> lemma ejercicio_48c:<br /> assumes &quot;¬p ∨ ¬q&quot;<br /> shows &quot;¬(p ∧ q)&quot;<br /> using assms by auto<br /> <br /> lemma ej48: &quot;¬p ∨ ¬q ⟹ ¬(p ∧ q)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule disjE)<br /> apply (erule notE, assumption)+<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 49. Demostrar<br /> ⊢ ¬(p ∧ ¬p)<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_49a:<br /> &quot;¬(p ∧ ¬p)&quot;<br /> proof<br /> assume &quot;p ∧ ¬p&quot;<br /> then have &quot;p&quot; ..<br /> have &quot;¬ p&quot; using `p ∧ ¬p` ..<br /> then show False using `p` ..<br /> qed<br /> <br /> lemma ejercicio_49b:<br /> &quot;¬(p ∧ ¬p)&quot;<br /> by auto<br /> <br /> lemma ej49: &quot;¬(p ∧ ¬p)&quot;<br /> apply (rule notI)<br /> apply (erule conjE)<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 50. Demostrar<br /> p ∧ ¬p ⊢ q<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_50:<br /> assumes 1: &quot;p ∧ ¬p&quot; <br /> shows &quot;q&quot;<br /> proof-<br /> have 2: &quot;p&quot; using 1 by (rule conjunct1)<br /> have 3: &quot;¬p&quot; using 1 by (rule conjunct2) <br /> have 4: &quot;False&quot; using 3 2 by (rule notE)<br /> show &quot;q&quot; using 4 by (rule FalseE)<br /> qed<br /> <br /> <br /> lemma ejercicio_50b:<br /> assumes &quot;p ∧ ¬p&quot; <br /> shows &quot;q&quot;<br /> proof (rule notE)<br /> show &quot;p&quot; using ‹p ∧ ¬p› by (rule conjunct1)<br /> show &quot;¬p&quot; using ‹p ∧ ¬p› by (rule conjunct2)<br /> qed<br /> <br /> lemma ej50: &quot;p ∧ ¬p ⟹ q&quot;<br /> apply (erule conjE)<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 51. Demostrar<br /> ¬¬p ⊢ p<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_51a:<br /> assumes &quot;¬¬p&quot;<br /> shows &quot;p&quot;<br /> using assms by (rule notnotD)<br /> <br /> lemma ejercicio_51b:<br /> assumes &quot;¬¬p&quot;<br /> shows &quot;p&quot;<br /> using assms by auto<br /> <br /> lemma ej51: &quot;¬¬p ⟹ p&quot;<br /> apply (erule notnotD)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 52. Demostrar<br /> ⊢ p ∨ ¬p<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_52a:<br /> &quot;p ∨ ¬p&quot;<br /> proof -<br /> have &quot;¬¬p ∨ ¬p&quot; ..<br /> then show &quot;p ∨ ¬p&quot; by simp<br /> qed<br /> <br /> lemma ejercicio_52b:<br /> &quot;p ∨ ¬p&quot;<br /> proof -<br /> have &quot;¬p ∨ p&quot; ..<br /> then show &quot;p ∨ ¬p&quot; by (rule ejercicio_27a)<br /> qed<br /> <br /> <br /> lemma ejercicio_52c:<br /> &quot;p ∨ ¬p&quot;<br /> by auto<br /> <br /> lemma ej52: &quot;p ∨ ¬p&quot;<br /> apply (cut_tac P=&quot;¬p&quot; in excluded_middle)<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (erule notnotD)<br /> apply (erule disjI2)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 53. Demostrar<br /> ⊢ ((p ⟶ q) ⟶ p) ⟶ p<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_53b:<br /> &quot;((p ⟶ q) ⟶ p) ⟶ p&quot;<br /> proof (rule impI)<br /> assume &quot;(p ⟶ q) ⟶ p&quot;<br /> show &quot;p&quot;<br /> proof (rule ccontr)<br /> assume &quot;¬p&quot;<br /> have &quot;¬ (p ⟶ q)&quot; using `(p ⟶ q) ⟶ p` `¬p` by (rule mt)<br /> have &quot;p ⟶ q&quot; <br /> proof (rule impI)<br /> assume &quot;p&quot;<br /> show &quot;q&quot; using `¬p` `p` by (rule notE)<br /> qed<br /> show False using `¬ (p ⟶ q)` `p ⟶ q` ..<br /> qed<br /> qed<br /> <br /> <br /> lemma ejercicio_53a:<br /> &quot;((p ⟶ q) ⟶ p) ⟶ p&quot;<br /> proof (rule impI)<br /> assume &quot;(p ⟶ q) ⟶ p&quot;<br /> have &quot;¬p ∨ p&quot; by (rule excluded_middle)<br /> then show &quot;p&quot;<br /> proof (rule disjE)<br /> assume &quot;¬p&quot;<br /> have &quot;¬(p⟶ q)&quot; using `(p ⟶ q) ⟶ p` `¬p` by (rule mt)<br /> have &quot;p⟶ q&quot;<br /> proof (rule impI)<br /> assume &quot;p&quot;<br /> show &quot;q&quot; using `¬p``p` by (rule notE)<br /> qed<br /> show &quot;p&quot; using `¬(p⟶ q)` `p⟶ q` by (rule notE)<br /> next<br /> assume &quot;p&quot;<br /> then show &quot;p&quot; .<br /> qed<br /> qed<br /> <br /> <br /> <br /> lemma ejercicio_53c:<br /> &quot;((p ⟶ q) ⟶ p) ⟶ p&quot;<br /> by auto<br /> <br /> lemma ej53: &quot;((p ⟶ q) ⟶ p) ⟶ p&quot;<br /> apply (rule impI)<br /> apply (rule ccontr)<br /> (* apply (case_tac &quot;p ⟶ q&quot;) *)<br /> apply (cut_tac P=&quot;p ⟶ q&quot; in excluded_middle)<br /> apply (erule disjE)<br /> apply (erule_tac P=&quot;p ⟶ q&quot; in notE)<br /> apply (rule impI)<br /> apply (erule notE)<br /> apply assumption<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule notE)<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 54. Demostrar<br /> ¬q ⟶ ¬p ⊢ p ⟶ q<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_54:<br /> assumes &quot;¬q ⟶ ¬p&quot;<br /> shows &quot;p ⟶ q&quot;<br /> proof<br /> assume &quot;p&quot;<br /> then have &quot;¬¬p&quot; by (rule notnotI)<br /> with assms have &quot;¬¬q&quot; by (rule mt)<br /> then show &quot;q&quot; by (rule notnotD)<br /> qed<br /> <br /> lemma ej54: &quot;¬q ⟶ ¬p ⟹ p ⟶ q&quot;<br /> apply (rule impI)<br /> apply (rule ccontr)<br /> apply (erule impE)<br /> apply assumption<br /> apply (erule notE)+<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 55. Demostrar<br /> ¬(¬p ∧ ¬q) ⊢ p ∨ q<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_55a:<br /> assumes &quot;¬(¬p ∧ ¬q)&quot;<br /> shows &quot;p ∨ q&quot;<br /> proof -<br /> have &quot;¬p ∨ p&quot; ..<br /> then show &quot;p∨q&quot;<br /> proof<br /> assume &quot;¬p&quot;<br /> have &quot;¬q ∨ q&quot; ..<br /> then show &quot;p∨q&quot;<br /> proof<br /> assume &quot;¬q&quot;<br /> with `¬p` have &quot;¬p ∧ ¬q&quot; by (rule conjI)<br /> with assms show &quot;p∨q&quot; by (rule notE)<br /> next<br /> assume &quot;q&quot;<br /> then show &quot;p ∨ q&quot; ..<br /> qed<br /> next<br /> assume &quot;p&quot;<br /> then show &quot;p ∨q&quot; ..<br /> qed<br /> qed<br /> <br /> lemma ejercicio_55c:<br /> assumes &quot;¬(¬p ∧ ¬q)&quot;<br /> shows &quot;p ∨ q&quot;<br /> using assms by auto<br /> <br /> lemma ej55: &quot;¬(¬p ∧ ¬q) ⟹ p ∨ q&quot;<br /> apply (cut_tac P=p in excluded_middle)<br /> apply (erule disjE)<br /> apply (cut_tac P=q in excluded_middle)<br /> apply (erule disjE)<br /> apply (erule notE)<br /> apply (rule conjI)<br /> apply assumption+<br /> apply (erule disjI2)<br /> apply (erule disjI1)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 56. Demostrar<br /> ¬(¬p ∨ ¬q) ⊢ p ∧ q<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_56a:<br /> assumes &quot;¬(¬p ∨ ¬q)&quot; <br /> shows &quot;p ∧ q&quot;<br /> proof<br /> show &quot;p&quot;<br /> proof -<br /> have &quot;¬p ∨ p&quot; ..<br /> then show &quot;p&quot;<br /> proof<br /> assume &quot;¬p&quot;<br /> then have &quot;¬p ∨ ¬q&quot; by (rule disjI1)<br /> with `¬(¬p ∨ ¬q)` show &quot;p&quot; by (rule notE)<br /> next<br /> assume &quot;p&quot; then show &quot;p&quot; .<br /> qed<br /> qed<br /> next<br /> show &quot;q&quot;<br /> proof -<br /> have &quot;¬q ∨ q&quot; ..<br /> then show &quot;q&quot;<br /> proof<br /> assume &quot;¬q&quot;<br /> then have &quot;¬p ∨ ¬q&quot; by (rule disjI2)<br /> with `¬(¬p ∨ ¬q)` show &quot;q&quot; by (rule notE)<br /> next<br /> assume &quot;q&quot; then show &quot;q&quot; .<br /> qed<br /> qed<br /> qed<br /> <br /> <br /> lemma ejercicio_56c:<br /> assumes &quot;¬(¬p ∨ ¬q)&quot; <br /> shows &quot;p ∧ q&quot;<br /> using assms by auto<br /> <br /> lemma ej56: &quot;¬(¬p ∨ ¬q) ⟹ p ∧ q&quot;<br /> apply (rule conjI)<br /> apply (rule ccontr)<br /> apply (erule notE)<br /> apply (erule disjI1)<br /> apply (rule ccontr)<br /> apply (erule notE)<br /> apply (erule disjI2)<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 57. Demostrar<br /> ¬(p ∧ q) ⊢ ¬p ∨ ¬q<br /> ------------------------------------------------------------------ ›<br /> <br /> lemma ejercicio_57a:<br /> assumes &quot;¬(p ∧ q)&quot;<br /> shows &quot;¬p ∨ ¬q&quot;<br /> proof -<br /> have &quot;¬p ∨p&quot; ..<br /> then show &quot;¬p ∨ ¬q&quot;<br /> proof <br /> assume &quot;¬p&quot;<br /> then show &quot;¬p ∨ ¬q&quot; ..<br /> next<br /> assume &quot;p&quot;<br /> have &quot;¬q ∨ q&quot; ..<br /> then show &quot;¬p ∨ ¬q&quot;<br /> proof<br /> assume &quot;¬q&quot;<br /> then show &quot;¬p ∨ ¬q&quot; ..<br /> next<br /> assume &quot;q&quot;<br /> with `p` have &quot;p∧q&quot; by (rule conjI)<br /> with assms show &quot;¬p ∨ ¬q&quot; by (rule notE)<br /> qed<br /> qed<br /> qed<br /> <br /> lemma ejercicio_57c:<br /> assumes &quot;¬(p ∧ q)&quot;<br /> shows &quot;¬p ∨ ¬q&quot;<br /> using assms by auto<br /> <br /> lemma ej57: &quot;¬(p ∧ q) ⟹ ¬p ∨ ¬q&quot;<br /> apply (cut_tac P=p in excluded_middle)<br /> apply (erule disjE)<br /> apply (erule disjI1)<br /> apply (cut_tac P=q in excluded_middle)<br /> apply (erule disjE)<br /> apply (erule disjI2)<br /> apply (erule notE)<br /> apply (rule conjI)<br /> apply assumption+<br /> done<br /> <br /> lemma ej57_b:<br /> &quot;⟦¬(p ∧ q)⟧ ⟹ ¬p ∨ ¬q&quot;<br /> apply (rule ccontr)<br /> apply (erule notE)<br /> apply (rule conjI)<br /> apply (rule ccontr)<br /> apply (erule notE)<br /> apply (rule disjI1)<br /> apply assumption<br /> apply (rule ccontr)<br /> apply (erule notE)<br /> apply (rule disjI2)<br /> apply assumption<br /> done<br /> <br /> text ‹ --------------------------------------------------------------- <br /> Ejercicio 58. Demostrar<br /> ⊢ (p ⟶ q) ∨ (q ⟶ p)<br /> ------------------------------------------------------------------<br /> ›<br /> <br /> lemma ejercicio_58a:<br /> &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> proof -<br /> have &quot;¬p ∨ p&quot; by (rule excluded_middle)<br /> then show &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> proof <br /> assume &quot;¬p&quot;<br /> show &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> proof (rule disjI1)<br /> show &quot;p ⟶ q&quot;<br /> proof<br /> assume &quot;p&quot;<br /> with `¬ p` show &quot;q&quot; by (rule notE)<br /> qed<br /> qed<br /> next<br /> assume &quot;p&quot;<br /> show &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> proof (rule disjI2)<br /> show &quot;q ⟶ p&quot;<br /> proof (rule impI)<br /> assume &quot;q&quot;<br /> show &quot;p&quot; using `p` .<br /> qed<br /> qed<br /> qed<br /> qed<br /> <br /> <br /> lemma ejercicio_58b:<br /> &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> proof -<br /> have &quot;¬p ∨ p&quot; .. (* by (rule excluded_middle) *)<br /> then show &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> proof<br /> assume &quot;¬p&quot;<br /> show &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> proof (rule disjI1)<br /> show &quot;p ⟶ q&quot;<br /> proof<br /> assume &quot;p&quot;<br /> with `¬ p` show &quot;q&quot; .. (* by (rule notE) *)<br /> qed<br /> qed<br /> next<br /> assume &quot;p&quot;<br /> show &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> proof (rule disjI2)<br /> show &quot;q ⟶ p&quot;<br /> proof (* (rule impI) *)<br /> assume &quot;q&quot;<br /> show &quot;p&quot; using `p` .<br /> qed<br /> qed<br /> qed<br /> qed<br /> <br /> <br /> lemma ejercicio_58c:<br /> &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> by auto<br /> <br /> lemma ej58: &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> apply (cut_tac P=p in excluded_middle)<br /> apply (erule disjE)<br /> apply (rule disjI1)<br /> apply (rule impI)<br /> apply (erule notE)<br /> apply assumption<br /> apply (rule disjI2)<br /> apply (rule impI)<br /> apply assumption<br /> done<br /> <br /> end<br /> <br /> <br /> &lt;/source&gt;</div> Mjoseh