doc-src/IsarRef/conversion.tex
author wenzelm
Sun, 15 Oct 2000 19:51:56 +0200
changeset 10223 31346d22bb54
parent 10160 bb8f9412fec6
child 10239 979336bd0aed
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
     1
10160
wenzelm
parents: 10153
diff changeset
     2
\chapter{Isabelle/Isar Conversion Guide}\label{ap:conv}
9607
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
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
     5
of old Isabelle ML proof scripts and new Isabelle/Isar theories.  There are
10111
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
10160
wenzelm
parents: 10153
diff changeset
     9
  of \emph{internal} theory and theorem values.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    10
\item Port old-style theory files to new-style ones (very easy), and ML proof
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    11
  scripts to Isar tactic-emulation scripts (quite easy).
10160
wenzelm
parents: 10153
diff changeset
    12
\item Actually redo ML proof scripts as human-readable Isar proof texts
10111
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
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    19
Internally, Isabelle is able to handle both old and new-style theories at the
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    20
same time; the theory loader automatically detects the input format.  In any
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    21
case, the results are certain internal ML values of type \texttt{theory} and
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    22
\texttt{thm}.  These may be accessed from either classic Isabelle or
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    23
Isabelle/Isar, provided that some minimal precautions are observed.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    24
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    25
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    26
\subsection{Referring to theorem and theory values}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    27
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    28
\begin{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    29
thm         : xstring -> thm
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    30
thms        : xstring -> thm list
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    31
the_context : unit -> theory
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    32
theory      : string -> theory
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    33
\end{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    34
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    35
These functions provide general means to refer to logical objects from ML.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    36
Old-style theories used to emit many ML bindings of theorems and theories, but
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    37
this is no longer done in new-style Isabelle/Isar theories.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    38
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    39
\begin{descr}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    40
\item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    41
  in the current theory context, including any ancestor node.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    42
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    43
  The convention of old-style theories was to bind any theorem as an ML value
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    44
  as well.  New-style theories no longer do this, so ML code may require
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    45
  \texttt{thm~"foo"} rather than just \texttt{foo}.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    46
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    47
\item [$\mathtt{the_context()}$] refers to the current theory context.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    48
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    49
  Old-style theories often use the ML binding \texttt{thy}, which is
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    50
  dynamically created by the ML code generated from old theory source.  This
10160
wenzelm
parents: 10153
diff changeset
    51
  is no longer the recommended way in any case!  Function \texttt{the_context}
wenzelm
parents: 10153
diff changeset
    52
  should be used for old scripts as well.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    53
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    54
\item [$\mathtt{theory}~name$] retrieves the named theory from the global
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    55
  theory-loader database.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    56
  
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    57
  The ML code generated from old-style theories would include an ML binding
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    58
  $name\mathtt{.thy}$ as part of an ML structure.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    59
\end{descr}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    60
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    61
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    62
\subsection{Storing theorem values}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    63
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    64
\begin{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    65
qed        : string -> unit
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    66
bind_thm   : string * thm -> unit
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    67
bind_thms  : string * thm list -> unit
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    68
\end{ttbox}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    69
10160
wenzelm
parents: 10153
diff changeset
    70
ML proof scripts have to be well-behaved by storing theorems properly within
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    71
the current theory context, in order to enable new-style theories to retrieve
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    72
these these later.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    73
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    74
\begin{descr}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    75
\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
    76
  ML.  This already manages entry in the theorem database of the current
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    77
  theory context.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    78
\item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
10160
wenzelm
parents: 10153
diff changeset
    79
  store theorems that have been produced in ML in an ad-hoc manner.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    80
\end{descr}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    81
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    82
Note that the original ``LCF-system'' approach of binding theorem values on
10160
wenzelm
parents: 10153
diff changeset
    83
the ML toplevel only has long been given up in Isabelle!  Despite of this, old
wenzelm
parents: 10153
diff changeset
    84
legacy proof scripts occasionally contain code such as \texttt{val foo =
wenzelm
parents: 10153
diff changeset
    85
  result();} which is ill-behaved in several respects.  Apart from preventing
wenzelm
parents: 10153
diff changeset
    86
access from Isar theories, it also omits the result from the WWW presentation,
wenzelm
parents: 10153
diff changeset
    87
for example.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    88
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    89
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    90
\subsection{ML declarations in Isar}
10111
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} \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    94
  \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    95
\end{matharray}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    96
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    97
Isabelle/Isar theories may contain ML declarations as well.  For example, an
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    98
old-style theorem binding may be mimicked as follows.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    99
\[
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   100
\isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   101
\]
10160
wenzelm
parents: 10153
diff changeset
   102
Note that this command cannot be undone, so invalid theorem bindings in ML may
wenzelm
parents: 10153
diff changeset
   103
persist.  Also note that the current theory may not be modified; use
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   104
$\isarkeyword{ML_setup}$ for declarations that act on the current context.
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   105
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   106
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   107
\section{Porting theories and proof scripts}\label{sec:port-scripts}
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   108
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   109
Porting legacy theory and ML files to proper Isabelle/Isar theories has
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   110
several advantages.  For example, the Proof~General user interface
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   111
\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable to
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   112
use than the version for classic Isabelle.  This is due to the fact that the
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   113
generic ML toplevel has been replaced by a separate Isar interaction loop,
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   114
with full control over input synchronization and error conditions.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   115
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   116
Furthermore, the Isabelle document preparation system (see also
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   117
\cite{isabelle-sys}) only works properly with new-style theories.  Output of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   118
old-style sources is at the level of individual characters (and symbols),
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   119
without proper document markup as in Isabelle/Isar theories.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   120
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   121
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   122
\subsection{Theories}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   123
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   124
Basically, the Isabelle/Isar theory syntax is a proper superset of the classic
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   125
one.  Only a few quirks and legacy problems have been eliminated, resulting in
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   126
simpler rules and less special cases.  The main changes of theory syntax are
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   127
as follows.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   128
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   129
\begin{itemize}
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   130
\item Quoted strings may contain arbitrary white space, and span several lines
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   131
  without requiring \verb,\,\,\dots\verb,\, escapes.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   132
\item Names may always be quoted.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   133
  
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   134
  The old syntax would occasionally demand plain identifiers vs.\ quoted
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   135
  strings to accommodate certain syntactic features.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   136
\item Types and terms have to be \emph{atomic} as far as the theory syntax is
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   137
  concerned; this typically requires quoting of input strings, e.g.\ ``$x +
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   138
  y$''.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   139
  
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   140
  The old theory syntax used to fake part of the syntax of types in order to
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   141
  require less quoting in common cases; this was hard to predict, though.  On
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   142
  the other hand, Isar does not require quotes for simple terms, such as plain
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   143
  identifiers $x$, numerals $1$, or symbols $\forall$ (input as
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   144
  \verb,\<forall>,).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   145
\item Theorem declarations require an explicit colon to separate the name from
10160
wenzelm
parents: 10153
diff changeset
   146
  the statement (the name is usually optional).  Cf.\ the syntax of $\DEFS$ in
wenzelm
parents: 10153
diff changeset
   147
  \S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   148
\end{itemize}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   149
10160
wenzelm
parents: 10153
diff changeset
   150
Note that Isabelle/Isar error messages are usually quite explicit about the
wenzelm
parents: 10153
diff changeset
   151
problem at hand.  So in cases of doubt, input syntax may be just as well tried
wenzelm
parents: 10153
diff changeset
   152
out interactively.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   153
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   154
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   155
\subsection{Goal statements}\label{sec:conv-goal}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   156
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   157
In ML the canonical a goal statement together with a complete proof script is
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   158
as follows:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   159
\begin{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   160
 Goal "\(\phi\)";
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   161
 by \(tac@1\);
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   162
   \(\vdots\)
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   163
 qed "\(name\)";
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   164
\end{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   165
This form may be turned into an Isar tactic-emulation script like this:
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   166
\begin{matharray}{l}
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   167
  \LEMMA{name}\texttt"{\phi}\texttt" \\
10223
wenzelm
parents: 10160
diff changeset
   168
  \quad \APPLY{meth@1} \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   169
  \qquad \vdots \\
10223
wenzelm
parents: 10160
diff changeset
   170
  \quad \DONE \\
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   171
\end{matharray}
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   172
Note that the main statement may be $\THEOREMNAME$ as well.  See
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   173
\S\ref{sec:conv-tac} for further details on how to convert actual tactic
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   174
expressions into proof methods.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   175
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   176
\medskip Classic Isabelle provides many variant forms of goal commands, see
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   177
\cite{isabelle-ref} for further details.  The second most common one is
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   178
\texttt{Goalw}, which expands definitions before commencing the actual proof
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   179
script.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   180
\begin{ttbox}
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   181
 Goalw [\(def@1\), \(\dots\)] "\(\phi\)";
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   182
\end{ttbox}
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   183
This is replaced by using the $unfold$ proof method explicitly.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   184
\begin{matharray}{l}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   185
\LEMMA{name}\texttt"{\phi}\texttt" \\
10223
wenzelm
parents: 10160
diff changeset
   186
\quad \APPLY{unfold~def@1~\dots} \\
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   187
\end{matharray}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   188
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   189
%FIXME "goal" and higher-order rules;
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   190
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   191
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   192
\subsection{Tactics}\label{sec:conv-tac}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   193
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   194
Isar Proof methods closely resemble traditional tactics, when used in
10223
wenzelm
parents: 10160
diff changeset
   195
unstructured sequences of $\APPLYNAME$ commands (cf.\ \S\ref{sec:conv-goal}).
wenzelm
parents: 10160
diff changeset
   196
Isabelle/Isar provides emulations for all major ML tactics of classic Isabelle
wenzelm
parents: 10160
diff changeset
   197
--- mostly for the sake of easy porting of existing developments, as actual
wenzelm
parents: 10160
diff changeset
   198
Isar proof texts would demand much less diversity of proof methods.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   199
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   200
Unlike tactic expressions in ML, Isar proof methods provide proper concrete
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   201
syntax for additional arguments, options, modifiers etc.  Thus a typical
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   202
method text is usually more concise than the corresponding ML tactic.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   203
Furthermore, the Isar versions of classic Isabelle tactics often cover several
10160
wenzelm
parents: 10153
diff changeset
   204
variant forms by a single method with separate options to tune the behavior.
wenzelm
parents: 10153
diff changeset
   205
For example, method $simp$ replaces all of \texttt{simp_tac}~/
wenzelm
parents: 10153
diff changeset
   206
\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac},
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   207
there is also concrete syntax for augmenting the Simplifier context (the
10160
wenzelm
parents: 10153
diff changeset
   208
current ``simpset'') in a handsome way.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   209
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   210
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   211
\subsubsection{Resolution tactics}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   212
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   213
Classic Isabelle provides several variant forms of tactics for single-step
10160
wenzelm
parents: 10153
diff changeset
   214
rule applications (based on higher-order resolution).  The space of resolution
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   215
tactics has the following main dimensions.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   216
\begin{enumerate}
10160
wenzelm
parents: 10153
diff changeset
   217
\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\ 
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   218
  \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   219
  \texttt{forward_tac}).
10160
wenzelm
parents: 10153
diff changeset
   220
\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\ 
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   221
  \texttt{res_inst_tac}).
10160
wenzelm
parents: 10153
diff changeset
   222
\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\ 
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   223
  \texttt{rtac}).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   224
