Jalonso en 07:51 16 jul 2018

2018-07-16T07:51:11Z

Jalonso: Protegió «Rel 7» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2011-02-22T05:28:36Z

Protegió «Rel 7» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* 7ª relación de ejercicios } theory Relacion_7_sol imports Main Efficient_Nat begin section { Contador de occurrencias } text { --------...'

2011-02-22T05:28:25Z

Página creada con '<source lang="isar"> header {* 7ª relación de ejercicios *} theory Relacion_7_sol imports Main Efficient_Nat begin section {* Contador de occurrencias *} text {* --------...'

Página nueva

<source lang="isar">
header {* 7ª relación de ejercicios *}

theory Relacion_7_sol
imports Main Efficient_Nat
begin

section {* Contador de occurrencias *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
veces :: "'a ⇒ 'a list ⇒ nat"
tal que (veces x ys) es el número de occurrencias del elemento x en la
lista ys. Por ejemplo,
veces (2::nat) [2,1,2,5,2] = 3
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
veces a (xs @ ys) = veces a xs + veces a ys
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar:
veces a xs = veces a (rev xs)
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar:
"veces a xs ≤ length xs".
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 5. Sabiendo que la función map aplica una función a todos los
elementos de una lista:
map f [x\<^isub>1,…,x\<^isub>n] = [f x\<^isub>1,…,f x\<^isub>n],
demostrar o refutar
veces a (map f xs) = veces (f a) xs
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 6. La función
filter :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list"
está definida por
filter P [] = []
filter P (x # xs) = (if P x then x # filter P xs else filter P xs)
Encontrar una expresión e que no contenga filter tal que se verifique
la siguiente propiedad:
veces a (filter P xs) = e
---------------------------------------------------------------------
*}

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

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

text {*
---------------------------------------------------------------------
Ejercicio 8. Encontrar una expresión e que no contenga la función
borraDups tal que se verifique
veces x (borraDups xs) = e
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 9. Usando la función "veces", definir la función
distintos :: "'a list ⇒ bool"
tal que (distintos xs) se verifica si cada elemento de xs aparece tan
solo una vez. Por ejemplo,
distintos [1,4,3]
¬ distintos [1,4,1]

Nota: La función "distintos" es equivalente a la predefinida "distinct".
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que el valor de "borraDups" verifica "distintos".
---------------------------------------------------------------------
*}

end
</source>

← Revisión anterior		Revisión del 07:51 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* 7ª relación de ejercicios *}		header {* 7ª relación de ejercicios *}

← Revisión anterior	Revisión del 05:28 22 feb 2011
(Sin diferencias)

Rel 7 - Historial de revisiones

Jalonso en 07:51 16 jul 2018

Jalonso: Protegió «Rel 7» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* 7ª relación de ejercicios *} theory Relacion_7_sol imports Main Efficient_Nat begin section {* Contador de occurrencias *} text {* --------...'

Jalonso: Página creada con ' header {* 7ª relación de ejercicios } theory Relacion_7_sol imports Main Efficient_Nat begin section { Contador de occurrencias } text { --------...'