doc-src/IsarRef/pure.tex
author wenzelm
Sun, 13 Jun 2004 15:30:08 +0200
changeset 14934 bf9f525d4821
parent 14817 321ff6bf29d1
child 14955 08ee855c1d94
permissions -rw-r--r--
added display_drafts and print_drafts commands;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     1
13048
wenzelm
parents: 13042
diff changeset
     2
\chapter{Basic language elements}\label{ch:pure-syntax}
7167
wenzelm
parents: 7141
diff changeset
     3
13039
wenzelm
parents: 13024
diff changeset
     4
Subsequently, we introduce the main part of Pure theory and proof commands,
wenzelm
parents: 13024
diff changeset
     5
together with fundamental proof methods and attributes.
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
     6
Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
     7
tools and packages (such as the Simplifier) that are either part of Pure
12879
wenzelm
parents: 12621
diff changeset
     8
Isabelle or pre-installed in most object logics.  Chapter~\ref{ch:logics}
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
     9
refers to object-logic specific elements (mainly for HOL and ZF).
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
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
    16
are subsequently marked by ``$^*$'', are often helpful when developing proof
13039
wenzelm
parents: 13024
diff changeset
    17
documents, while their use is discouraged for the final human-readable
wenzelm
parents: 13024
diff changeset
    18
outcome.  Typical examples are diagnostic commands that print terms or
wenzelm
parents: 13024
diff changeset
    19
theorems according to the current context; other commands emulate old-style
wenzelm
parents: 13024
diff changeset
    20
tactical theorem proving.
7167
wenzelm
parents: 7141
diff changeset
    21
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    22
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    23
\section{Theory commands}
7134
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
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    27
\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{context}\indexisarcmd{end}
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} \\
8510
863bc8086f62 fixed theory, context typing;
wenzelm
parents: 8485
diff changeset
    30
  \isarcmd{theory} & : & \isartrans{toplevel}{theory} \\
863bc8086f62 fixed theory, context typing;
wenzelm
parents: 8485
diff changeset
    31
  \isarcmd{context}^* & : & \isartrans{toplevel}{theory} \\
863bc8086f62 fixed theory, context typing;
wenzelm
parents: 8485
diff changeset
    32
  \isarcmd{end} & : & \isartrans{theory}{toplevel} \\
7134
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
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    41
The first ``real'' command of any theory has to be $\THEORY$, which starts a
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    42
new theory based on the merge of existing ones.  Just preceding $\THEORY$,
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    43
there may be an optional $\isarkeyword{header}$ declaration, which is relevant
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    44
to document preparation only; it acts very much like a special pre-theory
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    45
markup command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}).  The
13039
wenzelm
parents: 13024
diff changeset
    46
$\END$ command concludes a theory development; it has to be the very last
wenzelm
parents: 13024
diff changeset
    47
command of any theory file loaded in batch-mode.  The theory context may be
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    48
also changed interactively by $\CONTEXT$ without creating a new theory.
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
7167
wenzelm
parents: 7141
diff changeset
    58
  filespecs: 'files' ((name | parname) +);
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    59
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    60
7167
wenzelm
parents: 7141
diff changeset
    61
\begin{descr}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    62
\item [$\isarkeyword{header}~text$] provides plain text markup just preceding
8547
wenzelm
parents: 8533
diff changeset
    63
  the formal beginning of a theory.  In actual document preparation the
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    64
  corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    65
  produce chapter or section headings.  See also \S\ref{sec:markup-thy} and
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    66
  \S\ref{sec:markup-prf} for further markup commands.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    67
  
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    68
\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] starts a new theory $A$ based
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    69
  on the merge of existing theories $B@1, \dots, B@n$.
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    70
  
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    71
  Due to inclusion of several ancestors, the overall theory structure emerging
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    72
  in an Isabelle session forms a directed acyclic graph (DAG).  Isabelle's
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    73
  theory loader ensures that the sources contributing to the development graph
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    74
  are always up-to-date.  Changed files are automatically reloaded when
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    75
  processing theory headers interactively; batch-mode explicitly distinguishes
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    76
  \verb,update_thy, from \verb,use_thy,, see also \cite{isabelle-ref}.
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    77
  
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    78
  The optional $\isarkeyword{files}$ specification declares additional
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    79
  dependencies on ML files.  Files will be loaded immediately, unless the name
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    80
  is put in parentheses, which merely documents the dependency to be resolved
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    81
  later in the text (typically via explicit $\isarcmd{use}$ in the body text,
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    82
  see \S\ref{sec:ML}).  In reminiscence of the old-style theory system of
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    83
  Isabelle, \texttt{$A$.thy} may be also accompanied by an additional file
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    84
  \texttt{$A$.ML} consisting of ML code that is executed in the context of the
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    85
  \emph{finished} theory $A$.  That file should not be included in the
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    86
  $\isarkeyword{files}$ dependency declaration, though.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
    87
  
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
    88
\item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
7981
wenzelm
parents: 7974
diff changeset
    89
  mode, so only a limited set of commands may be performed without destroying
wenzelm
parents: 7974
diff changeset
    90
  the theory.  Just as for $\THEORY$, the theory loader ensures that $B$ is
wenzelm
parents: 7974
diff changeset
    91
  loaded and up-to-date.
7175
wenzelm
parents: 7167
diff changeset
    92
  
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    93
  This command is occasionally useful for quick interactive experiments;
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    94
  normally one should always commence a new context via $\THEORY$.
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    95
  
7167
wenzelm
parents: 7141
diff changeset
    96
\item [$\END$] concludes the current theory definition or context switch.
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    97
  Note that this command cannot be undone, but the whole theory definition has
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    98
  to be retracted.
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
    99
7167
wenzelm
parents: 7141
diff changeset
   100
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   101
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   102
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   103
\subsection{Markup commands}\label{sec:markup-thy}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   104
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   105
\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   106
\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   107
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   108
  \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
7167
wenzelm
parents: 7141
diff changeset
   109
  \isarcmd{section} & : & \isartrans{theory}{theory} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   110
  \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   111
  \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   112
  \isarcmd{text} & : & \isartrans{theory}{theory} \\
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   113
  \isarcmd{text_raw} & : & \isartrans{theory}{theory} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   114
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   115
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   116
Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
7981
wenzelm
parents: 7974
diff changeset
   117
a structured way to insert text into the document generated from a theory (see
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   118
\cite{isabelle-sys} for more information on Isabelle's document preparation
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   119
tools).
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   120
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   121
\railalias{textraw}{text\_raw}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   122
\railterm{textraw}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   123
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   124
\begin{rail}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   125
  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   126
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   127
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   128
7167
wenzelm
parents: 7141
diff changeset
   129
\begin{descr}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   130
\item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   131
  $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   132
  and section headings.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   133
\item [$\TEXT$] specifies paragraphs of plain text, including references to
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   134
  formal entities (see also \S\ref{sec:antiq} on ``antiquotations'').
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   135
\item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   136
  without additional markup.  Thus the full range of document manipulations
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   137
  becomes available.
7167
wenzelm
parents: 7141
diff changeset
   138
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   139
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   140
Any of these markup elements corresponds to a {\LaTeX} command with the name
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   141
prefixed by \verb,\isamarkup,.  For the sectioning commands this is a plain
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   142
macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   143
$\isarkeyword{chapter}$.  The $\isarkeyword{text}$ markup results in a
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   144
{\LaTeX} environment \verb,\begin{isamarkuptext}, {\dots}
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   145
  \verb,\end{isamarkuptext},, while $\isarkeyword{text_raw}$ causes the text
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   146
to be inserted directly into the {\LaTeX} source.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   147
8485
80ddf678e533 moved "cases" to generic.tex;
wenzelm
parents: 8448
diff changeset
   148
\medskip
80ddf678e533 moved "cases" to generic.tex;
wenzelm
parents: 8448
diff changeset
   149
80ddf678e533 moved "cases" to generic.tex;
wenzelm
parents: 8448
diff changeset
   150
Additional markup commands are available for proofs (see
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   151
\S\ref{sec:markup-prf}).  Also note that the $\isarkeyword{header}$
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   152
declaration (see \S\ref{sec:begin-thy}) admits to insert section markup just
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   153
preceding the actual theory definition.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   154
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   155
7135
wenzelm
parents: 7134
diff changeset
   156
