Razonamiento automático (2010-11) - Contribuciones del usuario [es]

Relación 9

2011-03-22T17:29:47Z

Antonio:

<source lang="isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· 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
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof (rule impI)
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

text {* el 5 no me sale no entiendo como pasar de p a q dandole la vuelta*}

lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
by simp

lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
by simp

lemma ejercicio_7:
"p ⟹ q⟶p"
by simp

lemma ejercicio_8:
"p⟶(q⟶p)"
by simp

lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
by simp

lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
by simp

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
by simp

lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
by simp

lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
by simp

lemma ejercicio_13a:
"⟦p; q⟧ ⟹ p∧q"
by (rule conjI)

lemma ejercicio_14:
"p∧q ⟹ p"
by simp

lemma ejercicio_14a:
"p∧q ⟹ p"
by (rule conjunct1)

lemma ejercicio_15:
"p∧q ⟹ q"
by simp

lemma ejercicio_15a:
"p∧q ⟹ q"
by (rule conjunct2)

lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
by simp

text {* no entiendo por que no es capaz de resolverlo si ya lo tengo calculado en pyqyr*}

lemma ejercicio_16a:
"p∧(q∧r) ⟹ (p∧q)∧r"
proof -
assume p:"p"
assume q:"q"
assume qr:"q∧r"
assume pqr:"p∧(q∧r)"

from qr have r:"r" by (rule ejercicio_15a)
from pqr have pqr2:"(p∧q)∧r" by simp
from pqr2 have pyq:"(p∧q)" by (rule ejercicio_14a)
from pyq and r have pyqyr:"(p∧q)∧r" by (rule ejercicio_13a)
from pyqyr show "(p∧q)∧r" by simp
qed

lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
by simp

lemma ejercicio_18:
"p∧q ⟹ p⟶q"
by simp

lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
by simp

lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
by simp

lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
by simp

lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
by simp

lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
by simp

lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
by simp

lemma ejercicio_25:
"p ⟹ p∨q"
by simp

lemma ejercicio_26:
"q ⟹ p∨q"
by simp

lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops

lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops

lemma ejercicio_29:
"p∨p ⟹ p"
oops

lemma ejercicio_30:
"p ⟹ p∨p"
oops

lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops

lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops

lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops

lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops

lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops

lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
"p ⟹ ¬¬p"
oops

lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops

lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops

lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops

lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops

lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops

lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops

lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops

lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops

lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
"p∧¬p ⟹ q"
oops

lemma ejercicio_51:
"¬¬p ⟹ p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops

lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops

lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops

lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops

lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops

end
</source>

Relación 9

2011-03-22T17:28:39Z

Antonio:

<source lang="isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· 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
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof (rule impI)
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

text {* el 5 no me sale *}

lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
by simp

lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
by simp

lemma ejercicio_7:
"p ⟹ q⟶p"
by simp

lemma ejercicio_8:
"p⟶(q⟶p)"
by simp

lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
by simp

lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
by simp

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
by simp

lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
by simp

lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
by simp

lemma ejercicio_13a:
"⟦p; q⟧ ⟹ p∧q"
by (rule conjI)

lemma ejercicio_14:
"p∧q ⟹ p"
by simp

lemma ejercicio_14a:
"p∧q ⟹ p"
by (rule conjunct1)

lemma ejercicio_15:
"p∧q ⟹ q"
by simp

lemma ejercicio_15a:
"p∧q ⟹ q"
by (rule conjunct2)

lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
by simp

text {* no entiendo por que no es capaz de resolverlo si ya lo tengo calculado en pyqyr*}

lemma ejercicio_16a:
"p∧(q∧r) ⟹ (p∧q)∧r"
proof -
assume p:"p"
assume q:"q"
assume qr:"q∧r"
assume pqr:"p∧(q∧r)"

from qr have r:"r" by (rule ejercicio_15a)
from pqr have pqr2:"(p∧q)∧r" by simp
from pqr2 have pyq:"(p∧q)" by (rule ejercicio_14a)
from pyq and r have pyqyr:"(p∧q)∧r" by (rule ejercicio_13a)
from pyqyr show "(p∧q)∧r" by simp
qed

lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
by simp

lemma ejercicio_18:
"p∧q ⟹ p⟶q"
by simp

lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
by simp

lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
by simp

lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
by simp

lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
by simp

lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
by simp

lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
by simp

lemma ejercicio_25:
"p ⟹ p∨q"
by simp

lemma ejercicio_26:
"q ⟹ p∨q"
by simp

lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops

lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops

lemma ejercicio_29:
"p∨p ⟹ p"
oops

lemma ejercicio_30:
"p ⟹ p∨p"
oops

lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops

lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops

lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops

lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops

lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops

lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
"p ⟹ ¬¬p"
oops

lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops

lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops

lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops

lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops

lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops

lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops

lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops

lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops

lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
"p∧¬p ⟹ q"
oops

lemma ejercicio_51:
"¬¬p ⟹ p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops

lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops

lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops

lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops

lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops

end
</source>

Relación 9

2011-03-22T17:21:02Z

Antonio:

<source lang="isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· 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
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof (rule impI)
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

text {* el 5 no me sale *}

lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
by simp

lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
by simp

lemma ejercicio_7:
"p ⟹ q⟶p"
by simp

lemma ejercicio_8:
"p⟶(q⟶p)"
by simp

lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
by simp

lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
by simp

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
by simp

lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
by simp

lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
by simp

lemma ejercicio_13a:
"⟦p; q⟧ ⟹ p∧q"
by (rule conjI)

lemma ejercicio_14:
"p∧q ⟹ p"
by simp

lemma ejercicio_14a:
"p∧q ⟹ p"
by (rule conjunct1)

lemma ejercicio_15:
"p∧q ⟹ q"
by simp

lemma ejercicio_15a:
"p∧q ⟹ q"
by (rule conjunct2)

lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
by simp

text {* no entiendo por que no es capaz de resolverlo si ya lo tengo calculado en pyqyr*}

lemma ejercicio_16a:
"p∧(q∧r) ⟹ (p∧q)∧r"
proof -
assume p:"p"
assume q:"q"
assume qr:"q∧r"
assume pqr:"p∧(q∧r)"

from qr have r:"r" by (rule ejercicio_15a)
from pqr have pqr2:"(p∧q)∧r" by simp
from pqr2 have pyq:"(p∧q)" by (rule ejercicio_14a)
from pyq and r have pyqyr:"(p∧q)∧r" by (rule ejercicio_13a)
from pyqyr show "(p∧q)∧r" by simp
qed

lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
oops

lemma ejercicio_18:
"p∧q ⟹ p⟶q"
oops

lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
oops

lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
oops

lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
oops

lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
oops

lemma ejercicio_25:
"p ⟹ p∨q"
oops

lemma ejercicio_26:
"q ⟹ p∨q"
oops

lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops

lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops

lemma ejercicio_29:
"p∨p ⟹ p"
oops

lemma ejercicio_30:
"p ⟹ p∨p"
oops

lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops

lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops

lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops

lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops

lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops

lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
"p ⟹ ¬¬p"
oops

lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops

lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops

lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops

lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops

lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops

lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops

lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops

lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops

lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
"p∧¬p ⟹ q"
oops

lemma ejercicio_51:
"¬¬p ⟹ p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops

lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops

lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops

lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops

lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops

end
</source>

Relación 9

2011-03-22T17:02:55Z

Antonio:

<source lang="isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· 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
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof (rule impI)
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
by simp

lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
"p ⟹ q⟶p"
oops

lemma ejercicio_8:
"p⟶(q⟶p)"
oops

lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
oops

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops

lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
oops

lemma ejercicio_14:
"p∧q ⟹ p"
oops

lemma ejercicio_15:
"p∧q ⟹ q"
oops

lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
oops

lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
oops

lemma ejercicio_18:
"p∧q ⟹ p⟶q"
oops

lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
oops

lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
oops

lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
oops

lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
oops

lemma ejercicio_25:
"p ⟹ p∨q"
oops

lemma ejercicio_26:
"q ⟹ p∨q"
oops

lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops

lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops

lemma ejercicio_29:
"p∨p ⟹ p"
oops

lemma ejercicio_30:
"p ⟹ p∨p"
oops

lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops

lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops

lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops

lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops

lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops

lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
"p ⟹ ¬¬p"
oops

lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops

lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops

lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops

lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops

lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops

lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops

lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops

lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops

lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
"p∧¬p ⟹ q"
oops

lemma ejercicio_51:
"¬¬p ⟹ p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops

lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops

lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops

lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops

lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops

end
</source>

Relación 9

2011-03-15T19:29:39Z

Antonio:

<source lang="isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· 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
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof (rule impI)
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
oops

lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
"p ⟹ q⟶p"
oops

lemma ejercicio_8:
"p⟶(q⟶p)"
oops

lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
oops

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops

lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
oops

lemma ejercicio_14:
"p∧q ⟹ p"
oops

lemma ejercicio_15:
"p∧q ⟹ q"
oops

lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
oops

lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
oops

lemma ejercicio_18:
"p∧q ⟹ p⟶q"
oops

lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
oops

lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
oops

lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
oops

lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
oops

lemma ejercicio_25:
"p ⟹ p∨q"
oops

lemma ejercicio_26:
"q ⟹ p∨q"
oops

lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops

lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops

lemma ejercicio_29:
"p∨p ⟹ p"
oops

lemma ejercicio_30:
"p ⟹ p∨p"
oops

lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops

lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops

lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops

lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops

lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops

lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
"p ⟹ ¬¬p"
oops

lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops

lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops

lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops

lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops

lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops

lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops

lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops

lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops

lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
"p∧¬p ⟹ q"
oops

lemma ejercicio_51:
"¬¬p ⟹ p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops

lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops

lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops

lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops

lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops

end
</source>

Relación 9

2011-03-15T18:57:05Z

Antonio:

<source lang="isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· 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
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 have q: "q" by (rule mp)
from q show "q" by simp
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
proof -
from 1 and 3 have 4:"q" by (rule ejercicio_1)
from 2 and 4 have 5:"r" by (rule ejercicio_1)
from 5 show "r" by simp
qed

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
proof -
from 1 and 3 have qr:"q⟶r" by (rule ejercicio_1)
from 2 and qr and 3 have r:"r" by (rule ejercicio_2)
from r show "r" by simp
qed

text {*
creo que debe ser algo asi el 4 pero no termino de verlo claro
ya que consigo p y r pero para engancharlos no me va la regla de
inclusion de la implicacion tengo que mirarlo con detenimiento*}

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
proof -
assume p:"p"
from 1 and 2 and p have r:"r" by (rule ejercicio_2)
from p and r show "p⟶r" by (rule impI)
qed

lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
oops

lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
"p ⟹ q⟶p"
oops

lemma ejercicio_8:
"p⟶(q⟶p)"
oops

lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
oops

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops

lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
oops

lemma ejercicio_14:
"p∧q ⟹ p"
oops

lemma ejercicio_15:
"p∧q ⟹ q"
oops

lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
oops

lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
oops

lemma ejercicio_18:
"p∧q ⟹ p⟶q"
oops

lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
oops

lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
oops

lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
oops

lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
oops

lemma ejercicio_25:
"p ⟹ p∨q"
oops

lemma ejercicio_26:
"q ⟹ p∨q"
oops

lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops

lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops

lemma ejercicio_29:
"p∨p ⟹ p"
oops

lemma ejercicio_30:
"p ⟹ p∨p"
oops

lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops

lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops

lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops

lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops

lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops

lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
"p ⟹ ¬¬p"
oops

lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops

lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops

lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops

lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops

lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops

lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops

lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops

lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops

lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
"p∧¬p ⟹ q"
oops

lemma ejercicio_51:
"¬¬p ⟹ p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops

lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops

lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops

lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops

lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops

end
</source>

Relación 9

2011-03-15T16:41:33Z

Antonio:

<source lang="isar">
theory Relacion_9
imports Main
begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· 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
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
from 1 and 2 show "q" by (rule mp)
qed

lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
oops

lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
oops

lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
oops

lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
oops

lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
"p ⟹ q⟶p"
oops

lemma ejercicio_8:
"p⟶(q⟶p)"
oops

lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
oops

lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops

lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
oops

lemma ejercicio_14:
"p∧q ⟹ p"
oops

lemma ejercicio_15:
"p∧q ⟹ q"
oops

lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
oops

lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
oops

lemma ejercicio_18:
"p∧q ⟹ p⟶q"
oops

lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
oops

lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
oops

lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
oops

lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
oops

lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
oops

lemma ejercicio_25:
"p ⟹ p∨q"
oops

lemma ejercicio_26:
"q ⟹ p∨q"
oops

lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops

lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops

lemma ejercicio_29:
"p∨p ⟹ p"
oops

lemma ejercicio_30:
"p ⟹ p∨p"
oops

lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops

lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops

lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops

lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops

lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops

lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
"p ⟹ ¬¬p"
oops

lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops

lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops

lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops

lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops

lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops

lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops

lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops

lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops

lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops

lemma ejercicio_49:
"¬(p∧¬p)"
oops

lemma ejercicio_50:
"p∧¬p ⟹ q"
oops

lemma ejercicio_51:
"¬¬p ⟹ p"
oops

lemma ejercicio_52:
"p∨¬p"
oops

lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops

lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops

lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops

lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops

lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops

lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops

end
</source>