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