RA2014: Razonamiento sobre tipos recursivos en Isabelle/HOL

En la tercera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado

cómo definir árboles binarios en Isabelle/HOL y cómo demostrar sus propiedades,
cómo definir y razonar con funciones recursivas que no son primitivas recursivas y
cómo definir y razonar con tipos de datos mutuamente recursivos.

La correspondiente teoría Isabelle/HOL se muestra a continuación

theory T4b
imports Main
begin

text {* 
  Ejemplo de definición de tipos recursivos:
  Definir un tipo de dato para los árboles binarios.
*}

datatype 'a arbolB = Hoja "'a" 
                   | Nodo "'a" "'a arbolB" "'a arbolB"

text {* 
  Ejemplo de definición sobre árboles binarios:
  Definir la función "espejo" que aplicada a un árbol devuelve su imagen
  especular.  
*}

fun espejo :: "'a arbolB ⇒ 'a arbolB" where
  "espejo (Hoja x) = (Hoja x)"
| "espejo (Nodo x i d) = (Nodo x (espejo d) (espejo i))"

value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))"
-- "= Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))"

text {* 
  Ejemplo de demostración sobre árboles binarios:
  Demostrar que la función "espejo" es involutiva; es decir, para
  cualquier árbol a, se tiene que 
     espejo(espejo(a)) = a.
*}

-- "La demostración estructurada es"
lemma espejo_involutiva:
  fixes a :: "'b arbolB" 
  shows "espejo (espejo a) = a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (Hoja x)" by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "espejo(espejo(Nodo x i d)) = espejo(Nodo x (espejo d) (espejo i))"
      by simp
    also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" by simp
    also have "… = Nodo x i d" using h1 h2 by simp 
    finally show ?thesis .
 qed
qed

text {*
  Comentarios sobre la demostración anterior:
  · (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario
    cuyos elementos son de tipo b". 
  · (induct a) indica que el método de demostración es por inducción
    en el árbol binario a.
  · Se generan dos casos:
    1. ⋀a. espejo (espejo (Hoja a)) = Hoja a
    2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2; 
                   espejo (espejo a3) = a3⟧
                  ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3
*}

-- "La demostración automática es"
lemma espejo_involutiva_1: 
  "espejo (espejo a ) = a"
by (induct a) auto

text {* 
  Ejemplo. [Aplanamiento de árboles]
  Definir la función "aplana" que aplane los árboles recorriéndolos en
  orden infijo.  
*}

fun aplana :: "'a arbolB ⇒ 'a list" where
  "aplana (Hoja x)     = [x]"
| "aplana (Nodo x i d) = (aplana i) @ [x] @ (aplana d)"

value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))"
-- "= [c, b, d, a, e]"

text {* 
  Ejemplo. [Aplanamiento de la imagen especular] Demostrar que
     aplana (espejo a) = rev (aplana a)
*}

-- "La demostración estructurada es"
lemma 
  fixes a :: "'b arbolB"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (Hoja x)" by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "aplana (espejo (Nodo x i d)) = 
          aplana (Nodo x (espejo d) (espejo i))" by simp
    also have "… = (aplana(espejo d))@[x]@(aplana(espejo i))" by simp
    also have "… = (rev(aplana d))@[x]@(rev(aplana i))" using h1 h2 by simp
    also have "… = rev((aplana i)@[x]@(aplana d))" by simp
    also have "… = rev(aplana (Nodo x i d))" by simp
    finally show ?thesis .
 qed
qed

-- "La demostración automática es"
lemma "aplana (espejo a) = rev (aplana a)"
by (induct a) auto

section {* Heurísticas para la inducción *}

text {*
  Definición. [Definición recursiva de inversa]
  (inversa xs) la inversa de la lista xs. Por ejemplo,
     inversa [a,b,c] = [c,b,a] 
*}

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

value "inversa [a,b,c]"

text {* 
  Definición. [Definición de inversa con acumuladores]
  (inversaAc xs) es la inversa de la lista xs calculada con
  acumuladores. Por ejemplo,
     inversaAc [a,b,c]       = [c,b,a] 
     inversaAcAux [a,b,c] [] = [c,b,a] 
*}

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

definition inversaAc :: "'a list ⇒ 'a list" where
  "inversaAc xs ≡ inversaAcAux xs []"

value "inversaAcAux [a,b,c] []"
value "inversaAc [a,b,c]"

text {* 
  Lema. [Ejemplo de equivalencia entre las definiciones]
  La inversa de [a,b,c] es lo mismo calculada con la primera definición
  que con la segunda.
*}

lemma "inversaAc [a,b,c] = inversa [a,b,c]"
by (simp add: inversaAc_def)

text {*
  Nota. [Ejemplo fallido de demostración por inducción]
  El siguiente intento de demostrar que para cualquier lista xs, se
  tiene que  "inversaAc xs = inversa xs" falla.
*}

lemma "inversaAc xs = inversa xs"
proof (induct xs)
  show "inversaAc [] = inversa []" by (simp add: inversaAc_def)
next
  fix a xs assume HI: "inversaAc xs = inversa xs"
  have "inversaAc (a#xs) = inversaAcAux (a#xs) []" by (simp add: inversaAc_def)
  also have "… = inversaAcAux xs [a]" by simp
  also have "… = inversa (a#xs)"
  -- "Problema: la hipótesis de inducción no es aplicable."
oops

text {* 
  Nota. [Heurística de generalización]
  Cuando se use demostración estructural, cuantificar universalmente las 
  variables libres (o, equivalentemente, considerar las variables libres
  como variables arbitrarias).

  Lema. [Lema con generalización]
  Para toda lista ys se tiene 
     inversaAcAux xs ys = (inversa xs) @ ys
*}

-- "La demostración estructurada es"
lemma inversaAcAux_es_inversa:
  "inversaAcAux xs ys = (inversa xs)@ys"
proof (induct xs arbitrary: ys)
  show "⋀ys. inversaAcAux [] ys = (inversa [])@ys" by simp
next
  fix a xs 
  assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"
  show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"
  proof -
    fix ys
    have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" by simp
    also have "… = inversa xs@(a#ys)" using HI by simp
    also have "… = inversa (a#xs)@ys" using [[simp_trace]] by simp 
    finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp
  qed
qed

-- "La demostración automática es"
lemma inversaAcAux_es_inversa_1:
  "inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

text {*
  Corolario.  Para cualquier lista xs, se tiene que
     inversaAc xs = inversa xs
*}

corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa inversaAc_def)

text {*
  Nota. En el paso "inversa xs@(a#ys) = inversa (a#xs)@ys" se usan
  lemas de la teoría List. Se puede observar, insertano 
     using [[simp_trace]]
  entre la igualdad y by simp, que los lemas usados son 
  · List.append_simps_1: []@ys = ys
  · List.append_simps_2: (x#xs)@ys = x#(xs@ys)
  · List.append_assoc:   (xs @ ys) @ zs = xs @ (ys @ zs)
  Las dos primeras son las ecuaciones de la definición de append.

  En la siguiente demostración se detallan los lemas utilizados.
*}

lemma "(inversa xs)@(a#ys) = (inversa (a#xs))@ys"
proof -
  have "(inversa xs)@(a#ys) = (inversa xs)@(a#([]@ys))" 
    by (simp only: append.simps(1))
  also have "… = (inversa xs)@([a]@ys)" by (simp only: append.simps(2))
  also have "… = ((inversa xs)@[a])@ys" by (simp only: append_assoc)
  also have "… = (inversa (a#xs))@ys" by (simp only: inversa.simps(2))
  finally show ?thesis .
qed

section {* Recursión general. La función de Ackermann *}

text {* 
  El objetivo de esta sección es mostrar el uso de las definiciones
  recursivas generales y sus esquemas de inducción. Como ejemplo se usa la
  función de Ackermann (se puede consultar información sobre dicha función en
  http://en.wikipedia.org/wiki/Ackermann_function).

  Definición.  La función de Ackermann se define por
    A(m,n) = n+1,             si m=0,
             A(m-1,1),        si m>0 y n=0,
             A(m-1,A(m,n-1)), si m>0 y n>0
  para todo los números naturales. 

  La función de Ackermann es recursiva, pero no es primitiva recursiva. 
*}

fun ack :: "nat ⇒ nat ⇒ nat" where
  "ack 0       n       = n+1" 
| "ack (Suc m) 0       = ack m 1" 
| "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"

-- "Ejemplo de evaluación"
value "ack 2 3" (* devuelve 9 *)

text {*
  Esquema de inducción correspondiente a una función:
  · Al definir una función recursiva general se genera una regla de
    inducción. En la definición anterior, la regla generada es
    ack.induct: 
       ⟦⋀n. P 0 n; 
        ⋀m. P m 1 ⟹ P (Suc m) 0;
        ⋀m n. ⟦P (Suc m) n; P m (ack (Suc m) n)⟧ ⟹ P (Suc m) (Suc n)⟧
       ⟹ P a b
*}

text {*
  Ejemplo de demostración por la inducción correspondiente a una función:
  Demostrar que para todos m y n, A(m,n) > n.
*} 

-- "La demostración detallada es"
lemma "ack m n > n"
proof (induct m n rule: ack.induct)
  fix n
  show "ack 0 n > n" by simp
next
  fix m 
  assume "ack m 1 > 1"
  then show "ack (Suc m) 0 > 0" by simp
next  
  fix m n
  assume "n < ack (Suc m) n" and 
         "ack (Suc m) n < ack m (ack (Suc m) n)"
  then show "Suc n < ack (Suc m) (Suc n)" by simp
qed

text {*
  Comentarios sobre la demostración anterior:
  · (induct m n rule: ack.induct) indica que el método de demostración
    es el esquema de recursión correspondiente a la definición de 
    (ack m n).
  · Se generan 3 casos:
    1. ⋀n. n < ack 0 n
    2. ⋀m. 1 < ack m 1 ⟹ 0 < ack (Suc m) 0
    3. ⋀m n. ⟦n < ack (Suc m) n; 
              ack (Suc m) n < ack m (ack (Suc m) n)⟧
             ⟹ Suc n < ack (Suc m) (Suc n)
*}

-- "La demostración automática es"
lemma "ack m n > n"
by (induct m n rule: ack.induct) auto

section {* Recursión mutua e inducción *}

text {*
  Nota. [Ejemplo de definición de tipos mediante recursión cruzada]
  · Un árbol de tipo a es una hoja o un nodo de tipo a junto con un
    bosque de tipo a.
  · Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo
    un árbol de tipo a a un bosque de tipo a.
*}

datatype 'a arbol = Hoja | Nodo "'a" "'a bosque"
     and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"

text {*
  Regla de inducción correspondiente a la recursión cruzada:
  La regla de inducción sobre árboles y bosques es arbol_bosque.induct:
     ⟦P1 Hoja; 
      ⋀x b. P2 b ⟹ P1 (Nodo x b); 
      P2 Vacio;
      ⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧ 
     ⟹ P1 a ∧ P2 b
*}

text {* 
  Ejemplos de definición por recursión cruzada:
  · aplana_arbol a) es la lista obtenida aplanando el árbol a.   
  · (aplana_bosque b) es la lista obtenida aplanando el bosque b.   
  · (map_arbol a h) es el árbol obtenido aplicando la función h a
    todos los nodos del árbol a.   
  · (map_bosque b h) es el bosque obtenido aplicando la función h a
    todos los nodos del bosque b. 
*}

fun aplana_arbol :: "'a arbol ⇒ 'a list" and 
    aplana_bosque :: "'a bosque ⇒ 'a list" where
  "aplana_arbol Hoja = []"
| "aplana_arbol (Nodo x b) = x#(aplana_bosque b)"
| "aplana_bosque Vacio = []"
| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)"

fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and
    map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where
  "map_arbol  f Hoja        = Hoja"
| "map_arbol  f (Nodo x b)  = Nodo (f x) (map_bosque f b)"
| "map_bosque f Vacio       = Vacio"
| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)"

text {*
  Ejemplo de demostración por inducción cruzada:
  Demostrar que:
  · aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
  · aplana_bosque (map_bosque f b) = map f (aplana_bosque b)
*}

-- "La demostración detallada es"
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
  show "aplana_arbol (map_arbol f Hoja ) = map f (aplana_arbol Hoja)" 
    by simp
next
  fix x b
  assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_arbol (map_arbol f (Nodo x b)) = 
        aplana_arbol (Nodo (f x) (map_bosque f b))" by simp
  also have "… = (f x)#(aplana_bosque (map_bosque f b))" by simp
  also have "… = (f x)#(map f (aplana_bosque b))" using HI by simp
  also have "… = map f (aplana_arbol (Nodo x b))" by simp
  finally show "aplana_arbol (map_arbol f (Nodo x b))
                = map f (aplana_arbol (Nodo x b))" .
next
  show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" 
    by simp
next
  fix a b
  assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
     and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_bosque (map_bosque f (ConsB a b)) = 
        aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp
  also have "… = aplana_arbol(map_arbol f a)@aplana_bosque(map_bosque f b)" 
    by simp
  also have "… = (map f (aplana_arbol a))@(map f (aplana_bosque b))" 
    using HI1 HI2 by simp
  also have "… = map f (aplana_bosque (ConsB a b))" by simp
  finally show "aplana_bosque (map_bosque f (ConsB a b)) 
                = map f (aplana_bosque (ConsB a b))" by simp
qed

text {*
  Comentarios sobre la demostración anterior:
  · (induct_tac a and b) indica que el método de demostración es por
    inducción cruzada sobre a y b.
  · Se generan 4 casos:
    1. aplana_arbol (map_arbol arbol.Hoja h) = map h (aplana_arbol arbol.Hoja)
    2. ⋀a bosque.
          aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹
          aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =
          map h (aplana_arbol (arbol.Nodo a bosque))
    3. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)
    4. ⋀arbol bosque.
          ⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);
           aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧
          ⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =
             map h (aplana_bosque (ConsB arbol bosque))
*}

-- "La demostración automática es"
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
by (induct_tac a and b) auto

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

329

330

331

332

333

334

335

336

337

338

339

340

341

342

343

344

345

346

347

348

349

350

351

352

353

354

355

356

357

358

359

360

361

362

363

364

365

366

367

368

369

370

371

372

373

374

375

376

377

378

379

380

381

382

383

384

385

386

387

388

389

390

391

392

393

394

395

396

397

398

399

400

401

402

403

404

405

406

407

408

409

410

411

412

413

414

415

416

417

418

419

420

421

422

423

424

425

theory T4b

imports Main

begin

text {*

Ejemplo de definición de tipos recursivos:

Definir un tipo de dato para los árboles binarios.

datatype 'a arbolB = Hoja "'a"

| Nodo "'a" "'a arbolB" "'a arbolB"

text {*

Ejemplo de definición sobre árboles binarios:

Definir la función "espejo" que aplicada a un árbol devuelve su imagen

especular.

fun espejo :: "'a arbolB ⇒ 'a arbolB" where

"espejo (Hoja x) = (Hoja x)"

| "espejo (Nodo x i d) = (Nodo x (espejo d) (espejo i))"

value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))"

-- "= Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))"

text {*

Ejemplo de demostración sobre árboles binarios:

Demostrar que la función "espejo" es involutiva; es decir, para

cualquier árbol a, se tiene que

espejo(espejo(a)) = a.

-- "La demostración estructurada es"

lemma espejo_involutiva:

fixes a :: "'b arbolB"

shows "espejo (espejo a) = a" (is "?P a")

proof (induct a)

fix x

show "?P (Hoja x)" by simp

fix x

fix i assume h1: "?P i"

fix d assume h2: "?P d"

show "?P (Nodo x i d)"

proof -

have "espejo(espejo(Nodo x i d)) = espejo(Nodo x (espejo d) (espejo i))"

by simp

also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" by simp

also have "… = Nodo x i d" using h1 h2 by simp

finally show ?thesis .

qed

text {*

Comentarios sobre la demostración anterior:

· (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario

cuyos elementos son de tipo b".

· (induct a) indica que el método de demostración es por inducción

en el árbol binario a.

· Se generan dos casos:

1. ⋀a. espejo (espejo (Hoja a)) = Hoja a

2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2;

espejo (espejo a3) = a3⟧

⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3

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

lemma espejo_involutiva_1:

"espejo (espejo a ) = a"

by (induct a) auto

text {*

Ejemplo. [Aplanamiento de árboles]

Definir la función "aplana" que aplane los árboles recorriéndolos en

orden infijo.

fun aplana :: "'a arbolB ⇒ 'a list" where

"aplana (Hoja x) = [x]"

| "aplana (Nodo x i d) = (aplana i) @ [x] @ (aplana d)"

value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))"

-- "= [c, b, d, a, e]"

text {*

Ejemplo. [Aplanamiento de la imagen especular] Demostrar que

aplana (espejo a) = rev (aplana a)

-- "La demostración estructurada es"

lemma

fixes a :: "'b arbolB"

shows "aplana (espejo a) = rev (aplana a)" (is "?P a")

proof (induct a)

fix x

show "?P (Hoja x)" by simp

fix x

fix i assume h1: "?P i"

fix d assume h2: "?P d"

show "?P (Nodo x i d)"

proof -

have "aplana (espejo (Nodo x i d)) =

aplana (Nodo x (espejo d) (espejo i))" by simp

also have "… = (aplana(espejo d))@[x]@(aplana(espejo i))" by simp

also have "… = (rev(aplana d))@[x]@(rev(aplana i))" using h1 h2 by simp

also have "… = rev((aplana i)@[x]@(aplana d))" by simp

also have "… = rev(aplana (Nodo x i d))" by simp

finally show ?thesis .

qed

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

lemma "aplana (espejo a) = rev (aplana a)"

by (induct a) auto

section {* Heurísticas para la inducción *}

text {*

Definición. [Definición recursiva de inversa]

(inversa xs) la inversa de la lista xs. Por ejemplo,

inversa [a,b,c] = [c,b,a]

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

"inversa [] = []"

| "inversa (x#xs) = (inversa xs) @ [x]"

value "inversa [a,b,c]"

text {*

Definición. [Definición de inversa con acumuladores]

(inversaAc xs) es la inversa de la lista xs calculada con

acumuladores. Por ejemplo,

inversaAc [a,b,c] = [c,b,a]

inversaAcAux [a,b,c] [] = [c,b,a]

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

"inversaAcAux [] ys = ys"

| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

definition inversaAc :: "'a list ⇒ 'a list" where

"inversaAc xs ≡ inversaAcAux xs []"

value "inversaAcAux [a,b,c] []"

value "inversaAc [a,b,c]"

text {*

Lema. [Ejemplo de equivalencia entre las definiciones]

La inversa de [a,b,c] es lo mismo calculada con la primera definición

que con la segunda.

lemma "inversaAc [a,b,c] = inversa [a,b,c]"

by (simp add: inversaAc_def)

text {*

Nota. [Ejemplo fallido de demostración por inducción]

El siguiente intento de demostrar que para cualquier lista xs, se

tiene que "inversaAc xs = inversa xs" falla.

lemma "inversaAc xs = inversa xs"

proof (induct xs)

show "inversaAc [] = inversa []" by (simp add: inversaAc_def)

fix a xs assume HI: "inversaAc xs = inversa xs"

have "inversaAc (a#xs) = inversaAcAux (a#xs) []" by (simp add: inversaAc_def)

also have "… = inversaAcAux xs [a]" by simp

also have "… = inversa (a#xs)"

-- "Problema: la hipótesis de inducción no es aplicable."

oops

text {*

Nota. [Heurística de generalización]

Cuando se use demostración estructural, cuantificar universalmente las

variables libres (o, equivalentemente, considerar las variables libres

como variables arbitrarias).

Lema. [Lema con generalización]

Para toda lista ys se tiene

inversaAcAux xs ys = (inversa xs) @ ys

-- "La demostración estructurada es"

lemma inversaAcAux_es_inversa:

"inversaAcAux xs ys = (inversa xs)@ys"

proof (induct xs arbitrary: ys)

show "⋀ys. inversaAcAux [] ys = (inversa [])@ys" by simp

fix a xs

assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"

show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"

proof -

fix ys

have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" by simp

also have "… = inversa xs@(a#ys)" using HI by simp

also have "… = inversa (a#xs)@ys" using [[simp_trace]] by simp

finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp

qed

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

lemma inversaAcAux_es_inversa_1:

"inversaAcAux xs ys = (inversa xs)@ys"

by (induct xs arbitrary: ys) auto

text {*

Corolario. Para cualquier lista xs, se tiene que

inversaAc xs = inversa xs

corollary "inversaAc xs = inversa xs"

by (simp add: inversaAcAux_es_inversa inversaAc_def)

text {*

Nota. En el paso "inversa xs@(a#ys) = inversa (a#xs)@ys" se usan

lemas de la teoría List. Se puede observar, insertano

using [[simp_trace]]

entre la igualdad y by simp, que los lemas usados son

· List.append_simps_1: []@ys = ys

· List.append_simps_2: (x#xs)@ys = x#(xs@ys)

· List.append_assoc: (xs @ ys) @ zs = xs @ (ys @ zs)

Las dos primeras son las ecuaciones de la definición de append.

En la siguiente demostración se detallan los lemas utilizados.

lemma "(inversa xs)@(a#ys) = (inversa (a#xs))@ys"

proof -

have "(inversa xs)@(a#ys) = (inversa xs)@(a#([]@ys))"

by (simp only: append.simps(1))

also have "… = (inversa xs)@([a]@ys)" by (simp only: append.simps(2))

also have "… = ((inversa xs)@[a])@ys" by (simp only: append_assoc)

also have "… = (inversa (a#xs))@ys" by (simp only: inversa.simps(2))

finally show ?thesis .

qed

section {* Recursión general. La función de Ackermann *}

text {*

El objetivo de esta sección es mostrar el uso de las definiciones

recursivas generales y sus esquemas de inducción. Como ejemplo se usa la

función de Ackermann (se puede consultar información sobre dicha función en

http://en.wikipedia.org/wiki/Ackermann_function).

Definición. La función de Ackermann se define por

A(m,n) = n+1, si m=0,

A(m-1,1), si m>0 y n=0,

A(m-1,A(m,n-1)), si m>0 y n>0

para todo los números naturales.

La función de Ackermann es recursiva, pero no es primitiva recursiva.

fun ack :: "nat ⇒ nat ⇒ nat" where

"ack 0 n = n+1"

| "ack (Suc m) 0 = ack m 1"

| "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"

-- "Ejemplo de evaluación"

value "ack 2 3" (* devuelve 9 *)

text {*

Esquema de inducción correspondiente a una función:

· Al definir una función recursiva general se genera una regla de

inducción. En la definición anterior, la regla generada es

ack.induct:

⟦⋀n. P 0 n;

⋀m. P m 1 ⟹ P (Suc m) 0;

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

⟹ P a b

text {*

Ejemplo de demostración por la inducción correspondiente a una función:

Demostrar que para todos m y n, A(m,n) > n.

-- "La demostración detallada es"

lemma "ack m n > n"

proof (induct m n rule: ack.induct)

fix n

show "ack 0 n > n" by simp

fix m

assume "ack m 1 > 1"

then show "ack (Suc m) 0 > 0" by simp

fix m n

assume "n < ack (Suc m) n" and

"ack (Suc m) n < ack m (ack (Suc m) n)"

then show "Suc n < ack (Suc m) (Suc n)" by simp

qed

text {*

Comentarios sobre la demostración anterior:

· (induct m n rule: ack.induct) indica que el método de demostración

es el esquema de recursión correspondiente a la definición de

(ack m n).

· Se generan 3 casos:

1. ⋀n. n < ack 0 n

2. ⋀m. 1 < ack m 1 ⟹ 0 < ack (Suc m) 0

3. ⋀m n. ⟦n < ack (Suc m) n;

ack (Suc m) n < ack m (ack (Suc m) n)⟧

⟹ Suc n < ack (Suc m) (Suc n)

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

lemma "ack m n > n"

by (induct m n rule: ack.induct) auto

section {* Recursión mutua e inducción *}

text {*

Nota. [Ejemplo de definición de tipos mediante recursión cruzada]

· Un árbol de tipo a es una hoja o un nodo de tipo a junto con un

bosque de tipo a.

· Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo

un árbol de tipo a a un bosque de tipo a.

datatype 'a arbol = Hoja | Nodo "'a" "'a bosque"

and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"

text {*

Regla de inducción correspondiente a la recursión cruzada:

La regla de inducción sobre árboles y bosques es arbol_bosque.induct:

⟦P1 Hoja;

⋀x b. P2 b ⟹ P1 (Nodo x b);

P2 Vacio;

⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧

⟹ P1 a ∧ P2 b

text {*

Ejemplos de definición por recursión cruzada:

· aplana_arbol a) es la lista obtenida aplanando el árbol a.

· (aplana_bosque b) es la lista obtenida aplanando el bosque b.

· (map_arbol a h) es el árbol obtenido aplicando la función h a

todos los nodos del árbol a.

· (map_bosque b h) es el bosque obtenido aplicando la función h a

todos los nodos del bosque b.

fun aplana_arbol :: "'a arbol ⇒ 'a list" and

aplana_bosque :: "'a bosque ⇒ 'a list" where

"aplana_arbol Hoja = []"

| "aplana_arbol (Nodo x b) = x#(aplana_bosque b)"

| "aplana_bosque Vacio = []"

| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)"

fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and

map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where

"map_arbol f Hoja = Hoja"

| "map_arbol f (Nodo x b) = Nodo (f x) (map_bosque f b)"

| "map_bosque f Vacio = Vacio"

| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)"

text {*

Ejemplo de demostración por inducción cruzada:

Demostrar que:

· aplana_arbol (map_arbol f a) = map f (aplana_arbol a)

· aplana_bosque (map_bosque f b) = map f (aplana_bosque b)

-- "La demostración detallada es"

lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)

∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"

proof (induct_tac a and b)

show "aplana_arbol (map_arbol f Hoja ) = map f (aplana_arbol Hoja)"

by simp

fix x b

assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"

have "aplana_arbol (map_arbol f (Nodo x b)) =

aplana_arbol (Nodo (f x) (map_bosque f b))" by simp

also have "… = (f x)#(aplana_bosque (map_bosque f b))" by simp

also have "… = (f x)#(map f (aplana_bosque b))" using HI by simp

also have "… = map f (aplana_arbol (Nodo x b))" by simp

finally show "aplana_arbol (map_arbol f (Nodo x b))

= map f (aplana_arbol (Nodo x b))" .

show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)"

by simp

fix a b

assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"

and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"

have "aplana_bosque (map_bosque f (ConsB a b)) =

aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp

also have "… = aplana_arbol(map_arbol f a)@aplana_bosque(map_bosque f b)"

by simp

also have "… = (map f (aplana_arbol a))@(map f (aplana_bosque b))"

using HI1 HI2 by simp

also have "… = map f (aplana_bosque (ConsB a b))" by simp

finally show "aplana_bosque (map_bosque f (ConsB a b))

= map f (aplana_bosque (ConsB a b))" by simp

qed

text {*

Comentarios sobre la demostración anterior:

· (induct_tac a and b) indica que el método de demostración es por

inducción cruzada sobre a y b.

· Se generan 4 casos:

1. aplana_arbol (map_arbol arbol.Hoja h) = map h (aplana_arbol arbol.Hoja)

2. ⋀a bosque.

aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹

aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =

map h (aplana_arbol (arbol.Nodo a bosque))

3. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)

4. ⋀arbol bosque.

⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);

aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧

⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =

map h (aplana_bosque (ConsB arbol bosque))

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

lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)

∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"

by (induct_tac a and b) auto

end

Se puede imprimir o compartir con