RA2013: Razonamiento por casos y por inducción (1)

La clase de hoy del curso de Razonamiento automático ha tenido dos partes: comentar las soluciones de los ejercicios de la relación 4 y empezar el estudio del tema 4.

En la relación 4 se define la función cons que añade un elemento al final de la lista y se demuestra algunas de sus propiedades. Lo interesante es el uso de algunas propiedades en la demostración de otras (como en el ejercicio 5). Las ejercicios y sus soluciones son

header {* R4: Cons inverso *}

theory R4
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir recursivamente la función 
     snoc :: "'a list ⇒ 'a ⇒ 'a list"
  tal que (snoc xs a) es la lista obtenida al añadir el elemento a al
  final de la lista xs. Por ejemplo, 
     value "snoc [2,5] (3::int)" == [2,5,3]

  Nota: No usar @.
  --------------------------------------------------------------------- 
*}

fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
  "snoc [] a = [a]"
| "snoc (x#xs) a = x # (snoc xs a)"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar automáticamente el siguiente teorema 
     snoc xs a = xs @ [a]
  --------------------------------------------------------------------- 
*}

lemma "snoc xs a = xs @ [a]"
by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar detalladamente el siguiente teorema 
     snoc xs a = xs @ [a]
  --------------------------------------------------------------------- 
*}

lemma snoc_append: "snoc xs a = xs @ [a]"
proof (induct "xs") 
  show "snoc [] a = [] @ [a]"
  proof -
    have "snoc [] a = [a]" by simp
    also have "… = [] @ [a]" by simp
    finally show "snoc [] a = [] @ [a]" .
  qed
next
  fix b xs assume HI: "snoc xs a = xs @ [a]"
  show "snoc (b # xs) a = (b # xs) @ [a]"
  proof -
    have "snoc (b # xs) a = b # (snoc xs a)" by simp
    also have "… = b # (xs @ [a])" using HI by simp
    also have "… = (b # xs) @ [a]" by simp
    finally show "snoc (b # xs) a = (b # xs) @ [a]" .
  qed
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4. Demostrar automáticamente el siguiente lema
     rev (x # xs) = snoc (rev xs) x"
  --------------------------------------------------------------------- 
*}

lemma "rev (x # xs) = snoc (rev xs) x"
by (auto simp add: snoc_append)

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5. Demostrar detalladamente el siguiente lema
     rev (x # xs) = snoc (rev xs) x"
  --------------------------------------------------------------------- 
*}

theorem "rev (x # xs) = snoc (rev xs) x"
proof -
  have "rev (x # xs) = (rev xs) @ [x]" by simp
  also have "… = snoc (rev xs) x" by (simp add:snoc_append)
  finally show "rev (x # xs) = snoc (rev xs) x" .
qed

end

header {* R4: Cons inverso *}

theory R4

imports Main

begin

text {*

---------------------------------------------------------------------

Ejercicio 1. Definir recursivamente la función

snoc :: "'a list ⇒ 'a ⇒ 'a list"

tal que (snoc xs a) es la lista obtenida al añadir el elemento a al

final de la lista xs. Por ejemplo,

value "snoc [2,5] (3::int)" == [2,5,3]

Nota: No usar @.

---------------------------------------------------------------------

fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where

"snoc [] a = [a]"

| "snoc (x#xs) a = x # (snoc xs a)"

text {*

---------------------------------------------------------------------

Ejercicio 2. Demostrar automáticamente el siguiente teorema

snoc xs a = xs @ [a]

---------------------------------------------------------------------

lemma "snoc xs a = xs @ [a]"

by (induct xs) auto

text {*

---------------------------------------------------------------------

Ejercicio 3. Demostrar detalladamente el siguiente teorema

snoc xs a = xs @ [a]

---------------------------------------------------------------------

lemma snoc_append: "snoc xs a = xs @ [a]"

proof (induct "xs")

show "snoc [] a = [] @ [a]"

proof -

have "snoc [] a = [a]" by simp

also have "… = [] @ [a]" by simp

finally show "snoc [] a = [] @ [a]" .

qed

fix b xs assume HI: "snoc xs a = xs @ [a]"

show "snoc (b # xs) a = (b # xs) @ [a]"

proof -

have "snoc (b # xs) a = b # (snoc xs a)" by simp

also have "… = b # (xs @ [a])" using HI by simp

also have "… = (b # xs) @ [a]" by simp

finally show "snoc (b # xs) a = (b # xs) @ [a]" .

qed

text {*

---------------------------------------------------------------------

Ejercicio 4. Demostrar automáticamente el siguiente lema

rev (x # xs) = snoc (rev xs) x"

---------------------------------------------------------------------

lemma "rev (x # xs) = snoc (rev xs) x"

by (auto simp add: snoc_append)

text {*

---------------------------------------------------------------------

Ejercicio 5. Demostrar detalladamente el siguiente lema

rev (x # xs) = snoc (rev xs) x"

---------------------------------------------------------------------

theorem "rev (x # xs) = snoc (rev xs) x"

proof -

have "rev (x # xs) = (rev xs) @ [x]" by simp

also have "… = snoc (rev xs) x" by (simp add:snoc_append)

finally show "rev (x # xs) = snoc (rev xs) x" .

qed

end

En la segunda parte hememos profundizado en el estudio de las demostraciones por casos y por inducción. En concreto, se ha estudiado

el razonamiento por casos booleanos,
el razonamiento por casos booleanos sobre una variable,
el razonamiento por casos sobre listas,
el razonamiento por inducción sobre números naturales con patrones,
el razonamiento sobre definiciones con existenciales,
el uso de librerías auxiliares (como Parity) y
el uso de otros métodos de domtración (como presburg).

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

header {* Tema 4: Razonamiento por casos y por inducción *}

theory T4_Razonamiento_por_casos_y_por_induccion
imports Main Parity
begin

text {*
  En este tema se amplían los métodos de demostración por casos y por
  inducción iniciados en el tema anterior.
*}

section {* Razonamiento por distinción de casos *}

subsection {* Distinción de casos booleanos *}

text {*
  Ejemplo de demostración por distinción de casos booleanos:
  Demostrar "¬A ∨ A".
*}

-- "La demostración estructurada es"
lemma "¬A ∨ A" 
proof cases
  assume "A" 
  then show "¬A ∨ A" ..
next
  assume "¬A" 
  then show "¬A ∨ A" ..
qed

text {*
  Comentarios de la demostración anterior:
  · "proof cases" indica que el método de demostración será por distinción de 
    casos. 
  · Se generan 2 casos:
       1. ?P ⟹ ¬A ∨ A
       2. ¬?P ⟹ ¬A ∨ A
    donde ?P es una variable sobre las fórmulas.
  · (assume "A") indica que se está usando "A" en lugar de la variable
    ?P.
  · "then" indica usando la fórmula anterior.
  · ".." indica usando la regla lógica necesaria (las reglas lógicas se
    estudiarán en los siguientes temas).
  · "next" indica el siguiente caso (se puede observar cómo ha
    sustituido ¬?P por ¬A.
*}

-- "La demostración automática es"
lemma "¬A ∨ A" 
by auto

text {*
  Ejemplo de demostración por distinción de casos booleanos con nombres: 
  Demostrar "¬A ∨ A".
*}

-- "La demostración estructurada es"
lemma "¬A ∨ A" 
proof (cases "A")
  case True 
  then show "¬A ∨ A" ..
next
  case False 
  thus "¬A ∨ A" .. 
qed

text {*
  Comentarios sobre la demostración anterior:
  · (cases "A") indica que la demostración se hará por casos según los
    distintos valores de "A".
  · Como "A" es una fórmula, sus posibles valores son verdadero o falso.
  · "case True" indica que se está suponiendo que A es verdadera. Es
    equivalente a "assume A".
  · "case False" indica que se está suponiendo que A es falsa. Es
    equivalente a "assume ¬A".
  · En general, 
    · el método (cases F) es una abreviatura de la aplicación de la regla
         ⟦F ⟹ Q; ¬F ⟹ Q⟧ ⟹ Q  
    · La expresión "case True" es una abreviatura de F.
    · La expresión "case False" es una abreviatura de ¬F.
  · Ventajas de "cases" con nombre: 
    · reduce la escritura de la fórmula y
    · es independiente del orden de los casos.
*}

subsection {* Distinción de casos sobre otros tipos de datos *}

text {*
  Ejemplo de distinción de casos sobre listas: 
  Demostrar que la longitud del resto de una lista es la longitud de la
  lista menos 1. 
*}

-- "La demostración detallada es"
lemma "length (tl xs) = length xs - 1" 
proof (cases xs)
  assume "xs = []"
  then show "length (tl xs) = length xs - 1" by simp
next
  fix y ys
  assume "xs = y#ys"
  then show "length(tl xs) = length xs - 1" by simp 
qed

text {*
  Comentarios sobre la demostración anterior:
  · "(cases xs)" indica que la demostración se hará por casos sobre los
    posibles valores de xs.
  · Como xs es una lista, sus posibles valores son la lista vacía ([]) o
    una lista no vacía (de la forma (y#ys)).
  · Se generan 2 casos:
       1. xs = [] ⟹ length (tl xs) = length xs - 1
       2. ⋀a list. xs = a # list ⟹ length (tl xs) = length xs - 1
*}

-- "La demostración simplificada es"
lemma "length (tl xs) = length xs - 1" 
proof (cases xs)
  case Nil 
  then show ?thesis by simp
next
  case Cons 
  then show ?thesis by simp 
qed

text {*
  Comentarios sobre la dmostración anterior:
  · "case Nil" es una abreviatura de 
       "assume xs =[]".
  · "case Cons" es una abreviatura de 
       "fix y ys assume xs = y#ys"
  · ?thesis es una abreviatura de la conclusión del lema.
*}

-- "La demostración automática es"
lemma "length (tl xs) = length xs - 1" 
by auto

text {*
  Een el siguiente ejemplo vamos a demostrar una propiedad de la función
  drop que está definida en la teoría List de forma que (drop n xs) la
  lista obtenida eliminando en xs} los n primeros elementos. Su
  definición es la siguiente   
     drop_Nil:  "drop n []     = []" 
     drop_Cons: "drop n (x#xs) = (case n of 
                                    0 => x#xs | 
                                    Suc(m) => drop m xs)"
*}

text {*
  Ejemplo de análisis de casos:
  Demostrar que el resultado de eliminar los n+1 primeros elementos de
  xs es el mismo que eliminar los n primeros elementos del resto de xs.  
*}

-- "La demostración detallada es"
lemma "drop (n + 1) xs = drop n (tl xs)"
proof (cases xs)
  case Nil 
  then show ?thesis by simp
next
  case Cons 
  then show ?thesis by simp
qed

-- "La demostración automática es"
lemma "drop (n + 1) xs = drop n (tl xs)"
by (cases xs) auto

section {* Inducción matemática *}

text {*
  [Principio de inducción matemática]
  Para demostrar una propiedad P para todos los números naturales basta
  probar que el 0 tiene la propiedad P y que si n tiene la propiedad P,
  entonces n+1 también la tiene. 
     ⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P m

  En Isabelle el principio de inducción matemática está formalizado en
  el teorema nat.induct y puede verse con
     thm nat.induct
*}

text {*  
  Ejemplo de demostración por inducción: Usaremos el principio de
  inducción matemática para demostrar que 
     1 + 3 + ... + (2n-1) = n^2

  Definición. [Suma de los primeros impares] 
  (suma_impares n) la suma de los n números impares. Por ejemplo,
     suma_impares 3  =  9
*}

fun suma_impares :: "nat ⇒ nat" where
  "suma_impares 0 = 0" 
| "suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n"

value "suma_impares 3"

text {*
  Ejemplo de demostración por inducción matemática:
  Demostrar que la suma de los n primeros números impares es n^2.
*}

-- "Demostración del lema anterior por inducción y razonamiento ecuacional"
lemma "suma_impares n = n * n"
proof (induct n)
  show "suma_impares 0 = 0 * 0" by simp
next
  fix n assume HI: "suma_impares n = n * n"
  have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n" by simp
  also have "… = (2 * (Suc n) - 1) + n * n" using HI by simp
  also have "… = n * n + 2 * n + 1" by simp
  finally show "suma_impares (Suc n) = (Suc n) * (Suc n)" by simp
qed

-- "Demostración del lema anterior con patrones y razonamiento ecuacional"
lemma "suma_impares n = n * n" (is "?P n")
proof (induct n)
  show "?P 0" by simp
next
  fix n 
  assume HI: "?P n"
  have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n" by simp
  also have "… = (2 * (Suc n) - 1) + n * n" using HI by simp
  also have "… = n * n + 2 * n + 1" by simp
  finally show "?P (Suc n)" by simp
qed

text {*
  Comentario sobre la demostración anterior:
  · Con la expresión
       "suma_impares n = n * n" (is "?P n")
    se abrevia "suma_impares n = n * n" como "?P n". Por tanto, 
       "?P 0"       es una abreviatura de "suma_impares 0 = 0 * 0"
       "?P (Suc n)" es una abreviatura de "suma_impares (Suc n) = (Suc n) * (Suc n)"
  · En general, cualquier fórmula seguida de (is patrón) equipara el
    patrón con la fórmula. 
*}

-- "La demostración usando patrones es"
lemma "suma_impares n = n * n" (is "?P n")
proof (induct n)
  show "?P 0" by simp
next
  fix n 
  assume "?P n"
  then show "?P (Suc n)" by simp
qed

-- "La demostración automática es"
lemma "suma_impares n = n * n"
by (induct n) auto


text {* 
  Ejemplo de definición con existenciales. 
  Un número natural n es par si existe un natural m tal que n=m+m.   
*}

definition par :: "nat ⇒ bool" where
  "par n ≡ ∃m. n=m+m"

text {* 
  Ejemplo de inducción y existenciales: 
  Demostrar que para todo número natural n, se verifica que n*(n+1) par. 
*}

-- "Demostración detallada por inducción"
lemma 
  fixes n :: "nat"
  shows "par (n*(n+1))"
proof (induct n)
  show "par (0*(0+1))" by (simp add: par_def)
next
  fix n 
  assume "par (n*(n+1))"
  then have "∃m. n*(n+1) = m+m" by (simp add:par_def)
  then obtain m where m: "n*(n+1) = m+m" ..
  then have "(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)" by auto
  then have "∃m. (Suc n)*((Suc n)+1) = m+m" ..
  then show "par ((Suc n)*((Suc n)+1))" by (simp add:par_def)
qed

text {*
  Comentarios sobre la demostración anterior:
  · (fixes n :: "nat") es una abreviatura de "sea n un número natural".
*}

text {*
  En Isabelle puede demostrarse de manera más simple un lema equivalente
  usando en lugar de la función "par" la función "even" definida en la
  teoría Parity por
     even x ⟷ x mod 2 = 0"
*}

lemma 
  fixes n :: "nat"
  shows "even (n*(n+1))"
by auto

text {*
  Comentarios sobre la demostración anterior:
  · Para poder usar la función "even" de la librería Parity es necesario
    importar dicha librería. Por ello, anter del inicio de la teoría aparece
       imports Main Parity
*}

text {*
  Para completar la demostración basta demostrar la equivalencia de las
  funciones "par" y "even". 
*}

lemma 
  fixes n :: "nat"
  shows "par n = even n"
proof - 
  have "par n = (∃m. n = m+m)" by (simp add:par_def)
  then show "par n = even n" by presburger
qed

text {*
  Comentarios sobre la demostración anterior:
  · "by presburger" indica que se use como método de demostración el
    algoritmo de decisión de la aritmética de Presburger.
*}

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

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

287

288

289

290

291

292

293

294

295

296

297

298

299

300

301

302

303

304

305

306

307

308

309

310

311

312

313

314

315

316

317

318

319

320

321

322

323

324

325

326

327

328

header {* Tema 4: Razonamiento por casos y por inducción *}

theory T4_Razonamiento_por_casos_y_por_induccion

imports Main Parity

begin

text {*

En este tema se amplían los métodos de demostración por casos y por

inducción iniciados en el tema anterior.

section {* Razonamiento por distinción de casos *}

subsection {* Distinción de casos booleanos *}

text {*

Ejemplo de demostración por distinción de casos booleanos:

Demostrar "¬A ∨ A".

-- "La demostración estructurada es"

lemma "¬A ∨ A"

proof cases

assume "A"

then show "¬A ∨ A" ..

assume "¬A"

then show "¬A ∨ A" ..

qed

text {*

Comentarios de la demostración anterior:

· "proof cases" indica que el método de demostración será por distinción de

casos.

· Se generan 2 casos:

1. ?P ⟹ ¬A ∨ A

2. ¬?P ⟹ ¬A ∨ A

donde ?P es una variable sobre las fórmulas.

· (assume "A") indica que se está usando "A" en lugar de la variable

?P.

· "then" indica usando la fórmula anterior.

· ".." indica usando la regla lógica necesaria (las reglas lógicas se

estudiarán en los siguientes temas).

· "next" indica el siguiente caso (se puede observar cómo ha

sustituido ¬?P por ¬A.

-- "La demostración automática es"

lemma "¬A ∨ A"

by auto

text {*

Ejemplo de demostración por distinción de casos booleanos con nombres:

Demostrar "¬A ∨ A".

-- "La demostración estructurada es"

lemma "¬A ∨ A"

proof (cases "A")

case True

then show "¬A ∨ A" ..

case False

thus "¬A ∨ A" ..

qed

text {*

Comentarios sobre la demostración anterior:

· (cases "A") indica que la demostración se hará por casos según los

distintos valores de "A".

· Como "A" es una fórmula, sus posibles valores son verdadero o falso.

· "case True" indica que se está suponiendo que A es verdadera. Es

equivalente a "assume A".

· "case False" indica que se está suponiendo que A es falsa. Es

equivalente a "assume ¬A".

· En general,

· el método (cases F) es una abreviatura de la aplicación de la regla

⟦F ⟹ Q; ¬F ⟹ Q⟧ ⟹ Q

· La expresión "case True" es una abreviatura de F.

· La expresión "case False" es una abreviatura de ¬F.

· Ventajas de "cases" con nombre:

· reduce la escritura de la fórmula y

· es independiente del orden de los casos.

subsection {* Distinción de casos sobre otros tipos de datos *}

text {*

Ejemplo de distinción de casos sobre listas:

Demostrar que la longitud del resto de una lista es la longitud de la

lista menos 1.

-- "La demostración detallada es"

lemma "length (tl xs) = length xs - 1"

proof (cases xs)

assume "xs = []"

then show "length (tl xs) = length xs - 1" by simp

fix y ys

assume "xs = y#ys"

then show "length(tl xs) = length xs - 1" by simp

qed

text {*

Comentarios sobre la demostración anterior:

· "(cases xs)" indica que la demostración se hará por casos sobre los

posibles valores de xs.

· Como xs es una lista, sus posibles valores son la lista vacía ([]) o

una lista no vacía (de la forma (y#ys)).

· Se generan 2 casos:

1. xs = [] ⟹ length (tl xs) = length xs - 1

2. ⋀a list. xs = a # list ⟹ length (tl xs) = length xs - 1

-- "La demostración simplificada es"

lemma "length (tl xs) = length xs - 1"

proof (cases xs)

case Nil

then show ?thesis by simp

case Cons

then show ?thesis by simp

qed

text {*

Comentarios sobre la dmostración anterior:

· "case Nil" es una abreviatura de

"assume xs =[]".

· "case Cons" es una abreviatura de

"fix y ys assume xs = y#ys"

· ?thesis es una abreviatura de la conclusión del lema.

-- "La demostración automática es"

lemma "length (tl xs) = length xs - 1"

by auto

text {*

Een el siguiente ejemplo vamos a demostrar una propiedad de la función

drop que está definida en la teoría List de forma que (drop n xs) la

lista obtenida eliminando en xs} los n primeros elementos. Su

definición es la siguiente

drop_Nil: "drop n [] = []"

drop_Cons: "drop n (x#xs) = (case n of

0 => x#xs |

Suc(m) => drop m xs)"

text {*

Ejemplo de análisis de casos:

Demostrar que el resultado de eliminar los n+1 primeros elementos de

xs es el mismo que eliminar los n primeros elementos del resto de xs.

-- "La demostración detallada es"

lemma "drop (n + 1) xs = drop n (tl xs)"

proof (cases xs)

case Nil

then show ?thesis by simp

case Cons

then show ?thesis by simp

qed

-- "La demostración automática es"

lemma "drop (n + 1) xs = drop n (tl xs)"

by (cases xs) auto

section {* Inducción matemática *}

text {*

[Principio de inducción matemática]

Para demostrar una propiedad P para todos los números naturales basta

probar que el 0 tiene la propiedad P y que si n tiene la propiedad P,

entonces n+1 también la tiene.

⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P m

En Isabelle el principio de inducción matemática está formalizado en

el teorema nat.induct y puede verse con

thm nat.induct

text {*

Ejemplo de demostración por inducción: Usaremos el principio de

inducción matemática para demostrar que

1 + 3 + ... + (2n-1) = n^2

Definición. [Suma de los primeros impares]

(suma_impares n) la suma de los n números impares. Por ejemplo,

suma_impares 3 = 9

fun suma_impares :: "nat ⇒ nat" where

"suma_impares 0 = 0"

| "suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n"

value "suma_impares 3"

text {*

Ejemplo de demostración por inducción matemática:

Demostrar que la suma de los n primeros números impares es n^2.

-- "Demostración del lema anterior por inducción y razonamiento ecuacional"

lemma "suma_impares n = n * n"

proof (induct n)

show "suma_impares 0 = 0 * 0" by simp

fix n assume HI: "suma_impares n = n * n"

have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n" by simp

also have "… = (2 * (Suc n) - 1) + n * n" using HI by simp

also have "… = n * n + 2 * n + 1" by simp

finally show "suma_impares (Suc n) = (Suc n) * (Suc n)" by simp

qed

-- "Demostración del lema anterior con patrones y razonamiento ecuacional"

lemma "suma_impares n = n * n" (is "?P n")

proof (induct n)

show "?P 0" by simp

fix n

assume HI: "?P n"

have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n" by simp

also have "… = (2 * (Suc n) - 1) + n * n" using HI by simp

also have "… = n * n + 2 * n + 1" by simp

finally show "?P (Suc n)" by simp

qed

text {*

Comentario sobre la demostración anterior:

· Con la expresión

"suma_impares n = n * n" (is "?P n")

se abrevia "suma_impares n = n * n" como "?P n". Por tanto,

"?P 0" es una abreviatura de "suma_impares 0 = 0 * 0"

"?P (Suc n)" es una abreviatura de "suma_impares (Suc n) = (Suc n) * (Suc n)"

· En general, cualquier fórmula seguida de (is patrón) equipara el

patrón con la fórmula.

-- "La demostración usando patrones es"

lemma "suma_impares n = n * n" (is "?P n")

proof (induct n)

show "?P 0" by simp

fix n

assume "?P n"

then show "?P (Suc n)" by simp

qed

-- "La demostración automática es"

lemma "suma_impares n = n * n"

by (induct n) auto

text {*

Ejemplo de definición con existenciales.

Un número natural n es par si existe un natural m tal que n=m+m.

definition par :: "nat ⇒ bool" where

"par n ≡ ∃m. n=m+m"

text {*

Ejemplo de inducción y existenciales:

Demostrar que para todo número natural n, se verifica que n*(n+1) par.

-- "Demostración detallada por inducción"

lemma

fixes n :: "nat"

shows "par (n*(n+1))"

proof (induct n)

show "par (0*(0+1))" by (simp add: par_def)

fix n

assume "par (n*(n+1))"

then have "∃m. n*(n+1) = m+m" by (simp add:par_def)

then obtain m where m: "n*(n+1) = m+m" ..

then have "(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)" by auto

then have "∃m. (Suc n)*((Suc n)+1) = m+m" ..

then show "par ((Suc n)*((Suc n)+1))" by (simp add:par_def)

qed

text {*

Comentarios sobre la demostración anterior:

· (fixes n :: "nat") es una abreviatura de "sea n un número natural".

text {*

En Isabelle puede demostrarse de manera más simple un lema equivalente

usando en lugar de la función "par" la función "even" definida en la

teoría Parity por

even x ⟷ x mod 2 = 0"

lemma

fixes n :: "nat"

shows "even (n*(n+1))"

by auto

text {*

Comentarios sobre la demostración anterior:

· Para poder usar la función "even" de la librería Parity es necesario

importar dicha librería. Por ello, anter del inicio de la teoría aparece

imports Main Parity

text {*

Para completar la demostración basta demostrar la equivalencia de las

funciones "par" y "even".

lemma

fixes n :: "nat"

shows "par n = even n"

proof -

have "par n = (∃m. n = m+m)" by (simp add:par_def)

then show "par n = even n" by presburger

qed

text {*

Comentarios sobre la demostración anterior:

· "by presburger" indica que se use como método de demostración el

algoritmo de decisión de la aritmética de Presburger.

end

Como tarea para la próxima clase se propuso la resolución de los ejercicios de la relación 5.

Se puede imprimir o compartir con