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

doc-src/IsarRef/Thy/document/Introduction.tex

author | wenzelm |

Fri Oct 29 11:49:56 2010 +0200 (2010-10-29) | |

changeset 40255 | 9ffbc25e1606 |

parent 30242 | aea5d7fa7ef5 |

child 40406 | 313a24b66a8d |

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

eliminated obsolete \_ escapes in rail environments;

1 %

2 \begin{isabellebody}%

3 \def\isabellecontext{Introduction}%

4 %

5 \isadelimtheory

6 %

7 \endisadelimtheory

8 %

9 \isatagtheory

10 \isacommand{theory}\isamarkupfalse%

11 \ Introduction\isanewline

12 \isakeyword{imports}\ Main\isanewline

13 \isakeyword{begin}%

14 \endisatagtheory

15 {\isafoldtheory}%

16 %

17 \isadelimtheory

18 %

19 \endisadelimtheory

20 %

21 \isamarkupchapter{Introduction%

22 }

23 \isamarkuptrue%

24 %

25 \isamarkupsection{Overview%

26 }

27 \isamarkuptrue%

28 %

29 \begin{isamarkuptext}%

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

31 infrastructure for building deductive systems (programmed in

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

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

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

35 pursue their everyday theorem proving tasks.

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

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

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

40 top-level provides a more robust and comfortable development

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

42 transactions with unlimited undo etc. The Isabelle/Isar version of

43 the \emph{Proof~General} user interface

44 \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end

45 for interactive theory and proof development in this advanced

46 theorem proving environment, even though it is somewhat biased

47 towards old-style proof scripts.

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

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

51 conceptually different view on machine-checked proofs

52 \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for

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

54 traditions of informal mathematical proof texts and high-level

55 programming languages, Isar offers a versatile environment for

56 structured formal proof documents. Thus properly written Isar

57 proofs become accessible to a broader audience than unstructured

58 tactic scripts (which typically only provide operational information

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

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

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

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

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

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

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

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

68 well as some means for interactive experimentation and debugging of

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

70 styles, both readable and unreadable ones.

72 \medskip The generic Isabelle/Isar framework (see

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

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

75 Isabelle/Pure framework. Specific language elements introduced by

76 the major object-logics are described in \chref{ch:hol}

77 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}

78 (Isabelle/ZF). The main language elements are already provided by

79 the Isabelle/Pure framework. Nevertheless, examples given in the

80 generic parts will usually refer to Isabelle/HOL as well.

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

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

84 attributes introduced later are classified as improper as well.

85 Improper Isar language elements, which are marked by ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'' in the subsequent chapters; they are often helpful

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

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

88 commands that print terms or theorems according to the current

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

90 \end{isamarkuptext}%

91 \isamarkuptrue%

92 %

93 \isadelimtheory

94 %

95 \endisadelimtheory

96 %

97 \isatagtheory

98 \isacommand{end}\isamarkupfalse%

99 %

100 \endisatagtheory

101 {\isafoldtheory}%

102 %

103 \isadelimtheory

104 %

105 \endisadelimtheory

106 \isanewline

107 \end{isabellebody}%

108 %%% Local Variables:

109 %%% mode: latex

110 %%% TeX-master: "root"

111 %%% End: