Relación 7

chapter {* R7: Deducción natural en lógica de primer orden *}

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
  · excluded_middel:(¬P ∨ 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)
  ------------------------------------------------------------------ *}

lemma ejercicio_1a: carmarria
  assumes 1: "∀x. P x ⟶ Q x"
  shows   "(∀x. P x) ⟶ (∀x. Q x)"
proof -
  {assume 2: "! x. P x"
    {fix a
    have 3: "P a ⟶ Q a" using 1 by (rule allE)
    have 4: "P a" using 2 by (rule allE)
    have 5: "Q a" using 3 4 by (rule mp)
  }
  hence 6: "! x. Q x" by (rule allI)
}
  thus "(! x. P x) ⟶ (! x. Q x)" by (rule impI)
qed

joslopjim4

  assumes "∀x. P x ⟶ Q x"
  shows   "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
  assume "∀x. P x"
  show "∀x. Q x"
  proof (rule allI)
    fix a
    have "P a ⟶ Q a" using assms by (rule allE)
    have "P a" using `∀x. P x` by (rule allE)
    show "Q a" using  `P a ⟶ Q a` `P a`  by (rule mp)
  qed
qed

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

lemma ejercicio_2a: carmarria
  assumes 1: "∃x. ¬(P x)"
  shows   "¬(∀x. P x)"
proof -
  obtain a where 2: "¬(P a)" using 1 by (rule exE)
  {assume 3: "! x. P x"
    have 4: "P a" using 3 by (rule allE)
    have 5: False using 2 4 by (rule notE)
  }
  thus "¬(! x. P x)" by (rule notI)
qed

joslopjim4

  assumes "∃x. ¬(P x)"
  shows   "¬(∀x. P x)"
proof (rule ccontr)
  assume "¬¬(∀x. P x)"
  then have "∀x. P x" by (rule notnotD)
  obtain a where "¬(P a)" using assms by (rule exE)
  have "P a" using `∀x. P x` by (rule allE)
  show False using `¬(P a)` `P a` by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
       ∀x. P x ⊢ ∀y. P y
  ------------------------------------------------------------------ *}

lemma ejercicio_3a: carmarria
  assumes 1: "∀x. P x"
  shows   "∀y. P y"
proof -
  {fix a
    have 2: "P a" using 1 by (rule allE)
  }
  thus "! y. P y" by (rule allI)
qed

joslopjim4

  assumes "∀x. P x"
  shows   "∀y. P y"
proof (rule allI)
  fix a
  show "P a" using assms by (rule allE)
qed

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

lemma ejercicio_4: carmarria
  assumes 1: "∀x. P x ⟶ Q x"
  shows   "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof -
  {assume 2: "!x. ¬(Q x)"
      {fix a
    have 3: "¬(Q a)" using 2 by (rule allE)
    have 4: "P a ⟶ Q a" using 1 by (rule allE)
    have 5: "¬(P a)" using 4 3 by (rule mt)
  }
  hence 6: "!x. ¬ (P x)" by (rule allI)
}
  thus "(!x. ¬(Q x)) ⟶ (!x. ¬ (P x))" by (rule impI)
qed

joslopjim4

  assumes "∀x. P x ⟶ Q x"
  shows   "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof (rule impI)
  assume "∀x. ¬(Q x)"
  show "∀x. ¬ (P x)"
  proof (rule allI)
    fix a
    have "¬(Q a)" using `∀x. ¬(Q x)` by (rule allE)
    have "P a ⟶ Q a" using assms by (rule allE)
    thus "¬(P a)" using `¬(Q a)` by (rule mt)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
       ∀x. P x  ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_5: carmarria
  assumes 1: "∀x. P x  ⟶ ¬(Q x)"
  shows   "¬(∃x. P x ∧ Q x)"
proof -
  {assume 2: "? x. P x & Q x"
    obtain a where 3: "P a & Q a" using 2 by (rule exE)
    have 4: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
    have 5: "P a" using 3 by (rule conjunct1)
    have 6: "Q a" using 3 by (rule conjunct2)
    have 7: "¬(Q a)" using 4 5 by (rule mp)
    have 8: False using 7 6 by (rule notE)
  }
  thus "¬(? x. P x & Q x)" by (rule notI)
qed

