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
