doc-src/IsarRef/basics.tex
author wenzelm
Thu Oct 21 17:42:21 1999 +0200 (1999-10-21)
changeset 7895 7c492d8bc8e3
parent 7466 7df66ce6508a
child 7981 5120a2a15d06
permissions -rw-r--r--
updated;
wenzelm@7046
     1
wenzelm@7297
     2
\chapter{Basic Concepts}\label{ch:basics}
wenzelm@7297
     3
wenzelm@7895
     4
\section{Isabelle/Isar theories}
wenzelm@7895
     5
wenzelm@7297
     6
Isabelle/Isar offers two main improvements over classic Isabelle:
wenzelm@7297
     7
\begin{enumerate}
wenzelm@7466
     8
\item A new \emph{theory format}, occasionally referred to as ``new-style
wenzelm@7895
     9
  theories'', supporting interactive development and unlimited undo operation.
wenzelm@7895
    10
\item A \emph{formal proof document language} designed to support intelligible
wenzelm@7895
    11
  semi-automated reasoning.  Instead of putting together unreadable tactic
wenzelm@7895
    12
  scripts, the author is enabled to express the reasoning in way that is close
wenzelm@7895
    13
  to mathematical practice.
wenzelm@7297
    14
\end{enumerate}
wenzelm@7046
    15
wenzelm@7297
    16
The Isar proof language is embedded into the new theory format as a proper
wenzelm@7297
    17
sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
wenzelm@7895
    18
$\LEMMANAME$ at the theory level, and left again with the final conclusion
wenzelm@7895
    19
(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
wenzelm@7466
    20
well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
wenzelm@7466
    21
the representing sets.
wenzelm@7297
    22
wenzelm@7297
    23
New-style theory files may still be associated with an ML file consisting of
wenzelm@7315
    24
plain old tactic scripts.  There is no longer any ML binding generated for the
wenzelm@7466
    25
theory and theorems, though.  ML functions \texttt{theory}, \texttt{thm}, and
wenzelm@7466
    26
\texttt{thms} retrieve this information \cite{isabelle-ref}.  Nevertheless,
wenzelm@7466
    27
migration between classic Isabelle and Isabelle/Isar is relatively easy.  Thus
wenzelm@7466
    28
users may start to benefit from interactive theory development even before
wenzelm@7466
    29
they have any idea of the Isar proof language.
wenzelm@7315
    30
wenzelm@7315
    31
\begin{warn}
wenzelm@7466
    32
  Currently Proof~General does \emph{not} support mixed interactive
wenzelm@7895
    33
  development of classic Isabelle theory files and tactic scripts, together
wenzelm@7466
    34
  with Isar documents at the same time.  The ``\texttt{isa}'' and
wenzelm@7466
    35
  ``\texttt{isar}'' versions of Proof~General are handled as two different
wenzelm@7895
    36
  theorem proving systems, only one of these may be active.
wenzelm@7315
    37
\end{warn}
wenzelm@7297
    38
wenzelm@7466
    39
Porting of existing tactic scripts is best done by running two separate
wenzelm@7466
    40
Proof~General sessions, one for replaying the old script and the other for the
wenzelm@7466
    41
emerging Isabelle/Isar document.
wenzelm@7466
    42
wenzelm@7046
    43
wenzelm@7046
    44
\section{The Isar proof language}
wenzelm@7046
    45
wenzelm@7466
    46
Sorry, this important section has not been written yet!  Refer to
wenzelm@7297
    47
\cite{Wenzel:1999:TPHOL} for the time being.
wenzelm@7297
    48
wenzelm@7297
    49
\subsection{Commands}
wenzelm@7297
    50
wenzelm@7297
    51
\subsubsection{Isar primitives}
wenzelm@7297
    52
wenzelm@7297
    53
\subsubsection{Derived elements}
wenzelm@7297
    54
wenzelm@7135
    55
wenzelm@7135
    56
\subsection{Methods}
wenzelm@7046
    57
wenzelm@7046
    58
\subsection{Attributes}
wenzelm@7046
    59
wenzelm@7046
    60
%%% Local Variables: 
wenzelm@7046
    61
%%% mode: latex
wenzelm@7046
    62
%%% TeX-master: "isar-ref"
wenzelm@7046
    63
%%% End: