DAO2011: Ejercicios de razonamiento sobre programas con Isabelle
En la clase de hoy del curso de Demostración asistida por ordenador se han comentado las soluciones propuestas por los alumnos a los ejercicios de demostración con Isabelle de propiedades de programas funcionales.
La teoría correspondiente a la clase es Relacion_1.thy cuyo contenido se muestra a continuación
|
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 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 |
header {* Razonamiento en Isabelle sobre programas *} theory Tema_2_ej_sol imports Main Efficient_Nat begin text {* --------------------------------------------------------------- Ejercicio 1. Definir la función sumaImpares :: "nat ⇒ nat" tal que (sumaImpares n) es la suma de los n primeros números impares. Por ejemplo, sumaImpares 5 = 25 ------------------------------------------------------------------ *} fun sumaImpares :: "nat ⇒ nat" where "sumaImpares 0 = 0" | "sumaImpares (Suc n) = sumaImpares n + (2*n+1)" value "sumaImpares 5" -- "= 25" text {* --------------------------------------------------------------- Ejercicio 2. Demostrar que sumaImpares n = n*n ------------------------------------------------------------------- *} lemma "sumaImpares n = n*n" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 3. Definir la función sumaPotenciasDeDosMasUno :: "nat ⇒ nat" tal que (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. Por ejemplo, sumaPotenciasDeDosMasUno 3 = 16 ------------------------------------------------------------------ *} fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where "sumaPotenciasDeDosMasUno 0 = 2" | "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)" value "sumaPotenciasDeDosMasUno 3" text {* --------------------------------------------------------------- Ejercicio 4. Demostrar que sumaPotenciasDeDosMasUno n = 2^(n+1) ------------------------------------------------------------------- *} lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 5. Definir la función copia :: "nat ⇒ 'a ⇒ 'a list" tal que (copia n x) es la lista formado por n copias del elemento x. Por ejemplo, copia 3 2 = [2,2,2] ------------------------------------------------------------------ *} fun copia :: "nat ⇒ 'a ⇒ 'a list" where "copia 0 x = []" | "copia (Suc n) x = x # copia n x" value "copia 3 2" -- "= [2,2,2]" text {* --------------------------------------------------------------- Ejercicio 6. Definir la función todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" tal que (todos p xs) se verifica si todos los elementos de xs cumplen la propiedad p. Por ejemplo, todos (λx. x>(1::nat)) [2,6,4] = True todos (λx. x>(2::nat)) [2,6,4] = False Nota; La conjunción se representa por ∧ ------------------------------------------------------------------ *} fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where "todos p [] = True" | "todos p (x#xs) = (p x ∧ todos p xs)" value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True" value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False" text {* --------------------------------------------------------------- Ejercicio 7. Demostrar que todos los elementos de (copia n x) son iguales a x. ------------------------------------------------------------------- *} lemma "todos (λy. y=x) (copia n x)" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 8. Definir la función factR :: "nat ⇒ nat" tal que (factR n) es el factorial de n. Por ejemplo, factR 4 = 24 ------------------------------------------------------------------ *} fun factR :: "nat ⇒ nat" where "factR 0 = 1" | "factR (Suc n) = Suc n * factR n" value "factR 4" -- "= 24" text {* --------------------------------------------------------------- Ejercicio 9. Se considera la siguiente definición iterativa de la función factorial factI :: Integer -> Integer factI n = factI' n 1 factI' :: Integer -> Integer -> Integer factI' 0 x = x -- factI'.1 factI' (n+1) x = factI' n (n+1)*x -- factI'.2 Comprobar con QuickCheck que factI y factR son equivalentes sobre los números naturales. ------------------------------------------------------------------- *} fun factI' :: "nat ⇒ nat ⇒ nat" where "factI' 0 x = x" | "factI' (Suc n) x = factI' n (Suc n)*x" fun factI :: "nat ⇒ nat" where "factI n = factI' n 1" value "factI 4" -- "= 24" text {* --------------------------------------------------------------- Ejercicio 10. Demostrar que, para todo n y todo x, se tiene factI' n x = x * factR n y, como corolario, que factI n = factR n ------------------------------------------------------------------- *} lemma fact: "factI' n x = x * factR n" by (induct n arbitrary: x) auto corollary "factI n = factR n" by (simp add: fact) text {* --------------------------------------------------------------- Ejercicio 12. Definir, recursivamente y sin usar (@). la función amplia :: "'a list ⇒ 'a ⇒ 'a list" tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al final de la lista xs. Por ejemplo, amplia [2,5] 3 = [2,5,3] ------------------------------------------------------------------ *} fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where "amplia [] y = [y]" | "amplia (x#xs) y = x # amplia xs y" value "amplia [2,5] 3" -- "= [2,5,3]" text {* --------------------------------------------------------------- Ejercicio 13. Demostrar que amplia xs y = xs @ [y] ------------------------------------------------------------------- *} lemma "amplia xs y = xs @ [y]" by (induct xs) auto end |