doc-src/IsarRef/generic.tex
author wenzelm
Mon Aug 23 11:43:21 1999 +0200 (1999-08-23)
changeset 7319 3907d597cae6
parent 7315 76a39a3784b5
child 7321 b4dcc32310fb
permissions -rw-r--r--
tuned;
wenzelm@7135
     1
wenzelm@7167
     2
\chapter{Generic Tools and Packages}\label{ch:gen-tools}
wenzelm@7167
     3
wenzelm@7315
     4
\section{Basic proof methods}\label{sec:pure-meth}
wenzelm@7167
     5
wenzelm@7167
     6
\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
wenzelm@7167
     7
\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
wenzelm@7167
     8
\indexisarmeth{rule}\indexisarmeth{erule}
wenzelm@7167
     9
\begin{matharray}{rcl}
wenzelm@7167
    10
  fail & : & \isarmeth \\
wenzelm@7167
    11
  succeed & : & \isarmeth \\
wenzelm@7167
    12
  - & : & \isarmeth \\
wenzelm@7167
    13
  assumption & : & \isarmeth \\
wenzelm@7167
    14
  finish & : & \isarmeth \\
wenzelm@7167
    15
  fold & : & \isarmeth \\
wenzelm@7167
    16
  unfold & : & \isarmeth \\
wenzelm@7167
    17
  rule & : & \isarmeth \\
wenzelm@7167
    18
  erule^* & : & \isarmeth \\
wenzelm@7167
    19
\end{matharray}
wenzelm@7167
    20
wenzelm@7167
    21
\begin{rail}
wenzelm@7167
    22
  ('fold' | 'unfold' | 'rule' | 'erule') thmrefs
wenzelm@7167
    23
  ;
wenzelm@7167
    24
\end{rail}
wenzelm@7167
    25
wenzelm@7167
    26
\begin{descr}
wenzelm@7167
    27
\item [$ $]
wenzelm@7167
    28
\end{descr}
wenzelm@7167
    29
wenzelm@7167
    30
FIXME
wenzelm@7167
    31
wenzelm@7167
    32
%FIXME sort
wenzelm@7167
    33
%FIXME thmref (single)
wenzelm@7167
    34
%FIXME var vs. term
wenzelm@7167
    35
wenzelm@7315
    36
wenzelm@7315
    37
\section{Miscellaneous attributes}
wenzelm@7315
    38
wenzelm@7167
    39
\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
wenzelm@7167
    40
\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
wenzelm@7167
    41
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
wenzelm@7167
    42
\begin{matharray}{rcl}
wenzelm@7167
    43
  tag & : & \isaratt \\
wenzelm@7167
    44
  untag & : & \isaratt \\
wenzelm@7167
    45
  COMP & : & \isaratt \\
wenzelm@7167
    46
  RS & : & \isaratt \\
wenzelm@7167
    47
  OF & : & \isaratt \\
wenzelm@7167
    48
  where & : & \isaratt \\
wenzelm@7167
    49
  of & : & \isaratt \\
wenzelm@7167
    50
  standard & : & \isaratt \\
wenzelm@7167
    51
  elimify & : & \isaratt \\
wenzelm@7167
    52
  transfer & : & \isaratt \\
wenzelm@7167
    53
  export & : & \isaratt \\
wenzelm@7167
    54
\end{matharray}
wenzelm@7167
    55
wenzelm@7167
    56
\begin{rail}
wenzelm@7167
    57
  ('tag' | 'untag') (nameref+)
wenzelm@7167
    58
  ;
wenzelm@7175
    59
\end{rail}
wenzelm@7175
    60
wenzelm@7175
    61
\begin{rail}
wenzelm@7167
    62
  ('COMP' | 'RS') nat? thmref
wenzelm@7167
    63
  ;
wenzelm@7167
    64
  'OF' thmrefs
wenzelm@7167
    65
  ;
wenzelm@7175
    66
\end{rail}
wenzelm@7175
    67
wenzelm@7175
    68
\begin{rail}
wenzelm@7175
    69
  'where' (name '=' term * 'and')
wenzelm@7167
    70
  ;
wenzelm@7175
    71
  'of' (inst * ) ('concl' ':' (inst * ))?
wenzelm@7167
    72
  ;
wenzelm@7167
    73
wenzelm@7167
    74
  inst: underscore | term
wenzelm@7167
    75
  ;
wenzelm@7167
    76
\end{rail}
wenzelm@7167
    77
wenzelm@7167
    78
\begin{descr}
wenzelm@7167
    79
\item [$ $]
wenzelm@7167
    80
\end{descr}
wenzelm@7167
    81
wenzelm@7167
    82
FIXME
wenzelm@7135
    83
wenzelm@7315
    84
wenzelm@7315
    85
