Jalonso en 06:34 16 mar 2013

2013-03-16T06:34:29Z

Jalonso: Página creada con ' 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 deducc...'

2013-03-16T06:34:15Z

Página creada con '<source lang="isar"> 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 deducc...'

Página nueva

<source lang="isar">
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
</source>

@@ Línea 1: / Línea 1: @@
 <source lang="isar">
-header {* Tema 4: Deducción natural en lógica de primer orden *}
+header {* Tema 2: Deducción natural en lógica de primer orden *}
-theory T4
+theory T2
 imports Main
 begin

GLC T2 - Historial de revisiones

Jalonso en 06:34 16 mar 2013

Jalonso: Página creada con ' 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 deducc...'

Jalonso: Página creada con ' 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 deducc...'