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

Relación 7

2014-12-04T11:29:09Z

Marnajgom:

<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, marnajgom"
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, marnajgom"
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, marnajgom"
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, marnajgom"
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, marnajgom (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, marnajgom (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, marnajgom (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, marnajgom"
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, marnajgom"
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, marnajgom"
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, marnajgom"
(*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, marnajgom"
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,marnajgom"

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, marnajgom"
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,marnajgom"
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-11-27T10:00:40Z

Marnajgom:

<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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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-20T10:32:22Z

Marnajgom:

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

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

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"

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"
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"
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"
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"
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"
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"
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"
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"
lemma "algunos (λx. x=y) xs = estaEn y xs"
by (induct xs) auto

--"jeshorcob,davoremar"
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"
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"
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"
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"
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"
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"
(* 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*)
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"
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"
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-20T10:12:31Z

Marnajgom:

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

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"

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"

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

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-12T10:00:37Z

Marnajgom:

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

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"

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"

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"

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"

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"

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

-- "davoremar juacorvic marnajgom"

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"

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"

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

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"

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

-- "davoremar marnajgom"

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

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

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"

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"

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"

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"

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

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