Jalonso en 07:49 16 jul 2018

2018-07-16T07:49:51Z

Jalonso en 07:23 11 feb 2012

2012-02-11T07:23:14Z

Mostrar los cambios

Jalonso: Protegió «Rel 3» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2011-02-14T22:48:17Z

Protegió «Rel 3» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* 3ª relación de ejercicios } theory Relacion_3 imports Main begin section { Cons inverso } text { -------------------------------------...'

2011-02-14T22:48:01Z

Página creada con '<source lang="isar"> header {* 3ª relación de ejercicios *} theory Relacion_3 imports Main begin section {* Cons inverso *} text {* -------------------------------------...'

Página nueva

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

theory Relacion_3
imports Main
begin

section {* Cons inverso *}

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir recursivamente la función
snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
tal que (snoc xs a) es la lista obtenida al añadir el elemento a al
final de la lista xs. Por ejemplo,
value "snoc [2,5] (3::int)" == [2,5,3]

Nota: No usar @.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar el siguiente teorema
snoc xs a = xs @ [a]
---------------------------------------------------------------------
*}

-- "La demostración automática del lema es"
lemma "snoc xs a = xs @ [a]"
oops

-- "La demostración estructurada del lema es"
lemma snoc_append: "snoc xs a = xs @ [a]"
oops

text {*
---------------------------------------------------------------------
Ejercicio 3. Demostrar el siguiente teorema
rev (x # xs) = snoc (rev xs) x"
---------------------------------------------------------------------
*}

-- "La demostración automática del teorema es"
theorem rev_cons_auto: "rev (x # xs) = snoc (rev xs) x"
oops

-- "La demostración estructurada del teorema es"
theorem rev_cons: "rev (x # xs) = snoc (rev xs) x"
oops

section {* Cuantificadores sobre listas *}

text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
todos :: ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool
tal que (todos p xs) se verifica si todos los elementos de la lista
xs cumplen la propiedad p. Por ejemplo, se verifica
todos (\<lambda>x. 1<length x) [[2,1,4],[1,3]]
\<not> todos (\<lambda>x. 1<length x) [[2,1,4],[3]]

Nota: La función todos es equivalente a la predefinida list_all.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
algunos :: ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool
tal que (algunos p xs) se verifica si algunos elementos de la lista
xs cumplen la propiedad p. Por ejemplo, se verifica
algunos (\<lambda>x. 1<length x) [[2,1,4],[3]]
\<not> algunos (\<lambda>x. 1<length x) [[],[3]]"

Nota: La función algunos es equivalente a la predefinida list_ex.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar:
todos (\<lambda>x. P x \<and> Q x) xs = (todos P xs \<and> todos Q xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "todos (\<lambda>x. P x \<and> Q x) xs = (todos P xs \<and> todos Q xs)"
oops

-- "La demostración estructurada es"
lemma "todos (\<lambda>x. P x \<and> Q x) xs = (todos P xs \<and> todos Q xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar o refutar:
todos P (x @ y) = (todos P x \<and> todos P y)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "todos P (x @ y) = (todos P x \<and> todos P y)"
oops

-- "La demostración estructurada es"
lemma todos_append [simp]:
"todos P (x @ y) = (todos P x \<and> todos P y)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar:
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "todos P (rev xs) = todos P xs"
oops

-- "La demostración estructurada es"
lemma "todos P (rev xs) = todos P xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar o refutar:
algunos (\<lambda>x. P x \<and> Q x) xs = (algunos P xs \<and> algunos Q xs)
---------------------------------------------------------------------
*}

-- "Se busca un contraejemplo con nitpick"
lemma "algunos (\<lambda>x. P x \<and> Q x) xs = (algunos P xs \<and> algunos Q xs)"
oops

text {*
El contraejemplo encontrado es
*}

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar o refutar:
algunos P (map f xs) = algunos (P \<circ> f) xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "algunos P (map f xs) = algunos (P o f) xs"
oops

-- "La demostración estructurada es"
lemma "algunos P (map f xs) = algunos (P \<circ> f) xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar o refutar:
algunos P (xs @ ys) = (algunos P xs \<or> algunos P ys)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "algunos P (xs @ ys) = (algunos P xs \<or> algunos P ys)"
oops

-- "La demostración estructurada es"
lemma algunos_append:
"algunos P (xs @ ys) = (algunos P xs \<or> algunos P ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar:
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "algunos P (rev xs) = algunos P xs"
oops

-- "La demostración estructurada es"
lemma "algunos P (rev xs) = algunos P xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 13. Encontrar un término no trivial Z tal que sea cierta la
siguiente ecuación:
algunos (\<lambda>x. P x \<or> Q x) xs = Z
---------------------------------------------------------------------
*}

text {*
Solución: La ecuación se verifica eligiendo como Z el término
algunos P xs \<or> algunos Q xs
En efecto,
*}

lemma "algunos (\<lambda>x. P x \<or> Q x) xs = (algunos P xs \<or> algunos Q xs)"
oops

-- "De forma estructurada"
lemma "algunos (\<lambda>x. P x \<or> Q x) xs = (algunos P xs \<or> algunos Q xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar:
algunos P xs = (\<not> todos (\<lambda>x. (\<not> P x)) xs)
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "algunos P xs = (\<not> todos (\<lambda>x. (\<not> P x)) xs)"
oops

-- "La demostración estructurada es"
lemma "algunos P xs = (\<not> todos (\<lambda>x. (\<not> P x)) xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la funcion primitiva recursiva
estaEn :: 'a \<Rightarrow> 'a list \<Rightarrow> bool
tal que (estaEn x xs) se verifica si el elemento x está en la lista
xs. Por ejemplo,
estaEn (2::nat) [3,2,4] = True
estaEn (1::nat) [3,2,4] = False
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 16. Expresar la relación existente entre estaEn y algunos.
---------------------------------------------------------------------
*}

text {*
Solución: La relación es

En efecto,
*}

text {*
---------------------------------------------------------------------
Ejercicio 17. Definir la función primitiva recursiva
sinDuplicados :: 'a list \<Rightarrow> bool
tal que (sinDuplicados xs) se verifica si la lista xs no contiene
duplicados. Por ejemplo,
sinDuplicados [1::nat,4,2] = True
sinDuplicados [1::nat,4,2,4] = False
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 18. Definir la función primitiva recursiva
borraDuplicados :: 'a list \<Rightarrow> bool
tal que (borraDuplicados xs) es la lista obtenida eliminando los
elementos duplicados de la lista xs. Por ejemplo,
borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

Nota: La función borraDuplicados es equivalente a la predefinida remdups.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 19. Demostrar o refutar:
length (borraDuplicados xs) \<le> length xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma "length (borraDuplicados xs) \<le> length xs"
oops

-- "La demostración estructurada es"
lemma length_borraDuplicados:
"length (borraDuplicados xs) \<le> length xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 20. Demostrar o refutar:
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
*}

-- "La demostración automática es"
lemma estaEn_borraDuplicados_auto:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

-- "La demostración estructurada es"
lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 21. Demostrar o refutar:
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

-- "La demostración automática"
lemma "sinDuplicados (borraDuplicados xs)"
oops

-- "La demostración estructurada es"
lemma sinDuplicados_borraDuplicados:
"sinDuplicados (borraDuplicados xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 22. Demostrar o refutar:
borraDuplicados (rev xs) = rev (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
oops

end
</source>

← Revisión anterior		Revisión del 07:49 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* 3ª relación de ejercicios *}		header {* 3ª relación de ejercicios *}

← Revisión anterior	Revisión del 22:48 14 feb 2011
(Sin diferencias)

Rel 3 - Historial de revisiones

Jalonso en 07:49 16 jul 2018

Jalonso en 07:23 11 feb 2012

Jalonso: Protegió «Rel 3» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* 3ª relación de ejercicios *} theory Relacion_3 imports Main begin section {* Cons inverso *} text {* -------------------------------------...'

Jalonso: Página creada con ' header {* 3ª relación de ejercicios } theory Relacion_3 imports Main begin section { Cons inverso } text { -------------------------------------...'