Tema 8

header {* Tema 8: Deducción natural en lógica de primer orden *}

theory Tema8
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 ejemlo_11b:
  assumes "s = t"
  shows   "t = s"
using assms
by auto

end