joslopjim4

  assumes "∀x. P x  ⟶ ¬(Q x)"
  shows   "¬(∃x. P x ∧ Q x)"
proof (rule ccontr)
  assume "¬¬(∃x. P x ∧ Q x)"
  then have "∃x. P x ∧ Q x" by (rule notnotD)
  obtain b where "P b ∧ Q b" using `∃x. P x ∧ Q x` by (rule exE)
  have "P b" using `P b ∧ Q b` by (rule conjunct1)
  have "Q b" using `P b ∧ Q b` by (rule conjunct2)
  have "P b ⟶ ¬(Q b)"
  proof -
    fix b
    show "P b ⟶ ¬(Q b)" using assms by (rule allE)
  qed
  have "¬(Q b)" using `P b ⟶ ¬(Q b)` `P b` by (rule mp)
  show False using `¬(Q b)` `Q b` by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
       ∀x y. P x y ⊢ ∀u v. P u v
  ------------------------------------------------------------------ *}

lemma ejercicio_6: carmarria
  assumes 1: "∀x y. P x y"
  shows   "∀u v. P u v"
proof -
  {fix a
    have 2: "! y. P a y" using 1 by (rule allE)
    {fix b
      have 3: "P a b" using 2 by (rule allE)
    }
    hence 4: "!v. P a v" by (rule allI)
  }
  thus "!u v. P u v" by (rule allI)
qed

joslopjim4

  assumes "∀x y. P x y"
  shows   "∀u v. P u v"
proof (rule allI)
  fix a
  have "∀y. P a y" using assms by (rule allE)
  show "∀v. P a v"
  proof (rule allI)
  fix b
  show "P a b" using `∀y. P a y` by (rule allE)
qed
qed

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

lemma ejercicio_7: carmarria
  assumes 1: "∃x y. P x y"
  shows   "∃u v. P u v"
proof -
  obtain a where 2: "? y. P a y" using 1 by (rule exE)
  obtain b where 3: "P a b" using 2 by (rule exE)
  have 4: "? v. P a v" using 3 by (rule exI)
  show 5: "? u v. P u v" using 4 by (rule exI)
qed

joslopjim4

  assumes "∃x y. P x y"
  shows   "∃u v. P u v"
proof-
  obtain a where "∃y. P a y" using assms by (rule exE)
  obtain b where "P a b" using `∃y. P a y` by (rule exE)
  then have "∃v. P a v" by (rule exI)
  thus "∃u v. P u v" by (rule exI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
       ∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
  ------------------------------------------------------------------ *}

lemma ejercicio_8: carmarria
  assumes 1: "∃x. ∀y. P x y"
  shows   "∀y. ∃x. P x y"
proof -
  obtain a where 2: "! y. P a y" using 1 by (rule exE)
  {fix b
    have 3: "P a b" using 2 by (rule allE)
    have 4: "? x. P x b" using 3 by (rule exI)
  }
  thus "! y. ? x. P x y" by (rule allI)
qed

joslopjim4 

  assumes "∃x. ∀y. P x y"
  shows   "∀y. ∃x. P x y"
proof (rule allI)
  fix b
  obtain a where "∀y. P a y" using assms by (rule exE)
  then have "P a b" by (rule allE)
  then show "∃x. P x b" by (rule exI)
qed

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

lemma ejercicio_9: carmarria
  assumes 1: "∃x. P a ⟶ Q x"
  shows   "P a ⟶ (∃x. Q x)"
proof -
  {assume 2: "P a"
    obtain b where 3: "P a ⟶ Q b" using 1 by (rule exE)
    have 4: "Q b" using 3 2 by (rule mp)
    have 5: "? x. Q x" using 4 by (rule exI)
  }
  thus "P a ⟶ (? x. Q x)" by (rule impI)
qed

joslopjim4

  assumes "∃x. P a ⟶ Q x"
  shows   "P a ⟶ (∃x. Q x)"
proof (rule impI)
  assume "P a"
  obtain b where "P a ⟶ Q b" using assms by (rule exE)
  then have "Q b" using `P a` by (rule mp)
  thus "∃x. Q x" by (rule exI)
qed

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

lemma ejercicio_10a: carmarria
  fixes P Q :: "'b ⇒ bool" 
  assumes 1: "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
  have 2: "¬(P a) ∨ (P a)" by (rule excluded_middle)
  moreover {assume 3: "¬(P a)" 
    {assume 4: "P a"
      have 5: False using 3 4 by (rule notE)
      have 6: "Q b" using 5 by (rule FalseE)
    }
    hence 7: "P a ⟶Q b" by (rule impI)
    have 8: "? x. P a ⟶ Q x" using 7 by (rule exI)
  }
  moreover {assume 9: "P a"
    have 10: "? x. Q x" using 1 9 by (rule mp)
    obtain b where 11: "Q b" using 10 by (rule exE)
    {assume 12: "P a"
      have 13: "Q b" using 11 by this
    }
    hence 13: "P a ⟶ Q b" by (rule impI)
    have 14: "? x. P a ⟶ Q x" using 13 by (rule exI)
  }
  ultimately show "? x. P a ⟶ Q x" by (rule disjE)
qed 

joslopjim4

  fixes P Q :: "'b ⇒ bool" 
  assumes "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof-
  have "¬(P a) ∨ P a" by (rule excluded_middle)
  thus "∃x. P a ⟶ Q x"
  proof 
    assume "P a"
    have "∃x. Q x" using assms `P a` by (rule mp)
    obtain b where "Q b" using `∃x. Q x` by (rule exE)
    have "P a ⟶ Q b" 
    proof
      assume "P a"
      show "Q b" using `Q b` by this
    qed
    show "∃x. P a ⟶ Q x" using `P a ⟶ Q b` by (rule exI)
  next
    assume "¬(P a)"
    have "P a ⟶ Q a"
    proof
      assume "P a"
      have False using `¬(P a)` `P a` by (rule notE)
      thus "Q a" by (rule FalseE)
    qed
    show "∃x. P a ⟶ Q x" using `P a ⟶ Q a` by (rule exI)
  qed
qed

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

lemma ejercicio_11a: carmarria
  assumes 1:"(∃x. P x) ⟶ Q a"
  shows   "∀x. P x ⟶ Q a"
  proof-
  {fix b
    {assume 2: "P b"
      have 3: "? x. P x" using 2 by (rule exI)
      have 4: "Q a" using 1 3 by (rule mp)
    }
    hence 5: "P b ⟶ Q a" by (rule impI)
  }
  thus "! x. P x ⟶ Q a" by (rule allI)
qed


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

lemma ejercicio_12a: carmarria
  assumes 1: "∀x. P x ⟶ Q a"
  shows   "∃x. P x ⟶ Q a"
