Relación 9

header {* R9: Deducción natural en Isabelle/HOL *}

theory R9
imports Main 
begin

text {*
  Demostrar o refutar los siguientes lemas usando sólo las reglas
  básicas de deducción natural de la lógica proposicional, de los
  cuantificadores y de la igualdad: 
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · 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

  · allI:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  · allE:       (⋀x. P x) ⟹ ∀x. P x
  · exI:        P x ⟹ ∃x. P x
  · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

  · refl:       t = t
  · subst:      ⟦s = t; P s⟧ ⟹ P t
  · trans:      ⟦r = s; s = t⟧ ⟹ r = t
  · sym:        s = t ⟹ t = s
  · not_sym:    t ≠ s ⟹ s ≠ t
  · ssubst:     ⟦t = s; P s⟧ ⟹ P t
  · box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
  · arg_cong:   x = y ⟹ f x = f y
  · fun_cong:   f = g ⟹ f x = g x
  · cong:       ⟦f = g; x = y⟧ ⟹ f x = g y
*}

text {*
  Se usarán las reglas notnotI, mt y not_ex que demostramos a continuación.
  *}

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

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

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
     p ∨ q, ¬q ⊢ p
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_1:
  assumes 1:"p ∨ q" and 2:"¬q"
  shows "p"
using 1
proof
  assume 3: "p"
  then show "p" .
next
  assume 4:"q"
  show "p" using 2 4 by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_2:
  assumes 1:"p ∧ q"
  shows "¬(¬p ∨ ¬ q)"
proof
  assume 2:"¬p ∨ ¬q"
  show "False"
  using 2
  proof
    assume 3:"¬p"
    have 4:"p" using 1 by (rule conjunct1)
    show "False" using 3 4 by (rule notE)
  next
    assume 5:"¬q"
    have 6:"q" using 1 by (rule conjunct2)
    show "False" using 5 6 by (rule notE)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
     ¬(p ∨ q) ⊢ ¬p ∧ ¬q
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_3:
  assumes 1:"¬(p ∨ q)"
  shows "¬p ∧ ¬q"
proof
  {assume 2:"p"
  have 3:"p ∨ q" using 2 by (rule disjI1)
  also have 4:"False" using 1 3 by (rule notE)}
  then show "¬p" ..
next
  {assume 5:"q"
  have 6:"p ∨ q" using 5 by (rule disjI2)
  also have 7:"False" using 1 6 by (rule notE)}
  then show "¬q" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_4:
  assumes 1:"¬p ∧ ¬q"
  shows "¬(p ∨ q)"
proof
  assume 2:"p ∨ q"
  show "False"
  using 2
  proof
    assume 3:"p"
    have 4:"¬p" using 1 by (rule conjunct1)
    then show "False" using 3 ..
  next
    assume 5:"q"
    have 6:"¬q" using 1 by (rule conjunct2)
    then show "False" using 5 ..
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_5:
  assumes 1:"¬p ∨ ¬q"
  shows "¬(p ∧ q)"
proof
  assume 2:"p ∧ q"
  have 3:"p" using 2 by (rule conjunct1)
  have 4:"q" using 2 by (rule conjunct2)
  show "False"
  using 1
  proof
    assume 5:"¬p"
    then show "False" using 3 ..
  next
    assume 6:"¬q"
    then show "False" using 4 ..
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_6:
  shows "((p ⟶ q) ⟶ p ) ⟶ p"
proof
  assume 1:"(p ⟶ q) ⟶ p"
  show "p"
  proof (rule ccontr)
    assume 2:"¬p"
    have 3:"¬(p ⟶ q)" using 1 2 by (rule mt)
    {assume 4:"p"
    have "False" using 2 4 ..
    then have "q" ..}
    then have 5:"p ⟶ q" ..
    show "False" using 3 5 ..
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_7:
  assumes 1:"¬q ⟶ ¬p"
  shows "p ⟶ q"
proof -
  {assume 2:"p"
  then have 3:"¬¬p" by (rule notnotI)
  have 4:"¬¬q" using 1 3 by (rule mt)
  then have 5:"q" by (rule notnotD)}
  then show "p ⟶ q" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_8:
  assumes 1:"¬(¬p ∧ ¬q)"
  shows "p ∨ q"
proof -
  {assume 2:"¬(p ∨ q)"
  have 3:"¬p ∧ ¬q" using 2 by (rule ej_3)
  also have "False" using 1 3 ..}
  then show "p ∨ q" by (rule ccontr)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_9:
  assumes 1:"¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof
  have 2:"¬¬p ∧ ¬¬q" using 1 by (rule ej_3)
  have 3:"¬¬p" using 2 by (rule conjunct1)
  have 4:"¬¬q" using 2 by (rule conjunct2)
  show "p" using 3 by (rule notnotD)
  show "q" using 4 by (rule notnotD)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_10:
  assumes 1:"¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof -
  {assume 2:"¬(¬p ∨ ¬q)"
  have 3:"p ∧ q" using 2 by (rule ej_9)
  have "False" using 1 3 ..}
  then show "¬p ∨ ¬q" by (rule ccontr)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_11:
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have 1:"¬(p ⟶ q) ∨ (p ⟶ q)" ..
  show "(p ⟶ q) ∨ (q ⟶ p)"
  using 1
  proof
    assume 2:"p ⟶ q"
    then show "(p ⟶ q) ∨ (q ⟶ p)" ..
  next
    {assume 3:"¬(p ⟶ q)"
    {assume 4:"q"
    {assume 5:"p"
    have 6:"q" using 4 .}
    then have 7:"p ⟶ q" ..
    with 3 have "False" ..
    then have "p" ..}
    then have "q ⟶ p" ..
    then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
       P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x 
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar
       {∀x y z. R x y ∧ R y z ⟶ R x z, 
        ∀x. ¬(R x x)}
       ⊢ ∀x y. R x y ⟶ ¬(R y x)
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar o refutar
       (∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_14:
  assumes 1:"∀x. ∃y. P x y"
  shows "∃y. ∀x. P x y"
quickcheck
oops

text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar o refutar
       (∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_15:
  assumes 1:"∃y. ∀x. P x y"
  shows "∀x. ∃y. P x y"
proof -
  {fix a
  obtain b where 2:"∀x. P x b" using 1 ..
  have "P a b" using 2 ..
  then have "∃y. P a y" ..}
  then show "∀x. ∃y. P x y" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar o refutar
     {∀x. P a x x, 
      ∀x y z. P x y z ⟶ P (f x) y (f z)⟧
     ⊢ ∃z. P (f a) z (f (f a))
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_16:
  assumes 1:"∀x. P a x x" and 2:"∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof -
  have 4:"P a (f a) (f a)" using 1 ..
  also have 5:"∀y z. P a y z ⟶ P (f a) y (f z)" using 2 ..
  then have 6:"∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
  then have 7:"P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
  also have 8:"P (f a) (f a) (f (f a))" using 7 4 by (rule mp)
  then show "∃z. P (f a) z (f (f a))" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 17. Demostrar o refutar
     {∀y. Q a y, 
      ∀x y. Q x y ⟶ Q (s x) (s y)} 
     ⊢ ∃z. Qa z ∧ Q z (s (s a))
  ------------------------------------------------------------------ *}

--"davoremar"
lemma ej_17:
  assumes 1:"∀y. Q a y" and 2:"∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
proof
  have 3:"Q a (s a)" using 1 ..
  also have 4:"∀y. Q a y ⟶ Q (s a) (s y)" using 2 ..
  then have 5:"Q a (s a) ⟶ Q (s a) (s (s a))" ..
  then have 6:"Q (s a) (s (s a))" using 3 by (rule mp)
  show "Q a (s a) ∧ Q (s a) (s (s a))" using 3 6 by (rule conjI)
qed

end