10

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?

chris
  • 4,988
  • 20
  • 36
user1494846
  • 244
  • 3
  • 10
  • FYI, in case you don't get the answer you're looking for here, it might be worth it also asking the question on cs.stackexchange.com or cstheory.stackexchange.com ... – reuben Jul 05 '12 at 00:58
  • 2
    @reuben: Neither site is there for tool support. Isabelle's [documentation](http://isabelle.in.tum.de/documentation.html) and [community](https://isabelle.in.tum.de/community) is the correct place to go. – Raphael Jul 05 '12 at 22:50
  • 8
    Note to closers: this question is squarely on-topic on Stack Overflow. Isabelle is a theorem prover, and those are a special kind of programming environment ([tag:coq] and [tag:agda] are other examples that have a small but existing community on SO). Using a programming tool is on-topic on Stack Overflow. (@Raphael No, the question is fine here.) – Gilles 'SO- stop being evil' Jul 05 '12 at 22:51
  • 2
    @reuben Not CSTheory, this isn't a research-level question. Maybe [cs.se], at this point it's borderline, we haven't settled on a policy that would place this question on one side of the border yet. – Gilles 'SO- stop being evil' Jul 05 '12 at 22:57
  • 1
    More to the point of the question: you can import nothing, or copy `main.thy` and remove `List` and all dependent stuff. I would strongly advise against this, though. Would you throw away the standard library and implement your own sorting algorithm? Building lists from the ground up is a good exercise -- and not trivial, too! Just call it `MyList` or something. – Raphael Jul 05 '12 at 23:16

3 Answers3

7

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.

Makarius
  • 2,165
  • 18
  • 20
4

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.

Lars Noschinski
  • 3,667
  • 16
  • 29
  • 2
    "Plain" doesn't work. There is a need for such deconstruction, because it helps with learning a lot. – ged Apr 04 '19 at 21:42
0

You may import HOL only, as in 

theory Test_Theory
imports HOL
begin
  …
end

I often do it for testing and investigating about Isabelle.

However, you will lack data‑type definitions, and will probably need to import Datatype (and may be even Record) as well, in order to be able to write your List theory.

theory Test_Theory
imports HOL Datatype Record
begin
  …
end

As both Datatype and Record imports HOL, you may simply have:

theory Test_Theory
imports Datatype Record
begin
  …
end

That's not easy to do without theory Main, but not impossible. Just be aware you will have to do without many widely used theorems, and may have to write and prove your owns.

Hibou57
  • 6,870
  • 6
  • 52
  • 56
  • I didn't knew about `FunDef`, thanks for the tip, will have a look at it. I'm indeed interested too is “less bloated” base theories, at least because it consumes a lot of memory (I'm running a 1G RAM machine, which is small for Isabelle… I'm planning to get some more RAM especially for Isabelle). Also, another reason to seek for another theories set than what `Main` provides, is that some theories are not well suited for some kind of proof. As an example, I feel the axiomatization the set theory use, is not handy, and wish to set up my own (if possible). – Hibou57 Mar 04 '13 at 01:58
  • 1
    Note that importing anything below `Main` HOL is unspecified, and odd effects are to be expected. 1 GB RAM is a bad reason for entering the internals of how Isabelle/HOL is bootstrapped. – Makarius Mar 15 '13 at 14:30
  • Isn't it the same with `Pure`? (I will have look, thanks for the point). – Hibou57 Mar 16 '13 at 04:54
  • The only valid reason to start with `Pure` is if you want to implement your own logic. But it is a stable entry point -- it marks the complete setup of the logical framework. The intermediate theories of HOL however are just arranged in a way that works to get to `Main`. Everything might change if we find a better way to organize HOL. Also, some proof tools might have an not-yet complete setup. – Lars Noschinski May 23 '13 at 06:37