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

2020-05-18T16:07:32Z

Protegió «T2 sol» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « text ‹Ejercicio 2 de Lógica Matemática y Fundamentos (12-mayo-2020)› theory Ejercicio_2_sol imports Main begin lemma notnotI: "P ⟹ ¬¬…»

2020-05-18T16:07:18Z

Página creada con «<source lang ="isabelle"> text ‹Ejercicio 2 de Lógica Matemática y Fundamentos (12-mayo-2020)› theory Ejercicio_2_sol imports Main begin lemma notnotI: "P ⟹ ¬¬…»

Página nueva

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

theory Ejercicio_2_sol
imports Main
begin

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

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

text ‹------------------------------------------------------------------
Se define la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de xs cumplen
la propiedad p. Por ejemplo,
todos (λx. x>(1::nat)) [2,6,4] = True
todos (λx. x>(2::nat)) [2,6,4] = False
Nota: La conjunción se representa por ∧
---------------------------------------------------------------------›

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

text ‹------------------------------------------------------------------
Se define la función
filtra :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list"
tal que (filtra p xs) es la lista de los elementos de xs que cumplen
la propiedad p. Por ejemplo,
filtra (λx. x>(1::nat)) [2,6,4] = [2, 6, 4]
filtra (λx. x>(4::nat)) [2,6,4] = [6]
----------------------------------------------------------------- ›

fun filtra :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
"filtra p [] = []"
| "filtra p (x#xs) = (if p x
then x # filtra p xs
else filtra p xs)"

text ‹Ejercicio: Demostrar que todos los elementos de la lista
(filtra p xs) verifican el predicado p, de las formas siguientes:
+ 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 automática›
lemma "todos p (filtra p xs)"
apply (induct xs)
apply simp_all
done

― ‹Demostración en lenguaje natural
Por inducción en xs.

+ Caso base: xs = []
todos (filtra p [])
= todos [] (por def. de filtra)
= True (por def. de todos)

+ Paso inductivo: Sean x un elemento y xs una lista de elementos.
La hipótesis de inducción (HI) es "todos p (filtra p xs)"
Hay que probar que "todos p (filtra p (x#xs))"
Consideramos los dos casos siguientes:

+ Caso 1: Supongamos que se verifica "p x". Entonces,
todos p (filtra p (x#xs))
= todos p (x # filtra p xs) (por def. de filtra)
= p x /\ todos p (filtra p xs) (por def. de todos)
= True (por HI y caso 1)

+ Caso 2: Supongamos que no se verifica "p x". Entonces,
todos p (filtra p (x#xs))
= todos p (filtra p xs) (por def. de filtra)
= True (por HI)
›

― ‹Demostración aplicativa detallada›
lemma "todos p (filtra p xs)"
apply (induct xs)
apply (simp only: filtra.simps(1)
todos.simps(1))
apply (simp only: filtra.simps(2))
apply (split if_split)
apply (rule conjI)
apply (simp only: todos.simps(2))
apply (rule impI)
apply (rule conjI, assumption)
apply (simp only: implies_True_equals)
apply (rule impI, assumption)
done

― ‹Demostración estructurada›
lemma "todos p (filtra p xs)"
proof (induct xs)
show "todos p (filtra p [])"
by simp
next
fix x xs
assume HI: "todos p (filtra p xs)"
show "todos p (filtra p (x#xs))"
proof cases
assume "p x"
then have 1: "filtra p (x#xs) = x # filtra p xs"
by simp
have "(p x ∧ todos p (filtra p xs))"
using ‹p x› HI by (rule conjI)
then show "todos p (filtra p (x#xs))"
using 1 by simp
next
assume "¬ p x"
then have 2: "filtra p (x#xs) = filtra p xs"
by simp
then show "todos p (filtra p (x#xs))"
using 2 HI by simp
qed
qed

― ‹Demostración declarativa detallada›
lemma "todos p (filtra p xs)"
proof (induct xs)
show "todos p (filtra p [])"
by (simp only: filtra.simps(1) todos.simps(1))
next
fix x xs
assume HI: "todos p (filtra p xs)"
show "todos p (filtra p (x#xs))"
proof cases
assume "p x"
then have 1: "filtra p (x#xs) = x # filtra p xs"
by (simp only: filtra.simps(2) if_True)
have "(p x ∧ todos p (filtra p xs))"
using ‹p x› HI by (rule conjI)
then have "todos p (x#(filtra p xs))"
by (simp only: todos.simps(2))
then show "todos p (filtra p (x#xs))"
using 1 by (simp only: if_True)
next
assume "¬ p x"
then have "filtra p (x#xs) = filtra p xs"
by (simp only: filtra.simps(2) if_False)
then show "todos p (filtra p (x#xs))"
using HI by (simp only: if_True)
qed
qed

― ‹2ª Demostración declarativa detallada›
lemma "todos p (filtra p xs)"
proof (induct xs)
show "todos p (filtra p [])"
by (simp only: filtra.simps(1) todos.simps(1))
next
fix x xs
assume HI: "todos p (filtra p xs)"
show "todos p (filtra p (x#xs))"
proof cases
assume "p x"
then have "todos p (filtra p (x#xs)) = todos p (x # filtra p xs)"
by (simp only: filtra.simps(2) if_True)
also have "… = (p x ∧ todos p (filtra p xs))"
by (simp only: todos.simps(2))
also have "… = (True ∧ True)"
by (simp only: ‹p x› HI)
also have "… = True"
by (simp only: conj_absorb)
finally show "todos p (filtra p (x#xs))"
by (simp only: eq_True)
next
assume "¬ p x"
then have "todos p (filtra p (x#xs)) = todos p (filtra p xs)"
by (simp only: filtra.simps(2) if_False)
also have "… = True"
by (simp only: HI)
finally show "todos p (filtra p (x#xs))"
by (simp only: eq_True)
qed
qed

― ‹Demostración declarativa detallada con lemas auxiliares›
lemma filtraTrue:
assumes "p x"
shows "filtra p (x#xs) = x# filtra p xs"
using assms
by (simp only: filtra.simps(2) if_True)

lemma filtraFalse:
assumes "¬ p x"
shows "filtra p (x#xs) = filtra p xs"
using assms
by (simp only: filtra.simps(2) if_False)

lemma "todos p (filtra p xs)"
proof (induct xs)
show "todos p (filtra p [])"
by (simp only: filtra.simps(1) todos.simps(1))
next
fix x xs
assume HI: "todos p (filtra p xs)"
show "todos p (filtra p (x#xs))"
proof cases
assume "p x"
then have 1: "filtra p (x#xs) = x # filtra p xs"
by (rule filtraTrue)
have "(p x ∧ todos p (filtra p xs))"
using ‹p x› HI by (rule conjI)
then have "todos p (x#(filtra p xs))"
by (simp only: todos.simps(2))
then show "todos p (filtra p (x#xs))"
using 1 by (simp only: if_True)
next
assume "¬ p x"
then have "filtra p (x#xs) = filtra p xs"
by (rule filtraFalse)
then show "todos p (filtra p (x#xs))"
using HI by (simp only: if_True)
qed
qed

end

</source>

← Revisión anterior	Revisión del 16:07 18 may 2020
(Sin diferencias)

T2 sol - Historial de revisiones

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

Mjoseh: Página creada con « text ‹Ejercicio 2 de Lógica Matemática y Fundamentos (12-mayo-2020)› theory Ejercicio_2_sol imports Main begin lemma notnotI: "P ⟹ ¬¬…»