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