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;
     1

     2 \chapter{Basic Concepts}\label{ch:basics}

     3

     4 Isabelle/Isar offers two main improvements over classic Isabelle:

     5 \begin{enumerate}

     6 \item A new \emph{theory format}, often referred to as new-style theories'',

     7   supporting interactive development and unlimited undo operation.

     8 \item A \emph{formal proof language} designed to support intelligible

     9   semi-automated reasoning.  Rather than putting together tactic scripts, the

    10   author is enabled to express the reasoning in way that is close to

    11   mathematical practice.

    12 \end{enumerate}

    13

    14 The Isar proof language is embedded into the new theory format as a proper

    15 sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or

    16 $\LEMMANAME$ at the theory levels, and left with the final end of proof (e.g.\

    17 via $\QEDNAME$).  Some theory extension mechanisms require proof as well, such

    18 as the HOL $\isarkeyword{typedef}$ mechanism that only works for non-empty

    19 representing sets.

    20

    21 New-style theory files may still be associated with an ML file consisting of

    22 plain old tactic scripts.  There is no longer any ML binding generated for the

    23 theory and theorems, though.  Functions \texttt{theory}, \texttt{thm}, and

    24 \texttt{thms} may be used to retrieve this information from ML (see also

    25 \cite{isabelle-ref}).  Nevertheless, migration between classic Isabelle and

    26 Isabelle/Isar is relatively easy.  Thus users may start to benefit from

    27 interactive theory development even before they have any idea of the Isar

    28 proof language.

    29

    30 \begin{warn}

    31   Proof~General does \emph{not} support mixed interactive development of

    32   classic Isabelle theory files and tactic scripts together with Isar

    33   documents at the same time.  The \texttt{isa} and \texttt{isar} versions of

    34   Proof~General appear as two different theorem proving systems; only one

    35   prover may be active at any time.

    36 \end{warn}

    37

    38

    39 \section{The Isar proof language}

    40

    41 This rather important section has not been written yet!  Refer to

    42 \cite{Wenzel:1999:TPHOL} for the time being.

    43

    44 \subsection{Commands}

    45

    46 \subsubsection{Isar primitives}

    47

    48 \subsubsection{Derived elements}

    49

    50

    51 \subsection{Methods}

    52

    53 \subsection{Attributes}

    54

    55

    56 %%% Local Variables:

    57 %%% mode: latex

    58 %%% TeX-master: "isar-ref"

    59 %%% End: