Ver el código de «GLC T2R2a» - DAO (Demostración asistida por ordenador)

<source lang="isabelle">
header {* T2R2a: Argumentación en lógica de primer orden *}

theory T2R2a
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta relación es formalizar y demostrar la corrección
  de los argumentos usando sólo las reglas básicas de deducción natural
  de la lógica de primer orden (sin usar el método auto). 

  Las reglas básicas de la deducción natural son las siguientes:
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · notnotI:    P ⟹ ¬¬ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · mt:         ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  · 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
  · excluded_middle: ¬P ∨ 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

  --------------------------------------------------------------------- 
*}

text {*
  Se usarán las reglas notnotI y mt 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 
     Sócrates es un hombre. 
     Los hombres son mortales. 
     Luego, Sócrates es mortal.
  Usar s    para Sócrates
       H(x) para x es un hombre          
       M(x) para x es mortal
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_1a:
  "⟦H(s); ∀x. H(x) ⟶ M(x)⟧ ⟹ M(s)"
by auto

-- "La demostración estructurada es"
lemma ejercicio_1b:
  assumes "H(s)" 
          "∀x. H(x) ⟶ M(x)"
  shows   "M(s)"
proof -
  have "H(s) ⟶ M(s)" using assms(2) ..
  thus "M(s)" using assms(1) ..  
qed

-- "La demostración detallada es"
lemma ejercicio_1c:
  assumes "H(s)" 
          "∀x. H(x) ⟶ M(x)"
  shows   "M(s)"
proof -
  have "H(s) ⟶ M(s)" using assms(2) by (rule allE)
  thus "M(s)" using assms(1) 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
  ------------------------------------------------------------------ *}

-- "La refutación automática es"
lemma ejercicio_2a:
  "(∃x. I(x)) ∧ (∃x. T(x)) ⟹ ∃x. I(x) ∧ T(x)"
quickcheck
oops

text {*
El argumento es incorrecto como muestra el siguiente contraejemplo:
   I = {a1}
   T = {a2}
*}

text {* --------------------------------------------------------------- 
  Ejercicio 3. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Todos los participantes son vencedores. Hay como máximo un
     vencedor. Hay como máximo un participante. Por lo tanto, hay
     exactamente un participante. 
  Usar P(x) para x es un participante
       V(x) para x es un vencedor
  ------------------------------------------------------------------ *}

-- "La refutación automática es"
lemma ejercicio_3a: 
  "⟦∀x. P(x) ⟶ V(x); 
    ∀x y. V(x) ∧ V(y) ⟶ x=y; 
    ∀x y. P(x) ∧ P(y) ⟶ x=y⟧
   ⟹ ∃x. P(x) ∧ (∀y. P(y) ⟶ x=y)"
quickcheck  
oops

text {*
El argumento es incorrecto como muestra el siguiente contraejemplo:
   V = {}
   P = {}
*}

text {* --------------------------------------------------------------- 
  Ejercicio 4. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Todo aquel que entre en el país y no sea un VIP será cacheado por
     un aduanero. Hay un contrabandista que entra en el país y que solo
     podrá ser cacheado por contrabandistas. Ningún contrabandista es un
     VIP. Por tanto, algún aduanero es contrabandista.
  Usar A(x)    para x es aduanero
       Ca(x,y) para x cachea a y
       Co(x)   para x es contrabandista
       E(x)    para x entra en el pais
       V(x)    para x es un VIP
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_4a:
  "⟦∀x. E(x) ∧ ¬V(x) ⟶ (∃y. A(y) ∧ Ca(y,x));
    ∃x. Co(x) ∧ E(x) ∧ (∀y. Ca(y,x) ⟶ Co(y));
    ¬(∃x. Co(x) ∧ V(x))⟧
   ⟹ ∃x. A(x) ∧ Co(x)"
by metis

-- "La demostración estructurada es"
lemma ejercicio_4b:
  assumes "∀x. E(x) ∧ ¬V(x) ⟶ (∃y. A(y) ∧ Ca(y,x))"
           "∃x. Co(x) ∧ E(x) ∧ (∀y. Ca(y,x) ⟶ Co(y))"
           "¬(∃x. Co(x) ∧ V(x))"
  shows    "∃x. A(x) ∧ Co(x)"
proof -
  obtain a where a: "Co(a) ∧ E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" 
    using assms(2) ..
  have "∃y. A(y) ∧ Ca(y,a)"
  proof -
    have "E(a) ∧ ¬V(a) ⟶ (∃y. A(y) ∧ Ca(y,a))" using assms(1) ..
    moreover
    have "E(a) ∧ ¬V(a)"
    proof
      have "E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" using a ..
      thus "E(a)" ..
    next
      have "∀x. ¬(Co(x) ∧ V(x))" using assms(3) by (rule no_ex)
      hence "¬(Co(a) ∧ V(a))" ..
      have "Co(a)" using a ..
      show "¬V(a)" 
      proof
        assume "V(a)"
        with `Co(a)` have "Co(a) ∧ V(a)" ..
        with `¬(Co(a) ∧ V(a))` show False ..
      qed
    qed
    ultimately show "∃y. A(y) ∧ Ca(y,a)" ..
  qed
  then obtain b where "A(b) ∧ Ca(b,a)" ..
  hence "A(b)" ..
  moreover
  have "Co(b)"
    proof -
      have "E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" using a ..
      hence "∀y. Ca(y,a) ⟶ Co(y)" ..
      hence "Ca(b,a) ⟶ Co(b)" ..
      have "Ca(b,a)" using `A(b) ∧ Ca(b,a)` ..
      with `Ca(b,a) ⟶ Co(b)` show "Co(b)" ..
    qed
  ultimately have "A(b) ∧ Co(b)" ..
  thus "∃x. A(x) ∧ Co(x)" ..
qed

-- "La demostración detallada es"
lemma ejercicio_4c:
  assumes "∀x. E(x) ∧ ¬V(x) ⟶ (∃y. A(y) ∧ Ca(y,x))"
           "∃x. Co(x) ∧ E(x) ∧ (∀y. Ca(y,x) ⟶ Co(y))"
           "¬(∃x. Co(x) ∧ V(x))"
  shows    "∃x. A(x) ∧ Co(x)"
proof -
  obtain a where a: "Co(a) ∧ E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" 
    using assms(2) by (rule exE)
  have "∃y. A(y) ∧ Ca(y,a)"
  proof -
    have "E(a) ∧ ¬V(a) ⟶ (∃y. A(y) ∧ Ca(y,a))" using assms(1) by (rule allE)
    moreover
    have "E(a) ∧ ¬V(a)"
    proof
      have "E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" using a by (rule conjunct2)
      thus "E(a)" by (rule conjunct1)
    next
      have "∀x. ¬(Co(x) ∧ V(x))" using assms(3) by (rule no_ex)
      hence "¬(Co(a) ∧ V(a))" by (rule allE)
      have "Co(a)" using a by (rule conjunct1)
      show "¬V(a)" 
      proof (rule notI)
        assume "V(a)"
        with `Co(a)` have "Co(a) ∧ V(a)" by (rule conjI)
        with `¬(Co(a) ∧ V(a))` show False by (rule notE)
      qed
    qed
    ultimately show "∃y. A(y) ∧ Ca(y,a)" by (rule mp)
  qed
  then obtain b where "A(b) ∧ Ca(b,a)" by (rule exE)
  hence "A(b)" by (rule conjunct1)
  moreover
  have "Co(b)"
    proof -
      have "E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" using a by (rule conjunct2)
      hence "∀y. Ca(y,a) ⟶ Co(y)" by (rule conjunct2)
      hence "Ca(b,a) ⟶ Co(b)" by (rule allE)
      have "Ca(b,a)" using `A(b) ∧ Ca(b,a)` by (rule conjunct2)
      with `Ca(b,a) ⟶ Co(b)` show "Co(b)" by (rule mp)
    qed
  ultimately have "A(b) ∧ Co(b)" by (rule conjI)
  thus "∃x. A(x) ∧ Co(x)" by (rule exI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
     María y a Pedro.
  Usar j      para Juan  
       m      para María
       p      para Pedro
       T(x,y) para x teme a y
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_5a:
  "⟦T(j,m); T(j,p)⟧ ⟹ ∃x. T(x,m) ∧ T(x,p)"
by auto

-- "La demostración estructurada es"
lemma ejercicio_5b:
  assumes "T(j,m)" 
          "T(j,p)"
  shows   "∃x. T(x,m) ∧ T(x,p)"
proof
  show "T(j,m) ∧ T(j,p)" using assms ..
qed

-- "La demostración detallada es"
lemma ejercicio_5c:
  assumes "T(j,m)" 
          "T(j,p)"
  shows   "∃x. T(x,m) ∧ T(x,p)"
proof (rule exI)
  show "T(j,m) ∧ T(j,p)" using assms by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. 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
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_6a:
  assumes "∀x y. H(x,y) ⟶ H(y,x)"
          "∀x y z. H(x,y) ∧ P(z,x) ⟶ P(z,y)"
          "H(j,l)"
          "P(c,l)"
  shows   "P(c,j)"
using assms
by metis

-- "La demostración estructurada es"
lemma ejercicio_6b:
  fixes H P :: "'a × 'a ⇒ bool" 
  assumes "∀x y. H(x,y) ⟶ H(y,x)"
          "∀x y z. H(x,y) ∧ P(z,x) ⟶ P(z,y)"
          "H(j,l)"
          "P(c,l)"
  shows   "P(c,j)"
proof -
  have "H(l,j) ∧ P(c,l) ⟶ P(c,j)" 
  proof -
    have "∀y z. H(l,y) ∧ P(z,l) ⟶ P(z,y)" using assms(2) ..
    hence "∀z. H(l,j) ∧ P(z,l) ⟶ P(z,j)" ..
    thus "H(l,j) ∧ P(c,l) ⟶ P(c,j)" ..
  qed
  moreover
  have "H(l,j) ∧ P(c,l)"
  proof
    have "∀y. H(j,y) ⟶ H(y,j)" using assms(1) ..
    hence "H(j,l) ⟶ H(l,j)" .. 
    thus "H(l,j)" using assms(3) ..
  next
    show "P(c,l)" using assms(4) .
  qed
  ultimately show "P(c,j)" .. 
qed

-- "La demostración detallada es"
lemma ejercicio_6c:
  fixes H P :: "'a × 'a ⇒ bool" 
  assumes "∀x y. H(x,y) ⟶ H(y,x)"
          "∀x y z. H(x,y) ∧ P(z,x) ⟶ P(z,y)"
          "H(j,l)"
          "P(c,l)"
  shows   "P(c,j)"
proof -
  have "H(l,j) ∧ P(c,l) ⟶ P(c,j)" 
  proof -
    have "∀y z. H(l,y) ∧ P(z,l) ⟶ P(z,y)" using assms(2) by (rule allE)
    hence "∀z. H(l,j) ∧ P(z,l) ⟶ P(z,j)" by (rule allE)
    thus "H(l,j) ∧ P(c,l) ⟶ P(c,j)" by (rule allE)
  qed
  moreover
  have "H(l,j) ∧ P(c,l)"
  proof (rule conjI)
    have "∀y. H(j,y) ⟶ H(y,j)" using assms(1) by (rule allE)
    hence "H(j,l) ⟶ H(l,j)" by (rule allE)
    thus "H(l,j)" using assms(3) by (rule mp)
  next
    show "P(c,l)" using assms(4) by this
  qed
  ultimately show "P(c,j)" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. Formalizar, y decidir la corrección, del siguiente
  argumento 
     La existencia de algún canal de TV pública, supone un acicate para
     cualquier canal de TV privada; el que un canal de TV tenga un
     acicate, supone una gran satisfacción para cualquiera de sus
     directivos; en Madrid hay varios canales públicos de TV; TV5 es un
     canal de TV privada; por tanto, todos los directivos de TV5 están
     satisfechos. 
  Usar Pu(x)  para x es un canal de TV pública
       Pr(x)  para x es un canal de TV privada
       A(x)   para x posee un acicate
       D(x,y) para x es un directivo del canal y
       S(x)   para x está satisfecho 
       t      para TV5
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_7a:
  assumes "(∃x. Pu(x)) ⟶ (∀x. Pr(x) ⟶ A(x))"
          "∀x. A(x) ⟶ (∀y. D(y,x) ⟶ S(y))"
          "∃x. Pu(x)"
          "Pr(t)"
  shows   "∀x. D(x,t) ⟶ S(x)"
using assms
by auto

-- "La demostración estructurada es"
lemma ejercicio_7b:
  assumes "(∃x. Pu(x)) ⟶ (∀x. Pr(x) ⟶ A(x))"
          "∀x. A(x) ⟶ (∀y. D(y,x) ⟶ S(y))"
          "∃x. Pu(x)"
          "Pr(t)"
  shows   "∀x. D(x,t) ⟶ S(x)"
proof
  fix a 
  show "D(a,t) ⟶ S(a)"
  proof
    assume "D(a,t)"
    have "∀x. Pr(x) ⟶ A(x)" using assms(1) assms(3) ..
    hence "Pr(t) ⟶ A(t)" ..
    hence "A(t)" using assms(4) ..
    have "A(t) ⟶ (∀y. D(y,t) ⟶ S(y))" using assms(2) ..
    hence "∀y. D(y,t) ⟶ S(y)" using `A(t)` ..
    hence "D(a,t) ⟶ S(a)" ..
    thus "S(a)" using `D(a,t)` ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_7c:
  assumes "(∃x. Pu(x)) ⟶ (∀x. Pr(x) ⟶ A(x))"
          "∀x. A(x) ⟶ (∀y. D(y,x) ⟶ S(y))"
          "∃x. Pu(x)"
          "Pr(t)"
  shows   "∀x. D(x,t) ⟶ S(x)"
proof (rule allI)
  fix a 
  show "D(a,t) ⟶ S(a)"
  proof (rule impI)
    assume "D(a,t)"
    have "∀x. Pr(x) ⟶ A(x)" using assms(1) assms(3) by (rule mp)
    hence "Pr(t) ⟶ A(t)" by (rule allE)
    hence "A(t)" using assms(4) by (rule mp)
    have "A(t) ⟶ (∀y. D(y,t) ⟶ S(y))" using assms(2) by (rule allE)
    hence "∀y. D(y,t) ⟶ S(y)" using `A(t)` by (rule mp)
    hence "D(a,t) ⟶ S(a)" by (rule allE)
    thus "S(a)" using `D(a,t)` by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 8. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Quien intente entrar en un país y no tenga pasaporte, encontrará
     algún aduanero que le impida el paso. A algunas personas
     motorizadas que intentan entrar en un país le impiden el paso
     únicamente personas motorizadas. Ninguna persona motorizada tiene
     pasaporte. Por tanto, ciertos aduaneros están motorizados.
  Usar E(x)   para x entra en un país
       P(x)   para x tiene pasaporte
       A(x)   para x es aduanero
       I(x,y) para x impide el paso a y
       M(x)   para x está motorizada
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_8a:
  assumes "∀x. E(x) ∧ ¬P(x) ⟶ (∃y. A(y) ∧ I(y,x))"
          "∃x. M(x) ∧ E(x) ∧ (∀y. I(y,x) ⟶ M(y))"
          "∀x. M(x) ⟶ ¬P(x)"
  shows "∃x. A(x) ∧ M(x)"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_8b:
  assumes "∀x. E(x) ∧ ¬P(x) ⟶ (∃y. A(y) ∧ I(y,x))"
          "∃x. M(x) ∧ E(x) ∧ (∀y. I(y,x) ⟶ M(y))"
          "∀x. M(x) ⟶ ¬P(x)"
  shows "∃x. A(x) ∧ M(x)"
proof - 
  obtain a where a: "M(a) ∧ E(a) ∧ (∀y. I(y,a) ⟶ M(y))" using assms(2) ..
  hence "M(a)" ..
  have "M(a) ⟶ ¬P(a)" using assms(3) ..
  hence "¬P(a)" using `M(a)` ..
  have a1: "E(a) ∧ (∀y. I(y,a) ⟶ M(y))" using a ..
  hence "E(a)" ..
  hence "E(a) ∧ ¬P(a)" using `¬P(a)` ..
  have "E(a) ∧ ¬P(a) ⟶ (∃y. A(y) ∧ I(y,a))" using assms(1) ..
  hence "∃y. A(y) ∧ I(y,a)" using `E(a) ∧ ¬P(a)`..
  then obtain b where b: "A(b) ∧ I(b,a)" ..
  have "A(b) ∧ M(b)"
  proof
    show "A(b)" using b ..
  next
    have "I(b,a)" using b ..
    have "∀y. I(y,a) ⟶ M(y)" using a1 ..
    hence "I(b,a) ⟶ M(b)" ..
    thus "M(b)" using `I(b,a)` ..
  qed
  thus "∃x. A(x) ∧ M(x)" ..
qed

-- "La demostración detallada es"
lemma ejercicio_8c:
  assumes "∀x. E(x) ∧ ¬P(x) ⟶ (∃y. A(y) ∧ I(y,x))"
          "∃x. M(x) ∧ E(x) ∧ (∀y. I(y,x) ⟶ M(y))"
          "∀x. M(x) ⟶ ¬P(x)"
  shows "∃x. A(x) ∧ M(x)"
proof - 
  obtain a where a: "M(a) ∧ E(a) ∧ (∀y. I(y,a) ⟶ M(y))" 
    using assms(2) by (rule exE)
  hence "M(a)" by (rule conjunct1)
  have "M(a) ⟶ ¬P(a)" using assms(3) by (rule allE)
  hence "¬P(a)" using `M(a)` by (rule mp)
  have a1: "E(a) ∧ (∀y. I(y,a) ⟶ M(y))" using a by (rule conjunct2)
  hence "E(a)" by (rule conjunct1)
  hence "E(a) ∧ ¬P(a)" using `¬P(a)` by (rule conjI)
  have "E(a) ∧ ¬P(a) ⟶ (∃y. A(y) ∧ I(y,a))" 
    using assms(1) by (rule allE)
  hence "∃y. A(y) ∧ I(y,a)" using `E(a) ∧ ¬P(a)`by (rule mp)
  then obtain b where b: "A(b) ∧ I(b,a)" by (rule exE)
  have "A(b) ∧ M(b)"
  proof (rule conjI)
    show "A(b)" using b by (rule conjunct1)
  next
    have "I(b,a)" using b by (rule conjunct2)
    have "∀y. I(y,a) ⟶ M(y)" using a1 by (rule conjunct2)
    hence "I(b,a) ⟶ M(b)" by (rule allE)
    thus "M(b)" using `I(b,a)`by (rule mp)
  qed
  thus "∃x. A(x) ∧ M(x)" by (rule exI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 9. 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
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_9a:
  assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
          "∀x. E(x) ⟶ ¬Ap(j,x)"
  shows   "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_9b:
  assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
          "∀x. E(x) ⟶ ¬Ap(j,x)"
  shows   "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
proof
  assume "∃x. E(x) ∧ N(x)"
  then obtain a where a: "E(a) ∧ N(a)" ..
  show "¬Af(j)"
  proof
    assume "Af(j)"
    have "Af(j) ⟶ (∀y. E(y) ⟶ Ap(j,y))" using assms(1) ..
    hence "∀y. E(y) ⟶ Ap(j,y)" using `Af(j)` ..
    hence "E(a) ⟶ Ap(j,a)" ..
    have "E(a)" using a ..
    with `E(a) ⟶ Ap(j,a)` have "Ap(j,a)" ..
    have "E(a) ⟶ ¬Ap(j,a)" using assms(2) ..
    hence "¬Ap(j,a)" using `E(a)` ..
    thus False using `Ap(j,a)` ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_9c:
  assumes "∀x. Af(x) ⟶ (∀y. 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 a: "E(a) ∧ N(a)" by (rule exE)
  show "¬Af(j)"
  proof (rule notI)
    assume "Af(j)"
    have "Af(j) ⟶ (∀y. E(y) ⟶ Ap(j,y))" using assms(1) by (rule allE)
    hence "∀y. E(y) ⟶ Ap(j,y)" using `Af(j)` by (rule mp)
    hence "E(a) ⟶ Ap(j,a)" by (rule allE)
    have "E(a)" using a by (rule conjunct1)
    with `E(a) ⟶ Ap(j,a)` have "Ap(j,a)" by (rule mp)
    have "E(a) ⟶ ¬Ap(j,a)" using assms(2) by (rule allE)
    hence "¬Ap(j,a)" using `E(a)` by (rule mp)
    thus False using `Ap(j,a)` by (rule notE)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 10. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Ningún aristócrata debe ser condenado a galeras a menos que sus
     crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
     hay aristócratas que han cometido crímenes vergonzosos aunque su
     forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
     que no está condenado a galeras. 
  Usar A(x)  para x es aristócrata
       G(x)  para x está condenado a galeras
       L(x)  para x lleva una vida licenciosa
       V(x)  para x ha cometido crímenes vergonzoso
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_10a:
  assumes "∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x)"
          "∃x. A(x) ∧ V(x) ∧ ¬L(x)"
  shows   "∃x. A(x) ∧ ¬G(x)"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_10b:
  assumes "∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x)"
          "∃x. A(x) ∧ V(x) ∧ ¬L(x)"
  shows   "∃x. A(x) ∧ ¬G(x)"
proof -
  obtain b where b: "A(b) ∧ V(b) ∧ ¬L(b)" using assms(2) ..
  have "A(b) ∧ ¬G(b)"
  proof
    show "A(b)" using b ..
  next
    show "¬G(b)"
    proof
      assume "G(b)"
      have "¬L(b)"
      proof -
        have "V(b) ∧ ¬L(b)" using b ..
        thus "¬L(b)" ..
      qed
      moreover have "L(b)"
      proof -
        have "A(b) ∧ G(b) ⟶ L(b) ∧ V(b)" using assms(1) ..
        have "A(b)" using b ..
        hence "A(b) ∧ G(b)" using `G(b)` ..
        with `A(b) ∧ G(b) ⟶ L(b) ∧ V(b)` have "L(b) ∧ V(b)" ..
        thus "L(b)" ..
      qed
      ultimately show False ..
    qed
  qed
  thus "∃x. A(x) ∧ ¬G(x)" ..
qed

-- "La demostración detallada es"
lemma ejercicio_10c:
  assumes "∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x)"
          "∃x. A(x) ∧ V(x) ∧ ¬L(x)"
  shows   "∃x. A(x) ∧ ¬G(x)"
proof -
  obtain b where b: "A(b) ∧ V(b) ∧ ¬L(b)" using assms(2) by (rule exE)
  have "A(b) ∧ ¬G(b)"
  proof (rule conjI)
    show "A(b)" using b by (rule conjunct1)
  next
    show "¬G(b)"
    proof (rule notI)
      assume "G(b)"
      have "¬L(b)"
      proof -
        have "V(b) ∧ ¬L(b)" using b by (rule conjunct2)
        thus "¬L(b)" by (rule conjunct2)
      qed
      moreover have "L(b)"
      proof -
        have "A(b) ∧ G(b) ⟶ L(b) ∧ V(b)" using assms(1) by (rule allE)
        have "A(b)" using b by (rule conjunct1)
        hence "A(b) ∧ G(b)" using `G(b)` by (rule conjI)
        with `A(b) ∧ G(b) ⟶ L(b) ∧ V(b)` have "L(b) ∧ V(b)" by (rule mp)
        thus "L(b)" by (rule conjunct1)
      qed
      ultimately show False by (rule notE)
    qed
  qed
  thus "∃x. A(x) ∧ ¬G(x)" by (rule exI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 11. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Todo individuo que esté conforme con el contenido de cualquier
     acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
     políticos. Cualquiera que se inhiba de los asuntos políticos, no
     participará en el próximo referéndum. Todo español, está conforme
     con el acuerdo internacional de Maastricht, al que sin embargo no
     apoya. Por tanto, cualquier individuo o no es español, o en otro
     caso, está conforme con el contenido del acuerdo internacional de
     Maastricht y no participará en el próximo referéndum. 
  Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
       A(x,y) para la persona x apoya el acuerdo y
       I(x)   para la persona x se inibe de asuntos políticos
       R(x)   para la persona x participará en el próximo referéndum
       E(x)   para la persona x es española
       m      para el acuerdo de Maastricht
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_11a:
  assumes "∀x y. C(x,y) ⟶ A(x,y) ∨ I(x)"
          "∀x. I(x) ⟶ ¬R(x)"
          "∀x. E(x) ⟶ C(x,m) ∧ ¬A(x,m)"
  shows   "∀x. ¬E(x) ∨ (C(x,m) ∧ ¬R(x))"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_11b:
  assumes "∀x y. C(x,y) ⟶ A(x,y) ∨ I(x)"
          "∀x. I(x) ⟶ ¬R(x)"
          "∀x. E(x) ⟶ C(x,m) ∧ ¬A(x,m)"
  shows   "∀x. ¬E(x) ∨ (C(x,m) ∧ ¬R(x))"
proof
  fix a
  have "¬E(a) ∨ E(a)" ..
  thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))"
  proof
    assume "¬E(a)"
    thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))" ..
  next
    assume "E(a)"
    have "E(a) ⟶ C(a,m) ∧ ¬A(a,m)" using assms(3) ..
    hence "C(a,m) ∧ ¬A(a,m)" using `E(a)` ..
    hence "C(a,m)" .. 
    have "∀y. C(a,y) ⟶ A(a,y) ∨ I(a)" using assms(1) ..
    hence "C(a,m) ⟶ A(a,m) ∨ I(a)" ..
    hence "A(a,m) ∨ I(a)" using `C(a,m)` ..
    hence "¬R(a)"
    proof 
      assume "A(a,m)"
      have "¬A(a,m)" using `C(a,m) ∧ ¬A(a,m)`..
      thus "¬R(a)" using `A(a,m)` ..
    next
      assume "I(a)"
      have "I(a) ⟶ ¬R(a)" using assms(2) ..
      thus "¬R(a)" using `I(a)` ..
    qed
    with `C(a,m)` have "C(a,m) ∧ ¬R(a)" ..
    thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))" ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_11c:
  assumes "∀x y. C(x,y) ⟶ A(x,y) ∨ I(x)"
          "∀x. I(x) ⟶ ¬R(x)"
          "∀x. E(x) ⟶ C(x,m) ∧ ¬A(x,m)"
  shows   "∀x. ¬E(x) ∨ (C(x,m) ∧ ¬R(x))"
proof (rule allI)
  fix a
  have "¬E(a) ∨ E(a)" by (rule excluded_middle)
  thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))" 
  proof (rule disjE)
    assume "¬E(a)"
    thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))" by (rule disjI1)
  next
    assume "E(a)"
    have "E(a) ⟶ C(a,m) ∧ ¬A(a,m)" using assms(3) by (rule allE)
    hence "C(a,m) ∧ ¬A(a,m)" using `E(a)` by (rule mp)
    hence "C(a,m)" by (rule conjunct1)
    have "∀y. C(a,y) ⟶ A(a,y) ∨ I(a)" using assms(1) by (rule allE)
    hence "C(a,m) ⟶ A(a,m) ∨ I(a)" by (rule allE)
    hence "A(a,m) ∨ I(a)" using `C(a,m)` by (rule mp)
    hence "¬R(a)"
    proof (rule disjE)
      assume "A(a,m)"
      have "¬A(a,m)" using `C(a,m) ∧ ¬A(a,m)`by (rule conjunct2)
      thus "¬R(a)" using `A(a,m)` by (rule notE)
    next
      assume "I(a)"
      have "I(a) ⟶ ¬R(a)" using assms(2) by (rule allE)
      thus "¬R(a)" using `I(a)` by (rule mp)
    qed
    with `C(a,m)` have "C(a,m) ∧ ¬R(a)" by (rule conjI)
    thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))" by (rule disjI2)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 12. 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
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_12a:
  assumes "∀x. ¬R(x) ⟶ R(p(x))"
  shows   "∃x. R(x) ∧ R(p(p(x)))"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_12b:
  assumes "∀x. ¬R(x) ⟶ R(p(x))"
  shows   "∃x. R(x) ∧ R(p(p(x)))"
proof -
  have "∃x. R(x)"
  proof (rule ccontr)
    assume "¬(∃x. R(x))"
    hence "∀x. ¬R(x)" by (rule no_ex)
    hence "¬R(a)" ..
    have "¬R(a) ⟶ R(p(a))" using assms ..
    hence "R(p(a))" using `¬R(a)` ..
    hence "∃x. R(x)" ..
    with `¬(∃x. R(x))` show False ..
  qed
  then obtain a where "R(a)" ..
  have "¬R(p(p(a))) ∨ R(p(p(a)))" by (rule excluded_middle)
  thus "∃x. R(x) ∧ R(p(p(x)))"
  proof
    assume "¬R(p(p(a)))"
    have "R(p(a)) ∧ R(p(p(p(a))))"
    proof
      show "R(p(a))"
      proof (rule ccontr)
        assume "¬R(p(a))"
        have "¬R(p(a)) ⟶ R(p(p(a)))" using assms ..
        hence "R(p(p(a)))" using `¬R(p(a))` ..
        with `¬R(p(p(a)))` show False ..
      qed
    next
      show "R(p(p(p(a))))"
      proof -
        have "¬R(p(p(a))) ⟶ R(p(p(p(a))))" using assms ..
        thus "R(p(p(p(a))))" using `¬R(p(p(a)))` .. 
      qed
    qed
    thus "∃x. R(x) ∧ R(p(p(x)))" ..
  next
    assume "R(p(p(a)))"
    with `R(a)` have "R(a) ∧ R(p(p(a)))" ..
    thus "∃x. R(x) ∧ R(p(p(x)))" ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_12c:
  assumes "∀x. ¬R(x) ⟶ R(p(x))"
  shows   "∃x. R(x) ∧ R(p(p(x)))"
proof -
  have "∃x. R(x)"
  proof (rule ccontr)
    assume "¬(∃x. R(x))"
    hence "∀x. ¬R(x)" by (rule no_ex)
    hence "¬R(a)" by (rule allE)
    have "¬R(a) ⟶ R(p(a))" using assms by (rule allE)
    hence "R(p(a))" using `¬R(a)` by (rule mp)
    hence "∃x. R(x)" by (rule exI)
    with `¬(∃x. R(x))` show False by (rule notE)
  qed
  then obtain a where "R(a)" by (rule exE)
  have "¬R(p(p(a))) ∨ R(p(p(a)))" by (rule excluded_middle)
  thus "∃x. R(x) ∧ R(p(p(x)))"
  proof (rule disjE)
    assume "¬R(p(p(a)))"
    have "R(p(a)) ∧ R(p(p(p(a))))"
    proof (rule conjI)
      show "R(p(a))"
      proof (rule ccontr)
        assume "¬R(p(a))"
        have "¬R(p(a)) ⟶ R(p(p(a)))" using assms by (rule allE)
        hence "R(p(p(a)))" using `¬R(p(a))` by (rule mp)
        with `¬R(p(p(a)))` show False by (rule notE)
      qed
    next
      show "R(p(p(p(a))))"
      proof -
        have "¬R(p(p(a))) ⟶ R(p(p(p(a))))" using assms by (rule allE)
        thus "R(p(p(p(a))))" using `¬R(p(p(a)))` by (rule mp)
      qed
    qed
    thus "∃x. R(x) ∧ R(p(p(x)))" by (rule exI)
  next
    assume "R(p(p(a)))"
    with `R(a)` have "R(a) ∧ R(p(p(a)))" by (rule conjI)
    thus "∃x. R(x) ∧ R(p(p(x)))" by (rule exI)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 13. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Todo deprimido que estima a un submarinista es listo. Cualquiera
     que se estime a sí mismo es listo. Ningún deprimido se estima a sí
     mismo. Por tanto, ningún deprimido estima a un submarinista.
  Usar D(x)   para x está deprimido
       E(x,y) para x estima a y
       L(x)   para x es listo
       S(x)   para x es submarinista
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_13a:
  assumes "∀x. D(x) ∧ (∃y. S(y) ∧ E(x,y)) ⟶ L(x)"
          "∀x. E(x,x) ⟶ L(x)"
          "¬(∃x. D(x) ∧ E(x,x))"
  shows   "¬(∃x. D(x) ∧ (∃y. S(y) ∧ E(x,y)))"
quickcheck
oops

text {*
  El argumento es incorrecto como muestra el siguiente contraejemplo:
     Quickcheck found a counterexample:
     D = {a2}
     S = {a1}
     E = {(a2, a1)}
     L = {a2}
*}

text {* --------------------------------------------------------------- 
  Ejercicio 14. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Todos los robots obedecen a los amigos del programador jefe.
     Alvaro es amigo del programador jefe, pero Benito no le
     obedece. Por tanto, Benito no es un robot.
  Usar R(x)    para x es un robot
       Ob(x,y) para x obedece a y
       A(x)    para x es amigo del programador jefe
       b       para Benito
       a       para Alvaro
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_14a:
  assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
          "A(a)"
          "¬Ob(b,a)"
  shows   "¬R(b)"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_14b:
  fixes R A :: "'a ⇒ bool" and
        Ob :: "'a × 'a ⇒ bool"
  assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
          "A(a)"
          "¬Ob(b,a)"
  shows   "¬R(b)"
proof
  assume "R(b)"
  have "∀y. R(b) ∧ A(y) ⟶ Ob(b,y)" using assms(1) ..
  hence "R(b) ∧ A(a) ⟶ Ob(b,a)" ..
  have "R(b) ∧ A(a)" using `R(b)` assms(2) ..
  with `R(b) ∧ A(a) ⟶ Ob(b,a)` have "Ob(b,a)" ..
  with assms(3) show False ..
qed

-- "La demostración detallada es"
lemma ejercicio_14c:
  fixes R A :: "'a ⇒ bool" and
        Ob :: "'a × 'a ⇒ bool"
  assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
          "A(a)"
          "¬Ob(b,a)"
  shows   "¬R(b)"
proof (rule notI)
  assume "R(b)"
  have "∀y. R(b) ∧ A(y) ⟶ Ob(b,y)" using assms(1) by (rule allE)
  hence "R(b) ∧ A(a) ⟶ Ob(b,a)" by (rule allE)
  have "R(b) ∧ A(a)" using `R(b)` assms(2) by (rule conjI)
  with `R(b) ∧ A(a) ⟶ Ob(b,a)` have "Ob(b,a)" by (rule mp)
  with assms(3) show False by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 15. Formalizar, y decidir la corrección, del siguiente
  argumento 
     En una pecera nadan una serie de peces. Se observa que:
     * Hay algún pez x que para cualquier pez y, si el pez x no se come
       al pez y entonces existe un pez z tal que z es un tiburón o bien
       z protege al pez y. 
     * No hay ningún pez que se coma a todos los demás.
     * Ningún pez protege a ningún otro.
     Por tanto, existe algún tiburón en la pecera.
  Usar C(x,y) para x se come a y 
       P(x,y) para x protege a y
       T(x)   para x es un tiburón
   ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_15a:
  assumes "∃x. ∀y. ¬C(x,y) ⟶ (∃z. T(z) ∨ P(z,y))"
          "∀x. ∃y. ¬C(x,y)"
          "∀x y. ¬P(x,y)"
  shows   "∃x. T(x)"
using assms
by auto

-- "La demostración estructurada es"
lemma ejercicio_15b:
  assumes "∃x. ∀y. ¬C(x,y) ⟶ (∃z. T(z) ∨ P(z,y))"
          "∀x. ∃y. ¬C(x,y)"
          "∀x y. ¬P(x,y)"
  shows   "∃x. T(x)"
proof - 
  obtain a where  a: "∀y. ¬C(a,y) ⟶ (∃z. T(z) ∨ P(z,y))" 
    using assms(1) ..
  have "∃y. ¬C(a,y)" using assms(2) ..
  then obtain b where "¬C(a,b)" ..
  have "¬C(a,b) ⟶ (∃z. T(z) ∨ P(z,b))" using a ..
  hence "∃z. T(z) ∨ P(z,b)" using `¬C(a,b)` ..
  then obtain c where "T(c) ∨ P(c,b)" ..
  thus "∃x. T(x)"
  proof 
    assume "T(c)"
    thus "∃x. T(x)" ..
  next
    assume "P(c,b)"
    have "∀y. ¬P(c,y)" using assms(3) ..
    hence "¬P(c,b)" ..
    thus "∃x. T(x)" using `P(c,b)` ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_15c:
  assumes "∃x. ∀y. ¬C(x,y) ⟶ (∃z. T(z) ∨ P(z,y))"
          "∀x. ∃y. ¬C(x,y)"
          "∀x y. ¬P(x,y)"
  shows   "∃x. T(x)"
proof - 
  obtain a where  a: "∀y. ¬C(a,y) ⟶ (∃z. T(z) ∨ P(z,y))" 
    using assms(1) by (rule exE)
  have "∃y. ¬C(a,y)" using assms(2) by (rule allE)
  then obtain b where "¬C(a,b)" by (rule exE)
  have "¬C(a,b) ⟶ (∃z. T(z) ∨ P(z,b))" using a by (rule allE)
  hence "∃z. T(z) ∨ P(z,b)" using `¬C(a,b)` by (rule mp)
  then obtain c where "T(c) ∨ P(c,b)" by (rule exE)
  thus "∃x. T(x)"
  proof (rule disjE)
    assume "T(c)"
    thus "∃x. T(x)" by (rule exI)
  next
    assume "P(c,b)"
    have "∀y. ¬P(c,y)" using assms(3) by (rule allE)
    hence "¬P(c,b)" by (rule allE)
    thus "∃x. T(x)" using `P(c,b)` by (rule notE)
  qed
qed

end
</source>