Relación 9
De Razonamiento automático (2013-14)
Revisión del 14:40 23 ene 2014 de Pabflomar (discusión | contribuciones)
header {* R9: Deducción natural proposicional (1) *}
theory R9
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación es lemas usando sólo las reglas básicas
de deducción natural de la lógica proposicional.
Las reglas básicas de la deducción natural necesarias son las
siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬P ⟹ P
· notnotI: P ⟹ ¬¬P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
---------------------------------------------------------------------
*}
text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
section {* Implicaciones *}
text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei,julrobrel, pabflomar juaruipav domlloriv"
lemma ej1_auto:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
using assms
by auto
lemma ej1:
assumes 1:"p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof -
{assume 2:"q"
{assume 3:"p"
have 4:"q⟶r" using 1 3 by (rule mp)
have "r" using 4 2 by (rule mp)}
then have "p⟶r" by (rule impI)}
then show "q⟶(p⟶r)" by (rule impI)
qed
-- "diecabmen1"
lemma Ejercicio_1:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof -
{ assume "q"
{ assume "p"
with assms have "q ⟶ r" ..
then have "r" using `q` .. }
then have "p ⟶ r" .. }
then show "q ⟶ (p ⟶ r)" ..
qed
-- "maresccas4"
lemma
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof
assume "q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ (q ⟶ r)` have "q ⟶ r" ..
thus "r" using `q`..
qed
qed
--"marescpla"
lemma 01:
assumes "p⟶(q⟶r)"
shows "q ⟶ (p⟶r)"
proof-
{assume 1: "q"
{assume 2: "p"
have "q⟶r" using assms(1) 2 by (rule mp)
then have "r" using 1 by (rule mp)}
then have "p⟶r" ..}
then show "q ⟶(p⟶r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei,julrobrel, pabflomar, domlloriv"
lemma ej2_auto:
assumes " p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
using assms by auto
lemma ej2:
assumes 1:" p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof -
{assume 2:"(p ⟶ q)"
{assume 3:"p"
have 4:"q" using 2 3 by (rule mp)
have 5:"q⟶r" using 1 3 by (rule mp)
have "r" using 5 4 by (rule mp)}
then have "p⟶r" by (rule impI)}
then show "(p ⟶ q)⟶(p⟶r)" by (rule impI)
qed
-- "diecabmen1"
lemma Ejercicio_2:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using assms `p` ..
then show "r" using `q` ..
qed
qed
-- "maresccas4"
lemma
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume "p"
have "q" using `p ⟶ q` `p` ..
have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` ..
show "r" using `q ⟶ r` `q` ..
qed
qed
--"marescpla"
lemma 02:
assumes "p⟶(q⟶r)"
shows "(p⟶q) ⟶ (p⟶r)"
proof-
{assume 1: "p⟶q"
{assume 2: "p"
have "q" using 1 2 by (rule mp)
have "q⟶r" using assms(1) 2 by (rule mp)
then have "r" using `q` by (rule mp)}
then have "p⟶r"..}
then show "(p⟶q) ⟶ (p⟶r)" ..
qed
-- "juaruipav"
lemma ej2-jua:
assumes 1: " p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume 2: " p ⟶ q"
show "p ⟶ r"
proof
assume 3: "p"
have 4: "q" using 2 3 by (rule mp)
have 5: "q⟶r" using 1 3 by (rule mp)
show "r" using 5 4 by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}
-- "irealetei, domlloriv, pabflomar"
lemma ej3_auto:"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
by auto
lemma ej3:"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof -
{ assume 1:"(p⟶(q⟶r))"
{assume 3:"p⟶q"
{assume 4:"p"
have 5: "q⟶r" using 1 4 by (rule mp)
have 6:"q" using 3 4 by (rule mp)
have "r" using 5 6 by (rule mp)}
then have "p⟶r" by (rule impI)}
then have "(p⟶q)⟶p⟶r" by (rule impI)}
then show "(p⟶(q⟶r))⟶((p⟶q)⟶p⟶r)" by (rule impI)
qed
-- "diecabmen1, maresccas4"
lemma Ejercicio_3:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume "p ⟶ q ⟶ r"
show "(p ⟶ q) ⟶ p ⟶ r"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using `p ⟶ q ⟶ r` `p` ..
then show "r" using `q` ..
qed
qed
qed
--"julrobrel"
lemma ejer_3_auto:
shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
by auto
thm ej2_auto
lemma ejer_3_detalle:
shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof -
show "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" using ej2_auto by (rule impI)
qed
--"marescpla"
lemma 03:
"(p ⟶ (q ⟶ r))⟶((p ⟶ q) ⟶ (p ⟶ r))"
proof-
{assume 1: "(p ⟶ (q ⟶ r))"
{assume 2: "(p ⟶ q)"
{assume 3: "p"
have "q" using 2 3 by (rule mp)
have "q ⟶r" using 1 3 by (rule mp)
then have "r" using `q` by (rule mp)}
then have"p⟶r" by (rule impI)}
then have "((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI)}
then show "(p ⟶ (q ⟶ r))⟶((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI)
qed
--"juaruipav"
lemma ej3-jua: " (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume 1: "p ⟶ q ⟶ r"
show "(p ⟶ q) ⟶ p ⟶ r"
proof
assume 2: "p⟶q"
show "p ⟶ r"
proof
assume 3: "p"
have 4:"q" using 2 3 ..
have 5: "q⟶r" using 1 3 by (rule mp)
show "r" using 5 4 ..
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei,julrobrel, domlloriv"
lemma ej4_auto:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
using assms by auto
-- "maresccas4"
lemma
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q ⟶ r"
proof
assume "q"
hence "p ⟶ q" ..
show "r" using `(p ⟶ q) ⟶ r` `p ⟶ q` ..
qed
qed
-- "juaruipav"
lemma ej4-jua:
assumes 1: "(p ⟶ q) ⟶ r"
shows " p ⟶ (q ⟶ r)"
proof
assume 2: "p"
show "q⟶r"
proof
assume 3: "q"
have 4: "p⟶q" using 3 by (rule impI)
show "r" using 1 4 by (rule mp)
qed
qed
--"marescpla"
lemma 04:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof-
{assume 1: "p"
{assume 2: "q"
then have "r" using 1 2 assms by simp}
then have "q⟶r" by (rule impI)}
then show "p⟶ (q ⟶ r)" by (rule impI)
qed
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}
-- "irealetei,julrobrel, domlloriv"
lemma ej5_auto:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
using assms by auto
lemma ej5:
assumes 1:"(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof -
{assume 2:"p"
have 3: "p⟶q" using 1 by (rule conjunct1)
have 4: "p⟶r" using 1 by (rule conjunct2)
have 5: "q" using 3 2 by (rule mp)
have 6: "r" using 4 2 by (rule mp)
have "q ∧ r" using 5 6 by (rule conjI)}
then show "p ⟶ q ∧ r" by (rule impI)
qed
-- "diecabmen1, maresccas4"
lemma Ejercicio_5:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof
assume "p"
have "(p ⟶ q)" using assms ..
then have "q" using `p` ..
have "(p ⟶ r)" using assms ..
then have "r" using `p` ..
with `q` show "q ∧ r" ..
qed
--"julrobrel, pabflomar, marescpla(Pero usando assms en vez de la etiqueta 0)"
lemma ejer_5_detalle:
assumes 0:"(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof -
have 1:"p⟶q" using 0 by (rule conjunct1)
have 2:"p⟶r" using 0 by (rule conjunct2)
{assume 3:"p"
have 4:"q" using 1 3 by (rule mp)
have 5:"r" using 2 3 by (rule mp)
have 6:"q ∧ r" using 4 5 by (rule conjI)
}then show "p ⟶ q ∧ r" by (rule impI)
qed
-- "juaruipav"
lemma ej5-jua:
assumes 1:"(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof
assume 2: "p"
have 3: "(p ⟶ q)" using 1 by (rule conjunct1)
have 4:"(p ⟶ r)" using 1 by (rule conjunct2)
have 5:"q" using 3 2 by (rule mp)
have 6:"r" using 4 2 by (rule mp)
show "q∧r" using 5 6 by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei,julrobrel"
lemma ej6_auto:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
using assms by auto
-- "pabflomar"
{* Me he peleado un buen rato intentando asumiendo solo una vez p. Al mirar el wiki y tal vi esta versión que hace lo que yo quería hacer usando sólo una ves una asumción. ¿Cómo se hace?
*}
lemma ej6:
assumes 1:"p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof -
{assume 2:"p"
have 3:"q∧r" using 1 2 by (rule mp)
have "q" using 3 by (rule conjunct1)}
then have 4:"p⟶q" by (rule impI)
{assume 5:"p"
have 6:"q∧r" using 1 5 by (rule mp)
have "r" using 6 by (rule conjunct2)}
then have 5:"p⟶r" by (rule impI)
show "(p⟶q) ∧ (p ⟶r)" using 4 5 by (rule conjI)
qed
-- "diecabmen1, maresccas4"
lemma Ejercicio_6:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof
{assume "p"
with assms have "q ∧ r" ..
then have "q" ..}
then show "p ⟶ q" ..
{assume "p"
with assms have "q ∧ r" ..
then have "r" ..}
then show "p ⟶ r" ..
qed
--"juaruipav"
lemma ej6-jua:
assumes 1: " p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof
{assume 2: "p"
have 3:"q∧r" using 1 2 by (rule mp)
have "q" using 3 by (rule conjunct1)}
then show "p⟶q" ..
next
{assume 5: "p"
have 6:"q∧r" using 1 5 by (rule mp)
have "r" using 6 by (rule conjunct2)}
then show "p⟶r" ..
qed
--"marescpla"
lemma 06:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof-
{assume "p"
with assms have "q ∧ r" by (rule mp)
then have "q" by (rule conjunct1)}
then have C: "p⟶q" by (rule impI)
{assume "p"
with assms have "q ∧ r" by (rule mp)
have "r" using `q ∧ r` by (rule conjunct2)}
then have "p ⟶ r" by (rule impI)
with C show "(p ⟶ q) ∧ (p ⟶ r)" by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
-- "irealetei,julrobrel, pabflomar, domlloriv"
lemma ej7_auto:
assumes " p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
using assms by auto
lemma ej7:
assumes 1:" p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof -
have 2:"p" using 1 by (rule conjunct1)
have 3:"q⟶r" using 1 by (rule conjunct2)
{assume 4:"p⟶q"
have 5:"q" using 4 2 by (rule mp)
have "r" using 3 5 by (rule mp)}
then show "(p⟶q)⟶r" by (rule impI)
qed
-- "diecabmen1, maresccas4"
lemma Ejercicio_7:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
assume "p ⟶ q"
have "p" using assms ..
with `p ⟶ q` have "q" ..
have "q ⟶ r" using assms ..
then show "r" using `q` ..
qed
-- "juaruipav"
lemma ej7:
assumes 1: " p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
assume 2: " p ⟶ q "
have 3:"p" using 1 by (rule conjunct1)
have 4:"q⟶r" using 1 by (rule conjunct2)
have 5:"q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed
--"marescpla"
lemma 07:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof-
{assume H: "(p ⟶ q)"
have "p" using assms by (rule conjunct1)
with H have "q" by (rule mp)
have "q⟶r" using assms by (rule conjunct2)
then have "r" using `q` by (rule mp)}
then show "(p ⟶ q) ⟶ r" by (rule impI)
qed
section {* Disyunciones *}
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
-- "irealetei diecabmen1, julrobrel"
lemma ej8_auto:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
using assms by auto
lemma ej8:
assumes 1:"q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof -
{assume 2:"p ∨ q"
moreover
{assume "p"
then have "p ∨ r" by (rule disjI1)}
moreover
{assume 3:"q"
have "r" using 1 3 by (rule mp)
then have "p ∨ r" by (rule disjI2)}
ultimately have "p ∨ r" by (rule disjE)}
then show "p ∨ q ⟶ p ∨ r" by (rule impI)
qed
--"julrobrel: no estoy seguro de que esto esté bien"
lemma ejer_8_detallado2:
assumes 0:"q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (cases)
assume "¬p"
show "p ∨ q ⟶ p ∨ r" using 0 by simp
next
assume "¬¬p"
show "p ∨ q ⟶ p ∨ r" using 0 by simp
qed
-- "maresccas4"
lemma
assumes "q ⟶ r"
shows "(p ∨ q) ⟶ (p ∨ r)"
proof
assume "p ∨ q"
thus "p ∨ r"
proof
{ assume "p"
thus "p ∨ r" .. }
next
{ assume "q"
have "r" using assms `q` ..
thus "p ∨ r" .. }
qed
qed
--"juaruipav: Si quito el moreover no pasa nada.. ¿y eso? tengo dos objetivos en proof"
lemma ej8:
assumes 1: " q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume 2:"p ∨ q"
thus " p ∨ r"
proof
{assume 3: "p"
then show "p ∨ r" ..}
moreover
{ assume 4: "q"
have "r" using 1 4 by (rule mp)
then show "p ∨ r" ..}
qed
qed
--"marescpla"
lemma 08:
assumes "q⟶r"
shows "p ∨ q ⟶ p ∨ r"
proof-
{assume 1: "p ∨ q"
{assume "p"
then have "p ∨ r" by (rule disjI1)}
then have 2: "p⟹p ∨ r" by simp
{assume q
with assms have "r" by (rule mp)
then have "p ∨ r" by (rule disjI2)}
then have 3: "q⟹p ∨ r" by simp
have "p ∨ q ⟹ p ∨ r" using 1 2 3 by (rule disjE)}
then show "p ∨ q ⟶ p ∨ r" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
-- "irealetei diecabmen1, julrobrel, domlloriv"
lemma ej9_auto:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
using assms by auto
lemma ej9:
assumes 1:"(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof -
{assume "p ∨ q "
moreover
{assume 2:"p"
have 3:"(p ⟶ r)" using 1 by (rule conjunct1)
have "r" using 3 2 by (rule mp)}
moreover
{assume 4:"q"
have 5:"(q ⟶ r)" using 1 by (rule conjunct2)
have "r" using 5 4 by (rule mp)}
ultimately have "r" ..}
then show "p ∨ q ⟶ r" by (rule impI)
qed
lemma ejer_9_detalle:
assumes 0:"(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof -
{assume 1:"p∨q"
moreover
{assume 2:"p"
have 3:"p⟶r" using 0 by (rule conjunct1)
have 4:"r" using 3 2 by (rule mp)}
moreover
{assume 5:"q"
have 6:"q⟶r" using 0 by (rule conjunct2)
have 7:"r" using 6 5 by (rule mp)}
ultimately have 8:"r" by (rule disjE)}
then show "p ∨ q ⟶ r" by (rule impI)
qed
-- "maresccas4"
lemma
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof
assume "p ∨ q"
thus "r"
proof
{ assume "p"
have "p ⟶ r" using assms ..
thus "r" using `p` ..}
next
{ assume "q"
have "q ⟶ r" using assms ..
thus "r" using `q`..}
qed
qed
--"juaruipav"
lemma ej9:
assumes 1: "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof
assume 2: "p ∨ q"
thus "r"
proof
{assume 3: "p"
have 4: "p⟶r" using 1 by (rule conjunct1)
show "r" using 4 3 by (rule mp)}
moreover
{assume 5: "q"
have 6: "q⟶r" using 1 by (rule conjunct2)
show "r" using 6 5 by (rule mp)}
qed
qed
--"marescpla"
lemma 09:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof-
have "p⟶r" using assms by (rule conjunct1)
have "q ⟶ r" using assms by (rule conjunct2)
{assume 1: "p ∨ q"
{assume "p"
with `p⟶r` have "r" by (rule mp)}
then have 2: "p⟹r" by simp
{assume "q"
with `q⟶r` have "r" by (rule mp)}
then have 3: "q⟹r" by simp
have "p ∨ q ⟹ r" using 1 2 3 by (rule disjE)}
then show "p ∨ q ⟶ r" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei diecabmen1, julrobrel"
lemma ej10_auto:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
using assms by auto
lemma ej10:
assumes 1:"p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof -
{assume 2:"p"
have 3:"p∨q" using 2 by (rule disjI1)
have "r" using 1 3 by (rule mp)}
then have 4:"p⟶r" by (rule impI)
{assume 5:"q"
have 6:"p∨q" using 5 by (rule disjI2)
have 7:"r" using 1 6 by (rule mp)}
then have 8:"q⟶r" by (rule impI)
show "(p⟶r)∧(q⟶r)" using 4 8 by (rule conjI)
qed
-- "maresccas4"
lemma
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof
{ assume "p"
have "p ∨ q" using `p` ..
have "r" using assms `p ∨ q` ..}
then show "p ⟶ r" ..
next
{ assume "q"
have "p ∨ q" using `q` ..
have "r" using assms `p ∨ q` ..}
thus "q ⟶ r" ..
qed
--"juaruipav, pabflomar"
lemma ej10:
assumes 1:" p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof
{assume 2 :"p"
have 3: "p ∨ q" using 2 by (rule disjI1)
have 4: "r" using 1 3 by (rule mp)}
then show "p⟶r" ..
moreover
{assume 5 :"q"
have 6: "p ∨ q" using 5 by (rule disjI2)
have 7: "r" using 1 6 by (rule mp)}
then show "q⟶r" ..
qed
--"marescpla"
lemma 10:
assumes "p ∨ q ⟶ r"
shows"(p ⟶ r) ∧ (q ⟶ r)"
proof-
{assume "p"
then have "r" using assms by simp}
then have 1: "p⟶r" by (rule impI)
{assume "q"
then have "r" using assms by simp}
then have 2: "q⟶r" by (rule impI)
show "(p ⟶ r) ∧ (q ⟶ r)" using 1 2 by (rule conjI)
qed
end