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