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

Relación 8

2014-12-11T07:32:07Z

Domcadgom:

<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 jeshorcob,davoremar, domcadgom"
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"

--"davoremar"
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. *)

--"jeshorcob, domcadgom"
fun pr1 :: "arbol => nat" where
"pr1 H = 0"
|"pr1 (N i d) = Suc(max (pr1 i) (pr1 d))"

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 jeshorcob,davoremar, domcadgom"
fun abc :: "nat ⇒ arbol" where
"abc 0 = H"
| "abc (Suc n) = N (abc n) (abc n)"

--"jeshorcob" (*¿Pudiera ser que esta sea más rápida?*)
fun abc1 :: "nat ⇒ arbol" where
"abc1 0 = H"
|"abc1 (Suc n) = (let a = abc1 n in N a a)"

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))"

--"jeshorcob,davoremar, domcadgom"
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
|"es_abc f (N i d) = (f i = f d ∧ es_abc f i ∧ es_abc f d)"

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

(*jeshorcob: creo que tengo una demostración mas elegante tan
sólo hace falta encontrar la relacion entre hojas y profundidad*)

--"jeshorcob"
lemma a1:
assumes "es_abc hojas a"
shows "hojas a = 2^(pr1 a)"
using assms by (induct a, simp_all)

--"jeshorcob"
lemma cpr1_chojas: "es_abc pr1 a = es_abc hojas a"
by (induct a, auto simp add: a1)

(*jeshorcob: esta la detallada*)
--"jeshorcob"
lemma "es_abc pr1 a = es_abc hojas a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i d
assume h1: "?P i"
assume h2: "?P d"
have "es_abc pr1 (N i d) =
(pr1 i = pr1 d ∧ es_abc pr1 i ∧ es_abc pr1 d )" by simp
also have "... = (pr1 i = pr1 d ∧ es_abc hojas i ∧ es_abc hojas d)"
using h1 and h2 by simp
also have "... = (hojas i = hojas d
∧ es_abc hojas i ∧ es_abc hojas d)" using a1 by auto
also have "... = es_abc hojas (N i d)" by simp
finally show "?P (N i d)" by simp
qed

-- "domcadgom"
lemma aux1: "(es_abc profundidad a) ⟹ (hojas a) = (2^(profundidad a))"
by (induct a,simp_all)

lemma completo1: "(es_abc (profundidad) a) = (es_abc (hojas) a)"
proof (induct a, simp)
fix a1 :: arbol and a2 :: arbol
assume a1: "es_abc profundidad a1 = es_abc hojas a1"
assume a2: "es_abc profundidad a2 = es_abc hojas a2"
have "es_abc profundidad a2 ∧ es_abc profundidad a1 ⟶ es_abc profundidad
(N a1 a2) = es_abc hojas (N a1 a2)" using a1 a2 by (simp add: aux1)
thus "es_abc profundidad (N a1 a2) = es_abc hojas (N a1 a2)"
using a1 a2 es_abc.simps(2) by blast
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

(*jeshorcob: aquí similar*)

--"jeshorcob"
lemma a2:
assumes "es_abc size a"
shows "hojas a = (size a) + 1"
using assms by (induct a, simp_all)

--"jeshorcob"
lemma chojas_cnodos: "es_abc hojas a = es_abc size a"
by (induct a, auto simp add: a2)

--"jeshorcob"
lemma "es_abc hojas a = es_abc size a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i d
assume h1: "?P i"
assume h2: "?P d"
have "es_abc hojas (N i d) =
(hojas i = hojas d ∧ es_abc hojas i ∧ es_abc hojas d )" by simp
also have "... = (hojas i = hojas d ∧ es_abc size i ∧ es_abc size d)"
using h1 and h2 by simp
also have "... = (size i = size d
∧ es_abc size i ∧ es_abc size d)" using a2 by auto
also have "... = es_abc size (N i d)" by simp
finally show "?P (N i d)" by simp
qed

--"domcadgom"

lemma aux2: "(es_abc size a) ⟹ ((hojas a) = ((size a) +1))"
by (induct a, simp_all)

lemma completo2: "es_abc hojas a = es_abc (size) a"
proof (induct a, simp)
fix a1 :: arbol and a2 :: arbol
assume a1: "es_abc hojas a1 = es_abc size a1"
assume a2: "es_abc hojas a2 = es_abc size a2"
hence "es_abc size a2 ∧ es_abc size a1 ⟶
es_abc hojas (N a1 a2) = es_abc size (N a1 a2)" using a1 by (simp add: aux2)
thus "es_abc hojas (N a1 a2) = es_abc size (N a1 a2)"
using a1 a2 es_abc.simps(2) by blast
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

(*jeshorcob: sale directo como corolario de los anteriores*)
--"jeshorcob"
lemma "es_abc pr1 a = es_abc size a"
using cpr1_chojas and chojas_cnodos by simp_all

--"domcadgom"

corollary completo3: "es_abc profundidad a = es_abc size a"
using completo1 completo2 by simp

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

--"jeshorcob,davoremar, domcadgom"
lemma "es_abc f (abc n)"
by (induct n, simp_all)

--"jeshorcob"
lemma "es_abc f (abc n)" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix n assume h: "?P n"
have "es_abc f (abc (Suc n)) = es_abc f (N (abc n) (abc n))" by simp
also have "... = (f (abc n) = f (abc n) ∧
es_abc f (abc n) ∧ es_abc f (abc n))" by simp
also have "... = True" using h by simp
finally show "?P (Suc n)" by simp
qed

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

--"jeshorcob"
lemma "es_abc pr1 a ⟹ (a = abc (pr1 a))"
by (induct a, simp_all)

--"davoremar, domcadgom"
lemma "es_abc profundidad a ⟹ (a = abc (profundidad a))"
by (induct a, simp_all)

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

(*jeshorcob: usando size en lugar de nodos, se encuentra el
mismo contraejemplo*)
--"jeshorcob, domcadgom"
lemma "es_abc f = es_abc size"
quickcheck
(*
el contraejemplo es:

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

Evaluated terms:
es_abc f x = True
es_abc size x = False
*)

--"davoremar"
lemma "es_abc f t = es_abc size t"
quickcheck
oops

end
</source>

Relación 8

2014-12-10T21:35:53Z

Domcadgom:

<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 jeshorcob,davoremar, domcadgom"
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"

--"davoremar"
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. *)

--"jeshorcob, domcadgom"
fun pr1 :: "arbol => nat" where
"pr1 H = 0"
|"pr1 (N i d) = Suc(max (pr1 i) (pr1 d))"

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 jeshorcob,davoremar, domcadgom"
fun abc :: "nat ⇒ arbol" where
"abc 0 = H"
| "abc (Suc n) = N (abc n) (abc n)"

--"jeshorcob" (*¿Pudiera ser que esta sea más rápida?*)
fun abc1 :: "nat ⇒ arbol" where
"abc1 0 = H"
|"abc1 (Suc n) = (let a = abc1 n in N a a)"

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))"

--"jeshorcob,davoremar, domcadgom"
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
|"es_abc f (N i d) = (f i = f d ∧ es_abc f i ∧ es_abc f d)"

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

(*jeshorcob: creo que tengo una demostración mas elegante tan
sólo hace falta encontrar la relacion entre hojas y profundidad*)

--"jeshorcob"
lemma a1:
assumes "es_abc hojas a"
shows "hojas a = 2^(pr1 a)"
using assms by (induct a, simp_all)

--"jeshorcob"
lemma cpr1_chojas: "es_abc pr1 a = es_abc hojas a"
by (induct a, auto simp add: a1)

(*jeshorcob: esta la detallada*)
--"jeshorcob"
lemma "es_abc pr1 a = es_abc hojas a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i d
assume h1: "?P i"
assume h2: "?P d"
have "es_abc pr1 (N i d) =
(pr1 i = pr1 d ∧ es_abc pr1 i ∧ es_abc pr1 d )" by simp
also have "... = (pr1 i = pr1 d ∧ es_abc hojas i ∧ es_abc hojas d)"
using h1 and h2 by simp
also have "... = (hojas i = hojas d
∧ es_abc hojas i ∧ es_abc hojas d)" using a1 by auto
also have "... = es_abc hojas (N i d)" by simp
finally show "?P (N i d)" by simp
qed

-- "domcadgom"
lemma aux1: "(es_abc profundidad a) ⟹ (hojas a) = (2^(profundidad a))"
by (induct a,simp_all)

lemma completo1: "(es_abc (profundidad) a) = (es_abc (hojas) a)"
proof (induct a, simp)
fix a1 :: arbol and a2 :: arbol
assume a1: "es_abc profundidad a1 = es_abc hojas a1"
assume a2: "es_abc profundidad a1 = es_abc hojas a1"
assume a3: "es_abc profundidad a2 = es_abc hojas a2"
assume a4: "es_abc profundidad a2 = es_abc hojas a2"
have "es_abc profundidad a2 ∧ es_abc profundidad a1 ⟶ es_abc profundidad
(N a1 a2) = es_abc hojas (N a1 a2)" using a1 a3 by (simp add: aux1)
thus "es_abc profundidad (N a1 a2) = es_abc hojas (N a1 a2)"
using a2 a4 es_abc.simps(2) by blast
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

(*jeshorcob: aquí similar*)

--"jeshorcob"
lemma a2:
assumes "es_abc size a"
shows "hojas a = (size a) + 1"
using assms by (induct a, simp_all)

--"jeshorcob"
lemma chojas_cnodos: "es_abc hojas a = es_abc size a"
by (induct a, auto simp add: a2)

--"jeshorcob"
lemma "es_abc hojas a = es_abc size a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i d
assume h1: "?P i"
assume h2: "?P d"
have "es_abc hojas (N i d) =
(hojas i = hojas d ∧ es_abc hojas i ∧ es_abc hojas d )" by simp
also have "... = (hojas i = hojas d ∧ es_abc size i ∧ es_abc size d)"
using h1 and h2 by simp
also have "... = (size i = size d
∧ es_abc size i ∧ es_abc size d)" using a2 by auto
also have "... = es_abc size (N i d)" by simp
finally show "?P (N i d)" by simp
qed

--"domcadgom"

lemma aux2: "(es_abc size a) ⟹ ((hojas a) = ((size a) +1))"
by (induct a, simp_all)

lemma completo2: "es_abc hojas a = es_abc (size) a"
proof (induct a, simp)
fix a1 :: arbol and a2 :: arbol
assume a1: "es_abc hojas a1 = es_abc size a1"
assume a2: "es_abc hojas a2 = es_abc size a2"
hence "es_abc size a2 ∧ es_abc size a1 ⟶
es_abc hojas (N a1 a2) = es_abc size (N a1 a2)" using a1 by (simp add: aux2)
thus "es_abc hojas (N a1 a2) = es_abc size (N a1 a2)"
using a1 a2 es_abc.simps(2) by blast
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

(*jeshorcob: sale directo como corolario de los anteriores*)
--"jeshorcob"
lemma "es_abc pr1 a = es_abc size a"
using cpr1_chojas and chojas_cnodos by simp_all

--"domcadgom"

corollary completo3: "es_abc profundidad a = es_abc size a"
using completo1 completo2 by simp

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

--"jeshorcob,davoremar, domcadgom"
lemma "es_abc f (abc n)"
by (induct n, simp_all)

--"jeshorcob"
lemma "es_abc f (abc n)" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix n assume h: "?P n"
have "es_abc f (abc (Suc n)) = es_abc f (N (abc n) (abc n))" by simp
also have "... = (f (abc n) = f (abc n) ∧
es_abc f (abc n) ∧ es_abc f (abc n))" by simp
also have "... = True" using h by simp
finally show "?P (Suc n)" by simp
qed

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

--"jeshorcob"
lemma "es_abc pr1 a ⟹ (a = abc (pr1 a))"
by (induct a, simp_all)

--"davoremar, domcadgom"
lemma "es_abc profundidad a ⟹ (a = abc (profundidad a))"
by (induct a, simp_all)

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

(*jeshorcob: usando size en lugar de nodos, se encuentra el
mismo contraejemplo*)
--"jeshorcob, domcadgom"
lemma "es_abc f = es_abc size"
quickcheck
(*
el contraejemplo es:

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

Evaluated terms:
es_abc f x = True
es_abc size x = False
*)

--"davoremar"
lemma "es_abc f t = es_abc size t"
quickcheck
oops

end
</source>

Relación 8

2014-12-10T21:32:45Z

Domcadgom:

<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 jeshorcob,davoremar, domcadgom"
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"

--"davoremar"
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. *)

--"jeshorcob, domcadgom"
fun pr1 :: "arbol => nat" where
"pr1 H = 0"
|"pr1 (N i d) = Suc(max (pr1 i) (pr1 d))"

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 jeshorcob,davoremar, domcadgom"
fun abc :: "nat ⇒ arbol" where
"abc 0 = H"
| "abc (Suc n) = N (abc n) (abc n)"

--"jeshorcob" (*¿Pudiera ser que esta sea más rápida?*)
fun abc1 :: "nat ⇒ arbol" where
"abc1 0 = H"
|"abc1 (Suc n) = (let a = abc1 n in N a a)"

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))"

--"jeshorcob,davoremar, domcadgom"
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
|"es_abc f (N i d) = (f i = f d ∧ es_abc f i ∧ es_abc f d)"

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

(*jeshorcob: creo que tengo una demostración mas elegante tan
sólo hace falta encontrar la relacion entre hojas y profundidad*)

--"jeshorcob"
lemma a1:
assumes "es_abc hojas a"
shows "hojas a = 2^(pr1 a)"
using assms by (induct a, simp_all)

--"jeshorcob"
lemma cpr1_chojas: "es_abc pr1 a = es_abc hojas a"
by (induct a, auto simp add: a1)

(*jeshorcob: esta la detallada*)
--"jeshorcob"
lemma "es_abc pr1 a = es_abc hojas a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i d
assume h1: "?P i"
assume h2: "?P d"
have "es_abc pr1 (N i d) =
(pr1 i = pr1 d ∧ es_abc pr1 i ∧ es_abc pr1 d )" by simp
also have "... = (pr1 i = pr1 d ∧ es_abc hojas i ∧ es_abc hojas d)"
using h1 and h2 by simp
also have "... = (hojas i = hojas d
∧ es_abc hojas i ∧ es_abc hojas d)" using a1 by auto
also have "... = es_abc hojas (N i d)" by simp
finally show "?P (N i d)" by simp
qed

-- "domcadgom"
lemma aux1: "(es_abc profundidad a) ⟹ (hojas a) = (2^(profundidad a))"
by (induct a,simp_all)

lemma completo1: "(es_abc (profundidad) a) = (es_abc (hojas) a)"
proof (induct a, simp)
fix a1 :: arbol and a2 :: arbol
assume a1: "es_abc profundidad a1 = es_abc hojas a1"
assume a2: "es_abc profundidad a1 = es_abc hojas a1"
assume a3: "es_abc profundidad a2 = es_abc hojas a2"
assume a4: "es_abc profundidad a2 = es_abc hojas a2"
have "es_abc profundidad a2 ∧ es_abc profundidad a1 ⟶ es_abc profundidad
(N a1 a2) = es_abc hojas (N a1 a2)" using a1 a3 by (simp add: aux1)
thus "es_abc profundidad (N a1 a2) = es_abc hojas (N a1 a2)"
using a2 a4 es_abc.simps(2) by blast
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

(*jeshorcob: aquí similar*)

--"jeshorcob"
lemma a2:
assumes "es_abc size a"
shows "hojas a = (size a) + 1"
using assms by (induct a, simp_all)

--"jeshorcob"
lemma chojas_cnodos: "es_abc hojas a = es_abc size a"
by (induct a, auto simp add: a2)

--"jeshorcob"
lemma "es_abc hojas a = es_abc size a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i d
assume h1: "?P i"
assume h2: "?P d"
have "es_abc hojas (N i d) =
(hojas i = hojas d ∧ es_abc hojas i ∧ es_abc hojas d )" by simp
also have "... = (hojas i = hojas d ∧ es_abc size i ∧ es_abc size d)"
using h1 and h2 by simp
also have "... = (size i = size d
∧ es_abc size i ∧ es_abc size d)" using a2 by auto
also have "... = es_abc size (N i d)" by simp
finally show "?P (N i d)" by simp
qed

--"domcadgom"

lemma aux2: "(es_abc size a) ⟹ ((hojas a) = ((size a) +1))"
by (induct a, simp_all)

lemma completo2: "es_abc hojas a = es_abc (size) a"
proof (induct a, simp)
fix a1 :: arbol and a2 :: arbol
assume a1: "es_abc hojas a1 = es_abc size a1"
assume a2: "es_abc hojas a2 = es_abc size a2"
hence "es_abc hojas a2 ∧ es_abc hojas a1 ⟶
es_abc hojas (N a1 a2) = es_abc size (N a1 a2)" using a1 aux2 by auto
thus "es_abc hojas (N a1 a2) = es_abc size (N a1 a2)"
using a1 a2 es_abc.simps(2) by blast
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

(*jeshorcob: sale directo como corolario de los anteriores*)
--"jeshorcob"
lemma "es_abc pr1 a = es_abc size a"
using cpr1_chojas and chojas_cnodos by simp_all

--"domcadgom"

corollary completo3: "es_abc profundidad a = es_abc size a"
using completo1 completo2 by simp

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

--"jeshorcob,davoremar, domcadgom"
lemma "es_abc f (abc n)"
by (induct n, simp_all)

--"jeshorcob"
lemma "es_abc f (abc n)" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix n assume h: "?P n"
have "es_abc f (abc (Suc n)) = es_abc f (N (abc n) (abc n))" by simp
also have "... = (f (abc n) = f (abc n) ∧
es_abc f (abc n) ∧ es_abc f (abc n))" by simp
also have "... = True" using h by simp
finally show "?P (Suc n)" by simp
qed

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

--"jeshorcob"
lemma "es_abc pr1 a ⟹ (a = abc (pr1 a))"
by (induct a, simp_all)

--"davoremar, domcadgom"
lemma "es_abc profundidad a ⟹ (a = abc (profundidad a))"
by (induct a, simp_all)

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

(*jeshorcob: usando size en lugar de nodos, se encuentra el
mismo contraejemplo*)
--"jeshorcob, domcadgom"
lemma "es_abc f = es_abc size"
quickcheck
(*
el contraejemplo es:

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

Evaluated terms:
es_abc f x = True
es_abc size x = False
*)

--"davoremar"
lemma "es_abc f t = es_abc size t"
quickcheck
oops

end
</source>

Relación 7

2014-12-04T11:18:17Z

Domcadgom:

<source lang="isar">
header {* R7: Recorridos de árboles *}

theory R7
imports Main
begin

text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que tiene información en los nodos y en las hojas.
Por ejemplo, el árbol
e
/ \
/ \
c g
/ \ / \
a d f h
se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
---------------------------------------------------------------------
*}

datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol"

value "N e (N c (H a) (H d)) (N g (H f) (H h))"

text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
preOrden :: "'a arbol ⇒ 'a list"
tal que (preOrden a) es el recorrido pre orden del árbol a. Por
ejemplo,
preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom"
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden (H x) = [x]"
|"preOrden (N x yy zz) = x#(preOrden yy @ preOrden zz)"

value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [e,c,a,d,g,f,h]" -- "True"

value "preOrden (N e (N c (N a1 (H a2) (H a3)) (H d)) (N g (H f) (H h)))
= [e, c, a1, a2, a3, d, g, f, h]" -- "True"

text {*
---------------------------------------------------------------------
Ejercicio 3. Definir la función
postOrden :: "'a arbol ⇒ 'a list"
tal que (postOrden a) es el recorrido post orden del árbol a. Por
ejemplo,
postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,d,c,f,h,g,e]
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
fun postOrden :: "'a arbol ⇒ 'a list" where
"postOrden (H x) = [x]"
|"postOrden (N x yy zz)= postOrden yy @ postOrden zz @ [x]"

value "postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,d,c,f,h,g,e]" -- "True"

text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
inOrden :: "'a arbol ⇒ 'a list"
tal que (inOrden a) es el recorrido in orden del árbol a. Por
ejemplo,
inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
fun inOrden :: "'a arbol ⇒ 'a list" where
"inOrden (H x) = [x]"
|"inOrden (N x yy zz) = inOrden yy @ [x] @ inOrden zz"

value "inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
= [a,c,d,e,f,g,h]" -- "True"

text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
espejo :: "'a arbol ⇒ 'a arbol"
tal que (espejo a) es la imagen especular del árbol a. Por ejemplo,
espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
= N e (N g (H h) (H f)) (N c (H d) (H a))
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
fun espejo :: "'a arbol ⇒ 'a arbol" where
"espejo (H x) = (H x)"
|"espejo (N x yy zz) = (N x (espejo zz) (espejo yy))"

value "espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
= N e (N g (H h) (H f)) (N c (H d) (H a))" -- "True"

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar que
preOrden (espejo a) = rev (postOrden a)
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,carvelcab"
lemma "preOrden (espejo a) = rev (postOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar,carvelcab"
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x yy zz
assume h1: "?P yy"
assume h2: "?P zz"
have "preOrden (espejo (N x yy zz))
= preOrden (N x (espejo zz) (espejo yy))" by simp
also have "... = x#(preOrden(espejo zz)@preOrden(espejo yy))" by simp
also have "... = x#rev(postOrden zz)@rev(postOrden yy)"
using h1 h2 by simp
also have "... = rev((postOrden yy)@(postOrden zz)@[x])" by simp
finally show "?P (N x yy zz)" by simp
qed

-- "juacorvic, domcadgom (Igual pero un paso más. Se usan variables sugeridas)"
lemma "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
fix a
show "?P (H a)" by simp
next
fix a1 a2 a3
assume h1: "?P a2"
assume h2: "?P a3"
have "preOrden (espejo (N a1 a2 a3)) = preOrden (N a1 (espejo a3)
(espejo a2))" by simp
also have "... = a1#(preOrden (espejo a3) @ preOrden (espejo a2))"
by simp
also have "... = a1#(rev (postOrden a3) @ rev(postOrden a2))"
using h1 h2 by simp
also have "... = rev( (postOrden a2) @ (postOrden a3) @[a1] )"
by simp
also have "... = rev (postOrden (N a1 a2 a3))" by simp
finally show "?P (N a1 a2 a3)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que
postOrden (espejo a) = rev (preOrden a)
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar,carvelcab"
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x y z
assume h1: "?P y"
assume h2: "?P z"
have "postOrden (espejo (N x y z)) =
postOrden (N x (espejo z) (espejo y))" by simp
also have "... = postOrden(espejo z)@postOrden(espejo y)@[x]" by simp
also have "... = rev(preOrden z)@rev(preOrden y)@[x]"
using h1 h2 by simp
also have "... = rev(x#(preOrden y)@(preOrden z))" by simp
finally show "?P (N x y z)" by simp
qed

-- "juacorvic, domcadgom (Igual pero un paso más. Se usan variables sugeridas)"
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
fix a
show "?P (H a)" by simp
next
fix a1 a2 a3
assume h1: "?P a2"
assume h2: "?P a3"
have "postOrden (espejo (N a1 a2 a3)) = postOrden (N a1 (espejo a3)
(espejo a2))" by simp
also have "... = postOrden (espejo a3) @ postOrden (espejo a2) @ [a1]"
by simp
also have "... = rev (preOrden a3) @ rev (preOrden a2) @ [a1]"
using h1 h2 by simp
also have "... = rev(a1#(preOrden a2)@(preOrden a3))" by simp
also have "... = rev(preOrden (N a1 a2 a3))" by simp
finally show "?P (N a1 a2 a3)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que
inOrden (espejo a) = rev (inOrden a)
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar,carvelcab"
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x y z
assume h1: "?P y"
assume h2: "?P z"
have "inOrden(espejo (N x y z)) =
inOrden(N x (espejo z) (espejo y))" by simp
also have "... = inOrden(espejo z)@[x]@inOrden(espejo y)" by simp
also have "... = rev(inOrden z)@[x]@rev(inOrden y)" using h1 h2 by simp
also have "... = rev(inOrden y @ [x] @ inOrden z)" by simp
finally show "?P (N x y z)" by simp
qed

-- "juacorvic, domcadgom (Igual pero un paso más. Se usan variables sugeridas)"
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
fix a
show "?P (H a)" by simp
next
fix a1 a2 a3
assume h1: "?P a2"
assume h2: "?P a3"
have "inOrden (espejo (N a1 a2 a3)) = inOrden (N a1 (espejo a3)
(espejo a2))" by simp
also have "... = inOrden (espejo a3) @ [a1] @ inOrden (espejo a2)"
by simp
also have "... = rev (inOrden a3) @ [a1] @ rev (inOrden a2)"
using h1 h2 by simp
also have "... = rev (inOrden a2 @ [a1] @ inOrden a3)" by simp
also have "... = rev (inOrden (N a1 a2 a3))" by simp
finally show "?P (N a1 a2 a3)" by simp
qed

text {*
---------------------------------------------------------------------
Ejercicio 9. Definir la función
raiz :: "'a arbol ⇒ 'a"
tal que (raiz a) es la raiz del árbol a. Por ejemplo,
raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e
---------------------------------------------------------------------
*}
--"jeshorcob,davoremar, domcadgom"
fun raiz :: "'a arbol ⇒ 'a" where
"raiz (H x) = x"
|"raiz (N x _ _ ) = x"

--"juacorvic,carvelcab"
fun raiz2 :: "'a arbol ⇒ 'a" where
"raiz2 (H x) = x"
| "raiz2 (N x yy zz) = x"

(*juacorvic: A partir de aquí en mis definiciones cambio variables por _ .
Pero, ¿Existe alguna diferencia si usamos variables en vez de _?, ¿Es
solo por ahorrarnos escribir?
*)

value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e" -- "True"

text {*
---------------------------------------------------------------------
Ejercicio 10. Definir la función
extremo_izquierda :: "'a arbol ⇒ 'a"
tal que (extremo_izquierda a) es el nodo más a la izquierda del árbol
a. Por ejemplo,
extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
"extremo_izquierda (H x) = x"
|"extremo_izquierda (N _ yy _) = extremo_izquierda yy"

value "extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h)))" -- "= a"

text {*
---------------------------------------------------------------------
Ejercicio 11. Definir la función
extremo_derecha :: "'a arbol ⇒ 'a"
tal que (extremo_derecha a) es el nodo más a la derecha del árbol
a. Por ejemplo,
extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic, carvelcab, domcadgom"
fun extremo_derecha :: "'a arbol ⇒ 'a" where
"extremo_derecha (H x) = x"
|"extremo_derecha (N _ _ zz) = extremo_derecha zz"

value "extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h)))" -- "= h"

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar
last (inOrden a) = extremo_derecha a
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
(*jeshorcob: al intentar hacer la prueba automática, el sistema se
pregunta por el caso en el que la lista sea vacía. Debemos indicar que
esto no puede ocurrir y para ello añadimos un lema auxiliar.*)
lemma a1: "inOrden a ≠ []"
by (induct a, simp_all)

--"jeshorcob,davoremar,juacorvic, domcadgom"
theorem "last (inOrden a) = extremo_derecha a"
by (induct a, simp_all add: a1)

--"jeshorcob,davoremar,juacorvic, domcadgom"
lemma "inOrden a ≠ []"
proof (induct a)
fix x::"'a" show "inOrden (H x) ≠ []" by simp
next
fix x::"'a" and y z::"'a arbol"
assume h1: "inOrden y ≠ []"
assume h2: "inOrden z ≠ []"
show "inOrden (N x y z) ≠ []" using h1 h2 by simp
qed

--"jeshorcob,davoremar,carvelcab, domcadgom"
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x y z
assume h2: "?P z"
have "last(inOrden(N x y z))=last(inOrden y @[x]@ inOrden z)" by simp
also have "... = last(inOrden z)" by (simp add: a1)
also have "... = extremo_derecha z" using h2 by simp
finally show "?P (N x y z)" by simp
qed

--"juacorvic"
(* En mi demostración no uso patrones y no consigo demostrar *)
theorem "last (inOrden a) = extremo_derecha a"
proof (induct a)
fix a::"'a"
show "last (inOrden (H a)) = extremo_derecha (H a)" by simp
next
fix a1::"'a"
fix a2 a3::"'a arbol"
assume h1: "last (inOrden a2) = extremo_derecha a2"
assume h2: "last (inOrden a3) = extremo_derecha a3"
have "last (inOrden (N a1 a2 a3)) = last(inOrden a2 @[a1]@ inOrden a3)"
by simp
then have "... = last (inOrden a3)" by (simp add: a1)
then have "... = extremo_derecha a3" using h2 by simp
thus "last (inOrden(N a1 a2 a3))=extremo_derecha(N a1 a2 a3)" by simp
qed
oops

--"Pedrosrei"
theorem "last (inOrden a) = extremo_derecha a"
apply (induct a, simp_all) apply (metis append_is_Nil_conv arbol.exhaust
inOrden.simps(1) inOrden.simps(2) list.distinct(1)) done

text {*
---------------------------------------------------------------------
Ejercicio 13. Demostrar o refutar
hd (inOrden a) = extremo_izquierda a
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic, domcadgom"
(*jeshorcob: aquí necesitamos el mismo lema por un motivo similar*)
theorem "hd (inOrden a) = extremo_izquierda a"
by (induct a, simp_all add: a1)

--"jeshorcob,davoremar,carvelcab, domcadgom"
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x y z
assume h1: "?P y"
have "hd(inOrden(N x y z))=hd(inOrden y @[x]@ inOrden z)" by simp
also have "... = hd(inOrden y)" by (simp add: a1)
also have "... = extremo_izquierda y" using h1 by simp
finally show "?P (N x y z)" by simp
qed

--"juacorvic"
(*Sin patrones, pero esta si funciona. ¿Porque no la del ejercicio 12?*)
theorem "hd (inOrden a) = extremo_izquierda a"
proof (induct a)
fix a::"'a"
show " hd (inOrden (H a)) = extremo_izquierda (H a)" by simp
next
fix a1::"'a"
fix a2::"'a arbol"
fix a3::"'a arbol"
assume h1: "hd(inOrden a2) = extremo_izquierda a2"
assume h2: "hd (inOrden a3) = extremo_izquierda a3"
have "hd (inOrden (N a1 a2 a3)) = hd (inOrden a2 @[a1]@ inOrden a3)"
by simp
also have "... = hd (inOrden a2)" by (simp add: a1)
also have "... = extremo_izquierda a2" using h1 by simp
finally show " hd (inOrden (N a1 a2 a3)) =
extremo_izquierda (N a1 a2 a3)" by simp
qed

--"Pedrosrei"
theorem "hd (inOrden a) = extremo_izquierda a"
apply (induct a, simp_all) apply (metis Nil_is_append_conv
extremo_izquierda.cases hd_append inOrden.simps(1) inOrden.simps(2)
list.distinct(1)) done

text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
hd (preOrden a) = last (postOrden a)
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic, domcadgom"
theorem "hd (preOrden a) = last (postOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar,juacorvic"
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x::"'a" and y z
have "hd(preOrden(N x y z)) = hd(x#(preOrden y @ preOrden z))" by simp
also have "... = x" by simp
also have "... = last(postOrden y @ postOrden z @[x])" by simp
finally show "?P (N x y z)" by simp
qed

--"juacorvic"
(* Muy detallada *)
theorem "hd (preOrden a) = last (postOrden a)"
proof (induct a)
fix a::"'a"
show "hd (preOrden (H a)) = last (postOrden (H a))" by simp
next
fix a1::"'a"
fix a2::"'a arbol"
fix a3::"'a arbol"
(*La siguiente línea puede eliminarse. No se usa hipótesis h1*)
assume h1: "hd (preOrden a2) = last (postOrden a2)"
(*La siguiente línea puede eliminarse. No se usa hipótesis h2*)
assume h2: " hd (preOrden a3) = last (postOrden a3)"
have "hd(preOrden (N a1 a2 a3))= hd(a1#(preOrden a2 @ preOrden a3))"
by simp
also have "... = hd [a1]" by simp
also have "... = a1" by simp
also have "... = last(postOrden a2 @ postOrden a3 @ [a1])" by simp
also have "... = last (postOrden (N a1 a2 a3))" by simp
finally show "hd (preOrden (N a1 a2 a3)) =
last (postOrden (N a1 a2 a3))" by simp
qed

--"carvelcab, domcadgom"

theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x ii dd
assume h1: "?P ii"
assume h2: "?P dd"
have "hd (preOrden (N x ii dd)) = hd (x#(preOrden ii @ preOrden dd))" by simp
also have "... = x" by simp
finally show "?P (N x ii dd)" by simp
qed

-- es una orden mas corta que la primera

text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
hd (preOrden a) = raiz a
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,carvelcab, domcadgom"
theorem "hd (preOrden a) = raiz a"
by (induct a, simp_all)

--"jeshorcob,davoremar"
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x::"'a" and y z
have "hd(preOrden(N x y z)) = hd(x#(preOrden y @ preOrden z))" by simp
also have "... = x" by simp
finally show "?P (N x y z)" by simp
qed

--"juacorvic"
(* Muy detallada *)
theorem "hd (preOrden a) = raiz a"
proof (induct a)
fix a::"'a"
show " hd (preOrden (H a)) = raiz (H a)" by simp
next
fix a1::"'a"
fix a2::"'a arbol"
fix a3::"'a arbol"
(*La siguiente línea puede eliminarse. No se usa hipótesis h1*)
assume h1: "hd (preOrden a2) = raiz a2"
(*La siguiente línea puede eliminarse. No se usa hipótesis h2*)
assume h2: " hd (preOrden a3) = raiz a3"
have "hd (preOrden (N a1 a2 a3)) = hd(a1#(preOrden a2 @ preOrden a3))"
by simp
also have "... = a1" by simp
also have "... = raiz (N a1 a2 a3)" by simp
finally show "hd (preOrden (N a1 a2 a3)) = raiz (N a1 a2 a3)" by simp
qed

--"carvelcab, domcadgom"

theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x ii dd
assume h1: "?P ii"
assume h2: "?P dd"
have "hd (preOrden (N x ii dd)) = hd (x# preOrden ii @ preOrden dd)" by simp
also have "... = x" by simp
also have "... = raiz (N x ii dd)" by simp
finally show "?P (N x ii dd)" by simp
qed

-- esta tambien es una orden mas corta que la primera, pero a pesar de no usar las hipotesis, me da una advertencia si las quito.

text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
hd (inOrden a) = raiz a
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,carvelcab, domcadgom"
theorem "hd (inOrden a) = raiz a"
quickcheck
oops
(*Encuentra el contrajemplo:
a = N a⇩1 (H a⇩2) (H a⇩1)

ya que evaluando se ve que son distindos:
hd (inOrden a) = a⇩2
raiz a = a⇩1
*)

text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
last (postOrden a) = raiz a
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar, domcadgom"
theorem "last (postOrden a) = raiz a"
by (induct a, simp_all)

--"jeshorcob,davoremar"
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x show "?P (H x)" by simp
next
fix x::"'a" and y z
have "last(postOrden(N x y z)) =
last(postOrden y @ postOrden z @ [x])" by simp
also have "... = x" by simp
finally show "?P (N x y z)" by simp
qed

--"juacorvic"
(*Muy detallada*)
theorem "last (postOrden a) = raiz a"
proof (induct a)
fix a::"'a"
show " last (postOrden (H a)) = raiz (H a)" by simp
next
fix a1::"'a"
fix a2::"'a arbol"
fix a3::"'a arbol"
(*La siguiente línea puede eliminarse. No se usa hipótesis h1*)
assume h1:"last (postOrden a2) = raiz a2"
(*La siguiente línea puede eliminarse. No se usa hipótesis h2*)
assume h2:"last (postOrden a3) = raiz a3"
have "last (postOrden (N a1 a2 a3)) =
last(postOrden a2 @ postOrden a3 @ [a1])" by simp
also have "... = a1" by simp
also have "... = raiz (N a1 a2 a3)" by simp
thus "last (postOrden (N a1 a2 a3)) = raiz (N a1 a2 a3)" by simp
qed

--"carvelcab, domcadgom"
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
fix x
show "?P (H x)" by simp
next
fix x ii dd
assume h1:"?P ii"
assume h2:"?P dd"
have "last (postOrden (N x ii dd)) = last (postOrden ii @ postOrden dd @[x])" by simp
also have "... = x" by simp
finally show "?P (N x ii dd)" by simp
qed

-- Lo mismo de antes, con una orden menos.
end
</source>

Relación 6

2014-12-04T11:04:54Z

Domcadgom:

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

theory R6
imports Main
begin

text {*
Nota: En esta relación se pide hacer las demostraciones de forma
automática. *}

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

--"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom, domcadgom"
fun sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
"sust x y [] = []"
|"sust x y (z#zs) = (if z = x then y#(sust x y zs) else z#(sust x y zs))"

value "sust (1::int) 2 [1,2,3,4,1,2,3,4]" -- "= [2,2,3,4,2,2,3,4]"

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

--"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom, domcadgom"
lemma sust_append:
"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
by (induct xs) auto

(*Pedrosrei: no es necesario auto, sirve simp_all*)

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

--"jeshorcob,davoremar,marnajgom, domcadgom"
lemma rev_sust:
"rev(sust x y zs) = sust x y (rev zs)"
by (induct zs, simp_all add: sust_append)

--"juacorvic"
lemma rev_sust2:
"rev(sust x y zs) = sust x y (rev zs)"
by (induct zs) (auto simp add:sust_append)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "sust x y (sust u v zs) = sust u v (sust x y zs)"
quickcheck
oops
(*Encuentra el contraejemplo:
x = a⇩1
y = a⇩2
u = a⇩2
v = a⇩1
zs = [a⇩1]
*)
text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar:
sust y z (sust x y zs) = sust x z zs
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "sust y z (sust x y zs) = sust x z zs"
quickcheck
oops
(*Encuentra el contraejemplo:
y = a⇩1
z = a⇩2
x = a⇩2
zs = [a⇩1]
*)

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

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
fun borra :: "'a ⇒ 'a list ⇒ 'a list" where
"borra x [] = []"
|"borra x (y#ys) = (if y=x then ys else y#borra x ys)"

value "borra (2::int) [1,2,3,2]" -- "= [1,3,2]"

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
fun borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
"borraTodas x [] = []"
|"borraTodas x (y#ys) = (if y = x then borraTodas x ys
else y#borraTodas x ys)"

value "borraTodas (2::int) [1,2,3,2]" -- "= [1,3]"

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma l1: "borra x (borraTodas x xs) = borraTodas x xs"
by (induct xs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "borraTodas x (borraTodas x xs) = borraTodas x xs"
by (induct xs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma borraTodas_borra:
"borraTodas x (borra x xs) = borraTodas x xs"
by (induct xs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "borra x (borra y xs) = borra y (borra x xs)"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar automáticamente
borraTodas x (borra y xs) = borra y (borraTodas x xs)
---------------------------------------------------------------------
*}

--"jeshorcob,juacorvic"
lemma "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
by (induct xs, simp_all add: l1)

--"davoremar"
lemma "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
by (induct xs, simp_all add: borraTodas_borra)
(*Pedrosrei: me da fallo esta última con simp_all pero no con auto *)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "borra y (sust x y xs) = borra x xs"
quickcheck
oops
(* Encuentra el contraejemplo:
y = a⇩1
x = a⇩2
xs = [a⇩1]
*)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "borraTodas y (sust x y xs) = borraTodas x xs"
quickcheck
oops
(* Encuentra el contraejemplo:
y = a⇩1
x = a⇩2
xs = [a⇩1]
*)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "sust x y (borraTodas x zs) = borraTodas x zs"
by (induct zs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "sust x y (borraTodas z zs) = borraTodas z (sust x y zs)"
quickcheck
oops
(* Encuentra el contraejemplo:
x = a⇩1
y = a⇩2
z = a⇩1
zs = [a⇩1]
*)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "rev (borra x xs) = borra x (rev xs)"
quickcheck
oops
(* Encuentra el contraejemplo:
x = a⇩1
xs = [a⇩1, a⇩2, a⇩1]
*)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma borraTodas_append:
"borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
by (induct xs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "rev (borraTodas x xs) = borraTodas x (rev xs)"
by (induct xs, simp_all add: borraTodas_append)

end
</source>

Relación 6

2014-12-04T10:31:12Z

Domcadgom:

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

theory R6
imports Main
begin

text {*
Nota: En esta relación se pide hacer las demostraciones de forma
automática. *}

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

--"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom, domcadgom"
fun sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
"sust x y [] = []"
|"sust x y (z#zs) = (if z = x then y#(sust x y zs) else z#(sust x y zs))"

value "sust (1::int) 2 [1,2,3,4,1,2,3,4]" -- "= [2,2,3,4,2,2,3,4]"

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

--"jeshorcob, emimarriv,davoremar,juacorvic,marnajgom, domcadgom"
lemma sust_append:
"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
by (induct xs) auto

(*Pedrosrei: no es necesario auto, sirve simp_all*)

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

--"jeshorcob,davoremar,marnajgom, domcadgom"
lemma rev_sust:
"rev(sust x y zs) = sust x y (rev zs)"
by (induct zs, simp_all add: sust_append)

--"juacorvic"
lemma rev_sust2:
"rev(sust x y zs) = sust x y (rev zs)"
by (induct zs) (auto simp add:sust_append)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "sust x y (sust u v zs) = sust u v (sust x y zs)"
quickcheck
oops
(*Encuentra el contraejemplo:
x = a⇩1
y = a⇩2
u = a⇩2
v = a⇩1
zs = [a⇩1]
*)
text {*
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar:
sust y z (sust x y zs) = sust x z zs
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "sust y z (sust x y zs) = sust x z zs"
quickcheck
oops
(*Encuentra el contraejemplo:
y = a⇩1
z = a⇩2
x = a⇩2
zs = [a⇩1]
*)

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

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
fun borra :: "'a ⇒ 'a list ⇒ 'a list" where
"borra x [] = []"
|"borra x (y#ys) = (if y=x then ys else y#borra x ys)"

value "borra (2::int) [1,2,3,2]" -- "= [1,3,2]"

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
fun borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
"borraTodas x [] = []"
|"borraTodas x (y#ys) = (if y = x then borraTodas x ys
else y#borraTodas x ys)"

value "borraTodas (2::int) [1,2,3,2]" -- "= [1,3]"

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma l1: "borra x (borraTodas x xs) = borraTodas x xs"
by (induct xs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "borraTodas x (borraTodas x xs) = borraTodas x xs"
by (induct xs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma borraTodas_borra:
"borraTodas x (borra x xs) = borraTodas x xs"
by (induct xs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "borra x (borra y xs) = borra y (borra x xs)"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar o refutar automáticamente
borraTodas x (borra y xs) = borra y (borraTodas x xs)
---------------------------------------------------------------------
*}

--"jeshorcob,juacorvic"
lemma "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
by (induct xs, simp_all add: l1)

--"davoremar"
lemma "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
by (induct xs, simp_all add: borraTodas_borra)
(*Pedrosrei: me da fallo esta última con simp_all pero no con auto *)

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

--"jeshorcob,davoremar,juacorvic,marnajgom, domcadgom"
lemma "borra y (sust x y xs) = borra x xs"
quickcheck
oops
(* Encuentra el contraejemplo:
y = a⇩1
x = a⇩2
xs = [a⇩1]
*)

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

--"jeshorcob,davoremar,juacorvic,marnajgom"
lemma "borraTodas y (sust x y xs) = borraTodas x xs"
quickcheck
oops
(* Encuentra el contraejemplo:
y = a⇩1
x = a⇩2
xs = [a⇩1]
*)

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

--"jeshorcob,davoremar,juacorvic,marnajgom"
lemma "sust x y (borraTodas x zs) = borraTodas x zs"
by (induct zs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom"
lemma "sust x y (borraTodas z zs) = borraTodas z (sust x y zs)"
quickcheck
oops
(* Encuentra el contraejemplo:
x = a⇩1
y = a⇩2
z = a⇩1
zs = [a⇩1]
*)

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

--"jeshorcob,davoremar,juacorvic,marnajgom"
lemma "rev (borra x xs) = borra x (rev xs)"
quickcheck
oops
(* Encuentra el contraejemplo:
x = a⇩1
xs = [a⇩1, a⇩2, a⇩1]
*)

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

--"jeshorcob,davoremar,juacorvic,marnajgom"
lemma borraTodas_append:
"borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
by (induct xs, simp_all)

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

--"jeshorcob,davoremar,juacorvic,marnajgom"
lemma "rev (borraTodas x xs) = borraTodas x (rev xs)"
by (induct xs, simp_all add: borraTodas_append)

end
</source>

Relación 5

2014-11-20T14:19:24Z

Domcadgom:

<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,juacorvic,davoremar, marnajgom, domcadgom"
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"

--"emimarriv"
fun todos3 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos3 p [] = True"
| "todos3 p (x#xs) = (if p x then (todos3 p xs) else False)"
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.
---------------------------------------------------------------------
*}

(* Errata. Debe ser False el caso base seguro porque si no,
la función devuelve siempre True*)
--"jeshorcob,javrodviv1,juacorvic,davoremar, marnajgom, domcadgom"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = False"
|"algunos p (x#xs) = (p x ∨ algunos p xs)"

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

value "algunos (λx. x>10) [3::int,2]"
value "algunos2 (λx. x>10) [3::int,2]"

-- "javrodviv1"
fun algunos3 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos3 p [] = False"
|"algunos3 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*)
(* jeshorcob: Debe ser False y la función tiene una errata en
la segunda linea porque la recursión la debe hacer sobre la función
algunos3 en lugar de todos *)

--"emimarriv"
fun algunos4 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos4 p [] =False"
| "algunos4 p (x#xs) = (if p x then True else (algunos4 p xs))"

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

--"jeshorcob,javrodviv1,davoremar, marnajgom, domcadgom"
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

-- "juacorvic, marnajgom, domcadgom" (*Muy parecida a la solución anterior*)
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 ∧ Q x ∧ todos P xs ∧ todos Q xs)" by simp
also have "... = ((P x ∧ todos P xs) ∧ (Q x ∧ todos Q xs))" by arith
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

--"emimarriv"

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) =((todos (λx. P x ∧ Q x) [x]) ∧ (todos (λx. P x ∧ Q x) xs))" by simp
also have "... = ((todos P [x] ∧ todos Q [x]) ∧ (todos P xs ∧ todos Q xs))" using HI by simp
also have "... = ((todos P [x] ∧ todos P xs) ∧ (todos Q [x] ∧ todos Q xs))" by simp
also have "... = (todos P (x#xs) ∧ todos Q (x#xs))" by simp (* emimarriv: Esta linea puede suprimirse, pero la dejo porque se sigue
mejor el proceso*)
finally show "todos (λx. P x ∧ Q x) (x#xs) = (todos P (x#xs) ∧ todos Q (x#xs))" by auto
qed

--"davoremar"

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 "... = ((todos P (x#xs)) ∧ (todos Q (x#xs)))" by auto
finally show "todos (λx. P x ∧ Q x) (x#xs) = (todos P (x#xs) ∧ todos Q (x#xs))" by simp
qed

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

--"jeshorcob,javrodviv1,juacorvic,davoremar, marnajgom, domcadgom"
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, emimarriv"
(* es igual que la de jeshorcob pero nos podemos ahorrar
una linea de comando*)

lemma todos_append2:
"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

-- "juacorvic, marnajgom, domcadgom"
(* es igual que las anteriores pero salió con mayor nivel de detalle *)

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 "... = ((P a ∧ todos P x) ∧ todos P y)" 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

--"davoremar"

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 x xs
assume HI: "todos P (xs @ y) = (todos P xs ∧ todos P y)"
have "todos P ((x#xs) @ y) = ((P x) ∧ (todos P (xs @ y)))" by simp
also have "... = ((P x) ∧ (todos P xs ∧ todos P y))" using HI by simp
finally show "todos P ((x#xs) @ y) = (todos P (x#xs) ∧ 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, juacorvic,davoremar, marnajgom, domcadgom"

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, juacorvic, marnajgom, domcadgom"
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, emimarriv"

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

--"davoremar"

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
finally show "todos P (rev (x#xs)) = todos P (x#xs)" by auto
qed

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

(*Pedrosrei: No sé cómo has conseguido el contraejemplo,
probablemente algún fallo en los paréntesis, ya que la propiedad
resulta cierta como expongo abajo:
*)
(* jeshorcob: el contraejemplo existe. Fijate en lo siguiente: *)
fun p1 :: "int ⇒ bool" where
"p1 x = (x=3)"
fun q1 :: "int ⇒ bool" where
"q1 x = (x=2)"
value "algunos (λx. p1 x ∧ q1 x) [3,2]" -- "= False
(porque ningún elemento de la lista cumple a la vez p1 y q1)"
value "(algunos p1 [3,2] ∧ algunos q1 [3,2])" -- "= True
(porque cada elemento de la lista cumple una sola de p1 y q1)"
(*Por tanto:*)
value "algunos (λx. p1 x ∧ q1 x) [3,2] =
(algunos p1 [3,2] ∧ algunos q1 [3,2])" -- "= False"
(*Esta es una instancia del contraejemplo que encuentra QuickCheck*)

lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
by (metis (full_types) algunos.simps(1) algunos.simps(2) list_nonempty_induct)

(*Al cambiar la definición de algunos para que coincida con list_ex es cierto el
contraejemplo de Jesús
*)

-- "juacorvic"
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
(* Ya no podemos seguir más ya que no se cuemple:
also have "... = ((P a ∨ algunos P xs) ∧ (Q a ∨ algunos Q xs))
Tenemos que buscar un contraejemplo:
*)
oops

--"jeshorcob, emimarriv, juacorvic,davoremar, marnajgom, domcadgom"
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]
*}

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

-- "javrodviv1, jeshorcob, juacorvic,davoremar, marnajgom, domcadgom"

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, jeshorcob, emimarriv, juacorvic, domcadgom"

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

--"davoremar, marnajgom"

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

text {*
---------------------------------------------------------------------
Ejercicio 8.1. Demostrar o refutar automáticamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}
(*Pedrosrei: Pongo la automática que parece se os resiste.*)

lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (metis algunos.simps(1) algunos.simps(2) list_nonempty_induct)

(*Si corregís la definición de algunos sería: *)

lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs, auto)

(*jeshorcob: Pedro, a la tuya no sé que le pasa que no me la coge bien.
Dejo la mía *)

--"jeshorcob,juacorvic,davoremar, marnajgom, domcadgom"
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs) auto

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

-- "javrodviv1, jeshorcob, emimarriv, domcadgom"
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

(*Igual que anterior, cambia uso de paréntesis y un paso más*)
-- "juacorvic, marnajgom"
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
also have "... = (algunos P (a # xs) ∨ algunos P ys)" by simp
finally show "algunos P ((a # xs) @ ys) = (algunos P (a # xs) ∨ algunos P ys)" by simp
qed

--"davoremar"

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 x xs
assume HI: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
have "algunos P ((x#xs) @ ys) = ((P x) ∨ algunos P (xs @ ys))" by simp
also have "... = ((P x) | (algunos P xs ∨ algunos P ys))" using HI by simp
finally show "algunos P ((x#xs) @ ys) = (algunos P (x#xs) ∨ algunos P ys)" by simp
qed

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

-- "javrodviv1, jeshorcob, juacorvic,davoremar, marnajgom, domcadgom"
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, jeshorcob"
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

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

-- "juacorvic, domcadgom"
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 (rev xs) ∨ algunos P [a])" by (simp add: algunos_append)
also have "... = (algunos P xs ∨ algunos P [a])" using HI by simp
also have "... = (algunos P [a] ∨ algunos P xs)" by arith
also have "... = algunos P (a # xs)" by simp
finally show "algunos P (rev (a # xs)) = algunos P (a # xs)" by simp
qed

--"davoremar, marnajgom"

lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next
fix x xs
assume HI: "algunos P (rev xs) = algunos P xs"
have "algunos P (rev (x#xs)) = algunos P ((rev xs) @ [x])" by simp
also have "... = (algunos P (rev xs) ∨ (algunos P [x]))" by (simp add: algunos_append)
also have "... = (algunos P xs ∨ algunos P [x])" using HI by simp
also have "... = (algunos P xs ∨ (P x))" by simp
finally show "algunos P (rev (x#xs)) = algunos P (x#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.
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
by (induct xs) auto

--"jeshorcob"
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 x xs
assume hi:"algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
have "algunos (λx. P x ∨ Q x) (x # xs) = ((P x ∨ Q x)
∨ algunos (λx. P x ∨ Q x) xs)" by simp
also have "... = ((P x ∨ Q x) ∨ (algunos P xs ∨ algunos Q xs))"
using hi by simp
also have "... = (P x ∨ algunos P xs ∨ Q x ∨ algunos Q xs)" by arith
finally show " algunos (λx. P x ∨ Q x) (x # xs) =
(algunos P (x # xs) ∨ algunos Q (x # xs))" by simp
qed

--"davoremar"

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 x xs
assume HI: "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
have "algunos (λx. P x ∨ Q x) (x#xs) = (P x ∨ Q x ∨ algunos (λx. P x | Q x) xs)" by simp
also have "... = (P x ∨ Q x ∨ algunos P xs ∨ algunos Q xs)" using HI by simp
finally show "algunos (λx. P x ∨ Q x) (x#xs) = (algunos P (x#xs) ∨ algunos Q (x#xs))" by auto
qed

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

(*Pedrosrei: Es falso.

Por ejemplo P= esVacio, xs = []. P es la propiedad de ser vacío
con nuestra construcción de algunos es cierto "algunos esVacio []"
Sin embargo, todos (λx. (¬ esVacio {})) [] es lo mismo que
todos _ [] = True, por lo que ¬(todos (λx. (¬ esVacio {})) []) = False,
siendo falsa nuestra definición. Podemos coger de todas maneras la propiedad
que queramos y sigue siendo falso porque
(algunos _ [] True) ∧ (¬(todos _ [])= False)
*)
lemma
shows "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
quickcheck
oops
(*Al corregir la definición de "algunos" deja de ser cierto lo dicho y
correcto lo de abajo.
*)

(*jeshorcob: está claro que el fallo en todo era la definición esa*)

-- "javrodviv1, jeshorcob, juacorvic,davoremar, marnajgom, domcadgom"
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, jeshorcob,davoremar, domcadgom"
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

-- "juacorvic, marnajgom"
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
also have "... = (¬ todos (λx. ¬ P x) (a # xs))" by simp
(* Este paso lo he puesto por inercia de otras demostraciones
pero realmente no veo como hacerlo más detallado *)
finally show "algunos P (a # xs) = (¬ todos (λx. ¬ P x) (a # xs))" by simp
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, jeshorcob, davoremar, domcadgom"
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = ((x=a) ∨ estaEn x xs)"

-- "juacorvic, marnajgom"
(*Si cambiamos el orden de la igualdad no tenemos que
utilizar auto en la demostración*)
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (a = x ∨ estaEn x xs)"

value "estaEn (2::nat) [3,2,4]" --"= True"
value "estaEn (1::nat) [3,2,4]" --"= False"

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

--"jeshorcob,juacorvic,davoremar, marnajgom, domcadgom"
lemma "algunos (λx. x=y) xs = estaEn y xs"
by (induct xs) auto

--"jeshorcob,davoremar, domcadgom"
lemma "algunos (λx. x=y) xs = estaEn y xs" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume HI: "?P xs"
have "estaEn y (x#xs) = (y=x ∨ estaEn y xs)" by simp
also have "… = (y=x ∨ algunos (λx. (x=y)) xs)" using HI by simp
finally show "?P (x#xs)" by auto
qed

-- "juacorvic, marnajgom"
lemma "algunos (λx. x=y) xs = estaEn y xs"
proof (induct xs)
show "algunos (λx. x = y) [] = estaEn y []" by simp
next
fix a xs
assume HI: "algunos (λx. x = y) xs = estaEn y xs"
have "algunos (λx. x = y) (a # xs) = (a = y ∨ algunos (λx. x = y) xs)" by simp
also have "... = (a = y ∨ estaEn y xs)" using HI by simp
also have "... = (estaEn y (a # xs))" by simp
finally show "algunos (λx. x = y) (a # xs) = estaEn y (a # xs)" by simp
qed

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)"

(*jeshorcob: Esta definición no es correcta. Véanse:*)
value "sinDuplicados [1::nat,4,2]" -- "= True"
value "sinDuplicados [1::nat,4,2,4]" -- "= False"

--"jeshorcob, juacorvic,davoremar, marnajgom, domcadgom"
fun sinDuplicados2 :: "'a list ⇒ bool" where
"sinDuplicados2 [] = True"
|"sinDuplicados2 (x#xs) = (¬(estaEn x xs) ∧ sinDuplicados2 xs)"

value "sinDuplicados2 [1::nat,4,2]" -- "= True"
value "sinDuplicados2 [1::nat,4,2,4]" -- "= False"

--"emimarriv"
fun sinDuplicados3 :: "'a list ⇒ bool" where
"sinDuplicados3 [] = True"
| "sinDuplicados3 (x#xs) = (if estaEn x xs then False else sinDuplicados3 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, jeshorcob, juacorvic,davoremar, marnajgom, domcadgom"
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, jeshorcob, juacorvic,davoremar, domcadgom"
lemma "length (borraDuplicados xs) ≤ length xs"
by (induct xs) auto

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

-- "javrodviv1, jeshorcob,davoremar"
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

-- "juacorvic"
(*Igual pero con 1 paso más*)
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
also have "... ≤ length (a # xs)" by simp
finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)" by simp
qed
(*Nota: así conseguimos demostrar el caso de que el elemento 'a' no esté repetido
en la lista. Que pasa con la demostración para el caso de una lista cuyos los elementos
sean todos duplicados. Por ejemplo [1::nat,1,1,1,1,1,1].
Esto no se reduce:
have "length (borraDuplicados (a # xs)) ≤ length (borraDuplicados xs)" by simp
*)

-- "marnajgom, domcadgom"
lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a
fix xs
assume HI: "length (borraDuplicados xs) ≤ length xs"
show "length (borraDuplicados (a # xs)) ≤ length (a # xs)"
proof (cases)
assume H1:"estaEn a xs"
have "length (borraDuplicados (a # xs)) = length (borraDuplicados xs)" using H1 by simp
also have "... ≤ length xs" using HI by simp
also have "... ≤ 1+length xs" by simp
also have "... ≤ length (a#xs)" by simp
finally show ?thesis.
next
assume H2: "¬estaEn a xs"
have "length (borraDuplicados (a # xs)) = length (a# borraDuplicados xs)" using H2 by simp
also have "... = 1+ length (borraDuplicados xs)" by simp
also have "... ≤ 1+ length xs" using HI by simp
also have "... ≤ length (a#xs)" by simp
finally show ?thesis.
qed
qed

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

-- "javrodviv1, juacorvic,davoremar, marnajgom, domcadgom"
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs) auto

--"jeshorcob"
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs, auto)
done

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

(*Pedrosrei: con esta definición de borraDuplicados es falso si cogemos
xs= []. Además del quickcheck, podemos hacer "apply (induct xs, auto)"
y ver que nos pide que demostremos False.
*)
lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops

(*jeshorcob: dejo la prueba por inducción y casos*)
--"jeshorcob,davoremar"
lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
fix x xs
assume hi: "estaEn a (borraDuplicados xs) = estaEn a xs"
show "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#xs)"
proof (cases)
assume a1:"estaEn x xs"
then have "estaEn a (borraDuplicados (x#xs)) =
estaEn a (borraDuplicados xs)" by simp
also have "... = estaEn a xs" using hi by simp
also have "... = estaEn a (x#xs)" using a1 by auto
finally show ?thesis by simp
next
assume a2:"¬(estaEn x xs)"
then have "estaEn a (borraDuplicados (x#xs)) =
estaEn a (x#borraDuplicados xs)" by simp
also have "... = (a = x ∨ estaEn a (borraDuplicados xs))" by simp
finally show ?thesis using hi by simp
qed
qed

-- "juacorvic, marnajgom, domcadgom"
(* Es identica a la anterior, salvo un paso que no se resuelve.
Tampoco entiendo que aplica jeshorcob en ese paso *)
lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
fix aa xs
assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
show "estaEn a (borraDuplicados (aa # xs)) = estaEn a (aa # xs)"
proof (cases)
assume HI1: "estaEn aa xs"
then have "estaEn a (borraDuplicados (aa # xs)) = estaEn a (borraDuplicados xs)" by simp
also have "... = estaEn a xs" using HI by simp
also have "... = estaEn a (aa # xs)" using HI1 by auto (*marnajgom: Así me funciona a mi*)
finally show "estaEn a (borraDuplicados (aa # xs)) = estaEn a (aa # xs)" by simp
next
assume HI2: "¬(estaEn aa xs)"
then have "estaEn a (borraDuplicados (aa # xs)) = estaEn a (aa#borraDuplicados xs)" by simp
also have "... = (aa = a ∨ estaEn a (borraDuplicados xs))" by simp
also have "... = (aa =a ∨ estaEn a xs) " using HI by simp
also have "... = estaEn a (aa # xs)" using HI2 by simp (*marnajgom: te faltaba using HI2*)
(* also have "... = estaEn a (aa # xs)" by simp --juacorvic: Tal y como lo tenía funciona *)
finally show "estaEn a (borraDuplicados (aa # xs)) = estaEn a (aa # xs)" by simp
qed
qed

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

--"jeshorcob,davoremar, marnajgom, domcadgom"
lemma "sinDuplicados2 (borraDuplicados xs)"
by (induct xs) (auto simp add: estaEn_borraDuplicados)

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

--"jeshorcob,davoremar"
lemma sinDuplicados_borraDuplicados:
"sinDuplicados2 (borraDuplicados xs)"
proof (induct xs)
show "sinDuplicados2 (borraDuplicados [])" by simp
next
fix x::"'a"
fix xs::"'a list"
assume hi: "sinDuplicados2 (borraDuplicados xs)"
have "sinDuplicados2 (borraDuplicados (x#xs)) =
sinDuplicados2 ((if estaEn x xs then borraDuplicados xs
else x # borraDuplicados xs))" by simp
also have "... = (if estaEn x xs
then sinDuplicados2 (borraDuplicados xs)
else sinDuplicados2 (x#borraDuplicados xs))" by simp
also have "...= (if estaEn x xs then sinDuplicados2 (borraDuplicados xs)
else (¬estaEn x (borraDuplicados xs)
∧ sinDuplicados2 (borraDuplicados xs)))" by simp
also have "...= (if estaEn x xs then sinDuplicados2 (borraDuplicados xs)
else (¬estaEn x xs ∧ sinDuplicados2 (borraDuplicados xs)))"
by (simp add: estaEn_borraDuplicados)
then show "sinDuplicados2 (borraDuplicados (x#xs))"
using hi by (simp add: estaEn_borraDuplicados)
qed

-- "marnajgom"
lemma sinDuplicados_borraDuplicados:
"sinDuplicados (borraDuplicados xs)"
proof (induct xs)
show "sinDuplicados (borraDuplicados [])" by simp
next
fix a xs
assume HI: "sinDuplicados (borraDuplicados xs)"
show "sinDuplicados (borraDuplicados (a # xs))"
proof (cases)
assume H1: "estaEn a xs"
thus "sinDuplicados (borraDuplicados (a#xs))" using HI by simp
next
assume H2: "¬estaEn a xs"
thus "sinDuplicados (borraDuplicados (a#xs))" using HI by (auto simp add:estaEn_borraDuplicados)
qed
qed

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

(*Pedrosrei: es falso, como podemos ver si cogemos [1,2,1] y evaluamos:
*)
lemma "borraDuplicados' (rev xs) = rev (borraDuplicados' xs)"
quickcheck
oops

--"jeshorcob,davoremar, marnajgom, domcadgom"
lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
quickcheck
oops

text {* Encuentra el contraejemplo
xs = [a⇩1, a⇩2, a⇩1]
Evaluated terms:
borraDuplicados (rev xs) = [a⇩2, a⇩1]
rev (borraDuplicados xs) = [a⇩1, a⇩2]
*}

end
</source>

Relación 4

2014-11-20T14:09:25Z

Domcadgom:

<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, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom"

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, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom"

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

(*Pedrosrei:no hace falta usar auto, sirve simp_all*)

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

-- "davoremar,javrodviv1, jeshorcob, emimarriv, juacorvic, marnajgom, domcadgom"

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, jeshorcob, marnajgom"

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

(*Pedrosrei:no hace falta usar auto, sirve simp*)

-- "juacorvic, domcadgom"
lemma "rev (x # xs) = snoc (rev xs) x"
by (simp add: snoc_append)

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

-- "davoremar,javrodviv1, jeshorcob, juacorvic, marnajgom, domcadgom"

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-12T20:28:03Z

Domcadgom:

<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"

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"

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"

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"

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"

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"

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

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"

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"

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"
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"

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"

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>