Jalonso: Página creada con ' theory Tema8 imports Main Efficient_Nat begin header {* Misceláneas } text { Contenido: * Definición del algoritmo de Huffman * Definiciones ind...'

2011-02-21T07:49:56Z

Página creada con '<source lang="isar"> theory Tema8 imports Main Efficient_Nat begin header {* Misceláneas *} text {* Contenido: * Definición del algoritmo de Huffman * Definiciones ind...'

Página nueva

<source lang="isar">
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
</source>

Misceláneas - Historial de revisiones

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

Jalonso: Página creada con ' theory Tema8 imports Main Efficient_Nat begin header {* Misceláneas } text { Contenido: * Definición del algoritmo de Huffman * Definiciones ind...'

@@ Línea 1: / Línea 1: @@
-<source lang="isar">
+<source lang="isabelle">
 theory Tema8
 imports Main Efficient_Nat

Misceláneas - Historial de revisiones

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

Jalonso: Página creada con ' theory Tema8 imports Main Efficient_Nat begin header {* Misceláneas *} text {* Contenido: * Definición del algoritmo de Huffman * Definiciones ind...'

Jalonso: Página creada con ' theory Tema8 imports Main Efficient_Nat begin header {* Misceláneas } text { Contenido: * Definición del algoritmo de Huffman * Definiciones ind...'