Checking datatypes in Isabelle

Question

Importing Main allows you to use types such as nat and int, but you won't have the info on how these are defined without digging though the source.

Is there a way to check/print the definition of datatypes in your own program, without having to manually search in the source?

Answer 1

When you use datatype in Isabelle, you are actually defining a new type, and several new constants and new theorems.

A simple example. When you write

datatype blub = A | B

1. You define the new type blub.

2. You define several constants:

   find_consts name: "blub."
   
   found 6 constant(s):
     Scratch.blub.case_blub :: "'a ⇒ 'a ⇒ blub ⇒ 'a"
     Scratch.blub.rec_blub :: "'a ⇒ 'a ⇒ blub ⇒ 'a"
     Scratch.blub.typerep_blub_IITN_blub_inst.typerep_blub_IITN_blub ::
       "blub.blub_IITN_blub itself ⇒ typerep"
     Scratch.blub.size_blub :: "blub ⇒ nat"
     Scratch.blub.A :: "blub"
     Scratch.blub.B :: "blub"
   

3. You define new theorems:

   find_theorems name: "blub."
   found 28 theorem(s):
     Scratch.blub.simps(1): A ≠ B
     Scratch.blub.simps(2): B ≠ A
     Scratch.blub.size(3): size A = 0
     Scratch.blub.size(4): size B = 0
     Scratch.blub.size(1): size_blub A = 0
     Scratch.blub.size(2): size_blub B = 0
     ...
   

You can search for the new constants and theorems using the respective search commands or the query panel using the common name prefix. If you want to see the real definition, just use jedit (e.g. Ctrl-click) to jump to the definition.

For foundational types like nat it is a bit more complex, because nat is defined before the datatype command and later made to behave as if it was defined with datatype.