Tema 4a

chapter ‹Tema 4a: Deducción natural en lógica de primer orden›

theory T4a_Deduccion_natural_en_logica_de_primer_orden
imports Main 
begin

text ‹El objetivo de este tema es presentar la deducción natural en 
  lógica de primer orden con Isabelle/HOL. La presentación se 
  basa en los ejemplos de tema 4 del curso LMF que se encuentra 
  en http://goo.gl/uJj8d (que a su vez se basa en el libro de 
  Huth y Ryan "Logic in Computer Science" http://goo.gl/qsVpY ). 

  La página al lado de cada ejemplo indica la página de las 
  transparencias de LMF donde se encuentra la demostración.›

section ‹Reglas del cuantificador universal›

text ‹Las reglas del cuantificador universal son
  · allE:    ⟦∀x. P x; P a ⟹ R⟧ ⟹ R
  · allI:    (⋀x. P x) ⟹ ∀x. P x
›

subsection ‹Ejemplo 1›

text ‹Ejemplo 1 (p. 10). Demostrar que
     P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c)
›

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
lemma ejemplo_1a: 
  assumes 1: "P(c)" and
          2: "∀x. (P(x) ⟶ ¬Q(x))"
  shows "¬Q(c)"
proof -
  have 3: "P(c) ⟶ ¬Q(c)" using 2 by (rule allE)
  show 4: "¬Q(c)" using 3 1 by (rule mp)
qed

subsubsection ‹Demostración estructurada›

― ‹La demostración estructurada es›
lemma ejemplo_1b: 
  assumes "P(c)"
          "∀x. (P(x) ⟶ ¬Q(x))"
  shows "¬Q(c)"
proof -
  have "P(c) ⟶ ¬Q(c)" using assms(2) ..
  then show "¬Q(c)" using assms(1) ..
qed

subsubsection ‹Demostración automática›

― ‹La demostración automática es›
lemma ejemplo_1c: 
  assumes "P(c)"
          "∀x. (P(x) ⟶ ¬Q(x))"
  shows "¬Q(c)"
  using assms
  by auto

subsubsection ‹Demostración aplicativa›

lemma ejemplo_1d: 
  "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
  apply (erule allE) (* da ⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c *)
  apply (erule mp)   (* da P c ⟹ P c *)
  apply assumption   (* da No subgoals! *)
  done
    
text ‹Explicaciones
  apply (erule allE) 
  + Objetivo:       "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
  + allE:           "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
  + Unificador de   ("¬Q(c)", "∀x. (P(x) ⟶ ¬Q(x))") y
                    ("?R",    "∀x. ?P x")
    es              ?R / ¬Q(c)
                    ?P x / P(x) ⟶ ¬Q(x) 
  + Nuevo objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c"

  apply (erule mp)   
  + Objetivo:       "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c"
  + mp:             "⟦?P ⟶ ?Q; ?P⟧ ⟹ ?Q"
  + Unificador de   ("¬ Q c", "P ?x ⟶ ¬ Q ?x") y
                    ("?Q",    "?P ⟶ ?Q")
    es              ?Q / ¬ Q c
                    ?P / P c
  + Nuevo objetivo: "P c ⟹ P c" 
›

subsection ‹Ejemplo 2›

text ‹Ejemplo 2 (p. 11). Demostrar que
     ∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x)
›

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
lemma ejemplo_2a: 
  assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
          2: "∀x. P x"
  shows "∀x. ¬(Q x)"
proof -
  { fix a
    have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
    have 4: "P a" using 2 by (rule allE)
    have 5: "¬(Q a)" using 3 4 by (rule mp) }
  then show "∀x. ¬(Q x)" by (rule allI)
qed

― ‹La demostración detallada hacia atrás es›
lemma ejemplo_2b: 
  assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
          2: "∀x. P x"
  shows "∀x. ¬(Q x)"
proof (rule allI)
  fix a
  have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
  have 4: "P a" using 2 by (rule allE)
  show 5: "¬(Q a)" using 3 4 by (rule mp) 
qed

subsubsection ‹Demostración estructurada›

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

subsubsection ‹Demostración automática›

― ‹La demostración automática es›
lemma ejemplo_2d: 
  assumes "∀x. (P x ⟶ ¬(Q x))"
          "∀x. P x"
  shows   "∀x. ¬(Q x)"
  using assms
  by auto

subsubsection ‹Demostración aplicativa›

lemma ejemplo_2e: 
  "⟦∀x. (P x ⟶ ¬(Q x)); ∀y. P y⟧ ⟹ ∀z. ¬(Q z)"
  apply (rule allI)   (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z);
                                 P (?y4 z)⟧
                                ⟹ ¬ Q z*)
  apply (erule allE)+ (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z);
                                 P (?y4 z)⟧
                                ⟹ ¬ Q z *)
  apply (erule mp)    (* da ⋀z. P (?y4 z) ⟹ P z *)
  apply assumption    (* da No subgoals! *) 
  done

section ‹Reglas del cuantificador existencial›

text ‹Las reglas del cuantificador existencial son
  · exI:     P a ⟹ ∃x. P x
  · exE:     ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

  En la regla exE la nueva variable se introduce mediante la declaración 
  "obtain ... where ... by (rule exE)" 
›

subsection ‹Ejemplo 3›

text ‹Ejemplo 3 (p. 12). Demostrar que
     ∀x. P x ⊢ ∃x. P x
›

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
lemma ejemplo_3a:
  assumes "∀x. P x"
  shows "∃x. P x"
proof -
  fix a
  have "P a" using assms by (rule allE)
  then show "∃x. P x" by (rule exI)
qed

subsubsection ‹Demostración estructurada›

― ‹La demostración estructurada es›
lemma ejemplo_3b:
  assumes "∀x. P x"
  shows "∃x. P x"
proof -
  fix a
  have "P a" using assms ..
  then show "∃x. P x" ..
qed

― ‹La demostración estructurada se puede simplificar›
lemma ejemplo_3c:
  assumes "∀x. P x"
  shows "∃x. P x"
proof (rule exI)
  fix a
  show "P a" using assms ..
qed

― ‹La demostración estructurada se puede simplificar aún más›
lemma ejemplo_3d:
  assumes "∀x. P x"
  shows "∃x. P x"
proof 
  fix a
  show "P a" using assms ..
qed

subsubsection ‹Demostración automática›

― ‹La demostración automática es›
lemma ejemplo_3e:
  assumes "∀x. P x"
  shows "∃x. P x"
  using assms
  by auto

subsubsection ‹Demostración aplicativa›

lemma ejemplo_3f: 
  "∀x. P x ⟹ ∃y. P y"
  apply (erule allE) (* da P ?x ⟹ ∃y. P y *)
  apply (erule exI)  (* da No subgoals! *)
  done

subsection ‹Ejemplo 4›

text ‹Ejemplo 4 (p. 13). Demostrar
     ∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x
›

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
lemma ejemplo_4a:
  assumes 1: "∀x. (P x ⟶ Q x)" and
          2: "∃x. P x"
  shows "∃x. Q x"
proof -
  obtain a where 3: "P a" using 2 by (rule exE)
  have 4: "P a ⟶ Q a" using 1 by (rule allE)
  have 5: "Q a" using 4 3 by (rule mp)
  then show 6: "∃x. Q x" by (rule exI)
qed

subsubsection ‹Demostración estructurada›

― ‹La demostración estructurada es›
lemma ejemplo_4b:
  assumes "∀x. (P x ⟶ Q x)"
          "∃x. P x"
  shows "∃x. Q x"
proof -
  obtain a where "P a" using assms(2) ..
  have "P a ⟶ Q a" using assms(1) ..
  then have "Q a" using ‹P a› ..
  then show "∃x. Q x" ..
qed

subsubsection ‹Demostración automática›

― ‹La demostración automática es›
lemma ejemplo_4c:
  assumes "∀x. (P x ⟶ Q x)"
          "∃x. P x"
  shows "∃x. Q x"
  using assms
  by auto

subsubsection ‹Demostración aplicativa›

lemma ejemplo_4f: 
  "⟦∀x. P x ⟶ Q x; ∃y. P y⟧ ⟹ ∃z. Q z"
  apply (erule exE)  (* da ⋀y. ⟦∀x. P x ⟶ Q x; P y⟧ ⟹ ∃z. Q z *)
  apply (erule allE) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ ∃z. Q z *)
  apply (rule exI)   (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ Q (?z4 y) *)
  apply (erule mp)   (* da ⋀y. P y ⟹ P (?x2 y) *)
  apply assumption   (* da No subgoals! *)
  done

section ‹Demostración de equivalencias›

subsection ‹Ejemplo 5.1›

text ‹Ejemplo 5.1 (p. 15). Demostrar
     ¬∀x. P x  ⊢ ∃x. ¬(P x)›

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
lemma ejemplo_5_1a:
  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 (rule ccontr)
      assume "¬P(a)"
      then have "∃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

subsubsection ‹Demostración estructurada›

― ‹La demostración estructurada es›
lemma ejemplo_5_1b:
  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 (rule ccontr)
      assume "¬P(a)"
      then have "∃x. ¬P(x)" ..
      with ‹¬(∃x. ¬P(x))› show False ..
    qed
  qed
  with assms show False ..
qed

subsubsection ‹Demostración automática›

― ‹La demostración automática es›
lemma ejemplo_5_1c:
  assumes "¬(∀x. P(x))"
  shows   "∃x. ¬P(x)"
  using assms
  by auto

subsubsection ‹Demostración aplicativa›

lemma ejemplo_5_1d: "¬(∀x. P x) ⟹ ∃y. ¬P y"
  apply (rule ccontr) (* da ⟦¬ (∀x. P x); ∄y. ¬ P y⟧ ⟹ False *)
  apply (erule notE)  (* da ∄y. ¬ P y ⟹ ∀x. P x *)
  apply (rule allI)   (* da ⋀x. ∄y. ¬ P y ⟹ P x *)
  apply (rule ccontr) (* da ⋀x. ⟦∄y. ¬ P y; ¬ P x⟧ ⟹ False *)
  apply (erule notE)  (* da ⋀x. ¬ P x ⟹ ∃y. ¬ P y *)
   apply (erule exI)  (* da No subgoals! *)
  done


text ‹
  Ejemplo 5.2 (p. 16). Demostrar
     ∃x. ¬(P x)  ⊢ ¬∀x. P x›

― ‹La demostración detallada es›
lemma ejemplo_5_2a:
  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)
  with ‹¬P(a)› show False by (rule notE)
qed

― ‹La demostración estructurada es›
lemma ejemplo_5_2b:
  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)› ..
  with ‹¬P(a)› show False ..
qed

― ‹La demostración automática es›
lemma ejemplo_5_2c:
  assumes "∃x. ¬P(x)"
  shows   "¬(∀x. P(x))"
using assms
by auto

text ‹
  Ejemplo 5.3 (p. 17). Demostrar
     ⊢ ¬∀x. P x  ⟷ ∃x. ¬(P x)›

― ‹La demostración detallada es›
lemma ejemplo_5_3a:
  "(¬(∀x. P(x))) ⟷ (∃x. ¬P(x))"
proof (rule iffI)
  assume "¬(∀x. P(x))"
  then show "∃x. ¬P(x)" by (rule ejemplo_5_1a)
next
  assume "∃x. ¬P(x)"
  then show "¬(∀x. P(x))" by (rule ejemplo_5_2a)
qed

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

text ‹
  Ejemplo 6.1 (p. 18). Demostrar
     ∀x. P(x) ∧ Q(x) ⊢  (∀x. P(x)) ∧ (∀x. Q(x))›

― ‹La demostración detallada es›
lemma ejemplo_6_1a:
  assumes "∀x. P(x) ∧ Q(x)"
  shows   "(∀x. P(x)) ∧ (∀x. Q(x))"
proof (rule conjI)
  show "∀x. P(x)"
  proof (rule allI)
    fix a
    have "P(a) ∧ Q(a)" using assms by (rule allE)
    then show "P(a)" by (rule conjunct1)
  qed
next
  show "∀x. Q(x)"
  proof (rule allI)
    fix a
    have "P(a) ∧ Q(a)" using assms by (rule allE)
    then show "Q(a)" by (rule conjunct2)
  qed
qed

― ‹La demostración estructurada es›
lemma ejemplo_6_1b:
  assumes "∀x. P(x) ∧ Q(x)"
  shows   "(∀x. P(x)) ∧ (∀x. Q(x))"
proof 
  show "∀x. P(x)"
  proof 
    fix a
    have "P(a) ∧ Q(a)" using assms ..
    then show "P(a)" ..
  qed
next
  show "∀x. Q(x)"
  proof 
    fix a
    have "P(a) ∧ Q(a)" using assms ..
    then show "Q(a)" ..
  qed
qed

― ‹La demostración automática es›
lemma ejemplo_6_1c:
  assumes "∀x. P(x) ∧ Q(x)"
  shows   "(∀x. P(x)) ∧ (∀x. Q(x))"
using assms
by auto

text ‹
  Ejemplo 6.2 (p. 19). Demostrar
     (∀x. P(x)) ∧ (∀x. Q(x)) ⊢ ∀x. P(x) ∧ Q(x)›

― ‹La demostración detallada es›
lemma ejemplo_6_2a:
  assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
  shows   "∀x. P(x) ∧ Q(x)"
proof (rule allI)
  fix a
  have "∀x. P(x)" using assms by (rule conjunct1)
  then have "P(a)" by (rule allE)
  have "∀x. Q(x)" using assms by (rule conjunct2)
  then have "Q(a)" by (rule allE)
  with ‹P(a)› show "P(a) ∧ Q(a)" by (rule conjI)
qed

― ‹La demostración estructurada es›
lemma ejemplo_6_2b:
  assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
  shows   "∀x. P(x) ∧ Q(x)"
proof
  fix a
  have "∀x. P(x)" using assms ..
  then have "P(a)" by (rule allE)
  have "∀x. Q(x)" using assms ..
  then have "Q(a)" ..
  with ‹P(a)› show "P(a) ∧ Q(a)" ..
qed

― ‹La demostración automática es›
lemma ejemplo_6_2c:
  assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
  shows   "∀x. P(x) ∧ Q(x)"
using assms
by auto

text ‹
  Ejemplo 6.3 (p. 20). Demostrar
     ⊢ ∀x. P(x) ∧ Q(x) ⟷ (∀x. P(x)) ∧ (∀x. Q(x))›

― ‹La demostración detallada es›
lemma ejemplo_6_3a:
  "(∀x. P(x) ∧ Q(x)) ⟷ ((∀x. P(x)) ∧ (∀x. Q(x)))"
proof (rule iffI)
  assume "∀x. P(x) ∧ Q(x)"
  then show "(∀x. P(x)) ∧ (∀x. Q(x))" by (rule ejemplo_6_1a)
next
  assume "(∀x. P(x)) ∧ (∀x. Q(x))"
  then show "∀x. P(x) ∧ Q(x)" by (rule ejemplo_6_2a)
qed

text ‹
  Ejemplo 7.1 (p. 21). Demostrar
     (∃x. P(x)) ∨ (∃x. Q(x)) ⊢ ∃x. P(x) ∨ Q(x)›

― ‹La demostración detallada es›
lemma ejemplo_7_1a:
  assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
  shows   "∃x. P(x) ∨ Q(x)"
using assms
proof (rule disjE)
  assume "∃x. P(x)"
  then obtain a where "P(a)" by (rule exE)
  then have "P(a) ∨ Q(a)" by (rule disjI1)
  then show "∃x. P(x) ∨ Q(x)" by (rule exI)
next
  assume "∃x. Q(x)"
  then obtain a where "Q(a)" by (rule exE)
  then have "P(a) ∨ Q(a)" by (rule disjI2)
  then show "∃x. P(x) ∨ Q(x)" by (rule exI)
qed

― ‹La demostración estructurada es›
lemma ejemplo_7_1b:
  assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
  shows   "∃x. P(x) ∨ Q(x)"
using assms
proof
  assume "∃x. P(x)"
  then obtain a where "P(a)" ..
  then have "P(a) ∨ Q(a)" ..
  then show "∃x. P(x) ∨ Q(x)" ..
next
  assume "∃x. Q(x)"
  then obtain a where "Q(a)" ..
  then have "P(a) ∨ Q(a)" ..
  then show "∃x. P(x) ∨ Q(x)" ..
qed

― ‹La demostración automática es›
lemma ejemplo_7_1c:
  assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
  shows   "∃x. P(x) ∨ Q(x)"
using assms
by auto

text ‹
  Ejemplo 7.2 (p. 22). Demostrar
     ∃x. P(x) ∨ Q(x) ⊢ (∃x. P(x)) ∨ (∃x. Q(x))›

― ‹La demostración detallada es›
lemma ejemplo_7_2a:
  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)
  then show "(∃x. P(x)) ∨ (∃x. Q(x))"
  proof (rule disjE)
    assume "P(a)"
    then have "∃x. P(x)" by (rule exI)
    then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI1)
  next
    assume "Q(a)"
    then have "∃x. Q(x)" by (rule exI)
    then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI2)
  qed
qed

― ‹La demostración estructurada es›
lemma ejercicio_7_2b:
  assumes "∃x. P(x) ∨ Q(x)"
  shows   "(∃x. P(x)) ∨ (∃x. Q(x))"
proof -
  obtain a where "P(a) ∨ Q(a)" using assms ..
  then show "(∃x. P(x)) ∨ (∃x. Q(x))"
  proof 
    assume "P(a)"
    then have "∃x. P(x)" ..
    then show "(∃x. P(x)) ∨ (∃x. Q(x))" ..
  next
    assume "Q(a)"
    then have "∃x. Q(x)" ..
    then show "(∃x. P(x)) ∨ (∃x. Q(x))" ..
  qed
qed

― ‹La demostración automática es›
lemma ejercicio_7_2c:
  assumes "∃x. P(x) ∨ Q(x)"
  shows   "(∃x. P(x)) ∨ (∃x. Q(x))"
using assms
by auto

text ‹
  Ejemplo 7.3 (p. 23). Demostrar
     ⊢ ((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))›

― ‹La demostración detallada es›
lemma ejemplo_7_3a:
  "((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))"
proof (rule iffI)
  assume "(∃x. P(x)) ∨ (∃x. Q(x))"
  then show "∃x. P(x) ∨ Q(x)" by (rule ejemplo_7_1a)
next
  assume "∃x. P(x) ∨ Q(x)"
  then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule ejemplo_7_2a)
qed

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

text ‹
  Ejemplo 8.1 (p. 24). Demostrar
     ∃x y. P(x,y) ⊢ ∃y x. P(x,y)›

― ‹La demostración detallada es›
lemma ejemplo_8_1a:
  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)
  then obtain b where "P(a,b)" by (rule exE)
  then have "∃x. P(x,b)" by (rule exI)
  then show "∃y x. P(x,y)" by (rule exI)
qed

― ‹La demostración estructurada es›
lemma ejemplo_8_1b:
  assumes "∃x y. P(x,y)"
  shows   "∃y x. P(x,y)"
proof -
  obtain a where "∃y. P(a,y)" using assms ..
  then obtain b where "P(a,b)" ..
  then have "∃x. P(x,b)" ..
  then show "∃y x. P(x,y)" ..
qed

― ‹La demostración automática es›
lemma ejemplo_8_1c:
  assumes "∃x y. P(x,y)"
  shows   "∃y x. P(x,y)"
using assms
by auto

text ‹
  Ejemplo 8.2. Demostrar
     ∃y x. P(x,y) ⊢ ∃x y. P(x,y)›

― ‹La demostración detallada es›
lemma ejemplo_8_2a:
  assumes "∃y x. P(x,y)"
  shows   "∃x y. P(x,y)"
proof -
  obtain b where "∃x. P(x,b)" using assms by (rule exE)
  then obtain a where "P(a,b)" by (rule exE)
  then have "∃y. P(a,y)" by (rule exI)
  then show "∃x y. P(x,y)" by (rule exI)
qed

― ‹La demostración estructurada es›
lemma ejemplo_8_2b:
  assumes "∃y x. P(x,y)"
  shows   "∃x y. P(x,y)"
proof -
  obtain b where "∃x. P(x,b)" using assms ..
  then obtain a where "P(a,b)" ..
  then have "∃y. P(a,y)" ..
  then show "∃x y. P(x,y)" ..
qed

― ‹La demostración estructurada es›
lemma ejemplo_8_2c:
  assumes "∃y x. P(x,y)"
  shows   "∃x y. P(x,y)"
using assms
by auto

text ‹
  Ejemplo 8.3 (p. 25). Demostrar
     ⊢ (∃x y. P(x,y)) ⟷ (∃y x. P(x,y))›

― ‹La demostración detallada es›
lemma ejemplo_8_3a:
  "(∃x y. P(x,y)) ⟷ (∃y x. P(x,y))"
proof (rule iffI)
  assume "∃x y. P(x,y)"
  then show "∃y x. P(x,y)" by (rule ejemplo_8_1a)
next
  assume "∃y x. P(x,y)"
  then show "∃x y. P(x,y)" by (rule ejemplo_8_2a)
qed

― ‹La demostración automática es›
lemma ejemplo_8_3b:
  "(∃x y. P(x,y)) ⟷ (∃y x. P(x,y))"
by auto

section ‹Reglas de la igualdad›

text ‹
  Las reglas básicas de la igualdad son:
  · refl:  t = t
  · subst: ⟦s = t; P s⟧ ⟹ P t
›

text ‹
  Ejemplo 9 (p. 27). Demostrar
     x + 1 = 1 + x, x + 1 > 1 ⟶ x + 1 > 0 ⊢ 1 + x > 1 ⟶ 1 + x > 0
›

― ‹La demostración detallada es›
lemma ejemplo_9a: 
  assumes "x + 1 = 1 + x" 
          "x + 1 > 1 ⟶ x + 1 > 0"
  shows   "1 + x > 1 ⟶ 1 + x > 0"
proof -
  show "1 + x > 1 ⟶ 1 + x > 0" using assms by (rule subst)
qed

― ‹La demostración estructurada es›
lemma ejemplo_9b: 
  assumes "x + 1 = 1 + x" 
          "x + 1 > 1 ⟶ x + 1 > 0"
  shows   "1 + x > 1 ⟶ 1 + x > 0"
using assms 
by (rule subst)

― ‹La demostración automática es›
lemma ejemplo_9c: 
  assumes "x + 1 = 1 + x" 
          "x + 1 > 1 ⟶ x + 1 > 0"
  shows   "1 + x > 1 ⟶ 1 + x > 0"
using assms 
by auto

text ‹
  Ejemplo 10 (p. 27). Demostrar
     x = y, y = z ⊢ x = z
›

― ‹La demostración detallada es›
lemma ejemplo_10a:
  assumes "x = y" 
          "y = z"
  shows   "x = z"
proof -
  show "x = z" using assms(2,1) by (rule subst)
qed

― ‹La demostración estructurada es›
lemma ejemplo_10b: 
  assumes "x = y" 
          "y = z"
  shows   "x = z"
using assms(2,1)
by (rule subst)

― ‹La demostración automática es›
lemma ejemplo_10c: 
  assumes "x = y" 
          "y = z"
  shows   "x = z"
using assms
by auto

text ‹
  Ejemplo 11 (p. 28). Demostrar
     s = t ⊢ t = s
›

― ‹La demostración detallada es›
lemma ejemplo_11a:
  assumes "s = t"
  shows   "t = s"
proof -
  have "s = s" by (rule refl)
  with assms show "t = s" by (rule subst)
qed

― ‹La demostración automática es›
lemma ejemplo_11b:
  assumes "s = t"
  shows   "t = s"
using assms
by auto

end