RA12 Relación 9

header {* R9: Cons inverso *}

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

fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
  "snoc xs a = undefined"

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

lemma snoc_append: 
  "snoc xs a = xs @ [a]"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar el siguiente teorema 
     rev (x # xs) = snoc (rev xs) x"
  --------------------------------------------------------------------- 
*}

theorem rev_cons: 
  "rev (x # xs) = snoc (rev xs) x"
oops

end