RA2015: Ejercicios de razonamiento automático sobre programas con Isabelle/HOL
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha comentado las soluciones de la 2ª relación de ejercicios cuyo objetivo es demostrar automáticamente con Isabelle/HOL propiedades de programas.
Los ejercicios y sus soluciones se muestran 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 |
header {* R2: Razonamiento automático sobre programas *} theory R2 imports Main 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" -- "= 16" 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 x = [x,x,x] ------------------------------------------------------------------ *} fun copia :: "nat ⇒ 'a ⇒ 'a list" where "copia 0 x = []" | "copia (Suc n) x = x # copia n x" value "copia 3 x" -- "= [x,x,x]" 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 ------------------------------------------------------------------ *} 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 :: "nat ⇒ nat" where factI n = factI' n 1 factI' :: nat ⇒ nat ⇒ nat" where factI' 0 x = x factI' (Suc n) x = factI' n (Suc n)*x Demostrar que, para todo n y todo x, se tiene factI' n x = x * factR n ------------------------------------------------------------------- *} fun factI' :: "nat ⇒ nat ⇒ nat" where "factI' 0 x = x" | "factI' (Suc n) x = factI' n (x * Suc n)" fun factI :: "nat ⇒ nat" where "factI n = factI' n 1" value "factI 4" -- "= 24" lemma fact: "factI' n x = x * factR n" by (induct n arbitrary: x) (auto simp del: mult_Suc) text {* --------------------------------------------------------------- Ejercicio 10. Demostrar que factI n = factR n ------------------------------------------------------------------- *} corollary "factI n = factR n" by (simp add: fact) text {* --------------------------------------------------------------- Ejercicio 11. 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 [d,a] t = [d,a,t] ------------------------------------------------------------------ *} fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where "amplia [] y = [y]" | "amplia (x#xs) y = x # amplia xs y" value "amplia [d,a] t" -- "= [d,a,t]" text {* --------------------------------------------------------------- Ejercicio 12. Demostrar que amplia xs y = xs @ [y] ------------------------------------------------------------------- *} lemma "amplia xs y = xs @ [y]" by (induct xs) auto end |