text ‹Ejercicio 5 de Lógica Matemática y Fundamentos (2-junio-2020)›
theory ej_2jun
imports Main
begin
text ‹
Apellidos:
Nombre:
›
text ‹Sustituye la palabra ej_2jun por tu usuario de la Universidad de
Sevilla y graba el fichero con dicho usuario.thy›
text ‹Nota 1: El tiempo de realización del ejercicio, incluida su
entrega en la PEV, es de 15:30 a 17:30.›
text ‹Nota 2: Además de las reglas básicas de deducción natural de la
lógica proposicional y de primer orden, también se pueden usar las
reglas notnotI y mt que demostramos a continuación.›
text ‹Nota 3: En el proceso de corrección del ejercicio, y antes de la
publicación de las calificaciones del mismo, se podrá requerir
aclaraciones sobre su respuesta. Estas aclaraciones se harán por
alguno de los procedimientos virtuales previstos en la PEV. ›
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
text ‹-----------------------------------------------------------------
Ejercicio 1. Consideremos el árbol binario definido por
datatype 'a arbol = H
| N "'a" "'a arbol" "'a arbol"
Por ejemplo, el árbol
e
/ \
/ \
c g
/ \ / \
se representa por "N e (N c H H) (N g H H)".
Se define las funciones
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden H = []"
| "preOrden (N x i d) = x#(preOrden i)@(preOrden d)"
fun preOrdenAaux :: "'a arbol ⇒ 'a list ⇒ 'a list" where
"preOrdenAaux H xs = xs"
| "preOrdenAaux (N x i d) xs = (preOrdenAaux d (preOrdenAaux i (xs@[x])))"
definition preOrdenA :: "'a arbol ⇒ 'a list" where
"preOrdenA a ≡ preOrdenAaux a []"
tales que
+ (preOrden a) es el recorrido post orden del árbol a. Por
ejemplo,
preOrden (N e (N c H H) (N g H H)) = [c, g, e]
+ (preOrdenA a) es el recorrido post orden del árbol a, calculado
con la función auxiliar preOrdenAaux que usa un acumulador. Por
ejemplo,
preOrdenA (N e (N c H H) (N g H H)) = [c, g, e]
Demostrar detalladamente que las funciones preOrden y preOrdenA son
equivalentes; es decir,
preOrdenA a = preOrden a
-------------------------------------------------------------------›
section ‹Definiciones›
datatype 'a arbol = H
| N "'a" "'a arbol" "'a arbol"
fun preOrden :: "'a arbol ⇒ 'a list" where
"preOrden H = []"
| "preOrden (N x i d) = x#(preOrden i)@(preOrden d)"
fun preOrdenAaux :: "'a arbol ⇒ 'a list ⇒ 'a list" where
"preOrdenAaux H xs = xs"
| "preOrdenAaux (N x i d) xs = (preOrdenAaux d (preOrdenAaux i (xs@[x])))"
definition preOrdenA :: "'a arbol ⇒ 'a list" where
"preOrdenA a ≡ preOrdenAaux a []"
― ‹Lema preOrdenAux›
― ‹Demostración en lenguaje natural›
― ‹Demostración detallada de preOrdenAux›
lemma preOrdenAux:
"preOrdenAaux a xs = xs @ preOrden a"
oops
― ‹Demostraciones de preOrdenA›
― ‹Demostración en lenguaje natural›
― ‹Demostración detallada›
theorem preOrdenA:
"preOrdenA a = preOrden a"
oops
text ‹------------------------------------------------------------------
Ejercicio 2. Sea G un grupo. Demostrar detalladamente lo siguiente:
x = y ⋅ z^ si y sólo si y = x ⋅ z
Nota: No usar ninguno de los métodos automáticos: auto, blast, force,
fast, arith o metis
------------------------------------------------------------------ ›
locale grupo =
fixes prod :: "['a, 'a] ⇒ 'a" (infixl "⋅" 70)
and neutro ("𝟭")
and inverso ("_^" [100] 100)
assumes asociativa: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
and neutro_i: "𝟭 ⋅ x = x"
and neutro_d: "x ⋅ 𝟭 = x"
and inverso_i: "x^ ⋅ x = 𝟭"
(* Notas sobre notación:
* El producto es ⋅ y se escribe con \ cdot (sin espacio entre ellos).
* El neutro es 𝟭 y se escribe con \ y one (sin espacio entre ellos).
* El inverso de x es x^ y se escribe pulsando 2 veces en ^. *)
context grupo
begin
― ‹Demostración detallada›
lemma
"x = y ⋅ z^ ⟷ y = x ⋅ z"
oops
end
end