Menu Close

RA2018: Deducción natural de primer orden con Isabelle/HOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha presentado la deducción natural de primer orden Isabelle/HOL. La presentación se basa en los ejemplos del tema 8 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

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

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la última que es automática.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

La teoría con los ejemplos presentados en la clase es la siguiente:

chapter {* Tema 8b: Deducción natural en lógica de primer orden *}
 
theory T8b_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 8 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
  *}
 
text {* 
  Ejemplo 1 (p. 10). Demostrar que
     P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c)
*}
 
-- "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
 
-- "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) ..
  thus "¬Q(c)" using assms(1) ..
qed
 
-- "La demostración automática es"
lemma ejemplo_1c: 
  assumes "P(c)"
          "∀x. (P(x) ⟶ ¬Q(x))"
  shows "¬Q(c)"
using assms
by auto
 
text {* 
  Ejemplo 2 (p. 11). Demostrar que
     ∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x)
*}
 
-- "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) }
  thus "∀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
 
-- "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) ..
  thus "¬(Q a)" using `P a` ..
qed
 
-- "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
 
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)" 
  *}
 
text {* 
  Ejemplo  (p. 12). Demostrar que
     ∀x. P x ⊢ ∃x. P x
*}
 
-- "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)
  thus "∃x. P x" by (rule exI)
qed
 
-- "La demostración estructurada es"
lemma ejemplo_3b:
  assumes "∀x. P x"
  shows "∃x. P x"
proof -
  fix a
  have "P a" using assms ..
  thus "∃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
 
-- "La demostración automática es"
lemma ejemplo_3e:
  assumes "∀x. P x"
  shows "∃x. P x"
using assms
by auto
 
text {* 
  Ejemplo 4 (p. 13). Demostrar
     ∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x
*}
 
-- "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)
  thus 6: "∃x. Q x" by (rule exI)
qed
 
-- "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) ..
  hence "Q a" using `P a` ..
  thus "∃x. Q x" ..
qed
 
-- "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
 
section {* Demostración de equivalencias *}
 
text {* 
  Ejemplo 5.1 (p. 15). Demostrar
     ¬∀x. P x  ⊢ ∃x. ¬(P x) *}
 
-- "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)"
      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 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)"
      hence "∃x. ¬P(x)" ..
      with(∃x. ¬P(x))` show False ..
    qed
  qed
  with assms show False ..
qed
 
-- "La demostración automática es"
lemma ejemplo_5_1c:
  assumes "¬(∀x. P(x))"
  shows   "∃x. ¬P(x)"
using assms
by auto
 
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))"
  thus "∃x. ¬P(x)" by (rule ejemplo_5_1a)
next
  assume "∃x. ¬P(x)"
  thus "¬(∀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)
    thus "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)
    thus "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 ..
    thus "P(a)" ..
  qed
next
  show "∀x. Q(x)"
  proof 
    fix a
    have "P(a) ∧ Q(a)" using assms ..
    thus "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)
  hence "P(a)" by (rule allE)
  have "∀x. Q(x)" using assms by (rule conjunct2)
  hence "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 ..
  hence "P(a)" by (rule allE)
  have "∀x. Q(x)" using assms ..
  hence "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)"
  thus "(∀x. P(x)) ∧ (∀x. Q(x))" by (rule ejemplo_6_1a)
next
  assume "(∀x. P(x)) ∧ (∀x. Q(x))"
  thus "∀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)
  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
 
-- "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)" ..
  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
 
-- "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)
  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 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 ..
  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 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))"
  thus "∃x. P(x) ∨ Q(x)" by (rule ejemplo_7_1a)
next
  assume "∃x. P(x) ∨ Q(x)"
  thus "(∃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)
  hence "∃x. P(x,b)" by (rule exI)
  thus "∃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)" ..
  hence "∃x. P(x,b)" ..
  thus "∃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)
  hence "∃y. P(a,y)" by (rule exI)
  thus "∃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)" ..
  hence "∃y. P(a,y)" ..
  thus "∃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)"
  thus "∃y x. P(x,y)" by (rule ejemplo_8_1a)
next
  assume "∃y x. P(x,y)"
  thus "∃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
RA2018