Is it possible not to import any theory into Isabel?

Question

I want to define my own type of list in a theory called List , but there is already a theory with that name. Is there a lighter theory than Main ?

Answer 1

You cannot import anything into Isabelle (since import is necessary even for basic logic). The Isabelle HOL implementation has three supported entry points: Main , Complex_Main (which is Main plus some analysis) and Plain , but only the first two are for regular use.

Normal already contains the basic logic, but understands almost nothing in the standard library (for example, there are no lists). But important tools such as QuickCheck, Sledgehammer, and a code generator are also missing. Moreover, if you start with Plain to be able to name your own list of theories, keep in mind that your theory will be incompatible with any construction of work on Main (that's almost all).

So, if you have no good reason for this, I would suggest the next comment by Raphael and give your list a different name.

Answer 2

Note that $ISABELLE_HOME/src/HOL/ex/Seq.thy provides a minimal example of defining your own list data type for experimentation without resorting to the delicate question of how to work with the system below the Main entry point. (Beginners get confused, and experts don't.)

Theoretically, the most primitive theory you can import is Pure , but it's just a bare logical structure without any object-logical model such as HOL. Just for curiosity, you can look at $ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy , which starts with Pure and defines the minimum version of HOL in fact, without any of the advanced theories and tools you would expect from a full Isabelle / HOL, though.

Answer 3

You can import only HOL , as in

 theory Test_Theory imports HOL begin … end 

I often do this to test and study Isabelle.

However, you are missing data type definitions and you probably need to import Datatype (and maybe even Record ) to be able to write your List theory.

 theory Test_Theory imports HOL Datatype Record begin … end 

Since both Datatype and Record import HOL , you can simply:

 theory Test_Theory imports Datatype Record begin … end 

It is not easy to do without Main theory, but not impossible. Just keep in mind that you will have to do without many widely used theorems and may have to write and prove your rights.