Ver el código de «Rel 5»

<source lang = "isabelle">
chapter ‹R5: Deducción natural de primer orden›

theory R5_sol
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)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_1a: 
  "∀x. P x ⟶ Q x ⟹ (∀x. P x) ⟶ (∀x. Q x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_1b: 
  assumes "∀x. P x ⟶ Q x"
  shows   "(∀x. P x) ⟶ (∀x. Q x)"
proof
  assume "∀x. P x"
  show "∀x. Q x"
  proof
    fix a
    have "P a" using ‹∀x. P x› ..
    have "P a ⟶ Q a" using assms(1) ..
    thus "Q a" using ‹P a› ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_1c: 
  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" using ‹∀x. P x› by (rule allE)
    have "P a ⟶ Q a" using assms(1) by (rule allE)
    thus "Q a" using ‹P a› by (rule mp)
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_1d: 
  "⟦∀x. P x ⟶ Q x⟧ ⟹(∀x. P x) ⟶ (∀x. Q x)"
  apply (rule impI)
  apply (rule allI)
  apply (erule_tac x = x in allE)
  apply (erule_tac x = x in allE)
  apply (drule mp)
  apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 2. Demostrar
       ∃x. ¬(P x) ⊢ ¬(∀x. P x)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_2a: "∃x. ¬(P x) ⟹ ¬(∀x. P x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_2b: 
  assumes "∃x. ¬(P x)"
  shows   "¬(∀x. P x)"
proof
  assume "∀x. P x"
  obtain a where "¬(P a)" using assms(1) .. 
  have "P a" using ‹∀x. P x› ..
  with ‹¬(P a)› show False ..
qed

― ‹La demostración detallada es›
lemma ejercicio_2c: 
  assumes "∃x. ¬(P x)"
  shows   "¬(∀x. P x)"
proof (rule notI)
  assume "∀x. P x"
  obtain a where "¬(P a)" using assms(1) by (rule exE)
  have "P a" using ‹∀x. P x› by (rule allE)
  with ‹¬(P a)› show False by (rule notE)
qed

― ‹La demostración aplicativa es›
lemma ejercicio_2d: "⟦∃x. ¬(P x)⟧ ⟹ ¬(∀x. P x)"  
  apply (rule notI)
  apply (erule exE)
  apply (erule allE)
  apply (erule notE)
  apply assumption
  done

text ‹--------------------------------------------------------------- 
  Ejercicio 3. Demostrar
       ∀x. P x ⊢ ∀y. P y
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_3a: "∀x. P x  ⟹ ∀y. P y"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_3b: 
  assumes "∀x. P x"
  shows   "∀y. P y"
proof
  fix a
  show "P a" using assms ..
qed

― ‹La demostración estructurada es›
lemma ejercicio_3c: 
  assumes "∀x. P x"
  shows   "∀y. P y"
proof (rule allI)
  fix a
  show "P a" using assms by (rule allE)
qed

― ‹La demostración estructurada es›
lemma ejercicio_3d: "⟦∀x. P x⟧ ⟹ ∀y. P y"  
  apply (rule allI)
  apply (erule allE)
  apply assumption
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 4. Demostrar
       ∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_4a: 
  "∀x. P x ⟶ Q x ⟹ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_4b: 
  assumes "∀x. P x ⟶ Q x"
  shows   "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof
  assume "∀x. ¬(Q x)"
  show "∀x. ¬(P x)"
  proof
    fix a
    show "¬(P a)"
    proof
      assume "P a"
      have "P a ⟶ Q a" using assms ..
      hence "Q a" using ‹P a› ..
      have "¬(Q a)" using ‹∀x. ¬(Q x)› ..
      thus False using ‹Q a› ..
    qed
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_4c: 
  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
    show "¬(P a)"
    proof
      assume "P a"
      have "P a ⟶ Q a" using assms by (rule allE)
      hence "Q a" using ‹P a› by (rule mp)
      have "¬(Q a)" using ‹∀x. ¬(Q x)› by (rule allE) 
      thus False using ‹Q a› by (rule notE)
    qed
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_4d: 
   "⟦∀x. P x ⟶ Q x⟧⟹(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"  
  apply (rule impI)
  apply (rule allI)
  apply (erule_tac x = x in allE)
  apply (erule_tac x = x in allE)
  apply (drule mt)
   apply assumption+
    done

text ‹--------------------------------------------------------------- 
  Ejercicio 5. Demostrar
       ∀x. P x  ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_5a: 
  "∀x. P x  ⟶ ¬(Q x) ⟹ ¬(∃x. P x ∧ Q x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_5b: 
  assumes "∀x. P x  ⟶ ¬(Q x)"
  shows   "¬(∃x. P x ∧ Q x)"
