Re: [mizar] notes on isabelle vs. mizar

[Makarius <makarius@sketis.net>]

On Thu, 7 Feb 2008, Josef Urban wrote:

> someone here might be interested a couple of fairly raw (and sometimes
> probably incorrect) notes comparing some features of isabelle and mizar:
> http://www.google.com/notebook/public/13713103740520825807/BDQ7EQwoQw4TZgfwi .

Just some notes on this from the Isabelle perspective.


* Semantics:

Isabelle/Pure (the logical framework) and Isabelle/HOL (a major 
application within that) should not be confused, as appears to be done in 
the discussion about axiomatic vs. definitional extensions.

Starting from the Pure theory, initial extensions are usually axiomatic 
(declaring types, consts, axioms), in order specify an object-logic (say 
FOL, ZF, HOL, HOLCF).  Normal applications never do this -- it would 
require to reconsider the whole logical foundations of axiomatizations.  
Isabelle does provide proper definitional elements that are also 
explicitly checked, similar to HOL4 and HOL-Light (although the latter is 
much more picky about this).

At times, some adventurous individuals do extend an existing logical base 
by new axioms, as has been done for HOLCF (HOL + Scott domain theory) and 
HOLZF (HOL + ZF axioms).

If you look at regular applications within Isabelle/HOL or Isabelle/ZF it 
is all just definitions and proofs, as in Mizar.


* Locales, type classes vs. structures: It would be *very* interesting to 
look more closely at this.  I would also like to understand Mizar 
aggregates better, especially the version that has been presented at MKM 
2007.


* Set theory in Isabelle/HOL:

You write "I wonder how one gets around the limitation that sets is 
defined as a predicate on a particular type".  Well you just suffer, and 
restrict yourself to applications where this does not matter, or is even 
quite natural in the first place (e.g. modeling programming-style 
concepts, similar to ML or Haskell).

Personally, I would like to move on to full set-theory in the style of 
Isabelle/ZF.  But this would need a layer for proper syntactic type 
checking, similar to the present one in HOL, but without the theoretical 
limitations.  In his paper on TPHOLs 2007, Freek makes a point about a 
type-system being either "foundational" (as in HOL or Coq) or just a 
convenience for the user, claiming that the latter is what you want. I 
agree, but it is still a long way to go until this happens in Isabelle/ZF.


* Partial functions in HOL: very cumbersome indeed.

People usually use total functions with underspecification on "undefined" 
parts.  There is also an Isabelle/HOL insider joke going like this:

  if undefined = arbitrary then (SOME x. True) else (SOME x. False)

Of course, you can model proper partial functions, cf. 'a => 'b option in 
ML, or as sets/graphs, but then you need further wrappings that make 
things a bit more complicated.

Here you also mention "lambda calculus/type theory" in a way that seems to 
cover both simple type-theory (HOL) or dependent type-theory (e.g. Coq).  
This is fine at a certain level of abstraction, but for the purpose of 
partial functions it could make a big difference.  (Although I cannot 
really speak for Coq here.)


* Automation:

You say "automation much better in Isabelle".  Well, Isabelle/Pure merely 
provides higher-order unification, which is nice but not so much 
automation.  Everything else is implemented on top of the existing system.  
The important point here is that this can be done, i.e. Isabelle is an 
open system, unlike Mizar.


* Library:

You say "large parts of the library are not distributed with Isabelle only 
available through http://afp.sourceforge.net/ this will eventually lead to 
their incompatibility with the system and distributed library".

AFP is surprisingly easy to maintain.  We do it continously as we go on 
modifying the main Isabelle distribution.  So these two are practically in 
sync all the time.  There are official AFP distributions corresponding to 
official Isabelle releases.


You say "Browsing of Isabelle formalizations sucks".  I basically agree, 
but nobody really browses the sources or HTML pages.  Did you try 
find_theorems within the live Isabelle session?


You say "some Isabelle formalization have ML code in them this should be 
completely hidden from mathematicians, Mizar seems to be better just for 
browsing formal mathematics".  I disagree with that.  While ML is harder 
to read than common Isabelle/Isar source specifications, it is an integral 
part in building up the library, enabling almost arbitrary extensions to 
the system as you move on.  Some details can be still improved, but we 
have gone a far way from the traditional ``LCF'' approach of ML-only 
theories that is still present in HOL / HOL-Light (here even basic 
specifications and proofs are all in ML).  Isabelle has always tried to 
minimize ML, but not to abolish it.  Recently we have even started to 
integrate ML into Isar more seriously.


* Isar vs. Mizar:

I would say you can practically forget about "thus" and "hence" in Isar -- 
today I would prefer to get rid of these slightly odd abbreviations of 
"then show" and "then have" altogether.  Apart from the shared "assume", 
this makes the keywords of both proof languages almost disjoint, which is 
adequate, as the exect meaning is quite different.

Comparing Isar and Mizar is nevertheless interesting, but requires a more 
detailed inspection.  (I've done some of this together with Freek in 2002, 
and some more with Adam last summer at Bertinoro.)


* Proof General:

You write "It is a nuisance that Proof General has to stop Isabelle 
running for one buffer". Most users just invoke several isabelle-interface 
processes at the same time as required, e.g. when porting existing 
libraries from one version of Isabelle to another.  This does not mean 
that Proof General is the last word on user interfaces for theorem 
provers.

The interaction model of Proof General is that of traditional interactive 
proof checkers (LCF, HOL, Coq etc.).  Isabelle/Isar also emulates this, 
because of its heritage, but it is much more flexibile inside.  At the 
TYPES workshop at Edinburgh last fall, I've proposed an interaction model 
that is essentially a synthesis of Mizar-style whole-text processing with 
traditional LCF-style interaction, see also 
http://homepages.inf.ed.ac.uk/rpollack/mathWiki/slides/Wenzel.pdf


	Makarius