src/Doc/Eisbach/Preface.thy
author wenzelm
Sun May 17 23:03:49 2015 +0200 (2015-05-17)
changeset 60288 d7f636331176
child 60298 7c278b692aae
permissions -rw-r--r--
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
     1 (*:wrap=hard:maxLineLen=78:*)
     2 
     3 theory Preface
     4 imports Base "../Eisbach_Tools"
     5 begin
     6 
     7 text \<open>
     8   \emph{Eisbach} is a collection of tools which form the basis for defining
     9   new proof methods in Isabelle/Isar~@{cite "Wenzel-PhD"}. It can be thought
    10   of as a ``proof method language'', but is more precisely an infrastructure
    11   for defining new proof methods out of existing ones.
    12 
    13   The core functionality of Eisbach is provided by the Isar @{command method}
    14   command. Here users may define new methods by combining existing ones with
    15   the usual Isar syntax These methods can be abstracted over terms, facts and
    16   other methods, as one might expect in any higher-order functional language.
    17 
    18   Additional functionality is provided by extending the space of methods and
    19   attributes. The new @{method match} method allows for explicit control-flow,
    20   by taking a match target and a list of pattern-method pairs. By using the
    21   functionality provided by Eisbach, additional support methods can be easily
    22   written. For example, the @{method catch} method, which provides basic
    23   try-catch functionality, only requires a few lines of ML.
    24 
    25   Eisbach is meant to allow users to write automation using only Isar syntax.
    26   Traditionally proof methods have been written in Isabelle/ML, which poses a
    27   high barrier-to-entry for many users.
    28 
    29   \medskip This manual is written for users familiar with Isabelle/Isar, but
    30   not necessarily Isabelle/ML. It covers the usage of the @{command method} as
    31   well as the @{method match} method, as well as discussing their integration
    32   with existing Isar concepts such as @{command named_theorems}.
    33 \<close>
    34 
    35 end