Relación 1

header {* 1ª relación de ejercicios *}

theory Relacion_1
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  Demostrar los siguientes lemas usando sólo las reglas básicas de
  deducción natural de la lógica proposicional.
  --------------------------------------------------------------------- 
*}

lemma ej1_d1: "A ⟶ A"
by (rule imp_refl)

-- "Se puede hacer automáticamente"
lemma ej1_d2: "A ⟶  A"
by auto

-- "Otra forma (más explicita)"
lemma ej1_d3: "A ⟶ A"
proof (rule impI)
  assume 1: "A"
qed

lemma ej2_d1:
  assumes 1:"A ∧ B" 
  shows "B ∧ A" 
proof -
  from 1 have 2:"A" by (rule conjunct1)
  from 1 have 3:"B" by (rule conjunct2)
  from 3 2 show "B ∧ A" by (rule conjI)
qed

text {* 
  El ejercicio anterior hecho de un modo automático (dado que no es
  posible hacerlo por auto, es un buen candidato a que lo resuelvan
  otros demostradores automáticos proposicionales
*}

lemma ej2_d2:
  assumes 1:"A ∧ B" 
  shows  "B ∧ A" 
by (metis 1) 

text {*
  Comentario de J.A. Alonso: El ejercicio 2 puede resolverse por
  auto. 
*}

lemma ej3_d1: "A ∧ B ⟶ A ∨ B"
proof
  assume "A ∧ B"
  hence "A" ..
  thus "A ∨ B" ..
qed

-- "Otra versión"
lemma ej3_d2: "A ∧ B ⟶ A ∨ B"
proof
  assume 1: "A ∧ B"
  from 1 have 2: "A" by (rule conjunct1)
  from 2 show "A ∨ B" by (rule disjI1)
qed

lemma ej4_d1:
  assumes 1:"(A ∨ B) ∨ C"
  shows "A ∨ (B ∨ C)"
proof -
note 1
 moreover
 { assume 2: "C"
   from 2 have 3:"B ∨ C" by (rule disjI2) 
   from 3 have "A ∨ (B ∨ C)" by (rule disjI2)}
 moreover
 { assume 4: "A ∨ B"
   from 4 have "(A ∨ B) ∨ C" by (rule disjI1) }
ultimately show "A ∨ (B ∨ C) " by simp
qed

-- "Otra forma (más explícita)"
lemma ej4_d2: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
proof
  assume 1: "(A ∨ B) ∨ C"
  show "A ∨ (B ∨ C)"
  proof -
    note 1
    moreover{
      assume 2: "A ∨ B"
      have "A ∨ (B ∨ C)"
        proof -
          note 2
          moreover{
            assume 3: "A"
            from 3 have 4:"A ∨ (B ∨ C)" by (rule disjI1)
          }
          moreover{
            assume 5:"B"
            from 5 have 6: "B ∨ C" by (rule disjI1)
            from 6 have 7: "A ∨ (B ∨ C)" by (rule disjI2)
          }
          ultimately show "A ∨ (B ∨ C)" by (rule disjE)
        qed
      }
      moreover{
        assume 8: "C"
        from 8 have 9: "B ∨ C" by (rule disjI2)
        from 9 have "A ∨ (B ∨ C)" by (rule disjI2)
      }
      ultimately show "A ∨ (B ∨ C)" by (rule disjE)
    qed
qed

text {*
  Comentario de J.A. Alonso: El enunciado de ej4_d2 no es exactamente
  el mismo que el original y la demostración es demasiado larga. 
*}

text {* 
  La versión anterior de la propiedad asociativa de la disyunción (es
  decir, en forma de proposición implicativa) demostrada de forma muy
  automática y breve. 
*}

lemma ej4_d3: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
by auto

text {*
  Comentario de J.A. Alonso: El enunciado de ej4_d3 no es exactamente
  el mismo que el original.
*}

-- "Otra versión. la sentencia note no es necesaria."
lemma ej4_d4: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
proof
  assume 1: "(A ∨ B) ∨ C"
   moreover
  { assume 4: "(A ∨ B)"
    moreover
    { assume 5: "A"
      from 5 have 6: "A ∨ (B ∨ C)" by (rule disjI1)}
    moreover
    { assume 7: "B"
      from 7 have 8: "(B ∨ C)" by (rule disjI1)
      from 8 have 9: "A ∨ (B ∨ C)" by (rule disjI2)}
    ultimately have "A ∨ (B ∨ C)" by (rule disjE)}
  moreover
  { assume 2: "C"
    from 2 have 3: "(B ∨ C)" by (rule disjI2)
    from 3 have "A ∨ (B ∨ C)" by (rule disjI2)}
  ultimately show "A ∨ (B ∨ C)" by (rule disjE)
qed

text {*
  Comentario de J.A. Alonso: El enunciado de ej4_d4 no es exactamente
  el mismo que el original y la demostración es demasiado larga. 
*}

lemma ej5_aux:
  assumes "A"
  shows "B ⟶ A"
using assms 
by simp

lemma ej5_d1: "A ⟶ (B ⟶ A)"
proof
  assume 1: "A"
  from 1 show "B ⟶ A" by (rule ej5_aux)
qed

text {*
  Comentario de J.A. Alonso: En la prueba anterior puede eliminarse la
  etiqueta. 
*}

-- "Éste también se puede obtener de forma totalmente automática."
lemma ej5_d2: "A ⟶ (B ⟶ A)"
by auto

lemma ej6_d1: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
proof
  assume 1:"A ⟶ (B ⟶ C)"
  show "(A ⟶ B) ⟶ (A ⟶ C)"
    proof
      assume 2:"(A ⟶ B)"
      show "A ⟶ C"
      proof
        assume 3:"A"
        from 2 3 have 4:"B" by (rule mp)
        from 1 3 have 5:"B ⟶ C" by (rule mp)
        from 5 4 show "C" by (rule mp)
      qed
    qed
qed

-- "Por simplificación es inmediata su justificación"
lemma ej6_d2: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
by auto

lemma ej7_d1: "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
proof
  assume 1:"A ⟶ B"
  show "(B ⟶ C) ⟶ (A ⟶ C)"
  proof 
    assume 2:"B ⟶ C"
    show "A ⟶ C"
    proof
      assume 3:"A"
      from 1 3 have 4:"B" by (rule mp)
      from 2 4 show "C" by (rule mp)
    qed
  qed
qed

-- "Por simplificación es inmediata su justificación"
lemma ej7_d2: "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
by simp

lemma ej8_d1: "¬¬A ⟶ A"
proof
  assume 1:"¬¬A"
  from 1 show "A" by (rule notnotD)
qed

-- "Está claro que éste sale por auto y por simp"
lemma ej8_d2: "¬¬A ⟶ A"
by simp

lemma ej9_d1: "A ⟶ ¬¬A"
proof
  assume 1:"A"
  from 1 show "¬¬A" by (rule contrapos_pn)
qed

text {*
  Comentario de J.A. Alonso: Puede demostrase sin etiquetas.
*}

lemma MT: -- "ej10"
  assumes 1:"F ⟶ G" and 2:"¬G"
  shows "¬F"
proof (rule notI)
  assume 3:"F"
  from 1 and 3 have 4: "G" by (rule mp)
  from 2 and 4 show False by (rule notE)
qed

lemma ej11_d1: "(¬A ⟶ B) ⟶ (¬B ⟶ A)"
proof
  assume 1:"(¬A ⟶ B)"
  show "¬B ⟶ A"
  proof
    assume 2:"¬B"
    from 1 2 have 3:"¬¬A" by (rule MT)
    from 3 show "A" by (rule notnotD)
  qed
qed

lemma ej12_d1: "((A ⟶ B) ⟶ A) ⟶ A"
proof
  assume 1: "(A ⟶ B) ⟶ A"
  have 8: "¬¬A"
  proof (rule notI)
    assume 2: "¬A"
    have 3: "A ⟶ B"
    proof (rule impI)
      assume 4: "A"
      from 2 and 4 show "B" by (rule notE)
    qed
    from 1 and 3 have 5: "A" by (rule mp)
    from 2 and 5 show False by (rule notE)
  qed
  from 8 show "A" by (rule notnotD)
qed

-- "Éste sale por auto pero no por el método simp"
lemma ej12_d2: "((A ⟶ B) ⟶ A) ⟶ A"
by auto

lemma ej13_d1: "A ∨ ¬A"
proof cases
  assume "A" thus ?thesis ..
next
  assume "¬A" thus ?thesis ..
qed

-- "Demostración aún más corta y automática"
lemma ej13_d2: "A ∨ ¬A"
by simp

lemma ej14_d1: "(¬(A ∧ B)) = (¬A ∨ ¬B)"
proof
  {
  assume 1: "¬(A ∧ B)"
  have 2: "¬A ∨ A" by (rule excluded_middle)
  thus "¬A ∨ ¬B"
    proof (rule disjE)
      { assume 3: "¬A"
        thus  "¬A ∨ ¬B" by (rule disjI1) }
    next
      { assume 4: "A"
        have 5: "¬B ∨ B" by (rule excluded_middle)
        thus "¬A ∨ ¬B"
        proof (rule disjE)
          {assume 6: "¬B"
            thus "¬A ∨ ¬B" by (rule disjI2) }
          next
          {assume 7: "B"
             from 4 and 7 have 8: "A ∧ B" by (rule conjI)
             from 1 and 8 show "¬A ∨ ¬B" by (rule notE) }
        qed
      }      
    qed
  }
next
  { assume 1: "¬A ∨ ¬B"
    show "¬(A ∧ B)"
    proof (rule notI)
      assume 2: "A ∧ B"
      from 1 have 3:"¬A ∨ ¬B" .
      moreover
      { assume 4: "¬A"
        from 2 have 5:"A" by (rule conjunct1)
        from 4 and 5 have False by (rule notE) }
      moreover
      { assume 6: "¬B"
        from 2 have 7: "B" by (rule conjunct2)
        from 6 and 7 have False by (rule notE) }
      ultimately show False by (rule disjE)        
    qed
  }
qed

-- "Si no queremos entrar en detalles lo podríamos mandar a la 'maza'"
lemma ej14_d2: "(¬(A ∧ B)) = (¬A ∨ ¬B)"
by metis

end