Relación 5

header {* R5: Eliminación de conectivas *}

theory R5
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta es relación es demostrar cómo a partir de las
  conectivas False, ∧ y ⟶ pueden definirse las restantes.
  --------------------------------------------------------------------- 
*}


text {* --------------------------------------------------------------- 
  Ejercicio 1. Definir ⟷ usando ∧ y ⟶; es decir, sustituir en
      (A ⟷ B) = indefinida
  la indefinida por una fórmula que sólo usa las conectivas ∧ y ⟷ y
  demostrar la equivalencia. 
  ------------------------------------------------------------------ *}
text {* Pedro Ros. Lo divido en dos subpruebas por resultarme más cómodo *}
lemma ejercicio_1a:
assumes 0: "(A ⟷ B)"
shows "(A⟶B)∧(B⟶A)"
proof -
have 1:"A⟶ B" using 0 ..
have 2:"B⟶A" using 0 ..
show "(A⟶B)∧(B⟶A)" using 1 2 ..
qed

lemma ejercicio_1b:
assumes "(A⟶B)∧(B⟶A)"
shows "(A ⟷ B)"
proof 
  assume A
  have 1: "(A⟶B)" using assms ..
  show B using 1 `A` ..
next
  assume B  
  have 2: "(B⟶A)" using assms ..
  show A using 2 `B` ..
qed
text {* --------------------------------------------------------------- 
  Ejercicio 2. Definir ¬ usando ⟶ y False; es decir, sustituir en
      (¬A) = indefinida
  la indefinida por una fórmula que sólo usa las conectivas ⟶ y False 
  y demostrar la equivalencia. 
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 3. Definir ∨ usando ⟶ y False; es decir, sustituir en
      (A ∨ B) = indefinida
  la indefinida por una fórmula que sólo usa las conectivas ⟶ y False 
  y demostrar la equivalencia. 
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 4. Encontrar una fórmula equivalente a 
     (A ∨ (B ∧ C)) ⟷ A
  que sólo use las conectivas False, ∧ y ⟶ y demostrar la 
  equivalencia.   
  ------------------------------------------------------------------ *}

end