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 @.
  --------------------------------------------------------------------- 
*}
-- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav marescpla"
fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
  "snoc [] a = [a]"
| "snoc (x#xs) a = x # (snoc xs a)" 

value "snoc [2,5] (3::int)" -- "[2,5,3]"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar automáticamente el siguiente teorema 
     snoc xs a = xs @ [a]
  --------------------------------------------------------------------- 
*}
-- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav marescpla"
lemma "snoc xs a = xs @ [a]"
by (induct xs) auto


text {*
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar detalladamente el siguiente teorema 
     snoc xs a = xs @ [a]
  --------------------------------------------------------------------- 
*}
-- "pabflomar irealetei maresccas4 domlloriv diecabmen1 jaisalmen juaruipav marescpla"
lemma snoc_append: "snoc xs a = xs @ [a]"
proof (induct xs)
  show " snoc [] a = [] @ [a]" by simp
next
  fix aa xs
  assume HI: "snoc xs a = xs @ [a]"
  have "snoc (aa # xs) a = aa # snoc xs a" by simp
  also have "... = aa # xs @ [a]" using HI by simp
  finally show "snoc (aa # xs) a = (aa # xs) @ [a]" by simp
qed

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

-- "pabflomar irealetei maresccas4 domlloriv jaisalmen juaruipav marescpla"
lemma "rev (x # xs) = snoc (rev xs) x"
by (simp add: snoc_append)

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

(* maresccas4 - ¿Tiene sentido realizar la demostración automática por simplificación y 
posteriormente hacerla detallada haciendo uso de la inducción? *)

(* pabflomar - Marco llevas razón, pero yo fui el primero en los anteriores ejercicios, PRINGAO :P, como dirían en forocoches... POLE *)
(* pabflomar - Irene, transfuga.*)
(* pabflomar - Obviamente, la solución de Marco es la correcta. Dejo esta por motivos de demostrar mi estupidez al querer ser el primero :) *)


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


-- "maresccas4 irealetei domlloriv jaisalmen juaruipav marescpla" (* Marco, como siempre, tiene razón. Abandono el barco, Pablo*)(*definitivamente esto es magia callejera para mi. Marco podrías poner una breve explicación de como obtuviste la definición de rev para poner el rev.simp?, diecabmen1*)
lemma "rev (x # xs) = snoc (rev xs) x"
proof -
 have "rev (x#xs) = rev xs @ [x]" by (simp only:rev.simps)
 also have "... = snoc (rev xs) x" by (simp add:snoc_append)
 finally show "rev (x#xs) = snoc (rev xs) x" by simp
qed

end