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 @.
  --------------------------------------------------------------------- 
*}

-- "davoremar"

fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
  "snoc [] a = [a]"
| "snoc (x#xs) a = x # (snoc xs a)"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar automáticamente el siguiente teorema 
     snoc xs a = xs @ [a]
  --------------------------------------------------------------------- 
*}

-- "davoremar"

lemma "snoc xs a = xs @ [a]"
by (induct xs) auto

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar detalladamente el siguiente teorema 
     snoc xs a = xs @ [a]
  --------------------------------------------------------------------- 
*}

-- "davoremar"

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

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

-- "davoremar"

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

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

-- "davoremar"

lemma "rev (x # xs) = snoc (rev xs) x"
proof -
  have "rev (x # xs) = (rev xs) @ [x]" by simp
  also have "... = snoc (rev xs) x" by (simp add:snoc_append)
  finally show "rev (x # xs) = snoc (rev xs) x" by simp
qed

end