doc-src/IsarRef/basics.tex
author wenzelm
Sun Aug 22 21:13:20 1999 +0200 (1999-08-22)
changeset 7315 76a39a3784b5
parent 7297 c1eeeadbe80a
child 7335 abba35b98892
permissions -rw-r--r--
checkpoint;
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@7315
    16
$\LEMMANAME$ at the theory levels, 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@7315
    18
as the HOL $\isarkeyword{typedef}$ mechanism that only works for non-empty
wenzelm@7315
    19
representing 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@7315
    24
\texttt{thms} may be used to retrieve this information from ML (see also
wenzelm@7315
    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@7315
    33
  documents at the same time.  The \texttt{isa} and \texttt{isar} versions of
wenzelm@7315
    34
  Proof~General appear as two different theorem proving systems; only one
wenzelm@7315
    35
  prover may be active at any time.
wenzelm@7315
    36
\end{warn}
wenzelm@7297
    37
wenzelm@7046
    38
wenzelm@7046
    39
\section{The Isar proof language}
wenzelm@7046
    40
wenzelm@7297
    41
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: