doc-src/IsarRef/conversion.tex
author nipkow
Wed, 04 Aug 2004 11:25:08 +0200
changeset 15106 e8cef6993701
parent 13625 ca86e84ce200
permissions -rw-r--r--
aded comment
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
     1
13048
wenzelm
parents: 13042
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.
13048
wenzelm
parents: 13042
diff changeset
    42
10111
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}.
13048
wenzelm
parents: 13042
diff changeset
    46
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    47
\item [$\mathtt{the_context()}$] refers to the current theory context.
13048
wenzelm
parents: 13042
diff changeset
    48
10111
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.
13048
wenzelm
parents: 13042
diff changeset
    53
10111
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.
13048
wenzelm
parents: 13042
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
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
    72
these later.
10111
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}
13048
wenzelm
parents: 13042
diff changeset
    75
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    76
\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
    77
  ML.  This already manages entry in the theorem database of the current
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    78
  theory context.
13048
wenzelm
parents: 13042
diff changeset
    79
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    80
\item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
10160
wenzelm
parents: 10153
diff changeset
    81
  store theorems that have been produced in ML in an ad-hoc manner.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
    82
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    83
\end{descr}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    84
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    85
Note that the original ``LCF-system'' approach of binding theorem values on
10160
wenzelm
parents: 10153
diff changeset
    86
the ML toplevel only has long been given up in Isabelle!  Despite of this, old
wenzelm
parents: 10153
diff changeset
    87
legacy proof scripts occasionally contain code such as \texttt{val foo =
wenzelm
parents: 10153
diff changeset
    88
  result();} which is ill-behaved in several respects.  Apart from preventing
wenzelm
parents: 10153
diff changeset
    89
access from Isar theories, it also omits the result from the WWW presentation,
wenzelm
parents: 10153
diff changeset
    90
for example.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    91
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    92
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    93
\subsection{ML declarations in Isar}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    94
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    95
\begin{matharray}{rcl}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    96
  \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
    97
  \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    98
\end{matharray}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
    99
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   100
Isabelle/Isar theories may contain ML declarations as well.  For example, an
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   101
old-style theorem binding may be mimicked as follows.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   102
\[
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   103
\isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   104
\]
10160
wenzelm
parents: 10153
diff changeset
   105
Note that this command cannot be undone, so invalid theorem bindings in ML may
wenzelm
parents: 10153
diff changeset
   106
persist.  Also note that the current theory may not be modified; use
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   107
$\isarkeyword{ML_setup}$ for declarations that act on the current context.
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   108
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   109
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   110
\section{Porting theories and proof scripts}\label{sec:port-scripts}
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   111
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   112
Porting legacy theory and ML files to proper Isabelle/Isar theories has
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   113
several advantages.  For example, the Proof~General user interface
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   114
\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable to
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   115
use than the version for classic Isabelle.  This is due to the fact that the
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   116
generic ML toplevel has been replaced by a separate Isar interaction loop,
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   117
with full control over input synchronization and error conditions.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   118
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   119
Furthermore, the Isabelle document preparation system (see also
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   120
\cite{isabelle-sys}) only works properly with new-style theories.  Output of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   121
old-style sources is at the level of individual characters (and symbols),
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   122
without proper document markup as in Isabelle/Isar theories.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   123
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   124
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   125
\subsection{Theories}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   126
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   127
Basically, the Isabelle/Isar theory syntax is a proper superset of the classic
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   128
one.  Only a few quirks and legacy problems have been eliminated, resulting in
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   129
simpler rules and less special cases.  The main changes of theory syntax are
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   130
as follows.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   131
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   132
\begin{itemize}
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   133
\item Quoted strings may contain arbitrary white space, and span several lines
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   134
  without requiring \verb,\,\,\dots\verb,\, escapes.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   135
\item Names may always be quoted.
13048
wenzelm
parents: 13042
diff changeset
   136
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   137
  The old syntax would occasionally demand plain identifiers vs.\ quoted
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   138
  strings to accommodate certain syntactic features.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   139
\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
   140
  concerned; this typically requires quoting of input strings, e.g.\ ``$x +
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   141
  y$''.
13048
wenzelm
parents: 13042
diff changeset
   142
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   143
  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
   144
  require less quoting in common cases; this was hard to predict, though.  On
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   145
  the other hand, Isar does not require quotes for simple terms, such as plain
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   146
  identifiers $x$, numerals $1$, or symbols $\forall$ (input as
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   147
  \verb,\<forall>,).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   148
\item Theorem declarations require an explicit colon to separate the name from
10160
wenzelm
parents: 10153
diff changeset
   149
  the statement (the name is usually optional).  Cf.\ the syntax of $\DEFS$ in
wenzelm
parents: 10153
diff changeset
   150
  \S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   151
\end{itemize}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   152
10160
wenzelm
parents: 10153
diff changeset
   153
Note that Isabelle/Isar error messages are usually quite explicit about the
wenzelm
parents: 10153
diff changeset
   154
problem at hand.  So in cases of doubt, input syntax may be just as well tried
wenzelm
parents: 10153
diff changeset
   155
out interactively.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   156
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   157
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   158
\subsection{Goal statements}\label{sec:conv-goal}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   159
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   160
\subsubsection{Simple goals}
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   161
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   162
In ML the canonical a goal statement together with a complete proof script is
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   163
as follows:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   164
\begin{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   165
 Goal "\(\phi\)";
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   166
 by \(tac@1\);
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   167
   \(\vdots\)
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   168
 qed "\(name\)";
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   169
\end{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   170
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
   171
\begin{matharray}{l}
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   172
  \LEMMA{name}{\texttt"{\phi}\texttt"} \\
10223
wenzelm
parents: 10160
diff changeset
   173
  \quad \APPLY{meth@1} \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   174
  \qquad \vdots \\
10223
wenzelm
parents: 10160
diff changeset
   175
  \quad \DONE \\
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   176
\end{matharray}
13013
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   177
Note that the main statement may be $\THEOREMNAME$ or $\COROLLARYNAME$ as
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   178
well.  See \S\ref{sec:conv-tac} for further details on how to convert actual
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   179
tactic expressions into proof methods.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   180
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   181
\medskip Classic Isabelle provides many variant forms of goal commands, see
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   182
also \cite{isabelle-ref} for further details.  The second most common one is
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   183
\texttt{Goalw}, which expands definitions before commencing the actual proof
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   184
script.
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   185
\begin{ttbox}
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   186
 Goalw [\(def@1\), \(\dots\)] "\(\phi\)";
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   187
\end{ttbox}
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   188
This may be replaced by using the $unfold$ proof method explicitly.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   189
\begin{matharray}{l}
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   190
\LEMMA{name}{\texttt"{\phi}\texttt"} \\
13042
wenzelm
parents: 13041
diff changeset
   191
\quad \APPLY{(unfold~def@1~\dots)} \\
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   192
\end{matharray}
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   193
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   194
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   195
\subsubsection{Deriving rules}
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   196
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   197
Deriving non-atomic meta-level propositions requires special precautions in
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   198
classic Isabelle: the primitive \texttt{goal} command decomposes a statement
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   199
into the atomic conclusion and a list of assumptions, which are exhibited as
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   200
ML values of type \texttt{thm}.  After the proof is finished, these premises
13013
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   201
are discharged again, resulting in the original rule statement.  The ``long
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   202
format'' of Isabelle/Isar goal statements admits to emulate this technique
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   203
nicely.  The general ML goal statement for derived rules looks like this:
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   204
\begin{ttbox}
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   205
 val [\(prem@1\), \dots] = goal "\(\phi@1 \Imp \dots \Imp \psi\)";
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   206
 by \(tac@1\);
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   207
   \(\vdots\)
13013
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   208
 qed "\(a\)"
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   209
\end{ttbox}
13013
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   210
This form may be turned into a tactic-emulation script as follows:
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   211
\begin{matharray}{l}
13013
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   212
  \LEMMA{a}{} \\
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   213
  \quad \ASSUMES{prem@1}{\texttt"\phi@1\texttt"}~\AND~\dots \\
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   214
  \quad \SHOWS{}{\texttt"{\psi}\texttt"} \\
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   215
  \qquad \APPLY{meth@1} \\
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   216
  \qquad\quad \vdots \\
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   217
  \qquad \DONE \\
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   218
\end{matharray}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   219
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   220
\medskip In practice, actual rules are often rather direct consequences of
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   221
corresponding atomic statements, typically stemming from the definition of a
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   222
new concept.  In that case, the general scheme for deriving rules may be
11498
wenzelm
parents: 10740
diff changeset
   223
greatly simplified, using one of the standard automated proof tools, such as
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   224
$simp$, $blast$, or $auto$.  This could work as follows:
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   225
\begin{matharray}{l}
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   226
  \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
13042
wenzelm
parents: 13041
diff changeset
   227
  \quad \BYY{(unfold~defs)}{blast} \\
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   228
\end{matharray}
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   229
Note that classic Isabelle would support this form only in the special case
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   230
where $\phi@1$, \dots are atomic statements (when using the standard
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   231
\texttt{Goal} command).  Otherwise the special treatment of rules would be
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   232
applied, disturbing this simple setup.
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   233
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   234
\medskip Occasionally, derived rules would be established by first proving an
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   235
appropriate atomic statement (using $\forall$ and $\longrightarrow$ of the
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   236
object-logic), and putting the final result into ``rule format''.  In classic
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   237
Isabelle this would usually proceed as follows:
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   238
\begin{ttbox}
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   239
 Goal "\(\phi\)";
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   240
 by \(tac@1\);
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   241
   \(\vdots\)
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   242
 qed_spec_mp "\(name\)";
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   243
\end{ttbox}
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   244
The operation performed by \texttt{qed_spec_mp} is also performed by the Isar
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   245
attribute ``$rule_format$'', see also \S\ref{sec:object-logic}.  Thus the
10239
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   246
corresponding Isar text may look like this:
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   247
\begin{matharray}{l}
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   248
  \LEMMA{name~[rule_format]}{\texttt"{\phi}\texttt"} \\
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   249
  \quad \APPLY{meth@1} \\
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   250
  \qquad \vdots \\
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   251
  \quad \DONE \\
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   252
\end{matharray}
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   253
Note plain ``$rule_format$'' actually performs a slightly different operation:
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   254
it fully replaces object-level implication and universal quantification
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   255
throughout the whole result statement.  This is the right thing in most cases.
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   256
For historical reasons, \texttt{qed_spec_mp} would only operate on the
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   257
conclusion; one may get this exact behavior by using
979336bd0aed "Deriving rules";
wenzelm
parents: 10223
diff changeset
   258
``$rule_format~(no_asm)$'' instead.
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   259
13013
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   260
\medskip Actually ``$rule_format$'' is a bit unpleasant to work with, since
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   261
the final result statement is not shown in the text.  An alternative is to
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   262
state the resulting rule in the intended form in the first place, and have the
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   263
initial refinement step turn it into internal object-logic form using the
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   264
$atomize$ method indicated below.  The remaining script is unchanged.
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   265
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   266
\begin{matharray}{l}
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   267
  \LEMMA{name}{\texttt"{\All{\vec x}\vec\phi \Imp \psi}\texttt"} \\
13042
wenzelm
parents: 13041
diff changeset
   268
  \quad \APPLY{(atomize~(full))} \\
13013
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   269
  \quad \APPLY{meth@1} \\
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   270
  \qquad \vdots \\
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   271
  \quad \DONE \\
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   272
\end{matharray}
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   273
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   274
In many situations the $atomize$ step above is actually unnecessary,
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   275
especially if the subsequent script mainly consists of automated tools.
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   276
13013
4db07fc3d96f improved ``deriving rules'';
wenzelm
parents: 12621
diff changeset
   277
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   278
\subsection{Tactics}\label{sec:conv-tac}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   279
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   280
Isar Proof methods closely resemble traditional tactics, when used in
10223
wenzelm
parents: 10160
diff changeset
   281
unstructured sequences of $\APPLYNAME$ commands (cf.\ \S\ref{sec:conv-goal}).
wenzelm
parents: 10160
diff changeset
   282
Isabelle/Isar provides emulations for all major ML tactics of classic Isabelle
wenzelm
parents: 10160
diff changeset
   283
--- mostly for the sake of easy porting of existing developments, as actual
wenzelm
parents: 10160
diff changeset
   284
Isar proof texts would demand much less diversity of proof methods.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   285
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   286
Unlike tactic expressions in ML, Isar proof methods provide proper concrete
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   287
syntax for additional arguments, options, modifiers etc.  Thus a typical
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   288
method text is usually more concise than the corresponding ML tactic.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   289
Furthermore, the Isar versions of classic Isabelle tactics often cover several
10160
wenzelm
parents: 10153
diff changeset
   290
variant forms by a single method with separate options to tune the behavior.
wenzelm
parents: 10153
diff changeset
   291
For example, method $simp$ replaces all of \texttt{simp_tac}~/
wenzelm
parents: 10153
diff changeset
   292
\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac},
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   293
there is also concrete syntax for augmenting the Simplifier context (the
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   294
current ``simpset'') in a convenient way.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   295
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   296
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   297
\subsubsection{Resolution tactics}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   298
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   299
Classic Isabelle provides several variant forms of tactics for single-step
10160
wenzelm
parents: 10153
diff changeset
   300
rule applications (based on higher-order resolution).  The space of resolution
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   301
tactics has the following main dimensions.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   302
\begin{enumerate}
13048
wenzelm
parents: 13042
diff changeset
   303
\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   304
  \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   305
  \texttt{forward_tac}).
13048
wenzelm
parents: 13042
diff changeset
   306
\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   307
  \texttt{res_inst_tac}).
13048
wenzelm
parents: 13042
diff changeset
   308
\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   309
  \texttt{rtac}).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   310
\end{enumerate}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   311
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   312
Basically, the set of Isar tactic emulations $rule_tac$, $erule_tac$,
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   313
$drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   314
cover the four modes, either with or without instantiation, and either with
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   315
single or multiple arguments.  Although it is more convenient in most cases to
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   316
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
   317
``improper'' variants $erule$, $drule$, $frule$ (see
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   318
\S\ref{sec:misc-meth-att}).  Note that explicit goal addressing is only
10160
wenzelm
parents: 10153
diff changeset
   319
supported by the actual $rule_tac$ version.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   320
10160
wenzelm
parents: 10153
diff changeset
   321
With this in mind, plain resolution tactics may be ported as follows.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   322
\begin{matharray}{lll}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   323
  \texttt{rtac}~a~1 & & rule~a \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   324
  \texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   325
  \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~1 & &
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   326
  rule_tac~x@1 = t@1~and~\dots~in~a \\[0.5ex]
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   327
  \texttt{rtac}~a~i & & rule_tac~[i]~a \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   328
  \texttt{resolve_tac}~[a@1, \dots]~i & & rule_tac~[i]~a@1~\dots \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   329
  \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~i & &
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   330
  rule_tac~[i]~x@1 = t@1~and~\dots~in~a \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   331
\end{matharray}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   332
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   333
Note that explicit goal addressing may be usually avoided by changing the
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   334
order of subgoals with $\isarkeyword{defer}$ or $\isarkeyword{prefer}$ (see
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   335
\S\ref{sec:tactic-commands}).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   336
10740
8256cfec2040 ares_tac, [edf]atac;
wenzelm
parents: 10239
diff changeset
   337
\medskip Some further (less frequently used) combinations of basic resolution
8256cfec2040 ares_tac, [edf]atac;
wenzelm
parents: 10239
diff changeset
   338
tactics may be expressed as follows.
8256cfec2040 ares_tac, [edf]atac;
wenzelm
parents: 10239
diff changeset
   339
\begin{matharray}{lll}
8256cfec2040 ares_tac, [edf]atac;
wenzelm
parents: 10239
diff changeset
   340
  \texttt{ares_tac}~[a@1, \dots]~1 & & assumption~|~rule~a@1~\dots \\
8256cfec2040 ares_tac, [edf]atac;
wenzelm
parents: 10239
diff changeset
   341
  \texttt{eatac}~a~n~1 & & erule~(n)~a \\
8256cfec2040 ares_tac, [edf]atac;
wenzelm
parents: 10239
diff changeset
   342
  \texttt{datac}~a~n~1 & & drule~(n)~a \\
