Relación 7

header {* R7: Deducción natural en lógica de primer orden con Isabelle/HOL *}

theory R7
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 y mt que demostramos a continuación.
  *}

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

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

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       ∀x. P x ⟶ Q x ⊢ (∀x. P x) ⟶ (∀x. Q x)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_1: 
  assumes "∀x. P x ⟶ Q x"
  shows   "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
  assume 1:"∀x. P x"
  {fix a
  have 2:"P a ⟶ Q a" using assms..
  have "P a" using 1..
  with 2 have "Q a"..}
  thus "∀x. Q x"..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
       ∃x. ¬(P x) ⊢ ¬(∀x. P x)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_2: 
  assumes "∃x. ¬(P x)"
  shows   "¬(∀x. P x)"
proof
  assume 1:"(∀x. P x)"
  obtain a where 2:"¬(P a)" using assms..
  have "P a" using 1..
  with 2 show False..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
       ∀x. P x ⊢ ∀y. P y
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_3: 
  assumes "∀x. P x"
  shows   "∀y. P y"
using assms .

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
       ∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_4: 
  assumes "∀x. P x ⟶ Q x"
  shows   "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof
  assume 1:"(∀x. ¬(Q x))"
  {fix a
  have 2:"P a ⟶ Q a" using assms..
  have "¬(Q a)" using 1..
  with 2 have "¬(P a)" by (rule mt)}
  thus "∀x. ¬(P x)"..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
       ∀x. P x  ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_5: 
  assumes "∀x. P x  ⟶ ¬(Q x)"
  shows   "¬(∃x. P x ∧ Q x)"
proof
  assume "(∃x. P x ∧ Q x)"
  then obtain a where 1: "P a ∧ Q a"..
  hence 2:"P a"..
  have 3:"Q a" using 1..
  have "P a ⟶ ¬(Q a)" using assms..
  hence "¬(Q a)" using 2..
  thus False using 3..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
       ∀x y. P x y ⊢ ∀u v. P u v
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_6: 
  assumes "∀x y. P x y"
  shows   "∀u v. P u v"
using assms .

text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar
       ∃x y. P x y ⟹ ∃u v. P u v
  ------------------------------------------------------------------ *}

lemma ejercicio_7: 
  assumes "∃x y. P x y"
  shows   "∃u v. P u v"
using assms .

text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
       ∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_8: 
  assumes "∃x. ∀y. P x y"
  shows   "∀y. ∃x. P x y"
proof -
  obtain a where 1: "∀y. P a y" using assms..
  {fix b
   have "P a b" using 1..
   hence "∃x. P x b"..}
  thus ?thesis ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
       ∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_9: 
  assumes "∃x. P a ⟶ Q x"
  shows   "P a ⟶ (∃x. Q x)"
proof
  assume 1:"P a"
  obtain b where 2: "P a⟶ Q b" using 0..
  hence "Q b" using 1..
  thus "∃x. Q x"..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
       P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x 
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_10: 
  fixes P Q :: "'b ⇒ bool" 
  assumes "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
  have "¬(P a)∨ P a"..
  moreover
  {assume "¬(P a)"
    hence "P a ⟶ Q a" by (rule ejercicio_40f)
    hence ?thesis..}
  moreover
  {assume "P a"
  with assms have "∃x. Q x"..
  then obtain b where "Q b"..
  hence "P a ⟶ Q b"..
  hence ?thesis..}
  ultimately
  show ?thesis..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
       (∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_11: 
  assumes "(∃x. P x) ⟶ Q a"
  shows   "∀x. P x ⟶ Q a"
proof-
  have "¬(Q a)∨ (Q a)"..
  moreover
  {assume 2: "¬(Q a)"
    {fix b
    have 3:"¬(∃x. P x)"using 1 2 by (rule mt)
    have "¬(P b)"
    proof
      assume "P b"
      hence "∃x. P x"..
      with 3 show False..
    qed
    hence 3:"P b⟶ Q a" by (rule ejercicio_40f)}
    hence ?thesis..}
  moreover
   {assume 2: "Q a"
     {fix b
     have "P b ⟶ Q a"using 2..}
     hence ?thesis ..}
   ultimately
    show ?thesis..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
       ∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_12: 
  assumes "∀x. P x ⟶ Q a"
  shows   "∃x. P x ⟶ Q a"
proof-
  fix w
  have "P w ⟶ Q a"using assms..
  thus "∃x. P x ⟶ Q a"..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar
       (∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_13: 
  assumes "(∀x. P x) ∨ (∀x. Q x)"
  shows   "∀x. P x ∨ Q x"
proof-
  note `(∀x. P x) ∨ (∀x. Q x)`
  moreover
  {assume 1:"∀x. P x"
    {fix a
    have "P a"using 1..
    hence "P a ∨ Q a"..}
    hence ?thesis..}
  moreover
   {assume 1:"∀x. Q x"
    {fix a
    have "Q a"using 1..
    hence "P a ∨ Q a"..}
    hence ?thesis..}
   ultimately
   show ?thesis..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
       ∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_14: 
  assumes "∃x. P x ∧ Q x"
  shows   "(∃x. P x) ∧ (∃x. Q x)"
proof-
  obtain a where 1: "P a ∧ Q a" using assms..
  hence "P a"..
  hence 2:"∃x. P x"..
  have "Q a" using 1..
  hence "∃x. Q x"..
  with 2 show ?thesis..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar
       ∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_15: 
  assumes "∀x y. P y ⟶ Q x"
  shows   "(∃y. P y) ⟶ (∀x. Q x)"
proof
  assume "(∃y. P y)"
  then obtain a where 1: "P a"..
  {fix b
  have "∀x. P x ⟶ Q b" using 0..
  hence "P a ⟶ Q b"..
  hence "Q b" using 1..}
  thus "∀x. Q x"..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar
       ¬(∀x. ¬(P x)) ⊢ ∃x. P x
  ------------------------------------------------------------------ *}

lemma ejercicio_16: 
  assumes "¬(∀x. ¬(P x))"
  shows   "∃x. P x"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 17. Demostrar
       ∀x. ¬(P x) ⊢ ¬(∃x. P x)
  ------------------------------------------------------------------ *}

lemma ejercicio_17: 
  assumes "∀x. ¬(P x)"
  shows   "¬(∃x. P x)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 18. Demostrar
       ∃x. P x ⊢ ¬(∀x. ¬(P x))
  ------------------------------------------------------------------ *}

lemma ejercicio_18: 
  assumes "∃x. P x"
  shows   "¬(∀x. ¬(P x))"
oops

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

lemma ejercicio_19: 
  assumes "P a ⟶ (∀x. Q x)"
  shows   "∀x. P a ⟶ Q x"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 20. 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)
  ------------------------------------------------------------------ *}

