doc-src/IsarImplementation/implementation.tex
author huffman
Thu Apr 19 10:49:47 2012 +0200 (2012-04-19)
changeset 47579 28f6f4ad69bf
parent 46295 2548a85b0e02
permissions -rw-r--r--
tuned lemmas (v)image_id;
removed duplicate of vimage_id
wenzelm@18537
     1
\documentclass[12pt,a4paper,fleqn]{report}
wenzelm@18537
     2
\usepackage{latexsym,graphicx}
wenzelm@18537
     3
\usepackage[refpage]{nomencl}
wenzelm@18537
     4
\usepackage{../iman,../extra,../isar,../proof}
wenzelm@26862
     5
\usepackage[nohyphen,strings]{../underscore}
wenzelm@42632
     6
\usepackage{../../lib/texinputs/isabelle}
wenzelm@42632
     7
\usepackage{../../lib/texinputs/isabellesym}
wenzelm@42632
     8
\usepackage{../../lib/texinputs/railsetup}
wenzelm@42632
     9
\usepackage{../ttbox}
wenzelm@18537
    10
\usepackage{style}
wenzelm@18537
    11
\usepackage{../pdfsetup}
wenzelm@18537
    12
wenzelm@18537
    13
wenzelm@18537
    14
\hyphenation{Isabelle}
wenzelm@18537
    15
\hyphenation{Isar}
wenzelm@18537
    16
wenzelm@18537
    17
\isadroptag{theory}
wenzelm@18537
    18
\title{\includegraphics[scale=0.5]{isabelle_isar}
wenzelm@18537
    19
  \\[4ex] The Isabelle/Isar Implementation}
wenzelm@28780
    20
\author{\emph{Makarius Wenzel}  \\[3ex]
wenzelm@28780
    21
  With Contributions by
wenzelm@28780
    22
  Florian Haftmann
wenzelm@28780
    23
  and Larry Paulson
wenzelm@28780
    24
}
wenzelm@18537
    25
wenzelm@18537
    26
\makeindex
wenzelm@18537
    27
wenzelm@18537
    28
wenzelm@18537
    29
\begin{document}
wenzelm@18537
    30
wenzelm@35031
    31
\maketitle
wenzelm@18537
    32
wenzelm@18537
    33
\begin{abstract}
wenzelm@18537
    34
  We describe the key concepts underlying the Isabelle/Isar
wenzelm@18537
    35
  implementation, including ML references for the most important
wenzelm@20451
    36
  functions.  The aim is to give some insight into the overall system
wenzelm@20488
    37
  architecture, and provide clues on implementing applications within
wenzelm@20488
    38
  this framework.
wenzelm@18537
    39
\end{abstract}
wenzelm@18537
    40
wenzelm@19189
    41
\vspace*{2.5cm}
wenzelm@19189
    42
\begin{quote}
wenzelm@35031
    43
wenzelm@19189
    44
  {\small\em Isabelle was not designed; it evolved.  Not everyone
wenzelm@19189
    45
    likes this idea.  Specification experts rightly abhor
wenzelm@19189
    46
    trial-and-error programming.  They suggest that no one should
wenzelm@20024
    47
    write a program without first writing a complete formal
wenzelm@19189
    48
    specification. But university departments are not software houses.
wenzelm@19189
    49
    Programs like Isabelle are not products: when they have served
wenzelm@19189
    50
    their purpose, they are discarded.}
wenzelm@35031
    51
wenzelm@19189
    52
  Lawrence C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
wenzelm@19189
    53
wenzelm@19189
    54
  \vspace*{1cm}
wenzelm@35031
    55
wenzelm@19189
    56
  {\small\em As I did 20 years ago, I still fervently believe that the
wenzelm@19189
    57
    only way to make software secure, reliable, and fast is to make it
wenzelm@20064
    58
    small.  Fight features.}
wenzelm@35031
    59
wenzelm@19189
    60
  Andrew S. Tanenbaum
wenzelm@19189
    61
wenzelm@35031
    62
  \vspace*{1cm}
wenzelm@35031
    63
wenzelm@35031
    64
  {\small\em One thing that UNIX does not need is more features. It is
wenzelm@35031
    65
    successful in part because it has a small number of good ideas
wenzelm@35031
    66
    that work well together. Merely adding features does not make it
wenzelm@35031
    67
    easier for users to do things --- it just makes the manual
wenzelm@35031
    68
    thicker. The right solution in the right place is always more
wenzelm@35031
    69
    effective than haphazard hacking.}
wenzelm@35031
    70
wenzelm@35031
    71
  Rob Pike and Brian W. Kernighan
wenzelm@35031
    72
wenzelm@19189
    73
\end{quote}
wenzelm@19189
    74
wenzelm@19189
    75
\thispagestyle{empty}\clearpage
wenzelm@19189
    76
wenzelm@20514
    77
\pagenumbering{roman}
wenzelm@20514
    78
\tableofcontents
wenzelm@20514
    79
\listoffigures
wenzelm@20514
    80
\clearfirst
wenzelm@18537
    81
wenzelm@39822
    82
\setcounter{chapter}{-1}
wenzelm@39822
    83
wenzelm@39822
    84
\input{Thy/document/ML.tex}
wenzelm@29755
    85
\input{Thy/document/Prelim.tex}
wenzelm@29755
    86
\input{Thy/document/Logic.tex}
wenzelm@39852
    87
\input{Thy/document/Syntax.tex}
wenzelm@29755
    88
\input{Thy/document/Tactic.tex}
wenzelm@46295
    89
\input{Thy/document/Eq.tex}
wenzelm@29755
    90
\input{Thy/document/Proof.tex}
wenzelm@29755
    91
\input{Thy/document/Isar.tex}
wenzelm@29755
    92
\input{Thy/document/Local_Theory.tex}
wenzelm@29755
    93
\input{Thy/document/Integration.tex}
wenzelm@18537
    94
wenzelm@18537
    95
\begingroup
wenzelm@18537
    96
\tocentry{\bibname}
wenzelm@30116
    97
\bibliographystyle{abbrv} \small\raggedright\frenchspacing
wenzelm@18537
    98
\bibliography{../manual}
wenzelm@18537
    99
\endgroup
wenzelm@18537
   100
wenzelm@18537
   101
\tocentry{\indexname}
wenzelm@18537
   102
\printindex
wenzelm@18537
   103
wenzelm@18537
   104
\end{document}
wenzelm@18537
   105
wenzelm@18537
   106
wenzelm@35031
   107
%%% Local Variables:
wenzelm@18537
   108
%%% mode: latex
wenzelm@18537
   109
%%% TeX-master: t
wenzelm@35031
   110
%%% End: