Rel 1

header {* Razonamiento en Isabelle sobre programas *}

theory Relacion_1_sol
imports Main Efficient_Nat
begin

text {* --------------------------------------------------------------- 
  Ejercicio 1. Definir la función
     sumaImpares :: "nat \<Rightarrow> nat"
  tal que (sumaImpares n) es la suma de los n primeros números
  impares. Por ejemplo,
     sumaImpares 5  =  25
  ------------------------------------------------------------------ *}

fun sumaImpares :: "nat \<Rightarrow> 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 \<Rightarrow> nat"
  tal que 
     (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. 
  Por ejemplo, 
     sumaPotenciasDeDosMasUno 3  =  16
  ------------------------------------------------------------------ *}

fun sumaPotenciasDeDosMasUno :: "nat \<Rightarrow> 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 \<Rightarrow> 'a \<Rightarrow> '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 \<Rightarrow> 'a \<Rightarrow> '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 \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
  tal que (todos p xs) se verifica si todos los elementos de xs cumplen
  la propiedad p. Por ejemplo,
     todos (\<lambda>x. x>(1::nat)) [2,6,4] = True
     todos (\<lambda>x. x>(2::nat)) [2,6,4] = False
  Nota; La conjunción se representa por \<and>
  ------------------------------------------------------------------ *}

fun todos :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
  "todos p []     = True"
| "todos p (x#xs) = (p x \<and> todos p xs)"

value "todos (\<lambda>x. x>(1::nat)) [2,6,4]" -- "= True"
value "todos (\<lambda>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 (\<lambda>y. y=x) (copia n x)"
by (induct n) auto

text {* --------------------------------------------------------------- 
  Ejercicio 8. Definir la función
    factR :: "nat \<Rightarrow> nat"
  tal que (factR n) es el factorial de n. Por ejemplo,
    factR 4  =  24
  ------------------------------------------------------------------ *}

fun factR :: "nat \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> nat" where
  "factI' 0       x = x"
| "factI' (Suc n) x = factI' n (Suc n)*x"

fun factI :: "nat \<Rightarrow> 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 \<Rightarrow> 'a \<Rightarrow> '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 \<Rightarrow> 'a \<Rightarrow> '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