Rel 9 (rev 1)

chapter ‹ R9: Programación funcional en Isabelle/HOL (II) ›
 
theory R9_wiki_rev
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
  ------------------------------------------------------------------ ›
 
(*antrivmar inehenluq enrniecar dessanriv juanarcon carboncar rosmargon1 laudiasan1
monlagare*)
  fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
  "sumaPotenciasDeDosMasUno 0 = 1 + 2^0 "
 |"sumaPotenciasDeDosMasUno (Suc m ) = sumaPotenciasDeDosMasUno m + 2^(Suc m)"

(*inmrodmon anapalsan3 elivazser manmorgar12*)
 fun sumaPotenciasDeDosMasUno1 :: "nat ⇒ nat" where
  "sumaPotenciasDeDosMasUno1 0 = 1 + 2^0"
| "sumaPotenciasDeDosMasUno1 n = 2^n + sumaPotenciasDeDosMasUno (n-1)"
value "sumaPotenciasDeDosMasUno 3" ― ‹= 16›
   

(*dantruvar josfloval*)
fun sumaPotenciasDeDosMasUno2 :: "nat ⇒ nat" where
  "sumaPotenciasDeDosMasUno2 0 = 2"
| "sumaPotenciasDeDosMasUno2 (Suc n) = 2^(Suc n) + sumaPotenciasDeDosMasUno2 n"

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

  ------------------------------------------------------------------- ›
 (* enrniecar antrivmar inmrodmon anapalsan3 dessanriv dantruvar elivazser
 juanarcon josfloval carboncar manmorgar12 laudiasan1 monlagare*)
fun factI' :: "nat ⇒ nat ⇒ nat" where
 "factI' 0       x = x"
|"factI' (Suc n) x = factI' n (Suc n)*x"

fun factI :: "nat ⇒ nat" where
   "factI n = factI' n 1"
 
(* 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]
  ------------------------------------------------------------------ ›
 (*inehenluq antrivmar anapalsan3 dessanriv josfloval carboncar monlagare*)
fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
 "amplia [] y = [y]"
|"amplia (x#xs) y = x#(amplia xs y)"
 
(*enrniecar*)
fun amplia2 :: "'a list ⇒ 'a ⇒ 'a list" where
  "amplia2 xs y = rev (Cons y (rev(xs)))"

(*dantruvar elivazser rosmargon1*)
fun amplia3 :: "'a list ⇒ 'a ⇒ 'a list" where
  "amplia3 [] x = [x]"
| "amplia3 (Cons x xs) y = Cons x (amplia3 xs y)"

(* juanarcon *)
fun amplia4 :: "'a list ⇒ 'a ⇒ 'a list" where
  "amplia4 xs y = xs @ [y]"

(* manmorgar12*)
fun amplia5 :: "'a list ⇒ 'a ⇒ 'a list" where
  "amplia5 [] y = [y]" 
| "amplia5 xs y = rev(y#(rev(xs)))"

(* laudiasan1 *)
fun amplia'6 :: "'a list ⇒ 'a list ⇒ 'a list" where
  "amplia'6 [] ys = ys"
| "amplia'6 xs ys = amplia'6 (butlast xs) ((last xs)#ys)"

fun amplia6 :: "'a list ⇒ 'a ⇒ 'a list" where
  "amplia6 xs y = amplia'6 xs [y]"

value "amplia6 [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 ∧
  ----------------------------------------------------------------- ›
 (*inehenluq inmrodmon antrivmar anapalsan3 dessanriv carboncar manmorgar12 laudiasan1
monlagare*)
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos p [] = True"
| "todos p (x#xs) = ((p x) ∧ (todos p xs))" 

(*enrniecar juanarcon josfloval rosmargon1(dentro de if basta con "p x") *) 
fun todos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos2 p [] = True"
| "todos2 p (Cons x xs) = (if (p x) =True then (todos p xs) else False)"

(*dantruvar elivazser*)
fun todos3 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos3 p [] = True"
| "todos3 p (Cons x xs) = (p x ∧ todos3 p xs)"

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. 
  --------------------------------------------------------------------- 
›
(*inehenluq anapalsan3 dessanriv carboncar manmorgar12 laudiasan1 monlagare*)
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
 "algunos p [] = False"
|"algunos p (x#xs) = ((p x) ∨ (algunos p xs))"

(*enrniecar rosmargon1*)
fun algunos1  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos1 p [] =False "
| "algunos1 p (Cons x xs) =(if (p x) = True then True else algunos1 p xs)"
 
(*antrivmar inmrodmon*)
fun algunos2  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos2 p [] = False"
|"algunos2 p (x#xs) = (if p x then True else algunos p xs)"

(*dantruvar elivazser juanarcon josfloval*)
fun algunos3  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos3 p [] = False"
| "algunos3 p (Cons x xs) = (p x ∨ algunos3 p xs)"

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
  --------------------------------------------------------------------- 
›
(*inehenluq anapalsan3 dessanriv dantruvar carboncar laudiasan1 monlagare*)
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
 "estaEn x [] = False"
|"estaEn x (y#ys) = ((x=y)∨(estaEn x ys))"

(*enrniecar juanarcon*)
fun estaEn2 :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn2 x [] = False"
| "estaEn2 y (Cons x xs) =(if x=y then True else estaEn2 y xs)"

(*rosmargon1*)
fun estaEn1 :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn1 y [] = False"
| "estaEn1 y (Cons x xs) =((y=x) ∨ (estaEn1 y xs))"

(*inmrodmon*)
fun estaEn3 :: "'a ⇒ 'a list ⇒ bool" where
    "estaEn3 x [] = False"
|   "estaEn3 x xs = (if x=(hd xs) then True else estaEn1 x (tl xs))" 

(*antrivmar manmorgar12*)
fun estaEn4 :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn4 y [] = False"
| "estaEn4 y (x#xs) = (if y = x then True else estaEn4 y xs)"

(*elivazser*)
fun estaEn5 :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn5 x [] = False"
| "estaEn5 x (Cons y xs) = ( x = y ∨ estaEn5 x xs)"

(*josfloval*)
fun estaEn6 :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn6 x xs = algunos (λy. y=x) xs"

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
  --------------------------------------------------------------------- 
›
(*inehenluq *)
fun sinDuplicados :: "'a list ⇒ bool" where
 "sinDuplicados [] = True"
|"sinDuplicados [x] = True"
|"sinDuplicados (x#(y#xs))=((¬(x=y))∧(sinDuplicados (x#xs))∧(sinDuplicados (y#xs))
                            ∧(sinDuplicados xs))"

(* Comentario: para definir sinDuplicados es conveniente usar la función estaEn *)

(*enrniecar dessanriv dantruvar elivazser josfloval laudiasan1 monlagare*)
fun sinDuplicados2 :: "'a list ⇒ bool" where
  "sinDuplicados2 [] = True"
| "sinDuplicados2 (Cons x xs) = ((¬estaEn x xs) ∧ (sinDuplicados2 xs))" 
   (*estaEn está definida en el ejercicio anterior*)

(*antrivmar inmrodmon juanarcon carboncar manmorgar12*)
fun sinDuplicados3 :: "'a list ⇒ bool" where
 "sinDuplicados3 [] = True"
|"sinDuplicados3 (x#xs) = (if (estaEn x xs) then False else sinDuplicados3 xs)"

(*anapalsan3*)
fun sinDuplicados4 :: "'a list ⇒ bool" where
 "sinDuplicados4 [] = True"
|"sinDuplicados4 (x#xs) =( (¬(estaEn x xs))  ∧ (sinDuplicados4 xs))" 

(*rosmargon1*)
fun sinDuplicados5 :: "'a list ⇒ bool" where
  "sinDuplicados5 [] = True"
| "sinDuplicados5 (Cons x xs) = (if (estaEn x xs) then False else sinDuplicados5 xs)"

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. 
  --------------------------------------------------------------------- 
›
(*enrniecar*)
fun aux :: "'a list ⇒ 'a list ⇒ 'a list" where
 "aux [] ys=ys"
|"aux (Cons x xs) ys=(if estaEn x ys then aux xs ys else aux xs (Cons x ys))"

fun borraDuplicados :: "'a list ⇒ 'a list" where
   "borraDuplicados xs= aux (rev(xs)) []"

(*antrivmar inmrodmon dessanriv anapalsan3 dantruvar josfloval carboncar manmorgar12 laudiasan1*)
fun borraDuplicados1 :: "'a list ⇒ 'a list" where
 "borraDuplicados1 [] = []"
|"borraDuplicados1 (x#xs) = 
  (if (estaEn x xs ) then borraDuplicados1 xs else  x#(borraDuplicados1 xs))"

(*elivazser juanarcon rosmargon1*)
fun borraDuplicados2 :: "'a list ⇒ 'a list" where
  "borraDuplicados2 [] = []"
| "borraDuplicados2 (Cons x xs) = 
  (if (estaEn x xs) then (borraDuplicados2 xs) else (Cons x (borraDuplicados2 xs)))"

end