Menu Close

Categoría: LMF2019

LMF2019: Desarrollo de teorías formalizadas con Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo desarrollar en Isabelle/HOL teorías axiomáticas usando entornos locales (“locales”) y clases de tipos (“class”). Se ha aplicado al desarrollo de las teorías de grupos y a las de órdenes. videoconferencia.

La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:

  • Primera parte:

  • Segunda parte:

La teoría con los ejemplos presentados en la clase es la siguiente:

Vídeos de las clases de razonamiento automático con Isabelle/HOL

LMF2019: Razonamiento sobre árboles y bosques en Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo definir y razonar en Isabelle/HOL tipos de datos recursivos como árboles binarios, árboles generales y bosques. En su definición se usa recursión cruzada y en la demostración de sus propiedades se usa inducción doble.

La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:

  • Primera parte: Razonamiento sobre árboles binarios

  • Segunda parte: Árboles y bosques: Recursión mutua e inducción

La teoría utilizada es la siguiente

chapter ‹Tema 8: Razonamiento sobre árboles›
 
theory T8_Razonamiento_sobre_arboles
imports Main 
begin
 
text ‹En este tema se estudia razonamiento sobre otras estructuras
  recursivas como árboles binarios, árboles generales y bosques.
 
  También se muestra cómo definir tipos de datos por recursión cruzada y
  la demostración de sus propiedades por inducción.›
 
section ‹Razonamiento sobre árboles binarios›
 
text ‹Ejemplo de definición de tipos recursivos:
  Definir un tipo de dato para los árboles binarios.›
 
datatype 'a arbolB = Hoja "'a" 
                   | Nodo "'a" "'a arbolB" "'a arbolB"
 
text ‹Regla de inducción correspondiente a los árboles binarios:
  La regla de inducción sobre árboles binarios es arbolB.induct:
  ⟦ ⋀x. P (Hoja x);
    ⋀x i d. ⟦P i; P d⟧ ⟹ P (Nodo x i d)⟧ 
  ⟹ P a
›
 
thm arbolB.induct
 
text ‹Ejemplo de definición sobre árboles binarios:
  Definir la función "espejo" que aplicada a un árbol devuelve su imagen
  especular.›
 
fun espejo :: "'a arbolB ⇒ 'a arbolB" where
  "espejo (Hoja x)     = Hoja x"
| "espejo (Nodo x i d) = Nodo x (espejo d) (espejo i)"
 
value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = 
      Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))"
 
text ‹Ejemplo de demostración sobre árboles binarios:
  Demostrar que la función "espejo" es involutiva; es decir, para
  cualquier árbol a, se tiene que 
     espejo (espejo a) = a.›
 
― ‹La demostración declarativa es›
lemma 
  fixes a :: "'b arbolB" 
  shows "espejo (espejo a) = a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (Hoja x)"  
    by simp 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "espejo (espejo (Nodo x i d)) = 
          espejo (Nodo x (espejo d) (espejo i))" 
      by simp
    also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" 
      by simp
    also have "… = Nodo x i d" 
      using h1 h2 by simp 
    finally show "?P (Nodo x i d)" 
      by this
  qed
qed
 
― ‹La demostración declarativa detallada es›
lemma 
  fixes a :: "'b arbolB" 
  shows "espejo (espejo a) = a" (is "?P a")
proof (induct a)
  fix x 
  show "?P (Hoja x)"  
    by (simp only: espejo.simps(1)) 
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "espejo (espejo (Nodo x i d)) = 
          espejo (Nodo x (espejo d) (espejo i))" 
      by (simp only: espejo.simps(2))
    also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" 
      by (simp only: espejo.simps(2))
    also have "… = Nodo x i d" 
      using h1 h2
      by (simp only:) 
    finally show ?thesis 
      by this
  qed
qed
 
text ‹Comentarios sobre la demostración anterior:
  · (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario
    cuyos elementos son de tipo b". 
  · (induct a) indica que el método de demostración es por inducción
    en el árbol binario a.
  · Se generan dos casos:
    1. ⋀a. espejo (espejo (Hoja a)) = Hoja a
    2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2; 
                   espejo (espejo a3) = a3⟧
                  ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3›
 
― ‹La demostración aplicativa es›
lemma  
  "espejo (espejo a) = a"
  apply (induct a)
   apply simp
  apply simp
  done
 
― ‹La demostración aplicativa detallada es›
lemma  
  "espejo (espejo a) = a"
  apply (induct a)
   apply (simp only: espejo.simps(1))
  apply (simp only: espejo.simps(2))
  done
 
― ‹La demostración automática es›
lemma  
  "espejo (espejo a) = a"
  by (induct a) simp+ 
 
― ‹La demostración automática detallada es›
lemma  
  "espejo (espejo a) = a"
  by (induct a) (simp only: espejo.simps)+  
 
text ‹Ejemplo. [Aplanamiento de árboles]
  Definir la función "aplana" que aplane los árboles recorriéndolos en
  orden infijo.›
 
fun aplana :: "'a arbolB ⇒ 'a list" where
  "aplana (Hoja x)     = [x]"
| "aplana (Nodo x i d) = aplana i @ [x] @ aplana d"
 
value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = 
      [c, b, d, a, e]"
 
text ‹Ejemplo. [Aplanamiento de la imagen especular] Demostrar que
     aplana (espejo a) = rev (aplana a)›
 
― ‹La demostración declarativa es›
lemma 
  fixes a :: "'b arbolB"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (Hoja x)" 
    by simp 
next
  fix x 
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "aplana (espejo (Nodo x i d)) = 
          aplana (Nodo x (espejo d) (espejo i))" 
      by simp
    also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" 
      by simp
    also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" 
      using h1 h2 by simp
    also have "… = rev ((aplana i) @ [x] @ (aplana d))" 
      by simp
    also have "… = rev (aplana (Nodo x i d))" 
      by simp
    finally show "?P (Nodo x i d)" 
      by this
  qed
qed
 
― ‹Lema auxiliar para la demostración declarativa detallada›
lemma rev_unit: "rev [x] = [x]"
proof -
  have "rev [x] = rev [] @ [x]" 
    by (simp only: rev.simps(2))
  also have "… = [] @ [x]"
    by (simp only: rev.simps(1))
  also have "… = [x]"
    by (simp only: append.simps(1))
  finally show ?thesis
    by this
qed
 
― ‹La demostración estructurada y detallada es›
lemma 
  fixes a :: "'b arbolB"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x :: 'b
  have "aplana (espejo (Hoja x)) = aplana (Hoja x)"
    by (simp only: espejo.simps(1))
  also have "… = [x]"
    by (simp only: aplana.simps(1))
  also have "… = rev [x]"
    by (simp only: rev_unit)
  also have "… = rev (aplana (Hoja x))"
    by (simp only: aplana.simps(1))
  finally show "?P (Hoja x)" 
    by this 
next
  fix x :: 'b
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (Nodo x i d)" 
  proof -
    have "aplana (espejo (Nodo x i d)) = 
          aplana (Nodo x (espejo d) (espejo i))" 
      by (simp only: espejo.simps(2))
    also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" 
      by (simp only: aplana.simps(2))
    also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" 
      by (simp only: h1 h2)
    also have "… = rev ((aplana i) @ [x] @ (aplana d))"
      (* find_theorems "rev (_ @ _)" *)
      by (simp only: rev_append rev_unit append_assoc)
    also have "… = rev (aplana (Nodo x i d))" 
      by (simp only: aplana.simps(2))
    finally show ?thesis 
      by this
  qed
qed
 
― ‹La demostración aplicativa es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply simp
  apply simp
  done
 
― ‹La demostración aplicativa detallada es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply (simp only: espejo.simps(1) aplana.simps(1))
   apply (simp only: rev_unit)
  apply (simp only: espejo.simps(2) aplana.simps(2))
  apply (simp only: rev_append)
  apply (simp only: rev_unit)
  apply (simp only: append_assoc)
  done
 
― ‹La demostración aplicativa detallada compacta es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply (simp only: 
      espejo.simps(1) 
      aplana.simps(1)
      rev_unit
      espejo.simps(2) 
      aplana.simps(2)
      rev_append
      append_assoc)+
  done
 
― ‹La demostración aplicativa detallada más compacta es›
lemma "aplana (espejo a) = rev (aplana a)"
  apply (induct a)
   apply (simp only: 
      espejo.simps
      aplana.simps
      rev_unit
      rev_append
      append_assoc)+
  done
 
― ‹La demostración automática es›
lemma "aplana (espejo a) = rev (aplana a)"
  by (induct a) simp_all
 
― ‹La demostración automática detallada es›
lemma "aplana (espejo a) = rev (aplana a)"
  by (induct a)
     (simp only: 
      espejo.simps
      aplana.simps
      rev_unit
      rev_append
      append_assoc)+
 
section ‹Árboles y bosques. Recursión mutua e inducción›
 
text ‹Nota. [Ejemplo de definición de tipos mediante recursión cruzada]
  · Un árbol de tipo a es una hoja o un nodo de tipo a junto con un
    bosque de tipo a.
  · Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo
    un árbol de tipo a a un bosque de tipo a.›
 
datatype 'a arbol = Nodo "'a" "'a bosque"
     and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"
 
text ‹Regla de inducción correspondiente a la recursión cruzada:
  La regla de inducción sobre árboles y bosques es arbol_bosque.induct:
     ⟦⋀x b. P2 b ⟹ P1 (Nodo x b); 
      P2 Vacio;
      ⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧ 
     ⟹ P1 a ∧ P2 b›
 
thm arbol_bosque.induct
 
text ‹Ejemplos de definición por recursión cruzada:
  · aplana_arbol a) es la lista obtenida aplanando el árbol a.   
  · (aplana_bosque b) es la lista obtenida aplanando el bosque b.   
  · (map_arbol f a) es el árbol obtenido aplicando la función f a
    todos los nodos del árbol a.   
  · (map_bosque f b) es el bosque obtenido aplicando la función f a
    todos los nodos del bosque b. ›
 
