Razonamiento automático (2010-11) - Contribuciones del usuario [es]

Relación 5

2011-02-15T15:52:20Z

Julianmina:

<source lang="isar">
header {* 5ª relación de ejercicios *}

theory Relacion_5
imports Main
begin

section {* Menor posición válida *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"
tal que (menorValida p xs) es el índice del primer elemento de una
lista xs que satisface el predicado p y es la longitud de xs si
ningún elemento satisface el predicado p. Por ejemplo,
menorValida (λx. 4<x) [1::nat, 3, 5, 3, 1] = 2
menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1] = 5
menorValida (λx. 1<length x) [[], [1, 2], [3]] = 1
---------------------------------------------------------------------
*}

primrec menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where
"menorValida P [] = 0"
| "menorValida P (x#xs) = (if P x then 0 else ((menorValida P xs)+1))"

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar que menorValida devuelve la longitud de la
lista syss ningún elemento satisface el predicado dado.
---------------------------------------------------------------------
*}

lemma "menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1] = 5"
by auto

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar si n es el valor de (menorValida P xs),
entonces ninguno de los primeros n elementos de la lista xs verifica
la propiedad P.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 4. ¿Cómo se puede relacionar
"menorValida (λ x. P x ∨ Q x) xs"
con
"menorValida P xs" y "menorValida Q xs"?
¿Se puede decir algo parecido con la conjunción de P y Q?
Prueba tus conjeturas.
---------------------------------------------------------------------
*}

text {*
La relación es la siguiente: La menor posición de los elementos que
verifican la propiedad "P ∨ Q" es el mínimo de la menor posición de
los elementos que verifican P y de la menor posición de los elementos
que verifican Q.
*}

text {*
---------------------------------------------------------------------
Ejercicio 5. Si P implica Q, ¿qué relación puede deducirse entre
"menorValida P xs" y "menorValida Q xs"?
---------------------------------------------------------------------
*}

end
</source>

Relación 5

2011-02-15T15:40:02Z

Julianmina:

<source lang="isar">
header {* 5ª relación de ejercicios *}

theory Relacion_5
imports Main
begin

section {* Menor posición válida *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"
tal que (menorValida p xs) es el índice del primer elemento de una
lista xs que satisface el predicado p y es la longitud de xs si
ningún elemento satisface el predicado p. Por ejemplo,
menorValida (λx. 4<x) [1::nat, 3, 5, 3, 1] = 2
menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1] = 5
menorValida (λx. 1<length x) [[], [1, 2], [3]] = 1
---------------------------------------------------------------------
*}

primrec menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where
"menorValida P [] = 0"
| "menorValida P (x#xs) = (if P x then 0 else ((menorValida P xs)+1))"

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar que menorValida devuelve la longitud de la
lista syss ningún elemento satisface el predicado dado.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar si n es el valor de (menorValida P xs),
entonces ninguno de los primeros n elementos de la lista xs verifica
la propiedad P.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 4. ¿Cómo se puede relacionar
"menorValida (λ x. P x ∨ Q x) xs"
con
"menorValida P xs" y "menorValida Q xs"?
¿Se puede decir algo parecido con la conjunción de P y Q?
Prueba tus conjeturas.
---------------------------------------------------------------------
*}

text {*
La relación es la siguiente: La menor posición de los elementos que
verifican la propiedad "P ∨ Q" es el mínimo de la menor posición de
los elementos que verifican P y de la menor posición de los elementos
que verifican Q.
*}

text {*
---------------------------------------------------------------------
Ejercicio 5. Si P implica Q, ¿qué relación puede deducirse entre
"menorValida P xs" y "menorValida Q xs"?
---------------------------------------------------------------------
*}

end
</source>

Usuario:Jgalanp

2011-02-15T15:27:02Z

Julianmina: Página creada con 'Juan Galán'

Juan Galán

Usuario:Jmuros

2011-02-15T15:25:00Z

Julianmina: Página creada con 'Jesús Muros'

Jesús Muros

Usuario:Julianmina

2011-02-15T15:21:44Z

Julianmina: Página creada con 'Julián Mina'

Julián Mina

Relación 4

2011-02-14T20:06:48Z

Julianmina:

<source lang="isar">
header {* 4ª relación de ejercicios *}

theory Relacion_4
imports Main
begin

section {* Sustitución, inversión y eliminación *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list"
tal que (sust x y zs) es la lista obtenida sustituyendo cada
occurrencia de x por y en la lista zs. Por ejemplo,
sust (1::nat) 2 [1,2,3,4,1,2,3,4] = [2,2,3,4,2,2,3,4]
---------------------------------------------------------------------
*}

primrec sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
"sust x y [] = []"
| "sust x y (w#zs) = (if w=x then y#(sust x y zs) else w#(sust x y zs))"

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar o refutar:
sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
---------------------------------------------------------------------
*}

text {*
--Usando la sentencia refute puede obtenerse un contraejemplo fácilmente.
--Además, al ejecutarse con la aplicación, ya directamente propone un contraejemplo.
*}

-- "La demostración automática es"
lemma sust_append_auto:
"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
refute
oops

-- "La demostración estructurada es"
lemma sust_append:
"sust x y (xs @ ys) = (sust x y xs)@(sust x y ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar o refutar:
rev (sust x y zs) = sust x y (rev zs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "rev(sust x y zs) = sust x y (rev zs)"
refute
oops

-- "La demostración estructurada es"
theorem rev_sust:
"rev (sust x y zs) = sust x y (rev zs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar o refutar:
sust x y (sust u v zs) = sust u v (sust x y zs)
---------------------------------------------------------------------
*}

theorem "sust x y (sust u v zs) = sust u v (sust x y zs)"
refute
oops

text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar:
sust y z (sust x y zs) = sust x z zs
---------------------------------------------------------------------
*}

theorem "sust y z (sust x y zs) = sust x z zs"
refute
oops

text {*
---------------------------------------------------------------------
Ejercicio 6. Definir la función
borra :: "'a ⇒ 'a list ⇒ 'a list"
tal que (borra x ys) es la lista obtenida borrando la primera
ocurrencia del elemento x en la lista ys. Por ejemplo,
borra (2::nat) [1,2,3,2] = [1,3,2]

Nota: La función borra es equivalente a la predefinida remove1.
---------------------------------------------------------------------
*}

primrec borra :: "'a ⇒ 'a list ⇒ 'a list" where
"borra x [] = []"
| "borra x (w#ys) = (if x=w then ys else (w#(borra x ys)))"

text {*
---------------------------------------------------------------------
Ejercicio 7. Definir la función
borraTodas :: "'a ⇒ 'a list ⇒ 'a list"
tal que (borraTodas x ys) es la lista obtenida borrando todas las
ocurrencias del elemento x en la lista ys. Por ejemplo,
borraTodas (2::nat) [1,2,3,2] = [1,3]
---------------------------------------------------------------------
*}

primrec borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
"borraTodas x [] = []"
| "borraTodas x (w#ys) = (if x=w then (borraTodas x ys) else (w#(borraTodas x ys)))"

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar:
borra x (borraTodas x xs) = borraTodas x xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borra x (borraTodas x xs) = borraTodas x xs"
refute
oops

-- "La demostración estructurada es"
theorem "borra x (borraTodas x xs) = borraTodas x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar o refutar:
borraTodas x (borraTodas x xs) = borraTodas x xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borraTodas x (borraTodas x xs) = borraTodas x xs"
refute
oops

-- "La demostración estructurada es"
theorem "borraTodas x (borraTodas x xs) = borraTodas x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar o refutar:
borraTodas x (borra x xs) = borraTodas x xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borraTodas x (borra x xs) = borraTodas x xs"
oops

-- "La demostración estructurada es"
theorem borraTodas_borra:
"borraTodas x (borra x xs) = borraTodas x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar o refutar:
borra x (borra y xs) = borra y (borra x xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borra x (borra y xs) = borra y (borra x xs)"
oops

-- "La demostración estructurada es"
theorem "borra x (borra y xs) = borra y (borra x xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar el teorema:
borraTodas x (borra y xs) = borra y (borraTodas x xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
oops

-- "La demostración estructurada es"
theorem "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar:
borra y (sust x y xs) = borra x xs
---------------------------------------------------------------------
*}

theorem "borra y (sust x y xs) = borra x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar:
borraTodas y (sust x y xs) = borraTodas x xs"
---------------------------------------------------------------------
*}

theorem "borraTodas y (sust x y xs) = borraTodas x xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar:
sust x y (borraTodas x zs) = borraTodas x zs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "sust x y (borraTodas x zs) = borraTodas x zs"
oops

-- "La demostración estructurada es"
theorem sust_borraTodas:
"sust x y (borraTodas x zs) = borraTodas x zs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar:
sust x y (borraTodas z zs) = borraTodas z (sust x y zs)
---------------------------------------------------------------------
*}

theorem "sust x y (borraTodas z zs) = borraTodas z (sust x y zs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar:
rev (borra x xs) = borra x (rev xs)
---------------------------------------------------------------------
*}

theorem "rev (borra x xs) = borra x (rev xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18. Demostrar o refutar el teorema:
borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
oops

-- "La demostración estructurada es"
lemma borraTodas_append:
"borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 19. Demostrar o refutar el teorema:
rev (borraTodas x xs) = borraTodas x (rev xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
theorem "rev (borraTodas x xs) = borraTodas x (rev xs)"
oops

-- "La demostración estructurada es"
theorem "rev (borraTodas x xs) = borraTodas x (rev xs)"
oops

end
</source>