R10

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