\end{enumerate}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   225
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   226
Basically, the set of Isar tactic emulations $rule_tac$, $erule_tac$,
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   227
$drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   228
cover the four modes, either with or without instantiation, and either with
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   229
single or multiple arguments.  Although it is more convenient in most cases to
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   230
use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   231
``improper'' variants $erule$, $drule$, $frule$ (see
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   232
\S\ref{sec:misc-methods}).  Note that explicit goal addressing is only
10160
wenzelm
parents: 10153
diff changeset
   233
supported by the actual $rule_tac$ version.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   234
10160
wenzelm
parents: 10153
diff changeset
   235
With this in mind, plain resolution tactics may be ported as follows.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   236
\begin{matharray}{lll}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   237
  \texttt{rtac}~a~1 & & rule~a \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   238
  \texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   239
  \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~1 & &
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   240
  rule_tac~x@1 = t@1~and~\dots~in~a \\[0.5ex]
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   241
  \texttt{rtac}~a~i & & rule_tac~[i]~a \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   242
  \texttt{resolve_tac}~[a@1, \dots]~i & & rule_tac~[i]~a@1~\dots \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   243
  \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~i & &
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   244
  rule_tac~[i]~x@1 = t@1~and~\dots~in~a \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   245
\end{matharray}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   246
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   247
Note that explicit goal addressing may be usually avoided by changing the
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   248
order of subgoals with $\isarkeyword{defer}$ or $\isarkeyword{prefer}$ (see
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   249
\S\ref{sec:tactic-commands}).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   250
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   251
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   252
\subsubsection{Simplifier tactics}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   253
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   254
The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   255
(cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   256
methods (see \S\ref{sec:simp}).  Note that there is no individual goal
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   257
addressing available, simplification acts either on the first goal ($simp$)
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   258
or all goals ($simp_all$).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   259
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   260
\begin{matharray}{lll}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   261
  \texttt{Asm_full_simp_tac 1} & & simp \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   262
  \texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex]
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   263
  \texttt{Simp_tac 1} & & simp~(no_asm) \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   264
  \texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   265
  \texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   266
\end{matharray}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   267
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   268
Isar also provides separate method modifier syntax for augmenting the
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   269
Simplifier context (see \S\ref{sec:simp}), which is known as the ``simpset''
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   270
in ML.  A typical ML expression with simpset changes looks like this:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   271
\begin{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   272
asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   273
\end{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   274
The corresponding Isar text is as follows:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   275
\[
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   276
simp~add:~a@1~\dots~del:~b@1~\dots
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   277
\]
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   278
Global declarations of Simplifier rules (e.g.\ \texttt{Addsimps}) are covered
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   279
by application of attributes, see \S\ref{sec:conv-decls} for more information.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   280
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   281
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   282
\subsubsection{Classical Reasoner tactics}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   283
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   284
The Classical Reasoner provides a rather large number of variations of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   285
automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   286
\texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}).  The corresponding Isar
10160
wenzelm
parents: 10153
diff changeset
   287
methods usually share the same base name, such as $blast$, $fast$, $clarify$
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   288
etc.\ (see \S\ref{sec:classical-auto}).
9798
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   289
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   290
Similar to the Simplifier, there is separate method modifier syntax for
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   291
augmenting the Classical Reasoner context, which is known as the ``claset'' in
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   292
ML.  A typical ML expression with claset changes looks like this:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   293
\begin{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   294
blast_tac (claset () addIs [\(a@1\), \(\dots\)] addSEs [\(b@1\), \(\dots\)]) 1
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   295
\end{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   296
The corresponding Isar text is as follows:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   297
\[
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   298
blast~intro:~a@1~\dots~elim!:~b@1~\dots
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   299
\]
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   300
Global declarations of Classical Reasoner rules (e.g.\ \texttt{AddIs}) are
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   301
covered by application of attributes, see \S\ref{sec:conv-decls} for more
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   302
information.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   303
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   304
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   305
\subsubsection{Miscellaneous tactics}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   306
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   307
There are a few additional tactics defined in various theories of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   308
Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF.  The most
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   309
common ones of these may be ported to Isar as follows.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   310
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   311
\begin{matharray}{lll}
9798
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   312
  \texttt{stac}~a~1 & & subst~a \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   313
  \texttt{hyp_subst_tac}~1 & & hypsubst \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   314
  \texttt{strip_tac}~1 & \approx & intro~strip \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   315
  \texttt{split_all_tac}~1 & & simp~(no_asm_simp)~only:~split_tupled_all \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   316
                         & \approx & simp~only:~split_tupled_all \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   317
                         & \ll & clarify \\
9798
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   318
\end{matharray}
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   319
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   320
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   321
\subsubsection{Tacticals}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   322
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   323
Classic Isabelle provides a huge amount of tacticals for combination and
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   324
modification of existing tactics.  This has been greatly reduced in Isar,
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   325
providing the bare minimum of combinators only: ``$,$'' (sequential
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   326
composition), ``$|$'' (alternative choices), ``$?$'' (try), ``$+$'' (repeat at
10160
wenzelm
parents: 10153
diff changeset
   327
least once).  These are usually sufficient in practice; if all fails,
wenzelm
parents: 10153
diff changeset
   328
arbitrary ML tactic code may be invoked via the $tactic$ method (see
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   329
\S\ref{sec:tactics}).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   330
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   331
\medskip Common ML tacticals may be expressed directly in Isar as follows:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   332
\begin{matharray}{lll}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   333
tac@1~\texttt{THEN}~tac@2 & & meth@1, meth@2 \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   334
tac@1~\texttt{ORELSE}~tac@2 & & meth@1~|~meth@2 \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   335
\texttt{TRY}~tac & & meth? \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   336
\texttt{REPEAT1}~tac & & meth+ \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   337
\texttt{REPEAT}~tac & & (meth+)? \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   338
\texttt{EVERY}~[tac@1, \dots] & & meth@1, \dots \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   339
\texttt{FIRST}~[tac@1, \dots] & & meth@1~|~\dots \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   340
\end{matharray}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   341
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   342
\medskip \texttt{CHANGED} (see \cite{isabelle-ref}) is usually not required in
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   343
Isar, since most basic proof methods already fail unless there is an actual
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   344
change in the goal state.  Nevertheless, ``$?$'' (try) may be used to accept
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   345
\emph{unchanged} results as well.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   346
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   347
\medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref})
10160
wenzelm
parents: 10153
diff changeset
   348
are not available in Isar, since there is no direct goal addressing.
wenzelm
parents: 10153
diff changeset
   349
Nevertheless, some basic methods address all goals internally, notably
wenzelm
parents: 10153
diff changeset
   350
$simp_all$ (see \S\ref{sec:simp}).  Also note that \texttt{ALLGOALS} may be
wenzelm
parents: 10153
diff changeset
   351
often replaced by ``$+$'' (repeat at least once), although this usually has a
wenzelm
parents: 10153
diff changeset
   352
different operational behavior, such as solving goals in a different order.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   353
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   354
\medskip Iterated resolution, such as
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   355
\texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   356
using the $intro$ and $elim$ methods of Isar (see
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   357
\S\ref{sec:classical-basic}).
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   358
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   359
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   360
\subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   361
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   362
Apart from proof commands and tactic expressions, almost all of the remaining
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   363
ML code occurring in legacy proof scripts are either global context
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   364
declarations (such as \texttt{Addsimps}) or ad-hoc operations on theorems
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   365
(such as \texttt{RS}).  In Isar both of these are covered by theorem
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   366
expressions with \emph{attributes}.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   367
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   368
\medskip Theorem operations may be attached as attributes in the very place
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   369
where theorems are referenced, say within a method argument.  The subsequent
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   370
common ML combinators may be expressed directly in Isar as follows.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   371
\begin{matharray}{lll}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   372
  thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\
10160
wenzelm
parents: 10153
diff changeset
   373
  thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   374
  thm@1~\texttt{COMP}~thm@2 & & thm@1~[COMP~thm@2] \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   375
  \relax[thm@1, \dots]~\texttt{MRS}~thm & & thm~[OF~thm@1~\dots] \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   376
  \texttt{read_instantiate}~[(x@1, t@1), \dots]~thm & & thm~[where~x@1 = t@1~and~\dots] \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   377
  \texttt{standard}~thm & & thm~[standard] \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   378
  \texttt{make_elim}~thm & & thm~[elim_format] \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   379
\end{matharray}
10160
wenzelm
parents: 10153
diff changeset
   380
wenzelm
parents: 10153
diff changeset
   381
Note that $OF$ is often more readable as $THEN$; likewise positional
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   382
instantiation with $of$ is more handsome than $where$.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   383
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   384
The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be
10160
wenzelm
parents: 10153
diff changeset
   385
replaced by passing the result of a proof through $rule_format$.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   386
10223
wenzelm
parents: 10160
diff changeset
   387
\medskip Global ML declarations may be expressed using the $\DECLARE$ command
wenzelm
parents: 10160
diff changeset
   388
(see \S\ref{sec:tactic-commands}) together with appropriate attributes.  The
wenzelm
parents: 10160
diff changeset
   389
most common ones are as follows.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   390
\begin{matharray}{lll}
10223
wenzelm
parents: 10160
diff changeset
   391
  \texttt{Addsimps}~[thm] & & \DECLARE~thm~[simp] \\
wenzelm
parents: 10160
diff changeset
   392
  \texttt{Delsimps}~[thm] & & \DECLARE~thm~[simp~del] \\
wenzelm
parents: 10160
diff changeset
   393
  \texttt{Addsplits}~[thm] & & \DECLARE~thm~[split] \\
wenzelm
parents: 10160
diff changeset
   394
  \texttt{Delsplits}~[thm] & & \DECLARE~thm~[split~del] \\[0.5ex]
wenzelm
parents: 10160
diff changeset
   395
  \texttt{AddIs}~[thm] & & \DECLARE~thm~[intro] \\
wenzelm
parents: 10160
diff changeset
   396
  \texttt{AddEs}~[thm] & & \DECLARE~thm~[elim] \\
wenzelm
parents: 10160
diff changeset
   397
  \texttt{AddDs}~[thm] & & \DECLARE~thm~[dest] \\
wenzelm
parents: 10160
diff changeset
   398
  \texttt{AddSIs}~[thm] & & \DECLARE~thm~[intro!] \\
wenzelm
parents: 10160
diff changeset
   399
  \texttt{AddSEs}~[thm] & & \DECLARE~thm~[elim!] \\
wenzelm
parents: 10160
diff changeset
   400
  \texttt{AddSDs}~[thm] & & \DECLARE~thm~[dest!] \\[0.5ex]
wenzelm
parents: 10160
diff changeset
   401
  \texttt{AddIffs}~[thm] & & \DECLARE~thm~[iff] \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   402
\end{matharray}
10223
wenzelm
parents: 10160
diff changeset
   403
Note that explicit $\DECLARE$ commands are actually needed only very rarely;
wenzelm
parents: 10160
diff changeset
   404
Isar admits to declare theorems on-the-fly wherever they emerge.  Consider the
wenzelm
parents: 10160
diff changeset
   405
following ML idiom:
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   406
\begin{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   407
Goal "\(\phi\)";
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   408
 \(\vdots\)
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   409
qed "name";
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   410
Addsimps [name];
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   411
\end{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   412
This may be expressed more concisely in Isar like this:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   413
\begin{matharray}{l}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   414
  \LEMMA{name~[simp]}{\phi} \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   415
  \quad\vdots
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   416
\end{matharray}
10160
wenzelm
parents: 10153
diff changeset
   417
The $name$ may be even omitted, although this would make it difficult to
wenzelm
parents: 10153
diff changeset
   418
declare the theorem otherwise later (e.g.\ as $[simp~del]$).
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   419
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   420
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   421
\section{Converting to actual Isar proof texts}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   422
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   423
Porting legacy ML proof scripts into Isar tactic emulation scripts (see
10160
wenzelm
parents: 10153
diff changeset
   424
\S\ref{sec:port-scripts}) is mainly a technical issue, since the basic
wenzelm
parents: 10153
diff changeset
   425
representation of formal ``proof script'' is preserved.  In contrast,
wenzelm
parents: 10153
diff changeset
   426
converting existing Isabelle developments into actual human-readably Isar
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   427
proof texts is more involved, due to the fundamental change of the underlying
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   428
paradigm.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   429
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   430
This issue is comparable to that of converting programs written in a low-level
10160
wenzelm
parents: 10153
diff changeset
   431
programming languages (say Assembler) into higher-level ones (say Haskell).
wenzelm
parents: 10153
diff changeset
   432
In order to accomplish this, one needs a working knowledge of the target
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   433
language, as well an understanding of the \emph{original} idea of the piece of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   434
code expressed in the low-level language.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   435
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   436
As far as Isar proofs are concerned, it is usually much easier to re-use only
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   437
definitions and the main statements directly, while following the arrangement
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   438
of proof scripts only very loosely.  Ideally, one would also have some
10160
wenzelm
parents: 10153
diff changeset
   439
\emph{informal} proof outlines available for guidance as well.  In the worst
wenzelm
parents: 10153
diff changeset
   440
case, obscure proof scripts would have to be re-engineered by tracing forth
wenzelm
parents: 10153
diff changeset
   441
and backwards, and by educated guessing!
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   442
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   443
\medskip This is a possible schedule to embark on actual conversion of legacy
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   444
proof scripts into Isar proof texts.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   445
\begin{enumerate}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   446
\item Port ML scripts to Isar tactic emulation scripts (see
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   447
  \S\ref{sec:port-scripts}).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   448
\item Get sufficiently acquainted with Isabelle/Isar proof
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   449
  development.\footnote{As there is still no Isar tutorial around, it is best
10160
wenzelm
parents: 10153
diff changeset
   450
    to look at existing Isar examples, see also \S\ref{sec:isar-howto}.}
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   451
\item Recover the proof structure of a few important theorems.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   452
\item Rephrase the original intention of the course of reasoning in terms of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   453
  Isar proof language elements.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   454
\end{enumerate}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   455
10160
wenzelm
parents: 10153
diff changeset
   456
Certainly, rewriting formal reasoning in Isar requires much additional effort.
wenzelm
parents: 10153
diff changeset
   457
On the other hand, one gains a human-readable representation of
wenzelm
parents: 10153
diff changeset
   458
machine-checked formal proof.  Depending on the context of application, this
wenzelm
parents: 10153
diff changeset
   459
might be even indispensable to start with!
wenzelm
parents: 10153
diff changeset
   460
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   461
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   462
%%% Local Variables: 
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   463
%%% mode: latex
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   464
%%% TeX-master: "isar-ref"
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   465
%%% End: