Razonamiento automático (2014-15) Razonamiento automático (2014-15)

header {* R11: Plegados de listas y de árboles *}
 
theory R11
imports Main 
begin 
 
section {* Nuevas funciones sobre listas *}
 
text {* 
  Nota. En esta relación se usará la función suma tal que (suma xs) es
  la suma de los elementos de xs, definida por
*}

(* Pedrosrei: corrijo, la definición que se pretendía era esta, debería
estar dada, es una errata. *)

--"jeshorcob,davoremar"
fun suma :: "nat list ⇒ nat" where
  "suma [] = 0"
 |"suma (x#xs) = x+suma xs"
 
text {* 
  Las funciones de plegado, foldr y foldl, están definidas en la teoría
  List.thy por
       foldr :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a list ⇒ 'b ⇒ 'b"
       foldr f []       = id
       foldr f (x # xs) = f x ∘ foldr f xs
 
       foldl :: "('b ⇒ 'a ⇒ 'b) ⇒ 'b ⇒ 'a list ⇒ 'b"
       foldl f a []       = a
       foldl f a (x # xs) = foldl f (f a x) xs"
 
  Por ejemplo,
     foldr (op +) [a,b,c] d        = a + (b + (c + d))
     foldl (op +) d [a,b,c]        = ((d + a) + b) + c
     foldr (op -) [9,4,2] (0::int) = 7
     foldl (op -) (0::int) [9,4,2] = -15
*}
 
value "foldr (op +) [a,b,c] d"        -- "= a + (b + (c + d))"
value "foldl (op +) d [a,b,c]"        -- "= ((d + a) + b) + c"
value "foldr (op -) [9,4,2] (0::int)" -- "= 7"
value "foldl (op -) (0::int) [9,4,2]" -- "= -15"
 
text {* 
  --------------------------------------------------------------------- 
  Ejercicio 1. Demostrar que
     suma xs = foldr (op +) xs 0
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
lemma suma_foldr: "suma xs = foldr (op +) xs 0"
by (induct xs, simp_all)

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar que
     length xs = foldr (λ x res. 1 + res) xs 0
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
lemma length_foldr: "length xs = foldr (λ x res. 1 + res) xs 0"
by (induct xs, simp_all)
 
text {* 
  --------------------------------------------------------------------- 
  Ejercicio 3. La aplicación repetida de foldr y map tiene el
  inconveniente de que la lista se recorre varias veces. Sin embargo, es
  suficiente recorrerla una vez como se muestra en el siguiente ejemplo,  
     suma (map (λx. x + 3) xs) = foldr h xs b
  Determinar los valores de h y b para que se verifique la igualdad
  anterior y demostrarla.
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
lemma "suma (map (λx. x + 3) xs) = foldr (λ x y. x+y+3) xs 0"
by (induct xs, simp_all)

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 4. Generalizar el resultado anterior; es decir determinar
  los valores de h y b para que se verifique la igualdad 
     foldr g (map f xs) a = foldr h xs b
  y demostrarla.
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
lemma "foldr g (map f xs) a = foldr (g∘f) xs a"
by (induct xs, simp_all)


text {* 
  --------------------------------------------------------------------- 
  Ejercicio 5. La siguiente función invierte una lista en tiempo lineal
     fun inversa_ac :: "['a list, 'a list] ⇒ 'a list" where
       "inversa_ac [] ys = ys"
     | "inversa_ac (x#xs) ys = (inversa_ac xs (x#ys))"
 
     definition inversa_ac :: "'a list ⇒ 'a list" where
       "inversa_ac xs ≡ inversa_ac_aux xs []"
  Por ejemplo, 
     inversa_ac [a,d,b,c] = [c, b, d, a]
  Demostrar que inversa_ac se puede definir unsando foldl.
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
fun inversa_ac_aux :: "['a list, 'a list] ⇒ 'a list" where
  "inversa_ac_aux [] ys = ys"
| "inversa_ac_aux (x#xs) ys = (inversa_ac_aux xs (x#ys))"

--"jeshorcob,davoremar"
definition inversa_ac :: "'a list ⇒ 'a list" where
  "inversa_ac xs ≡ inversa_ac_aux xs []"
 
value "inversa_ac [a,d,b,c]" -- "= [c, b, d, a]"

--"jeshorcob"
lemma inversa_ac_aux_foldl: 
  "inversa_ac_aux xs a = foldl (λ ys x. x#ys) a xs"
by (induct xs arbitrary: a, simp_all)

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar la siguiente propiedad distributiva de la suma
  sobre la concatenación:
     suma (xs @ ys) = suma xs + suma ys
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
lemma suma_append [simp]: 
  "suma (xs @ ys) = suma xs + suma ys"
by (induct xs, simp_all)

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar una propiedad similar para foldr
     foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)
  En este caso, hay que restringir el resultado teniendo en cuenta
  propiedades algebraicas de f y a.
  --------------------------------------------------------------------- 
*}

--"Pedrosrei: Dales nombre a las cosas Jesús, te las nombro yo:"

--"jeshorcob"
lemma l1:
  assumes neutr: "(∀ x. (f a x = x))" and
          assoc: "(∀x y z. f (f x y) z = f x (f y z))"
  shows "foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
proof (induct xs)
  show "foldr f ([] @ ys) a = f (foldr f [] a) (foldr f ys a)"
    using neutr by simp
next
  show "⋀aa xs.
       foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a) ⟹
       foldr f ((aa # xs) @ ys) a = f (foldr f (aa # xs) a) (foldr f ys a)"
    using assoc by simp
qed

(*jeshorcob:
saco fuera las hipotesis porque se usan tambien en el ejercicio siguiente,
ademas la prueba queda mas corta *)

--"jeshorcob,davoremar"
definition neutr :: "['a ⇒ 'b ⇒ 'b, 'a] ⇒ bool" where
  "neutr f a == (∀ x. (f a x = x))"

--"jeshorcob,davoremar"
definition assoc :: "['a ⇒ 'a ⇒ 'a] ⇒ bool" where
  "assoc f == (∀ x y z. f (f x y) z = f x (f y z))"

(* Pedrosrei: esta es la versión automática del lema anterior, ¿para qué
 cambias el enunciado por uno equivalente? *)

--"jeshorcob,davoremar"
lemma l2: "⟦neutr f a ; assoc f⟧ 
  ⟹ foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
by (induct xs, simp add: neutr_def, simp add: assoc_def)



text {* 
  --------------------------------------------------------------------- 
  Ejercicio 8. Definir, usando foldr, la función
     prod :: "nat list ⇒ nat"
  tal que (prod xs) es el producto de los elementos de xs. Por ejemplo,
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
definition prod :: "nat list ⇒ nat" where
  "prod xs ≡ foldr (op *) xs 1"
 
value "prod [2::nat,3,5] = 30" -- "True"
 
text {* 
  --------------------------------------------------------------------- 
  Ejercicio 9. Demostrar directamente (es decir, sin inducción) que
     prod (xs @ ys) = prod xs * prod ys
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
lemma "prod (xs @ ys) = prod xs * prod ys"
by (simp only: prod_def, rule l2, simp add: neutr_def, simp add: assoc_def)

section {* Functiones sobre árboles *}
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 10. Definir el tipo de datos arbol para representar los
  árboles binarios que tiene información sólo en los nodos. Por ejemplo,
  el árbol 
          e
         / \
        /   \
       c     g
      / \   / \
     ·   · ·   · 
  se representa por "N (N H c H) e (N H g H)"
  --------------------------------------------------------------------- 
*}
 
datatype 'a arbol = H | N "'a arbol" "'a" "'a arbol"
 
value "N (N H c H) e (N H g H)"
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 11. Definir la función 
     preOrden :: "'a arbol ⇒ 'a list"
  tal que (preOrden a) es el recorrido pre orden del árbol a. Por
  ejemplo, 
     preOrden (N (N H c H) e (N H g H))
     = [e,c,g]
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
fun preOrden :: "'a arbol ⇒ 'a list" where
  "preOrden H = []"
 |"preOrden (N i x d) = x#(preOrden i @ preOrden d)"
 
value "preOrden (N (N H c H) e (N H g H)) = [e,c,g]" -- "True"
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 12. Definir la función 
     postOrden :: "'a arbol ⇒ 'a list"
  tal que (postOrden a) es el recorrido post orden del árbol a. Por
  ejemplo, 
     postOrden (N (N H c H) e (N H g H))
     = [c,g,e]
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
fun postOrden :: "'a arbol ⇒ 'a list" where
  "postOrden H = []"
 |"postOrden (N i x d) = (postOrden i) @ (postOrden d) @ [x]"
 
value "postOrden (N (N H c H) e (N H g H)) = [c,g,e]" -- "True"
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 13. Definir, usando un acumulador, la función 
     postOrdenA :: "'a arbol ⇒ 'a list"
  tal que (postOrdenA a) es el recorrido post orden del árbol a. Por
  ejemplo, 
     postOrdenA (N (N H c H) e (N H g H))
     = [c,g,e]
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
fun postOrdenAaux :: "['a arbol, 'a list] ⇒ 'a list" where
  "postOrdenAaux H xs = xs"
 |"postOrdenAaux (N i x d) xs = (postOrdenAaux i (postOrdenAaux d (x#xs)))"

--"jeshorcob,davoremar"
definition postOrdenA :: "'a arbol ⇒ 'a list" where
  "postOrdenA a ≡ postOrdenAaux a []"
 
value "postOrdenA (N (N H c H) e (N H g H)) = [c,g,e]" -- "True"
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 14. Demostrar que
     postOrdenAaux a xs = (postOrden a) @ xs
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
lemma "postOrdenAaux a xs = (postOrden a) @ xs"
by (induct a arbitrary: xs, simp_all)
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 15. Definir la función
     foldl_arbol :: "('b => 'a => 'b) ⇒ 'b ⇒ 'a arbol ⇒ 'b" where
  tal que (foldl_arbol f b a) es el plegado izquierdo del árbol a con la
  operación f y elemento inicial b.
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
fun foldl_arbol :: "('b => 'a => 'b) ⇒ 'b ⇒ 'a arbol ⇒ 'b" where
  "foldl_arbol f b H = b"
 |"foldl_arbol f b (N i x d) = foldl_arbol f (foldl_arbol f (f b x) d) i"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 16. Demostrar que
     postOrdenAaux t a = foldl_arbol (λ xs x. Cons x xs) a t
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
lemma "postOrdenAaux t a = foldl_arbol (λ xs x. Cons x xs) a t"
by (induct t arbitrary: a, simp_all)
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 17. Definir la función
     suma_arbol :: "nat arbol ⇒ nat" 
  tal que (suma_arbol a) es la suma de los elementos del árbol de
  números naturales a.
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
fun suma_arbol :: "nat arbol ⇒ nat" where
  "suma_arbol H = 0"
 |"suma_arbol (N i x d) = (suma_arbol i) + x + (suma_arbol d)"
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 18. Demostrar que
     suma_arbol a = suma (preOrden a)"
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
lemma "suma_arbol a = suma (preOrden a)"
by (induct a, simp_all)
 
end