RA2018: Razonamiento sobre árboles y bosques en Isabelle/HOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir y razonar en Isabelle/HOL tipos de datos recursivos como árboles binarios, árboles generales y bosques. En su definición se usa recursión cruzada y en la demostración de sus propiedades se usa inducción doble.

La teoría utilizada es la siguiente

chapter {* Tema 5: Razonamiento sobre árboles *}

theory T5_Razonamiento_sobre_arboles
imports Main HOL.Parity
begin

text {*
  En este tema se estudia razonamiento sobre otras estructuras
  recursivas como árboles binarios, árboles generales y bosques.
  
  También se muestra cómo definir tipos de datos por recursión cruzada y
  la demostración de sus propiedades por inducción.
*}

section {* Razonamiento sobre árboles binarios *}

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 {* Árboles y bosques. 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 f a) es el árbol obtenido aplicando la función f a
    todos los nodos del árbol a.   
  · (map_bosque f b) es el bosque obtenido aplicando la función f 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)
*}

declare [[names_short]]

― ‹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

chapter {* Tema 5: Razonamiento sobre árboles *}

theory T5_Razonamiento_sobre_arboles

imports Main HOL.Parity

begin

text {*

En este tema se estudia razonamiento sobre otras estructuras

recursivas como árboles binarios, árboles generales y bosques.

También se muestra cómo definir tipos de datos por recursión cruzada y

la demostración de sus propiedades por inducción.

section {* Razonamiento sobre árboles binarios *}

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 {* Árboles y bosques. 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 f a) es el árbol obtenido aplicando la función f a

todos los nodos del árbol a.

· (map_bosque f b) es el bosque obtenido aplicando la función f 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)

declare [[names_short]]

― ‹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

En la segunda parte se comentó el contenido de las teorías de Main y de HOL.

Se puede imprimir o compartir con