Relación 11

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,juacorvic"
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,juacorvic"
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,davoremarm,juacorvic"
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,juacorvic"
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,juacorvic"
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,juacorvic"
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: a petición de juanjose.
El ejercicio pide que pruebes esa igualdad, pero claro, 
como no es verdad siempre, debemos pensar bajo que hipotesis es cierta la 
propiedad. Eso lo primero. Una vez nos hemos dado cuenta de cuales son las 
hipotesis (yo esto lo vi pensando en tres ejemplitos o asi y "haciendo" 
una ejecucion a mano sencillita) una vez te das cuenta, planteas el enunciado,
y ya solo tienes que hacerlo por induccion.

El caso base es sencillo, y es para el que se necesita la propiedad primera.
El otro caso es el paso de incuccion, se usa la otra hipotesis, y si te 
fijas, es solo escribir el caso, añadir la hipotesis y poner simp.

Consejo: muchas veces tambien ayuda bastante intentar hacer la demostracion 
y ver que es lo que isabelle te da como error para probar lo que le falta.

Espero que sea de ayuda, si no, pregunta o lo que sea
*)


(*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,juacorvic"
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,juacorvic"
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,juacorvic"
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