doc-src/IsarRef/pure.tex
author wenzelm
Wed, 08 Mar 2000 23:43:11 +0100
changeset 8379 4c7659e98eb9
parent 8250 f4029c34adef
child 8448 e7df316491d4
permissions -rw-r--r--
tuned ML types; improved translation functions; 'case' command; 'oops' command; "Emulating tactic scripts";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     1
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
     2
\chapter{Basic Isar Language Elements}\label{ch:pure-syntax}
7167
wenzelm
parents: 7141
diff changeset
     3
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
     4
Subsequently, we introduce the main part of the basic Isar theory and proof
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
     5
commands as provided by Isabelle/Pure.  Chapter~\ref{ch:gen-tools} describes
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
     6
further Isar elements provided by generic tools and packages (such as the
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
     7
Simplifier) that are either part of Pure Isabelle or pre-loaded by most object
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
     8
logics.  Chapter~\ref{ch:hol-tools} refers to actual object-logic specific
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
     9
elements of Isabelle/HOL.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    10
7167
wenzelm
parents: 7141
diff changeset
    11
\medskip
wenzelm
parents: 7141
diff changeset
    12
wenzelm
parents: 7141
diff changeset
    13
Isar commands may be either \emph{proper} document constructors, or
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
    14
\emph{improper commands}.  Some proof methods and attributes introduced later
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
    15
are classified as improper as well.  Improper Isar language elements, which
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
    16
are subsequently marked by $^*$, are often helpful when developing proof
7981
wenzelm
parents: 7974
diff changeset
    17
documents, while their use is discouraged for the final outcome.  Typical
wenzelm
parents: 7974
diff changeset
    18
examples are diagnostic commands that print terms or theorems according to the
wenzelm
parents: 7974
diff changeset
    19
current context; other commands even emulate old-style tactical theorem
wenzelm
parents: 7974
diff changeset
    20
proving, which facilitates porting of legacy proof scripts.
7167
wenzelm
parents: 7141
diff changeset
    21
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    22
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    23
\section{Theory commands}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    24
7167
wenzelm
parents: 7141
diff changeset
    25
\subsection{Defining theories}\label{sec:begin-thy}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    26
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    27
\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    28
\begin{matharray}{rcl}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    29
  \isarcmd{header} & : & \isarkeep{toplevel} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    30
  \isarcmd{theory} & : & \isartrans{\cdot}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    31
  \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    32
  \isarcmd{end} & : & \isartrans{theory}{\cdot} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    33
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    34
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    35
Isabelle/Isar ``new-style'' theories are either defined via theory files or
7981
wenzelm
parents: 7974
diff changeset
    36
interactively.  Both theory-level specifications and proofs are handled
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
    37
uniformly --- occasionally definitional mechanisms even require some explicit
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
    38
proof as well.  In contrast, ``old-style'' Isabelle theories support batch
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
    39
processing only, with the proof scripts collected in separate ML files.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    40
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    41
The first actual command of any theory has to be $\THEORY$, starting a new
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    42
theory based on the merge of existing ones.  Just preceding $\THEORY$, there
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    43
may be an optional $\isarkeyword{header}$ declaration, which is relevant to
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    44
document preparation only; it acts very much like a special pre-theory markup
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    45
command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}).  The theory
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    46
context may be also changed by $\CONTEXT$ without creating a new theory.  In
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    47
both cases, $\END$ concludes the theory development; it has to be the very
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    48
last command in a theory file.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    49
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    50
\begin{rail}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    51
  'header' text
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    52
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    53
  'theory' name '=' (name + '+') filespecs? ':'
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    54
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    55
  'context' name
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    56
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    57
  'end'
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    58
  ;;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    59
7167
wenzelm
parents: 7141
diff changeset
    60
  filespecs: 'files' ((name | parname) +);
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    61
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    62
7167
wenzelm
parents: 7141
diff changeset
    63
\begin{descr}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    64
\item [$\isarkeyword{header}~text$] provides plain text markup just preceding
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    65
  the formal begin of a theory.  In actual document preparation the
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    66
  corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    67
  produce chapter or section headings.  See also \S\ref{sec:markup-thy} and
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    68
  \S\ref{sec:markup-prf} for further markup commands.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    69
  
7981
wenzelm
parents: 7974
diff changeset
    70
\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$
wenzelm
parents: 7974
diff changeset
    71
  based on existing ones $B@1 + \cdots + B@n$.  Isabelle's theory loader
wenzelm
parents: 7974
diff changeset
    72
  system ensures that any of the base theories are properly loaded (and fully
wenzelm
parents: 7974
diff changeset
    73
  up-to-date when $\THEORY$ is executed interactively).  The optional
wenzelm
parents: 7974
diff changeset
    74
  $\isarkeyword{files}$ specification declares additional dependencies on ML
wenzelm
parents: 7974
diff changeset
    75
  files.  Unless put in parentheses, any file will be loaded immediately via
wenzelm
parents: 7974
diff changeset
    76
  $\isarcmd{use}$ (see also \S\ref{sec:ML}).  The optional ML file
wenzelm
parents: 7974
diff changeset
    77
  \texttt{$A$.ML} that may be associated with any theory should \emph{not} be
wenzelm
parents: 7974
diff changeset
    78
  included in $\isarkeyword{files}$, though.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    79
  
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    80
\item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
7981
wenzelm
parents: 7974
diff changeset
    81
  mode, so only a limited set of commands may be performed without destroying
wenzelm
parents: 7974
diff changeset
    82
  the theory.  Just as for $\THEORY$, the theory loader ensures that $B$ is
wenzelm
parents: 7974
diff changeset
    83
  loaded and up-to-date.
7175
wenzelm
parents: 7167
diff changeset
    84
  
7167
wenzelm
parents: 7141
diff changeset
    85
\item [$\END$] concludes the current theory definition or context switch.
7981
wenzelm
parents: 7974
diff changeset
    86
Note that this command cannot be undone, but the whole theory definition has
wenzelm
parents: 7974
diff changeset
    87
to be retracted.
7167
wenzelm
parents: 7141
diff changeset
    88
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    89
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    90
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    91
\subsection{Theory markup commands}\label{sec:markup-thy}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    92
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    93
\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    94
\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    95
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    96
  \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
7167
wenzelm
parents: 7141
diff changeset
    97
  \isarcmd{section} & : & \isartrans{theory}{theory} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    98
  \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    99
  \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   100
  \isarcmd{text} & : & \isartrans{theory}{theory} \\
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   101
  \isarcmd{text_raw} & : & \isartrans{theory}{theory} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   102
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   103
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   104
Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
7981
wenzelm
parents: 7974
diff changeset
   105
