R4

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

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

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

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

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

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

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

lemma "rev (x # xs) = snoc (rev xs) x"
oops

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

lemma "rev (x # xs) = snoc (rev xs) x"
oops

end