doc-src/IsarRef/conversion.tex
author wenzelm
Thu, 28 Sep 2000 19:07:09 +0200
changeset 10111 78a0397eaec1
parent 9846 bb848beb53f6
child 10153 482899aff303
permissions -rw-r--r--
some preliminary stuff on conversion;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
     1
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
     2
\chapter{The Isabelle/Isar Conversion Guide}
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
     3
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
     4
Subsequently, we give a few practical hints on working in a mixed environment
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
     5
with old Isabelle ML proof scripts and new Isabelle/Isar theories.  There are
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
     6
basically three ways to cope with this issue.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
     7
\begin{enumerate}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
     8
\item Do not convert old sources at all, but communicate directly at the level
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
     9
  of internal theory and theorem values.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    10
\item Manually port old-style theory files to new-style ones (very easy), and
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    11
  ML proof scripts to Isar tactic emulation scripts (quite easy).
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    12
\item Actually redo ML proof scripts as human readable Isar proof texts
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    13
  (probably hard, depending who wrote the original scripts).
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    14
\end{enumerate}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    15
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    16
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
    17
\section{No conversion}
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
    18
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    19
Internally, Isabelle handles both old and new-style theories at the same time;
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    20
the theory loader automatically detects the input format.  In any case, this
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    21
results in certain internal ML values of type \texttt{theory} and
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    22
\texttt{thm}.  These may be accessed from either the classic or Isar version,
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    23
provided that some minimal care is taken.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    24
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    25
\subsection{Referring to theorem and theory values}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    26
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    27
\begin{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    28
thm         : xstring -> thm
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    29
thms        : xstring -> thm list
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    30
the_context : unit -> theory
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    31
theory      : string -> theory
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    32
\end{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    33
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    34
These above functions provide general means to refer to logical objects from
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    35
ML.  While old-style theories used to emit many ML bindings to theorems (and
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    36
theories), this is no longer done for new-style Isabelle/Isar theories.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    37
Nevertheless, it is often more appropriate to use these explicit functions in
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    38
any case, even if referring to old theories.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    39
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    40
\begin{descr}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    41
\item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    42
  in the current theory context, including any ancestor node.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    43
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    44
  The convention of old-style theories was to bind any theorem as an ML value
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    45
  as well.  New-style theories no longer do this, so ML code may have to use
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    46
  \texttt{thm~"foo"} rather than just \texttt{foo}.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    47
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    48
\item [$\mathtt{the_context()}$] refers to the current theory context.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    49
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    50
  Old-style theories often use the ML binding \texttt{thy}, which is
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    51
  dynamically created as part of producing ML code out of the theory source.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    52
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    53
\item [$\mathtt{theory}~name$] retrieves the named theory from the global
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    54
  theory loader database.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    55
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    56
  The ML code generated from old style theories would include an ML binding
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    57
  $name\mathtt{.thy}$ as part of an ML structure.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    58
\end{descr}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    59
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    60
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    61
\subsection{Enabling new-style theories to retrieve theory values}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    62
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    63
\begin{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    64
qed        : string -> unit
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    65
bind_thm   : string * thm -> unit
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    66
bind_thms  : string * thm list -> unit
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    67
\end{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    68
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    69
ML proof scripts have to be well-behaved in storing theorems properly within
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    70
the current theory context, in order to enable new-style theories to retrieve
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    71
these these later.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    72
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    73
\begin{descr}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    74
\item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    75
  ML.  This already manages entry in the theorem database of the current
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    76
  theory context.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    77
\item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    78
  store theorems that are produced in ML in an ad-hoc manner.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    79
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    80
  Note that the original ``LCF'' system approach of binding theorem values on
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    81
  the ML toplevel only has long been given up in Isabelle.  Nevertheless,
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    82
  legacy proof scripts may occasionally contain ill-behaved code like this:
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    83
  \texttt{val foo = result();} So far, this form did not give any immediate
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    84
  feedback that there is something wrong, apart from theorems missing in the
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    85
  WWW presentation, for example.  Now it prevents such theorems to be referred
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    86
  from new-style theories.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    87
\end{descr}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    88
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    89
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    90
\subsection{Providing legacy ML bindings}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    91
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    92
\begin{matharray}{rcl}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    93
  \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    94
\end{matharray}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    95
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    96
New-style theories may provide ML bindings to accommodate legacy ML scripts as
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    97
follows.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    98
\[
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    99
\isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   100
\]
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   101
Note that this command cannot be undone; invalid theorem bindings in ML may
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   102
persist.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   103
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   104
By providing an old-style ML binding in the way that legacy proof scripts
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   105
usually expect, one may avoid to change all occurrences of a \texttt{foo}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   106
reference into \texttt{thm~"foo"}.
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   107
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   108
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   109
\section{Porting proof scripts}
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   110
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   111
Porting legacy theory and ML files to proper Isabelle/Isar theories has
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   112
several advantages.  For example, the Proof~General user interface
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   113
\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable than
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   114
the classic Isabelle version.  This is due to the fact that the generic ML
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   115
toplevel has been replaced by the new Isar interaction loop, with full control
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   116
over input synchronization and errors.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   117
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   118
Furthermore, the Isabelle document preparation system only properly with
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   119
new-style theories (see also \cite{isabelle-system}).  There is only very
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   120
basic document output of the plain sources of legacy theories, lacking
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   121
theorems and proof scripts.  Proper document markup is only available for
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   122
Isabelle/Isar theories.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   123
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   124
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   125
\subsection{Theory syntax}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   126
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   127
Basically, the new-style Isabelle/Isar theory syntax is a proper superset of
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   128
the old one.  Only a few quirks and legacy problems have been eliminated,
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   129
resulting in simpler rules with less exceptions.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   130
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   131
\medskip The main differences in the new syntax are as follows.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   132
\begin{itemize}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   133
\item Types and terms have to be \emph{atomic} as far as the theory syntax is
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   134
  concerned; this usually requires proper quoting of input strings.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   135
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   136
  The old theory syntax used to fake part of the syntax of types in order to
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   137
  require less quoting.  This has caused too many strange effects and is no
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   138
  longer supported.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   139
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   140
  Note that quotes are \emph{not} required for simple atomic terms, such as
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   141
  plain identifiers (e.g.\ $x$), numerals (e.g.\ $1$), or non-ASCII symbols
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   142
  (e.g.\ $\forall$, which is input as \verb,\<forall>,).
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   143
\item Every name may be quoted, if required.  The old syntax would
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   144
  occasionally demand plain identifiers vs.\ quoted strings to accommodate
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   145
  certain (discontinued) syntactic features.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   146
\item Theorem declarations now require an explicit colon to separate the name
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   147
  and the statement (e.g.\ see the syntax of $\DEFS$ in \S\ref{sec:consts}, or
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   148
  $\THEOREMNAME$ in \S\ref{sec:axms-thms}).
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   149
\end{itemize}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   150
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   151
Isabelle/Isar error messages are usually quite explicit about the problem, so
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   152
doubtful cases of syntax may as well just tried interactively.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   153
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   154
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   155
\subsection{Basic goal statements}\label{sec:conv-goal}
9798
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   156
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   157
In ML scripts, the canonical a goal statement with completed proof script is
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   158
as follows.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   159
\begin{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   160
Goal "\(\phi\)";
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   161
  by \(tac@1\);
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   162
  \(\vdots\);
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   163
  by \(tac@n\);
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   164
qed "\(name\)";
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   165
\end{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   166
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   167
This form may be turned into an Isar tactic emulation script like this:
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   168
\begin{matharray}{l}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   169
\LEMMA{name}\texttt"{\phi}\texttt" \\
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   170
\quad \isarkeyword{apply}~meth@1 \\
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   171
\quad \vdots \\
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   172
\quad \isarkeyword{apply}~meth@n \\
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   173
\quad \isarkeyword{done} \\
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   174
\end{matharray}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   175
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   176
The main statement may be $\THEOREMNAME$ as well.  See \S\ref{sec:conv-tac}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   177
for further details on how to convert actual tactic expressions into proof
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   178
methods.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   179
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   180
\medskip Classic Isabelle provides many variant forms of goal commands, see
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   181
\cite{isabelle-ref} for further details.  The second most common one is
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   182
\texttt{Goalw}, which expands definitions before commencing the actual proof
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   183
script.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   184
\begin{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   185
Goalw [defs] "\(\phi\)";
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   186
  \(\vdots\)
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   187
\end{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   188
This may be replaced by an explicit invocation of the $unfold$ proof method.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   189
\begin{matharray}{l}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   190
\LEMMA{name}\texttt"{\phi}\texttt" \\
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   191
\quad \isarkeyword{apply}~(unfold~defs) \\
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   192
\quad \vdots \\
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   193
\end{matharray}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   194
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   195
%FIXME "goal" and higher-order rules;
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   196
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   197
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   198
\subsection{Tactics vs.\ proof methods}\label{sec:conv-tac}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   199
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   200
Proof methods closely resemble traditional tactics, when used in unstructured
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   201
sequences of $\isarkeyword{apply}$ commands (cf.\ \S\ref{sec:conv-goal}).
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   202
Unlike tactics, proof methods provide proper concrete syntax for additional
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   203
arguments, options, and modifiers.  Thus a typical method text is usually more
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   204
concise than the corresponding tactic expression in ML.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   205
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   206
Well-structured Isar proof texts usually demand much less diverse methods than
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   207
traditional proof scripts, so basically a few methods would be sufficient.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   208
Isabelle/Isar provides emulations for any major ML tactic of classic Isabelle,
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   209
mostly for the sake of easy porting of existing developments.  Nevertheless,
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   210
the Isar versions often cover several old-style tactics by a single method.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   211
For example, $simp$ replaces all of \texttt{simp_tac}~/
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   212
\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac},
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   213
including concrete syntax for augmenting the Simplifier context (the current
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   214
``simpset'').
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   215
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   216
\bigskip
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   217
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   218
FIXME
9798
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   219
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   220
\begin{matharray}{llll}
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   221
  \texttt{rtac}~a~1 & & rule~a \\
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   222
  \texttt{resolve_tac}~[a@1, \dots, a@n]~1 & & rule~a@1~\dots~a@n \\
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   223
  \texttt{res_inst_tac}~[(x@1, t@1), \dots, (x@n, t@n)]~a~1 & &
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   224
  rule_tac~x@1 = t@1~\dots~x@n = t@n~\textrm{in}~a \\
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   225
  
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   226
%  \texttt{} & & \\
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   227
  \texttt{stac}~a~1 & & subst~a \\
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   228
  \texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\
9846
wenzelm
parents: 9819
diff changeset
   229
  \texttt{split_all_tac} & & simp~(no_asm_simp)~only:~split_tupled_all & \Text{(HOL)} \\
wenzelm
parents: 9819
diff changeset
   230
                         & \approx & simp~only:~split_tupled_all & \Text{(HOL)} \\
9819
wenzelm
parents: 9798
diff changeset
   231
                         & \ll & clarify & \Text{(HOL)} \\
9798
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   232
\end{matharray}
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   233
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   234
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   235
\subsection{Declarations and ad-hoc operations}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   236
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   237
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   238
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   239
%\section{Performing actual proof}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   240
%FIXME
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   241
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   242
%%% Local Variables: 
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   243
%%% mode: latex
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   244
%%% TeX-master: "isar-ref"
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   245
%%% End: