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

2020-09-10T08:20:02Z

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

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

2020-09-10T08:19:49Z

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

Página nueva

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

← Revisión anterior	Revisión del 08:20 10 sep 2020
(Sin diferencias)

Examen 2C sol - Historial de revisiones

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

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