Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

header {* Verificación de la ordenación por mezcla *}

theory Ordenacion_por_mezclas
imports Main
begin

text {* ---------------------------------------------------------------------------------
  En este trabajo se describe el algoritmo de ordenación de listas por mezclas y se
  propone comprobar que es correcto.

  El algoritmo de ordenación de listas por mezclas construye una lista ordenada a partir 
  de la lista original, para ello divide la lista original en dos trozos, los ordena
  siguiendo el mismo método y finalmente mezcla los resultados. Por ejemplo, dada la
  lista [2,7,5,1] el algoritmo actúa como se describe a continuación:
  - Lista a ordenar: [2,7,5,1]
    Trozos de la lista: [2,7] y [5,1]
  -- Lista a ordenar: [2,7]
     Trozos de la lista: [2] y [7]
  --- Lista a ordenar: [2]
      La lista está ordenada
  --- Lista a ordenar: [7]
      La lista está ordenada
  -- La mezcla ordenada de [2] y [7] es [2,7]
  -- Lista a ordenar [5,1]
     Trozos de la lista: [5] y [1]
  --- Lista a ordenar: [5]
      La lista está ordenada
  --- Lista a ordenar: [1]
      La lista está ordenada
  -- La mezcla ordenada de [5] y [1] es [1,5]
  - La mezcla ordenada de [2,7] y [1,5] es [1,2,5,7]

  Para implementar este algoritmo de ordenación se definen las siguientes funciones:
-------------------------------------------------------------------------------------- *}

text {* --------------------------------------------------------------------------------
  Consideramos 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 [] ys = ys" 
| "mezcla xs [] = xs" 
| "mezcla (x # xs) (y # ys) = (if x ≤ y
                               then x # mezcla xs (y # ys)
                               else y # mezcla (x # xs) ys)"

value "mezcla [1,2,5] [3,5,7]" -- "= [1,2,3,5,5,7]"

text {* ---------------------------------------------------------------------------------
  consideramos la función
     ordena :: int list ⇒ int list
  tal que '(ordena 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, 
     ordena [3,2,5,2] = [2,2,3,5]
-------------------------------------------------------------------------------------- *}

fun ordena :: "int list ⇒ int list" where
  "ordena [] = []" 
| "ordena [x] = [x]" 
| "ordena xs = mezcla (ordena (take (length xs div 2) xs)) 
                      (ordena (drop (length xs div 2) xs))"

value "ordena [3,2,5,2]" -- "= [2,2,3,5]"

section {* Corrección del algoritmo de ordenación *}

text {* ---------------------------------------------------------------------------------
  La corrección del algoritmo de ordenación consiste en comprobar dos propiedades:
  - El resultado del algoritmo de ordenación tiene los mismos elementos que la lista
    original.
  - El resultado del algoritmo de ordenación es una lista ordenada.

  A continuación definimos las funciones necesarias para comprobar la corrección del 
  algoritmo de ordenación.
-------------------------------------------------------------------------------------- *}

text {* ---------------------------------------------------------------------------------
  Consideramos la función
     menor :: int ⇒ int list ⇒ bool
  tal que '(menor a xs)' se verifica si el elemento '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 []     = True"
| "menor a (x#xs) = (a ≤ x ∧ menor a xs)"

value "menor 2 [3,2,5]" -- "= True"
value "menor 2 [3,0,5]" -- "= False"

text {* ---------------------------------------------------------------------------------
  Consideramos 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 []     = True"
| "ordenada (x#xs) = (menor x xs & ordenada xs)"

value "ordenada [2,3,3,5]" -- "= True" 
value "ordenada [2,4,3,5]" -- "= False" 

text {* ---------------------------------------------------------------------------------
  Consideramos 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 []     y = 0"
| "cuenta (x#xs) y = (if x = y then Suc(cuenta xs y) else cuenta xs y)"

value "cuenta [1,3,4,3,5] 3" -- "= 2"

text {* ---------------------------------------------------------------------------------
  Propiedad 1: El resultado del algoritmo de ordenación tiene los mismos elementos que la
  lista original.
-------------------------------------------------------------------------------------- *}

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

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

theorem cuenta_ordena: 
  "cuenta (ordena xs) x = cuenta xs x"
oops

text {* ---------------------------------------------------------------------------------
  Propiedad 2: El resultado del algoritmo de ordenación es una lista ordenada.
-------------------------------------------------------------------------------------- *}

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

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

text {* ---------------------------------------------------------------------------------
  Indicación: En este lema puede ser necesario utilizar las siguientes propiedades:
  · 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

theorem ordenada_ordena:
  "ordenada (ordena xs)"
oops

text {* ------------------------------------------------------------------------------ *}
 
end