Jalonso: Texto reemplazado: «lang="isar"» por «lang="isabelle"»

2018-07-15T11:57:32Z

Texto reemplazado: «lang="isar"» por «lang="isabelle"»

Jalonso: Página creada con ' header {* R14: Contador de occurrencias } theory R14 imports Main begin text { --------------------------------------------------------------------- ...'

2013-05-02T09:20:46Z

Página creada con '<source lang="isar"> header {* R14: Contador de occurrencias *} theory R14 imports Main begin text {* --------------------------------------------------------------------- ...'

Página nueva

<source lang="isar">
header {* R14: Contador de occurrencias *}

theory R14
imports Main
begin

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
---------------------------------------------------------------------
*}

fun veces :: "'a ⇒ 'a list ⇒ nat" where
"veces x ys = undefined"

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

lemma veces_append:
"veces a (xs @ ys) = veces a xs + veces a ys"
oops

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

lemma veces_rev:
"veces a xs = veces a (rev xs)"
oops

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

lemma veces_le_length_auto:
"veces a xs ≤ length xs"
oops

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
---------------------------------------------------------------------
*}

lemma veces_map:
"veces a (map f xs) = veces (f a) xs"
oops

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
y demostrar la conjetura.
---------------------------------------------------------------------
*}

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.
---------------------------------------------------------------------
*}

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

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

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".
---------------------------------------------------------------------
*}

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

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

lemma distintos_borraDups:
"distintos (borraDups xs)"
oops

end
</source>

← Revisión anterior		Revisión del 11:57 15 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R14: Contador de occurrencias *}		header {* R14: Contador de occurrencias *}

RA12 Relación 14 - Historial de revisiones

Jalonso: Texto reemplazado: «lang="isar"» por «lang="isabelle"»

Jalonso: Página creada con ' header {* R14: Contador de occurrencias *} theory R14 imports Main begin text {* --------------------------------------------------------------------- ...'

Jalonso: Página creada con ' header {* R14: Contador de occurrencias } theory R14 imports Main begin text { --------------------------------------------------------------------- ...'