wenzelm@42915

1 
theory Preface

wenzelm@42651

2 
imports Base Main

wenzelm@27035

3 
begin

wenzelm@27035

4 

wenzelm@58618

5 
chapter \<open>Preface\<close>

wenzelm@27035

6 

wenzelm@58618

7 
text \<open>

wenzelm@27035

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

wenzelm@27035

9 
infrastructure for building deductive systems (programmed in

wenzelm@27035

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

wenzelm@29743

11 
higherorder logics. Many years ago, even endusers would refer to

wenzelm@29743

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

wenzelm@29743

13 
pursue their everyday theorem proving tasks.

wenzelm@27035

14 

wenzelm@27035

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

wenzelm@27035

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

wenzelm@27035

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

wenzelm@27035

18 
toplevel provides a more robust and comfortable development

wenzelm@29743

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

wenzelm@51058

20 
transactions with unlimited undo etc.

wenzelm@51058

21 

wenzelm@51058

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

wenzelm@58552

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

wenzelm@58552

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

wenzelm@51058

25 
success of for interactive theory and proof development in this

wenzelm@51058

26 
advanced theorem proving environment, even though it was somewhat

wenzelm@51058

27 
biased towards oldstyle proof scripts. The more recent

wenzelm@58552

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

wenzelm@51058

29 
documentoriented approach of Isabelle/Isar again more explicitly.

wenzelm@27035

30 

wenzelm@27035

31 
\medskip Apart from the technical advances over barebones ML

wenzelm@27035

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

wenzelm@27035

33 
conceptually different view on machinechecked proofs

wenzelm@58552

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

wenzelm@29743

35 
\emph{Intelligible semiautomated reasoning}. Drawing from both the

wenzelm@27035

36 
traditions of informal mathematical proof texts and highlevel

wenzelm@27035

37 
programming languages, Isar offers a versatile environment for

wenzelm@27035

38 
structured formal proof documents. Thus properly written Isar

wenzelm@27035

39 
proofs become accessible to a broader audience than unstructured

wenzelm@27035

40 
tactic scripts (which typically only provide operational information

wenzelm@27035

41 
for the machine). Writing humanreadable proof texts certainly

wenzelm@27035

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

wenzelm@27035

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

wenzelm@27035

44 
other hand, humanreadable formal texts gain some value in their own

wenzelm@27035

45 
right, independently of the mechanic proofchecking process.

wenzelm@27035

46 

wenzelm@27035

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

wenzelm@27035

48 
assimilate the old tactical style as an ``improper'' sublanguage.

wenzelm@27035

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

wenzelm@29743

50 
well as some means for interactive experimentation and debugging of

wenzelm@29743

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

wenzelm@29743

52 
styles, both readable and unreadable ones.

wenzelm@27035

53 

wenzelm@29716

54 
\medskip The generic Isabelle/Isar framework (see

wenzelm@29743

55 
\chref{ch:isarframework}) works reasonably well for any Isabelle

wenzelm@29743

56 
objectlogic that conforms to the natural deduction view of the

wenzelm@29743

57 
Isabelle/Pure framework. Specific language elements introduced by

wenzelm@50109

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

wenzelm@48957

59 
language elements are already provided by the Isabelle/Pure

wenzelm@48957

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

wenzelm@48957

61 
Isabelle/HOL.

wenzelm@27040

62 

wenzelm@27040

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

wenzelm@27040

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

wenzelm@27040

65 
attributes introduced later are classified as improper as well.

wenzelm@27040

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

wenzelm@27040

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

wenzelm@27040

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

wenzelm@27040

69 
the final humanreadable outcome. Typical examples are diagnostic

wenzelm@27040

70 
commands that print terms or theorems according to the current

wenzelm@27040

71 
context; other commands emulate oldstyle tactical theorem proving.

wenzelm@58618

72 
\<close>

wenzelm@27035

73 

wenzelm@27035

74 
end
