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