Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

2018-07-15T11:55:20Z

Texto reemplazado: «"isar"» por «"isabelle"»

Jalonso: Página creada con ' header {* R11: Sustitución, inversión y eliminación } theory R11 imports Main begin section { Sustitución, inversión y eliminación } text { ...'

2013-05-02T09:15:40Z

Página creada con '<source lang="isar"> header {* R11: Sustitución, inversión y eliminación *} theory R11 imports Main begin section {* Sustitución, inversión y eliminación *} text {* ...'

Página nueva

<source lang="isar">
header {* R11: Sustitución, inversión y eliminación *}

theory R11
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]
---------------------------------------------------------------------
*}

fun sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
"sust x y zs = undefined"

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

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

lemma 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)
---------------------------------------------------------------------
*}

lemma
"sust x y (sust u v zs) = sust u v (sust x y zs)"
oops

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

lemma
"sust y z (sust x y zs) = sust x z zs"
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.
---------------------------------------------------------------------
*}

fun borra :: "'a ⇒ 'a list ⇒ 'a list" where
"borra x ys = undefined"

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

fun borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
"borraTodas x ys = undefined"

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

lemma
"borra x (borraTodas x xs) = borraTodas x xs"
oops

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

lemma
"borraTodas x (borraTodas x xs) = borraTodas x xs"
oops

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

lemma
"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)
---------------------------------------------------------------------
*}

lemma
"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)
---------------------------------------------------------------------
*}

lemma
"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
---------------------------------------------------------------------
*}

lemma
"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"
---------------------------------------------------------------------
*}

lemma
"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
---------------------------------------------------------------------
*}

lemma
"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)
---------------------------------------------------------------------
*}

lemma
"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)
---------------------------------------------------------------------
*}

lemma
"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)
---------------------------------------------------------------------
*}

lemma
"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)
---------------------------------------------------------------------
*}

lemma
"rev (borraTodas x xs) = borraTodas x (rev xs)"
oops

end
</source>

← Revisión anterior		Revisión del 11:55 15 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R11: Sustitución, inversión y eliminación *}		header {* R11: Sustitución, inversión y eliminación *}

RA12 Relación 11 - Historial de revisiones

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

Jalonso: Página creada con ' header {* R11: Sustitución, inversión y eliminación *} theory R11 imports Main begin section {* Sustitución, inversión y eliminación *} text {* ...'

Jalonso: Página creada con ' header {* R11: Sustitución, inversión y eliminación } theory R11 imports Main begin section { Sustitución, inversión y eliminación } text { ...'