8256cfec2040 ares_tac, [edf]atac;
wenzelm
parents: 10239
diff changeset
   343
  \texttt{fatac}~a~n~1 & & frule~(n)~a \\
8256cfec2040 ares_tac, [edf]atac;
wenzelm
parents: 10239
diff changeset
   344
\end{matharray}
8256cfec2040 ares_tac, [edf]atac;
wenzelm
parents: 10239
diff changeset
   345
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   346
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   347
\subsubsection{Simplifier tactics}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   348
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   349
The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   350
(cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
13048
wenzelm
parents: 13042
diff changeset
   351
methods (see \S\ref{sec:simplifier}).  Note that there is no individual goal
wenzelm
parents: 13042
diff changeset
   352
addressing available, simplification acts either on the first goal ($simp$) or
wenzelm
parents: 13042
diff changeset
   353
all goals ($simp_all$).
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   354
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   355
\begin{matharray}{lll}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   356
  \texttt{Asm_full_simp_tac 1} & & simp \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   357
  \texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex]
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   358
  \texttt{Simp_tac 1} & & simp~(no_asm) \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   359
  \texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   360
  \texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\
13625
ca86e84ce200 Documented new "asm_lr" option for simp.
berghofe
parents: 13048
diff changeset
   361
  \texttt{Asm_lr_simp_tac 1} & & simp~(asm_lr) \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   362
\end{matharray}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   363
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   364
Isar also provides separate method modifier syntax for augmenting the
13048
wenzelm
parents: 13042
diff changeset
   365
Simplifier context (see \S\ref{sec:simplifier}), which is known as the
wenzelm
parents: 13042
diff changeset
   366
``simpset'' in ML.  A typical ML expression with simpset changes looks like
wenzelm
parents: 13042
diff changeset
   367
this:
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   368
\begin{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   369
asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   370
\end{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   371
The corresponding Isar text is as follows:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   372
\[
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   373
simp~add:~a@1~\dots~del:~b@1~\dots
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   374
\]
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   375
Global declarations of Simplifier rules (e.g.\ \texttt{Addsimps}) are covered
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   376
by application of attributes, see \S\ref{sec:conv-decls} for more information.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   377
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   378
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   379
\subsubsection{Classical Reasoner tactics}
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   380
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   381
The Classical Reasoner provides a rather large number of variations of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   382
automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   383
\texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}).  The corresponding Isar
10160
wenzelm
parents: 10153
diff changeset
   384
methods usually share the same base name, such as $blast$, $fast$, $clarify$
13048
wenzelm
parents: 13042
diff changeset
   385
