Relación 4

header {* R4: Deducción natural de primer orden *}

theory R4
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: 
  assumes "∀x. P x ⟶ Q x"
  shows   "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
   assume 1: "∀x. P x" 
    show "∀x. Q x"
     proof (rule allI)
     {fix a 
      have 2: "P(a)" using 1 by (rule allE)
      have 3: "P(a)⟶Q(a)" using assms by (rule allE)
      show "Q a" using 3 2 by (rule mp)}
      qed
qed

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

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

lemma ejercicio_2a: 
  assumes "∃x. ¬(P x)"
  shows   "¬(∀x. P x)"
proof 
assume "∀x. P x" 
  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

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

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

lemma ejercicio_3a: 
  assumes "∀x. P x"
  shows   "∀y. P y"
proof 
{ fix a
  show "P a" using assms by (rule allE)}
qed

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

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

lemma ejercicio_4: 
  assumes "∀x. P x ⟶ Q x"
  shows   "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof 
assume "∀x. ¬(Q x)"
  { fix a
    have "P a ⟶ Q a" using assms by (rule allE)
    have "¬ (Q a)" using `∀x. ¬(Q x)` by (rule allE)
    have "¬(P a)" using `P a ⟶ Q a` `¬ (Q a)` by (rule mt)}
thus "∀x. ¬ (P x)" by (rule allI)
qed

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 by (rule allE)
  have 3 : "¬(Q a)" using 1 by (rule allE)
  have 4 : "¬(P a)" using 2 3 by (rule mt)}
hence "∀x. ¬ (P x)" by (rule allI)}
thus "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))" by (rule impI)
qed

--*
proof(rule impI)
assume 1: "∀x. ¬(Q x)"
show "∀x. ¬(P x)"
 proof-
 {fix a
 have 2: "P a ⟶ Q a" using assms by ( rule allE)
 have 3: " ¬( Q a)" using 1 by ( rule allE)
 have 4: " ¬( P a)" using 2 3 by ( rule mt)}
 thus "∀x. ¬(P x)" by ( rule allI)
qed
qed
text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
       ∀x. P x  ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
  ------------------------------------------------------------------ *}

lemma ejercicio_5: 
  assumes "∀x. P x  ⟶ ¬(Q x)"
  shows   "¬(∃x. P x ∧ Q x)"
proof 
assume "∃x. P x ∧ Q x" 
  obtain a where "P a ∧ Q a" using `∃x. P x ∧ Q x` by (rule exE)
  have "P a" using `P a ∧ Q a` by (rule conjE)
  have "Q a" using `P a ∧ Q a` by (rule conjE)
  have "P a  ⟶ ¬(Q a)" using assms by (rule allE)
  have "¬(Q a)" using `P a  ⟶ ¬(Q a)` `P a` by (rule mp)
show "False" using `¬(Q a)` `Q a` by (rule notE)
qed

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

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

lemma ejercicio_6: 
  assumes "∀x y. P x y"
  shows   "∀u v. P u v"
proof (rule allI)+
fix a b 
have  "∀y. P a y" using assms by (rule allE)
thus " P a b" by (rule allE)
qed

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

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"
proof -
obtain a where "∃y. P a y" using assms by (rule exE)
then obtain b where "P a b" by (rule exE)
hence "∃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: 
  assumes "∃x. ∀y. P x y"
  shows   "∀y. ∃x. P x y"
proof 
obtain a where "∀y. P a y" using assms by (rule exE)
fix b 
have "P a b" using `∀y. P a y` by (rule allE)
thus "∃x. P x b" by (rule exI)
qed
 
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 by (rule exE)
 {fix b 
  have 2 : "P a b" using 1 by (rule allE)
  have 3 : "∃x. P x b" using 2 by (rule exI)}
thus "∀y. ∃x. P x y" by (rule allI)
qed

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

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

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 assms by (rule exE)
have 3 : "Q b" using 2 1 by (rule mp)
have 4 : "∃x. Q x" using 3 by (rule exI)}
thus "P a ⟶ (∃x. Q x)" by (rule impI)
qed

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

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


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

lemma ejercicio_11a: 
  assumes "(∃x. P x) ⟶ Q a"
  shows   "∀x. P x ⟶ Q a"
proof 
     fix b
     show "P b ⟶ Q a"  
        proof
        assume "P b"
        hence "∃x. P x" by (rule exI)
        show "Q a" using assms `∃x. P x` by (rule mp)
    qed
qed
 
lemma ejercicio_11a: 
  assumes "(∃x. P x) ⟶ Q a"
  shows   "∀x. P x ⟶ Q a"
proof-
{fix b
 {assume 1 : "P b"
  have 2 : "∃x. P x" using 1 by (rule exI)
  have 3 : "Q a" using assms 2 by (rule mp)}
hence "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: 
  assumes "∀x. P x ⟶ Q a"
  shows   "∃x. P x ⟶ Q a"
proof -
fix b
have "P b ⟶ Q a" using assms by (rule allE)
thus "∃x. P x ⟶ Q a" by (rule exI)
qed

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

lemma ejercicio_13a: 
  assumes "(∀x. P x) ∨ (∀x. Q x)"
  shows   "∀x. P x ∨ Q x"
proof 
fix a
show "P a ∨ Q a" using assms
proof
assume "∀x. P x"
hence "P a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI1)
next
assume "∀x. Q x"
hence "Q a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI2)
qed
qed

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

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

lemma ejercicio_14a: 
  assumes "∃x. P x ∧ Q x"
  shows   "(∃x. P x) ∧ (∃x. Q x)"
proof
obtain a where "P a ∧ Q a" using assms by (rule exE)
hence "P a" by (rule conjunct1)
thus "∃x. P x" by (rule exI)
have "Q a" using  `P a ∧ Q a` by (rule conjunct2)
thus "∃x. Q x" by (rule exI)
qed
 

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

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

lemma ejercicio_15a: 
  assumes "∀x y. P y ⟶ Q x"
  shows   "(∃y. P y) ⟶ (∀x. Q x)"
proof
assume "∃y. P y"
then obtain b where "P b" by (rule exE)
{fix a 
have "∀y. P y ⟶ Q a" using assms by (rule allE)
hence "P b ⟶ Q a" by (rule allE)
have "Q a" using `P b ⟶ Q a` `P b` by (rule mp)}
thus "∀x. Q x" by (rule allI)
qed
 
lemma ejercicio_15a: 
  assumes "∀x y. P y ⟶ Q x"
  shows   "(∃y. P y) ⟶ (∀x. Q x)"
proof-
{assume 1 : "∃y. P y"
 {fix a
  obtain b where 2 : "P b" using 1 by (rule exE)
  have 3 : "∀y. P y ⟶ Q a" using assms by (rule allE)
  have 4 : "P b ⟶ Q a" using 3 by (rule allE)
  have 5 : "Q a" using 4 2 by (rule mp)}
hence "∀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: 
  assumes "¬(∀x. ¬(P x))"
  shows   "∃x. P x"
proof-
fix x0
{assume 2: "¬(∃x. P x)" 
 {fix x1
  {assume 3: "P x1"
   have 4: "∃x. P x" using 3 by (rule exI)
   have 5: "False" using 2 4 by (rule notE)}
 then have 6: "¬ P x1" by (rule notI)}
then have 7: "∀x. ¬ P x" by (rule allI)
have 8: "False" using 1 7 by (rule notE)}
then show "∃x. P x" by (rule ccontr)
qed 

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

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

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

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

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

lemma ejercicio_18a: 
  assumes "∃x. P x"
  shows   "¬(∀x. ¬(P x))"
proof 
assume "∀x. ¬(P x)"
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

lemma ejercicio_18a: 
  assumes "∃x. P x"
  shows   "¬(∀x. ¬(P x))"
proof-
{assume 1 : "∀x. ¬(P x)"
obtain a where 2 : "P a" using assms by (rule exE)
have 3 : "¬(P a)" using 1 by (rule allE)
have 4 : "False" using 3 2 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: 
  assumes "P a ⟶ (∀x. Q x)"
  shows   "∀x. P a ⟶ Q x"
proof 
fix b
show "P a ⟶ Q b"
proof 
assume "P a" 
have "∀x. Q x" using assms `P a` by (rule mp)
thus "Q b" by (rule allE)
qed
qed

lemma ejercicio_19a: 
  assumes "P a ⟶ (∀x. Q x)"
  shows   "∀x. P a ⟶ Q x"
proof-
{fix b
 {assume 1 : "P a"
  have 2 : "∀x. Q x" using assms 1 by (rule mp)
  have 3 : "Q b" using 2 by (rule allE)}
hence 4 : "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: 
  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)"


proof (rule allI)+
fix  a b 
show "R a b ⟶ ¬(R b a )" 
proof 
assume 1:"R a b"
show"¬(R b a)"
proof
assume 2:"R b a" 
have 3:"R a b ∧ R b a" using 1 2..
have  "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1)..
hence  "∀z. R a b ∧ R b z ⟶ R a z"..
hence 4:"R a b ∧ R b a ⟶ R a a"..
have 5:"R a a" using 4 3..
have 6:" ¬(R a a)" using assms(2)..
show False using 6 5..
qed
qed
qed

lemma ejercicio_20a: 
  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)"
proof-
{fix a
 {fix b
  {assume 1 : "R a b"
   {assume 2 : "R b a"
    have 3 : "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
    have 4 : "∀z. R a b ∧ R b z ⟶ R a z" using 3 by (rule allE)
    have 5 : "R a b ∧ R b a ⟶ R a a" using 4 by (rule allE)
    have 6 : " R a b ∧ R b a" using 1 2 by (rule conjI)
    have 7 : "R a a" using 5 6 by (rule mp)
    have 8 : "¬(R a a)" using assms(2) by (rule allE)
    have "False" using 8 7 by (rule notE)}
   hence "¬(R b a)" by (rule notI)}
  hence "R a b ⟶ ¬(R b a)" by (rule impI)}
hence  "∀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:
  assumes "∀x. P x ∨ Q x" 
          "∃x. ¬(Q x)" 
          "∀x. R x ⟶ ¬(P x)"
  shows   "∃x. ¬(R x)" 
proof-
obtain a where "¬(Q a)" using assms(2) by (rule exE)
have "P a ∨ Q a" using assms(1) by (rule allE)
show "∃x. ¬(R x)" using `P a ∨ Q a`
proof
assume "P a"
hence 1:"¬¬(P a)" by (rule notnotI)
have 2:"R a ⟶ ¬(P a)" using assms(3) by (rule allE)
have "¬(R a)" using 2 1 by (rule mt)
thus "∃x. ¬(R x)" by (rule exI)
next
assume "Q a"
have False using `¬(Q a)` `Q a` by (rule notE) 
thus "∃x. ¬(R x)" by (rule ccontr)
qed
qed


lemma ejercicio_21a:
  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) by (rule exE)
have 2 : "P a ∨ Q a" using assms(1) by (rule allE)
have  "P a ∨ Q a" using 2 by this
moreover
{assume 3 : "P a"
have 4 : "R a ⟶ ¬(P a)" using assms(3) by (rule allE)
have 5 : "¬¬(P a)" using 3 by (rule notnotI)
have 6 : "¬(R a)" using 4 5 by (rule mt)
have "∃x. ¬(R x)" using 6 by (rule exI)}
moreover 
{assume 7 : "Q a"
have "∃x. ¬(R x)"  using 1 7 by (rule notE)}
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:
  assumes "∀x. P x ⟶ Q x ∨ R x" 
          "¬(∃x. P x ∧ R x)"
  shows   "∀x. P x ⟶ Q x"
proof
fix a 
show "P a ⟶ Q a"
proof 
assume 1:"P a"
have 2:"P a ⟶ Q a ∨ R a" using assms(1) by (rule allE)
have 3:"Q a ∨ R a" using  2 1 by (rule mp)
show "Q a" using 3 
proof
assume "Q a"
next 
assume 4:"R a"
have "P a ∧ R a" using 1 4 by (rule conjI)
hence 5:"∃x. P x ∧ R x" by (rule exI)
have False using assms(2) 5 by (rule notE)
thus "Q a" by (rule ccontr)
qed
qed
qed
 
lemma ejercicio_22a:
  assumes "∀x. P x ⟶ Q x ∨ R x" 
          "¬(∃x. P x ∧ R x)"
  shows   "∀x. P x ⟶ Q x"
proof-
{fix a
 {assume 1 : "P a"
 have 2 : "P a ⟶ Q a ∨ R a" using assms(1) by (rule allE)
 have 3 : "Q a ∨ R a" using 2 1 by (rule mp)
 moreover
 {assume 4 : "Q a"
  have "Q a" using 4 by this}
 moreover
 {assume 5 : "R a"
 have 6 : "P a ∧ R a" using 1 5 by (rule conjI)
 have 7 : "∃x. P x ∧ R x" using 6 by (rule exI)
 have "Q a" using assms(2) 7 by (rule notE)}
 ultimately have "Q a" by (rule disjE)}
hence "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:
  assumes "∃x y. R x y ∨ R y x"
  shows   "∃x y. R x y"
proof -
obtain a where "∃y. R a y ∨ R y a " using assms by (rule exE)
then obtain b where 1:"R a b ∨ R b a" by (rule exE)
show "∃x y. R x y" using 1
proof
assume "R a b"
hence "∃y. R a y" by (rule exI)
thus "∃x y. R x y" by (rule exI)
next
assume "R b a"
hence "∃y. R b y" by (rule exI)
thus "∃x y. R x y" by (rule exI)
qed
qed

lemma ejercicio_23a:
  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 by (rule exE)
obtain b where 2: "R a b ∨ R b a" using 1 by (rule exE)
moreover
{assume 3 : "R a b"
have 4 : "∃y. R a y" using 3 by (rule exI)
have 5 : "∃x y. R x y" using 4 by (rule exI)}
moreover
{assume 6 : "R b a"
have 7 : "∃y. R b y" using 6 by (rule exI)
have 8 : "∃x y. R x y" using 7 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: 
  "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof-
{assume 1 : "∃x. ∀y. P x y"
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)}
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: 
  "(∀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 "(∃x. P x) ⟶ Q"  by (rule impI)}
next
{assume 6 : "(∃x. P x) ⟶ Q"
 {fix a
  {assume 7 : "P a"
   have 8 : "∃x. P x" using 7 by (rule exI)
   have 9 : "Q" using 6 8 by (rule mp)}
 hence "P a ⟶ Q" by (rule impI)}
thus "∀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: 
  "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof (rule iffI)
{assume 1 : "(∀x. P x) ∧ (∀x. Q x)"
 {fix a
  have 2 : "∀x. P x" using 1 by (rule conjunct1)
  have 3 : "P a" using 2 by (rule allE)
  have 4 : "∀x. Q x" using 1 by (rule conjunct2)
  have 5 : "Q a" using 4 by (rule allE)
  have "P a ∧ Q a" using 3 5 by (rule conjI)}
thus "∀x. P x ∧ Q x" by (rule allI)}
next
{assume 6 : "∀x. P x ∧ Q x"
 {fix a
 have 7 : "P a ∧ Q a" using 6 by (rule allE)
 have 8 : "P a" using 7 by (rule conjunct1)}
hence 9 : "∀x. P x" by (rule allI)
 {fix a
 have 10 : "P a ∧ Q a" using 6 by (rule allE)
 have 11 : " Q a" using 10 by (rule conjunct2)}
hence 12: "∀x. Q x" by (rule allI)
show "(∀x. P x) ∧ (∀x. Q x)" using 9 12 by (rule conjI)}
qed

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

lemma ejercicio_27a: 
  "((∀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_28a: 
  "((∃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 "(∃x. P x) ∨ (∃x. Q x)" using 13 by (rule disjI1)}
moreover
 {assume 14 : "Q a"
  have 15 : "∃x. Q x" using 14 by (rule exI)
  have "(∃x. P x) ∨ (∃x. Q x)" using 15 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: 

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

lemma ejercicio_30a: 
  "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof (rule iffI)
   assume 1: "¬(∀x. P x)"
   show  "∃x. ¬P x"
   proof (rule ccontr)
   assume 2: "¬(∃x. ¬P x)"
   show "False"
   proof -
   { 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 ccontr)}
   hence 7: "∀x. P x" by (rule allI)
   show 8: "False" using 1 7 by (rule notE)
qed
qed
next
   assume 9: "∃x. ¬P x"
   show "¬(∀x. P x)"
   proof -
   {assume 10: "¬¬(∀x. P x)"
    have 11: "∀x. P x" using 10 by (rule notnotD)
    obtain a where 12: "¬P a" using 9 by (rule exE)
    have 13: "P a" using 11 by (rule allE)
    have 14: "False" using 12 13 by (rule notE)}
   thus 15: "¬(∀x. P x)" by (rule ccontr)
qed
qed

lemma ejercicio_30a: 
  "(¬(∀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 "P a" by (rule ccontr)}
 hence 6 : "∀x. P x" by (rule allI)
 have "False" using 1  6 by (rule notE)}
thus "∃x. ¬P x" by (rule ccontr)}
next
{assume 7 : "∃x. ¬P x"
 {assume 8 : "∀x. P x"
  obtain a where 9 : "¬P a" using 7 by (rule exE)
  have 10 : "P a" using 8 by (rule allE)
  have "False" using 9 10 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:
  assumes "P a"
  shows   "∀x. x = a ⟶ P x"
proof (rule allI)
  fix b
  show "b = a ⟶ P b"
  proof (rule impI)
  assume 1: "b = a"
  show "P b"
  proof -
  have 2: "a = b" using 1 by (rule sym)
  show 3: "P b" using 2 assms(1) by (rule subst)
qed
qed
qed


lemma ejercicio_31a:
  assumes "P a"
  shows   "∀x. x = a ⟶ P x"
proof-
{fix b
 {assume 1 : "b = a"
  have 3 : "P b" using 1 assms by (rule ssubst)}
hence "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:
  fixes R :: "'c ⇒ 'c ⇒ bool"
  assumes "∃x y. R x y ∨ R y x"
          "¬(∃x. R x x)"
  shows   "∃(x::'c) y. x ≠ y"
proof-
obtain a where 1 : "∃y. R a y ∨ R y a" using assms(1) by (rule exE)
obtain b where 2 : "R a b ∨ R b a" using 1 by (rule exE)
{assume 3 : "a = b"
have "R a b ∨ R b a"  using 2 by this
moreover
 {assume 4 : "R a b"
  have 5 : "R b b" using 3 4 by (rule subst)
  have 6 : "∃x. R x x" using 5 by (rule exI)
  have "False" using assms(2) 6 by (rule notE)}
moreover
 {assume 7 : "R b a"
  have 8 : "R b b" using 3 7 by (rule subst)
  have 9 : "∃x. R x x" using  8 by (rule exI)
  have "False" using assms(2) 9 by (rule notE)}
ultimately have "False" by (rule disjE)}
hence 10 : "¬(a = b)" by (rule notI)
have 11 : "∃y. ¬(a = y)" using 10 by (rule exI)
show "∃(x::'c) y. x ≠ y" using 11 by (rule exI)
qed

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:
  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)"
proof -
    have 1: "P a a a" using assms(1) by (rule allE)
    have 2: "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
    have 3: "∀z. P a a z ⟶ P (f a) a (f z)" using 2 by (rule allE)
    have 4: "P a a a ⟶ P (f a) a (f a)" using 3 by (rule allE)
    show 5: "P (f a) a (f a)" using 4 1 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:
  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))"

proof - 
   have 1: "P a (f a) (f a)" using assms(1) by (rule allE)
   have 2: "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
   have 3: "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" using 2 by (rule allE)
   have 4: "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" using 3 by (rule allE)
   have 5: "P (f a) (f a) (f (f a))" using 4 1 by (rule mp)
   show 6: "∃z. P (f a) z (f (f a))" using 5 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:
  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))"
proof -
    have 1: "Q a (s a)" using assms(1) by (rule allE)
    have 2: "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) by (rule allE)
    have 3: "Q a (s a) ⟶ Q (s a) (s (s a))" using 2 by (rule allE)
    have 4: "Q (s a) (s (s a))" using 3 1 by (rule mp)
    have 5: "Q a (s a) ∧ Q (s a) (s (s a))" using 1 4 by (rule conjI)
    show 6: "∃z. Q a z ∧ Q z (s (s a))" using 5 by (rule exI)
qed
text {* --------------------------------------------------------------- 
  Ejercicio 36. Demostrar o refutar
     {x = f x, odd (f x)} ⊢ odd x
  ------------------------------------------------------------------ *}

lemma ejercicio_36a:
  assumes "x = f x" and
          "odd (f x)"
  shows "odd x"
proof -
  show "odd x" using assms(1) assms(2) by (rule ssubst)
qed

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

lemma ejercicio_37a:
  assumes "x = f x" and
          "triple (f x) (f x) x"
  shows "triple x x x"

proof -
   show "triple x x x" using assms(1) assms(2) by (rule ssubst)
qed

end