fun aplana_arbol :: "'a arbol ⇒ 'a list" and 
    aplana_bosque :: "'a bosque ⇒ 'a list" where
  "aplana_arbol (Nodo x b)   = x # (aplana_bosque b)"
| "aplana_bosque Vacio       = []"
| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)"
 
fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and
    map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where
  "map_arbol  f (Nodo x b)  = Nodo (f x) (map_bosque f b)"
| "map_bosque f Vacio       = Vacio"
| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)"
 
text ‹Ejemplo de demostración por inducción cruzada:
  Demostrar que:
  · aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
  · aplana_bosque (map_bosque f b) = map f (aplana_bosque b)›
 
declare [[names_short]] 
 
― ‹La demostración declarativa es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
  fix x b
  assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_arbol (map_arbol f (Nodo x b)) = 
        aplana_arbol (Nodo (f x) (map_bosque f b))" 
    by simp
  also have "… = (f x) # (aplana_bosque (map_bosque f b))" 
    by simp
  also have "… = (f x) # (map f (aplana_bosque b))" 
    using HI by simp
  also have "… = map f (aplana_arbol (Nodo x b))" 
    by simp
  finally show "aplana_arbol (map_arbol f (Nodo x b)) =
                map f (aplana_arbol (Nodo x b))" 
    by this
next
  show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" 
    by simp
next
  fix a b
  assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
     and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_bosque (map_bosque f (ConsB a b)) = 
        aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp
  also have "… = aplana_arbol (map_arbol f a) @ 
                  aplana_bosque (map_bosque f b)" 
    by simp
  also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))" 
    using HI1 HI2 by simp
  also have "… = map f (aplana_bosque (ConsB a b))" by simp
  finally show "aplana_bosque (map_bosque f (ConsB a b)) =
                map f (aplana_bosque (ConsB a b))" 
    by this
qed
 
― ‹La demostración declarativa detallada es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
  fix x b
  assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_arbol (map_arbol f (Nodo x b)) = 
        aplana_arbol (Nodo (f x) (map_bosque f b))" 
    by (simp only: map_arbol.simps(1))
  also have "… = (f x) # (aplana_bosque (map_bosque f b))" 
    by (simp only: aplana_arbol.simps(1))
  also have "… = (f x) # (map f (aplana_bosque b))"
    using HI
    by (simp only:)
  also have "… = map f (aplana_arbol (Nodo x b))" 
    (* find_theorems "map _ (_ # _)" *)
    by (simp only: list.map aplana_arbol.simps(1))
  finally show "aplana_arbol (map_arbol f (Nodo x b)) =
                map f (aplana_arbol (Nodo x b))" 
    by this
next
  show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" 
    by (simp only: aplana_bosque.simps(1)
                   map_bosque.simps(1)
                   list.map)
next
  fix a b
  assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
     and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  have "aplana_bosque (map_bosque f (ConsB a b)) = 
        aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" 
    by (simp only: map_bosque.simps(2))
  also have "… = aplana_arbol (map_arbol f a) @ 
                  aplana_bosque (map_bosque f b)" 
    by (simp only: aplana_bosque.simps(2))
  also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))" 
    by (simp only: HI1 HI2)
  also have "… = map f (aplana_arbol a @ aplana_bosque b)"
    (* find_theorems "map _ (_ @ _)" *)
    by (simp only: map_append)
  also have "… = map f (aplana_bosque (ConsB a b))" 
    by (simp only: aplana_bosque.simps(2))
  finally show "aplana_bosque (map_bosque f (ConsB a b)) =
                map f (aplana_bosque (ConsB a b))" 
    by this
