RA2012: Recursión e inducción cruzada en Isabelle/HOL
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha presentado cómo definir tipos de datos mutamente recursivos y cómo demostrar propiedades por inducción cruzada sobre dichos tipos.
La teoría con los ejemplos presentados en la clase es la siguiente:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 |
theory T6 imports Main begin 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 arbol ⇒ ('a ⇒ 'b) ⇒ 'b arbol" and map_bosque :: "'a bosque ⇒ ('a ⇒ 'b) ⇒ 'b bosque" where "map_arbol Hoja h = Hoja" | "map_arbol (Nodo x b) h = Nodo (h x) (map_bosque b h)" | "map_bosque Vacio h = Vacio" | "map_bosque (ConsB a b) h = ConsB (map_arbol a h) (map_bosque b h)" text {* Ejemplo de dempstración por inducción cruzada: · aplana_arbol (map_arbol a h) = map h (aplana_arbol a) · aplana_bosque (map_bosque b h) = map h (aplana_bosque b) *} -- "La demostración automática es" lemma "aplana_arbol (map_arbol a h) = map h (aplana_arbol a) ∧ aplana_bosque (map_bosque b h) = map h (aplana_bosque b)" by (induct_tac a and b) auto -- "La demostración detallada es" lemma "aplana_arbol (map_arbol a h) = map h (aplana_arbol a) ∧ aplana_bosque (map_bosque b h) = map h (aplana_bosque b)" proof (induct_tac a and b) show "aplana_arbol (map_arbol Hoja h) = map h (aplana_arbol Hoja)" by simp next fix x b assume HI: "aplana_bosque (map_bosque b h) = map h (aplana_bosque b)" have "aplana_arbol (map_arbol (Nodo x b) h) = aplana_arbol (Nodo (h x) (map_bosque b h))" by simp also have "… = (h x)#(aplana_bosque (map_bosque b h))" by simp also have "… = (h x)#(map h (aplana_bosque b))" using HI by simp also have "… = map h (aplana_arbol (Nodo x b))" by simp finally show "aplana_arbol (map_arbol (Nodo x b) h) = map h (aplana_arbol (Nodo x b))" . next show "aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)" by simp next fix a b assume HI1: "aplana_arbol (map_arbol a h) = map h (aplana_arbol a)" and HI2: "aplana_bosque (map_bosque b h) = map h (aplana_bosque b)" have "aplana_bosque (map_bosque (ConsB a b) h) = aplana_bosque (ConsB (map_arbol a h) (map_bosque b h))" by simp also have "… = aplana_arbol(map_arbol a h)@aplana_bosque(map_bosque b h)" by simp also have "… = (map h (aplana_arbol a))@(map h (aplana_bosque b))" using HI1 HI2 by simp also have "… = map h (aplana_bosque (ConsB a b))" by simp finally show "aplana_bosque (map_bosque (ConsB a b) h) = map h (aplana_bosque (ConsB a b))" by simp qed |