Mjoseh: Protegió «Rel 9 (rev 1)» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-04-20T17:57:23Z

Protegió «Rel 9 (rev 1)» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹ R9: Programación funcional en Isabelle/HOL (II) › theory R9_wiki_rev imports Main begin text ‹ ------------------------…»

2020-04-20T17:56:41Z

Página creada con «<source lang = "isabelle"> chapter ‹ R9: Programación funcional en Isabelle/HOL (II) › theory R9_wiki_rev imports Main begin text ‹ ------------------------…»

Página nueva

<source lang = "isabelle">

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

</source>

← Revisión anterior	Revisión del 17:57 20 abr 2020
(Sin diferencias)

Rel 9 (rev 1) - Historial de revisiones

Mjoseh: Protegió «Rel 9 (rev 1)» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹ R9: Programación funcional en Isabelle/HOL (II) › theory R9_wiki_rev imports Main begin text ‹ ------------------------…»