Acciones

Tema 6a: Verificación de la ordenación por inserción

De Razonamiento automático (2018-19)

Revisión del 15:28 13 dic 2018 de Jalonso (discusión | contribuciones) (Página creada con «<source lang="isabelle"> chapter {* T6a: Verificación de la ordenación por inserción *} theory T6a_Verificacion_de_la_ordenacion_por_insercion imports Main begin text…»)
(dif) ← Revisión anterior | Revisión actual (dif) | Revisión siguiente → (dif)

<source lang="isabelle"> chapter {* T6a: Verificación de la ordenación por inserción *}

theory T6a_Verificacion_de_la_ordenacion_por_insercion imports Main begin

text {* 

 En este de tema 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 :: int ⇒ int list ⇒ int 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 :: "int ⇒ int list ⇒ int list" where 

 "inserta a []     = [a]"

| "inserta a (x#xs) = (if a ≤ x 

                      then a # x # xs 
                      else x # inserta a xs)"

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

text {* 

 --------------------------------------------------------------------- 
 Ejercicio 2. Definir la función
    ordena :: int list ⇒ int 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 :: "int list ⇒ int list" where 

 "ordena []     = []"

| "ordena (x#xs) = inserta x (ordena xs)"

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

text {* 

 --------------------------------------------------------------------- 
 Ejercicio 3. 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 []     = 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 {* 

 --------------------------------------------------------------------- 
 Ejercicio 4. 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 []     = True"

| "ordenada (x#xs) = (menor x xs & ordenada xs)"

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 zs y x ≤ y,
 entonces x es una cota inferior de zs.
 ------------------------------------------------------------------ *}

― ‹La demostración automática es› lemma menor_menor: 

 assumes "x ≤ y"  
 shows   "menor y zs ⟶ menor x zs"

using assms by (induct zs) auto

― ‹La demostración estructurada es› lemma menor_menor_2: 

 assumes "x ≤ y"  
 shows   "menor y zs ⟶ menor x zs"

proof (induct zs) 

 show "menor y [] ⟶ menor x []" by simp

next 

 fix z zs
 assume HI: "menor y zs ⟶ menor x zs"  
 show "menor y (z # zs) ⟶ menor x (z # zs)"
 proof
   assume sup: "menor y (z # zs)"
   show "menor x (z # zs)"
   proof (simp only: menor.simps(2))
     show "x ≤ z ∧ menor x zs"
     proof
         have "x ≤ y" using assms .
         also have "y ≤ z" using sup by simp
         finally show "x ≤ z" .
     next
       have "menor y zs" using sup by simp
       with HI show "menor x zs" by simp
     qed
   qed
 qed

qed

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.
 ------------------------------------------------------------------ *}

― ‹La demostración automática es› lemma menor_inserta: 

 "menor x (inserta y zs) = (x ≤ y ∧ menor x zs)"

by (induct zs) auto

― ‹La demostración estructurada es› lemma menor_inserta_2: 

 "menor x (inserta y zs) = (x ≤ y ∧ menor x zs)"

proof (induct zs) 

 show "menor x (inserta y []) = (x ≤ y ∧ menor x [])" by simp

next 

 fix z zs
 assume HI: "menor x (inserta y zs) = (x ≤ y ∧ menor x zs)"
 show "menor x (inserta y (z#zs)) = (x ≤ y ∧ menor x (z#zs))" 
 proof (cases "y ≤ z")
   assume "y ≤ z"
   hence "menor x (inserta y (z#zs)) = menor x (y#z#zs)" by simp
   also have "… = (x ≤ y ∧ menor x (z#zs))" by simp
   finally show ?thesis by simp
 next
   assume "¬(y ≤ z)"
   hence "menor x (inserta y (z#zs)) = 
          menor x (z # inserta y zs)" by simp
   also have "… = (x ≤ z ∧ menor x (inserta y zs))" by simp
   also have "… = (x ≤ z ∧ x ≤ y ∧ menor x zs)" using HI by simp
   also have "… = (x ≤ y ∧ menor x (z#zs))" by auto
   finally show ?thesis by simp
 qed

qed

text {* 

 --------------------------------------------------------------------- 
 Ejercicio 6. Demostrar que al insertar un elemento la lista obtenida
 está ordenada syss lo estaba la original.
 ------------------------------------------------------------------ *}

― ‹La demostración automática es› lemma ordenada_inserta: 

 "ordenada (inserta a xs) = ordenada xs"

by (induct xs) (auto simp add: menor_menor menor_inserta)

― ‹La demostración estructurada es› lemma ordenada_inserta_2: 

 "ordenada (inserta a xs) = ordenada xs"

proof (induct xs) 

 show "ordenada (inserta a []) = ordenada []" by simp

next 

 fix x xs
 assume HI: "ordenada (inserta a xs) = ordenada xs" 
 show "ordenada (inserta a (x # xs)) = ordenada (x # xs)" 
 proof (cases "a ≤ x")
   assume "a ≤ x"
   hence "ordenada (inserta a (x # xs)) = 
          ordenada (a # x # xs)" by simp
   also have "… = (menor a (x#xs) ∧ ordenada (x # xs))" by simp
   also have "… = ordenada (x # xs)"  
     using `a ≤ x`  by (auto simp add: menor_menor)
   finally show "ordenada (inserta a (x # xs)) = ordenada (x # xs)" 
     by simp
 next
   assume "¬(a ≤ x)"
   hence "ordenada (inserta a (x # xs)) = 
          ordenada (x # inserta a xs)" by simp
   also have "… = (menor x (inserta a xs) ∧ ordenada (inserta a xs))" 
     by simp
   also have "… = (menor x (inserta a xs) ∧ ordenada xs)" 
     using HI by simp
   also have "… = (menor x xs ∧ ordenada xs)" 
     using `¬(a ≤ x)` by (simp add: menor_inserta)
   also have "… = ordenada (x # xs)" by simp
   finally show "ordenada (inserta a (x # xs)) = ordenada (x # xs)" 
     by simp
 qed

qed

text {* 

 --------------------------------------------------------------------- 
 Ejercicio 7. Demostrar que, para toda lista xs, (ordena xs) está
 ordenada. 
 ------------------------------------------------------------------ *}

― ‹La demostración automática es› theorem ordenada_ordena: 

 "ordenada (ordena xs)"

by (induct xs) (auto simp add: ordenada_inserta)

― ‹La demostración estructurada es› theorem ordenada_ordena_2: 

 "ordenada (ordena xs)"

proof (induct xs) 

 show "ordenada (ordena [])" by simp

next 

 fix x xs
 assume "ordenada (ordena xs)" 
 then have "ordenada (inserta x (ordena xs))" 
   by (simp add: ordenada_inserta)  
 then show "ordenada (ordena (x # xs))" by simp

qed

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 garantizarlo, definimos la función cuenta.
 ------------------------------------------------------------------ *}

text {* 

 --------------------------------------------------------------------- 
 Ejercicio 8. 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 []     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 {* 

 --------------------------------------------------------------------- 
 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; 
 ------------------------------------------------------------------ *}

― ‹La demostración automática es› lemma cuenta_inserta: 

 "cuenta (inserta x xs) y =
  (if x=y then Suc (cuenta xs y) else cuenta xs y)"

by (induct xs) auto

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.
 ------------------------------------------------------------------ *}

― ‹La demostración automática es› theorem cuenta_ordena: 

 "cuenta (ordena xs) y = cuenta xs y"

by (induct xs) (auto simp add: cuenta_inserta)

― ‹La demostración estructurada es› theorem cuenta_ordena_2: 

 "cuenta (ordena xs) y = cuenta xs y"

proof (induct xs) 

 show "cuenta (ordena []) y = cuenta [] y" by simp

next 

 fix x xs
 assume HI: "cuenta (ordena xs) y = cuenta xs y"
 show "cuenta (ordena (x # xs)) y = cuenta (x # xs) y" 
 proof (cases "x = y")
   assume "x = y"
   have "cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y" 
     by simp
   also have "… = Suc (cuenta (ordena xs) y)" using `x = y` 
     by (simp add: cuenta_inserta) 
   also have "… = Suc (cuenta xs y)" using HI by simp
   also have "… = cuenta (x # xs) y" using `x = y` by simp
   finally show "cuenta (ordena (x # xs)) y = cuenta (x # xs) y" by simp
 next
   assume "x ≠ y"
   have "cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y" 
     by simp
   also have "… = cuenta (ordena xs) y" using `x ≠ y` 
     by (simp add: cuenta_inserta) 
   also have "… = cuenta xs y" using HI by simp
   also have "… = cuenta (x # xs) y" using `x ≠ y` by simp
   finally show "cuenta (ordena (x # xs)) y = cuenta (x # xs) y" 
     by simp
 qed

qed

end </end>

Obtenido de «https://www.glc.us.es/~jalonso/RA2018/index.php?title=Tema_6a:_Verificación_de_la_ordenación_por_inserción&oldid=188»