Ver el código de «Tema 2: Isabelle como un lenguaje funcional» - Demostración asistida por ordenador (2012-13)

<source lang="isar">
header {* Tema 2: Isabelle como un lenguaje funcional *}

theory Tema_2
imports Main 
begin

section {* Introducción *}

text {* Esta notas son una introducción a la demostración asistida
  utilizando el sistema Isabelle/HOL/Isar. La versión de Isabelle
  utilizada es la 2012.

  En este capítulos 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::nat 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 descomposió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 sesión 47 de "Isabelle/HOL — Higher-Order Logic"
  http://goo.gl/sFsFF se encuentran más definiciones y propiedades de
  las listas. *}

section {* Registros *}

text {* Un registro es una colección de campos y valores. 

  Por ejemplo, los puntos del plano se pueden representar mediante
  registros con dos campos, las coordenadas, con valores enteros. *}

record punto = 
  coordenada_x :: int
  coordenada_y :: int

text {* Ejemplo, el punto pt tiene de coordenadas 3 y 7. *}

definition pt :: punto where
  "pt ≡ (|coordenada_x = 3, coordenada_y = 7|)"

text {* Ejemplo, la coordenada x del punto pt es 3. *}

value "coordenada_x pt" -- "= 3" 

text {* Ejemplo, sea pt2 el punto obtenido a partir del punto pt
  cambiando el valor de su coordenada x por 4. Entonces la coordenada x
  del punto pt2 es 4. *}

value "let pt2 = pt(|coordenada_x:=4|) in coordenada_x (pt2)" -- "= 4" 

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::nat" -- "= 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 recursión primitiva *}

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"

text {* Prop.: La suma de los n primeros numeros impares es n\<^sup>2
  Dem.: Por induccion en n. *}

lemma "sumaImpares n = n * n"
by (induct n) auto

end
</source>