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

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar que 
     sumaImpares n = n*n
  ------------------------------------------------------------------- *}

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

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

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

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

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

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

text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar que 
     amplia xs y = xs @ [y]
  ------------------------------------------------------------------- *}

end