CODEWITHSUNDEEP
isabelle
davidg
davidg

Reputation: 6007

How do I view hidden type variables in Isabelle proof goals?

In Isabelle, one can often hit proof goals where the intermediate type of terms is critical to a proof's correctness. For instance, consider the following lemma converting the nat 42 into an 'a word then back again:

theory Test
imports "~~/src/HOL/Word/Word"
begin

lemma "unat (of_nat 42) = 42"
  ...

Now the truth of this statement depends on the type of of_nat 42: if it is 32 word, then the statement is true, if it is a 2 word, however, the statement is false.

Unfortunately, I can't seem to get Isabelle to display this intermediate type to me.

I have tried the following:

all of which just display:

unat (of_nat (42::nat)) = (42::nat)

In a pinch, one can do:

apply (tactic {* (fn t => (tracing (PolyML.makestring (prems_of t)); all_tac t))  *})

do get a raw dump of the term, but I was hoping there was a better way.

Is there a good way of displaying intermediate term types in a proof goal?

Upvotes: 3

Views: 1303

Answers (3)

davidg
davidg

Reputation: 6007

Running the command:

setup {* Config.put_global show_all_types true *}

seems to do the trick.

The goal unat (of_nat 3) = 3 becomes the hideous (but complete):

goal (1 subgoal):
 1. (Trueprop::bool => prop)
     ((op =::nat => nat => bool)
       ((unat::'a word => nat)
         ((of_nat::nat => 'a word)
           ((numeral::num => nat)
             ((num.Bit1::num => num) (num.One::num)))))
       ((numeral::num => nat)
         ((num.Bit1::num => num) (num.One::num))))

as desired.

It is interesting that a declare [[show_all_types]] does not work; the source looks like it should. Perhaps it is a bug in Isabelle2013?

Upvotes: 2

lsf37
lsf37

Reputation: 535

To make Isabelle show you the type of unat in this example, you want to declare the following:

  declare [[show_types]]
  declare [[show_sorts]]
  declare [[show_consts]]

The last line prints the type of each constant used in the goal in the output window. This works both in jEdit and ProofGeneral.

There is a problem with this solution: if unat occurs multiple times with different types, it will print all these instances, but it will not tell you which type instance is which occurrence. Apart from the jEdit hover, I don't know of any solution for that, though.

Upvotes: 4

chris
chris

Reputation: 5018

In Isabelle/jEdit you can always "control-hover" (i.e., keep the control-button pressed and hover the mouse) over a constant in order to get additional information. For of_nat in

lemma "unat (of_nat 42) = 42"

This results in

constant "Nat.semiring_1_class.of_nat"
:: nat => 'a word

Now you can recursively do the same on 'a of 'a word and will get

:: len
free type variable

which tells you that 'a is of sort len (by control-clicking len, you could directly jump to the definition of this type class, which is also quite handy).

So the answer to your question is: yes, control-hover in Isabelle/jEdit.

Upvotes: 4

Related Questions