RA2014: Ejercicios de razonamiento sobre cons inverso en Isabelle/HOL
En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de los ejercicios de la relación 4 sobre función snoc (cons inverso) que añade un elemento al final. Lo interesante es el uso de algunas propiedades en la demostración de otras (como en el ejercicio 5). Las ejercicios y sus soluciones son
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 |
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 [] a = [a]" | "snoc (x#xs) a = x # (snoc xs a)" text {* --------------------------------------------------------------------- Ejercicio 2. Demostrar automáticamente el siguiente teorema snoc xs a = xs @ [a] --------------------------------------------------------------------- *} lemma "snoc xs a = xs @ [a]" by (induct xs) auto text {* --------------------------------------------------------------------- Ejercicio 3. Demostrar detalladamente el siguiente teorema snoc xs a = xs @ [a] --------------------------------------------------------------------- *} lemma snoc_append: "snoc xs a = xs @ [a]" proof (induct "xs") show "snoc [] a = [] @ [a]" proof - have "snoc [] a = [a]" by simp also have "… = [] @ [a]" by simp finally show "snoc [] a = [] @ [a]" . qed next fix b xs assume HI: "snoc xs a = xs @ [a]" show "snoc (b # xs) a = (b # xs) @ [a]" proof - have "snoc (b # xs) a = b # (snoc xs a)" by simp also have "… = b # (xs @ [a])" using HI by simp also have "… = (b # xs) @ [a]" by simp finally show "snoc (b # xs) a = (b # xs) @ [a]" . qed qed text {* --------------------------------------------------------------------- Ejercicio 4. Demostrar automáticamente el siguiente lema rev (x # xs) = snoc (rev xs) x" --------------------------------------------------------------------- *} lemma "rev (x # xs) = snoc (rev xs) x" by (auto simp add: snoc_append) text {* --------------------------------------------------------------------- Ejercicio 5. Demostrar detalladamente el siguiente lema rev (x # xs) = snoc (rev xs) x" --------------------------------------------------------------------- *} theorem "rev (x # xs) = snoc (rev xs) x" proof - have "rev (x # xs) = (rev xs) @ [x]" by simp also have "… = snoc (rev xs) x" by (simp add:snoc_append) finally show "rev (x # xs) = snoc (rev xs) x" . qed end |