Relación 1

header {* Razonamiento en Isabelle sobre programas *}

theory Relacion_1
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*(Suc n) - 1)"

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^(Suc n)" 

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar que 
     sumaPotenciasDeDosMasUno n = 2^(n+1)
  ------------------------------------------------------------------- *}

lemma "sumaPotenciasDeDosMasUno n = 2^(Suc n)"
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)"

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 ∧
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar que todos los elementos de (copia n x) son
  iguales a x. 
  ------------------------------------------------------------------- *}

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 \<Rightarrow> nat" where
"factR 0 = 1"
|"factR (Suc n)= (Suc n)* factR n"

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"

lemma "factI = factR"
quickcheck
oops

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
  ------------------------------------------------------------------- *}

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 \<Rightarrow> 'a \<Rightarrow> 'a list" where

"amplia [] y = [y]"
|"amplia (x#xs) y = x # (amplia xs y)"
text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar que 
     amplia xs y = xs @ [y]
  ------------------------------------------------------------------- *}

end