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

Relación 11

2015-01-18T15:22:30Z

Davoremar:

<source lang="isar">
header {* R11: Plegados de listas y de árboles *}

theory R11
imports Main
begin

section {* Nuevas funciones sobre listas *}

text {*
Nota. En esta relación se usará la función suma tal que (suma xs) es
la suma de los elementos de xs, definida por
*}

(* Pedrosrei: corrijo, la definición que se pretendía era esta, debería
estar dada, es una errata. *)

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

text {*
Las funciones de plegado, foldr y foldl, están definidas en la teoría
List.thy por
foldr :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a list ⇒ 'b ⇒ 'b"
foldr f [] = id
foldr f (x # xs) = f x ∘ foldr f xs

foldl :: "('b ⇒ 'a ⇒ 'b) ⇒ 'b ⇒ 'a list ⇒ 'b"
foldl f a [] = a
foldl f a (x # xs) = foldl f (f a x) xs"

Por ejemplo,
foldr (op +) [a,b,c] d = a + (b + (c + d))
foldl (op +) d [a,b,c] = ((d + a) + b) + c
foldr (op -) [9,4,2] (0::int) = 7
foldl (op -) (0::int) [9,4,2] = -15
*}

value "foldr (op +) [a,b,c] d" -- "= a + (b + (c + d))"
value "foldl (op +) d [a,b,c]" -- "= ((d + a) + b) + c"
value "foldr (op -) [9,4,2] (0::int)" -- "= 7"
value "foldl (op -) (0::int) [9,4,2]" -- "= -15"

text {*
---------------------------------------------------------------------
Ejercicio 1. Demostrar que
suma xs = foldr (op +) xs 0
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma suma_foldr: "suma xs = foldr (op +) xs 0"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar que
length xs = foldr (λ x res. 1 + res) xs 0
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma length_foldr: "length xs = foldr (λ x res. 1 + res) xs 0"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 3. La aplicación repetida de foldr y map tiene el
inconveniente de que la lista se recorre varias veces. Sin embargo, es
suficiente recorrerla una vez como se muestra en el siguiente ejemplo,
suma (map (λx. x + 3) xs) = foldr h xs b
Determinar los valores de h y b para que se verifique la igualdad
anterior y demostrarla.
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "suma (map (λx. x + 3) xs) = foldr (λ x y. x+y+3) xs 0"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 4. Generalizar el resultado anterior; es decir determinar
los valores de h y b para que se verifique la igualdad
foldr g (map f xs) a = foldr h xs b
y demostrarla.
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "foldr g (map f xs) a = foldr (g∘f) xs a"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 5. La siguiente función invierte una lista en tiempo lineal
fun inversa_ac :: "['a list, 'a list] ⇒ 'a list" where
"inversa_ac [] ys = ys"
| "inversa_ac (x#xs) ys = (inversa_ac xs (x#ys))"

definition inversa_ac :: "'a list ⇒ 'a list" where
"inversa_ac xs ≡ inversa_ac_aux xs []"
Por ejemplo,
inversa_ac [a,d,b,c] = [c, b, d, a]
Demostrar que inversa_ac se puede definir unsando foldl.
---------------------------------------------------------------------
*}

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

--"jeshorcob,davoremar"
definition inversa_ac :: "'a list ⇒ 'a list" where
"inversa_ac xs ≡ inversa_ac_aux xs []"

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

--"jeshorcob"
lemma inversa_ac_aux_foldl:
"inversa_ac_aux xs a = foldl (λ ys x. x#ys) a xs"
by (induct xs arbitrary: a, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar la siguiente propiedad distributiva de la suma
sobre la concatenación:
suma (xs @ ys) = suma xs + suma ys
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma suma_append [simp]:
"suma (xs @ ys) = suma xs + suma ys"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar una propiedad similar para foldr
foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)
En este caso, hay que restringir el resultado teniendo en cuenta
propiedades algebraicas de f y a.
---------------------------------------------------------------------
*}

--"Pedrosrei: Dales nombre a las cosas Jesús, te las nombro yo:"

--"jeshorcob"
lemma l1:
assumes neutr: "(∀ x. (f a x = x))" and
assoc: "(∀x y z. f (f x y) z = f x (f y z))"
shows "foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
proof (induct xs)
show "foldr f ([] @ ys) a = f (foldr f [] a) (foldr f ys a)"
using neutr by simp
next
show "⋀aa xs.
foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a) ⟹
foldr f ((aa # xs) @ ys) a = f (foldr f (aa # xs) a) (foldr f ys a)"
using assoc by simp
qed

(*jeshorcob:
saco fuera las hipotesis porque se usan tambien en el ejercicio siguiente,
ademas la prueba queda mas corta *)

--"jeshorcob,davoremar"
definition neutr :: "['a ⇒ 'b ⇒ 'b, 'a] ⇒ bool" where
"neutr f a == (∀ x. (f a x = x))"

--"jeshorcob,davoremar"
definition assoc :: "['a ⇒ 'a ⇒ 'a] ⇒ bool" where
"assoc f == (∀ x y z. f (f x y) z = f x (f y z))"

(* Pedrosrei: esta es la versión automática del lema anterior, ¿para qué
cambias el enunciado por uno equivalente? *)

--"jeshorcob,davoremar"
lemma l2: "⟦neutr f a ; assoc f⟧
⟹ foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
by (induct xs, simp add: neutr_def, simp add: assoc_def)

text {*
---------------------------------------------------------------------
Ejercicio 8. Definir, usando foldr, la función
prod :: "nat list ⇒ nat"
tal que (prod xs) es el producto de los elementos de xs. Por ejemplo,
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
definition prod :: "nat list ⇒ nat" where
"prod xs ≡ foldr (op *) xs 1"

value "prod [2::nat,3,5] = 30" -- "True"

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar directamente (es decir, sin inducción) que
prod (xs @ ys) = prod xs * prod ys
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "prod (xs @ ys) = prod xs * prod ys"
by (simp only: prod_def, rule l2, simp add: neutr_def, simp add: assoc_def)

section {* Functiones sobre árboles *}

text {*
---------------------------------------------------------------------
Ejercicio 10. Definir el tipo de datos arbol para representar los
árboles binarios que tiene información sólo en los nodos. Por ejemplo,
el árbol
e
/ \
/ \
c g
/ \ / \
· · · ·
se representa por "N (N H c H) e (N H g H)"
---------------------------------------------------------------------
*}

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

value "N (N H c H) e (N H g H)"

text {*
---------------------------------------------------------------------
Ejercicio 11. 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 (N H c H) e (N H g H))
= [e,c,g]
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden H = []"
|"preOrden (N i x d) = x#(preOrden i @ preOrden d)"

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

text {*
---------------------------------------------------------------------
Ejercicio 12. 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 (N H c H) e (N H g H))
= [c,g,e]
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
fun postOrden :: "'a arbol ⇒ 'a list" where
"postOrden H = []"
|"postOrden (N i x d) = (postOrden i) @ (postOrden d) @ [x]"

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

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

--"jeshorcob,davoremar"
fun postOrdenAaux :: "['a arbol, 'a list] ⇒ 'a list" where
"postOrdenAaux H xs = xs"
|"postOrdenAaux (N i x d) xs = (postOrdenAaux i (postOrdenAaux d (x#xs)))"

--"jeshorcob,davoremar"
definition postOrdenA :: "'a arbol ⇒ 'a list" where
"postOrdenA a ≡ postOrdenAaux a []"

value "postOrdenA (N (N H c H) e (N H g H)) = [c,g,e]" -- "True"

text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar que
postOrdenAaux a xs = (postOrden a) @ xs
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "postOrdenAaux a xs = (postOrden a) @ xs"
by (induct a arbitrary: xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la función
foldl_arbol :: "('b => 'a => 'b) ⇒ 'b ⇒ 'a arbol ⇒ 'b" where
tal que (foldl_arbol f b a) es el plegado izquierdo del árbol a con la
operación f y elemento inicial b.
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
fun foldl_arbol :: "('b => 'a => 'b) ⇒ 'b ⇒ 'a arbol ⇒ 'b" where
"foldl_arbol f b H = b"
|"foldl_arbol f b (N i x d) = foldl_arbol f (foldl_arbol f (f b x) d) i"

text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar que
postOrdenAaux t a = foldl_arbol (λ xs x. Cons x xs) a t
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "postOrdenAaux t a = foldl_arbol (λ xs x. Cons x xs) a t"
by (induct t arbitrary: a, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 17. Definir la función
suma_arbol :: "nat arbol ⇒ nat"
tal que (suma_arbol a) es la suma de los elementos del árbol de
números naturales a.
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
fun suma_arbol :: "nat arbol ⇒ nat" where
"suma_arbol H = 0"
|"suma_arbol (N i x d) = (suma_arbol i) + x + (suma_arbol d)"

text {*
---------------------------------------------------------------------
Ejercicio 18. Demostrar que
suma_arbol a = suma (preOrden a)"
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "suma_arbol a = suma (preOrden a)"
by (induct a, simp_all)

end
</source>

Relación 8

2015-01-18T14:52:46Z

Davoremar:

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

theory R8
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, carvelcab, juacorvic"
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, carvelcab, juacorvic"
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, carvelcab, juacorvic"
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_abc1 :: "(arbol => 'a) => arbol => bool" where
"es_abc1 f H = True"
| "es_abc1 f (N a b) = ((f a = f b) ∧ (es_abc1 f a ∧ es_abc1 f b))"

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

-- "juacorvic"
fun es_abc3 :: "(arbol => 'a) => arbol => bool" where
"es_abc3 f H = True"
| "es_abc3 f (N i d) = ( es_abc3 f i ∧ es_abc3 f d ∧ f i = 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
---------------------------------------------------------------------
*}

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

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

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

(* 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, carvelcab"
lemma a1:
assumes "es_abc hojas a"
shows "hojas a = 2^(pr1 a)"
using assms
by (induct a, simp_all)

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

(* mjeshorcob: esta es la detallada*)
-- "jeshorcob,caarvelcab"
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

--"davoremar"
lemma prof_hojas:
assumes "es_abc hojas t"
shows "hojas t = 2^(profundidad t)"
using assms by (induct t, simp_all)

--"davoremar"
lemma profundidad_hojas: "es_abc profundidad t = es_abc hojas t"
by (induct t) (auto simp add: prof_hojas)

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 más
sencillo, tan sólo hay que encontrar una relación de igualdad entre
hojas y size, que para este caso es sencillo.*)

-- "Javrodviv1,carvelcab"
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"
by (induct a, simp_all add: hojasize_igualdad)

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

-- "juacorvic"
(* número de hojas es size + 1 *)
lemma l_hojas_size: "hojas x = size x + 1"
proof (induct x)
show " hojas H = size H + 1" by simp
next
fix x1 x2
assume h1: "hojas x1 = size x1 + 1"
assume h2:"hojas x2 = size x2 + 1"
have "hojas (N x1 x2) = hojas x1 + hojas x2" by simp
also have "... = size x1 + 1 + size x2 + 1" using h1 h2 by simp
also have "... = (1 + size x1 + size x2) + 1" by simp
also have "... = size (N x1 x2) + 1" by simp
finally show "hojas (N x1 x2) = size (N x1 x2) + 1" by simp
qed

-- "juacorvic"
(* usando lema anterior *)
lemma rel_size_igualdad: " es_abc size a = es_abc hojas a"
by (induct a, simp_all add: l_hojas_size)

--"davoremar"
lemma hojas_size_igualdad: "hojas x = size x + 1"
by (induct x) simp_all

-"davoremar"
lemma size_hojas: "es_abc size a = es_abc hojas a"
by (induct a) (simp_all add: hojas_size_igualdad)

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

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

--"juacorvic"
(* 1.- En apartado 7 se demuestra que:
es_abc profundidad a ⟷ es_abc hojas a
2.- En apartado 8 se demuestra que:
es_abc hojas a ⟷ es_abc size a
3.- Luego podremos demostrar usando las anteriores:
es_abc profundidad a ⟷ es_abc size a

Nota: Aplico demostración de "domcadgom" de apartado 7, que no he
conseguido reproducir *)

lemma "es_abc profundidad a = es_abc size a"
using completo1 rel_size_igualdad by simp_all

--"davoremar"
lemma "es_abc hojas a = es_abc size a"
using profundidad_hojas size_hojas[symmetric] by simp_all

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, carvelcab, juacorvic"
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

-- "juacorvic"
(* Más detallada *)
lemma "es_abc f (abc n)"
proof (induct n)
show " es_abc f (abc 0)" by simp
next
fix n
assume h1: "es_abc f (abc n)"
have "es_abc f (abc (Suc n)) = es_abc f (N (abc n) (abc n))" by simp
also have "... = (es_abc f (abc n) ∧ es_abc f (abc n) ∧
(f (abc n) = f (abc n)))" by simp
also have "... = (f (abc n) = f (abc n) )" using h1 by simp
also have "... = True " by simp
finally show "es_abc f (abc n) ⟹ es_abc f (abc (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)

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

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

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

-- "juacorvic"
fun medida :: "arbol => nat" where
"medida H = 0"
| "medida (N i d) = 0"

lemma "es_abc medida a = es_abc size a"
quickcheck
oops

(*Contraejemplo
value "es_abc medida (N H (N H H))" (*devuelve true*)
value "es_abc size (N H (N H H))" (*devuelve false*)
*)

end
</source>

Relación 10

2015-01-16T17:11:06Z

Davoremar:

<source lang="isar">
header {* R10: Formalización y argumentación con Isabelle/HOL *}

theory R10
imports Main R9
begin

text {* davoremar: Para no tener que demostrar todos los lemas de R9,
importamos este archivo poniendo arriba R9 *}

text {*
---------------------------------------------------------------------
El objetivo de esta es relación formalizar y demostrar la corrección
de los argumentos usando sólo las reglas básicas de deducción natural
de la lógica (sin usar el método auto).

· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P

· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI, mt, no_ex y no_para_todo que demostramos
a continuación.
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

lemma no_para_todo: "¬(∀x. P(x)) ⟹ ∃x. ¬P(x)"
by auto

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no está el mañana ni el ayer escrito, entonces no está el mañana
escrito.
Usar M: El mañana está escrito.
A: El ayer está escrito.
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_1_10:
assumes 1:"¬M ∧ ¬A"
shows "¬M"
proof -
show "¬M" using 1 by (rule conjunct1)
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar, y demostrar la corrección, del siguiente
argumento
Siempre que un número x es divisible por 10, acaba en 0. El número
x no acaba en 0. Por lo tanto, x no es divisible por 10.
Usar D para "el número es divisible por 10" y
C para "el número acaba en cero".
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_2_10:
assumes 1:"D ⟶ C"
shows "¬ C ⟶ ¬ D"
proof -
{assume 2:"¬ C"
have 3: "¬ D" using 1 2 by (rule mt)}
then show "¬ C ⟶ ¬ D" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no hay control de nacimientos, entonces la población crece
ilimitadamente; pero si la población crece ilimitadamente,
aumentará el índice de pobreza. Por consiguiente, si no hay control
de nacimientos, aumentará el índice de pobreza.
Usar N: Hay control de nacimientos.
P: La población crece ilimitadamente,
I: Aumentará el índice de pobreza.
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_3_10:
assumes 1:"¬ N ⟶ P" and 2:"P ⟶ I"
shows "¬N ⟶ I"
proof -
{assume 3:"¬ N"
have 4:"P" using 1 3 by (rule mp)
have 5:"I" using 2 4 by (rule mp)}
then show "¬N ⟶ I" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar, y demostrar la corrección, del siguiente
argumento
Si te llamé por teléfono, entonces recibiste mi llamada y no es
cierto que no te avisé del peligro que corrías. Por consiguiente,
como te llamé, es cierto que te avisé del peligro que corrías.
Usar T: Te llamé por teléfono.
R: Recibiste mi llamada.
P: Te avisé del peligro que corrías.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar, y demostrar la corrección, del siguiente
argumento
Si la válvula está abierta o la monitorización está preparada,
entonces se envía una señal de reconocimiento y un mensaje de
funcionamiento al controlador del ordenador. Si se envía un mensaje
de funcionamiento al controlador del ordenador o el sistema está en
estado normal, entonces se aceptan las órdenes del operador. Por lo
tanto, si la válvula está abierta, entonces se aceptan las órdenes
del operador.
Usar A : La válvula está abierta.
P : La monitorización está preparada.
R : Envía una señal de reconocimiento.
F : Envía un mensaje de funcionamiento.
N : El sistema está en estado normal.
O : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}

--"davoremar"
text{* Hay que poner X en vez de O, porque sale un error *}

lemma ej_5_10:
assumes 1:"(A ∨ P) ⟶ (R ∧ F)" and 2:"(F ∨ N) ⟶ X"
shows "A ⟶ X"
proof -
{assume 3:"A"
have 4:"A ∨ P" using 3 by (rule disjI1)
have 5:"R ∧ F" using 1 4 by (rule mp)
have 6:"F" using 5 by (rule conjunct2)
have 7:"F ∨ N" using 6 by (rule disjI1)
have 8:"X" using 2 7 by (rule mp)}
then show "A ⟶ X" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar, y demostrar la corrección, del siguiente
argumento
Cuando tanto la temperatura como la presión atmosférica permanecen
contantes, no llueve. La temperatura permanece constante. Por lo
tanto, en caso de que llueva, la presión atmosférica no permanece
constante.
Usar T para "La temperatura permanece constante",
P para "La presión atmosférica permanece constante" y
L para "Llueve".
------------------------------------------------------------------ *}

--"davoremar"
lemma aux_6:
assumes 1:"p ∨ q" and 2:"¬p"
shows "q"
using 1
proof
assume 3: "q"
then show "q" .
next
assume 4:"p"
show "q" using 2 4 by (rule notE)
qed

lemma ej_6_10:
assumes 1:"(T ∧ P) ⟶ ¬ L" and 2:"T"
shows "L ⟶ ¬ P"
proof -
{assume 3:"L"
have 4:"¬¬L" using 3 by (rule notnotI)
have 5:"¬ (T ∧ P)" using 1 4 by (rule mt)
have 6:"¬ T ∨ ¬ P" using 5 by (rule ej_10)
have 7:"¬¬ T" using 2 by (rule notnotI)
have 8:"¬ P" using 6 7 by (rule aux_6)}
then show "L ⟶ ¬ P" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar, y demostrar la corrección, del siguiente
argumento
Si el general era leal, hubiera obedecido las órdenes, y si era
inteligente las hubiera comprendido. O el general desobedeció las
órdenes o no las comprendió. Luego, el general era desleal o no era
inteligente.
Usar L: El general es leal.
Ob: El general obedece las órdenes.
I: El general es inteligente.
C: El general comprende las órdenes.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente
argumento
Me matan si no trabajo y si trabajo me matan. Me matan siempre me
matan.
Usar M: Me matan.
T: Trabajo.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente
argumento
En cierto experimento, cuando hemos empleado un fármaco A, el
paciente ha mejorado considerablemente en el caso, y sólo en el
caso, en que no se haya empleado también un fármaco B. Además, o se
ha empleado el fármaco A o se ha empleado el fármaco B. En
consecuencia, podemos afirmar que si no hemos empleado el fármaco
B, el paciente ha mejorado considerablemente.
Usar A: Hemos empleado el fármaco A.
B: Hemos empleado el fármaco B.
M: El paciente ha mejorado notablemente.
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_9_10:
assumes 1:"A ∧ (¬ B) ⟶ M" and 2:"A ∨ B"
shows "¬ B ⟶ M"
proof -
{assume 3:"¬ B"
have 4:"A" using 2 3 by (rule ej_1)
have 5:"A ∧ (¬B)" using 4 3 by (rule conjI)
have 6:"M" using 1 5 by (rule mp)}
then show "¬ B ⟶ M" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar, y demostrar la corrección, del siguiente
argumento
Si trabajo gano dinero, pero si no trabajo gozo de la vida. Sin
embargo, si trabajo no gozo de la vida, mientras que si no trabajo
no gano dinero. Por lo tanto, gozo de la vida si y sólo si no gano
dinero.
Usar p: Trabajo
q: Gano dinero.
r: Gozo de la vida.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar, y demostrar la corrección, del siguiente
argumento
Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo
haría. Si Dios fuera incapaz de evitar el mal, no sería
omnipotente; si no quisiera evitar el mal sería malévolo. Dios no
evita el mal. Si Dios existe, es omnipotente y no es
malévolo. Luego, Dios no existe.
Usar C: Dios es capaz de evitar el mal.
Q: Dios quiere evitar el mal.
Om: Dios es omnipotente.
M: Dios es malévolo.
P: Dios evita el mal.
E: Dios existe.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar, y decidir la corrección, del siguiente
argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar, y decidir la corrección, del siguiente
argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 14. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar, y decidir la corrección, del siguiente
argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar, y decidir la corrección, del siguiente
argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar, y decidir la corrección, del siguiente
argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar, y decidir la corrección, del siguiente
argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 19. Formalizar, y decidir la corrección, del siguiente
argumento
Quien intente entrar en un país y no tenga pasaporte, encontrará
algún aduanero que le impida el paso. A algunas personas
motorizadas que intentan entrar en un país le impiden el paso
únicamente personas motorizadas. Ninguna persona motorizada tiene
pasaporte. Por tanto, ciertos aduaneros están motorizados.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar, y decidir la corrección, del siguiente
argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar, y decidir la corrección, del siguiente
argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar, y decidir la corrección, del siguiente
argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar, y decidir la corrección, del siguiente
argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar, y decidir la corrección, del siguiente
argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 25. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 26. Formalizar, y decidir la corrección, del siguiente
argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Formalizar, y decidir la corrección, del siguiente
argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 28. Formalizar, y decidir la corrección, del siguiente
argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Formalizar, y decidir la corrección, del siguiente
argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 30. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar, y decidir la corrección, del
siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. Formalizar, y decidir la corrección, del siguiente
argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 32. Formalizar, y decidir la corrección, del siguiente
argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 33. Formalizar, y decidir la corrección, del siguiente
argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 34. Formalizar, y decidir la corrección, del siguiente
argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 35. Formalizar, y decidir la corrección, del siguiente
argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 36. Formalizar, y decidir la corrección, del siguiente
argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 37. Formalizar, y decidir la corrección, del siguiente
argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 38. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 39. Formalizar, y decidir la corrección, del siguiente
argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 40. Formalizar, y decidir la corrección, del siguiente
argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 41. Formalizar, y decidir la corrección, del siguiente
argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 42. Formalizar, y decidir la corrección, del siguiente
argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 43. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 44. Formalizar, y decidir la corrección, del siguiente
argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 45. Formalizar, y decidir la corrección, del siguiente
argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 46. Formalizar, y decidir la corrección, del siguiente
argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 47. Formalizar, y decidir la corrección, del siguiente
argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}

end
</source>

Relación 10

2015-01-16T16:04:18Z

Davoremar:

<source lang="isar">
header {* R10: Formalización y argumentación con Isabelle/HOL *}

theory R10
imports Main R9
begin

text {* davoremar: Para no tener que demostrar todos los lemas de R9,
importamos este archivo poniendo arriba R9 *}

text {*
---------------------------------------------------------------------
El objetivo de esta es relación formalizar y demostrar la corrección
de los argumentos usando sólo las reglas básicas de deducción natural
de la lógica (sin usar el método auto).

· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P

· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI, mt, no_ex y no_para_todo que demostramos
a continuación.
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

lemma no_para_todo: "¬(∀x. P(x)) ⟹ ∃x. ¬P(x)"
by auto

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no está el mañana ni el ayer escrito, entonces no está el mañana
escrito.
Usar M: El mañana está escrito.
A: El ayer está escrito.
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_1_10:
assumes 1:"¬M ∧ ¬A"
shows "¬M"
proof -
show "¬M" using 1 by (rule conjunct1)
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar, y demostrar la corrección, del siguiente
argumento
Siempre que un número x es divisible por 10, acaba en 0. El número
x no acaba en 0. Por lo tanto, x no es divisible por 10.
Usar D para "el número es divisible por 10" y
C para "el número acaba en cero".
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_2_10:
assumes 1:"D ⟶ C"
shows "¬ C ⟶ ¬ D"
proof -
{assume 2:"¬ C"
have 3: "¬ D" using 1 2 by (rule mt)}
then show "¬ C ⟶ ¬ D" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no hay control de nacimientos, entonces la población crece
ilimitadamente; pero si la población crece ilimitadamente,
aumentará el índice de pobreza. Por consiguiente, si no hay control
de nacimientos, aumentará el índice de pobreza.
Usar N: Hay control de nacimientos.
P: La población crece ilimitadamente,
I: Aumentará el índice de pobreza.
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_3_10:
assumes 1:"¬ N ⟶ P" and 2:"P ⟶ I"
shows "¬N ⟶ I"
proof -
{assume 3:"¬ N"
have 4:"P" using 1 3 by (rule mp)
have 5:"I" using 2 4 by (rule mp)}
then show "¬N ⟶ I" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar, y demostrar la corrección, del siguiente
argumento
Si te llamé por teléfono, entonces recibiste mi llamada y no es
cierto que no te avisé del peligro que corrías. Por consiguiente,
como te llamé, es cierto que te avisé del peligro que corrías.
Usar T: Te llamé por teléfono.
R: Recibiste mi llamada.
P: Te avisé del peligro que corrías.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar, y demostrar la corrección, del siguiente
argumento
Si la válvula está abierta o la monitorización está preparada,
entonces se envía una señal de reconocimiento y un mensaje de
funcionamiento al controlador del ordenador. Si se envía un mensaje
de funcionamiento al controlador del ordenador o el sistema está en
estado normal, entonces se aceptan las órdenes del operador. Por lo
tanto, si la válvula está abierta, entonces se aceptan las órdenes
del operador.
Usar A : La válvula está abierta.
P : La monitorización está preparada.
R : Envía una señal de reconocimiento.
F : Envía un mensaje de funcionamiento.
N : El sistema está en estado normal.
O : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}

--"davoremar"
text{* Hay que poner X en vez de O, porque sale un error *}

lemma ej_5_10:
assumes 1:"(A ∨ P) ⟶ (R ∧ F)" and 2:"(F ∨ N) ⟶ X"
shows "A ⟶ X"
proof -
{assume 3:"A"
have 4:"A ∨ P" using 3 by (rule disjI1)
have 5:"R ∧ F" using 1 4 by (rule mp)
have 6:"F" using 5 by (rule conjunct2)
have 7:"F ∨ N" using 6 by (rule disjI1)
have 8:"X" using 2 7 by (rule mp)}
then show "A ⟶ X" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar, y demostrar la corrección, del siguiente
argumento
Cuando tanto la temperatura como la presión atmosférica permanecen
contantes, no llueve. La temperatura permanece constante. Por lo
tanto, en caso de que llueva, la presión atmosférica no permanece
constante.
Usar T para "La temperatura permanece constante",
P para "La presión atmosférica permanece constante" y
L para "Llueve".
------------------------------------------------------------------ *}

--"davoremar"
lemma aux_6:
assumes 1:"p ∨ q" and 2:"¬p"
shows "q"
using 1
proof
assume 3: "q"
then show "q" .
next
assume 4:"p"
show "q" using 2 4 by (rule notE)
qed

lemma ej_6_10:
assumes 1:"(T ∧ P) ⟶ ¬ L" and 2:"T"
shows "L ⟶ ¬ P"
proof -
{assume 3:"L"
have 4:"¬¬L" using 3 by (rule notnotI)
have 5:"¬ (T ∧ P)" using 1 4 by (rule mt)
have 6:"¬ T ∨ ¬ P" using 5 by (rule ej_10)
have 7:"¬¬ T" using 2 by (rule notnotI)
have 8:"¬ P" using 6 7 by (rule aux_6)}
then show "L ⟶ ¬ P" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar, y demostrar la corrección, del siguiente
argumento
Si el general era leal, hubiera obedecido las órdenes, y si era
inteligente las hubiera comprendido. O el general desobedeció las
órdenes o no las comprendió. Luego, el general era desleal o no era
inteligente.
Usar L: El general es leal.
Ob: El general obedece las órdenes.
I: El general es inteligente.
C: El general comprende las órdenes.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente
argumento
Me matan si no trabajo y si trabajo me matan. Me matan siempre me
matan.
Usar M: Me matan.
T: Trabajo.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente
argumento
En cierto experimento, cuando hemos empleado un fármaco A, el
paciente ha mejorado considerablemente en el caso, y sólo en el
caso, en que no se haya empleado también un fármaco B. Además, o se
ha empleado el fármaco A o se ha empleado el fármaco B. En
consecuencia, podemos afirmar que si no hemos empleado el fármaco
B, el paciente ha mejorado considerablemente.
Usar A: Hemos empleado el fármaco A.
B: Hemos empleado el fármaco B.
M: El paciente ha mejorado notablemente.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar, y demostrar la corrección, del siguiente
argumento
Si trabajo gano dinero, pero si no trabajo gozo de la vida. Sin
embargo, si trabajo no gozo de la vida, mientras que si no trabajo
no gano dinero. Por lo tanto, gozo de la vida si y sólo si no gano
dinero.
Usar p: Trabajo
q: Gano dinero.
r: Gozo de la vida.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar, y demostrar la corrección, del siguiente
argumento
Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo
haría. Si Dios fuera incapaz de evitar el mal, no sería
omnipotente; si no quisiera evitar el mal sería malévolo. Dios no
evita el mal. Si Dios existe, es omnipotente y no es
malévolo. Luego, Dios no existe.
Usar C: Dios es capaz de evitar el mal.
Q: Dios quiere evitar el mal.
Om: Dios es omnipotente.
M: Dios es malévolo.
P: Dios evita el mal.
E: Dios existe.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar, y decidir la corrección, del siguiente
argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar, y decidir la corrección, del siguiente
argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 14. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar, y decidir la corrección, del siguiente
argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar, y decidir la corrección, del siguiente
argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar, y decidir la corrección, del siguiente
argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar, y decidir la corrección, del siguiente
argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 19. Formalizar, y decidir la corrección, del siguiente
argumento
Quien intente entrar en un país y no tenga pasaporte, encontrará
algún aduanero que le impida el paso. A algunas personas
motorizadas que intentan entrar en un país le impiden el paso
únicamente personas motorizadas. Ninguna persona motorizada tiene
pasaporte. Por tanto, ciertos aduaneros están motorizados.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar, y decidir la corrección, del siguiente
argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar, y decidir la corrección, del siguiente
argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar, y decidir la corrección, del siguiente
argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar, y decidir la corrección, del siguiente
argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar, y decidir la corrección, del siguiente
argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 25. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 26. Formalizar, y decidir la corrección, del siguiente
argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Formalizar, y decidir la corrección, del siguiente
argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 28. Formalizar, y decidir la corrección, del siguiente
argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Formalizar, y decidir la corrección, del siguiente
argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 30. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar, y decidir la corrección, del
siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. Formalizar, y decidir la corrección, del siguiente
argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 32. Formalizar, y decidir la corrección, del siguiente
argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 33. Formalizar, y decidir la corrección, del siguiente
argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 34. Formalizar, y decidir la corrección, del siguiente
argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 35. Formalizar, y decidir la corrección, del siguiente
argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 36. Formalizar, y decidir la corrección, del siguiente
argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 37. Formalizar, y decidir la corrección, del siguiente
argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 38. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 39. Formalizar, y decidir la corrección, del siguiente
argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 40. Formalizar, y decidir la corrección, del siguiente
argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 41. Formalizar, y decidir la corrección, del siguiente
argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 42. Formalizar, y decidir la corrección, del siguiente
argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 43. Formalizar, y decidir la corrección, del siguiente
argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 44. Formalizar, y decidir la corrección, del siguiente
argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 45. Formalizar, y decidir la corrección, del siguiente
argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 46. Formalizar, y decidir la corrección, del siguiente
argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 47. Formalizar, y decidir la corrección, del siguiente
argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}

end
</source>

Relación 11

2015-01-16T16:00:22Z

Davoremar:

<source lang="isar">
header {* R11: Plegados de listas y de árboles *}

theory R11
imports Main
begin

section {* Nuevas funciones sobre listas *}

text {*
Nota. En esta relación se usará la función suma tal que (suma xs) es
la suma de los elementos de xs, definida por
*}

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

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

text {*
Las funciones de plegado, foldr y foldl, están definidas en la teoría
List.thy por
foldr :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a list ⇒ 'b ⇒ 'b"
foldr f [] = id
foldr f (x # xs) = f x ∘ foldr f xs

foldl :: "('b ⇒ 'a ⇒ 'b) ⇒ 'b ⇒ 'a list ⇒ 'b"
foldl f a [] = a
foldl f a (x # xs) = foldl f (f a x) xs"

Por ejemplo,
foldr (op +) [a,b,c] d = a + (b + (c + d))
foldl (op +) d [a,b,c] = ((d + a) + b) + c
foldr (op -) [9,4,2] (0::int) = 7
foldl (op -) (0::int) [9,4,2] = -15
*}

value "foldr (op +) [a,b,c] d" -- "= a + (b + (c + d))"
value "foldl (op +) d [a,b,c]" -- "= ((d + a) + b) + c"
value "foldr (op -) [9,4,2] (0::int)" -- "= 7"
value "foldl (op -) (0::int) [9,4,2]" -- "= -15"

text {*
---------------------------------------------------------------------
Ejercicio 1. Demostrar que
suma xs = foldr (op +) xs 0
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma suma_foldr: "suma xs = foldr (op +) xs 0"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 2. Demostrar que
length xs = foldr (λ x res. 1 + res) xs 0
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma length_foldr: "length xs = foldr (λ x res. 1 + res) xs 0"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 3. La aplicación repetida de foldr y map tiene el
inconveniente de que la lista se recorre varias veces. Sin embargo, es
suficiente recorrerla una vez como se muestra en el siguiente ejemplo,
suma (map (λx. x + 3) xs) = foldr h xs b
Determinar los valores de h y b para que se verifique la igualdad
anterior y demostrarla.
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "suma (map (λx. x + 3) xs) = foldr (λ x y. x+y+3) xs 0"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 4. Generalizar el resultado anterior; es decir determinar
los valores de h y b para que se verifique la igualdad
foldr g (map f xs) a = foldr h xs b
y demostrarla.
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "foldr g (map f xs) a = foldr (g∘f) xs a"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 5. La siguiente función invierte una lista en tiempo lineal
fun inversa_ac :: "['a list, 'a list] ⇒ 'a list" where
"inversa_ac [] ys = ys"
| "inversa_ac (x#xs) ys = (inversa_ac xs (x#ys))"

definition inversa_ac :: "'a list ⇒ 'a list" where
"inversa_ac xs ≡ inversa_ac_aux xs []"
Por ejemplo,
inversa_ac [a,d,b,c] = [c, b, d, a]
Demostrar que inversa_ac se puede definir unsando foldl.
---------------------------------------------------------------------
*}

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

--"jeshorcob,davoremar"
definition inversa_ac :: "'a list ⇒ 'a list" where
"inversa_ac xs ≡ inversa_ac_aux xs []"

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

--"jeshorcob"
lemma inversa_ac_aux_foldl:
"inversa_ac_aux xs a = foldl (λ ys x. x#ys) a xs"
by (induct xs arbitrary: a, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar la siguiente propiedad distributiva de la suma
sobre la concatenación:
suma (xs @ ys) = suma xs + suma ys
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma suma_append [simp]:
"suma (xs @ ys) = suma xs + suma ys"
by (induct xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar una propiedad similar para foldr
foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)
En este caso, hay que restringir el resultado teniendo en cuenta
propiedades algebraicas de f y a.
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma l1:
assumes a1: "(∀ x. (f a x = x))" and
a2: "(∀x y z. f (f x y) z = f x (f y z))"
shows "foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
proof (induct xs)
show "foldr f ([] @ ys) a = f (foldr f [] a) (foldr f ys a)"
using a1 by simp
next
show "⋀aa xs.
foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a) ⟹
foldr f ((aa # xs) @ ys) a = f (foldr f (aa # xs) a) (foldr f ys a)"
using a2 by simp
qed

(*jeshorcob:
saco fuera las hipotesis porque se usan tambien en el ejercicio siguiente,
ademas la prueba queda mas corta *)

--"jeshorcob"
definition a1 :: "['a ⇒ 'b ⇒ 'b, 'a] ⇒ bool" where
"a1 f a == (∀ x. (f a x = x))"

--"jeshorcob"
definition a2 :: "['a ⇒ 'a ⇒ 'a] ⇒ bool" where
"a2 f == (∀ x y z. f (f x y) z = f x (f y z))"

--"jeshorcob"
lemma l2: "⟦a1 f a ; a2 f⟧
⟹ foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"
by (induct xs, simp add: a1_def, simp add: a2_def)

text {*
---------------------------------------------------------------------
Ejercicio 8. Definir, usando foldr, la función
prod :: "nat list ⇒ nat"
tal que (prod xs) es el producto de los elementos de xs. Por ejemplo,
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
definition prod :: "nat list ⇒ nat" where
"prod xs ≡ foldr (op *) xs 1"

value "prod [2::nat,3,5] = 30" -- "True"

text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar directamente (es decir, sin inducción) que
prod (xs @ ys) = prod xs * prod ys
---------------------------------------------------------------------
*}

--"jeshorcob"
lemma "prod (xs @ ys) = prod xs * prod ys"
by (simp only: prod_def, rule l2, simp add: a1_def, simp add: a2_def)

section {* Functiones sobre árboles *}

text {*
---------------------------------------------------------------------
Ejercicio 10. Definir el tipo de datos arbol para representar los
árboles binarios que tiene información sólo en los nodos. Por ejemplo,
el árbol
e
/ \
/ \
c g
/ \ / \
· · · ·
se representa por "N (N H c H) e (N H g H)"
---------------------------------------------------------------------
*}

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

value "N (N H c H) e (N H g H)"

text {*
---------------------------------------------------------------------
Ejercicio 11. 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 (N H c H) e (N H g H))
= [e,c,g]
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden H = []"
|"preOrden (N i x d) = x#(preOrden i @ preOrden d)"

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

text {*
---------------------------------------------------------------------
Ejercicio 12. 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 (N H c H) e (N H g H))
= [c,g,e]
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
fun postOrden :: "'a arbol ⇒ 'a list" where
"postOrden H = []"
|"postOrden (N i x d) = (postOrden i) @ (postOrden d) @ [x]"

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

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

--"jeshorcob,davoremar"
fun postOrdenAaux :: "['a arbol, 'a list] ⇒ 'a list" where
"postOrdenAaux H xs = xs"
|"postOrdenAaux (N i x d) xs = (postOrdenAaux i (postOrdenAaux d (x#xs)))"

--"jeshorcob,davoremar"
definition postOrdenA :: "'a arbol ⇒ 'a list" where
"postOrdenA a ≡ postOrdenAaux a []"

value "postOrdenA (N (N H c H) e (N H g H)) = [c,g,e]" -- "True"

text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar que
postOrdenAaux a xs = (postOrden a) @ xs
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "postOrdenAaux a xs = (postOrden a) @ xs"
by (induct a arbitrary: xs, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 15. Definir la función
foldl_arbol :: "('b => 'a => 'b) ⇒ 'b ⇒ 'a arbol ⇒ 'b" where
tal que (foldl_arbol f b a) es el plegado izquierdo del árbol a con la
operación f y elemento inicial b.
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
fun foldl_arbol :: "('b => 'a => 'b) ⇒ 'b ⇒ 'a arbol ⇒ 'b" where
"foldl_arbol f b H = b"
|"foldl_arbol f b (N i x d) = foldl_arbol f (foldl_arbol f (f b x) d) i"

text {*
---------------------------------------------------------------------
Ejercicio 16. Demostrar que
postOrdenAaux t a = foldl_arbol (λ xs x. Cons x xs) a t
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "postOrdenAaux t a = foldl_arbol (λ xs x. Cons x xs) a t"
by (induct t arbitrary: a, simp_all)

text {*
---------------------------------------------------------------------
Ejercicio 17. Definir la función
suma_arbol :: "nat arbol ⇒ nat"
tal que (suma_arbol a) es la suma de los elementos del árbol de
números naturales a.
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
fun suma_arbol :: "nat arbol ⇒ nat" where
"suma_arbol H = 0"
|"suma_arbol (N i x d) = (suma_arbol i) + x + (suma_arbol d)"

text {*
---------------------------------------------------------------------
Ejercicio 18. Demostrar que
suma_arbol a = suma (preOrden a)"
---------------------------------------------------------------------
*}

--"jeshorcob,davoremar"
lemma "suma_arbol a = suma (preOrden a)"
by (induct a, simp_all)

end
</source>

Relación 9

2014-12-24T15:55:33Z

Davoremar:

<source lang="isar">
header {* R9: Deducción natural en Isabelle/HOL *}

theory R9
imports Main
begin

text {*
Demostrar o refutar los siguientes lemas usando sólo las reglas
básicas de deducción natural de la lógica proposicional, de los
cuantificadores y de la igualdad:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P

· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
*}

text {*
Se usarán las reglas notnotI, mt y not_ex que demostramos a continuación.
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ∨ q, ¬q ⊢ p
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_1:
assumes 1:"p ∨ q" and 2:"¬q"
shows "p"
using 1
proof
assume 3: "p"
then show "p" .
next
assume 4:"q"
show "p" using 2 4 by (rule notE)
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_2:
assumes 1:"p ∧ q"
shows "¬(¬p ∨ ¬ q)"
proof
assume 2:"¬p ∨ ¬q"
show "False"
using 2
proof
assume 3:"¬p"
have 4:"p" using 1 by (rule conjunct1)
show "False" using 3 4 by (rule notE)
next
assume 5:"¬q"
have 6:"q" using 1 by (rule conjunct2)
show "False" using 5 6 by (rule notE)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_3:
assumes 1:"¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
{assume 2:"p"
have 3:"p ∨ q" using 2 by (rule disjI1)
also have 4:"False" using 1 3 by (rule notE)}
then show "¬p" ..
next
{assume 5:"q"
have 6:"p ∨ q" using 5 by (rule disjI2)
also have 7:"False" using 1 6 by (rule notE)}
then show "¬q" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_4:
assumes 1:"¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume 2:"p ∨ q"
show "False"
using 2
proof
assume 3:"p"
have 4:"¬p" using 1 by (rule conjunct1)
then show "False" using 3 ..
next
assume 5:"q"
have 6:"¬q" using 1 by (rule conjunct2)
then show "False" using 5 ..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_5:
assumes 1:"¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume 2:"p ∧ q"
have 3:"p" using 2 by (rule conjunct1)
have 4:"q" using 2 by (rule conjunct2)
show "False"
using 1
proof
assume 5:"¬p"
then show "False" using 3 ..
next
assume 6:"¬q"
then show "False" using 4 ..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_6:
shows "((p ⟶ q) ⟶ p ) ⟶ p"
proof
assume 1:"(p ⟶ q) ⟶ p"
show "p"
proof (rule ccontr)
assume 2:"¬p"
have 3:"¬(p ⟶ q)" using 1 2 by (rule mt)
{assume 4:"p"
have "False" using 2 4 ..
then have "q" ..}
then have 5:"p ⟶ q" ..
show "False" using 3 5 ..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_7:
assumes 1:"¬q ⟶ ¬p"
shows "p ⟶ q"
proof -
{assume 2:"p"
then have 3:"¬¬p" by (rule notnotI)
have 4:"¬¬q" using 1 3 by (rule mt)
then have 5:"q" by (rule notnotD)}
then show "p ⟶ q" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_8:
assumes 1:"¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
{assume 2:"¬(p ∨ q)"
have 3:"¬p ∧ ¬q" using 2 by (rule ej_3)
also have "False" using 1 3 ..}
then show "p ∨ q" by (rule ccontr)
qed

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_9:
assumes 1:"¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
have 2:"¬¬p ∧ ¬¬q" using 1 by (rule ej_3)
have 3:"¬¬p" using 2 by (rule conjunct1)
have 4:"¬¬q" using 2 by (rule conjunct2)
show "p" using 3 by (rule notnotD)
show "q" using 4 by (rule notnotD)
qed

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_10:
assumes 1:"¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
{assume 2:"¬(¬p ∨ ¬q)"
have 3:"p ∧ q" using 2 by (rule ej_9)
have "False" using 1 3 ..}
then show "¬p ∨ ¬q" by (rule ccontr)
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_11:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
have 1:"¬(p ⟶ q) ∨ (p ⟶ q)" ..
show "(p ⟶ q) ∨ (q ⟶ p)"
using 1
proof
assume 2:"p ⟶ q"
then show "(p ⟶ q) ∨ (q ⟶ p)" ..
next
{assume 3:"¬(p ⟶ q)"
{assume 4:"q"
{assume 5:"p"
have 6:"q" using 4 .}
then have 7:"p ⟶ q" ..
with 3 have "False" ..
then have "p" ..}
then have "q ⟶ p" ..
then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
{∀x y z. R x y ∧ R y z ⟶ R x z,
∀x. ¬(R x x)}
⊢ ∀x y. R x y ⟶ ¬(R y x)
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_14:
assumes 1:"∀x. ∃y. P x y"
shows "∃y. ∀x. P x y"
quickcheck
oops

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar o refutar
(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_15:
assumes 1:"∃y. ∀x. P x y"
shows "∀x. ∃y. P x y"
proof -
{fix a
obtain b where 2:"∀x. P x b" using 1 ..
have "P a b" using 2 ..
then have "∃y. P a y" ..}
then show "∀x. ∃y. P x y" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)⟧
⊢ ∃z. P (f a) z (f (f a))
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_16:
assumes 1:"∀x. P a x x" and 2:"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
proof -
have 4:"P a (f a) (f a)" using 1 ..
also have 5:"∀y z. P a y z ⟶ P (f a) y (f z)" using 2 ..
then have 6:"∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
then have 7:"P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
also have 8:"P (f a) (f a) (f (f a))" using 7 4 by (rule mp)
then show "∃z. P (f a) z (f (f a))" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar o refutar
{∀y. Q a y,
∀x y. Q x y ⟶ Q (s x) (s y)}
⊢ ∃z. Qa z ∧ Q z (s (s a))
------------------------------------------------------------------ *}

--"davoremar"
lemma ej_17:
assumes 1:"∀y. Q a y" and 2:"∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
proof
have 3:"Q a (s a)" using 1 ..
also have 4:"∀y. Q a y ⟶ Q (s a) (s y)" using 2 ..
then have 5:"Q a (s a) ⟶ Q (s a) (s (s a))" ..
then have 6:"Q (s a) (s (s a))" using 3 by (rule mp)
show "Q a (s a) ∧ Q (s a) (s (s a))" using 3 6 by (rule conjI)
qed

end
</source>

Relación 8

2014-12-10T17:36:24Z

Davoremar:

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

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

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

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"
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"
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"
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-11-30T15:53:42Z

Davoremar:

<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"
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"
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"
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"
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"
lemma "preOrden (espejo a) = rev (postOrden a)"
by (induct a, simp_all)

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

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

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

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

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

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

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

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"
fun raiz :: "'a arbol ⇒ 'a" where
"raiz (H x) = x"
|"raiz (N x _ _ ) = x"

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"
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"
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"
(*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"
theorem "last (inOrden a) = extremo_derecha a"
by (induct a, simp_all add: a1)

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

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

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

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

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

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

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

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

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

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

end
</source>

Relación 6

2014-11-23T21:42:11Z

Davoremar:

<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"
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"
lemma sust_append:
"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
by (induct xs) auto

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

--"jeshorcob,davoremar"
lemma rev_sust:
"rev(sust x y zs) = sust x y (rev zs)"
by (induct zs, simp_all 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"
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"
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"
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"
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"
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"
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"
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"
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"
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)

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

--"jeshorcob,davoremar"
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"
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"
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"
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"
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"
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"
lemma "rev (borraTodas x xs) = borraTodas x (rev xs)"
by (induct xs, simp_all add: borraTodas_append)

end
</source>

Relación 5

2014-11-19T15:04:22Z

Davoremar:

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

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

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"

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

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"
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"
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"
(*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"
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"
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"
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"
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::1,1,1,1,1,1].
Esto no se reduce:
have "length (borraDuplicados (a # xs)) ≤ length (borraDuplicados xs)" by simp
*)

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

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

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

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

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"
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-14T13:30:50Z

Davoremar:

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

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"

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

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

-- "davoremar"

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"

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

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

-- "davoremar"

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-09T17:53:53Z

Davoremar:

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

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2*n+1) + sumaImpares 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"

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"

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"

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"

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

-- "davoremar"

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"

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"

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"

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

-- "davoremar"

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

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"

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

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

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

-- "davoremar"

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

-- "davoremar"

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

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"

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

-- "davoremar"

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
finally show "amplia (x#xs) y = (x#xs) @ [y]" by simp
qed

end
</source>

Relación 1

2014-11-04T20:21:04Z

Davoremar:

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

theory R1
imports Main
begin

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

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

value "factorial 4" -- "24"

-- "juacorvic"
fun factorial2 :: "nat ⇒ nat" where
"factorial2 0 = 1"
| "factorial2 n = n * factorial2 (n - 1)"

value "factorial 4" -- "24"

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

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

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

-- "juacorvic"
fun longitud2 :: "'a list ⇒ nat" where
"longitud2 [] = 0"
| "longitud2 xs = 1 + longitud2 (tl (xs))"

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

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

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

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

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

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

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

-- "juacorvic"
fun inversa3 :: "'a list ⇒ 'a list" where
"inversa3 [] = []"
| "inversa3 xs = inversa3(tl xs)@ (hd xs#[])"

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

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

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

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

-- "juacorvic"
fun repite2 :: "nat ⇒ 'a ⇒ 'a list" where
"repite2 0 x = []"
| "repite2 n x = (x # (repite2 (n - 1) x ) )"

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

-- "davoremar"
fun repite3 :: "nat ⇒ 'a ⇒ 'a list" where
"repite3 0 x = []"
| "repite (Suc n) x = (repite n x) @ [x]"

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

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

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

-- "juacorvic"
fun conc2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc2 xs ys = xs @ ys"

-- "juacorvic"
fun conc3:: "'a list ⇒ 'a list ⇒ 'a list" where
"conc3 [] ys = ys"
| "conc3 xs ys = (hd xs)#(conc3 (tl xs) ys)"

-- "davoremar"
fun conc4 :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc xs [] = xs"
| "conc xs (y#ys) = conc (cs @ [y]) ys"

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

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

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

-- "juacorvic"
fun coge2 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge2 0 xs = []"
| "coge2 n xs = (hd xs) # coge2 (n - 1) (tl xs)"

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

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

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

-- "juacorvic"
fun elimina2 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina2 0 xs = xs"
| "elimina2 n xs = elimina2 (n - 1 ) (tl xs)"

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

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

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

-- "juacorvic"
fun esVacia2 :: "'a list ⇒ bool" where
"esVacia2 xs = (if xs=[] then True
else False)"

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

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

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

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

-- "juacorvic"
fun inversaAcAux2 :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux2 [] ys = ys"
| "inversaAcAux2 xs ys = inversaAcAux2 (tl xs) ((hd xs) # ys)"
fun inversaAc2 :: "'a list ⇒ 'a list" where
"inversaAc2 xs = inversaAcAux2 xs []"

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

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

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

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

-- "juarcorvic"
fun sum3 :: "nat list ⇒ nat" where
"sum3 [] = 0"
| "sum3 xs = (hd xs) + sum3 (tl xs)"

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

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

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

-- "juacorvic"
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f xs = (f (hd xs)) # (map f (tl xs))"

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

end
</source>