a structured way to insert text into the document generated from a theory (see
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   106
\cite{isabelle-sys} for more information on Isabelle's document preparation
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   107
tools).
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   108
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   109
\railalias{textraw}{text\_raw}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   110
\railterm{textraw}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   111
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   112
\begin{rail}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   113
  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   114
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   115
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   116
7167
wenzelm
parents: 7141
diff changeset
   117
\begin{descr}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   118
\item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   119
  $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   120
  and section headings.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   121
\item [$\TEXT$] specifies paragraphs of plain text, including references to
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   122
  formal entities.\footnote{The latter feature is not yet supported.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   123
    Nevertheless, any source text of the form
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   124
    ``\texttt{\at\ttlbrace$\dots$\ttrbrace}'' should be considered as reserved
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   125
    for future use.}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   126
\item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   127
  without additional markup.  Thus the full range of document manipulations
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   128
  becomes available.  A typical application would be to emit
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   129
  \verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   130
  parts from the final document.\footnote{This requires the \texttt{comment}
7981
wenzelm
parents: 7974
diff changeset
   131
    package to be included in {\LaTeX}.}
7167
wenzelm
parents: 7141
diff changeset
   132
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   133
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   134
Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}
7981
wenzelm
parents: 7974
diff changeset
   135
macro with the name prefixed by \verb,\isamarkup, (e.g.\ 
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   136
\verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}
7981
wenzelm
parents: 7974
diff changeset
   137
argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands
wenzelm
parents: 7974
diff changeset
   138
may be included here as well.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   139
7981
wenzelm
parents: 7974
diff changeset
   140
\medskip Additional markup commands are available for proofs (see
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   141
\S\ref{sec:markup-prf}).  Also note that the $\isarkeyword{header}$
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   142
declaration (see \S\ref{sec:begin-thy}) admits to insert document markup
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   143
elements just preceding the actual theory definition.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   144
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   145
7135
wenzelm
parents: 7134
diff changeset
   146
\subsection{Type classes and sorts}\label{sec:classes}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   147
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   148
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   149
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   150
  \isarcmd{classes} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   151
  \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   152
  \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   153
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   154
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   155
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   156
  'classes' (classdecl comment? +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   157
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   158
  'classrel' nameref '<' nameref comment?
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   159
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   160
  'defaultsort' sort comment?
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   161
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   162
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   163
7167
wenzelm
parents: 7141
diff changeset
   164
\begin{descr}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   165
\item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   166
  of existing classes $\vec c$.  Cyclic class structures are ruled out.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   167
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   168
  existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   169
  $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way to
7175
wenzelm
parents: 7167
diff changeset
   170
  introduce proven class relations.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   171
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   172
  any type variables given without sort constraints.  Usually, the default
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   173
  sort would be only changed when defining new logics.
7167
wenzelm
parents: 7141
diff changeset
   174
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   175
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   176
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   177
\subsection{Primitive types and type abbreviations}\label{sec:types-pure}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   178
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   179
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   180
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   181
  \isarcmd{types} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   182
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   183
  \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   184
  \isarcmd{arities} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   185
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   186
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   187
\begin{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   188
  'types' (typespec '=' type infix? comment? +)
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   189
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   190
  'typedecl' typespec infix? comment?
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   191
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   192
  'nonterminals' (name +) comment?
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   193
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   194
  'arities' (nameref '::' arity comment? +)
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   195
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   196
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   197
7167
wenzelm
parents: 7141
diff changeset
   198
\begin{descr}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   199
\item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   200
  $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   201
  as are available in Isabelle/HOL for example, type synonyms are just purely
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   202
  syntactic abbreviations without any logical significance.  Internally, type
7981
wenzelm
parents: 7974
diff changeset
   203
  synonyms are fully expanded.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   204
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   205
  $t$, intended as an actual logical type.  Note that object-logics such as
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   206
  Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.
7175
wenzelm
parents: 7167
diff changeset
   207
\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
wenzelm
parents: 7167
diff changeset
   208
  $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
wenzelm
parents: 7167
diff changeset
   209
  Isabelle's inner syntax of terms or types.
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   210
\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   211
  signature of types by new type constructor arities.  This is done
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   212
  axiomatically!  The $\isarkeyword{instance}$ command (see
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   213
  \S\ref{sec:axclass}) provides a way to introduce proven type arities.
7167
wenzelm
parents: 7141
diff changeset
   214
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   215
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   216
7981
wenzelm
parents: 7974
diff changeset
   217
\subsection{Constants and simple definitions}\label{sec:consts}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   218
7175
wenzelm
parents: 7167
diff changeset
   219
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   220
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   221
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   222
  \isarcmd{defs} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   223
  \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   224
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   225
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   226
\begin{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   227
  'consts' (constdecl +)
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   228
  ;
7608
8069542cba82 defs: axmdecl;
wenzelm
parents: 7510
diff changeset
   229
  'defs' (axmdecl prop comment? +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   230
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   231
  'constdefs' (constdecl prop comment? +)
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   232
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   233
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   234
  constdecl: name '::' type mixfix? comment?
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   235
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   236
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   237
7167
wenzelm
parents: 7141
diff changeset
   238
\begin{descr}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   239
\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   240
  scheme $\sigma$.  The optional mixfix annotations may attach concrete syntax
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   241
  to the constants declared.
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   242
\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   243
  existing constant.  See \cite[\S6]{isabelle-ref} for more details on the
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   244
  form of equations admitted as constant definitions.
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   245
\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   246
  definitions of constants, using canonical name $c_def$ for the definitional
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   247
  axiom.
7167
wenzelm
parents: 7141
diff changeset
   248
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   249
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   250
7981
wenzelm
parents: 7974
diff changeset
   251
\subsection{Syntax and translations}\label{sec:syn-trans}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   252
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   253
\indexisarcmd{syntax}\indexisarcmd{translations}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   254
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   255
  \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   256
  \isarcmd{translations} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   257
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   258
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   259
\begin{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   260
  'syntax' ('(' name 'output'? ')')? (constdecl +)
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   261
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   262
  'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   263
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   264
  transpat: ('(' nameref ')')? string
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   265
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   266
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   267
7167
wenzelm
parents: 7141
diff changeset
   268
\begin{descr}
7175
wenzelm
parents: 7167
diff changeset
   269
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
wenzelm
parents: 7167
diff changeset
   270
  except that the actual logical signature extension is omitted.  Thus the
wenzelm
parents: 7167
diff changeset
   271
  context free grammar of Isabelle's inner syntax may be augmented in
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   272
  arbitrary ways, independently of the logic.  The $mode$ argument refers to
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   273
  the print mode that the grammar rules belong; unless there is the
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   274
  \texttt{output} flag given, all productions are added both to the input and
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   275
  output grammar.
7175
wenzelm
parents: 7167
diff changeset
   276
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
7981
wenzelm
parents: 7974
diff changeset
   277
  rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   278
  (\texttt{=>}), or print rules (\texttt{<=}).  Translation patterns may be
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   279
  prefixed by the syntactic category to be used for parsing; the default is
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   280
  \texttt{logic}.
7167
wenzelm
parents: 7141
diff changeset
   281
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   282
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   283
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   284
\subsection{Axioms and theorems}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   285
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   286
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   287
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   288
  \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   289
  \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   290
  \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   291
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   292
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   293
\begin{rail}
7135
wenzelm
parents: 7134
diff changeset
   294
  'axioms' (axmdecl prop comment? +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   295
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   296
  ('theorems' | 'lemmas') thmdef? thmrefs
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   297
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   298
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   299
7167
wenzelm
parents: 7141
diff changeset
   300
\begin{descr}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   301
\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   302
  axioms of the meta-logic.  In fact, axioms are ``axiomatic theorems'', and
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   303
  may be referred later just as any other theorem.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   304
  
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   305
  Axioms are usually only introduced when declaring new logical systems.
7175
wenzelm
parents: 7167
diff changeset
   306
  Everyday work is typically done the hard way, with proper definitions and
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   307
  actual theorems.
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   308
\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
7981
wenzelm
parents: 7974
diff changeset
   309
  Typical applications would also involve attributes, to augment the
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   310
  Simplifier context, for example.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   311
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   312
  tags the results as ``lemma''.
7167
wenzelm
parents: 7141
diff changeset
   313
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   314
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   315
7167
wenzelm
parents: 7141
diff changeset
   316
\subsection{Name spaces}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   317
7167
wenzelm
parents: 7141
diff changeset
   318
\indexisarcmd{global}\indexisarcmd{local}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   319
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   320
  \isarcmd{global} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   321
  \isarcmd{local} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   322
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   323
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   324
Isabelle organizes any kind of name declarations (of types, constants,
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   325
theorems etc.)  by hierarchically structured name spaces.  Normally the user
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   326
never has to control the behavior of name space entry by hand, yet the
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   327
following commands provide some way to do so.
7175
wenzelm
parents: 7167
diff changeset
   328
7167
wenzelm
parents: 7141
diff changeset
   329
\begin{descr}
wenzelm
parents: 7141
diff changeset
   330
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
wenzelm
parents: 7141
diff changeset
   331
  name declaration mode.  Initially, theories start in $\isarkeyword{local}$
wenzelm
parents: 7141
diff changeset
   332
  mode, causing all names to be automatically qualified by the theory name.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   333
  Changing this to $\isarkeyword{global}$ causes all names to be declared
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   334
  without the theory prefix, until $\isarkeyword{local}$ is declared again.
7167
wenzelm
parents: 7141
diff changeset
   335
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   336
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   337
7167
wenzelm
parents: 7141
diff changeset
   338
\subsection{Incorporating ML code}\label{sec:ML}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   339
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   340
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-setup}\indexisarcmd{setup}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   341
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   342
  \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   343
  \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   344
  \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
7175
wenzelm
parents: 7167
diff changeset
   345
  \isarcmd{setup} & : & \isartrans{theory}{theory} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   346
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   347
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   348
\railalias{MLsetup}{ML\_setup}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   349
\railterm{MLsetup}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   350
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   351
\begin{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   352
  'use' name
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   353
  ;
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   354
  ('ML' | MLsetup | 'setup') text
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   355
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   356
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   357
7167
wenzelm
parents: 7141
diff changeset
   358
\begin{descr}
7175
wenzelm
parents: 7167
diff changeset
   359
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   360
  The current theory context (if present) is passed down to the ML session,
7981
wenzelm
parents: 7974
diff changeset
   361
  but may not be modified.  Furthermore, the file name is checked with the
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   362
  $\isarkeyword{files}$ dependency declaration given in the theory header (see
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   363
  also \S\ref{sec:begin-thy}).
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   364
  
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   365
\item [$\isarkeyword{ML}~text$] executes ML commands from $text$.  The theory
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   366
  context is passed in the same way as for $\isarkeyword{use}$.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   367
  
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   368
\item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$.  The
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   369
  theory context is passed down to the ML session, and fetched back
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   370
  afterwards.  Thus $text$ may actually change the theory as a side effect.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   371
  
7167
wenzelm
parents: 7141
diff changeset
   372
\item [$\isarkeyword{setup}~text$] changes the current theory context by
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   373
  applying $text$, which refers to an ML expression of type
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   374
  \texttt{(theory~->~theory)~list}.  The $\isarkeyword{setup}$ command is the
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   375
  canonical way to initialize object-logic specific tools and packages written
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   376
  in ML.
7167
wenzelm
parents: 7141
diff changeset
   377
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   378
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   379
8250
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   380
\subsection{Syntax translation functions}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   381
8250
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   382
\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   383
\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   384
\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   385
\begin{matharray}{rcl}
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   386
  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   387
  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   388
  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   389
  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   390
  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   391
  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   392
\end{matharray}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   393
8250
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   394
Syntax translation functions written in ML admit almost arbitrary
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   395
manipulations of Isabelle's inner syntax.  Any of the above commands have a
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   396
single \railqtoken{text} argument that refers to an ML expression of
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   397
appropriate type.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   398
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   399
\begin{ttbox}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   400
val parse_ast_translation   : (string * (ast list -> ast)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   401
val parse_translation       : (string * (term list -> term)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   402
val print_translation       : (string * (term list -> term)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   403
val typed_print_translation :
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   404
  (string * (bool -> typ -> term list -> term)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   405
val print_ast_translation   : (string * (ast list -> ast)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   406
val token_translation       :
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   407
  (string * string * (string -> string * real)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   408
\end{ttbox}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   409
See \cite[\S8]{isabelle-ref} for more information on syntax transformations.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   410
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   411
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   412
\subsection{Oracles}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   413
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   414
\indexisarcmd{oracle}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   415
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   416
  \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   417
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   418
7175
wenzelm
parents: 7167
diff changeset
   419
Oracles provide an interface to external reasoning systems, without giving up
wenzelm
parents: 7167
diff changeset
   420
control completely --- each theorem carries a derivation object recording any
wenzelm
parents: 7167
diff changeset
   421
oracle invocation.  See \cite[\S6]{isabelle-ref} for more information.
wenzelm
parents: 7167
diff changeset
   422
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   423
\begin{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   424
  'oracle' name '=' text comment?
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   425
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   426
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   427
7167
wenzelm
parents: 7141
diff changeset
   428
\begin{descr}
7175
wenzelm
parents: 7167
diff changeset
   429
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   430
  function $text$, which has to be of type
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   431
  \texttt{Sign.sg~*~Object.T~->~term}.
7167
wenzelm
parents: 7141
diff changeset
   432
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   433
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   434
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   435
\section{Proof commands}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   436
7987
wenzelm
parents: 7981
diff changeset
   437
Proof commands perform transitions of Isar/VM machine configurations, which
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   438
are block-structured, consisting of a stack of nodes with three main
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   439
components: logical proof context, current facts, and open goals.  Isar/VM
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   440
transitions are \emph{typed} according to the following three three different
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   441
modes of operation:
7167
wenzelm
parents: 7141
diff changeset
   442
\begin{descr}
wenzelm
parents: 7141
diff changeset
   443
\item [$proof(prove)$] means that a new goal has just been stated that is now
wenzelm
parents: 7141
diff changeset
   444
  to be \emph{proven}; the next command may refine it by some proof method
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   445
  (read: tactic), and enter a sub-proof to establish the actual result.
7167
wenzelm
parents: 7141
diff changeset
   446
\item [$proof(state)$] is like an internal theory mode: the context may be
7987
wenzelm
parents: 7981
diff changeset
   447
  augmented by \emph{stating} additional assumptions, intermediate results
wenzelm
parents: 7981
diff changeset
   448
  etc.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   449
\item [$proof(chain)$] is intermediate between $proof(state)$ and
7987
wenzelm
parents: 7981
diff changeset
   450
  $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
wenzelm
parents: 7981
diff changeset
   451
  register) have been just picked up in order to be used when refining the
wenzelm
parents: 7981
diff changeset
   452
  goal claimed next.
7167
wenzelm
parents: 7141
diff changeset
   453
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   454
7167
wenzelm
parents: 7141
diff changeset
   455
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   456
\subsection{Proof markup commands}\label{sec:markup-prf}
7167
wenzelm
parents: 7141
diff changeset
   457
7987
wenzelm
parents: 7981
diff changeset
   458
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   459
\indexisarcmd{txt}\indexisarcmd{txt-raw}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   460
\begin{matharray}{rcl}
8101
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   461
  \isarcmd{sect} & : & \isartrans{proof}{proof} \\
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   462
  \isarcmd{subsect} & : & \isartrans{proof}{proof} \\
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   463
  \isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   464
  \isarcmd{txt} & : & \isartrans{proof}{proof} \\
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   465
  \isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   466
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   467
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   468
These markup commands for proof mode closely correspond to the ones of theory
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   469
mode (see \S\ref{sec:markup-thy}).  Note that $\isarkeyword{txt_raw}$ is
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   470
special in the same way as $\isarkeyword{text_raw}$.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   471
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   472
\railalias{txtraw}{txt\_raw}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   473
\railterm{txtraw}
7175
wenzelm
parents: 7167
diff changeset
   474
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   475
\begin{rail}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   476
  ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   477
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   478
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   479
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   480
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   481
\subsection{Proof context}\label{sec:proof-context}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   482
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   483
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   484
\indexisarcmd{case}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   485
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   486
  \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   487
  \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   488
  \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   489
  \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   490
  \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   491
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   492
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   493
The logical proof context consists of fixed variables and assumptions.  The
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   494
former closely correspond to Skolem constants, or meta-level universal
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   495
quantification as provided by the Isabelle/Pure logical framework.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   496
Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
7987
wenzelm
parents: 7981
diff changeset
   497
a local value that may be used in the subsequent proof as any other variable
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   498
or constant.  Furthermore, any result $\edrv \phi[x]$ exported from the
7987
wenzelm
parents: 7981
diff changeset
   499
context will be universally closed wrt.\ $x$ at the outermost level: $\edrv
wenzelm
parents: 7981
diff changeset
   500
\All x \phi$ (this is expressed using Isabelle's meta-variables).
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   501
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   502
Similarly, introducing some assumption $\chi$ has two effects.  On the one
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   503
hand, a local theorem is created that may be used as a fact in subsequent
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   504
proof steps.  On the other hand, any result $\chi \drv \phi$ exported from the
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   505
context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   506
Thus, solving an enclosing goal using such a result would basically introduce
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   507
a new subgoal stemming from the assumption.  How this situation is handled
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   508
depends on the actual version of assumption command used: while $\ASSUMENAME$
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   509
insists on solving the subgoal by unification with some premise of the goal,
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   510
$\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   511
user.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   512
7319
wenzelm
parents: 7315
diff changeset
   513
Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
7987
wenzelm
parents: 7981
diff changeset
   514
combining $\FIX x$ with another version of assumption that causes any
wenzelm
parents: 7981
diff changeset
   515
hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
wenzelm
parents: 7981
diff changeset
   516
Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
7175
wenzelm
parents: 7167
diff changeset
   517
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   518
\medskip Basically, Isar proof contexts have to be built up explicitly using
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   519
any of the above commands.  In typical verification tasks this can become hard
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   520
to manage, though, with a large number of local contexts emerging from case
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   521
analysis or induction, for example.  The $\CASENAME$ command provides a
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   522
shorthand to refer to certain parts of logical context symbolically.  Proof
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   523
methods may provide an environment of named ``cases'' of the form $c\colon
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   524
\vec x, \vec \chi$.  Then the effect of $\CASE{c}$ is exactly the same as
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   525
$\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   526
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   527
It is important to note that $\CASENAME$ does \emph{not} provide means to peek
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   528
at the current goal state, which is considered strictly non-observable in
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   529
Isar.  Instead, the cases considered here typically emerge in a canonical way
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   530
from certain pieces of specification that appears in the theory somewhere,
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   531
such as an inductive definition, or recursive function.  See \S\ref{sec:FIXME}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   532
for more details of how this works in HOL.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   533
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   534
\begin{rail}
7431
83e60a678c3a fix: vars;
wenzelm
parents: 7397
diff changeset
   535
  'fix' (vars + 'and') comment?
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   536
  ;
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   537
  ('assume' | 'presume') (assm comment? + 'and')
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   538
  ;
7175
wenzelm
parents: 7167
diff changeset
   539
  'def' thmdecl? \\ var '==' term termpat? comment?
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   540
  ;
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   541
  'case' name
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   542
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   543
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   544
  var: name ('::' type)?
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   545
  ;
7458
bb282845ca77 updated;
wenzelm
parents: 7431
diff changeset
   546
  vars: (name+) ('::' type)?
7431
83e60a678c3a fix: vars;
wenzelm
parents: 7397
diff changeset
   547
  ;
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   548
  assm: thmdecl? (prop proppat? +)
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   549
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   550
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   551
7167
wenzelm
parents: 7141
diff changeset
   552
\begin{descr}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   553
\item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   554
\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   555
  $\Phi$ by assumption.  Subsequent results applied to an enclosing goal
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   556
  (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   557
  able to unify with existing premises in the goal, while $\PRESUMENAME$
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   558
  leaves $\Phi$ as new subgoals.
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   559
  
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   560
  Several lists of assumptions may be given (separated by
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   561
  $\isarkeyword{and}$); the resulting list of current facts consists of all of
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   562
  these concatenated.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   563
\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   564
  In results exported from the context, $x$ is replaced by $t$.  Basically,
7987
wenzelm
parents: 7981
diff changeset
   565
  $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   566
  resulting hypothetical equation solved by reflexivity.
7431
83e60a678c3a fix: vars;
wenzelm
parents: 7397
diff changeset
   567
  
83e60a678c3a fix: vars;
wenzelm
parents: 7397
diff changeset
   568
  The default name for the definitional equation is $x_def$.
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   569
\item [$\CASE{c}$] invokes local context $c\colon \vec x, \vec \chi$, as
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   570
  provided by an appropriate proof method.  This abbreviates $\FIX{\vec
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   571
    x}~\ASSUME{c}{\vec\chi}$.
7167
wenzelm
parents: 7141
diff changeset
   572
\end{descr}
wenzelm
parents: 7141
diff changeset
   573
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   574
The special name $prems$\indexisarthm{prems} refers to all assumptions of the
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   575
current context as a list of theorems.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   576
7167
wenzelm
parents: 7141
diff changeset
   577
wenzelm
parents: 7141
diff changeset
   578
\subsection{Facts and forward chaining}
wenzelm
parents: 7141
diff changeset
   579
wenzelm
parents: 7141
diff changeset
   580
\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
wenzelm
parents: 7141
diff changeset
   581
\begin{matharray}{rcl}
wenzelm
parents: 7141
diff changeset
   582
  \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm
parents: 7141
diff changeset
   583
  \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm
parents: 7141
diff changeset
   584
  \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm
parents: 7141
diff changeset
   585
  \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm
parents: 7141
diff changeset
   586
\end{matharray}
wenzelm
parents: 7141
diff changeset
   587
7319
wenzelm
parents: 7315
diff changeset
   588
New facts are established either by assumption or proof of local statements.
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   589
Any fact will usually be involved in further proofs, either as explicit
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   590
arguments of proof methods or when forward chaining towards the next goal via
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   591
$\THEN$ (and variants).  Note that the special theorem name
7987
wenzelm
parents: 7981
diff changeset
   592
$this$\indexisarthm{this} refers to the most recently established facts.
7167
wenzelm
parents: 7141
diff changeset
   593
\begin{rail}
wenzelm
parents: 7141
diff changeset
   594
  'note' thmdef? thmrefs comment?
wenzelm
parents: 7141
diff changeset
   595
  ;
wenzelm
parents: 7141
diff changeset
   596
  'then' comment?
wenzelm
parents: 7141
diff changeset
   597
  ;
wenzelm
parents: 7141
diff changeset
   598
  ('from' | 'with') thmrefs comment?
wenzelm
parents: 7141
diff changeset
   599
  ;
wenzelm
parents: 7141
diff changeset
   600
\end{rail}
wenzelm
parents: 7141
diff changeset
   601
wenzelm
parents: 7141
diff changeset
   602
\begin{descr}
7175
wenzelm
parents: 7167
diff changeset
   603
\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
wenzelm
parents: 7167
diff changeset
   604
  as $a$.  Note that attributes may be involved as well, both on the left and
wenzelm
parents: 7167
diff changeset
   605
  right hand sides.
7167
wenzelm
parents: 7141
diff changeset
   606
\item [$\THEN$] indicates forward chaining by the current facts in order to
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   607
  establish the goal to be claimed next.  The initial proof method invoked to
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   608
  refine that will be offered the facts to do ``anything appropriate'' (cf.\ 
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   609
  also \S\ref{sec:proof-steps}).  For example, method $rule$ (see
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   610
  \S\ref{sec:pure-meth}) would typically do an elimination rather than an
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   611
  introduction.  Automatic methods usually insert the facts into the goal
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   612
  state before operation.
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   613
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
7458
bb282845ca77 updated;
wenzelm
parents: 7431
diff changeset
   614
  equivalent to $\FROM{this}$.
7175
wenzelm
parents: 7167
diff changeset
   615
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
wenzelm
parents: 7167
diff changeset
   616
  chaining is from earlier facts together with the current ones.
7167
wenzelm
parents: 7141
diff changeset
   617
\end{descr}
wenzelm
parents: 7141
diff changeset
   618
7389
f647f463abeb '_' theorem;
wenzelm
parents: 7335
diff changeset
   619
Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   620
multiple facts to be given in their proper order, corresponding to a prefix of
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   621
the premises of the rule involved.  Note that positions may be easily skipped
7458
bb282845ca77 updated;
wenzelm
parents: 7431
diff changeset
   622
using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example.  This involves
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   623
the trivial rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   624
as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
7389
f647f463abeb '_' theorem;
wenzelm
parents: 7335
diff changeset
   625
7167
wenzelm
parents: 7141
diff changeset
   626
wenzelm
parents: 7141
diff changeset
   627
\subsection{Goal statements}
wenzelm
parents: 7141
diff changeset
   628
wenzelm
parents: 7141
diff changeset
   629
\indexisarcmd{theorem}\indexisarcmd{lemma}
wenzelm
parents: 7141
diff changeset
   630
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
wenzelm
parents: 7141
diff changeset
   631
\begin{matharray}{rcl}
wenzelm
parents: 7141
diff changeset
   632
  \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
wenzelm
parents: 7141
diff changeset
   633
  \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
7987
wenzelm
parents: 7981
diff changeset
   634
  \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
wenzelm
parents: 7981
diff changeset
   635
  \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
7167
wenzelm
parents: 7141
diff changeset
   636
  \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm
parents: 7141
diff changeset
   637
  \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm
parents: 7141
diff changeset
   638
\end{matharray}
wenzelm
parents: 7141
diff changeset
   639
7175
wenzelm
parents: 7167
diff changeset
   640
Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   641
and $\LEMMANAME$.  New local goals may be claimed within proof mode as well.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   642
Four variants are available, indicating whether the result is meant to solve
7987
wenzelm
parents: 7981
diff changeset
   643
some pending goal or whether forward chaining is employed.
7175
wenzelm
parents: 7167
diff changeset
   644
7167
wenzelm
parents: 7141
diff changeset
   645
\begin{rail}
wenzelm
parents: 7141
diff changeset
   646
  ('theorem' | 'lemma') goal
wenzelm
parents: 7141
diff changeset
   647
  ;
wenzelm
parents: 7141
diff changeset
   648
  ('have' | 'show' | 'hence' | 'thus') goal
wenzelm
parents: 7141
diff changeset
   649
  ;
wenzelm
parents: 7141
diff changeset
   650
wenzelm
parents: 7141
diff changeset
   651
  goal: thmdecl? proppat comment?
wenzelm
parents: 7141
diff changeset
   652
  ;
wenzelm
parents: 7141
diff changeset
   653
\end{rail}
wenzelm
parents: 7141
diff changeset
   654
wenzelm
parents: 7141
diff changeset
   655
\begin{descr}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   656
\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   657
  eventually resulting in some theorem $\turn \phi$ put back into the theory.
7987
wenzelm
parents: 7981
diff changeset
   658
\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as
7167
wenzelm
parents: 7141
diff changeset
   659
  ``lemma''.
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   660
\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
7167
wenzelm
parents: 7141
diff changeset
   661
  theorem with the current assumption context as hypotheses.
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   662
\item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   663
  pending goal with the result \emph{exported} into the corresponding context
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   664
  (cf.\ \S\ref{sec:proof-context}).
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   665
\item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   666
  to be proven by forward chaining the current facts.  Note that $\HENCENAME$
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   667
  is also equivalent to $\FROM{this}~\HAVENAME$.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   668
\item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$.  Note that $\THUSNAME$ is
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   669
  also equivalent to $\FROM{this}~\SHOWNAME$.
7167
wenzelm
parents: 7141
diff changeset
   670
\end{descr}
wenzelm
parents: 7141
diff changeset
   671
wenzelm
parents: 7141
diff changeset
   672
wenzelm
parents: 7141
diff changeset
   673
\subsection{Initial and terminal proof steps}\label{sec:proof-steps}
wenzelm
parents: 7141
diff changeset
   674
7175
wenzelm
parents: 7167
diff changeset
   675
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
wenzelm
parents: 7167
diff changeset
   676
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
wenzelm
parents: 7167
diff changeset
   677
\begin{matharray}{rcl}
wenzelm
parents: 7167
diff changeset
   678
  \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
wenzelm
parents: 7167
diff changeset
   679
  \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   680
  \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   681
  \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   682
  \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   683
  \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   684
\end{matharray}
wenzelm
parents: 7167
diff changeset
   685
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   686
Arbitrary goal refinement via tactics is considered harmful.  Consequently the
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   687
Isar framework admits proof methods to be invoked in two places only.
7167
wenzelm
parents: 7141
diff changeset
   688
\begin{enumerate}
7175
wenzelm
parents: 7167
diff changeset
   689
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   690
  goal to a number of sub-goals that are to be solved later.  Facts are passed
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   691
  to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
7167
wenzelm
parents: 7141
diff changeset
   692
  
7987
wenzelm
parents: 7981
diff changeset
   693
\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
wenzelm
parents: 7981
diff changeset
   694
  remaining goals.  No facts are passed to $m@2$.
7167
wenzelm
parents: 7141
diff changeset
   695
\end{enumerate}
wenzelm
parents: 7141
diff changeset
   696
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   697
The only other proper way to affect pending goals is by $\SHOWNAME$ (or
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   698
$\THUSNAME$), which involves an explicit statement of what is to be solved.
7167
wenzelm
parents: 7141
diff changeset
   699
7175
wenzelm
parents: 7167
diff changeset
   700
\medskip
wenzelm
parents: 7167
diff changeset
   701
7167
wenzelm
parents: 7141
diff changeset
   702
Also note that initial proof methods should either solve the goal completely,
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   703
or constitute some well-understood reduction to new sub-goals.  Arbitrary
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   704
automatic proof tools that are prone leave a large number of badly structured
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   705
sub-goals are no help in continuing the proof document in any intelligible
7987
wenzelm
parents: 7981
diff changeset
   706
way.
wenzelm
parents: 7981
diff changeset
   707
%FIXME
wenzelm
parents: 7981
diff changeset
   708
%A more appropriate technique would be to $\SHOWNAME$ some non-trivial
wenzelm
parents: 7981
diff changeset
   709
%reduction as an explicit rule, which is solved completely by some automated
wenzelm
parents: 7981
diff changeset
   710
%method, and then applied to some pending goal.
7167
wenzelm
parents: 7141
diff changeset
   711
7175
wenzelm
parents: 7167
diff changeset
   712
\medskip
wenzelm
parents: 7167
diff changeset
   713
wenzelm
parents: 7167
diff changeset
   714
Unless given explicitly by the user, the default initial method is
wenzelm
parents: 7167
diff changeset
   715
``$default$'', which is usually set up to apply a single standard elimination
7458
bb282845ca77 updated;
wenzelm
parents: 7431
diff changeset
   716
or introduction rule according to the topmost symbol involved.  There is no
7987
wenzelm
parents: 7981
diff changeset
   717
separate default terminal method.  In any case, any goals left after that are
wenzelm
parents: 7981
diff changeset
   718
solved by assumption as the very last step.
7167
wenzelm
parents: 7141
diff changeset
   719
wenzelm
parents: 7141
diff changeset
   720
\begin{rail}
wenzelm
parents: 7141
diff changeset
   721
  'proof' interest? meth? comment?
wenzelm
parents: 7141
diff changeset
   722
  ;
wenzelm
parents: 7141
diff changeset
   723
  'qed' meth? comment?
wenzelm
parents: 7141
diff changeset
   724
  ;
wenzelm
parents: 7141
diff changeset
   725
  'by' meth meth? comment?
wenzelm
parents: 7141
diff changeset
   726
  ;
wenzelm
parents: 7141
diff changeset
   727
  ('.' | '..' | 'sorry') comment?
wenzelm
parents: 7141
diff changeset
   728
  ;
wenzelm
parents: 7141
diff changeset
   729
wenzelm
parents: 7141
diff changeset
   730
  meth: method interest?
wenzelm
parents: 7141
diff changeset
   731
  ;
wenzelm
parents: 7141
diff changeset
   732
\end{rail}
wenzelm
parents: 7141
diff changeset
   733
wenzelm
parents: 7141
diff changeset
   734
\begin{descr}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   735
\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   736
  forward chaining are passed if so indicated by $proof(chain)$ mode.
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   737
\item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   738
  concludes the sub-proof by assumption.  If the goal had been $\SHOWNAME$ (or
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   739
  $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   740
  from the result \emph{exported} into the enclosing goal context.  Thus
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   741
  $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   742
  rule does not fit to any pending goal\footnote{This includes any additional
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   743
    ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   744
  context.  Debugging such a situation might involve temporarily changing
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   745
  $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   746
  some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   747
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
7987
wenzelm
parents: 7981
diff changeset
   748
  abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,
wenzelm
parents: 7981
diff changeset
   749
  though.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   750
  by expanding its definition; in many cases $\PROOF{m@1}$ is already
7175
wenzelm
parents: 7167
diff changeset
   751
  sufficient to see what is going wrong.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   752
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   753
  abbreviates $\BY{default}$.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   754
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
8195
af2575a5c5ae '.' == by this;
wenzelm
parents: 8101
diff changeset
   755
  abbreviates $\BY{this}$.
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   756
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   757
  \texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   758
  goal without further ado.  Of course, the result is a fake theorem only,
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   759
  involving some oracle in its internal derivation object (this is indicated
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   760
  as ``$[!]$'' in the printed result).  The main application of $\SORRY$ is to
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   761
  support experimentation and top-down proof development.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   762
\end{descr}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   763
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   764
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   765
\subsection{Term abbreviations}\label{sec:term-abbrev}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   766
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   767
\indexisarcmd{let}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   768
\begin{matharray}{rcl}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   769
  \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   770
  \isarkeyword{is} & : & syntax \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   771
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   772
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   773
Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
7987
wenzelm
parents: 7981
diff changeset
   774
or by annotating assumptions or goal statements with a list of patterns
wenzelm
parents: 7981
diff changeset
   775
$\ISS{p@1\;\dots}{p@n}$.  In both cases, higher-order matching is invoked to
wenzelm
parents: 7981
diff changeset
   776
bind extra-logical term variables, which may be either named schematic
wenzelm
parents: 7981
diff changeset
   777
variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
wenzelm
parents: 7981
diff changeset
   778
(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
wenzelm
parents: 7981
diff changeset
   779
patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
wenzelm
parents: 7981
diff changeset
   780
postfix position.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   781
7319
wenzelm
parents: 7315
diff changeset
   782
Term abbreviations are quite different from actual local definitions as
wenzelm
parents: 7315
diff changeset
   783
introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   784
visible within the logic as actual equations, while abbreviations disappear
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   785
during the input process just after type checking.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   786
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   787
\begin{rail}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   788
  'let' ((term + 'as') '=' term comment? + 'and')
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   789
  ;  
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   790
\end{rail}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   791
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   792
The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   793
\railnonterm{proppat} (see \S\ref{sec:term-pats}).
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   794
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   795
\begin{descr}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   796
\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   797
  by simultaneous higher-order matching against terms $\vec t$.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   798
\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   799
  preceding statement.  Also note that $\ISNAME$ is not a separate command,
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   800
  but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   801
\end{descr}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   802
7988
wenzelm
parents: 7987
diff changeset
   803
A few \emph{automatic} term abbreviations\index{term abbreviations} for goals
wenzelm
parents: 7987
diff changeset
   804
and facts are available as well.  For any open goal,
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   805
$\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   806
(which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   807
(atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   808
object-logical statement.  The latter two abstract over any meta-level
7987
wenzelm
parents: 7981
diff changeset
   809
parameters.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   810
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   811
Fact statements resulting from assumptions or finished goals are bound as
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   812
$\Var{this_prop}$\indexisarvar{this-prop},
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   813
$\Var{this_concl}$\indexisarvar{this-concl}, and
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   814
$\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above.  In case
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   815
$\Var{this}$ refers to an object-logic statement that is an application
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   816
$f(t)$, then $t$ is bound to the special text variable
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   817
``$\dots$''\indexisarvar{\dots} (three dots).  The canonical application of
7987
wenzelm
parents: 7981
diff changeset
   818
the latter are calculational proofs (see \S\ref{sec:calculation}).
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   819
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   820
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   821
\subsection{Block structure}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   822
7397
wenzelm
parents: 7389
diff changeset
   823
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
wenzelm
parents: 7389
diff changeset
   824
\begin{matharray}{rcl}
wenzelm
parents: 7389
diff changeset
   825
  \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
7974
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   826
  \BG & : & \isartrans{proof(state)}{proof(state)} \\
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   827
  \EN & : & \isartrans{proof(state)}{proof(state)} \\
7397
wenzelm
parents: 7389
diff changeset
   828
\end{matharray}
wenzelm
parents: 7389
diff changeset
   829
7167
wenzelm
parents: 7141
diff changeset
   830
While Isar is inherently block-structured, opening and closing blocks is
wenzelm
parents: 7141
diff changeset
   831
mostly handled rather casually, with little explicit user-intervention.  Any
wenzelm
parents: 7141
diff changeset
   832
local goal statement automatically opens \emph{two} blocks, which are closed
wenzelm
parents: 7141
diff changeset
   833
again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   834
different context within a sub-proof may be switched via $\isarkeyword{next}$,
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   835
which is just a single block-close followed by block-open again.  Thus the
7987
wenzelm
parents: 7981
diff changeset
   836
effect of $\isarkeyword{next}$ to reset the local proof context. There is no
wenzelm
parents: 7981
diff changeset
   837
goal focus involved here!
7167
wenzelm
parents: 7141
diff changeset
   838
7175
wenzelm
parents: 7167
diff changeset
   839
For slightly more advanced applications, there are explicit block parentheses
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   840
as well.  These typically achieve a stronger forward style of reasoning.
7167
wenzelm
parents: 7141
diff changeset
   841
wenzelm
parents: 7141
diff changeset
   842
\begin{descr}
wenzelm
parents: 7141
diff changeset
   843
\item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   844
  resetting the local context to the initial one.
7167
wenzelm
parents: 7141
diff changeset
   845
\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   846
  close blocks.  Any current facts pass through ``$\isarkeyword{\{\{}$''
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   847
  unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   848
  \emph{exported} into the enclosing context.  Thus fixed variables are
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   849
  generalized, assumptions discharged, and local definitions unfolded (cf.\ 
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   850
  \S\ref{sec:proof-context}).  There is no difference of $\ASSUMENAME$ and
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   851
  $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   852
  backward reasoning with the result exported at $\SHOWNAME$ time.
7167
wenzelm
parents: 7141
diff changeset
   853
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   854
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   855
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   856
\section{Other commands}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   857
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   858
\subsection{Diagnostics}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   859
7974
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   860
\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   861
\indexisarcmd{print-facts}\indexisarcmd{print-binds}\indexisarcmd{print-cases}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   862
\begin{matharray}{rcl}
7974
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   863
  \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   864
  \isarcmd{term} & : & \isarkeep{theory~|~proof} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   865
  \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
7974
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   866
  \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   867
  \isarcmd{print_facts} & : & \isarkeep{proof} \\
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   868
  \isarcmd{print_binds} & : & \isarkeep{proof} \\
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   869
  \isarcmd{print_cases} & : & \isarkeep{proof} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   870
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   871
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   872
These commands are not part of the actual Isabelle/Isar syntax, but assist
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   873
interactive development.  Also note that $undo$ does not apply here, since the
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   874
theory or proof configuration is not changed.
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   875
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   876
\begin{rail}
7974
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   877
  'thm' thmrefs
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   878
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   879
  'term' term
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   880
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   881
  'prop' prop
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   882
  ;
7974
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   883
  'typ' type
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   884
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   885
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   886
7167
wenzelm
parents: 7141
diff changeset
   887
\begin{descr}
7974
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   888
\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   889
  theory or proof context.  Note that any attributes included in the theorem
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   890
  specifications are applied to a temporary context derived from the current
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   891
  theory or proof; the result is discarded, i.e.\ attributes involved in
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   892
  $thms$ do not have any permanent effect.
7987
wenzelm
parents: 7981
diff changeset
   893
\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-check and
wenzelm
parents: 7981
diff changeset
   894
  print terms or propositions according to the current theory or proof
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   895
  context; the inferred type of $t$ is output as well.  Note that these
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   896
  commands are also useful in inspecting the current environment of term
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   897
  abbreviations.
7974
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   898
\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
   899
  according to the current theory or proof context.
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   900
\item [$\isarkeyword{print_facts}$] prints any named facts of the current
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   901
  context, including assumptions and local results.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   902
\item [$\isarkeyword{print_binds}$] prints all term abbreviations present in
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   903
  the context.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   904
\item [$\isarkeyword{print_cases}$] prints all local contexts (also known as
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   905
  ``cases'') of the current goal context.
7167
wenzelm
parents: 7141
diff changeset
   906
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   907
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   908
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   909
\subsection{Meta-linguistic features}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   910
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   911
\indexisarcmd{oops}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   912
\begin{matharray}{rcl}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   913
  \isarcmd{oops}^* & : & \isartrans{proof}{theory} \\
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   914
\end{matharray}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   915
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   916
The $\OOPS$ command discontinues the current proof attempt, while considering
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   917
the partial proof text as properly processed.  This is conceptually quite
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   918
different from ``faking'' actual proofs via $\SORRY$ (see
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   919
\S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all,
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   920
but goes back right to the theory level.  Furthermore, $\OOPS$ does not
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   921
produce any result theorem --- there is no claim to be able to complete the
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   922
proof anyhow.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   923
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   924
A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   925
system itself, in conjunction with the document preparation tools of Isabelle
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   926
described in \cite{isabelle-sys}.  Thus partial or even wrong proof attempts
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   927
can be discussed in a logically sound manner.  Note that the Isabelle {\LaTeX}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   928
macros can be easily adapted to print something like ``$\dots$'' instead of an
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   929
``$\OOPS$'' keyword.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   930
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   931
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   932
\subsection{System operations}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   933
7167
wenzelm
parents: 7141
diff changeset
   934
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
wenzelm
parents: 7141
diff changeset
   935
\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   936
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   937
  \isarcmd{cd} & : & \isarkeep{\cdot} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   938
  \isarcmd{pwd} & : & \isarkeep{\cdot} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   939
  \isarcmd{use_thy} & : & \isarkeep{\cdot} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   940
  \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   941
  \isarcmd{update_thy} & : & \isarkeep{\cdot} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   942
  \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   943
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   944
7167
wenzelm
parents: 7141
diff changeset
   945
\begin{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   946
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   947
  process.
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   948
\item [$\isarkeyword{pwd}~$] prints the current working directory.
7175
wenzelm
parents: 7167
diff changeset
   949
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
7987
wenzelm
parents: 7981
diff changeset
   950
  $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   951
  theory given as $name$ argument.  These commands are basically the same as
7987
wenzelm
parents: 7981
diff changeset
   952
  the corresponding ML functions\footnote{The ML versions also change the
wenzelm
parents: 7981
diff changeset
   953
    implicit theory context to that of the theory loaded.}  (see also
wenzelm
parents: 7981
diff changeset
   954
  \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar versions may
wenzelm
parents: 7981
diff changeset
   955
  load new- and old-style theories alike.
7167
wenzelm
parents: 7141
diff changeset
   956
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   957
7987
wenzelm
parents: 7981
diff changeset
   958
These system commands are scarcely used when working with the Proof~General
wenzelm
parents: 7981
diff changeset
   959
interface, since loading of theories is done fully transparently.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   960
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   961
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   962
\subsection{Emulating tactic scripts}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   963
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   964
The following elements emulate unstructured tactic scripts to some extent.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   965
While these are anathema for writing proper Isar proof documents, they might
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   966
come in handy for interactive exploration and debugging.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   967
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   968
\indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{back}\indexisarmeth{tactic}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   969
\begin{matharray}{rcl}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   970
  \isarcmd{apply} & : & \isartrans{proof(prove)}{proof(prove)} \\
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   971
  \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   972
  tactic & : & \isarmeth \\
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   973
  \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   974
\end{matharray}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   975
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   976
\railalias{applyend}{apply\_end}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   977
\railterm{applyend}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   978
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   979
\begin{rail}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   980
  'apply' method
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   981
  ;
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   982
  applyend method
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   983
  ;
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   984
  'tactic' text
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   985
  ;
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   986
  'back'
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   987
  ;
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   988
\end{rail}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   989
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   990
\begin{descr}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   991
\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in an initial
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   992
  position, but retains ``$prove$'' mode (unlike $\PROOFNAME$).  Thus
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   993
  consecutive method applications may be given just as in tactic scripts.  In
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   994
  order to complete the proof properly, any of the actual structured proof
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   995
  commands (e.g.\ ``$\DOT$'') has to be given eventually.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   996
  
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   997
  Facts are passed to $m$ as indicated by the goal's forward-chain mode.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   998
  Common use of $\isarkeyword{apply}$ would be in a purely backward manner,
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   999
  though.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1000
\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1001
  terminal position.  Basically, this simulates a multi-step tactic script for
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1002
  $\QEDNAME$, but may be given anywhere within the proof body.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1003
  
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1004
  No facts are passed to $m$.  Furthermore, the static context is that of the
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1005
  enclosing goal (as for actual $\QEDNAME$).  Thus the proof method may not
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1006
  refer to any assumptions introduced in the current body, for example.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1007
\item [$tactic~text$] produces a proof method from any ML text of type
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1008
  \texttt{tactic}.  Apart from the usual ML environment, and the current
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1009
  implicit theory context, the ML code may refer to the following locally
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1010
  bound values:
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1011
  \begin{ttbox}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1012
val ctxt  : Proof.context
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1013
val facts : thm list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1014
val thm   : string -> thm
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1015
val thms  : string -> thm list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1016
  \end{ttbox}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1017
  Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1018
  indicates any current facts for forward-chaining, and
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1019
  \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1020
  theorems) from the context.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1021
\item [$\isarkeyword{back}$] does back-tracking over the result sequence of
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1022
  the latest proof command.\footnote{Unlike the ML function \texttt{back}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1023
    \cite{isabelle-ref}, the Isar command does not search upwards for further
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1024
    branch points.} Basically, any proof command may return multiple results.
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1025
\end{descr}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1026
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
  1027
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
  1028
%%% Local Variables: 
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
  1029
%%% mode: latex
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
  1030
%%% TeX-master: "isar-ref"
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
  1031
%%% End: