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