etc.\ (see \S\ref{sec:classical}).
9798
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   386
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   387
Similar to the Simplifier, there is separate method modifier syntax for
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   388
augmenting the Classical Reasoner context, which is known as the ``claset'' in
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   389
ML.  A typical ML expression with claset changes looks like this:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   390
\begin{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   391
blast_tac (claset () addIs [\(a@1\), \(\dots\)] addSEs [\(b@1\), \(\dots\)]) 1
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   392
\end{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   393
The corresponding Isar text is as follows:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   394
\[
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   395
blast~intro:~a@1~\dots~elim!:~b@1~\dots
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   396
\]
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   397
Global declarations of Classical Reasoner rules (e.g.\ \texttt{AddIs}) are
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   398
covered by application of attributes, see \S\ref{sec:conv-decls} for more
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   399
information.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   400
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   401
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   402
\subsubsection{Miscellaneous tactics}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   403
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   404
There are a few additional tactics defined in various theories of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   405
Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF.  The most
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   406
common ones of these may be ported to Isar as follows.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   407
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   408
\begin{matharray}{lll}
9798
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   409
  \texttt{stac}~a~1 & & subst~a \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   410
  \texttt{hyp_subst_tac}~1 & & hypsubst \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   411
  \texttt{strip_tac}~1 & \approx & intro~strip \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   412
  \texttt{split_all_tac}~1 & & simp~(no_asm_simp)~only:~split_tupled_all \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   413
                         & \approx & simp~only:~split_tupled_all \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   414
                         & \ll & clarify \\
9798
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   415
\end{matharray}
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   416
21b36757a9a5 some stuff;
wenzelm
parents: 9607
diff changeset
   417
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   418
\subsubsection{Tacticals}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   419
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   420
Classic Isabelle provides a huge amount of tacticals for combination and
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   421
modification of existing tactics.  This has been greatly reduced in Isar,
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   422
providing the bare minimum of combinators only: ``$,$'' (sequential
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   423
composition), ``$|$'' (alternative choices), ``$?$'' (try), ``$+$'' (repeat at
10160
wenzelm
parents: 10153
diff changeset
   424
least once).  These are usually sufficient in practice; if all fails,
wenzelm
parents: 10153
diff changeset
   425
arbitrary ML tactic code may be invoked via the $tactic$ method (see
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   426
\S\ref{sec:tactics}).
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   427
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   428
\medskip Common ML tacticals may be expressed directly in Isar as follows:
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   429
\begin{matharray}{lll}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   430
tac@1~\texttt{THEN}~tac@2 & & meth@1, meth@2 \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   431
tac@1~\texttt{ORELSE}~tac@2 & & meth@1~|~meth@2 \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   432
\texttt{TRY}~tac & & meth? \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   433
\texttt{REPEAT1}~tac & & meth+ \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   434
\texttt{REPEAT}~tac & & (meth+)? \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   435
\texttt{EVERY}~[tac@1, \dots] & & meth@1, \dots \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   436
\texttt{FIRST}~[tac@1, \dots] & & meth@1~|~\dots \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   437
\end{matharray}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   438
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   439
\medskip \texttt{CHANGED} (see \cite{isabelle-ref}) is usually not required in
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   440
Isar, since most basic proof methods already fail unless there is an actual
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   441
change in the goal state.  Nevertheless, ``$?$'' (try) may be used to accept
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   442
\emph{unchanged} results as well.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   443
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   444
\medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref})
10160
wenzelm
parents: 10153
diff changeset
   445
are not available in Isar, since there is no direct goal addressing.
wenzelm
parents: 10153
diff changeset
   446
Nevertheless, some basic methods address all goals internally, notably
13048
wenzelm
parents: 13042
diff changeset
   447
$simp_all$ (see \S\ref{sec:simplifier}).  Also note that \texttt{ALLGOALS} may
wenzelm
parents: 13042
diff changeset
   448
be often replaced by ``$+$'' (repeat at least once), although this usually has
wenzelm
parents: 13042
diff changeset
   449
a different operational behavior, such as solving goals in a different order.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   450
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   451
\medskip Iterated resolution, such as
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   452
\texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
13048
wenzelm
parents: 13042
diff changeset
   453
