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

lemma ejercicio_2b:
assumes "¬A"
shows "A⟶ False"
proof
    assume "A"
    show "False" using assms `A` by (rule notE)
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.   
  ------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo. Usaré el ejercicio 1 que ha puesto Pedro y el 3 que he puesto yo"

lemma ejercicio_4a:
assumes "(A ∨ B ∧ C) ⟷ A"
shows "(((A ⟶ False) ⟶ B ∧ C) ⟶ A) ∧ (A⟶((A ⟶ False)⟶ B ∧ C))"
proof -
  have 1: "((A ∨ B ∧ C) ⟶ A) ∧ (A ⟶ (A ∨ B ∧ C))" using assms by (rule ejercicio_1a)
  hence 2: "(A ∨ B ∧ C) ⟶ A"..
  have 3: "A ⟶ (A ∨ B ∧ C)" using 1..
  have 4: "((A ⟶ False) ⟶ B ∧ C) ⟶ A"
  proof
    assume "(A ⟶ False) ⟶ B ∧ C"
    hence 5: "A ∨ B ∧ C" by (rule ejercicio_3a)
    show "A"
    using 5
    proof 
      assume "A"
      thus "A".
      next
      assume "B ∧ C"
      hence "A ∨ B ∧ C"..
      with 2 show "A"..
    qed  
  qed  
  have 6: "A⟶((A ⟶ False)⟶ B ∧ C)"
  proof
    assume "A"
    with 3 have "A ∨ B ∧ C"..
    thus "(A ⟶ False)⟶ B ∧ C" by (rule ejercicio_3b)
  qed  
  show "(((A ⟶ False) ⟶ B ∧ C) ⟶ A) ∧ (A⟶((A ⟶ False)⟶ B ∧ C))" using 4 6..
qed

lemma ejercicio_4b:
assumes "(((A ⟶ False) ⟶ B ∧ C) ⟶ A) ∧ (A⟶((A ⟶ False)⟶ B ∧ C))"
shows "(A ∨ B ∧ C) ⟷ A"
proof 
  have 1: "((A ⟶ False) ⟶ B ∧ C) ⟷ A" using assms by (rule ejercicio_1b)
  {assume "A ∨ B ∧ C"
   hence "(A ⟶ False) ⟶ B ∧ C" by (rule ejercicio_3b)
   with 1 show "A"..}
  {assume "A"
   with 1 have "(A ⟶ False) ⟶ B ∧ C"..
   thus "A ∨ B ∧ C" by (rule ejercicio_3a)}
qed

end