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. 
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_2a:
assumes "(A⟶ False)"
shows "¬A"
using ccontr
proof
  assume "¬¬False"
  thus "False" by (rule notnotD)
  next
  show "¬A"
  proof (rule ccontr)
    assume "¬¬A"
    hence "A" by (rule notnotD)
    show "False" using assms `A` ..
  qed
qed


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. 
  ------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_3a:
assumes "(A ⟶ False) ⟶ B"
shows "A ∨ B"
proof (rule disjE)
  show "¬A ∨ A" by (rule excluded_middle)
  next
  assume "¬A"
    {assume "A"
     have False using `¬A` `A`..}
  hence "A ⟶ False"..
  with assms(1) have "B"..
  thus "A ∨ B"..
  next
  assume "A"
  thus "A ∨ B"..
qed 

lemma ejercicio_3b:
assumes "A ∨ B"
shows "(A ⟶ False) ⟶ B"
proof
  assume 1: "A ⟶ False"
  show "B" using assms(1)
  proof
    assume "A"
    with 1 have False..
    thus "B"..
    next
    assume "B"
    thus "B".
  qed
qed 

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