Jalonso en 12:04 15 jul 2018

2018-07-15T12:04:10Z

Jalonso: Página creada con ' 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 o...'

2013-05-23T11:44:33Z

Página creada con '<source lang="isar"> 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 o...'

Página nueva

<source lang="isar">
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
</source>

← Revisión anterior		Revisión del 12:04 15 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R17: Ordenación de listas por inserción *}		header {* R17: Ordenación de listas por inserción *}

RA12 Relación 17 - Historial de revisiones

Jalonso en 12:04 15 jul 2018

Jalonso: Página creada con ' 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 o...'

Jalonso: Página creada con ' 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 o...'