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
