¿Es posible no importar ninguna teoría en Isabelle?

Question

Quiero definir mi propio tipo de lista en una teoría llamada List, pero ya existe una teoría con ese nombre. ¿Existe una teoría más ligera que Main?

Answer 1

No se puede importar nada en Isabelle (ya que la importación es necesaria incluso para la lógica básica). La implementación de HOL en Isabelle tiene tres puntos de entrada admitidos: Main, Complex_Main (que es Main más algunos Análisis) y Plain, pero solo los dos primeros están destinados para el uso regular.

simple ya contiene la lógica básica, pero casi nada en términos de la biblioteca estándar (por ejemplo, sin listas). Pero también faltan herramientas importantes como QuickCheck, Sledgehammer y el generador de códigos. Además, si comienzas desde Plain para poder nombrar tu propia lista teórica, ten en cuenta que tu teoría será incompatible con cualquier trabajo que se desarrolle en Main (que es casi todo).

Así que, a menos que tengas muy buenas razones para hacerlo, te sugiero seguir el comentario de Raphael y darle a tu lista la teoría de otro nombre.

Answer 2

Puede importar sólo HOL, como en

theory Test_Theory 
imports HOL 
begin 
    … 
end 

hago a menudo para probar e investigar acerca de Isabelle.

Sin embargo, carecerá de las definiciones de tipo de datos, y probablemente necesitará importar Datatype (y puede ser incluso Record), así, con el fin de ser capaz de escribir su teoría List.

theory Test_Theory 
imports HOL Datatype Record 
begin 
    … 
end 

Como ambos Datatype y Record importaciones HOL, simplemente puede tener:

theory Test_Theory 
imports Datatype Record 
begin 
    … 
end 

Eso no es fácil de hacer sin teoría Main, pero no imposible. Solo tenga en cuenta que tendrá que prescindir de muchos teoremas ampliamente utilizados, y puede tener que escribir y probar sus propios.

Answer 3

Tenga en cuenta que $ISABELLE_HOME/src/HOL/ex/Seq.thy proporciona un ejemplo mínimo de la definición de su propio tipo de datos de lista para la experimentación, sin abordar la delicada cuestión de cómo trabajar con el sistema debajo de su punto de entrada Main. (Los principiantes se confunden y los expertos no lo hacen)

Teóricamente, la teoría más primitiva que podría importar es Pure, pero eso es solo el marco lógico básico, sin ninguna lógica de objeto como HOL todavía. Solo por curiosidad, puede consultar $ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy que comienza en Pure y define una versión mínima de H.O.L. Además de eso, sin ninguna de las teorías y herramientas avanzadas que esperarías de Isabelle/HOL completo.