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..
  show "((A ⟶ False) ⟶ B ∧ C) ⟶ A"
  proof
    assume "(A ⟶ False) ⟶ B ∧ C"
    hence "A ∨ B ∧ C" by (rule ejercicio_3a)
    with 2 show "A"..
  qed  
  show "A⟶((A ⟶ False)⟶ B ∧ C)"
  proof
    assume "A"
    with 3 have "A ∨ B ∧ C"..
    thus "(A ⟶ False)⟶ B ∧ C" by (rule ejercicio_3b)
  qed
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


text {* Pedro Ros.
Por si alguien tiene curiosidad, defino todas las conectivas con las dos que son maximales, las puertas lógicas NAND y NOR: *}

definition nand :: "bool ⇒ bool ⇒ bool" where
"(nand a b) = (¬( a ∧ b))"
declare nand_def[simp]

lemma negnand:
"(¬p) = (nand p p)"
by auto

lemma ynand:
"(p∧q) = (nand (nand p q) (nand p q))"
by auto

lemma onand:
"(p∨q) = (nand (nand p p) (nand q q))"
by auto

lemma impnand:
"(p⟶q)= (nand  p (nand q q))"
by auto

lemma siinand:
"(p⟷q)= (nand (nand (nand p (nand q q)) (nand (nand p p) q)) (nand (nand p (nand q q)) (nand (nand p p) q)))"
by auto

definition nor :: "bool ⇒ bool ⇒ bool" where
"(nor a b) = (¬( a ∨ b))"
declare nor_def[simp]

lemma negnor:
"(¬p)= (nor p p)"
by auto

lemma onor:
"(p∨q) = (nor (nor p q) (nor p q))"
by auto

lemma ynor:
"(p∧q) = (nor (nor p p) (nor q q))"
by auto

lemma impnor:
"(p⟶q) = (nor (nor (nor p p) q ) (nor (nor p p) q ))"
by auto


end