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

2020-06-17T15:38:37Z

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

Mjoseh: Página creada con « theory ej_2jun_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P" by auto lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" by auto text ‹-------…»

2020-06-17T15:38:27Z

Página creada con «<source lang = "isabelle"> theory ej_2jun_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P" by auto lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" by auto text ‹-------…»

Página nueva

<source lang = "isabelle">
theory ej_2jun_sol
imports Main
begin

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 postOrden y postOrdenA son
equivalentes; es decir,
preOrdenA a = preOrden a

Nota: Los únicos métodos que se pueden usar son induct y simp.
-------------------------------------------------------------------›

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

section ‹Demostraciones del lema preOrdenAux›

subsection ‹Demostración estructurada de preOrdenAux›

lemma preOrdenAuxE:
"preOrdenAaux a xs = xs @ preOrden a"
proof (induct a arbitrary: xs)
case H
then show ?case by simp
next
case (N x1 a1 a2)
then show ?case by simp
qed

subsection ‹Demostración automática de preOrdenAux›

lemma preOrdenAuxA:
"preOrdenAaux a xs = xs @ preOrden a"
by (induct a arbitrary: xs) simp_all

subsection ‹Demostración declarativa detallada de preOrdenAux›

lemma append_unitaria:
"[x] @ ys = x # ys"
proof -
have "[x] @ ys = x # ([] @ ys)"
by (simp only: append.simps(2))
also have "… = x # ys"
by (simp only: append.simps(1))
finally show "[x] @ ys = x # ys"
by this
qed

lemma preOrdenAux:
"preOrdenAaux a xs = xs @ preOrden a"
proof (induct a arbitrary: xs)
fix xs :: "'a list"
have "preOrdenAaux H xs = xs"
by (simp only: preOrdenAaux.simps(1))
also have "… = xs @ []"
by (simp only: append_Nil2)
also have "… = xs @ preOrden H"
by (simp only: preOrden.simps(1))
finally show "preOrdenAaux H xs = xs @ preOrden H"
by this
next
fix x :: "'a" and i d :: "'a arbol" and xs :: "'a list"
assume HI1: "⋀xs. preOrdenAaux i xs = xs @ preOrden i"
and HI2: "⋀xs. preOrdenAaux d xs = xs @ preOrden d"
have "preOrdenAaux (N x i d) xs =
preOrdenAaux d (preOrdenAaux i (xs @ [x]))"
by (simp only: preOrdenAaux.simps(2))
also have "… = preOrdenAaux d ((xs @ [x]) @ (preOrden i))"
by (simp only: HI1)
also have "… = ((xs @ [x]) @ (preOrden i)) @ (preOrden d)"
by (simp only: HI2)
also have "… = xs @ ([x] @ preOrden i @ preOrden d)"
by (simp only: append.assoc)
also have "… = xs @ (x # preOrden i @ preOrden d)"
by (simp only: append_unitaria)
also have "… = xs @ (preOrden (N x i d))"
by (simp only: preOrden.simps(2))
finally show "preOrdenAaux (N x i d) xs =
xs @ preOrden (N x i d)"
by this
qed

section ‹Demostraciones de preOrdenA›

subsection ‹Demostración automática de preOrdenA›

theorem preOrdenA_A:
"preOrdenA a = preOrden a"
by (simp add: preOrdenA_def preOrdenAux)

subsection ‹Demostración declarativa detallada de preOrdenA›

theorem preOrdenA:
"preOrdenA a = preOrden a"
proof -
have "preOrdenA a = preOrdenAaux a []"
by (simp only: preOrdenA_def)
also have "… = [] @ (preOrden a)"
by (simp only: preOrdenAux)
also have "... = preOrden a"
by (simp only: append.simps(1))
finally show "preOrdenA a = preOrden a"
by this
qed

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

lemma inverso_d:
"x ⋅ x^ = 𝟭"
proof -
have "x ⋅ x^ = 𝟭 ⋅ (x ⋅ x^)"
by (simp only: neutro_i)
also have "… = (𝟭 ⋅ x) ⋅ x^"
by (simp only: asociativa)
also have "… = (((x^)^ ⋅ x^) ⋅ x) ⋅ x^"
by (simp only: inverso_i)
also have "… = ((x^)^ ⋅ (x^ ⋅ x)) ⋅ x^"
by (simp only: asociativa)
also have "… = ((x^)^ ⋅ 𝟭) ⋅ x^"
by (simp only: inverso_i)
also have "… = (x^)^ ⋅ (𝟭 ⋅ x^)"
by (simp only: asociativa)
also have "… = (x^)^ ⋅ x^"
by (simp only: neutro_i)
also have "… = 𝟭"
by (simp only: inverso_i)
finally show ?thesis
by this
qed

lemma condicion_necesaria:
assumes "x = y ⋅ z^"
shows "y = x ⋅ z"
proof -
have "x ⋅ z = (y ⋅ z^) ⋅ z"
using assms(1)
by (rule arg_cong)
also have "… = y ⋅ (z^ ⋅ z)"
by (simp only: asociativa)
also have "… = y ⋅ 𝟭"
by (simp only: inverso_i)
also have "… = y"
by (simp only: neutro_d)
finally have "x ⋅ z = y"
by this
then show "y = x ⋅ z"
by (rule sym)
qed

lemma condicion_suficiente:
assumes "y = x ⋅ z"
shows "x = y ⋅ z^"
proof -
have "y ⋅ z^ = (x ⋅ z) ⋅ z^"
using assms(1)
by (rule arg_cong)
also have "… = x ⋅ (z ⋅ z^)"
by (simp only: asociativa)
also have "… = x ⋅ 𝟭"
by (simp only: inverso_d)
also have "… = x"
by (simp only: neutro_d)
finally have "y ⋅ z^ = x"
by this
then show "x = y ⋅ z^"
by (rule sym)
qed

lemma condicion_necesaria_y_suficiente:
"x = y ⋅ z^ ⟷ y = x ⋅ z"
proof (rule iffI)
assume "x = y ⋅ z^"
then show "y = x ⋅ z"
by (rule condicion_necesaria)
next
assume "y = x ⋅ z"
then show "x = y ⋅ z^"
by (rule condicion_suficiente)
qed

end

end
</source>

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

T5-2 sol - Historial de revisiones

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

Mjoseh: Página creada con « theory ej_2jun_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P" by auto lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" by auto text ‹-------…»