author | wenzelm |
Tue, 18 May 2021 15:17:55 +0200 | |
changeset 73723 | 1bbbaae6b5e3 |
parent 73401 | 8b464825d2b5 |
permissions | -rw-r--r-- |
18537 | 1 |
\documentclass[12pt,a4paper,fleqn]{report} |
55365 | 2 |
\usepackage[T1]{fontenc} |
73401 | 3 |
\usepackage{graphicx} |
18537 | 4 |
\usepackage[refpage]{nomencl} |
48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
5 |
\usepackage{iman,extra,isar,proof} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
6 |
\usepackage[nohyphen,strings]{underscore} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
7 |
\usepackage{isabelle} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
8 |
\usepackage{isabellesym} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
9 |
\usepackage{railsetup} |
52412 | 10 |
\usepackage{supertabular} |
18537 | 11 |
\usepackage{style} |
48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
12 |
\usepackage{pdfsetup} |
18537 | 13 |
|
14 |
||
15 |
\hyphenation{Isabelle} |
|
16 |
\hyphenation{Isar} |
|
17 |
||
18 |
\isadroptag{theory} |
|
73723 | 19 |
\title{\includegraphics[scale=0.5]{isabelle_logo} |
18537 | 20 |
\\[4ex] The Isabelle/Isar Implementation} |
28780 | 21 |
\author{\emph{Makarius Wenzel} \\[3ex] |
22 |
With Contributions by |
|
52412 | 23 |
Stefan Berghofer, \\ |
28780 | 24 |
Florian Haftmann |
25 |
and Larry Paulson |
|
26 |
} |
|
18537 | 27 |
|
28 |
\makeindex |
|
29 |
||
30 |
||
31 |
\begin{document} |
|
32 |
||
35031 | 33 |
\maketitle |
18537 | 34 |
|
35 |
\begin{abstract} |
|
36 |
We describe the key concepts underlying the Isabelle/Isar |
|
37 |
implementation, including ML references for the most important |
|
20451 | 38 |
functions. The aim is to give some insight into the overall system |
20488 | 39 |
architecture, and provide clues on implementing applications within |
40 |
this framework. |
|
18537 | 41 |
\end{abstract} |
42 |
||
19189 | 43 |
\vspace*{2.5cm} |
44 |
\begin{quote} |
|
35031 | 45 |
|
19189 | 46 |
{\small\em Isabelle was not designed; it evolved. Not everyone |
47 |
likes this idea. Specification experts rightly abhor |
|
48 |
trial-and-error programming. They suggest that no one should |
|
20024 | 49 |
write a program without first writing a complete formal |
19189 | 50 |
specification. But university departments are not software houses. |
51 |
Programs like Isabelle are not products: when they have served |
|
52 |
their purpose, they are discarded.} |
|
35031 | 53 |
|
19189 | 54 |
Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers'' |
55 |
||
56 |
\vspace*{1cm} |
|
35031 | 57 |
|
19189 | 58 |
{\small\em As I did 20 years ago, I still fervently believe that the |
59 |
only way to make software secure, reliable, and fast is to make it |
|
20064 | 60 |
small. Fight features.} |
35031 | 61 |
|
19189 | 62 |
Andrew S. Tanenbaum |
63 |
||
35031 | 64 |
\vspace*{1cm} |
65 |
||
66 |
{\small\em One thing that UNIX does not need is more features. It is |
|
67 |
successful in part because it has a small number of good ideas |
|
68 |
that work well together. Merely adding features does not make it |
|
69 |
easier for users to do things --- it just makes the manual |
|
70 |
thicker. The right solution in the right place is always more |
|
71 |
effective than haphazard hacking.} |
|
72 |
||
73 |
Rob Pike and Brian W. Kernighan |
|
74 |
||
51660 | 75 |
\vspace*{1cm} |
76 |
||
77 |
{\small\em If you look at software today, through the lens of the |
|
78 |
history of engineering, it's certainly engineering of a sort--but |
|
79 |
it's the kind of engineering that people without the concept of |
|
80 |
the arch did. Most software today is very much like an Egyptian |
|
81 |
pyramid with millions of bricks piled on top of each other, with |
|
82 |
no structural integrity, but just done by brute force and |
|
83 |
thousands of slaves.} |
|
84 |
||
85 |
Alan Kay |
|
86 |
||
19189 | 87 |
\end{quote} |
88 |
||
89 |
\thispagestyle{empty}\clearpage |
|
90 |
||
20514 | 91 |
\pagenumbering{roman} |
92 |
\tableofcontents |
|
93 |
\listoffigures |
|
94 |
\clearfirst |
|
18537 | 95 |
|
39822 | 96 |
\setcounter{chapter}{-1} |
97 |
||
48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
98 |
\input{ML.tex} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
99 |
\input{Prelim.tex} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
100 |
\input{Logic.tex} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
101 |
\input{Syntax.tex} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
102 |
\input{Tactic.tex} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
103 |
\input{Eq.tex} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
104 |
\input{Proof.tex} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
105 |
\input{Isar.tex} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
106 |
\input{Local_Theory.tex} |
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
107 |
\input{Integration.tex} |
18537 | 108 |
|
109 |
\begingroup |
|
110 |
\tocentry{\bibname} |
|
30116 | 111 |
\bibliographystyle{abbrv} \small\raggedright\frenchspacing |
48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
46295
diff
changeset
|
112 |
\bibliography{manual} |
18537 | 113 |
\endgroup |
114 |
||
115 |
\tocentry{\indexname} |
|
116 |
\printindex |
|
117 |
||
118 |
\end{document} |
|
119 |
||
120 |
||
35031 | 121 |
%%% Local Variables: |
18537 | 122 |
%%% mode: latex |
123 |
%%% TeX-master: t |
|
35031 | 124 |
%%% End: |