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 I: "A ⟶ A"
by (rule imp_refl)

lemma 
  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

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

lemma
  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


lemma K: "A ⟶ (B ⟶ A)"
oops

lemma S: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
oops

lemma "(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

lemma "¬¬A ⟶ A"
oops

lemma "A ⟶ ¬¬A"
oops

lemma "(¬A ⟶ B) ⟶ (¬B ⟶ A)"
oops

lemma "((A ⟶ B) ⟶ A) ⟶ A"
oops

lemma "A ∨ ¬A"
oops

lemma "(¬(A ∧ B)) = (¬A ∨ ¬B)"
oops

end