Relación 7

chapter {* R7: Deducción natural de primer orden *}

theory R7_Deduccion_natural_de_primer_orden_alu
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 
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes "P a ⟶ (∃x. Q x)"
  shows "∃x. P a ⟶ Q x"
proof (rule ccontr)
  assume "∄x. P a ⟶ Q x"
  have "P a ⟶ (∃x. P a ⟶ Q x)"
  proof
    assume "P a"
    with assms have "∃x. Q x" by (rule mp)
    moreover have "⋀x. Q x ⟹ ∃x'. P a ⟶ Q x'"
    proof -
      fix x
      assume "Q x"
      hence "P a ⟶ Q x" by (rule impI)
      thus "∃x'. P a ⟶ Q x'" by (rule exI)
    qed
    ultimately show "∃x. P a ⟶ Q x" by (rule exE)
  qed
  moreover note `∄x. P a ⟶ Q x`
  ultimately have "¬(P a)" by (rule mt)
  have "¬(P a) ⟶ (∃x. P a ⟶ Q x)"
  proof 
    fix x
    assume "¬(P a)"
    have "P a ⟶ Q x"
    proof
      assume "P a"
      with `¬(P a)` have "False" by (rule notE)
      thus "Q x" by (rule FalseE)
    qed
    thus "∃x. P a ⟶ Q x" by (rule exI)
  qed
  moreover note `∄x. P a ⟶ Q x`
  ultimately have "¬¬(P a)" by (rule mt)
  moreover note `¬(P a)`
  ultimately show "False" by (rule notE)
qed

(* alfmarcua *)
lemma ejercicio_52:
  "p ∨ ¬p"
proof (rule ccontr)
  assume 1: "¬(p ∨ ¬p)"
  have 2: "¬p" proof (rule notI)
    assume p hence 3: "p ∨ ¬p" by (rule disjI1)
    show "False" using 1 3 by (rule notE)
  qed
  have 4: "p ∨ ¬p" using 2 by (rule disjI2)
  show "False" using 1 4 by (rule notE)
qed

lemma ejercicio_1:
  assumes "P a ⟶ (∃x. Q x)"
  shows "∃x. P a ⟶ Q x"
proof (rule disjE)
  show "P a ∨ ¬ P a" by (rule ejercicio_52)
next
  assume "P a"
  have "∃x. Q x" using assms `P a` by (rule mp)
  then obtain b where "Q b" by (rule exE)
  have "P a ⟹ Q b" using `P a` `Q b` by simp
  have "P a ⟶ Q b" using `P a ⟹ Q b` by (rule impI)
  then show "∃x. P a ⟶ Q x" by (rule exI)
next
  assume "¬ P a"
  fix b
  have "P a ⟶ Q b"
  proof (rule impI)
    assume "P a"
    with `¬(P a)` have "False" by (rule notE)
    then show "Q b" by (rule FalseE)
  qed
  thus "∃x. P a ⟶ Q x" by (rule exI)
qed

(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2
   hugrubsan pabbergue enrparalv giafus1 antramhur *) 
lemma ejercicio_1b:
  assumes "P a ⟶ (∃x. Q x)"
  shows "∃x. P a ⟶ Q x"
proof (rule disjE)
  show "¬P a ∨ P a" by (rule excluded_middle)
next
  fix b
  assume 3: "¬P a"
  have "P a ⟶ Q b" proof (rule impI)
    assume 4: "P a" show "Q b" using 3 4 by (rule notE)
  qed
  thus ?thesis by (rule exI)
next
  assume 1: "P a"
  have "∃x. Q x" using assms(1) 1 by (rule mp)
  then obtain b where 2: "Q b" by (rule exE)
  have "P a ⟶ Q b" proof (rule impI)
    assume "P a" show "Q b" using 2 .
  qed
  thus ?thesis by (rule exI)
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)
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes A1: "∀x y z. R x y ∧ R y z ⟶ R x z"
    and A2: "∀x. ¬(R x x)"
  shows "∀x y. R x y ⟶ ¬(R y x)"
proof -
  {
    fix x y
    {
      assume "R x y"
      have "¬ (R y x)"
      proof (rule ccontr)
        assume "¬ ¬ (R y x)"
        hence "R y x" by (rule notnotD)

        note `∀x y z. R x y ∧ R y z ⟶ R x z`
        moreover have "∀ y z. R x y ∧ R y z ⟶ R x z ⟹ False"
        proof -
          assume "∀ y z. R x y ∧ R y z ⟶ R x z"
          moreover have "∀ z. R x y ∧ R y z ⟶ R x z ⟹ False"
          proof -
            assume "∀ z. R x y ∧ R y z ⟶ R x z"
            moreover have "R x y ∧ R y x ⟶ R x x ⟹ False"
            proof -
              assume "R x y ∧ R y x ⟶ R x x"
              moreover {
                note `R x y`
                moreover note `R y x`
                ultimately have "R x y ∧ R y x" by (rule conjI)
              }
              ultimately have "R x x" by (rule mp)

              note `∀x. ¬(R x x)`
              moreover {
                assume "¬(R x x)"
                moreover note `R x x`
                ultimately have "False" by (rule notE)
              }
              ultimately show "False" by (rule allE)
            qed
            ultimately show "False" by (rule allE)
          qed
          ultimately show "False" by (rule allE)
        qed
        ultimately show "False" by (rule allE)
      qed
    }
    hence "R x y ⟶ ¬ (R y x)" by (rule impI)
  }
  hence "⋀x. ∀y. R x y ⟶ ¬ (R y x)" by (rule allI)
  thus ?thesis by (rule allI)
qed

(* alfmarcua marfruman1 enrparalv*)
lemma ejercicio_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 (rule allI)
  fix a
  show "∀y. R a y ⟶ ¬ R y a"
  proof (rule allI, rule impI)
    fix b
    assume "R a b"
    show "¬ R b a"
    proof (rule notI)
      assume "R b a"
      have "R a b ∧ R b a" using `R a b` `R b a` by (rule conjI)
      have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
      then have "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
      then have "R a b ∧ R b a ⟶ R a a" by (rule allE)
      then have "R a a" using `R a b ∧ R b a` by (rule mp)
      have "¬ (R a a)" using assms(2) by (rule allE)
      then show False using `R a a` by (rule notE)
    qed
  qed
qed


(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan
   pabbergue giafus1 antramhur *) 
lemma ejercicio_2b:
  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 (rule allI)
  fix a
  show "∀y. R a y ⟶ ¬(R y a)"
  proof (rule allI)
    fix b
    have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
    hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
    hence 1: "R a b ∧ R b a ⟶ R a a" by (rule allE)
    have 2: "¬(R a a)" using assms(2) by (rule allE)
    show "R a b ⟶ ¬(R b a)" proof (rule impI)
      assume 3: "R a b"
      show "¬(R b a)"
      proof (rule ccontr)
        assume "¬¬R b a"
        hence 4: "R b a" by (rule notnotD)
        have 5: "R a b ∧ R b a" using 3 4 by (rule conjI)
        have 6: "R a a" using 1 5 by (rule mp)
        show False using 2 6 by (rule notE)
      qed
    qed
  qed
qed

(* pabalagon *)
lemma ejercicio_2_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
      have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
      hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
      hence 1: "R a b ∧ R b a ⟶ R a a" by (rule allE)
      have 2: "¬(R a a)" using assms(2) by (rule allE)
      have "R a b ⟶ ¬(R b a)" proof (rule impI)
        assume 3: "R a b"
        show "¬(R b a)"
        proof (rule ccontr)
          assume "¬¬R b a"
          hence 4: "R b a" by (rule notnotD)
          have 5: "R a b ∧ R b a" using 3 4 by (rule conjI)
          have 6: "R a a" using 1 5 by (rule mp)
          show False using 2 6 by (rule notE)
        qed
      qed}
    hence "∀y. R a y ⟶ ¬(R y a)" by (rule allI)}
  thus "∀x y. R x y ⟶ ¬(R y x)" by (rule allI)
qed

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

(* benber pabbergue*)
(* No es cierto si el universo consiste en más que un objeto. En ese
   caso, asignar la igualdad (=) a P es un contraejemplo. *)

(* alfmarcua marfruman1 raffergon2 enrparalv*)
lemma ejercicio_3:
  "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
  quickcheck
  oops

(* pabalagon manperjim pabbergue josgomrom4 gleherlop hugrubsan giafus1
   antramhur *) 
text{*
  Contraejemplo en los naturales, para todo x existe y tal que x < y, pero no
  existe y tal que para todo x, x < y
*}
lemma ejercicio_3: "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
  quickcheck
  oops

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

(* benber *)
lemma "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof
  assume "∃y. ∀x. P x y"
  moreover have "⋀y. ∀x. P x y ⟹ ∀x. ∃y'. P x y'"
  proof
    fix x y
    assume "∀x'. P x' y"
    hence "P x y" by (rule allE)
    thus "∃y'. P x y'" by (rule exI)
  qed
  ultimately show "∀x. ∃y. P x y" by (rule exE)
qed

(* alfmarcua marfruman1 raffergon2 enrparalv *)
lemma ejercicio_4: 
  "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof (rule impI, rule allI)
  fix a
  assume "∃y. ∀x. P x y"
  then obtain b where "∀x. P x b" by (rule exE)
  then have "P a b" by (rule allE)
  then show "∃y. P a y" by (rule exI)
qed

(* pabalagon manperjim josgomrom4 gleherlop hugrubsan pabbergue
   antramhur *) 
lemma ejercicio_4_2: "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof (rule impI)
  assume "∃y. ∀x. P x y"
  moreover have "⋀y. ∀x. P x y ⟹ ∀x. ∃y. P x y"
  proof
    fix x0 y0
    assume "∀x. P x y0"
    hence "P x0 y0" by (rule allE)
    thus "∃y. P x0 y" by (rule exI)
  qed
  ultimately show "∀x. ∃y. P x y" by (rule exE)
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))
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes A1: "∀ x. P a x x"
    and A2: "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof
  from A2
  have "∀y z. P a y z ⟶ P (f a) y (f z)" by (rule allE)
  hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
  hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
  moreover have "P a (f a) (f a)" using A1 by (rule allE)
  ultimately show "P (f a) (f a) (f (f a))" by (rule mp)
qed

(* alfmarcua enrparalv *)
lemma ejercicio_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 (rule exI, rule mp)
  show "P a (f a) (f a)" using assms(1) by (rule allE)
next
  have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
  then have "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
  then show "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
qed

(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2
   hugrubsan pabbergue giafus1 antramhur *) 
lemma ejercicio_5_2:
  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 (rule exI)
  have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) ..
  hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
  hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
  moreover have "P a (f a) (f a)" using assms(1) by (rule allE)
  ultimately show "P (f a) (f a) (f (f a))" by (rule mp)
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))
  ------------------------------------------------------------------ *}

(* benber alfmarcua giafus1 *)
lemma
  assumes "∀y. Q a y"
      and "∀x y. Q x y ⟶ Q (s x) (s y)"
    shows "∃z. Q a z ∧ Q z (s (s a))"
proof
  have "Q a a" using `∀y. Q a y` by (rule allE)
  moreover have "Q a (s (s a))" using `∀y. Q a y` by (rule allE)
  ultimately show "Q a a ∧ Q a (s (s a))" by (rule conjI)
qed

(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2
   hugrubsan pabbergue enrparalv antramhur *) 
lemma ejercicio_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 (rule exI)
  have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) by (rule allE)
  hence "Q a (s a) ⟶ Q (s a) (s (s a))" by (rule allE)
  moreover have "Q a (s a)" using assms(1) by (rule allE)
  ultimately have "Q (s a) (s (s a))" by (rule mp)
  with `Q a (s a)` show "Q a (s a) ∧ Q (s a) (s (s a))" 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.
  ------------------------------------------------------------------ *}

(* benber manperjim alfmarcua pabalagon marfruman1 josgomrom4 gleherlop
   raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
lemma
  assumes "A ∨ P ⟶ R ∧ F"
    and "F ∨ N ⟶ Or"
  shows "A ⟶ Or"
proof
  assume "A"
  hence "A ∨ P" by (rule disjI1)
  with `A ∨ P ⟶ R ∧ F` have "R ∧ F" by (rule mp)
  hence "F" by (rule conjunct2)
  hence "F ∨ N" by (rule disjI1)
  with `F ∨ N ⟶ Or` show "Or" by (rule mp)
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.
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes "A ⟶ (M ⟷ ¬B)"
    and "A ∨ B"
  shows "¬B ⟶ M"
proof
  assume "¬B"
  note `A ∨ B`
  moreover {
    assume "A"
    with `A ⟶ (M ⟷ ¬B)` have "M ⟷ ¬B" by (rule mp)
    hence "¬B ⟹ M" by (rule iffD2)
    hence "M" using `¬B` .
  }
  moreover {
    note `¬B`
    moreover assume "B"
    ultimately have "M" by (rule notE)
  }
  ultimately show "M" by (rule disjE)
qed

(* alfmarcua marfruman1 *)
lemma ejercicio_8:
  assumes "A ∧ ¬ B ⟶ M"
          "A ∨ B"
  shows "¬ B ⟶ M"
proof (rule impI)
  assume "¬B"
  show "M" using assms(2)
  proof (rule disjE)
    assume "A"
    then have "A ∧ ¬ B" using `¬ B` by (rule conjI)
    show "M" using assms(1) `A ∧ ¬ B` by (rule mp)
  next
    assume "B"
    show "M" using `¬ B` `B` by (rule notE)
  qed
qed

(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan
   pabbergue enrparalv giafus1 antramhur *) 
lemma ejercicio_8_2:
  assumes "A ⟶ (M ⟷ ¬B)"
          "A ∨ B"
        shows "¬B ⟶ M"
using assms(2) proof (rule disjE)
  assume 1: A
  have 2: "M ⟷ ¬B" using assms(1) 1 by (rule mp)
  show "¬B ⟶ M" proof (rule impI)
    assume 3: "¬B" show M using 2 3 by (rule iffD2)
  qed
next
  assume 4: B
  show ?thesis proof (rule impI)
    assume "¬B" thus M using 4 by (rule notE)
  qed
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
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes "∀x. ¬ R x ⟶ R (p x)"
  shows "∃x. R x ∧ R (p (p x))"
proof -
  have 0: "p ∨ ¬ p" for p
  proof (rule ccontr)
    assume "¬ (p ∨ ¬ p)"
    moreover {
      have "p"
      proof (rule ccontr)
        assume "¬ p"
        hence "p ∨ ¬ p" by (rule disjI2)
        with `¬ (p ∨ ¬ p)` show "False" by (rule notE)
      qed
      hence "p ∨ ¬ p" by (rule disjI1)
    }
    ultimately show "False" by (rule notE)
  qed

  have "¬ R x ⟶ R (p x)" for x using assms(1) by (rule allE)
  hence 1: "¬ R x ⟹ R (p x)" for x by (rule mp)

  have 2: "⟦R y; ¬ R (p y)⟧ ⟹ ?thesis" for y
  proof
    assume "R y"
    assume "¬ R (p y)"
    hence "R (p (p y))" by (rule 1)
    with `R y` show "R y ∧ R (p (p y))" by (rule conjI)
  qed

  have 3: "R y ⟹ ?thesis" for y
  proof -
    assume "R y"

    have "R (p y) ∨ ¬ R (p y)" by (rule 0)
    moreover {
      assume "R (p y)"
      have "R (p (p y)) ∨ ¬ R (p (p y))" by (rule 0)
      moreover {
        assume "R (p (p y))"
        with `R y` have "R y ∧ R (p (p y))" by (rule conjI)
        hence ?thesis by (rule exI)
      }
      moreover {
        assume "¬ R (p (p y))"
        with `R (p y)` have ?thesis by (rule 2)
      }
      ultimately have ?thesis by (rule disjE)
    }
    moreover {
      assume "¬ R (p y)"
      with `R y` have ?thesis by (rule 2)
    }
    ultimately show ?thesis by (rule disjE)
  qed

  fix y
  have "R y ∨ ¬ R y" by (rule 0)
  moreover {
    assume "R y"
    hence ?thesis by (rule 3)
  }
  moreover {
    assume "¬ R y"
    hence "R (p y)" by (rule 1)
    hence ?thesis by (rule 3)
  }
  ultimately show ?thesis by (rule disjE)
qed

(* alfmarcua *)
lemma ejercicio_9_2:
  assumes "∀ x. ¬ R x ⟶ R (p x)"
  shows "∃x. R x ∧ R (p (p x))"
proof (rule disjE, rule ejercicio_52)
  have prelemma:"(∃y. ¬ R (p y)) ⟶ ?thesis"
  proof (rule impI)
    assume "∃y. ¬ R (p y)"
    then obtain b where  "¬ R (p b)" by (rule exE)
    have "¬ R (p b) ⟶ R (p (p b))" using assms by (rule allE)
    then have "R (p (p b))" using `¬ R (p b)` by (rule mp)
    have "¬ R b ⟶ R (p b)" using assms by (rule allE)
    then have "¬¬ R b" using `¬ R (p b)` by (rule mt)
    then have "R b" by (rule notnotD)
    then have "R b ∧ R (p (p b))" using `R (p (p b))` by (rule conjI)
    then show "∃x. R x ∧ R (p (p x))" by (rule exI)
  qed
  
  fix a
  show "R (p a) ⟹ ?thesis"
  proof (rule disjE, rule ejercicio_52)
    assume "R (p a)"
    show "R (p (p a)) ⟹ ?thesis"
    proof (rule disjE, rule ejercicio_52)
      assume "R (p (p (p a)))"
      have "R (p a) ∧ R (p (p (p a)))" using `R (p a)` `R (p (p (p a)))`  by (rule conjI)
      then show ?thesis by (rule exI)
    next
      assume "¬ R (p (p (p a)))"
      then have "∃y. ¬ R (p y)" by (rule exI)
      show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
    qed
  next
    assume "¬ R (p (p a))"
    then have "∃y. ¬ R (p y)" by (rule exI)
    show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
  qed

  assume "¬ R (p a)"
  then have "∃y. ¬ R (p y)" by (rule exI)
  show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
qed

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop raffergon2
   hugrubsan pabbergue enrparalv giafus1 antramhur *) 
lemma ejercicio_9_3:
  assumes "∀x. ¬R x ⟶ R (p x)"
  shows "∃x. R x ∧ R (p (p x))"
proof -
  fix y
  have s1: "⟦¬R (p y)⟧ ⟹ ?thesis" for y proof (rule exI)
    assume 2: "¬R (p y)"
    have "¬R (p y) ⟶ R (p (p y))" using assms(1) by (rule allE)
    hence 3: "R (p (p y))" using 2 by (rule mp)
    have "¬R y ⟶ R (p y)" using assms(1) by (rule allE)
    hence "¬¬R y" using 2 by (rule mt)
    hence "R y" by (rule notnotD)
    thus "R y ∧ R (p (p y))" using 3 by (rule conjI)
  qed
  have s2: "R y ⟹ ?thesis" for y proof -
    assume 2: "R y"
    have "¬R (p y) ∨ R (p y)" by (rule excluded_middle)
    thus ?thesis proof (rule disjE)
      assume 3: "¬R (p y)" thus ?thesis by (rule s1)
    next
      assume 4: "R (p y)"
      have "¬R (p (p y)) ∨ R (p (p y))" by (rule excluded_middle)
      thus ?thesis proof (rule disjE)
        assume "¬R (p (p y))" thus ?thesis by (rule s1)
      next
        assume "R (p (p y))"
        with `R y` have "R y ∧ R (p (p y))" by (rule conjI)
        thus ?thesis by (rule exI)
      qed
    qed
  qed
  have "¬R y ∨ R y" by (rule excluded_middle)
  thus ?thesis proof (rule disjE)
    assume 2: "R y" thus ?thesis by (rule s2)
  next
    assume 4: "¬R y"
    have "¬R y ⟶ R (p y)" using assms(1) by (rule allE)
    hence "R (p y)" using 4 by (rule mp)
    thus ?thesis by (rule s2)
  qed
qed

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
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes "∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)"
    and "∀x. E x ⟶ ¬ Ap j x"
  shows "(∃x. E x ∧ N x) ⟶ ¬ Af j"
proof
  assume "∃x. E x ∧ N x"

  show "¬ Af j"
  proof (rule ccontr)
    assume "¬ ¬ Af j"
    hence "Af j" by (rule notnotD)

    note `∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)`
    hence "Af j ⟶ (∀x. E x ⟶ Ap j x)" by (rule allE)
    moreover note `Af j`
    ultimately have "∀x. E x ⟶ Ap j x" by (rule mp)

    note `∃x. E x ∧ N x`
    moreover have "E x ∧ N x ⟹ False" for x
    proof -
      assume "E x ∧ N x"
      hence "E x" by (rule conjunct1)

      note `∀x. E x ⟶ Ap j x`
      hence "E x ⟶ Ap j x" by (rule allE)
      hence "Ap j x" using `E x`  by (rule mp)

      note `∀x. E x ⟶ ¬ Ap j x`
      hence "E x ⟶ ¬ Ap j x" by (rule allE)
      hence "¬ Ap j x" using `E x` by (rule mp)
      thus "False" using `Ap j x` by (rule notE)
    qed
    ultimately show "False" by (rule exE)
  qed
qed

(* alfmarcua marfruman1 *)
lemma ejercicio_10_2:
  assumes "∀x y. Af x ∧ E y ⟶ Ap x y"
          "∀y. E y ⟶ ¬ Ap j y"
  shows "(∃y. E y ∧ N y) ⟶ ¬ Af j"
proof (rule impI)
  assume "∃x. E x ∧ N x"
  then obtain a where "E a ∧ N a" by (rule exE)
  then have "E a" by (rule conjunct1)
  show "¬ Af j"
  proof (rule notI, rule notE)
    assume "Af j"
    then show "Af j ∧ E a" using `E a` by (rule conjI)
  next
    have "E a ⟶ ¬ Ap j a" using assms(2) by (rule allE)
    then have "¬ Ap j a" using `E a` by (rule mp)
    have "∀y. Af j ∧ E y ⟶ Ap j y" using assms(1) by (rule allE)
    then have "Af j ∧ E a ⟶ Ap j a" by (rule allE)
    then show "¬ (Af j ∧ E a)" using `¬ Ap j a` by (rule mt)
  qed
qed

(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan
   pabbergue enrparalv giafus1 antramhur *) 
lemma ejercicio_10_3:
  assumes "∀x y. Af x ∧ E y ⟶ Ap x y"
          "∀x y. x = j ∧ E y ⟶ ¬(Ap x y)"
  shows "(∃ x. (E x ∧ N x)) ⟶ ¬(Af j)"
proof (rule impI)
  assume 1: "∃x. E x ∧ N x"
  show "¬(Af j)" proof (rule ccontr)
    fix a
    assume "¬¬Af j" hence 2: "Af j" by (rule notnotD)
    obtain a where 3: "E a ∧ N a" using 1 by (rule exE)
    hence 4: "E a" by (rule conjunct1)
    have 5: "N a" using 3 by (rule conjunct2)
    have "∀y. Af j ∧ E y ⟶ Ap j y" using assms(1) by (rule allE)
    hence 6: "Af j ∧ E a ⟶ Ap j a" by (rule allE)
    have 7: "Af j ∧ E a" using 2 4 by (rule conjI)
    have 8: "Ap j a" using 6 7 by (rule mp)
    have "∀y. j = j ∧ E y ⟶ ¬(Ap j y)" using assms(2) by (rule allE)
    hence 9: "j = j ∧ E a ⟶ ¬(Ap j a)" by (rule allE)
    have "j = j" by (rule refl)
    hence 10: "j = j ∧ E a" using 4 by (rule conjI)
    have "¬(Ap j a)" using 9 10 by (rule mp)
    thus False using 8 by (rule notE)
  qed
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
   ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes A1: "∀x. P x ⟶ R x"
    and A2: "∀x. P x ⟶ (¬(Q x) ⟶ R x)"
    and "¬(R a)"
  shows "P a ⟶ Q a"
proof
  have "P a ⟶ (¬(Q a) ⟶ R a)" using A2 by (rule allE)
  moreover assume "P a"
  ultimately have "¬(Q a) ⟶ R a" by (rule mp)

  show "Q a"
  proof (rule ccontr)
    assume "¬(Q a)"
    with `¬(Q a) ⟶ R a` have "R a" by (rule mp)
    with `¬(R a)` show "False" by (rule notE)
  qed
qed

(* alfmarcua *)
lemma ejercicio_11:
  assumes "∄x. P x ∧ R x"
          "∀x. P x ∧ (¬ Q x) ⟶ R x"
  shows "P a ⟶ Q a"
proof (rule impI, rule ccontr)
  assume "P a" "¬ Q a"
  then have "P a ∧ (¬ Q a)" by (rule conjI)
  have "P a ∧ (¬ Q a) ⟶ R a" using assms(2) by (rule allE)
  then have "R a" using `P a ∧ (¬ Q a)` by (rule mp)
  have "P a ∧ R a" using `P a` `R a` by (rule conjI)
  then have "∃x. P x ∧ R x" by (rule exI)
  show False using assms(1) `∃x. P x ∧ R x` by (rule notE)
qed

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop hugrubsan
   pabbergue enrparalv giafus1 antramhur *) 
lemma ejercicio_11_2:
  assumes "¬(∃x. P x ∧ R x)"
          "∀x. P x ∧ ¬Q x ⟶ R x"
  shows "P a ⟶ Q a"
proof (rule impI)
  assume 1: "P a"
  show "Q a" proof (rule ccontr)
    assume 2: "¬Q a"
    have 3: "P a ∧ ¬Q a" using 1 2 by (rule conjI)
    have 4: "P a ∧ ¬ Q a ⟶R a" using assms(2) by (rule allE)
    hence 5: "R a" using 3 by (rule mp)
    have 6: "P a ∧ R a" using 1 5 by (rule conjI)
    hence 7: "∃x. P x ∧ R x" by (rule exI)
    show False using assms(1) 7 by (rule notE)
  qed
qed

end