proof
  assume "∃x. P x ∧ Q x"
  then obtain a where "P a ∧ Q a" ..
  hence "P a" ..
  have "P a ⟶ ¬(Q a)" using assms ..
  hence "¬(Q a)" using ‹P a› ..
  have "Q a" using ‹P a ∧ Q a› ..
  with ‹¬(Q a)› show False ..
qed

― ‹La demostración estructurada es›
lemma ejercicio_5c: 
  assumes "∀x. P x  ⟶ ¬(Q x)"
  shows   "¬(∃x. P x ∧ Q x)"
proof (rule notI)
  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

― ‹La demostración aplicativa es›
lemma ejercicio_5d: 
  "⟦∀x. P x  ⟶ ¬(Q x)⟧ ⟹ ¬(∃x. P x ∧ Q x)"
  apply (rule notI)
  apply (erule exE)
  apply (frule conjunct2)
  apply (rule notE)
  apply (erule allE)
   apply (drule mp)
  apply (rule conjunct1)
  apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 6. Demostrar
       ∀x y. P x y ⊢ ∀u v. P u v
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_6a: 
  "∀x y. P x y ⟹ ∀u v. P u v"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_6b: 
  assumes "∀x y. P x y"
  shows   "∀u v. P u v"
proof 
  fix a 
  show "∀v. P a v"
  proof
    fix b
    have "∀y. P a y" using assms .. 
    thus "P a b" ..
  qed
qed

― ‹La demostración estructurada simplificada es›
lemma ejercicio_6b2: 
  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 .. 
  thus "P a b" ..
qed

― ‹La demostración detallada es›
lemma ejercicio_6c: 
  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

― ‹La demostración aplicativa es›
lemma ejercicio_6e: "⟦∀x y. P x y ⟧ ⟹ ∀u v. P u v"
  apply (rule allI)
  apply (rule allI)
  apply (erule allE)+
  apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 7. Demostrar
       ∃x y. P x y ⟹ ∃u v. P u v
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_7a: 
  "∃x y. P x y ⟹ ∃u v. P u v"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_7b: 
  assumes "∃x y. P x y"
  shows   "∃u v. P u v"
proof -
  obtain a where "∃y. P a y" using assms ..
  then obtain b where "P a b" ..
  hence "∃v. P a v" ..
  thus "∃u v. P u v" ..
qed


― ‹La demostración aplicativa es›
lemma ejercicio_7d: "⟦∃x y. P x y ⟧ ⟹ ∃u v. P u v"
  apply (erule exE)+
  apply (rule exI)
  apply (rule exI)
  apply assumption+
  done

text ‹--------------------------------------------------------------- 
  Ejercicio 8. Demostrar
       ∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_8a: 
  "∃x. ∀y. P x y ⟹ ∀y. ∃x. P x y"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_8b: 
  assumes "∃x. ∀y. P x y"
  shows   "∀y. ∃x. P x y"
proof
  fix b
  obtain a where "∀y. P a y" using assms ..
  hence "P a b" ..
  thus "∃x. P x b" ..
qed

― ‹La demostración detallada es›
lemma ejercicio_8c: 
  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)
  hence "P a b" by (rule allE)
  thus "∃x. P x b" by (rule exI)
qed

― ‹La demostración aplicativa es›
lemma ejercicio_8d: "⟦∃x. ∀y. P x y ⟧ ⟹ ∀y. ∃x. P x y" 
  apply (rule allI)
  apply (rule exE)
  apply assumption+
  apply (rule allE)
  apply assumption+
  apply (rule exI)
  apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 9. Demostrar
       ∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_9a: 
  "∃x. P a ⟶ Q x ⟹ P a ⟶ (∃x. Q x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_9b: 
  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 ..
  hence "Q b" using ‹P a› ..
  thus "∃x. Q x" ..
qed

― ‹La demostración detallada es›
lemma ejercicio_9c: 
  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)
  hence "Q b" using ‹P a› by (rule mp)
  thus "∃x. Q x" by (rule exI)
qed

― ‹La demostración aplicativa es›
lemma ejercicio_9d: "⟦∃x. P a ⟶ Q x ⟧ ⟹ P a ⟶ (∃x. Q x)" 
  apply (rule impI)
  apply (rule exE)
   apply assumption+
  apply (drule mp)
   apply assumption+
  apply (rule exI)
   apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 10. Demostrar
       P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x 
  ------------------------------------------------------------------›

lemma ejercicio_10a: 
  "P a ⟶ (∃x. Q x) ⟹ ∃x. P a ⟶ Q x"
by auto


lemma ejercicio_10b: 
  fixes P Q :: "'b ⇒ bool" 
  assumes "P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
  have "¬(P a) ∨ P a" ..
  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" ..
    qed
    thus "∃x. P a ⟶ Q x" ..
  next
    assume "P a"
    with assms have "∃x. Q x" by (rule mp)
    then obtain b where "Q b" .. 
    have "P a ⟶ Q b"
    proof
      assume "P a"
      note ‹Q b› 
      thus "Q b" .
    qed
    thus "∃x. P a ⟶ Q x" ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_10c: 
  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 (rule disjE)
    assume "¬(P a)"
    have "P a ⟶ Q a"
    proof (rule impI)
      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 (rule impI)
      assume "P a"
      note ‹Q b› 
      thus "Q b" by this
    qed
    thus "∃x. P a ⟶ Q x" by (rule exI)
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_10d: 
   "P a ⟶ (∃x. Q x) ⟹ ∃x. P a ⟶ Q x"
  apply (cut_tac P="P a" in excluded_middle)
  apply (erule disjE)
   apply (rule exI)
   apply (rule impI)
   apply (erule notE, assumption)
  apply (drule mp, assumption)
  apply (erule exE)
  apply (rule_tac x = "x" in exI)
  apply (rule impI, assumption)
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 11. Demostrar
       (∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_11a: 
  "(∃x. P x) ⟶ Q a ⟹ ∀x. P x ⟶ Q a"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_11b: 
  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" ..
    with assms show "Q a" ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_11c: 
  assumes "(∃x. P x) ⟶ Q a"
  shows   "∀x. P x ⟶ Q a"
proof (rule allI)
  fix b
  show "P b ⟶ Q a"
  proof (rule impI)
    assume "P b"
    hence "∃x. P x" by (rule exI)
    with assms show "Q a" by (rule mp)
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_11d: "⟦(∃x. P x) ⟶ Q a ⟧ ⟹ ∀x. P x ⟶ Q a" 
   apply (rule allI)
  apply (rule impI)
  apply (erule mp)
  apply (rule exI)
  apply assumption+
  done

text ‹--------------------------------------------------------------- 
  Ejercicio 12. Demostrar
       ∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_12a: 
  "∀x. P x ⟶ Q a ⟹ ∃x. P x ⟶ Q a"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_12b: 
  assumes "∀x. P x ⟶ Q a"
  shows   "∃x. P x ⟶ Q a"
proof -
  have "P b ⟶ Q a" using assms ..
  thus "∃x. P x ⟶ Q a" ..
qed

― ‹La demostración detallada es›
lemma ejercicio_12c: 
  assumes "∀x. P x ⟶ Q a"
  shows   "∃x. P x ⟶ Q a"
proof -
  have "P b ⟶ Q a" using assms by (rule allE)
  thus "∃x. P x ⟶ Q a" by (rule exI)
qed

― ‹La demostración aplicativa es›
lemma ejercicio_12d: "⟦∀x. P x ⟶ Q a ⟧ ⟹ ∃x. P x ⟶ Q a" 
  apply (erule allE)
  apply (rule exI)  
   apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 13. Demostrar
       (∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_13a: 
  "(∀x. P x) ∨ (∀x. Q x) ⟹ ∀x. P x ∨ Q x"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_13b: 
  assumes "(∀x. P x) ∨ (∀x. Q x)"
  shows   "∀x. P x ∨ Q x"
proof
  fix a
  note assms
  thus "P a ∨ Q a"
  proof
    assume "∀x. P x"
    hence "P a" ..
    thus "P a ∨ Q a" ..
  next
    assume "∀x. Q x"
    hence "Q a" ..
    thus "P a ∨ Q a" ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_13c: 
  assumes "(∀x. P x) ∨ (∀x. Q x)"
  shows   "∀x. P x ∨ Q x"
proof (rule  allI)
  fix a
  note assms
  thus "P a ∨ Q a"
  proof (rule disjE)
    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

― ‹La demostración aplicativa es›
lemma ejercicio_13d: "⟦(∀x. P x) ∨ (∀x. Q x) ⟧ ⟹ ∀x. P x ∨ Q x" 
  apply (rule allI)
  apply (rule disjE)
    apply assumption+
  apply (rule disjI1)
  apply (rule allE)
    apply assumption+
  apply (rule disjI2)
   apply (rule allE)
   apply assumption+
 done

text ‹--------------------------------------------------------------- 
  Ejercicio 14. Demostrar
       ∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_14a: 
  "∃x. P x ∧ Q x ⟹ (∃x. P x) ∧ (∃x. Q x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_14b: 
  assumes "∃x. P x ∧ Q x"
  shows   "(∃x. P x) ∧ (∃x. Q x)"
proof
  obtain a where "P a ∧ Q a" using assms ..
  hence "P a" ..
  thus "∃x. P x" ..
next
  obtain a where "P a ∧ Q a" using assms ..
  hence "Q a" ..
  thus "∃x. Q x" ..
qed

― ‹La demostración detallada es›
lemma ejercicio_14c: 
  assumes "∃x. P x ∧ Q x"
  shows   "(∃x. P x) ∧ (∃x. Q x)"
proof (rule conjI)
  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)
next
  obtain a where "P a ∧ Q a" using assms by (rule exE)
  hence "Q a" by (rule conjunct2)
  thus "∃x. Q x" by (rule exI)
qed

― ‹La demostración aplicativa es›
lemma ejercicio_14e: 
  "⟦∃x. P x ∧ Q x⟧ ⟹ (∃x. P x) ∧ (∃x. Q x)"
  apply (rule conjI)
    apply (erule exE)
    apply (rule exI)
    apply (rule conjunct1)
      apply assumption+
    apply (erule exE)
    apply (rule exI)
    apply (rule conjunct2)
      apply assumption+
 done


text ‹--------------------------------------------------------------- 
  Ejercicio 15. Demostrar
       ∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_15a: 
  "∀x y. P y ⟶ Q x ⟹ (∃y. P y) ⟶ (∀x. Q x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_15b: 
  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" ..
  show "∀x. Q x"
  proof
    fix a
    have "∀y. P y ⟶ Q a" using assms ..
    hence "P b ⟶ Q a" ..
    thus "Q a" using ‹P b› ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_15c: 
  assumes "∀x y. P y ⟶ Q x"
  shows   "(∃y. P y) ⟶ (∀x. Q x)"
proof (rule impI)
  assume "∃y. P y"
  then obtain b where "P b" by (rule exE)
  show "∀x. Q x"
  proof (rule allI)
    fix a
    have "∀y. P y ⟶ Q a" using assms by (rule allE)
    hence "P b ⟶ Q a" by (rule allE)
    thus "Q a" using ‹P b› by (rule mp)
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_15d: 
  "⟦∀x y. P y ⟶ Q x⟧⟹(∃y. P y) ⟶ (∀x. Q x)"
  apply (rule impI)
  apply (rule allI)
  apply (rule exE)
   apply assumption+
  apply (erule allE)
  apply (rule allE)
 apply assumption+
   apply (rule mp)
    apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 16. Demostrar
       ¬(∀x. ¬(P x)) ⊢ ∃x. P x
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_16a: 
  "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_16b: 
  assumes "¬(∀x. ¬(P x))"
  shows   "∃x. P x"
proof (rule ccontr)
  assume "¬(∃x. P x)"
  have "∀x. ¬(P x)"
  proof
    fix a
    show "¬(P a)"
    proof
      assume "P a"
      hence "∃x. P x" ..
      with ‹¬(∃x. P x)› show False ..
    qed
  qed
  with assms show False ..
qed

― ‹La demostración detallada es›
lemma ejercicio_16c: 
  assumes "¬(∀x. ¬(P x))"
  shows   "∃x. P x"
proof (rule ccontr)
  assume "¬(∃x. P x)"
  have "∀x. ¬(P x)"
  proof (rule allI)
    fix a
    show "¬(P a)"
    proof
      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

― ‹La demostración aplicativa es›
lemma ejercicio_16d: 
  "⟦¬(∀x. ¬(P x))⟧ ⟹ ∃x. P x"
  apply (rule notnotD)
  apply (rule notI)
  apply (erule notE)
  apply (rule allI)
  apply (rule notI)
  apply (erule notE)
  apply (rule exI)
  apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 17. Demostrar
       ∀x. ¬(P x) ⊢ ¬(∃x. P x)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_17a: 
  "∀x. ¬(P x) ⟹ ¬(∃x. P x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_17b: 
  assumes "∀x. ¬(P x)"
  shows   "¬(∃x. P x)"
proof
  assume "∃x. P x"
  then obtain a where "P a" ..
  have "¬(P a)" using assms ..
  thus False using ‹P a› ..
qed

― ‹La demostración detallada es›
lemma ejercicio_17c: 
  assumes "∀x. ¬(P x)"
  shows   "¬(∃x. P x)"
proof (rule notI)
  assume "∃x. P x"
  then obtain a where "P a" by (rule exE)
  have "¬(P a)" using assms by (rule allE)
  thus False using ‹P a› by (rule notE)
qed

― ‹La demostración aplicativa es›
lemma ejercicio_17d: 
  "⟦∀x. ¬(P x)⟧ ⟹ ¬(∃x. P x)"
  apply (rule notI)
  apply (erule exE)
  apply (rule notE)
  apply (rule allE)
    apply assumption+ 
  done

text ‹--------------------------------------------------------------- 
  Ejercicio 18. Demostrar
       ∃x. P x ⊢ ¬(∀x. ¬(P x))
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_18a: 
  "∃x. P x ⟹ ¬(∀x. ¬(P x))"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_18b: 
  assumes "∃x. P x"
  shows   "¬(∀x. ¬(P x))"
proof
  assume "∀x. ¬(P x)"
  obtain a where "P a" using assms ..
  have "¬(P a)" using ‹∀x. ¬(P x)› ..
  thus False using ‹P a› ..
qed

― ‹La demostración detallada es›
lemma ejercicio_18c: 
  assumes "∃x. P x"
  shows   "¬(∀x. ¬(P x))"
proof (rule notI)
  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

― ‹La demostración aplicativa es›
lemma ejercicio_18d:
"∃x. P x ⟹ ¬(∀x. ¬(P x))"
  apply (rule notI)
  apply (erule exE)+
   apply (erule allE)+
  apply (rule notE)
  apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 19. Demostrar
       P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_19a:
  "P a ⟶ (∀x. Q x) ⟹ ∀x. P a ⟶ Q x"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_19b: 
  assumes "P a ⟶ (∀x. Q x)"
  shows   "∀x. P a ⟶ Q x"
proof
  fix b
  show "P a ⟶ Q b"
  proof
    assume "P a"
    with assms have "∀x. Q x" ..
    thus "Q b" ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_19c: 
  assumes "P a ⟶ (∀x. Q x)"
  shows   "∀x. P a ⟶ Q x"
proof (rule allI)
  fix b
  show "P a ⟶ Q b"
  proof (rule impI)
    assume "P a"
    with assms have "∀x. Q x" by (rule mp)
    thus "Q b" by (rule allE)
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_19d:
"P a ⟶ (∀x. Q x) ⟹ ∀x. P a ⟶ Q x"
  apply (rule allI)
  apply (rule impI)
  apply (rule allE)
  apply (rule mp)
    apply assumption+
  done


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

― ‹La demostración automática es›
lemma ejercicio_20a: 
  "⟦∀x y z. R x y ∧ R y z ⟶ R x z; ∀x. ¬(R x x)⟧ ⟹ ∀x y. R x y ⟶ ¬(R y x)"
by metis

― ‹La demostración estructurada es›
lemma ejercicio_20b: 
  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 "R a b"
    show "¬(R b a)"
    proof 
      assume "R b a"
      show False
      proof -
        have "R a b ∧ R b a" using ‹R a b› ‹R b a› ..
        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 "R a b ∧ R b a ⟶ R a a" ..
        hence "R a a" using ‹R a b ∧ R b a› ..
        have "¬(R a a)" using assms(2) ..
        thus False using ‹R a a› ..
      qed
    qed
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_20c: 
  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 (rule impI)
    assume "R a b"
    show "¬(R b a)"
    proof (rule notI)
      assume "R b a"
      show False
      proof -
        have "R a b ∧ R b a" using ‹R a b› ‹R b a› by (rule conjI)
        have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
        hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
        hence "R a b ∧ R b a ⟶ R a a" by (rule allE)
        hence "R a a" using ‹R a b ∧ R b a› by (rule mp)
        have "¬(R a a)" using assms(2) by (rule allE)
        thus False using ‹R a a› by (rule notE)
      qed
    qed
  qed
qed


― ‹La demostración aplicativa es›
lemma ejercicio_20d: 
  "⟦∀x y z. R x y ∧ R y z ⟶ R x z; ∀x. ¬(R x x)⟧ ⟹
     ∀x y. R x y ⟶ ¬(R y x)"
  apply (rule allI)+
  apply (rule impI)
  apply (erule_tac x = "x" in allE)
  apply (erule_tac x = "x" in allE)
  apply (erule_tac x = "y" in allE)
   apply (erule_tac x = "x" in allE)
  apply (rule notI)
  apply (drule mp)
   apply (rule conjI, assumption+)
  apply (erule notE, assumption)
  done

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

― ‹La demostración automática es›
lemma ejercicio_21a:
  "⟦∀x. P x ∨ Q x; ∃x. ¬(Q x); ∀x. R x ⟶ ¬(P x)⟧ ⟹ ∃x. ¬(R x)" 
by auto

― ‹La demostración estructurada es›
lemma ejercicio_21b:
  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) ..
  have "P a ∨ Q a" using assms(1) ..
  hence "P a"
  proof
    assume "P a"
    thus "P a" .
  next
    assume "Q a"
    with ‹¬(Q a)› show "P a" ..
  qed
  hence "¬¬(P a)" by (rule notnotI)
  have "R a ⟶ ¬(P a)" using assms(3) ..
  hence "¬(R a)" using ‹¬¬(P a)› by (rule mt)
  thus "∃x. ¬(R x)" ..
qed

― ‹La demostración detallada es›
lemma ejercicio_21c:
  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)
  hence "P a"
  proof (rule disjE)
    assume "P a"
    thus "P a" by this
  next
    assume "Q a"
    with ‹¬(Q a)› show "P a" by (rule notE)
  qed
  hence "¬¬(P a)" by (rule notnotI)
  have "R a ⟶ ¬(P a)" using assms(3) by (rule allE)
  hence "¬(R a)" using ‹¬¬(P a)› by (rule mt)
  thus "∃x. ¬(R x)" by (rule exI)
qed

― ‹La demostración aplicativa es›
lemma ejercicio_21d:
  "⟦∀x. P x ∨ Q x;∃x. ¬(Q x);∀x. R x ⟶ ¬(P x)⟧ ⟹
                               ∃x. ¬(R x)" 
  apply (erule exE)
  apply (rule_tac x = "x" in exI)
  apply (rule notI)
  apply (erule_tac x = "x" in allE)
  apply (erule disjE)
   apply (erule_tac x = "x" in allE)
   apply (drule mp, assumption)
  apply (erule_tac P = "P x" in notE, assumption)
  apply (erule_tac P = "Q x" in notE, assumption)
  done

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

― ‹La demostración automática es›
lemma ejercicio_22a:
  "⟦∀x. P x ⟶ Q x ∨ R x; ¬(∃x. P x ∧ R x)⟧ ⟹ ∀x. P x ⟶ Q x"
by auto 

― ‹La demostración estructurada es›
lemma ejercicio_22b:
  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 "P a"
    have "P a ⟶ Q a ∨ R a" using assms(1) ..
    hence "Q a ∨ R a" using ‹P a› ..
    thus "Q a"
    proof
      assume "Q a"
      thus "Q a" .
    next
      assume "R a"
      with ‹P a› have "P a ∧ R a" ..
      hence "∃x. P x ∧ R x" ..
      with assms(2) show "Q a" ..
    qed
  qed 
qed

― ‹La demostración detallada es›
lemma ejercicio_22c:
  assumes "∀x. P x ⟶ Q x ∨ R x" 
          "¬(∃x. P x ∧ R x)"
  shows   "∀x. P x ⟶ Q x"
proof (rule allI)
  fix a
  show "P a ⟶ Q a"
  proof (rule impI)
    assume "P a"
    have "P a ⟶ Q a ∨ R a" using assms(1) by (rule allE)
    hence "Q a ∨ R a" using ‹P a› by (rule mp)
    thus "Q a"
    proof (rule disjE)
      assume "Q a"
      thus "Q a" by this
    next
      assume "R a"
      with ‹P a› have "P a ∧ R a" by (rule conjI)
      hence "∃x. P x ∧ R x" by (rule exI)
      with assms(2) show "Q a" by (rule notE)
    qed
  qed 
qed

― ‹La demostración aplicativa es›
lemma ejercicio_22d:
 "⟦∀x. P x ⟶ Q x ∨ R x;¬(∃x. P x ∧ R x)⟧ ⟹ ∀x. P x ⟶ Q x"
    apply (rule allI)
    apply (rule impI)
    apply (rule disjE)
    apply (erule allE)
    apply (rule mp)
    apply assumption+
    apply (rule notE)
    apply assumption+
    apply (rule exI)
    apply (erule conjI)
    apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     ∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_23a:
  "∃x y. R x y ∨ R y x ⟹ ∃x y. R x y"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_23b:
  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 ..
  then obtain b where "R a b ∨ R b a" ..
  thus "∃x y. R x y"
  proof
    assume "R a b"
    hence "∃y. R a y" ..
    thus "∃ x y. R x y" ..
  next
    assume "R b a"
    hence "∃y. R b y" ..
    thus "∃ x y. R x y" ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_23c:
  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 "R a b ∨ R b a" by (rule exE)
  thus "∃x y. R x y"
  proof (rule disjE)
    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

― ‹La demostración aplicativa es›
lemma ejercicio_23d:
  "⟦∃x y. R x y ∨ R y x⟧ ⟹ ∃x y. R x y"
  apply (erule exE)+
  apply (erule disjE)
  apply (rule exI)
  apply (rule exI)
  apply assumption+
  apply (rule exI)
  apply (rule exI)
  apply assumption+
  done 

