RA2012: Introducción a la demostración asistida con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha presentado:

una visión panorámica del razonamiento asistido por computador,
un panorama del contenido de la asignatura:
- deducción natural en Isabelle/HOL,
- programación funcional en Isabelle/HOL,
- razonamiento sobre programas.
un ejemplo de demostración por deducción natural en Isabelle/HOL
una visión general de las teorías de HOL.

El ejemplo que se ha visto para introducir los elementos del lenguaje de demostración es el siguiente

header {* Tema 3: Deducción natural proposicional con Isabelle/HOL *}

theory T3
imports Main 
begin

text {*
  En esta sección se presentan los ejemplos del tema de deducción natural
  proposicional siguiendo la presentación de Huth y Ryan en su libro
  "Logic in Computer Science" http://goo.gl/qsVpY y, más concretamente,
  a la forma como se explica en la asignatura de "Lógica informática" (LI) 
  http://goo.gl/AwDiv
 
  La página al lado de cada ejemplo indica la página de las transparencias 
  de LI donde se encuentra la demostración. *}

subsection {* Reglas de la conjunción *}

text {* 
  Ejemplo 1 (p. 4). Demostrar que
     p ∧ q, r ⊢ q ∧ r.
  *}     

-- "La demostración detallada es"
lemma ejemplo_1_1:
  assumes 1: "p ∧ q" and
          2: "r" 
  shows "q ∧ r"     
proof -
  have 3: "q" using 1 by (rule conjunct2)
  show 4: "q ∧ r" using 3 2 by (rule conjI)
qed

text {*
  Notas sobre el lenguaje: En la demostración anterior se ha usado
  · "assumes" para indicar las hipótesis,
  · "and" para separar las hipótesis,
  · "shows" para indicar la conclusión,
  · "proof" para iniciar la prueba,
  · "qed" para terminar la pruebas,
  · "-" (después de "proof") para no usar el método por defecto,
  · "have" para establecer un paso,
  · "using" para usar hechos en un paso,
  · "by (rule ..)" para indicar la regla con la que se peueba un hecho,
  · "show" para establecer la conclusión.

  Notas sobre la lógica: Las reglas de la conjunción son
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
*}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_2:
  assumes 1: "p ∧ q" and 
          2: "r" 
  shows "q ∧ r"     
proof -
  have 3: "q" using 1 .. 
  show 4: "q ∧ r" using 3 2 ..
qed

text {*
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · ".." para indicar que se prueba por la regla correspondiente. *}

text {* Se pueden eliminar las etiquetas como sigue *}

lemma ejemplo_1_3:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
proof -
  have "q" using assms(1) ..
  thus "q ∧ r" using assms(2) ..
qed

text {*
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "assms(n)" para indicar la hipótesis n y
  · "thus" para demostrar la conclusión usando el hecho anterior.
  Además, no es necesario usar and entre las hipótesis. *}

text {* Se puede automatizar la demostración como sigue *}
  
lemma ejemplo_1_4:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
using assms
by auto

text {*
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "assms" para indicar las hipótesis y
  · "by auto" para demostrar la conclusión automáticamente. *}

text {* Se puede automatizar totalmente la demostración como sigue *}

lemma ejemplo_1_5:
  "⟦p ∧ q; r⟧ ⟹ q ∧ r"
by auto

text {*
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "⟦ ... ⟧" para representar las hipótesis,
  · ";" para separar las hipótesis y
  · "⟹" para separar las hipótesis de la conclusión. *}

text {* Se puede hacer la demostración por razonamiento hacia atrás,
  como sigue *}

lemma ejemplo_1_6:
  assumes "p ∧ q" 
      and "r" 
  shows   "q ∧ r"     
proof (rule conjI)
  show "q" using assms(1) by (rule conjunct2)
next
  show "r" using assms(2) by this
qed

text {*
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "proof (rule r)" para indicar que se hará la demostración con la
    regla r,
  · "next" para indicar el comienzo de la prueba del siguiente
    subobjetivo,
  · "this" para indicar el hecho actual. *}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_7:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
proof 
  show "q" using assms(1) ..
next
  show "r" using assms(2) . 
qed

text {*
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "." para indicar por el hecho actual. *}

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

header {* Tema 3: Deducción natural proposicional con Isabelle/HOL *}

theory T3

imports Main

begin

text {*

En esta sección se presentan los ejemplos del tema de deducción natural

proposicional siguiendo la presentación de Huth y Ryan en su libro

"Logic in Computer Science" http://goo.gl/qsVpY y, más concretamente,

a la forma como se explica en la asignatura de "Lógica informática" (LI)

http://goo.gl/AwDiv

La página al lado de cada ejemplo indica la página de las transparencias

de LI donde se encuentra la demostración. *}

subsection {* Reglas de la conjunción *}

text {*

Ejemplo 1 (p. 4). Demostrar que

p ∧ q, r ⊢ q ∧ r.

-- "La demostración detallada es"

lemma ejemplo_1_1:

assumes 1: "p ∧ q" and

2: "r"

shows "q ∧ r"

proof -

have 3: "q" using 1 by (rule conjunct2)

show 4: "q ∧ r" using 3 2 by (rule conjI)

qed

text {*

Notas sobre el lenguaje: En la demostración anterior se ha usado

· "assumes" para indicar las hipótesis,

· "and" para separar las hipótesis,

· "shows" para indicar la conclusión,

· "proof" para iniciar la prueba,

· "qed" para terminar la pruebas,

· "-" (después de "proof") para no usar el método por defecto,

· "have" para establecer un paso,

· "using" para usar hechos en un paso,

· "by (rule ..)" para indicar la regla con la que se peueba un hecho,

· "show" para establecer la conclusión.

Notas sobre la lógica: Las reglas de la conjunción son

· conjI: ⟦P; Q⟧ ⟹ P ∧ Q

· conjunct1: P ∧ Q ⟹ P

· conjunct2: P ∧ Q ⟹ Q

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_2:

assumes 1: "p ∧ q" and

2: "r"

shows "q ∧ r"

proof -

have 3: "q" using 1 ..

show 4: "q ∧ r" using 3 2 ..

qed

text {*

Nota sobre el lenguaje: En la demostración anterior se ha usado

· ".." para indicar que se prueba por la regla correspondiente. *}

text {* Se pueden eliminar las etiquetas como sigue *}

lemma ejemplo_1_3:

assumes "p ∧ q"

"r"

shows "q ∧ r"

proof -

have "q" using assms(1) ..

thus "q ∧ r" using assms(2) ..

qed

text {*

Nota sobre el lenguaje: En la demostración anterior se ha usado

· "assms(n)" para indicar la hipótesis n y

· "thus" para demostrar la conclusión usando el hecho anterior.

Además, no es necesario usar and entre las hipótesis. *}

text {* Se puede automatizar la demostración como sigue *}

lemma ejemplo_1_4:

assumes "p ∧ q"

"r"

shows "q ∧ r"

using assms

by auto

text {*

Nota sobre el lenguaje: En la demostración anterior se ha usado

· "assms" para indicar las hipótesis y

· "by auto" para demostrar la conclusión automáticamente. *}

text {* Se puede automatizar totalmente la demostración como sigue *}

lemma ejemplo_1_5:

"⟦p ∧ q; r⟧ ⟹ q ∧ r"

by auto

text {*

Nota sobre el lenguaje: En la demostración anterior se ha usado

· "⟦ ... ⟧" para representar las hipótesis,

· ";" para separar las hipótesis y

· "⟹" para separar las hipótesis de la conclusión. *}

text {* Se puede hacer la demostración por razonamiento hacia atrás,

como sigue *}

lemma ejemplo_1_6:

assumes "p ∧ q"

and "r"

shows "q ∧ r"

proof (rule conjI)

show "q" using assms(1) by (rule conjunct2)

show "r" using assms(2) by this

qed

text {*

Nota sobre el lenguaje: En la demostración anterior se ha usado

· "proof (rule r)" para indicar que se hará la demostración con la

regla r,

· "next" para indicar el comienzo de la prueba del siguiente

subobjetivo,

· "this" para indicar el hecho actual. *}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_7:

assumes "p ∧ q"

"r"

shows "q ∧ r"

proof

show "q" using assms(1) ..

show "r" using assms(2) .

qed

text {*

Nota sobre el lenguaje: En la demostración anterior se ha usado

· "." para indicar por el hecho actual. *}

end

Se puede imprimir o compartir con