summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Isar_Ref/Preface.thy

author | wenzelm |

Wed Mar 25 11:39:52 2015 +0100 (2015-03-25) | |

changeset 59809 | 87641097d0f3 |

parent 58618 | 782f0b662cae |

child 60286 | 410115884a92 |

permissions | -rw-r--r-- |

tuned signature;

1 theory Preface

2 imports Base Main

3 begin

5 chapter \<open>Preface\<close>

7 text \<open>

8 The \emph{Isabelle} system essentially provides a generic

9 infrastructure for building deductive systems (programmed in

10 Standard ML), with a special focus on interactive theorem proving in

11 higher-order logics. Many years ago, even end-users would refer to

12 certain ML functions (goal commands, tactics, tacticals etc.) to

13 pursue their everyday theorem proving tasks.

15 In contrast \emph{Isar} provides an interpreted language environment

16 of its own, which has been specifically tailored for the needs of

17 theory and proof development. Compared to raw ML, the Isabelle/Isar

18 top-level provides a more robust and comfortable development

19 platform, with proper support for theory development graphs, managed

20 transactions with unlimited undo etc.

22 In its pioneering times, the Isabelle/Isar version of the

23 \emph{Proof~General} user interface @{cite proofgeneral and

24 "Aspinall:TACAS:2000"} has contributed to the

25 success of for interactive theory and proof development in this

26 advanced theorem proving environment, even though it was somewhat

27 biased towards old-style proof scripts. The more recent

28 Isabelle/jEdit Prover IDE @{cite "Wenzel:2012"} emphasizes the

29 document-oriented approach of Isabelle/Isar again more explicitly.

31 \medskip Apart from the technical advances over bare-bones ML

32 programming, the main purpose of the Isar language is to provide a

33 conceptually different view on machine-checked proofs

34 @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD"}. \emph{Isar} stands for

35 \emph{Intelligible semi-automated reasoning}. Drawing from both the

36 traditions of informal mathematical proof texts and high-level

37 programming languages, Isar offers a versatile environment for

38 structured formal proof documents. Thus properly written Isar

39 proofs become accessible to a broader audience than unstructured

40 tactic scripts (which typically only provide operational information

41 for the machine). Writing human-readable proof texts certainly

42 requires some additional efforts by the writer to achieve a good

43 presentation, both of formal and informal parts of the text. On the

44 other hand, human-readable formal texts gain some value in their own

45 right, independently of the mechanic proof-checking process.

47 Despite its grand design of structured proof texts, Isar is able to

48 assimilate the old tactical style as an ``improper'' sub-language.

49 This provides an easy upgrade path for existing tactic scripts, as

50 well as some means for interactive experimentation and debugging of

51 structured proofs. Isabelle/Isar supports a broad range of proof

52 styles, both readable and unreadable ones.

54 \medskip The generic Isabelle/Isar framework (see

55 \chref{ch:isar-framework}) works reasonably well for any Isabelle

56 object-logic that conforms to the natural deduction view of the

57 Isabelle/Pure framework. Specific language elements introduced by

58 Isabelle/HOL are described in \partref{part:hol}. Although the main

59 language elements are already provided by the Isabelle/Pure

60 framework, examples given in the generic parts will usually refer to

61 Isabelle/HOL.

63 \medskip Isar commands may be either \emph{proper} document

64 constructors, or \emph{improper commands}. Some proof methods and

65 attributes introduced later are classified as improper as well.

66 Improper Isar language elements, which are marked by ``@{text

67 "\<^sup>*"}'' in the subsequent chapters; they are often helpful

68 when developing proof documents, but their use is discouraged for

69 the final human-readable outcome. Typical examples are diagnostic

70 commands that print terms or theorems according to the current

71 context; other commands emulate old-style tactical theorem proving.

72 \<close>

74 end