Diferencia entre revisiones de «Relación 9»
De Razonamiento automático (2013-14)
(Página creada con '<source lang="isar"> header {* R9: Deducción natural proposicional (1) *} theory R9 imports Main begin text {* ------------------------------------------------------------...') |
|||
Línea 43: | Línea 43: | ||
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r) | p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r) | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | |||
+ | -- "irealetei" | ||
+ | lemma ej1_auto: | ||
+ | assumes "p ⟶ (q ⟶ r)" | ||
+ | shows "q ⟶ (p ⟶ r)" | ||
+ | using assms | ||
+ | by auto | ||
+ | |||
+ | lemma ej1: | ||
+ | assumes 1:"p ⟶ (q ⟶ r)" | ||
+ | shows "q ⟶ (p ⟶ r)" | ||
+ | proof - | ||
+ | {assume 2:"q" | ||
+ | {assume 3:"p" | ||
+ | have 4:"q⟶r" using 1 3 by (rule mp) | ||
+ | have 5:"r" using 4 2 by (rule mp)} | ||
+ | then have "p⟶r" by (rule impI)} | ||
+ | then show "q⟶(p⟶r)" by (rule impI) | ||
+ | qed | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 48: | Línea 67: | ||
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r) | p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r) | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | |||
+ | -- "irealetei" | ||
+ | lemma ej2_auto: | ||
+ | assumes " p ⟶ (q ⟶ r)" | ||
+ | shows "(p ⟶ q) ⟶ (p ⟶ r)" | ||
+ | using assms by auto | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 54: | Línea 79: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | -- "irealetei" | ||
+ | lemma ej3_auto:"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" | ||
+ | by auto | ||
+ | |||
+ | lemma ej3:"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" | ||
+ | proof - | ||
+ | { assume 1:"(p⟶(q⟶r))" | ||
+ | {assume 3:"p⟶q" | ||
+ | {assume 4:"p" | ||
+ | have 5: "q⟶r" using 1 4 by (rule mp) | ||
+ | have 6:"q" using 3 4 by (rule mp) | ||
+ | have 7:"r" using 5 6 by (rule mp)} | ||
+ | then have "p⟶r" by (rule impI)} | ||
+ | then have "(p⟶q)⟶p⟶r" by (rule impI)} | ||
+ | then show "(p⟶(q⟶r))⟶((p⟶q)⟶p⟶r)" by (rule impI) | ||
+ | qed | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 4. Demostrar | Ejercicio 4. Demostrar | ||
Línea 59: | Línea 100: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | -- "irealetei" | ||
+ | lemma ej4_auto: | ||
+ | assumes "(p ⟶ q) ⟶ r" | ||
+ | shows "p ⟶ (q ⟶ r)" | ||
+ | using assms by auto | ||
section {* Conjunciones *} | section {* Conjunciones *} | ||
Línea 65: | Línea 111: | ||
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r | (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | |||
+ | -- "irealetei" | ||
+ | lemma ej5_auto: | ||
+ | assumes "(p ⟶ q) ∧ (p ⟶ r)" | ||
+ | shows "p ⟶ q ∧ r" | ||
+ | using assms by auto | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 70: | Línea 122: | ||
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r) | p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r) | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | |||
+ | -- "irealetei" | ||
+ | lemma ej6_auto: | ||
+ | assumes "p ⟶ q ∧ r" | ||
+ | shows "(p ⟶ q) ∧ (p ⟶ r)" | ||
+ | using assms by auto | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 75: | Línea 133: | ||
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r | p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | |||
+ | -- "irealetei" | ||
+ | lemma ej7_auto: | ||
+ | assumes " p ∧ (q ⟶ r)" | ||
+ | shows "(p ⟶ q) ⟶ r" | ||
+ | using assms by auto | ||
section {* Disyunciones *} | section {* Disyunciones *} | ||
Línea 82: | Línea 146: | ||
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r | q ⟶ r ⊢ p ∨ q ⟶ p ∨ r | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | |||
+ | -- "irealetei" | ||
+ | lemma ej8_auto: | ||
+ | assumes "q ⟶ r" | ||
+ | shows "p ∨ q ⟶ p ∨ r" | ||
+ | using assms by auto | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 87: | Línea 157: | ||
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r | (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | |||
+ | -- "irealetei" | ||
+ | lemma ej9_auto: | ||
+ | assumes "(p ⟶ r) ∧ (q ⟶ r)" | ||
+ | shows "p ∨ q ⟶ r" | ||
+ | using assms by auto | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 93: | Línea 169: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
+ | -- "irealetei" | ||
+ | lemma ej10_auto: | ||
+ | assumes "p ∨ q ⟶ r" | ||
+ | shows "(p ⟶ r) ∧ (q ⟶ r)" | ||
+ | using assms by auto | ||
end | end | ||
</source> | </source> |
Revisión del 00:17 19 ene 2014
header {* R9: Deducción natural proposicional (1) *}
theory R9
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación es lemas usando sólo las reglas básicas
de deducción natural de la lógica proposicional.
Las reglas básicas de la deducción natural necesarias son las
siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬P ⟹ P
· notnotI: P ⟹ ¬¬P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
---------------------------------------------------------------------
*}
text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
section {* Implicaciones *}
text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej1_auto:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
using assms
by auto
lemma ej1:
assumes 1:"p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof -
{assume 2:"q"
{assume 3:"p"
have 4:"q⟶r" using 1 3 by (rule mp)
have 5:"r" using 4 2 by (rule mp)}
then have "p⟶r" by (rule impI)}
then show "q⟶(p⟶r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej2_auto:
assumes " p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej3_auto:"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
by auto
lemma ej3:"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof -
{ assume 1:"(p⟶(q⟶r))"
{assume 3:"p⟶q"
{assume 4:"p"
have 5: "q⟶r" using 1 4 by (rule mp)
have 6:"q" using 3 4 by (rule mp)
have 7:"r" using 5 6 by (rule mp)}
then have "p⟶r" by (rule impI)}
then have "(p⟶q)⟶p⟶r" by (rule impI)}
then show "(p⟶(q⟶r))⟶((p⟶q)⟶p⟶r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej4_auto:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
using assms by auto
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej5_auto:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej6_auto:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej7_auto:
assumes " p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
using assms by auto
section {* Disyunciones *}
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej8_auto:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej9_auto:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
-- "irealetei"
lemma ej10_auto:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
using assms by auto
end