Relación 9

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_1b:
  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:
  assumes 1: "p⟶(q⟶r)"
  shows "q⟶(p⟶r)"
oops

lemma ejercicio_6:
  assumes 1: "p⟶(q⟶r)" 
  shows "(p⟶q)⟶(p⟶r)"
oops

lemma ejercicio_7:
  assumes 1: "p" 
  shows "q⟶p"
oops

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

lemma ejercicio_9:
  assumes 1: "p⟶q"  
  shows "(q⟶r)⟶(p⟶r)"
oops

lemma ejercicio_10:
  assumes 1: "p⟶(q⟶(r⟶s))"
  shows "r⟶(q⟶(p⟶s))"
oops

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

lemma ejercicio_12:
  assumes 1: "(p⟶q)⟶r" 
  shows "p⟶(q⟶r)"
oops

lemma ejercicio_13:
  assumes 1: "p" and  
          2: "q" 
  shows "p∧q"
oops

lemma ejercicio_14:
  assumes 1: "p∧q" 
  shows "p"
oops

lemma ejercicio_15:
  assumes 1: "p∧q" 
  shows "q"
oops

lemma ejercicio_16:
  assumes 1: "p∧(q∧r)"
  shows "(p∧q)∧r"
oops

lemma ejercicio_17:
  assumes 1: "(p∧q)∧r"
  shows "p∧(q∧r)"
oops

lemma ejercicio_18:
  assumes 1: "p∧q"
  shows "p⟶q"
oops

lemma ejercicio_19:
  assumes 1: "(p⟶q)∧(p⟶r)" 
  shows "p⟶q∧r"
oops

lemma ejercicio_20:
  assumes 1: "p⟶q∧r" 
  shows "(p⟶q)∧(p⟶r)"
oops

lemma ejercicio_21:
  assumes 1: "p⟶(q⟶r)" 
  shows "p∧q⟶r"
oops

lemma ejercicio_22:
  assumes 1: "p∧q⟶r"  
  shows "p⟶(q⟶r)"
oops

lemma ejercicio_23:
  assumes 1: "(p⟶q)⟶r" 
  shows "p∧q⟶r"
oops

lemma ejercicio_24:
  assumes 1: "p∧(q⟶r)"  
  shows "(p⟶q)⟶r"
oops

lemma ejercicio_25:
  assumes 1: "p" 
  shows "p∨q"
oops

lemma ejercicio_26:
  assumes 1: "q"  
  shows "p∨q"
oops

lemma ejercicio_27:
  assumes 1: "p∨q" 
  shows "q∨p"
oops

lemma ejercicio_28:
  assumes 1: "q⟶r" 
  shows "p∨q⟶p∨r"
oops

lemma ejercicio_29:
  assumes 1: "p∨p" 
  shows "p"
oops

lemma ejercicio_30:
  assumes 1: "p" 
  shows "p∨p"
oops

lemma ejercicio_31:
  assumes 1: "p∨(q∨r)"
  shows "(p∨q)∨r"
oops

lemma ejercicio_32:
  assumes 1: "(p∨q)∨r"
  shows "p∨(q∨r)"
oops

lemma ejercicio_33:
  assumes 1: "p∧(q∨r)" 
  shows "(p∧q)∨(p∧r)"
oops

lemma ejercicio_34:
  assumes 1: "(p∧q)∨(p∧r)" 
  shows "p∧(q∨r)"
oops

lemma ejercicio_35:
  assumes 1: "p∨(q∧r)"
  shows "(p∨q)∧(p∨r)"
oops

lemma ejercicio_36:
  assumes 1: "(p∨q)∧(p∨r)"
  shows "p∨(q∧r)"
oops

lemma ejercicio_37:
  assumes 1: "(p⟶r)∧(q⟶r)" 
  shows "p∨q⟶r"
oops

lemma ejercicio_38:
  assumes 1: "p∨q⟶r"  
  shows "(p⟶r)∧(q⟶r)"
oops

lemma ejercicio_39:
  assumes 1: "p"
  shows "¬¬p"
oops

lemma ejercicio_40:
  assumes 1: "¬p"  
  shows "p⟶q"
oops

lemma ejercicio_41:
  assumes 1: "p⟶q"
  shows "¬q⟶¬p"
oops

lemma ejercicio_42:
  assumes 1: "p∨q" and
          2: "¬q" 
  shows "p"
oops

lemma ejercicio_43:
  assumes 1: "p∨q" and
          2: "¬p" 
  shows "q"
oops

lemma ejercicio_44:
  assumes 1: "p∨q"
  shows "¬(¬p∧¬q)"
oops

lemma ejercicio_45:
  assumes 1: "p∧q"
  shows "¬(¬p∨¬q)"
oops

lemma ejercicio_46:
  assumes 1: "¬(p∨q)"
  shows "¬p∧¬q"
oops

lemma ejercicio_47:
  assumes 1: "¬p∧¬q"  
  shows "¬(p∨q)"
oops

lemma ejercicio_48:
  assumes 1: "¬p∨¬q"
  shows "¬(p∧q)"
oops

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

lemma ejercicio_50:
  assumes 1: "p∧¬p"
  shows "q"
oops

lemma ejercicio_51:
  assumes 1: "¬¬p"
  shows "p"
oops

lemma ejercicio_52:
  "p∨¬p"
oops

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

lemma ejercicio_54:
  assumes 1: "¬q⟶¬p"
  shows "p⟶q"
oops

lemma ejercicio_55:
  assumes 1: "¬(¬p∧¬q)"
  shows "p∨q"
oops

lemma ejercicio_56:
  assumes 1: "¬(¬p∨¬q)"
  shows "p∧q"
oops

lemma ejercicio_57:
  assumes 1: "¬(p∧q)"
  shows "¬p∨¬q"
oops

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

end