lemma ejercicio_20: 
  assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
          "∀x. ¬(R x x)" 
  shows   "∀x y. R x y ⟶ ¬(R y x)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 21. Demostrar
     {∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_21:
  assumes "∀x. P x ∨ Q x" 
          "∃x. ¬(Q x)" 
          "∀x. R x ⟶ ¬(P x)"
  shows   "∃x. ¬(R x)" 
proof -
  obtain a where 1: "¬ (Q a)" using assms(2)..
  have "P a∨ Q a" using assms(1) ..
  hence "P a" using 1 by (rule ejercicio_42)
  hence 2:"¬¬P a" by (rule notnotI)
  have "R a ⟶ ¬(P a)" using assms(3)..
  hence "¬(R a)" using 2 by (rule mt)
  thus ?thesis ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 22. Demostrar
     {∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_22:
  assumes "∀x. P x ⟶ Q x ∨ R x" 
          "¬(∃x. P x ∧ R x)"
  shows   "∀x. P x ⟶ Q x"
proof
  fix a
  have 1:"P a ⟶ Q a ∨ R a" using assms(1)..
  show "P a ⟶ Q a"
  proof -
    have "¬(P a) ∨ P a"..
    moreover
    {assume "¬(P a)"
      hence "(P a) ⟶ Q a" by (rule ejercicio_40f)}
    moreover
    {assume "P a"
      with 1 have 2:"Q a ∨ R a"..
      have "Q a"
      proof (rule ccontr)
        assume "¬(Q a)"
        with 2 have "R a" by (rule ejercicio_43)
        with `P a` have "P a ∧ R a"..
        hence "∃x. P x ∧ R x"..
        with assms(2) show False..
        qed
        hence "P a ⟶ Q a"..}
    ultimately show "P a ⟶ Q a"..
    qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     ∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_23:
  assumes "∃x y. R x y ∨ R y x"
  shows   "∃x y. R x y"
proof-
  obtain a where 1: "∃y. R a y ∨ R y a" using assms..
  then obtain b where "R a b ∨ R b a"..
  moreover
  {assume "R a b"
    hence "∃x. R a x"..
    hence ?thesis..}
  moreover
  {assume "R b a"
    hence "∃x. R b x"..
    hence ?thesis..}
  ultimately show ?thesis ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 24. Demostrar
       (∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_24: 
  "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof
  assume "(∃x. ∀y. P x y)"
  then obtain a where 1:"∀y. P a y"..
  {fix b
    have "P a b" using 1..
    hence "∃x. P x b"..}
  thus "∀y. ∃x. P x y"..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
       (∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
  ------------------------------------------------------------------ *}

lemma ejercicio_25: 
  "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
       ((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_26: 
  "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof
  assume 1:"((∀x. P x) ∧ (∀x. Q x))"
  hence 2:"∀x. P x"..
  have 3:"∀x. Q x" using 1..
  {fix a
    have 4:"P a" using 2..
    have "Q a" using 3..
    with 4 have "P a ∧ Q a"..}
  thus "∀x. P x ∧ Q x"..
next
  assume 1: "(∀x. P x ∧ Q x)"
  {fix a
  have "P a ∧ Q a" using 1..
  hence "P a"..}
  hence 2: "∀x. P x"..
  {fix a
  have "P a ∧ Q a" using 1..
  hence "Q a"..}
  hence 3: "∀x. Q x"..
  with 2 show "(∀x. P x)∧(∀x. Q x)"..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 27. Demostrar o refutar
       ((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_27: 
  "((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar o refutar
       ((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_28: 
  "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
oops

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

lemma ejercicio_29: 
  "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar o refutar
       (¬(∀x. P x)) ⟷ (∃x. ¬P x)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_30: 
  "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof
  assume 1:"(¬(∀x. P x))"
  show 2:"(∃x. ¬P x)"
  proof (rule ccontr)
    assume 3:"¬(∃x. ¬P x)"
    {fix a
    have 4: "P a"
    proof (rule ccontr)
      assume "¬(P a)"
      hence "∃x. ¬(P x)"..
      with 3 show False..
    qed}
    hence "∀x. P x"..
    with 1 show False..
  qed
next
  assume 1: "(∃x. ¬P x)"
  then obtain a where 2: "¬ (P a)"..
  show 3:"¬(∀x. P x)"
  proof
    assume "∀x. P x"
    hence "P a"..
    with 2 show False..
  qed
qed

section {* Ejercicios sobre igualdad *}

text {* --------------------------------------------------------------- 
  Ejercicio 31. Demostrar o refutar
       P a ⟹ ∀x. x = a ⟶ P x
  ------------------------------------------------------------------ *}

lemma ejercicio_31b:
  assumes "P a"
  shows   "∀x. x = a ⟶ P x"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 32. Demostrar o refutar
       ∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
  ------------------------------------------------------------------ *}

lemma ejercicio_32:
  fixes R :: "'c ⇒ 'c ⇒ bool"
  assumes "∃x y. R x y ∨ R y x"
          "¬(∃x. R x x)"
  shows   "∃(x::'c) y. x ≠ y"
oops

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

lemma ejercicio_33:
  assumes "∀x. P a x x"
          "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows   "P (f a) a (f a)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 34. 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))
  ------------------------------------------------------------------ *}

lemma ejercicio_34b:
  assumes "∀x. P a x x" 
          "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows   "∃z. P (f a) z (f (f a))"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 35. 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))
  ------------------------------------------------------------------ *}

lemma ejercicio_35:
  assumes "∀y. Q a y" 
          "∀x y. Q x y ⟶ Q (s x) (s y)" 
  shows   "∃z. Q a z ∧ Q z (s (s a))"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 36. Demostrar o refutar
     {x = f x, odd (f x)} ⊢ odd x
  ------------------------------------------------------------------ *}

lemma ejercicio_36b:
  "⟦x = f x; odd (f x)⟧ ⟹ odd x"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 37. Demostrar o refutar
     {x = f x, triple (f x) (f x) x} ⊢ triple x x x
  ------------------------------------------------------------------ *}

lemma ejercicio_37b:
  "⟦x = f x; triple (f x) (f x) x⟧ ⟹ triple x x x"
oops

end