Ver el código de «Relación 7» - Razonamiento automático (2017-18)

<source lang="isar">
chapter {* R7: Deducción natural proposicional en Isabelle/HOL *}

theory R7_Deduccion_natural_proposicional
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
     ¬q ⟶ ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

(*anddonram*)
lemma ej_1:
  assumes 1: "¬q ⟶ ¬p"
   shows "p ⟶ q"
  proof (rule impI)
    assume 2: "p"
    show 3: "q"
    proof (rule ccontr)
      assume 4: "¬q"
      have 5: "¬p" using 1 4 by (rule impE)
      then show False using 2 by (rule notE)
    qed
qed

(*luicedval*)
lemma ej_1_2:
  assumes 1: "¬q ⟶ ¬p" 
  shows "p ⟶ q"
proof -
  { assume 2: "p"
    have 3: "¬¬p" using 2 by (rule notnotI)
    have 4: "¬¬q" using 1 3 by (rule mt) 
    have 5: "q" using 4 by (rule notnotD) } 
  thus "p ⟶ q" by (rule impI)
qed    

(* cesgongut *)
lemma impConv:
  assumes "¬q ⟶ ¬p"
  shows "p ⟶ q"
proof
  assume "p"
  then have "¬¬p" by (rule notnotI)
  have "¬¬q" using assms `¬¬p` by (rule mt)
  then show "q" by (rule notnotD)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------ *}

(*anddonram luicedval*)
lemma l_e_m:
  "F ∨ ¬F"
by auto

lemma ej_2:
  assumes 1:"¬(¬p ∧ ¬q)"
  shows "p ∨ q"
proof (rule disjE)
  { 
    assume 2: "q"
    show "p ∨ q" using 2 by (rule disjI2)
  }
  moreover{
    assume 4:"¬q"
    show "p ∨ q"
     proof(rule disjI1)
      show "p"
      proof (rule ccontr)
        assume 5:"¬p"
        then have "¬p ∧ ¬q" using 4 by (rule conjI)
        with 1 show False by (rule notE)
      qed
    qed
  }
  moreover
  show 1: "q ∨ ¬q" by (rule l_e_m)
qed

(* cesgongut *)
lemma conjnotDM1:
  assumes "¬(¬p ∧ ¬q)"
  shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
  have "p"
  proof (rule ccontr)
    assume "¬p"
    have "q"
    proof (rule ccontr)
      assume "¬q"
      have "¬p ∧ ¬q" using `¬p` `¬q` ..
      then show False using assms by contradiction
    qed
    then have "p ∨ q" by (rule disjI2)
    then show False using `¬(p ∨ q)` by contradiction
  qed
  then have "p ∨ q" by (rule disjI1)
  then show False using `¬(p ∨ q)` by contradiction
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}

(*anddonram luicedval cesgongut *)
lemma ej_3:
  assumes 1:" ¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof (rule conjI)
  show "p"
  proof (rule ccontr)
    assume "¬p"
    then have "(¬p ∨ ¬q)" by (rule disjI1)
    with 1 show False by (rule notE)
  qed
next
  show "q"
  proof (rule ccontr)
    assume "¬q"
    then have "(¬p ∨ ¬q)" by (rule disjI2)
    with 1 show False by (rule notE)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}

(*anddonram luicedval*)
lemma ej_4:
  assumes 1: "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof(rule disjE)
  {
    assume 2:"p"
    show "¬p ∨ ¬q"
    proof (rule disjI2)
      show "¬q"
      proof (rule notI)
        assume "q"
        with 2 have "p∧q" by (rule conjI)
        with 1 show False by (rule notE)
      qed
    qed
  }
  moreover
  {
    assume "¬p"
    then show "¬p ∨ ¬q" by (rule disjI1) 
  }
  moreover
  show 1: "p ∨ ¬p" by (rule l_e_m)
qed

(* cesgongut *)
lemma conjDM1:
  assumes "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof (rule ccontr)
  assume "¬(¬p ∨ ¬q)"
  then have "p ∧ q" by (rule ej_3)
  with assms show False by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
  ------------------------------------------------------------------ *}

(*anddonram luicedval*)
lemma ej_5:
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjE) 
  
  { 
    assume 2: "q"
    show "(p ⟶ q) ∨ (q ⟶ p)"
    proof(rule disjI1)
      show "p ⟶ q" using 2 by (rule impI)
    qed
  }
  moreover{
    assume 4:" ¬q"
    show "(p ⟶ q) ∨ (q ⟶ p)"
     proof(rule disjI2)
      show "q ⟶ p"
      proof (rule impI)
        assume 5:"q"
        with 4 show "p"  by (rule notE)
      qed
    qed
  }
  moreover
  show 1: "q ∨ ¬q" by (rule l_e_m)
qed

(* cesgongut *)
lemma disjDM1:
  assumes "¬(p ∨ q)"
  shows "¬p ∧ ¬q"
proof
  show "¬p" proof (rule notI)
    assume "p"
    then have "p ∨ q" ..
    then show False using assms by contradiction
  qed
  show "¬q" proof (rule notI)
    assume "q"
    then have "p ∨ q" ..
    then show False using assms by contradiction
  qed
qed

lemma notimpD1:
  assumes "¬(p ⟶ q)"
  shows "p ∧ ¬q"
proof
  show "¬q" proof (rule notI)
    assume "q"
    have "p ⟶ q" proof (rule impI)
      assume "p"
      show "q" proof (rule ccontr)
        assume "¬q"
        then show False using `q` by contradiction
      qed
    qed
    then show False using assms by contradiction
  qed
next
  show "p" proof (rule ccontr)
    assume "¬p"
    have "p ⟶ q" proof (rule impI)
      assume "p"
      show "q" proof (rule ccontr)
        assume "¬q"
        show False using `p` `¬p` by contradiction
      qed
    qed
    then show False using assms by contradiction
  qed
qed

lemma ej5b: "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
  assume "¬?thesis"
  then have "¬(p ⟶ q) ∧ ¬(q ⟶ p)" by (rule disjDM1)
  then have "¬(p ⟶ q)" ..
  then have "p ∧ ¬q" by (rule notimpD1)
  then have "p" ..
  have "¬(q ⟶ p)" using `¬(p ⟶ q) ∧ ¬(q ⟶ p)` ..
  then have "q ∧ ¬p" by (rule notimpD1)
  then have "¬p" ..
  then show False using `p` by contradiction
qed

end
</source>