IsarMathLib and Isabelle/ZF

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.


Tags: ,

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: