header {* R17: Ordenación de listas por inserción *}
theory R17
imports Main
begin
text {*
En esta relación de ejercicios se define el algoritmo de ordenación de
listas por inserción y se demuestra que es correcto.
*}
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
inserta :: nat ⇒ nat list ⇒ nat list
tal que (inserta a xs) es la lista obtenida insertando a delante del
primer elemento de xs que es mayor o igual que a. Por ejemplo,
inserta 3 [2,5,1,7] = [2,3,5,1,7]
------------------------------------------------------------------ *}
fun inserta :: "nat ⇒ nat list ⇒ nat list" where
"inserta a xs = undefined"
value "inserta 3 [2,5,1,7]" -- "= [2,3,5,1,7]"
text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
ordena :: nat list ⇒ nat list
tal que (ordena xs) es la lista obtenida ordenando xs por inserción.
Por ejemplo,
ordena [3,2,5,3] = [2,3,3,5]
------------------------------------------------------------------ *}
fun ordena :: "nat list ⇒ nat list" where
"ordena xs = undefined"
value "ordena [3,2,5,3]" -- "[2,3,3,5]"
text {*
---------------------------------------------------------------------
Ejercicio 3. Definir la función
menor :: nat ⇒ nat 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 :: "nat ⇒ nat list ⇒ bool" where
"menor a xs = undefined"
value "menor 2 [3,2,5]" -- "= True"
value "menor 2 [3,0,5]" -- "= False"
text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
ordenada :: nat 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 :: "nat list ⇒ bool" where
"ordenada xs = undefined"
value "ordenada [2,3,3,5]" -- "= True"
value "ordenada [2,4,3,5]" -- "= False"
text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar que si y es una cota inferior de xs y x ≤ y,
entonces x es una cota inferior de xs.
------------------------------------------------------------------ *}
lemma menor_menor:
assumes "x ≤ y"
shows "menor y xs ⟶ menor x xs"
oops
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar el siguiente teorema de corrección: x es una
cota inferior de la lista obtenida insertando y en zs syss x ≤ y y x
es una cota inferior de zs.
------------------------------------------------------------------ *}
lemma menor_inserta:
"menor x (inserta y zs) = (x ≤ y ∧ menor x zs)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que al insertar un elemento la lista obtenida
está ordenada syss lo estaba la original.
------------------------------------------------------------------ *}
lemma ordenada_inserta:
"ordenada (inserta a xs) = ordenada xs"
oops
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que, para toda lista xs, (ordena xs) está
ordenada.
------------------------------------------------------------------ *}
theorem ordenada_ordena:
"ordenada (ordena xs)"
oops
text {*
---------------------------------------------------------------------
Nota. El teorema anterior no garantiza que ordena sea correcta, ya que
puede que (ordena xs) no tenga los mismos elementos que xs. Por
ejemplo, si se define (ordena xs) como [] se tiene que (ordena xs)
está ordenada pero no es una ordenación de xs. Para ello, definimos la
función cuenta.
------------------------------------------------------------------ *}
text {*
---------------------------------------------------------------------
Ejercicio 8. Definir la función
cuenta :: nat list => nat => 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 :: "nat list => nat => nat" where
"cuenta xs y = undefined"
value "cuenta [1,3,4,3,5] 3" -- "= 2"
text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar que el número de veces que aparece y en
(inserta x xs) es
* uno más el número de veces que aparece en xs, si y = x;
* el número de veces que aparece en xs, si y ≠ x;
------------------------------------------------------------------ *}
lemma cuenta_inserta:
"cuenta (inserta x xs) y =
(if x=y then Suc (cuenta xs y) else cuenta xs y)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que el número de veces que aparece y en
(ordena xs) es el número de veces que aparece en xs.
------------------------------------------------------------------ *}
theorem cuenta_ordena:
"cuenta (ordena xs) y = cuenta xs y"
oops
end
