Mjoseh: Protegió «T5-1» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-06-17T15:36:03Z

Protegió «T5-1» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « text ‹Ejercicio 5 de Lógica Matemática y Fundamentos (2-junio-2020)› theory ej_2_jun imports Main begin text ‹ Apellidos: Nombre:…»

2020-06-17T15:35:53Z

Página creada con «<source lang = "isabelle"> text ‹Ejercicio 5 de Lógica Matemática y Fundamentos (2-junio-2020)› theory ej_2_jun imports Main begin text ‹ Apellidos: Nombre:…»

Página nueva

<source lang = "isabelle">

text ‹Ejercicio 5 de Lógica Matemática y Fundamentos (2-junio-2020)›

theory ej_2_jun
imports Main
begin

text ‹
Apellidos:
Nombre:
›

text ‹Sustituye la palabra ej_2_jun 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 nHojas :: "'a arbol ⇒ nat" where
"nHojas H = 1"
| "nHojas (N x i d) = nHojas i + nHojas d"

fun nHojasAaux :: "'a arbol ⇒ nat ⇒ nat" where
"nHojasAaux H n = n + 1"
| "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)"

definition nHojasA :: "'a arbol ⇒ nat" where
"nHojasA a ≡ nHojasAaux a 0"
tales que
+ (nHojas a) es el número de hojas del árbol a. Por ejemplo,
nHojas (N e (N c H H) (N g H H)) = 4
+ (nHojasAA a) es el número de hojas del árbol a, calculado
con la función auxiliar nHojasAaux que el el segundo argumento va
acumulando el resultado. Por ejemplo,
nHojasA (N e (N c H H) (N g H H)) = 4

Demostrar detalladamente que las funciones nHojas y nHojasA son
equivalentes; es decir,
nHojasA a = nHojas a
-------------------------------------------------------------------›

section ‹Definiciones›

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

fun nHojas :: "'a arbol ⇒ nat" where
"nHojas H = 1"
| "nHojas (N x i d) = nHojas i + nHojas d"

fun nHojasAaux :: "'a arbol ⇒ nat ⇒ nat" where
"nHojasAaux H n = n + 1"
| "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)"

definition nHojasA :: "'a arbol ⇒ nat" where
"nHojasA a ≡ nHojasAaux a 0"

value "nHojas (N e (N c H H) (N g H H)) = 4"
value "nHojasA (N e (N c H H) (N g H H)) = 4"

― ‹Lema nHojasAux›

― ‹Demostración en lenguaje natural›

― ‹Demostración detallada de nHojasAux›

lemma nHojasAux:
"nHojasAaux a n = (nHojas a) + n"
oops

― ‹Demostraciones de nHojasA›

― ‹Demostración en lenguaje natural›

― ‹Demostración detallada›

theorem nHojasA:
"nHojasA a = nHojas a"
oops

text ‹------------------------------------------------------------------
Ejercicio 2. Sea G un grupo. Demostrar detalladamente lo siguiente:
x = y^ ⋅ z si y sólo si z = y ⋅ x

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 ⟷ z = y ⋅ x"
oops

end

end
</source>

← Revisión anterior	Revisión del 15:36 17 jun 2020
(Sin diferencias)

T5-1 - Historial de revisiones

Mjoseh: Protegió «T5-1» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « text ‹Ejercicio 5 de Lógica Matemática y Fundamentos (2-junio-2020)› theory ej_2_jun imports Main begin text ‹ Apellidos: Nombre:…»