Jalonso: Protegió «Tema 5: Patrones de demostración» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2012-11-20T17:47:20Z

Protegió «Tema 5: Patrones de demostración» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* Tema 5: Patrones de demostración } theory Tema_5 imports Main begin section { Demostraciones por casos } text { Nota. [Regla de elimin...'

2012-11-20T17:36:47Z

Página creada con '<source lang="isar"> header {* Tema 5: Patrones de demostración *} theory Tema_5 imports Main begin section {* Demostraciones por casos *} text {* Nota. [Regla de elimin...'

Página nueva

<source lang="isar">
header {* Tema 5: Patrones de demostración *}

theory Tema_5
imports Main
begin

section {* Demostraciones por casos *}

text {*
Nota. [Regla de eliminación de la disyunción]
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R

Lema. [Ejemplo de demostración por casos]
P ∨ Q ⟹ Q ∨ P
*}

lemma disj_conmutativa: "P ∨ Q ⟹ Q ∨ P"
proof -
assume "P ∨ Q"
thus "Q ∨ P"
proof (rule disjE)
assume P
thus ?thesis ..
next
assume Q
thus ?thesis ..
qed
qed

text {*
Nota. El lema anterior puede demostrarse automáticamente como se
muestra a continuación.
*}

lemma disj_conmutativa_auto: "P ∨ Q ⟹ Q ∨ P"
by auto

section {* Negación *}

text {*
Reglas de la negación:
· notI: (P ⟹ False) ⟹ ¬P
· notE: ⟦¬P; P⟧ ⟹ R

Lema. [Ejemplo de demostración con negaciones]
Si x\<^bsup>2\<^esup>+y=13 e y ≠ 4, entonces x ≠ 3.
*}

lemma
fixes x :: "nat"
assumes 1: "x * x + y = 13"
and 2: "y ≠ 4"
shows "x ≠ 3"
proof (rule notI)
assume "x = 3"
with 1 have "y = 4" by simp
with 2 show "False" by (rule notE)
qed

text {*
La demostración puede hacerse automáticamente como se muestra a
continuación.
*}

lemma
fixes x :: "nat"
assumes 1: "x * x + y = 13"
and 2: "y ≠ 4"
shows "x ≠ 3"
proof (rule notI)
assume "x = 3"
with 1 2 show "False" by auto
qed

text {*
El lema anterior puede demostrarse más automáticamente como se muestra a
continuación.
*}

lemma
fixes x :: "nat"
assumes 1: "x * x + y = 13"
and 2: "y ≠ 4"
shows "x ≠ 3"
using assms
by auto

section {* Contradicciones *}

text {*
Regla de contradicción:
· FalseE: False ⟹ P

Lema. [Ejemplo de uso de la regla de contradicción]
Si 1=2, entonces 3=7.
*}

lemma
assumes "1 = (2::nat)"
shows "3 = (7::nat)"
proof -
have "False" using assms by simp
thus "3 = (7::nat)" by (rule FalseE)
qed

text {*
El lema puede demostrarse automáticamente, como sigue.
*}

lemma
assumes "1 = (2::nat)"
shows "3 = (7::nat)"
using assms
by auto

text {*
Lema. [Ejemplo de demostración por casos y contradicción]
¬P, P ∨ Q ⊢ Q
*}

lemma disjCE:
assumes "¬P" and "P ∨ Q"
shows "Q"
using `P ∨ Q`
proof (rule disjE)
assume "P"
thus "Q" using `¬P` by contradiction
next
assume "Q"
thus "Q" by assumption
qed

section {* Equivalencias *}

text {*
Reglas de equivalencia:
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P

Lema. [Ejemplo de introducción de equivalencia]
La fórmula
(R ⟶ C) ∧ (S ⟶ C))
es equivalente a
R ∨ S ⟶ C
*}

lemma "((R ⟶ C) ∧ (S ⟶ C)) = (R ∨ S ⟶ C)"
proof (rule iffI)
assume "(R ⟶ C) ∧ (S ⟶ C)"
thus "R ∨ S ⟶ C" by blast
next
assume "R ∨ S ⟶ C"
thus "(R ⟶ C) ∧ (S ⟶ C)" by blast
qed

text {*
El método "blast":
En la demostración anterior es la primera vez que se usa el método de
razonamiento automático "blast".

Nota. El lema anterior puede demostrarse automáticamente como se
muestra a continuación.
*}

lemma "((R ⟶ C) ∧ (S ⟶ C)) = (R ∨ S ⟶ C)"
by auto

text {*
Lema. [Ejemplo de eliminación de equivalencia]
· A ⟷ B, A ⊢ B
· A ⟷ B, B ⊢ A
*}

lemma assumes "A = B" and "A" shows "B"
using assms
by (rule iffD1)

lemma assumes "A = B" and "B" shows "A"
using assms
by (rule iffD2)

end
</source>

← Revisión anterior	Revisión del 17:47 20 nov 2012
(Sin diferencias)

Tema 5: Patrones de demostración - Historial de revisiones

Jalonso: Protegió «Tema 5: Patrones de demostración» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso: Página creada con ' header {* Tema 5: Patrones de demostración *} theory Tema_5 imports Main begin section {* Demostraciones por casos *} text {* Nota. [Regla de elimin...'

Jalonso: Página creada con ' header {* Tema 5: Patrones de demostración } theory Tema_5 imports Main begin section { Demostraciones por casos } text { Nota. [Regla de elimin...'