Razonamiento automático (2010-11) Razonamiento automático (2010-11)

theory Tema8
imports Main Efficient_Nat
begin

header {* Misceláneas *}

text {*
  Contenido:
  * Definición del algoritmo de Huffman
  * Definiciones inductivas
    * Demostraciones por introducción
    * Demostraciones por inducción sobre conjuntos inductivos
  * Clases
    * Subclase
    * Instanciación de clases
  * Ámbitos ("Locales")
  * Demostraciones estructuradas: inducción y encadenamiento
  * Un ejemplo elemental de álgebra
    * Definición de clases
    * Instanciación de clases
    * Instancias recursivas
    * Subclases
  * Las clases de tipos como ámbitos
    * Razonamiento abstracto
    * Definiciones derivadas
    * Analogía entre clases y functores
    * Relaciones de subclase adicionales
  * Otras cuestiones
    * Clases de tipos y generación de código
    * Inspección del universo de las clases de tipos
  * Sledgehammer
  * Refute
    * Refutaciones en lógica proposicional
      * Refutaciones en lógica de predicados
      * Refutaciones con funciones e igualdad
    * Ejemplos con listas
  * Nitpick
    * Refutación proposicional
    * Skolemizaciónn
*}

section {* Definición del algoritmo de Huffman *}

text {* 
  Ejemplo de definición de tipo de datos recursivo: árboles binarios.
*}

datatype 'a arbol = Hoja nat 'a | Nodo nat "('a arbol)" "('a arbol)"

text {* 
  Ejemplo de definición primitiva recursiva sobre un tipo definido:
  Definición del valor de un árbol. 
*}

primrec "valor" where
  "valor (Hoja n _) = n" 
| "valor (Nodo n _ _) = n"

text {*
  Ejemplo de definición no recursiva: Mezcla de dos árboles.
*}

definition "mezcla t1 t2 = Nodo (valor t1 + valor t2) t1 t2"

text {* 
  Definición de la inserción de un árbol en un bosque.
*}

fun ins where
  "ins u (t#ts) = (if valor u ≤ valor t then u # t # ts else t # ins u ts)" 
| "ins u [] = [u]"

text {* 
  Lema para usar en las demostraciones de terminación. En particular, en
  la definición de creaArbol. 
*}

lemma size_ins[termination_simp]: "size(ins u ts) = size ts + 1"
by (induct ts) simp_all

text {* 
  Creación de árboles a partir de listas 
*}

fun creaArbol where
  "creaArbol(t1#t2#ts) = creaArbol(ins (mezcla t1 t2) ts)" 
| "creaArbol[t] = t"

text {*
  Ejemplo de formas normales: creación de árboles de Huffman.
*}

value
  "creaArbol[Hoja 3 a, Hoja 6 b, Hoja 12 c, Hoja 24 d]"

text {* 
  El árbol creado es
  "Nodo 45 (Nodo 21 (Nodo 9 (Hoja 3 a) (Hoja 6 b)) (Hoja 12 c)) (Hoja 24 d)" *}

value
  "creaArbol[Hoja 24 d, Hoja 6 b, Hoja 12 c, Hoja 3 a]"

text {* 
  El árbol creado es
  "Nodo 45 (Nodo 15 (Hoja 12 c) (Hoja 3 a)) (Nodo 30 (Hoja 24 d) (Hoja 6 b))"
*}

section {* Definiciones inductivas *}

text {*
  En esta sección vamos a trabajar con una gramática cuyo alfabeto consta de
  dos símbolos: A y B. En primer lugar, se define el alfabeto (alfa)
  como un tipo con dos elementos. 
*}

datatype alfa = A | B

text {*
  Se define la gramática S como el conjunto de las listas de elementos del
  alfabeto generadas mediante las siguientes reglas:
  · La lista vacía está en S,
  · Si w está en S, entonces AwB también lo está.
  · Si v y w están en S, entonces vw también lo está. 
*}

inductive_set S :: "alfa list set" where
  S1: "[] ∈ S" 
| S2: "w ∈ S ⟹ [A] @ w @ [B] ∈ S" 
| S3: "v ∈ S ⟹ w ∈ S ⟹ v @ w ∈ S"

subsection {* Demostraciones por introducción *}

text {*
    La lista [A, B] está en S.
*}

lemma "[A, B] ∈ S"
proof -
  have "[] ∈ S" by (rule S1)
  hence "[A] @ [] @ [B] ∈ S" by (rule S2)
  thus ?thesis by simp
qed

subsection {* Demostraciones por inducción sobre conjuntos inductivos *}

text {*
  Ninguna palabra de la gramática empieze por B.
*}

lemma "w ∈ S ⟹ ¬ (∃v. w = B # v)"
proof (induct set:S)
  case S1
  thus ?case by simp
next
  case S2
  thus ?case by simp
next
  case S3
  thus ?case (* sledgehammer *) by (simp add: append_eq_Cons_conv)  
qed

section {* Clases *}

text {*
  El tutorial sobre clases está en la teoría Clases.thy.
  
  La clase de los órdenes es la colección de los tipos que poseen una
  relación ≼ verificando las siguientes propiedades
  · reflexiva: x ≼ x
  · transitiva: x ≼ y ⟹ y ≼ z ⟹ x ≼ z
  · antisimétrica: x ≼ y ⟹ y ≼ x ⟹ x = y
*}

class orden = 
  fixes menor_ig :: "'a ⇒ 'a ⇒ bool"  (infix "≼" 50)
  assumes refl: "x ≼ x"
      and trans: "x ≼ y ⟹ y ≼ z ⟹ x ≼ z"
      and antisim: "x ≼ y ⟹ y ≼ x ⟹ x = y"

text {*
  Ha generado los teoremas correspondientes a los axiomas. Pueden consultarse
  mediante thm como se muestra a continuación.
*}

thm refl

text {*
  Se inicia el contexto orden en el que se van a realizar definiciones y
  demostraciones. 
*}

context orden
begin

text {*
  x es menor que y si x es menor o igual que y y no son iguales.
*}

definition menor :: "'a ⇒ 'a ⇒ bool"  (infix "≺" 50)
  where "x ≺ y ⟷ x ≼ y ∧ ¬ y ≼ x"

text {*
    La relación menor es irreflexiva.
*}

lemma irrefl: "¬ x ≺ x"
by (auto simp:menor_def)

text {*
  La relación menor es transitiva.
*}

lemma menor_trans: "x ≺ y ⟹ y ≺ z ⟹ x ≺ z"
by (auto simp:menor_def intro:trans)

text {*
  La relación menor es asimétrica; es decir, si x ≺ y e y ≺ x, entonces
  se verifica cualquier propiedad P. 
*}

lemma asimetrica: "x ≺ y ⟹ y ≺ x ⟹ P"
by (auto simp:menor_def)

end

subsection {* Subclase *}

text {*
  Un orden lineal es un orden en que cada par de elementos son comparables.
*}

class ordenLineal = orden +
  assumes lineal: "x ≼ y ∨ y ≼ x"
begin

text {*
  En los órdenes lineales se tiene que x ≺ y ∨ x=y ∨ y ≺ x.
*}

lemma "x ≺ y ∨ x=y ∨ y ≺ x"
using menor_def lineal antisim  
by blast

end

subsection {* Instanciación de clases *}

text {*
  El producto de dos órdenes es un orden.
*}

instantiation prod :: (orden, orden) orden
begin

inductive menor_ig_prod :: "'a × 'b ⇒ 'a × 'b ⇒ bool" where
  menor_ig_fst: "x ≺ v ⟹ (x, y) ≼ (v, w)" 
| menor_ig_snd: "x = v ⟹ y ≼ w ⟹ (x, y) ≼ (v, w)"

instance
proof
  fix p :: "'a × 'b"
  show "p ≼ p" by (cases p) (auto intro!: menor_ig_snd refl)
next
  fix p q r :: "'a × 'b"
  assume "p ≼ r" and "r ≼ q"
  then show "p ≼ q"
    by (induct p r rule:menor_ig_prod.induct)
       (auto elim!:menor_ig_prod.cases 
             intro:menor_ig_fst menor_ig_snd trans menor_trans)
next
  fix p q :: "'a × 'b"
  assume "p ≼ q" and "q ≼ p"
  then show "p = q"
    by (induct p q rule:menor_ig_prod.induct)
       (auto elim!:menor_ig_prod.cases 
             elim:asimetrica 
             intro:antisim 
             simp:irrefl)
qed

end

section {* Ámbitos ("Locales") *}


text {*
  Un orden es una estructura con una relación reflexiva, transitiva y
  antisimétrica. 
*}

locale Orden =
  fixes menor_ig :: "'a ⇒ 'a ⇒ bool"  (infix "⊑" 50)
  assumes refl: "x ⊑ x"
      and trans: "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z"
      and antisim: "x ⊑ y ⟹ y ⊑ x ⟹ x = y"

text {*
    Los teoremas se diferencian por el nombre y el ámbito. Por ejemplo,
    refl: ?x ≼ ?x
    Orden.refl: Orden ?menor_ig ⟹ ?menor_ig ?x ?x
    Orden_def: Orden ?menor_ig ≡
               (∀x. ?menor_ig x x) ∧
               (∀x y z. ?menor_ig x y ⟶ ?menor_ig y z ⟶ ?menor_ig x z) ∧
               (∀x y. ?menor_ig x y ⟶ ?menor_ig y x ⟶ x = y)
*}

thm refl
thm Orden.refl
thm Orden_def

text {*
  Un orden lineal es un orden en el que todos los pares de elementos son 
  comparables. 
*}

locale OrdenLineal = Orden +
  assumes lineal: "x ⊑ y ∨ y ⊑ x"

text {*
  Los boooleanos está ordenados con el condicional.
*}

interpretation Orden_imp: Orden "op ⟶"
proof
  fix P show "P ⟶ P" by blast
next
  fix P Q R show "P ⟶ Q ⟹ Q ⟶ R ⟹ P ⟶ R" by blast
next
  fix P Q show "P ⟶ Q ⟹ Q ⟶ P ⟹ P = Q" by blast
qed

thm dvd.order_trans
thm dvd.less_le_trans

text {*
  Los naturales con la relación de divisibilidad es un conjunto ordenado.
*}

interpretation Orden_dvd: Orden "op dvd :: nat ⇒ nat ⇒ bool"
proof qed (auto intro: dvd_refl dvd_trans dvd_antisym)

text {*
  Ámbito de las funciones monótonas (ver la página 12 del tutorial de
  locales). 
*}

locale Mono =
  le1: Orden le1 +
  le2: Orden le2 
    for le1 (infix "⊑\<^isub>1" 50) and le2 (infix "⊑\<^isub>2" 50) +
  fixes f :: "'a ⇒ 'b"
  assumes mono: "x ⊑\<^isub>1 y ⟹ f(x) ⊑\<^isub>2 f(y)"

text {*
  Si f es monótona, x ⊑\<^isub>1 y e y ⊑\<^isub>1 z, entonces f(x) ⊑\<^isub>2 f(z).
*}

lemma (in Mono) mono_trans: 
  assumes "x ⊑\<^isub>1 y" and "y ⊑\<^isub>1 z" 
  shows "f(x) ⊑\<^isub>2 f(z)"
proof -
  have "x ⊑\<^isub>1 z" using assms and le1.trans by blast
  thus "f(x) ⊑\<^isub>2 f(z)" using mono by simp
qed

text {*
  El teorema generado se llama Mono.mono_trans.
*}

thm Mono.mono_trans

text {*
  En el contexto Mono el nombre es mono_trans.
*}

context Mono begin thm mono_trans end

text {*
  El predicado `ser par' es un operador monótono entre los naturales con la
  relación de divisibilidad y los booleanos con el condicional; es decir, 
     x dvd y ⟹ 2 dvd x ⟶ 2 dvd y
*}

interpretation Mono "op dvd" "op ⟶" "λn::nat. 2 dvd n"
proof
  fix x y :: nat 
  show "x dvd y ⟹ 2 dvd x ⟶ 2 dvd y"
    proof 
      assume "x dvd y" and "2 dvd x"
      thus "2 dvd y" using dvd.order_trans by blast
    qed
qed

section {* Demostraciones estructuradas: inducción y encadenamiento *}

text {*
    El siguiente ejemplo se encuentra en Wenzel2006 pp. 3--5 y el código
    en Isar_Example/Puzzle.thy. Una demostración más actualizada se
    encuentra en Nipkow2009 p.1 basada en la de Tao2006 pp. 34--36. 
*}

theorem identity1: 
  fixes f :: "nat ⇒ nat"
  assumes fff: "⋀n. f(f(n)) < f(Suc(n))"
  shows "f(n) = n"
proof -
  { fix m n have key: "n ≤ m ⟹ n ≤ f(m)"
    proof(induct n arbitrary: m)
      case 0 show ?case by simp
    next
      case (Suc n)
      have HI1: "⋀k. n ≤ k ⟹ n ≤ f k" using Suc by simp
      have HI2: "Suc n ≤ m" using Suc by simp
      hence "m ≠ 0" by simp
      then obtain k where [simp]: "m = Suc k" by (metis not0_implies_Suc)
      have "n ≤ k" using HI2 by simp
      have "n ≤ f(k)" using Suc by simp
      hence "n ≤ f(f(k))" using Suc by simp
      also have "… < f(m)" using fff by simp
      finally show ?case by simp
    qed }
  hence "⋀n. n ≤ f(n)" by simp
  hence "⋀n. f(n) < f(Suc n)" by(metis fff order_le_less_trans)
  hence "f(n) < n+1" by (metis fff lift_Suc_mono_less_iff[of f] Suc_eq_plus1)
  with `n ≤ f(n)` show "f n = n" by arith
qed

section {* Un ejemplo elemental de álgebra *}

subsection {* Definición de clases *}

text {*
  Un semigrupo es una estructura compuesta por un conjunto A y una
  operación binaria en A.
*}

class semigrupo =
  fixes mult :: "'a ⇒ 'a ⇒ 'a" (infixl "⊗" 70) 
  assumes asoc: "(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z )"

subsection {* Instanciación de clases *}

text {*
  Los enteros con la suma forman un semigrupo.
*}

instantiation int :: semigrupo 
begin 
definition 
  mult_int_def: "i ⊗ j = i + (j ::int)" 

instance proof 
  fix i j k :: "int" 
  have "(i + j ) + k = i + (j + k)" by simp 
  thus "(i ⊗ j ) ⊗ k = i ⊗ (j ⊗ k)" unfolding mult_int_def . 
qed 
end 

text {*
  Los naturales con la suma forman un semigrupo.
*}

instantiation nat :: semigrupo 
begin 
primrec mult_nat where 
  "(0::nat) ⊗ n = n" 
| "Suc m ⊗ n = Suc (m ⊗ n)" 

instance proof 
  fix m n q :: "nat" 
  show "m ⊗ n ⊗ q = m ⊗ (n ⊗ q)" 
    by (induct m) auto
qed 
end

subsection {* Instancias recursivas *}

text {*
  Si (A,⊗) y (B,⊗) son semigrupos, entonces ((A×B,⊗), donde el producto
  se define por 
     (x,y)⊗(x',y') = (x⊗x',y⊗y'),
  es un semigrupo.
*}
 
instantiation prod :: (semigrupo, semigrupo) semigrupo 
begin 

definition 
  mult_prod_def : "p1 ⊗ p2 = (fst p1 ⊗ fst p2, snd p1 ⊗ snd p2)" 

instance proof 
  fix p1 p2 p3 :: "'a::semigrupo × 'b::semigrupo" 
  show "(p1 ⊗ p2) ⊗ p3 = p1 ⊗ (p2 ⊗ p3)" 
    unfolding mult_prod_def by (simp add: asoc) 
qed 
end

subsection {* Subclases *}

text {*
  Un monoide izquierdo es un semigrupo con elemento neutro por la izquierda. 
*}

class monoideI = semigrupo + 
  fixes neutro :: "'a" ("1") 
  assumes neutroI: "1 ⊗ x = x"

text {*
  Los naturales y los enteros con la suma forman monoides por la izquierda.
*}

instantiation nat and int :: monoideI 
begin 

definition 
  neutro_nat_def : "1 = (0::nat)" 

definition 
  neutro_int_def : "1 = (0::int)" 

instance proof 
  fix n :: nat 
  show "1 ⊗ n = n" unfolding neutro_nat_def by simp
next 
  fix k :: int 
  show "1 ⊗ k = k" unfolding neutro_int_def mult_int_def by simp 
qed 
end

text {*
  El producto de dos monoides por la izquierda es un monoide por la
  izquierda, donde el neutro es el par formado por los elementos neutros.
*}

instantiation prod :: (monoideI , monoideI) monoideI 
begin 

definition 
  neutro_prod_def : "1 = (1, 1)" 

instance proof 
  fix p :: "'a::monoideI × 'b::monoideI" 
  show "1 ⊗ p = p" 
    unfolding neutro_prod_def mult_prod_def by (simp add: neutroI) 
qed 
end

text {*
  Un monoide es un monoide por la izquierda cuyo elemento neutro por la
  izquierda lo es también por la derecha.
*}

class monoide = monoideI + 
  assumes neutro: "x ⊗ 1 = x" 

text {*
  Los naturales y los enteros con la suma son monoides.
*}

instantiation nat and int :: monoide 
begin 

instance proof 
  fix n :: nat 
  show "n ⊗ 1 = n" 
    unfolding neutro_nat_def by (induct n) simp_all 
next 
  fix k :: int 
  show "k ⊗ 1 = k" 
    unfolding neutro_int_def mult_int_def by simp 
qed
end

text {*
  El producto de dos monoides es un monoide.
*}

instantiation prod :: (monoide, monoide) monoide 
begin 

instance proof 
  fix p :: "'a::monoide × 'b::monoide" 
  show "p ⊗ 1 = p" 
    unfolding neutro_prod_def mult_prod_def by (simp add: neutro) 
qed 
end

text {*
  Un grupo es un monoide por la izquierda tal que todo elemento posee un
  inverso por la izquierda.
*}

class grupo = monoideI + 
  fixes inverso :: "'a ⇒ 'a" ("(_⁻)" [1000] 999)
  assumes inversoI: "x⁻ ⊗ x = 1" 

text {*
  Los enteros con la suma forman un grupo.
*}

instantiation int :: grupo 
begin 

definition
  inverso_int_def: "i⁻ = -(i::int)"

instance proof 
  fix i :: "int" 
  have "-i + i = 0" by simp 
  then show "i⁻ ⊗ i = 1" 
    unfolding mult_int_def neutro_int_def inverso_int_def . 
qed 
end

section {* Las clases de tipos como ámbitos *}

subsection {* Razonamiento abstracto *}

text {*
  En los grupos se verifica la propiedad cancelativa por la izquierda, i.e.
     x ⊗ y = x ⊗ z ⟷ y = z
*}

lemma (in grupo) cancelativa_izq: "x ⊗ y = x ⊗ z ⟷ y = z" 
proof 
  assume "x ⊗ y = x ⊗ z"
  hence "x⁻ ⊗ (x ⊗ y) = x⁻ ⊗ (x ⊗ z)" by simp 
  hence "(x⁻ ⊗ x) ⊗ y = (x⁻ ⊗ x) ⊗ z" using asoc by simp 
  thus "y = z" using neutroI and inversoI by simp
next 
  assume "y = z" 
  thus "x ⊗ y = x ⊗ z" by simp
qed

thm Tema8.grupo.cancelativa_izq

text {*
  Se genera el teorema Tema8b.grupo.cancelativa_izq
     class.grupo ?mult ?neutro ?inverso ⟹ 
     (?mult ?x ?y = ?mult ?x ?z) = (?y = ?z)

  El teorema se aplica automáticamente a todas las instancias de la clase
  grupo. Por ejemplo, a los enteros.
*}

subsection {* Definiciones derivadas *}

text {*
  En los monoides se define la potencia natural por
  · x^0=1
  · x^{n+1}=x*x^n
*}

primrec (in monoide) potencia_nat :: "nat ⇒ 'a ⇒ 'a" where 
  "potencia_nat 0 x = 1"  
| "potencia_nat (Suc n) x = x ⊗ potencia_nat n x"

subsection {* Analogía entre clases y functores *}

text {*
  Las listas con la operación de concatenación y la lista vacía como elemento
  neutro forman un monoide.
*}

interpretation list_monoide: monoide "append" "[]"
  proof qed auto

text {*
  Se pueden aplicar propiedades de los monides a las listas. Por ejemplo,
*}

lemma "append [] xs = xs"
by simp

text {*
  (repite n xs) es la lista obtenida concatenando n veces la lista xs. 
*}

primrec repite :: "nat ⇒ 'a list ⇒ 'a list" where 
  "repite 0 _ = []"
| "repite (Suc n) xs = xs @ repite n xs"

text {*
  Las listas con la operación de concatenación y la lista vacía como elemento
  neutro forman un monoide. Además, la potencia natural se intepreta como
  repite. 
*}

interpretation list_monoide: monoide "append" "[]" where 
  "monoide.potencia_nat append [] = repite" 
proof -
  interpret monoide "append" "[]" .. 
  show "monoide.potencia_nat append [] = repite" 
  proof 
    fix n 
    show "monoide.potencia_nat append [] n = repite n" 
      by (induct n) auto 
  qed 
qed intro_locales

subsection {* Relaciones de subclase adicionales *}

text {*
  Los grupos son monoides.
*}

subclass (in grupo) monoide 
proof 
  fix x 
  have "x⁻ ⊗ (x ⊗ 1) = x⁻ ⊗ (x ⊗ (x⁻ ⊗ x))" using inversoI by simp
  also have "... = (x⁻ ⊗ x) ⊗ (x⁻ ⊗ x)" using asoc [symmetric] by simp
  also have "... = 1 ⊗ (x⁻ ⊗ x)" using inversoI by simp
  also have "... = x⁻ ⊗ x" using neutroI by simp
  finally have "x⁻ ⊗ (x ⊗ 1) = x⁻ ⊗ x" . 
  thus "x ⊗ 1 = x" using cancelativa_izq by simp
qed

text {*
  La potencia entera en los grupos se define a partir de la potencia natural
  como sigue:
  · x^k = x^k si k ≥ 0
  · x^k = (x^{-k})^{-1}, en caso contrario.
*}

definition (in grupo) potencia_entera :: "int ⇒ 'a ⇒ 'a" where 
  "potencia_entera k x = 
   (if k >= 0 
    then potencia_nat (nat k) x 
    else (potencia_nat (nat (- k)) x)⁻)"

section {* Otras cuestiones *}

subsection {* Clases de tipos y generación de código *}

text {*
  Ejemplo para evaluar.
*}

definition ejemplo :: int where 
  "ejemplo = potencia_entera 10 (-2)"

text {*
  Al evaluar la siguiente expresión se obtiene como valor -20.
*}

value "ejemplo"

text {*
  Ejemplo de generación de código Haskell.
*}

export_code ejemplo
  in Haskell file "codigoHaskell/"

text {*
  El código Haskell se exporta en el fichero codigoHaskell/Tema8b.hs
*}

subsection {* Inspección del universo de las clases de tipos *}

text {*
  Se puede obtener la lista de las clases con print_classes. Por
  ejemplo, evaluando la siguiente expresión se obtiene
      class semigrupo:
        supersort: type
        parameters:
          mult :: 'a ⇒ 'a ⇒ 'a
        instances:
          int :: semigrupo, nat :: semigrupo,
            prod :: (semigrupo, semigrupo) semigrupo
      
      class monoideI:
        supersort: semigrupo
        parameters:
          neutro :: 'a
        instances:
          int :: monoideI, nat :: monoideI, prod :: (monoideI, monoideI) monoideI
      
      class monoide:
        supersort: monoideI
        instances: int :: monoide, nat :: monoide, prod :: (monoide, monoide) monoide
      
      class grupo:
        supersort: monoide
        parameters:
          inverso :: 'a ⇒ 'a
        instances: int :: grupo
*}

print_classes

text {*
  Se puede obtener el grafo de las clases con class_deps.
*}

class_deps

section {* Sledgehammer *}

text {*
  Demostración con Sledgehammer de la paradoja del bebedor: ``hay una persona
  en el bar, tal que si dicha persona bebe todos beben''.
*}
lemma "∃x. P x ⟶ (∀y. P y)"
by metis

section {* Refute *}

subsection {* Refutaciones en lógica proposicional *}

text {*
  Ejemplo de refutación proposicional.
*}
lemma "P ⟷ Q"
refute
oops

text {*
  El resultado obtenido es
      *** Model found: ***
      empty universe (no type variables in term)
      Q: True
      P: False
*}

subsubsection {* Refutaciones en lógica de predicados *}

text {*
  Ejemplo de refutación en lógica de primer orden.
*}

lemma "(∃x. P x) ⟶ (∀x. P x)"
refute
oops

text {*
  El resultado obtenido es
      *** Model found: ***
      Size of types: 'a: 2
      P: {(a0, True), (a1, False)}
  que da un contraejemplo cuyo universo es {a₀, a₁} y sólo se verifica
  en a₀. 
*}

text {*
  Ejemplo de refutación en lógica de primer orden con relaciones binarias.
*}

lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
refute
oops

text {*
  El resultado obtenido es
      *** Model found: ***
      Size of types: 'a: 2, 'b: 2
      P: {(a0, {(b0, True), (b1, False)}), (a1, {(b0, False), (b1, True)})}
  que da un contraejemplo cuyo universo es {a₀, a₁, b₀, b₁} y P sólo se
  verifica en {(a₀,b₁),(a₁,b₀)}. 
*}

text {* 
  Conjetura: Toda relación reflexiva y simétrica es transitiva. 
*}

lemma "⟦ ∀x. P x x; ∀x y. P x y ⟶ P y x ⟧ ⟹ P x y ⟶ P y z ⟶ P x z"
refute
oops

text {*
  El resultado obtenido es
      *** Model found: ***
      Size of types: 'a: 3
      z: a0
      y: a2
      x: a1
      P: {(a0, {(a0, True), (a1, False), (a2, True)}), 
                (a1, {(a0, False), (a1, True), (a2, True)}), 
                (a2, {(a0, True), (a1, True), (a2, True)})}
  que da un contraejemplo cuyo universo es {a₀, a₁, a₂} y P sólo se
  verifica en 
     {(a₀,a₀),(a₀,a₁),(a₀,a₂),(a₁,a₀),(a₁,a₁),(a₂,a₀),(a₂,a₂)}.
  Entonces P es reflexiva y simétrica, pero no es transitiva porque 
  se tiene que P(a₂,a₀) y P(a₀,a₁) y no se verifica P(a₂,a₁).
*}

subsubsection {* Refutaciones con funciones e igualdad *}

text {*
  En los siguientes ejemplos se consideran símbolos de función y el de
  igualdad.

  Ejemplo de fallo en la refutación de la paradoja del mentiroso.
*}

lemma "∃x. f x = g x ⟶ f = g"
refute [maxsize=4]
apply (auto simp add: ext)
done 

text {* 
  Refutación de una versión incorrecta de la paradoja del bebedor.
*}

lemma "(∃x. f x = g x) ⟶ f = g"
refute
oops

text {*
  Se obtiene
      *** Model found: ***
      Size of types: 'a: 2, 'b: 2
      g: {(a0, b1), (a1, b1)}
      f: {(a0, b0), (a1, b1)}
*}

text {* 
    La composición de funciones es conmutativa.
*}

lemma "f (g x) = g (f x)"
refute
oops

text {*
  Se obtiene
      *** Model found: ***
      Size of types: 'a: 2
      x: a0
      g: {(a0, a1), (a1, a0)}
      f: {(a0, a1), (a1, a1)}
*}

text {* 
  Toda función suprayectiva tiene inversa.
*}

lemma "(∀y. ∃x. y = f x) ⟶ (∃g. ∀x. g (f x) = x)"
refute
oops

text {*
  Se obtiene
      *** Model found: ***
      Size of types: 'a: 1, 'b: 2
      f: {(b0, a0), (b1, a0)}
*}

text {* 
  Toda función que tiene inversa es suprayectiva.
*}

lemma "(∃g. ∀x. g (f x) = x) ⟶ (∀y. ∃x. y = f x)"
refute
oops

text {*
  Se obtiene
      *** Model found: ***
      Size of types: 'b: 1, 'a: 2
      f: {(b0, a1)}
*}

subsection {* Ejemplos con listas *}

text {*
  La concatenación de listas es conmutativa.
*}

lemma "xs @ ys = ys @ xs"
refute
oops

text {*
  Se obtiene
      *** Model found: ***
      Size of types: 'a list: 3, 'a: 2
      ys: [a0]
      xs: [a1]
*}

section {* Nitpick *}

text {* 
  Notas:
  · Nitpick es un generador de contraejemplos.
  · Los ejemplos están elegidos de Nitpick_Examples.thy. 
  · Para los ejemplos de Nitpick se deshabilita el QuicCheck automático.
  · Nitpick va a usar MiniSATJNI con una hebra. 
*} 
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]

subsection {* Refutación proposicional *}

lemma "P ⟷ Q"
nitpick
oops

text {* 
  Se obtiene
      Nitpick found a counterexample:
        Free variables:
          P = True
          Q = False
*}

subsection {* Skolemizaciónn *}

text {* 
  Conjetura: Las funciones que tienen inversa son suprayectivas. 
*}

lemma "∃g. ∀x. g (f x) = x ⟹ ∀y. ∃x. y = f x"
nitpick
oops

text {* 
  Se obtiene 
      Nitpick found a counterexample for card 'a = 2 and card 'b = 1:
      
        Free variable:
          f = (λx. _)(b\<^bsub>1\<^esub> := a\<^bsub>1\<^esub>)
        Skolem constants:
          g = (λx. _)(a\<^bsub>1\<^esub> := b\<^bsub>1\<^esub>, a\<^bsub>2\<^esub> := b\<^bsub>1\<^esub>)
          y = a\<^bsub>2\<^esub>
  Significa que que Nitpick ha encontrado un contraejemplo donde
  · A={a\<^bsub>1\<^esub>,a\<^bsub>2\<^esub>}
  · B={b\<^bsub>1\<^esub>}
  · f: B → A tal que f(b\<^sub>1)=a\<^sub>1
  Entonces, f tiene inversa (la función g: A → B tal que g(a\<^sub>1)=b\<^sub>1 y
  g(a\<^sub>2)=b\<^sub>1), pero no es suprayectiva (el elemento a\<^sub>2 no tiene antiimagen).
*} 

end