Is it possible to not import any theory in Isabelle?

Question

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

Answer 1

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

Theoretically, the most primitive theory you could import is Pure, but that is just the bare-bones logical framework, without any object-logic like HOL yet. Just for curiosity, you may look at $ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy which starts from Pure and defines a minimal version of H.O.L. on top of it, without any of the advanced theories and tools you would expect from full Isabelle/HOL, though.

Answer 2

You cannot import nothing in Isabelle (as the import is necessary even for the basic logic). The implementation of HOL in Isabelle has three supported entry points: Main, Complex_Main (which is Main plus some Analysis) and Plain, but only the first two are intendend for regular usage.

Plain already contains the basic logic, but almost nothing in terms of the standard library (e.g. no lists). But also important tools like QuickCheck, Sledgehammer and the code generator are missing. Moreover, if you start from Plain to be able to name your own theory List, be aware that your theory will be incompatible with any work building on Main (which is almost everything).

So, unless you have really good reasons to do so, I would suggest following Raphael's comment and give your list theory another name.