qed
 
text ‹Comentarios sobre la demostración anterior:
  · (induct_tac a and b) indica que el método de demostración es por
    inducción cruzada sobre a y b.
  · Se generan 3 casos:
    1. ⋀a bosque.
          aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹
          aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =
          map h (aplana_arbol (arbol.Nodo a bosque))
    2. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)
    3. ⋀arbol bosque.
          ⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);
           aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧
          ⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =
             map h (aplana_bosque (ConsB arbol bosque))›
 
― ‹La demostración aplicativa es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply simp+
  done
 
― ‹La demostración aplicativa detallada es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply (simp only: map_arbol.simps aplana_arbol.simps)
    apply (simp only: list.map(2))
   apply (simp only: map_bosque.simps(1) aplana_bosque.simps(1))
   apply (simp only: list.map(1))
  apply (simp only: map_bosque.simps(2) aplana_bosque.simps(2))
  apply (simp only: map_append)
  done
 
― ‹La demostración aplicativa detallada compacta es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply (simp only: 
      map_arbol.simps 
      aplana_arbol.simps
      list.map(2)
      map_bosque.simps(1) 
      aplana_bosque.simps(1)
      list.map(1)
      map_bosque.simps(2) 
      aplana_bosque.simps(2)
      map_append)+
  done
 
― ‹La demostración aplicativa detallada más compacta es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  apply (induct_tac a and b)
    apply (simp only: 
      map_arbol.simps 
      map_bosque.simps
      aplana_arbol.simps
      aplana_bosque.simps
      list.map
      map_append)+
  done
 
― ‹La demostración automática es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  by (induct_tac a and b) simp+
 
― ‹La demostración automática detallada es›
lemma "aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)
     ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
  by (induct_tac a and b) 
     (simp only: 
      map_arbol.simps 
      map_bosque.simps
      aplana_arbol.simps
      aplana_bosque.simps
      list.map
      map_append)+
 
end

LMF2019: Razonamiento por casos y por inducción en Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático hemos profundizado en el estudio de las demostraciones por casos y por inducción. En concreto, se ha estudiado

  • el razonamiento por casos booleanos,
  • el razonamiento por casos booleanos sobre una variable,
  • el razonamiento por casos sobre listas,
  • el razonamiento por inducción sobre números naturales con patrones,
  • el razonamiento sobre definiciones con existenciales,
  • el uso de librerías auxiliares (como Parity) y
  • el uso de otros métodos de demostración (como presburg).

La clase se ha dado mediante videoconferencia y el vídeo correspondiente es:

La teoría con los ejemplos presentados en la clase es la siguiente:

LMF2019: Razonamiento sobre programas con Isabelle/HOL (2º parte)

En la clase de hoy del curso de Lógica matemática y fundamentos se ha concluido el estudio, iniciado en la clase anterior, de cómo se pueden demostrar manualmente propiedades de programas Haskell y cómo traducir dichas demostraciones a Isabelle/HOL.

Para ello, se han usado las transparencias del tema 8 del curso de Informática (de 1º del Grado en Matemática). Como lectura complementaria se recomienda el capítulo 13 del libro de G. Hutton Programming in Haskell.

De cada propiedad se han presentados distintas demostracciones:

  • automática,
  • aplicativa estructurada (usando simp)
  • aplicativa detallada (usando simp only)
  • declarativa estructurada (usando simp)
  • declarativa detallada (usando simp only)

La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:

  • Primera parte:

  • Segunda parte:

  • Tercera parte:

Las transparencia utilizadas son las del tema a partir de la página 29.

La teoría con los ejemplos presentados en la clase es la siguiente:

LMF2019: Razonamiento sobre programas con Isabelle/HOL (1º parte)

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell y cómo traducir dichas demostraciones a Isabelle/HOL.

Para ello, se han usado las transparencias del tema 8 del curso de Informática (de 1º del Grado en Matemática). Como lectura complementaria se recomienda el capítulo 13 del libro de G. Hutton Programming in Haskell.

La traducción de los enunciado de las propiedades es inmediato: basta escribir la palabra lemma y a continuación la propiedad entre comillas dobles; por ejemplo,

lemma "longitud (repite n x) = n"

También se puede poner un nombre al lema, por ejemplo,

lemma inversaAcAux_es_inversa:
  "inversaAcAux xs ys = (inversa xs)@ys"

