<source lang="isar">
header {* 1ª relación de ejercicios *}

theory Relacion_1
imports Main
begin

text {*
---------------------------------------------------------------------
Demostrar los siguientes lemas usando sólo las reglas básicas de
deducción natural de la lógica proposicional.
---------------------------------------------------------------------
*}

lemma I: "A ⟶ A"
by (rule imp_refl)

-- "Se puede hacer automáticamente"
lemma I_d2: "A ⟶ A"
by auto

-- "Otra forma (más explicita)"
lemma I_d3: "A ⟶ A"
proof (rule impI)
assume 1: "A"
qed

lemma
assumes 1:"A ∧ B"
shows "B ∧ A"
proof -
from 1 have 2:"A" by (rule conjunct1)
from 1 have 3:"B" by (rule conjunct2)
from 3 2 show "B ∧ A" by (rule conjI)
qed

-- "El ejercicio anterior hecho de un modo
automático (dado que no es posible hacerlo
por auto, es un buen candidato a que lo
resuelvan otros demostradores automáticos
proposicionales)"
lemma
assumes 1:"A ∧ B"
shows "B ∧ A"
by (metis 1)

lemma "A ∧ B ⟶ A ∨ B"
proof
assume "A ∧ B"
hence "A" ..
thus "A ∨ B" ..
qed

-- "El anterior lemma
demostrado de forma aún más breve"
lemma "A ∧ B ⟶ A ∨ B"
by simp

lemma
assumes 1:"(A ∨ B) ∨ C"
shows "A ∨ ( B ∨ C)"
proof -
note 1
moreover
{ assume 2: "C"
from 2 have 3:"B ∨ C" by (rule disjI2)
from 3 have "A ∨ (B ∨ C)" by (rule disjI2)}
moreover
{ assume 4: "A ∨ B"
from 4 have "(A ∨ B) ∨ C" by (rule disjI1) }
ultimately show "A ∨ (B ∨ C) " by (simp)
qed

-- Otra forma (más explícita)
lemma version2: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
proof
assume 1: "(A ∨ B) ∨ C"
show "A ∨ (B ∨ C)"
proof -
note 1
moreover{
assume 2: "A ∨ B"
have "A ∨ (B ∨ C)"
proof -
note 2
moreover{
assume 3: "A"
from 3 have 4:"A ∨ (B ∨ C)" by (rule disjI1)
}
moreover{
assume 5:"B"
from 5 have 6: "B ∨ C" by (rule disjI1)
from 6 have 7: "A ∨ (B ∨ C)" by (rule disjI2)
}
ultimately show "A ∨ (B ∨ C)" by (rule disjE)
qed
}
moreover{
assume 8: "C"
from 8 have 9: "B ∨ C" by (rule disjI2)
from 9 have "A ∨ (B ∨ C)" by (rule disjI2)
}
ultimately show "A ∨ (B ∨ C)" by (rule disjE)
qed
qed

-- La versión anterior de la propiedad asociativa de la
disyunción (es decir, en forma de proposición implicativa)
demostrada de forma muy automática y breve.
lemma version2: "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
by auto

-- Otra versión. la sentencia "note" no es necesaria.

lemma "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
proof
assume 1: "(A ∨ B) ∨ C"
moreover
{ assume 4: "(A ∨ B)"
moreover
{ assume 5: "A"
from 5 have 6: "A ∨ (B ∨ C)" by (rule disjI1)}
moreover
{ assume 7: "B"
from 7 have 8: "(B ∨ C)" by (rule disjI1)
from 8 have 9: "A ∨ (B ∨ C)" by (rule disjI2)}
ultimately have "A ∨ (B ∨ C)" by (rule disjE)}
moreover
{ assume 2: "C"
from 2 have 3: "(B ∨ C)" by (rule disjI2)
from 3 have "A ∨ (B ∨ C)" by (rule disjI2)}
ultimately show "A ∨ (B ∨ C)" by (rule disjE)
qed

lemma Aux:
assumes "A"
shows "B ⟶ A"
using assms by simp

lemma K: "A ⟶ (B ⟶ A)"
proof
assume 1: "A"
from 1 show "B ⟶ A" by (rule Aux)
qed

-- "Éste también se puede
obtener de forma totalmente
automática"
lemma K: "A ⟶ (B ⟶ A)"
by auto

lemma "(A ⟶ (B ⟶C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
proof
assume 1:"A ⟶ (B ⟶ C)"
show "(A ⟶ B) ⟶ (A ⟶C)"
proof
assume 2:"(A ⟶ B)"
show "A ⟶C"
proof
assume 3:"A"
from 2 3 have 4:"B" by (rule mp)
from 1 3 have 5:"B ⟶ C" by (rule mp)
from 5 4 show "C" by (rule mp)
qed
qed
qed

-- "Por simplificación es inmediata
su justificación"
lemma "(A ⟶ (B ⟶C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
by auto

lemma "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
proof
assume 1:"(A ⟶ B)"
show "((B ⟶ C) ⟶ (A ⟶ C))"
proof
assume 2:"(B ⟶ C)"
show "(A ⟶ C)"
proof
assume 3:"A"
from 1 3 have 4:"B" by (rule mp)
from 2 4 show "C" by (rule mp)
qed
qed
qed

-- "También se puede obtener directamente
por simplificación"
lemma "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
by simp

lemma "¬¬A ⟶ A"
proof
assume 1:"¬¬A"
from 1 show "A" by (rule notnotD)
qed

-- "Está claro que éste sale
por auto y por simp"
lemma "¬¬A ⟶ A"
by simp

lemma "A ⟶ ¬¬A"
proof
assume 1:"A"
from 1 show "¬¬A" by (rule contrapos_pn)
qed

lemma MT:
assumes 1:"F ⟶ G" and 2:"¬G"
shows "¬F"
proof (rule notI)
assume 3:"F"
from 1 and 3 have 4:"G" by (rule mp)
from 2 and 4 show False by (rule notE)
qed

lemma "(¬A ⟶ B) ⟶ (¬B ⟶ A)"
proof
assume 1:"(¬A ⟶ B)"
show "(¬B ⟶ A)"
proof
assume 2:"¬B"
from 1 2 have 3:"¬¬A" by (rule MT)
from 3 show "A" by (rule notnotD)
qed
qed

lemma "((A ⟶ B) ⟶ A) ⟶ A"
proof
assume 1: "(A ⟶ B) ⟶ A"
have 8: "¬¬A"
proof (rule notI)
assume 2: "¬A"
have 3: "A ⟶ B"
proof (rule impI)
assume 4: "A"
from 2 and 4 show "B" by (rule notE)
qed
from 1 and 3 have 5: "A" by (rule mp)
from 2 and 5 show False by (rule notE)
qed
from 8 show "A" by (rule notnotD)
qed

-- "Éste sale por auto pero no
por el método simp"
lemma "((A ⟶ B) ⟶ A) ⟶ A"
by auto

lemma "A ∨ ¬A"
proof cases
assume "A" thus ?thesis ..
next
assume "¬A" thus ?thesis ..
qed

-- "Demostración aún más corta
y automática"
lemma "A ∨ ¬A"
by simp

lemma "(¬(A ∧ B)) = (¬A ∨ ¬B)"
proof
{
assume 1: "¬(A ∧ B)"
have 2: "¬A ∨ A" by (rule excluded_middle)
thus "¬A ∨ ¬B"
proof (rule disjE)
{ assume 3: "¬A"
thus "¬A ∨ ¬B" by (rule disjI1) }
next
{ assume 4: "A"
have 5: "¬B ∨ B" by (rule excluded_middle)
thus "¬A ∨ ¬B"
proof (rule disjE)
{assume 6: "¬B"
thus "¬A ∨ ¬B" by (rule disjI2) }
next
{assume 7: "B"
from 4 and 7 have 8: "A ∧ B" by (rule conjI)
from 1 and 8 show "¬A ∨ ¬B" by (rule notE) }
qed
}
qed
}
next
{ assume 1: "¬A ∨ ¬B"
show "¬(A ∧ B)"
proof (rule notI)
assume 2: "A ∧ B"
from 1 have 3:"¬A ∨ ¬B" .
moreover
{ assume 4: "¬A"
from 2 have 5:"A" by (rule conjunct1)
from 4 and 5 have False by (rule notE) }
moreover
{ assume 6: "¬B"
from 2 have 7: "B" by (rule conjunct2)
from 6 and 7 have False by (rule notE) }
ultimately show False by (rule disjE)
qed

}
qed

-- "Si no queremos entrar en detalles
lo podríamos mandar a la 'maza'"
lemma "(¬(A ∧ B)) = (¬A ∨ ¬B)"
by metis

end
</source>

Relación 2

2011-02-03T19:36:04Z

Jmuros: