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