RA2016: Ejercicios de razonamiento automático sobre programas en Isabelle/HOL
En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 2ª relación de ejercicios sobre razonamiento automático sobre programas en Isabelle/HOL
La teoría con las soluciones de los ejercicios es la siguiente
|
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 |
chapter {* R2: Razonamiento automático sobre programas *} theory R2 imports Main begin declare [[names_short]] text {* --------------------------------------------------------------- Ejercicio 1.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 1.2. Demostrar que sumaImpares n = n*n ------------------------------------------------------------------- *} lemma "sumaImpares n = n*n" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 2.1. 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 2.2. Demostrar que sumaPotenciasDeDosMasUno n = 2^(n+1) ------------------------------------------------------------------- *} lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 3.1. 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 3.2. 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 3.3. 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 4.1. 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 4.2. Demostrar que amplia xs y = xs @ [y] ------------------------------------------------------------------- *} lemma "amplia xs y = xs @ [y]" by (induct xs) auto end |