proof -
  have 2: "P b ⟶ Q a" using 1 by (rule allE)
  show 3: "? x. P x ⟶ Q a" using 2 by (rule exI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar
       (∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
  ------------------------------------------------------------------ *}

lemma ejercicio_13a: carmarria
  assumes 1: "(∀x. P x) ∨ (∀x. Q x)"
  shows   "∀x. P x ∨ Q x"
proof -
  {fix a
    have 2: "(! x. P x) ∨ (! x. Q x)" using 1 by this
    moreover {assume 3:"! x. P x"
      have 4: "P a" using 3 by (rule allE)
      have 5: "P a | Q a" using 4 by (rule disjI1)
    }
    moreover {assume 6: "! x. Q x" 
      have 7: "Q a" using 6 by (rule allE)
      have 8: "P a | Q a" using 7 by (rule disjI2)
    }
    ultimately have 9: "P a | Q a" by (rule disjE)
  }
  thus "! x. P x | Q x" by (rule allI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
       ∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_14a: carmarria
  assumes 1: "∃x. P x ∧ Q x"
  shows   "(∃x. P x) ∧ (∃x. Q x)"
proof -
  obtain a where 2: "P a & Q a" using 1 by (rule exE)
  have 3: "P a" using 2 by (rule conjunct1)
  have 4: "Q a" using 2 by (rule conjunct2)
  have 5: "? x. P x" using 3 by (rule exI)
  have 6: "? x. Q x" using 4 by (rule exI)
  show "(? x. P x) ∧ (? x. Q x)" using 5 6 by (rule conjI)
qed

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

lemma ejercicio_15a: carmarria
  assumes 1: "∀x y. P y ⟶ Q x"
  shows   "(∃y. P y) ⟶ (∀x. Q x)"
proof -
  {assume 2: "? y. P y"
    {fix a
      have 3: "! y. P y ⟶ Q a" using 1 by (rule allE)
      obtain b where 4: "P b" using 2 by (rule exE)
      have 5: "P b ⟶ Q a" using 3 by (rule allE)
      have 6: "Q a" using 5 4 by (rule mp)
    }
    hence 7: "! x. Q x" by (rule allI)
  }
  thus "(? y. P y) ⟶ (! x. Q x)" by (rule impI)
qed

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

lemma ejercicio_16a: carmarria
  assumes 1: "¬(∀x. ¬(P x))"
  shows   "∃x. P x"
proof -
    {assume 2: "¬(? x. P x)"
      {fix b
        {assume 3: "P b"
          have 4: "? x. P x" using 3 by (rule exI)
          have 5: False using 2 4 by (rule notE)
        }
        hence 6: "¬(P b)" by (rule notI)
      }
      hence 7: "! x. ¬(P x)" by (rule allI)
      have 8: False using 1 7 by (rule notE)
    }
    hence 9: "¬¬(? x. P x)" by (rule notI)
    show "? x. P x" using 9 by (rule notnotD)
  qed

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

lemma ejercicio_17a: carmarria
  assumes 1: "∀x. ¬(P x)"
  shows   "¬(∃x. P x)"
proof -
  {assume 2: "? x. P x"
    obtain a where 3: "P a" using 2 by (rule exE)
    have 4: "¬(P a)" using 1 by (rule allE)
    have 5: False using 4 3 by (rule notE)
  }
  thus "¬(? x. P x)" by (rule notI)
qed

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

lemma ejercicio_18a: carmarria
  assumes 1: "∃x. P x"
  shows   "¬(∀x. ¬(P x))"
proof-
  {assume 2: "! x. ¬(P x)"
    obtain a where 3: "P a" using 1 by (rule exE)
    have 4: "¬(P a)" using 2 by (rule allE)
    have 5: False using 4 3 by (rule notE)
  }
  thus "¬(! x. ¬(P x))" by (rule notI)
qed

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

lemma ejercicio_19a: carmarria
  assumes 1: "P a ⟶ (∀x. Q x)"
  shows   "∀x. P a ⟶ Q x"
proof -
  {fix b
    {assume 2: "P a"
      have 3: "! x. Q x" using 1 2 by (rule mp)
      have 4: "Q b" using 3 by (rule allE)
    }
    hence 5: "P a ⟶ Q b" by (rule impI)
  }
  thus "! x. P a ⟶ Q x" by (rule allI)
qed

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_20a: carmarria
  assumes 1: "∀x y z. R x y ∧ R y z ⟶ R x z" and
          2: "∀x. ¬(R x x)" 
  shows   "∀x y. R x y ⟶ ¬(R y x)"
proof -
  {fix a
    {fix b
      {assume 3: "R a b"
        have 4: "! y z. R a y & R y z ⟶ R a z" using 1 by (rule allE)
        have 5: "! z. R a b & R b z ⟶ R a z" using 4 by (rule allE)
        have 6: "R a b & R b a ⟶ R a a" using 5 by (rule allE)
        have 7: "¬(R a a)" using 2 by (rule allE)
        have 8: "¬(R a b & R b a)" using 6 7 by (rule mt)
        {assume 9: "R b a"
          have 10: "R a b & R b a" using 3 9 by (rule conjI)
          have 11: False using 8 10 by (rule notE)
        }
        hence 12: "¬(R b a)" by (rule notI)
      }
      hence 13: "R a b ⟶ ¬(R b a)" by (rule impI)
    }
    hence 14: "! y. R a y ⟶ ¬(R y a)" by (rule allI)
  }
  thus "! x y. R x y ⟶ ¬(R y x)" by (rule allI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 21. Demostrar
     {∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
  ------------------------------------------------------------------ *}

lemma ejercicio_21a: carmarria
  assumes 1: "∀x. P x ∨ Q x" and
          2: "∃x. ¬(Q x)" and
          3: "∀x. R x ⟶ ¬(P x)"
  shows   "∃x. ¬(R x)" 
proof -
  obtain a where 4: "¬(Q a)" using 2 by (rule exE)
    have 5: "P a | Q a" using 1 by (rule allE)
    moreover {assume 6: "P a"
      have 7: "¬¬(P a)" using 6 by (rule notnotI)
      have 8: "R a ⟶ ¬(P a)" using 3 by (rule allE)
      have 9: "¬(R a)" using 8 7 by (rule mt)
      have 10: "? x. ¬(R x)" using 9 by (rule exI)
    }
    moreover {assume 10: "Q a"
      have 11: False using 4 10 by (rule notE)
      have 12: "? x. ¬(R x)" using 11 by (rule FalseE)
    }
    ultimately show "? x. ¬(R x)" by (rule disjE)
  qed

text {* --------------------------------------------------------------- 
  Ejercicio 22. Demostrar
     {∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
  ------------------------------------------------------------------ *}

lemma ejercicio_22a: carmarria
  assumes 1: "∀x. P x ⟶ Q x ∨ R x" and
          2: "¬(∃x. P x ∧ R x)"
  shows   "∀x. P x ⟶ Q x"
proof -
  {fix a
    {assume 3: "P a"
      have 4: "P a ⟶ Q a | R a" using 1 by (rule allE)
      have 5: "Q a | R a" using 4 3 by (rule mp)
      moreover {assume 6: "Q a"
      }
      moreover {assume 7: "R a" 
        have 8: "P a & R a" using 3 7 by (rule conjI)
        have 9: "? x. P x & R x" using 8 by (rule exI)
        have 10: False using 2 9 by (rule notE)
        have 11: "Q a" using 10 by (rule FalseE)
      }
      ultimately have 12: "Q a" by (rule disjE)
    }
    hence 13: "P a ⟶ Q a" by (rule impI)
  }
  thus "! x. P x ⟶ Q x" by (rule allI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     ∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
  ------------------------------------------------------------------ *}

lemma ejercicio_23a: carmarria
  assumes 1: "∃x y. R x y ∨ R y x"
  shows   "∃x y. R x y"
proof -
  obtain a where 2: "? y. R a y | R y a" using 1 by (rule exE)
  obtain b where 3: "R a b | R b a" using 2 by (rule exE)
  moreover {assume 4: "R a b"
    have 5: "? y. R a y" using 4 by (rule exI)
    have 6: "? x y. R x y" using 5 by (rule exI)
  }
  moreover {assume 7: "R b a"
    have 8: "? y. R b y" using 7 by (rule exI)
    have 9: "? x y. R x y" using 8 by (rule exI)
  }
  ultimately show "? x y. R x y" by (rule disjE)
qed

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

lemma ejercicio_24a: carmarria
  "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof -
  {assume 1: "? x. ! y. P x y"
    {fix b
    obtain a where 2: "! y. P a y" using 1 by (rule exE)
    have 3: "P a b" using 2 by (rule allE)
    have 4: "? x. P x b" using 3 by (rule exI)
  }
  hence 5: "! y. ? x. P x y" by (rule allI)
}
  thus "(? x. ! y. P x y) ⟶ (! y. ? x. P x y)" by (rule impI)
qed

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

lemma ejercicio_25a: carmarria
  "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
proof (rule iffI)
  {assume 1: "! x. P x ⟶ Q"
    {assume 2: "? x. P x" 
      obtain a where 3: "P a" using 2 by (rule exE)
      have 4: "P a ⟶ Q" using 1 by (rule allE)
      have 5: Q using 4 3 by (rule mp)
    }
    thus 6: "(? x. P x) ⟶ Q" by (rule impI)
  }
next
  {assume 7: "(? x. P x) ⟶ Q" 
    {fix a
      {assume 8: "P a"
        have 9: "? x. P x" using 8 by (rule exI)
        have 10: Q using 7 9 by (rule mp)
      }
      hence 11: "P a ⟶ Q" by (rule impI)
    }
    thus 12: "! x. P x ⟶ Q" by (rule allI)
  }
qed

text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
       ((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_26a: carmarria
  "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof (rule iffI)
  {assume 1: "((! x. P x) ∧ (! x. Q x))"
    have 2: "! x. P x" using 1 by (rule conjunct1)
    have 3: "! x. Q x" using 1 by (rule conjunct2)
    {fix a 
      have 4: "P a" using 2 by (rule allE)
      have 5: "Q a" using 3 by (rule allE)
      have 6: "P a & Q a" using 4 5 by (rule conjI)
    }
    thus 7: "! x. P x & Q x" by (rule allI)
  }
next
  {assume 8: "! x. P x & Q x"
    {fix a
      have 9: "P a & Q a" using 8 by (rule allE)
      have 10: "P a" using 9 by (rule conjunct1)
    }
    hence 11: "! x. P x" by (rule allI)
    {fix a
      have 12: "P a & Q a" using 8 by (rule allE)
      have 13: "Q a" using 12 by (rule conjunct2)
    }
    hence 14: "! x. Q x" by (rule allI)
    show "(! x. P x) & (! x. Q x)" using 11 14 by (rule conjI)
  }
qed

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

lemma ejercicio_27a: carmarria
  "((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
proof (rule iffI)
  {assume 1: "(! x. P x) | (! x. Q x)" 
    moreover {assume 2: "! x. P x"
      {fix a
        have 3: "P a" using 2 by (rule allE)
        have 4: "P a | Q a" using 3 by (rule disjI1)
      }
      hence 5: "! x. P x | Q x" by (rule allI)
    }
    moreover {assume 6: "! x. Q x"
      {fix a
        have 7: "Q a" using 6 by (rule allE)
        have 8:"P a | Q a" using 7 by (rule disjI2)
      }
      hence 9: "! x. P x | Q x" by (rule allI)
    }
    ultimately show "! x. P x | Q x" by (rule disjE)
    }
  next
    {assume 10: "! x. P x | Q x"
      oops

  (* Si tomamos el universo {1,2}, P(x): x=1, Q(x): x=2. Tenemos que es verdad que 
(∀x. x=1 ∨ x=2), pero no se cumple ni (∀x. x=1) ni (∀x. x=2), por lo tanto el bicondicional es falso *)


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

lemma ejercicio_28a: carmarria
  "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
proof (rule iffI)
  {assume 1:"(? x. P x) | (? x. Q x)"
    moreover {assume 2: "? x. P x"
      obtain a where 3: "P a" using 2 by (rule exE)
      have 4: "P a | Q a" using 3 by (rule disjI1)
      have 5: "? x. P x | Q x" using 4 by (rule exI)
    }
    moreover {assume 6: "? x. Q x"
      obtain a where 7: "Q a" using 6 by (rule exE)
      have 8: "P a | Q a" using 7 by (rule disjI2)
      have 9: "? x. P x | Q x" using 8 by (rule exI)
    }
    ultimately show "? x. P x | Q x" by (rule disjE)
  }
next
  {assume 10: "? x. P x | Q x"
    obtain a where 11: "P a | Q a" using 10 by (rule exE)
    moreover {assume 12: "P a"
      have 13: "? x. P x" using 12 by (rule exI)
      have 14: "(? x. P x) | (? x. Q x)" using 13 by (rule disjI1)
    }
    moreover {assume 15: "Q a"
      have 16: "? x. Q x" using 15 by (rule exI)
      have 17: "(? x. P x) | (? x. Q x)" using 16 by (rule disjI2)
    }
    ultimately show "(? x. P x) | (? x. Q x)" by (rule disjE)
  }
qed

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

lemma ejercicio_29: carmarria
  "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
  oops 
(* Si tomamos el universo {1,2} y P(x,y): x=y, entonces tenemos que (∀x. ∃y. x=y) pero no se cumple
que (∃y. ∀x. x=y) *)

text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar o refutar
       (¬(∀x. P x)) ⟷ (∃x. ¬P x)
  ------------------------------------------------------------------ *}

lemma ejercicio_30a: carmarria
  "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof (rule iffI)
  {assume 1: "¬(! x. P x)" 
    {assume 2: "¬(? x. ¬(P x))"
      {fix a
        {assume 3: "¬P a"
          have 4: "? x. ¬P x" using 3 by (rule exI)
          have 5: False using 2 4 by (rule notE)
        }
        hence 6: "¬(¬P a)" by (rule notI)
        have 7: "P a" using 6 by (rule notnotD)
      }
      hence 8: "! x. P x" by (rule allI)
      have 9: False using 1 8 by (rule notE)
    }
    hence 10: "¬¬(? x. ¬(P x))" by (rule notI)
    show "? x. ¬(P x)" using 10 by (rule notnotD)
  }
next
  {assume 11: "? x. ¬P x"
    obtain a where 12: "¬P a" using 11 by (rule exE)
    {assume 13: "! x. P x" 
      have 14: "P a" using 13 by (rule allE)
      have 15: False using 12 14 by (rule notE)
    }
    thus "¬(! x. P x)" by (rule notI)
  }
qed

section {* Ejercicios sobre igualdad *}

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

lemma ejercicio_31a: carmarria
  assumes 1: "P a"
  shows   "∀x. x = a ⟶ P x"
proof -
  {fix b
    {assume 2: "b = a" 
      have 3: "a = b" using 2 by (rule sym)
      have 4: "P b" using 3 1 by (rule subst)
    }
    hence 5: "b = a ⟶ P b" by (rule impI)
  }
  thus "! x. x = a ⟶ P x" by (rule allI)
qed

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

lemma ejercicio_32a: carmarria
  fixes R :: "'c ⇒ 'c ⇒ bool"
  assumes 1: "∃x y. R x y ∨ R y x" and
          2: "¬(∃x. R x x)"
  shows   "∃(x::'c) y. x ≠ y"
proof -
  obtain a where 3: "? y. R a y | R y a" using 1 by (rule exE)
  obtain b where 4: "R a b | R b a" using 3 by (rule exE)
  {assume 5: "a = b"
    have 6: "R a b | R b a" using 4 by this
    moreover {assume 7: "R a b" 
      have 8: "R b b" using 5 7 by (rule subst)
    }
    moreover {assume 9: "R b a" 
      have 10: "R b b" using 5 9 by (rule subst)
    }
    ultimately have 11: "R b b" by (rule disjE)
    have 12: "? x. R x x" using 11 by (rule exI)
    have 13: False using 2 12 by (rule notE)
  }
  hence 14: " a ≠ b " by (rule notI)
  have 15: "? y. a ≠ y" using 14 by (rule exI)
  show "? x y. (x ≠ y)" (* using 15 by (rule exI) *)
    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_33a: carmarria
  assumes 1: "∀x. P a x x" and
          2: "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows   "P (f a) a (f a)"
proof -
  have 3: "P a a a" using 1 by (rule allE)
  have 4: "! y z. P a y z ⟶ P (f a) y (f z)" using 2 by (rule allE)
  have 5: "! z. P a a z ⟶ P (f a) a (f z)" using 4 by (rule allE)
  have 6: "P a a a ⟶ P (f a) a (f a)" using 5 by (rule allE)
  show "P (f a) a (f a)" using 6 3 by (rule mp)
qed

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_34a: carmarria
  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 3: "P a (f a) (f a)" using 1 by (rule allE)
  have 4: "! y z. P a y z ⟶ P (f a) y (f z)" using 2 by (rule allE)
  have 5: "! z. P a (f a) z ⟶ P (f a) (f a) (f z)" using 4 by (rule allE)
  have 6: "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" using 5 by (rule allE)
  have 7: "P (f a) (f a) (f (f a))" using 6 3 by (rule mp)
  show 8: "? z. P (f a) z (f (f a))" using 7 by (rule exI)
qed

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_35a: carmarria
  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: "! y. Q a y ⟶ Q (s a) (s y)" using 2 by (rule allE)
  have 4: "Q a (s a) ⟶ Q (s a) (s (s a))" using 3 by (rule allE)
  have 5: "Q a (s a)" using 1 by (rule allE)
  have 6: "Q (s a) (s (s a))" using 4 5 by (rule mp)
  have 7: "Q a (s a) & Q (s a) (s (s a))" using 5 6 by (rule conjI)
  show "? z. Q a z & Q z (s (s a))" using 7 by (rule exI)
qed

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

lemma ejercicio_36a: carmarria
  assumes 1: "x = f x" and
          2: "odd (f x)"
  shows "odd x"
proof -
  have 3: "f x = x" using 1 by (rule sym)
  show "odd x" using 3 2 by (rule subst)
qed

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

lemma ejercicio_37a: carmarria
  assumes 1: "x = f x" and
          2: "triple (f x) (f x) x"
  shows "triple x x x"
proof -
 have 3: "f x = x" using 1 by (rule sym)
  show 4: "triple x x x" using 3 2 by (rule subst)
qed


end