Relación 2

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

theory R2
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)"

  
 (*Solución M.Cumplido*)
proof(rule impI)
assume "∀x. P x"
show "∀x. Q x"
  proof(rule allI)
  fix a
  have "P a" using `∀x. P x` by (rule allE)  
  have "P a ⟶ Q a" using assms by (rule allE)
  thus "Q a" using `P a` by (rule mp) 
  qed
qed

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

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

   (*Solución M.Cumplido*)
proof
obtain "a" where "¬(P a)" using assms by (rule exE)
assume "∀x. P x"
hence "P a" by (rule allE)
with `¬(P a)` show False by (rule notE)
qed

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

lemma ejercicio_3a: 
  assumes "∀x. P x"
  shows   "∀y. P y"
  (*Solución M.Cumplido*)
proof
fix y
show "P y" using assms by (rule allE)
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))"

  (*Solución M.Cumplido*)  
proof
assume "∀x. ¬(Q x)"
show "∀x. ¬ (P x)"
  proof
  fix a
  have "P a ⟶ Q a" using assms by (rule allE)
  have " ¬(Q a)" using  `∀x. ¬(Q x)` by (rule allE)
  with `P a ⟶ Q a` show "¬(P a)" by (rule mt)
  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)"

    (*Solución M.Cumplido*)
proof
assume "∃x. P x ∧ Q x"
then obtain a where "P a ∧ Q a" by (rule exE)
hence "P a" by (rule conjunct1)
have "P a  ⟶ ¬(Q a)"  using assms by (rule allE)
hence "¬(Q a)" using `P a` by (rule mp)
have "Q a" using `P a ∧ Q a` by (rule conjunct2)
with `¬(Q a)` show False by (rule notE)
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"

(*Solución M.Cumplido*)
proof
fix u
have "∀y. P u y" using assms by (rule allE)
show "∀v. P u v"
  proof
  fix v
  show "P u v" using  `∀y. P u y` by (rule allE)  
  qed
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"

  (*Solución M.Cumplido*)
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"

    (*Solución M.Cumplido*)
proof
fix a
obtain b where " ∀y. P b y" using assms by (rule exE)
hence "P b a" by (rule allE)
thus "∃c. P c a " by (rule exI)
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)"
     
 (*Solución M.Cumplido*)
proof
assume "P a"
obtain b where "P a ⟶ Q b" using assms by (rule exE)
hence "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: 
  fixes P Q :: "'b ⇒ bool" 
  assumes "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"

(*Solución M.Cumplido*)

proof -
have "¬(P a)∨ P a" by (rule excluded_middle)
thus "∃x. P a ⟶ Q x"
  proof
  assume "¬(P a)"
  have "P a ⟶ Q a"
    proof
    assume "P a"
    with `¬(P a)` show "Q a" by (rule notE)
    qed
  thus  "∃x. P a ⟶ Q x" by (rule exI) 
  next
  assume "P a"
  with assms have "∃x. Q x" by (rule mp)
  then obtain b where "Q b" by (rule exE)
  have "P a⟶ Q b"
    proof
    assume "P a"
    show "Q b" using `Q b ` by this
    qed
  thus  "∃x. P a ⟶ Q x" by (rule exI)  
  qed
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"

(*Solución M.Cumplido*)  
proof
fix c
show "P c ⟶ Q a"
  proof(rule impI)
  assume "P c"
  hence "∃x. P x" by (rule exI)
  with assms show "Q a" by (rule mp)
  qed
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"

  (*Solución M.Cumplido*)
proof -
have "P x ⟶ 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"

  
   (*Solución M.Cumplido*)
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)  }
  {assume "∀x. Q x"
   hence "Q a" by (rule allE)
   thus "P a ∨ Q a" by (rule disjI2)  }
  qed
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)"

 (*Solución M.Cumplido*) 
proof
obtain x where "P x ∧ Q x" using assms by (rule exE)
hence "P x" by (rule conjunct1)
thus "∃x. P x" by (rule exI)
next
obtain x where "P x ∧ Q x" using assms by (rule exE)
hence "Q x" by (rule conjunct2)
thus "∃x. Q x" by (rule exI)
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)"

   (*Solución M.Cumplido*) 
proof(rule impI)
assume "∃y. P y"
show "∀x. Q x"
  proof
  fix x
  obtain y where "P y" using `∃y. P y`  by (rule exE)
  have "∀y. P y ⟶ Q x" using assms by (rule allE)
  hence "P y ⟶ Q x"  by (rule allE)
  thus "Q x" using `P y` by (rule mp)
  qed
qed

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

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

(*Solución M.Cumplido*)
proof(rule ccontr)
assume "¬(∃x. P x)"
have "∀x. ¬(P x)"
    proof
    fix a
    show "¬(P a)"
      proof(rule notI)
      assume "P a"
      hence "∃x. P x" by (rule exI)
      with `¬(∃x. P x)` show False by (rule notE)
      qed
    qed
with assms show False by (rule notE)    
qed
 

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

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

(*Solución M.Cumplido*)
proof
assume "∃x. P x"
then obtain x where "P x" by (rule exE)
have "¬(P x)" using assms by (rule allE)
thus False using `P x` by (rule notE) 
qed

text {* --------------------------------------------------------------- 
  Ejercicio 18. Demostrar
       ∃x. P x ⊢ ¬(∀x. ¬(P x))
  ------------------------------------------------------------------ *}
 
lemma ejercicio_18a: 
  assumes "∃x. P x"
  shows   "¬(∀x. ¬(P x))"

  (*Solución M.Cumplido*)
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)
thus False using `P a` by (rule notE)
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"

  (*Solución M.Cumplido*)
proof
fix x
show "P a ⟶ Q x"
    proof(rule impI)
    assume "P a"
    with assms have "∀x. Q x" by (rule mp)
    thus "Q x" by (rule allE)
    qed
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)"

  (*Solución M.Cumplido*)
proof
fix x
have "¬(R x x)" using assms(2) by (rule allE)
show "∀y. R x y ⟶ ¬(R y x)"
  proof
  fix y
  show " R x y ⟶ ¬(R y x)"
    proof(rule impI)
    have "∀y z. R x y ∧ R y z ⟶ R x z" using assms(1) by (rule allE)
    hence "∀z. R x y ∧ R y z ⟶ R x z" by (rule allE)
    hence "R x y ∧ R y x ⟶ R x x" by (rule allE)
    hence "¬(R x y ∧ R y x )" using `¬(R x x)` by (rule mt)
    assume "R x y"
    show "¬(R y x)" 
      proof
      assume "R y x"
      with `R x y` have "R x y ∧ R y x " by (rule conjI)
      with `¬(R x y ∧ R y x )` show False by (rule notE)
      qed
    qed  
  qed
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)" 

  (*Solución M.Cumplido*)
proof-  
obtain x where "¬(Q x)" using assms(2) by (rule exE)
have "P x ∨ Q x" using assms(1) by (rule allE)
hence "P x"
  proof
  assume "P x"
  thus "P x" by this
  next
  assume "Q x"
  with `¬(Q x)` show "P x" by (rule notE)
  qed
hence "¬¬(P x)" by (rule notnotI)  
have  "R x ⟶ ¬(P x)" using assms(3) by (rule allE)  
hence "¬(R x)" using `¬¬(P x)` by (rule mt)
thus  "∃x. ¬(R x)"  by (rule exI)
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"

  (*Solución M.Cumplido*)
proof
fix x
show  "P x ⟶ Q x"
  proof(rule impI)
  assume "P x"
  have  "P x ⟶ Q x ∨ R x" using assms(1) by (rule allE)
  hence "Q x ∨ R x" using `P x` by (rule  mp)
  thus "Q x"
    proof
    assume "Q x"
    thus "Q x" by this
    next
    assume "R x"
    with `P x` have  "P x & R x" by (rule conjI)
    hence "∃x. P x & R x" by (rule exI)
    with assms(2) show "Q x" by (rule notE)
    qed
  qed
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"

  (*Solución M.Cumplido*)
proof-
obtain a where "∃y. R a y ∨ R y a" using assms by (rule exE)
then obtain b where "R a b ∨ R b a"  by (rule exE)
thus "∃x y. R x y" 
  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

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

  (*Solución M.Cumplido*)
proof
assume "(∃x. ∀y. P x y)"
show "(∀y. ∃x. P x y)"
  proof(rule allI)
  fix b
  obtain a where "(∀y. P a y)" using `(∃x. ∀y. P x y)` by (rule exE)
  hence "P a b" by (rule allE)
  thus "∃x. P x b" by (rule exI)
  qed
qed

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

  (*Solución M.Cumplido*)
proof
assume "∀x. P x ⟶ Q"
show "((∃x. P x) ⟶ Q)"
  proof(rule impI)
  assume "∃x. P x"
  then obtain a where "P a" by (rule exE)
  have "P a ⟶ Q" using `∀x. P x ⟶ Q` by (rule allE)
  thus Q using `P a` by (rule mp)
  qed
next
assume "((∃x. P x) ⟶ Q)"
show "∀x. P x ⟶ Q"
  proof
  fix a
  show "P a ⟶ Q"
    proof(rule impI)
    assume "P a"
    hence "∃x. P x" by (rule exI)
    with `((∃x. P x) ⟶ Q)` show Q by (rule mp)
    qed
  qed  
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)"

  (*Solución M.Cumplido*)
proof
assume"(∀x. P x) ∧ (∀x. Q x)"
hence "(∀x. P x)" by (rule conjunct1)
have "(∀x. Q x)" using `(∀x. P x) ∧ (∀x. Q x)` by (rule conjunct2)
show "(∀x. P x ∧ Q x)"
  proof
  fix a
  have "P a" using `(∀x. P x)` by (rule allE)
  have "Q a" using `(∀x. Q x)` by (rule allE)
  with `P a` show "P a ∧ Q a" by (rule conjI)
  qed
next
assume "(∀x. P x ∧ Q x)"
show "(∀x. P x) ∧ (∀x. Q x)"
  proof
  show "∀x. P x" 
    proof
    fix a
    have "P a ∧ Q a" using `(∀x. P x ∧ Q x)` by (rule allE)
    thus "P a" by (rule conjunct1)
    qed
  next
  show "∀x. Q x" 
    proof
    fix a
    have "P a ∧ Q a" using `(∀x. P x ∧ Q x)` by (rule allE)
    thus "Q a" by (rule conjunct2)
    qed     
  qed
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)"
quickcheck
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)"


(*Solución M.Cumplido*)
proof
assume "(∃x. P x) ∨ (∃x. Q x)"
thus "(∃x. P x ∨ Q x)"
  proof
  assume "∃x. P x"
  then obtain b where "P b" by (rule exE)
  hence "P b ∨ Q b" by (rule disjI1)
  thus "(∃x. P x ∨ Q x)" by (rule exI)
  next
  assume "∃x. Q x"
  then obtain b where "Q b" by (rule exE)
  hence "P b ∨ Q b" by (rule disjI2)
  thus "(∃x. P x ∨ Q x)" by (rule exI)
  qed
next  
assume "(∃x. P x ∨ Q x)"
then obtain b where "P b ∨ Q b" by (rule exE)
thus "(∃x. P x) ∨ (∃x. Q x)"
  proof
  assume "P b"
  hence "(∃x. P x)" by (rule exI)
  thus "(∃x. P x) ∨ (∃x. Q x)" by (rule disjI1)
  next
  assume "Q b"
  hence "(∃x. Q x)" by (rule exI)
  thus "(∃x. P x) ∨ (∃x. Q x)" by (rule disjI2)
  qed
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)"
quickcheck
oops

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

lemma ejercicio_30a: 
  "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"

(*Solución M.Cumplido*)
proof
assume "¬(∀x. P x)" 
show "(∃x. ¬P x)"
  proof(rule ccontr)
    assume "¬(∃x. ¬P x)"
    have "(∀x. P x)"
      proof 
      fix a
      show "P a"
        proof(rule ccontr)
        assume "¬(P a)"
        hence "(∃x. ¬P x)" by (rule exI)
        with `¬(∃x. ¬P x)` show False by (rule notE)
        qed
      qed
    with  `¬(∀x. P x)` show False by (rule notE) 
    qed
next
assume  "(∃x. ¬P x)" 
thus  "¬(∀x. P x)" by (rule ejercicio_2a)
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"

(*Solución M.Cumplido*)
proof
fix x
show "x = a ⟶ P x"
  proof
  assume "x=a"
  hence "a=x" by (rule sym)
  thus "P x" using assms by (rule subst)
  qed
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"

  (*Solución M.Cumplido*)
proof-
obtain a where "∃y. R a y ∨ R y a" using assms(1) by (rule exE)
then obtain b where " R a b ∨ R b a"  by (rule exE)
have "a≠b ∨ a=b " by (rule excluded_middle)
thus  "∃(x::'c) y. x ≠ y"
  proof
  assume "a≠b"
  hence "∃y. a ≠ y" by (rule exI)
  thus  "∃(x::'c) y. x ≠ y" by (rule exI)
  next
  assume "a=b"
  show "∃(x::'c) y. x ≠ y" using `R a b ∨ R b a`  
    proof
    assume "R a b"
    with `a=b` have "R b b" by (rule subst)
    hence "(∃x. R x x)" by (rule exI)
    with `¬(∃x. R x x)` show "∃(x::'c) y. x ≠ y" by (rule notE)
    next
    assume "R b a"
    with `a=b` have "R b b" by (rule subst)
    hence "(∃x. R x x)" by (rule exI)
    with `¬(∃x. R x x)` show "∃(x::'c) y. x ≠ y" by (rule notE)
    qed
  qed
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)"

  (*Solución M.Cumplido*)
proof-
have "P a a a" using assms(1) by (rule allE)
have " ∀y z. P a  y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
hence  " ∀z. P a  a z ⟶ P (f a) a (f z)"  by (rule allE)
hence " P a  a a ⟶ P (f a) a (f a)" by (rule allE)
thus  "P (f a) a (f a)" using `P a a a` 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))"
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_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))"
oops

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

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


end