\section{Calculational proof}\label{sec:calculation}
wenzelm@7315
    86
wenzelm@7315
    87
\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
wenzelm@7315
    88
\begin{matharray}{rcl}
wenzelm@7315
    89
  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7315
    90
  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7315
    91
  trans & : & \isaratt \\
wenzelm@7315
    92
\end{matharray}
wenzelm@7315
    93
wenzelm@7315
    94
Calculational proof is forward reasoning with implicit application of
wenzelm@7315
    95
transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
wenzelm@7315
    96
an auxiliary register $calculation$\indexisarreg{calculation} for accumulating
wenzelm@7315
    97
results obtained by transitivity obtained together with the current facts.
wenzelm@7315
    98
Command $\ALSO$ updates $calculation$ from the most recent result, while
wenzelm@7315
    99
$\FINALLY$ exhibits the final result by forward chaining towards the next goal
wenzelm@7315
   100
statement.  Both commands require valid current facts, i.e.\ may occur only
wenzelm@7315
   101
after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
wenzelm@7315
   102
some finished $\HAVENAME$ or $\SHOWNAME$.
wenzelm@7315
   103
wenzelm@7315
   104
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
wenzelm@7315
   105
application with calculational proofs.  It automatically refers to the
wenzelm@7315
   106
argument\footnote{The argument of a curried infix expression is its right-hand
wenzelm@7315
   107
  side.} of the preceding statement.
wenzelm@7315
   108
wenzelm@7315
   109
Isabelle/Isar calculations are implicitly subject to block structure in the
wenzelm@7315
   110
sense that new threads of calculational reasoning are commenced for any new
wenzelm@7315
   111
block (as opened by a local goal, for example).  This means that, apart from
wenzelm@7315
   112
being able to nest calculations, there is no separate \emph{begin-calculation}
wenzelm@7315
   113
command required.
wenzelm@7315
   114
wenzelm@7315
   115
\begin{rail}
wenzelm@7315
   116
  ('also' | 'finally') transrules? comment?
wenzelm@7315
   117
  ;
wenzelm@7315
   118
  'trans' (() | 'add' ':' | 'del' ':') thmrefs
wenzelm@7315
   119
  ;
wenzelm@7315
   120
wenzelm@7315
   121
  transrules: '(' thmrefs ')' interest?
wenzelm@7315
   122
  ;
wenzelm@7315
   123
\end{rail}
wenzelm@7315
   124
wenzelm@7315
   125
\begin{descr}
wenzelm@7315
   126
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
wenzelm@7315
   127
  follows.  The first occurrence of $\ALSO$ in some calculational thread
wenzelm@7315
   128
  initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the
wenzelm@7315
   129
  \emph{same} level of block-structure updates $calculation$ by some
wenzelm@7315
   130
  transitivity rule applied to $calculation$ and $facts$ (in that order).
wenzelm@7315
   131
  Transitivity rules are picked from the current context plus those given as
wenzelm@7315
   132
  $thms$ (the latter have precedence).
wenzelm@7315
   133
  
wenzelm@7315
   134
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
wenzelm@7315
   135
  $\ALSO$, and concludes the current calculational thread.  The final result
wenzelm@7315
   136
  is exhibited as fact for forward chaining towards the next goal. Basically,
wenzelm@7315
   137
  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  A typical proof
wenzelm@7315
   138
  idiom is $\FINALLY~\SHOW~\VVar{thesis}~\DOT$.
wenzelm@7315
   139
  
wenzelm@7315
   140
\item [Attribute $trans$] maintains the set of transitivity rules of the
wenzelm@7315
   141
  theory or proof context, by adding or deleting the theorems provided as
wenzelm@7315
   142
  arguments.  The default is adding of rules.
wenzelm@7315
   143
\end{descr}
wenzelm@7315
   144
wenzelm@7315
   145
See theory \texttt{HOL/Isar_examples/Group} for a simple applications of
wenzelm@7315
   146
calculations for basic equational reasoning.
wenzelm@7315
   147
\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
wenzelm@7315
   148
calculational steps in combination with natural deduction.
wenzelm@7315
   149
wenzelm@7315
   150
wenzelm@7135
   151
\section{Axiomatic Type Classes}\label{sec:axclass}
wenzelm@7135
   152
wenzelm@7135
   153
\indexisarcmd{axclass}\indexisarcmd{instance}
wenzelm@7135
   154
\begin{matharray}{rcl}
wenzelm@7135
   155
  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
wenzelm@7135
   156
  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7319
   157
  expand_classes & : & \isarmeth \\
wenzelm@7135
   158
\end{matharray}
wenzelm@7135
   159
wenzelm@7135
   160
Axiomatic type classes are provided by Isabelle/Pure as a purely
wenzelm@7135
   161
\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
wenzelm@7135
   162
any object logic may make use of this light-weight mechanism for abstract
wenzelm@7135
   163
theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
wenzelm@7135
   164
tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
wenzelm@7135
   165
the standard Isabelle documentation.
wenzelm@7135
   166
wenzelm@7135
   167
\begin{rail}
wenzelm@7135
   168
  'axclass' classdecl (axmdecl prop comment? +)
wenzelm@7135
   169
  ;
wenzelm@7135
   170
  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
wenzelm@7135
   171
  ;
wenzelm@7135
   172
\end{rail}
wenzelm@7135
   173
wenzelm@7167
   174
\begin{descr}
wenzelm@7135
   175
\item [$\isarkeyword{axclass}~$] FIXME
wenzelm@7135
   176
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
wenzelm@7135
   177
  c@2$] setup up a goal stating the class relation or type arity.  The proof
wenzelm@7135
   178
  would usually proceed by the $expand_classes$ method, and then establish the
wenzelm@7141
   179
  characteristic theorems of the type classes involved.  After finishing the
wenzelm@7141
   180
  proof the theory will be augmented by a type signature declaration
wenzelm@7135
   181
  corresponding to the resulting theorem.
wenzelm@7319
   182
\item [Method $expand_classes$] iteratively expands the class introduction
wenzelm@7319
   183
  rules
wenzelm@7167
   184
\end{descr}
wenzelm@7135
   185
wenzelm@7319
   186
See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
wenzelm@7319
   187
axiomatic type classes, including instantiation proofs.
wenzelm@7135
   188
wenzelm@7135
   189
wenzelm@7135
   190
\section{The Simplifier}
wenzelm@7135
   191
wenzelm@7315
   192
\subsection{Simplification methods}
wenzelm@7315
   193
wenzelm@7315
   194
\indexisarmeth{simp}\indexisarmeth{asm_simp}\indexisaratt{simp}
wenzelm@7315
   195
\begin{matharray}{rcl}
wenzelm@7315
   196
  simp & : & \isarmeth \\
wenzelm@7315
   197
  asm_simp & : & \isarmeth \\
wenzelm@7315
   198
  simp & : & \isaratt \\
wenzelm@7315
   199
\end{matharray}
wenzelm@7315
   200
wenzelm@7315
   201
\begin{rail}
wenzelm@7319
   202
  'simp' (simpmod * )
wenzelm@7315
   203
  ;
wenzelm@7315
   204
wenzelm@7315
   205
  simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
wenzelm@7315
   206
  ;
wenzelm@7315
   207
\end{rail}
wenzelm@7315
   208
wenzelm@7319
   209
FIXME
wenzelm@7319
   210
wenzelm@7315
   211
wenzelm@7315
   212
\subsection{Forward simplification}
wenzelm@7315
   213
wenzelm@7315
   214
\indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify}
wenzelm@7315
   215
\begin{matharray}{rcl}
wenzelm@7315
   216
  simplify & : & \isaratt \\
wenzelm@7315
   217
  asm_simplify & : & \isaratt \\
wenzelm@7315
   218
  full_simplify & : & \isaratt \\
wenzelm@7315
   219
  asm_full_simplify & : & \isaratt \\
wenzelm@7315
   220
\end{matharray}
wenzelm@7315
   221
wenzelm@7315
   222
FIXME
wenzelm@7315
   223
wenzelm@7315
   224
wenzelm@7135
   225
\section{The Classical Reasoner}
wenzelm@7135
   226
wenzelm@7315
   227
\subsection{Single step methods}
wenzelm@7315
   228
wenzelm@7315
   229
\subsection{Automatic methods}
wenzelm@7315
   230
wenzelm@7315
   231
\subsection{Combined automatic methods}
wenzelm@7315
   232
wenzelm@7315
   233
\subsection{Modifying the context}
wenzelm@7315
   234
wenzelm@7315
   235
wenzelm@7135
   236
wenzelm@7135
   237
%\indexisarcmd{}
wenzelm@7135
   238
%\begin{matharray}{rcl}
wenzelm@7135
   239
%  \isarcmd{} & : & \isartrans{}{} \\
wenzelm@7135
   240
%\end{matharray}
wenzelm@7135
   241
wenzelm@7135
   242
%\begin{rail}
wenzelm@7135
   243
  
wenzelm@7135
   244
%\end{rail}
wenzelm@7135
   245
wenzelm@7167
   246
%\begin{descr}
wenzelm@7135
   247
%\item [$ $]
wenzelm@7167
   248
%\end{descr}
wenzelm@7135
   249
wenzelm@7135
   250
wenzelm@7135
   251
%%% Local Variables: 
wenzelm@7135
   252
%%% mode: latex
wenzelm@7135
   253
%%% TeX-master: "isar-ref"
wenzelm@7135
   254
%%% End: