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:

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