Demostración asistida por ordenador (2011-12) Demostración asistida por ordenador (2011-12)

header {* Tema 6: Isabelle como un lenguaje funcional *}

theory Tema_6
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 2011.

  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. El ejemplo del lema más trivial es el siguiente *}
*}

lemma elMasTrivial: "True" 
by simp

text {* 
  En este capítulos se presenta el lenguaje funcional que está incluido en
  Isabelle. 

  El lenguaje funcional es muy parecido al ML estándard.
*}

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 n" (el sucesor de n). 
  
  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. 

  Lema [Ejemplo de simplificación de números naturales]
  El siguiente del 0 es el 1.
*}

lemma "Suc 0 = 1" 
by simp

text {* 
  En Isabelle están definida la suma y el producto de números naturales:
  · "x+y" es la suma de x e y 
  · "x*y" es el producto de x e y 

  Lema [Ejemplo de suma]
  La suma de los números naturales 1 y 2 es el número natural 3.
*}

lemma "1 + 2 = (3::nat)" 
by simp

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

  Lema [Ejemplo de producto]
  El producto de los números naturales 2 y 3 es el número natural 6.
*}

lemma "2 * 3 = (6::nat)" 
by simp

text {* 
  En Isabelle está definida la división de números naturales: 
  · "n div m" es el cociente entero de n entre "m"
  · "n mod m" es el resto de dividir "n" entre "m".

  Lema [Ejemplo de división]
  La división natural de 7 entre 3 es 2.
*}

lemma "7 div 3 = (2::nat)" 
by simp

text {* 
  Lema [Ejemplo de resto]
  El resto de dividir 7 entre 3 es 1.
*}

lemma "7 mod 3 = (1::nat)" 
by simp

text {* 
  En Isabelle también están definidos los números enteros. 

  El tipo de los enteros se representa por int.

  Lema [Ejemplo de operación con enteros]
  La suma de 1 y -2 es el número entero -1.
*}

lemma "1 + -2 = (-1::int)" 
by simp

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, False", 
  · las conectivas "\<not>, \<and>, \<or>, \<longrightarrow>, \<leftrightarrow>" y 
  · los cuantificadores "\<forall>, \<exists>". 

  El tipo de los booleanos es bool. 

  Lema [Ejemplos de evaluaciones booleanas]
    · La conjunción de dos fórmulas verdaderas es verdadera.
    · La conjunción de un fórmula verdadera y una falsa es falsa.
    · La disyunción de una fórmula verdadera y una falsa es verdadera.
    · La disyunción de dos fórmulas falsas es falsa.
    · La negación de una fórmula verdadera es falsa.
    · Una fórmula falsa implica una fórmula verdadera.
    · Todo elemento es igual a sí mismo.
    · Existe un elemento igual a 1.
*}

lemma "True \<and> True = True" 
by simp

lemma "True \<and> False = False" 
by simp
 
lemma "True \<or> False = True" 
by simp

lemma "False \<or> False = False" 
by simp

lemma "\<not> True = (False::bool)" 
by simp

lemma "False \<longrightarrow> True" 
by simp

lemma "\<forall> x. x = x" 
by simp

lemma "\<exists> x. x = 1" 
by simp

section {* Definiciones no recursivas *}

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

definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
  "xor A B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"

text {* 
  Lema [Ejemplo de demostración con definiciones no recursivas]
  La disyunción exclusiva de dos fórmulas verdaderas es falsa.

  Demostración. 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 exlusiva al conjunto de reglas de
  simplificación automáticas.
*}

declare xor_def[simp]

section {* Definiciones locales *}

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

  Lema [Ejemplo de entorno local]
  Sea x el número natural 3. Entonces "x \<times> x = 9".
*}

lemma "(let x = 3::nat in x * x = 9)" 
by simp

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.

  Lema [Ejemplo de uso de pares]
  Sea p el par de números naturales (2,3). La suma del primer elemento de
  p y 1 es igual al segundo elemento de p.
*}

lemma "let p = (2,3)::nat \<times> nat in fst p + 1 = snd p" 
by simp

section {* Listas *}

text {*
  Una lista se representa escribiendo los elementos entre corchetes y separados
  por coma.
  
  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 a#l representa la lista obtenida añadiendo el elemento a al
  principio de la lista l.

  Lema [Ejemplo de construcción de listas]
  La lista obtenida añadiendo sucesivamente a la lista vacía los elementos 3,
  2 y 1 es [1,2,3]. 
*}

lemma "1#(2#(3#[])) = [1,2,3]" 
by simp

text {* 
  (hd l) es el primer elemento de la lista l.

  (tl l) es el resto de la lista l.

  Lema [Ejemplo de cálculo con listas]
  Sea l la lista de números naturales [1,2,3]. Entonces, el primero de l es 1 y
  el resto de l es [2,3].  
*}

lemma "let l = [1,2,3]::(nat list) in hd l = 1 \<and> tl l = [2,3]" 
by simp

text {* 
  (length l)es la longitud de la lista l.

  Lema [Ejemplo de cálculo de longitud]
  La longitud de la lista [1,2,3] es 3.
*}

lemma "length [1,2,3] = 3" 
by simp

text {* 
  En la sesión 38 de "HOL: The basis of Higher-Order Logic"
  (en http://isabelle.informatik.tu-muenchen.de/library/HOL/outline.pdf)
  se encuentran  más definiciones y propiedades de las listas.
*}

section {* Registros *}

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

  Definición [Ejemplo de definición de registro]
  Los puntos del plano pueden representarse mediante registros con dos campos,
  las coordenadas, con valores enteros.  
*}

record punto = 
  coordenada_x :: int
  coordenada_y :: int

text {* 
  Definición [Ejemplo de definición de un registro]
  El punto pt tiene de coordenadas 3 y 7.  
*}

definition pt :: punto where
  "pt \<equiv> \<lparr>coordenada_x = 3, coordenada_y = 7\<rparr>"

text {* 
  Lema [Ejemplo de propiedad de registro]
  La coordenada x del punto pt es 3.  
*}

lemma "coordenada_x pt = 3" 
by (simp add: pt_def)

text {* 
  Lema [Ejemplo de actualización de un registro]
  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. 
*}

lemma "let pt2=pt\<lparr>coordenada_x:=4\<rparr> in coordenada_x (pt2) = 4" 
by (simp add: pt_def)

section {* Funciones anónimas *}

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

  Lema [Ejemplo de uso de funciones anónimas]
  El valor de la función que a un número le asigna su doble aplicada a 1 es 2.  
*}

lemma "(\<lambda> x. x + x) 1 = (2::nat)" 
by simp

section {* Condicionales *}

text {*
  Definición [Ejemplo con el condicional if]
  El valor absoluto del entero x es x, si "x \<ge> 0" y es -x en caso
  contrario.    
*}

definition absoluto :: "int \<Rightarrow> int" where
  "absoluto x \<equiv> (if x \<ge> 0 then x else -x)"

text {* 
  Lema [Ejemplo de simplificación con el condicional if]
  El valor absoluto de -3 es 3.  
*}

lemma "absoluto(-3) = 3"
by (simp add:absoluto_def) 

text {* 
  Definición [Ejemplo con el condicional case]
  Un número natural n es un sucesor si es de la forma "Suc m".
*}

definition es_sucesor :: "nat \<Rightarrow> bool" where
  "es_sucesor n \<equiv>
  (case n of 
    0     \<Rightarrow> False 
  | Suc m \<Rightarrow> True)"

text {* 
  Lema [Ejemplo de simplificación con el condicional case]
  El número 3 es sucesor.  
*}

lemma "es_sucesor 3"
by (simp add: es_sucesor_def)

section {* Tipos de datos y recursión primitiva *}

text {*
  Definición [Ejemplo de definición de tipo de dato recursivo]
  Una lista de elementos de tipo a es la lista Vacia o se obtiene añadiendo,
  con ConsLista, un elemento de tipo a a una lista de elementos de tipo a.
*}

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

text {* 
  Definición [Ejemplo de definición primitiva recursiva]
  (conc xs ys) es la concatenación de las lista xs e ys.  
*}

primrec conc :: "'a Lista \<Rightarrow> 'a Lista \<Rightarrow> 'a Lista" where
  "conc Vacia ys = ys"
| "conc (ConsLista x xs) ys = ConsLista x (conc xs ys)"

text {* 
  Lema [Ejemplo de simplificación con tipo de dato recursivo]
  La concatenación de la lista formada por 1 y 2 con la lista formada por el 3
  es la lista cuyos elementos son 1,2 y 3.
*}

lemma "conc (ConsLista 1 (ConsLista 2 Vacia)) (ConsLista 3 Vacia) =
       (ConsLista 1 (ConsLista 2 (ConsLista 3 Vacia)))"
by simp

text {* 
  Ejercicio [Ejemplo de definición primitiva recursiva sobre los naturales] 
  Definir una función que sume los primeros n números naturales y usarla para
  comprobar que la suma de los 3 primeros números naturales es 6.
*}

primrec suma :: "nat \<Rightarrow> nat" where
  "suma 0 = 0"
| "suma (Suc m) = (Suc m) + suma m"

lemma "suma 3 = 6"
by (simp add: suma_def) 

value "suma 3"
value "2+(3::int)"

end