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