RA2012: Razonamiento por casos y por inducción en Isabelle/HOL (1)

En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha presentado los métodos de demostración por casos y por inducción iniciados en Isabelle/HOL.

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

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

theory T6
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:
     ¬A ∨ A
*}

-- "La demostración estructurada es"
lemma "¬A ∨ A" 
proof cases
  assume "A" 
  thus ?thesis ..
next
  assume "¬A" 
  thus ?thesis ..
qed

-- "La demostración detallada es"
lemma "¬A ∨ A" 
proof cases
  assume "A" 
  thus ?thesis by (rule disjI2)
next
  assume "¬A" 
  thus ?thesis by (rule disjI1)
qed

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

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

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

-- "La demostración detallada es"
lemma "¬A ∨ A" 
proof (cases "A")
  case True 
  thus ?thesis by (rule disjI2)
next
  case False 
  thus ?thesis by (rule disjI1)
qed

text {*
  El método "cases" sobre una fórmula:
  · 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: 
  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)
  case Nil thus ?thesis by simp
next
  case Cons thus ?thesis by simp 
qed

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

text {*
  Distinción de casos sobre listas:
  · El método de distinción de casos se activa con (cases xs) donde xs
    es del tipo lista. 
  · "case Nil" es una abreviatura de 
       "assume Nil: xs =[]".
  · "case Cons" es una abreviatura de 
       "fix ? ?? assume Cons: xs = ? # ??"
    donde ? y ?? son variables anónimas. 
*}

text {*
  Ejemplo de análisis de casos:
  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 thus "drop (n + 1) xs = drop n (tl xs)" by simp
next
  case Cons thus "drop (n + 1) xs = drop n (tl xs)" by simp
qed

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

text {*
  La función drop 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)"
*}

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:
  La suma de los n primeros números impares es n^2.
*}

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

-- "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"
  thus "?P (Suc n)" by simp
qed

text {*
  Patrones: Cualquier fórmula seguida de (is patrón) equipara el patrón
  con la fórmula.
*}

-- "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

-- "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

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] Para todo número natural
  n, se verifica que n*(n+1) par. 
*}

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))"
  hence "∃m. n*(n+1) = m+m" by (simp add:par_def)
  then obtain m where m: "n*(n+1) = m+m" by (rule exE)
  hence "(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)" by auto
  hence "∃m. (Suc n)*((Suc n)+1) = m+m" by (rule exI)
  thus "par ((Suc n)*((Suc n)+1))" by (simp add:par_def)
qed

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 {*
  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)
  thus "par n = even n" by presburger
qed

text {*
  En la demostración anterior hemos usado la táctica "presburger" que
  corresponde a la aritmética de Presburger.
*}

section {* Inducción estructural *}

text {*
  Inducción estructural:
  · En Isabelle puede hacerse inducción estructural sobre cualquier tipo
    recursivo.
  · La inducción matemática es la inducción estructural sobre el tipo de
    los naturales.
  · El esquema de inducción estructural sobre listas es
    · list.induct: ⟦P []; ⋀x ys. P ys ⟹ P (x # ys)⟧ ⟹ P zs
  · Para demostrar una propiedad para todas las listas basta demostrar
    que la lista vacía tiene la propiedad y que al añadir un elemento a una
    lista que tiene la propiedad se obtiene una lista que también tiene la
    propiedad. 
  · En Isabelle el principio de inducción sobre listas está formalizado
    mediante el teorema list.induct que puede verse con 
       thm list.induct
*}

text {*
  Concatenación de listas:
  En la teoría List.thy está definida la concatenación de listas (que
  se representa por @) como sigue
     append_Nil:  "[]@ys = ys"
     append_Cons: "(x#xs)@ys = x#(xs@ys)"
*}

text {*
  Lema. [Ejemplo de inducción sobre listas]
  La concatenación de listas es asociativa.
*}

-- "La demostración automática es"
lemma conc_asociativa_1: "xs @ (ys @ zs) = (xs @ ys) @ zs"
by (induct xs) simp_all

-- "La demostración estructurada es"
lemma conc_asociativa: "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  show "[] @ (ys @ zs) = ([] @ ys) @ zs"
  proof -
    have "[] @ (ys @ zs) = ys @ zs" by simp
    also have "… = ([] @ ys) @ zs" by simp
    finally show ?thesis .
  qed
next
  fix x xs
  assume HI: "xs @ (ys @ zs) = (xs @ ys) @ zs"
  show "(x#xs) @ (ys @ zs) = ((x#xs) @ ys) @ zs"
  proof -
    have "(x#xs) @ (ys @ zs) = x#(xs @ (ys @ zs))" by simp
    also have "… = x#((xs @ ys) @ zs)" using HI by simp
    also have "… = (x#(xs @ ys)) @ zs" by simp
    also have "… = ((x#xs) @ ys) @ zs" by simp
    finally show ?thesis .
  qed
qed

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 a) = (Hoja a)"
| "espejo (Nodo f x y) = (Nodo f (espejo y) (espejo x))"

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

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

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

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 a) = [a]"
| "aplana (Nodo x t1 t2) = (aplana t1)@[x]@(aplana t2)"

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

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

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

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 automática es"
lemma inversaAcAux_es_inversa_1:
  "inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

-- "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" by simp 
    finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp
  qed
qed

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, activando "Trace
  Simplifier" y D"|Trace Rules", que los lemas usados son 
  · append_assoc:       (xs @ ys) @ zs = xs @ (ys @ zs)
  · append.append_Cons: (x#xs)@ys = x#(xs@ys)
  · append.append_Nil:  []@ys = ys
  Los dos últimos 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.append_Nil)
  also have "… = (inversa xs)@([a]@ys)" by (simp only:append.append_Cons)
  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:
  Para todos m y n, A(m,n) > n.
*} 

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

-- "La demostración detallada es"
lemma "ack m n > n"
proof (induct m n rule: ack.induct)
  fix n :: "nat"
  show "ack 0 n > n" by simp
next
  fix m assume "ack m 1 > 1"
  thus "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)"
  thus "Suc n < ack (Suc m) (Suc n)" by simp
qed

text {*
  Nota. [Inducción sobre recursión]
  El formato para iniciar una demostración por inducción en la regla
  inductiva correspondiente a la definición recursiva de la función f m
  n es 
     proof (induct m n rule:f.induct) 
*}

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

426

427

428

429

430

431

432

433

434

435

436

437

438

439

440

441

442

443

444

445

446

447

448

449

450

451

452

453

454

455

456

457

458

459

460

461

462

463

464

465

466

467

468

469

470

471

472

473

474

475

476

477

478

479

480

481

482

483

484

485

486

487

488

489

490

491

492

493

494

495

496

497

498

499

500

501

502

503

504

505

506

507

508

509

510

511

512

513

514

515

516

517

518

519

520

521

522

523

524

525

526

527

528

529

530

531

532

533

534

535

536

537

538

539

540

541

542

543

544

545

546

547

548

549

550

551

552

553

554

555

556

557

558

559

560

561

562

563

564

565

566

567

568

569

570

571

572

573

574

575

576

577

578

579

580

581

582

583

584

585

586

587

588

589

590

591

592

593

594

595

596

597

598

599

600

601

602

603

604

605

606

607

608

609

610

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

theory T6

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:

¬A ∨ A

-- "La demostración estructurada es"

lemma "¬A ∨ A"

proof cases

assume "A"

thus ?thesis ..

assume "¬A"

thus ?thesis ..

qed

-- "La demostración detallada es"

lemma "¬A ∨ A"

proof cases

assume "A"

thus ?thesis by (rule disjI2)

assume "¬A"

thus ?thesis by (rule disjI1)

qed

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

lemma "¬A ∨ A"

by auto

text {*

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

¬A ∨ A

-- "La demostración estructurada es"

lemma "¬A ∨ A"

proof (cases "A")

case True

thus ?thesis ..

case False

thus ?thesis ..

qed

-- "La demostración detallada es"

lemma "¬A ∨ A"

proof (cases "A")

case True

thus ?thesis by (rule disjI2)

case False

thus ?thesis by (rule disjI1)

qed

text {*

El método "cases" sobre una fórmula:

· 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:

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)

case Nil thus ?thesis by simp

case Cons thus ?thesis by simp

qed

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

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

by auto

text {*

Distinción de casos sobre listas:

· El método de distinción de casos se activa con (cases xs) donde xs

es del tipo lista.

· "case Nil" es una abreviatura de

"assume Nil: xs =[]".

· "case Cons" es una abreviatura de

"fix ? ?? assume Cons: xs = ? # ??"

donde ? y ?? son variables anónimas.

text {*

Ejemplo de análisis de casos:

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 thus "drop (n + 1) xs = drop n (tl xs)" by simp

case Cons thus "drop (n + 1) xs = drop n (tl xs)" by simp

qed

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

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

by (cases xs) auto

text {*

La función drop 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)"

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:

La suma de los n primeros números impares es n^2.

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

lemma "suma_impares n = n * n"

by (induct n) simp_all

-- "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"

thus "?P (Suc n)" by simp

qed

text {*

Patrones: Cualquier fórmula seguida de (is patrón) equipara el patrón

con la fórmula.

-- "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

-- "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

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] Para todo número natural

n, se verifica que n*(n+1) par.

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))"

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

then obtain m where m: "n*(n+1) = m+m" by (rule exE)

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

hence "∃m. (Suc n)*((Suc n)+1) = m+m" by (rule exI)

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

qed

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 {*

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)

thus "par n = even n" by presburger

qed

text {*

En la demostración anterior hemos usado la táctica "presburger" que

corresponde a la aritmética de Presburger.

section {* Inducción estructural *}

text {*

Inducción estructural:

· En Isabelle puede hacerse inducción estructural sobre cualquier tipo

recursivo.

· La inducción matemática es la inducción estructural sobre el tipo de

los naturales.

· El esquema de inducción estructural sobre listas es

· list.induct: ⟦P []; ⋀x ys. P ys ⟹ P (x # ys)⟧ ⟹ P zs

· Para demostrar una propiedad para todas las listas basta demostrar

que la lista vacía tiene la propiedad y que al añadir un elemento a una

lista que tiene la propiedad se obtiene una lista que también tiene la

propiedad.

· En Isabelle el principio de inducción sobre listas está formalizado

mediante el teorema list.induct que puede verse con

thm list.induct

text {*

Concatenación de listas:

En la teoría List.thy está definida la concatenación de listas (que

se representa por @) como sigue

append_Nil: "[]@ys = ys"

append_Cons: "(x#xs)@ys = x#(xs@ys)"

text {*

Lema. [Ejemplo de inducción sobre listas]

La concatenación de listas es asociativa.

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

lemma conc_asociativa_1: "xs @ (ys @ zs) = (xs @ ys) @ zs"

by (induct xs) simp_all

-- "La demostración estructurada es"

lemma conc_asociativa: "xs @ (ys @ zs) = (xs @ ys) @ zs"

proof (induct xs)

show "[] @ (ys @ zs) = ([] @ ys) @ zs"

proof -

have "[] @ (ys @ zs) = ys @ zs" by simp

also have "… = ([] @ ys) @ zs" by simp

finally show ?thesis .

qed

fix x xs

assume HI: "xs @ (ys @ zs) = (xs @ ys) @ zs"

show "(x#xs) @ (ys @ zs) = ((x#xs) @ ys) @ zs"

proof -

have "(x#xs) @ (ys @ zs) = x#(xs @ (ys @ zs))" by simp

also have "… = x#((xs @ ys) @ zs)" using HI by simp

also have "… = (x#(xs @ ys)) @ zs" by simp

also have "… = ((x#xs) @ ys) @ zs" by simp

finally show ?thesis .

qed

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 a) = (Hoja a)"

| "espejo (Nodo f x y) = (Nodo f (espejo y) (espejo x))"

text {*

Ejemplo de demostración sobre árboles binarios:

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

cualquier árbol t, se tiene que

espejo (espejo(t)) = t.

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

lemma espejo_involutiva_1:

"espejo(espejo(t)) = t"

by (induct t) auto

-- "La demostración estructurada es"

lemma espejo_involutiva:

"espejo(espejo(t)) = t" (is "?P t")

proof (induct t)

fix x :: 'a show "?P (Hoja x)" by simp

fix t1 :: "'a arbolB" assume h1: "?P t1"

fix t2 :: "'a arbolB" assume h2: "?P t2"

fix x :: 'a

show "?P (Nodo x t1 t2)"

proof -

have "espejo(espejo(Nodo x t1 t2)) = espejo(Nodo x (espejo t2) (espejo t1))"

by simp

also have "… = Nodo x (espejo (espejo t1)) (espejo (espejo t2))" by simp

also have "… = Nodo x t1 t2" using h1 h2 by simp

finally show ?thesis .

qed

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 a) = [a]"

| "aplana (Nodo x t1 t2) = (aplana t1)@[x]@(aplana t2)"

text {*

Ejemplo. [Aplanamiento de la imagen especular] Demostrar que

aplana (espejo t) = rev (aplana t)

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

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

by (induct t) auto

-- "La demostración estructurada es"

lemma "aplana (espejo t) = rev (aplana t)" (is "?P t")

proof (induct t)

fix x :: 'a

show "?P (Hoja x)" by simp

fix t1 :: "'a arbolB" assume h1: "?P t1"

fix t2 :: "'a arbolB" assume h2: "?P t2"

fix x :: 'a

show "?P (Nodo x t1 t2)"

proof -

have "aplana (espejo (Nodo x t1 t2)) =

aplana (Nodo x (espejo t2) (espejo t1))" by simp

also have "… = (aplana(espejo t2))@[x]@(aplana(espejo t1))" by simp

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

also have "… = rev((aplana t1)@[x]@(aplana t2))" by simp

also have "… = rev(aplana (Nodo x t1 t2))" by simp

finally show ?thesis .

qed

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 automática es"

lemma inversaAcAux_es_inversa_1:

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

by (induct xs arbitrary: ys) auto

-- "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" by simp

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

qed

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, activando "Trace

Simplifier" y D"|Trace Rules", que los lemas usados son

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

· append.append_Cons: (x#xs)@ys = x#(xs@ys)

· append.append_Nil: []@ys = ys

Los dos últimos 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.append_Nil)

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

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:

Para todos m y n, A(m,n) > n.

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

lemma "ack m n > n"

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

-- "La demostración detallada es"

lemma "ack m n > n"

proof (induct m n rule: ack.induct)

fix n :: "nat"

show "ack 0 n > n" by simp

fix m assume "ack m 1 > 1"

thus "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)"

thus "Suc n < ack (Suc m) (Suc n)" by simp

qed

text {*

Nota. [Inducción sobre recursión]

El formato para iniciar una demostración por inducción en la regla

inductiva correspondiente a la definición recursiva de la función f m

n es

proof (induct m n rule:f.induct)

end

Se puede imprimir o compartir con