My impression that the new Isabelle 2007 does not break anything related to ZF was a bit premature. It turns out that the interpretation of locales has changed. There is a locale (context) in IsarMathLib called *MMIsar0 *that is used for Metamath to Isabelle/ZF translation. This locale has twenty five assumptions corresponding to Metamath’s axioms for complex numbers. The *MMIsar_valid * theorem in *Metamath_interface.thy *shows that if we take a model of real numbers (i.e. a completely ordered field) and construct the complex numbers from it in the standard way, then all Metamath axioms about complex numbers are satisfied. The problem is that those assumptions in *MMIsar0 *are interpreted by Isabelle 2007 not as a flat conjunction, but are grouped with parentheses into a complicated structure nested up to four levels deep in some places. It is not a show stopper, but it will take me some time to reflect this nesting structure in the proof.

This is a symptom of a deeper, architectural problem. When verifying a proof written in Isar Isabelle searches for a low-level proof and once it finds one it considers the Isar proof verified, so it discards the low-level proof. This causes problems every time the proof searching algorithm is changed – that is with every new Isabelle release. Some proofs that were successfully verified before don’t check any more. The only solution to this is to design a system so that the low-level proof is not discarded. Once the low-level proof corresponding to high-level source constructs is found, it can serve as the basis of verification and does not need to be generated again. I think while Isar is great for a high-level proof language, something like Metamath would be great as the underlying low-level language.

### Like this:

Like Loading...

*Related*

Tags: Isabelle/ZF, IsarMathLib

This entry was posted on December 22, 2007 at 9:43 pm and is filed under Uncategorized. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

## Leave a Reply