Demostración asistida por ordenador (2011-12) Demostración asistida por ordenador (2011-12)

header {* Tema 9: Patrones de demostración *}

theory Tema_9
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  by (rule disjI2)
  next
    assume Q 
    thus ?thesis by (rule disjI1) 
  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