Re: [isabelle] Length of Proofs



On Thu, 22 Nov 2012, Lawrence Paulson wrote:

You still have the capacity to code your own proof procedures; ML is just one level down. And you get a much more readable proof language.

The situation is a bit more general than this, and it is hard to arrange Isar vs. ML in "levels" in particular. Both are intertwined, cf. my explanation of Isabelle/Isar and Isabelle/ML as as the Yin and Yang of Isabelle https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-April/msg00066.html

In general Isar vs. its embedded languages works like this:

  * Isar is the main framework of Isabelle to integrate many
    other languages.

  * The Isar languages for specifications (e.g. 'theorem', 'definition',
    'function') and proofs (e.g. 'fix', 'assume', 'show' ...) are the
    primary applications of the Isar framework.

  * The logical language (Pure types/terms/propositions with specific HOL
    notation) is another important embedded language, cf. the quotes that
    have been around this language even in the ancient ML-only times of
    Isabelle in the 1990-ies.

  * ML is embedded into Isar in a similar manner, but at the same
    time it is the implementation language of Isar.  Moreover, ML quoted
    inside Isar can antiquote logic/Isar expressions.  So the image for
    that is http://en.wikipedia.org/wiki/File:Yin_and_Yang.svg

In everyday life you don't use the ML inside Isar a lot, but you can whenever you need to. It is more convenient than the ancient ML toplevel ever was. In Isabelle/jEdit you also have substantial IDE integration for this ML inside Isar.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.