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

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

theory Ordenacion_por_insercion
imports Main
begin

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

  El algoritmo de ordenación de listas por inserción construye una lista ordenada a
  partir de la lista original, realizando una operación básica de inserción de cada
  elemento de la lista original en la lista ordenada preservando el orden de ésta. Por
  ejemplo, dada la lista [2,5,1,7] el algoritmo actúa como se describe a continuación:
  - Lista a ordenar: [2,5,1,7]
    Lista ordenada: []
  - Lista a ordenar: [5,1,7]
    Lista ordenada: [2]
  - Lista a ordenar: [1,7]
    Lista ordenada: [2,5]
  - Lista a ordenar: [7]
    Lista ordenada: [1,2,5]
  - Lista a ordenar: []
    Lista ordenada: [1,2,5,7]

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

text {* ---------------------------------------------------------------------------------
  Consideramos la función
     inserta :: int ⇒ int list ⇒ int list
  tal que '(inserta y xs)' es la lista obtenida insertando el elemento 'y' delante del
  primer elemento de la lista 'xs' que es mayor o igual que 'y'. Por ejemplo,
     inserta 3 [2,5,1,7] = [2,3,5,1,7]
-------------------------------------------------------------------------------------- *}

fun inserta :: "int ⇒ int list ⇒ int list" where
  "inserta y []     = [y]"  
| "inserta y (x#xs) = (if y ≤ x 
                       then y # x # xs 
                       else x # inserta y xs)"

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

text {* ---------------------------------------------------------------------------------
  Consideramos la función
     ordena :: int list ⇒ int list
  tal que '(ordena xs)' es la lista obtenida ordenando la lista 'xs' por inserción. Por
  ejemplo, 
     ordena [3,2,5,3] = [2,3,3,5]
-------------------------------------------------------------------------------------- *}

fun ordena :: "int list ⇒ int list" where
  "ordena []     = []"
| "ordena (x#xs) = inserta x (ordena xs)"

value "ordena [3,2,5,3]" -- "[2,3,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 y xs)' se verifica si el elemento 'y' 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 y []     = True"
| "menor y (x#xs) = (y ≤ x ∧ menor y 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_inserta:
  "cuenta (inserta x xs) y = (if x = y then Suc (cuenta xs y) 
                                       else cuenta xs y)"
oops

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

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

lemma conjConmutativaAsociativa[simp]:
  "(P ∧ Q ∧ R) = (Q ∧ P ∧ R)"
oops

lemma menor_menor: 
  assumes "x ≤ y"  
  shows   "menor y zs ⟶ menor x zs"
oops

lemma menor_inserta:
  "menor x (inserta y zs) = (x ≤ y ∧ menor x zs)"
oops

lemma ordenada_inserta:
  "ordenada (inserta a xs) = ordenada xs"
oops

theorem ordenada_ordena:
  "ordenada (ordena xs)"
oops

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

end