Razonamiento automático (2014-15) - Contribuciones del usuario [es]

Relación 8

2014-12-08T12:49:18Z

Javrodviv1:

<source lang="isar">
header {* R8: Árboles binarios completos *}

theory R8_Arboles_binarios_completos
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que no tienen información ni en los nodos y ni en las
hojas. Por ejemplo, el árbol
·
/ \
/ \
· ·
/ \ / \
· · · ·
se representa por "N (N H H) (N H H)".
---------------------------------------------------------------------
*}

datatype arbol = H | N arbol arbol

value "N (N H H) (N H H)"

text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
hojas :: "arbol => nat"
tal que (hojas a) es el número de hojas del árbol a. Por ejemplo,
hojas (N (N H H) (N H H)) = 4
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun hojas :: "arbol => nat" where
"hojas H = 1"
| "hojas (N i d) = hojas i + hojas d"

value "hojas (N (N H H) (N H H))" -- "= 4"

text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
profundidad :: "arbol => nat"
tal que (profundidad a) es la profundidad del árbol a. Por ejemplo,
profundidad (N (N H H) (N H H)) = 2
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun max :: "nat ⇒ nat ⇒ nat" where
"max a b= (if a≥ b then a else b)"

value "max 6 3" -- "= 6"

fun profundidad :: "arbol => nat" where
"profundidad H = 0"
| "profundidad (N a b) = 1 + max (profundidad a) (profundidad b)"

value "profundidad (N (N H H) (N H H))" -- "= 2"

(* Javrodviv1: Explico estas dos funciones, la que utilizo para los
lemas de abajo es profundidad ya que profundidad1 me encuentra
contraejemplos y para evitar eso busque definir profundidad
definidad de manera distinta. No obstante la que a mi me parece
mas sensata para definir la profundidad de un árbol es la
profundidad1 *)

(* Javrodviv1: Fallo mio ya lo corregí*)

(*Pedrosrei: La profundidad correcta es la mayor. Si te encuentra
contraejemplos más adelante es que te has equivocado en los
enunciados. Las funciones máximo y mínimo vienen predefinidas
ya sin necesidad de definirlas. *)

text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
abc :: "nat ⇒ arbol"
tal que (abc n) es el árbol binario completo de profundidad n. Por
ejemplo,
abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun abc :: "nat ⇒ arbol" where
"abc 0 = H"
| "abc (Suc n) = N (abc n) (abc n)"

value "abc 3" -- "= N (N (N H H) (N H H)) (N (N H H) (N H H))"

text {*
---------------------------------------------------------------------
Ejercicio 6. Un árbol binario a es completo respecto de la medida f si
a es una hoja o bien a es de la forma (N i d) y se cumple que tanto i
como d son árboles binarios completos respecto de f y, además,
f(i) = f(r).

Definir la función
es_abc :: "(arbol => 'a) => arbol => bool
tal que (es_abc f a) se verifica si a es un árbol binario completo
respecto de f.
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
| "es_abc f (N a b) = ((f a = f b) ∧ (es_abc f a ∧ es_abc f b))"

text {*
---------------------------------------------------------------------
Nota. (size a) es el número de nodos del árbol a. Por ejemplo,
size (N (N H H) (N H H)) = 3
---------------------------------------------------------------------
*}

text{*Para entenderme he cambiado de función de tamaño, la demostración
es análoga pero buscando las simplificaciones de size cuando correspondan
*}

fun nodos::"arbol ⇒ nat" where
"nodos H = 0"
|"nodos (N i d) = 1+(nodos i)+(nodos d)"

lemma "size t= nodos t"
apply (induct t, auto)done

value "size (N (N H H) (N H H))"
value "size (N (N (N H H) (N H H)) (N (N H H) (N H H)))"

text {*
---------------------------------------------------------------------
Nota. Tenemos 3 funciones de medida sobre los árboles: número de
hojas, número de nodos y profundidad. A cada una le corresponde un
concepto de completitud. En los siguientes ejercicios demostraremos
que los tres conceptos de completitud son iguales.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de hojas.
---------------------------------------------------------------------
*}

text{*Pedrosrei: Los enunciados y demostraciones que vienen a continuación
son feos y engorrosos. Yo he optado por demostrarlo todo a través de
una propiedad extraña a la demostración en principio. Animo encarecidamente
a que pongáis una demostración más corta y directa. Voy explicando paso
a paso qué he hecho en cada momento. Hecha esta demostración, el resto
son triviales por una cadena de resultados.
No existe relación de implicación en ningún sentido
entre hojas y profundidad, como es obvio y muestran los siguientes
contraejemplos: *}
lemma "(((hojas(t1) = hojas(t2)))-->(profundidad(t1) = profundidad(t2)))"
quickcheck
oops
lemma "((profundidad(t1) = profundidad(t2)) -->
((hojas(t1) = hojas(t2))))"
quickcheck
oops
lemma "((profundidad(t1) = profundidad(t2)) <->
((hojas(t1) = hojas(t2))))"
quickcheck
oops
text {* Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:

t1 = N (N H H) (N H H)
t2 = N H (N H H)

Evaluated terms:
hojas t1 = 4
hojas t2 = 3

Ahora pongo una serie de resultados auxiliares que ayudarán en la prueba
*}

lemma auxprof:"(es_abc profundidad t)∧(profundidad t = n)==> (t= abc n)"
apply (induct t arbitrary:n, auto)done

lemma eq_1_iff_exp_0:"Suc 0 = 2 ^ n <-> n=0" apply (cases n, auto) done

lemma auxhojas:"(t= abc n)==> (es_abc hojas t)"
apply (induct n arbitrary: t, auto simp add: eq_1_iff_exp_0) done

lemma auxhoja:"(t= abc n)==>((hojas t = 2^n))"
apply (induct n arbitrary: t rule: abc.induct, auto)done

text{* Pedrosrei. Y aquí viene la demostración larga y fea que os animo a mejorar.
He dejado los pasos exactamente que indica el razonador para que
veáis qué hace en cada caso:
*}

lemma prof_eq_hoja:"es_abc profundidad t <-> es_abc hojas t"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc hojas t" using auxhojas by auto
next
show "es_abc hojas t ==> es_abc profundidad t" apply (induct t, auto)
proof -
fix t1 t2
assume a1:"es_abc profundidad t1"
thus "es_abc profundidad t2 ==>
es_abc hojas t1 ==>
es_abc hojas t2 ==>
hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2" proof -
assume a2:"es_abc profundidad t2"
thus "es_abc hojas t1 ==>
es_abc hojas t2 ==>
hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2"proof-
assume a3:"es_abc hojas t1"
thus "es_abc hojas t2 ==>
hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2"proof-
assume a4:"es_abc hojas t2"
thus "hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2" proof -
assume a5:"hojas t1 = hojas t2"
thus "profundidad t1 = profundidad t2"
proof-
obtain n where 1:"profundidad t1 = n" by auto
with a1 have 2:"t1 = abc n"using auxprof by auto
hence 3:"es_abc hojas t1" using auxhojas by auto
have "hojas t1 = (2::nat)^n" using 2 auxhoja by auto
hence 3:"hojas t2 = (2::nat)^n" using a5 by auto
obtain m where 4:"profundidad t2 = m" by auto
with a2 have 5:"t2 = abc m"using auxprof by auto
hence 6:"es_abc hojas t2" using auxhojas by auto
have "hojas t2 = (2::nat)^m" using 5 auxhoja by auto
with 3 have " (2::nat)^m = (2::nat) ^n" by auto
hence "m = n" apply (induct, auto)done
hence "t2 = abc n" using 5 by auto
with 2 have "t1= t2" by auto
thus "profundidad t1 = profundidad t2" by auto
qed
qed
qed
qed
qed
qed
qed

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que un árbol binario a es completo respecto del
número de hojas syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}
(* Javrodviv1: Bueno yo para este ejercicio he encontrado algo mas sencillo,
tan solo hay que encontrar una relación de igualdad entre hojas y size,
que para este caso es sencillo.*)
-- "Javrodviv1"

lemma hojasize_igualdad:
"hojas x = size x + 1"
by (induct x, simp_all)

(*lemma "es_abc size a <-> es_abc hojas a" Son equivalentes = es lo mismo que <->
matemáticamente hablando*)

lemma " es_abc size a = es_abc hojas a"
quickcheck
by (induct a, simp_all add: hojasize_igualdad)

text{* Pedrosrei. Aquí dejo esta. Es trivial debido a la demostración anterior,
sólo hace falta coger el mismo desvío. Aquí sí que podéis encontrar
una mucho más directa: *}

lemma auxnodo:"(t= abc n)==>(es_abc nodos t)∧(nodos t = (2^n - 1))"
apply (induct n arbitrary: t rule: abc.induct, auto)done

lemma nodos_eq_hoja:"es_abc nodos t <-> es_abc hojas t" (is "?P t")
proof -
have 1:"es_abc hojas t <-> es_abc profundidad t" using prof_eq_hoja by auto
hence 2:"?P t = (es_abc profundidad t <-> es_abc nodos t)" by auto
have "(es_abc profundidad t <-> es_abc nodos t)"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc nodos t" using auxnodo by auto
next
show "es_abc nodos t ==> es_abc profundidad t" apply (induct t, auto)
proof -
fix t1 t2
assume a1:"es_abc profundidad t1"
thus "es_abc profundidad t2 ==>
es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a2:"es_abc profundidad t2"
thus "es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a3:"es_abc nodos t1"
thus "es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a4:"es_abc nodos t2"
thus "nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a5:"nodos t1 = nodos t2"
thus "profundidad t1 = profundidad t2"
proof-
obtain n where 1:"profundidad t1 = n" by auto
with a1 have 2:"t1 = abc n"using auxprof by auto
hence 3:"es_abc nodos t1" using auxnodo by auto
have "nodos t1 = (2::nat)^n - 1" using 2 auxnodo by auto
hence 3:"nodos t2 = (2::nat)^n - 1" using a5 by auto
obtain m where 4:"profundidad t2 = m" by auto
with a2 have 5:"t2 = abc m"using auxprof by auto
hence 6:"es_abc nodos t2" using auxnodo by auto
have "nodos t2 = (2::nat)^m - 1" using 5 auxnodo by auto
with 3 have 7:" (2::nat)^m - 1 = (2::nat) ^n - 1" by auto
hence "m = n" proof -
have " (2::nat)^m - 1 = (2::nat) ^n - 1"using 7 by auto
hence "(2::nat)^m - 1 + 1 = (2::nat) ^n" by auto
hence "(2::nat)^m = (2::nat) ^n" by auto
thus ?thesis apply (induct, auto)done
qed
hence "t2 = abc n" using 5 by auto
with 2 have "t1= t2" by auto
thus "profundidad t1 = profundidad t2" by auto
qed
qed
qed
qed
qed
qed
qed
with 1 2 show ?thesis by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}

text {* Pedrosrei. De hecho, esta es una parte de la anterior: *}

lemma prof_eq_nodos: "(es_abc profundidad t <-> es_abc nodos t)"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc nodos t" using auxnodo by auto
next
show "es_abc nodos t ==> es_abc profundidad t" apply (induct t, auto)
proof -
fix t1 t2
assume a1:"es_abc profundidad t1"
thus "es_abc profundidad t2 ==>
es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a2:"es_abc profundidad t2"
thus "es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a3:"es_abc nodos t1"
thus "es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a4:"es_abc nodos t2"
thus "nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a5:"nodos t1 = nodos t2"
thus "profundidad t1 = profundidad t2"
proof-
obtain n where 1:"profundidad t1 = n" by auto
with a1 have 2:"t1 = abc n"using auxprof by auto
hence 3:"es_abc nodos t1" using auxnodo by auto
have "nodos t1 = (2::nat)^n - 1" using 2 auxnodo by auto
hence 3:"nodos t2 = (2::nat)^n - 1" using a5 by auto
obtain m where 4:"profundidad t2 = m" by auto
with a2 have 5:"t2 = abc m"using auxprof by auto
hence 6:"es_abc nodos t2" using auxnodo by auto
have "nodos t2 = (2::nat)^m - 1" using 5 auxnodo by auto
with 3 have 7:" (2::nat)^m - 1 = (2::nat) ^n - 1" by auto
hence "m = n" proof -
have " (2::nat)^m - 1 = (2::nat) ^n - 1"using 7 by auto
hence "(2::nat)^m - 1 + 1 = (2::nat) ^n" by auto
hence "(2::nat)^m = (2::nat) ^n" by auto
thus ?thesis apply (induct, auto)done
qed
hence "t2 = abc n" using 5 by auto
with 2 have "t1= t2" by auto
thus "profundidad t1 = profundidad t2" by auto
qed
qed
qed
qed
qed
qed
qed

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que (abc n) es un árbol binario completo.
---------------------------------------------------------------------
*}
--"Pedrosrei:"
lemma " es_abc f (abc n)"
apply (induct n, auto) done

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar que si a es un árbolo binario completo
respecto de la profundidad, entonces a es (abc (profundidad a)).
---------------------------------------------------------------------
*}
--"Pedrosrei:"
lemma "es_abc profundidad a ==> (a= abc (profundidad a))"
apply (induct a, auto) done

text {*
---------------------------------------------------------------------
Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de
(es_abc size).
---------------------------------------------------------------------
*}
--"Pedrosrei:"
lemma "es_abc f = es_abc nodos
quickcheck
oops
text {*
El contraejemplo no es más que una medida constante, la trivial:

Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:

f = λx. a⇣1
x = N H (N H H)

Evaluated terms:
es_abc f x = True
es_abc R8_Arboles_binarios_completos.size x = False
*}
end
</source>

Relación 8

2014-12-08T12:36:39Z

Javrodviv1:

<source lang="isar">
header {* R8: Árboles binarios completos *}

theory R8_Arboles_binarios_completos
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que no tienen información ni en los nodos y ni en las
hojas. Por ejemplo, el árbol
·
/ \
/ \
· ·
/ \ / \
· · · ·
se representa por "N (N H H) (N H H)".
---------------------------------------------------------------------
*}

datatype arbol = H | N arbol arbol

value "N (N H H) (N H H)"

text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
hojas :: "arbol => nat"
tal que (hojas a) es el número de hojas del árbol a. Por ejemplo,
hojas (N (N H H) (N H H)) = 4
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun hojas :: "arbol => nat" where
"hojas H = 1"
| "hojas (N i d) = hojas i + hojas d"

value "hojas (N (N H H) (N H H))" -- "= 4"

text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
profundidad :: "arbol => nat"
tal que (profundidad a) es la profundidad del árbol a. Por ejemplo,
profundidad (N (N H H) (N H H)) = 2
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun max :: "nat ⇒ nat ⇒ nat" where
"max a b= (if a≥ b then a else b)"

value "max 6 3" -- "= 6"

fun profundidad :: "arbol => nat" where
"profundidad H = 0"
| "profundidad (N a b) = 1 + max (profundidad a) (profundidad b)"

value "profundidad (N (N H H) (N H H))" -- "= 2"

(* Javrodviv1: Explico estas dos funciones, la que utilizo para los
lemas de abajo es profundidad ya que profundidad1 me encuentra
contraejemplos y para evitar eso busque definir profundidad
definidad de manera distinta. No obstante la que a mi me parece
mas sensata para definir la profundidad de un árbol es la
profundidad1 *)

(* Javrodviv1: Fallo mio ya lo corregí*)

(*Pedrosrei: La profundidad correcta es la mayor. Si te encuentra
contraejemplos más adelante es que te has equivocado en los
enunciados. Las funciones máximo y mínimo vienen predefinidas
ya sin necesidad de definirlas. *)

text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
abc :: "nat ⇒ arbol"
tal que (abc n) es el árbol binario completo de profundidad n. Por
ejemplo,
abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun abc :: "nat ⇒ arbol" where
"abc 0 = H"
| "abc (Suc n) = N (abc n) (abc n)"

value "abc 3" -- "= N (N (N H H) (N H H)) (N (N H H) (N H H))"

text {*
---------------------------------------------------------------------
Ejercicio 6. Un árbol binario a es completo respecto de la medida f si
a es una hoja o bien a es de la forma (N i d) y se cumple que tanto i
como d son árboles binarios completos respecto de f y, además,
f(i) = f(r).

Definir la función
es_abc :: "(arbol => 'a) => arbol => bool
tal que (es_abc f a) se verifica si a es un árbol binario completo
respecto de f.
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
| "es_abc f (N a b) = ((f a = f b) ∧ (es_abc f a ∧ es_abc f b))"

text {*
---------------------------------------------------------------------
Nota. (size a) es el número de nodos del árbol a. Por ejemplo,
size (N (N H H) (N H H)) = 3
---------------------------------------------------------------------
*}

text{*Para entenderme he cambiado de función de tamaño, la demostración
es análoga pero buscando las simplificaciones de size cuando correspondan
*}

fun nodos::"arbol ⇒ nat" where
"nodos H = 0"
|"nodos (N i d) = 1+(nodos i)+(nodos d)"

lemma "size t= nodos t"
apply (induct t, auto)done

value "size (N (N H H) (N H H))"
value "size (N (N (N H H) (N H H)) (N (N H H) (N H H)))"

text {*
---------------------------------------------------------------------
Nota. Tenemos 3 funciones de medida sobre los árboles: número de
hojas, número de nodos y profundidad. A cada una le corresponde un
concepto de completitud. En los siguientes ejercicios demostraremos
que los tres conceptos de completitud son iguales.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de hojas.
---------------------------------------------------------------------
*}

text{*Pedrosrei: Los enunciados y demostraciones que vienen a continuación
son feos y engorrosos. Yo he optado por demostrarlo todo a través de
una propiedad extraña a la demostración en principio. Animo encarecidamente
a que pongáis una demostración más corta y directa. Voy explicando paso
a paso qué he hecho en cada momento. Hecha esta demostración, el resto
son triviales por una cadena de resultados.
No existe relación de implicación en ningún sentido
entre hojas y profundidad, como es obvio y muestran los siguientes
contraejemplos: *}
lemma "(((hojas(t1) = hojas(t2)))-->(profundidad(t1) = profundidad(t2)))"
quickcheck
oops
lemma "((profundidad(t1) = profundidad(t2)) -->
((hojas(t1) = hojas(t2))))"
quickcheck
oops
lemma "((profundidad(t1) = profundidad(t2)) <->
((hojas(t1) = hojas(t2))))"
quickcheck
oops
text {* Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:

t1 = N (N H H) (N H H)
t2 = N H (N H H)

Evaluated terms:
hojas t1 = 4
hojas t2 = 3

Ahora pongo una serie de resultados auxiliares que ayudarán en la prueba
*}

lemma auxprof:"(es_abc profundidad t)∧(profundidad t = n)==> (t= abc n)"
apply (induct t arbitrary:n, auto)done

lemma eq_1_iff_exp_0:"Suc 0 = 2 ^ n <-> n=0" apply (cases n, auto) done

lemma auxhojas:"(t= abc n)==> (es_abc hojas t)"
apply (induct n arbitrary: t, auto simp add: eq_1_iff_exp_0) done

lemma auxhoja:"(t= abc n)==>((hojas t = 2^n))"
apply (induct n arbitrary: t rule: abc.induct, auto)done

text{* Pedrosrei. Y aquí viene la demostración larga y fea que os animo a mejorar.
He dejado los pasos exactamente que indica el razonador para que
veáis qué hace en cada caso:
*}

lemma prof_eq_hoja:"es_abc profundidad t <-> es_abc hojas t"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc hojas t" using auxhojas by auto
next
show "es_abc hojas t ==> es_abc profundidad t" apply (induct t, auto)
proof -
fix t1 t2
assume a1:"es_abc profundidad t1"
thus "es_abc profundidad t2 ==>
es_abc hojas t1 ==>
es_abc hojas t2 ==>
hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2" proof -
assume a2:"es_abc profundidad t2"
thus "es_abc hojas t1 ==>
es_abc hojas t2 ==>
hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2"proof-
assume a3:"es_abc hojas t1"
thus "es_abc hojas t2 ==>
hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2"proof-
assume a4:"es_abc hojas t2"
thus "hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2" proof -
assume a5:"hojas t1 = hojas t2"
thus "profundidad t1 = profundidad t2"
proof-
obtain n where 1:"profundidad t1 = n" by auto
with a1 have 2:"t1 = abc n"using auxprof by auto
hence 3:"es_abc hojas t1" using auxhojas by auto
have "hojas t1 = (2::nat)^n" using 2 auxhoja by auto
hence 3:"hojas t2 = (2::nat)^n" using a5 by auto
obtain m where 4:"profundidad t2 = m" by auto
with a2 have 5:"t2 = abc m"using auxprof by auto
hence 6:"es_abc hojas t2" using auxhojas by auto
have "hojas t2 = (2::nat)^m" using 5 auxhoja by auto
with 3 have " (2::nat)^m = (2::nat) ^n" by auto
hence "m = n" apply (induct, auto)done
hence "t2 = abc n" using 5 by auto
with 2 have "t1= t2" by auto
thus "profundidad t1 = profundidad t2" by auto
qed
qed
qed
qed
qed
qed
qed

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que un árbol binario a es completo respecto del
número de hojas syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}
text{* Pedrosrei. Aquí dejo esta. Es trivial debido a la demostración anterior,
sólo hace falta coger el mismo desvío. Aquí sí que podéis encontrar
una mucho más directa: *}

lemma auxnodo:"(t= abc n)==>(es_abc nodos t)∧(nodos t = (2^n - 1))"
apply (induct n arbitrary: t rule: abc.induct, auto)done

lemma nodos_eq_hoja:"es_abc nodos t <-> es_abc hojas t" (is "?P t")
proof -
have 1:"es_abc hojas t <-> es_abc profundidad t" using prof_eq_hoja by auto
hence 2:"?P t = (es_abc profundidad t <-> es_abc nodos t)" by auto
have "(es_abc profundidad t <-> es_abc nodos t)"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc nodos t" using auxnodo by auto
next
show "es_abc nodos t ==> es_abc profundidad t" apply (induct t, auto)
proof -
fix t1 t2
assume a1:"es_abc profundidad t1"
thus "es_abc profundidad t2 ==>
es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a2:"es_abc profundidad t2"
thus "es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a3:"es_abc nodos t1"
thus "es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a4:"es_abc nodos t2"
thus "nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a5:"nodos t1 = nodos t2"
thus "profundidad t1 = profundidad t2"
proof-
obtain n where 1:"profundidad t1 = n" by auto
with a1 have 2:"t1 = abc n"using auxprof by auto
hence 3:"es_abc nodos t1" using auxnodo by auto
have "nodos t1 = (2::nat)^n - 1" using 2 auxnodo by auto
hence 3:"nodos t2 = (2::nat)^n - 1" using a5 by auto
obtain m where 4:"profundidad t2 = m" by auto
with a2 have 5:"t2 = abc m"using auxprof by auto
hence 6:"es_abc nodos t2" using auxnodo by auto
have "nodos t2 = (2::nat)^m - 1" using 5 auxnodo by auto
with 3 have 7:" (2::nat)^m - 1 = (2::nat) ^n - 1" by auto
hence "m = n" proof -
have " (2::nat)^m - 1 = (2::nat) ^n - 1"using 7 by auto
hence "(2::nat)^m - 1 + 1 = (2::nat) ^n" by auto
hence "(2::nat)^m = (2::nat) ^n" by auto
thus ?thesis apply (induct, auto)done
qed
hence "t2 = abc n" using 5 by auto
with 2 have "t1= t2" by auto
thus "profundidad t1 = profundidad t2" by auto
qed
qed
qed
qed
qed
qed
qed
with 1 2 show ?thesis by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}

text {* Pedrosrei. De hecho, esta es una parte de la anterior: *}

lemma prof_eq_nodos: "(es_abc profundidad t <-> es_abc nodos t)"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc nodos t" using auxnodo by auto
next
show "es_abc nodos t ==> es_abc profundidad t" apply (induct t, auto)
proof -
fix t1 t2
assume a1:"es_abc profundidad t1"
thus "es_abc profundidad t2 ==>
es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a2:"es_abc profundidad t2"
thus "es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a3:"es_abc nodos t1"
thus "es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a4:"es_abc nodos t2"
thus "nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a5:"nodos t1 = nodos t2"
thus "profundidad t1 = profundidad t2"
proof-
obtain n where 1:"profundidad t1 = n" by auto
with a1 have 2:"t1 = abc n"using auxprof by auto
hence 3:"es_abc nodos t1" using auxnodo by auto
have "nodos t1 = (2::nat)^n - 1" using 2 auxnodo by auto
hence 3:"nodos t2 = (2::nat)^n - 1" using a5 by auto
obtain m where 4:"profundidad t2 = m" by auto
with a2 have 5:"t2 = abc m"using auxprof by auto
hence 6:"es_abc nodos t2" using auxnodo by auto
have "nodos t2 = (2::nat)^m - 1" using 5 auxnodo by auto
with 3 have 7:" (2::nat)^m - 1 = (2::nat) ^n - 1" by auto
hence "m = n" proof -
have " (2::nat)^m - 1 = (2::nat) ^n - 1"using 7 by auto
hence "(2::nat)^m - 1 + 1 = (2::nat) ^n" by auto
hence "(2::nat)^m = (2::nat) ^n" by auto
thus ?thesis apply (induct, auto)done
qed
hence "t2 = abc n" using 5 by auto
with 2 have "t1= t2" by auto
thus "profundidad t1 = profundidad t2" by auto
qed
qed
qed
qed
qed
qed
qed

text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que (abc n) es un árbol binario completo.
---------------------------------------------------------------------
*}
--"Pedrosrei:"
lemma " es_abc f (abc n)"
apply (induct n, auto) done

text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar que si a es un árbolo binario completo
respecto de la profundidad, entonces a es (abc (profundidad a)).
---------------------------------------------------------------------
*}
--"Pedrosrei:"
lemma "es_abc profundidad a ==> (a= abc (profundidad a))"
apply (induct a, auto) done

text {*
---------------------------------------------------------------------
Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de
(es_abc size).
---------------------------------------------------------------------
*}
--"Pedrosrei:"
lemma "es_abc f = es_abc nodos
quickcheck
oops
text {*
El contraejemplo no es más que una medida constante, la trivial:

Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:

f = λx. a⇣1
x = N H (N H H)

Evaluated terms:
es_abc f x = True
es_abc R8_Arboles_binarios_completos.size x = False
*}
end
</source>

Relación 8

2014-12-06T12:10:52Z

Javrodviv1:

Relación 5

2014-11-16T15:23:42Z

Javrodviv1:

<source lang="isar">
header {* R5: Cuantificadores sobre listas *}

theory R5
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ 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 (λx. 1<length x) [[2,1,4],[1,3]]
¬todos (λx. 1<length x) [[2,1,4],[3]]

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

--"jeshorcob,javrodviv1"
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
|"todos p (x#xs) = (p x ∧ todos p xs)"

--"jeshorcob"
fun todos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos2 p xs = foldr (λx. op ∧ (p x)) xs True"

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

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

--"jeshorcob,javrodviv1"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = True"
|"algunos p (x#xs) = (p x ∨ todos p xs)"

--"jeshorcob"
fun algunos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos2 p xs = foldr (λx. op ∨ (p x)) xs True"

-- "javrodviv1"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = False"
|"algunos p (x#xs) = (p x ∨ todos p xs)"
(* Nota. Nos da igual que sea True o False, pero para una proposición
de más a delante necesitamos que sea False*)

text {*
---------------------------------------------------------------------
Ejercicio 3.1. Demostrar o refutar automáticamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob,javrodviv1"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 3.2. Demostrar o refutar detalladamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob"

lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix x xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (x#xs) =
((P x ∧ Q x) ∧ todos (λx. P x ∧ Q x) xs) " by simp
also have "... = (P x∧Q x∧todos P xs∧todos Q xs)" using HI by simp
also have "... = ((P x∧todos P xs)∧(Q x ∧ todos Q xs))" by arith
also have "... = (todos P (x#xs) ∧ (Q x ∧ todos Q xs))" by simp
also have "... = (todos P (x#xs) ∧ todos Q (x#xs))" by simp
finally show "todos (λx. P x ∧ Q x) (x#xs) =
(todos P (x#xs) ∧ todos Q (x#xs))" by simp
qed

-- "javrodviv1"

lemma todo_append:
"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix a xs
assume HI:"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (a # xs) = (((P a) ∧ (Q a)) ∧ todos (λx. P x ∧ Q x) xs)" by simp
also have " ... = ((P a) ∧ (Q a) ∧ todos P xs ∧ todos Q xs)" using HI by simp
finally show "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 4.1. Demostrar o refutar automáticamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

--"jeshorcob,javrodviv1"
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x) auto

text {*
---------------------------------------------------------------------
Ejercicio 4.2. Demostrar o refutar detalladamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a#x)@y) = (P a ∧ todos P (x@y))" by simp
also have "... = (P a ∧ todos P x ∧ todos P y)" using HI by simp
also have "... = (todos P (a#x) ∧ todos P y)" by simp
finally show "todos P ((a#x)@y) =
(todos P (a#x) ∧ todos P y)" by simp
qed

-- "javrodviv1"
(* es igual que la de jeshorcob pero nos podemos ahorrar
una linea de comando*)

lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI:"todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a # x) @ y) = ((P a) ∧ todos P (x @ y))" by simp
also have " ... = ((P a) ∧ todos P x ∧ todos P y)" using HI by simp
finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)"
by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 5.1. Demostrar o refutar automáticamente
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
apply (induct xs)
apply (auto simp add: todos_append)
done

-- "javrodviv1"

lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)

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

--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []" by simp
next
fix x xs
assume HI: "todos P (rev xs) = todos P xs"
have "todos P (rev (x#xs)) = todos P ((rev xs) @ [x])" by simp
also have "... = (todos P (rev xs) ∧ todos P [x])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [x])" using HI by simp
also have "... = (todos P xs ∧ P x)" by simp
also have "... = (P x ∧ todos P xs)" by arith
also have "... = todos P (x#xs)" by simp
finally show "todos P (rev (x#xs)) = todos P (x#xs)" by simp
qed

-- "javrodviv1"

lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show " todos P (rev []) = todos P []" by simp
next
fix a xs
assume HI: "todos P (rev xs) = todos P xs "
have "todos P (rev (a # xs)) = todos P ((rev xs) @ [a])" by simp
also have " ... = (todos P (rev xs) ∧ todos P [a])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [a])" using HI by simp
finally show " todos P (rev (a # xs)) = todos P (a # xs)" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar:
algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops

text {* Encuentra el contraejemplo
P = {a⇩1}
Q = {a⇩2}
xs = [a⇩1, a⇩2]
*}

-- "javrodviv1"
(* A mi no me encuentra contraejemplo así que decidí probarlo pero me
atasque, dejo mi demostración hasta donde estoy atascado*)

lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
proof (induct xs)
show "algunos (λx. P x ∧ Q x) [] = (algunos P [] ∧ algunos Q [])" by simp
next
fix a xs
assume HI:"algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
have "algunos (λx. P x ∧ Q x) (a # xs) = ((P a) ∧ (Q a) ∨ algunos (λx. P x ∧ Q x) xs)"
by simp
also have "... = (((P a) ∧ (Q a)) ∨ (algunos P xs ∧ algunos Q xs))" using HI by simp
oops

text {*
---------------------------------------------------------------------
Ejercicio 7.1. Demostrar o refutar automáticamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

-- "javrodviv1"

lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 7.2. Demostrar o refutar datalladamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

-- "javrodviv1"

lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
show " algunos P (map f []) = algunos (P ∘ f) []" by simp
next
fix a xs
assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
have "algunos P (map f (a # xs)) = ((P (f a)) ∨ algunos P (map f xs))" by simp
also have " ... = (((P ∘ f) a) ∨ algunos (P ∘ f) xs)" using HI by simp
finally show " algunos P (map f (a # xs)) = algunos (P ∘ f) (a # xs)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 8.1. Demostrar o refutar automáticamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 8.2. Demostrar o refutar detalladamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma algunos_append:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
show "algunos P ([] @ ys) = (algunos P [] ∨ algunos P ys)" by simp
next
fix a xs
assume HI:"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
have "algunos P ((a # xs) @ ys) = ((P a) ∨ algunos P (xs@ys))" by simp
also have "... = ((P a) ∨ (algunos P xs ∨ algunos P ys))"
using HI by simp
finally show "algunos P ((a # xs) @ ys) =
(algunos P (a # xs) ∨ algunos P ys)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 9.1. Demostrar o refutar automáticamente
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add: algunos_append)

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

-- "javrodviv1"
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next
fix a xs
assume HI:"algunos P (rev xs) = algunos P xs"
have "algunos P (rev (a # xs)) = algunos P (rev xs @[a])" by simp
also have "... = (algunos P xs ∨ (P a))" using HI using algunos_append by auto
finally show " algunos P (rev (a # xs)) = algunos P (a # xs)" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 10. Encontrar un término no trivial Z tal que sea cierta la
siguiente ecuación:
algunos (λx. P x ∨ Q x) xs = Z
y demostrar la equivalencia de forma automática y detallada.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 11.1. Demostrar o refutar automáticamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 11.2. Demostrar o refutar datalladamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
show " algunos P [] = (¬ todos (λx. ¬ P x) [])" by simp
next
fix a xs
assume HI:"algunos P xs = (¬ todos (λx. ¬ P x) xs)"
have "algunos P (a # xs) = ((P a) ∨ algunos P xs)" by simp
also have "... = ((P a) ∨ (¬ todos (λx. ¬ P x) xs))" using HI by simp
finally show "algunos P (a # xs) =(¬ todos (λx. ¬ P x) (a#xs))" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 12. Definir la funcion primitiva recursiva
estaEn :: 'a ⇒ 'a list ⇒ 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
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = ((x=a) ∨ estaEn x xs)"

text {*
---------------------------------------------------------------------
Ejercicio 13. Expresar la relación existente entre estaEn y algunos.
Demostrar dicha relación de forma automática y detallada.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 14. Definir la función primitiva recursiva
sinDuplicados :: 'a list ⇒ 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
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados [] = False"
| "sinDuplicados (x#xs) = (estaEn x xs ∨ sinDuplicados xs)"

text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la función primitiva recursiva
borraDuplicados :: 'a list ⇒ 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.
---------------------------------------------------------------------
*}

-- "javrodviv1"
fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados [] = []"
| "borraDuplicados (x#xs) = (if estaEn x xs then borraDuplicados xs else (x#(borraDuplicados xs)))"

text {*
---------------------------------------------------------------------
Ejercicio 16.1. Demostrar o refutar automáticamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma "length (borraDuplicados xs) ≤ length xs"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 16.2. Demostrar o refutar detalladamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a xs
assume HI:"length (borraDuplicados xs) ≤ length xs"
have "length (borraDuplicados (a#xs))≤length (a#borraDuplicados xs)" by simp
also have "... = 1+ length (borraDuplicados xs)" by simp
also have "... ≤ 1+ length xs" using HI by simp
finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 17.1. Demostrar o refutar automáticamente
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs) auto

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

lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18.1. Demostrar o refutar automáticamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma "sinDuplicados (borraDuplicados xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18.2. Demostrar o refutar detalladamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma sinDuplicados_borraDuplicados:
"sinDuplicados (borraDuplicados xs)"
oops

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

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

end
</source>

Relación 5

2014-11-16T14:21:55Z

Javrodviv1:

<source lang="isar">
header {* R5: Cuantificadores sobre listas *}

theory R5
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ 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 (λx. 1<length x) [[2,1,4],[1,3]]
¬todos (λx. 1<length x) [[2,1,4],[3]]

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

--"jeshorcob,javrodviv1"
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
|"todos p (x#xs) = (p x ∧ todos p xs)"

--"jeshorcob"
fun todos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos2 p xs = foldr (λx. op ∧ (p x)) xs True"

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

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

--"jeshorcob,javrodviv1"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = True"
|"algunos p (x#xs) = (p x ∨ todos p xs)"

--"jeshorcob"
fun algunos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos2 p xs = foldr (λx. op ∨ (p x)) xs True"

-- "javrodviv1"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = False"
|"algunos p (x#xs) = (p x ∨ todos p xs)"
(* Nota. Nos da igual que sea True o False, pero para una proposición
de más a delante necesitamos que sea False*)

text {*
---------------------------------------------------------------------
Ejercicio 3.1. Demostrar o refutar automáticamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob,javrodviv1"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 3.2. Demostrar o refutar detalladamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob"

lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix x xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (x#xs) =
((P x ∧ Q x) ∧ todos (λx. P x ∧ Q x) xs) " by simp
also have "... = (P x∧Q x∧todos P xs∧todos Q xs)" using HI by simp
also have "... = ((P x∧todos P xs)∧(Q x ∧ todos Q xs))" by arith
also have "... = (todos P (x#xs) ∧ (Q x ∧ todos Q xs))" by simp
also have "... = (todos P (x#xs) ∧ todos Q (x#xs))" by simp
finally show "todos (λx. P x ∧ Q x) (x#xs) =
(todos P (x#xs) ∧ todos Q (x#xs))" by simp
qed

-- "javrodviv1"

lemma todo_append:
"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix a xs
assume HI:"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (a # xs) = (((P a) ∧ (Q a)) ∧ todos (λx. P x ∧ Q x) xs)" by simp
also have " ... = ((P a) ∧ (Q a) ∧ todos P xs ∧ todos Q xs)" using HI by simp
finally show "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 4.1. Demostrar o refutar automáticamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

--"jeshorcob,javrodviv1"
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x) auto

text {*
---------------------------------------------------------------------
Ejercicio 4.2. Demostrar o refutar detalladamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a#x)@y) = (P a ∧ todos P (x@y))" by simp
also have "... = (P a ∧ todos P x ∧ todos P y)" using HI by simp
also have "... = (todos P (a#x) ∧ todos P y)" by simp
finally show "todos P ((a#x)@y) =
(todos P (a#x) ∧ todos P y)" by simp
qed

-- "javrodviv1"
(* es igual que la de jeshorcob pero nos podemos ahorrar
una linea de comando*)

lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI:"todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a # x) @ y) = ((P a) ∧ todos P (x @ y))" by simp
also have " ... = ((P a) ∧ todos P x ∧ todos P y)" using HI by simp
finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)"
by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 5.1. Demostrar o refutar automáticamente
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
apply (induct xs)
apply (auto simp add: todos_append)
done

-- "javrodviv1"

lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)

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

--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []" by simp
next
fix x xs
assume HI: "todos P (rev xs) = todos P xs"
have "todos P (rev (x#xs)) = todos P ((rev xs) @ [x])" by simp
also have "... = (todos P (rev xs) ∧ todos P [x])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [x])" using HI by simp
also have "... = (todos P xs ∧ P x)" by simp
also have "... = (P x ∧ todos P xs)" by arith
also have "... = todos P (x#xs)" by simp
finally show "todos P (rev (x#xs)) = todos P (x#xs)" by simp
qed

-- "javrodviv1"

lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show " todos P (rev []) = todos P []" by simp
next
fix a xs
assume HI: "todos P (rev xs) = todos P xs "
have "todos P (rev (a # xs)) = todos P ((rev xs) @ [a])" by simp
also have " ... = (todos P (rev xs) ∧ todos P [a])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [a])" using HI by simp
finally show " todos P (rev (a # xs)) = todos P (a # xs)" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar:
algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops

text {* Encuentra el contraejemplo
P = {a⇩1}
Q = {a⇩2}
xs = [a⇩1, a⇩2]
*}

-- "javrodviv1"
(* A mi no me encuentra contraejemplo así que decidí probarlo pero me
atasque, dejo mi demostración hasta donde estoy atascado*)

lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
proof (induct xs)
show "algunos (λx. P x ∧ Q x) [] = (algunos P [] ∧ algunos Q [])" by simp
next
fix a xs
assume HI:"algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
have "algunos (λx. P x ∧ Q x) (a # xs) = ((P a) ∧ (Q a) ∨ algunos (λx. P x ∧ Q x) xs)"
by simp
also have "... = (((P a) ∧ (Q a)) ∨ (algunos P xs ∧ algunos Q xs))" using HI by simp
oops

text {*
---------------------------------------------------------------------
Ejercicio 7.1. Demostrar o refutar automáticamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

-- "javrodviv1"

lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 7.2. Demostrar o refutar datalladamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

-- "javrodviv1"

lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
show " algunos P (map f []) = algunos (P ∘ f) []" by simp
next
fix a xs
assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
have "algunos P (map f (a # xs)) = ((P (f a)) ∨ algunos P (map f xs))" by simp
also have " ... = (((P ∘ f) a) ∨ algunos (P ∘ f) xs)" using HI by simp
finally show " algunos P (map f (a # xs)) = algunos (P ∘ f) (a # xs)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 8.1. Demostrar o refutar automáticamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 8.2. Demostrar o refutar detalladamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma algunos_append:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
show "algunos P ([] @ ys) = (algunos P [] ∨ algunos P ys)" by simp
next
fix a xs
assume HI:"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
have "algunos P ((a # xs) @ ys) = ((P a) ∨ algunos P (xs@ys))" by simp
also have "... = ((P a) ∨ (algunos P xs ∨ algunos P ys))"
using HI by simp
finally show "algunos P ((a # xs) @ ys) =
(algunos P (a # xs) ∨ algunos P ys)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 9.1. Demostrar o refutar automáticamente
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add: algunos_append)

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

-- "javrodviv1"
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next
fix a xs
assume HI:"algunos P (rev xs) = algunos P xs"
have "algunos P (rev (a # xs)) = algunos P (rev xs @[a])" by simp
also have "... = (algunos P xs ∨ (P a))" using HI using algunos_append by auto
finally show " algunos P (rev (a # xs)) = algunos P (a # xs)" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 10. Encontrar un término no trivial Z tal que sea cierta la
siguiente ecuación:
algunos (λx. P x ∨ Q x) xs = Z
y demostrar la equivalencia de forma automática y detallada.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 11.1. Demostrar o refutar automáticamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 11.2. Demostrar o refutar datalladamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

-- "javrodviv1"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
show " algunos P [] = (¬ todos (λx. ¬ P x) [])" by simp
next
fix a xs
assume HI:"algunos P xs = (¬ todos (λx. ¬ P x) xs)"
have "algunos P (a # xs) = ((P a) ∨ algunos P xs)" by simp
also have "... = ((P a) ∨ (¬ todos (λx. ¬ P x) xs))" using HI by simp
finally show "algunos P (a # xs) =(¬ todos (λx. ¬ P x) (a#xs))" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 12. Definir la funcion primitiva recursiva
estaEn :: 'a ⇒ 'a list ⇒ 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
---------------------------------------------------------------------
*}

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x xs = undefined"

text {*
---------------------------------------------------------------------
Ejercicio 13. Expresar la relación existente entre estaEn y algunos.
Demostrar dicha relación de forma automática y detallada.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 14. Definir la función primitiva recursiva
sinDuplicados :: 'a list ⇒ 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
---------------------------------------------------------------------
*}

fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados xs = undefined"

text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la función primitiva recursiva
borraDuplicados :: 'a list ⇒ 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.
---------------------------------------------------------------------
*}

fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados xs = undefined"

text {*
---------------------------------------------------------------------
Ejercicio 16.1. Demostrar o refutar automáticamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}

lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 16.2. Demostrar o refutar detalladamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}

lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 17.1. Demostrar o refutar automáticamente
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
*}

lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
oops

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

lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18.1. Demostrar o refutar automáticamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma "sinDuplicados (borraDuplicados xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18.2. Demostrar o refutar detalladamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma sinDuplicados_borraDuplicados:
"sinDuplicados (borraDuplicados xs)"
oops

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

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

end
</source>

Relación 5

2014-11-16T13:17:12Z

Javrodviv1:

<source lang="isar">
header {* R5: Cuantificadores sobre listas *}

theory R5
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ 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 (λx. 1<length x) [[2,1,4],[1,3]]
¬todos (λx. 1<length x) [[2,1,4],[3]]

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

--"jeshorcob,javrodviv1"
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
|"todos p (x#xs) = (p x ∧ todos p xs)"

--"jeshorcob"
fun todos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos2 p xs = foldr (λx. op ∧ (p x)) xs True"

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

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

--"jeshorcob,javrodviv1"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = True"
|"algunos p (x#xs) = (p x ∨ todos p xs)"

--"jeshorcob"
fun algunos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos2 p xs = foldr (λx. op ∨ (p x)) xs True"

-- "javrodviv1"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = False"
|"algunos p (x#xs) = (p x ∨ todos p xs)"
(* Nota. Nos da igual que sea True o False, pero para una proposición
de más a delante necesitamos que sea False*)

text {*
---------------------------------------------------------------------
Ejercicio 3.1. Demostrar o refutar automáticamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob,javrodviv1"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 3.2. Demostrar o refutar detalladamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob"

lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix x xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (x#xs) =
((P x ∧ Q x) ∧ todos (λx. P x ∧ Q x) xs) " by simp
also have "... = (P x∧Q x∧todos P xs∧todos Q xs)" using HI by simp
also have "... = ((P x∧todos P xs)∧(Q x ∧ todos Q xs))" by arith
also have "... = (todos P (x#xs) ∧ (Q x ∧ todos Q xs))" by simp
also have "... = (todos P (x#xs) ∧ todos Q (x#xs))" by simp
finally show "todos (λx. P x ∧ Q x) (x#xs) =
(todos P (x#xs) ∧ todos Q (x#xs))" by simp
qed

-- "javrodviv1"

lemma todo_append:
"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix a xs
assume HI:"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (a # xs) = (((P a) ∧ (Q a)) ∧ todos (λx. P x ∧ Q x) xs)" by simp
also have " ... = ((P a) ∧ (Q a) ∧ todos P xs ∧ todos Q xs)" using HI by simp
finally show "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 4.1. Demostrar o refutar automáticamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

--"jeshorcob,javrodviv1"
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x) auto

text {*
---------------------------------------------------------------------
Ejercicio 4.2. Demostrar o refutar detalladamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a#x)@y) = (P a ∧ todos P (x@y))" by simp
also have "... = (P a ∧ todos P x ∧ todos P y)" using HI by simp
also have "... = (todos P (a#x) ∧ todos P y)" by simp
finally show "todos P ((a#x)@y) =
(todos P (a#x) ∧ todos P y)" by simp
qed

-- "javrodviv1"
(* es igual que la de jeshorcob pero nos podemos ahorrar
una linea de comando*)

lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI:"todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a # x) @ y) = ((P a) ∧ todos P (x @ y))" by simp
also have " ... = ((P a) ∧ todos P x ∧ todos P y)" using HI by simp
finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)"
by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 5.1. Demostrar o refutar automáticamente
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
apply (induct xs)
apply (auto simp add: todos_append)
done

-- "javrodviv1"

lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)

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

--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []" by simp
next
fix x xs
assume HI: "todos P (rev xs) = todos P xs"
have "todos P (rev (x#xs)) = todos P ((rev xs) @ [x])" by simp
also have "... = (todos P (rev xs) ∧ todos P [x])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [x])" using HI by simp
also have "... = (todos P xs ∧ P x)" by simp
also have "... = (P x ∧ todos P xs)" by arith
also have "... = todos P (x#xs)" by simp
finally show "todos P (rev (x#xs)) = todos P (x#xs)" by simp
qed

-- "javrodviv1"

lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show " todos P (rev []) = todos P []" by simp
next
fix a xs
assume HI: "todos P (rev xs) = todos P xs "
have "todos P (rev (a # xs)) = todos P ((rev xs) @ [a])" by simp
also have " ... = (todos P (rev xs) ∧ todos P [a])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [a])" using HI by simp
finally show " todos P (rev (a # xs)) = todos P (a # xs)" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar:
algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops

text {* Encuentra el contraejemplo
P = {a⇩1}
Q = {a⇩2}
xs = [a⇩1, a⇩2]
*}

-- "javrodviv1"
(* A mi no me encuentra contraejemplo así que decidí probarlo pero me
atasque, dejo mi demostración hasta donde estoy atascado*)

lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
proof (induct xs)
show "algunos (λx. P x ∧ Q x) [] = (algunos P [] ∧ algunos Q [])" by simp
next
fix a xs
assume HI:"algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
have "algunos (λx. P x ∧ Q x) (a # xs) = ((P a) ∧ (Q a) ∨ algunos (λx. P x ∧ Q x) xs)"
by simp
also have "... = (((P a) ∧ (Q a)) ∨ (algunos P xs ∧ algunos Q xs))" using HI by simp
oops

text {*
---------------------------------------------------------------------
Ejercicio 7.1. Demostrar o refutar automáticamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

-- "javrodviv1"

lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 7.2. Demostrar o refutar datalladamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

-- "javrodviv1"

lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
show " algunos P (map f []) = algunos (P ∘ f) []" by simp
next
fix a xs
assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
have "algunos P (map f (a # xs)) = ((P (f a)) ∨ algunos P (map f xs))" by simp
also have " ... = (((P ∘ f) a) ∨ algunos (P ∘ f) xs)" using HI by simp
finally show " algunos P (map f (a # xs)) = algunos (P ∘ f) (a # xs)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 8.1. Demostrar o refutar automáticamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 8.2. Demostrar o refutar detalladamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

lemma algunos_append:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 9.1. Demostrar o refutar automáticamente
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}

lemma "algunos P (rev xs) = algunos P xs"
oops

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

lemma "algunos P (rev xs) = algunos P xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 10. Encontrar un término no trivial Z tal que sea cierta la
siguiente ecuación:
algunos (λx. P x ∨ Q x) xs = Z
y demostrar la equivalencia de forma automática y detallada.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 11.1. Demostrar o refutar automáticamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 11.2. Demostrar o refutar datalladamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 12. Definir la funcion primitiva recursiva
estaEn :: 'a ⇒ 'a list ⇒ 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
---------------------------------------------------------------------
*}

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x xs = undefined"

text {*
---------------------------------------------------------------------
Ejercicio 13. Expresar la relación existente entre estaEn y algunos.
Demostrar dicha relación de forma automática y detallada.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 14. Definir la función primitiva recursiva
sinDuplicados :: 'a list ⇒ 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
---------------------------------------------------------------------
*}

fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados xs = undefined"

text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la función primitiva recursiva
borraDuplicados :: 'a list ⇒ 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.
---------------------------------------------------------------------
*}

fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados xs = undefined"

text {*
---------------------------------------------------------------------
Ejercicio 16.1. Demostrar o refutar automáticamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}

lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 16.2. Demostrar o refutar detalladamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}

lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 17.1. Demostrar o refutar automáticamente
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
*}

lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
oops

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

lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18.1. Demostrar o refutar automáticamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma "sinDuplicados (borraDuplicados xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18.2. Demostrar o refutar detalladamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma sinDuplicados_borraDuplicados:
"sinDuplicados (borraDuplicados xs)"
oops

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

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

end
</source>

Relación 5

2014-11-15T20:31:28Z

Javrodviv1:

<source lang="isar">
header {* R5: Cuantificadores sobre listas *}

theory R5
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ 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 (λx. 1<length x) [[2,1,4],[1,3]]
¬todos (λx. 1<length x) [[2,1,4],[3]]

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

--"jeshorcob,javrodviv1"
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
|"todos p (x#xs) = (p x ∧ todos p xs)"

--"jeshorcob"
fun todos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos2 p xs = foldr (λx. op ∧ (p x)) xs True"

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

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

--"jeshorcob,javrodviv1"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = True"
|"algunos p (x#xs) = (p x ∨ todos p xs)"

--"jeshorcob"
fun algunos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos2 p xs = foldr (λx. op ∨ (p x)) xs True"

text {*
---------------------------------------------------------------------
Ejercicio 3.1. Demostrar o refutar automáticamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob,javrodviv1"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 3.2. Demostrar o refutar detalladamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob"

lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix x xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (x#xs) =
((P x ∧ Q x) ∧ todos (λx. P x ∧ Q x) xs) " by simp
also have "... = (P x∧Q x∧todos P xs∧todos Q xs)" using HI by simp
also have "... = ((P x∧todos P xs)∧(Q x ∧ todos Q xs))" by arith
also have "... = (todos P (x#xs) ∧ (Q x ∧ todos Q xs))" by simp
also have "... = (todos P (x#xs) ∧ todos Q (x#xs))" by simp
finally show "todos (λx. P x ∧ Q x) (x#xs) =
(todos P (x#xs) ∧ todos Q (x#xs))" by simp
qed

-- "javrodviv1"

lemma todo_append:
"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix a xs
assume HI:"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (a # xs) = (((P a) ∧ (Q a)) ∧ todos (λx. P x ∧ Q x) xs)" by simp
also have " ... = ((P a) ∧ (Q a) ∧ todos P xs ∧ todos Q xs)" using HI by simp
finally show "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 4.1. Demostrar o refutar automáticamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

--"jeshorcob,javrodviv1"
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x) auto

text {*
---------------------------------------------------------------------
Ejercicio 4.2. Demostrar o refutar detalladamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a#x)@y) = (P a ∧ todos P (x@y))" by simp
also have "... = (P a ∧ todos P x ∧ todos P y)" using HI by simp
also have "... = (todos P (a#x) ∧ todos P y)" by simp
finally show "todos P ((a#x)@y) =
(todos P (a#x) ∧ todos P y)" by simp
qed

-- "javrodviv1"
(* es igual que la de jeshorcob pero nos podemos ahorrar
una linea de comando*)

lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI:"todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a # x) @ y) = ((P a) ∧ todos P (x @ y))" by simp
also have " ... = ((P a) ∧ todos P x ∧ todos P y)" using HI by simp
finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)"
by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 5.1. Demostrar o refutar automáticamente
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
apply (induct xs)
apply (auto simp add: todos_append)
done

-- "javrodviv1"

lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)

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

--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []" by simp
next
fix x xs
assume HI: "todos P (rev xs) = todos P xs"
have "todos P (rev (x#xs)) = todos P ((rev xs) @ [x])" by simp
also have "... = (todos P (rev xs) ∧ todos P [x])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [x])" using HI by simp
also have "... = (todos P xs ∧ P x)" by simp
also have "... = (P x ∧ todos P xs)" by arith
also have "... = todos P (x#xs)" by simp
finally show "todos P (rev (x#xs)) = todos P (x#xs)" by simp
qed

-- "javrodviv1"

lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show " todos P (rev []) = todos P []" by simp
next
fix a xs
assume HI: "todos P (rev xs) = todos P xs "
have "todos P (rev (a # xs)) = todos P ((rev xs) @ [a])" by simp
also have " ... = (todos P (rev xs) ∧ todos P [a])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [a])" using HI by simp
finally show " todos P (rev (a # xs)) = todos P (a # xs)" by auto
qed

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar:
algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops

text {* Encuentra el contraejemplo
P = {a⇩1}
Q = {a⇩2}
xs = [a⇩1, a⇩2]
*}

-- "javrodviv1"
(* A mi no me encuentra contraejemplo así que decidí probarlo pero me
atasque, dejo mi demostración hasta donde estoy atascado*)

lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
proof (induct xs)
show "algunos (λx. P x ∧ Q x) [] = (algunos P [] ∧ algunos Q [])" by simp
next
fix a xs
assume HI:"algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
have "algunos (λx. P x ∧ Q x) (a # xs) = ((P a) ∧ (Q a) ∨ algunos (λx. P x ∧ Q x) xs)"
by simp
also have "... = (((P a) ∧ (Q a)) ∨ (algunos P xs ∧ algunos Q xs))" using HI by simp
oops

text {*
---------------------------------------------------------------------
Ejercicio 7.1. Demostrar o refutar automáticamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

-- "javrodviv1"

lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto

text {*
---------------------------------------------------------------------
Ejercicio 7.2. Demostrar o refutar datalladamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}

-- "javrodviv1"

lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
show " algunos P (map f []) = algunos (P ∘ f) []" by simp
next
fix a xs
assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
have "algunos P (map f (a # xs)) = ((P (f a)) ∨ algunos P (map f xs))" by simp
also have " ... = (((P ∘ f) a) ∨ algunos (P ∘ f) xs)" using HI by simp
finally show " algunos P (map f (a # xs)) = algunos (P ∘ f) (a # xs)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 8.1. Demostrar o refutar automáticamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 8.2. Demostrar o refutar detalladamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}

lemma algunos_append:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 9.1. Demostrar o refutar automáticamente
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}

lemma "algunos P (rev xs) = algunos P xs"
oops

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

lemma "algunos P (rev xs) = algunos P xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 10. Encontrar un término no trivial Z tal que sea cierta la
siguiente ecuación:
algunos (λx. P x ∨ Q x) xs = Z
y demostrar la equivalencia de forma automática y detallada.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 11.1. Demostrar o refutar automáticamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 11.2. Demostrar o refutar datalladamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}

lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 12. Definir la funcion primitiva recursiva
estaEn :: 'a ⇒ 'a list ⇒ 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
---------------------------------------------------------------------
*}

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x xs = undefined"

text {*
---------------------------------------------------------------------
Ejercicio 13. Expresar la relación existente entre estaEn y algunos.
Demostrar dicha relación de forma automática y detallada.
---------------------------------------------------------------------
*}

text {*
---------------------------------------------------------------------
Ejercicio 14. Definir la función primitiva recursiva
sinDuplicados :: 'a list ⇒ 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
---------------------------------------------------------------------
*}

fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados xs = undefined"

text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la función primitiva recursiva
borraDuplicados :: 'a list ⇒ 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.
---------------------------------------------------------------------
*}

fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados xs = undefined"

text {*
---------------------------------------------------------------------
Ejercicio 16.1. Demostrar o refutar automáticamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}

lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 16.2. Demostrar o refutar detalladamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}

lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 17.1. Demostrar o refutar automáticamente
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
*}

lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
oops

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

lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18.1. Demostrar o refutar automáticamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma "sinDuplicados (borraDuplicados xs)"
oops

text {*
---------------------------------------------------------------------
Ejercicio 18.2. Demostrar o refutar detalladamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}

lemma sinDuplicados_borraDuplicados:
"sinDuplicados (borraDuplicados xs)"
oops

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

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

end
</source>

Relación 4

2014-11-14T17:09:15Z

Javrodviv1:

<source lang="isar">
header {* R4: Cons inverso *}

theory R4
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir recursivamente la función
snoc :: "'a list ⇒ 'a ⇒ '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 @.
---------------------------------------------------------------------
*}

-- "davoremar,javrodviv1"

fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
"snoc [] a = [a]"
| "snoc (x#xs) a = x # (snoc xs a)"

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

-- "davoremar,javrodviv1"

lemma "snoc xs a = xs @ [a]"
by (induct xs) auto

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

-- "davoremar,javrodviv1"

lemma snoc_append: "snoc xs a = xs @ [a]"
proof (induct xs)
show "snoc [] a = [] @ [a]" by simp
next
fix x xs
assume HI: "snoc xs a = xs @ [a]"
have "snoc (x#xs) a = x # (snoc xs a)" by simp
also have "... = x # (xs @ [a])" using HI by simp
finally show "snoc (x#xs) a = (x#xs) @ [a]" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 4. Demostrar automáticamente el siguiente lema
rev (x # xs) = snoc (rev xs) x"
---------------------------------------------------------------------
*}

-- "davoremar,javrodviv1"

lemma "rev (x # xs) = snoc (rev xs) x"
by (auto simp add: snoc_append)

text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar detalladamente el siguiente lema
rev (x # xs) = snoc (rev xs) x"
---------------------------------------------------------------------
*}

-- "davoremar,javrodviv1"

lemma "rev (x # xs) = snoc (rev xs) x"
proof -
have "rev (x # xs) = (rev xs) @ [x]" by simp
also have "... = snoc (rev xs) x" by (simp add:snoc_append)
finally show "rev (x # xs) = snoc (rev xs) x" by simp
qed

end
</source>

Relación 3

2014-11-13T11:50:30Z

Javrodviv1:

<source lang="isar">
header {* R3: Razonamiento sobre programas en Isabelle/HOL *}

theory R3
imports Main
begin

text {* ---------------------------------------------------------------
Ejercicio 1. Definir la función
sumaImpares :: nat ⇒ nat
tal que (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 5 = 25
------------------------------------------------------------------ *}
(* Pedrosrei: como no veo a nadie animarse pongo las dos primeras a ver si sirve de ayuda: *)

-- "davoremar juacorvic jeshorcob domcadgom javrodviv1"

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2*n+1) + sumaImpares n"

-- "marnajgom"
fun sumaImpares2 :: "nat ⇒ nat" where
"sumaImpares2 0 = 0"
| "sumaImpares2 (Suc n) = (Suc n)+ n + sumaImpares2 n"

-- "jeshorcob"
fun sumaImpares3 :: "nat ⇒ nat" where
"sumaImpares3 n = foldr (λ x y. y + (2 * x) + 1) (upt 0 n) 0"

(* Esta definición en principio es más eficiente pero a la hora de
demostrar se complica todo. Estaría bien si en clase pudieramos
explicar si se puede demostrar el lema usando esta definición de
manera sencilla o explicar un poco cómo iría la prueba *)

value "sumaImpares 5" -- "= 25"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
sumaImpares n = n*n
------------------------------------------------------------------- *}
(* Pedrosrei: lo dejo de menos a más estructurado *)

lemma "sumaImpares n = n*n"
apply (induct n) apply auto
done

-- "davoremar juacorvic jeshorcob"

lemma "sumaImpares n = n*n"
by (induct n) auto

lemma "sumaImpares n = n*n"
proof (induct n)
show "sumaImpares 0 = 0 * 0" by simp
next
fix n
assume HI: "sumaImpares n = n * n"
thus "sumaImpares (Suc n) = Suc n * Suc n" by simp
qed

-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"

lemma "sumaImpares n = n*n"
proof (induct n)
show "sumaImpares 0 = 0 * 0" by simp
next
fix n
assume HI: "sumaImpares n = n*n"
have "sumaImpares (Suc n) = sumaImpares n + (2*n + 1)" by simp
also have "... = n*n + 2*n + 1" using HI by simp
also have "... = (n + 1) * (n + 1)" by simp
finally show "sumaImpares (Suc n) = Suc n * Suc n" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
sumaPotenciasDeDosMasUno :: nat ⇒ nat
tal que
(sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.
Por ejemplo,
sumaPotenciasDeDosMasUno 3 = 16
------------------------------------------------------------------ *}

-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno 0 = 2"
| "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n) + sumaPotenciasDeDosMasUno n"

value "sumaPotenciasDeDosMasUno 3" -- "= 16"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

-- "davoremar juacorvic jeshorcob"

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
by (induct n) auto

-- "jeshorcob"

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
show "sumaPotenciasDeDosMasUno 0 = 2^(0+1)" by simp
next
fix n
assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
thus "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n + 1)" by simp
qed

-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
proof (induct n)
show "sumaPotenciasDeDosMasUno 0 = 2^(0+1)" by simp
next
fix n
assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)"
have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(Suc n)" by simp
also have "... = 2^(n+1) + 2^(Suc n)" using HI by simp
also have "... = 2^(Suc n + 1)" by simp
finally show "sumaPotenciasDeDosMasUno (Suc n) = 2^(Suc n + 1)" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
copia :: nat ⇒ 'a ⇒ 'a list
tal que (copia n x) es la lista formado por n copias del elemento
x. Por ejemplo,
copia 3 x = [x,x,x]
------------------------------------------------------------------ *}

-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia 0 x = []"
| "copia (Suc n) x = x # copia n x"

value "copia 3 x" -- "= [x,x,x]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de xs cumplen
la propiedad p. Por ejemplo,
todos (λx. x>(1::nat)) [2,6,4] = True
todos (λx. x>(2::nat)) [2,6,4] = False
Nota: La conjunción se representa por ∧
----------------------------------------------------------------- *}

-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
| "todos p (x#xs) = ((p x) ∧ (todos p xs))"

(* jeshorcob: me gustaría saber por qué es necesario poner el paréntesis en la definición(2) *)
(*Pedrosrei: porque aunque están predefinidas las prioridades entre la suma y el producto en
los cuerpos y anillos más comunes, la conjunción y la igualdad no tienen definida esa prioridad*)

value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"
value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar que todos los elementos de (copia n x) son
iguales a x.
------------------------------------------------------------------- *}

-- "davoremar juacorvic jeshorcob"

lemma "todos (λy. y=x) (copia n x)"
by (induct n) auto

-- "davoremar marnajgom jeshorcob domcadgom javrodviv1"

lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
show "todos (λy. y=x) (copia 0 x)" by simp
next
fix n
assume HI: "todos (λy. y=x) (copia n x)"
have "todos (λy. y=x) (copia (Suc n) x) = todos (λy. y=x) (x#(copia n x))" by simp
also have "... = todos (λy. y=x) (copia n x)" by simp
finally show "todos (λy. y=x) (copia (Suc n) x)" using HI by simp
qed

-- "juacorvic jeshorcob"
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
show "todos (λy. y=x) (copia 0 x)" by simp
fix n
assume HI: "todos (λy. y=x) (copia n x)"
thus "todos (λy. y=x) (copia (Suc n) x)" by simp
qed

-- "juacorvic"
lemma "todos (λy. y=x) (copia n x)"
proof (induct n)
show "todos (λy. y=x) (copia 0 x)" by simp
next
fix n
assume HI: "todos (λy. y=x) (copia n x)"
have "todos (λy. y=x) (copia (Suc n) x) = todos (λy. y=x) (x # (copia n x))" by simp
also have "...=todos (λy. y=x)[x]" using HI by simp
finally show "todos (λy. y=x) (copia (Suc n) x)" using HI by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ *}

-- "davoremar juacorvic marnajgom jeshorcob domcadgom javrodviv1"

fun factR :: "nat ⇒ nat" where
"factR 0 = 1"
| "factR (Suc n) = (Suc n) * factR n"

value "factR 4" -- "= 24"

text {* ---------------------------------------------------------------
Ejercicio 9. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
------------------------------------------------------------------- *}

fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (Suc n)*x"

fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"

value "factI 4" -- "= 24"

-- "davoremar jeshorcob domcadgom"
lemma fact1: "factI' n x = x* factR n"
by (induct n arbitrary: x) auto

(*juacorvic: ¿Por que tenemos que indicar arbitrary:x? *)
(*Pedrosrei: no tienes que hacerlo como resulta de mi ejemplo o las
correcciones que he indicado en el tuyo. En este caso concreto totalmente
automatizado es porque posees dos variables y tienes que decirle
qué hacer con cada una. En una haces la inducción pero la otra la dejas sin
tocar, o como solemos decir: "sea un x cualquiera..."
*)
-- "davoremar jeshorcob domcadgom"

lemma fact: "factI' n x = x * factR n"
proof (induct n arbitrary: x)
show "⋀x. factI' 0 x = x * factR 0" by simp
next
fix n x
assume HI: "⋀x. factI' n x = x * factR n"
have "factI' (Suc n) x = factI' n (Suc n)*x" by simp
also have "... = x * factI' n (Suc n)" by simp
also have "... = x * ((Suc n) * factR n)" using HI by simp
also have "... = x * factR (Suc n)" by simp
finally show "factI' (Suc n) x = x * factR (Suc n)" by simp
qed

(* marnajgom: no entiendo el paso "also have "... = x * factI'
n (Suc n)" by simp" ¿Por qué no sacas fuera (Suc n)*x, sólo sacas
x?*)

(* Pedrosrei: También podemos prescindir de arbitrary x *)

lemma fact2: "factI' n x = x * factR n"
proof (induct n)
show "factI' 0 x = x * factR 0" by simp
next
fix n
assume HI: "factI' n x = x * factR n"
show "factI' (Suc n) x = x * factR (Suc n)"
proof -
have "factI' (Suc n) x = (factI' n (Suc n))*x" by simp
also have " ... = ((Suc n) * factR n) * x" using HI fact by simp
-- "Si usamos auto: finally show ?thesis by auto "
also have " ... = x * factR (Suc n)" by simp
finally show ?thesis .
qed
qed

(*Pedrosrei: no resuelve finally debido a la conjunción grande que emplea isabelle para
indicarte un "para todo de cualquier conjunto" (en realidad es la conjunción de conjuntos, creo recordar).
Si quieres poner un para todo recurre a ! ó \forall. Si sólo has puesto lo que te ha indicado la máquina,
quería indicarte un valor cualquiera, vamos, lo que fijas con "arbitrary".

Sólo tienes que eliminar los ⋀ de la prueba
y añadirle un paso intermedio con la regla adecuada (usa find_theorem y el nombre que crees
que tendrá) entre el also have último y el finally
para que vea la igualdad de derecha a izquierda y listo. También puedes emplear "by arith" para
estas cosas tan sencillas y no tener que irte a la regla exacta de la aritmética (que no siempre
es fácil).

*)
-- "juacorvic" (* Se intenta demostración en sentido inverso: '' x * factR n = factI' n x ''
No resuelve finally *)

lemma fact: " x * factR n = factI' n x "
proof (induct n)
show "⋀x. x * factR 0 = factI' 0 x" by simp
next
fix n
assume HI: "⋀x. x * factR n = factI' n x "
have "x * factR (Suc n) = x * (factR n * (Suc n))" by simp
also have "... = x * ((Suc n) * factR n)" by simp
also have "... = x * (factI' n (Suc n))" using HI by simp
also have "... = factI' (Suc n) x" by simp
finally show " x * factR (Suc n) = factI' (Suc n) x" by simp
qed
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
factI n = factR n
------------------------------------------------------------------- *}

-- "davoremar juacorvic jeshorcob domcadgom"

corollary "factI n = factR n"
by (simp add: fact)

-- "juacorvic"

corollary "factI n = factR n"
proof -
show "factI n = factR n" by (simp add:fact)
qed

-- "davoremar juacorvic jeshorcob"

corollary "factI n = factR n"
proof -
have "factI n = factI' n 1" by simp
also have "... = 1 * factR n" by (simp add: fact)
finally show "factI n = factR n" by simp
qed

-- "marnajgom javrodviv1"
corollary "factI n = factR n"
proof (induct n)
show "factI 0 = factR 0" by simp
next
fix n
assume HI:"factI n = factR n"
have "factI (Suc n) = factI' (Suc n) 1" by simp
also have "... = factI' n (Suc n)*1" by simp
also have "... = (Suc n)*1 * factR n" using fact by simp
also have "... = (Suc n) * factR n" by simp
finally show "factI (Suc n) = factR (Suc n)" by simp
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Definir, recursivamente y sin usar (@), la función
amplia :: 'a list ⇒ 'a ⇒ 'a list
tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
final de la lista xs. Por ejemplo,
amplia [d,a] t = [d,a,t]
------------------------------------------------------------------ *}

-- "davoremar marnajgom jeshorcob domcadgom javrodviv1"

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia [] y = [y]"
| "amplia (x#xs) y = x # (amplia xs y)"

value "amplia [d,a] t" -- "= [d,a,t]"

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

-- "davoremar"

lemma "amplia xs y = xs @ [y]"
by (induct xs) auto

-- "juacorvic" (*Añado esquema intermedio*)
lemma "amplia xs y = xs @ [y]"
proof (induct xs)
show "amplia [] y = [] @ [y]" by simp
next
fix a xs
assume HI: "amplia xs y = xs @ [y]"
thus "amplia (a # xs) y = (a # xs) @ [y]" by simp
qed

-- "davoremar marnajgom jeshorcob domcadgom javrodviv1"

lemma "amplia xs y = xs @ [y]"
proof (induct xs)
show "amplia [] y = [] @ [y]" by simp
next
fix x xs
assume HI: "amplia xs y = xs @ [y]"
have "amplia (x#xs) y = x # amplia xs y" by simp
also have "... = x # (xs @ [y])" using HI by simp
also have "... = (x#xs) @ [y]" by simp (*Pedrosrei: prescindible *)
finally show "amplia (x#xs) y = (x#xs) @ [y]" by simp
qed

(*Pedrosrei: las variables son mudas. Da igual 'a' que 'x', del mismo modo que da igual en papel el nombre de
la incógnita. Puedes usar 'incognitabonita' y sigue siendo lo mismo *)
-- "juacorvic" (* Demostración idéntica a 'davoremar' pero el sistema me sugirió usar 'a' en vez de 'x' *)
lemma "amplia xs y = xs @ [y]"
proof (induct xs)
show "amplia [] y = [] @ [y]" by simp
next
fix a xs
assume HI: "amplia xs y = xs @ [y]"
have "amplia (a # xs) y = a # (amplia xs y) " by simp
also have "... = a # (xs @ [y])" using HI by simp
also have "... = (a # xs) @ [y]" by simp
finally show "amplia (a # xs) y = (a # xs) @ [y]" by simp
qed

end
</source>

Relación 1

2014-11-02T09:22:36Z

Javrodviv1:

<source lang="isar">
header {* R1: Programación funcional en Isabelle *}

theory R1
imports Main
begin

text {* ----------------------------------------------------------------
Ejercicio 0. Definir, por recursión, la función
factorial :: nat ⇒ nat
tal que (factorial n) es el factorial de n. Por ejemplo,
factorial 4 = 24
------------------------------------------------------------------- *}

-- "jeshorcob","javrodviv1"
fun factorial :: "nat ⇒ nat" where
"factorial 0 = 1 "
|"factorial (Suc m) = (Suc m) * factorial m"

value "factorial 4" -- "24"

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

-- "jeshorcob","javrodviv1"
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
|"longitud (x#xs) = 1 + longitud xs"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

-- "jeshorcob","javrodviv1"
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

-- "jeshorcob"
fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
|"inversa (x#xs) = (inversa xs) @ [x]"

--"javrodviv1"
fun inversa2 :: "'a list ⇒ 'a list" where
"inversa2 [] = []"
| "inversa2 xs = (last xs)#(inversa2 (butlast xs))"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 4. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

-- "jeshorcob","javrodviv1"
fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
|"repite (Suc m) x = x # (repite m x)"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

-- "jeshorcob","javrodviv1"
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
|"conc (x#xs) ys = x#(conc xs ys)"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

-- "jeshorcob","javrodviv1"
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge _ [] = []"
|"coge 0 xs = []"
|"coge (Suc m) (x#xs) = x#(coge m xs)"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

-- "jeshorcob","javrodviv1"
fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina _ [] = []"
|"elimina 0 xs = xs"
|"elimina (Suc m) (x#xs) = elimina m xs"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

-- "jeshorcob","javrodviv1"
fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
|"esVacia _ = False"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

-- "jeshorcob"
fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
|"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

-- "jeshorcob"
fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 10. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

-- "jeshorcob","javrodviv1"
fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
|"sum (x#xs) = x + sum xs"

-- "jeshorcob"
fun sum2 :: "nat list ⇒ nat" where
"sum2 xs = foldr (op +) xs 0"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

-- "jeshorcob","javrodviv1"
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
|"map f (x#xs) = (f x)#(map f xs)"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

end
</source>