\subsection{Type classes and sorts}\label{sec:classes}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   157
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   158
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   159
\begin{matharray}{rcll}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   160
  \isarcmd{classes} & : & \isartrans{theory}{theory} \\
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   161
  \isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   162
  \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   163
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   164
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   165
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   166
  'classes' (classdecl +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   167
  ;
14817
321ff6bf29d1 'classrel': support multiple arguments;
wenzelm
parents: 14642
diff changeset
   168
  'classrel' (nameref ('<' | subseteq) nameref + 'and')
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   169
  ;
12879
wenzelm
parents: 12621
diff changeset
   170
  'defaultsort' sort
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   171
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   172
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   173
7167
wenzelm
parents: 7141
diff changeset
   174
\begin{descr}
11100
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11017
diff changeset
   175
\item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11017
diff changeset
   176
  subclass of existing classes $\vec c$.  Cyclic class structures are ruled
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11017
diff changeset
   177
  out.
14817
321ff6bf29d1 'classrel': support multiple arguments;
wenzelm
parents: 14642
diff changeset
   178
\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states subclass relations
11100
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 11017
diff changeset
   179
  between existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
10223
wenzelm
parents: 10160
diff changeset
   180
  $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce
wenzelm
parents: 10160
diff changeset
   181
  proven class relations.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   182
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   183
  any type variables given without sort constraints.  Usually, the default
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   184
  sort would be only changed when defining a new object-logic.
7167
wenzelm
parents: 7141
diff changeset
   185
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   186
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   187
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   188
\subsection{Primitive types and type abbreviations}\label{sec:types-pure}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   189
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   190
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   191
\begin{matharray}{rcll}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   192
  \isarcmd{types} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   193
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   194
  \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   195
  \isarcmd{arities} & : & \isartrans{theory}{theory} & (axiomatic!) \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   196
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   197
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   198
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   199
  'types' (typespec '=' type infix? +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   200
  ;
12879
wenzelm
parents: 12621
diff changeset
   201
  'typedecl' typespec infix?
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   202
  ;
12879
wenzelm
parents: 12621
diff changeset
   203
  'nonterminals' (name +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   204
  ;
12879
wenzelm
parents: 12621
diff changeset
   205
  'arities' (nameref '::' arity +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   206
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   207
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   208
7167
wenzelm
parents: 7141
diff changeset
   209
\begin{descr}
13039
wenzelm
parents: 13024
diff changeset
   210
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   211
\item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   212
  $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   213
  as are available in Isabelle/HOL for example, type synonyms are just purely
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   214
  syntactic abbreviations without any logical significance.  Internally, type
7981
wenzelm
parents: 7974
diff changeset
   215
  synonyms are fully expanded.
13039
wenzelm
parents: 13024
diff changeset
   216
  
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   217
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
13039
wenzelm
parents: 13024
diff changeset
   218
  $t$, intended as an actual logical type.  Note that the Isabelle/HOL
wenzelm
parents: 13024
diff changeset
   219
  object-logic overrides $\isarkeyword{typedecl}$ by its own version
wenzelm
parents: 13024
diff changeset
   220
  (\S\ref{sec:hol-typedef}).
wenzelm
parents: 13024
diff changeset
   221
7175
wenzelm
parents: 7167
diff changeset
   222
\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
wenzelm
parents: 7167
diff changeset
   223
  $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
wenzelm
parents: 7167
diff changeset
   224
  Isabelle's inner syntax of terms or types.
13039
wenzelm
parents: 13024
diff changeset
   225
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   226
\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   227
  signature of types by new type constructor arities.  This is done
10223
wenzelm
parents: 10160
diff changeset
   228
  axiomatically!  The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a
wenzelm
parents: 10160
diff changeset
   229
  way to introduce proven type arities.
13039
wenzelm
parents: 13024
diff changeset
   230
7167
wenzelm
parents: 7141
diff changeset
   231
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   232
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   233
7981
wenzelm
parents: 7974
diff changeset
   234
\subsection{Constants and simple definitions}\label{sec:consts}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   235
7175
wenzelm
parents: 7167
diff changeset
   236
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   237
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   238
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   239
  \isarcmd{defs} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   240
  \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   241
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   242
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   243
\begin{rail}
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   244
  'consts' ((name '::' type mixfix?) +)
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   245
  ;
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   246
  'defs' ('(' 'overloaded' ')')? (axmdecl prop +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   247
  ;
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   248
\end{rail}
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   249
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   250
\begin{rail}
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   251
  'constdefs' structs? (constdecl? constdef +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   252
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   253
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   254
  structs: '(' 'structure' (vars + 'and') ')'
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   255
  ;
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   256
  constdecl: (name '::' type) mixfix | (name '::' type) | name 'where' | mixfix
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   257
  ;
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   258
  constdef: thmdecl? prop
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   259
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   260
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   261
7167
wenzelm
parents: 7141
diff changeset
   262
\begin{descr}
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   263
\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   264
  scheme $\sigma$.  The optional mixfix annotations may attach concrete syntax
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   265
  to the constants declared.
9308
4adf25becaa4 defs: (overloaded) option;
wenzelm
parents: 9273
diff changeset
   266
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   267
\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   268
  existing constant.  See \cite[\S6]{isabelle-ref} for more details on the
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   269
  form of equations admitted as constant definitions.
9308
4adf25becaa4 defs: (overloaded) option;
wenzelm
parents: 9273
diff changeset
   270
  
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   271
  The $(overloaded)$ option declares definitions to be potentially overloaded.
9308
4adf25becaa4 defs: (overloaded) option;
wenzelm
parents: 9273
diff changeset
   272
  Unless this option is given, a warning message would be issued for any
4adf25becaa4 defs: (overloaded) option;
wenzelm
parents: 9273
diff changeset
   273
  definitional equation with a more special type than that of the
4adf25becaa4 defs: (overloaded) option;
wenzelm
parents: 9273
diff changeset
   274
  corresponding constant declaration.
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   275
  
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   276
\item [$\CONSTDEFS$] provides a streamlined combination of constants
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   277
  declarations and definitions: type-inference takes care of the most general
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   278
  typing of the given specification (the optional type constraint may refer to
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   279
  type-inference dummies ``$_$'' as usual).  The resulting type declaration
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   280
  needs to agree with that of the specification; overloading is \emph{not}
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   281
  supported here!
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   282
  
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   283
  The constant name may be omitted altogether, if neither type nor syntax
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   284
  declarations are given.  The canonical name of the definitional axiom for
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   285
  constant $c$ will be $c_def$, unless specified otherwise.  Also note that
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   286
  the given list of specifications is processed in a strictly sequential
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   287
  manner, with type-checking being performed independently.
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   288
  
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   289
  An optional initial context of $(structure)$ declarations admits use of
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   290
  indexed syntax, using the special symbol \verb,\<index>, (printed as
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   291
  ``\i'').  The latter concept is particularly useful with locales (see also
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   292
  \S\ref{sec:locale}).
7167
wenzelm
parents: 7141
diff changeset
   293
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   294
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   295
7981
wenzelm
parents: 7974
diff changeset
   296
\subsection{Syntax and translations}\label{sec:syn-trans}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   297
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   298
\indexisarcmd{syntax}\indexisarcmd{translations}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   299
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   300
  \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   301
  \isarcmd{translations} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   302
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   303
10640
562e20e543b1 alternative syntax for "translations": harpoons;
wenzelm
parents: 10584
diff changeset
   304
\railalias{rightleftharpoons}{\isasymrightleftharpoons}
562e20e543b1 alternative syntax for "translations": harpoons;
wenzelm
parents: 10584
diff changeset
   305
\railterm{rightleftharpoons}
562e20e543b1 alternative syntax for "translations": harpoons;
wenzelm
parents: 10584
diff changeset
   306
562e20e543b1 alternative syntax for "translations": harpoons;
wenzelm
parents: 10584
diff changeset
   307
\railalias{rightharpoonup}{\isasymrightharpoonup}
562e20e543b1 alternative syntax for "translations": harpoons;
wenzelm
parents: 10584
diff changeset
   308
\railterm{rightharpoonup}
562e20e543b1 alternative syntax for "translations": harpoons;
wenzelm
parents: 10584
diff changeset
   309
562e20e543b1 alternative syntax for "translations": harpoons;
wenzelm
parents: 10584
diff changeset
   310
\railalias{leftharpoondown}{\isasymleftharpoondown}
562e20e543b1 alternative syntax for "translations": harpoons;
wenzelm
parents: 10584
diff changeset
   311
\railterm{leftharpoondown}
562e20e543b1 alternative syntax for "translations": harpoons;
wenzelm
parents: 10584
diff changeset
   312
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   313
\begin{rail}
9727
5e18de753e0f 'syntax': improved mode spec;
wenzelm
parents: 9695
diff changeset
   314
  'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   315
  ;
12879
wenzelm
parents: 12621
diff changeset
   316
  'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   317
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   318
  transpat: ('(' nameref ')')? string
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   319
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   320
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   321
7167
wenzelm
parents: 7141
diff changeset
   322
\begin{descr}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   323
  
7175
wenzelm
parents: 7167
diff changeset
   324
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
wenzelm
parents: 7167
diff changeset
   325
  except that the actual logical signature extension is omitted.  Thus the
wenzelm
parents: 7167
diff changeset
   326
  context free grammar of Isabelle's inner syntax may be augmented in
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   327
  arbitrary ways, independently of the logic.  The $mode$ argument refers to
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   328
  the print mode that the grammar rules belong; unless the
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   329
  $\isarkeyword{output}$ indicator is given, all productions are added both to
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   330
  the input and output grammar.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   331
  
7175
wenzelm
parents: 7167
diff changeset
   332
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   333
  rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   334
  rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   335
  Translation patterns may be prefixed by the syntactic category to be used
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   336
  for parsing; the default is $logic$.
7167
wenzelm
parents: 7141
diff changeset
   337
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   338
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   339
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
   340
\subsection{Axioms and theorems}\label{sec:axms-thms}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   341
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   342
\indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems}
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   343
\begin{matharray}{rcll}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   344
  \isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   345
  \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   346
  \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   347
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   348
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   349
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   350
  'axioms' (axmdecl prop +)
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   351
  ;
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
   352
  ('lemmas' | 'theorems') locale? (thmdef? thmrefs + 'and')
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   353
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   354
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   355
7167
wenzelm
parents: 7141
diff changeset
   356
\begin{descr}
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
   357
  
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   358
\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   359
  axioms of the meta-logic.  In fact, axioms are ``axiomatic theorems'', and
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   360
  may be referred later just as any other theorem.
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   361
  
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   362
  Axioms are usually only introduced when declaring new logical systems.
7175
wenzelm
parents: 7167
diff changeset
   363
  Everyday work is typically done the hard way, with proper definitions and
13039
wenzelm
parents: 13024
diff changeset
   364
  proven theorems.
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
   365
  
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
   366
\item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores existing facts
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
   367
  in the theory context, or the specified locale (see also
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
   368
  \S\ref{sec:locale}).  Typical applications would also involve attributes, to
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
   369
  declare Simplifier rules, for example.
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
   370
  
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   371
\item [$\isarkeyword{theorems}$] is essentially the same as
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   372
  $\isarkeyword{lemmas}$, but marks the result as a different kind of facts.
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
   373
7167
wenzelm
parents: 7141
diff changeset
   374
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   375
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   376
7167
wenzelm
parents: 7141
diff changeset
   377
\subsection{Name spaces}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   378
8726
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   379
\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   380
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   381
  \isarcmd{global} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   382
  \isarcmd{local} & : & \isartrans{theory}{theory} \\
8726
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   383
  \isarcmd{hide} & : & \isartrans{theory}{theory} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   384
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   385
8726
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   386
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   387
  'hide' name (nameref + )
8726
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   388
  ;
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   389
\end{rail}
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   390
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   391
Isabelle organizes any kind of name declarations (of types, constants,
8547
wenzelm
parents: 8533
diff changeset
   392
theorems etc.) by separate hierarchically structured name spaces.  Normally
8726
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   393
the user does not have to control the behavior of name spaces by hand, yet the
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   394
following commands provide some way to do so.
7175
wenzelm
parents: 7167
diff changeset
   395
7167
wenzelm
parents: 7141
diff changeset
   396
\begin{descr}
wenzelm
parents: 7141
diff changeset
   397
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
wenzelm
parents: 7141
diff changeset
   398
  name declaration mode.  Initially, theories start in $\isarkeyword{local}$
wenzelm
parents: 7141
diff changeset
   399
  mode, causing all names to be automatically qualified by the theory name.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   400
  Changing this to $\isarkeyword{global}$ causes all names to be declared
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   401
  without the theory prefix, until $\isarkeyword{local}$ is declared again.
8726
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   402
  
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   403
  Note that global names are prone to get hidden accidently later, when
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   404
  qualified names of the same base name are introduced.
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   405
  
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   406
\item [$\isarkeyword{hide}~space~names$] removes declarations from a given
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   407
  name space (which may be $class$, $type$, or $const$).  Hidden objects
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   408
  remain valid within the logic, but are inaccessible from user input.  In
7b15f4bdd72f 'global' / 'local': comment;
wenzelm
parents: 8696
diff changeset
   409
  output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   410
  full internal name.  Unqualified (global) names may not be hidden.
7167
wenzelm
parents: 7141
diff changeset
   411
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   412
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   413
7167
wenzelm
parents: 7141
diff changeset
   414
\subsection{Incorporating ML code}\label{sec:ML}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   415
8682
82ebf8618e6b added 'ML_command';
wenzelm
parents: 8664
diff changeset
   416
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-command}
82ebf8618e6b added 'ML_command';
wenzelm
parents: 8664
diff changeset
   417
\indexisarcmd{ML-setup}\indexisarcmd{setup}
9199
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   418
\indexisarcmd{method-setup}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   419
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   420
  \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   421
  \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
8682
82ebf8618e6b added 'ML_command';
wenzelm
parents: 8664
diff changeset
   422
  \isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   423
  \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
7175
wenzelm
parents: 7167
diff changeset
   424
  \isarcmd{setup} & : & \isartrans{theory}{theory} \\
9199
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   425
  \isarcmd{method_setup} & : & \isartrans{theory}{theory} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   426
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   427
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   428
\railalias{MLsetup}{ML\_setup}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   429
\railterm{MLsetup}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   430
9199
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   431
\railalias{methodsetup}{method\_setup}
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   432
\railterm{methodsetup}
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   433
8682
82ebf8618e6b added 'ML_command';
wenzelm
parents: 8664
diff changeset
   434
\railalias{MLcommand}{ML\_command}
82ebf8618e6b added 'ML_command';
wenzelm
parents: 8664
diff changeset
   435
\railterm{MLcommand}
82ebf8618e6b added 'ML_command';
wenzelm
parents: 8664
diff changeset
   436
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   437
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   438
  'use' name
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   439
  ;
12879
wenzelm
parents: 12621
diff changeset
   440
  ('ML' | MLcommand | MLsetup | 'setup') text
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   441
  ;
12879
wenzelm
parents: 12621
diff changeset
   442
  methodsetup name '=' text text
9199
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   443
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   444
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   445
7167
wenzelm
parents: 7141
diff changeset
   446
\begin{descr}
7175
wenzelm
parents: 7167
diff changeset
   447
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   448
  The current theory context (if present) is passed down to the ML session,
7981
wenzelm
parents: 7974
diff changeset
   449
  but may not be modified.  Furthermore, the file name is checked with the
7466
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   450
  $\isarkeyword{files}$ dependency declaration given in the theory header (see
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   451
  also \S\ref{sec:begin-thy}).
7df66ce6508a updated;
wenzelm
parents: 7458
diff changeset
   452
  
8682
82ebf8618e6b added 'ML_command';
wenzelm
parents: 8664
diff changeset
   453
\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML
82ebf8618e6b added 'ML_command';
wenzelm
parents: 8664
diff changeset
   454
  commands from $text$.  The theory context is passed in the same way as for
10858
wenzelm
parents: 10686
diff changeset
   455
  $\isarkeyword{use}$, but may not be changed.  Note that the output of
8682
82ebf8618e6b added 'ML_command';
wenzelm
parents: 8664
diff changeset
   456
  $\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   457
  
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   458
\item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$.  The
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   459
  theory context is passed down to the ML session, and fetched back
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   460
  afterwards.  Thus $text$ may actually change the theory as a side effect.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   461
  
7167
wenzelm
parents: 7141
diff changeset
   462
\item [$\isarkeyword{setup}~text$] changes the current theory context by
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   463
  applying $text$, which refers to an ML expression of type
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   464
  \texttt{(theory~->~theory)~list}.  The $\isarkeyword{setup}$ command is the
8547
wenzelm
parents: 8533
diff changeset
   465
  canonical way to initialize any object-logic specific tools and packages
wenzelm
parents: 8533
diff changeset
   466
  written in ML.
9199
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   467
  
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   468
\item [$\isarkeyword{method_setup}~name = text~description$] defines a proof
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   469
  method in the current theory.  The given $text$ has to be an ML expression
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   470
  of type \texttt{Args.src -> Proof.context -> Proof.method}.  Parsing
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   471
  concrete method syntax from \texttt{Args.src} input can be quite tedious in
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   472
  general.  The following simple examples are for methods without any explicit
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   473
  arguments, or a list of theorems, respectively.
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   474
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   475
{\footnotesize
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   476
\begin{verbatim}
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
   477
 Method.no_args (Method.METHOD (fn facts => foobar_tac))
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
   478
 Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
10899
5de31ddf9c03 more method_setup examples;
wenzelm
parents: 10858
diff changeset
   479
 Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   480
 Method.thms_ctxt_args (fn thms => fn ctxt =>
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   481
    Method.METHOD (fn facts => foobar_tac))
9199
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   482
\end{verbatim}
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   483
}
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   484
7a1a856f0571 facts: support multiple lists of arguments;
wenzelm
parents: 9030
diff changeset
   485
Note that mere tactic emulations may ignore the \texttt{facts} parameter
13039
wenzelm
parents: 13024
diff changeset
   486
above.  Proper proof methods would do something appropriate with the list of
wenzelm
parents: 13024
diff changeset
   487
current facts, though.  Single-rule methods usually do strict forward-chaining
wenzelm
parents: 13024
diff changeset
   488
(e.g.\ by using \texttt{Method.multi_resolves}), while automatic ones just
wenzelm
parents: 13024
diff changeset
   489
insert the facts using \texttt{Method.insert_tac} before applying the main
wenzelm
parents: 13024
diff changeset
   490
tactic.
7167
wenzelm
parents: 7141
diff changeset
   491
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   492
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   493
8250
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   494
\subsection{Syntax translation functions}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   495
8250
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   496
\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   497
\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   498
\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   499
\begin{matharray}{rcl}
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   500
  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   501
  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   502
  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   503
  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   504
  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   505
  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   506
\end{matharray}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   507
9273
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   508
\railalias{parseasttranslation}{parse\_ast\_translation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   509
\railterm{parseasttranslation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   510
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   511
\railalias{parsetranslation}{parse\_translation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   512
\railterm{parsetranslation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   513
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   514
\railalias{printtranslation}{print\_translation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   515
\railterm{printtranslation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   516
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   517
\railalias{typedprinttranslation}{typed\_print\_translation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   518
\railterm{typedprinttranslation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   519
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   520
\railalias{printasttranslation}{print\_ast\_translation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   521
\railterm{printasttranslation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   522
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   523
\railalias{tokentranslation}{token\_translation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   524
\railterm{tokentranslation}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   525
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   526
\begin{rail}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   527
  ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   528
  printasttranslation ) ('(' 'advanced' ')')? text;
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   529
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   530
  tokentranslation text
9273
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   531
\end{rail}
798673f65f02 allow comment in more commands;
wenzelm
parents: 9238
diff changeset
   532
8250
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   533
Syntax translation functions written in ML admit almost arbitrary
f4029c34adef Syntax translation functions;
wenzelm
parents: 8207
diff changeset
   534
manipulations of Isabelle's inner syntax.  Any of the above commands have a
13048
wenzelm
parents: 13042
diff changeset
   535
single \railqtok{text} argument that refers to an ML expression of appropriate
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   536
type, which are as follows by default:
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   537
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   538
\begin{ttbox}
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   539
val parse_ast_translation   : (string * (ast list -> ast)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   540
val parse_translation       : (string * (term list -> term)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   541
val print_translation       : (string * (term list -> term)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   542
val typed_print_translation :
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   543
  (string * (bool -> typ -> term list -> term)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   544
val print_ast_translation   : (string * (ast list -> ast)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   545
val token_translation       :
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   546
  (string * string * (string -> string * real)) list
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   547
\end{ttbox}
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   548
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   549
In case that the $(advanced)$ option is given, the corresponding translation
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   550
functions may depend on the signature of the current theory context.  This
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   551
allows to implement advanced syntax mechanisms, as translations functions may
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   552
refer to specific theory declarations and auxiliary data.
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   553
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   554
See also \cite[\S8]{isabelle-ref} for more information on the general concept
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   555
of syntax transformations in Isabelle.
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   556
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   557
\begin{ttbox}
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   558
val parse_ast_translation:
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   559
  (string * (Sign.sg -> ast list -> ast)) list
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   560
val parse_translation:
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   561
  (string * (Sign.sg -> term list -> term)) list
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   562
val print_translation:
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   563
  (string * (Sign.sg -> term list -> term)) list
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   564
val typed_print_translation:
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   565
  (string * (Sign.sg -> bool -> typ -> term list -> term)) list
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   566
val print_ast_translation:
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   567
  (string * (Sign.sg -> ast list -> ast)) list
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14285
diff changeset
   568
\end{ttbox}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   569
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   570
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   571
\subsection{Oracles}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   572
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   573
\indexisarcmd{oracle}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   574
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   575
  \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   576
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   577
7175
wenzelm
parents: 7167
diff changeset
   578
Oracles provide an interface to external reasoning systems, without giving up
wenzelm
parents: 7167
diff changeset
   579
control completely --- each theorem carries a derivation object recording any
wenzelm
parents: 7167
diff changeset
   580
oracle invocation.  See \cite[\S6]{isabelle-ref} for more information.
wenzelm
parents: 7167
diff changeset
   581
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   582
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   583
  'oracle' name '=' text
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   584
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   585
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   586
7167
wenzelm
parents: 7141
diff changeset
   587
\begin{descr}
7175
wenzelm
parents: 7167
diff changeset
   588
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
8379
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   589
  function $text$, which has to be of type
4c7659e98eb9 tuned ML types;
wenzelm
parents: 8250
diff changeset
   590
  \texttt{Sign.sg~*~Object.T~->~term}.
7167
wenzelm
parents: 7141
diff changeset
   591
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   592
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   593
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   594
\section{Proof commands}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   595
7987
wenzelm
parents: 7981
diff changeset
   596
Proof commands perform transitions of Isar/VM machine configurations, which
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   597
are block-structured, consisting of a stack of nodes with three main
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   598
components: logical proof context, current facts, and open goals.  Isar/VM
8547
wenzelm
parents: 8533
diff changeset
   599
transitions are \emph{typed} according to the following three different modes
wenzelm
parents: 8533
diff changeset
   600
of operation:
7167
wenzelm
parents: 7141
diff changeset
   601
\begin{descr}
wenzelm
parents: 7141
diff changeset
   602
\item [$proof(prove)$] means that a new goal has just been stated that is now
8547
wenzelm
parents: 8533
diff changeset
   603
  to be \emph{proven}; the next command may refine it by some proof method,
wenzelm
parents: 8533
diff changeset
   604
  and enter a sub-proof to establish the actual result.
10858
wenzelm
parents: 10686
diff changeset
   605
\item [$proof(state)$] is like a nested theory mode: the context may be
7987
wenzelm
parents: 7981
diff changeset
   606
  augmented by \emph{stating} additional assumptions, intermediate results
wenzelm
parents: 7981
diff changeset
   607
  etc.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   608
\item [$proof(chain)$] is intermediate between $proof(state)$ and
7987
wenzelm
parents: 7981
diff changeset
   609
  $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
wenzelm
parents: 7981
diff changeset
   610
  register) have been just picked up in order to be used when refining the
wenzelm
parents: 7981
diff changeset
   611
  goal claimed next.
7167
wenzelm
parents: 7141
diff changeset
   612
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   613
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   614
The proof mode indicator may be read as a verb telling the writer what kind of
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   615
operation may be performed next.  The corresponding typings of proof commands
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   616
restricts the shape of well-formed proof texts to particular command
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   617
sequences.  So dynamic arrangements of commands eventually turn out as static
13039
wenzelm
parents: 13024
diff changeset
   618
texts of a certain structure.  Appendix~\ref{ap:refcard} gives a simplified
wenzelm
parents: 13024
diff changeset
   619
grammar of the overall (extensible) language emerging that way.
7167
wenzelm
parents: 7141
diff changeset
   620
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   622
\subsection{Markup commands}\label{sec:markup-prf}
7167
wenzelm
parents: 7141
diff changeset
   623
7987
wenzelm
parents: 7981
diff changeset
   624
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   625
\indexisarcmd{txt}\indexisarcmd{txt-raw}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   626
\begin{matharray}{rcl}
8101
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   627
  \isarcmd{sect} & : & \isartrans{proof}{proof} \\
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   628
  \isarcmd{subsect} & : & \isartrans{proof}{proof} \\
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   629
  \isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   630
  \isarcmd{txt} & : & \isartrans{proof}{proof} \\
ae555dd9585b proof markup: any mode;
wenzelm
parents: 7988
diff changeset
   631
  \isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   632
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   633
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   634
These markup commands for proof mode closely correspond to the ones of theory
8684
dfe444b748aa improved document preparation;
wenzelm
parents: 8682
diff changeset
   635
mode (see \S\ref{sec:markup-thy}).
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   636
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   637
\railalias{txtraw}{txt\_raw}
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   638
\railterm{txtraw}
7175
wenzelm
parents: 7167
diff changeset
   639
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   640
\begin{rail}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   641
  ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   642
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   643
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   644
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   645
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   646
\subsection{Context elements}\label{sec:proof-context}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   647
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   648
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   649
\begin{matharray}{rcl}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   650
  \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   651
  \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   652
  \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   653
  \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   654
\end{matharray}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   655
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   656
The logical proof context consists of fixed variables and assumptions.  The
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   657
former closely correspond to Skolem constants, or meta-level universal
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   658
quantification as provided by the Isabelle/Pure logical framework.
13039
wenzelm
parents: 13024
diff changeset
   659
Introducing some \emph{arbitrary, but fixed} variable via ``$\FIX x$'' results
wenzelm
parents: 13024
diff changeset
   660
in a local value that may be used in the subsequent proof as any other
wenzelm
parents: 13024
diff changeset
   661
variable or constant.  Furthermore, any result $\edrv \phi[x]$ exported from
wenzelm
parents: 13024
diff changeset
   662
the context will be universally closed wrt.\ $x$ at the outermost level:
wenzelm
parents: 13024
diff changeset
   663
$\edrv \All x \phi$ (this is expressed using Isabelle's meta-variables).
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   664
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   665
Similarly, introducing some assumption $\chi$ has two effects.  On the one
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   666
hand, a local theorem is created that may be used as a fact in subsequent
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   667
proof steps.  On the other hand, any result $\chi \drv \phi$ exported from the
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   668
context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   669
Thus, solving an enclosing goal using such a result would basically introduce
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   670
a new subgoal stemming from the assumption.  How this situation is handled
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   671
depends on the actual version of assumption command used: while $\ASSUMENAME$
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   672
insists on solving the subgoal by unification with some premise of the goal,
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   673
$\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   674
user.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   675
13039
wenzelm
parents: 13024
diff changeset
   676
Local definitions, introduced by ``$\DEF{}{x \equiv t}$'', are achieved by
wenzelm
parents: 13024
diff changeset
   677
combining ``$\FIX x$'' with another version of assumption that causes any
7987
wenzelm
parents: 7981
diff changeset
   678
hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
wenzelm
parents: 7981
diff changeset
   679
Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
7175
wenzelm
parents: 7167
diff changeset
   680
10686
60c795d6bd9e 'def': equiv;
wenzelm
parents: 10640
diff changeset
   681
\railalias{equiv}{\isasymequiv}
60c795d6bd9e 'def': equiv;
wenzelm
parents: 10640
diff changeset
   682
\railterm{equiv}
60c795d6bd9e 'def': equiv;
wenzelm
parents: 10640
diff changeset
   683
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   684
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   685
  'fix' (vars + 'and')
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   686
  ;
12879
wenzelm
parents: 12621
diff changeset
   687
  ('assume' | 'presume') (props + 'and')
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   688
  ;
12879
wenzelm
parents: 12621
diff changeset
   689
  'def' thmdecl? \\ name ('==' | equiv) term termpat?
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   690
  ;
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   691
\end{rail}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
   692
7167
wenzelm
parents: 7141
diff changeset
   693
\begin{descr}
13039
wenzelm
parents: 13024
diff changeset
   694
  
8547
wenzelm
parents: 8533
diff changeset
   695
\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables
wenzelm
parents: 8533
diff changeset
   696
  $\vec x$.
13039
wenzelm
parents: 13024
diff changeset
   697
  
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   698
\item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   699
  theorems $\vec\phi$ by assumption.  Subsequent results applied to an
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   700
  enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   701
  expects to be able to unify with existing premises in the goal, while
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   702
  $\PRESUMENAME$ leaves $\vec\phi$ as new subgoals.
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   703
  
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   704
  Several lists of assumptions may be given (separated by
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   705
  $\isarkeyword{and}$); the resulting list of current facts consists of all of
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   706
  these concatenated.
13039
wenzelm
parents: 13024
diff changeset
   707
  
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   708
\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   709
  In results exported from the context, $x$ is replaced by $t$.  Basically,
13039
wenzelm
parents: 13024
diff changeset
   710
  ``$\DEF{}{x \equiv t}$'' abbreviates ``$\FIX{x}~\ASSUME{}{x \equiv t}$'',
wenzelm
parents: 13024
diff changeset
   711
  with the resulting hypothetical equation solved by reflexivity.
7431
83e60a678c3a fix: vars;
wenzelm
parents: 7397
diff changeset
   712
  
83e60a678c3a fix: vars;
wenzelm
parents: 7397
diff changeset
   713
  The default name for the definitional equation is $x_def$.
13039
wenzelm
parents: 13024
diff changeset
   714
7167
wenzelm
parents: 7141
diff changeset
   715
\end{descr}
wenzelm
parents: 7141
diff changeset
   716
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   717
The special name $prems$\indexisarthm{prems} refers to all assumptions of the
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   718
current context as a list of theorems.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   719
7167
wenzelm
parents: 7141
diff changeset
   720
wenzelm
parents: 7141
diff changeset
   721
\subsection{Facts and forward chaining}
wenzelm
parents: 7141
diff changeset
   722
wenzelm
parents: 7141
diff changeset
   723
\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   724
\indexisarcmd{using}
7167
wenzelm
parents: 7141
diff changeset
   725
\begin{matharray}{rcl}
wenzelm
parents: 7141
diff changeset
   726
  \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm
parents: 7141
diff changeset
   727
  \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm
parents: 7141
diff changeset
   728
  \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm
parents: 7141
diff changeset
   729
  \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   730
  \isarcmd{using} & : & \isartrans{proof(prove)}{proof(prove)} \\
7167
wenzelm
parents: 7141
diff changeset
   731
\end{matharray}
wenzelm
parents: 7141
diff changeset
   732
7319
wenzelm
parents: 7315
diff changeset
   733
New facts are established either by assumption or proof of local statements.
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   734
Any fact will usually be involved in further proofs, either as explicit
8547
wenzelm
parents: 8533
diff changeset
   735
arguments of proof methods, or when forward chaining towards the next goal via
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   736
$\THEN$ (and variants); $\FROMNAME$ and $\WITHNAME$ are composite forms
13039
wenzelm
parents: 13024
diff changeset
   737
involving $\NOTENAME$.  The $\USINGNAME$ elements augments the collection of
wenzelm
parents: 13024
diff changeset
   738
used facts \emph{after} a goal has been stated.  Note that the special theorem
wenzelm
parents: 13024
diff changeset
   739
name $this$\indexisarthm{this} refers to the most recently established facts,
wenzelm
parents: 13024
diff changeset
   740
but only \emph{before} issuing a follow-up claim.
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   741
7167
wenzelm
parents: 7141
diff changeset
   742
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   743
  'note' (thmdef? thmrefs + 'and')
7167
wenzelm
parents: 7141
diff changeset
   744
  ;
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   745
  ('from' | 'with' | 'using') (thmrefs + 'and')
7167
wenzelm
parents: 7141
diff changeset
   746
  ;
wenzelm
parents: 7141
diff changeset
   747
\end{rail}
wenzelm
parents: 7141
diff changeset
   748
wenzelm
parents: 7141
diff changeset
   749
\begin{descr}
13039
wenzelm
parents: 13024
diff changeset
   750
7175
wenzelm
parents: 7167
diff changeset
   751
\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
wenzelm
parents: 7167
diff changeset
   752
  as $a$.  Note that attributes may be involved as well, both on the left and
wenzelm
parents: 7167
diff changeset
   753
  right hand sides.
13039
wenzelm
parents: 13024
diff changeset
   754
7167
wenzelm
parents: 7141
diff changeset
   755
\item [$\THEN$] indicates forward chaining by the current facts in order to
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   756
  establish the goal to be claimed next.  The initial proof method invoked to
13039
wenzelm
parents: 13024
diff changeset
   757
  refine that will be offered the facts to do ``anything appropriate'' (see
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   758
  also \S\ref{sec:proof-steps}).  For example, method $rule$ (see
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   759
  \S\ref{sec:pure-meth-att}) would typically do an elimination rather than an
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   760
  introduction.  Automatic methods usually insert the facts into the goal
8547
wenzelm
parents: 8533
diff changeset
   761
  state before operation.  This provides a simple scheme to control relevance
wenzelm
parents: 8533
diff changeset
   762
  of facts in automated proof search.
13039
wenzelm
parents: 13024
diff changeset
   763
  
wenzelm
parents: 13024
diff changeset
   764
\item [$\FROM{\vec b}$] abbreviates ``$\NOTE{}{\vec b}~\THEN$''; thus $\THEN$
wenzelm
parents: 13024
diff changeset
   765
  is equivalent to ``$\FROM{this}$''.
wenzelm
parents: 13024
diff changeset
   766
  
wenzelm
parents: 13024
diff changeset
   767
\item [$\WITH{\vec b}$] abbreviates ``$\FROM{\vec b~\AND~this}$''; thus the
wenzelm
parents: 13024
diff changeset
   768
  forward chaining is from earlier facts together with the current ones.
wenzelm
parents: 13024
diff changeset
   769
  
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   770
\item [$\USING{\vec b}$] augments the facts being currently indicated for use
13039
wenzelm
parents: 13024
diff changeset
   771
  by a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$).
wenzelm
parents: 13024
diff changeset
   772
7167
wenzelm
parents: 7141
diff changeset
   773
\end{descr}
wenzelm
parents: 7141
diff changeset
   774
13039
wenzelm
parents: 13024
diff changeset
   775
Forward chaining with an empty list of theorems is the same as not chaining at
wenzelm
parents: 13024
diff changeset
   776
all.  Thus ``$\FROM{nothing}$'' has no effect apart from entering
wenzelm
parents: 13024
diff changeset
   777
$prove(chain)$ mode, since $nothing$\indexisarthm{nothing} is bound to the
wenzelm
parents: 13024
diff changeset
   778
empty list of theorems.
9238
ad37b21c0dc6 added "nothing" (empty list of theorems);
wenzelm
parents: 9233
diff changeset
   779
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   780
Basic proof methods (such as $rule$) expect multiple facts to be given in
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   781
their proper order, corresponding to a prefix of the premises of the rule
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   782
involved.  Note that positions may be easily skipped using something like
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   783
$\FROM{\Text{\texttt{_}}~a~b}$, for example.  This involves the trivial rule
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   784
$\PROP\psi \Imp \PROP\psi$, which happens to be bound in Isabelle/Pure as
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   785
``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   786
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   787
Automated methods (such as $simp$ or $auto$) just insert any given facts
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   788
before their usual operation.  Depending on the kind of procedure involved,
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   789
the order of facts is less significant here.
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   790
7167
wenzelm
parents: 7141
diff changeset
   791
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
   792
\subsection{Goal statements}\label{sec:goals}
7167
wenzelm
parents: 7141
diff changeset
   793
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   794
\indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary}
7167
wenzelm
parents: 7141
diff changeset
   795
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
wenzelm
parents: 7141
diff changeset
   796
\begin{matharray}{rcl}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   797
  \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
7167
wenzelm
parents: 7141
diff changeset
   798
  \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   799
  \isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\
7987
wenzelm
parents: 7981
diff changeset
   800
  \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
wenzelm
parents: 7981
diff changeset
   801
  \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
7167
wenzelm
parents: 7141
diff changeset
   802
  \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm
parents: 7141
diff changeset
   803
  \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm
parents: 7141
diff changeset
   804
\end{matharray}
wenzelm
parents: 7141
diff changeset
   805
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   806
From a theory context, proof mode is entered by an initial goal command such
13039
wenzelm
parents: 13024
diff changeset
   807
as $\LEMMANAME$, $\THEOREMNAME$, or $\COROLLARYNAME$.  Within a proof, new
wenzelm
parents: 13024
diff changeset
   808
claims may be introduced locally as well; four variants are available here to
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   809
indicate whether forward chaining of facts should be performed initially (via
13039
wenzelm
parents: 13024
diff changeset
   810
$\THEN$), and whether the final result is meant to solve some pending goal.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   811
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   812
Goals may consist of multiple statements, resulting in a list of facts
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   813
eventually.  A pending multi-goal is internally represented as a meta-level
13039
wenzelm
parents: 13024
diff changeset
   814
conjunction (printed as \verb,&&,), which is usually split into the
wenzelm
parents: 13024
diff changeset
   815
corresponding number of sub-goals prior to an initial method application, via
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   816
$\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$
13039
wenzelm
parents: 13024
diff changeset
   817
(\S\ref{sec:tactic-commands}).  The $induct$ method covered in
wenzelm
parents: 13024
diff changeset
   818
\S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   819
13016
wenzelm
parents: 12976
diff changeset
   820
Claims at the theory level may be either in short or long form.  A short goal
wenzelm
parents: 12976
diff changeset
   821
merely consists of several simultaneous propositions (often just one).  A long
wenzelm
parents: 12976
diff changeset
   822
goal includes an explicit context specification for the subsequent
wenzelm
parents: 12976
diff changeset
   823
conclusions, involving local parameters; here the role of each part of the
wenzelm
parents: 12976
diff changeset
   824
statement is explicitly marked by separate keywords (see also
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   825
\S\ref{sec:locale}).
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   826
7167
wenzelm
parents: 7141
diff changeset
   827
\begin{rail}
13016
wenzelm
parents: 12976
diff changeset
   828
  ('lemma' | 'theorem' | 'corollary') locale? (goal | longgoal)
7167
wenzelm
parents: 7141
diff changeset
   829
  ;
13016
wenzelm
parents: 12976
diff changeset
   830
  ('have' | 'show' | 'hence' | 'thus') goal
7167
wenzelm
parents: 7141
diff changeset
   831
  ;
12966
6373b4d09325 'using' command;
wenzelm
parents: 12879
diff changeset
   832
  
13016
wenzelm
parents: 12976
diff changeset
   833
  goal: (props + 'and')
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   834
  ;
13016
wenzelm
parents: 12976
diff changeset
   835
  longgoal: thmdecl? (contextelem *) 'shows' goal
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   836
  ;
7167
wenzelm
parents: 7141
diff changeset
   837
\end{rail}
wenzelm
parents: 7141
diff changeset
   838
wenzelm
parents: 7141
diff changeset
   839
\begin{descr}
13039
wenzelm
parents: 13024
diff changeset
   840
  
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   841
\item [$\LEMMA{a}{\vec\phi}$] enters proof mode with $\vec\phi$ as main goal,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   842
  eventually resulting in some fact $\turn \vec\phi$ to be put back into the
13039
wenzelm
parents: 13024
diff changeset
   843
  theory context, or into the specified locale (cf.\ \S\ref{sec:locale}).  An
wenzelm
parents: 13024
diff changeset
   844
  additional \railnonterm{context} specification may build up an initial proof
wenzelm
parents: 13024
diff changeset
   845
  context for the subsequent claim; this includes local definitions and syntax
wenzelm
parents: 13024
diff changeset
   846
  as well, see the definition of $contextelem$ in \S\ref{sec:locale}.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   847
  
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   848
\item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   849
  the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   850
  being of a different kind.  This discrimination acts like a formal comment.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   851
  
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   852
\item [$\HAVE{a}{\vec\phi}$] claims a local goal, eventually resulting in a
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   853
  fact within the current logical context.  This operation is completely
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   854
  independent of any pending sub-goals of an enclosing goal statements, so
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   855
  $\HAVENAME$ may be freely used for experimental exploration of potential
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   856
  results within a proof body.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   857
  
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   858
\item [$\SHOW{a}{\vec\phi}$] is like $\HAVE{a}{\vec\phi}$ plus a second stage
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   859
  to refine some pending sub-goal for each one of the finished result, after
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   860
  having been exported into the corresponding context (at the head of the
13039
wenzelm
parents: 13024
diff changeset
   861
  sub-proof of this $\SHOWNAME$ command).
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   862
  
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   863
  To accommodate interactive debugging, resulting rules are printed before
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   864
  being applied internally.  Even more, interactive execution of $\SHOWNAME$
13039
wenzelm
parents: 13024
diff changeset
   865
  predicts potential failure and displays the resulting error as a warning
wenzelm
parents: 13024
diff changeset
   866
  beforehand.  Watch out for the following message:
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   867
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   868
  \begin{ttbox}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   869
  Problem! Local statement will fail to solve any pending goal
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   870
  \end{ttbox}
13039
wenzelm
parents: 13024
diff changeset
   871
  
wenzelm
parents: 13024
diff changeset
   872
\item [$\HENCENAME$] abbreviates ``$\THEN~\HAVENAME$'', i.e.\ claims a local
wenzelm
parents: 13024
diff changeset
   873
  goal to be proven by forward chaining the current facts.  Note that
wenzelm
parents: 13024
diff changeset
   874
  $\HENCENAME$ is also equivalent to ``$\FROM{this}~\HAVENAME$''.
wenzelm
parents: 13024
diff changeset
   875
  
wenzelm
parents: 13024
diff changeset
   876
\item [$\THUSNAME$] abbreviates ``$\THEN~\SHOWNAME$''.  Note that $\THUSNAME$
wenzelm
parents: 13024
diff changeset
   877
  is also equivalent to ``$\FROM{this}~\SHOWNAME$''.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   878
7167
wenzelm
parents: 7141
diff changeset
   879
\end{descr}
wenzelm
parents: 7141
diff changeset
   880
13039
wenzelm
parents: 13024
diff changeset
   881
Any goal statement causes some term abbreviations (such as $\Var{thesis}$) to
wenzelm
parents: 13024
diff changeset
   882
be bound automatically, see also \S\ref{sec:term-abbrev}.  Furthermore, the
wenzelm
parents: 13024
diff changeset
   883
local context of a (non-atomic) goal is provided via the
13048
wenzelm
parents: 13042
diff changeset
   884
$rule_context$\indexisarcase{rule-context} case.
10550
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   885
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   886
\medskip
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   887
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   888
\begin{warn}
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   889
  Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   890
    schematic variables}, although this does not conform to the aim of
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   891
  human-readable proof documents!  The main problem with schematic goals is
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   892
  that the actual outcome is usually hard to predict, depending on the
13039
wenzelm
parents: 13024
diff changeset
   893
  behavior of the proof methods applied during the course of reasoning.  Note
10550
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   894
  that most semi-automated methods heavily depend on several kinds of implicit
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   895
  rule declarations within the current theory context.  As this would also
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   896
  result in non-compositional checking of sub-proofs, \emph{local goals} are
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   897
  not allowed to be schematic at all.  Nevertheless, schematic goals do have
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   898
  their use in Prolog-style interactive synthesis of proven results, usually
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   899
  by stepwise refinement via emulation of traditional Isabelle tactic scripts
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   900
  (see also \S\ref{sec:tactic-commands}).  In any case, users should know what
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   901
  they are doing.
10550
93ca45370c59 schematic goals;
wenzelm
parents: 10223
diff changeset
   902
\end{warn}
8991
dc70b797827f case 'antecedent';
wenzelm
parents: 8947
diff changeset
   903
7167
wenzelm
parents: 7141
diff changeset
   904
wenzelm
parents: 7141
diff changeset
   905
\subsection{Initial and terminal proof steps}\label{sec:proof-steps}
wenzelm
parents: 7141
diff changeset
   906
7175
wenzelm
parents: 7167
diff changeset
   907
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
wenzelm
parents: 7167
diff changeset
   908
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
wenzelm
parents: 7167
diff changeset
   909
\begin{matharray}{rcl}
wenzelm
parents: 7167
diff changeset
   910
  \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
wenzelm
parents: 7167
diff changeset
   911
  \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   912
  \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   913
  \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   914
  \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   915
  \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm
parents: 7167
diff changeset
   916
\end{matharray}
wenzelm
parents: 7167
diff changeset
   917
8547
wenzelm
parents: 8533
diff changeset
   918
Arbitrary goal refinement via tactics is considered harmful.  Properly, the
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   919
Isar framework admits proof methods to be invoked in two places only.
7167
wenzelm
parents: 7141
diff changeset
   920
\begin{enumerate}
7175
wenzelm
parents: 7167
diff changeset
   921
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   922
  goal to a number of sub-goals that are to be solved later.  Facts are passed
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   923
  to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
7167
wenzelm
parents: 7141
diff changeset
   924
  
7987
wenzelm
parents: 7981
diff changeset
   925
\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
wenzelm
parents: 7981
diff changeset
   926
  remaining goals.  No facts are passed to $m@2$.
7167
wenzelm
parents: 7141
diff changeset
   927
\end{enumerate}
wenzelm
parents: 7141
diff changeset
   928
13039
wenzelm
parents: 13024
diff changeset
   929
The only other (proper) way to affect pending goals in a proof body is by
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   930
$\SHOWNAME$, which involves an explicit statement of what is to be solved
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   931
eventually.  Thus we avoid the fundamental problem of unstructured tactic
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   932
scripts that consist of numerous consecutive goal transformations, with
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   933
invisible effects.
7167
wenzelm
parents: 7141
diff changeset
   934
7175
wenzelm
parents: 7167
diff changeset
   935
\medskip
wenzelm
parents: 7167
diff changeset
   936
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   937
As a general rule of thumb for good proof style, initial proof methods should
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   938
either solve the goal completely, or constitute some well-understood reduction
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   939
to new sub-goals.  Arbitrary automatic proof tools that are prone leave a
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
   940
large number of badly structured sub-goals are no help in continuing the proof
13039
wenzelm
parents: 13024
diff changeset
   941
document in an intelligible manner.
7175
wenzelm
parents: 7167
diff changeset
   942
8547
wenzelm
parents: 8533
diff changeset
   943
Unless given explicitly by the user, the default initial method is ``$rule$'',
wenzelm
parents: 8533
diff changeset
   944
which applies a single standard elimination or introduction rule according to
wenzelm
parents: 8533
diff changeset
   945
the topmost symbol involved.  There is no separate default terminal method.
wenzelm
parents: 8533
diff changeset
   946
Any remaining goals are always solved by assumption in the very last step.
7167
wenzelm
parents: 7141
diff changeset
   947
wenzelm
parents: 7141
diff changeset
   948
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
   949
  'proof' method?
7167
wenzelm
parents: 7141
diff changeset
   950
  ;
12879
wenzelm
parents: 12621
diff changeset
   951
  'qed' method?
7167
wenzelm
parents: 7141
diff changeset
   952
  ;
12879
wenzelm
parents: 12621
diff changeset
   953
  'by' method method?
7167
wenzelm
parents: 7141
diff changeset
   954
  ;
12879
wenzelm
parents: 12621
diff changeset
   955
  ('.' | '..' | 'sorry')
7167
wenzelm
parents: 7141
diff changeset
   956
  ;
wenzelm
parents: 7141
diff changeset
   957
\end{rail}
wenzelm
parents: 7141
diff changeset
   958
wenzelm
parents: 7141
diff changeset
   959
\begin{descr}
13039
wenzelm
parents: 13024
diff changeset
   960
  
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   961
\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   962
  forward chaining are passed if so indicated by $proof(chain)$ mode.
13039
wenzelm
parents: 13024
diff changeset
   963
  
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   964
\item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   965
  concludes the sub-proof by assumption.  If the goal had been $\SHOWNAME$ (or
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   966
  $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   967
  from the result \emph{exported} into the enclosing goal context.  Thus
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   968
  $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   969
  rule does not fit to any pending goal\footnote{This includes any additional
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   970
    ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   971
  context.  Debugging such a situation might involve temporarily changing
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   972
  $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
13039
wenzelm
parents: 13024
diff changeset
   973
  occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
wenzelm
parents: 13024
diff changeset
   974
  
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   975
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
13039
wenzelm
parents: 13024
diff changeset
   976
  abbreviates $\PROOF{m@1}~\QED{m@2}$, but with backtracking across both
wenzelm
parents: 13024
diff changeset
   977
  methods.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
wenzelm
parents: 13024
diff changeset
   978
  by expanding its definition; in many cases $\PROOF{m@1}$ (or even
wenzelm
parents: 13024
diff changeset
   979
  $\APPLY{m@1}$) is already sufficient to see the problem.
wenzelm
parents: 13024
diff changeset
   980
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   981
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   982
  abbreviates $\BY{rule}$.
13039
wenzelm
parents: 13024
diff changeset
   983
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
   984
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
8195
af2575a5c5ae '.' == by this;
wenzelm
parents: 8101
diff changeset
   985
  abbreviates $\BY{this}$.
13039
wenzelm
parents: 13024
diff changeset
   986
  
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   987
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   988
  the pending claim without further ado.  This only works in interactive
13039
wenzelm
parents: 13024
diff changeset
   989
  development, or if the \texttt{quick_and_dirty} flag is enabled.  Facts
wenzelm
parents: 13024
diff changeset
   990
  emerging from fake proofs are not the real thing.  Internally, each theorem
wenzelm
parents: 13024
diff changeset
   991
  container is tainted by an oracle invocation, which is indicated as
wenzelm
parents: 13024
diff changeset
   992
  ``$[!]$'' in the printed result.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   993
  
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
   994
  The most important application of $\SORRY$ is to support experimentation and
13039
wenzelm
parents: 13024
diff changeset
   995
  top-down proof development.
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   996
\end{descr}
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   997
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   998
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
   999
\subsection{Fundamental methods and attributes}\label{sec:pure-meth-att}
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1000
8547
wenzelm
parents: 8533
diff changeset
  1001
The following proof methods and attributes refer to basic logical operations
wenzelm
parents: 8533
diff changeset
  1002
of Isar.  Further methods and attributes are provided by several generic and
wenzelm
parents: 8533
diff changeset
  1003
object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
  1004
\ref{ch:logics}).
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1005
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1006
\indexisarmeth{$-$}\indexisarmeth{assumption}
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1007
\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
  1008
\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
  1009
\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
14175
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13827
diff changeset
  1010
\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1011
\begin{matharray}{rcl}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1012
  - & : & \isarmeth \\
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1013
  assumption & : & \isarmeth \\
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1014
  this & : & \isarmeth \\
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1015
  rule & : & \isarmeth \\
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1016
  rules & : & \isarmeth \\[0.5ex]
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1017
  intro & : & \isaratt \\
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1018
  elim & : & \isaratt \\
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1019
  dest & : & \isaratt \\
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1020
  rule & : & \isaratt \\[0.5ex]
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1021
  OF & : & \isaratt \\
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1022
  of & : & \isaratt \\
14175
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13827
diff changeset
  1023
  where & : & \isaratt \\
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1024
\end{matharray}
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1025
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1026
\begin{rail}
8547
wenzelm
parents: 8533
diff changeset
  1027
  'rule' thmrefs?
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1028
  ;
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1029
  'rules' ('!' ?) (rulemod *)
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1030
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1031
  rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1032
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1033
  ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1034
  ;
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1035
  'rule' 'del'
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1036
  ;
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1037
  'OF' thmrefs
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1038
  ;
8693
feb1f9af3836 'insts' syntax;
wenzelm
parents: 8684
diff changeset
  1039
  'of' insts ('concl' ':' insts)?
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1040
  ;
14175
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13827
diff changeset
  1041
  'where' (name '=' term * 'and')
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13827
diff changeset
  1042
  ;
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1043
\end{rail}
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1044
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1045
\begin{descr}
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1046
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1047
\item [``$-$''] does nothing but insert the forward chaining facts as premises
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1048
  into the goal.  Note that command $\PROOFNAME$ without any method actually
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1049
  performs a single reduction step using the $rule$ method; thus a plain
13039
wenzelm
parents: 13024
diff changeset
  1050
  \emph{do-nothing} proof step would be ``$\PROOF{-}$'' rather than
wenzelm
parents: 13024
diff changeset
  1051
  $\PROOFNAME$ alone.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1052
  
13039
wenzelm
parents: 13024
diff changeset
  1053
\item [$assumption$] solves some goal by a single assumption step.  All given
wenzelm
parents: 13024
diff changeset
  1054
  facts are guaranteed to participate in the refinement; this means there may
wenzelm
parents: 13024
diff changeset
  1055
  be only $0$ or $1$ in the first place.  Recall that $\QEDNAME$ (see
wenzelm
parents: 13024
diff changeset
  1056
  \S\ref{sec:proof-steps}) already concludes any remaining sub-goals by
wenzelm
parents: 13024
diff changeset
  1057
  assumption, so structured proofs usually need not quote the $assumption$
wenzelm
parents: 13024
diff changeset
  1058
  method at all.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1059
  
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1060
\item [$this$] applies all of the current facts directly as rules.  Recall
13039
wenzelm
parents: 13024
diff changeset
  1061
  that ``$\DOT$'' (dot) abbreviates ``$\BY{this}$''.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1062
  
8547
wenzelm
parents: 8533
diff changeset
  1063
\item [$rule~\vec a$] applies some rule given as argument in backward manner;
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1064
  facts are used to reduce the rule before applying it to the goal.  Thus
13039
wenzelm
parents: 13024
diff changeset
  1065
  $rule$ without facts is plain introduction, while with facts it becomes
wenzelm
parents: 13024
diff changeset
  1066
  elimination.
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1067
  
8547
wenzelm
parents: 8533
diff changeset
  1068
  When no arguments are given, the $rule$ method tries to pick appropriate
wenzelm
parents: 8533
diff changeset
  1069
  rules automatically, as declared in the current context using the $intro$,
wenzelm
parents: 8533
diff changeset
  1070
  $elim$, $dest$ attributes (see below).  This is the default behavior of
wenzelm
parents: 8533
diff changeset
  1071
  $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1072
  \S\ref{sec:proof-steps}).
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1073
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1074
\item [$rules$] performs intuitionistic proof search, depending on
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1075
  specifically declared rules from the context, or given as explicit
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1076
  arguments.  Chained facts are inserted into the goal before commencing proof
13039
wenzelm
parents: 13024
diff changeset
  1077
  search; ``$rules!$'' means to include the current $prems$ as well.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1078
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1079
  Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$''
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1080
  indicator refers to ``safe'' rules, which may be applied aggressively
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1081
  (without considering back-tracking later).  Rules declared with ``$?$'' are
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1082
  ignored in proof search (the single-step $rule$ method still observes
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1083
  these).  An explicit weight annotation may be given as well; otherwise the
13039
wenzelm
parents: 13024
diff changeset
  1084
  number of rule premises will be taken into account here.
wenzelm
parents: 13024
diff changeset
  1085
  
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1086
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1087
  destruct rules, to be used with the $rule$ and $rules$ methods.  Note that
13039
wenzelm
parents: 13024
diff changeset
  1088
  the latter will ignore rules declared with ``$?$'', while ``$!$'' are used
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1089
  most aggressively.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1090
  
13048
wenzelm
parents: 13042
diff changeset
  1091
  The classical reasoner (see \S\ref{sec:classical}) introduces its own
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1092
  variants of these attributes; use qualified names to access the present
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1093
  versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1094
  
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1095
\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1096
  
8547
wenzelm
parents: 8533
diff changeset
  1097
\item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in
wenzelm
parents: 8533
diff changeset
  1098
  parallel).  This corresponds to the \texttt{MRS} operator in ML
wenzelm
parents: 8533
diff changeset
  1099
  \cite[\S5]{isabelle-ref}, but note the reversed order.  Positions may be
13039
wenzelm
parents: 13024
diff changeset
  1100
  effectively skipped by including ``$\_$'' (underscore) as argument.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1101
  
14285
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1102
\item [$of~\vec t$] performs positional instantiation of term
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1103
  variables.  The terms $\vec t$ are substituted for any schematic
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1104
  variables occurring in a theorem from left to right; ``\texttt{_}''
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1105
  (underscore) indicates to skip a position.  Arguments following a
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1106
  ``$concl\colon$'' specification refer to positions of the conclusion
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1107
  of a rule.
13024
0461b281c2b5 more stuff;
wenzelm
parents: 13016
diff changeset
  1108
  
14285
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1109
\item [$where~\vec x = \vec t$] performs named instantiation of
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1110
  schematic type and term variables occurring in a theorem.  Schematic
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1111
  variables have to be specified on the left-hand side (e.g.\
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1112
  $?x1\!.\!3$).  The question mark may be omitted if the variable name
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1113
  is neither a keyword nor contains a dot.  Types are instantiated
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1114
  before terms, and instantiations have to be written in that order.
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1115
  Because type instantiations are inferred from term instantiations,
92ed032e83a1 Isar: where attribute supports instantiation of type vars.
ballarin
parents: 14212
diff changeset
  1116
  explicit type instantiations are seldom necessary.
14175
dbd16ebaf907 Method rule_tac understands Isar contexts: documentation.
ballarin
parents: 13827
diff changeset
  1117
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1118
\end{descr}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1119
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1120
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1121
\subsection{Term abbreviations}\label{sec:term-abbrev}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1122
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1123
\indexisarcmd{let}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1124
\begin{matharray}{rcl}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1125
  \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1126
  \isarkeyword{is} & : & syntax \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1127
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1128
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1129
Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
7987
wenzelm
parents: 7981
diff changeset
  1130
or by annotating assumptions or goal statements with a list of patterns
13039
wenzelm
parents: 13024
diff changeset
  1131
``$\ISS{p@1\;\dots}{p@n}$''.  In both cases, higher-order matching is invoked
wenzelm
parents: 13024
diff changeset
  1132
to bind extra-logical term variables, which may be either named schematic
7987
wenzelm
parents: 7981
diff changeset
  1133
variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
wenzelm
parents: 7981
diff changeset
  1134
(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
wenzelm
parents: 7981
diff changeset
  1135
patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
wenzelm
parents: 7981
diff changeset
  1136
postfix position.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1137
12621
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
  1138
Polymorphism of term bindings is handled in Hindley-Milner style, similar to
48cafea0684b next round of updates;
wenzelm
parents: 12618
diff changeset
  1139
ML.  Type variables referring to local assumptions or open goal statements are
8620
3786d47f5570 support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents: 8547
diff changeset
  1140
\emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur
3786d47f5570 support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents: 8547
diff changeset
  1141
in \emph{arbitrary} instances later.  Even though actual polymorphism should
3786d47f5570 support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents: 8547
diff changeset
  1142
be rarely used in practice, this mechanism is essential to achieve proper
3786d47f5570 support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents: 8547
diff changeset
  1143
incremental type-inference, as the user proceeds to build up the Isar proof
13039
wenzelm
parents: 13024
diff changeset
  1144
text from left to right.
8620
3786d47f5570 support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents: 8547
diff changeset
  1145
3786d47f5570 support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents: 8547
diff changeset
  1146
\medskip
3786d47f5570 support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents: 8547
diff changeset
  1147
13039
wenzelm
parents: 13024
diff changeset
  1148
Term abbreviations are quite different from local definitions as introduced
wenzelm
parents: 13024
diff changeset
  1149
via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are visible within
wenzelm
parents: 13024
diff changeset
  1150
the logic as actual equations, while abbreviations disappear during the input
wenzelm
parents: 13024
diff changeset
  1151
process just after type checking.  Also note that $\DEFNAME$ does not support
wenzelm
parents: 13024
diff changeset
  1152
polymorphism.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1153
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1154
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
  1155
  'let' ((term + 'and') '=' term + 'and')
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1156
  ;  
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1157
\end{rail}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1158
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1159
The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11549
diff changeset
  1160
\railnonterm{proppat} (see \S\ref{sec:term-decls}).
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1161
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1162
\begin{descr}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1163
\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1164
  by simultaneous higher-order matching against terms $\vec t$.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1165
\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1166
  preceding statement.  Also note that $\ISNAME$ is not a separate command,
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1167
  but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1168
\end{descr}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1169
10160
wenzelm
parents: 9936
diff changeset
  1170
Some \emph{automatic} term abbreviations\index{term abbreviations} for goals
7988
wenzelm
parents: 7987
diff changeset
  1171
and facts are available as well.  For any open goal,
10160
wenzelm
parents: 9936
diff changeset
  1172
$\Var{thesis}$\indexisarvar{thesis} refers to its object-level statement,
wenzelm
parents: 9936
diff changeset
  1173
abstracted over any meta-level parameters (if present).  Likewise,
wenzelm
parents: 9936
diff changeset
  1174
$\Var{this}$\indexisarvar{this} is bound for fact statements resulting from
wenzelm
parents: 9936
diff changeset
  1175
assumptions or finished goals.  In case $\Var{this}$ refers to an object-logic
wenzelm
parents: 9936
diff changeset
  1176
statement that is an application $f(t)$, then $t$ is bound to the special text
wenzelm
parents: 9936
diff changeset
  1177
variable ``$\dots$''\indexisarvar{\dots} (three dots).  The canonical
wenzelm
parents: 9936
diff changeset
  1178
application of the latter are calculational proofs (see
wenzelm
parents: 9936
diff changeset
  1179
\S\ref{sec:calculation}).
wenzelm
parents: 9936
diff changeset
  1180
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
  1181
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
  1182
\subsection{Block structure}
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
  1183
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8883
diff changeset
  1184
\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}}
7397
wenzelm
parents: 7389
diff changeset
  1185
\begin{matharray}{rcl}
8448
e7df316491d4 tuned 'case';
wenzelm
parents: 8379
diff changeset
  1186
  \NEXT & : & \isartrans{proof(state)}{proof(state)} \\
7974
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
  1187
  \BG & : & \isartrans{proof(state)}{proof(state)} \\
34245feb6e82 improved;
wenzelm
parents: 7895
diff changeset
  1188
  \EN & : & \isartrans{proof(state)}{proof(state)} \\
7397
wenzelm
parents: 7389
diff changeset
  1189
\end{matharray}
wenzelm
parents: 7389
diff changeset
  1190
7167
wenzelm
parents: 7141
diff changeset
  1191
While Isar is inherently block-structured, opening and closing blocks is
wenzelm
parents: 7141
diff changeset
  1192
mostly handled rather casually, with little explicit user-intervention.  Any
wenzelm
parents: 7141
diff changeset
  1193
local goal statement automatically opens \emph{two} blocks, which are closed
wenzelm
parents: 7141
diff changeset
  1194
again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
8448
e7df316491d4 tuned 'case';
wenzelm
parents: 8379
diff changeset
  1195
different context within a sub-proof may be switched via $\NEXT$, which is
13039
wenzelm
parents: 13024
diff changeset
  1196
just a single block-close followed by block-open again.  The effect of $\NEXT$
wenzelm
parents: 13024
diff changeset
  1197
is to reset the local proof context; there is no goal focus involved here!
7167
wenzelm
parents: 7141
diff changeset
  1198
7175
wenzelm
parents: 7167
diff changeset
  1199
For slightly more advanced applications, there are explicit block parentheses
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
  1200
as well.  These typically achieve a stronger forward style of reasoning.
7167
wenzelm
parents: 7141
diff changeset
  1201
wenzelm
parents: 7141
diff changeset
  1202
\begin{descr}
8448
e7df316491d4 tuned 'case';
wenzelm
parents: 8379
diff changeset
  1203
\item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the
e7df316491d4 tuned 'case';
wenzelm
parents: 8379
diff changeset
  1204
  local context to the initial one.
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8883
diff changeset
  1205
\item [$\BG$ and $\EN$] explicitly open and close blocks.  Any current facts
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8883
diff changeset
  1206
  pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
  1207
  \emph{exported} into the enclosing context.  Thus fixed variables are
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
  1208
  generalized, assumptions discharged, and local definitions unfolded (cf.\ 
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
  1209
  \S\ref{sec:proof-context}).  There is no difference of $\ASSUMENAME$ and
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
  1210
  $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain
7c492d8bc8e3 updated;
wenzelm
parents: 7608
diff changeset
  1211
  backward reasoning with the result exported at $\SHOWNAME$ time.
7167
wenzelm
parents: 7141
diff changeset
  1212
\end{descr}
7134
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
  1213
320b412e5800 more stuff;
wenzelm
parents: 7046
diff changeset
  1214
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1215
\subsection{Emulating tactic scripts}\label{sec:tactic-commands}
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1216
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1217
The Isar provides separate commands to accommodate tactic-style proof scripts
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1218
within the same system.  While being outside the orthodox Isar proof language,
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1219
these might come in handy for interactive exploration and debugging, or even
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1220
actual tactical proof within new-style theories (to benefit from document
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1221
preparation, for example).  See also \S\ref{sec:tactics} for actual tactics,
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1222
that have been encapsulated as proof methods.  Proper proof methods may be
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1223
used in scripts, too.
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1224
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1225
\indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{done}
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1226
\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back}
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1227
\indexisarcmd{declare}
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1228
\begin{matharray}{rcl}
8533
d534ddf14076 res_inst_tac etc.;
wenzelm
parents: 8515
diff changeset
  1229
  \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1230
  \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\
8946
40e06237934c "done" command;
wenzelm
parents: 8896
diff changeset
  1231
  \isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\
8533
d534ddf14076 res_inst_tac etc.;
wenzelm
parents: 8515
diff changeset
  1232
  \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\
d534ddf14076 res_inst_tac etc.;
wenzelm
parents: 8515
diff changeset
  1233
  \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\
d534ddf14076 res_inst_tac etc.;
wenzelm
parents: 8515
diff changeset
  1234
  \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1235
  \isarcmd{declare}^* & : & \isartrans{theory}{theory} \\
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1236
\end{matharray}
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1237
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1238
\railalias{applyend}{apply\_end}
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1239
\railterm{applyend}
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1240
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1241
\begin{rail}
12879
wenzelm
parents: 12621
diff changeset
  1242
  ( 'apply' | applyend ) method
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1243
  ;
12879
wenzelm
parents: 12621
diff changeset
  1244
  'defer' nat?
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1245
  ;
12879
wenzelm
parents: 12621
diff changeset
  1246
  'prefer' nat
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1247
  ;
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
  1248
  'declare' locale? (thmrefs + 'and')
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1249
  ;
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1250
\end{rail}
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1251
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1252
\begin{descr}
13042
wenzelm
parents: 13039
diff changeset
  1253
10223
wenzelm
parents: 10160
diff changeset
  1254
\item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike
wenzelm
parents: 10160
diff changeset
  1255
  $\PROOFNAME$ it retains ``$proof(prove)$'' mode.  Thus consecutive method
wenzelm
parents: 10160
diff changeset
  1256
  applications may be given just as in tactic scripts.
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1257
  
8881
0467dd0d66ff 'apply' consumes facts;
wenzelm
parents: 8726
diff changeset
  1258
  Facts are passed to $m$ as indicated by the goal's forward-chain mode, and
10223
wenzelm
parents: 10160
diff changeset
  1259
  are \emph{consumed} afterwards.  Thus any further $\APPLYNAME$ command would
wenzelm
parents: 10160
diff changeset
  1260
  always work in a purely backward manner.
8946
40e06237934c "done" command;
wenzelm
parents: 8896
diff changeset
  1261
  
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1262
\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1263
  terminal position.  Basically, this simulates a multi-step tactic script for
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1264
  $\QEDNAME$, but may be given anywhere within the proof body.
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1265
  
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1266
  No facts are passed to $m$.  Furthermore, the static context is that of the
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1267
  enclosing goal (as for actual $\QEDNAME$).  Thus the proof method may not
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1268
  refer to any assumptions introduced in the current body, for example.
13039
wenzelm
parents: 13024
diff changeset
  1269
  
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1270
\item [$\isarkeyword{done}$] completes a proof script, provided that the
13039
wenzelm
parents: 13024
diff changeset
  1271
  current goal state is solved completely.  Note that actual structured proof
wenzelm
parents: 13024
diff changeset
  1272
  commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to conclude proof
wenzelm
parents: 13024
diff changeset
  1273
  scripts as well.
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1274
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1275
\item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1276
  of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1277
  by default), while $prefer$ brings goal $n$ to the top.
13039
wenzelm
parents: 13024
diff changeset
  1278
  
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1279
\item [$\isarkeyword{back}$] does back-tracking over the result sequence of
13039
wenzelm
parents: 13024
diff changeset
  1280
  the latest proof command.  Basically, any proof command may return multiple
wenzelm
parents: 13024
diff changeset
  1281
  results.
9605
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1282
  
60d8c954390f added 'declare' command;
wenzelm
parents: 9471
diff changeset
  1283
\item [$\isarkeyword{declare}~thms$] declares theorems to the current theory
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
  1284
  context (or the specified locale, see also \S\ref{sec:locale}).  No theorem
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
  1285
  binding is involved here, unlike $\isarkeyword{theorems}$ or
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
  1286
  $\isarkeyword{lemmas}$ (cf.\ \S\ref{sec:axms-thms}), so
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
  1287
  $\isarkeyword{declare}$ only has the effect of applying attributes as
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12966
diff changeset
  1288
  included in the theorem specification.
13042
wenzelm
parents: 13039
diff changeset
  1289
9006
3832cc6f4a43 tuned tactic emulation;
wenzelm
parents: 8991
diff changeset
  1290
\end{descr}
3832cc6f4a43 tuned tactic emulation;
wenzelm
parents: 8991
diff changeset
  1291
3832cc6f4a43 tuned tactic emulation;
wenzelm
parents: 8991
diff changeset
  1292
Any proper Isar proof method may be used with tactic script commands such as
10223
wenzelm
parents: 10160
diff changeset
  1293
$\APPLYNAME$.  A few additional emulations of actual tactics are provided as
wenzelm
parents: 10160
diff changeset
  1294
well; these would be never used in actual structured proofs, of course.
9006
3832cc6f4a43 tuned tactic emulation;
wenzelm
parents: 8991
diff changeset
  1295
8515
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1296
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1297
\subsection{Meta-linguistic features}
160739e1f443 pure methods / atts moved here;
wenzelm
parents: 8510
diff changeset
  1298
160739e1f443 pure methods / atts moved here;
wenze&#