Jalonso: Protegió «R10» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-02-13T14:14:34Z

Protegió «R10» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

← Revisión anterior	Revisión del 14:14 13 feb 2020
(Sin diferencias)

Jalonso: Página creada con « chapter ‹R10: Verificación de la ordenación por mezcla› theory R10_Verificacion_de_la_ordenacion_por_mezcla imports Main begin text ‹En e…»

2020-02-13T14:13:24Z

Página creada con «<source lang="isabelle"> chapter ‹R10: Verificación de la ordenación por mezcla› theory R10_Verificacion_de_la_ordenacion_por_mezcla imports Main begin text ‹En e…»

Página nueva

<source lang="isabelle">
chapter ‹R10: Verificación de la ordenación por mezcla›

theory R10_Verificacion_de_la_ordenacion_por_mezcla
imports Main
begin

text ‹En esta relación de ejercicios se define el algoritmo de
ordenación de listas por mezcla y se demuestra que es correcto.›

section ‹Ordenación de listas›

text ‹-----------------------------------------------------------------
Ejercicio 1. Definir la función
menor :: int ⇒ int list ⇒ bool
tal que (menor a xs) se verifica si a es menor o igual que todos los
elementos de xs.Por ejemplo,
menor 2 [3,2,5] = True
menor 2 [3,0,5] = False
------------------------------------------------------------------›

fun menor :: "int ⇒ int list ⇒ bool" where
"menor a xs = undefined"

text ‹------------------------------------------------------------------
Ejercicio 2. Definir la función
ordenada :: int list ⇒ bool
tal que (ordenada xs) se verifica si xs es una lista ordenada de
manera creciente. Por ejemplo,
ordenada [2,3,3,5] = True
ordenada [2,4,3,5] = False
---------------------------------------------------------------------›

fun ordenada :: "int list ⇒ bool" where
"ordenada xs = undefined"

text ‹------------------------------------------------------------------
Ejercicio 3. Definir la función
cuenta :: int list => int => nat
tal que (cuenta xs y) es el número de veces que aparece el elemento y
en la lista xs. Por ejemplo,
cuenta [1,3,4,3,5] 3 = 2
---------------------------------------------------------------------›

fun cuenta :: "int list => int => nat" where
"cuenta xs y = undefined"

section ‹Ordenación por mezcla›

text ‹------------------------------------------------------------------
Ejercicio 4. Definir la función
mezcla :: int list ⇒ int list ⇒ int list
tal que (mezcla xs ys) es la lista obtenida mezclando las listas
ordenadas xs e ys. Por ejemplo,
mezcla [1,2,5] [3,5,7] = [1,2,3,5,5,7]
---------------------------------------------------------------------›

fun mezcla :: "int list ⇒ int list ⇒ int list" where
"mezcla xs ys = undefined"

text ‹------------------------------------------------------------------
Ejercicio 5. Definir la función
ordenaM :: int list ⇒ int list
tal que (ordenaM xs) es la lista obtenida ordenando la lista xs
mediante mezclas; es decir, la divide en dos mitades, las ordena y las
mezcla. Por ejemplo,
ordenaM [3,2,5,2] = [2,2,3,5]
---------------------------------------------------------------------›

fun ordenaM :: "int list ⇒ int list" where
"ordenaM xs = undefined"

text ‹------------------------------------------------------------------
Ejercicio 6. Sea x ≤ y. Si y es menor o igual que todos los elementos
de xs, entonces x es menor o igual que todos los elementos de xs
---------------------------------------------------------------------›

lemma menor_menor:
"x ≤ y ⟹ menor y xs ⟶ menor x xs"
oops

text ‹------------------------------------------------------------------
Ejercicio 7. Demostrar que el número de veces que aparece n en la
mezcla de dos listas es igual a la suma del número de apariciones en
cada una de las listas
---------------------------------------------------------------------›

lemma cuenta_mezcla:
"cuenta (mezcla xs ys) n = cuenta xs n + cuenta ys n"
oops

text ‹------------------------------------------------------------------
Ejercicio 8. Demostrar que si x es menor que todos los elementos de
ys y de zs, entonces también lo es de su mezcla.
---------------------------------------------------------------------›

lemma menor_mezcla:
assumes "menor x ys"
"menor x zs"
shows "menor x (mezcla ys zs)"
oops

text ‹------------------------------------------------------------------
Ejercicio 9. Demostrar que la mezcla de dos listas ordenadas es una
lista ordenada.

Indicación: Usar los siguientes lemas
· linorder_not_le: (¬ x ≤ y) = (y < x)
· order_less_le: (x < y) = (x ≤ y ∧ x ≠ y)
------------------------------------------------------------------›

lemma ordenada_mezcla:
assumes "ordenada xs"
"ordenada ys"
shows "ordenada (mezcla xs ys)"
oops

text ‹------------------------------------------------------------------
Ejercicio 10. Demostrar que si x es mayor que 1, entonces el mínimo de
x y su mitad es menor que x.
---------------------------------------------------------------------›

lemma min_mitad:
"1 < x ⟹ min x (x div 2::int) < x"
oops

text ‹------------------------------------------------------------------
Ejercicio 11. Demostrar que si x es mayor que 1, entonces x menos su
mitad es menor que x.
---------------------------------------------------------------------›

lemma menos_mitad:
"1 < x ⟹ x - x div (2::int) < x"
oops

text ‹------------------------------------------------------------------
Ejercicio 11. Demostrar que (ordenaM xs) está ordenada.
---------------------------------------------------------------------›

theorem ordenada_ordenaM:
"ordenada (ordenaM xs)"
oops

text ‹------------------------------------------------------------------
Ejercicio 12. Demostrar que el número de apariciones de un elemento en
la concatenación de dos listas es la suma del número de apariciones en
cada una.
---------------------------------------------------------------------›

lemma cuenta_conc:
"cuenta (xs @ ys) x = cuenta xs x + cuenta ys x"
oops

text ‹------------------------------------------------------------------
Ejercicio 13. Demostrar que las listas xs y (ordenaM xs) tienen los
mismos elementos.
---------------------------------------------------------------------›

theorem cuenta_ordenaM:
"cuenta (ordenaM xs) x = cuenta xs x"
oops

end
</source>

R10 - Historial de revisiones

Jalonso: Protegió «R10» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Jalonso: Página creada con « chapter ‹R10: Verificación de la ordenación por mezcla› theory R10_Verificacion_de_la_ordenacion_por_mezcla imports Main begin text ‹En e…»