Lógica matemática y fundamentos [Curso 2019-20] - Contribuciones del usuario [es]

Ejercicios

2021-01-21T10:16:28Z

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

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

Ejercicios

2021-01-21T10:16:14Z

Mjoseh:

Examen 2C sol

2020-09-10T08:20:02Z

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

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

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

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

text ‹------------------------------------------------------------------
Ejercicio 1. (2.5 puntos) Demostrar detalladamente con Isabelle,
sin usar métodos automáticos (como simp, auto, ...) sino sólo las
reglas básicas, que el siguiente argumento es correcto:
Ningún individuo que sea candidato será derrotado si hace una
buena campaña. Todo individuo que se postula es un candidato. Cualquier
candidato que no sea derrotado, será elegido. Todo individuo que sea
elegido hace una buena campaña. Por tanto, todo individuo que se
postula será elegido si y sólo si hace una buena campaña.

Simbología: I(x): x es individuo, C(x): x es candidato,
D(x): x es derrotado, B(x): x hace una buena campaña,
P(x): x se postula, E(x): x es elegido.
---------------------------------------------------------------------›
lemma
assumes "∀x. (I(x)∧C(x))∧B(x)⟶¬D(x)"
"∀x. I(x)∧P(x) ⟶ C(x)"
"∀x. C(x) ∧ ¬D(x) ⟶ E(x)"
"∀x. I(x)∧E(x) ⟶ B(x)"
shows "∀x. I(x)∧P(x)⟶(E(x)⟷B(x))"
proof (rule allI)
fix a
show "I(a)∧P(a) ⟶ (E(a)⟷B(a))"
proof
assume "I(a)∧P(a)"
show "E(a)⟷B(a)"
proof
assume "E(a)"
show "B(a)"
proof -
have "I(a)" using ‹I(a)∧P(a)› by (rule conjunct1)
then have 1:"I(a)∧E(a)" using ‹E(a)› by (rule conjI)
have "I(a)∧E(a) ⟶ B(a)" using assms(4) by (rule allE)
then show "B(a)" using 1 by (rule mp)
qed
next
assume "B(a)"
show "E(a)"
proof -
have "I(a)∧P(a) ⟶ C(a)" using assms(2) by (rule allE)
then have "C(a)" using ‹I(a)∧P(a)› by (rule mp)
have "I(a)" using ‹I(a)∧P(a)› by (rule conjunct1)
then have "I(a)∧C(a)" using ‹C(a)› by (rule conjI)
then have 2:"(I(a)∧C(a))∧B(a)" using ‹B(a)›
by (rule conjI)
have "(I(a)∧C(a))∧B(a)⟶¬D(a)" using assms(1)
by (rule allE)
then have "¬D(a)" using 2 by (rule mp)
have 3:"C(a) ∧ ¬D(a) ⟶ E(a)" using assms(3)
by (rule allE)
have "C(a)∧¬D(a)" using ‹C(a)› ‹¬D(a)› by (rule conjI)
with 3 show "E(a)" by (rule mp)
qed
qed
qed
qed

text ‹ -----------------------------------------------------------------
Ejercicio 2. (2.5 puntos) Consideramos la función
menores :: int ⇒ int list ⇒ bool
tal que (menores a xs) es la lista de los elementos de la lista xs que
son menores que a. Por ejemplo,
value "menores 2 [3,0,1] = [0,1]"
value "menores 2 [3,0,5] = [0]"
-----------------------------------------------------------------------›

fun menores :: "int ⇒ int list ⇒ int list" where
"menores a [] = []"
| "menores a (x#xs) = (if x < a then x # (menores a xs)
else (menores a xs))"

value "menores 2 [3,0,1] = [0,1]"
value "menores 2 [3,0,5] = [0]"

text ‹ -----------------------------------------------------------------
Demostrar que la longitud de la lista de elementos menores que uno
dado es menor o igual que la longitud de la lista original.
-----------------------------------------------------------------------›

― ‹Demostración estructurada:›

lemma menores_menor_1:
"length (menores x xs) < Suc (length xs)"
proof(induct xs)
show "length (menores x [])<Suc(length [])" by simp
next
fix xs a
assume HI: "length (menores x xs) < Suc (length xs)"
show "length (menores x (a#xs))< Suc(length (a#xs))"
proof(cases "a<x")
case True
then have "length (menores x (a#xs)) = length(a#(menores x xs))"
by simp
also have "... = Suc(length(menores x xs))" by simp
also have "...< Suc(Suc( length xs))" using HI by simp
also have "... = Suc(length(a#xs))" by simp
finally show ?thesis by simp
next
case False
then have "length (menores x (a#xs)) = length(menores x xs)" by simp
also have "... < Suc (length xs)" using HI by simp
also have "... < Suc (length (a#xs))" by simp
finally show ?thesis by simp
qed
qed

― ‹Demostración detallada:›

lemma menores_menor_detallada:
"length (menores x xs) < Suc (length xs)"
proof(induct xs)
show "length (menores x []) < Suc (length [])"
by (simp only: list.size lessI menores.simps(1))
next
fix xs a
assume HI: "length (menores x xs) < Suc (length xs)"
show "length (menores x (a#xs))< Suc(length (a#xs))"
proof (cases "a<x")
case True
then have "menores x (a#xs) = a#(menores x xs)"
by (simp only:if_True menores.simps)
then have "length (menores x (a#xs)) = length(a#(menores x xs))"
by (simp only:)
also have "... = Suc(length(menores x xs))" by (simp only:list.size)
also have "...< Suc(Suc( length xs))" using HI by (simp only:)
also have "... = Suc(length(a#xs))" by (simp only: list.size)
finally show ?thesis by this
next
case False
then have "menores x (a#xs) = menores x xs"
by (simp only: if_False menores.simps(2))
then have "length (menores x (a#xs)) = length(menores x xs)"
by (simp only:)
also have "... < Suc (length xs)" using HI by (simp only:)
also have "... < Suc (length (a#xs))" by (simp only: list.size)
finally show ?thesis by this
qed
qed

― ‹Demostración aplicativa:›

lemma menores_menor_aplicativa:
"length (menores x xs) < Suc (length xs)"
apply (induct xs)
apply (simp only: list.size lessI menores.simps(1))
apply (simp only:menores.simps(2))
apply(split if_split)
apply (rule conjI)
apply (rule impI)
apply (simp only: list.size)
apply (rule impI)
apply (simp only: list.size)
done

― ‹Demostración automática:›

lemma menores_menor_auto:
"length (menores x xs) < Suc (length xs)"
by (induct xs) auto

lemma
"length (menores x xs) < 1 + length xs"
proof(induct xs)
show "length (menores x []) < 1 + (length [])"
by (simp only: list.size lessI menores.simps(1))
next
fix xs a
assume HI: "length (menores x xs) < 1 + length xs"
show "length (menores x (a#xs)) < 1 + length (a#xs)"
proof (cases "a<x")
case True
then have "menores x (a#xs) = a#(menores x xs)"
by (simp only:if_True menores.simps)
then have "length (menores x (a#xs)) = length(a#(menores x xs))"
by (simp only:)
also have "... = 1 + (length(menores x xs))" by (simp only:list.size)
also have "...< 1 + (1 + ( length xs))" using HI by (simp only:)
also have "... = 1 + (length(a#xs))" by (simp only: list.size)
finally show ?thesis by this
next
case False
then have "menores x (a#xs) = menores x xs"
by (simp only: if_False menores.simps(2))
then have "length (menores x (a#xs)) = length(menores x xs)"
by (simp only:)
also have "... < 1 + (length xs)" using HI by (simp only:)
also have "... < 1 + (length (a#xs))" by (simp only: list.size)
finally show ?thesis by this
qed
qed

text ‹------------------------------------------------------------------
Ejercicio 3. (2.5 puntos) Sea G un grupo. Demostrar que si se verifica
∀x y. (((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭), entonces también se verifica
∀x. ∀y. ∀z. x ⋅ y = z ⋅ x ⟶ y = 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_d: "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
assumes "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
shows "x ⋅ y = z ⋅ x ⟶ y = z"
proof (rule impI)
assume 1: "x ⋅ y = z ⋅ x"
show "y = z"
proof-
have 2: "x ⋅ y = y ⋅ x"
proof-
have "x ⋅ y = (x ⋅ y) ⋅ 𝟭" by (simp only: neutro_d)
also have "… = (x ⋅ y) ⋅ (((y^ ⋅ x^) ⋅ y) ⋅ x)"
using assms by (simp only:)
also have "… = (x ⋅ (y ⋅ y^) ⋅ x^) ⋅ y ⋅ x"
by (simp only: asociativa)
also have "… = (x ⋅ 𝟭 ⋅ x^) ⋅ y ⋅ x"
by (simp only: inverso_d)
also have "… = (x ⋅ x^) ⋅ y ⋅ x"
by (simp only: neutro_d)
also have "… = 𝟭 ⋅ y ⋅ x"
by (simp only: inverso_d)
also have "… = y ⋅ x"
by (simp only: neutro_i)
finally show "x ⋅ y = y ⋅ x"
by this
qed
have "y ⋅ x = z ⋅ x" using 1 2 by (simp only:)
then have "(y ⋅ x) ⋅ x^ = (z ⋅ x) ⋅ x^" by (simp only:)
then have "y ⋅ (x ⋅ x^) = z ⋅ (x ⋅ x^)" by (simp only:asociativa)
then have "y ⋅ 𝟭 = z ⋅ 𝟭" by (simp only:inverso_d)
then show "y = z " by (simp only:neutro_d)
qed
qed

end

text ‹-----------------------------------------------------------------
Ejercicio 4. (2.5 puntos) El conjunto de los conjuntos finitos
se define inductivamente por
inductive_set Finito :: "'a set set"
where
vacioI: "{} ∈ Finito" |
insertaI: "A ∈ Finito ⟹ insert a A ∈ Finito"

Demostrar detalladamente que la unión de dos conjuntos finitos es
finito; es decir.
⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito

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

inductive_set Finito :: "'a set set"
where
vacioI: "{} ∈ Finito" |
insertaI: "A ∈ Finito ⟹ insert a A ∈ Finito"

― ‹ Demostración declarativa detallada ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
proof (induct rule: Finito.induct)
assume "B ∈ Finito"
then show "{} ∪ B ∈ Finito" by (simp only: Un_empty_left)
next
fix A a
assume AF: "A ∈ Finito" and
HI: "B ∈ Finito ⟹ A ∪ B ∈ Finito" and
BF: "B ∈ Finito"
have "A ∪ B ∈ Finito" by (simp only: HI BF)
then have "insert a (A ∪ B) ∈ Finito" by (simp only: insertaI)
then show "(insert a A) ∪ B ∈ Finito"
by (simp only: Set.Un_insert_left)
qed

― ‹ Demostración estructurada ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
proof (induct rule: Finito.induct)
assume "B ∈ Finito"
then show "{} ∪ B ∈ Finito" by simp
next
fix A a
assume "A ∈ Finito"
"B ∈ Finito ⟹ A ∪ B ∈ Finito"
"B ∈ Finito"
then have "A ∪ B ∈ Finito" by simp
then show "(insert a A) ∪ B ∈ Finito" by (simp add: insertaI)
qed

― ‹ Demostración aplicativa detallada ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
apply (erule Finito.induct)
apply (simp only: Un_empty_left)
apply (simp only: Set.Un_insert_left)
apply (simp only: insertaI)
done

― ‹ Demostración aplicativa estructurada ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
apply (erule Finito.induct)
apply simp
apply (auto intro: insertaI)
done

― ‹ Demostración automática ›
lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
by (induct rule: Finito.induct)
(auto intro: insertaI)

end
</source>

Examen 2C sol

2020-09-10T08:19:49Z

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

Examen 2C

2020-09-10T08:18:50Z

Mjoseh: Protegió «Examen 2C» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

<source lang = "isabelle">
text ‹Examen de Lógica Matemática y Fundamentos (9-septiembre-2020)›

theory examen_9_sep
imports Main
begin

text ‹
Apellidos:
Nombre:
›

text ‹Sustituye la palabra examen_9_sep 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 es de 9:30 a 11: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.›

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

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

text ‹------------------------------------------------------------------
Ejercicio 1. (2.5 puntos) Demostrar detalladamente con Isabelle,
sin usar métodos automáticos (como simp, auto, ...) sino sólo las
reglas básicas, que el siguiente argumento es correcto:
Ningún individuo que sea candidato será derrotado si hace una
buena campaña. Todo individuo que se postula es un candidato. Cualquier
candidato que no sea derrotado, será elegido. Todo individuo que sea
elegido hace una buena campaña. Por tanto, todo individuo que se
postula será elegido si y sólo si hace una buena campaña.

Simbología: I(x): x es individuo, C(x): x es candidato,
D(x): x es derrotado, B(x): x hace una buena campaña,
P(x): x se postula, E(x): x es elegido.
---------------------------------------------------------------------›

text ‹ -----------------------------------------------------------------
Ejercicio 2. (2.5 puntos) Consideramos la función
menores :: int ⇒ int list ⇒ bool
tal que (menores a xs) es la lista de los elementos de la lista xs que
son menores que a. Por ejemplo,
value "menores 2 [3,0,1] = [0,1]"
value "menores 2 [3,0,5] = [0]"

fun menores :: "int ⇒ int list ⇒ int list" where
"menores a [] = []"
| "menores a (x#xs) = (if x < a then x # (menores a xs)
else (menores a xs))"

Demostrar que la longitud de la lista de elementos menores que uno
dado es menor o igual que la longitud de la lista original.
-----------------------------------------------------------------------›

fun menores :: "int ⇒ int list ⇒ int list" where
"menores a [] = []"
| "menores a (x#xs) = (if x < a then x # (menores a xs)
else (menores a xs))"

value "menores 2 [3,0,1] = [0,1]"
value "menores 2 [3,0,5] = [0]"

lemma menores_menor:
"length (menores x xs) < 1 + (length xs)"
oops

text ‹------------------------------------------------------------------
Ejercicio 3. (2.5 puntos) Sea G un grupo. Demostrar que si se verifica
∀x y. (((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭), entonces también se verifica
∀x. ∀y. ∀z. x ⋅ y = z ⋅ x ⟶ y = 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_d: "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
assumes "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
shows "x ⋅ y = z ⋅ x ⟶ y = z"
oops

end

text ‹-----------------------------------------------------------------
Ejercicio 4. (2.5 puntos) El conjunto de los conjuntos finitos
se define inductivamente por
inductive_set Finito :: "'a set set"
where
vacioI: "{} ∈ Finito" |
insertaI: "A ∈ Finito ⟹ insert a A ∈ Finito"

Demostrar detalladamente que la unión de dos conjuntos finitos es
finito; es decir.
⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito

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

inductive_set Finito :: "'a set set"
where
vacioI: "{} ∈ Finito" |
insertaI: "A ∈ Finito ⟹ insert a A ∈ Finito"

lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
oops

end

</source>

Examen 2C

2020-09-10T08:18:36Z

Mjoseh: Página creada con «<source lang = "isabelle"> text ‹Examen de Lógica Matemática y Fundamentos (9-septiembre-2020)› theory examen_9_sep imports Main begin text ‹ Apellidos: Nomb…»

Ejercicios

2020-09-10T08:16:58Z

Mjoseh:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]], [[Relación 1 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf Una solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]], [[Relación 2 |Solución colaborativa]], [[Rel 2 |Una solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]], [[Relación 3 |Solución colaborativa]], [[Rel 3 |Una solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]], [[Relación 4 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf Una solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]], [[Relación 5 |Solución colaborativa]], [[Rel 5 |Una solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]], [[Relación 6 |Solución colaborativa]] , [[Rel 6 |Una solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]], [[Relación 8 |Solución colaborativa]]).
** [[Rel 8 (rev 1) | Primera corrección]]
** [[Rel 8 (sol) | Una solución]]
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]], [[Relación 9 |Solución colaborativa]]).
** [[Rel 9 (rev 1) | Primera corrección]]
** [[Rel 9 (sol) | Una solución]]
* '''Ejercicio 1 (24-04-2020)''': ([[T1 |Enunciado]], [[T1 sol |Una solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]], [[Relación 10 |Solución colaborativa]]).
** [[Rel 10 (sol) | Una solución]]
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]], [[Relación 11 |Solución colaborativa]]).
** [[Rel 11 (sol) | Una solución]]
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]], [[Relación 12 |Solución colaborativa]]).
** [[Rel 12 (sol) | Una solución]]
* '''Ejercicio 2 (12-05-2020)''': ([[T2 |Enunciado]], [[T2 sol |Una solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]], [[Relación 13 |Solución colaborativa]]).
** [[Rel 13 (sol) | Una solución]]
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomátización de la Geometría.] ([[R14 |Enunciado]], [[Relación 14 |Solución colaborativa]]).
** [[Rel 14 (sol) | Una solución]]
* '''Ejercicio 3 (19-05-2020)''': ([[T3 |Enunciado]], [[T3 sol |Una solución]]).
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]], [[Relación 15 |Solución colaborativa]]).
** [[Rel 15 (sol) | Una solución]]
* '''Ejercicio 4 (26-05-2020)''': ([[T4 |Enunciado]], [[T4 sol |Una solución]]).
* '''Ejercicio 5 (02-06-2020)''':
** ([[T5-1 |Enunciado (1)]], [[T5-1 sol |Una solución]]).
** ([[T5-2 |Enunciado (2)]], [[T5-2 sol |Una solución]]).
* '''Trabajo final''': ([[TF |Enunciado]], [[TF sol |Una solución]]).
* '''Examen (2-07-2020)''': ([[Examen 1C |Enunciado]], [[Examen 1C sol |Una solución]]).
* '''Examen (9-09-2020)''': ([[Examen 2C |Enunciado]], [[Examen 2C sol |Una solución]]).

Examen 1C

2020-07-06T12:32:54Z

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

<source lang = "isabelle">
text ‹Examen de Lógica Matemática y Fundamentos (2-julio-2020)›

theory examen_2_jul
imports Main
begin

text ‹
Apellidos:
Nombre:
›

text ‹Sustituye la palabra examen_2_jul 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 es de 9:30 a 11: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 examen, 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. Demostrar detalladamente con Isabelle, sin usar métodos
automáticos (como simp, auto, ...) sino sólo las reglas básicas,
que el siguiente argumento es correcto
Si todas las medicinas están contaminadas, entonces todos los
técnicos negligentes son unos bribones. Si hay medicinas
contaminadas, entonces todas las medicinas están contaminadas y son
peligrosas. Todos los germicidas son medicinas. Sólo los
negligentes son distraídos. Por tanto, si cualquier técnico es
distraído y si algunos germicidas están contaminados, los técnicos
son bribones.
Usar la siguiente simbología:
M(x): x es medicina, C(x): x está contaminada,
T(x): x es técnico, N(x): x es un negligente,
B(x): x es un bribón, G(x): x es germicida,
D(x): x es distraído, P(x): x es peligrosa.
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 2. Se consideran las definiciones de las siguientes
funciones (que se dan a continuación)
estaEn :: 'a ⇒ 'a list ⇒ bool
sublista :: "'a list ⇒ 'a list ⇒ bool
elimina :: nat ⇒ 'a list ⇒ 'a list
tales 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
+ (sublista xs ys) se verifica si todos los elementos de la lista xs
están en la lista ys. Por ejemplo,
sublista [(1::nat),2,3] [3,2,1,2] = True
sublista [(1::nat),2,3] [2,1,2] = False
+ (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]

Demostrar detalladamente que
sublista (elimina n xs) xs
---------------------------------------------------------------------›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (a=x ∨ estaEn x xs)"

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

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

lemma eliminaSublista: "sublista (elimina n xs) xs"
oops

text ‹------------------------------------------------------------------
Ejercicio 3. Sea G un grupo. Demostrar que las siguientes condiciones
son equivalentes:
(+) G es commutativo, es decir, ∀x y. (x ⋅ y = y ⋅ x)
(+) ∀x y. (((y^ ⋅ x^) ⋅ 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

lemma
assumes "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
shows "x ⋅ y = y ⋅ x"
oops

lemma
assumes "x ⋅ y = y ⋅ x"
shows "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
oops

end

text ‹------------------------------------------------------------------
Ejercicio 4. Se define la clausura reflexiva, simétrica y transitiva
de una relación binaria r como sigue:
inductive rst :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
for r where
refl1: "rst r x x"
| trans1: "r x y ⟹ rst r y z ⟹ rst r x z"
| trans2: "r y x ⟹ rst r y z ⟹ rst r x z"

Demostrar detalladamente que la relación (rst es r) simétrica.
---------------------------------------------------------------------›

inductive rst :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
for r where
refl1: "rst r x x"
| trans1: "r x y ⟹ rst r y z ⟹ rst r x z"
| trans2: "r y x ⟹ rst r y z ⟹ rst r x z"

lemma rst_es_simetrica : "rst r x y ⟹ rst r y x"
oops

end

</source>

Examen 1C

2020-07-06T12:32:42Z

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

Examen 1C sol

2020-07-06T12:31:30Z

Mjoseh: Protegió «Examen 1C sol» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

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

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

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

text ‹------------------------------------------------------------------
Ejercicio 1. Demostrar detalladamente con Isabelle, sin usar métodos
automáticos (como simp, auto, ...) sino sólo las reglas básicas,
que el siguiente argumento es correcto
Si todas las medicinas están contaminadas, entonces todos los
técnicos negligentes son unos bribones. Si hay medicinas
contaminadas, entonces todas las medicinas están contaminadas y son
peligrosas. Todos los germicidas son medicinas. Sólo los
negligentes son distraídos. Por tanto, si cualquier técnico es
distraído y si algunos germicidas están contaminados, los técnicos
son bribones.
Usar la siguiente simbología:
M(x): x es medicina, C(x): x está contaminada,
T(x): x es técnico, N(x): x es un negligente,
B(x): x es un bribón, G(x): x es germicida,
D(x): x es distraído, P(x): x es peligrosa.
---------------------------------------------------------------------›

― ‹Formalización y demostración›

― ‹Formalización:›
lemma
assumes "(∀x. M(x) ⟶ C(x)) ⟶ (∀y. (T(y) ∧ N(y)) ⟶ B(y))"
"(∃x. M(x) ∧ C(x)) ⟶ (∀x. M(x) ⟶ C(x) ∧ P(x))"
"∀x. G(x) ⟶ M(x)"
"∀y. ¬N(y) ⟶ ¬D(y)"
shows "(∀y. T y ⟶ D y) ∧ (∃x. G x ∧ C x) ⟶ (∀z. T z ⟶ B z)"
oops

― ‹Auxiliar›
lemma previo:
assumes "∀x. M(x) ⟶ C(x) ∧ P(x)"
shows "∀x. M(x) ⟶ C(x)"
proof (rule allI)
fix a
show "M(a) ⟶ C(a)"
proof (rule impI)
assume "M(a)"
have "M(a) ⟶ C(a) ∧ P(a)" using assms by (rule allE)
then have "C(a) ∧ P(a)" using ‹M(a)› by (rule mp)
then show "C(a)" by (rule conjunct1)
qed
qed

― ‹Demostración declarativa detallada:›
lemma
assumes "(∀x. M(x) ⟶ C(x)) ⟶ (∀y. (T(y) ∧ N(y)) ⟶ B(y))"
"(∃x. M(x) ∧ C(x)) ⟶ (∀x. M(x) ⟶ C(x) ∧ P(x))"
"∀x. G(x) ⟶ M(x)"
"∀y. ¬N(y) ⟶ ¬D(y)"
shows "(∀y. T y ⟶ D y) ∧ (∃x. G x ∧ C x) ⟶ (∀z. T z ⟶ B z)"
proof (rule impI)
assume 1: "(∀y. T(y) ⟶ D(y)) ∧ (∃x. G(x) ∧ C(x))"
show "∀z. T(z) ⟶ B(z)"
proof (rule allI)
fix a
show "T(a) ⟶ B(a)"
proof (rule impI)
assume "T(a)"
show "B(a)"
proof -
have "∀y. T(y) ⟶ D(y)" using 1 by (rule conjunct1)
then have "T(a) ⟶ D(a)" by (rule allE)
then have "D(a)" using `T(a)` by (rule mp)
then have "¬¬D(a)" by (rule notnotI)
have "¬N(a)⟶¬D(a)" using assms(4) by (rule allE)
then have "¬¬N(a)" using `¬¬D(a)` by (rule mt)
then have "N(a)" by (rule notnotD)
have "∃x. G(x) ∧ C(x)" using 1 by (rule conjunct2)
then obtain b where "G(b) ∧ C(b)" by (rule exE)
then have "G(b)" by (rule conjunct1)
have "C(b)" using `G(b) ∧ C(b)` by (rule conjunct2)
have "G(b) ⟶ M(b)" using assms(3) by (rule allE)
then have "M(b)" using `G(b)` by (rule mp)
then have "M(b) ∧ C(b)" using `C(b)` by (rule conjI)
then have "∃x. M(x) ∧ C(x)" by (rule exI)
with assms(2) have "∀x. M(x) ⟶ C(x) ∧ P(x)" by (rule mp)
then have "∀x. M(x) ⟶ C(x)" by (rule previo)
with assms(1) have "∀y. (T(y) ∧ N(y)) ⟶ B(y)" by (rule mp)
then have "(T(a) ∧ N(a))⟶B(a)" by (rule allE)
have "T(a) ∧ N(a)" using `T(a)` `N(a)` by (rule conjI)
with `(T(a) ∧ N(a)) ⟶ B(a)` show "B(a)" by (rule mp)
qed
qed
qed
qed

text ‹------------------------------------------------------------------
Ejercicio 2. Se consideran las definiciones de las siguientes
funciones (que se dan a continuación)
estaEn :: 'a ⇒ 'a list ⇒ bool
sublista :: "'a list ⇒ 'a list ⇒ bool
elimina :: nat ⇒ 'a list ⇒ 'a list
tales 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
+ (sublista xs ys) se verifica si todos los elementos de la lista xs
están en la lista ys. Por ejemplo,
sublista [(1::nat),2,3] [3,2,1,2] = True
sublista [(1::nat),2,3] [2,1,2] = False
+ (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]

Demostrar detalladamente que
sublista (elimina n xs) xs
---------------------------------------------------------------------›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (a=x ∨ estaEn x xs)"

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

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

― ‹Auxiliares:›

lemma sublistaMono: "sublista xs ys ⟹ sublista xs (y#ys)"
apply (induct xs)
apply (simp only: sublista.simps(1))
apply (simp only: sublista.simps(2))
apply (rule conjI)
apply (erule conjE)
apply (simp only: estaEn.simps(2))
apply (rule disjI2)
apply (simp only: implies_True_equals)+
done

lemma estaEn1: "estaEn x (x#xs)"
apply (simp only: estaEn.simps(2))
apply (rule disjI1)
apply (rule refl)
done

lemma sublistaReflexiva: "sublista xs xs"
apply (induct xs)
apply (simp only: sublista.simps(1))
apply (simp only: sublista.simps(2))
apply (rule conjI)
apply (rule estaEn1)
apply (rule sublistaMono, assumption)
done

― ‹Demostración declarativa detallada:›
lemma eliminaSublista_dec: "sublista (elimina n xs) xs"
proof (induct rule: elimina.induct)
fix n
show "sublista (elimina n []) []"
by (simp only: elimina.simps(1) sublista.simps(1))
next
fix x :: "'a" and xs :: "'a list"
show "sublista (elimina 0 (x # xs)) (x # xs)"
by (simp only: elimina.simps(2) sublistaReflexiva)
next
fix n and x :: "'a" and xs :: "'a list"
show "sublista (elimina n xs) xs ⟹
sublista (elimina (Suc n) (x # xs)) (x # xs)"
by (simp only: elimina.simps(3) sublistaMono)
qed

text ‹------------------------------------------------------------------
Ejercicio 3. Sea G un grupo. Demostrar que las siguientes condiciones
son equivalentes:
(+) G es commutativo, es decir, ∀x y. (x ⋅ y = y ⋅ x)
(+) ∀x y. (((y^ ⋅ x^) ⋅ 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

― ‹Auxiliar para una implicación:›

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
assumes "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
shows "x ⋅ y = y ⋅ x"
proof -
have "x ⋅ y = (x ⋅ y) ⋅ 𝟭"
by (rule neutro_d [THEN sym])
also have "… = (x ⋅ y) ⋅ (((y^ ⋅ x^) ⋅ y) ⋅ x)"
using assms by (rule arg_cong [THEN sym])
also have "… = (x ⋅ ((y ⋅ y^) ⋅ x^) ⋅ y) ⋅ x"
by (simp only: asociativa)
also have "… = ((x ⋅ (𝟭 ⋅ x^)) ⋅ y) ⋅ x"
by (simp only: inverso_d)
also have "… = (x ⋅ ((𝟭 ⋅ x^) ⋅ y)) ⋅ x "
by (simp only: asociativa)
also have "… = (x ⋅ (x^ ⋅ y)) ⋅ x"
by (simp only: neutro_i)
also have "… = ((x ⋅ x^) ⋅ y) ⋅ x"
by (simp only: asociativa)
also have "… = (𝟭 ⋅ y) ⋅ x"
by (simp only: inverso_d)
also have "… = 𝟭 ⋅ (y ⋅ x)"
by (simp only: asociativa)
also have "… = y ⋅ x"
by (simp only: neutro_i)
finally show "x ⋅ y = y ⋅ x"
by this
qed

― ‹Recíproco:›
lemma
assumes "x ⋅ y = y ⋅ x"
shows "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
proof -
have "y ⋅ x = x ⋅ y" using assms by (rule sym)
then have "x^ ⋅ (y ⋅ x) = x^ ⋅ (x ⋅ y)" by (rule arg_cong)
then have "y^ ⋅ (x^ ⋅ (y ⋅ x)) =y^ ⋅ (x^ ⋅ (x ⋅ y))" by (rule arg_cong)
then have "((y^ ⋅ x^) ⋅ y) ⋅ x =y^ ⋅ ((x^ ⋅ x) ⋅ y)"
by (simp only: asociativa)
also have "... = y^ ⋅ (𝟭 ⋅ y)" by (simp only: inverso_i)
also have "... = y^ ⋅ y " by (simp only: neutro_i)
also have "... = 𝟭" by (simp only: inverso_i)
finally show "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭" by this
qed

end

text ‹------------------------------------------------------------------
Ejercicio 4. Se define la clausura reflexiva, simétrica y transitiva
de una relación binaria r como sigue:
inductive rst :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
for r where
refl1: "rst r x x"
| trans1: "r x y ⟹ rst r y z ⟹ rst r x z"
| trans2: "r y x ⟹ rst r y z ⟹ rst r x z"

Demostrar detalladamente que la relación (rst es r) simétrica.
---------------------------------------------------------------------›

inductive rst :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
for r where
refl1: "rst r x x"
| trans1: "r x y ⟹ rst r y z ⟹ rst r x z"
| trans2: "r y x ⟹ rst r y z ⟹ rst r x z"

― ‹Lemas auxiliares:›

lemma r_subset_rst: "r x y ⟹ rst r x y"
by (simp only: refl1 trans1)

lemma r_subset_rst_b: "r x y ⟹ rst r y x"
by (simp only: refl1 trans2)

lemma rst_sc1_declarativo: "rst r x y ⟹ r y z ⟹ rst r x z"
proof (induct rule:rst.induct)
case (refl1 x)
then show ?case by (rule r_subset_rst)
next
case (trans1 x y z)
then show ?case by (simp only: rst.trans1)
next
case (trans2 y x z)
then show ?case by (simp only: rst.trans2)
qed

lemma rst_sc2_declarativo: "rst r z y ⟹ r x y ⟹ rst r z x"
proof (induct rule:rst.induct)
case (refl1 x)
then show ?case by (rule r_subset_rst_b)
next
case (trans1 x y z)
then show ?case by (simp only: rst.trans1)
next
case (trans2 y x z)
then show ?case by (simp only: rst.trans2)
qed

― ‹Demostración declarativa detallada:›
lemma rstSimetrica_declarativa: "rst r x y ⟹ rst r y x"
proof (induct rule: rst.induct)
fix x
show "rst r x x" by (rule refl1)
next
fix x y z
assume "r x y" and "rst r y z" and "rst r z y"
then show "rst r z x" by (simp only: rst_sc2_declarativo)
next
fix x y z
assume "r y x" and "rst r y z" and "rst r z y"
then show "rst r z x" by (simp only: rst_sc1_declarativo)
qed

end
</source>

Examen 1C sol

2020-07-06T12:31:10Z

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

Ejercicios

2020-07-06T12:28:46Z

Mjoseh:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]], [[Relación 1 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf Una solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]], [[Relación 2 |Solución colaborativa]], [[Rel 2 |Una solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]], [[Relación 3 |Solución colaborativa]], [[Rel 3 |Una solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]], [[Relación 4 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf Una solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]], [[Relación 5 |Solución colaborativa]], [[Rel 5 |Una solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]], [[Relación 6 |Solución colaborativa]] , [[Rel 6 |Una solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]], [[Relación 8 |Solución colaborativa]]).
** [[Rel 8 (rev 1) | Primera corrección]]
** [[Rel 8 (sol) | Una solución]]
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]], [[Relación 9 |Solución colaborativa]]).
** [[Rel 9 (rev 1) | Primera corrección]]
** [[Rel 9 (sol) | Una solución]]
* '''Ejercicio 1 (24-04-2020)''': ([[T1 |Enunciado]], [[T1 sol |Una solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]], [[Relación 10 |Solución colaborativa]]).
** [[Rel 10 (sol) | Una solución]]
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]], [[Relación 11 |Solución colaborativa]]).
** [[Rel 11 (sol) | Una solución]]
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]], [[Relación 12 |Solución colaborativa]]).
** [[Rel 12 (sol) | Una solución]]
* '''Ejercicio 2 (12-05-2020)''': ([[T2 |Enunciado]], [[T2 sol |Una solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]], [[Relación 13 |Solución colaborativa]]).
** [[Rel 13 (sol) | Una solución]]
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomátización de la Geometría.] ([[R14 |Enunciado]], [[Relación 14 |Solución colaborativa]]).
** [[Rel 14 (sol) | Una solución]]
* '''Ejercicio 3 (19-05-2020)''': ([[T3 |Enunciado]], [[T3 sol |Una solución]]).
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]], [[Relación 15 |Solución colaborativa]]).
** [[Rel 15 (sol) | Una solución]]
* '''Ejercicio 4 (26-05-2020)''': ([[T4 |Enunciado]], [[T4 sol |Una solución]]).
* '''Ejercicio 5 (02-06-2020)''':
** ([[T5-1 |Enunciado (1)]], [[T5-1 sol |Una solución]]).
** ([[T5-2 |Enunciado (2)]], [[T5-2 sol |Una solución]]).
* '''Trabajo final''': ([[TF |Enunciado]], [[TF sol |Una solución]]).
* '''Examen (2-07-2020)''': ([[Examen 1C |Enunciado]], [[Examen 1C sol |Una solución]]).

Rel 15 (sol)

2020-06-29T15:38:38Z

Mjoseh: Protegió «Rel 15 (sol)» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

<source lang = "isabelle">
chapter ‹ R15: Definiciones inductivas: clausuras ›

theory R15_sol
imports Main
begin

section ‹ La clausura reflexiva transitiva ›

text ‹
· Las definiciones inductivas aceptan parámetros; por tanto, permiten
expresar funciones que construyen conjuntos.

· La relaciones binarias son conjuntos de pares; por tanto, se pueden
definir inductivamente.
›

text ‹
· La clausura reflexiva y transitiva de una relación r es la menor
relación reflexiva y transitiva que contiene a r.

· Se representa por r*.

· Se puede definir inductivamente, como conjunto:
· (x,x) ∈ r*
· Si (x,y) ∈ r e (y,z) ∈ r*, entonces (x,z) ∈ r*

· La definición inductiva, como conjunto, se puede expresar en
Isabelle/HOL como sigue:
›

inductive_set
crt :: "('a × 'a) set ⇒ ('a × 'a) set" ("_*" [1000] 999)
for r :: "('a × 'a) set"
where
crt_refl [iff]: "(x,x) ∈ r*"
| crt_paso: "⟦(x,y) ∈ r; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"

text ‹
Notas:
· La sintaxis concreta permite escribir r* en lugar de (crt r).
· La definición consta de dos reglas.
· A la regla reflexiva se le añade el atributo iff para aumentar la
automatización.
· A la regla del paso no se le añade ningún atributo, porque r* ocurre
en la izquierda.
· En el resto de esta sección se demuestra que esta definición
coincide con la menor relación reflexiva y transitiva que contiene a
r.
›

text ‹
Lema. La relación r* es reflexiva.
›

lemma "(x,x) ∈ r*"
by (rule crt_refl)

text ‹
Lema. La relación r* contiene a r.
›

― ‹La demostración aplicativa es ›
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"
apply (erule crt_paso)
(* (y, y) ∈ r**)
apply (rule crt_refl)
(* *)
done

― ‹La demostración automática es›
lemma r_contenida_clausura [intro]:
"(x,y) ∈ r ⟹ (x,y) ∈ r*"
by (simp add: crt_paso)
(* by (auto intro: crt_paso) *)

― ‹La demostración declarativa es›
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"
proof -
assume 1: "(x, y) ∈ r"
have 2: "(y, y) ∈ r*" by simp
show "(x,y) ∈ r*" using 1 2 by (rule crt_paso)
qed

text ‹
Notas:
· La ventaja del lema es que se puede declarar como regla de
introducción, porque r* ocurre sólo en la derecha.
· Con la declaración, algunas demostraciones que usan crt_paso se
hacen de manera automática.
›

text ‹
El esquema de inducción de la clausura reflexiva transitiva es
· crt.induct:
⟦(x1, x2) ∈ r*;
⋀x. P x x;
⋀x y z. ⟦(x,y) ∈ r; (y,z) ∈ r*; P y z⟧ ⟹ P x z⟧
⟹ P x1 x2
›

text ‹
Lema. La relación r* es transitiva.
›

― ‹ La demostración aplicativa es›
lemma "⟦(x,y) ∈ r*; (y,z) ∈ r*⟧ ⟹ (x,z) ∈ r*"
apply (induction rule:crt.induct)
(* 1. ⋀x. (x, z) ∈ r* ⟹ (x, z) ∈ r*
2. ⋀x y za. ⟦(x, y) ∈ r; (y, za) ∈ r*;
(za, z) ∈ r* ⟹ (y, z) ∈ r*;
(za, z) ∈ r*⟧
⟹ (x, z) ∈ r* *)
apply simp
(* 1. ⋀x y za. ⟦(x, y) ∈ r; (y, za) ∈ r*;
(za, z) ∈ r* ⟹ (y, z) ∈ r*;
(za, z) ∈ r*⟧
⟹ (x, z) ∈ r**)
apply (simp add: crt_paso)
(* *)
done

lemma "⟦ (x,y) ∈ r*; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"
by (induction rule: crt.induct)
(simp_all add: crt_paso)

text ‹
Otra formulación del lema, con la variable y a la derecha.
›

― ‹La demostración aplicativa es›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
apply (induction rule: crt.induct)
(* 1. ⋀x. (x, z) ∈ r* ⟶ (x, z) ∈ r*
2. ⋀x y za. ⟦(x, y) ∈ r;
(y, za) ∈ r*;
(za, z) ∈ r* ⟶ (y, z) ∈ r*⟧
⟹ (za, z) ∈ r* ⟶ (x, z) ∈ r* *)
apply simp
(* ⋀x y za. ⟦(x, y) ∈ r;
(y, za) ∈ r*;
(za, z) ∈ r* ⟶ (y, z) ∈ r*⟧
⟹ (za, z) ∈ r* ⟶ (x, z) ∈ r* *)
apply (rule impI)
(* ⋀x y za. ⟦(x, y) ∈ r;
(y, za) ∈ r*;
(za, z) ∈ r* ⟶ (y, z) ∈ r*;
(za, z) ∈ r*⟧
⟹ (za, z) ∈ r* ⟶ (x, z) ∈ r* *)
apply (drule mp)
(* 1. ⋀x y za. ⟦(x, y) ∈ r; (y, za) ∈ r*; (za, z) ∈ r*⟧
⟹ (za, z) ∈ r*
2. ⋀x y za. ⟦(x, y) ∈ r;
(y, za) ∈ r*;
(za, z) ∈ r*;
(y, z) ∈ r*⟧
⟹ (x, z) ∈ r* *)
apply assumption
(* ⋀x y za. ⟦(x, y) ∈ r;
(y, za) ∈ r*;
(za, z) ∈ r*;
(y, z) ∈ r*⟧
⟹ (x, z) ∈ r* *)
apply (erule crt_paso)
(* ⋀x y za. ⟦(y, za) ∈ r*; (za, z) ∈ r*; (y, z) ∈ r*⟧
⟹ (y, z) ∈ r**)
apply assumption
(* *)
done

― ‹La demostración automática es›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
by (induction rule:crt.induct)
(auto simp add: crt_paso)

― ‹La demostración declarativa es›
lemma crt_trans [rule_format]:
"(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
proof (induction rule:crt.induct)
show "⋀x. (x,z) ∈ r* ⟶ (x,z) ∈ r*" by simp
next
fix x y u
assume H1: "(x,y) ∈ r" and
H2: "(y,u) ∈ r*" and
H3: "(u,z) ∈ r* ⟶ (y,z) ∈ r*"
show "(u,z) ∈ r* ⟶ (x,z) ∈ r*"
proof
assume "(u,z) ∈ r*"
with H3 have "(y,z) ∈ r*" ..
with H1 show "(x,z) ∈ r*" by (rule crt_paso)
qed
qed

text ‹
Notas:
· La reformulación anterior es un caso particular de la siguiente
heurística:
"Para probar una fórmula por inducción sobre (x1,...,xn) ∈ R,
poner todas las premisas conteniendo cualquiera de lax xi en la
conclusión usando ⟶".
· El atributo "rule_format" transforma ⟶ en ⟹.
›

text ‹
La relación r* está contenida en cualquier relación reflexiva y
transitiva que contenga a r.

Mediante (crt2 r) se define la menor relación reflexiva y transitiva
que contiene a r.
›

inductive_set
crt2 :: "('a × 'a)set ⇒ ('a × 'a)set"
for r :: "('a × 'a)set"
where
"(x,y) ∈ r ⟹ (x,y) ∈ crt2 r" (* contiene a r *)
| "(x,x) ∈ crt2 r" (* reflexiva *)
| "⟦(x,y) ∈ crt2 r; (y,z) ∈ crt2 r⟧ ⟹ (x,z) ∈ crt2 r" (* transitiva *)

text ‹ Probaremos que r* coincide con (crt2 r) ›

text ‹
Lema. La relación (crt2 r) está contenida en r*.
›

― ‹Demostración aplicativa›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
apply (induction rule: crt2.induct)
(* 1. ⋀x y. (x, y) ∈ r ⟹ (x, y) ∈ r*
2. ⋀x. (x, x) ∈ r*
3. ⋀x y z. ⟦(x, y) ∈ crt2 r; (x, y) ∈ r*;
(y, z) ∈ crt2 r; (y, z) ∈ r*⟧
⟹ (x, z) ∈ r* *)
apply (erule r_contenida_clausura)
(* 1. ⋀x. (x, x) ∈ r*
2. ⋀x y z. ⟦(x, y) ∈ crt2 r; (x, y) ∈ r*;
(y, z) ∈ crt2 r; (y, z) ∈ r*⟧
⟹ (x, z) ∈ r* *)
apply simp
(* ⋀x y z. ⟦(x, y) ∈ crt2 r; (x, y) ∈ r*;
(y, z) ∈ crt2 r; (y, z) ∈ r*⟧
⟹ (x, z) ∈ r* *)
apply (erule crt_trans)
(* ⋀x y z. ⟦(x, y) ∈ crt2 r; (y, z) ∈ crt2 r; (y, z) ∈ r*⟧
⟹ (y, z) ∈ r* *)
apply assumption
(* *)
done

― ‹ La demostración automática es ›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
by (induction rule: crt2.induct)
(auto simp add: r_contenida_clausura
crt_trans)

― ‹ La demostración declarativa es ›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
proof (induction rule: crt2.induct)
fix x y
assume "(x,y) ∈ r"
then show "(x,y) ∈ r*" by (rule r_contenida_clausura)
next
fix x
show "(x,x) ∈ r*" by (rule crt_refl)
next
fix x y z
assume H1: "(x,y) ∈ crt2 r" and
H2: "(x,y) ∈ r*" and
H3: "(y,z) ∈ crt2 r" and
H4: "(y,z) ∈ r*"
show "(x,z) ∈ r*" using H2 H4 by (rule crt_trans)
qed

text ‹
Lema. La relación r* está contenida en (crt2 r).
›

― ‹ La demostración aplicativa es ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
apply (induction rule: crt.induct)
(* 1. ⋀x. (x, x) ∈ crt2 r
2. ⋀x y z. ⟦(x, y) ∈ r; (y, z) ∈ r*; (y, z) ∈ crt2 r⟧
⟹ (x, z) ∈ crt2 r *)
apply (rule crt2.intros(2))
(* ⋀x y z. ⟦(x, y) ∈ r; (y, z) ∈ r*; (y, z) ∈ crt2 r⟧
⟹ (x, z) ∈ crt2 r *)
apply (drule crt2.intros(1))
(* ⋀x y z. ⟦(y, z) ∈ r*; (y, z) ∈ crt2 r; (x, y) ∈ crt2 r⟧
⟹ (x, z) ∈ crt2 r *)
apply (drule_tac x=x and z=z in crt2.intros(3))
(* 1. ⋀x y z. ⟦(y, z) ∈ r*; (y, z) ∈ crt2 r⟧
⟹ (y, z) ∈ crt2 r
2. ⋀x y z. ⟦(y, z) ∈ r*; (y, z) ∈ crt2 r; (x, z) ∈ crt2 r⟧
⟹ (x, z) ∈ crt2 r *)
apply assumption+
(* *)
done

― ‹ La demostración automática es ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
by (induction rule: crt.induct)
(auto intro: crt2.intros)

― ‹ La demostración declarativa es ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
proof (induction rule:crt.induct)
fix x
show "(x,x) ∈ crt2 r" by (rule crt2.intros(2))
next
fix x y z
assume H1: "(x,y) ∈ r" and
H2: "(y,z) ∈ r*" and
H3: "(y,z) ∈ crt2 r"
have "(x,y) ∈ crt2 r" using H1 by (rule crt2.intros(1))
then show "(x,z) ∈ crt2 r" using H3 by (rule crt2.intros(3))
qed

text ‹ ----------------------------------------------------------------
Ejercicio 1. Demostrar que si (x,y) ∈ r* e (y,z) ∈ r, entonces
(x,z) ∈ r*
------------------------------------------------------------------- ›

― ‹ Demostración aplicativa ›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
apply (induction rule: crt.induct)
(* 1. ⋀x. (x, z) ∈ r ⟶ (x, z) ∈ r*
2. ⋀x y za. ⟦(x, y) ∈ r;
(y, za) ∈ r*;
(za, z) ∈ r ⟶ (y, z) ∈ r*⟧
⟹ (za, z) ∈ r ⟶ (x, z) ∈ r* *)
apply (simp add: r_contenida_clausura)
(* ⋀x y za. ⟦(x, y) ∈ r;
(y, za) ∈ r*;
(za, z) ∈ r ⟶ (y, z) ∈ r*⟧
⟹ (za, z) ∈ r ⟶ (x, z) ∈ r* *)
apply (simp add: crt_paso)
done

― ‹ Demostración automática ›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
by (induction rule: crt.induct)
(auto simp add: r_contenida_clausura
crt_paso)

― ‹ Demostración declarativa ›
lemma crt_paso2 [rule_format]:
"(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
proof (induction rule: crt.induct)
fix x
show "(x,z) ∈ r ⟶ (x,z) ∈ r*" by (simp add: r_contenida_clausura)
next
fix x y u
assume H1: "(x,y) ∈ r" and
H2: "(y,u) ∈ r*" and
H3: "(u,z) ∈ r ⟶ (y,z) ∈ r*"
show "(u,z) ∈ r ⟶ (x,z) ∈ r*"
proof
assume "(u,z) ∈ r"
with H3 have "(y,z) ∈ r*" by (rule mp)
with H1 show "(x,z) ∈ r*" by (rule crt_paso)
qed
qed

text ‹ ----------------------------------------------------------------
Ejercicio 2. Considerar la siguiente definición de la clausura tran-
sitiva de una relación r, y probar que es la menor relación reflexiva
y transitiva que contiene a r.

Nota: Establecer los lemas necesarios.
------------------------------------------------------------------- ›

inductive star' :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl': "star' r x x"
| step': "star' r x y ⟹ r y z ⟹ star' r x z"

― ‹ Demostración de que (star' r) es reflexiva ›
lemma star'Refl: "star' r x x"
by (simp add: refl')

― ‹ Demostración aplicativa de r contenida en (star' r) ›
lemma "r x y ⟹ star' r x y"
apply (rule_tac y=x in step')
(* 1. r x y ⟹ star' r x x
2. r x y ⟹ r x y *)
apply (rule refl')
(* r x y ⟹ r x y *)
apply assumption
(* *)
done

― ‹ Demostración automática de r contenida en (star' r) ›
lemma "r x y ⟹ star' r x y"
by (meson refl' step')

lemma rsubsetStar'_b: "r x y ⟹ star' r x y"
by (simp add:step'[OF refl'[of r x]])

― ‹ Demostración declarativa de r contenida en (star' r) ›
lemma rsubsetStar': "r x y ⟹ star' r x y"
proof -
assume 1:"r x y"
have 2: "star' r x x" by (simp add: refl')
show "star' r x y" using 2 1 by (simp add: step')
qed

text ‹ A continuación se prueba una condición suficiente para star' r ›

― ‹ Demostración aplicativa ›
lemma
"⟦star' r y z; r x y⟧ ⟹ star' r x z"
apply (induct rule: star'.induct)
(* 1. ⋀xa. r x xa ⟹ star' r x xa
2. ⋀xa y z. ⟦star' r xa y; r x xa ⟹ star' r x y; r y z; r x xa⟧
⟹ star' r x z *)
apply (simp add: rsubsetStar')
(* ⋀xa y z. ⟦star' r xa y; r x xa ⟹ star' r x y; r y z; r x xa⟧
⟹ star' r x z *)
apply (simp add: step')
(* *)
done

― ‹ Demostración automática ›
lemma star'_subset_star'_l1:
"⟦star' r y z; r x y⟧ ⟹ star' r x z"
by (induct rule: star'.induct)
(auto simp add: rsubsetStar' step')

― ‹ Demostraciones de que (star' r) es transitiva ›

― ‹ Demostración aplicativa ›
lemma "⟦star' r x y; star' r y z⟧ ⟹ star' r x z"
apply (induction rule: star'.induct)
(* 1. ⋀x. star' r x z ⟹ star' r x z
2. ⋀x y za. ⟦star' r x y; star' r y z ⟹ star' r x z; r y za;
star' r za z⟧
⟹ star' r x z *)
apply simp
(* ⋀x y za. ⟦star' r x y; star' r y z ⟹ star' r x z; r y za;
star' r za z⟧
⟹ star' r x z *)
apply (simp add: star'_subset_star'_l1)
(* *)
done

― ‹ Demostración automática ›
lemma star'Trans:
"⟦star' r x y; star' r y z⟧ ⟹ star' r x z"
by (induction rule: star'.induct)
(auto simp add: star'_subset_star'_l1)

text ‹
---------------------------------------------------------------------
Ejercicio 3. Considerar la siguiente definición inductiva. Probar que
"star' r x y syss (∃n. iter r n x y)"
------------------------------------------------------------------- ›

inductive iter :: "('a ⇒ 'a ⇒ bool) ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool"
for r where
iterRefl: "iter r 0 x x"
| iterStep: "⟦iter r n x y; r y z⟧ ⟹ iter r (n+1) x z"

― ‹ El esquema de inducción correspondiente es ›
thm iter.induct
(*
⟦iter ?r ?x1.0 ?x2.0 ?x3.0;
⋀x. ?P 0 x x;
⋀n x y z. ⟦iter ?r n x y; ?P n x y; ?r y z⟧ ⟹ ?P (n + 1) x z⟧
⟹ ?P ?x1.0 ?x2.0 ?x3.0
*)

― ‹ Algunos teoremas derivados son ›

thm iterRefl
(* iter ?r 0 ?x ?x *)

thm iterRefl [of r y]
(* iter r 0 y y *)

thm iterStep
(* ⟦iter ?r ?n ?x ?y; ?r ?y ?z⟧ ⟹ iter ?r (?n + 1) ?x ?z *)

thm iterStep [of r x y n z]
(* ⟦iter r x y n; r n z⟧ ⟹ iter r (x + 1) y z *)

thm iterStep [of r x y 0 y]
(* ⟦iter r x y 0; r 0 y⟧ ⟹ iter r (x + 1) y y *)

text ‹
---------------------------------------------------------------------
Ejercicio 3.1. Demostrar
star' r x y ⟹ (∃n. iter r n x y)
------------------------------------------------------------------- ›

― ‹ Demostración aplicativa ›
lemma "star' r x y ⟹ (∃n. iter r n x y)"
apply (induct rule: star'.induct)
(* 1. ⋀x. ∃n. iter r n x x
2. ⋀x y z. ⟦star' r x y; ∃n. iter r n x y; r y z⟧
⟹ ∃n. iter r n x z *)
apply (rule_tac x=0 in exI)
(* 1. ⋀x. iter r 0 x x
2. ⋀x y z. ⟦star' r x y; ∃n. iter r n x y; r y z⟧
⟹ ∃n. iter r n x z *)
apply (rule iterRefl)
(* ⋀x y z. ⟦star' r x y; ∃n. iter r n x y; r y z⟧
⟹ ∃n. iter r n x z *)
apply (erule exE)
(* ⋀x y z n. ⟦star' r x y; r y z; iter r n x y⟧
⟹ ∃n. iter r n x z *)
apply (rule_tac x="n+1" in exI)
(* ⋀x y z n. ⟦star' r x y; r y z; iter r n x y⟧
⟹ iter r (n + 1) x z *)
apply (erule iterStep)
(* ⋀x y z n. ⟦star' r x y; r y z⟧ ⟹ r y z *)
apply assumption
(* *)
done

― ‹ Demostración automática ›
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"
by (induct rule: star'.induct)
(auto intro: iterRefl iterStep)

― ‹ Demostración declarativa ›
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"
proof (induct rule: star'.induct)
fix x
have "iter r 0 x x" by (rule iterRefl)
then show "∃n. iter r n x x" by (rule exI)
next
fix x y z
assume 1: "star' r x y" and
2: "∃n. iter r n x y" and
3: "r y z"
from 2 obtain m where "iter r m x y" by (rule exE)
then have "iter r (m+1) x z" using 3 by (rule iterStep)
then show "∃n. iter r n x z" by (rule exI)
qed

text ‹
---------------------------------------------------------------------
Ejercicio 3.2. Demostrar
(∃n. iter r n x y) ⟹ star' r x y
------------------------------------------------------------------- ›

― ‹ En la demostración se usará el siguiente lema:
iter r n x y ⟹ star' r x y ›

― ‹ Demostración aplicativa del lema ›
lemma iter_star'_subset: "iter r n x y ⟹ star' r x y"
apply (induct rule: iter.induct)
(* 1. ⋀x. star' r x x
2. ⋀n x y z. ⟦iter r n x y; star' r x y; r y z⟧
⟹ star' r x z *)
apply (rule refl')
(* ⋀n x y z. ⟦iter r n x y; star' r x y; r y z⟧
⟹ star' r x z *)
apply (erule step')
(* ⋀n x y z. ⟦iter r n x y; r y z⟧ ⟹ r y z*)
apply assumption
done

― ‹ Demostración automática del lema ›
lemma "iter r n x y ⟹ star' r x y"
by (induct rule: iter.induct)
(auto simp add: refl' step')

― ‹ Demostración aplicativa ›
lemma "(∃n. iter r n x y) ⟹ star' r x y"
apply (erule exE)
(* ⋀n. iter r n x y ⟹ star' r x y *)
apply (erule iter_star'_subset)
(* *)
done

― ‹ Demostración automática ›
lemma "(∃n. iter r n x y) ⟹ star' r x y"
by (auto simp add: iter_star'_subset)

― ‹ Demostración declarativa ›
lemma assumes "(∃n. iter r n x y)"
shows "star' r x y"
proof -
have "∃n. iter r n x y" using assms .
then obtain k where "iter r k x y" by (rule exE)
then show "star' r x y" by (rule iter_star'_subset)
qed

end

</source>

Rel 15 (sol)

2020-06-29T15:38:30Z

Mjoseh: Página creada con «<source lang = "isabelle"> chapter ‹ R15: Definiciones inductivas: clausuras › theory R15_sol imports Main begin section ‹ La clausura reflexiva transitiva › tex…»

Ejercicios

2020-06-29T15:37:27Z

Mjoseh:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]], [[Relación 1 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf Una solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]], [[Relación 2 |Solución colaborativa]], [[Rel 2 |Una solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]], [[Relación 3 |Solución colaborativa]], [[Rel 3 |Una solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]], [[Relación 4 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf Una solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]], [[Relación 5 |Solución colaborativa]], [[Rel 5 |Una solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]], [[Relación 6 |Solución colaborativa]] , [[Rel 6 |Una solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]], [[Relación 8 |Solución colaborativa]]).
** [[Rel 8 (rev 1) | Primera corrección]]
** [[Rel 8 (sol) | Una solución]]
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]], [[Relación 9 |Solución colaborativa]]).
** [[Rel 9 (rev 1) | Primera corrección]]
** [[Rel 9 (sol) | Una solución]]
* '''Ejercicio 1 (24-04-2020)''': ([[T1 |Enunciado]], [[T1 sol |Una solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]], [[Relación 10 |Solución colaborativa]]).
** [[Rel 10 (sol) | Una solución]]
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]], [[Relación 11 |Solución colaborativa]]).
** [[Rel 11 (sol) | Una solución]]
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]], [[Relación 12 |Solución colaborativa]]).
** [[Rel 12 (sol) | Una solución]]
* '''Ejercicio 2 (12-05-2020)''': ([[T2 |Enunciado]], [[T2 sol |Una solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]], [[Relación 13 |Solución colaborativa]]).
** [[Rel 13 (sol) | Una solución]]
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomátización de la Geometría.] ([[R14 |Enunciado]], [[Relación 14 |Solución colaborativa]]).
** [[Rel 14 (sol) | Una solución]]
* '''Ejercicio 3 (19-05-2020)''': ([[T3 |Enunciado]], [[T3 sol |Una solución]]).
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]], [[Relación 15 |Solución colaborativa]]).
** [[Rel 15 (sol) | Una solución]]
* '''Ejercicio 4 (26-05-2020)''': ([[T4 |Enunciado]], [[T4 sol |Una solución]]).
* '''Ejercicio 5 (02-06-2020)''':
** ([[T5-1 |Enunciado (1)]], [[T5-1 sol |Una solución]]).
** ([[T5-2 |Enunciado (2)]], [[T5-2 sol |Una solución]]).
* '''Trabajo final''': ([[TF |Enunciado]], [[TF sol |Una solución]]).

TF sol

2020-06-18T07:13:48Z

Mjoseh:

<source lang = "isabelle">

chapter ‹Expresiones booleanas y expresiones condicionales›

theory Trabajo_final_sol
imports Main
begin

section ‹Expresiones booleanas›

text ‹------------------------------------------------------------------
Ejercicio 1. La expresiones booleanas se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e es una expresión, entonces ¬e también lo es.
* Si e1 y e2 son expresiones, entonces e1 ∧ e2 también lo es.

Definir exp_booleana como el tipo de las expresiones booleanas.
---------------------------------------------------------------------›

datatype exp_booleana = Const bool
| Var nat
| Neg exp_booleana
| And exp_booleana exp_booleana

section ‹El valor de las expresiones boolenas›

text ‹------------------------------------------------------------------
Ejercicio 2. Una interpretación es una función i que asigna a cada
número natural un booleano de forma que el valor de la variable
'Var n' en la interpretación 'i' es 'i(n)'.

Definir la función
valor :: exp_booleana ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor e i) es el valor de la expresión booleana e en la
interpretación i. Por ejemplo,
value "(valor (Var 3) (λx. False))
es False
---------------------------------------------------------------------›

fun valor :: "exp_booleana ⇒ (nat ⇒ bool) ⇒ bool" where
"valor (Const b) _ = b"
| "valor (Var n) i = i n "
| "valor (Neg e) i = (¬ (valor e i))"
| "valor (And e1 e2) i = (valor e1 i ∧ valor e2 i)"

section ‹Expresiones If›

text ‹------------------------------------------------------------------
Ejercicio 3. La expresiones if se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e, e1 y e2 son expresiones, entonces (if e e1 e2) también lo es.

Definir exp_if como el tipo de las expresiones if.
---------------------------------------------------------------------›

datatype exp_if = CIF bool
| VIF nat
| IF exp_if exp_if exp_if

text ‹------------------------------------------------------------------
Ejercicio 4. Definir la función
valor_if :: exp_if ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor_if e i) es el valor de la expresión if e en la
interpretación i.
---------------------------------------------------------------------›

fun valor_if :: "exp_if ⇒ (nat ⇒ bool) ⇒ bool" where
"valor_if (CIF b) _ = b"
| "valor_if (VIF n) i = i n"
| "valor_if (IF e e1 e2) i = (if (valor_if e i)
then (valor_if e1 i)
else (valor_if e2 i))"

section ‹Transformación de expresiones booleanas en expresiones if›

subsection ‹Definición de bool2if›

text ‹------------------------------------------------------------------
Ejercicio 5. Definir la función
bool2if :: exp_booleana ⇒ exp_if
tal que (bool2if e) es una expresión if equivalente a la expresión
booleana e.
---------------------------------------------------------------------›

fun bool2if :: "exp_booleana ⇒ exp_if" where
"bool2if (Const b) = CIF b"
| "bool2if (Var n) = VIF n"
| "bool2if (Neg e) = IF (bool2if e) (CIF False) (CIF True)"
| "bool2if (And e1 e2) = IF (bool2if e1) (bool2if e2) (CIF False)"

text ‹------------------------------------------------------------------
Ejercicio 6. Demostrar que para cualquier expresión boolena e, son
equivalentes (bool2if e) y e.
---------------------------------------------------------------------›

subsection ‹Demostraciones de valor_if_bool2if›

subsubsection ‹Demostración estructurada de valor_if_bool2if›
lemma valor_if_bool2if_E:
"valor_if (bool2if e) ent = valor e ent"
proof (induct e)
case (Const x)
then show ?case by simp
next
case (Var x)
then show ?case by simp
next
case (Neg e)
then show ?case by simp
next
case (And e1 e2)
then show ?case by simp
qed

subsubsection ‹Demostración automática de valor_if_bool2if›

lemma valor_if_bool2if_A:
"valor_if (bool2if e) ent = valor e ent"
by (induct e) simp_all

subsubsection ‹Demostración declarativa detallada de valor_if_bool2if›

lemma valor_if_bool2if:
"valor_if (bool2if e) ent = valor e ent"
proof (induct e)
fix b
have "valor_if (bool2if (Const b)) ent = valor_if (CIF b) ent"
by (simp only: bool2if.simps(1))
also have "… = b"
by (simp only: valor_if.simps(1))
also have "… = valor (Const b) ent"
by (simp only: valor.simps(1))
finally show "valor_if (bool2if (Const b)) ent = valor (Const b) ent"
by this
next
fix n
have "valor_if (bool2if (Var n)) ent = valor_if (VIF n) ent"
by (simp only: bool2if.simps(2))
also have "… = ent n"
by (simp only: valor_if.simps(2))
also have "… = valor (Var n) ent"
by (simp only: valor.simps(2))
finally show "valor_if (bool2if (Var n)) ent = valor (Var n) ent"
by this
next
fix e
assume HI: "valor_if (bool2if e) ent = valor e ent"
have "valor_if (bool2if (Neg e)) ent =
valor_if (IF (bool2if e) (CIF False) (CIF True)) ent"
by (simp only: bool2if.simps(3))
also have "… = (if valor_if (bool2if e) ent
then valor_if (CIF False) ent
else valor_if (CIF True) ent)"
by (simp only: valor_if.simps(3))
also have "… = (if valor e ent
then False
else True)"
by (simp only: HI valor_if.simps(1))
also have "… = (¬ valor e ent)"
by (rule SMT.z3_rule(52))
also have "… = valor (Neg e) ent"
by (simp only: valor.simps(3))
finally show "valor_if (bool2if (Neg e)) ent = valor (Neg e) ent"
by this
next
fix e1 e2
assume HI1: "valor_if (bool2if e1) ent = valor e1 ent" and
HI2: "valor_if (bool2if e2) ent = valor e2 ent"
have "valor_if (bool2if (And e1 e2)) ent =
valor_if (IF (bool2if e1) (bool2if e2) (CIF False)) ent"
by (simp only: bool2if.simps(4))
also have "… = (if valor_if (bool2if e1) ent
then valor_if (bool2if e2) ent
else valor_if (CIF False) ent)"
by (simp only: valor_if.simps(3))
also have "… = (if valor e1 ent
then valor e2 ent
else False)"
by (simp only: HI1 HI2 valor_if.simps(1))
also have "… = ((valor e1 ent ∧ valor e2 ent) ∨
(¬(valor e1 ent) ∧ False))"
by (rule if_bool_eq_disj)
also have "… = ((valor e1 ent ∧ valor e2 ent) ∨ False)"
by (simp only: simp_thms(23))
also have "… = (valor e1 ent ∧ valor e2 ent)"
by (simp only: simp_thms(31))
also have "… = valor (And e1 e2) ent"
by (simp only: valor.simps(4))
finally show "valor_if (bool2if (And e1 e2)) ent =
valor (And e1 e2) ent"
by this
qed

subsubsection ‹Demostración aplicativa detallada de valor_if_bool2if›

lemma valor_if_bool2if_aplicativa:
"valor_if (bool2if e) ent = valor e ent"
apply (induct e)
apply (simp only: bool2if.simps valor_if.simps valor.simps)
apply (simp only: bool2if.simps valor_if.simps valor.simps)
apply (simp only: bool2if.simps)
apply (simp only: valor_if.simps)
apply (simp only: valor.simps)
apply (split if_split)
apply (rule conjI)
apply (rule impI)
apply (rule iffI)
apply (rule ccontr, assumption)
apply (erule notE, assumption)
apply (rule impI)
apply (rule iffI, assumption)
apply (simp only: TrueI)
apply (simp only: bool2if.simps)
apply (simp only: valor_if.simps)
apply (simp only: valor.simps)
apply (split if_split)
apply (rule conjI)
apply (rule impI)
apply (rule iffI)
apply (erule conjI, assumption)
apply (erule conjunct2)
apply (rule impI)
apply (rule iffI)
apply (rule FalseE, assumption)
apply (erule notE)
apply (erule conjunct1)
done

section ‹Formas normales›

subsection ‹Definición de es_normal›

text ‹------------------------------------------------------------------
Ejercicio 6. Un expresión if, e, está en forma normal si para cada
subexpresión de e de la forma (if c e1 e2) se tiene que c es una
constante o una variable.

Definir la función
es_normal :: exp_if ⇒ bool
tal que (es_normal e) se verifica si e está en forma normal.
---------------------------------------------------------------------›

fun es_normal :: "exp_if ⇒ bool" where
"es_normal (CIF _) = True"
| "es_normal (VIF _) = True"
| "es_normal (IF (CIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal (IF (VIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal _ = False"

subsection ‹Definición de normal›

text ‹------------------------------------------------------------------
Ejercicio 7. Definir la función
normal :: exp_if ⇒ exp_if
tal que (normal e) es una expresión if en forma normal equivalente a
la expresión e.
--------------------------------------------------------------------- ›

fun normalAux :: "exp_if ⇒ exp_if ⇒ exp_if ⇒ exp_if" where
"normalAux (CIF b) e1 e2 = IF (CIF b) e1 e2"
| "normalAux (VIF n) e1 e2 = IF (VIF n) e1 e2"
| "normalAux (IF a a1 a2) e1 e2 =
normalAux a (normalAux a1 e1 e2) (normalAux a2 e1 e2)"

fun normal :: "exp_if ⇒ exp_if" where
"normal (CIF b) = CIF b"
| "normal (VIF n) = VIF n"
| "normal (IF e e1 e2) = normalAux e (normal e1) (normal e2)"

section ‹Corrección de la normalización›

text ‹------------------------------------------------------------------
Ejercicio 8. Demostrar que la forma normal de una expresión if es
equivalente a la expresión; es decir,
valor_if (normal e) i = valor_if e i
---------------------------------------------------------------------›

subsection ‹Lema auxiliar valor_if_normalAux›

subsubsection ‹Demostración estructurada de valor_if_normalAux›

lemma valor_if_normalAux_E:
"valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
proof (induct e arbitrary: e1 e2)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF e1 e2 e3)
then show ?case by simp
qed

subsubsection ‹Demostración automática de valor_if_normalAux›

lemma valor_if_normalAux_A:
"valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
by (induct e arbitrary: e1 e2) simp_all

subsubsection ‹Demostración declarativa detallada de valor_if_normalAux›

lemma if_if:
fixes A and A1 and A2 and C1 and C2 :: bool
shows
"(if A
then (if A1 then C1 else C2)
else (if A2 then C1 else C2)) =
(if (if A then A1 else A2)
then C1
else C2)"
by (cases A; cases A1; cases A2)
(simp_all only: if_True if_False)

lemma valor_if_IF:
"valor_if (IF a (IF a1 c1 c2) (IF a2 c1 c2)) ent =
valor_if (IF (IF a a1 a2) c1 c2) ent"
by (simp only: valor_if.simps(3) if_if)

lemma valor_if_normalAux:
"valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
proof (induct e arbitrary: e1 e2)
fix b e1 e2
show "valor_if (normalAux (CIF b) e1 e2) ent =
valor_if (IF (CIF b) e1 e2) ent"
by (simp only: normalAux.simps(1))
next
fix n e1 e2
show "valor_if (normalAux (VIF n) e1 e2) ent =
valor_if (IF (VIF n) e1 e2) ent"
by (simp only: normalAux.simps(2))
next
fix a a1 a2 c1 c2
assume HI: "⋀e1 e2. valor_if (normalAux a e1 e2) ent =
valor_if (IF a e1 e2) ent" and
HI1: "⋀e1 e2. valor_if (normalAux a1 e1 e2) ent =
valor_if (IF a1 e1 e2) ent" and
HI2: "⋀e1 e2. valor_if (normalAux a2 e1 e2) ent =
valor_if (IF a2 e1 e2) ent"
show "valor_if (normalAux (IF a a1 a2) c1 c2) ent =
valor_if (IF (IF a a1 a2) c1 c2) ent"
proof -
have "valor_if (normalAux (IF a a1 a2) c1 c2) ent =
valor_if (normalAux a
(normalAux a1 c1 c2)
(normalAux a2 c1 c2)) ent"
by (simp only: normalAux.simps(3))
also have "… = valor_if (IF a
(normalAux a1 c1 c2)
(normalAux a2 c1 c2)) ent"
by (simp only: HI)
also have "… = (if valor_if a ent
then valor_if (normalAux a1 c1 c2) ent
else valor_if (normalAux a2 c1 c2) ent)"
by (simp only: valor_if.simps(3))
also have "… = (if valor_if a ent
then valor_if (IF a1 c1 c2) ent
else valor_if (IF a2 c1 c2) ent)"
by (simp only: HI1 HI2)
also have "… = valor_if (IF a (IF a1 c1 c2) (IF a2 c1 c2)) ent"
by (simp only: valor_if.simps(3))
also have "… = valor_if (IF (IF a a1 a2) c1 c2) ent"
by (simp only: valor_if_IF)
finally show ?thesis
by this
qed
qed

subsubsection ‹Demostración aplicativa detallada de valor_if_normalAux›

lemma valor_if_normalAux_aplicativo:
"∀e1 e2. valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
apply (induct e)
apply (rule allI)+
apply (simp only: normalAux.simps(1))
apply (rule allI)+
apply (simp only: normalAux.simps(2))
apply (rule allI)+
apply (simp only: normalAux.simps(3))
apply (simp only: valor_if.simps(3))
apply (case_tac "valor_if e1 ent")
apply (simp only: if_True)
apply (simp only: if_False)
done

subsection ‹Demostraciones del teorema valor_if_normal›

subsubsection ‹Demostración estructurada del teorema valor_if_normal›

theorem valor_if_normal_E:
"valor_if (normal b) ent = valor_if b ent"
proof (induct b)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF b1 b2 b3)
then show ?case by (simp add: valor_if_normalAux)
qed

subsubsection ‹Demostración automática del teorema valor_if_normal›

theorem valor_if_normal_A:
"valor_if (normal b) ent = valor_if b ent"
by (induct b) (simp_all add: valor_if_normalAux)

subsubsection ‹Demostración declarativa detallada del teorema valor_if_normal›

theorem valor_if_normal:
"valor_if (normal b) ent = valor_if b ent"
proof (induct b)
fix b
show "valor_if (normal (CIF b)) ent = valor_if (CIF b) ent"
by (simp only: normal.simps(1) valor_if.simps(1))
next
fix n
show "valor_if (normal (VIF n)) ent = valor_if (VIF n) ent"
by (simp only: normal.simps(2) valor_if.simps(2))
next
fix e e1 e2
assume HI: "valor_if (normal e) ent = valor_if e ent" and
HI1: "valor_if (normal e1) ent = valor_if e1 ent" and
HI2: "valor_if (normal e2) ent = valor_if e2 ent"
show "valor_if (normal (IF e e1 e2)) ent =
valor_if (IF e e1 e2) ent"
proof -
have "valor_if (normal (IF e e1 e2)) ent =
valor_if (normalAux e (normal e1) (normal e2)) ent"
by (simp only: normal.simps(3))
also have "… = valor_if (IF e (normal e1) (normal e2)) ent"
by (simp only: valor_if_normalAux)
also have "… = (if (valor_if e ent)
then (valor_if (normal e1) ent)
else (valor_if (normal e2) ent))"
by (simp only: valor_if.simps(3))
also have "… = (if (valor_if e ent)
then (valor_if e1 ent)
else (valor_if e2 ent))"
by (simp only: HI1 HI2)
also have "… = valor_if (IF e e1 e2) ent"
by (simp only: valor_if.simps(3))
finally show ?thesis
by this
qed
qed

subsubsection ‹Demostración aplicativa detallada del teorema valor_if_normal›

lemma valor_if_normal_aplicativo:
"valor_if (normal b) ent = valor_if b ent"
apply (induct b)
apply (simp only: normal.simps(1))
apply (simp only: normal.simps(2))
apply (simp only: normal.simps(3))
apply (simp only: valor_if_normalAux_aplicativo)
apply (simp only: valor_if.simps(3))
done

text ‹------------------------------------------------------------------
Ejercicio 9. Demostrar que para toda expresión if e, (normal e) está
en forma normal.
---------------------------------------------------------------------›

subsection ‹Lema auxiliar es_normal_normalAux›

subsubsection ‹Demostración estructurada de es_normal_normalAux›

lemma es_normal_normalAux_E:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
proof (induct e arbitrary: e1 e2)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF e1 e2 e3)
then show ?case by simp
qed

subsubsection ‹Demostración automática de es_normal_normalAux›

lemma es_normal_normalAux_A:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
by (induct e arbitrary: e1 e2) simp_all

subsubsection ‹Demostración declarativa detallada de es_normal_normalAux›

lemma es_normal_normalAux:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
proof (induct e arbitrary: e1 e2)
fix b e1 e2
have "es_normal (normalAux (CIF b) e1 e2) =
es_normal (IF (CIF b) e1 e2)"
by (simp only: normalAux.simps(1))
also have "… = (es_normal e1 ∧ es_normal e2)"
by (simp only: es_normal.simps(3))
finally show "es_normal (normalAux (CIF b) e1 e2) =
(es_normal e1 ∧ es_normal e2)"
by this
next
fix n e1 e2
have "es_normal (normalAux (VIF n) e1 e2) =
es_normal (IF (VIF n) e1 e2)"
by (simp only: normalAux.simps(2))
also have "… = (es_normal e1 ∧ es_normal e2)"
by (simp only: es_normal.simps(4))
finally show "es_normal (normalAux (VIF n) e1 e2) =
(es_normal e1 ∧ es_normal e2)"
by this
next
fix a a1 a2 e1 e2
assume
HI: "⋀e1 e2. es_normal (normalAux a e1 e2) =
(es_normal e1 ∧ es_normal e2)" and
HI1: "⋀e1 e2. es_normal (normalAux a1 e1 e2) =
(es_normal e1 ∧ es_normal e2)" and
HI2: "⋀e1 e2. es_normal (normalAux a2 e1 e2) =
(es_normal e1 ∧ es_normal e2)"
have "es_normal (normalAux (IF a a1 a2) e1 e2) =
es_normal (normalAux a
(normalAux a1 e1 e2)
(normalAux a2 e1 e2))"
by (simp only: normalAux.simps(3))
also have "… = (es_normal (normalAux a1 e1 e2) ∧
es_normal (normalAux a2 e1 e2))"
by (simp only: HI)
also have "… = ((es_normal e1 ∧ es_normal e2) ∧
(es_normal e1 ∧ es_normal e2))"
by (simp only: HI1 HI2)
also have "… = (es_normal e1 ∧ es_normal e2)"
by (simp only: conj_absorb)
finally show "es_normal (normalAux (IF a a1 a2) e1 e2) =
(es_normal e1 ∧ es_normal e2)"
by this
qed

subsubsection ‹Demostración aplicativa detallada de es_normal_normalAux›

lemma es_normal_normalAux_aplicativa:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
apply (induct e arbitrary: e1 e2)
apply (simp only: normalAux.simps es_normal.simps)+
apply (rule iffI)
apply (erule conjunct2)
apply (rule conjI)
apply assumption+
done

subsection ‹Demostraciones del teorema es_normal_normal›

subsubsection ‹Demostración estructurada del teorema es_normal_normal›

theorem es_normal_normal_E:
"es_normal (normal b)"
proof (induct b)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF b1 b2 b3)
then show ?case by (simp add: es_normal_normalAux)
qed

subsubsection ‹Demostración automática del teorema es_normal_normal›

theorem es_normal_normal_A:
"es_normal (normal b)"
by (induct b) (simp_all add: es_normal_normalAux)

subsubsection ‹Demostración declarativa detallada del teorema
es_normal_normal›

theorem es_normal_normal:
"es_normal (normal b)"
proof (induct b)
fix b
show "es_normal (normal (CIF b))"
by (simp only: normal.simps(1) es_normal.simps(1))
next
fix n
show "es_normal (normal (VIF n))"
by (simp only: normal.simps(2) es_normal.simps(2))
next
fix e e1 e2
assume "es_normal (normal e)"
"es_normal (normal e1)"
"es_normal (normal e2)"
then show "es_normal (normal (IF e e1 e2))"
by (simp only: normal.simps(3) es_normal_normalAux)
qed

subsubsection ‹Demostración aplicativa detallada del teorema
es_normal_normal›

lemma es_normal_normal_aplicativa:
"es_normal (normal b)"
apply (induct b)
apply (simp only: normal.simps(1))
apply (simp only: es_normal.simps(1))
apply (simp only: normal.simps(2))
apply (simp only: es_normal.simps(2))
apply (simp only: normal.simps)
apply (simp only: es_normal_normalAux_aplicativa)
done

section ‹Definición de bool2ifN›

text ‹------------------------------------------------------------------
Ejercicio 10. Definir la función
bool2ifN :: exp_booleana ⇒ exp_if
tal que (bool2ifN e) es una expresión if en forma normal equivalente a
la expresión Booleana e.
---------------------------------------------------------------------›

definition bool2ifN :: "exp_booleana ⇒ exp_if" where
"bool2ifN e ≡ normal (bool2if e)"

section ‹Lema es_normal_bool2ifN›

text ‹------------------------------------------------------------------
Ejercicio 11. Demostrar que para toda expresión booleana e,
(bool2ifN e) está en forma normal.
---------------------------------------------------------------------›

subsection ‹Demostración automática de es_normal_bool2ifN›

theorem es_normal_bool2ifN_A:
"es_normal (bool2ifN e)"
by (simp only: bool2ifN_def es_normal_normal)

subsection ‹Demostración declarativa detallada de es_normal_bool2ifN›

lemma es_normal_bool2ifN:
"es_normal (bool2ifN e)"
proof-
have "bool2ifN e = normal (bool2if e)"
by (simp only: bool2ifN_def)
then show "es_normal (bool2ifN e)"
by (simp only: es_normal_normal)
qed

subsection ‹Demostración aplicativa detallada de es_normal_bool2ifN›

lemma es_normal_bool2ifN_aplicativa:
"es_normal (bool2ifN e)"
apply (simp only: bool2ifN_def)
apply (simp only: es_normal_normal)
done

section ‹Lema valor_if_bool2ifN›

text ‹------------------------------------------------------------------
Ejercicio 12. Demostrar que para toda expresión booleana e,
(bool2ifN e) es equivalente a e.
---------------------------------------------------------------------›

subsection ‹Demostración automática de valor_if_bool2ifN›

theorem valor_if_bool2ifN_A:
"valor_if (bool2ifN e) ent = valor e ent"
by (simp only: bool2ifN_def valor_if_bool2if valor_if_normal)

subsection ‹Demostración declarativa detallada de valor_if_bool2ifN›

lemma valor_if_bool2ifN:
"valor_if (bool2ifN e) ent = valor e ent"
proof -
have "bool2ifN e ≡ normal (bool2if e)"
by (simp only: bool2ifN_def)
then have "valor_if (bool2ifN e) ent =
valor_if (normal (bool2if e)) ent"
by (simp only: )
also have "… = valor_if (bool2if e) ent"
by (simp only: valor_if_normal)
also have "… = valor e ent"
by (simp only: valor_if_bool2if)
finally show "valor_if (bool2ifN e) ent = valor e ent"
by this
qed

subsection ‹Demostración aplicativa detallada de valor_if_bool2ifN›

lemma valor_if_bool2ifN_aplicativa:
"valor_if (bool2ifN e) ent = valor e ent"
apply (simp only: bool2ifN_def)
apply (simp only: valor_if_normal)
apply (simp only: valor_if_bool2if)
done

end

</source>

TF sol

2020-06-18T06:53:16Z

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

<source lang = "isabelle">
chapter ‹Expresiones booleanas y expresiones condicionales›

theory Trabajo_final_sol
imports Main
begin

section ‹Expresiones booleanas›

text ‹------------------------------------------------------------------
Ejercicio 1. La expresiones booleanas se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e es una expresión, entonces ¬e también lo es.
* Si e1 y e2 son expresiones, entonces e1 ∧ e2 también lo es.

Definir exp_booleana como el tipo de las expresiones booleanas.
---------------------------------------------------------------------›

datatype exp_booleana = Const bool
| Var nat
| Neg exp_booleana
| And exp_booleana exp_booleana

section ‹El valor de las expresiones boolenas›

text ‹------------------------------------------------------------------
Ejercicio 2. Una interpretación es una función i que asigna a cada
número natural un booleano de forma que el valor de la variable
'Var n' en la interpretación 'i' es 'i(n)'.

Definir la función
valor :: exp_booleana ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor e i) es el valor de la expresión booleana e en la
interpretación i. Por ejemplo,
value "(valor (Var 3) (λx. False))
es False
---------------------------------------------------------------------›

fun valor :: "exp_booleana ⇒ (nat ⇒ bool) ⇒ bool" where
"valor (Const b) _ = b"
| "valor (Var n) i = i n "
| "valor (Neg e) i = (¬ (valor e i))"
| "valor (And e1 e2) i = (valor e1 i ∧ valor e2 i)"

section ‹Expresiones If›

text ‹------------------------------------------------------------------
Ejercicio 3. La expresiones if se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e, e1 y e2 son expresiones, entonces (if e e1 e2) también lo es.

Definir exp_if como el tipo de las expresiones if.
---------------------------------------------------------------------›

datatype exp_if = CIF bool
| VIF nat
| IF exp_if exp_if exp_if

text ‹------------------------------------------------------------------
Ejercicio 4. Definir la función
valor_if :: exp_if ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor_if e i) es el valor de la expresión if e en la
interpretación i.
---------------------------------------------------------------------›

fun valor_if :: "exp_if ⇒ (nat ⇒ bool) ⇒ bool" where
"valor_if (CIF b) _ = b"
| "valor_if (VIF n) i = i n"
| "valor_if (IF e e1 e2) i = (if (valor_if e i)
then (valor_if e1 i)
else (valor_if e2 i))"

section ‹Transformación de expresiones booleanas en expresiones if›

subsection ‹Definición de bool2if›

text ‹------------------------------------------------------------------
Ejercicio 5. Definir la función
bool2if :: exp_booleana ⇒ exp_if
tal que (bool2if e) es una expresión if equivalente a la expresión
booleana e.
---------------------------------------------------------------------›

fun bool2if :: "exp_booleana ⇒ exp_if" where
"bool2if (Const b) = CIF b"
| "bool2if (Var n) = VIF n"
| "bool2if (Neg e) = IF (bool2if e) (CIF False) (CIF True)"
| "bool2if (And e1 e2) = IF (bool2if e1) (bool2if e2) (CIF False)"

text ‹------------------------------------------------------------------
Ejercicio 6. Demostrar que para cualquier expresión boolena e, son
equivalentes (bool2if e) y e.
---------------------------------------------------------------------›

subsection ‹Demostraciones de valor_if_bool2if›

subsubsection ‹Demostración estructurada de valor_if_bool2if›
lemma valor_if_bool2if_E:
"valor_if (bool2if e) ent = valor e ent"
proof (induct e)
case (Const x)
then show ?case by simp
next
case (Var x)
then show ?case by simp
next
case (Neg e)
then show ?case by simp
next
case (And e1 e2)
then show ?case by simp
qed

subsubsection ‹Demostración automática de valor_if_bool2if›
lemma valor_if_bool2if_A:
"valor_if (bool2if e) ent = valor e ent"
by (induct e) simp_all

subsubsection ‹Demostración declarativa detallada de valor_if_bool2if›
lemma valor_if_bool2if:
"valor_if (bool2if e) ent = valor e ent"
proof (induct e)
fix b
have "valor_if (bool2if (Const b)) ent = valor_if (CIF b) ent"
by (simp only: bool2if.simps(1))
also have "… = b"
by (simp only: valor_if.simps(1))
also have "… = valor (Const b) ent"
by (simp only: valor.simps(1))
finally show "valor_if (bool2if (Const b)) ent = valor (Const b) ent"
by this
next
fix n
have "valor_if (bool2if (Var n)) ent = valor_if (VIF n) ent"
by (simp only: bool2if.simps(2))
also have "… = ent n"
by (simp only: valor_if.simps(2))
also have "… = valor (Var n) ent"
by (simp only: valor.simps(2))
finally show "valor_if (bool2if (Var n)) ent = valor (Var n) ent"
by this
next
fix e
assume HI: "valor_if (bool2if e) ent = valor e ent"
have "valor_if (bool2if (Neg e)) ent =
valor_if (IF (bool2if e) (CIF False) (CIF True)) ent"
by (simp only: bool2if.simps(3))
also have "… = (if valor_if (bool2if e) ent
then valor_if (CIF False) ent
else valor_if (CIF True) ent)"
by (simp only: valor_if.simps(3))
also have "… = (if valor e ent
then False
else True)"
by (simp only: HI valor_if.simps(1))
also have "… = (¬ valor e ent)"
by (rule SMT.z3_rule(52))
also have "… = valor (Neg e) ent"
by (simp only: valor.simps(3))
finally show "valor_if (bool2if (Neg e)) ent = valor (Neg e) ent"
by this
next
fix e1 e2
assume HI1: "valor_if (bool2if e1) ent = valor e1 ent" and
HI2: "valor_if (bool2if e2) ent = valor e2 ent"
have "valor_if (bool2if (And e1 e2)) ent =
valor_if (IF (bool2if e1) (bool2if e2) (CIF False)) ent"
by (simp only: bool2if.simps(4))
also have "… = (if valor_if (bool2if e1) ent
then valor_if (bool2if e2) ent
else valor_if (CIF False) ent)"
by (simp only: valor_if.simps(3))
also have "… = (if valor e1 ent
then valor e2 ent
else False)"
by (simp only: HI1 HI2 valor_if.simps(1))
also have "… = ((valor e1 ent ∧ valor e2 ent) ∨
(¬(valor e1 ent) ∧ False))"
by (rule if_bool_eq_disj)
also have "… = ((valor e1 ent ∧ valor e2 ent) ∨ False)"
by (simp only: simp_thms(23))
also have "… = (valor e1 ent ∧ valor e2 ent)"
by (simp only: simp_thms(31))
also have "… = valor (And e1 e2) ent"
by (simp only: valor.simps(4))
finally show "valor_if (bool2if (And e1 e2)) ent =
valor (And e1 e2) ent"
by this
qed

subsubsection ‹Demostración aplicativa detallada de valor_if_bool2if›
lemma valor_if_bool2if_aplicativa:
"valor_if (bool2if e) ent = valor e ent"
apply(induct e)
apply(simp only: bool2if.simps
valor_if.simps
valor.simps)
apply(simp only: bool2if.simps
valor_if.simps
valor.simps)
apply(simp only: bool2if.simps)
apply(simp only: valor_if.simps)
apply(simp only: valor.simps)
apply(split if_split)
apply(rule conjI)
apply(rule impI)
apply(rule iffI)
apply(rule ccontr, assumption)
apply(erule notE, assumption)
apply(rule impI)
apply(rule iffI, assumption)
apply(simp only: TrueI)
apply(simp only: bool2if.simps)
apply(simp only: valor_if.simps)
apply(simp only: valor.simps)
apply(split if_split)
apply(rule conjI)
apply(rule impI)
apply(rule iffI)
apply(erule conjI, assumption)
apply(erule conjunct2)
apply(rule impI)
apply(rule iffI)
apply (rule FalseE, assumption)
apply(erule notE)
apply(erule conjunct1)
done

section ‹Formas normales›

subsection ‹Definición de es_normal›

text ‹------------------------------------------------------------------
Ejercicio 6. Un expresión if, e, está en forma normal si para cada
subexpresión de e de la forma (if c e1 e2) se tiene que c es una
constante o una variable.

Definir la función
es_normal :: exp_if ⇒ bool
tal que (es_normal e) se verifica si e está en forma normal.
---------------------------------------------------------------------›

fun es_normal :: "exp_if ⇒ bool" where
"es_normal (CIF _) = True"
| "es_normal (VIF _) = True"
| "es_normal (IF (CIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal (IF (VIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal _ = False"

subsection ‹Definición de normal›

text ‹------------------------------------------------------------------
Ejercicio 7. Definir la función
normal :: exp_if ⇒ exp_if
tal que (normal e) es una expresión if en forma normal equivalente a
la expresión e.
--------------------------------------------------------------------- ›

fun normalAux :: "exp_if ⇒ exp_if ⇒ exp_if ⇒ exp_if" where
"normalAux (CIF b) e1 e2 = IF (CIF b) e1 e2"
| "normalAux (VIF n) e1 e2 = IF (VIF n) e1 e2"
| "normalAux (IF a a1 a2) e1 e2 =
normalAux a (normalAux a1 e1 e2) (normalAux a2 e1 e2)"

fun normal :: "exp_if ⇒ exp_if" where
"normal (CIF b) = CIF b"
| "normal (VIF n) = VIF n"
| "normal (IF e e1 e2) = normalAux e (normal e1) (normal e2)"

section ‹Corrección de la normalización›

text ‹------------------------------------------------------------------
Ejercicio 8. Demostrar que la forma normal de una expresión if es
equivalente a la expresión; es decir,
valor_if (normal e) i = valor_if e i
---------------------------------------------------------------------›

subsection ‹Lema auxiliar valor_if_normalAux›

subsubsection ‹Demostración estructurada de valor_if_normalAux›
lemma valor_if_normalAux_E:
"valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
proof (induct e arbitrary: e1 e2)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF e1 e2 e3)
then show ?case by simp
qed

subsubsection ‹Demostración automática de valor_if_normalAux›
lemma valor_if_normalAux_A:
"valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
by (induct e arbitrary: e1 e2) simp_all

subsubsection ‹Demostración declarativa detallada de valor_if_normalAux›

lemma if_if:
fixes A and A1 and A2 and C1 and C2 :: bool
shows
"(if A
then (if A1 then C1 else C2)
else (if A2 then C1 else C2)) =
(if (if A then A1 else A2)
then C1
else C2)"
by (cases A; cases A1; cases A2)
(simp_all only: if_True if_False)

lemma valor_if_IF:
"valor_if (IF a (IF a1 c1 c2) (IF a2 c1 c2)) ent =
valor_if (IF (IF a a1 a2) c1 c2) ent"
by (simp only: valor_if.simps(3) if_if)

lemma valor_if_normalAux:
"valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
proof (induct e arbitrary: e1 e2)
fix b e1 e2
show "valor_if (normalAux (CIF b) e1 e2) ent =
valor_if (IF (CIF b) e1 e2) ent"
by (simp only: normalAux.simps(1))
next
fix n e1 e2
show "valor_if (normalAux (VIF n) e1 e2) ent =
valor_if (IF (VIF n) e1 e2) ent"
by (simp only: normalAux.simps(2))
next
fix a a1 a2 c1 c2
assume HI: "⋀e1 e2. valor_if (normalAux a e1 e2) ent =
valor_if (IF a e1 e2) ent" and
HI1: "⋀e1 e2. valor_if (normalAux a1 e1 e2) ent =
valor_if (IF a1 e1 e2) ent" and
HI2: "⋀e1 e2. valor_if (normalAux a2 e1 e2) ent =
valor_if (IF a2 e1 e2) ent"
show "valor_if (normalAux (IF a a1 a2) c1 c2) ent =
valor_if (IF (IF a a1 a2) c1 c2) ent"
proof -
have "valor_if (normalAux (IF a a1 a2) c1 c2) ent =
valor_if (normalAux a
(normalAux a1 c1 c2)
(normalAux a2 c1 c2)) ent"
by (simp only: normalAux.simps(3))
also have "… = valor_if (IF a
(normalAux a1 c1 c2)
(normalAux a2 c1 c2)) ent"
by (simp only: HI)
also have "… = (if valor_if a ent
then valor_if (normalAux a1 c1 c2) ent
else valor_if (normalAux a2 c1 c2) ent)"
by (simp only: valor_if.simps(3))
also have "… = (if valor_if a ent
then valor_if (IF a1 c1 c2) ent
else valor_if (IF a2 c1 c2) ent)"
by (simp only: HI1 HI2)
also have "… = valor_if (IF a (IF a1 c1 c2) (IF a2 c1 c2)) ent"
by (simp only: valor_if.simps(3))
also have "… = valor_if (IF (IF a a1 a2) c1 c2) ent"
by (simp only: valor_if_IF)
finally show ?thesis
by this
qed
qed

subsubsection ‹Demostración aplicativa detallada de valor_if_normalAux›
lemma valor_if_normalAux_aplicativo:
"∀e1 e2. valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
apply (induct e)
apply (rule allI)+
apply (simp only: normalAux.simps(1))
apply (rule allI)+
apply (simp only: normalAux.simps(2))
apply (rule allI)+
apply (simp only: normalAux.simps(3))
apply (simp only: valor_if.simps(3))
apply (case_tac "valor_if e1 ent")
apply (simp only: if_True)
apply (simp only: if_False)
done

subsection ‹Demostraciones del teorema valor_if_normal›

subsubsection ‹Demostración estructurada del teorema valor_if_normal›
theorem valor_if_normal_E:
"valor_if (normal b) ent = valor_if b ent"
proof (induct b)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF b1 b2 b3)
then show ?case by (simp add: valor_if_normalAux)
qed

subsubsection ‹Demostración automática del teorema valor_if_normal›
theorem valor_if_normal_A:
"valor_if (normal b) ent = valor_if b ent"
by (induct b) (simp_all add: valor_if_normalAux)

subsubsection ‹Demostración declarativa detallada del teorema valor_if_normal›
theorem valor_if_normal:
"valor_if (normal b) ent = valor_if b ent"
proof (induct b)
fix b
show "valor_if (normal (CIF b)) ent = valor_if (CIF b) ent"
by (simp only: normal.simps(1) valor_if.simps(1))
next
fix n
show "valor_if (normal (VIF n)) ent = valor_if (VIF n) ent"
by (simp only: normal.simps(2) valor_if.simps(2))
next
fix e e1 e2
assume HI: "valor_if (normal e) ent = valor_if e ent" and
HI1: "valor_if (normal e1) ent = valor_if e1 ent" and
HI2: "valor_if (normal e2) ent = valor_if e2 ent"
show "valor_if (normal (IF e e1 e2)) ent =
valor_if (IF e e1 e2) ent"
proof -
have "valor_if (normal (IF e e1 e2)) ent =
valor_if (normalAux e (normal e1) (normal e2)) ent"
by (simp only: normal.simps(3))
also have "… = valor_if (IF e (normal e1) (normal e2)) ent"
by (simp only: valor_if_normalAux)
also have "… = (if (valor_if e ent)
then (valor_if (normal e1) ent)
else (valor_if (normal e2) ent))"
by (simp only: valor_if.simps(3))
also have "… = (if (valor_if e ent)
then (valor_if e1 ent)
else (valor_if e2 ent))"
by (simp only: HI1 HI2)
also have "… = valor_if (IF e e1 e2) ent"
by (simp only: valor_if.simps(3))
finally show ?thesis
by this
qed
qed

subsubsection ‹Demostración aplicativa detallada del teorema valor_if_normal›

lemma valor_if_normal_aplicativo:
"valor_if (normal b) ent = valor_if b ent"
apply (induct b)
apply (simp only: normal.simps(1))
apply (simp only: normal.simps(2))
apply (simp only: normal.simps(3))
apply (simp only: valor_if_normalAux_aplicativo)
apply (simp only: valor_if.simps(3))
done

text ‹------------------------------------------------------------------
Ejercicio 9. Demostrar que para toda expresión if e, (normal e) está
en forma normal.
---------------------------------------------------------------------›

subsection ‹Lema auxiliar es_normal_normalAux›

subsubsection ‹Demostración estructurada de es_normal_normalAux›
lemma es_normal_normalAux_E:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
proof (induct e arbitrary: e1 e2)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF e1 e2 e3)
then show ?case by simp
qed

subsubsection ‹Demostración automática de es_normal_normalAux›
lemma es_normal_normalAux_A:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
by (induct e arbitrary: e1 e2) simp_all

subsubsection ‹Demostración declarativa detallada de es_normal_normalAux›
lemma es_normal_normalAux:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
proof (induct e arbitrary: e1 e2)
fix b e1 e2
have "es_normal (normalAux (CIF b) e1 e2) =
es_normal (IF (CIF b) e1 e2)"
by (simp only: normalAux.simps(1))
also have "… = (es_normal e1 ∧ es_normal e2)"
by (simp only: es_normal.simps(3))
finally show "es_normal (normalAux (CIF b) e1 e2) =
(es_normal e1 ∧ es_normal e2)"
by this
next
fix n e1 e2
have "es_normal (normalAux (VIF n) e1 e2) =
es_normal (IF (VIF n) e1 e2)"
by (simp only: normalAux.simps(2))
also have "… = (es_normal e1 ∧ es_normal e2)"
by (simp only: es_normal.simps(4))
finally show "es_normal (normalAux (VIF n) e1 e2) =
(es_normal e1 ∧ es_normal e2)"
by this
next
fix a a1 a2 e1 e2
assume
HI: "⋀e1 e2. es_normal (normalAux a e1 e2) =
(es_normal e1 ∧ es_normal e2)" and
HI1: "⋀e1 e2. es_normal (normalAux a1 e1 e2) =
(es_normal e1 ∧ es_normal e2)" and
HI2: "⋀e1 e2. es_normal (normalAux a2 e1 e2) =
(es_normal e1 ∧ es_normal e2)"
have "es_normal (normalAux (IF a a1 a2) e1 e2) =
es_normal (normalAux a
(normalAux a1 e1 e2)
(normalAux a2 e1 e2))"
by (simp only: normalAux.simps(3))
also have "… = (es_normal (normalAux a1 e1 e2) ∧
es_normal (normalAux a2 e1 e2))"
by (simp only: HI)
also have "… = ((es_normal e1 ∧ es_normal e2) ∧
(es_normal e1 ∧ es_normal e2))"
by (simp only: HI1 HI2)
also have "… = (es_normal e1 ∧ es_normal e2)"
by (simp only: conj_absorb)
finally show "es_normal (normalAux (IF a a1 a2) e1 e2) =
(es_normal e1 ∧ es_normal e2)"
by this
qed

subsubsection ‹Demostración aplicativa detallada de es_normal_normalAux›
lemma es_normal_normalAux_aplicativa:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
apply(induct e arbitrary: e1 e2)
apply(simp only: normalAux.simps
es_normal.simps)+
apply(rule iffI)
apply(erule conjunct2)
apply(rule conjI)
apply assumption+
done

subsection ‹Demostraciones del teorema es_normal_normal›

subsubsection ‹Demostración estructurada del teorema es_normal_normal›
theorem es_normal_normal_E:
"es_normal (normal b)"
proof (induct b)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF b1 b2 b3)
then show ?case by (simp add: es_normal_normalAux)
qed

subsubsection ‹Demostración automática del teorema es_normal_normal›
theorem es_normal_normal_A:
"es_normal (normal b)"
by (induct b) (simp_all add: es_normal_normalAux)

subsubsection ‹Demostración declarativa detallada del teorema
es_normal_normal›
theorem es_normal_normal:
"es_normal (normal b)"
proof (induct b)
fix b
show "es_normal (normal (CIF b))"
by (simp only: normal.simps(1) es_normal.simps(1))
next
fix n
show "es_normal (normal (VIF n))"
by (simp only: normal.simps(2) es_normal.simps(2))
next
fix e e1 e2
assume "es_normal (normal e)"
"es_normal (normal e1)"
"es_normal (normal e2)"
then show "es_normal (normal (IF e e1 e2))"
by (simp only: normal.simps(3) es_normal_normalAux)
qed

subsubsection ‹Demostración aplicativa detallada del teorema
es_normal_normal›
lemma es_normal_normal_aplicativa:
"es_normal (normal b)"
apply(induct b)
apply(simp only: normal.simps(1))
apply(simp only: es_normal.simps(1))
apply(simp only: normal.simps(2))
apply(simp only: es_normal.simps(2))
apply(simp only: normal.simps)
apply(simp only: es_normal_normalAux_aplicativa)
done

section ‹Definición de bool2ifN›

text ‹------------------------------------------------------------------
Ejercicio 10. Definir la función
bool2ifN :: exp_booleana ⇒ exp_if
tal que (bool2ifN e) es una expresión if en forma normal equivalente a
la expresión Booleana e.
---------------------------------------------------------------------›

definition bool2ifN :: "exp_booleana ⇒ exp_if" where
"bool2ifN e ≡ normal (bool2if e)"

section ‹Lema es_normal_bool2ifN›

text ‹------------------------------------------------------------------
Ejercicio 11. Demostrar que para toda expresión booleana e,
(bool2ifN e) está en forma normal.
---------------------------------------------------------------------›

subsection ‹Demostración automática de es_normal_bool2ifN›
theorem es_normal_bool2ifN_A:
"es_normal (bool2ifN e)"
by (simp only:bool2ifN_def es_normal_normal)

subsection ‹Demostración declarativa detallada de es_normal_bool2ifN›

lemma es_normal_bool2ifN:
"es_normal (bool2ifN e)"
proof-
have "bool2ifN e = normal (bool2if e)" by (simp only:bool2ifN_def)
then show "es_normal (bool2ifN e)" by
(simp only:es_normal_normal)
qed

subsection ‹Demostración aplicativa detallada de es_normal_bool2ifN›

lemma es_normal_bool2ifN_aplicativa:
"es_normal (bool2ifN e)"
apply (simp only:bool2ifN_def)
apply (simp only:es_normal_normal)
done

section ‹Lema valor_if_bool2ifN›

text ‹------------------------------------------------------------------
Ejercicio 12. Demostrar que para toda expresión booleana e,
(bool2ifN e) es equivalente a e.
---------------------------------------------------------------------›

subsection ‹Demostración automática de valor_if_bool2ifN›
theorem valor_if_bool2ifN_A:
"valor_if (bool2ifN e) ent = valor e ent"
by (simp only: bool2ifN_def valor_if_bool2if valor_if_normal)

subsection ‹Demostración declarativa detallada de valor_if_bool2ifN›

lemma valor_if_bool2ifN:
"valor_if (bool2ifN e) ent = valor e ent"
proof-
have "bool2ifN e ≡ normal (bool2if e)" by (simp only:bool2ifN_def)
then have "valor_if (bool2ifN e) ent =
valor_if (normal (bool2if e)) ent" by (simp only:)
also have "… = valor_if (bool2if e) ent"
by (simp only: valor_if_normal)
also have "… = valor e ent" by (simp only:valor_if_bool2if)
finally show "valor_if (bool2ifN e) ent = valor e ent" by this
qed

subsection ‹Demostración aplicativa detallada de valor_if_bool2ifN›

lemma valor_if_bool2ifN_aplicativa:
"valor_if (bool2ifN e) ent = valor e ent"
apply (simp only:bool2ifN_def)
apply (simp only: valor_if_normal)
apply (simp only:valor_if_bool2if)
done

end

</source>

TF sol

2020-06-18T06:53:06Z

Mjoseh: Página creada con «<source lang = "isabelle"> chapter ‹Expresiones booleanas y expresiones condicionales› theory Trabajo_final_sol imports Main begin section ‹Expresiones booleanas…»

<source lang = "isabelle">
chapter ‹Expresiones booleanas y expresiones condicionales›

theory Trabajo_final_sol
imports Main
begin

section ‹Expresiones booleanas›

text ‹------------------------------------------------------------------
Ejercicio 1. La expresiones booleanas se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e es una expresión, entonces ¬e también lo es.
* Si e1 y e2 son expresiones, entonces e1 ∧ e2 también lo es.

Definir exp_booleana como el tipo de las expresiones booleanas.
---------------------------------------------------------------------›

datatype exp_booleana = Const bool
| Var nat
| Neg exp_booleana
| And exp_booleana exp_booleana

section ‹El valor de las expresiones boolenas›

text ‹------------------------------------------------------------------
Ejercicio 2. Una interpretación es una función i que asigna a cada
número natural un booleano de forma que el valor de la variable
'Var n' en la interpretación 'i' es 'i(n)'.

Definir la función
valor :: exp_booleana ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor e i) es el valor de la expresión booleana e en la
interpretación i. Por ejemplo,
value "(valor (Var 3) (λx. False))
es False
---------------------------------------------------------------------›

fun valor :: "exp_booleana ⇒ (nat ⇒ bool) ⇒ bool" where
"valor (Const b) _ = b"
| "valor (Var n) i = i n "
| "valor (Neg e) i = (¬ (valor e i))"
| "valor (And e1 e2) i = (valor e1 i ∧ valor e2 i)"

section ‹Expresiones If›

text ‹------------------------------------------------------------------
Ejercicio 3. La expresiones if se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e, e1 y e2 son expresiones, entonces (if e e1 e2) también lo es.

Definir exp_if como el tipo de las expresiones if.
---------------------------------------------------------------------›

datatype exp_if = CIF bool
| VIF nat
| IF exp_if exp_if exp_if

text ‹------------------------------------------------------------------
Ejercicio 4. Definir la función
valor_if :: exp_if ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor_if e i) es el valor de la expresión if e en la
interpretación i.
---------------------------------------------------------------------›

fun valor_if :: "exp_if ⇒ (nat ⇒ bool) ⇒ bool" where
"valor_if (CIF b) _ = b"
| "valor_if (VIF n) i = i n"
| "valor_if (IF e e1 e2) i = (if (valor_if e i)
then (valor_if e1 i)
else (valor_if e2 i))"

section ‹Transformación de expresiones booleanas en expresiones if›

subsection ‹Definición de bool2if›

text ‹------------------------------------------------------------------
Ejercicio 5. Definir la función
bool2if :: exp_booleana ⇒ exp_if
tal que (bool2if e) es una expresión if equivalente a la expresión
booleana e.
---------------------------------------------------------------------›

fun bool2if :: "exp_booleana ⇒ exp_if" where
"bool2if (Const b) = CIF b"
| "bool2if (Var n) = VIF n"
| "bool2if (Neg e) = IF (bool2if e) (CIF False) (CIF True)"
| "bool2if (And e1 e2) = IF (bool2if e1) (bool2if e2) (CIF False)"

text ‹------------------------------------------------------------------
Ejercicio 6. Demostrar que para cualquier expresión boolena e, son
equivalentes (bool2if e) y e.
---------------------------------------------------------------------›

subsection ‹Demostraciones de valor_if_bool2if›

subsubsection ‹Demostración estructurada de valor_if_bool2if›
lemma valor_if_bool2if_E:
"valor_if (bool2if e) ent = valor e ent"
proof (induct e)
case (Const x)
then show ?case by simp
next
case (Var x)
then show ?case by simp
next
case (Neg e)
then show ?case by simp
next
case (And e1 e2)
then show ?case by simp
qed

subsubsection ‹Demostración automática de valor_if_bool2if›
lemma valor_if_bool2if_A:
"valor_if (bool2if e) ent = valor e ent"
by (induct e) simp_all

subsubsection ‹Demostración declarativa detallada de valor_if_bool2if›
lemma valor_if_bool2if:
"valor_if (bool2if e) ent = valor e ent"
proof (induct e)
fix b
have "valor_if (bool2if (Const b)) ent = valor_if (CIF b) ent"
by (simp only: bool2if.simps(1))
also have "… = b"
by (simp only: valor_if.simps(1))
also have "… = valor (Const b) ent"
by (simp only: valor.simps(1))
finally show "valor_if (bool2if (Const b)) ent = valor (Const b) ent"
by this
next
fix n
have "valor_if (bool2if (Var n)) ent = valor_if (VIF n) ent"
by (simp only: bool2if.simps(2))
also have "… = ent n"
by (simp only: valor_if.simps(2))
also have "… = valor (Var n) ent"
by (simp only: valor.simps(2))
finally show "valor_if (bool2if (Var n)) ent = valor (Var n) ent"
by this
next
fix e
assume HI: "valor_if (bool2if e) ent = valor e ent"
have "valor_if (bool2if (Neg e)) ent =
valor_if (IF (bool2if e) (CIF False) (CIF True)) ent"
by (simp only: bool2if.simps(3))
also have "… = (if valor_if (bool2if e) ent
then valor_if (CIF False) ent
else valor_if (CIF True) ent)"
by (simp only: valor_if.simps(3))
also have "… = (if valor e ent
then False
else True)"
by (simp only: HI valor_if.simps(1))
also have "… = (¬ valor e ent)"
by (rule SMT.z3_rule(52))
also have "… = valor (Neg e) ent"
by (simp only: valor.simps(3))
finally show "valor_if (bool2if (Neg e)) ent = valor (Neg e) ent"
by this
next
fix e1 e2
assume HI1: "valor_if (bool2if e1) ent = valor e1 ent" and
HI2: "valor_if (bool2if e2) ent = valor e2 ent"
have "valor_if (bool2if (And e1 e2)) ent =
valor_if (IF (bool2if e1) (bool2if e2) (CIF False)) ent"
by (simp only: bool2if.simps(4))
also have "… = (if valor_if (bool2if e1) ent
then valor_if (bool2if e2) ent
else valor_if (CIF False) ent)"
by (simp only: valor_if.simps(3))
also have "… = (if valor e1 ent
then valor e2 ent
else False)"
by (simp only: HI1 HI2 valor_if.simps(1))
also have "… = ((valor e1 ent ∧ valor e2 ent) ∨
(¬(valor e1 ent) ∧ False))"
by (rule if_bool_eq_disj)
also have "… = ((valor e1 ent ∧ valor e2 ent) ∨ False)"
by (simp only: simp_thms(23))
also have "… = (valor e1 ent ∧ valor e2 ent)"
by (simp only: simp_thms(31))
also have "… = valor (And e1 e2) ent"
by (simp only: valor.simps(4))
finally show "valor_if (bool2if (And e1 e2)) ent =
valor (And e1 e2) ent"
by this
qed

subsubsection ‹Demostración aplicativa detallada de valor_if_bool2if›
lemma valor_if_bool2if_aplicativa:
"valor_if (bool2if e) ent = valor e ent"
apply(induct e)
apply(simp only: bool2if.simps
valor_if.simps
valor.simps)
apply(simp only: bool2if.simps
valor_if.simps
valor.simps)
apply(simp only: bool2if.simps)
apply(simp only: valor_if.simps)
apply(simp only: valor.simps)
apply(split if_split)
apply(rule conjI)
apply(rule impI)
apply(rule iffI)
apply(rule ccontr, assumption)
apply(erule notE, assumption)
apply(rule impI)
apply(rule iffI, assumption)
apply(simp only: TrueI)
apply(simp only: bool2if.simps)
apply(simp only: valor_if.simps)
apply(simp only: valor.simps)
apply(split if_split)
apply(rule conjI)
apply(rule impI)
apply(rule iffI)
apply(erule conjI, assumption)
apply(erule conjunct2)
apply(rule impI)
apply(rule iffI)
apply (rule FalseE, assumption)
apply(erule notE)
apply(erule conjunct1)
done

section ‹Formas normales›

subsection ‹Definición de es_normal›

text ‹------------------------------------------------------------------
Ejercicio 6. Un expresión if, e, está en forma normal si para cada
subexpresión de e de la forma (if c e1 e2) se tiene que c es una
constante o una variable.

Definir la función
es_normal :: exp_if ⇒ bool
tal que (es_normal e) se verifica si e está en forma normal.
---------------------------------------------------------------------›

fun es_normal :: "exp_if ⇒ bool" where
"es_normal (CIF _) = True"
| "es_normal (VIF _) = True"
| "es_normal (IF (CIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal (IF (VIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal _ = False"

subsection ‹Definición de normal›

text ‹------------------------------------------------------------------
Ejercicio 7. Definir la función
normal :: exp_if ⇒ exp_if
tal que (normal e) es una expresión if en forma normal equivalente a
la expresión e.
--------------------------------------------------------------------- ›

fun normalAux :: "exp_if ⇒ exp_if ⇒ exp_if ⇒ exp_if" where
"normalAux (CIF b) e1 e2 = IF (CIF b) e1 e2"
| "normalAux (VIF n) e1 e2 = IF (VIF n) e1 e2"
| "normalAux (IF a a1 a2) e1 e2 =
normalAux a (normalAux a1 e1 e2) (normalAux a2 e1 e2)"

fun normal :: "exp_if ⇒ exp_if" where
"normal (CIF b) = CIF b"
| "normal (VIF n) = VIF n"
| "normal (IF e e1 e2) = normalAux e (normal e1) (normal e2)"

section ‹Corrección de la normalización›

text ‹------------------------------------------------------------------
Ejercicio 8. Demostrar que la forma normal de una expresión if es
equivalente a la expresión; es decir,
valor_if (normal e) i = valor_if e i
---------------------------------------------------------------------›

subsection ‹Lema auxiliar valor_if_normalAux›

subsubsection ‹Demostración estructurada de valor_if_normalAux›
lemma valor_if_normalAux_E:
"valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
proof (induct e arbitrary: e1 e2)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF e1 e2 e3)
then show ?case by simp
qed

subsubsection ‹Demostración automática de valor_if_normalAux›
lemma valor_if_normalAux_A:
"valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
by (induct e arbitrary: e1 e2) simp_all

subsubsection ‹Demostración declarativa detallada de valor_if_normalAux›

lemma if_if:
fixes A and A1 and A2 and C1 and C2 :: bool
shows
"(if A
then (if A1 then C1 else C2)
else (if A2 then C1 else C2)) =
(if (if A then A1 else A2)
then C1
else C2)"
by (cases A; cases A1; cases A2)
(simp_all only: if_True if_False)

lemma valor_if_IF:
"valor_if (IF a (IF a1 c1 c2) (IF a2 c1 c2)) ent =
valor_if (IF (IF a a1 a2) c1 c2) ent"
by (simp only: valor_if.simps(3) if_if)

lemma valor_if_normalAux:
"valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
proof (induct e arbitrary: e1 e2)
fix b e1 e2
show "valor_if (normalAux (CIF b) e1 e2) ent =
valor_if (IF (CIF b) e1 e2) ent"
by (simp only: normalAux.simps(1))
next
fix n e1 e2
show "valor_if (normalAux (VIF n) e1 e2) ent =
valor_if (IF (VIF n) e1 e2) ent"
by (simp only: normalAux.simps(2))
next
fix a a1 a2 c1 c2
assume HI: "⋀e1 e2. valor_if (normalAux a e1 e2) ent =
valor_if (IF a e1 e2) ent" and
HI1: "⋀e1 e2. valor_if (normalAux a1 e1 e2) ent =
valor_if (IF a1 e1 e2) ent" and
HI2: "⋀e1 e2. valor_if (normalAux a2 e1 e2) ent =
valor_if (IF a2 e1 e2) ent"
show "valor_if (normalAux (IF a a1 a2) c1 c2) ent =
valor_if (IF (IF a a1 a2) c1 c2) ent"
proof -
have "valor_if (normalAux (IF a a1 a2) c1 c2) ent =
valor_if (normalAux a
(normalAux a1 c1 c2)
(normalAux a2 c1 c2)) ent"
by (simp only: normalAux.simps(3))
also have "… = valor_if (IF a
(normalAux a1 c1 c2)
(normalAux a2 c1 c2)) ent"
by (simp only: HI)
also have "… = (if valor_if a ent
then valor_if (normalAux a1 c1 c2) ent
else valor_if (normalAux a2 c1 c2) ent)"
by (simp only: valor_if.simps(3))
also have "… = (if valor_if a ent
then valor_if (IF a1 c1 c2) ent
else valor_if (IF a2 c1 c2) ent)"
by (simp only: HI1 HI2)
also have "… = valor_if (IF a (IF a1 c1 c2) (IF a2 c1 c2)) ent"
by (simp only: valor_if.simps(3))
also have "… = valor_if (IF (IF a a1 a2) c1 c2) ent"
by (simp only: valor_if_IF)
finally show ?thesis
by this
qed
qed

subsubsection ‹Demostración aplicativa detallada de valor_if_normalAux›
lemma valor_if_normalAux_aplicativo:
"∀e1 e2. valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
apply (induct e)
apply (rule allI)+
apply (simp only: normalAux.simps(1))
apply (rule allI)+
apply (simp only: normalAux.simps(2))
apply (rule allI)+
apply (simp only: normalAux.simps(3))
apply (simp only: valor_if.simps(3))
apply (case_tac "valor_if e1 ent")
apply (simp only: if_True)
apply (simp only: if_False)
done

subsection ‹Demostraciones del teorema valor_if_normal›

subsubsection ‹Demostración estructurada del teorema valor_if_normal›
theorem valor_if_normal_E:
"valor_if (normal b) ent = valor_if b ent"
proof (induct b)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF b1 b2 b3)
then show ?case by (simp add: valor_if_normalAux)
qed

subsubsection ‹Demostración automática del teorema valor_if_normal›
theorem valor_if_normal_A:
"valor_if (normal b) ent = valor_if b ent"
by (induct b) (simp_all add: valor_if_normalAux)

subsubsection ‹Demostración declarativa detallada del teorema valor_if_normal›
theorem valor_if_normal:
"valor_if (normal b) ent = valor_if b ent"
proof (induct b)
fix b
show "valor_if (normal (CIF b)) ent = valor_if (CIF b) ent"
by (simp only: normal.simps(1) valor_if.simps(1))
next
fix n
show "valor_if (normal (VIF n)) ent = valor_if (VIF n) ent"
by (simp only: normal.simps(2) valor_if.simps(2))
next
fix e e1 e2
assume HI: "valor_if (normal e) ent = valor_if e ent" and
HI1: "valor_if (normal e1) ent = valor_if e1 ent" and
HI2: "valor_if (normal e2) ent = valor_if e2 ent"
show "valor_if (normal (IF e e1 e2)) ent =
valor_if (IF e e1 e2) ent"
proof -
have "valor_if (normal (IF e e1 e2)) ent =
valor_if (normalAux e (normal e1) (normal e2)) ent"
by (simp only: normal.simps(3))
also have "… = valor_if (IF e (normal e1) (normal e2)) ent"
by (simp only: valor_if_normalAux)
also have "… = (if (valor_if e ent)
then (valor_if (normal e1) ent)
else (valor_if (normal e2) ent))"
by (simp only: valor_if.simps(3))
also have "… = (if (valor_if e ent)
then (valor_if e1 ent)
else (valor_if e2 ent))"
by (simp only: HI1 HI2)
also have "… = valor_if (IF e e1 e2) ent"
by (simp only: valor_if.simps(3))
finally show ?thesis
by this
qed
qed

subsubsection ‹Demostración aplicativa detallada del teorema valor_if_normal›

lemma valor_if_normal_aplicativo:
"valor_if (normal b) ent = valor_if b ent"
apply (induct b)
apply (simp only: normal.simps(1))
apply (simp only: normal.simps(2))
apply (simp only: normal.simps(3))
apply (simp only: valor_if_normalAux_aplicativo)
apply (simp only: valor_if.simps(3))
done

text ‹------------------------------------------------------------------
Ejercicio 9. Demostrar que para toda expresión if e, (normal e) está
en forma normal.
---------------------------------------------------------------------›

subsection ‹Lema auxiliar es_normal_normalAux›

subsubsection ‹Demostración estructurada de es_normal_normalAux›
lemma es_normal_normalAux_E:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
proof (induct e arbitrary: e1 e2)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF e1 e2 e3)
then show ?case by simp
qed

subsubsection ‹Demostración automática de es_normal_normalAux›
lemma es_normal_normalAux_A:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
by (induct e arbitrary: e1 e2) simp_all

subsubsection ‹Demostración declarativa detallada de es_normal_normalAux›
lemma es_normal_normalAux:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
proof (induct e arbitrary: e1 e2)
fix b e1 e2
have "es_normal (normalAux (CIF b) e1 e2) =
es_normal (IF (CIF b) e1 e2)"
by (simp only: normalAux.simps(1))
also have "… = (es_normal e1 ∧ es_normal e2)"
by (simp only: es_normal.simps(3))
finally show "es_normal (normalAux (CIF b) e1 e2) =
(es_normal e1 ∧ es_normal e2)"
by this
next
fix n e1 e2
have "es_normal (normalAux (VIF n) e1 e2) =
es_normal (IF (VIF n) e1 e2)"
by (simp only: normalAux.simps(2))
also have "… = (es_normal e1 ∧ es_normal e2)"
by (simp only: es_normal.simps(4))
finally show "es_normal (normalAux (VIF n) e1 e2) =
(es_normal e1 ∧ es_normal e2)"
by this
next
fix a a1 a2 e1 e2
assume
HI: "⋀e1 e2. es_normal (normalAux a e1 e2) =
(es_normal e1 ∧ es_normal e2)" and
HI1: "⋀e1 e2. es_normal (normalAux a1 e1 e2) =
(es_normal e1 ∧ es_normal e2)" and
HI2: "⋀e1 e2. es_normal (normalAux a2 e1 e2) =
(es_normal e1 ∧ es_normal e2)"
have "es_normal (normalAux (IF a a1 a2) e1 e2) =
es_normal (normalAux a
(normalAux a1 e1 e2)
(normalAux a2 e1 e2))"
by (simp only: normalAux.simps(3))
also have "… = (es_normal (normalAux a1 e1 e2) ∧
es_normal (normalAux a2 e1 e2))"
by (simp only: HI)
also have "… = ((es_normal e1 ∧ es_normal e2) ∧
(es_normal e1 ∧ es_normal e2))"
by (simp only: HI1 HI2)
also have "… = (es_normal e1 ∧ es_normal e2)"
by (simp only: conj_absorb)
finally show "es_normal (normalAux (IF a a1 a2) e1 e2) =
(es_normal e1 ∧ es_normal e2)"
by this
qed

subsubsection ‹Demostración aplicativa detallada de es_normal_normalAux›
lemma es_normal_normalAux_aplicativa:
"es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
apply(induct e arbitrary: e1 e2)
apply(simp only: normalAux.simps
es_normal.simps)+
apply(rule iffI)
apply(erule conjunct2)
apply(rule conjI)
apply assumption+
done

subsection ‹Demostraciones del teorema es_normal_normal›

subsubsection ‹Demostración estructurada del teorema es_normal_normal›
theorem es_normal_normal_E:
"es_normal (normal b)"
proof (induct b)
case (CIF x)
then show ?case by simp
next
case (VIF x)
then show ?case by simp
next
case (IF b1 b2 b3)
then show ?case by (simp add: es_normal_normalAux)
qed

subsubsection ‹Demostración automática del teorema es_normal_normal›
theorem es_normal_normal_A:
"es_normal (normal b)"
by (induct b) (simp_all add: es_normal_normalAux)

subsubsection ‹Demostración declarativa detallada del teorema
es_normal_normal›
theorem es_normal_normal:
"es_normal (normal b)"
proof (induct b)
fix b
show "es_normal (normal (CIF b))"
by (simp only: normal.simps(1) es_normal.simps(1))
next
fix n
show "es_normal (normal (VIF n))"
by (simp only: normal.simps(2) es_normal.simps(2))
next
fix e e1 e2
assume "es_normal (normal e)"
"es_normal (normal e1)"
"es_normal (normal e2)"
then show "es_normal (normal (IF e e1 e2))"
by (simp only: normal.simps(3) es_normal_normalAux)
qed

subsubsection ‹Demostración aplicativa detallada del teorema
es_normal_normal›
lemma es_normal_normal_aplicativa:
"es_normal (normal b)"
apply(induct b)
apply(simp only: normal.simps(1))
apply(simp only: es_normal.simps(1))
apply(simp only: normal.simps(2))
apply(simp only: es_normal.simps(2))
apply(simp only: normal.simps)
apply(simp only: es_normal_normalAux_aplicativa)
done

section ‹Definición de bool2ifN›

text ‹------------------------------------------------------------------
Ejercicio 10. Definir la función
bool2ifN :: exp_booleana ⇒ exp_if
tal que (bool2ifN e) es una expresión if en forma normal equivalente a
la expresión Booleana e.
---------------------------------------------------------------------›

definition bool2ifN :: "exp_booleana ⇒ exp_if" where
"bool2ifN e ≡ normal (bool2if e)"

section ‹Lema es_normal_bool2ifN›

text ‹------------------------------------------------------------------
Ejercicio 11. Demostrar que para toda expresión booleana e,
(bool2ifN e) está en forma normal.
---------------------------------------------------------------------›

subsection ‹Demostración automática de es_normal_bool2ifN›
theorem es_normal_bool2ifN_A:
"es_normal (bool2ifN e)"
by (simp only:bool2ifN_def es_normal_normal)

subsection ‹Demostración declarativa detallada de es_normal_bool2ifN›

lemma es_normal_bool2ifN:
"es_normal (bool2ifN e)"
proof-
have "bool2ifN e = normal (bool2if e)" by (simp only:bool2ifN_def)
then show "es_normal (bool2ifN e)" by
(simp only:es_normal_normal)
qed

subsection ‹Demostración aplicativa detallada de es_normal_bool2ifN›

lemma es_normal_bool2ifN_aplicativa:
"es_normal (bool2ifN e)"
apply (simp only:bool2ifN_def)
apply (simp only:es_normal_normal)
done

section ‹Lema valor_if_bool2ifN›

text ‹------------------------------------------------------------------
Ejercicio 12. Demostrar que para toda expresión booleana e,
(bool2ifN e) es equivalente a e.
---------------------------------------------------------------------›

subsection ‹Demostración automática de valor_if_bool2ifN›
theorem valor_if_bool2ifN_A:
"valor_if (bool2ifN e) ent = valor e ent"
by (simp only: bool2ifN_def valor_if_bool2if valor_if_normal)

subsection ‹Demostración declarativa detallada de valor_if_bool2ifN›

lemma valor_if_bool2ifN:
"valor_if (bool2ifN e) ent = valor e ent"
proof-
have "bool2ifN e ≡ normal (bool2if e)" by (simp only:bool2ifN_def)
then have "valor_if (bool2ifN e) ent =
valor_if (normal (bool2if e)) ent" by (simp only:)
also have "… = valor_if (bool2if e) ent"
by (simp only: valor_if_normal)
also have "… = valor e ent" by (simp only:valor_if_bool2if)
finally show "valor_if (bool2ifN e) ent = valor e ent" by this
qed

subsection ‹Demostración aplicativa detallada de valor_if_bool2ifN›

lemma valor_if_bool2ifN_aplicativa:
"valor_if (bool2ifN e) ent = valor e ent"
apply (simp only:bool2ifN_def)
apply (simp only: valor_if_normal)
apply (simp only:valor_if_bool2if)
done

end

</source>

TF

2020-06-18T06:52:23Z

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

<source lang = "isabelle">
chapter ‹Expresiones booleanas y expresiones condicionales›

theory Trabajo_final
imports Main
begin

text ‹El objetivo del trabajo es demostrar las propiedades de los 5
ejercicios de la forma más detallada posible.›

text ‹------------------------------------------------------------------
Definición. La expresiones booleanas se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e es una expresión, entonces ¬e también lo es.
* Si e1 y e2 son expresiones, entonces e1 ∧ e2 también lo es.

Definir exp_booleana como el tipo de las expresiones booleanas.
---------------------------------------------------------------------›

datatype exp_booleana = Const bool
| Var nat
| Neg exp_booleana
| And exp_booleana exp_booleana

text ‹------------------------------------------------------------------
Definición. Una interpretación es una función i que asigna a cada
número natural un booleano de forma que el vlor de la variable
'Var n' en la interpretación 'i' es 'i(n)'.

Definir la función
valor :: exp_booleana ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor e i) es el valor de la expresión booleana e en la
interpretación i. Por ejemplo,
value "(valor (Var 3) (λx. False))
es False
---------------------------------------------------------------------›

fun valor :: "exp_booleana ⇒ (nat ⇒ bool) ⇒ bool" where
"valor (Const b) _ = b"
| "valor (Var n) i = i n "
| "valor (Neg e) i = (¬ (valor e i))"
| "valor (And e1 e2) i = (valor e1 i ∧ valor e2 i)"

text ‹------------------------------------------------------------------
Definición. La expresiones if se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e, e1 y e2 son expresiones, entonces (if e e1 e2) también lo es.

Definir exp_if como el tipo de las expresiones if.
---------------------------------------------------------------------›

datatype exp_if = CIF bool
| VIF nat
| IF exp_if exp_if exp_if

text ‹------------------------------------------------------------------
Definición. Definir la función
valor_if :: exp_if ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor_if e i) es el valor de la expresión if e en la
interpretación i.
---------------------------------------------------------------------›

fun valor_if :: "exp_if ⇒ (nat ⇒ bool) ⇒ bool" where
"valor_if (CIF b) _ = b"
| "valor_if (VIF n) i = i n"
| "valor_if (IF e e1 e2) i = (if (valor_if e i)
then (valor_if e1 i)
else (valor_if e2 i))"

text ‹------------------------------------------------------------------
Definición. Definir la función
bool2if :: exp_booleana ⇒ exp_if
tal que (bool2if e) es una expresión if equivalente a la expresión
booleana e.
---------------------------------------------------------------------›

fun bool2if :: "exp_booleana ⇒ exp_if" where
"bool2if (Const b) = CIF b"
| "bool2if (Var n) = VIF n"
| "bool2if (Neg e) = IF (bool2if e) (CIF False) (CIF True)"
| "bool2if (And e1 e2) = IF (bool2if e1) (bool2if e2) (CIF False)"

text ‹------------------------------------------------------------------
Ejercicio 1. Demostrar que para cualquier expresión boolena e, son
equivalentes (bool2if e) y e.
---------------------------------------------------------------------›

lemma valor_if_bool2if:
"valor_if (bool2if e) ent = valor e ent"
oops

text ‹------------------------------------------------------------------
Definición. Un expresión if, e, está en forma normal si para cada
subexpresión de e de la forma (if c e1 e2) se tiene que c es una
constante o una variable.

Definir la función
es_normal :: exp_if ⇒ bool
tal que (es_normal e) se verifica si e está en forma normal.
---------------------------------------------------------------------›

fun es_normal :: "exp_if ⇒ bool" where
"es_normal (CIF _) = True"
| "es_normal (VIF _) = True"
| "es_normal (IF (CIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal (IF (VIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal _ = False"

text ‹------------------------------------------------------------------
Definición. Definir la función
normal :: exp_if ⇒ exp_if
tal que (normal e) es una expresión if en forma normal equivalente a
la expresión e.
--------------------------------------------------------------------- ›

fun normalAux :: "exp_if ⇒ exp_if ⇒ exp_if ⇒ exp_if" where
"normalAux (CIF b) e1 e2 = IF (CIF b) e1 e2"
| "normalAux (VIF n) e1 e2 = IF (VIF n) e1 e2"
| "normalAux (IF a a1 a2) e1 e2 =
normalAux a (normalAux a1 e1 e2) (normalAux a2 e1 e2)"

fun normal :: "exp_if ⇒ exp_if" where
"normal (CIF b) = CIF b"
| "normal (VIF n) = VIF n"
| "normal (IF e e1 e2) = normalAux e (normal e1) (normal e2)"

text ‹------------------------------------------------------------------
Ejercicio 2. Demostrar que la forma normal de una expresión if es
equivalente a la expresión; es decir,
valor_if (normal e) i = valor_if e i
---------------------------------------------------------------------›

lemma valor_if_normal:
"valor_if (normal b) ent = valor_if b ent"
oops

text ‹------------------------------------------------------------------
Ejercicio 3. Demostrar que para toda expresión if e, (normal e) está
en forma normal.
---------------------------------------------------------------------›

lemma es_normal_normal:
"es_normal (normal b)"
oops

text ‹------------------------------------------------------------------
Definición. Definir la función
bool2ifN :: exp_booleana ⇒ exp_if
tal que (bool2ifN e) es una expresión if en forma normal equivalente a
la expresión Booleana e.
---------------------------------------------------------------------›

definition bool2ifN :: "exp_booleana ⇒ exp_if" where
"bool2ifN e ≡ normal (bool2if e)"

text ‹------------------------------------------------------------------
Ejercicio 4. Demostrar que para toda expresión booleana e,
(bool2ifN e) está en forma normal.
---------------------------------------------------------------------›

lemma es_normal_bool2ifN:
"es_normal (bool2ifN e)"
oops

text ‹------------------------------------------------------------------
Ejercicio 5. Demostrar que para toda expresión booleana e,
(bool2ifN e) es equivalente a e.
---------------------------------------------------------------------›

lemma valor_if_bool2ifN:
"valor_if (bool2ifN e) ent = valor e ent"
oops

end

</source>

TF

2020-06-18T06:52:13Z

Mjoseh: Página creada con «<source lang = "isabelle"> chapter ‹Expresiones booleanas y expresiones condicionales› theory Trabajo_final imports Main begin text ‹El objetivo del trabajo es dem…»

Ejercicios

2020-06-18T06:49:01Z

Mjoseh:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]], [[Relación 1 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf Una solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]], [[Relación 2 |Solución colaborativa]], [[Rel 2 |Una solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]], [[Relación 3 |Solución colaborativa]], [[Rel 3 |Una solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]], [[Relación 4 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf Una solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]], [[Relación 5 |Solución colaborativa]], [[Rel 5 |Una solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]], [[Relación 6 |Solución colaborativa]] , [[Rel 6 |Una solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]], [[Relación 8 |Solución colaborativa]]).
** [[Rel 8 (rev 1) | Primera corrección]]
** [[Rel 8 (sol) | Una solución]]
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]], [[Relación 9 |Solución colaborativa]]).
** [[Rel 9 (rev 1) | Primera corrección]]
** [[Rel 9 (sol) | Una solución]]
* '''Ejercicio 1 (24-04-2020)''': ([[T1 |Enunciado]], [[T1 sol |Una solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]], [[Relación 10 |Solución colaborativa]]).
** [[Rel 10 (sol) | Una solución]]
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]], [[Relación 11 |Solución colaborativa]]).
** [[Rel 11 (sol) | Una solución]]
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]], [[Relación 12 |Solución colaborativa]]).
** [[Rel 12 (sol) | Una solución]]
* '''Ejercicio 2 (12-05-2020)''': ([[T2 |Enunciado]], [[T2 sol |Una solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]], [[Relación 13 |Solución colaborativa]]).
** [[Rel 13 (sol) | Una solución]]
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomátización de la Geometría.] ([[R14 |Enunciado]], [[Relación 14 |Solución colaborativa]]).
** [[Rel 14 (sol) | Una solución]]
* '''Ejercicio 3 (19-05-2020)''': ([[T3 |Enunciado]], [[T3 sol |Una solución]]).
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]], [[Relación 15 |Solución colaborativa]]).
* '''Ejercicio 4 (26-05-2020)''': ([[T4 |Enunciado]], [[T4 sol |Una solución]]).
* '''Ejercicio 5 (02-06-2020)''':
** ([[T5-1 |Enunciado (1)]], [[T5-1 sol |Una solución]]).
** ([[T5-2 |Enunciado (2)]], [[T5-2 sol |Una solución]]).
* '''Trabajo final''': ([[TF |Enunciado]], [[TF sol |Una solución]]).

T5-2 sol

2020-06-17T15:38:37Z

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

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

T5-2 sol

2020-06-17T15:38:27Z

Mjoseh: 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 ‹-------…»

T5-2

2020-06-17T15:37:48Z

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

<source lang = "isabelle">
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
</source>

T5-2

2020-06-17T15:37:37Z

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

T5-1 sol

2020-06-17T15:36:57Z

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

<source lang = "isabelle">

theory ej_2_jun_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 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

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

section ‹Demostraciones del lema auxiliar nHojasAux›

subsection ‹Demostración estructurada de nHojasAux›

lemma nHojasAuxE:
"nHojasAaux a n = nHojas a + n"
proof (induct a arbitrary: n)
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 nHojasAux›

lemma nHojasAuxA:
"nHojasAaux a n = nHojas a + n"
by (induct a arbitrary: n) simp_all

subsection ‹Demostración declarativa detallada de nHojasAux›

lemma nHojasAux:
"nHojasAaux a n = (nHojas a) + n"
proof (induct a arbitrary: n)
fix n
have "nHojasAaux H n = n + 1"
by (simp only: nHojasAaux.simps(1))
also have "… = nHojas H + n"
by (simp only:nHojas.simps(1))
finally show "nHojasAaux H n = nHojas H + n"
by this
next
fix x :: 'a and i d :: "'a arbol" and n :: nat
assume HI1: "⋀n. nHojasAaux i n = nHojas i + n"
and HI2: "⋀n. nHojasAaux d n = nHojas d + n"
have "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)"
by (simp only: nHojasAaux.simps(2))
also have "… = nHojasAaux i (nHojas d + n)"
by (simp only: HI2)
also have "… = nHojas i + (nHojas d + n)"
by (simp only: HI1)
also have "… = (nHojas i + nHojas d) + n"
by (simp only: add.commute)
also have "… = nHojas (N x i d) + n"
by (simp only: nHojas.simps(2))
finally show "nHojasAaux (N x i d) n = nHojas (N x i d) + n"
by this
qed

section ‹Demostraciones del teorema nHojasA›

subsection ‹Demostración automática de nHojasA›

theorem nHojasA_A:
"nHojasA a = nHojas a"
by (simp add: nHojasA_def nHojasAux)

subsection "Demostración declarativa detallada de nHojasA"

theorem nHojasA:
"nHojasA a = nHojas a"
proof -
have "nHojasA a = nHojasAaux a 0"
by (simp only: nHojasA_def)
also have "… = nHojas a + 0"
by (simp only: nHojasAux)
also have "... = nHojas a"
by (simp only: add_0_right)
finally show "nHojasA a = nHojas a"
by this
qed

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

section ‹Demostraciones de inverso_d›

subsection ‹Demostración automática de inverso_d›

lemma inverso_d_A:
"x ⋅ x^ = 𝟭"
by (metis asociativa neutro_i inverso_i)

subsection ‹Demostración declarativa detallada de inverso_d›

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

section ‹Demostraciones de condicion_necesaria›

subsection ‹Demostración automática de condicion_necesaria›

lemma condicion_necesaria_A:
assumes "x = y^ ⋅ z"
shows "z = y ⋅ x"
using assms
by (metis asociativa neutro_i inverso_d)

subsection ‹Demostración declarativa detallada de condicion_necesaria›

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

section ‹Demostraciones de condicion_suficiente›

subsection ‹Demostración automática de condicion_suficiente›

lemma condicion_suficiente_A:
assumes "z = y ⋅ x"
shows "x = y^ ⋅ z"
using assms(1)
by (metis asociativa neutro_i inverso_i)

subsection ‹Demostración declarativa detallada de condicion_suficiente›

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

section ‹Demostraciones del teorema›

section ‹Demostraciones automática del teorema›

theorem condicion_necesaria_y_suficiente_A:
"x = y^ ⋅ z ⟷ z = y ⋅ x"
using condicion_necesaria
condicion_suficiente
by auto

section ‹Demostraciones declarativa detallada del teorema›

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

end

end
</source>

T5-1 sol

2020-06-17T15:36:45Z

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

T5-1

2020-06-17T15:36:03Z

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

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

T5-1

2020-06-17T15:35:53Z

Mjoseh: 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:…»

Ejercicios

2020-06-17T15:34:26Z

Mjoseh:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]], [[Relación 1 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf Una solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]], [[Relación 2 |Solución colaborativa]], [[Rel 2 |Una solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]], [[Relación 3 |Solución colaborativa]], [[Rel 3 |Una solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]], [[Relación 4 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf Una solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]], [[Relación 5 |Solución colaborativa]], [[Rel 5 |Una solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]], [[Relación 6 |Solución colaborativa]] , [[Rel 6 |Una solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]], [[Relación 8 |Solución colaborativa]]).
** [[Rel 8 (rev 1) | Primera corrección]]
** [[Rel 8 (sol) | Una solución]]
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]], [[Relación 9 |Solución colaborativa]]).
** [[Rel 9 (rev 1) | Primera corrección]]
** [[Rel 9 (sol) | Una solución]]
* '''Ejercicio 1 (24-04-2020)''': ([[T1 |Enunciado]], [[T1 sol |Una solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]], [[Relación 10 |Solución colaborativa]]).
** [[Rel 10 (sol) | Una solución]]
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]], [[Relación 11 |Solución colaborativa]]).
** [[Rel 11 (sol) | Una solución]]
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]], [[Relación 12 |Solución colaborativa]]).
** [[Rel 12 (sol) | Una solución]]
* '''Ejercicio 2 (12-05-2020)''': ([[T2 |Enunciado]], [[T2 sol |Una solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]], [[Relación 13 |Solución colaborativa]]).
** [[Rel 13 (sol) | Una solución]]
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomátización de la Geometría.] ([[R14 |Enunciado]], [[Relación 14 |Solución colaborativa]]).
** [[Rel 14 (sol) | Una solución]]
* '''Ejercicio 3 (19-05-2020)''': ([[T3 |Enunciado]], [[T3 sol |Una solución]]).
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]], [[Relación 15 |Solución colaborativa]]).
* '''Ejercicio 4 (26-05-2020)''': ([[T4 |Enunciado]], [[T4 sol |Una solución]]).
* '''Ejercicio 5 (02-06-2020)''':
** ([[T5-1 |Enunciado (1)]], [[T5-1 sol |Una solución]]).
** ([[T5-2 |Enunciado (2)]], [[T5-2 sol |Una solución]]).

T4 sol

2020-06-01T10:33:40Z

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

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

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

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

text ‹-----------------------------------------------------------------
Se define 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]
---------------------------------------------------------------------›

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

text ‹------------------------------------------------------------------
Ejercicio. Demostrar que
length (elimina n xs) ≤ length xs - n
---------------------------------------------------------------------›

― ‹Por inducción en n y xs según el esquema elimina.induct›

― ‹Estructurada›
lemma "length (elimina n xs) ≤ length xs"
proof(induct n xs rule :elimina.induct)
show "⋀n. length (elimina n []) ≤ length []" by simp
next
show "⋀v va. length (elimina 0 (v # va)) ≤ length (v # va)"
by simp
next
show "⋀n x xs.
length (elimina n xs) ≤ length xs ⟹
length (elimina (Suc n) (x # xs)) ≤ length (x # xs)"
by simp
qed

― ‹Automática›
lemma "length (elimina n xs) ≤ length xs"
by (induct n xs rule :elimina.induct) simp_all

― ‹Declarativa detallada›

lemma "length (elimina n xs) ≤ length xs"
proof(induct n xs rule :elimina.induct)
fix n ::"nat"
show "length (elimina n []) ≤ length []"
by (simp only: elimina.simps(1) list.size(3))
next
fix x::"'a" and xs::"'a list"
show "length (elimina 0 (x # xs)) ≤ length (x #xs)"
by (simp only: elimina.simps(2) list.size(2))
next
fix n ::"nat" and x::"'a" and xs::"'a list"
assume H:"length (elimina n xs) ≤ length xs"
have "length(elimina (Suc n) (x#xs)) = length(elimina n xs)"
by (simp only: elimina.simps(3))
also have "… ≤ length xs"
using H by (simp only:)
also have "… ≤ length (x#xs)"
by (simp only: list.size(4))
finally show "length(elimina (Suc n) (x#xs)) ≤ length (x#xs)".
qed

― ‹Aplicativa detallada›

lemma "length (elimina n xs) ≤ length xs"
apply (induct n xs rule :elimina.induct)
apply (simp only: elimina.simps(1))
apply (simp only: elimina.simps(2))
apply (simp only: elimina.simps(3))
apply (simp only: list.size)
done

― ‹Por inducción en n con xs arbitrario›

― ‹Auxiliar›
lemma elimina0: "elimina 0 xs = xs"
apply (cases xs)
apply (simp only: elimina.simps(1))
apply (simp only: elimina.simps(2))
done

― ‹Estructurada›
lemma "length (elimina n xs) ≤ length xs - n"
proof (induct n arbitrary: xs)
show "⋀xs. length (elimina 0 xs) ≤ length xs - 0"
by (simp only: elimina0)
next
fix n :: nat and xs :: "'a list"
assume HI: "⋀xs:: 'a list. length (elimina n xs) ≤ length xs - n"
show "length (elimina (Suc n) xs) ≤ length xs - (Suc n)"
proof (cases xs)
case Nil
then show ?thesis by simp
next
case (Cons a list)
then show ?thesis using HI by simp
qed
qed

― ‹Declarativa detallada›
lemma "length (elimina n xs) ≤ length xs - n"
proof (induct n arbitrary: xs)
fix xs :: "'a list"
show "length (elimina 0 xs) ≤ length xs - 0"
by (simp only: elimina0 list.size(3))
next
fix n :: nat and xs :: "'a list"
assume HI: "⋀xs:: 'a list. length (elimina n xs) ≤ length xs - n"
show "length (elimina (Suc n) xs) ≤ length xs - (Suc n)"
proof (cases xs)
assume "xs = []"
then have "elimina (Suc n) xs = elimina (Suc n) []"
by (rule arg_cong)
also have "… = []"
by (simp only: elimina.simps(1))
finally have "elimina (Suc n) xs = []"
by this
then have "length (elimina (Suc n) xs) = 0"
by (simp only: list.size(3))
then show "length (elimina (Suc n) xs) ≤ length xs - (Suc n)"
by (simp only: list.size(3))
next
fix y:: "'a" and ys :: "'a list"
assume 1: "xs = y # ys"
have 2: "length (elimina n ys) ≤ length ys - n"
using HI by this
have "length (elimina (Suc n) xs) = length (elimina (Suc n) (y#ys))"
using 1 by (rule arg_cong)
also have "… = length (elimina n ys)"
by (simp only: elimina.simps(3))
also have "… ≤ length ys - n"
using 2 by (simp only:)
also have "… = 1 + length ys - (Suc n)"
by (simp only: diff_Suc_Suc)
also have "… = length (y#ys) - (Suc n)"
by (simp only: list.size(4))
also have "… = length xs - (Suc n)"
using 1 by (simp only: list.size(4))
finally show "length (elimina (Suc n) xs) ≤ length xs - (Suc n)"
by this
qed
qed

― ‹Aplicativa detallada›

lemma "length (elimina n xs) ≤ length xs - n"
apply (induct n arbitrary: xs)
apply (simp only: elimina0)
apply (case_tac xs)
apply (simp only: elimina.simps)
apply (simp only: list.size(3))
apply (simp only: elimina.simps(3))
apply (simp only: list.size(4))
apply (simp only: add_Suc_right)
apply (simp only: add.right_neutral)
apply (simp only: diff_Suc_Suc)
done

― ‹Demostración por inducción en xs con n arbitrario›

― ‹Estructurada›

lemma "length (elimina n xs) ≤ length xs"
proof (induct xs arbitrary: n)
show "⋀n. length (elimina n []) ≤ length []" by simp
next
fix n::"nat" and x::'a and xs:: "'a list"
assume HI: " ⋀n. length (elimina n xs) ≤ length xs"
show "length (elimina n (x# xs)) ≤ length (x#xs)"
proof(cases n)
case 0
then show ?thesis by simp
next
case (Suc nat)
then show ?thesis using HI
by (metis elimina.simps(3) list.size(4) trans_le_add1)
qed
qed

― ‹Declarativa detallada›

lemma "length (elimina n xs) ≤ length xs"
proof (induct xs arbitrary: n)
fix n::"nat"
show "length (elimina n []) ≤ length []"
by (simp only: elimina.simps(1) list.size)
next
fix n::"nat" and x::'a and xs:: "'a list"
assume HI: " ⋀n. length (elimina n xs) ≤ length xs"
show "length (elimina n (x# xs)) ≤ length (x#xs)"
proof(cases n)
assume "n=0"
then have "(elimina n (x# xs)) =(x#xs)"
by (simp only: elimina.simps(2))
then have "length (elimina n (x# xs)) = length (x#xs)"
by (rule arg_cong)
then show "length (elimina n (x# xs)) ≤ length (x#xs)"
by (simp only: order_refl)
next
fix m:: nat
assume "n=(Suc m)"
then have "length (elimina n (x# xs)) =
length (elimina (Suc m) (x# xs))"
by (rule arg_cong)
also have "… =length (elimina m xs)"
by (simp only: elimina.simps(3))
also have "… ≤ length xs" using HI by (simp only:)
also have "… ≤ 1+length xs " by (simp only: le_add1)
also have "…≤ length (x#xs)" by (simp only: list.size)
finally show "length (elimina n (x# xs))≤length (x#xs)"
by (simp only:)
qed
qed

― ‹Aplicativa detallada›

lemma "length (elimina n xs) ≤ length xs - n"
apply (induct xs arbitrary: n)
apply (simp only: elimina.simps(1) list.size)
apply (case_tac n)
apply (simp only: elimina.simps(2) list.size)
apply (simp only: elimina.simps(3) list.size)
apply (simp only:add_Suc_right)
apply (simp only:add.right_neutral)
apply (simp only: diff_Suc_Suc)
done

text ‹------------------------------------------------------------------
Ejercicio 2. Demostrar que si se verifica
∀x. (P x ⟶ (∃y. Q y))
entonces se verifica
∀x. ∃y. (P x ⟶ Q y)

Nota: Hacer la demostración de forma detallada. Es opcional hacerla
de forma declarativa o aplicativa.
--------------------------------------------------------------------›

― ‹Demostración declarativa detallada›

lemma
fixes P Q :: "'b ⇒ bool"
assumes "∀x. ∃y. (P x ⟶ Q y)"
shows "∀x. (P x ⟶ (∃y. Q y))"
proof (rule allI)
fix x
show "P x ⟶ (∃y. Q y)"
proof (rule impI)
assume "P x"
have " ∃y. (P x ⟶ Q y)"
using assms by (rule allE)
then obtain b where "P x ⟶ Q b"
by (rule exE)
then have "Q b"
using ‹P x› by (rule mp)
then show "∃y. Q y"
by (rule exI)
qed
qed

― ‹Demostración aplicativa detallada›

lemma
"∀x. (P x ⟶ (∃y. Q y)) ⟹ ∀x. ∃y. (P x ⟶ Q y)"
apply(rule allI)
apply(erule_tac x = x in allE)
apply(case_tac "P x")
apply(drule mp, assumption)
apply(erule exE)
apply (rule_tac x = y in exI)
apply(rule impI, assumption)
apply (rule exI)
apply(rule impI)
apply(erule notE, assumption)
done

end
</source>

T4

2020-06-01T10:33:24Z

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

<source lang = "isabelle">
text ‹Ejercicio 4 de Lógica Matemática y Fundamentos (26-mayo-2020)›

theory uvus
imports Main
begin

text ‹
Apellidos:
Nombre:
›

text ‹Sustituye la palabra uvus 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 16:30.›

text ‹Nota 2: El segundo ejercicio se realizará de 16:00 a 17:00,
estando disponible desde la PEV a partir de las 17:00 .›

text ‹Nota 3: 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 4: 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 ‹------------------------------------------------------------------
Se define 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]
---------------------------------------------------------------------›

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

text ‹------------------------------------------------------------------
Ejercicio. Demostrar que
length (elimina n xs) ≤ length xs
---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural

›

― ‹Demostración detallada›

lemma "length (elimina n xs) ≤ length xs"
oops

text ‹------------------------------------------------------------------
Ejercicio 2. Demostrar que si se verifica
∀x. (P x ⟶ (∃y. Q y))
entonces se verifica
∀x. ∃y. (P x ⟶ Q y)

Nota: Hacer la demostración de forma detallada. Es opcional hacerla
de forma declarativa o aplicativa.
--------------------------------------------------------------------›

― ‹Demostración detallada›

lemma
fixes P Q :: "'b ⇒ bool"
assumes "∀x. (P x ⟶ (∃y. Q y))"
shows "∀x. ∃y. (P x ⟶ Q y)"
oops

end
</source>

T4

2020-06-01T10:33:15Z

Mjoseh:

T4 sol

2020-06-01T10:29:44Z

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

T4

2020-06-01T10:28:35Z

Mjoseh:

T4

2020-06-01T10:28:17Z

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

Ejercicios

2020-06-01T10:05:05Z

Mjoseh:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]], [[Relación 1 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf Una solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]], [[Relación 2 |Solución colaborativa]], [[Rel 2 |Una solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]], [[Relación 3 |Solución colaborativa]], [[Rel 3 |Una solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]], [[Relación 4 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf Una solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]], [[Relación 5 |Solución colaborativa]], [[Rel 5 |Una solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]], [[Relación 6 |Solución colaborativa]] , [[Rel 6 |Una solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]], [[Relación 8 |Solución colaborativa]]).
** [[Rel 8 (rev 1) | Primera corrección]]
** [[Rel 8 (sol) | Una solución]]
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]], [[Relación 9 |Solución colaborativa]]).
** [[Rel 9 (rev 1) | Primera corrección]]
** [[Rel 9 (sol) | Una solución]]
* '''Ejercicio 1 (24-04-2020)''': ([[T1 |Enunciado]], [[T1 sol |Una solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]], [[Relación 10 |Solución colaborativa]]).
** [[Rel 10 (sol) | Una solución]]
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]], [[Relación 11 |Solución colaborativa]]).
** [[Rel 11 (sol) | Una solución]]
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]], [[Relación 12 |Solución colaborativa]]).
** [[Rel 12 (sol) | Una solución]]
* '''Ejercicio 2 (12-05-2020)''': ([[T2 |Enunciado]], [[T2 sol |Una solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]], [[Relación 13 |Solución colaborativa]]).
** [[Rel 13 (sol) | Una solución]]
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomátización de la Geometría.] ([[R14 |Enunciado]], [[Relación 14 |Solución colaborativa]]).
** [[Rel 14 (sol) | Una solución]]
* '''Ejercicio 3 (19-05-2020)''': ([[T3 |Enunciado]], [[T3 sol |Una solución]]).
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]], [[Relación 15 |Solución colaborativa]]).
* '''Ejercicio 4 (26-05-2020)''': ([[T4 |Enunciado]], [[T4 sol |Una solución]]).

T3 sol

2020-05-28T09:39:28Z

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

<source lang = "isabelle">

text ‹Ejercicio 3 de Lógica Matemática y Fundamentos (19-mayo-2020)›

theory uvus_3_sol
imports Main
begin

text ‹
Apellidos:
Nombre:
›

text ‹Sustituye la palabra uvus 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 es de 15:30 a 17:00.
A continuación, se dispone de 30 minutos para su entrega en la PEV.›

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 ‹------------------------------------------------------------------
Se define 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]
---------------------------------------------------------------------›

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x # xs) = elimina n xs"

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

text ‹------------------------------------------------------------------
Se define la función
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
---------------------------------------------------------------------›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a # xs) = (a = x ∨ estaEn x xs)"

text ‹------------------------------------------------------------------
Ejercicio 1: Demostrar que
estaEn x (elimina n xs) ⟶ estaEn x xs

+ En lenguaje natural
+ En Isabelle/HOL, de forma detallada. Es opcional hacerlo de forma
declarativa o aplicativa.

Nota: Es recomendable pasar de la demostración en lenguaje natural a la
demostración estructurada. Y, a continuación, detallar los pasos de
simplificación hasta llegar a usar sólo el método (simp only:..).
----------------------------------------------------------------------›

― ‹Demostración declarativa detallada›

lemma
"estaEn x (elimina n xs) ⟶ estaEn x xs"
proof (induct rule: elimina.induct)
fix n
show "estaEn x (elimina n []) ⟶ estaEn x []"
proof (rule impI)
assume "estaEn x (elimina n [])"
then show "estaEn x []"
by (simp only: elimina.simps(1))
qed
next
fix y ys
show "estaEn x (elimina 0 (y # ys)) ⟶ estaEn x (y # ys)"
proof (rule impI)
assume "estaEn x (elimina 0 (y # ys))"
then show "estaEn x (y # ys)"
by (simp only: elimina.simps(2))
qed
next
fix n y ys
assume 1: "estaEn x (elimina n ys) ⟶ estaEn x ys"
show "estaEn x (elimina (Suc n) (y # ys)) ⟶ estaEn x (y # ys)"
proof (rule impI)
assume "estaEn x (elimina (Suc n) (y # ys))"
then have "estaEn x (elimina n ys)"
by (simp only: elimina.simps(3))
with 1 have "estaEn x ys"
by (rule mp)
then have "y = x ∨ estaEn x ys"
by (rule disjI2)
then show "estaEn x (y # ys)"
by (simp only: estaEn.simps(2))
qed
qed

― ‹Demostración aplicativa detallada (1)›
lemma eliminaEsta:
"estaEn x (elimina n xs) ⟹ estaEn x xs"
apply (induct rule: elimina.induct)
apply (simp only: elimina.simps(1))
apply (simp only: elimina.simps(2) estaEn.simps(1))
apply (simp only: elimina.simps(3))
apply (simp only: estaEn.simps(2))
apply (rule disjI2)
apply (simp only: implies_True_equals)
done

lemma
"estaEn x (elimina n xs) ⟶ estaEn x xs"
apply (rule impI)
apply (simp only: eliminaEsta)
done

― ‹Demostración aplicativa detallada (2)›
lemma
"estaEn x (elimina n xs) ⟶ estaEn x xs"
apply (induct rule: elimina.induct)
apply (simp only: elimina.simps(1) estaEn.simps(1))
apply (rule impI, assumption)
apply (simp only: elimina.simps(2) estaEn.simps(1))
apply (rule impI, assumption)
apply (simp only: elimina.simps(3))
apply (simp only: estaEn.simps(2))
apply (rule impI)
apply (rule disjI2)
apply (erule mp, assumption)
done

text ‹------------------------------------------------------------------
Ejercicio 2. Demostrar que si la relación binaria R verifica la
siguiente condición
∃y z. (∀x. ¬R(x, y)) ∨ (∀x. ¬R(x, z)))
entonces no se verifica que
∀y z. ∃x. (R(x,y) ∧ R(x,z)))
--------------------------------------------------------------------›

― ‹Demostración declarativa detallada›
lemma
"(∃y z. ((∀x. ¬R(x, y)) ∨ (∀x. ¬R(x, z))))
⟶ ¬ (∀y z. ∃x. (R(x,y) ∧ R(x,z)))"
proof (rule impI)
assume 0: "∃y z. ((∀x. ¬R(x, y)) ∨ (∀x. ¬R(x, z)))"
show "¬ (∀y z. ∃x. (R(x,y) ∧ R(x,z)))"
proof (rule notI)
assume 1: "∀y. ∀z. ∃x. (R(x,y) ∧ R(x,z))"
obtain b where "∃z. ((∀x. ¬R(x, b)) ∨ (∀x. ¬R(x, z)))"
using 0 by (rule exE)
then obtain c where 2: "((∀x. ¬R(x, b)) ∨ (∀x. ¬R(x, c)))"
by (rule exE)
have "∀z. ∃x. (R(x,b) ∧ R(x,z))"
using 1 by (rule allE)
then have "∃x. (R(x,b) ∧ R(x,c))"
by (rule allE)
then obtain a where 3 :"R(a,b) ∧ R(a,c)"
by (rule exE)
show False
using 2
proof (rule disjE)
assume "∀x. ¬ R (x, b)"
then have "¬R(a,b)"
by (rule allE)
have "R(a,b)"
using 3 by (rule conjunct1)
with `¬R(a,b)` show False
by (rule notE)
next
assume "∀x. ¬ R (x, c)"
then have "¬R(a,c)"
by (rule allE)
have "R(a,c)"
using 3 by (rule conjunct2)
with `¬R(a,c)` show False
by (rule notE)
qed
qed
qed

― ‹Demostración aplicativa detallada›
lemma
"(∃y z. ((∀x. ¬R(x,y)) ∨ (∀x. ¬R(x,z))))
⟶ ¬( ∀y z. ∃x. (R(x,y) ∧ R(x,z)))"
apply (rule impI)
apply (rule notI)
apply (erule exE)+
apply (erule_tac x = y in allE)
apply (erule_tac x = z in allE)
apply (erule disjE)
apply (erule exE)
apply (erule_tac x = x in allE)
apply (erule notE)
apply (erule conjunct1)
apply (erule exE)
apply (erule_tac x = x in allE)
apply (erule notE)
apply (erule conjunct2)
done

end
</source>

T3 sol

2020-05-28T09:39:19Z

Mjoseh: Página creada con «<source lang = "isabelle"> text ‹Ejercicio 3 de Lógica Matemática y Fundamentos (19-mayo-2020)› theory uvus_3_sol imports Main begin text ‹ Apellidos: Nombr…»

T3

2020-05-28T09:38:36Z

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

<source lang = "isabelle">
text ‹Ejercicio 3 de Lógica Matemática y Fundamentos (19-mayo-2020)›

theory uvus_3
imports Main
begin

text ‹
Apellidos:
Nombre:
›

text ‹Sustituye la palabra uvus 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 es de 15:30 a 17:00.
A continuación, se dispone de 30 minutos para su entrega en la PEV.›

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 ‹------------------------------------------------------------------
Se define 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]
---------------------------------------------------------------------›

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x # xs) = elimina n xs"

text ‹------------------------------------------------------------------
Se define la función
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
---------------------------------------------------------------------›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a # xs) = (a = x ∨ estaEn x xs)"

text ‹------------------------------------------------------------------
Ejercicio: Demostrar que
estaEn x (elimina n xs) ⟶ estaEn x xs

+ En lenguaje natural
+ En Isabelle/HOL, de forma detallada. Es opcional hacerlo de forma
declarativa o aplicativa.

Nota: Es recomendable pasar de la demostración en lenguaje natural a la
demostración estructurada. Y, a continuación, detallar los pasos de
simplificación hasta llegar a usar sólo el método (simp only:..).
----------------------------------------------------------------------›

― ‹Demostración en lenguaje natural

›

― ‹Demostración detallada›

lemma
"estaEn x (elimina n xs) ⟶ estaEn x xs"
oops

text ‹------------------------------------------------------------------
Ejercicio 2. Demostrar que si la relación binaria R verifica la
siguiente condición
∃y z. (∀x. ¬R(x, y)) ∨ (∀x. ¬R(x, z)))
entonces no se verifica que
∀y z. ∃x. (R(x,y) ∧ R(x,z)))

Nota: Hacer la demostración de forma detallada. Es opcional hacerla
de forma declarativa o aplicativa.
--------------------------------------------------------------------›

― ‹Demostración detallada›
lemma
"(∃y z. ((∀x. ¬R(x, y)) ∨ (∀x. ¬R(x, z))))
⟶ ¬ (∀y z. ∃x. (R(x,y) ∧ R(x,z)))"
oops
end
</source>

T3

2020-05-28T09:38:25Z

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

Ejercicios

2020-05-28T09:37:48Z

Mjoseh:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]], [[Relación 1 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf Una solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]], [[Relación 2 |Solución colaborativa]], [[Rel 2 |Una solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]], [[Relación 3 |Solución colaborativa]], [[Rel 3 |Una solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]], [[Relación 4 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf Una solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]], [[Relación 5 |Solución colaborativa]], [[Rel 5 |Una solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]], [[Relación 6 |Solución colaborativa]] , [[Rel 6 |Una solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]], [[Relación 8 |Solución colaborativa]]).
** [[Rel 8 (rev 1) | Primera corrección]]
** [[Rel 8 (sol) | Una solución]]
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]], [[Relación 9 |Solución colaborativa]]).
** [[Rel 9 (rev 1) | Primera corrección]]
** [[Rel 9 (sol) | Una solución]]
* '''Ejercicio 1 (24-04-2020)''': ([[T1 |Enunciado]], [[T1 sol |Una solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]], [[Relación 10 |Solución colaborativa]]).
** [[Rel 10 (sol) | Una solución]]
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]], [[Relación 11 |Solución colaborativa]]).
** [[Rel 11 (sol) | Una solución]]
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]], [[Relación 12 |Solución colaborativa]]).
** [[Rel 12 (sol) | Una solución]]
* '''Ejercicio 2 (12-05-2020)''': ([[T2 |Enunciado]], [[T2 sol |Una solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]], [[Relación 13 |Solución colaborativa]]).
** [[Rel 13 (sol) | Una solución]]
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomátización de la Geometría.] ([[R14 |Enunciado]], [[Relación 14 |Solución colaborativa]]).
** [[Rel 14 (sol) | Una solución]]
* '''Ejercicio 3 (19-05-2020)''': ([[T3 |Enunciado]], [[T3 sol |Una solución]]).
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]], [[Relación 15 |Solución colaborativa]]).

R15

2020-05-28T06:58:39Z

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

<source lang = "isabelle">
chapter ‹ R15: Definiciones inductivas: clausuras ›

theory R15
imports Main
begin

section ‹ La clausura reflexiva transitiva ›

text ‹
· Las definiciones inductivas aceptan parámetros; por tanto, permite
expresar funciones que construyen conjuntos.

· La relaciones binarias son conjuntos de pares; por tanto, se pueden
definir inductivamente.
›

text ‹
· La clausura reflexiva y transitiva de una relación r es la menor
relación reflexiva y transitiva que contiene a r.

· Se representa por r*.

· Se puede definir inductivamente, como conjunto:
· (x,x) ∈ r*
· Si (x,y) ∈ r e (y,z) ∈ r*, entonces (x,z) ∈ r*

· La definición inductiva, como conjunto, se puede expresar en
Isabelle/HOL como sigue:
›

inductive_set
crt :: "('a × 'a) set ⇒ ('a × 'a) set" ("_*" [1000] 999)
for r :: "('a × 'a) set"
where
crt_refl [iff]: "(x,x) ∈ r*"
| crt_paso: "⟦(x,y) ∈ r; (y,z) ∈ r* ⟧ ⟹ (x,z) ∈ r*"

text ‹
Notas:
· La sintaxis concreta permite escribir r* en lugar de (crt r).
· La definición consta de dos reglas.
· A la regla reflexiva se le añade el atributo iff para aumentar la
automatización.
· A la regla del paso no se le añade ningún atributo, porque r* ocurre
en la izquierda.
· En el resto de esta sección se demuestra que esta definición
coincide con la menor relación reflexiva y transitiva que contiene a
r.
›

text ‹Lema. La relación r* es reflexiva.›

lemma "(x,x) ∈ r*"
oops

text ‹Lema. La relación r* contiene a r.›

― ‹La demostración aplicativa es ›
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"
oops

― ‹La demostración automática es›
lemma r_contenida_clausura [intro]:
"(x,y) ∈ r ⟹ (x,y) ∈ r*"
oops

― ‹La demostración declarativa es ›
lemma "(x,y) ∈ r ⟹ (x,y) ∈ r*"
oops

text ‹
Notas:
· La ventaja del lema es que se puede declarar como regla de
introducción, porque r* ocurre sólo en la derecha.
· Con la declaración, algunas demostraciones que usan crt_paso se
hacen de manera automática.
›

text ‹El esquema de inducción de la clausura reflexiva transitiva es
· crt.induct:
⟦(x1, x2) ∈ r*;
⋀x. P x x;
⋀x y z. ⟦(x,y) ∈ r; (y,z) ∈ r*; P y z⟧ ⟹ P x z⟧
⟹ P x1 x2
›

text ‹Lema. La relación r* es transitiva.›

― ‹La demostración aplicativa es›
lemma "⟦(x,y) ∈ r*; (y,z) ∈ r*⟧ ⟹ (x,z) ∈ r*"
oops

― ‹La demostración automática es›
lemma "⟦(x,y) ∈ r*; (y,z) ∈ r*⟧ ⟹ (x,z) ∈ r*"
oops

― ‹La demostración declarativa es ›
lemma assumes "(x,y) ∈ r*" and
"(y,z) ∈ r*"
shows "(x,z) ∈ r*"
oops

text ‹Otra formulación del lema, con la variable y a la derecha.›

― ‹La demostración aplicativa es›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
oops

― ‹La demostración automática es›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
oops

― ‹ Demostración declarativa ›
lemma crt_trans [rule_format]:
"(x,y) ∈ r* ⟹ (y,z) ∈ r* ⟶ (x,z) ∈ r*"
oops

text ‹Notas:
· La reformulación anterior es un caso particular de la siguiente
heurística:
"Para probar una fórmula por inducción sobre (x1,...,xn) ∈ R,
poner todas las premisas conteniendo cualquiera de lax xi en la
conclusión usando ⟶".
· El atributo "rule_format" transforma ⟶ en ⟹.›

text ‹La relación r* está contenida en cualquier relación reflexiva y
transitiva que contenga a r.

Mediante (crt2 r) se define la menor relación reflexiva y transitiva
que contiene a r.›

inductive_set
crt2 :: "('a × 'a)set ⇒ ('a × 'a)set"
for r :: "('a × 'a)set"
where
"(x,y) ∈ r ⟹ (x,y) ∈ crt2 r" (* contiene a r *)
| "(x,x) ∈ crt2 r" (* reflexiva *)
| "⟦(x,y) ∈ crt2 r; (y,z) ∈ crt2 r⟧ ⟹ (x,z) ∈ crt2 r" (* transitiva *)

text ‹Probaremos que r* coincide con (crt2 r) ›

text ‹Lema. La relación (crt2 r) está contenida en r*.›

― ‹Demostración aplicativa ›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
oops

― ‹Demostración automática›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
oops

― ‹Demostración declarativa ›
lemma "(x,y) ∈ crt2 r ⟹ (x,y) ∈ r*"
oops

text ‹Lema. La relación r* está contenida en (crt2 r).›

― ‹Demostración aplicativa ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
oops

― ‹Demostración automática ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
oops

― ‹Demostración declarativa ›
lemma "(x,y) ∈ r* ⟹ (x,y) ∈ crt2 r"
oops

text ‹------------------------------------------------------------------
Ejercicio 1. Demostrar que si (x,y) ∈ r* e (y,z) ∈ r, entonces
(x,z) ∈ r*
------------------------------------------------------------------- ›

― ‹Demostración aplicativa ›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
oops

― ‹ Demostración automática ›
lemma "(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
oops

― ‹Demostración declarativa ›
lemma crt_paso2 [rule_format]:
"(x,y) ∈ r* ⟹ (y,z) ∈ r ⟶ (x,z) ∈ r*"
oops

text ‹----------------------------------------------------------------
Ejercicio 2. Considerar la siguiente definición de la clausura tran-
sitiva de una relación r, y probar que es la menor relación reflexiva
y transitiva que contiene a r.

Nota: Establecer los lemas necesarios.
------------------------------------------------------------------- ›

inductive star' :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl': "star' r x x"
| step': "star' r x y ⟹ r y z ⟹ star' r x z"

― ‹ Demostración de que (star' r) es reflexiva ›
lemma star'Refl: "star' r x x"
oops

― ‹ Demostración aplicativa de r contenida en (star' r) ›
lemma "r x y ⟹ star' r x y"
oops

― ‹ Demostración automática de r contenida en (star' r) ›
lemma "r x y ⟹ star' r x y"
oops

― ‹ Demostración declarativa de r contenida en (star' r) ›
lemma rsubsetStar': "r x y ⟹ star' r x y"
oops

text ‹ A continuación se prueba una condición suficiente para star' r ›

― ‹ Demostración aplicativa ›
lemma
"⟦star' r y z; r x y⟧ ⟹ star' r x z"
oops

― ‹ Demostración automática ›
lemma star'_subset_star'_l1:
"⟦star' r y z; r x y⟧ ⟹ star' r x z"
oops

― ‹ Demostraciones de que (star' r) es transitiva ›

― ‹ Demostración aplicativa ›
lemma "⟦star' r x y; star' r y z⟧ ⟹ star' r x z"
oops

― ‹ Demostración automática ›
lemma star'Trans:
"⟦star' r x y; star' r y z⟧ ⟹ star' r x z"
oops

text ‹
---------------------------------------------------------------------
Ejercicio 3. Considerar la siguiente definición inductiva. Probar que
"star' r x y syss (∃n. iter r n x y)"
------------------------------------------------------------------- ›

inductive iter :: "('a ⇒ 'a ⇒ bool) ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool"
for r where
iterRefl: "iter r 0 x x"
| iterStep: "⟦iter r n x y; r y z⟧ ⟹ iter r (n+1) x z"

― ‹ El esquema de inducción correspondiente es ›
thm iter.induct
(*
⟦iter ?r ?x1.0 ?x2.0 ?x3.0;
⋀x. ?P 0 x x;
⋀n x y z. ⟦iter ?r n x y; ?P n x y; ?r y z⟧ ⟹ ?P (n + 1) x z⟧
⟹ ?P ?x1.0 ?x2.0 ?x3.0
*)

― ‹ Algunos teoremas derivados son ›

thm iterRefl
(* iter ?r 0 ?x ?x *)

thm iterRefl [of r y]
(* iter r 0 y y *)

thm iterStep
(* ⟦iter ?r ?n ?x ?y; ?r ?y ?z⟧ ⟹ iter ?r (?n + 1) ?x ?z *)

thm iterStep [of r x y n z]
(* ⟦iter r x y n; r n z⟧ ⟹ iter r (x + 1) y z *)

thm iterStep [of r x y 0 y]
(* ⟦iter r x y 0; r 0 y⟧ ⟹ iter r (x + 1) y y *)

text ‹
---------------------------------------------------------------------
Ejercicio 3.1. Demostrar
star' r x y ⟹ (∃n. iter r n x y)
------------------------------------------------------------------- ›

― ‹ Demostración aplicativa ›
lemma "star' r x y ⟹ (∃n. iter r n x y)"
oops

― ‹ Demostración automática ›
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"
oops

― ‹ Demostración declarativa ›
lemma [rule_format]: "star' r x y ⟹ (∃n. iter r n x y)"
oops

text ‹
---------------------------------------------------------------------
Ejercicio 3.2. Demostrar
(∃n. iter r n x y) ⟹ star' r x y
------------------------------------------------------------------- ›

― ‹ En la demostración se usará el siguiente lema:
iter r n x y ⟹ star' r x y ›

― ‹ Demostración aplicativa del lema ›
lemma iter_star'_subset: "iter r n x y ⟹ star' r x y"
oops

― ‹ Demostración automática del lema ›
lemma "iter r n x y ⟹ star' r x y"
oops

― ‹ Demostración aplicativa ›
lemma "(∃n. iter r n x y) ⟹ star' r x y"
oops

― ‹ Demostración automática ›
lemma "(∃n. iter r n x y) ⟹ star' r x y"
oops

― ‹ Demostración declarativa ›
lemma assumes "(∃n. iter r n x y)"
shows "star' r x y"
oops

end

</source>

R15

2020-05-28T06:58:20Z

Mjoseh: Página creada con «<source lang = "isabelle"> chapter ‹ R15: Definiciones inductivas: clausuras › theory R15 imports Main begin section ‹ La clausura reflexiva transitiva › text…»

Rel 14 (sol)

2020-05-28T06:56:16Z

Mjoseh: Protegió «Rel 14 (sol)» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

<source lang = "isabelle">
theory R14_sol
imports Main

begin

text ‹------------------------------------------------------------------
Ejercicio 1. Hilbert publicó una axiomatización de la geometría que
incluía los siguientes axiomas:
1. Por dos puntos distintos pasa una línea recta.
2. Por dos puntos distintos no pasa más de una línea recta.
3. Toda línea tiene al menos dos puntos.
4. Existen al menos tres puntos no alineados.

Usando la relacion en(p,l) para representar que el punto p está en
la línea l, definir el entorno local Geom en el que se verifiquen los
4 axiomas anteriores.
---------------------------------------------------------------------›

locale Geom =
fixes en :: "'p ⇒ 'l ⇒ bool"
assumes linea_por_dos_puntos:
"a ≠ b ⟹ ∃l. en a l ∧ en b l"
and linea_por_dos_puntos_unica:
"⟦a ≠ b; en a l; en b l; en a m; en b m⟧ ⟹ l = m"
and dos_puntos_de_la_linea:
"∃a b. a ≠ b ∧ en a l ∧ en b l"
and tres_puntos_no_alineados:
"∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧
¬ (∃l. en a l ∧ en b l ∧ en c l)"
begin

text ‹------------------------------------------------------------------
Ejercicio 2. Demostrar que
∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)
---------------------------------------------------------------------›

― ‹ Demostración automática ›
lemma
"∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
using tres_puntos_no_alineados by auto

― ‹ Demostración estructurada ›
lemma tres_puntos_no_alineados_alt:
"∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
proof -
obtain a b c where distintos: "a ≠ b ∧ a ≠ c ∧ b ≠ c"
"¬ (∃l. en a l ∧ en b l ∧ en c l)"
using tres_puntos_no_alineados by blast
then have "∀l. en a l ∧ en b l ⟶ ¬ en c l"
by blast
then show ?thesis
using distintos by blast
qed

― ‹ Demostración detallada ›
lemma
"∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
proof -
have 1: "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ ¬ (∃l. en a l ∧ en b l ∧ en c l)"
by (rule tres_puntos_no_alineados)
obtain a b c where 2: "a ≠ b ∧ a ≠ c ∧ b ≠ c ∧
¬ (∃l. en a l ∧ en b l ∧ en c l)"
using 1 by (elim exE)
then have 3: "a ≠ b"
by (rule conjE)
have 4: "a ≠ c ∧ b ≠ c ∧ ¬ (∃l. en a l ∧ en b l ∧ en c l)"
using 2 by (rule conjE)
then have 5: "a ≠ c"
by (rule conjE)
have 6: "b ≠ c ∧ ¬ (∃l. en a l ∧ en b l ∧ en c l)"
using 4 by (rule conjE)
then have 7: "b ≠ c"
by (rule conjE)
with 5 have 8: "a ≠ c ∧ b ≠ c"
by (rule conjI)
with 3 have 9: "a ≠ b ∧ a ≠ c ∧ b ≠ c"
by (rule conjI)
have 10: " ¬ (∃l. en a l ∧ en b l ∧ en c l)"
using 6 by (rule conjE)
have 12: "∀l. en a l ∧ en b l ⟶ ¬ en c l"
proof (rule allI)
fix l
show "en a l ∧ en b l ⟶ ¬ en c l"
proof (rule impI)
assume 11: "en a l ∧ en b l"
show "¬ en c l"
proof (rule notI)
assume "en c l"
hence "en a l ∧ en b l ∧ en c l"
using 11 by blast
hence "∃l. en a l ∧ en b l ∧ en c l"
by (rule exI)
with 10 show False
by (rule notE)
qed
qed
qed
have "a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
using 9 12 by blast
then show
"∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
by (intro exI)
qed

text ‹------------------------------------------------------------------
Ejercicio 3. Demostrar que no todos los puntos pertenecen a la misma
línea.
---------------------------------------------------------------------›

― ‹Demostración automática›
lemma "∀l. ∃x. ¬ en x l"
using tres_puntos_no_alineados_alt by auto

― ‹ Demostración estructurada ›
lemma punto_no_en_linea: "∀l. ∃x. ¬ en x l"
proof
fix l
obtain a b c where l3: "¬ (en a l ∧ en b l ∧ en c l)"
using tres_puntos_no_alineados by blast
then show "∃x. ¬ en x l" by blast
qed

― ‹Demostración detallada ›
lemma "∀l. ∃x. ¬ en x l"
proof (rule allI)
fix l
have "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c
∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
by (rule tres_puntos_no_alineados_alt)
then obtain a b c where "a ≠ b ∧ a ≠ c ∧ b ≠ c
∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
by (elim exE)
then have "∀l. en a l ∧ en b l ⟶ ¬ en c l"
by (elim conjE)
then have 1:"en a l ∧ en b l ⟶ ¬ en c l"
by (rule allE)
show "∃x. ¬ en x l"
proof (cases)
assume "¬ en a l" then show "∃x. ¬ en x l"
by (rule exI)
next
assume "¬ ¬ en a l"
then have "en a l"
by (rule notnotD)
then show "∃x. ¬ en x l"
proof (cases)
assume "en b l"
with ‹en a l› have "en a l ∧ en b l"
by (rule conjI)
with 1 have "¬ en c l"
by (rule mp)
then show "∃x. ¬ en x l"
by (rule exI)
next
assume "¬ en b l" then show "∃x. ¬ en x l"
by (rule exI)
qed
qed
qed

text ‹------------------------------------------------------------------
Ejercicio 4. Demostrar que por cada punto pasa más de una línea.
---------------------------------------------------------------------›

― ‹ Demostración automática ›
lemma "∃l m. en x l ∧ en x m ∧ l ≠ m"
by (metis linea_por_dos_puntos tres_puntos_no_alineados_alt)

― ‹ Demostración estructurada ›
lemma dos_lineas_por_punto: "∃l m. en x l ∧ en x m ∧ l ≠ m"
proof -
obtain z where "z ≠ x" using dos_puntos_de_la_linea
by metis
then obtain l where xl: "en x l" and zl: "en z l"
using linea_por_dos_puntos by blast
obtain w where n_wl: "¬ en w l"
using punto_no_en_linea by blast
obtain m where wm: "en x m" and zm: "en w m"
using linea_por_dos_puntos xl by metis
then have "l ≠ m"
using n_wl by blast
then show ?thesis
using wm xl by blast
qed

text ‹------------------------------------------------------------------
Ejercicio 5. Demostrar que dos líneas distintas no pueden tener más
de un punto común.
---------------------------------------------------------------------›

― ‹ Demostración automática ›
lemma
assumes "l ≠ m"
"en x l"
"en x m"
"en y l"
"en y m"
shows "x = y"
using assms linea_por_dos_puntos_unica by blast

― ‹ Demostración estructurada ›
lemma interseccion_lineas_distintas:
assumes "l ≠ m"
"en x l"
"en x m"
"en y l"
"en y m"
shows "x = y"
proof (rule ccontr)
assume "x ≠ y"
then have "l = m"
using linea_por_dos_puntos_unica assms(2-5) by simp
then show "False"
using assms(1) by simp
qed

end

text ‹------------------------------------------------------------------
Ejercicio 6. Extender el ámbito ("locale") Geom definiendo la relación
colineal tal que (colineal a b c) se verifica si existe una línea
recta que pasa por los puntos a, b y c.
---------------------------------------------------------------------›

definition (in Geom)
colineal :: "'p ⇒ 'p ⇒ 'p ⇒ bool"
where "colineal a b c ≡ ∃l. en a l ∧ en b l ∧ en c l"

text ‹------------------------------------------------------------------
Ejercicio 7. Demostrar que existen tres puntos a, b y c tales que
¬ colineal a b c
---------------------------------------------------------------------›

― ‹ Demostración automática ›
lemma (in Geom) "∃a b c. ¬ colineal a b c"
using colineal_def tres_puntos_no_alineados by blast

― ‹ Demostración estructurada ›
lemma (in Geom) "∃a b c. ¬ colineal a b c"
proof -
have "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧
¬ (∃l. en a l ∧ en b l ∧ en c l)"
by (rule tres_puntos_no_alineados)
then have "∃a b c. ¬ (∃l. en a l ∧ en b l ∧ en c l)"
by blast
then show ?thesis
by (simp add: colineal_def)
qed

end

</source>

Rel 14 (sol)

2020-05-28T06:56:05Z

Mjoseh: Página creada con «<source lang = "isabelle"> theory R14_sol imports Main begin text ‹------------------------------------------------------------------ Ejercicio 1. Hilbert publicó u…»

Ejercicios

2020-05-28T06:54:50Z

Mjoseh:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]], [[Relación 1 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf Una solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]], [[Relación 2 |Solución colaborativa]], [[Rel 2 |Una solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]], [[Relación 3 |Solución colaborativa]], [[Rel 3 |Una solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]], [[Relación 4 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf Una solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]], [[Relación 5 |Solución colaborativa]], [[Rel 5 |Una solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]], [[Relación 6 |Solución colaborativa]] , [[Rel 6 |Una solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]], [[Relación 8 |Solución colaborativa]]).
** [[Rel 8 (rev 1) | Primera corrección]]
** [[Rel 8 (sol) | Una solución]]
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]], [[Relación 9 |Solución colaborativa]]).
** [[Rel 9 (rev 1) | Primera corrección]]
** [[Rel 9 (sol) | Una solución]]
* '''Ejercicio 1 (24-04-2020)''': ([[T1 |Enunciado]], [[T1 sol |Una solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]], [[Relación 10 |Solución colaborativa]]).
** [[Rel 10 (sol) | Una solución]]
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]], [[Relación 11 |Solución colaborativa]]).
** [[Rel 11 (sol) | Una solución]]
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]], [[Relación 12 |Solución colaborativa]]).
** [[Rel 12 (sol) | Una solución]]
* '''Ejercicio 2 (12-05-2020)''': ([[T2 |Enunciado]], [[T2 sol |Una solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]], [[Relación 13 |Solución colaborativa]]).
** [[Rel 13 (sol) | Una solución]]
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomátización de la Geometría.] ([[R14 |Enunciado]], [[Relación 14 |Solución colaborativa]]).
** [[Rel 14 (sol) | Una solución]]
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]], [[Relación 15 |Solución colaborativa]]).

R14

2020-05-21T14:47:02Z

Mjoseh:

<source lang ="isabelle">
chapter ‹R14: Una axiomatización de la Geometría›

theory R14
imports Main

begin

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 1. Hilbert publicó una axiomatización de la geometría que incluía los siguientes
axiomas:
1. Por dos puntos distintos pasa una línea recta.
2. Por dos puntos distintos no pasa más de una línea recta.
3. Toda línea tiene al menos dos puntos.
4. Existen al menos tres puntos no alineados.

Usando la relacion en(p,l) para representar que el punto p está en la línea l, definir el entorno
local Geom en el que se verifiquen los 4 axiomas anteriores.
--------------------------------------------------------------------------------------------------
›

locale Geom =
fixes en :: "'p ⇒ 'l ⇒ bool"
assumes linea_por_dos_puntos: "a ≠ b ⟹ ∃l. en a l ∧ en b l"
and linea_por_dos_puntos_unica: "⟦a ≠ b; en a l; en b l; en a m; en b m⟧ ⟹ l = m"
and dos_puntos_de_la_linea: "∃a b. a ≠ b ∧ en a l ∧ en b l"
and tres_puntos_no_alineados: "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧
¬ (∃l. en a l ∧ en b l ∧ en c l)"
begin

text ‹
--------------------------------------------------------------------------------------------------
Nota: En los ejercicios siguientes se pide la demostración
estructurada con el menor número de métodos automáticos posibles.
--------------------------------------------------------------------------------------------------
›

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 2. Demostrar que
∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
oops

― ‹ Demostración estructurada ›
lemma tres_puntos_no_alineados_alt:
"∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
oops

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 3. Demostrar que no todos los puntos pertenecen a la misma línea.
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma "∀l. ∃x. ¬ en x l"
oops

― ‹ Demostración estructurada ›
lemma punto_no_en_linea: "∀l. ∃x. ¬ en x l"
oops

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 4. Demostrar que por cada punto pasa más de una línea.
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma "∃l m. en x l ∧ en x m ∧ l ≠ m"
oops

― ‹ Demostración estructurada ›
lemma dos_lineas_por_punto: "∃l m. en x l ∧ en x m ∧ l ≠ m"
oops

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 5. Demostrar que dos líneas distintas no pueden tener más de un punto común.
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma
assumes "l ≠ m"
"en x l"
"en x m"
"en y l"
"en y m"
shows "x = y"
oops

― ‹ Demostración estructurada ›
lemma interseccion_lineas_distintas:
assumes "l ≠ m"
"en x l"
"en x m"
"en y l"
"en y m"
shows "x = y"
oops

end

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 6. Extender el ámbito ("locale") Geom definiendo la relación colineal tal que
(colineal a b c) se verifica si existe una línea recta que pasa por los puntos a, b y c.
--------------------------------------------------------------------------------------------------
›

definition (in Geom)
colineal :: "'p ⇒ 'p ⇒ 'p ⇒ bool"
where "colineal a b c ≡ ∃l. en a l ∧ en b l ∧ en c l"

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 7. Demostrar que existen tres puntos a, b y c tales que
¬ colineal a b c
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma (in Geom) "∃a b c. ¬ colineal a b c"
oops

― ‹ Demostración estructurada ›
lemma (in Geom) "∃a b c. ¬ colineal a b c"
oops

end

</source>

R14

2020-05-21T09:57:05Z

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

<source lang "isabelle">
chapter ‹R14: Una axiomatización de la Geometría›

theory R14
imports Main

begin

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 1. Hilbert publicó una axiomatización de la geometría que incluía los siguientes
axiomas:
1. Por dos puntos distintos pasa una línea recta.
2. Por dos puntos distintos no pasa más de una línea recta.
3. Toda línea tiene al menos dos puntos.
4. Existen al menos tres puntos no alineados.

Usando la relacion en(p,l) para representar que el punto p está en la línea l, definir el entorno
local Geom en el que se verifiquen los 4 axiomas anteriores.
--------------------------------------------------------------------------------------------------
›

locale Geom =
fixes en :: "'p ⇒ 'l ⇒ bool"
assumes linea_por_dos_puntos: "a ≠ b ⟹ ∃l. en a l ∧ en b l"
and linea_por_dos_puntos_unica: "⟦a ≠ b; en a l; en b l; en a m; en b m⟧ ⟹ l = m"
and dos_puntos_de_la_linea: "∃a b. a ≠ b ∧ en a l ∧ en b l"
and tres_puntos_no_alineados: "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧
¬ (∃l. en a l ∧ en b l ∧ en c l)"
begin

text ‹
--------------------------------------------------------------------------------------------------
Nota: En los ejercicios siguientes se pide la demostración
estructurada con el menor número de métodos automáticos posibles.
--------------------------------------------------------------------------------------------------
›

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 2. Demostrar que
∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
oops

― ‹ Demostración estructurada ›
lemma tres_puntos_no_alineados_alt:
"∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
oops

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 3. Demostrar que no todos los puntos pertenecen a la misma línea.
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma "∀l. ∃x. ¬ en x l"
oops

― ‹ Demostración estructurada ›
lemma punto_no_en_linea: "∀l. ∃x. ¬ en x l"
oops

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 4. Demostrar que por cada punto pasa más de una línea.
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma "∃l m. en x l ∧ en x m ∧ l ≠ m"
oops

― ‹ Demostración estructurada ›
lemma dos_lineas_por_punto: "∃l m. en x l ∧ en x m ∧ l ≠ m"
oops

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 5. Demostrar que dos líneas distintas no pueden tener más de un punto común.
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma
assumes "l ≠ m"
"en x l"
"en x m"
"en y l"
"en y m"
shows "x = y"
oops

― ‹ Demostración estructurada ›
lemma interseccion_lineas_distintas:
assumes "l ≠ m"
"en x l"
"en x m"
"en y l"
"en y m"
shows "x = y"
oops

end

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 6. Extender el ámbito ("locale") Geom definiendo la relación colineal tal que
(colineal a b c) se verifica si existe una línea recta que pasa por los puntos a, b y c.
--------------------------------------------------------------------------------------------------
›

definition (in Geom)
colineal :: "'p ⇒ 'p ⇒ 'p ⇒ bool"
where "colineal a b c ≡ ∃l. en a l ∧ en b l ∧ en c l"

text ‹
--------------------------------------------------------------------------------------------------
Ejercicio 7. Demostrar que existen tres puntos a, b y c tales que
¬ colineal a b c
--------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma (in Geom) "∃a b c. ¬ colineal a b c"
oops

― ‹ Demostración estructurada ›
lemma (in Geom) "∃a b c. ¬ colineal a b c"
oops

end

</source>

R14

2020-05-21T09:56:54Z

Mjoseh: Página creada con «<source lang "isabelle"> chapter ‹R14: Una axiomatización de la Geometría› theory R14 imports Main begin text ‹ -----------------------------------------------…»