T3 sol

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