Diferencia entre revisiones de «Relación 1»
De Razonamiento automático (2013-14)
Línea 5: | Línea 5: | ||
imports Main | imports Main | ||
begin | begin | ||
+ | |||
+ | text {* ---------------------------------------------------------------- | ||
+ | Ejercicio 0. Definir, por recursión, la función | ||
+ | factorial :: nat ⇒ nat | ||
+ | tal que (factorial n) es el factorial de n. Por ejemplo, | ||
+ | factorial 4 = 24 | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | fun factorial :: "nat ⇒ nat" where | ||
+ | "factorial n = undefined" | ||
+ | |||
+ | value "factorial 4" -- "24" | ||
text {* ---------------------------------------------------------------- | text {* ---------------------------------------------------------------- | ||
Línea 14: | Línea 26: | ||
-- "maresccas4" | -- "maresccas4" | ||
− | |||
fun longitud :: "'a list ⇒ nat" where | fun longitud :: "'a list ⇒ nat" where | ||
"longitud [] = 0" | "longitud [] = 0" | ||
− | + | | "longitud (x # xs) = Suc (longitud xs)" | |
+ | |||
+ | value "longitud [4,2,5]" -- "= 3" | ||
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun longitud2 :: "'a list ⇒ nat" where |
− | " | + | "longitud2 [] = (0::nat)" |
− | + | | "longitud2 xs = 1 + longitud2 (tl xs) " | |
− | value " | + | value "longitud2 [4,2,5]" -- "= 3" |
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 35: | Línea 48: | ||
-- "maresccas4" | -- "maresccas4" | ||
− | |||
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where | fun intercambia :: "'a × 'b ⇒ 'b × 'a" where | ||
"intercambia p = (snd p, fst p)" | "intercambia p = (snd p, fst p)" | ||
+ | |||
+ | value "intercambia (u,v)" -- "= (v,u)" | ||
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun intercambia2 :: "'a × 'b ⇒ 'b × 'a" where |
− | " | + | "intercambia2 (x,y) = (y,x)" |
− | value " | + | value "intercambia2 (u,v)" -- "= (v,u)" |
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 54: | Línea 68: | ||
-- "maresccas4" | -- "maresccas4" | ||
+ | fun inversa :: "'a list ⇒ 'a list" where | ||
+ | "inversa [] = []" | ||
+ | | "inversa (x#xs) = inversa xs @ (x#[])" | ||
− | + | value "inversa [a,d,c]" -- "= [c,d,a]" | |
− | |||
− | |||
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun inversa2 :: "'a list ⇒ 'a list" where |
− | " | + | "inversa2 [] = [] " |
− | + | | "inversa2 xs = inversa2 (tl xs) @ (hd xs#[])" | |
− | value " | + | value "inversa2 [a,d,c]" -- "= [c,d,a]" |
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 75: | Línea 90: | ||
-- "maresccas4" | -- "maresccas4" | ||
+ | fun repite :: "nat ⇒ 'a ⇒ 'a list" where | ||
+ | "repite 0 x = []" | ||
+ | | "repite (Suc n) x = x # repite n x" | ||
− | + | value "repite 3 a" -- "= [a,a,a]" | |
− | + | ||
− | + | (* La siguiente definición es incorrecta: | |
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun repite2 :: "nat ⇒ 'a ⇒ 'a list" where |
− | " | + | "repite2 (0::nat) x = []" |
− | + | | "repite2 n x = x # (repite2 (n-1) x) " | |
− | value " | + | value "repite2 3 a" -- "= [a,a,a]" |
+ | *) | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 96: | Línea 115: | ||
-- "maresccas4" | -- "maresccas4" | ||
+ | fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where | ||
+ | "conc [] ys = ys" | ||
+ | | "conc (x#xs) ys = x # conc xs ys" | ||
− | + | value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]" | |
− | |||
− | |||
-- irealetei | -- irealetei | ||
− | fun | + | fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where |
− | + | "conc2 xs [] = xs" | |
− | + | | "conc2 xs ys = hd ys # conc2 xs (tl ys)" | |
− | value " | + | value "conc2 [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]" |
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 117: | Línea 137: | ||
-- "maresccas4" | -- "maresccas4" | ||
− | |||
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where | fun coge :: "nat ⇒ 'a list ⇒ 'a list" where | ||
− | "coge 0 xs = []" | + | "coge 0 xs = []" |
− | + | | "coge n [] = []" | |
− | + | | "coge (Suc n) (x#xs) = x # (coge n xs)" | |
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun coge2 :: "nat ⇒ 'a list ⇒ 'a list" where |
− | + | "coge2 0 xs = []" | |
− | + | | "coge2 n xs = hd(xs) # (coge2 (n - 1) (tl xs))" | |
value "coge 2 [a,c,d,b,e]" -- "= [a,c]" | value "coge 2 [a,c,d,b,e]" -- "= [a,c]" | ||
Línea 139: | Línea 158: | ||
-- "maresccas4" | -- "maresccas4" | ||
+ | fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where | ||
+ | "elimina 0 xs = xs" | ||
+ | | "elimina n [] = []" | ||
+ | | "elimina (Suc n) (x#xs) = elimina n xs" | ||
− | + | value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]" | |
− | |||
− | |||
− | |||
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun elimina2 :: "nat ⇒ 'a list ⇒ 'a list" where |
− | + | " elimina2 0 xs = xs " | |
− | + | | "elimina2 n xs = elimina2 (n - 1) (tl xs)" | |
− | value " | + | value "elimina2 2 [a,c,d,b,e]" -- "= [d,b,e]" |
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 161: | Línea 181: | ||
-- "maresccas4" | -- "maresccas4" | ||
− | |||
fun esVacia :: "'a list ⇒ bool" where | fun esVacia :: "'a list ⇒ bool" where | ||
"esVacia [] = True" | "esVacia [] = True" | ||
− | + | | "esVacia (x#xs) = False" | |
value "esVacia []" -- "= True" | value "esVacia []" -- "= True" | ||
Línea 170: | Línea 189: | ||
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun esVacia2 :: "'a list ⇒ bool" where |
− | " | + | "esVacia2 [] = True" |
− | |" | + | | "esVacia2 xs = False" |
+ | |||
+ | value "esVacia2 []" -- "= True" | ||
+ | value "esVacia2 [1]" -- "= False" | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 183: | Línea 205: | ||
-- "maresccas4" | -- "maresccas4" | ||
− | |||
fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where | fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where | ||
− | "inversaAcAux [] ys = ys" | + | "inversaAcAux [] ys = ys" |
− | + | | "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)" | |
fun inversaAc :: "'a list ⇒ 'a list" where | fun inversaAc :: "'a list ⇒ 'a list" where | ||
"inversaAc xs = inversaAcAux xs []" | "inversaAc xs = inversaAcAux xs []" | ||
+ | |||
+ | value "inversaAc2 [a,c,b,e]" -- "= [e,b,c,a]" | ||
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun inversaAc2Aux :: "'a list ⇒ 'a list ⇒ 'a list" where |
− | " | + | "inversaAc2Aux xs [] = xs" |
− | + | | "inversaAc2Aux xs ys = inversaAc2Aux ((hd ys) # xs) (tl ys)" | |
− | fun | + | fun inversaAc2 :: "'a list ⇒ 'a list" where |
− | " | + | "inversaAc2 xs = inversaAc2Aux [] xs" |
− | value " | + | value "inversaAc2 [a,c,b,e]" -- "= [e,b,c,a]" |
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 209: | Línea 232: | ||
-- "maresccas4" | -- "maresccas4" | ||
+ | fun sum :: "nat list ⇒ nat" where | ||
+ | "sum [] = 0" | ||
+ | | "sum (x#xs) = x + sum xs" | ||
− | + | value "sum [3,2,5]" -- "= 10" | |
− | |||
− | |||
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun sum2 :: "nat list ⇒ nat" where |
− | " | + | "sum2 [] = 0" |
− | |" | + | |"sum2 xs = hd xs + sum2 (tl xs)" |
− | value " | + | value "sum2 [3,2,5]" -- "= 10" |
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 230: | Línea 254: | ||
-- "maresccas4" | -- "maresccas4" | ||
+ | fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where | ||
+ | "map f [] = []" | ||
+ | | "map f (x#xs) = (f x) # map f xs" | ||
− | + | value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]" | |
− | |||
− | |||
-- "irealetei" | -- "irealetei" | ||
− | fun | + | fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where |
− | " | + | "map2 f [] = []" |
− | |" | + | |"map2 f xs = f(hd xs) # map2 f (tl xs)" |
− | value " | + | value "map2 (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]" |
end | end | ||
</source> | </source> |
Revisión del 08:34 9 nov 2013
header {* R1: Programación funcional en Isabelle *}
theory R1
imports Main
begin
text {* ----------------------------------------------------------------
Ejercicio 0. Definir, por recursión, la función
factorial :: nat ⇒ nat
tal que (factorial n) es el factorial de n. Por ejemplo,
factorial 4 = 24
------------------------------------------------------------------- *}
fun factorial :: "nat ⇒ nat" where
"factorial n = undefined"
value "factorial 4" -- "24"
text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}
-- "maresccas4"
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x # xs) = Suc (longitud xs)"
value "longitud [4,2,5]" -- "= 3"
-- "irealetei"
fun longitud2 :: "'a list ⇒ nat" where
"longitud2 [] = (0::nat)"
| "longitud2 xs = 1 + longitud2 (tl xs) "
value "longitud2 [4,2,5]" -- "= 3"
text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}
-- "maresccas4"
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia p = (snd p, fst p)"
value "intercambia (u,v)" -- "= (v,u)"
-- "irealetei"
fun intercambia2 :: "'a × 'b ⇒ 'b × 'a" where
"intercambia2 (x,y) = (y,x)"
value "intercambia2 (u,v)" -- "= (v,u)"
text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}
-- "maresccas4"
fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ (x#[])"
value "inversa [a,d,c]" -- "= [c,d,a]"
-- "irealetei"
fun inversa2 :: "'a list ⇒ 'a list" where
"inversa2 [] = [] "
| "inversa2 xs = inversa2 (tl xs) @ (hd xs#[])"
value "inversa2 [a,d,c]" -- "= [c,d,a]"
text {* ---------------------------------------------------------------
Ejercicio 4. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}
-- "maresccas4"
fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
| "repite (Suc n) x = x # repite n x"
value "repite 3 a" -- "= [a,a,a]"
(* La siguiente definición es incorrecta:
-- "irealetei"
fun repite2 :: "nat ⇒ 'a ⇒ 'a list" where
"repite2 (0::nat) x = []"
| "repite2 n x = x # (repite2 (n-1) x) "
value "repite2 3 a" -- "= [a,a,a]"
*)
text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}
-- "maresccas4"
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # conc xs ys"
value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"
-- irealetei
fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc2 xs [] = xs"
| "conc2 xs ys = hd ys # conc2 xs (tl ys)"
value "conc2 [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"
text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}
-- "maresccas4"
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge 0 xs = []"
| "coge n [] = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"
-- "irealetei"
fun coge2 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge2 0 xs = []"
| "coge2 n xs = hd(xs) # (coge2 (n - 1) (tl xs))"
value "coge 2 [a,c,d,b,e]" -- "= [a,c]"
text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}
-- "maresccas4"
fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina 0 xs = xs"
| "elimina n [] = []"
| "elimina (Suc n) (x#xs) = elimina n xs"
value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"
-- "irealetei"
fun elimina2 :: "nat ⇒ 'a list ⇒ 'a list" where
" elimina2 0 xs = xs "
| "elimina2 n xs = elimina2 (n - 1) (tl xs)"
value "elimina2 2 [a,c,d,b,e]" -- "= [d,b,e]"
text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}
-- "maresccas4"
fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"
value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"
-- "irealetei"
fun esVacia2 :: "'a list ⇒ bool" where
"esVacia2 [] = True"
| "esVacia2 xs = False"
value "esVacia2 []" -- "= True"
value "esVacia2 [1]" -- "= False"
text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}
-- "maresccas4"
fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"
fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"
value "inversaAc2 [a,c,b,e]" -- "= [e,b,c,a]"
-- "irealetei"
fun inversaAc2Aux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAc2Aux xs [] = xs"
| "inversaAc2Aux xs ys = inversaAc2Aux ((hd ys) # xs) (tl ys)"
fun inversaAc2 :: "'a list ⇒ 'a list" where
"inversaAc2 xs = inversaAc2Aux [] xs"
value "inversaAc2 [a,c,b,e]" -- "= [e,b,c,a]"
text {* ---------------------------------------------------------------
Ejercicio 10. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}
-- "maresccas4"
fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"
value "sum [3,2,5]" -- "= 10"
-- "irealetei"
fun sum2 :: "nat list ⇒ nat" where
"sum2 [] = 0"
|"sum2 xs = hd xs + sum2 (tl xs)"
value "sum2 [3,2,5]" -- "= 10"
text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}
-- "maresccas4"
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"
value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"
-- "irealetei"
fun map2 :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map2 f [] = []"
|"map2 f xs = f(hd xs) # map2 f (tl xs)"
value "map2 (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"
end