Ver el código de «R10» - Lógica matemática y fundamentos (2018-19)

<source lang = "isabelle">
chapter {* R10: Programación funcional en Isabelle/HOL *}
 
theory R10
imports Main 
begin
 
    
    
text {* --------------------------------------------------------------- 
  Ejercicio 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 n = undefined"
 
(* value "sumaPotenciasDeDosMasUno 3" ― ‹= 16› *)
 
  
text {* --------------------------------------------------------------- 
  Ejercicio 2. Se considera la siguiente definición 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

  ------------------------------------------------------------------- *}
 
fun factI' :: "nat ⇒ nat ⇒ nat" where
  "factI' n x = undefined"

fun factI :: "nat ⇒ nat" where
  "factI n = undefined"
 
(* value "factI 4" ― ‹= 24› *)
 
 
text {* --------------------------------------------------------------- 
  Ejercicio 3. 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 xs = undefined"
 
(* value "amplia [d,a] t" ― ‹= [d,a,t]› *)
 
text {* --------------------------------------------------------------- 
  Ejercicio 4. 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 ∧
  ----------------------------------------------------------------- *}
 
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos p xs = undefined"
 
(* value "todos (λx. x>(1::nat)) [2,6,4]" ― ‹= True› *)
(* value "todos (λx. x>(2::nat)) [2,6,4]" ― ‹= False› *)
 
text {* 
  --------------------------------------------------------------------- 
  Ejercicio 5. Definir la función 
     algunos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
  tal que (algunos p xs) se verifica si algunos elementos de la lista 
  xs cumplen la propiedad p. Por ejemplo, se verifica 
     algunos (λx. 1<length x) [[2,1,4],[3]]
     ¬algunos (λx. 1<length x) [[],[3]]"

  Nota: La función algunos es equivalente a la predefinida list_ex. 
  --------------------------------------------------------------------- 
*}

fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p xs = undefined"

 text {*
  --------------------------------------------------------------------- 
  Ejercicio 6. Definir recursivamente la función 
     estaEn :: 'a ⇒ 'a list ⇒ bool
  tal que (estaEn x xs) se verifica si el elemento x está en la lista
  xs. Por ejemplo, 
     estaEn (2::nat) [3,2,4] = True
     estaEn (1::nat) [3,2,4] = False
  --------------------------------------------------------------------- 
*}

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x xs = undefined"

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 7. Definir recursivamemte la función
     sinDuplicados :: 'a list ⇒ bool
  tal que (sinDuplicados xs) se verifica si la lista xs no contiene
  duplicados. Por ejemplo,  
     sinDuplicados [1::nat,4,2]   = True
     sinDuplicados [1::nat,4,2,4] = False
  --------------------------------------------------------------------- 
*}

fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados xs = undefined"


text {* 
  --------------------------------------------------------------------- 
  Ejercicio 8. Definir la recursivamente la función
     borraDuplicados :: 'a list ⇒ bool
  tal que (borraDuplicados xs) es la lista obtenida eliminando los
  elementos duplicados de la lista xs. Por ejemplo, 
     borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

  Nota: La función borraDuplicados es equivalente a la predefinida 
  remdups. 
  --------------------------------------------------------------------- 
*}


fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados xs = undefined"


end


</source>