using the $intro$ and $elim$ methods of Isar (see \S\ref{sec:classical}).
10111
78a0397eaec1 some preliminary stuff on conversion;
wenzelm
parents: 9846
diff changeset
   454
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   455
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   456
\subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   457
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   458
Apart from proof commands and tactic expressions, almost all of the remaining
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   459
ML code occurring in legacy proof scripts are either global context
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   460
declarations (such as \texttt{Addsimps}) or ad-hoc operations on theorems
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   461
(such as \texttt{RS}).  In Isar both of these are covered by theorem
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   462
expressions with \emph{attributes}.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   463
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   464
\medskip Theorem operations may be attached as attributes in the very place
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   465
where theorems are referenced, say within a method argument.  The subsequent
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   466
ML combinators may be expressed directly in Isar as follows.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   467
\begin{matharray}{lll}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   468
  thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\
10160
wenzelm
parents: 10153
diff changeset
   469
  thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   470
  thm@1~\texttt{COMP}~thm@2 & & thm@1~[COMP~thm@2] \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   471
  \relax[thm@1, \dots]~\texttt{MRS}~thm & & thm~[OF~thm@1~\dots] \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   472
  \texttt{read_instantiate}~[(x@1, t@1), \dots]~thm & & thm~[where~x@1 = t@1~and~\dots] \\
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   473
  \texttt{make_elim}~thm & & thm~[elim_format] \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   474
  \texttt{standard}~thm & & thm~[standard] \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   475
\end{matharray}
10160
wenzelm
parents: 10153
diff changeset
   476
wenzelm
parents: 10153
diff changeset
   477
Note that $OF$ is often more readable as $THEN$; likewise positional
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   478
instantiation with $of$ is often more appropriate than $where$.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   479
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   480
The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be
10160
wenzelm
parents: 10153
diff changeset
   481
replaced by passing the result of a proof through $rule_format$.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   482
10223
wenzelm
parents: 10160
diff changeset
   483
\medskip Global ML declarations may be expressed using the $\DECLARE$ command
wenzelm
parents: 10160
diff changeset
   484
(see \S\ref{sec:tactic-commands}) together with appropriate attributes.  The
wenzelm
parents: 10160
diff changeset
   485
most common ones are as follows.
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   486
\begin{matharray}{lll}
10223
wenzelm
parents: 10160
diff changeset
   487
  \texttt{Addsimps}~[thm] & & \DECLARE~thm~[simp] \\
wenzelm
parents: 10160
diff changeset
   488
  \texttt{Delsimps}~[thm] & & \DECLARE~thm~[simp~del] \\
wenzelm
parents: 10160
diff changeset
   489
  \texttt{Addsplits}~[thm] & & \DECLARE~thm~[split] \\
wenzelm
parents: 10160
diff changeset
   490
  \texttt{Delsplits}~[thm] & & \DECLARE~thm~[split~del] \\[0.5ex]
wenzelm
parents: 10160
diff changeset
   491
  \texttt{AddIs}~[thm] & & \DECLARE~thm~[intro] \\
wenzelm
parents: 10160
diff changeset
   492
  \texttt{AddEs}~[thm] & & \DECLARE~thm~[elim] \\
wenzelm
parents: 10160
diff changeset
   493
  \texttt{AddDs}~[thm] & & \DECLARE~thm~[dest] \\
wenzelm
parents: 10160
diff changeset
   494
  \texttt{AddSIs}~[thm] & & \DECLARE~thm~[intro!] \\
wenzelm
parents: 10160
diff changeset
   495
  \texttt{AddSEs}~[thm] & & \DECLARE~thm~[elim!] \\
wenzelm
parents: 10160
diff changeset
   496
  \texttt{AddSDs}~[thm] & & \DECLARE~thm~[dest!] \\[0.5ex]
wenzelm
parents: 10160
diff changeset
   497
  \texttt{AddIffs}~[thm] & & \DECLARE~thm~[iff] \\
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   498
\end{matharray}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   499
Note that explicit $\DECLARE$ commands are rarely needed in practice; Isar
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   500
admits to declare theorems on-the-fly wherever they emerge.  Consider the
10223
wenzelm
parents: 10160
diff changeset
   501
following ML idiom:
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   502
\begin{ttbox}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   503
Goal "\(\phi\)";
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   504
 \(\vdots\)
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   505
qed "name";
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   506
Addsimps [name];
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   507
\end{ttbox}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   508
This may be expressed more succinctly in Isar like this:
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   509
\begin{matharray}{l}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   510
  \LEMMA{name~[simp]}{\phi} \\
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   511
  \quad\vdots
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   512
\end{matharray}
10160
wenzelm
parents: 10153
diff changeset
   513
The $name$ may be even omitted, although this would make it difficult to
wenzelm
parents: 10153
diff changeset
   514
declare the theorem otherwise later (e.g.\ as $[simp~del]$).
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   515
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   516
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   517
\section{Writing actual Isar proof texts}
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   518
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   519
Porting legacy ML proof scripts into Isar tactic emulation scripts (see
10160
wenzelm
parents: 10153
diff changeset
   520
\S\ref{sec:port-scripts}) is mainly a technical issue, since the basic
wenzelm
parents: 10153
diff changeset
   521
representation of formal ``proof script'' is preserved.  In contrast,
wenzelm
parents: 10153
diff changeset
   522
converting existing Isabelle developments into actual human-readably Isar
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   523
proof texts is more involved, due to the fundamental change of the underlying
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   524
paradigm.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   525
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   526
This issue is comparable to that of converting programs written in a low-level
10160
wenzelm
parents: 10153
diff changeset
   527
programming languages (say Assembler) into higher-level ones (say Haskell).
wenzelm
parents: 10153
diff changeset
   528
In order to accomplish this, one needs a working knowledge of the target
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   529
language, as well an understanding of the \emph{original} idea of the piece of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   530
code expressed in the low-level language.
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   531
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   532
As far as Isar proofs are concerned, it is usually much easier to re-use only
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   533
definitions and the main statements, while following the arrangement of proof
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   534
scripts only very loosely.  Ideally, one would also have some \emph{informal}
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   535
proof outlines available for guidance as well.  In the worst case, obscure
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   536
proof scripts would have to be re-engineered by tracing forth and backwards,
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   537
and by educated guessing!
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   538
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   539
\medskip This is a possible schedule to embark on actual conversion of legacy
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   540
proof scripts into Isar proof texts.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   541
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   542
\begin{enumerate}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   543
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   544
\item Port ML scripts to Isar tactic emulation scripts (see
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   545
  \S\ref{sec:port-scripts}).
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   546
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   547
\item Get sufficiently acquainted with Isabelle/Isar proof
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   548
  development.\footnote{As there is still no Isar tutorial around, it is best
10160
wenzelm
parents: 10153
diff changeset
   549
    to look at existing Isar examples, see also \S\ref{sec:isar-howto}.}
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   550
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   551
\item Recover the proof structure of a few important theorems.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   552
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   553
\item Rephrase the original intention of the course of reasoning in terms of
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   554
  Isar proof language elements.
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   555
10153
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   556
\end{enumerate}
482899aff303 added more stuff;
wenzelm
parents: 10111
diff changeset
   557
13041
6faccf7d0f25 *** empty log message ***
wenzelm
parents: 13024
diff changeset
   558
Certainly, rewriting formal reasoning in Isar requires some additional effort.
10160
wenzelm
parents: 10153
diff changeset
   559
On the other hand, one gains a human-readable representation of
wenzelm
parents: 10153
diff changeset
   560
machine-checked formal proof.  Depending on the context of application, this
wenzelm
parents: 10153
diff changeset
   561
might be even indispensable to start with!
wenzelm
parents: 10153
diff changeset
   562
13048
wenzelm
parents: 13042
diff changeset
   563
%%% Local Variables:
9607
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   564
%%% mode: latex
449b6108352a added conversion.tex;
wenzelm
parents:
diff changeset
   565
%%% TeX-master: "isar-ref"
13048
wenzelm
parents: 13042
diff changeset
   566
%%% End: