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_borra_auto: "borraTodas x (borra x xs) = borraTodas x xs"
by (induct xs) auto
-- "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)"
by (induct xs) auto
-- "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)"
by (induct xs arbitrary: ) (auto simp add: borraTodas_borra_auto)
-- "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
---------------------------------------------------------------------
*}
text {*
La igualdad propuesta es falsa.
El contraejemplo que encuentra Quickcheck es (retocándolo para que no dé
problemas al exportarlo a Isabelle):
y = a1
x = a2
xs = [a1]
El contraejemplo que encuentra Refute es idéntico salvo cambio de nombres:
x = a1
xs = [a2]
y = a2
Análogamente, el contraejemplo que encuentra Refute es idéntico salvo cambio de nombres:
y: a0
x: a1
xs: [a0]
*}
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"
---------------------------------------------------------------------
*}
text {*
La igualdad propuesta es falsa.
El contraejemplo que encuentra Quickcheck es (retocándolo para que no dé
problemas al exportarlo a Isabelle):
y = a1
x = a2
xs = [a1]
El contraejemplo que encuentra Refute es idéntico salvo cambio de nombres:
x = a1
xs = [a2]
y = a2
Análogamente, el contraejemplo que encuentra Refute es idéntico salvo cambio de nombres:
y: a0
x: a1
xs: [a0]
*}
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"
by (induct zs) auto
-- "La demostración estructurada es"
theorem sust_borraTodas:
"sust x y (borraTodas x zs) = borraTodas x zs"
proof (induct zs)
show "sust x y (borraTodas x []) = borraTodas x []" by auto
next
show "⋀a zs. sust x y (borraTodas x zs) = borraTodas x zs ⟹
sust x y (borraTodas x (a # zs)) = borraTodas x (a # zs)" by auto
qed
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)"
quickcheck
oops
text {*
Para este ejercicio quickcheck encuentra el siguiente contraejemplo:
zs = [0]
z = 1
y = 1
x = 0
*}
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_append_auto:
"borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
by (induct xs) auto
-- "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)"
by (induct xs arbitrary: x) (auto simp add: borraTodas_append_auto)
-- "La demostración estructurada es"
theorem "rev (borraTodas x xs) = borraTodas x (rev xs)"
oops
end
