Relación 10

chapter {* R10: Formalización y argumentación con Isabelle/HOL *}

theory R10_Formalizacion_y_argmentacion
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta es relación formalizar y demostrar la corrección
  de los argumentos automáticamente y detalladamente usando sólo las reglas
  básicas de deducción natural. 

  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · impI:       (P ⟹ Q) ⟹ P ⟶ Q
  · disjI1:     P ⟹ P ∨ Q
  · disjI2:     Q ⟹ P ∨ Q
  · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:     False ⟹ P
  · notE:       ⟦¬P; P⟧ ⟹ R
  · notI:       (P ⟹ False) ⟹ ¬P
  · iffI:       ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:      ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:      ⟦P = Q; Q⟧ ⟹ P
  · ccontr:     (¬P ⟹ False) ⟹ P

  · allI:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  · allE:       (⋀x. P x) ⟹ ∀x. P x
  · exI:        P x ⟹ ∃x. P x
  · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

  · refl:       t = t
  · subst:      ⟦s = t; P s⟧ ⟹ P t
  · trans:      ⟦r = s; s = t⟧ ⟹ r = t
  · sym:        s = t ⟹ t = s
  · not_sym:    t ≠ s ⟹ s ≠ t
  · ssubst:     ⟦t = s; P s⟧ ⟹ P t
  · box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
  · arg_cong:   x = y ⟹ f x = f y
  · fun_cong:   f = g ⟹ f x = g x
  · cong:       ⟦f = g; x = y⟧ ⟹ f x = g y
  --------------------------------------------------------------------- 
*}

text {*
  Se usarán las reglas notnotI, mt, no_ex y no_para_todo que demostramos
  a continuación. 
  *}

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

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

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

lemma no_para_todo: "¬(∀x. P(x)) ⟹ ∃x. ¬P(x)"
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si la válvula está abierta o la monitorización está preparada,
     entonces se envía una señal de reconocimiento y un mensaje de
     funcionamiento al controlador del ordenador. Si se envía un mensaje 
     de funcionamiento al controlador del ordenador o el sistema está en 
     estado normal, entonces se aceptan las órdenes del operador. Por lo
     tanto, si la válvula está abierta, entonces se aceptan las órdenes
     del operador. 
  Usar A : La válvula está abierta.
       P : La monitorización está preparada.
       R : Envía una señal de reconocimiento.
       F : Envía un mensaje de funcionamiento.
       N : El sistema está en estado normal.
       O, AO, OK : Se aceptan órdenes del operador.
  ------------------------------------------------------------------ *}

(* ivamenjim manmorjim1 crigomgom*)
(* Buscando, he detectado que 'O' es un carácter especial en Isabelle y que forma parte de su
sintaxis pre-definida, por lo que da problemas a la hora de formalizar y demostrar 
el argumento planteado. Por lo tanto, en su lugar he usado "AO: Se aceptan órdenes del operador" *)

lemma ejercicio_1:
  assumes 1: "(A ∨ P) ⟶ (R ∧ F)" 
  assumes 2: "(F ∨ N) ⟶ AO"
  shows "A ⟶ AO"
proof -
  {assume 3: "A"
   have 4: "A ∨ P" using 3 by (rule disjI1)
   have 5: "R ∧ F" using 1 4 by (rule mp)
   have 6: "F" using 5 by (rule conjunct2)
   have 7: "F ∨ N" using 6 by (rule disjI1)
   have 8: "AO" using 2 7 by (rule mp)}
  then show "A ⟶ AO" by (rule impI)
qed  

(*danrodcha ferrenseg anaprarod marcarmor13*)

lemma ej_1: 
  assumes "A ∨ P ⟶ R ∧ F" and 
          "F ∨ N ⟶ OK"
  shows "A ⟶ OK"
proof (rule impI)
{assume "A"
  hence "A ∨ P" by (rule disjI1)
  with assms(1) have "R ∧ F" by (rule mp)
  hence "F" by (rule conjE)
  hence "F ∨ N" by (rule disjI1)
  with assms(2) show "OK" by (rule mp)}
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
     tanto, hay estudiantes inteligentes y trabajadores.
  Usar I(x) para x es inteligente
       T(x) para x es trabajador
  ------------------------------------------------------------------ *}

(* ivamenjim ferrenseg danrodcha anaprarod crigomgom marcarmor13*)

lemma ejercicio_2:
  assumes "(∃x. I(x)) ∧ (∃x. T(x))"
  shows   "∃x. (I(x) ∧ T(x))"
  quickcheck
oops

(* Encontrando el contraejemplo: 
   I = {a1} 
   x = a1
   T = {a2}
   xa = a2 
*)


text {* --------------------------------------------------------------- 
  Ejercicio 3. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
     es padre de Luis. Por tanto, Carlos es padre de Juan.
  Usar H(x,y) para x es hermano de y
       P(x,y) para x es padre de y
       j      para Juan
       l      para Luis
       c      para Carlos
  ------------------------------------------------------------------ *}

(* ivamenjim crigomgom*)

lemma ejercicio_3:
  assumes 1: "∀x y. P(x,y) ⟶ (∀z. (H(z,y) ⟶ P(x,z)))" 
  assumes 2: "H(j,l)"
  assumes 3: "P(c,l)"
  shows "P(c,j)"
proof -
  have 4 : "∀y. P(c,y) ⟶ (∀z. (H(z,y) ⟶ P(c,z)))" using 1 by (rule allE)
  have 5 : "P(c,l) ⟶ (∀z. (H(z,l) ⟶ P(c,z)))" using 4 by (rule allE)
  then have 6 : "(∀z. (H(z,l) ⟶ P(c,z)))" using 3 by (rule mp)
  have 7 : "H(j,l) ⟶ P(c,j)" using 6 by (rule allE)
  then show "P(c,j)" using 2 by (rule mp)
qed    

(* danrodcha anaprarod ferrenseg marcarmor13*)
(* es casi igual que la anterior *)
lemma ej_3:
  assumes "∀x y. P(x,y) ⟶ (∀z. (H(z,y) ⟶ P(x,z)))" 
  assumes "H(j,l)"
  assumes "P(c,l)"
  shows "P(c,j)"
proof (rule mp)
  have 4 : "∀y. P(c,y) ⟶ (∀z. (H(z,y) ⟶ P(c,z)))" using assms(1) by (rule allE)
  hence "P(c,l) ⟶ (∀z. (H(z,l) ⟶ P(c,z)))" by (rule allE)
  hence "(∀z. (H(z,l) ⟶ P(c,z)))" using assms(3) by (rule mp)
  thus "H(j,l) ⟶ P(c,j)" by (rule allE)
  next
  show "H(j,l)" using assms(2) by this
qed 



text {* --------------------------------------------------------------- 
  Ejercicio 4. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Los aficionados al fútbol aplauden a cualquier futbolista
     extranjero. Juanito no aplaude a futbolistas extranjeros. Por
     tanto, si hay algún futbolista extranjero nacionalizado español,
     Juanito no es aficionado al fútbol.
  Usar Af(x)   para x es aficicionado al fútbol
       Ap(x,y) para x aplaude a y
       E(x)    para x es un futbolista extranjero
       N(x)    para x es un futbolista nacionalizado español
       j       para Juanito
  ------------------------------------------------------------------ *}
(* danrodcha  ferrenseg *)
(* danrodcha: Me gusta más la formalización de ana prado, aunque 
    son equivalentes *)
lemma ej_4:
  assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x,y)"
          "∀x. Ap(j,x) ⟶ ¬ E(x)"
  shows   "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
  proof (rule impI)
  assume "∃x. E(x) ∧ N(x)"
    then obtain a where "E(a) ∧ N(a)" by (rule exE)
    hence "E(a)" by (rule conjE)
    show "¬ Af(j)"
    proof (rule notI)
      assume "Af(j)"
      hence "Af(j) ∧ E(a)" using `E(a)` by (rule conjI)
      have "∀y. Af(j) ∧ E(y) ⟶ Ap(j,y)" using assms(1) by (rule allE)
      hence "Af(j) ∧ E(a) ⟶ Ap(j,a)" by (rule allE)
      hence "Ap(j,a)" using `Af(j) ∧ E(a)` by (rule mp)
      have "Ap(j,a) ⟶ ¬ E(a)" using assms(2) by (rule allE)
      hence "¬ E(a)" using `Ap(j,a)` by (rule mp)
      thus False using `E(a)` by (rule notE)
    qed
qed

(* ivamenjim crigomgom marcarmor13*)

lemma ejercicio_4:
  assumes 1: "∀x y. Af(x) ∧ E(y) ⟶ Ap(x,y)"
  assumes 2: "¬(∃x. E(x) ∧ Ap(j,x))"
  shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"  
  proof (rule impI)
  assume 3: "∃x. E(x) ∧ N(x)"
    then obtain a where 4: "E(a) ∧ N(a)" by (rule exE)
    then have 5: "E(a)" by (rule conjunct1)
    show 6: "¬Af(j)"
    proof (rule notI)
      assume 7: "Af(j)"
      then have 8: "Af(j) ∧ E(a)" using 5 by (rule conjI)
      have 9: "∀y. Af(j) ∧ E(y) ⟶ Ap(j,y)" using 1 by (rule allE)
      have 10: "Af(j) ∧ E(a) ⟶ Ap(j,a)" using 9 by (rule allE)
      have 11: "Ap(j,a)" using 10 8 by (rule mp)
      have 12: "E(a) ∧ Ap(j,a)" using 5 11 by (rule conjI)
      have 13: "∃x. E(x) ∧ Ap(j,x)" using 12 by (rule exI)
      show "False" using 2 13 by (rule notE)
    qed
qed  

(* anaprarod *)

(* Este auxiliar ya se probó en el ejercicio 4 de la rel 8 *)
lemma aux4: "¬(p∧q) ⟹¬p ∨ ¬q"
by (auto)

lemma ej_4:
  assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x,y)"
          "∀ x.(E(x) ⟶ ¬ Ap(j,x))"
  shows   "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
proof (rule impI)
  { assume "∃x. E(x) ∧ N(x)"
    then obtain a where 1: "E(a) ∧ N(a)" by (rule exE)
    have "∀ y. Af(j) ∧ E(y) ⟶ Ap(j,y)" using assms(1)  by (rule allE)
    hence 2: "Af(j) ∧ E(a) ⟶ Ap(j,a)" by (rule allE)
    have 3: "E(a)" using 1 by (rule conjunct1)
    have 4: "E(a) ⟶ ¬ Ap(j,a)" using assms(2) by (rule allE)
    have 5: "¬ Ap(j,a)" using 4 3 by (rule mp)
    have "¬(Af(j) ∧ E(a))" using 2 5 by (rule mt)
    hence "¬ Af(j) ∨ ¬ E(a)" by (rule aux4)
    thus " ¬Af(j)"
      proof (rule disjE)
      {assume "¬Af(j)"
        thus  "¬Af(j)" by this}
      next
      {assume 6: "¬ E(a)"
        show "¬ Af(j)" using 6 3 by (rule notE)}
      qed}
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Formalizar, y decidir la corrección, del siguiente
  argumento 
     El esposo de la hermana de Toni es Roberto. La hermana de Toni es
     María. Por tanto, el esposo de María es Roberto. 
  Usar e(x) para el esposo de x
       h    para la hermana de Toni
       m    para María
       r    para Roberto
  ------------------------------------------------------------------ *}

(* ivamenjim *)

lemma ejercicio_5:
  assumes 1: "e(h) = r" 
  assumes 2: "h = m"
  shows "e(m) = r"   
proof -
  have 3: "e(h) = e(m)" using 2 by (rule arg_cong)
  have 4: "e(m) = e(h)" using 3 by (rule sym)
  then show "e(m) = r" using 1 by (rule trans)
qed

(* danrodcha anaprarod crigomgom ferrenseg marcarmor13*)
lemma ej_5:
  assumes "e(h) = r" and
          "h = m"
  shows   "e(m) = r"
  proof -
    show "e(m) = r" using assms(2) assms(1) by (rule subst)
qed

end