De cada propiedad se han presentados distintas demostracciones:

  • automática,
  • aplicativa estructurada (usando simp)
  • aplicativa detallada (usando simp only)
  • declarativa estructurada (usando simp)
  • declarativa detallada (usando simp only)

La clase se ha dado mediante videoconferencia y el vídeo correspondiente a la primera parte es

y el de la segunda parte es

Las transparencia utilizadas son las 28 primeras páginas del tema

La teoría con los ejemplos presentados en la clase es la siguiente:

LMF2019: Programación funcional con Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha presentado la programación funcional en Isabelle/HOL resaltando la analogía con la programación en Haskell estudiada en primer curso en la asignatura de Informática

La clase se ha dado mediante videoconferencia y el correspondiente vídeo es

La teoría con los ejemplos presentados en la clase es

chapter ‹Tema 5 Programación funcional en Isabelle›
 
theory T5_Programacion_funcional_en_Isabelle
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" :: "nat"*)
 
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" :: "nat" *)
 
value "(1::nat) + 2 = 3"
(*"True" :: "bool" *) 
 
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" :: "nat"*)
 
value "(2::nat) * 3 = 6"
(*"True" :: "bool" *) 
 
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" :: "nat" *)
 
value "(7::nat) div 3 = 2"
(*"True" :: "bool" *)
 
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" :: "nat" *)
 
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" :: "int"*)
 
value "(5::nat) - 4"
 
 
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" :: "bool" *)
 
text ‹La conjunción de un fórmula verdadera y una falsa es falsa.› 
value "True ∧ False"  
(*"False" :: "bool" *)
 
text ‹La disyunción de una fórmula verdadera y una falsa es
  verdadera.› 
value "True ∨ False" 
(*"True" :: "bool" *)
 
text ‹La disyunción de dos fórmulas falsas es falsa.›
value "False ∨ False" 
(*"False" :: "bool"*)
 
text ‹La negación de una fórmula verdadera es falsa.›
value "¬True" 
(*"False" :: "bool"*)
 
text ‹Una fórmula falsa implica una fórmula verdadera.›
value "False ⟶ True" 
(*"True" :: "bool"*)
 
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.›
 
thm xor_def
 
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" :: "nat" *)
 
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" 
(*"True" :: "bool" *)
 
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 z, y y x a es [x,y,z].›
 
value "x#(y#(z#[]))" 
(*"[x, y, z]" :: "'a list" *)
 
value "(1::int)#(2#(3#[]))"
(*"[1, 2, 3]" :: "int list" *)
 
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" :: "bool" *)
 
text(length xs) es la longitud de la lista xs. Por ejemplo, la
  longitud de la lista [1,2,5] es 3.›
 
value "length [1::nat,2,5]" 
(*"3" :: "nat" *)
 
text ‹En la página 10 de "What's in Main" 
  https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2019/doc/main.pdf›
 
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" :: "nat" *)
 
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" :: "int" *)
 
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" :: "bool" *)
 
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)"
(* ↝ Lista.Cons a (Lista.Cons b (Lista.Cons c Vacia)) *)
 
text ‹Se puede declarar que acorte los nombres.›
 
declare [[names_short]]
 
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" :: nat *)
 
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 12" 
(*"9" :: nat *)
 
end

Como tarea se han propuesto los ejercicios de la relación 8.

LMF2019: Deducción natural en lógica de primer orden (2/2)

En la clase de hoy del curso Lógica matemática y fundamentos se ha completado el estudio del cálculo de deducción natural proposional para la lógica de primer orden demostrando algunas equivalencias notables y presentando las reglas de la igualdad

La clase se ha dado mediante videoconferencia y el correspondiente vídeo es

Las transparencias de esta clase son las páginas 14 a 29 del tema 4.

Descargar (PDF, 168KB)

A la vez que se han ido haciendo las demostraciones se ha explicado cómo hacerlas en Isabelle/HOL.

La teoría con los ejemplos presentados en la clase es la siguiente:

LMF2019: Deducción natural en lógica de primer orden (1/2)

En la clase de hoy del curso Lógica matemática y fundamentos se presentado la ampliación del cálculo de deducción natural proposional para tratar los cuantificadores.

Las transparencias de esta clase son las páginas 1 a 13 del tema 4.

Descargar (PDF, 168KB)

A la vez que se han ido haciendo las demostraciones se ha explicado cómo hacerlas en Isabelle/HOL.

La teoría con los ejemplos presentados en la clase es la siguiente: