Acciones

Diferencia entre revisiones de «Tema 4a»

De Lógica matemática y fundamentos (2018-19)

m
 
Línea 1: Línea 1:
 
<source lang="isabelle">
 
<source lang="isabelle">
chapter {* Tema 4a: Deducción natural en lógica de primer orden *}
+
chapter ‹Tema 4a: Deducción natural en lógica de primer orden›
  
 
theory T4a_Deduccion_natural_en_logica_de_primer_orden
 
theory T4a_Deduccion_natural_en_logica_de_primer_orden
Línea 6: Línea 6:
 
begin
 
begin
  
text {*
+
text ‹El objetivo de este tema es presentar la deducción natural en  
  El objetivo de este tema es presentar la deducción natural en  
 
 
   lógica de primer orden con Isabelle/HOL. La presentación se  
 
   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  
 
   basa en los ejemplos de tema 4 del curso LMF que se encuentra  
Línea 14: Línea 13:
  
 
   La página al lado de cada ejemplo indica la página de las  
 
   La página al lado de cada ejemplo indica la página de las  
   transparencias de LMF donde se encuentra la demostración. *}
+
   transparencias de LMF donde se encuentra la demostración.
  
section {* Reglas del cuantificador universal *}
+
section ‹Reglas del cuantificador universal›
  
text {*
+
text ‹Las reglas del cuantificador universal son
  Las reglas del cuantificador universal son
 
 
   · allE:    ⟦∀x. P x; P a ⟹ R⟧ ⟹ R
 
   · allE:    ⟦∀x. P x; P a ⟹ R⟧ ⟹ R
 
   · allI:    (⋀x. P x) ⟹ ∀x. P x
 
   · allI:    (⋀x. P x) ⟹ ∀x. P x
  *}
+
  
text {*
+
subsection ‹Ejemplo 1›
  Ejemplo 1 (p. 10). Demostrar que
+
 
 +
text ‹Ejemplo 1 (p. 10). Demostrar que
 
     P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c)
 
     P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c)
*}
+
 +
 
 +
subsubsection ‹Demostración detallada›
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 38: Línea 39:
 
   show 4: "¬Q(c)" using 3 1 by (rule mp)
 
   show 4: "¬Q(c)" using 3 1 by (rule mp)
 
qed
 
qed
 +
 +
subsubsection ‹Demostración estructurada›
  
 
― ‹La demostración estructurada es›
 
― ‹La demostración estructurada es›
Línea 48: Línea 51:
 
   then show "¬Q(c)" using assms(1) ..
 
   then show "¬Q(c)" using assms(1) ..
 
qed
 
qed
 +
 +
subsubsection ‹Demostración automática›
  
 
― ‹La demostración automática es›
 
― ‹La demostración automática es›
Línea 54: Línea 59:
 
           "∀x. (P(x) ⟶ ¬Q(x))"
 
           "∀x. (P(x) ⟶ ¬Q(x))"
 
   shows "¬Q(c)"
 
   shows "¬Q(c)"
using assms
+
  using assms
by auto
+
  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 {*
+
text ‹Ejemplo 2 (p. 11). Demostrar que
  Ejemplo 2 (p. 11). Demostrar que
 
 
     ∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x)
 
     ∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x)
*}
+
 +
 
 +
subsubsection ‹Demostración detallada›
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 86: Línea 123:
 
   show 5: "¬(Q a)" using 3 4 by (rule mp)  
 
   show 5: "¬(Q a)" using 3 4 by (rule mp)  
 
qed
 
qed
 +
 +
subsubsection ‹Demostración estructurada›
  
 
― ‹La demostración estructurada es›
 
― ‹La demostración estructurada es›
Línea 96: Línea 135:
 
   have "P a" using assms(2) ..
 
   have "P a" using assms(2) ..
 
   have "P a ⟶ ¬(Q a)" using assms(1) ..
 
   have "P a ⟶ ¬(Q a)" using assms(1) ..
   then show "¬(Q a)" using `P a` ..
+
   then show "¬(Q a)" using ‹P a› ..
 
qed
 
qed
 +
 +
subsubsection ‹Demostración automática›
  
 
― ‹La demostración automática es›
 
― ‹La demostración automática es›
Línea 104: Línea 145:
 
           "∀x. P x"
 
           "∀x. P x"
 
   shows  "∀x. ¬(Q x)"
 
   shows  "∀x. ¬(Q x)"
using assms
+
  using assms
by auto
+
  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 *}
+
section ‹Reglas del cuantificador existencial›
  
text {*
+
text ‹Las reglas del cuantificador existencial son
  Las reglas del cuantificador existencial son
 
 
   · exI:    P a ⟹ ∃x. P x
 
   · exI:    P a ⟹ ∃x. P x
 
   · exE:    ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
 
   · exE:    ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
Línea 116: Línea 170:
 
   En la regla exE la nueva variable se introduce mediante la declaración  
 
   En la regla exE la nueva variable se introduce mediante la declaración  
 
   "obtain ... where ... by (rule exE)"  
 
   "obtain ... where ... by (rule exE)"  
  *}
+
  
text {*
+
subsection ‹Ejemplo 3›
  Ejemplo  (p. 12). Demostrar que
+
 
 +
text ‹Ejemplo 3 (p. 12). Demostrar que
 
     ∀x. P x ⊢ ∃x. P x
 
     ∀x. P x ⊢ ∃x. P x
*}
+
 +
 
 +
subsubsection ‹Demostración detallada›
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 132: Línea 189:
 
   then show "∃x. P x" by (rule exI)
 
   then show "∃x. P x" by (rule exI)
 
qed
 
qed
 +
 +
subsubsection ‹Demostración estructurada›
  
 
― ‹La demostración estructurada es›
 
― ‹La demostración estructurada es›
Línea 160: Línea 219:
 
   show "P a" using assms ..
 
   show "P a" using assms ..
 
qed
 
qed
 +
 +
subsubsection ‹Demostración automática›
  
 
― ‹La demostración automática es›
 
― ‹La demostración automática es›
Línea 165: Línea 226:
 
   assumes "∀x. P x"
 
   assumes "∀x. P x"
 
   shows "∃x. P x"
 
   shows "∃x. P x"
using assms
+
  using assms
by auto
+
  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 {*
+
text ‹Ejemplo 4 (p. 13). Demostrar
  Ejemplo 4 (p. 13). Demostrar
 
 
     ∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x
 
     ∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x
*}
+
 +
 
 +
subsubsection ‹Demostración detallada›
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 184: Línea 256:
 
   then show 6: "∃x. Q x" by (rule exI)
 
   then show 6: "∃x. Q x" by (rule exI)
 
qed
 
qed
 +
 +
subsubsection ‹Demostración estructurada›
  
 
― ‹La demostración estructurada es›
 
― ‹La demostración estructurada es›
Línea 193: Línea 267:
 
   obtain a where "P a" using assms(2) ..
 
   obtain a where "P a" using assms(2) ..
 
   have "P a ⟶ Q a" using assms(1) ..
 
   have "P a ⟶ Q a" using assms(1) ..
   then have "Q a" using `P a` ..
+
   then have "Q a" using ‹P a› ..
 
   then show "∃x. Q x" ..
 
   then show "∃x. Q x" ..
 
qed
 
qed
 +
 +
subsubsection ‹Demostración automática›
  
 
― ‹La demostración automática es›
 
― ‹La demostración automática es›
Línea 202: Línea 278:
 
           "∃x. P x"
 
           "∃x. P x"
 
   shows "∃x. Q x"
 
   shows "∃x. Q x"
using assms
+
  using assms
by auto
+
  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›
  
section {* Demostración de equivalencias *}
+
text ‹Ejemplo 5.1 (p. 15). Demostrar
 +
    ¬∀x. P x  ⊢ ∃x. ¬(P x)›
  
text {*
+
subsubsection ‹Demostración detallada›
  Ejemplo 5.1 (p. 15). Demostrar
 
    ¬∀x. P x  ⊢ ∃x. ¬(P x) *}
 
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 224: Línea 314:
 
       assume "¬P(a)"
 
       assume "¬P(a)"
 
       then have "∃x. ¬P(x)" by (rule exI)
 
       then have "∃x. ¬P(x)" by (rule exI)
       with (∃x. ¬P(x))` show False by (rule notE)
+
       with ‹¬(∃x. ¬P(x))show False by (rule notE)
 
     qed
 
     qed
 
   qed
 
   qed
 
   with assms show False by (rule notE)
 
   with assms show False by (rule notE)
 
qed
 
qed
 +
 +
subsubsection ‹Demostración estructurada›
  
 
― ‹La demostración estructurada es›
 
― ‹La demostración estructurada es›
Línea 243: Línea 335:
 
       assume "¬P(a)"
 
       assume "¬P(a)"
 
       then have "∃x. ¬P(x)" ..
 
       then have "∃x. ¬P(x)" ..
       with (∃x. ¬P(x))` show False ..
+
       with ‹¬(∃x. ¬P(x))show False ..
 
     qed
 
     qed
 
   qed
 
   qed
 
   with assms show False ..
 
   with assms show False ..
 
qed
 
qed
 +
 +
subsubsection ‹Demostración automática›
  
 
― ‹La demostración automática es›
 
― ‹La demostración automática es›
Línea 253: Línea 347:
 
   assumes "¬(∀x. P(x))"
 
   assumes "¬(∀x. P(x))"
 
   shows  "∃x. ¬P(x)"
 
   shows  "∃x. ¬P(x)"
using assms
+
  using assms
by auto
+
  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 {*
+
text
 
   Ejemplo 5.2 (p. 16). Demostrar
 
   Ejemplo 5.2 (p. 16). Demostrar
     ∃x. ¬(P x)  ⊢ ¬∀x. P x *}
+
     ∃x. ¬(P x)  ⊢ ¬∀x. P x›
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 267: Línea 373:
 
   assume "∀x. P(x)"
 
   assume "∀x. P(x)"
 
   obtain a where "¬P(a)" using assms by (rule exE)
 
   obtain a where "¬P(a)" using assms by (rule exE)
   have "P(a)" using `∀x. P(x)` by (rule allE)
+
   have "P(a)" using ‹∀x. P(x)by (rule allE)
   with `¬P(a)` show False by (rule notE)
+
   with ‹¬P(a)show False by (rule notE)
 
qed
 
qed
  
Línea 278: Línea 384:
 
   assume "∀x. P(x)"
 
   assume "∀x. P(x)"
 
   obtain a where "¬P(a)" using assms ..
 
   obtain a where "¬P(a)" using assms ..
   have "P(a)" using `∀x. P(x)` ..
+
   have "P(a)" using ‹∀x. P(x)..
   with `¬P(a)` show False ..
+
   with ‹¬P(a)show False ..
 
qed
 
qed
  
Línea 289: Línea 395:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 5.3 (p. 17). Demostrar
 
   Ejemplo 5.3 (p. 17). Demostrar
     ⊢ ¬∀x. P x  ⟷ ∃x. ¬(P x) *}
+
     ⊢ ¬∀x. P x  ⟷ ∃x. ¬(P x)
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 309: Línea 415:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 6.1 (p. 18). Demostrar
 
   Ejemplo 6.1 (p. 18). Demostrar
     ∀x. P(x) ∧ Q(x) ⊢  (∀x. P(x)) ∧ (∀x. Q(x)) *}
+
     ∀x. P(x) ∧ Q(x) ⊢  (∀x. P(x)) ∧ (∀x. Q(x))
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 360: Línea 466:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 6.2 (p. 19). Demostrar
 
   Ejemplo 6.2 (p. 19). Demostrar
     (∀x. P(x)) ∧ (∀x. Q(x)) ⊢ ∀x. P(x) ∧ Q(x) *}
+
     (∀x. P(x)) ∧ (∀x. Q(x)) ⊢ ∀x. P(x) ∧ Q(x)
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 374: Línea 480:
 
   have "∀x. Q(x)" using assms by (rule conjunct2)
 
   have "∀x. Q(x)" using assms by (rule conjunct2)
 
   then have "Q(a)" by (rule allE)
 
   then have "Q(a)" by (rule allE)
   with `P(a)` show "P(a) ∧ Q(a)" by (rule conjI)
+
   with ‹P(a)show "P(a) ∧ Q(a)" by (rule conjI)
 
qed
 
qed
  
Línea 387: Línea 493:
 
   have "∀x. Q(x)" using assms ..
 
   have "∀x. Q(x)" using assms ..
 
   then have "Q(a)" ..
 
   then have "Q(a)" ..
   with `P(a)` show "P(a) ∧ Q(a)" ..
+
   with ‹P(a)show "P(a) ∧ Q(a)" ..
 
qed
 
qed
  
Línea 397: Línea 503:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 6.3 (p. 20). Demostrar
 
   Ejemplo 6.3 (p. 20). Demostrar
     ⊢ ∀x. P(x) ∧ Q(x) ⟷ (∀x. P(x)) ∧ (∀x. Q(x)) *}
+
     ⊢ ∀x. P(x) ∧ Q(x) ⟷ (∀x. P(x)) ∧ (∀x. Q(x))
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 412: Línea 518:
 
qed
 
qed
  
text {*
+
text
 
   Ejemplo 7.1 (p. 21). Demostrar
 
   Ejemplo 7.1 (p. 21). Demostrar
     (∃x. P(x)) ∨ (∃x. Q(x)) ⊢ ∃x. P(x) ∨ Q(x) *}
+
     (∃x. P(x)) ∨ (∃x. Q(x)) ⊢ ∃x. P(x) ∨ Q(x)
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 457: Línea 563:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 7.2 (p. 22). Demostrar
 
   Ejemplo 7.2 (p. 22). Demostrar
     ∃x. P(x) ∨ Q(x) ⊢ (∃x. P(x)) ∨ (∃x. Q(x)) *}
+
     ∃x. P(x) ∨ Q(x) ⊢ (∃x. P(x)) ∨ (∃x. Q(x))
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 504: Línea 610:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 7.3 (p. 23). Demostrar
 
   Ejemplo 7.3 (p. 23). Demostrar
     ⊢ ((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x)) *}
+
     ⊢ ((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 525: Línea 631:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 8.1 (p. 24). Demostrar
 
   Ejemplo 8.1 (p. 24). Demostrar
     ∃x y. P(x,y) ⊢ ∃y x. P(x,y) *}
+
     ∃x y. P(x,y) ⊢ ∃y x. P(x,y)
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 558: Línea 664:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 8.2. Demostrar
 
   Ejemplo 8.2. Demostrar
     ∃y x. P(x,y) ⊢ ∃x y. P(x,y) *}
+
     ∃y x. P(x,y) ⊢ ∃x y. P(x,y)
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 591: Línea 697:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 8.3 (p. 25). Demostrar
 
   Ejemplo 8.3 (p. 25). Demostrar
     ⊢ (∃x y. P(x,y)) ⟷ (∃y x. P(x,y)) *}
+
     ⊢ (∃x y. P(x,y)) ⟷ (∃y x. P(x,y))
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 611: Línea 717:
 
by auto
 
by auto
  
section {* Reglas de la igualdad *}
+
section ‹Reglas de la igualdad›
  
text {*
+
text
 
   Las reglas básicas de la igualdad son:
 
   Las reglas básicas de la igualdad son:
 
   · refl:  t = t
 
   · refl:  t = t
 
   · subst: ⟦s = t; P s⟧ ⟹ P t
 
   · subst: ⟦s = t; P s⟧ ⟹ P t
*}
+
  
text {*
+
text
 
   Ejemplo 9 (p. 27). Demostrar
 
   Ejemplo 9 (p. 27). Demostrar
 
     x + 1 = 1 + x, x + 1 > 1 ⟶ x + 1 > 0 ⊢ 1 + x > 1 ⟶ 1 + x > 0
 
     x + 1 = 1 + x, x + 1 > 1 ⟶ x + 1 > 0 ⊢ 1 + x > 1 ⟶ 1 + x > 0
*}
+
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 649: Línea 755:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 10 (p. 27). Demostrar
 
   Ejemplo 10 (p. 27). Demostrar
 
     x = y, y = z ⊢ x = z
 
     x = y, y = z ⊢ x = z
*}
+
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›
Línea 679: Línea 785:
 
by auto
 
by auto
  
text {*
+
text
 
   Ejemplo 11 (p. 28). Demostrar
 
   Ejemplo 11 (p. 28). Demostrar
 
     s = t ⊢ t = s
 
     s = t ⊢ t = s
*}
+
  
 
― ‹La demostración detallada es›
 
― ‹La demostración detallada es›

Revisión actual del 21:03 7 feb 2020

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