text ‹--------------------------------------------------------------- 
  Ejercicio 24. Demostrar
       (∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_24a: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_24b: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof 
  assume "∃x. ∀y. P x y"
  then obtain a where "∀y. P a y" ..
  show "∀y. ∃x. P x y"
  proof
    fix b
    have "P a b" using ‹∀y. P a y› ..
    thus "∃x. P x b" ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_24c: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof (rule impI)
  assume "∃x. ∀y. P x y"
  then obtain a where "∀y. P a y" by (rule exE)
  show "∀y. ∃x. P x y"
  proof (rule allI)
    fix b
    have "P a b" using ‹∀y. P a y› by (rule allE)
    thus "∃x. P x b" by (rule exI)
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_24d: 
  "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
  apply (rule impI)
  apply (rule allI)
  apply (erule exE)
  apply (erule allE)
  apply (rule exI)
  apply assumption+
  done

text ‹--------------------------------------------------------------- 
  Ejercicio 25. Demostrar
       (∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_25a: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_25b: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
proof
  assume "∀x. P x ⟶ Q"
  show "(∃x. P x) ⟶ Q"
  proof
    assume "∃x. P x"
    then obtain a where "P a" ..
    have "P a ⟶ Q" using ‹∀x. P x ⟶ Q› ..
    thus "Q" using ‹P a› ..
  qed
next
  assume "(∃x. P x) ⟶ Q"
  show "∀x. P x ⟶ Q"
  proof
    fix b
    show "P b ⟶ Q"
    proof
      assume "P b"
      hence "∃x. P x" ..
      with ‹(∃x. P x) ⟶ Q› show "Q" ..
    qed
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_25c: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
proof (rule iffI)
  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 (rule allI)
    fix b
    show "P b ⟶ Q"
    proof (rule impI)
      assume "P b"
      hence "∃x. P x" by (rule exI)
      with ‹(∃x. P x) ⟶ Q› show "Q" by (rule mp)
    qed
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_25d: 
  "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
  apply (rule iffI)
  prefer 2
   apply (rule allI)
   apply (rule impI)
   apply (rule mp)
   apply assumption+
   apply (rule exI)
   apply assumption+
  apply (rule impI)
  apply (erule exE)
   apply (erule allE)
    apply (rule mp)
     apply assumption+
  done


text ‹--------------------------------------------------------------- 
  Ejercicio 26. Demostrar
       ((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_26a: "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_26b: "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof
  assume "(∀x. P x) ∧ (∀x. Q x)"
  show "∀x. P x ∧ Q x"
  proof
    fix a
    have "∀x. P x" using ‹(∀x. P x) ∧ (∀x. Q x)› ..
    have "∀x. Q x" using ‹(∀x. P x) ∧ (∀x. Q x)› ..
    hence "Q a" .. 
    have "P a" using ‹∀x. P x› ..
    thus "P a ∧ Q a" using ‹Q a› ..
  qed
next
  assume "∀x. P x ∧ Q x"
  have "∀x. P x"
  proof
    fix a
    have "P a ∧ Q a" using ‹∀x. P x ∧ Q x› .. 
    thus "P a" ..
  qed
  moreover have "∀x. Q x"
  proof
    fix a
    have "P a ∧ Q a" using ‹∀x. P x ∧ Q x› .. 
    thus "Q a" ..
  qed
  ultimately show "(∀x. P x) ∧ (∀x. Q x)" ..
qed

― ‹La demostración detallada es›
lemma ejercicio_26c: "((∀x. P x) ∧ (∀x. Q x)) = (∀x. P x ∧ Q x)"
proof (rule iffI)
  assume "(∀x. P x) ∧ (∀x. Q x)"
  show "∀x. P x ∧ Q x"
  proof (rule allI)
    fix a
    have "∀x. P x" using ‹(∀x. P x) ∧ (∀x. Q x)› by (rule conjunct1)
    have "∀x. Q x" using ‹(∀x. P x) ∧ (∀x. Q x)› by (rule conjunct2)
    hence "Q a" by (rule allE)
    have "P a" using ‹∀x. P x› by (rule allE)
    thus "P a ∧ Q a" using ‹Q a› by (rule conjI)
  qed
next
  assume "∀x. P x ∧ Q x"
  have "∀x. P x"
  proof (rule allI)
    fix a
    have "P a ∧ Q a" using ‹∀x. P x ∧ Q x› by (rule allE) 
    thus "P a" by (rule conjunct1)
  qed
  moreover have "∀x. Q x"
  proof (rule allI)
    fix a
    have "P a ∧ Q a" using ‹∀x. P x ∧ Q x› by (rule allE) 
    thus "Q a" by (rule conjunct2)
  qed
  ultimately show "(∀x. P x) ∧ (∀x. Q x)" by (rule conjI)
qed

― ‹La demostración aplicativa es›
lemma ejercicio_26d: 
  "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
    apply (rule iffI)
     prefer 2 
     apply (rule conjI)
     apply (rule allI)
     apply (erule allE)
     apply (erule conjunct1)
     apply (rule allI)
     apply (erule allE)
     apply (erule conjunct2)
    apply (rule allI)
    apply (frule conjunct1)
    apply (frule conjunct2)
    apply (erule allE)+
    apply (rule conjI)
    apply assumption+
  done

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

(*
Auto Quickcheck found a counterexample:
P = {a⇩1}
Q = {a⇩2}
*)

text ‹--------------------------------------------------------------- 
  Ejercicio 28. Demostrar o refutar
       ((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_28a: 
  "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_28b: 
  "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
proof
  assume "(∃x. P x) ∨ (∃x. Q x)"
  thus "∃x. P x ∨ Q x"
  proof
    assume "∃x. P x"
    then obtain a where "P a" ..
    hence "P a ∨ Q a" ..
    thus "∃x. P x ∨ Q x" ..
  next
    assume "∃x. Q x"
    then obtain a where "Q a" ..
    hence "P a ∨ Q a" ..
    thus "∃x. P x ∨ Q x" ..
  qed
next
  assume "∃x. P x ∨ Q x"
  then obtain a where "P a ∨ Q a" ..
  thus "(∃x. P x) ∨ (∃x. Q x)"
  proof
    assume "P a"
    hence "∃x. P x" ..
    thus "(∃x. P x) ∨ (∃x. Q x)" ..
  next
    assume "Q a"
    hence "∃x. Q x" ..
    thus "(∃x. P x) ∨ (∃x. Q x)" ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_28c: 
  "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
proof (rule iffI)
  assume "(∃x. P x) ∨ (∃x. Q x)"
  thus "∃x. P x ∨ Q x"
  proof (rule disjE)
    assume "∃x. P x"
    then obtain a where "P a" by (rule exE)
    hence "P a ∨ Q a" by (rule disjI1)
    thus "∃x. P x ∨ Q x" by (rule exI)
  next
    assume "∃x. Q x"
    then obtain a where "Q a" by (rule exE)
    hence "P a ∨ Q a" by (rule disjI2)
    thus "∃x. P x ∨ Q x" by (rule exI)
  qed
next
  assume "∃x. P x ∨ Q x"
  then obtain a where "P a ∨ Q a" by (rule exE)
  thus "(∃x. P x) ∨ (∃x. Q x)"
  proof (rule disjE)
    assume "P a"
    hence "∃x. P x" by (rule exI)
    thus "(∃x. P x) ∨ (∃x. Q x)" by (rule disjI1)
  next
    assume "Q a"
    hence "∃x. Q x" by (rule exI)
    thus "(∃x. P x) ∨ (∃x. Q x)" by (rule disjI2)
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_28d: 
  "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
      apply (rule iffI)
      apply (erule disjE)
      apply (erule exE)
      apply (drule disjI1)
      apply (rule exI)
      apply assumption+
      apply (erule exE)
      apply (drule disjI2)
      apply (rule exI)
      apply assumption+
      apply (erule exE)
      apply (erule disjE)
      apply (rule disjI1)
      apply (rule exI)
      apply assumption+
      apply (rule disjI2)
      apply (rule exI)
      apply assumption+
  done


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
(*
Quickcheck found a counterexample:

P = (λx. undefined)((a⇩1 := {a⇩2}, a⇩2 := {a⇩1})
*)
oops

text ‹--------------------------------------------------------------- 
  Ejercicio 30. Demostrar o refutar
       (¬(∀x. P x)) ⟷ (∃x. ¬P x)
  ------------------------------------------------------------------›

― ‹La demostración automática es›
lemma ejercicio_30a: 
  "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
by auto

― ‹La demostración estructurada es›
lemma ejercicio_30b: 
  "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
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" ..
        with ‹¬(∃x. ¬P x)› show False ..
      qed
    qed
    with ‹¬(∀x. P x)› show False ..
  qed
next
  assume "∃x. ¬P x"
  then obtain a where "¬P a" ..
  show "¬(∀x. P x)"
  proof
    assume "∀x. P x"
    hence "P a" ..
    with ‹¬P a› show False ..
  qed
qed

― ‹La demostración detallada es›
lemma ejercicio_30c: 
  "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof (rule iffI)
  assume "¬(∀x. P x)"
  show "∃x. ¬P x"
  proof (rule ccontr)
    assume "¬(∃x. ¬P x)"
    have "∀x. P x"
    proof (rule allI)
      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"
  then obtain a where "¬P a" by (rule exE)
  show "¬(∀x. P x)"
  proof (rule notI)
    assume "∀x. P x"
    hence "P a" by (rule allE)
    show False using ‹¬P a› ‹P a› by (rule notE)
  qed
qed

― ‹La demostración aplicativa es›
lemma ejercicio_30d: 
  "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
  apply (rule iffI)
    apply (rule notnotD)
    apply (rule notI)
    apply (erule notE)
    apply (rule allI)
    apply (rule notnotD)
    apply (rule notI)
    apply (erule notE)
    apply (rule exI)
    apply assumption+
    apply (erule exE)
    apply (rule notI)
    apply (erule allE)
    apply (erule notE)
    apply assumption+ 
done


end



</source>