Tema 11: Métodos de demostración.

header {* T11: Métodos de demostración *}

theory T11
imports Main
begin

text {* "thm" escribe el enunciado de los teoremas cuyos nombres se
  indican. *}
thm conjI impI iffI notI

text{* Instanciación de teoremas con "of": *}
thm conjI
thm conjI[of "A" "B"]
thm conjI[of "A"]
thm conjI[of _ "B"]

text{* Instanciación de teoremas con "where": *}
thm conjI
thm conjI [where ?Q = "B"]

text {* Composición de teoremas con "OF": *}
thm refl
thm refl [of "a"]
thm conjI
thm conjI [OF refl [of "a"] refl [of "b"]]
thm conjI [OF refl [of "a"]]
thm conjI [OF _ refl [of "b"]]

text {* Ejemplos de demostración por pasos con apply. 
Uso de los métodos de demostración:
assumption, simp, simp_all, auto, blast, arith *}

text {* Una demostración por razonamiento hacia atrás: *}
lemma "⟦ A; B ⟧ ⟹ A ∧ B"
  apply (rule conjI)
  apply assumption
  apply assumption
  done

text {*
  Recordemos la definición de la función recursiva que suma números
  naturales.
*}

fun add :: "nat ⇒ nat ⇒ nat" where
  "add 0 n = n" 
| "add (Suc m) n = Suc(add m n)"

text{*
  Probar que la función add es asociativa y commutativa.
  Indicación: serán necesario lemas adicionales.
*}

lemma add_assoc: "add (add m n) p = add m (add n p)"
by (induct m) auto

lemma add_assoc_d: "add (add m n) p = add m (add n p)"
proof (induct m)
  show "add (add 0 n) p = add 0 (add n p)" by simp
  next
  fix m
  assume hi: "add (add m n) p = add m (add n p)"
  show "add (add (Suc m) n) p = add (Suc m) (add n p)"
    proof -
      have  "add (add (Suc m) n) p = add (Suc (add m n)) p" by simp
      also have "… = Suc (add (add m n) p)" by simp
      also have "… = Suc (add m (add n p))" using hi by simp
      also have "… = add (Suc m) (add n p)" by simp
      finally show ?thesis .   
    qed 
qed

text {*
lemma add_0_der: "add m 0 = m"
by (induct m) auto

lemma add_comm_suc: "add n (Suc m) = add (Suc n) m"
by (induct n) auto
*}

lemma add_comm_apply: "add m n = add n m"
oops

lemma add_comm_d: "add m n = add n m"
oops

lemma add_comm_auto: "add m n = add n m"
oops

text {* Métodos básicos para las reglas: rule, erule

Las reglas de introducción descomponen la formula de la 
derecha de =>.
   apply (rule <regla-intro>)
regla de introducción  [[A1; . . . ;An]] => A significa:
 * Para probar basta probar A1 . . .An
 * Aplicar la regla [[A1; . . . ;An]] => A al objetivo C:
     * Se unifica A y C
     * Se sustituye C por n nuevos subobjetivos A1 . . .An

Las reglas de eliminación descomponen las formulas de la 
izquierda de =>.
   apply (erule <regla-elim>)
regla de eliminación  [[A1; . . . ;An]] => A significa:
 * Si tenemos A1 y queremos probar A, basta probar A1 . . .An-1
 * Aplicar la regla [[A1; . . . ;An]] => A al objetivo C:
     * Se unifica A y C
     * Se unifica A1 con alguna hipótesis y se borra la hipótesis
     * Se sustituye C por n nuevos subobjetivos A1 . . .An-1
 *}

lemma disj_inter: "P ∨ Q ⟹ Q ∨ P"
  apply (erule disjE)
  apply (rule disjI2)
  apply assumption
  apply (rule disjI1)
  apply assumption
  done

lemma conj_inter: "P ∧ Q ⟹ Q ∧ P"
  apply (rule conjI)
  apply (rule conjunct2)
  apply assumption
  apply (rule conjunct1)
  apply assumption
  done

text {* Método simp:

* lemma nombre_thm[simp]
* declare nombre_thm[simp]
* declare nombre_thm[simp del]

En un paso concreto, cusndo no se ha declarado globalmente
* (simp add: thm1 thm2...)
* (simp del: thm1 thm2...)
* (simp only: thm1 thm2...)
*}

text {* Método blast *}

lemma "(( ∃ x. ∀ y. p(x)=p(y)) = (( ∃ x. q(x))=( ∀ y. p(y)))) =
       (( ∃ x. ∀ y. q(x)=q(y)) = (( ∃ x. p(x))=( ∀ y. q(y))))"
by blast

text {* Indicación de regla de introducción a "blast": *}

thm le_trans

lemma "⟦ (a::nat) ≤ b; b ≤ c; c ≤ d ⟧ ⟹ a ≤ d"
  by (blast intro: le_trans)

text {*
  Nota: Muchas propiedades de la LPO y de la teoría de conjuntos se
  pueden demostrar automáticamente.

  Prop.: Si T es total, A es antisimétrica y T es un subconjunto de A,
  entonces A es un subconjunto de T.
*}

lemma AT:
  "⟦ ∀x y. T x y ∨ T y x;
     ∀x y. A x y ∧ A y x ⟶ x = y;
     ∀x y. T x y ⟶ A x y ⟧
   ⟹ ∀x y. A x y ⟶ T x y"
by blast


text {* Nota: Con auto no se puede probar el lema anterior. *}

text {* Método arith *}

lemma "⟦ (a::nat) ≤ x + b; 2*x < c ⟧ ⟹ 2*a+1 ≤ 2*b+c"
by arith

end