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

2018-07-15T11:52:06Z

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

Jalonso: Página creada con ' header {* R15: Suma y aplanamiento de listas } theory R15 imports Main R10 begin section { Suma y aplanamiento de listas } text { --------------...'

2013-05-15T20:49:43Z

Página creada con '<source lang="isar"> header {* R15: Suma y aplanamiento de listas *} theory R15 imports Main R10 begin section {* Suma y aplanamiento de listas *} text {* --------------...'

Página nueva

<source lang="isar">
header {* R15: Suma y aplanamiento de listas *}

theory R15
imports Main R10
begin

section {* Suma y aplanamiento de listas *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
suma :: "nat list ⇒ nat"
tal que (suma xs) es la suma de los elementos de la lista de números
naturales xs. Por ejemplo,
suma [3::nat,2,4] = 9
---------------------------------------------------------------------
*}

fun suma :: "nat list ⇒ nat" where
"suma xs = undefined"

value "suma [3::nat,2,4]" -- "= 9"

text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
aplana :: "'a list list ⇒ 'a list"
tal que (aplana xss) es la obtenida concatenando los miembros de la
lista de listas "xss". Por ejemplo,
aplana [[2,3], [4,5], [7,9]] = [2,3,4,5,7,9]
---------------------------------------------------------------------
*}

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

value "aplana [[2::nat,3], [4,5], [7,9]]" -- "= [2,3,4,5,7,9]"

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar
length (aplana xs) = suma (map length xs)
---------------------------------------------------------------------
*}

lemma length_aplana:
"length (aplana xs) = suma (map length xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar
suma (xs @ ys) = suma xs + suma ys
---------------------------------------------------------------------
*}

lemma suma_append:
"suma (xs @ ys) = suma xs + suma ys"
oops

text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar
aplana (xs @ ys) = (aplana xs) @ (aplana ys)
---------------------------------------------------------------------
*}

lemma aplana_append:
"aplana (xs @ ys) = (aplana xs) @ (aplana ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar
aplana (map rev (rev xs)) = rev (aplana xs)
---------------------------------------------------------------------
*}

lemma aplana_map_rev_rev:
"aplana (map rev (rev xs)) = rev (aplana xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar o refutar
aplana (rev (map rev xs)) = rev (aplana xs)
---------------------------------------------------------------------
*}

lemma aplana_rev_map_rev:
"aplana (rev (map rev xs)) = rev (aplana xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar
list_all (list_all P) xs = list_all P (aplana xs)
---------------------------------------------------------------------
*}

lemma list_all_list_all:
"list_all (list_all P) xs = list_all P (aplana xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar o refutar
aplana (rev xs) = aplana xs
---------------------------------------------------------------------
*}

lemma aplana_rev:
"aplana (rev xs) = aplana xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar o refutar
suma (rev xs) = suma xs
---------------------------------------------------------------------
*}

lemma suma_rev:
"suma (rev xs) = suma xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 11. Buscar un predicado P para que se verifique la siguiente
propiedad
list_all P xs ⟶ length xs ≤ suma xs
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar
algunos (algunos P) xs = algunos P (aplana xs)
---------------------------------------------------------------------
*}

lemma algunos_algunos:
"algunos (algunos P) xs = algunos P (aplana xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 13. Redefinir, usando la función list_all, la función
algunos. Llamar la nueva función algunos2 y demostrar que es
equivalente a algunos.
---------------------------------------------------------------------
*}

fun algunos2 :: "('a ⇒ bool) ⇒ ('a list ⇒ bool)" where
"algunos2 P xs = undefined"

lemma algunos2_algunos:
"algunos2 P xs = algunos P xs"
oops

end
</source>

← Revisión anterior		Revisión del 11:52 15 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R15: Suma y aplanamiento de listas *}		header {* R15: Suma y aplanamiento de listas *}

RA12 Relación 15 - Historial de revisiones

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

Jalonso: Página creada con ' header {* R15: Suma y aplanamiento de listas *} theory R15 imports Main R10 begin section {* Suma y aplanamiento de listas *} text {* --------------...'

Jalonso: Página creada con ' header {* R15: Suma y aplanamiento de listas } theory R15 imports Main R10 begin section { Suma y aplanamiento de listas } text { --------------...'