Relación 4

header {* R4: Cons inverso *}

theory R4
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir recursivamente la función 
     snoc :: "'a list ⇒ 'a ⇒ 'a list"
  tal que (snoc xs a) es la lista obtenida al añadir el elemento a al
  final de la lista xs. Por ejemplo, 
     value "snoc [2,5] (3::int)" == [2,5,3]

  Nota: No usar @.
  --------------------------------------------------------------------- 
*}
-- "pabflomar"
fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
  "snoc [] a = [a]"
| "snoc (x#xs) a = x # (snoc xs a)" 

value "snoc [2,5] (3::int)" -- "[2,5,3]"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar automáticamente el siguiente teorema 
     snoc xs a = xs @ [a]
  --------------------------------------------------------------------- 
*}
-- "pabflomar"
lemma "snoc xs a = xs @ [a]"
by (induct xs) auto


text {*
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar detalladamente el siguiente teorema 
     snoc xs a = xs @ [a]
  --------------------------------------------------------------------- 
*}
-- "pabflomar"
lemma snoc_append: "snoc xs a = xs @ [a]"
proof (induct xs)
  show " snoc [] a = [] @ [a]" by simp
next
  fix aa xs
  assume HI: "snoc xs a = xs @ [a]"
  have "snoc (aa # xs) a = aa # snoc xs a" by simp
  also have "... = aa # xs @ [a]" using HI by simp
  finally show "snoc (aa # xs) a = (aa # xs) @ [a]" by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4. Demostrar automáticamente el siguiente lema
     rev (x # xs) = snoc (rev xs) x"
  --------------------------------------------------------------------- 
*}

-- "pabflomar"
lemma "rev (x # xs) = snoc (rev xs) x"
by (simp add: snoc_append)

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5. Demostrar detalladamente el siguiente lema
     rev (x # xs) = snoc (rev xs) x"
  --------------------------------------------------------------------- 
*}

-- "pabflomar"
lemma "rev (x # xs) = snoc (rev xs) x"
proof (induct xs)
  show "rev [x] = snoc (rev []) x" by simp
next
  fix a xs
  assume HI: "rev (x # xs) = snoc (rev xs) x"
  have "rev (x # a # xs) =rev (a # xs) @ rev [x]" by simp
  also have "... = snoc (rev (a # xs)) x" using HI by (simp add: snoc_append)
  finally show "rev (x # a # xs) = snoc (rev (a # xs)) x" by simp
qed  

end