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

header {* El lenguaje de demostración Isar *}

theory Tema_7
imports Main
begin

text {*
  Este tema describe los elementos básicos del lenguaje de demostración
  Isar (Intelligible semi-automated reasoning).
*}

section {* Panorama de la sintaxis (simplificada) de Isar *}

text {* 
  Representación de lemas (y teoremas)
  · Un lema (o teorema) comienza con una etiqueta seguida por algunas
    premisas y una conclusión.
  · Las premisas se introducen con la palabra "assumes" y se separan
    con "and".
  · Cada premisa puede etiquetarse para referenciarse en la demostración.
  · La conclusión se introduce con la palabra "shows".

  Gramática (simplificada) de las demostraciones en Isar
  <demostración> ::= proof <método> <declaración>* qed
                   | by <método>
  <declaración>  ::= fix <variable>+ 
                   | assume <proposición>+
                   | (from <hecho>+)? have <proposición>+ <demostración>
                   | (from <hecho>+)? show <proposición>+ <demostración>
  <proposición>  ::= (<etiqueta>:)? <cadena>
  hecho          ::= <etiqueta>
  método         ::= -
                   | this
                   | rule <hecho>
                   | simp 
                   | blast
                   | auto
                   | induct <variable>

  La declaración "show" demuestra la conclusión de la demostración
  mientras que la declaración "have" demuestra un resultado intermedio.
*}

section {* Razonamiento proposicional *}

text {* 
  Regla de introducción de la conjunción:
  · conjI: ⟦P; Q⟧ ⟹ P ∧ Q

  Nota: Se puede consultar mediante
     thm conjI     

  Lema. [Ejemplo de introducción de conjunción con razonamiento progresivo] 
    P, Q ⊢ P ∧ (Q ∧ P)  

  Demostración. Estamos suponiendo
     P                                     (1)
  y
     Q                                     (2)
  De (2) y (1), por introducción de la conjunción, se tiene
     Q ∧ P                                 (3)
  De (1) y (3), por introducción de la conjunción, se tiene
     P ∧ (Q ∧ P)
*}

lemma conj2: 
  assumes 1: P and 2: "Q" 
  shows "P ∧ (Q ∧ P)"
proof -
  from 2 1 have 3: "Q ∧ P" by (rule conjI)
  from 1 3 show "P ∧ (Q ∧ P)" by (rule conjI)
qed

text {* 
  Razonamiento progresivo y regresivo en Isabelle:
  · Isabelle soporta razonamiento progresivo. La anterior demostración
    es una muestra. 
  · Isabelle soporta razonamiento regresivo. La siguiente demostración
    es una muestra. 

  Lema. [Ejemplo de introducción de la conjunción con razonamiento regresivo] 
     P, Q ⊢ P ∧ (Q ∧ P)

  Demostración. Estamos suponiendo
     P                                    (1)
  y
     Q                                    (2)

  Para demostrar el lema, por introducción de la conjunción, basta probar
     P
  y
     Q ∧ P                                (3)

  La condición 'P' se tiene por la hipótesis (1). Para demostrar
  la condición (3), por introducción de la conjunción, basta probar
     Q                                     
  y
     P
  La condición 'Q' se tiene por la hipótesis (2) y la condición 'P' se
  tiene por la hipótesis (1).
*}

lemma 
  assumes 1: "P" and 2: "Q" 
  shows "P ∧ (Q ∧ P)"
proof (rule conjI)
  from 1 show "P" by this
next
  show "Q ∧ P"
  proof (rule conjI)
    from 2 show "Q" by this
  next
    from 1 show "P" by this
  qed
qed

text {* 
  El método "this" demuestra el objetivo usando el hecho actual; es
  decir, el de la cláusula "from".  

  Reglas de eliminación de la conjunción:
  · conjunct1: P ∧ Q ⟹ P
  · conjunct2: P ∧ Q ⟹ P

  Regla de introducción de la implicación:
  · impI: (P ⟹ Q) ⟹ P ⟶ Q

  Lema. [Ejemplo de razonamiento híbrido]
  Sean a y b dos números naturales. Si 0 < a y a < b, entonces a*a < b*b.    
*}

lemma
  fixes a b :: "nat"
  shows "0 < a ∧ a < b ⟶ a * a < b * b"
proof (rule impI)
  assume x: "0 < a ∧ a < b"
  from x have za: "0 < a" by (rule conjunct1)
  from x have ab: "a < b" by (rule conjunct2)
  from za ab have aa: "a*a < a*b" by simp
  from ab have bb: "a*b < b*b" by simp
  from aa bb show "a*a < b*b" by arith
qed

text {* 
  Modus ponens:
  · mp: ⟦P ⟶ Q; P⟧ ⟹ Q

  Reglas de introducción de la disyunción:
  · disjI1: P ⟹ P ∨ Q
  · disjI2: Q ⟹ P ∨ Q

  Regla de eliminación de la disyunción:
  . disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R

  Lema. [Razonamiento por casos] 
     A ∨ B, A ⟶ C, B ⟶ C ⊢ C
*}

lemma 
  assumes ab: "A ∨ B" and ac: "A ⟶ C" and bc: "B ⟶ C"
  shows "C"
proof -
  note ab
  moreover { 
    assume a: "A" 
    from ac a have "C" by (rule mp) } 
  moreover { 
    assume b: "B" 
    from bc b have "C" by (rule mp) }
  ultimately show "C" by (rule disjE)
qed

text {* 
  Resumen de reglas proposicionales:
  · TrueI:         True
  · FalseE:        False ⟹ P
  · conjI:         ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:     P ∧ Q ⟹ P
  · conjunct2:     P ∧ Q ⟹ Q
  · conjE:         ⟦P ∧ Q; ⟦P; Q⟧ ⟹ R⟧ ⟹ R
  · disjI1:        P ⟹ P ∨ Q
  · disjI2:        Q ⟹ P ∨ Q
  · disjE:         ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
  · notI:          (P ⟹ False) ⟹ ¬P
  · notE:          ⟦¬P; P⟧ ⟹ R
  · impI:          (P ⟹ Q) ⟹ P ⟶ Q
  · impE:          ⟦P ⟶ Q; P; Q ⟹ R⟧ ⟹ R
  · mp:            ⟦P ⟶ Q; P⟧ ⟹ Q
  · iff:           (P ⟶ Q) ⟶ (Q ⟶ P) ⟶ P = Q
  · iffI:          ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:         ⟦Q = P; Q⟧ ⟹ P
  · iffD2:         ⟦P = Q; Q⟧ ⟹ P
  · iffE:          ⟦P = Q; ⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R⟧ ⟹ R
  · ccontr:        (¬P ⟹ False) ⟹ P
  · classical:     (¬P ⟹ P) ⟹ P      && @{thm classical } \\
  · exlude_middle: ¬P ∨ P
  · disjCI:        (¬Q ⟹ P) ⟹ P ∨ Q
  · impCE:         ⟦P ⟶ Q; ¬P ⟹ R; Q ⟹ R⟧ ⟹ R
  · iffCE:         ⟦P = Q; ⟦P; Q⟧ ⟹ R; ⟦¬P; ¬Q⟧ ⟹ R⟧ ⟹ R
  · notnotD:       ¬¬P ⟹ P
  · swap:          ⟦¬P; ¬R ⟹ P⟧ ⟹ R

  Referencia de reglas de inferencia: Más información sobre las reglas
  de inferencia se encuentra en la sección  2.2 de "Isabelle's Logics:
  HOL".
*}

section {* Atajos de Isar *}

text {*
  Isar tiene muchos atajos, como los siguientes:
  this        | éste           | el hecho probado en la declaración anterior
  then        | entonces       | from this
  hence       | por lo tanto   | then have
  thus        | de esta manera | then show
  with hecho+ | con            | from hecho+ and this
  .           | por ésto       | by this
  ..          | trivialmente   | by regla (Isabelle adivina la regla)

  Razonamiento acumulativo:
  Una sucesión de hechos que se van a usar como premisa en una declaración
  puede agruparse usando "moreover" (además) y usarse en la declaración
  usando "ultimately" (finalmente). 

  Lema. [Ejemplo de uso de atajos y razonamiento acumulativo]
     A ∧ B ⊢ B ∧ A.
*}

lemma "A ∧ B ⟶ B ∧ A"
proof (rule impI)
  assume ab: "A ∧ B"
  hence "B" by (rule conjunct2)
  moreover from ab have "A" ..
  ultimately show "B ∧ A" by (rule conjI)
qed

section {* Cuantificadores universal y existencial *}

thm allE
text {* 
  Reglas del cuantificador universal:
  · allI: (⋀x. P x) ⟹ ∀x. P x
  · allE: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  En la regla allI la nueva variable se introduce mediante la palabra "fix".

  Lema. [Ejemplo con  cuantificadores universales]
     ∀x. P ⟶ Q x ⊢ P ⟶ (∀x. Q x)
*}

lemma
  assumes a: "∀ x. P ⟶ Q x"
  shows "P ⟶ (∀ x. Q x)"
proof (rule impI)
  assume p: "P"
  show "∀ x. Q x"
  proof (rule allI)
    fix y
    from a have pq: "P ⟶ Q y" by (rule allE)
    from pq p show "Q y" by (rule mp)
  qed
qed

text {* 
  Reglas del cuantificador existencial:
  · exI: P x ⟹ ∃x. P x
  · exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
  En la regla exE la nueva variable se introduce mediante la declaración 
  "obtain ... where ... by (rule exE)" 

  Lema. [Ejemplo con cuantificador existencial y demostración progresiva]
     ∃x. P ∧ Q(x) ⊢ P ∧ (∃x. Q(x))
*}

lemma
  assumes e: "∃ x. P ∧ Q(x)"
  shows "P ∧ (∃ x. Q(x))"
proof -
  from e obtain y where f: "P ∧ Q(y)" by (rule exE) 
  from f have p: "P" by (rule conjunct1)
  from f have q: "Q(y)" by (rule conjunct2)
  from q have eq: "∃ x. Q(x)" by (rule exI)
  from p eq show "P ∧ (∃ x. Q(x))" by (rule conjI)
qed

text {* 
  Lema. [Ejemplo con cuantificador existencial y demostración automática] 
     ∃x. P ∧ Q(x) ⊢ P ∧ (∃x. Q(x))
*}

lemma
  assumes e: "∃ x. P ∧ Q(x)"
  shows "P ∧ (∃ x. Q(x))"
proof -
  from e obtain y where f: "P ∧ Q(y)" ..
  from f have p: "P" ..
  from f have q: "Q(y)" ..
  from q have eq: "∃x. Q(x)" ..
  from p eq show "P ∧ (∃x. Q(x))" ..
qed

text {* 
  Lema. [Ejemplo con cuantificador existencial y demostración regresiva]
     ∃x. P ∧ Q(x) ⊢ P ∧ (∃x. Q(x))"
*}

lemma
  assumes e: "∃x. P ∧ Q(x)"
  shows "P ∧ (∃x. Q(x))"
proof (rule conjI)
  show "P"
    proof -
    from e obtain y where p: "P ∧ Q(y)" by (rule exE)
    from p show "P" by (rule conjunct1)
    qed
  show "∃x. Q(x)"
    proof -
    from e obtain y where p: "P ∧ Q(y)" by (rule exE)
    from p have q: "Q(y)" by (rule conjunct2)
    from q show "∃x. Q(x)" by (rule exI)
    qed
qed

text {* 
  Definición. [Ejemplo de definición existencial]
  El número natural x divide al número natural y si existe un natural k
  tal que k×x = y. Se representa por x | y. 
*}

definition divide :: "nat ⇒ nat ⇒ bool" ("_ | _" [80,80] 80) where
  "x | y ≡ ∃k. k*x = y"

text {* 
  Ejemplo de activación automática de regla de simplificación:
  La definición de divide se añade a las reglas de simplificación. 
*}

declare divide_def[simp]

text {* 
  Lema. [Transitividad de la divisibilidad]
  Sean a, b y c números naturales. Si b es divisible por a y c es
  divisible por b, entonces c es divisible por a. 
*}

lemma divide_trans: 
  fixes a b c :: "nat"
  assumes ab: "a | b" and bc: "b | c"
  shows "a | c"
proof simp
  from ab obtain m where m: "m*a = b" by auto
  from bc obtain n where n: "n*b = c" by auto
  from m n have "m*n*a = c" by auto
  thus "∃k. k*a = c" by (rule exI)
qed

text {* 
  Método auto: En el lema anterior es la primera vez que se usa el
  método automático "auto".

  Lema. [CNS de divisibilidad]
  Sean a y b dos números naturales. Entonces a es divisible por b syss
  el resto de dividir a entre b es cero.  
*}

lemma CNS_divisibilidad: 
  "(a | b) = (b mod a = 0)" 
by auto

section {* Razonamiento ecuacional *}

text {* 
  Elementos para el razonamiento ecuacional:
  El razonamiento ecuacional se realiza de manera más concisa usando la
  combinación de "also" (además) y "finally" (finalmente).
  
  Lema. [Ejemplo de razonamiento ecuacional]
  Si a=b, b=c y c=d, entonces a=d.  
*}

lemma 
  assumes 1: "a = b" and 2: "b = c" and 3: "c = d"
  shows "a = d"
proof -
  have "a = b" by (rule 1)
  also have "… = c" by (rule 2)
  also have "… = d" by (rule 3)
  finally show "a = d" .
qed

text {* 
  El lema anterior puede demostrarse automáticamente con la maza
  ("sledgehammer"). 
*}

lemma 
  assumes 1: "a = b" and 2: "b = c" and 3: "c = d"
  shows "a = d"
proof -
  show "a=d" by (metis 1 2 3)
qed

end