Razonamiento automático (2015-16) - Contribuciones del usuario [es]

R3

2018-07-16T10:55:29Z

WikiSysop:

<source lang="isabelle">
header {* R3: Razonamiento sobre programas en Isabelle/HOL *}

theory R3
imports Main
begin

text {* ---------------------------------------------------------------
Ejercicio 1. Definir la función
sumaImpares :: nat ⇒ nat
tal que (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 5 = 25
------------------------------------------------------------------ *}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares n = undefined"

value "sumaImpares 5" -- "= 25"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
sumaImpares n = n*n
------------------------------------------------------------------- *}

lemma "sumaImpares n = n*n"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
sumaPotenciasDeDosMasUno :: nat ⇒ nat
tal que
(sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.
Por ejemplo,
sumaPotenciasDeDosMasUno 3 = 16
------------------------------------------------------------------ *}

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno n = undefined"

value "sumaPotenciasDeDosMasUno 3" -- "= 16"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
oops

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
copia :: nat ⇒ 'a ⇒ 'a list
tal que (copia n x) es la lista formado por n copias del elemento
x. Por ejemplo,
copia 3 x = [x,x,x]
------------------------------------------------------------------ *}

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia n x = undefined"

value "copia 3 x" -- "= [x,x,x]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de xs cumplen
la propiedad p. Por ejemplo,
todos (λx. x>(1::nat)) [2,6,4] = True
todos (λx. x>(2::nat)) [2,6,4] = False
Nota: La conjunción se representa por ∧
----------------------------------------------------------------- *}

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p xs = undefined"

value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"
value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar que todos los elementos de (copia n x) son
iguales a x.
------------------------------------------------------------------- *}

lemma "todos (λy. y=x) (copia n x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ *}

fun factR :: "nat ⇒ nat" where
"factR n = undefined"

value "factR 4" -- "= 24"

text {* ---------------------------------------------------------------
Ejercicio 9. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
------------------------------------------------------------------- *}

fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (Suc n)*x"

fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"

value "factI 4" -- "= 24"

lemma fact: "factI' n x = x * factR n"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
factI n = factR n
------------------------------------------------------------------- *}

corollary "factI n = factR n"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Definir, recursivamente y sin usar (@), la función
amplia :: 'a list ⇒ 'a ⇒ 'a list
tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
final de la lista xs. Por ejemplo,
amplia [d,a] t = [d,a,t]
------------------------------------------------------------------ *}

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia xs y = undefined"

value "amplia [d,a] t" -- "= [d,a,t]"

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

lemma "amplia xs y = xs @ [y]"
oops

end
</source>

R2

2018-07-16T10:55:14Z

WikiSysop:

<source lang="isabelle">
header {* R2: Razonamiento sobre programas en Isabelle/HOL *}

theory R2
imports Main
begin

text {* ---------------------------------------------------------------
Ejercicio 1. Definir la función
sumaImpares :: nat ⇒ nat
tal que (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 5 = 25
------------------------------------------------------------------ *}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares n = undefined"

value "sumaImpares 5" -- "= 25"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
sumaImpares n = n*n
------------------------------------------------------------------- *}

lemma "sumaImpares n = n*n"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
sumaPotenciasDeDosMasUno :: nat ⇒ nat
tal que
(sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.
Por ejemplo,
sumaPotenciasDeDosMasUno 3 = 16
------------------------------------------------------------------ *}

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno n = undefined"

value "sumaPotenciasDeDosMasUno 3" -- "= 16"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
oops

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
copia :: nat ⇒ 'a ⇒ 'a list
tal que (copia n x) es la lista formado por n copias del elemento
x. Por ejemplo,
copia 3 x = [x,x,x]
------------------------------------------------------------------ *}

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia n x = undefined"

value "copia 3 x" -- "= [x,x,x]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de xs cumplen
la propiedad p. Por ejemplo,
todos (λx. x>(1::nat)) [2,6,4] = True
todos (λx. x>(2::nat)) [2,6,4] = False
Nota: La conjunción se representa por ∧
----------------------------------------------------------------- *}

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p xs = undefined"

value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"
value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar que todos los elementos de (copia n x) son
iguales a x.
------------------------------------------------------------------- *}

lemma "todos (λy. y=x) (copia n x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ *}

fun factR :: "nat ⇒ nat" where
"factR n = undefined"

value "factR 4" -- "= 24"

text {* ---------------------------------------------------------------
Ejercicio 9. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
------------------------------------------------------------------- *}

fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (Suc n)*x"

fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"

value "factI 4" -- "= 24"

lemma fact: "factI' n x = x * factR n"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
factI n = factR n
------------------------------------------------------------------- *}

corollary "factI n = factR n"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Definir, recursivamente y sin usar (@), la función
amplia :: 'a list ⇒ 'a ⇒ 'a list
tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
final de la lista xs. Por ejemplo,
amplia [d,a] t = [d,a,t]
------------------------------------------------------------------ *}

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia xs y = undefined"

value "amplia [d,a] t" -- "= [d,a,t]"

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

lemma "amplia xs y = xs @ [y]"
oops

end
</source>

R1

2018-07-16T10:54:59Z

WikiSysop:

<source lang="isabelle">
header {* R1: Programación funcional en Isabelle *}

theory R1
imports Main
begin

text {* ----------------------------------------------------------------
Ejercicio 0. Definir, por recursión, la función
factorial :: nat ⇒ nat
tal que (factorial n) es el factorial de n. Por ejemplo,
factorial 4 = 24
------------------------------------------------------------------- *}

fun factorial :: "nat ⇒ nat" where
"factorial n = undefined"

value "factorial 4" -- "24"

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud xs = undefined"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = undefined"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = undefined"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 4. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite n x = undefined"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc xs ys = undefined"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n xs = undefined"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n xs = undefined"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia xs = undefined"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux xs ys = undefined"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = undefined"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 10. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum xs = undefined"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f xs = undefined"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

end
</source>

Ejercicios

2018-07-16T10:54:44Z

WikiSysop:

Ejercicios

2018-07-16T10:53:59Z

WikiSysop: /* Relaciones de ejercicios */

En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deben tomarse como definitivas.

* '''Relación 1''': Programación funcional en Isabelle/HOL. ([[R1 |Enunciado]]).
* '''Relación 2''': Razonamiento automático sobre programas en Isabelle/HOL. ([[R2 |Enunciado]]).
* '''Relación 3''': Razonamiento estructurado sobre programas en Isabelle/HOL. ([[R3 |Enunciado]]).
* '''Relación 4''': Cons inverso. ([[R4 |Enunciado]]).
* '''Relación 5''': Cuantificadores sobre listas. ([[R5 |Enunciado]]).
* '''Relación 6''': Sustitución, inversión y eliminación. ([[R6 |Enunciado]]).
* '''Relación 7''': Recorridos de árboles. ([[R7 |Enunciado]]).
* '''Relación 8''': Árboles binarios completos. ([[R8 |Enunciado]]).
* '''Relación 9''': Deducción natural en Isabelle/HOL. ([[R9 |Enunciado]]).
* '''Relación 10''': Formalización y argumentación en Isabelle/HOL. ([[R10 |Enunciado]]).
* '''Relación 11''': Plegados de listas y de árboles. ([[R11 |Enunciado]]).

Tema 3: Razonamiento estructurado sobre programas en Isabelle/HOL

2018-07-16T10:52:34Z

WikiSysop:

<source lang="isabelle">
header {* Tema 3: Razonamiento sobre programas *}

theory T3_Razonamiento_sobre_programas
imports Main
begin

text {*
En este tema se demuestra con Isabelle las propiedades de los
programas funcionales como se expone en el tema 2a y se demostraron
automáticamente en el tema 2b. A diferencia del tema 2b, ahora
nos fijamos no sólo en el método de demostración sino en la estructura
de la prueba resaltando su semejanza con las del tema 2a. *}

section {* Razonamiento ecuacional *}

text {* ----------------------------------------------------------------
Ejemplo 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [a,c,d] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x#xs) = 1 + longitud xs"

value "longitud [a,c,d]" -- "= 3"

text {* ---------------------------------------------------------------
Ejemplo 2. Demostrar que
longitud [a,c,d] = 3
------------------------------------------------------------------- *}

lemma "longitud [a,c,d] = 3"
by simp

text {* ---------------------------------------------------------------
Ejemplo 3. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejemplo 4. (p.6) Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

-- "La demostración detallada es"
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
have "intercambia (intercambia (x,y)) = intercambia (y,x)"
by (simp only: intercambia.simps)
also have "... = (x,y)"
by (simp only: intercambia.simps)
finally show "intercambia (intercambia (x,y)) = (x,y)" by simp
qed

text {*
Notas sobre el lenguaje: En la demostración anterior se ha usado
· "proof" para iniciar la prueba,
· "-" (después de "proof") para no usar el método por defecto,
· "have" para establecer un paso,
· "by (simp only: intercambia.simps)" para indicar que sólo se usa
como regla de escritura la correspondiente a la definición de
intercambia,
· "also" para encadenar pasos ecuacionales,
· "..." para representar la igualdad anterior en un razonamiento
ecuacional,
· "finally" para indicar el último pasa de un razonamiento ecuacional,
· "show" para establecer la conclusión.
· "by simp" para indicar el método de demostración por simplificación y
· "qed" para terminar la pruebas,
*}

text {*
La definición de la función intercambia genera una regla de
simplificación
· intercambia.simps: intercambia (x,y) = (y,x)

Se puede ver con
· thm intercambia.simps
*}

-- "La demostración estructurada es"
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
have "intercambia (intercambia (x,y)) = intercambia (y,x)" by simp
also have "... = (x,y)" by simp
finally show "intercambia (intercambia (x,y)) = (x,y)" by simp
qed

text {*
Nota: La diferencia entre las dos demostraciones es que en los dos
primeros pasos no se explicita la regla de simplificación.
*}

-- "La demostración automática es"
lemma "intercambia (intercambia (x,y)) = (x,y)"
by simp

text {* ---------------------------------------------------------------
Ejemplo 5. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ [x]"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejemplo 6. (p. 9) Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

-- "La demostración detallada es"
lemma "inversa [x] = [x]"
proof -
have "inversa [x] = inversa (x#[])" by simp
also have "... = (inversa []) @ [x]" by (simp only: inversa.simps(2))
also have "... = [] @ [x]" by (simp only: inversa.simps(1))
also have "... = [x]" by (simp only: append_Nil)
finally show "inversa [x] = [x]" by simp
qed

text {*
En la demostración anterior se han usado las siguientes reglas:
· inversa.simps(1): inversa [] = []
· inversa.simps(2): inversa (x#xs) = inversa xs @ [x]
· append_Nil: [] @ ys = ys
*}

-- "La demostración estructurada es"
lemma "inversa [x] = [x]"
proof -
have "inversa [x] = inversa (x#[])" by simp
also have "... = (inversa []) @ [x]" by simp
also have "... = [] @ [x]" by simp
also have "... = [x]" by simp
finally show "inversa [x] = [x]" by simp
qed

-- "La demostración automática es"
lemma "inversa [x] = [x]"
by simp

section {* Razonamiento por inducción sobre los naturales *}

text {*
[Principio de inducción sobre los naturales] Para demostrar una
propiedad P para todos los números naturales basta probar que el 0
tiene la propiedad P y que si n tiene la propiedad P, entonces n+1
también la tiene.
⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P m

En Isabelle el principio de inducción sobre los naturales está
formalizado en el teorema nat.induct y puede verse con
thm nat.induct
*}

text {* ---------------------------------------------------------------
Ejemplo 7. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
| "repite (Suc n) x = x # (repite n x)"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejemplo 8. (p. 18) Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "longitud (repite n x) = n"
proof (induct n)
show "longitud (repite 0 x) = 0" by simp
next
fix n
assume HI: "longitud (repite n x) = n"
have "longitud (repite (Suc n) x) = longitud (x # (repite n x))"
by simp
also have "... = 1 + longitud (repite n x)" by simp
also have "... = 1 + n" using HI by simp
finally show "longitud (repite (Suc n) x) = Suc n" by simp
qed

text {*
Comentarios sobre la demostración anterior:
· A la derecha de proof se indica el método de la demostración.
· (induct n) indica que la demostración se hará por inducción en n.
· Se generan dos subobjetivos correspondientes a la base y el paso de
inducción:
1. longitud (repite 0 x) = 0
2. ⋀n. longitud (repite n x) = n ⟹ longitud (repite (Suc n) x) = Suc n
donde ⋀n se lee "para todo n".
· "next" indica el siguiente subobjetivo.
· "fix n" indica "sea n un número natural cualquiera"
· assume HI: "longitud (repite n x) = n" indica «supongamos que
"longitud (repite n x) = n" y sea HI la etiqueta de este supuesto».
· "using HI" usando la propiedad etiquetada con HI.
*}

-- "La demostración automática es"
lemma "longitud (repite n x) = n"
by (induct n) auto

section {* Razonamiento por inducción sobre listas *}

text {*
Para demostrar una propiedad para todas las listas basta demostrar
que la lista vacía tiene la propiedad y que al añadir un elemento a una
lista que tiene la propiedad se obtiene otra lista que también tiene la
propiedad.

En Isabelle el principio de inducción sobre listas está formalizado
mediante el teorema list.induct
⟦P [];
⋀x xs. P xs ⟹ P (x#xs)⟧
⟹ P xs
*}

text {* ---------------------------------------------------------------
Ejemplo 9. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejemplo 10. (p. 24) Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
show "conc [] (conc ys zs) = conc (conc [] ys) zs" by simp
next
fix x xs
assume HI: "conc xs (conc ys zs) = conc (conc xs ys) zs"
have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" by simp
also have "... = x # (conc (conc xs ys) zs)" using HI by simp
also have "... = conc (conc (x # xs) ys) zs" by simp
finally show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs" by simp
qed

text {*
Comentario sobre la demostración anterior
· (induct xs) genera dos subobjetivos:
1. conc [] (conc ys zs) = conc (conc [] ys) zs
2. ⋀a xs. conc xs (conc ys zs) = conc (conc xs ys) zs ⟹
conc (a#xs) (conc ys zs) = conc (conc (a#xs) ys) zs
*}

-- "La demostración automática es"
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejemplo 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

lemma "conc xs ys = conc ys xs"
quickcheck
oops

text {* Encuentra el contraejemplo,
xs = [a⇣2]
ys = [a⇣1] *}

text {* ---------------------------------------------------------------
Ejemplo 12. (p. 28) Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "conc xs [] = xs"
proof (induct xs)
show "conc [] [] = []" by simp
next
fix x xs
assume HI: "conc xs [] = xs"
have "conc (x # xs) [] = x # (conc xs [])" by simp
also have "... = x # xs" using HI by simp
finally show "conc (x # xs) [] = x # xs" by simp
qed

-- "La demostración automática es"
lemma "conc xs [] = xs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejemplo 13. (p. 30) Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

-- "La demostración automática es"
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
proof (induct xs)
show "longitud (conc [] ys) = longitud [] + longitud ys" by simp
next
fix x xs
assume HI: "longitud (conc xs ys) = longitud xs + longitud ys"
have "longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))"
by simp
also have "... = 1 + longitud (conc xs ys)" by simp
also have "... = 1 + longitud xs + longitud ys" using HI by simp
also have "... = longitud (x # xs) + longitud ys" by simp
finally show "longitud (conc (x # xs) ys) =
longitud (x # xs) + longitud ys" by simp
qed

-- "La demostración automática es"
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto

section {* Inducción correspondiente a la definición recursiva *}

text {* ---------------------------------------------------------------
Ejemplo 14. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []"
| "coge 0 xs = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejemplo 15. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {*
La definición coge genera el esquema de inducción coge.induct:
⟦⋀n. P n [];
⋀x xs. P 0 (x#xs);
⋀n x xs. P n xs ⟹ P (Suc n) (x#xs)⟧
⟹ P n x

Puede verse usando "thm coge.induct". *}

text {* ---------------------------------------------------------------
Ejemplo 16. (p. 35) Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "conc (coge n xs) (elimina n xs) = xs"
proof (induct rule: coge.induct)
fix n
show "conc (coge n []) (elimina n []) = []" by simp
next
fix x xs
show "conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs" by simp
next
fix n x xs
assume HI: "conc (coge n xs) (elimina n xs) = xs"
have "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) =
conc (x#(coge n xs)) (elimina n xs)" by simp
also have "... = x#(conc (coge n xs) (elimina n xs))" by simp
also have "... = x#xs" using HI by simp
finally show "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs"
by simp
qed

text {*
Comentario sobre la demostración anterior:
· (induct rule: coge.induct) indica que el método de demostración es
por el esquema de inducción correspondiente a la definición de la
función coge.
· Se generan 3 subobjetivos:
· 1. ⋀n. conc (coge n []) (elimina n []) = []
· 2. ⋀x xs. conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs
· 3. ⋀n x xs.
conc (coge n xs) (elimina n xs) = xs ⟹
conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs
*}

-- "La demostración automática es"
lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: coge.induct) auto

section {* Razonamiento por casos *}

text {* ---------------------------------------------------------------
Ejemplo 17. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejemplo 18 (p. 39) . Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
assume "xs = []"
then show "esVacia xs = esVacia (conc xs xs)" by simp
next
fix y ys
assume "xs = y#ys"
then show "esVacia xs = esVacia (conc xs xs)" by simp
qed

text {*
Comentarios sobre la demostración anterior:
· "(cases xs)" es el método de demostración por casos según xs.
· Se generan dos subobjetivos correspondientes a los dos
constructores de listas:
· 1. xs = [] ⟹ esVacia xs = esVacia (conc xs xs)
· 2. ⋀y ys. xs = y#ys ⟹ esVacia xs = esVacia (conc xs xs)
· "then" indica "usando la propiedad anterior"
*}

-- "La demostración estructurada simplificada es"
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
case Nil
thus "esVacia xs = esVacia (conc xs xs)" by simp
next
case Cons
thus "esVacia xs = esVacia (conc xs xs)" by simp
qed

text {*
Comentarios sobre la demostración anterior:
· "case Nil" es una abreviatura de "assume xs = []"
· "case Cons" es una abreviatura de "fix y ys assume xs = y#ys"
· "thus" es una abreviatura de "then show".
*}

-- "La demostración automática es"
lemma "esVacia xs = esVacia (conc xs xs)"
by (cases xs) auto

section {* Heurística de generalización *}

text {*
Heurística de generalización: Cuando se use demostración estructural,
cuantificar universalmente las variables libres (o, equivalentemente,
considerar las variables libres como variables arbitrarias). *}

text {* ---------------------------------------------------------------
Ejemplo 19. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejemplo 20. (p. 44) Demostrar que
inversaAcAux xs ys = (inversa xs) @ ys
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs) @ ys"
proof (induct xs arbitrary: ys)
show "⋀ys. inversaAcAux [] ys = inversa [] @ ys" by simp
next
fix a xs
assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"
show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"
proof -
fix ys
have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" by simp
also have "… = inversa xs@(a#ys)" using HI by simp
also have "… = inversa (a#xs)@ys" by simp
finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp
qed
qed

text {*
Comentarios sobre la demostración anterior:
· "(induct xs arbitrary: ys)" es el método de demostración por
inducción sobre xs usando ys como variable arbitraria.
· Se generan dos subobjetivos:
· 1. ⋀ys. inversaAcAux [] ys = inversa [] @ ys
· 2. ⋀a xs ys. (⋀ys. inversaAcAux xs ys = inversa xs @ ys) ⟹
inversaAcAux (a # xs) ys = inversa (a # xs) @ ys
· Dentro de una demostración se pueden incluir otras demostraciones.
· Para demostrar la propiedad universal "⋀ys. P(ys)" se elige una
lista arbitraria (con "fix ys") y se demuestra "P(ys)".
*}

-- "La demostración automática es"
lemma "inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

text {* ---------------------------------------------------------------
Ejemplo 21. (p. 43) Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

-- "La demostración automática es"
corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

text {*
Comentario de la demostración anterior:
· "(simp add: inversaAcAux_es_inversa)" es el método de demostración
por simplificación usando como regla de simplificación la propiedad
inversaAcAux_es_inversa.
*}

section {* Demostración por inducción para funciones de orden superior *}

text {* ---------------------------------------------------------------
Ejemplo 22. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejemplo 23. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

text {* ---------------------------------------------------------------
Ejemplo 24. (p. 45) Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
proof (induct xs)
show "sum (map (λx. 2*x) []) = 2 * (sum [])" by simp
next
fix a xs
assume HI: "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
have "sum (map (λx. 2*x) (a#xs)) = sum ((2*a)#(map (λx. 2*x) xs))"
by simp
also have "... = 2*a + sum (map (λx. 2*x) xs)" by simp
also have "... = 2*a + 2*(sum xs)" using HI by simp
also have "... = 2*(a + sum xs)" by simp
also have "... = 2*(sum (a#xs))" by simp
finally show "sum (map (λx. 2*x) (a#xs)) = 2*(sum (a#xs))" by simp
qed

-- "La demostración automática es"
lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejemplo 25. (p. 48) Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "longitud (map f xs) = longitud xs"
proof (induct xs)
show "longitud (map f []) = longitud []" by simp
next
fix a xs
assume HI: "longitud (map f xs) = longitud xs"
have "longitud (map f (a#xs)) = longitud (f a # (map f xs))" by simp
also have "... = 1 + longitud (map f xs)" by simp
also have "... = 1 + longitud xs" using HI by simp
also have "... = longitud (a#xs)" by simp
finally show "longitud (map f (a#xs)) = longitud (a#xs)" by simp
qed

-- "La demostración automática es"
lemma "longitud (map f xs) = longitud xs"
by (induct xs) auto

section {* Referencias *}

text {*
· J.A. Alonso. "Razonamiento sobre programas" http://goo.gl/R06O3
· G. Hutton. "Programming in Haskell". Cap. 13 "Reasoning about
programms".
· S. Thompson. "Haskell: the Craft of Functional Programming, 3rd
Edition. Cap. 8 "Reasoning about programms".
· L. Paulson. "ML for the Working Programmer, 2nd Edition". Cap. 6.
"Reasoning about functional programs".
*}

end
</source>

Tema 2b: Razonamiento automático sobre programas en Isabelle/HOL

2018-07-16T10:52:11Z

WikiSysop:

<source lang="isabelle">
header {* Tema 2: Razonamiento automático sobre programas en Isabelle/HOL *}

theory T2_Razonamiento_sobre_programas
imports Main
begin

text {*
En este tema se demuestra con Isabelle las propiedades de los
programas funcionales como se expone en el tema 8 del curso
"Informática" que puede leerse en http://goo.gl/Imvyt *}

section {* Razonamiento ecuacional *}

text {* ----------------------------------------------------------------
Ejemplo 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x#xs) = 1 + longitud xs"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejemplo 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

lemma "longitud [4,2,5] = 3"
by simp

text {* ---------------------------------------------------------------
Ejemplo 3. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejemplo 4. (p.6) Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

lemma "intercambia (intercambia (x,y)) = (x,y)"
by simp

text {* ---------------------------------------------------------------
Ejemplo 5. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ [x]"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejemplo 6. (p. 9) Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

lemma "inversa [x] = [x]"
by simp

section {* Razonamiento por inducción sobre los naturales *}

text {*
[Principio de inducción sobre los naturales] Para demostrar una
propiedad P para todos los números naturales basta probar que el 0
tiene la propiedad P y que si n tiene la propiedad P, entonces n+1
también la tiene.
⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P m

En Isabelle el principio de inducción sobre los naturales está
formalizado en el teorema nat.induct y puede verse con
thm nat.induct
*}

thm nat.induct

text {* ---------------------------------------------------------------
Ejemplo 7. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
| "repite (Suc n) x = x # (repite n x)"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejemplo 8. (p. 18) Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

lemma "longitud (repite n x) = n"
by (induct n) auto

section {* Razonamiento por inducción sobre listas *}

text {*
Para demostrar una propiedad para todas las listas basta demostrar
que la lista vacía tiene la propiedad y que al añadir un elemento a una
lista que tiene la propiedad se obtiene otra lista que también tiene la
propiedad.

En Isabelle el principio de inducción sobre listas está formalizado
mediante el teorema list.induct que puede verse con
thm list.induct
*}

thm list.induct

text {* ---------------------------------------------------------------
Ejemplo 9. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejemplo 10. (p. 24) Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejemplo 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

lemma "conc xs ys = conc ys xs"
quickcheck
oops

text {* Encuentra el contraejemplo,
xs = [a⇣2]
ys = [a⇣1] *}

text {* ---------------------------------------------------------------
Ejemplo 12. (p. 28) Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

lemma "conc xs [] = xs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejemplo 13. (p. 30) Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto

section {* Inducción correspondiente a la definición recursiva *}

text {* ---------------------------------------------------------------
Ejemplo 14. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []"
| "coge 0 xs = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejemplo 15. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {*
La definición coge genera el esquema de inducción coge.induct:
⟦⋀n. P n [];
⋀x xs. P 0 (x#xs);
⋀n x xs. P n xs ⟹ P (Suc n) (x#xs)⟧
⟹ P n x

Puede verse usando "thm coge.induct". *}

text {* ---------------------------------------------------------------
Ejemplo 16. (p. 35) Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: coge.induct) auto

section {* Razonamiento por casos *}

text {*
Distinción de casos sobre listas:
· El método de distinción de casos se activa con (cases xs) donde xs
es del tipo lista.
· "case Nil" es una abreviatura de
"assume Nil: xs =[]".
· "case Cons" es una abreviatura de
"fix ? ?? assume Cons: xs = ? # ??"
donde ? y ?? son variables anónimas. *}

text {* ---------------------------------------------------------------
Ejemplo 17. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejemplo 18 (p. 39) . Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

lemma "esVacia xs = esVacia (conc xs xs)"
by (cases xs) auto

section {* Heurística de generalización *}

text {*
Heurística de generalización: Cuando se use demostración estructural,
cuantificar universalmente las variables libres (o, equivalentemente,
considerar las variables libres como variables arbitrarias). *}

text {* ---------------------------------------------------------------
Ejemplo 19. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejemplo 20. (p. 44) Demostrar que
inversaAcAux xs ys = (inversa xs) @ ys
------------------------------------------------------------------- *}

lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

text {* ---------------------------------------------------------------
Ejemplo 21. (p. 43) Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

-- "La demostración automática es"
corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

section {* Demostración por inducción para funciones de orden superior *}

text {* ---------------------------------------------------------------
Ejemplo 22. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejemplo 23. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

text {* ---------------------------------------------------------------
Ejemplo 24. (p. 45) Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejemplo 25. (p. 48) Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

lemma "longitud (map f xs) = longitud xs"
by (induct xs) auto

section {* Referencias *}

text {*
· J.A. Alonso. "Razonamiento sobre programas" http://goo.gl/R06O3
· G. Hutton. "Programming in Haskell". Cap. 13 "Reasoning about
programms". http://bit.ly/1gMqK0X
· S. Thompson. "Haskell: the Craft of Functional Programming, 3rd
Edition. Cap. 8 "Reasoning about programms".
· L. Paulson. "ML for the Working Programmer, 2nd Edition". Cap. 6.
"Reasoning about functional programs". http://bit.ly/1gMqFKI
*}

end
</source>

Tema 1: Programación funcional en Isabelle

2018-07-16T10:51:54Z

WikiSysop:

<source lang="isabelle">
header {* Tema 1: Programación funcional en Isabelle *}

theory T1
imports Main
begin

section {* Introducción *}

text {* En este tema se presenta el lenguaje funcional que está
incluido en Isabelle. El lenguaje funcional es muy parecido a
Haskell. *}

section {* Números naturales, enteros y booleanos *}

text {* En Isabelle están definidos los número naturales con la sintaxis
de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).

Los números como el 1 son abreviaturas de los correspondientes en la
notación de Peano, en este caso "Suc 0".

El tipo de los números naturales es nat.

Por ejemplo, el siguiente del 0 es el 1. *}

value "Suc 0" -- "= 1"

text {* En Isabelle está definida la suma de los números naturales:
(x + y) es la suma de x e y.

Por ejemplo, la suma de los números naturales 1 y 2 es el número
natural 3. *}

value "(1::nat) + 2" -- "= 3"

text {* La notación del par de dos puntos se usa para asignar un tipo a
un término (por ejemplo, (1::nat) significa que se considera que 1 es
un número natural).

En Isabelle está definida el producto de los números naturales:
(x * y) es el producto de x e y.

Por ejemplo, el producto de los números naturales 2 y 3 es el número
natural 6. *}

value "(2::nat) * 3" -- "= 6"

text {* En Isabelle está definida la división de números naturales:
(n div m) es el cociente entero de x entre y.

Por ejemplo, la división natural de 7 entre 3 es 2. *}

value "(7::nat) div 3" -- "= 2"

text {* En Isabelle está definida el resto de división de números
naturales: (n mod m) es el resto de dividir n entre m.

Por ejemplo, el resto de dividir 7 entre 3 es 1. *}

value "(7::nat) mod 3" -- "= 1"

text {* En Isabelle también están definidos los números enteros. El tipo
de los enteros se representa por int.

Por ejemplo, la suma de 1 y -2 es el número entero -1. *}

value "(1::int) + -2" -- "= -1"

text {* Los numerales están sobrecargados. Por ejemplo, el 1 puede ser
un natural o un entero, dependiendo del contexto.

Isabelle resuelve ambigüedades mediante inferencia de tipos.

A veces, es necesario usar declaraciones de tipo para resolver la
ambigüedad.

En Isabelle están definidos los valores booleanos (True y False), las
conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃).

El tipo de los booleanos es bool. *}

text {* La conjunción de dos fórmulas verdaderas es verdadera. *}
value "True ∧ True" -- "= True"

text {* La conjunción de un fórmula verdadera y una falsa es falsa. *}
value "True ∧ False" -- "= False"

text {* La disyunción de una fórmula verdadera y una falsa es
verdadera. *}
value "True ∨ False" -- "= True"

text {* La disyunción de dos fórmulas falsas es falsa. *}
value "False ∨ False" -- "= False"

text {* La negación de una fórmula verdadera es falsa. *}
value "¬True" -- "= False"

text {* Una fórmula falsa implica una fórmula verdadera. *}
value "False ⟶ True" -- "= True"

text {* Un lema introduce una proposición seguida de una demostración.

Isabelle dispone de varios procedimientos automáticos para generar
demostraciones, uno de los cuales es el de simplificación (llamado
simp).

El procedimiento simp aplica un conjunto de reglas de reescritura, que
inicialmente contiene un gran número de reglas relativas a los objetos
definidos. *}

text {* Ej. de simp: Todo elemento es igual a sí mismo. *}
lemma "∀x. x = x"
by simp

text {* Ej. de simp: Existe un elemento igual a 1. *}
lemma "∃x. x = 1"
by simp

section {* Definiciones no recursivas *}

text {* La disyunción exclusiva de A y B se verifica si una es verdadera
y la otra no lo es. *}

definition xor :: "bool ⇒ bool ⇒ bool" where
"xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"

text {* Prop.: La disyunción exclusiva de dos fórmulas verdaderas es
falsa.

Dem.: Por simplificación, usando la definición de la disyunción
exclusiva.
*}

lemma "xor True True = False"
by (simp add: xor_def)

text {* Se añade la definición de la disyunción exclusiva al conjunto de
reglas de simplificación automáticas. *}

declare xor_def [simp]

lemma "xor True False = True"
by simp

section {* Definiciones locales *}

text {* Se puede asignar valores a variables locales mediante 'let' y
usarlo en las expresiones dentro de 'in'.

Por ejemplo, si x es el número natural 3, entonces "x*x=9". *}

value "let x = 3::int in x * x" -- "= 9"

section {* Pares *}

text {* Un par se representa escribiendo los elementos entre paréntesis
y separados por coma.

El tipo de los pares es el producto de los tipos.

La función fst devuelve el primer elemento de un par y la snd el
segundo.

Por ejemplo, si p es el par de números naturales (2,3), entonces la
suma del primer elemento de p y 1 es igual al segundo elemento de
p. *}

value "let p = (2,3)::nat × nat in fst p + 1 = snd p"

section {* Listas *}

text {* Una lista se representa escribiendo los elementos entre
corchetes y separados por comas.

La lista vacía se representa por [].

Todos los elementos de una lista tienen que ser del mismo tipo.

El tipo de las listas de elementos del tipo a es (a list).

El término (x#xs) representa la lista obtenida añadiendo el elemento x
al principio de la lista xs.

Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista
vacía los elementos c, b y a es [a,b,c]. *}

value "a#(b#(c#[]))" -- "= [a,b,c]"

text {* Funciones de descomposición de listas:
· (hd xs) es el primer elemento de la lista xs.
· (tl xs) es el resto de la lista xs.

Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a
y el resto de xs es [b,c]. *}

value "let xs = [a,b,c] in hd xs = a ∧ tl xs = [b,c]" -- "= True"

text {* (length xs) es la longitud de la lista xs. Por ejemplo, la
longitud de la lista [1,2,3] es 3. *}

value "length [1,2,3]" -- "= 3"

text {* En la página 8 de "What's in Main" http://bit.ly/1FYOzxq y
en la sesión 47 de "Isabelle/HOL — Higher-Order Logic"
http://bit.ly/1sKeuP3 se encuentran más definiciones y propiedades de
las listas. *}

section {* Funciones anónimas *}

text {* En Isabelle pueden definirse funciones anónimas.

Por ejemplo, el valor de la función que a un número le asigna su doble
aplicada a 1 es 2. *}

value "(λx. x + x) 1::int" -- "= 2"

section {* Condicionales *}

text {* El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso
contrario. *}

definition absoluto :: "int ⇒ int" where
"absoluto x ≡ (if x ≥ 0 then x else -x)"

text {* Ejemplo, el valor absoluto de -3 es 3. *}

value "absoluto(-3)" -- "= 3"

text {* Def.: Un número natural n es un sucesor si es de la forma
(Suc m). *}

definition es_sucesor :: "nat ⇒ bool" where
"es_sucesor n ≡ (case n of
0 ⇒ False
| Suc m ⇒ True)"

text {* Ejemplo, el número 3 es sucesor. *}

value "es_sucesor 3" -- "= True"

section {* Tipos de datos y definiciones recursivas *}

text {* Una lista de elementos de tipo a es la lista Vacia o se obtiene
añadiendo, con Cons, un elemento de tipo a a una lista de elementos de
tipo a. *}

datatype 'a Lista = Vacia | Cons 'a "'a Lista"

text {* (conc xs ys) es la concatenación de las lista xs e ys. Por
ejemplo,
conc (Cons a (Cons b Vacia)) (Cons c Vacia)
= Cons a (Cons b (Cons c Vacia))
*}

fun conc :: "'a Lista ⇒ 'a Lista ⇒ 'a Lista" where
"conc Vacia ys = ys"
| "conc (Cons x xs) ys = Cons x (conc xs ys)"

value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
-- "= Cons a (Cons b (Cons c Vacia))"

text {* (suma n) es la suma de los primeros n números naturales. Por
ejemplo,
suma 3 = 6
*}

fun suma :: "nat ⇒ nat" where
"suma 0 = 0"
| "suma (Suc m) = (Suc m) + suma m"

value "suma 3" -- "= 6"

text {* (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 3 = 9
*}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n"

value "sumaImpares 3" -- "= 9"

end
</source>

Razonamiento automático (2015-16)

2018-07-16T10:51:33Z

WikiSysop:

Este sitio contiene materiales del curso ''Razonamiento automático'' del [http://master.cs.us.es/Máster_Universitario_en_Lógica,_Computación_e_Inteligencia_Artificial Máster Universitario en Lógica, Computación e Inteligencia Artificial] de la [http://www.us.es Universidad de Sevilla].

== Material para el curso ==
* [[Temas]]: Teorías de los temas.
* [[Ejercicios]]: Relaciones de ejercicios.
* [[Documentación]]: Lecturas recomendadas.
* [[Sistemas]]: Sistemas utilizados.
* [http://www.glc.us.es/~jalonso/vestigium/tag/ra2015 Diario]: Descripción diaria de las clases.

MediaWiki:Common.css

2018-07-16T10:51:05Z

WikiSysop: Página creada con «/* Los estilos CSS colocados aquí se aplicarán a todas las apariencias */ @import url("/~jalonso/font-awesome-4.7.0/css/font-awesome.min.css");»

/* Los estilos CSS colocados aquí se aplicarán a todas las apariencias */
@import url("/~jalonso/font-awesome-4.7.0/css/font-awesome.min.css");

Relación 1

2015-11-24T14:05:37Z

WikiSysop: Desprotegió «Relación 1»

<source lang="isar">
header {* R1: Programación funcional en Isabelle *}

theory R1
imports Main
begin

text {* ----------------------------------------------------------------
Ejercicio 0. Definir, por recursión, la función
factorial :: nat ⇒ nat
tal que (factorial n) es el factorial de n. Por ejemplo,
factorial 4 = 24
------------------------------------------------------------------- *}

fun factorial :: "nat ⇒ nat" where
"factorial n = undefined"

value "factorial 4" -- "24"

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud xs = undefined"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = undefined"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = undefined"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 4. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite n x = undefined"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc xs ys = undefined"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n xs = undefined"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n xs = undefined"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia xs = undefined"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux xs ys = undefined"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = undefined"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 10. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum xs = undefined"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f xs = undefined"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

end
</source>

R1

2015-11-24T14:05:09Z

WikiSysop: Protegió «R1» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

R1

2015-11-24T14:04:56Z

WikiSysop: Página creada con '<source lang="isar"> header {* R1: Programación funcional en Isabelle *} theory R1 imports Main begin text {* ---------------------------------------------------------------...'

Relación 1

2015-11-24T14:04:25Z

WikiSysop: Protegió «Relación 1» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Relación 1

2015-11-24T14:04:13Z

Ejercicios

2015-11-24T14:03:21Z

WikiSysop: Protegió «Ejercicios» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

== Relaciones de ejercicios ==

En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deben tomarse como definitivas.

* '''Relación 1''': Programación funcional en Isabelle/HOL. ([[R1 |Enunciado]] y [[Relación 1 | Solución colaborativa]]).

Ejercicios

2015-11-24T14:03:09Z

WikiSysop:

Documentación

2015-10-15T06:21:18Z

WikiSysop: Página creada con 'En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (DAO). == Visiones generales de la DAO == # J.A. Alonso. [h...'

En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (DAO).

== Visiones generales de la DAO ==

# J.A. Alonso. [http://goo.gl/NWk7b Razonamiento formalizado: Del sueño a la realidad de las pruebas]. ''Vestigium'', 26 de diciembre de 2012.
# J. Avigad. [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation]. ICERM, 14 de diciembre de 2012.
# M. Davis. [http://www.cs.nyu.edu/cs/faculty/davism/early.ps The early history of automated deduction].
# J.P. Delahaye [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. ''Interstices'', 8 de julio de 2012.
# J. Germoni [http://images.math.cnrs.fr/Coq-et-caracteres.html Coq et caractères: Preuve formelle du théorème de Feit et Thompson]. ''Images des Mathématiques'', CNRS, 23 de noviembre de 2012.
# H. Geuvers [http://www.ias.ac.in/sadhana/Pdf2009Feb/3.pdf Proof assistants: History, ideas and future]. ''Sadhana'', Vol. 34-1, pp. 3-25, février 2009.
# G. Gonthier [http://www.ams.org/notices/200811/tx081101382p.pdf The four-color theorem]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1382-1393, 2008.
# T. Hales. [http://www.ams.org/notices/200811/tx081101370p.pdf Formal proof]. ''Notices of AMS'', Vol. 55, N. 11 (2008) pp. 1370-1380.
# J. Harrison. [http://www.cl.cam.ac.uk/~jrh13/papers/ab.html A short survey of automated reasoning]. ''Lecture Notes in Computer Science'', Vol. 4545, pp. 334-349, 2007.
# J. Harrison. [http://www.ams.org/notices/200811/tx081101395p.pdf Formal proof: Theory and practice]. ''Notices of the AMS'', Vol. 55, N. 11 (2008) p.1395-1406.
# G. Kolata. [http://www.nytimes.com/library/cyber/week/1210math.html Computer math proof shows reasoning power]. ''The New York Times'', 10 de diciembre de 1996.
# D. MacKenzie [http://www.bcs.org/server.php?show=ConWebDoc.4364 Computers and the sociology of mathematical proof].
# G. Sutcliffe. [http://www.cs.miami.edu/~tptp/OverviewOfATP.html What is automated theorem proving?].
# F. Wiedijk [http://www.cs.ru.nl/~freek/100/ Formalizing the «top 100» of mathematical theorems].
# F. Wiedijk [http://www.ams.org/notices/200811/tx081101408p.pdf Formal proof - Getting started]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1408-1414, 2008.
# F. Wiedijk, [http://www.cs.ru.nl/~freek/pubs/qed2.ps.gz The QED manifesto revisited]. ''Studies in Logic, Grammar and Rhetoric'', Vol. 10(23), pp. 121-133, 2007.

== Referencias sobre Isabelle/HOL ==
# B. Grechuk [http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf Isabelle primer for mathematicians].
# T. Nipkow [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/prog-prove.pdf Programming and proving in Isabelle/HOL]. 5 de diciembre de 2013.
# T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag. 5 de diciembre de 2013.
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 5 de diciembre de 2013.
# M. Wenzel [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/isar-ref.pdf The Isabelle/Isar Reference Manual]. 5 de diciembre de 2013.
# M. Wenzel [https://www.lri.fr/~wenzel/Isabelle2011-Paris/quickref.pdf The Isabelle/Isar quick reference].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref.pdf Quick Reference for Isabelle/Isar Propositional Logic].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref2.pdf Quick Reference for Isabelle/Isar More Proof Techniques].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref3.pdf Quick Reference for Isabelle/Isar First-Order Logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html Tutorials and manuals for Isabelle2013].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/i1m/temas/2012-13-IM-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# J.A. Alonso y M.J. Hidalgo [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# G. Hutton [http://goo.gl/pKqG Programming in Haskell]. Cambridge University Press, 2007.
# M. Lipovača [http://aprendehaskell.es ¡Aprende Haskell por el bien de todos!].

=== Lógica computacional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/temas/temas-LI-2012-13.pdf Temas de "Lógica informática" (2012-13)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# R. Bornat [http://bit.ly/oithic Proof and disproof in formal logic: an introduction for programmers]. Oxford University Press, 2005.
# K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers [http://pubs.doc.ic.ac.uk/reasoned-programming/reasoned-programming.pdf Reasoned programming]. Imperial College, 1994.
# K. Doets y J. van Eijck [http://www.ldc.usb.ve/~astorga/Haskell.Road.pdf The Haskell Road to Logic, Maths and Programming].
# M. Huth y M. Ryan [http://goo.gl/TMqOo Logic in computer science: Modelling and reasoning about systems]. Cambridge University Press, 2004. (Incluye el [http://www.cs.bham.ac.uk/research/lics/tutor/index.html tutor en la Red]).

== Cursos relacionados ==
=== Cursos con Isabelle/HOL ===
# Jeremy Avigad. [http://www.phil.cmu.edu/~avigad/formal/ Logic and Formal Verification]. (Carnegie Mellon, 2009).
# Clemens Ballarin. [http://cl-informatik.uibk.ac.at/teaching/ss08/atp/introduction.php Automatic Deduction]. (Univ de Innsbruck, 2008).
# Clemens Ballarin. [http://www4.in.tum.de/~ballarin/belgrade08-tut/ Introduction to the Isabelle Proof Assistant]. (Belgrado, 2008).
# Clemens Ballarin y Gerwin Klein [http://isabelle.in.tum.de/coursematerial/IJCAR04 Introduction to the Isabelle Proof Assistant]. (en el IJCAR-2004).
# Clemens Ballarin y Tjark Weber. [http://cl-informatik.uibk.ac.at/teaching/ws06/atp/introduction.php Automated Theorem Proving in Isabelle/HOL]. (Univ. de Innsbruck, 2006-07).
# A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. [http://archiv.infsec.ethz.ch/education/permanent/csmr.html Computer-supported Modeling and Reasoning]. (ETH Zurich, 2011).
# Mads Dam. [http://www.csc.kth.se/utbildning/kth/kurser/DD2453/aform07/ Advanced formal methods]. (KTH Royal Institute of Technology, 2007).
# Jacques Fleuriot y Paul Jackson. [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/ Automated reasoning]. (Univ. de Edimburgo, 2012-13).
# Thomas Genet [http://www.irisa.fr/celtique/genet/ACF Software formal analysis and design]. (Univ. de Rennes)
# Gerwin Klein. [http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04 Theorem Proving - Principles, Techniques, Applications]. (NICTA, 2004).
# Gerwin Klein. [http://www.cse.unsw.edu.au/~cs4161/index.html Advanced Topics in Software Verification]. (NICTA, 2012).
# Joao Marcos. [http://www.dimap.ufrn.br/~jmarcos/courses/LC/Ementa.htm Lógica computacional: Demonstração assistida e semi-automática de teoremas].(UFRN, 2000).
# Tobias Nipkow. [http://www4.informatik.tu-muenchen.de/~nipkow/semantics/ Semantics of programming languages]. (Univ. de Munich, 2012-13).
# Tobias Nipkow [http://isabelle.in.tum.de/coursematerial/PSV2009-1 Theorem Proving with Isabelle/HOL An Intensive Course].
# Larry Paulson. [http://www.cl.cam.ac.uk/teaching/0910/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2009-10).
# Arnd Poetzsch-Heffter. [https://softech.informatik.uni-kl.de/Homepage/SVHOL10 Specification and Verification with Higher-Order Logic].
# Viorel Preoteasa, Ralph-Johan Back y Charmi Panchal. [http://users.abo.fi/vpreotea/isabelle-2012 Introduction to mechanized reasoning with Isabelle/HOL]. (Åbo Akademi University, 2012).
# Jeremy G. Siek. [http://www.cs.colorado.edu/~siek/7000/spring07/ Practical Theorem Proving with Isabelle/Isar]. (Univ. de Colorado, 2007).
# Jeremy G. Siek. [http://ecee.colorado.edu/~siek/ecen5013/spring11/ Theorem proving in Isabelle]. (Univ. de Colorado, 2011).
# Jan-Georg Smaus. [http://www.informatik.uni-freiburg.de/~ki/teaching/ws0910/csmr/lecture.html Computer-supported modeling and reasoning]. (Univ. de Feiburgo, 2009).
# Christian Sternagel [http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php Experiments in Verification – Introduction to Isabelle/HOL]. (Univ. de Innsbruck, 2011-12).
# Tjark Weber. [http://www.cl.cam.ac.uk/teaching/1011/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2010-11).

=== Otros cursos ===
# José A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/ Lógica informática] (Univ. de Sevilla, 2012-13).
# Thorsten Altenkirch y Peter Morris [http://www.cs.nott.ac.uk/~txa/g52ifr Introduction to formal reasoning] (Univ. de Nottingham, 2010-11).
# Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi [http://www.di.ens.fr/~zappa/teaching/coq/ecole11 Modelling and verifying algorithms in Coq: an introduction]. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
# Pierre Castéran [http://www.labri.fr/perso/casteran/FM/Logique/index.html Logic (Master In Verification)] (Univ. de Burdeos, 2011-12).
# Adam Chlipala [http://stellar.mit.edu/S/course/6/fa11/6.892/ Interactive computer theorem proving]. (MIT, 2012-13).
# Adam Chlipala y Armando Solar Lezama [https://stellar.mit.edu/S/course/6/fa13/6.820/index.html Foundations of program analysis]. (MIT, 2013-14).
# Robby Findler [http://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall Certified programming with dependent types]. (Northwestern, 2013-14).
# Nuno Gaspar [http://www-sop.inria.fr/members/Nuno.Gaspar/teaching/coq2012.php Verification with the Coq Proof Assistant] (INRIA Sophia Antipolis, 2012-13).
# Carlos Luna y Gustavo Betarte. [https://eva.fing.edu.uy/course/view.php?id=363 Construcción formal de programas en teoría de tipos]. (Univ. de la República, Uruguay, 2013-14).
# Michael Genesereth [http://logic.stanford.edu/classes/cs157/2011/cs157.html Computational Logic] (Univ. de Stanford, 2011-12).
# Ian Hodkinson [http://www.doc.ic.ac.uk/~imh/teaching/140_logic/logic.html Logic] (Imperial College, Londres, 2010-11).
# Peter Lucas [http://www.cs.ru.nl/~peterl/teaching/KeR/ Knowledge Representation and Reasoning] (Radboud University # egen, 2011-12).
# Larry Paulson [http://www.cl.cam.ac.uk/Teaching/current/LogicProof/ Logic and Proof] (Univ. de Cambridge, 2011-12).
# David Pichardie [http://www.irisa.fr/celtique/pichardie/teaching/M2/MDV/ Méthode de vérification] (Universidad de Rennes, 2006-07).
# Michael Winter [Logic in Computer Science] (Brock University, Ontario, Canada, 2010-11).

== Bibliotecas de ejemplos de verificación ==
# [http://afp.sourceforge.net Archive of Formal Proofs].
# [http://www.cs.ru.nl/~freek/100 Formalizing 100 Theorems].
# [http://toccata.lri.fr/gallery Gallery of verified programs].
# [http://www.cs.nott.ac.uk/~lad/research/challenges/ Induction Challenge Problems].
# [http://automatedreasoning.net/ Larry Wos' Notebooks].
# [http://www.cs.miami.edu/~tptp/ The TPTP Problem Library for Automated Theorem Proving].
# [http://www.macs.hw.ac.uk/vstte10/Competition.html The 1st Verified Software Competition].
# [https://sites.google.com/site/vstte2012/compet The 2nd Verified Software Competition].
# [http://verifythis.cost-ic0701.org VerifyThis (A collection of verification benchmarks].

== Artículos recientes ==
Están en orden cronológico inverso a la fecha de su reseña en [http://www.glc.us.es/~jalonso/vestigium/tag/resena Vestigium]:
# [http://bit.ly/1iZjgqN Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem]. L. Noschinski
# [http://bit.ly/1iJ8uVz A graph library for Isabelle]. ~ L. Noschinski
# [http://bit.ly/I0CU80 Gödel’s incompleteness theorems]. ~ L.C. Paulson
# [http://bit.ly/I0CPRN The hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/HBiIJI Applications of real number theorem proving in PVS]. ~ H. Gottliebsen, R. Hardy, O. Lightfoot y U. Martin
# [http://bit.ly/1awnMLB A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/19lWeYy Verified AIG algorithms in ACL2]. ~ J. Davis y S. Swords
# [http://bit.ly/GAhC00 A formal model and correctness proof for an access control policy framework]. ~ C. Wu, X. Zhang y C. Urban
# [http://bit.ly/16SMvSS The ontological argument in PVS]. ~ J. Rushby
# [http://bit.ly/1dRt9n0 Formalizing Moessner’s theorem and generalizations in Nuprl]. ~ M. Bickford, D. Kozen y A. Silva
# [http://bit.ly/1bSeDNB Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model]. ~ M. Ayala y Y. Santos
# [http://bit.ly/1feFqWE Proof assistant based on didactic considerations]. ~ J. Pais y A Tasistro
# [http://bit.ly/18tHNBi Theory exploration for interactive theorem proving]. ~ M. Johansson
# [http://bit.ly/1b0242s From Tarski to Hilbert]. ~ G. Braun y J. Narboux
# [http://bit.ly/18HaXaR Formal verification of language-based concurrent noninterference]. ~ A. Popescu, J. Hölzl y T. Nipkow
# [http://bit.ly/1aRTQsU A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm]. ~ C. Muñoz, A. Narkawicz y J. Chamberlain
# [http://bit.ly/1dNwhDI Formal verification of cryptographic security proofs]. ~ M. Berg
# [http://bit.ly/17muAUv Polygonal numbers in Mizar]. ~ A. Grabowski
# [http://bit.ly/1hk5z6L A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle]. ~ L.C. Paulson
# [http://bit.ly/1cSL0wE Steps towards verified implementations of HOL Light]. ~ M.O. Myreen, S. Owens y R. Kumar
# [http://bit.ly/16Kbgm0 Generic datatypes à la carte]. ~ S. Keuchel y T. Schrijvers
# [http://bit.ly/1bqJGx4 Proof pearl: A verified bignum implementation in x86-64 machine code]. ~ M.O. Myreen y G. Curello
# [http://bit.ly/142ow2Q Mechanized metatheory for a λ λ-calculus with trust types]. ~ R. Ribeiro, C. Camarão y L. Figueiredo
# [http://bit.ly/15WZBDy Proving soundness of combinatorial Vickrey auctions and generating verified executable code]. ~ M.B. Caminati, M. Kerber, C. Lange y C. Rowat
# [http://bit.ly/198g4n9 A computer-assisted proof of correctness of a marching cubes algorithm]. ~ A.N. Chernikov y J. Xu
# [http://bit.ly/11QA5g7 Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm]. ~ L. Lambán, J. Rubio, F.J. Martín y J.L. Ruiz
# [http://bit.ly/1cJAXYk The Königsberg bridge problem and the friendship theorem]. ~ W. Li
# [http://bit.ly/13DBK9R Formal verification of a proof procedure for the description logic ALC]. ~ M. Chaabani, M. Mezghiche y M. Strecker
# [http://bit.ly/1ep2ex9 Pratt’s primality certificates]. ~ S. Wimmer y L. Noschinski
# [http://bit.ly/13C95Ci Reasoning about higher-order relational specifications]. ~ Y. Wang, K. Chaudhuri, A. Gacek y G. Nadathur
# [http://bit.ly/18QQLcL Proofs you can believe in – Proving equivalences between Prolog semantics in Coq]. ~ J. Kriener, A. King y S. Blazy
# [http://bit.ly/19uc82J Certified, efficient and sharp univariate Taylor models in Coq]. ~ E. Martin-Dorel, L. Rideau, L. Théry, M. Mayero y I. Paşca
# [http://bit.ly/1c4Rzel Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁]. ~ M. Norrish y B. Huffman
# [http://bit.ly/14b4Akz Program verification based on Kleene algebra in Isabelle/HOL] ~ A. Armstrong, G. Struth y T. Weber
# [http://bit.ly/1aOgRKx Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)]. ~ C. Ballarin
# [http://bit.ly/11HKixj Computational verification of network programs in Coq]. ~ G. Stewart
# [http://www.glc.us.es/~jalonso/vestigium/resena-certifying-homological-algorithms-to-study-biomedical-images Certifying homological algorithms to study biomedical images]. ~ M. Poza
# [http://bit.ly/16Nks9m Formalizing cut elimination of coalgebraic logics in Coq]. ~ H. Tews
# [http://www.glc.us.es/~jalonso/vestigium/resena-the-formalization-of-syntax-based-mathematical-algorithms-using-quotation-and-evaluation/ The formalization of syntax-based mathematical algorithms using quotation and evaluation]. ~ W.M. Farmer
# [http://www.glc.us.es/~jalonso/vestigium/resena-certified-symbolic-manipulation-bivariate-simplicial-polynomials/ Certified symbolic manipulation: Bivariate simplicial polynomials]. ~ L. Lambán, F.J. Martín, J. Rubio y J.L. Ruiz
# [http://www.glc.us.es/~jalonso/vestigium/resena-solveurs-cpfd-verifies-formellement/ Solveurs CP(FD) vérifiés formellement]. ~ C Dubois y A. Gotlieb
# [http://www.glc.us.es/~jalonso/vestigium/resena-formalizing-bounded-increase/ Formalizing bounded increase]. ~ R. Thiemann
# [http://www.glc.us.es/~jalonso/vestigium/resena-formal-mathematics-on-display-a-wiki-for-flyspeck/ Formal mathematics on display: A wiki for Flyspeck]. ~ C. Tankink, C. Kaliszyk, J. Urban y H. Geuvers
# [http://www.glc.us.es/~jalonso/vestigium/resena-theorem-of-three-circles-in-coq Theorem of three circles in Coq]. ~ J. Zsidó
# [http://bit.ly/19fiWAY Certified HLints with Isabelle/HOLCF-Prelude]. ~ J. Breitner, B. Huffman, N. Mitchell y C. Sternagel
# [http://bit.ly/ZfSQrQ Automatic data refinement]. ~ P. Lammich
# [http://bit.ly/18vyjm7 The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)]. ~ A. Mahboubi
# [http://bit.ly/114oyZV Mechanical verification of SAT refutations with extended resolution]. ~ N. Wetzler, M.J.H. Heule y W.A. Hunt Jr.
# [http://bit.ly/13H0REu Type classes and filters for mathematical analysis in Isabelle/HOL] ~ J. Hölzl, F. Immler y B. Huffman
# [http://bit.ly/10fv8wO Verifying refutations with extended resolution]. ~ M. J. H. Heule, W. A. Hunt, Jr. y N. Wetzler
# [http://bit.ly/10EcFWj A Web interface for Isabelle: The next generation]. ~ C. Lüth y M. Ring
# [http://bit.ly/18P9CSv On the formalization of continuous-time Markov chains in HOL]. ~ L. Liu, O. Hasan y S. Tahar
# [http://bit.ly/17H2mqy Formalizing Turing machines]. ~ A. Asperti y W. Ricciotti
# [http://bit.ly/YwuCeL Light-weight containers for Isabelle: efficient, extensible, nestable]. ~ A. Lochbihler
# [http://bit.ly/10XLrRA Graph theory]. ~ L. Noschinski
# [http://bit.ly/19kPEP4 A machine-checked proof of the odd order theorem]. ~ G. Gonthier et als.
# [http://goo.gl/LdihL A constructive theory of regular languages in Coq]. ~ C. Doczkal, J.O. Kaiser y G. Smolka
# [http://goo.gl/gwcwL A formal proof of Kruskal’s tree theorem in Isabelle/HOL]. ~ C. Sternagel
# [http://goo.gl/CUF3e Formalizing Knuth-Bendix orders and Knuth-Bendix completion]. ~ C. Sternagel y R. Thiemann
# [http://goo.gl/9JAfX Developing an auction theory toolbox]. ~ C. Lange, C. Rowat, W. Windsteiger y M. Kerber
# [http://goo.gl/6OfmQ Formalization of incremental simplex algorithm by stepwise refinement]. ~ M. Spasić y F. Marić
# [http://goo.gl/Guxky Coinductive pearl: Modular first-order logic completeness]. ~ J.C. Blanchette, A. Popescu y D. Traytel
# [http://goo.gl/HUOl8 A fully verified executable LTL model checker]. ~ J. Esparza et als.
# [http://goo.gl/RV54S ForMaRE - formal mathematical reasoning in economics]. ~ M. Kerber, C. Lange y C. Rowat.
# [http://goo.gl/Y7sIq AI over large formal knowledge bases: The first decade]. ~ J. Urban.
# [http://goo.gl/vvqNg Formalization of real analysis: A survey of proof assistants and libraries]. ~ S. Boldo, C. Lelay y G. Melquiond.
# [http://goo.gl/bEFYa Data refinement in Isabelle/HOL]. ~ F. Haftmann, A. Krauss, O. Kunčar y T. Nipkow
# [http://goo.gl/xTyvE Formalizing the confluence of orthogonal rewriting systems]. ~ A.C. Rocha y M. Ayala.
# [http://goo.gl/zCYHj Formalization of the complex number theory in HOL4]. ~ Z. Shi et als.
# [http://goo.gl/kM0dI Programming and reasonning with PowerLists in Coq]. ~ F. Loulergue y V. Niculescu
# [http://goo.gl/KkU6s A hierarchy of mathematical structures in ACL2]. ~ J. Heras, F.J. Martín y V. Pascual.
# [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing Machines and Computability Theory in Isabelle/HOL] ~ J. Xu, X. Zhang y C. Urban

Ejercicios

2015-10-15T06:20:48Z

WikiSysop: Página creada con '== Relaciones de ejercicios == En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deb...'

== Relaciones de ejercicios ==

En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deben tomarse como definitivas.

Tema 1: Programación funcional en Isabelle

2015-10-15T06:19:37Z

WikiSysop: Página creada con '<source lang="isar"> header {* Tema 1: Programación funcional en Isabelle *} theory T1 imports Main begin section {* Introducción *} text {* En este tema se presenta el le...'

<source lang="isar">
header {* Tema 1: Programación funcional en Isabelle *}

theory T1
imports Main
begin

section {* Introducción *}

text {* En este tema se presenta el lenguaje funcional que está
incluido en Isabelle. El lenguaje funcional es muy parecido a
Haskell. *}

section {* Números naturales, enteros y booleanos *}

text {* En Isabelle están definidos los número naturales con la sintaxis
de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).

Los números como el 1 son abreviaturas de los correspondientes en la
notación de Peano, en este caso "Suc 0".

El tipo de los números naturales es nat.

Por ejemplo, el siguiente del 0 es el 1. *}

value "Suc 0" -- "= 1"

text {* En Isabelle está definida la suma de los números naturales:
(x + y) es la suma de x e y.

Por ejemplo, la suma de los números naturales 1 y 2 es el número
natural 3. *}

value "(1::nat) + 2" -- "= 3"

text {* La notación del par de dos puntos se usa para asignar un tipo a
un término (por ejemplo, (1::nat) significa que se considera que 1 es
un número natural).

En Isabelle está definida el producto de los números naturales:
(x * y) es el producto de x e y.

Por ejemplo, el producto de los números naturales 2 y 3 es el número
natural 6. *}

value "(2::nat) * 3" -- "= 6"

text {* En Isabelle está definida la división de números naturales:
(n div m) es el cociente entero de x entre y.

Por ejemplo, la división natural de 7 entre 3 es 2. *}

value "(7::nat) div 3" -- "= 2"

text {* En Isabelle está definida el resto de división de números
naturales: (n mod m) es el resto de dividir n entre m.

Por ejemplo, el resto de dividir 7 entre 3 es 1. *}

value "(7::nat) mod 3" -- "= 1"

text {* En Isabelle también están definidos los números enteros. El tipo
de los enteros se representa por int.

Por ejemplo, la suma de 1 y -2 es el número entero -1. *}

value "(1::int) + -2" -- "= -1"

text {* Los numerales están sobrecargados. Por ejemplo, el 1 puede ser
un natural o un entero, dependiendo del contexto.

Isabelle resuelve ambigüedades mediante inferencia de tipos.

A veces, es necesario usar declaraciones de tipo para resolver la
ambigüedad.

En Isabelle están definidos los valores booleanos (True y False), las
conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃).

El tipo de los booleanos es bool. *}

text {* La conjunción de dos fórmulas verdaderas es verdadera. *}
value "True ∧ True" -- "= True"

text {* La conjunción de un fórmula verdadera y una falsa es falsa. *}
value "True ∧ False" -- "= False"

text {* La disyunción de una fórmula verdadera y una falsa es
verdadera. *}
value "True ∨ False" -- "= True"

text {* La disyunción de dos fórmulas falsas es falsa. *}
value "False ∨ False" -- "= False"

text {* La negación de una fórmula verdadera es falsa. *}
value "¬True" -- "= False"

text {* Una fórmula falsa implica una fórmula verdadera. *}
value "False ⟶ True" -- "= True"

text {* Un lema introduce una proposición seguida de una demostración.

Isabelle dispone de varios procedimientos automáticos para generar
demostraciones, uno de los cuales es el de simplificación (llamado
simp).

El procedimiento simp aplica un conjunto de reglas de reescritura, que
inicialmente contiene un gran número de reglas relativas a los objetos
definidos. *}

text {* Ej. de simp: Todo elemento es igual a sí mismo. *}
lemma "∀x. x = x"
by simp

text {* Ej. de simp: Existe un elemento igual a 1. *}
lemma "∃x. x = 1"
by simp

section {* Definiciones no recursivas *}

text {* La disyunción exclusiva de A y B se verifica si una es verdadera
y la otra no lo es. *}

definition xor :: "bool ⇒ bool ⇒ bool" where
"xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"

text {* Prop.: La disyunción exclusiva de dos fórmulas verdaderas es
falsa.

Dem.: Por simplificación, usando la definición de la disyunción
exclusiva.
*}

lemma "xor True True = False"
by (simp add: xor_def)

text {* Se añade la definición de la disyunción exclusiva al conjunto de
reglas de simplificación automáticas. *}

declare xor_def [simp]

lemma "xor True False = True"
by simp

section {* Definiciones locales *}

text {* Se puede asignar valores a variables locales mediante 'let' y
usarlo en las expresiones dentro de 'in'.

Por ejemplo, si x es el número natural 3, entonces "x*x=9". *}

value "let x = 3::int in x * x" -- "= 9"

section {* Pares *}

text {* Un par se representa escribiendo los elementos entre paréntesis
y separados por coma.

El tipo de los pares es el producto de los tipos.

La función fst devuelve el primer elemento de un par y la snd el
segundo.

Por ejemplo, si p es el par de números naturales (2,3), entonces la
suma del primer elemento de p y 1 es igual al segundo elemento de
p. *}

value "let p = (2,3)::nat × nat in fst p + 1 = snd p"

section {* Listas *}

text {* Una lista se representa escribiendo los elementos entre
corchetes y separados por comas.

La lista vacía se representa por [].

Todos los elementos de una lista tienen que ser del mismo tipo.

El tipo de las listas de elementos del tipo a es (a list).

El término (x#xs) representa la lista obtenida añadiendo el elemento x
al principio de la lista xs.

Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista
vacía los elementos c, b y a es [a,b,c]. *}

value "a#(b#(c#[]))" -- "= [a,b,c]"

text {* Funciones de descomposición de listas:
· (hd xs) es el primer elemento de la lista xs.
· (tl xs) es el resto de la lista xs.

Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a
y el resto de xs es [b,c]. *}

value "let xs = [a,b,c] in hd xs = a ∧ tl xs = [b,c]" -- "= True"

text {* (length xs) es la longitud de la lista xs. Por ejemplo, la
longitud de la lista [1,2,3] es 3. *}

value "length [1,2,3]" -- "= 3"

text {* En la página 8 de "What's in Main" http://bit.ly/1FYOzxq y
en la sesión 47 de "Isabelle/HOL — Higher-Order Logic"
http://bit.ly/1sKeuP3 se encuentran más definiciones y propiedades de
las listas. *}

section {* Funciones anónimas *}

text {* En Isabelle pueden definirse funciones anónimas.

Por ejemplo, el valor de la función que a un número le asigna su doble
aplicada a 1 es 2. *}

value "(λx. x + x) 1::int" -- "= 2"

section {* Condicionales *}

text {* El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso
contrario. *}

definition absoluto :: "int ⇒ int" where
"absoluto x ≡ (if x ≥ 0 then x else -x)"

text {* Ejemplo, el valor absoluto de -3 es 3. *}

value "absoluto(-3)" -- "= 3"

text {* Def.: Un número natural n es un sucesor si es de la forma
(Suc m). *}

definition es_sucesor :: "nat ⇒ bool" where
"es_sucesor n ≡ (case n of
0 ⇒ False
| Suc m ⇒ True)"

text {* Ejemplo, el número 3 es sucesor. *}

value "es_sucesor 3" -- "= True"

section {* Tipos de datos y definiciones recursivas *}

text {* Una lista de elementos de tipo a es la lista Vacia o se obtiene
añadiendo, con Cons, un elemento de tipo a a una lista de elementos de
tipo a. *}

datatype 'a Lista = Vacia | Cons 'a "'a Lista"

text {* (conc xs ys) es la concatenación de las lista xs e ys. Por
ejemplo,
conc (Cons a (Cons b Vacia)) (Cons c Vacia)
= Cons a (Cons b (Cons c Vacia))
*}

fun conc :: "'a Lista ⇒ 'a Lista ⇒ 'a Lista" where
"conc Vacia ys = ys"
| "conc (Cons x xs) ys = Cons x (conc xs ys)"

value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
-- "= Cons a (Cons b (Cons c Vacia))"

text {* (suma n) es la suma de los primeros n números naturales. Por
ejemplo,
suma 3 = 6
*}

fun suma :: "nat ⇒ nat" where
"suma 0 = 0"
| "suma (Suc m) = (Suc m) + suma m"

value "suma 3" -- "= 6"

text {* (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 3 = 9
*}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n"

value "sumaImpares 3" -- "= 9"

end
</source>

Temas

2015-10-15T06:18:59Z

WikiSysop:

== Temas de ''Razonamiento automático (2014-15)'' ==
* [[Tema 1: Programación funcional en Isabelle]].

Temas

2015-10-15T06:18:30Z

WikiSysop: Página creada con '== Temas de ''Razonamiento automático (2014-15)'' == * Tema 1: Programación funcional en Isabelle. * Tema 2: Razonamiento sobre programas: ** [http://www.cs.us.es/~jalonso...'

== Temas de ''Razonamiento automático (2014-15)'' ==
* [[Tema 1: Programación funcional en Isabelle]].
* Tema 2: Razonamiento sobre programas:
** [http://www.cs.us.es/~jalonso/cursos/i1m/temas/tema-8t.pdf Tema 2a: Razonamiento sobre programas Haskell]
** [[Tema 2b: Razonamiento automático sobre programas en Isabelle/HOL]].

Razonamiento automático (2015-16)

2015-10-15T06:16:55Z

WikiSysop: Página creada con '== Razonamiento automático (2015-16) == Este sitio contiene materiales del curso ''Razonamiento automático'' del [http://master.cs.us.es/Máster_Universitario_en_Lógica,_Comp...'

== Razonamiento automático (2015-16) ==
Este sitio contiene materiales del curso ''Razonamiento automático'' del [http://master.cs.us.es/Máster_Universitario_en_Lógica,_Computación_e_Inteligencia_Artificial Máster Universitario en Lógica, Computación e Inteligencia Artificial] de la [http://www.us.es Universidad de Sevilla].

== Material para el curso ==
* [[Temas]]: Teorías de los temas.
* [[Ejercicios]]: Relaciones de ejercicios.
* [[Documentación]]: Lecturas recomendadas.
* [[Sistemas]]: Sistemas utilizados.
* [http://www.glc.us.es/~jalonso/vestigium/tag/ra2015 Diario]: Descripción diaria de las clases.

MediaWiki:Mainpage

2015-10-15T06:15:53Z

WikiSysop: Página creada con 'Razonamiento automático (2015-16)'

Razonamiento automático (2015-16)

MediaWiki:Sidebar

2015-10-15T06:15:09Z

WikiSysop:

MediaWiki:Sidebar

2015-10-15T06:14:53Z