Relación 11

header {* R11: Deducción natural de primer orden *}

theory R11
imports Main 
begin

text {*
  Demostrar o refutar los siguientes lemas usando sólo las reglas
  básicas de deducción natural de la lógica proposicional, de los
  cuantificadores y de la igualdad: 
  · 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 y not_ex 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

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x 
  ------------------------------------------------------------------ *}

-- "maresccas4 irealetei" (* Una! nos ha salido Una!!! *)
lemma ej_1_auto:
  assumes " P a ⟶ (∃x. Q x)"
  shows "∃x. P a ⟶ Q x"
using assms by auto

lemma ej_1:
  fixes P Q :: "'b ⇒ bool" 
  assumes 0:"P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
  have "¬(P a) ∨ P a" by (rule excluded_middle)
  then show "∃x. P a ⟶ Q x"
  proof (rule disjE)
      {assume 2:"(P a)"
        have 4: "∃x. Q x" using 0 2 ..
        obtain b where "Q b" using 4 by (rule exE)
        then have "P a ⟶ Q b" ..
        then show "∃x. P a ⟶ Q x" by (rule exI)}
      next 
       {assume 2:"¬(P a)"
        {assume "¬(∃x. P a ⟶ Q x)"
         then have 3: "∀x. ¬(P a ⟶ Q x)" by (rule no_ex)
         fix b
         have "¬(P a ⟶ Q b)" using 3 ..
         then have "P a ∧ ¬Q b" by (rule Meson.not_impD)
         then have 4:"P a" ..
         have "False" using 2 4 ..}
        then show " ∃x. P a ⟶ Q x" by (rule ccontr)}
       qed
qed






-- "marescpla"
 lemma 1:
      assumes "P a ⟶ (∃x. Q x)"
      shows "∃x. P a ⟶ Q x"
  proof (rule disjE)
   show 0: "¬ P a ∨ P a" by (rule excluded_middle)
   next
   show "¬ P a ⟹(∃ x. P a ⟶ Q x)"
      proof-
        assume H2: "¬ P a"
        then show "∃x. P a ⟶ Q x"
        proof-
            {assume 1: "P a"
              have "Q b" using H2 1 by (rule notE)
              hence "Q b" .}
            hence "P a ⟶ Q b" .. 
            hence II: "∃x. P a ⟶ Q x" by (rule exI)
            hence "¬ P a ⟶ (∃x. P a ⟶ Q x)" ..
            thus "¬ P a ⟹ (∃x. P a ⟶ Q x)" ..
        qed
        next
        qed
   assume H1: "P a"
   then show "P a ⟹ ∃x. P a ⟶ Q x"
      proof-
        have "P a" using H1 .
        with assms(1) have 2: "∃x. Q x" ..
        obtain b where "Q b" using 2 ..
        then have H1:"P a ⟶ Q b" ..
        then have I: "∃x. P a ⟶ Q x" by (rule exI)
        then show "P a ⟹ ∃x. P a ⟶ Q x" .
      qed
  qed
  

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
       {∀x y z. R x y ∧ R y z ⟶ R x z, 
        ∀x. ¬(R x x)}
       ⊢ ∀x y. R x y ⟶ ¬(R y x)
  ------------------------------------------------------------------ *}

-- "irealetei maresccas4 pabflomar" (* Dos *)

lemma ej_2:
  assumes "∀x. ∀y. ∀z. R x y ∧ R y z ⟶ R x z"
          "∀x. ¬(R x x)"
  shows "∀x. ∀y. R x y ⟶ ¬(R y x)"
proof -
  {fix a
  {fix b
  {assume 1:"R a b"
  have  "¬(R b a)"
  proof (rule ccontr)
    assume "¬¬(R b a)"
    then have "R b a" by (rule notnotD)
    with 1 have 3:"R a b ∧ R b a" ..
    have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) ..
    then have "∀z. R a b ∧ R b z ⟶ R a z" ..
    then have "R a b ∧ R b a ⟶ R a a" ..
    then have "R a a" using 3 ..
    have "¬(R a a)" using assms(2) ..
    then show False using `R a a`..
  qed}
  then have 4:"R a b ⟶ ¬(R b a)" ..}
  then have "∀y. R a y ⟶ ¬ R y a" ..}
  then show "∀x y. R x y ⟶ ¬ R y x" ..
qed




-- "marescpla"
 lemma 2:
  assumes   "∀x. ∀y. ∀z. R x y ∧ R y z ⟶ R x z"
            "∀x. ¬(R x x)"
  shows "∀x. ∀y. R x y ⟶ ¬(R y x)"
  proof-
     {fix a 
     have 1: "∀y.∀z. R a y ∧ R y z ⟶ R a z" using assms(1) ..    
       {fix b
         have "∀z. R a b ∧ R b z ⟶ R a z" using 1 ..
         hence 2: "R a b ∧ R b a ⟶ R a a" ..
         {assume 1: "R a b"
           have 3: "¬ R a a" using assms(2) ..
           have 4: "¬(R b a) ∨ (R b a)" by (rule excluded_middle)
           {assume "R b a"
             with 1 have "R a b ∧ R b a" by (rule conjI)
             with 2 have "R a a" ..
             with 3 have "False" by (rule notE)
             then have "¬(R b a)"..}
           then have 5: "R b a ⟹ ¬(R b a)"..
           {assume "¬(R b a)"
             then have "¬(R b a)" .}
           with 4 have "¬(R b a)" using 5 ..}         
           then have 6: "R a b ⟶ ¬(R b a)" ..}
         then have "∀y. R a y ⟶ ¬(R y a)" ..}
         then show "∀x. ∀y. R x y ⟶ ¬(R y x)" ..
         qed
     
  text{*maerscpla: He tenido que alargar un poco más la demostración porque no sé
  por qué no me reconocía que "¬(R b a) ∨ (R b a)" y "R b a ⟹ False" ⟹ ¬(R b a)*}
  

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar o refutar
       (∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
  ------------------------------------------------------------------ *}
-- "irealetei maresccas4 domlloriv pabflomar jaisalmen zoiruicha marescpla"
lemma ej_3_auto:
  assumes "∀x. ∃y. P x y"
  shows "∃y. ∀x. P x y"
quickcheck
oops

(*Contra ejemplo
P = (λx. undefined)(a⇣1 := {a⇣2}, a⇣2 := {a⇣1})
*)

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar o refutar
       (∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
  ------------------------------------------------------------------ *}

-- "irealetei maresccas4 domlloriv"
lemma ej_4_auto:
  assumes "∃y. ∀x. P x y"
  shows "∀x. ∃y. P x y" 
using assms by auto

lemma ej_4:
  assumes 1:"∃y. ∀x. P x y"
  shows "∀x. ∃y. P x y" 
proof -
  {fix a
  obtain b where 2:"∀x. P x b" using 1 ..
  have "P a b" using 2 ..
  then have "∃y. P a y"  ..}
  then show "∀x. ∃y. P x y" ..
qed

lemma ej_4_bis:"(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)" 
proof 
  assume 1:"∃y. ∀x. P x y"
  {fix a
  obtain b where 2:"∀x. P x b" using 1 ..
  have "P a b" using 2 ..
  then have "∃y. P a y"  ..}
  then show "∀x. ∃y. P x y" ..
qed



-- "marescpla"
  lemma 4:
    "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
      proof 
      assume 1: "∃y. ∀x. P x y"
      obtain b  where 2:" ∀x. P x b" using 1 ..
      {fix a
        have "P a b" using 2 ..
        then have "∃y. P a y" ..}
      then show "∀x. ∃y. P x y" ..
      qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar o refutar
     {∀x. P a x x, 
      ∀x y z. P x y z ⟶ P (f x) y (f z)⟧
     ⊢ ∃z. P (f a) z (f (f a))
  ------------------------------------------------------------------ *}

-- "maresccas4, marescpla: Yo lo tengo sin rallita despues del proof y saltandome el ultimo paso, pero es lo mismo."
lemma ej_5:
  assumes "∀x. P a x x"
          "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof -
  have "P a (f a) (f a)" using assms(1) ..
  have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) ..
  then have "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
  then have "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
  then have "P (f a) (f a) (f (f a))" using `P a (f a) (f a)` ..
  then show "∃z. P (f a) z (f (f a))" ..
qed

-- "irealetei"
lemma ej_5_auto:
  assumes "∀x. P a x x"
  assumes "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
using assms by meson

lemma ej_5:
  assumes 1:"∀x. P a x x"
  assumes 2:"∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof -
  have 3:"P a (f a) (f a)" using 1 ..
  have  "∀y z. P a y z ⟶ P (f a) y (f z)" using 2 ..
  then have  "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)"  ..
  then have  4:" P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
  have 5:"P (f a) (f a) (f (f a))" using 4 3 by (rule mp)
  then show "∃z. P (f a) z (f (f a))" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar
     {∀y. Q a y, 
      ∀x y. Q x y ⟶ Q (s x) (s y)} 
     ⊢ ∃z. Qa z ∧ Q z (s (s a))
  ------------------------------------------------------------------ *}

-- "maresccas4, marescpla"
lemma ej_6:
  assumes "∀y. Q a y"
          "∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
proof -
  have "Q a (s a)" using assms(1) ..
  have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) ..
  then have "Q a (s a) ⟶ Q (s a) (s (s a))" ..
  then have "Q (s a) (s (s a))" using `Q a (s a)` ..
  with  `Q a (s a)` have "Q a (s a) ∧ Q (s a) (s (s a))"  by (rule conjI)
  then show "∃z. Q a z ∧ Q z (s (s a))" ..
qed

-- "irealetei"
lemma ej_6_auto:
  assumes "∀y. Q a y"
  assumes "∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
using assms by meson

lemma ej_6:
  assumes 1:"∀y. Q a y"
  assumes 2:"∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
proof
  have 3:"Q a (s a)" using 1 ..
  have "∀y. Q a y ⟶ Q (s a) (s y)" using 2 ..
  then have "Q a (s a) ⟶ Q (s a) (s (s a))" ..
  then have 4:"Q (s a) (s (s a))" using 3  by (rule mp)
  show "Q a (s a) ∧ Q (s a) (s (s a))" using 3 4 by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. (En APLI2 el ejercicio 13 de LP) 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.
       Or : Se aceptan órdenes del operador.
  ------------------------------------------------------------------ *}

-- "pabflomar maresccas4 domlloriv"

lemma ej7_pfm:
  assumes 1: "A ∨ P ⟶ R ∧ F" and
          2: "(F ∨ N) ⟶ Or"
 shows "A ⟶ Or"
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: "Or" using 2 7 by (rule mp)}
  then show "A ⟶ Or" ..
qed

-- "irealetei"
lemma ej_7_auto:
  assumes "A ∨ P ⟶ R ∧ F"
  assumes "F ∨ N ⟶ Or"
  shows "A ⟶ Or"
using assms by auto

lemma ej_7:
  assumes 1:"A ∨ P ⟶ R ∧ F"
  assumes 2:"F ∨ N ⟶ Or"
  shows "A ⟶ Or"
proof 
    assume "A"
    then have 3:"A ∨ P" ..
    have "R ∧ F" using 1 3 by (rule mp)
    then have "F" ..
    then have 4:"F ∨ N" ..
    show "Or" using 2 4 by (rule mp)
qed 

-- "marescpla"
 lemma 7:
 assumes "A ∨ P ⟶ R ∧ F "
          "(F ∨ N) ⟶ Or "
    shows "A ⟶ Or"
    proof (rule ccontr)
    assume "¬ (A ⟶ Or)"
    then have 1:"A ∧ ¬ Or" by simp
    then have 2: "¬ Or" ..
    have "A"using 1 by (rule conjunct1)
    then have "A ∨ P" by (rule disjI1)
    with assms(1) have "R ∧ F" by (rule mp)
    then have "F" ..
    hence "F ∨ N" ..
    with assms(2) have "Or" ..
    with 2 show "False" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 8. (En APLI2 el ejercicio 5 de LP) Formalizar, y demostrar
  la corrección, del siguiente argumento 
     En cierto experimento, cuando hemos empleado un fármaco A, el
     paciente ha mejorado considerablemente en el caso, y sólo en el
     caso, en que no se haya empleado también un fármaco B. Además, o se
     ha empleado el fármaco A o se ha empleado el fármaco B. En
     consecuencia, podemos afirmar que si no hemos empleado el fármaco
     B, el paciente ha mejorado considerablemente. 
  Usar A: Hemos empleado el fármaco A.
       B: Hemos empleado el fármaco B.
       M: El paciente ha mejorado notablemente.
  ------------------------------------------------------------------ *}
-- "pabflomar" 

lemma ej8_pfm:
  assumes  "A ⟶ (M ⟷ ¬B)" 
          "A ∨ B"
 shows "¬B ⟶ M"

proof (rule disjE)
  show "A ∨ B" using assms(2) by simp
  next
  { assume "A"
    with assms(1) have "M ⟷ ¬B"  by (rule mp)
    then show "¬B ⟶ M" using assms by simp}
  next
  { assume 1:"B"
    {assume 2:"¬B"
      then have "M" using 1 by (rule notE)}
      then show "¬B ⟶ M" by (rule impI)
 }
qed

-- "maresccas4 irealetei domlloriv"
lemma ej_8:
  assumes "(A ⟶ M) ⟷ ¬B"
          "A ∨ B"
  shows "¬B ⟶ M"
using assms(2)
proof
  { assume "A"
    { assume "¬B"
      have "¬B ⟶ (A ⟶ M)" using assms(1) ..
      then have "A ⟶ M" using `¬B` ..
      then have "M" using `A` .. }
    then show "¬B ⟶ M" ..
  }
next
  { assume "B"
    { assume "¬B"
      then have False using `B` ..
      then have "M" .. }
    then show "¬B ⟶ M" ..
  }
qed



-- "marescpla"
 lemma 8:
  assumes  "A ⟶ (M ⟷ ¬B)"
           "A ∨ B"
 shows "¬B ⟶ M"
proof (rule disjE)
  show "A ∨ B" using assms(2) .
  next
  assume "A"
    with assms(1) have 1: "M ⟷ ¬B"  by (rule mp)
    then show "¬B ⟶ M" ..
  next
  assume 1:"B"
    {assume 2:"¬B"
      then have "M" using 1 by (rule notE)}
      then show "¬B ⟶ M" by (rule impI)
  next
qed


text {* --------------------------------------------------------------- 
  Ejercicio 9. (En APLI2 el ejercicio 13 de LPO) Formalizar, y decidir
  la corrección, del siguiente argumento 
     Toda persona pobre tiene un padre rico. Por tanto, existe una
     persona rica que tiene un abuelo rico.
  Usar R(x) para x es rico
       p(x) para el padre de x
  ------------------------------------------------------------------ *}
-- "julrobrel "
lemma apli2_ej13_lpo:
    assumes "∀ x. ¬R(x) ⟶ R(p(x))"
      shows "∃ x. R(x) ∧ R(p(p(x)))"
using assms
by auto

lemma apli2_ej13_lpo_d:
    assumes 0:"∀ x. ¬R(x) ⟶ R(p(x))"
      shows "∃ x. R(x) ∧ R(p(p(x)))"
oops

-- "irealetei"
lemma ej_9_auto:
  assumes "∀x. ¬R(x)⟶R(p(x))"
  shows "∃y. R(y) ⟶ R(p(p(y)))"
using assms by auto

-- "maresccas4"
lemma ej_9:
  assumes "∀x. ¬R x ⟶ R (p x)"
  shows "∃x. R x ∧ R(p (p x))"
proof -
  have "¬(∃x. ¬R(p x)) ∨ (∃x. ¬R(p x))" by (rule excluded_middle)
  then show "∃x. R x ∧ R(p (p x))"
  proof (rule disjE)
    assume "¬(∃x. ¬R(p x))"
    then have 1:"∀x. ¬¬R(p x)" by (rule no_ex)
    {fix a
      have "¬¬R(p a)" using 1 ..
      then have "R(p a)" by (rule notnotD)}
    then have 2:"∀x. R(p x)" ..
    {fix a
      have 3:"R(p a)" using 2 ..
      have 4:"R(p (p (p a)))" using 2 ..
      have "R(p a) ∧ R(p (p (p a)))" using 3 4 ..}
    then show "∃x. R x ∧ R(p (p x))" ..
  next
    assume "∃x. ¬R(p x)"
    obtain a where 1:"¬R(p a)" using `∃x. ¬R(p x)` ..
    have "¬R(p a) ⟶ R(p (p a))" using assms ..
    then have 2:"R(p (p a))" using 1 ..
    have "¬R a ⟶ R(p a)" using assms ..
    then have "¬¬R a" using 1 by (rule mt)
    then have 3:"R a" by (rule notnotD)
    then have  "R a ∧ R(p (p a))" using 2 by (rule conjI)
    then show "∃x. R x ∧ R(p (p x))" ..
  qed
qed



-- "marescpla"
lemma 9:
     assumes  "∀x. ¬ R x ⟶ R(p(x)) "
     shows "∃x. R x ∧ R(p(p(x)))"
   proof (rule disjE)
     fix a
     show "¬ R(p(a)) ∨ R(p(a))" by (rule excluded_middle)
     next
     fix a
     have 1:"¬ R a ⟶ R(p(a))" using assms ..
     {assume 2: "¬ R(p(a))"
        with 1 have "¬ ¬ R a" by (rule mt)
        hence 3: "R a" by (rule notnotD)
        have "R(p(p(a)))" using assms 2  by simp
        with 3 have "R a ∧ R(p(p(a)))" by (rule conjI)
        then show "∃x. R x ∧ R(p(p(x)))" by (rule exI)}
     next
     fix a
     {assume "R(p(a))"
        then show "∃x. R x ∧ R (p (p x))" using assms by auto}
     next
     qed

text{* marescpla: Ya he visto y entendido el ejercicio de Marco y se 
donde tengo el fallo jeje, pero bueno, yo subo como lo tenía, que es
lo que realmente había hecho por mi misma *}


text {* --------------------------------------------------------------- 
  Ejercicio 10. (En APLI2 el ejercicio 10 de LPO) 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
  ------------------------------------------------------------------ *}
-- "julrobrel"
lemma apli2_ej10_lpo:
    assumes "∀ x. Af(x) ⟶ (∀ y. E(y) ⟶ Ap(x,y))"
            "∀ y. E(y) ⟶ ¬ Ap(j,y)"
      shows "∃ y. E(y) ∧ N(y) ⟶ ¬Af(j)"
using assms
by auto

lemma apli2_ej10_lpo_d:
    assumes 0:"∀ x. Af(x) ⟶ (∀ y. E(y) ⟶ Ap(x,y))"
        and 1:"∀ y. E(y) ⟶ ¬ Ap(j,y)"
      shows "∃ y. E(y) ∧ N(y) ⟶ ¬Af(j)"
oops

-- "irealetei"
lemma ej_10_auto:
  assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x, y)"
  assumes "∀y. E(y) ⟶ ¬Ap(j,y)"
  shows "∃y. N(y) ∧ E(y) ⟶ ¬Af(j)"
using assms by auto

-- "maresccas4"
lemma ej_10:
  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 -
  { fix a
    { assume 1:"E(a) ∧ N(a)"
      have "¬Af(j)"
      proof
        assume "Af(j)"
        have "E(a)" using 1 ..
        have 2:"Af(j) ∧ E(a)" using `Af(j)` `E(a)` ..
        have "∀x. Af(j) ∧ E(x) ⟶ Ap(j, x)" using assms(1) ..
        then have "Af(j) ∧ E(a) ⟶ Ap(j, a)" ..
        then have a:"Ap(j, a)" using 2 ..
        have "E(a) ⟶ ¬Ap(j, a)" using assms(2) ..
        then have "¬Ap(j, a)" using `E(a)` ..
        then show "False" using a ..
      qed}
    then have "E(a) ∧ N(a) ⟶ ¬Af(j)" ..}
  then show "∃x. E(x) ∧ N(x) ⟶ ¬Af(j)" ..
qed
-- pabflomar --

lemma ej10_pfm:
  assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x,y)"
          "∀x. E(x) ⟶ ¬Ap(j,x)"
  shows "∀x. E(x) ∧ N(x)  ⟶ ¬Af(j)"
using assms by auto

  
--"maerescpla" --
lemma 10:
  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-
  {fix a
    {assume 1: "E(a) ∧ N(a)"
      then have 2: "E(a)" by (rule conjunct1)
      have "E(a) ⟶ ¬Ap(j, a)" using assms(2)..
      hence 3: "¬Ap(j, a)" using 2 by (rule mp)
      have "∀y. (Af(j) ∧ E(y)) ⟶ Ap(j, y)" using assms(1) ..
      hence "(Af(j) ∧ E(a)) ⟶ Ap(j, a)" ..
      then have "¬(Af(j) ∧ E(a))" using 3 by (rule mt)
      hence "¬Af(j) ∨ ¬E(a)" by simp
      with 2 have "¬Af(j)" by simp}
    then have "E(a) ∧ N(a) ⟹ ¬Af(j)".}
  then show "∃x. E(x) ∧ N(x) ⟶ ¬Af(j)" by simp
  qed


text {* --------------------------------------------------------------- 
  Ejercicio 11. Formalizar, y decidir la corrección, del siguiente
  argumento
     Ningún socio del club está en deuda con el tesorero del club. Si
     un socio del club no paga su cuota está en deuda con el tesorero
     del club. Por tanto, si el tesorero del club es socio del club,
     entonces paga su cuota. 
  Usar P(x) para x es socio del club
       Q(x) para x paga su cuota
       R(x) para x está en deuda con el tesorero
       a    para el tesorero del club
   ------------------------------------------------------------------ *}

-- "julrobrel"
lemma apli2_ej24_lpo:
  assumes "¬ (∃ x. P(x) ∧ R(x))"
          "∀ x. P(x) ∧ ¬ Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
using assms
by auto

-- "julrobrel"
lemma apli2_ej24_lpo_d:
  assumes 0:"¬ (∃ x. P(x) ∧ R(x))"
      and 1:"∀ x. P(x) ∧ ¬ Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
oops

-- "julrobrel: cuatro sencillos lemas, aunque no faciles de demostrar, y al final el principal"

--"julrobrel: es el modus tollens(mt)"
lemma apli2_ej24_lpo_d_aux1:
  assumes 0:"p ∧ ¬q ⟶ r"
  shows   "¬r⟶¬p ∨ q"
using assms
by auto

lemma modus_tollens:
  assumes 1:"p ⟶ q"
      and 2:"¬q"
    shows   "¬p"
proof -
  {assume 3:"p"
   have   4:"q" using 1 3 by (rule mp)
   have   5:"False" using 2 4 by (rule notE)}
  thus "¬p" ..
qed

lemma modus_tollens2:
  assumes 1:"p ⟶ q"
    shows   "¬q ⟶ ¬p"
proof -
  {assume 2:"¬q"
  have 3:"¬p" using 1 2 by (rule modus_tollens)}
  thus 4:"¬q ⟶ ¬p" by (rule impI)
qed

lemma apli2_ej24_lpo_d_aux1_detalle:
  assumes 0:"p ∧ ¬q ⟶ r"
  shows   "¬r⟶¬p ∨ q"
proof -
  have 1:"(p ∧ ¬q) ⟶ r" using 0 .
  have 2:"¬r ⟶ ¬(p ∧ ¬q)" using 1 by (rule modus_tollens2)
  thus 3:"¬r ⟶ ¬p ∨ q" using 2 by auto (* cada vez estan saliendo mas demostraciones. Aqui hay que demostrar ¬(p ∧ ¬q) = ¬p ∨ q *)
qed

-- "julrobrel"
lemma apli2_ej24_lpo_d_aux2:
  assumes 0:"¬(p ∧ r)"
  shows   "p ⟶ ¬r"
using assms
by auto

--"julrobrel: este lema debe de tener un nombre..."
--"julrobrel: ya he encontrado como se llama: Hypothetical Syllogism (HS)"
lemma apli2_ej24_lpo_d_aux3:
  assumes "(p ⟶ q) ∧ (q ⟶ r)"
  shows   "p ⟶ r"
using assms
by auto

--"julrobrel"
lemma apli2_ej24_lpo_d_aux3_detalle:
  assumes 0:"(p ⟶ q) ∧ (q ⟶ r)"
  shows   "p ⟶ r"
proof -
  have 1:"p⟶q" using 0 by (rule conjunct1)
  have 2:"q⟶r" using 0 by (rule conjunct2)
  {assume 3:"p"
   have 4:"q" using 1 3 by (rule mp)
   have 5:"r" using 2 4 by (rule mp)}
  thus 6:"p⟶r" by (rule impI)
qed

-- "julrobrel"
lemma apli2_ej24_lpo_d_aux4:
  assumes 0:"p⟶(¬p ∨ q)"
  shows   "p ⟶ q"
using assms
by auto

-- "julrobrel"
lemma apli2_ej24_lpo_d:
  assumes 0:"¬ (∃ x. P(x) ∧ R(x))"
      and 1:"∀ x. P(x) ∧ ¬ Q(x) ⟶ R(x)"
    shows   "P(a)⟶Q(a)"
proof -
  have 2:"∀ x. ¬(P(x) ∧ R(x))" using 0 by (rule no_ex)
  fix a
  have 3:"¬(P(a) ∧ R(a))" using 2 ..
  have 4:"P(a) ∧ ¬ Q(a) ⟶ R(a)" using 1 ..
  have 5:"¬R(a) ⟶ ¬ P(a) ∨ Q(a)" using 4 by (rule apli2_ej24_lpo_d_aux1)
  have 6:"P(a)⟶¬R(a)" using 3 by (rule apli2_ej24_lpo_d_aux2)
  have 7:"(P(a)⟶¬R(a)) ∧ (¬R(a) ⟶ ¬P(a) ∨ Q(a))" using 6 5 by (rule conjI)
  have 8:"P(a)⟶(¬P(a) ∨ Q(a))" using 7 by (rule apli2_ej24_lpo_d_aux3)
  have 9:"P(a)⟶Q(a)" using 8 by (rule apli2_ej24_lpo_d_aux4)
  show "P(a)⟶Q(a)" using 9 .
qed


-- "irealetei"
lemma ej_11_auto:
  assumes "∀x. P(x) ⟶ ¬R(x)"
  assumes "∀y. P(y) ∧ ¬Q(y) ⟶ R(y)"
  shows "P(a) ⟶ Q(a)"
using assms by auto

lemma ej_11_irealetei:
  assumes 1:"∀x. P(x) ⟶ ¬R(x)"
  assumes 2:"∀y. P(y) ∧ ¬Q(y) ⟶ R(y)"
  shows "P(a) ⟶ Q(a)"
proof -
  {
   fix a
   assume 3:"P(a)"
   have "Q(a)" 
   proof (rule ccontr) 
     assume 4:"¬Q(a)"
     have 5:"P(a) ∧ ¬Q(a)" using 3 4 ..
     have "P(a) ∧ ¬Q(a) ⟶ R(a)" using 2 ..
     then have 6:"R(a)" using 5 by (rule mp)
     have "P(a) ⟶ ¬R(a)" using 1 ..
     then have "¬R(a)" using 3 by (rule mp)
     then show "False" using 6 ..
   qed}
then show "P (a) ⟶ Q (a)" ..
qed

-- "maresccas4"
lemma ej_11:
  assumes "∀x. P(x) ⟶ ¬R(x)"
          "∀x. (P(x) ∧ ¬Q(x)) ⟶ R(x)"
  shows "P(a) ⟶ Q(a)"
proof -
  {assume "P(a)"
  have "Q(a)"
  proof (rule ccontr)
    assume "¬Q(a)"
    have 1:"P(a) ∧ ¬Q(a)" using `P(a)` `¬Q(a)` ..
    have "P(a) ∧ ¬Q(a) ⟶ R(a)" using assms(2) ..
    then have a:"R(a)" using 1 ..
    have "P(a) ⟶ ¬R(a)" using assms(1) ..
    then have "¬R(a)" using `P(a)` ..
    then show "False" using a ..
  qed}
  then show "P(a) ⟶ Q(a)" ..
qed

 
-- "marescpla"
lemma 11:
  assumes "∀x. P(x) ⟶ ¬R(x)"
          "∀x. (P(x) ∧ ¬Q(x)) ⟶ R(x)"
  shows "P(a) ⟶ Q(a)"
  proof
  fix a
  assume 1: "P(a)"
  have "P(a) ⟶ ¬R(a)" using assms(1)..
  hence 2:"¬R(a)" using 1 ..
  have "(P(a) ∧ ¬Q(a)) ⟶ R(a)" using assms(2)..
  then have "¬(P(a) ∧ ¬Q(a))" using 2 by (rule mt)
  then have "¬P(a) ∨ ¬ ¬Q(a)" by simp
  then show "Q(a)"
  proof
    {assume "¬P(a)"
      hence "False" using 1 ..
      then show "Q(a)" ..}
    next
    {assume "¬¬Q(a)"
      then show "Q(a)" by (rule notnotD)}
    next
    qed
  qed


end