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

<source lang="isabelle">
header {* T1R2: Argumentación proposicional *}

theory T1R2
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta es relación formalizar y demostrar la corrección
  de los argumentos usando sólo las reglas básicas de deducción natural
  de la lógica proposicional (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
  --------------------------------------------------------------------- 
*}

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

text {* --------------------------------------------------------------- 
  Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Cuando tanto la temperatura como la presión atmosférica permanecen
     contantes, no llueve. La temperatura permanece constante. Por lo
     tanto, en caso de que llueva, la presión atmosférica no permanece
     constante. 
  Usar T para "La temperatura permanece constante",
       P para "La presión atmosférica permanece constante" y
       L para "Llueve".
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_1_1:
  "⟦T ∧ P ⟶ ¬L; T⟧ ⟹ L ⟶ ¬P"
by auto

-- "La demostración estructurada es"
lemma ejercicio_1_2:
  assumes "T ∧ P ⟶ ¬L"
          "T"
  shows   "L ⟶ ¬P"
proof
  assume "L"
  show "¬P"
  proof
    assume "P"
    with `T` have "T ∧ P" ..
    with assms(1) have "¬L" ..
    thus "False" using `L` .. 
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_1_3:
  assumes "T ∧ P ⟶ ¬L"
          "T"
  shows   "L ⟶ ¬P"
proof (rule impI)
  assume "L"
  show "¬P"
  proof
    assume "P"
    with `T` have "T ∧ P" by (rule conjI)
    with assms(1) have "¬L" by (rule mp)
    thus "False" using `L` by (rule notE)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Siempre que un número x es divisible por 10, acaba en 0. El número
     x no acaba en 0. Por lo tanto, x no es divisible por 10. 
  Usar D para "el número es divisible por 10" y
       C para "el número acaba en cero".
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_2_1:
  "⟦C ⟶ D; ¬D⟧ ⟹ ¬C"
by auto

-- "La demostración estructurada es"
lemma ejercicio_2_2:
  assumes "C ⟶ D" 
          "¬D"
  shows   "¬C"
proof 
  assume "C"
  with assms(1) have "D" .. 
  with assms(2) show False ..
qed

-- "La demostración detallada es"
lemma ejercicio_2_3:
  assumes "C ⟶ D" 
          "¬D"
  shows   "¬C"
proof 
  assume "C"
  with assms(1) have "D" by (rule mp)
  with assms(2) show False by (rule notE)
qed

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

-- "La demostración automática es"
lemma ejercicio_3_1:
  assumes "A ⟶ (M ⟷ ¬B)"
          "A ∨ B"
  shows   "¬B ⟶ M"
using assms
by auto

-- "La demostración estructurada es"
lemma ejercicio_3_2:
  assumes "A ⟶ (M ⟷ ¬B)"
          "A ∨ B"
  shows   "¬B ⟶ M"
proof
  assume "¬B"
  note `A ∨ B`
  hence "A"
  proof
    assume "A"
    thus "A" .
  next
    assume "B"
    with `¬B` show "A" .. 
  qed
  have "M ⟷ ¬B" using assms(1) `A` ..
  thus "M" using `¬B` ..
qed

-- "La demostración detallada es"
lemma ejercicio_3_3:
  assumes "A ⟶ (M ⟷ ¬B)"
          "A ∨ B"
  shows   "¬B ⟶ M"
proof (rule impI)
  assume "¬B"
  note `A ∨ B`
  hence "A"
  proof (rule disjE)
    assume "A"
    thus "A" by this
  next
    assume "B"
    with `¬B` show "A" by (rule notE)
  qed
  have "M ⟷ ¬B" using assms(1) `A` by (rule mp)
  thus "M" using `¬B` by (rule iffD2)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 4. Formalizar, y demostrar la corrección, del siguiente
  argumento
     Si no está el mañana ni el ayer escrito, entonces no está el mañana
     escrito. 
  Usar M: El mañana está escrito.
       A: El ayer está escrito.
  ------------------------------------------------------------------ *}

-- "La demostración automática es:"
lemma ejercicio_4_1:
  "¬M ∧ ¬A ⟹ ¬M"
by auto

-- "La demostración estructurada es:"
lemma ejercicio_4_2:
  assumes "¬M ∧ ¬A"
  shows   "¬M"
using assms ..

-- "La demostración detallada es:"
lemma ejercicio_4_3:
  assumes "¬M ∧ ¬A"
  shows   "¬M"
using assms by (rule conjunct1)

text {* --------------------------------------------------------------- 
  Ejercicio 5. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Me matan si no trabajo y si trabajo me matan. Me matan siempre me
     matan. 
  Usar M: Me matan.
       T: Trabajo.
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_5_1: 
  "(¬T ⟶ M) ∧ (T ⟶ M) ⟹ M"
by auto

-- "La demostración estructurada es"
lemma ejercicio_5_2: 
  assumes "(¬T ⟶ M) ∧ (T ⟶ M)" 
  shows   "M"
proof - 
  have "¬T ∨ T" ..
  thus "M"
  proof
    assume "¬T"
    have "¬T ⟶ M" using assms ..
    thus "M" using `¬T` ..
  next
    assume "T"
    have "T ⟶ M" using assms ..
    thus "M" using `T` ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_5_3: 
  assumes "(¬T ⟶ M) ∧ (T ⟶ M)" 
  shows   "M"
proof - 
  have "¬T ∨ T" by (rule excluded_middle)
  thus "M"
  proof (rule disjE)
    assume "¬T"
    have "¬T ⟶ M" using assms by (rule conjunct1)
    thus "M" using `¬T` by (rule mp)
  next
    assume "T"
    have "T ⟶ M" using assms by (rule conjunct2)
    thus "M" using `T` by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si te llamé por teléfono, entonces recibiste mi llamada y no es
     cierto que no te avisé del peligro que corrías. Por consiguiente,
     como te llamé, es cierto que te avisé del peligro que corrías.
  Usar T: Te llamé por teléfono.
       R: Recibiste mi llamada.
       P: Te avisé del peligro que corrías.
  ------------------------------------------------------------------ *}

-- "La demostración automática es:"
lemma ejercicio_6_1:
  "T ⟶ R ∧ ¬¬A ⟹ T ⟶ A"
by auto

-- "La demostración estructurada es:"
lemma ejercicio_6_2:
  assumes "T ⟶ R ∧ ¬¬A" 
  shows   "T ⟶ A"
proof
  assume "T"
  with assms have "R ∧ ¬¬A" ..
  hence "¬¬A" ..
  thus "A" by (rule notnotD)
qed

-- "La demostración detallada es:"
lemma ejercicio_6_3:
  assumes "T ⟶ R ∧ ¬¬A" 
  shows   "T ⟶ A"
proof (rule impI)
  assume "T"
  with assms(1) have "R ∧ ¬¬A" by (rule mp)
  hence "¬¬A" by (rule conjunct2)
  thus "A" by (rule notnotD)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si no hay control de nacimientos, entonces la población crece
     ilimitadamente; pero si la población crece ilimitadamente,
     aumentará el índice de pobreza. Por consiguiente, si no hay control
     de nacimientos, aumentará el índice de pobreza. 
  Usar N: Hay control de nacimientos. 
       P: La población crece ilimitadamente,
       I: Aumentará el índice de pobreza. 
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_7_1:
  "⟦¬N ⟶ P; P ⟶ I⟧ ⟹ ¬N ⟶ I"
by auto

-- "La demostración estructurada es"
lemma ejercicio_7_2:
  assumes "¬N ⟶ P" 
          "P ⟶ I" 
  shows   "¬N ⟶ I"
proof
  assume "¬N"
  with assms(1) have "P" ..
  with assms(2) show "I" ..
qed

-- "La demostración detallada es"
lemma ejercicio_7_3:
  assumes "¬N ⟶ P" 
          "P ⟶ I" 
  shows   "¬N ⟶ I"
proof (rule impI)
  assume "¬N"
  with assms(1) have "P" by (rule mp)
  with assms(2) show "I" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si el general era leal, hubiera obedecido las órdenes, y si era
     inteligente las hubiera comprendido. O el general desobedeció las
     órdenes o no las comprendió. Luego, el general era desleal o no era
     inteligente. 
  Usar L:  El general es leal.
       Ob: El general obedece las órdenes.
       I:  El general es inteligente.
       C:  El general comprende las órdenes.
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_8_1:
  "⟦(L ⟶ Ob) ∧ (I ⟶ C); ¬Ob ∨ ¬C⟧ ⟹ ¬L ∨ ¬I"
by auto

-- "La demostración estructurada es"
lemma ejercicio_8_2:
  assumes "(L ⟶ Ob) ∧ (I ⟶ C)" 
          "¬Ob ∨ ¬C" 
  shows   "¬L ∨ ¬I"
using assms(2)
proof
  assume "¬Ob"
  have "L ⟶ Ob" using assms(1) ..
  hence "¬L" using `¬Ob` by (rule mt)
  thus "¬L ∨ ¬I" ..
next
  assume "¬C"
  have "I ⟶ C" using assms(1) ..
  hence "¬I" using `¬C` by (rule mt)
  thus "¬L ∨ ¬I" ..
qed

-- "La demostración detallada es"
lemma ejercicio_8_3:
  assumes "(L ⟶ Ob) ∧ (I ⟶ C)" 
          "¬Ob ∨ ¬C" 
  shows   "¬L ∨ ¬I"
using assms(2)
proof (rule disjE)
  assume "¬Ob"
  have "L ⟶ Ob" using assms(1) by (rule conjunct1)
  hence "¬L" using `¬Ob` by (rule mt)
  thus "¬L ∨ ¬I" by (rule disjI1)
next
  assume "¬C"
  have "I ⟶ C" using assms(1) by (rule conjunct2)
  hence "¬I" using `¬C` by (rule mt)
  thus "¬L ∨ ¬I" by (rule disjI2)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo
     haría. Si Dios fuera incapaz de evitar el mal, no sería
     omnipotente; si no quisiera evitar el mal sería malévolo. Dios no
     evita el mal. Si Dios existe, es omnipotente y no es
     malévolo. Luego, Dios no existe. 
  Usar C:  Dios es capaz de evitar el mal.
       Q:  Dios quiere evitar el mal.
       Om: Dios es omnipotente.
       M:  Dios es malévolo.
       P:  Dios evita el mal.
       E:  Dios existe.
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_9_1:
  "⟦C ∧ Q ⟶ P; (¬C ⟶ ¬Om) ∧ (¬Q ⟶ M); ¬P; E ⟶ Om ∧ ¬M⟧ ⟹ ¬E"
by auto

-- "La demostración estructurada es"
lemma ejercicio_9_2:
  assumes "C ∧ Q ⟶ P" 
          "(¬C ⟶ ¬Om) ∧ (¬Q ⟶ M)" 
          "¬P" 
          "E ⟶ Om ∧ ¬M" 
  shows   "¬E"
proof
  assume "E"
  have "Om ∧ ¬M" using assms(4) `E` ..
  hence "Om" ..
  hence "¬¬Om" by (rule notnotI)
  have "¬C ⟶ ¬Om" using assms(2) ..
  hence "¬¬C" using `¬¬Om` by (rule mt)
  hence "C" by (rule notnotD)
  have "¬M" using `Om ∧ ¬M` ..
  have "¬Q ⟶ M" using assms(2) ..
  hence "¬¬Q" using `¬M` by (rule mt)
  hence "Q" by (rule notnotD)
  with `C` have "C ∧ Q" ..
  with assms(1) have "P" ..
  with assms(3) show False ..
qed

-- "La demostración detallada es"
lemma ejercicio_9_3:
  assumes "C ∧ Q ⟶ P" 
          "(¬C ⟶ ¬Om) ∧ (¬Q ⟶ M)" 
          "¬P" 
          "E ⟶ Om ∧ ¬M" 
  shows   "¬E"
proof (rule notI)
  assume "E"
  with assms(4) have "Om ∧ ¬M" by (rule mp)
  hence "Om" by (rule conjunct1)
  hence "¬¬Om" by (rule notnotI)
  have "¬C ⟶ ¬Om" using assms(2) by (rule conjunct1)
  hence "¬¬C" using `¬¬Om` by (rule mt)
  hence "C" by (rule notnotD)
  have "¬M" using `Om ∧ ¬M` by (rule conjunct2)
  have "¬Q ⟶ M" using assms(2) by (rule conjunct2)
  hence "¬¬Q" using `¬M` by (rule mt)
  hence "Q" by (rule notnotD)
  with `C` have "C ∧ Q" by (rule conjI)
  with assms(1) have "P" by (rule mp)
  with assms(3) show False by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 10. 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 : Se aceptan órdenes del operador.
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_10_1:
  "⟦A ∨ P ⟶ R ∧ F; F ∨ N ⟶ Or⟧ ⟹ A ⟶ Or"
by auto  

-- "La demostración estructurada es"
lemma ejercicio_10_2:
  assumes "A ∨ P ⟶ R ∧ F" 
          "F ∨ N ⟶ Or" 
  shows   "A ⟶ Or"
proof
  assume "A"
  hence "A ∨ P" ..
  with assms(1) have "R ∧ F" ..
  hence "F" ..
  hence "F ∨ N" ..
  with assms(2) show "Or" ..
qed

-- "La demostración detallada es"
lemma ejercicio_10_3:
  assumes "A ∨ P ⟶ R ∧ F" 
          "F ∨ N ⟶ Or" 
  shows   "A ⟶ Or"
proof (rule impI)
  assume "A"
  hence "A ∨ P" by (rule disjI1)
  with assms(1) have "R ∧ F" by (rule mp)
  hence "F" by (rule conjunct2)
  hence "F ∨ N" by (rule disjI1)
  with assms(2) show "Or" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 11. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si trabajo gano dinero, pero si no trabajo gozo de la vida. Sin
     embargo, si trabajo no gozo de la vida, mientras que si no trabajo
     no gano dinero. Por lo tanto, gozo de la vida si y sólo si no gano
  dinero. 
  Usar p: Trabajo
       q: Gano dinero.
       r: Gozo de la vida.
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_11_1:
  "⟦(p ⟶ q) ∧ (¬p ⟶ r); (p ⟶ ¬r) ∧ (¬p ⟶ ¬q)⟧ ⟹ r ⟷ ¬q"  
by auto

-- "La demostración estructurada es"
lemma ejercicio_11_2:
  assumes "(p ⟶ q) ∧ (¬p ⟶ r)" 
          "(p ⟶ ¬r) ∧ (¬p ⟶ ¬q)" 
  shows   "r ⟷ ¬q"  
proof
  assume "r"
  hence "¬¬r" by (rule notnotI)
  have "p ⟶ ¬r" using assms(2) ..
  hence "¬p" using `¬¬r` by (rule mt)
  have "¬p ⟶ ¬q" using assms(2) ..
  thus "¬q" using `¬p` ..
next
  assume "¬q"
  have "p ⟶ q" using assms(1) ..
  hence "¬p" using `¬q` by (rule mt)
  have "¬p ⟶ r" using assms(1) ..
  thus "r" using  `¬p` ..
qed

-- "La demostración detallada es"
lemma ejercicio_11_3:
  assumes "(p ⟶ q) ∧ (¬p ⟶ r)" 
          "(p ⟶ ¬r) ∧ (¬p ⟶ ¬q)" 
  shows   "r ⟷ ¬q"  
proof (rule iffI)
  assume "r"
  hence "¬¬r" by (rule notnotI)
  have "p ⟶ ¬r" using assms(2) by (rule conjunct1)
  hence "¬p" using `¬¬r` by (rule mt)
  have "¬p ⟶ ¬q" using assms(2) by (rule conjunct2)
  thus "¬q" using `¬p` by (rule mp)
next
  assume "¬q"
  have "p ⟶ q" using assms(1) by (rule conjunct1)
  hence "¬p" using `¬q` by (rule mt)
  have "¬p ⟶ r" using assms(1) by (rule conjunct2)
  thus "r" using  `¬p` by (rule mp)
qed

end
</source>