Isabelle

[Main][Contact][CV][Isabelle][Map Theory][Bibliography][Links]

Isabelle

Import Tool

I have implemented a tool for porting theorems from the HOL4 system to Isabelle/HOL. The tool is now part of the Isabelle2004 distribution.

Installing

Please read the README file in the src/HOL/Import/HOL directory of the Isabelle distribution.

Using

Once you have build the HOL4 image, you can access it as you would any other logic in Isabelle.

What's there?

The new theories are called HOL4Base (basic libraries), HOL4Real (real analysis), HOL4Prob (probabilistic algorithms), and HOL4Vec and HOL4Word32 (bit vectors). The theory HOL4 just includes all of the others.

The HOL4 types, constants, and theorems can be found easily in the the theories: In Isabelle, they will normally just be called <library>.<name>. For example, the theorem REAL_LT_RDIV found in the HOL4 library real can be accessed as real.REAL_LT_RDIV.

Sometimes, you won't find a certain type, constant, or theorem in the Isabelle theory. Then what? First, make sure the HOL4 library has even been ported (see the table below). If it has, then one of several things can have happened:

The construct already exists in Isabelle, and therefore is to be found in an "old" Isabelle theory. The constant NIL of the list library is found as List.list.Nil in Isabelle.
The construct has been renamed. The constant "==" in the word32 library, for example, clashes with Isabelle's meta-equality, and has therefore been renamed to EQUIV
The construct is not needed. This is a rare case, but can occur with theorems or constants that are needed for a type definition in HOL4, but where the type is already defined in Isabelle.

For all the above cases, try looking in the file <library>.imp. The information in the imp file might allow you to figure out what actually happened.

Which HOL4 libraries can be found in which Isabelle theory?
HOL4Base	arithmetic bool combin divides hrat hreal ind_type list marker num numeral one operator option pair pred_set prime prim_rec relation rich_list sum
HOL4Real	lim nets poly powser real realax seq topology transc
HOL4Prob	boolean_sequence prob prob_algebra prob_canon prob_extra prob_indep prob_pseudo prob_uniform state_transformer
HOL4Vec	bword_arith bword_bitop bword_num res_quan word_base word_bitop word_num
HOL4Word32	bits word32

[Main][Contact][CV][Isabelle][Map Theory][Bibliography][Links]

Isabelle