Tema 12c: Automatización

header {* T12c: Automatización *}

theory T12c_Automatizacion
imports Main
begin

section {* Lógica y conjuntos *}

subsection {* Demostraciones con auto *}

lemma "∀x. ∃y. x=y"
by auto

lemma "A ⊆ B ∩ C ⟹ A ⊆ B ∪ C"
by auto

subsection {* Demostraciones con fastforce *}

lemma "⟦ ∀xs ∈ A. ∃ys. xs = ys @ ys;  us:A ⟧ ⟹ ∃n. length us = n+n"
by fastforce

text {* Nota: Obsérvese la notación de los cuantificadores acotados: *} 

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

subsection {* Demostraciones con blast *}

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. *}

section{* Sledgehammer *}

lemma "⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys"
by (metis append_eq_conv_conj)

lemma "R^* ⊆ (R ∪ S)^*"
by (metis Un_upper1 rtrancl_mono)

lemma "a # xs = ys @ [a] ⟹ P"
oops

lemma "xs @ ys = ys @ xs ⟹ P"
oops

section {* Aritmética *}

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

end
De Razonamiento automático (2014-15)
