DAO (Demostración asistida por ordenador) DAO (Demostración asistida por ordenador)

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

theory T4
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 2 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_1_1: 
  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_1_2: 
  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_1_3: 
  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_2_1: 
  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_2_2: 
  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_2_3: 
  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_2_4: 
  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_3_1:
  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_3_2:
  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_3_3:
  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_3_4:
  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_3_5:
  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_4_1:
  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_4_2:
  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_4_3:
  assumes "∀x. (P x ⟶ Q x)"
          "∃x. P x"
  shows "∃x. Q x"
using assms
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 5 (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_5_1: 
  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_5_2: 
  "⟦x+1 = 1+x; x+1 > 1 ⟶ x+1 > 0⟧ ⟹ 1+x > 1 ⟶ 1+x > 0"
by (rule subst)

-- "La demostración automática es"
lemma ejemplo_5_3: 
  "⟦x+1 = 1+x; x+1 > 1 ⟶ x+1 > 0⟧ ⟹ 1+x > 1 ⟶ 1+x > 0"
by auto

text {* 
  Ejemplo 6 (p. 27). Demostrar
     x = y, y = z ⊢ x = z
*}

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

-- "La demostración estructurada es"
lemma ejemplo_6_2: 
  "⟦x = y; y = z⟧ ⟹ x = z"
by (rule subst)

-- "La demostración automática es"
lemma ejemplo_6_3: 
  "⟦x = y; y = z⟧ ⟹ x = z"
by auto

text {* 
  Ejemplo 7 (p. 27). Demostrar
     s = t ⊢ t = s
*}

-- "La demostración detallada es"
lemma ejemplo_7_1:
  "s = t ⟹ t = s"
proof -
  assume 1: "s = t"
  have 2: "s = s" by (rule refl)
  show "t = s" using 1 2 by (rule subst)
qed

-- "La demostración estructurada es"
lemma ejemlo_7_2:
  "s = t ⟹ t = s"
by (erule subst) (rule refl)

-- "La demostración automática es"
lemma ejemlo_7_3:
  "s = t ⟹ t = s"
by auto

text {*
  Algunas reglas derivadas de la igualdad son:
  · 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⟧ ⟹ c = 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
*}

-- "La demostración estructurada de not_sym es"
lemma not_sym_1: 
  assumes "t ≠ s"
  shows   "s ≠ t"
proof
  assume "s = t"
  hence "t = s" ..
  show False using assms(1) `t = s` .. 
qed

-- "La demostración detallada de not_sym es"
lemma not_sym_2: 
  assumes "t ≠ s"
  shows   "s ≠ t"
proof (rule notI)
  assume "s = t"
  hence "t = s" by (rule sym)
  show False using assms(1) `t = s` by (rule notE) 
qed

-- "La demostración automática de not_sym es"
lemma not_sym_3: 
  "t ≠ s ⟹ s ≠ t"
by auto

-- "La demostración estructurada de ssubst es"
lemma sssubs_1:
  assumes "t = s"
          "P s"
  shows   "P t"
proof -
  have "s = t" using assms(1) ..
  thus "P t" using assms(2) by (rule subst)
qed

-- "La demostración detallada de ssubst es"
lemma sssubs_2:
  assumes "t = s"
          "P s"
  shows   "P t"
proof -
  have "s = t" using assms(1) by (rule sym)
  thus "P t" using assms(2) by (rule subst)
qed

-- "La demostración automática de ssubst es"
lemma ssubst_3:
  "⟦t = s; P s⟧ ⟹ P t"
by auto

-- "La demostración detallada de box_equals es"
lemma box_equals_1: 
  assumes "a = b" 
          "a = c" 
          "b = d" 
  shows   "c = d"
proof -
  have "c = b" using assms(2) assms(1) by (rule subst) 
  with assms(3) show "c = d" by (rule subst) 
qed

-- "La demostración semiautomática de box_equals es"
lemma box_equals_2: 
  "⟦a = b; a = c; b = d⟧ ⟹ c = d"
by (rule box_equals)

-- "La demostración automática de box_equals es"
lemma box_equals_3: 
  "⟦a = b; a = c; b = d⟧ ⟹ c = d"
by auto

-- "La demostración detallada de arg_cong es"
lemma arg_cong_1:   
  assumes "x = y" 
  shows   "f x = f y"
proof -
  have "f x = f x" by (rule refl)
  with assms(1) show "f x = f y" by (rule subst)
qed

-- "La demostración semiautomática de arg_cong es"
lemma arg_cong_2:   
  "x = y ⟹ f x = f y"
by (rule arg_cong)

-- "La demostración automática de arg_cong es"
lemma arg_cong_3:   
  "x = y ⟹ f x = f y"
by auto

-- "La demostración detallada de fun_cong es"
lemma fun_cong_1:   
  assumes "f = g"
  shows   "f x = g x"
proof -
  have "f x = f x" by (rule refl)
  with assms(1) show "f x = g x" by (erule_tac P = "λh. f x = h x" in subst)
qed

-- "La demostración semiautomática de fun_cong es"
lemma fun_cong_2:   
  "f = g ⟹ f x = g x"
by (rule fun_cong)

-- "La demostración automática de fun_cong es"
lemma fun_cong_3:   
  "f = g ⟹ f x = g x"
by auto

-- "La demostración detallada de cong es"
lemma cong_1:       
  assumes "f = g" 
          "x = y" 
  shows   "f x = g y"
proof -
  have "f x = f x" by (rule refl)
  with assms(2) have "f x = f y" by (rule subst)
  with assms(1) show "f x = g y" by (erule_tac P = "λh. f x = h y" in subst)
qed
 
-- "La demostración semiautomática de cong es"
lemma cong_2:       
  "⟦f = g; x = y⟧ ⟹ f x = g y"
by (rule cong)
 
-- "La demostración automática de cong es"
lemma cong_3:       
  "⟦f = g; x = y⟧ ⟹ f x = g y"
by auto

section {* Ejemplo de razonamiento sobre programa *}

text {* 
  Definición. El número natural x divide al número natural y si existe
  un natural k tal que kx = y.
*}

definition divide :: "nat ⇒ nat ⇒ bool" where 
  "divide x y ≡ ∃k. k*x = y"

text {* 
  La definición de divide se añade a las reglas de simplificación. 
*}

declare divide_def[simp]

text {* 
  Ejemplo 8 [Transitividad de la divisibilidad]. Sean a, b y c números
  naturales. Si b es divisible por a y c es divisible por b, entonces c
  es divisible por a.  
*}

-- "La demostración estructurada es"
lemma ejemplo_8_1: 
  assumes "divide a b" 
          "divide b c"
  shows   "divide a c"
proof -
  from assms(1) obtain m where "m*a = b" by auto
  from assms(2) obtain n where "n*b = c" by auto
  hence "m*n*a = c" using `m*a = b` by auto
  hence "∃k. k*a = c" by (rule exI)
  thus "divide a c" by simp
qed

-- "La demostración puede simplificarse"
lemma ejemplo_8_2: 
  assumes "divide a b" 
          "divide b c"
  shows   "divide a c"
proof simp
  from assms(1) obtain m where "m*a = b" by auto
  from assms(2) obtain n where "n*b = c" by auto
  hence "m*n*a = c" using `m*a = b` by auto
  thus "∃k. k*a = c" ..
qed

-- "La demostración automática es"
lemma ejemplo_8_3: 
  "⟦divide a b; divide b c⟧ ⟹ divide a c"
by auto

section {* Razonamiento ecuacional *}

text {* 
  El razonamiento ecuacional se realiza usando la combinación de "also"
  (además) y "finally" (finalmente). 
*}

text {*  
  Ejemplo 9 [Razonamiento ecuacional]. Si a=b, b=c y c=d, entonces a=d.  
*}

-- "La demostración detallada es"
lemma ejemplo_9_1:
  assumes "a = b" 
          "b = c" 
          "c = d"
  shows   "a = d"
proof -
  have "a = b" by (rule assms(1))
  also have "… = c" by (rule assms(2))
  also have "… = d" by (rule assms(3))
  finally show "a = d" .
qed

text {* 
  El lema anterior puede demostrarse automáticamente con la maza
  ("sledgehammer"). 
*}

lemma  ejemplo_9_2:
  assumes "a = b" 
          "b = c" 
          "c = d"
  shows   "a = d"
proof -
  show "a=d" by (metis assms)
qed

end