T2

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