Tema 3 ej

header {* Deducción natural proposicional *}

theory Tema_3_ej
imports Main 
begin 

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"
oops

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
De Demostración asistida por ordenador (2011-12)
