doc-src/IsarRef/generic.tex
author wenzelm
Mon, 23 Aug 1999 15:27:27 +0200
changeset 7321 b4dcc32310fb
parent 7319 3907d597cae6
child 7335 abba35b98892
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7135
wenzelm
parents:
diff changeset
     1
7167
wenzelm
parents: 7141
diff changeset
     2
\chapter{Generic Tools and Packages}\label{ch:gen-tools}
wenzelm
parents: 7141
diff changeset
     3
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
     4
\section{Basic proof methods}\label{sec:pure-meth}
7167
wenzelm
parents: 7141
diff changeset
     5
wenzelm
parents: 7141
diff changeset
     6
\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
wenzelm
parents: 7141
diff changeset
     7
\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
wenzelm
parents: 7141
diff changeset
     8
\indexisarmeth{rule}\indexisarmeth{erule}
wenzelm
parents: 7141
diff changeset
     9
\begin{matharray}{rcl}
wenzelm
parents: 7141
diff changeset
    10
  - & : & \isarmeth \\
wenzelm
parents: 7141
diff changeset
    11
  assumption & : & \isarmeth \\
7321
wenzelm
parents: 7319
diff changeset
    12
  finish & : & \isarmeth \\[0.5ex]
wenzelm
parents: 7319
diff changeset
    13
  rule & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
    14
  erule^* & : & \isarmeth \\[0.5ex]
7167
wenzelm
parents: 7141
diff changeset
    15
  fold & : & \isarmeth \\
7321
wenzelm
parents: 7319
diff changeset
    16
  unfold & : & \isarmeth \\[0.5ex]
wenzelm
parents: 7319
diff changeset
    17
  fail & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
    18
  succeed & : & \isarmeth \\
7167
wenzelm
parents: 7141
diff changeset
    19
\end{matharray}
wenzelm
parents: 7141
diff changeset
    20
wenzelm
parents: 7141
diff changeset
    21
\begin{rail}
wenzelm
parents: 7141
diff changeset
    22
  ('fold' | 'unfold' | 'rule' | 'erule') thmrefs
wenzelm
parents: 7141
diff changeset
    23
  ;
wenzelm
parents: 7141
diff changeset
    24
\end{rail}
wenzelm
parents: 7141
diff changeset
    25
wenzelm
parents: 7141
diff changeset
    26
\begin{descr}
7321
wenzelm
parents: 7319
diff changeset
    27
\item [``$-$''] does nothing but insert the forward chaining facts as premises
wenzelm
parents: 7319
diff changeset
    28
  into the goal.  Note that command $\PROOFNAME$ without any method given
wenzelm
parents: 7319
diff changeset
    29
  actually performs a single reduction step using the $rule$ method (see
wenzelm
parents: 7319
diff changeset
    30
  below); thus a plain \emph{do-nothing} proof step would be $\PROOF{-}$
wenzelm
parents: 7319
diff changeset
    31
  rather than $\PROOFNAME$ alone.
wenzelm
parents: 7319
diff changeset
    32
\item [$assumption$] solves some goal by assumption (after inserting the
wenzelm
parents: 7319
diff changeset
    33
  goal's facts).
wenzelm
parents: 7319
diff changeset
    34
\item [$finish$] solves all remaining goals by assumption; this is the default
wenzelm
parents: 7319
diff changeset
    35
  terminal proof method for $\QEDNAME$, i.e.\ it usually does not have to be
wenzelm
parents: 7319
diff changeset
    36
  spelled out explicitly.
wenzelm
parents: 7319
diff changeset
    37
\item [$rule~thms$] applies some rule given as argument in backward manner;
wenzelm
parents: 7319
diff changeset
    38
  facts are used to reduce the rule before applying it to the goal.  Thus
wenzelm
parents: 7319
diff changeset
    39
  $rule$ without facts is plain \emph{introduction}, while with facts it
wenzelm
parents: 7319
diff changeset
    40
  becomes an \emph{elimination}.
wenzelm
parents: 7319
diff changeset
    41
  
wenzelm
parents: 7319
diff changeset
    42
  Note that the classical reasoner introduces another version of $rule$ that
wenzelm
parents: 7319
diff changeset
    43
  is able to pick appropriate rules automatically, whenever explicit $thms$
wenzelm
parents: 7319
diff changeset
    44
  are omitted (see \S\ref{sec:classical-basic}) .  That method is the default
wenzelm
parents: 7319
diff changeset
    45
  one for proof steps such as $\PROOFNAME$ and ``$\DDOT$'' (two dots).
wenzelm
parents: 7319
diff changeset
    46
  
wenzelm
parents: 7319
diff changeset
    47
\item [$erule~thms$] is similar to $rule$, but applies rules by
wenzelm
parents: 7319
diff changeset
    48
  elim-resolution.  This is an improper method, mainly for experimentation and
wenzelm
parents: 7319
diff changeset
    49
  porting of old script.  Actual elimination proofs are usually done with
wenzelm
parents: 7319
diff changeset
    50
  $rule$ (single step) or $elim$ (multiple steps, see
wenzelm
parents: 7319
diff changeset
    51
  \S\ref{sec:classical-basic}).
wenzelm
parents: 7319
diff changeset
    52
  
wenzelm
parents: 7319
diff changeset
    53
\item [$unfold~thms$ and $fold~thms$] expand and fold back again meta-level
wenzelm
parents: 7319
diff changeset
    54
  definitions $thms$ throughout all goals; facts may not be given.
7167
wenzelm
parents: 7141
diff changeset
    55
7321
wenzelm
parents: 7319
diff changeset
    56
\item [$fail$] yields an empty result sequence; it is the identify of the
wenzelm
parents: 7319
diff changeset
    57
  ``\texttt{|}'' method combinator.
wenzelm
parents: 7319
diff changeset
    58
  
wenzelm
parents: 7319
diff changeset
    59
\item [$succeed$] yields a singleton result, which is unchanged except for the
wenzelm
parents: 7319
diff changeset
    60
  change from $prove$ mode back to $state$; it is the identify of the
wenzelm
parents: 7319
diff changeset
    61
  ``\texttt{,}'' method combinator.
wenzelm
parents: 7319
diff changeset
    62
\end{descr}
7167
wenzelm
parents: 7141
diff changeset
    63
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    64
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    65
\section{Miscellaneous attributes}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    66
7167
wenzelm
parents: 7141
diff changeset
    67
\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
wenzelm
parents: 7141
diff changeset
    68
\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
wenzelm
parents: 7141
diff changeset
    69
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
wenzelm
parents: 7141
diff changeset
    70
\begin{matharray}{rcl}
wenzelm
parents: 7141
diff changeset
    71
  tag & : & \isaratt \\
7321
wenzelm
parents: 7319
diff changeset
    72
  untag & : & \isaratt \\[0.5ex]
wenzelm
parents: 7319
diff changeset
    73
  OF & : & \isaratt \\
7167
wenzelm
parents: 7141
diff changeset
    74
  RS & : & \isaratt \\
7321
wenzelm
parents: 7319
diff changeset
    75
  COMP & : & \isaratt \\[0.5ex]
7167
wenzelm
parents: 7141
diff changeset
    76
  where & : & \isaratt \\
7321
wenzelm
parents: 7319
diff changeset
    77
  of & : & \isaratt \\[0.5ex]
7167
wenzelm
parents: 7141
diff changeset
    78
  standard & : & \isaratt \\
wenzelm
parents: 7141
diff changeset
    79
  elimify & : & \isaratt \\
7321
wenzelm
parents: 7319
diff changeset
    80
  export & : & \isaratt \\
7167
wenzelm
parents: 7141
diff changeset
    81
  transfer & : & \isaratt \\
wenzelm
parents: 7141
diff changeset
    82
\end{matharray}
wenzelm
parents: 7141
diff changeset
    83
wenzelm
parents: 7141
diff changeset
    84
\begin{rail}
wenzelm
parents: 7141
diff changeset
    85
  ('tag' | 'untag') (nameref+)
wenzelm
parents: 7141
diff changeset
    86
  ;
wenzelm
parents: 7141
diff changeset
    87
  'OF' thmrefs
wenzelm
parents: 7141
diff changeset
    88
  ;
7321
wenzelm
parents: 7319
diff changeset
    89
  ('RS' | 'COMP') nat? thmref
7167
wenzelm
parents: 7141
diff changeset
    90
  ;
7175
wenzelm
parents: 7167
diff changeset
    91
  'of' (inst * ) ('concl' ':' (inst * ))?
7167
wenzelm
parents: 7141
diff changeset
    92
  ;
7321
wenzelm
parents: 7319
diff changeset
    93
  'where' (name '=' term * 'and')
wenzelm
parents: 7319
diff changeset
    94
  ;
7167
wenzelm
parents: 7141
diff changeset
    95
wenzelm
parents: 7141
diff changeset
    96
  inst: underscore | term
wenzelm
parents: 7141
diff changeset
    97
  ;
wenzelm
parents: 7141
diff changeset
    98
\end{rail}
wenzelm
parents: 7141
diff changeset
    99
wenzelm
parents: 7141
diff changeset
   100
\begin{descr}
7321
wenzelm
parents: 7319
diff changeset
   101
\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem,
wenzelm
parents: 7319
diff changeset
   102
  respectively.  Tags may be any list of strings that serve as comment for
wenzelm
parents: 7319
diff changeset
   103
  some tools (e.g.\ $\LEMMANAME$ causes tag ``$lemma$'' to be added to the
wenzelm
parents: 7319
diff changeset
   104
  result).
wenzelm
parents: 7319
diff changeset
   105
\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
wenzelm
parents: 7319
diff changeset
   106
  $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
wenzelm
parents: 7319
diff changeset
   107
  the reversed order).  $RS$ resolves with the $n$-th premise of $thm$; $COMP$
wenzelm
parents: 7319
diff changeset
   108
  is a version of $RS$ that does not include the automatic lifting process
wenzelm
parents: 7319
diff changeset
   109
  that is normally desired (see \texttt{RS} and \texttt{COMP} in
wenzelm
parents: 7319
diff changeset
   110
  \cite[\S5]{isabelle-ref}).
wenzelm
parents: 7319
diff changeset
   111
  
wenzelm
parents: 7319
diff changeset
   112
\item [$of~ts$ and $where~insts$] perform positional and named instantiation,
wenzelm
parents: 7319
diff changeset
   113
  respectively.  The terms given in $of$ are substituted for any variables
wenzelm
parents: 7319
diff changeset
   114
  occurring in a theorem from left to right; ``\texttt{_}'' (underscore)
wenzelm
parents: 7319
diff changeset
   115
  indicates to skip a position.
wenzelm
parents: 7319
diff changeset
   116
 
wenzelm
parents: 7319
diff changeset
   117
\item [$standard$] puts a theorem into the standard form of object-rules, just
wenzelm
parents: 7319
diff changeset
   118
  as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
wenzelm
parents: 7319
diff changeset
   119
  
wenzelm
parents: 7319
diff changeset
   120
\item [$elimify$] turns an destruction rule (such as projection $conjunct@1$
wenzelm
parents: 7319
diff changeset
   121
  into an elimination.
wenzelm
parents: 7319
diff changeset
   122
  
wenzelm
parents: 7319
diff changeset
   123
\item [$export$] lifts a local result out of the current proof context,
wenzelm
parents: 7319
diff changeset
   124
  generalizing all fixed variables and discharging all assumptions.  Export is
wenzelm
parents: 7319
diff changeset
   125
  usually done automatically behind the scenes.  This attribute is mainly for
wenzelm
parents: 7319
diff changeset
   126
  experimentation.
wenzelm
parents: 7319
diff changeset
   127
  
wenzelm
parents: 7319
diff changeset
   128
\item [$transfer$] promotes a theorem to the current theory context, which has
wenzelm
parents: 7319
diff changeset
   129
  to enclose the former one.  Normally, this is done automatically when rules
wenzelm
parents: 7319
diff changeset
   130
  are joined by inference.
wenzelm
parents: 7319
diff changeset
   131
7167
wenzelm
parents: 7141
diff changeset
   132
\end{descr}
wenzelm
parents: 7141
diff changeset
   133
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   134
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   135
\section{Calculational proof}\label{sec:calculation}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   136
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   137
\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   138
\begin{matharray}{rcl}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   139
  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   140
  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   141
  trans & : & \isaratt \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   142
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   143
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   144
Calculational proof is forward reasoning with implicit application of
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   145
transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   146
an auxiliary register $calculation$\indexisarreg{calculation} for accumulating
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   147
results obtained by transitivity obtained together with the current facts.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   148
Command $\ALSO$ updates $calculation$ from the most recent result, while
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   149
$\FINALLY$ exhibits the final result by forward chaining towards the next goal
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   150
statement.  Both commands require valid current facts, i.e.\ may occur only
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   151
after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   152
some finished $\HAVENAME$ or $\SHOWNAME$.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   153
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   154
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   155
application with calculational proofs.  It automatically refers to the
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   156
argument\footnote{The argument of a curried infix expression is its right-hand
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   157
  side.} of the preceding statement.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   158
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   159
Isabelle/Isar calculations are implicitly subject to block structure in the
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   160
sense that new threads of calculational reasoning are commenced for any new
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   161
block (as opened by a local goal, for example).  This means that, apart from
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   162
being able to nest calculations, there is no separate \emph{begin-calculation}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   163
command required.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   164
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   165
\begin{rail}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   166
  ('also' | 'finally') transrules? comment?
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   167
  ;
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   168
  'trans' (() | 'add' ':' | 'del' ':') thmrefs
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   169
  ;
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   170
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   171
  transrules: '(' thmrefs ')' interest?
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   172
  ;
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   173
\end{rail}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   174
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   175
\begin{descr}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   176
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   177
  follows.  The first occurrence of $\ALSO$ in some calculational thread
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   178
  initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   179
  \emph{same} level of block-structure updates $calculation$ by some
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   180
  transitivity rule applied to $calculation$ and $facts$ (in that order).
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   181
  Transitivity rules are picked from the current context plus those given as
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   182
  $thms$ (the latter have precedence).
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   183
  
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   184
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   185
  $\ALSO$, and concludes the current calculational thread.  The final result
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   186
  is exhibited as fact for forward chaining towards the next goal. Basically,
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   187
  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  A typical proof
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   188
  idiom is $\FINALLY~\SHOW~\VVar{thesis}~\DOT$.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   189
  
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   190
\item [Attribute $trans$] maintains the set of transitivity rules of the
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   191
  theory or proof context, by adding or deleting the theorems provided as
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   192
  arguments.  The default is adding of rules.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   193
\end{descr}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   194
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   195
See theory \texttt{HOL/Isar_examples/Group} for a simple applications of
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   196
calculations for basic equational reasoning.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   197
\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   198
calculational steps in combination with natural deduction.
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   199
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   200
7135
wenzelm
parents:
diff changeset
   201
\section{Axiomatic Type Classes}\label{sec:axclass}
wenzelm
parents:
diff changeset
   202
wenzelm
parents:
diff changeset
   203
\indexisarcmd{axclass}\indexisarcmd{instance}
wenzelm
parents:
diff changeset
   204
\begin{matharray}{rcl}
wenzelm
parents:
diff changeset
   205
  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
wenzelm
parents:
diff changeset
   206
  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
7319
wenzelm
parents: 7315
diff changeset
   207
  expand_classes & : & \isarmeth \\
7135
wenzelm
parents:
diff changeset
   208
\end{matharray}
wenzelm
parents:
diff changeset
   209
wenzelm
parents:
diff changeset
   210
Axiomatic type classes are provided by Isabelle/Pure as a purely
wenzelm
parents:
diff changeset
   211
\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
wenzelm
parents:
diff changeset
   212
any object logic may make use of this light-weight mechanism for abstract
wenzelm
parents:
diff changeset
   213
theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
wenzelm
parents:
diff changeset
   214
tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
wenzelm
parents:
diff changeset
   215
the standard Isabelle documentation.
wenzelm
parents:
diff changeset
   216
wenzelm
parents:
diff changeset
   217
\begin{rail}
wenzelm
parents:
diff changeset
   218
  'axclass' classdecl (axmdecl prop comment? +)
wenzelm
parents:
diff changeset
   219
  ;
wenzelm
parents:
diff changeset
   220
  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
wenzelm
parents:
diff changeset
   221
  ;
wenzelm
parents:
diff changeset
   222
\end{rail}
wenzelm
parents:
diff changeset
   223
7167
wenzelm
parents: 7141
diff changeset
   224
\begin{descr}
7321
wenzelm
parents: 7319
diff changeset
   225
\item [$\isarkeyword{axclass}~$] defines an axiomatic type class as the
wenzelm
parents: 7319
diff changeset
   226
  intersection of existing classes, with additional axioms holding.  Class
wenzelm
parents: 7319
diff changeset
   227
  axioms may not contain more than one type variable.  The class axioms (with
wenzelm
parents: 7319
diff changeset
   228
  implicit sort constraints added) are bound to the given names.  Furthermore
wenzelm
parents: 7319
diff changeset
   229
  a class introduction rule is generated, which is employed by method
wenzelm
parents: 7319
diff changeset
   230
  $expand_classes$ in support instantiation proofs of this class.
wenzelm
parents: 7319
diff changeset
   231
7135
wenzelm
parents:
diff changeset
   232
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
wenzelm
parents:
diff changeset
   233
  c@2$] setup up a goal stating the class relation or type arity.  The proof
wenzelm
parents:
diff changeset
   234
  would usually proceed by the $expand_classes$ method, and then establish the
7141
a67dde8820c0 even more stuff;
wenzelm
parents: 7135
diff changeset
   235
  characteristic theorems of the type classes involved.  After finishing the
a67dde8820c0 even more stuff;
wenzelm
parents: 7135
diff changeset
   236
  proof the theory will be augmented by a type signature declaration
7135
wenzelm
parents:
diff changeset
   237
  corresponding to the resulting theorem.
7319
wenzelm
parents: 7315
diff changeset
   238
\item [Method $expand_classes$] iteratively expands the class introduction
wenzelm
parents: 7315
diff changeset
   239
  rules
7167
wenzelm
parents: 7141
diff changeset
   240
\end{descr}
7135
wenzelm
parents:
diff changeset
   241
7319
wenzelm
parents: 7315
diff changeset
   242
See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
wenzelm
parents: 7315
diff changeset
   243
axiomatic type classes, including instantiation proofs.
7135
wenzelm
parents:
diff changeset
   244
wenzelm
parents:
diff changeset
   245
wenzelm
parents:
diff changeset
   246
\section{The Simplifier}
wenzelm
parents:
diff changeset
   247
7321
wenzelm
parents: 7319
diff changeset
   248
\subsection{Simplification methods}\label{sec:simp}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   249
7321
wenzelm
parents: 7319
diff changeset
   250
\indexisarmeth{simp}\indexisarmeth{asm_simp}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   251
\begin{matharray}{rcl}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   252
  simp & : & \isarmeth \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   253
  asm_simp & : & \isarmeth \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   254
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   255
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   256
\begin{rail}
7319
wenzelm
parents: 7315
diff changeset
   257
  'simp' (simpmod * )
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   258
  ;
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   259
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   260
  simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   261
  ;
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   262
\end{rail}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   263
7321
wenzelm
parents: 7319
diff changeset
   264
\begin{descr}
wenzelm
parents: 7319
diff changeset
   265
\item [Methods $simp$ and $asm_simp$] invoke Isabelle's simplifier, after
wenzelm
parents: 7319
diff changeset
   266
  modifying the context as follows adding or deleting given rules.  The
wenzelm
parents: 7319
diff changeset
   267
  \railtoken{only} modifier first removes all other rewrite rules and
wenzelm
parents: 7319
diff changeset
   268
  congruences, and then is like \railtoken{add}.  In contrast,
wenzelm
parents: 7319
diff changeset
   269
  \railtoken{other} ignores its arguments; nevertheless there may be
wenzelm
parents: 7319
diff changeset
   270
  side-effects on the context via attributes.  This provides a back door for
wenzelm
parents: 7319
diff changeset
   271
  arbitrary manipulation of the context.
wenzelm
parents: 7319
diff changeset
   272
  
wenzelm
parents: 7319
diff changeset
   273
  Both of these methods are based on \texttt{asm_full_simp_tac}, see
wenzelm
parents: 7319
diff changeset
   274
  \cite[\S10]{isabelle-ref}.
wenzelm
parents: 7319
diff changeset
   275
\end{descr}
wenzelm
parents: 7319
diff changeset
   276
wenzelm
parents: 7319
diff changeset
   277
\subsection{Modifying the context}
wenzelm
parents: 7319
diff changeset
   278
wenzelm
parents: 7319
diff changeset
   279
\indexisaratt{simp}
wenzelm
parents: 7319
diff changeset
   280
\begin{matharray}{rcl}
wenzelm
parents: 7319
diff changeset
   281
  simp & : & \isaratt \\
wenzelm
parents: 7319
diff changeset
   282
\end{matharray}
wenzelm
parents: 7319
diff changeset
   283
wenzelm
parents: 7319
diff changeset
   284
\begin{rail}
wenzelm
parents: 7319
diff changeset
   285
  'simp' (() | 'add' | 'del')
wenzelm
parents: 7319
diff changeset
   286
  ;
wenzelm
parents: 7319
diff changeset
   287
\end{rail}
wenzelm
parents: 7319
diff changeset
   288
wenzelm
parents: 7319
diff changeset
   289
\begin{descr}
wenzelm
parents: 7319
diff changeset
   290
\item [Attribute $simp$] adds or deletes rules from the theory or proof
wenzelm
parents: 7319
diff changeset
   291
  context.  The default is to add rules.
wenzelm
parents: 7319
diff changeset
   292
\end{descr}
7319
wenzelm
parents: 7315
diff changeset
   293
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   294
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   295
\subsection{Forward simplification}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   296
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   297
\indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   298
\begin{matharray}{rcl}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   299
  simplify & : & \isaratt \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   300
  asm_simplify & : & \isaratt \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   301
  full_simplify & : & \isaratt \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   302
  asm_full_simplify & : & \isaratt \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   303
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   304
7321
wenzelm
parents: 7319
diff changeset
   305
These attributes provide forward rules for simplification, which should be
wenzelm
parents: 7319
diff changeset
   306
used very rarely.  See the ML function of the same name in
wenzelm
parents: 7319
diff changeset
   307
\cite[\S10]{isabelle-ref} for more information.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   308
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   309
7135
wenzelm
parents:
diff changeset
   310
\section{The Classical Reasoner}
wenzelm
parents:
diff changeset
   311
7321
wenzelm
parents: 7319
diff changeset
   312
\subsection{Basic step methods}\label{sec:classical-basic}
wenzelm
parents: 7319
diff changeset
   313
wenzelm
parents: 7319
diff changeset
   314
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
wenzelm
parents: 7319
diff changeset
   315
\begin{matharray}{rcl}
wenzelm
parents: 7319
diff changeset
   316
  rule & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   317
  intro & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   318
  elim & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   319
  contradiction & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   320
\end{matharray}
wenzelm
parents: 7319
diff changeset
   321
wenzelm
parents: 7319
diff changeset
   322
\begin{rail}
wenzelm
parents: 7319
diff changeset
   323
  ('rule' | 'intro' | 'elim') thmrefs
wenzelm
parents: 7319
diff changeset
   324
  ;
wenzelm
parents: 7319
diff changeset
   325
\end{rail}
wenzelm
parents: 7319
diff changeset
   326
wenzelm
parents: 7319
diff changeset
   327
\begin{descr}
wenzelm
parents: 7319
diff changeset
   328
\item [Method $rule$] as offered by the classical reasoner is a refinement
wenzelm
parents: 7319
diff changeset
   329
  over the primitive one (see \S\ref{sec:pure-meth}).  In the case that no
wenzelm
parents: 7319
diff changeset
   330
  rules are provided as arguments, it automatically determines elimination and
wenzelm
parents: 7319
diff changeset
   331
  introduction rules from the context (see also \S\ref{sec:classical-mod}).
wenzelm
parents: 7319
diff changeset
   332
  In that form it is the default method for basic proof steps.
wenzelm
parents: 7319
diff changeset
   333
  
wenzelm
parents: 7319
diff changeset
   334
\item [Methods $intro$ and $elim$] repeatedly refine some goal by intro- or
wenzelm
parents: 7319
diff changeset
   335
  elim-resolution, after having inserted the facts.  Omitting the arguments
wenzelm
parents: 7319
diff changeset
   336
  refers to any suitable rules from the context, otherwise only the explicitly
wenzelm
parents: 7319
diff changeset
   337
  given ones may be applied.  The latter form admits better control of what is
wenzelm
parents: 7319
diff changeset
   338
  actually happening, thus it is appropriate as an initial proof method that
wenzelm
parents: 7319
diff changeset
   339
  splits up certain connectives of the goal, before entering the sub-proof.
wenzelm
parents: 7319
diff changeset
   340
wenzelm
parents: 7319
diff changeset
   341
\item [Method $contradiction$] solves some goal by contradiction: both $A$ and
wenzelm
parents: 7319
diff changeset
   342
  $\neg A$ have to be present in the assumptions.
wenzelm
parents: 7319
diff changeset
   343
\end{descr}
wenzelm
parents: 7319
diff changeset
   344
wenzelm
parents: 7319
diff changeset
   345
wenzelm
parents: 7319
diff changeset
   346
\subsection{Automatic methods}\label{sec:classical-auto}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   347
7321
wenzelm
parents: 7319
diff changeset
   348
\indexisarmeth{blast}
wenzelm
parents: 7319
diff changeset
   349
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow_best}
wenzelm
parents: 7319
diff changeset
   350
\begin{matharray}{rcl}
wenzelm
parents: 7319
diff changeset
   351
 blast & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   352
 fast & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   353
 best & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   354
 slow & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   355
 slow_best & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   356
\end{matharray}
wenzelm
parents: 7319
diff changeset
   357
wenzelm
parents: 7319
diff changeset
   358
\railalias{slowbest}{slow\_best}
wenzelm
parents: 7319
diff changeset
   359
\railterm{slowbest}
wenzelm
parents: 7319
diff changeset
   360
wenzelm
parents: 7319
diff changeset
   361
\begin{rail}
wenzelm
parents: 7319
diff changeset
   362
  'blast' nat? (clamod * )
wenzelm
parents: 7319
diff changeset
   363
  ;
wenzelm
parents: 7319
diff changeset
   364
  ('fast' | 'best' | 'slow' | slowbest) (clamod * )
wenzelm
parents: 7319
diff changeset
   365
  ;
wenzelm
parents: 7319
diff changeset
   366
wenzelm
parents: 7319
diff changeset
   367
  clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
wenzelm
parents: 7319
diff changeset
   368
  ;
wenzelm
parents: 7319
diff changeset
   369
\end{rail}
wenzelm
parents: 7319
diff changeset
   370
wenzelm
parents: 7319
diff changeset
   371
\begin{descr}
wenzelm
parents: 7319
diff changeset
   372
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
wenzelm
parents: 7319
diff changeset
   373
  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a applies a
wenzelm
parents: 7319
diff changeset
   374
  user-supplied search bound (default 20).
wenzelm
parents: 7319
diff changeset
   375
\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
wenzelm
parents: 7319
diff changeset
   376
  reasoner (see the corresponding tactics \texttt{fast_tac} etc.\ in
wenzelm
parents: 7319
diff changeset
   377
  \cite[\S11]{isabelle-ref}).
wenzelm
parents: 7319
diff changeset
   378
\end{descr}
wenzelm
parents: 7319
diff changeset
   379
wenzelm
parents: 7319
diff changeset
   380
Any of above methods support additional modifiers of the context of classical
wenzelm
parents: 7319
diff changeset
   381
rules.  There semantics is analogous to the attributes given in
wenzelm
parents: 7319
diff changeset
   382
\S\ref{sec:classical-mod}.
wenzelm
parents: 7319
diff changeset
   383
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   384
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   385
\subsection{Combined automatic methods}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   386
7321
wenzelm
parents: 7319
diff changeset
   387
\indexisarmeth{auto}\indexisarmeth{force}
wenzelm
parents: 7319
diff changeset
   388
\begin{matharray}{rcl}
wenzelm
parents: 7319
diff changeset
   389
  force & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   390
  auto & : & \isarmeth \\
wenzelm
parents: 7319
diff changeset
   391
\end{matharray}
wenzelm
parents: 7319
diff changeset
   392
wenzelm
parents: 7319
diff changeset
   393
\begin{rail}
wenzelm
parents: 7319
diff changeset
   394
  ('force' | 'auto') (clasimpmod * )
wenzelm
parents: 7319
diff changeset
   395
  ;
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   396
7321
wenzelm
parents: 7319
diff changeset
   397
  clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
wenzelm
parents: 7319
diff changeset
   398
    (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
wenzelm
parents: 7319
diff changeset
   399
\end{rail}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   400
7321
wenzelm
parents: 7319
diff changeset
   401
\begin{descr}
wenzelm
parents: 7319
diff changeset
   402
\item [$force$ and $auto$] provide access to Isabelle's combined
wenzelm
parents: 7319
diff changeset
   403
  simplification and classical reasoning tactics.  See \texttt{force_tac} and
wenzelm
parents: 7319
diff changeset
   404
  \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
wenzelm
parents: 7319
diff changeset
   405
  modifier arguments correspond to those given in \S\ref{sec:simp} and
wenzelm
parents: 7319
diff changeset
   406
  \S\ref{sec:classical-auto}.
wenzelm
parents: 7319
diff changeset
   407
\end{descr}
wenzelm
parents: 7319
diff changeset
   408
wenzelm
parents: 7319
diff changeset
   409
\subsection{Modifying the context}\label{sec:classical-mod}
7135
wenzelm
parents:
diff changeset
   410
7321
wenzelm
parents: 7319
diff changeset
   411
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{delrule}
wenzelm
parents: 7319
diff changeset
   412
\begin{matharray}{rcl}
wenzelm
parents: 7319
diff changeset
   413
  intro & : & \isaratt \\
wenzelm
parents: 7319
diff changeset
   414
  elim & : & \isaratt \\
wenzelm
parents: 7319
diff changeset
   415
  dest & : & \isaratt \\
wenzelm
parents: 7319
diff changeset
   416
  delrule & : & \isaratt \\
wenzelm
parents: 7319
diff changeset
   417
\end{matharray}
7135
wenzelm
parents:
diff changeset
   418
7321
wenzelm
parents: 7319
diff changeset
   419
\begin{rail}
wenzelm
parents: 7319
diff changeset
   420
  ('intro' | 'elim' | 'dest') (() | '!' | '!!')
wenzelm
parents: 7319
diff changeset
   421
  ;
wenzelm
parents: 7319
diff changeset
   422
\end{rail}
7135
wenzelm
parents:
diff changeset
   423
7321
wenzelm
parents: 7319
diff changeset
   424
\begin{descr}
wenzelm
parents: 7319
diff changeset
   425
\item [Attributes $intro$, $elim$, and $dest$] add introduction, elimination,
wenzelm
parents: 7319
diff changeset
   426
  and destruct rules, respectively.  By default, rules are considered as
wenzelm
parents: 7319
diff changeset
   427
  \emph{safe}, while a single ``!'' classifies as \emph{unsafe}, and ``!!'' as
wenzelm
parents: 7319
diff changeset
   428
  \emph{extra} (i.e.\ not applied in the search-oriented automatic methods).
wenzelm
parents: 7319
diff changeset
   429
wenzelm
parents: 7319
diff changeset
   430
\item [Attribute $delrule$] deletes introduction or elimination rules from the
wenzelm
parents: 7319
diff changeset
   431
  context.  Destruction rules would have to be turned into elimination rules
wenzelm
parents: 7319
diff changeset
   432
  first, e.g.\ by using the $elimify$ attribute.
wenzelm
parents: 7319
diff changeset
   433
\end{descr}
7135
wenzelm
parents:
diff changeset
   434
wenzelm
parents:
diff changeset
   435
wenzelm
parents:
diff changeset
   436
%%% Local Variables: 
wenzelm
parents:
diff changeset
   437
%%% mode: latex
wenzelm
parents:
diff changeset
   438
%%% TeX-master: "isar-ref"
wenzelm
parents:
diff changeset
   439
%%% End: