doc-src/IsarRef/generic.tex
author wenzelm
Sat Apr 08 22:51:06 2006 +0200 (2006-04-08)
changeset 19363 667b5ea637dd
parent 19145 990f59414e34
child 19379 c8cf1544b5a7
permissions -rw-r--r--
refined 'abbreviation';
wenzelm@7135
     1
wenzelm@13048
     2
\chapter{Generic tools and packages}\label{ch:gen-tools}
wenzelm@7167
     3
wenzelm@12621
     4
\section{Theory specification commands}
wenzelm@12618
     5
wenzelm@19070
     6
\subsection{Derived specifications}
wenzelm@19070
     7
wenzelm@19070
     8
\indexisarcmd{definition}\indexisaratt{defn}
wenzelm@19070
     9
\indexisarcmd{abbreviation}\indexisarcmd{axiomatization}
wenzelm@19070
    10
\begin{matharray}{rcll}
wenzelm@19070
    11
  \isarcmd{definition} & : & \isarkeep{local{\dsh}theory} \\
wenzelm@19070
    12
  defn & : & \isaratt \\
wenzelm@19070
    13
  \isarcmd{abbreviation} & : & \isarkeep{local{\dsh}theory} \\
wenzelm@19070
    14
  \isarcmd{axiomatization} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
wenzelm@19070
    15
\end{matharray}
wenzelm@19070
    16
wenzelm@19070
    17
These specification mechanisms provide a slightly more abstract view
wenzelm@19070
    18
than the underlying primitives of $\CONSTS$, $\DEFS$ (see
wenzelm@19070
    19
\S\ref{sec:consts}), and $\isarkeyword{axioms}$ (see
wenzelm@19070
    20
\S\ref{sec:axms-thms}).  In particular, type-inference is commonly
wenzelm@19070
    21
available, and result names need not be given.
wenzelm@19070
    22
wenzelm@19070
    23
\begin{rail}
wenzelm@19070
    24
  'definition' locale? (constdecl? constdef +)
wenzelm@19070
    25
  ;
wenzelm@19070
    26
wenzelm@19363
    27
  'abbreviation' locale? mode? (constdecl? prop +)
wenzelm@19070
    28
  ;
wenzelm@19070
    29
  'axiomatization' locale? consts? ('where' specs)?
wenzelm@19070
    30
  ;
wenzelm@19070
    31
wenzelm@19070
    32
  consts: ((name ('::' type)? structmixfix? | vars) + 'and')
wenzelm@19070
    33
  ;
wenzelm@19070
    34
  specs: (thmdecl? props + 'and')
wenzelm@19070
    35
  ;
wenzelm@19070
    36
\end{rail}
wenzelm@19070
    37
wenzelm@19070
    38
\begin{descr}
wenzelm@19070
    39
  
wenzelm@19070
    40
\item $\isarkeyword{definition}~c~\isarkeyword{where}~eq$ produces an
wenzelm@19070
    41
  internal definition $c \equiv t$ according to the specification
wenzelm@19070
    42
  given as $eq$, which is then turned into a proven fact.  The given
wenzelm@19070
    43
  proposition may deviate from internal meta-level equality according
wenzelm@19070
    44
  to the rewrite rules declared as $defn$ by the object-logic.  This
wenzelm@19070
    45
  typically covers object-level equality $x = t$ and equivalence $A
wenzelm@19070
    46
  \leftrightarrow B$.  Users normally need not change the $defn$
wenzelm@19070
    47
  setup.
wenzelm@19070
    48
  
wenzelm@19070
    49
  Definitions may be presented with explicit arguments on the LHS, as
wenzelm@19070
    50
  well as additional conditions, e.g.\ $f\;x\;y = t$ instead of $f
wenzelm@19070
    51
  \equiv \lambda x\;y. t$ and $y \not= 0 \Imp g\;x\;y = u$ instead of
wenzelm@19070
    52
  an unguarded $g \equiv \lambda x\;y. u$.
wenzelm@19070
    53
  
wenzelm@19070
    54
  Multiple definitions are processed consecutively; no overloading is
wenzelm@19070
    55
  supported here.
wenzelm@19070
    56
  
wenzelm@19070
    57
\item $\isarkeyword{abbreviation}~c~\isarkeyword{where}~eq$ introduces
wenzelm@19363
    58
  a syntactic constant which is associated with a certain term
wenzelm@19363
    59
  according to the meta-level equality $eq$.
wenzelm@19070
    60
  
wenzelm@19070
    61
  Abbreviations participate in the usual type-inference process, but
wenzelm@19363
    62
  are expanded before the logic ever sees them.  Pretty printing of
wenzelm@19363
    63
  terms involves higher-order rewriting with rules stemming from
wenzelm@19363
    64
  reverted abbreviations.  This needs some care to avoid overlapping
wenzelm@19363
    65
  or looping syntactic replacements!
wenzelm@19363
    66
  
wenzelm@19363
    67
  The optional $mode$ specification restricts output to a particular
wenzelm@19363
    68
  print mode; using ``$input$'' here achieves the effect of one-way
wenzelm@19363
    69
  abbreviations.  The mode may also include an ``$output$'' qualifier
wenzelm@19363
    70
  that affects the concrete syntax declared for abbreviations, cf.\ 
wenzelm@19363
    71
  $\isarkeyword{syntax}$ in \S\ref{sec:syn-trans}.
wenzelm@19070
    72
  
wenzelm@19070
    73
\item $\isarkeyword{axiomatization} ~ c@1 \dots c@n ~
wenzelm@19070
    74
  \isarkeyword{where} ~ A@1 \dots A@m$ introduces several constants
wenzelm@19070
    75
  simultaneously and states axiomatic properties for these.  The
wenzelm@19070
    76
  constants are marked as being specified once and for all, which
wenzelm@19070
    77
  prevents additional specifications being issued later on.
wenzelm@19070
    78
  
wenzelm@19070
    79
  Note that axiomatic specifications are only appropriate when
wenzelm@19070
    80
  declaring a new logical system.  Normal applications should only use
wenzelm@19070
    81
  definitional mechanisms!
wenzelm@19070
    82
wenzelm@19070
    83
\end{descr}
wenzelm@19070
    84
wenzelm@19070
    85
Any of these specifications support an optional target locale context
wenzelm@19070
    86
(cf.\ \S\ref{sec:locale}).  In the latter case, constants being
wenzelm@19070
    87
introduced depend on certain fixed parameters of the locale context;
wenzelm@19070
    88
the constant name is qualified by the locale base name.  A syntactic
wenzelm@19070
    89
abbreviation takes care for convenient input and output of such terms,
wenzelm@19070
    90
making the parameters implicit and using the original short name.
wenzelm@19070
    91
Outside the locale context, the specified entities are available in
wenzelm@19070
    92
generalized form, with the parameters being open to explicit
wenzelm@19070
    93
instantiation.
wenzelm@19070
    94
wenzelm@19070
    95
wenzelm@12618
    96
\subsection{Axiomatic type classes}\label{sec:axclass}
wenzelm@7167
    97
wenzelm@8517
    98
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
wenzelm@7167
    99
\begin{matharray}{rcl}
wenzelm@8517
   100
  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
wenzelm@8517
   101
  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@8517
   102
  intro_classes & : & \isarmeth \\
wenzelm@7167
   103
\end{matharray}
wenzelm@7167
   104
wenzelm@8517
   105
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
wenzelm@8517
   106
interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
wenzelm@8547
   107
may make use of this light-weight mechanism of abstract theories
wenzelm@8901
   108
\cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type
wenzelm@13024
   109
classes in Isabelle \cite{isabelle-axclass} that is part of the standard
wenzelm@8901
   110
Isabelle documentation.
wenzelm@8517
   111
wenzelm@7167
   112
\begin{rail}
wenzelm@12879
   113
  'axclass' classdecl (axmdecl prop +)
wenzelm@8517
   114
  ;
wenzelm@14605
   115
  'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
wenzelm@7167
   116
  ;
wenzelm@7167
   117
\end{rail}
wenzelm@7167
   118
wenzelm@7167
   119
\begin{descr}
wenzelm@17274
   120
  
wenzelm@13024
   121
\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
wenzelm@11100
   122
  the intersection of existing classes, with additional axioms holding.  Class
wenzelm@10223
   123
  axioms may not contain more than one type variable.  The class axioms (with
wenzelm@10223
   124
  implicit sort constraints added) are bound to the given names.  Furthermore
wenzelm@17274
   125
  a class introduction rule is generated (being bound as
wenzelm@17274
   126
  $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to
wenzelm@17274
   127
  support instantiation proofs of this class.
wenzelm@17274
   128
  
wenzelm@12976
   129
  The ``axioms'' are stored as theorems according to the given name
wenzelm@13039
   130
  specifications, adding the class name $c$ as name space prefix; the same
wenzelm@17274
   131
  facts are also stored collectively as $c_class{\dtt}axioms$.
wenzelm@14605
   132
  
wenzelm@14605
   133
\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
wenzelm@11100
   134
  goal stating a class relation or type arity.  The proof would usually
wenzelm@11100
   135
  proceed by $intro_classes$, and then establish the characteristic theorems
wenzelm@11100
   136
  of the type classes involved.  After finishing the proof, the theory will be
wenzelm@11100
   137
  augmented by a type signature declaration corresponding to the resulting
wenzelm@11100
   138
  theorem.
wenzelm@13041
   139
wenzelm@8517
   140
\item [$intro_classes$] repeatedly expands all class introduction rules of
wenzelm@10858
   141
  this theory.  Note that this method usually needs not be named explicitly,
wenzelm@13040
   142
  as it is already included in the default proof step (of $\PROOFNAME$ etc.).
wenzelm@13040
   143
  In particular, instantiation of trivial (syntactic) classes may be performed
wenzelm@13040
   144
  by a single ``$\DDOT$'' proof step.
wenzelm@13027
   145
wenzelm@7167
   146
\end{descr}
wenzelm@7167
   147
wenzelm@7315
   148
wenzelm@12618
   149
\subsection{Locales and local contexts}\label{sec:locale}
wenzelm@12618
   150
wenzelm@13040
   151
Locales are named local contexts, consisting of a list of declaration elements
wenzelm@13041
   152
that are modeled after the Isar proof context commands (cf.\
wenzelm@13040
   153
\S\ref{sec:proof-context}).
wenzelm@12976
   154
wenzelm@13048
   155
wenzelm@12976
   156
\subsubsection{Localized commands}
wenzelm@12618
   157
wenzelm@12976
   158
Existing locales may be augmented later on by adding new facts.  Note that the
wenzelm@12976
   159
actual context definition may not be changed!  Several theory commands that
wenzelm@12976
   160
produce facts in some way are available in ``localized'' versions, referring
wenzelm@12976
   161
to a named locale instead of the global theory context.
wenzelm@12967
   162
wenzelm@12976
   163
\indexouternonterm{locale}
wenzelm@12967
   164
\begin{rail}
wenzelm@12967
   165
  locale: '(' 'in' name ')'
wenzelm@12967
   166
  ;
wenzelm@12976
   167
\end{rail}
wenzelm@12967
   168
wenzelm@12976
   169
Emerging facts of localized commands are stored in two versions, both in the
wenzelm@12976
   170
target locale and the theory (after export).  The latter view produces a
wenzelm@12976
   171
qualified binding, using the locale name as a name space prefix.
wenzelm@12976
   172
wenzelm@12976
   173
For example, ``$\LEMMAS~(\IN~loc)~a = \vec b$'' retrieves facts $\vec b$ from
wenzelm@12976
   174
the locale context of $loc$ and augments its body by an appropriate
wenzelm@12976
   175
``$\isarkeyword{notes}$'' element (see below).  The exported view of $a$,
wenzelm@12976
   176
after discharging the locale context, is stored as $loc{.}a$ within the global
wenzelm@13041
   177
theory.  A localized goal ``$\LEMMANAME~(\IN~loc)~a:~\phi$'' works similarly,
wenzelm@13041
   178
only that the fact emerges through the subsequent proof, which may refer to
wenzelm@13041
   179
the full infrastructure of the locale context (covering local parameters with
wenzelm@13041
   180
typing and concrete syntax, assumptions, definitions etc.).  Most notably,
wenzelm@13411
   181
fact declarations of the locale are active during the proof as well (e.g.\ 
wenzelm@13041
   182
local $simp$ rules).
wenzelm@12976
   183
wenzelm@13411
   184
As a general principle, results exported from a locale context acquire
wenzelm@13411
   185
additional premises according to the specification.  Usually this is only a
wenzelm@13411
   186
single predicate according to the standard ``closed'' view of locale
wenzelm@13411
   187
specifications.
wenzelm@13411
   188
wenzelm@12976
   189
wenzelm@12976
   190
\subsubsection{Locale specifications}
wenzelm@12976
   191
wenzelm@12976
   192
\indexisarcmd{locale}\indexisarcmd{print-locale}\indexisarcmd{print-locales}
wenzelm@12976
   193
\begin{matharray}{rcl}
wenzelm@19070
   194
  \isarcmd{locale} & : & \isartrans{theory}{local{\dsh}theory} \\
wenzelm@12976
   195
  \isarcmd{print_locale}^* & : & \isarkeep{theory~|~proof} \\
wenzelm@12976
   196
  \isarcmd{print_locales}^* & : & \isarkeep{theory~|~proof} \\
wenzelm@12976
   197
\end{matharray}
wenzelm@12976
   198
wenzelm@12976
   199
\indexouternonterm{contextexpr}\indexouternonterm{contextelem}
wenzelm@18903
   200
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
wenzelm@18903
   201
\indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
wenzelm@12976
   202
wenzelm@12976
   203
\begin{rail}
wenzelm@13411
   204
  'locale' ('(open)')? name ('=' localeexpr)?
wenzelm@12976
   205
  ;
wenzelm@18903
   206
  'print\_locale' '!'? localeexpr
wenzelm@12976
   207
  ;
wenzelm@12976
   208
  localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
wenzelm@12976
   209
  ;
wenzelm@12976
   210
wenzelm@12976
   211
  contextexpr: nameref | '(' contextexpr ')' |
ballarin@16102
   212
  (contextexpr (name mixfix? +)) | (contextexpr + '+')
wenzelm@12976
   213
  ;
ballarin@16168
   214
  contextelem: fixes | constrains | assumes | defines | notes | includes
wenzelm@12976
   215
  ;
wenzelm@18854
   216
  fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
wenzelm@12976
   217
  ;
ballarin@16168
   218
  constrains: 'constrains' (name '::' type + 'and')
ballarin@16168
   219
  ;
wenzelm@12976
   220
  assumes: 'assumes' (thmdecl? props + 'and')
wenzelm@12976
   221
  ;
wenzelm@12976
   222
  defines: 'defines' (thmdecl? prop proppat? + 'and')
wenzelm@12976
   223
  ;
wenzelm@12976
   224
  notes: 'notes' (thmdef? thmrefs + 'and')
wenzelm@12976
   225
  ;
wenzelm@12976
   226
  includes: 'includes' contextexpr
wenzelm@12976
   227
  ;
wenzelm@12967
   228
\end{rail}
wenzelm@12618
   229
wenzelm@12976
   230
\begin{descr}
wenzelm@13411
   231
  
wenzelm@13411
   232
\item [$\LOCALE~loc~=~import~+~body$] defines a new locale $loc$ as a context
wenzelm@12976
   233
  consisting of a certain view of existing locales ($import$) plus some
wenzelm@12976
   234
  additional elements ($body$).  Both $import$ and $body$ are optional; the
wenzelm@13024
   235
  degenerate form $\LOCALE~loc$ defines an empty locale, which may still be
wenzelm@13024
   236
  useful to collect declarations of facts later on.  Type-inference on locale
wenzelm@12976
   237
  expressions automatically takes care of the most general typing that the
wenzelm@12976
   238
  combined context elements may acquire.
wenzelm@13041
   239
wenzelm@12976
   240
  The $import$ consists of a structured context expression, consisting of
wenzelm@12976
   241
  references to existing locales, renamed contexts, or merged contexts.
ballarin@16102
   242
  Renaming uses positional notation: $c~\vec x$ means that (a prefix of) the
wenzelm@12976
   243
  fixed parameters of context $c$ are named according to $\vec x$; a
ballarin@16102
   244
  ``\texttt{_}'' (underscore) \indexisarthm{_@\texttt{_}} means to skip that
ballarin@16102
   245
  position.  Renaming by default deletes existing syntax.  Optionally,
ballarin@16102
   246
  new syntax may by specified with a mixfix annotation.  Note that the
ballarin@16102
   247
  special syntax declared with ``$(structure)$'' (see below) is
ballarin@16102
   248
  neither deleted nor can it be changed.
wenzelm@13041
   249
  Merging proceeds from left-to-right, suppressing any duplicates stemming
wenzelm@13041
   250
  from different paths through the import hierarchy.
wenzelm@13041
   251
wenzelm@12976
   252
  The $body$ consists of basic context elements, further context expressions
wenzelm@12976
   253
  may be included as well.
wenzelm@12976
   254
wenzelm@12976
   255
  \begin{descr}
wenzelm@13041
   256
wenzelm@12976
   257
  \item [$\FIXES{~x::\tau~(mx)}$] declares a local parameter of type $\tau$
wenzelm@12976
   258
    and mixfix annotation $mx$ (both are optional).  The special syntax
wenzelm@13027
   259
    declaration ``$(structure)$'' means that $x$ may be referenced
wenzelm@13027
   260
    implicitly in this context.
wenzelm@13041
   261
ballarin@16168
   262
  \item [$\CONSTRAINS{~x::\tau}$] introduces a type constraint $\tau$
ballarin@16168
   263
    on the local parameter $x$.
ballarin@16168
   264
wenzelm@12976
   265
  \item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to
wenzelm@12976
   266
    $\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}).
wenzelm@13041
   267
wenzelm@12976
   268
  \item [$\DEFINES{a}{x \equiv t}$] defines a previously declared parameter.
wenzelm@13041
   269
    This is close to $\DEFNAME$ within a proof (cf.\
wenzelm@12976
   270
    \S\ref{sec:proof-context}), but $\DEFINESNAME$ takes an equational
wenzelm@13041
   271
    proposition instead of variable-term pair.  The left-hand side of the
wenzelm@13041
   272
    equation may have additional arguments, e.g.\ ``$\DEFINES{}{f~\vec x
wenzelm@13041
   273
      \equiv t}$''.
wenzelm@13041
   274
wenzelm@12976
   275
  \item [$\NOTES{a}{\vec b}$] reconsiders facts within a local context.  Most
wenzelm@12976
   276
    notably, this may include arbitrary declarations in any attribute
wenzelm@12976
   277
    specifications included here, e.g.\ a local $simp$ rule.
wenzelm@13041
   278
wenzelm@12976
   279
  \item [$\INCLUDES{c}$] copies the specified context in a statically scoped
ballarin@15763
   280
    manner.  Only available in the long goal format of \S\ref{sec:goals}.
wenzelm@13041
   281
wenzelm@12976
   282
    In contrast, the initial $import$ specification of a locale expression
wenzelm@12976
   283
    maintains a dynamic relation to the locales being referenced (benefiting
wenzelm@12976
   284
    from any later fact declarations in the obvious manner).
wenzelm@12976
   285
  \end{descr}
wenzelm@13411
   286
  
wenzelm@13041
   287
  Note that ``$\IS{p}$'' patterns given in the syntax of $\ASSUMESNAME$ and
wenzelm@13411
   288
  $\DEFINESNAME$ above are illegal in locale definitions.  In the long goal
wenzelm@13411
   289
  format of \S\ref{sec:goals}, term bindings may be included as expected,
wenzelm@13411
   290
  though.
wenzelm@13411
   291
  
wenzelm@13411
   292
  \medskip By default, locale specifications are ``closed up'' by turning the
wenzelm@13411
   293
  given text into a predicate definition $loc_axioms$ and deriving the
wenzelm@13411
   294
  original assumptions as local lemmas (modulo local definitions).  The
wenzelm@13411
   295
  predicate statement covers only the newly specified assumptions, omitting
wenzelm@13411
   296
  the content of included locale expressions.  The full cumulative view is
wenzelm@13411
   297
  only provided on export, involving another predicate $loc$ that refers to
wenzelm@13411
   298
  the complete specification text.
wenzelm@13411
   299
  
wenzelm@13411
   300
  In any case, the predicate arguments are those locale parameters that
wenzelm@13411
   301
  actually occur in the respective piece of text.  Also note that these
wenzelm@13411
   302
  predicates operate at the meta-level in theory, but the locale packages
wenzelm@13411
   303
  attempts to internalize statements according to the object-logic setup
wenzelm@13411
   304
  (e.g.\ replacing $\Forall$ by $\forall$, and $\Imp$ by $\imp$ in HOL; see
wenzelm@13411
   305
  also \S\ref{sec:object-logic}).  Separate introduction rules
wenzelm@13411
   306
  $loc_axioms.intro$ and $loc.intro$ are declared as well.
wenzelm@13411
   307
  
wenzelm@13411
   308
  The $(open)$ option of a locale specification prevents both the current
wenzelm@13411
   309
  $loc_axioms$ and cumulative $loc$ predicate constructions.  Predicates are
wenzelm@13411
   310
  also omitted for empty specification texts.
wenzelm@12976
   311
wenzelm@12976
   312
\item [$\isarkeyword{print_locale}~import~+~body$] prints the specified locale
wenzelm@12976
   313
  expression in a flattened form.  The notable special case
wenzelm@12976
   314
  $\isarkeyword{print_locale}~loc$ just prints the contents of the named
wenzelm@12976
   315
  locale, but keep in mind that type-inference will normalize type variables
ballarin@17228
   316
  according to the usual alphabetical order.  The command omits
ballarin@17228
   317
  $\isarkeyword{notes}$ elements by default.  Use
ballarin@17228
   318
  $\isarkeyword{print_locale}!$ to get them included.
wenzelm@13041
   319
wenzelm@12976
   320
\item [$\isarkeyword{print_locales}$] prints the names of all locales of the
wenzelm@12976
   321
  current theory.
wenzelm@12976
   322
wenzelm@12976
   323
\end{descr}
wenzelm@12976
   324
wenzelm@12621
   325
ballarin@15763
   326
\subsubsection{Interpretation of locales}
ballarin@15763
   327
ballarin@15763
   328
Locale expressions (more precisely, \emph{context expressions}) may be
ballarin@15763
   329
instantiated, and the instantiated facts added to the current context.
ballarin@15763
   330
This requires a proof of the instantiated specification and is called
ballarin@15763
   331
\emph{locale interpretation}.  Interpretation is possible in theories
ballarin@17043
   332
and locales
ballarin@17043
   333
(command $\isarcmd{interpretation}$) and also in proof contexts
ballarin@15763
   334
($\isarcmd{interpret}$).
ballarin@15763
   335
ballarin@15763
   336
\indexisarcmd{interpretation}\indexisarcmd{interpret}
ballarin@15763
   337
\indexisarcmd{print-interps}
ballarin@15763
   338
\begin{matharray}{rcl}
ballarin@15763
   339
  \isarcmd{interpretation} & : & \isartrans{theory}{proof(prove)} \\
ballarin@15763
   340
  \isarcmd{interpret} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
ballarin@15763
   341
  \isarcmd{print_interps}^* & : &  \isarkeep{theory~|~proof} \\
ballarin@15763
   342
\end{matharray}
ballarin@15763
   343
ballarin@15763
   344
\indexouternonterm{interp}
ballarin@15763
   345
ballarin@15763
   346
\railalias{printinterps}{print\_interps}
ballarin@15763
   347
\railterm{printinterps}
ballarin@15763
   348
ballarin@15763
   349
\begin{rail}
ballarin@17043
   350
  'interpretation' (interp | name ('<' | subseteq) contextexp)
ballarin@15763
   351
  ;
ballarin@15763
   352
  'interpret' interp
ballarin@15763
   353
  ;
ballarin@17139
   354
  printinterps '!'? name
ballarin@15763
   355
  ;
ballarin@15763
   356
  interp: thmdecl? contextexpr ('[' (inst+) ']')?
ballarin@15763
   357
  ;
ballarin@15763
   358
\end{rail}
ballarin@15763
   359
ballarin@17043
   360
ballarin@15763
   361
\begin{descr}
ballarin@15763
   362
ballarin@15763
   363
\item [$\isarcmd{interpretation}~expr~insts$]
ballarin@17043
   364
ballarin@17043
   365
  The first form of $\isarcmd{interpretation}$ interprets $expr$
ballarin@17043
   366
  in the theory.  The instantiation is given as a list of
ballarin@17043
   367
  terms $insts$ and is positional.
ballarin@15763
   368
  All parameters must receive an instantiation term --- with the
ballarin@15763
   369
  exception of defined parameters.  These are, if omitted, derived
ballarin@15763
   370
  from the defining equation and other instantiations.  Use ``\_'' to
ballarin@15763
   371
  omit an instantiation term.  Free variables are automatically
ballarin@15763
   372
  generalized.
ballarin@15763
   373
ballarin@17043
   374
  The command generates proof obligations for the instantiated
ballarin@17043
   375
  specifications (assumes and defines elements).  Once these are
ballarin@17043
   376
  discharged by the user, instantiated facts are added to the theory in
ballarin@17043
   377
  a post-processing phase.
ballarin@15763
   378
ballarin@15763
   379
  The command is aware of interpretations already active in the
ballarin@15763
   380
  theory.  No proof obligations are generated for those, neither is
ballarin@15763
   381
  post-processing applied to their facts.  This avoids duplication of
ballarin@15763
   382
  interpreted facts, in particular.  Note that, in the case of a
ballarin@15763
   383
  locale with import, parts of the interpretation may already be
ballarin@15763
   384
  active.  The command will only generate proof obligations and add
ballarin@15763
   385
  facts for new parts.
ballarin@15763
   386
ballarin@17043
   387
  The context expression may be preceded by a name and/or attributes.
ballarin@17043
   388
  These take effect in the post-processing of facts.  The name is used
ballarin@17043
   389
  to prefix fact names, for example to avoid accidental hiding of
ballarin@17043
   390
  other facts.  Attributes are applied after attributes of the
ballarin@17043
   391
  interpreted facts.
ballarin@17043
   392
ballarin@15763
   393
  Adding facts to locales has the
ballarin@15763
   394
  effect of adding interpreted facts to the theory for all active
ballarin@17043
   395
  interpretations also.  That is, interpretations dynamically
ballarin@17043
   396
  participate in any facts added to locales.
ballarin@17043
   397
ballarin@17043
   398
\item [$\isarcmd{interpretation}~name~\subseteq~expr$]
ballarin@17043
   399
ballarin@17043
   400
  This form of the command interprets $expr$ in the locale $name$.  It
ballarin@17043
   401
  requires a proof that the specification of $name$ implies the
ballarin@17043
   402
  specification of $expr$.  As in the localized version of the theorem
ballarin@17043
   403
  command, the proof is in the context of $name$.  After the proof
ballarin@17043
   404
  obligation has been dischared, the facts of $expr$
ballarin@17043
   405
  become part of locale $name$ as \emph{derived} context elements and
ballarin@17043
   406
  are available when the context $name$ is subsequently entered.
ballarin@17043
   407
  Note that, like import, this is dynamic: facts added to a locale
ballarin@17139
   408
  part of $expr$ after interpretation become also available in
ballarin@17043
   409
  $name$.  Like facts
ballarin@17043
   410
  of renamed context elements, facts obtained by interpretation may be
ballarin@17043
   411
  accessed by prefixing with the parameter renaming (where the parameters
ballarin@17043
   412
  are separated by `\_').
ballarin@17043
   413
ballarin@17043
   414
  Unlike interpretation in theories, instantiation is confined to the
ballarin@17043
   415
  renaming of parameters, which may be specified as part of the context
ballarin@17043
   416
  expression $expr$.  Using defined parameters in $name$ one may
ballarin@17043
   417
  achieve an effect similar to instantiation, though.
ballarin@17043
   418
ballarin@17043
   419
  Only specification fragments of $expr$ that are not already part of
ballarin@17043
   420
  $name$ (be it imported, derived or a derived fragment of the import)
ballarin@17043
   421
  are considered by interpretation.  This enables circular
ballarin@17043
   422
  interpretations.
ballarin@17043
   423
ballarin@17139
   424
  If interpretations of $name$ exist in the current theory, the
ballarin@17139
   425
  command adds interpretations for $expr$ as well, with the same
ballarin@17139
   426
  prefix and attributes, although only for fragments of $expr$ that
ballarin@17139
   427
  are not interpreted in the theory already.
ballarin@17139
   428
ballarin@15763
   429
\item [$\isarcmd{interpret}~expr~insts$]
ballarin@15763
   430
  interprets $expr$ in the proof context and is otherwise similar to
ballarin@17043
   431
  interpretation in theories.  Free variables in instantiations are not
ballarin@15763
   432
  generalized, however.
ballarin@15763
   433
ballarin@15763
   434
\item [$\isarcmd{print_interps}~loc$]
ballarin@15763
   435
  prints the interpretations of a particular locale $loc$ that are
ballarin@17139
   436
  active in the current context, either theory or proof context.  The
ballarin@19145
   437
  exclamation point argument triggers printing of
ballarin@17139
   438
  \emph{witness} theorems justifying interpretations.  These are
ballarin@17139
   439
  normally omitted from the output.
ballarin@17139
   440
ballarin@15763
   441
  
ballarin@15763
   442
\end{descr}
ballarin@15763
   443
ballarin@15837
   444
\begin{warn}
ballarin@15837
   445
  Since attributes are applied to interpreted theorems, interpretation
ballarin@15837
   446
  may modify the current simpset and claset.  Take this into
ballarin@15837
   447
  account when choosing attributes for local theorems.
ballarin@15837
   448
\end{warn}
ballarin@15837
   449
ballarin@16168
   450
\begin{warn}
ballarin@17043
   451
  An interpretation in a theory may subsume previous interpretations.
ballarin@17043
   452
  This happens if the same specification fragment is interpreted twice
ballarin@17043
   453
  and the instantiation of the second interpretation is more general
ballarin@17043
   454
  than the interpretation of the first.  A warning
ballarin@16168
   455
  is issued, since it is likely that these could have been generalized
ballarin@16168
   456
  in the first place.  The locale package does not attempt to remove
ballarin@16168
   457
  subsumed interpretations.  This situation is normally harmless, but
ballarin@16168
   458
  note that $blast$ gets confused by the presence of multiple axclass
ballarin@17139
   459
  instances of a rule.
ballarin@16168
   460
\end{warn}
ballarin@16168
   461
ballarin@15763
   462
wenzelm@12621
   463
\section{Derived proof schemes}
wenzelm@12621
   464
wenzelm@12621
   465
\subsection{Generalized elimination}\label{sec:obtain}
wenzelm@12621
   466
wenzelm@17864
   467
\indexisarcmd{obtain}\indexisarcmd{guess}
wenzelm@12621
   468
\begin{matharray}{rcl}
wenzelm@12621
   469
  \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@17864
   470
  \isarcmd{guess}^* & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@12621
   471
\end{matharray}
wenzelm@12621
   472
wenzelm@12621
   473
Generalized elimination means that additional elements with certain properties
wenzelm@13041
   474
may be introduced in the current context, by virtue of a locally proven
wenzelm@12621
   475
``soundness statement''.  Technically speaking, the $\OBTAINNAME$ language
wenzelm@12621
   476
element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see
wenzelm@12621
   477
\S\ref{sec:proof-context}), together with a soundness proof of its additional
wenzelm@12621
   478
claim.  According to the nature of existential reasoning, assumptions get
wenzelm@12621
   479
eliminated from any result exported from the context later, provided that the
wenzelm@12621
   480
corresponding parameters do \emph{not} occur in the conclusion.
wenzelm@12621
   481
wenzelm@12621
   482
\begin{rail}
wenzelm@18903
   483
  'obtain' parname? (vars + 'and') 'where' (props + 'and')
wenzelm@12621
   484
  ;
wenzelm@17864
   485
  'guess' (vars + 'and')
wenzelm@17864
   486
  ;
wenzelm@12621
   487
\end{rail}
wenzelm@12618
   488
wenzelm@12621
   489
$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
wenzelm@12621
   490
shall refer to (optional) facts indicated for forward chaining.
wenzelm@12621
   491
\begin{matharray}{l}
wenzelm@12621
   492
  \langle facts~\vec b\rangle \\
wenzelm@12621
   493
  \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
wenzelm@13041
   494
  \quad \HAVE{}{\All{thesis} (\All{\vec x} \vec\phi \Imp thesis) \Imp thesis} \\
wenzelm@13041
   495
  \quad \PROOF{succeed} \\
wenzelm@12621
   496
  \qquad \FIX{thesis} \\
wenzelm@13041
   497
  \qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\
wenzelm@13042
   498
  \qquad \THUS{}{thesis} \\
wenzelm@13042
   499
  \quad\qquad \APPLY{-} \\
wenzelm@13041
   500
  \quad\qquad \USING{\vec b}~~\langle proof\rangle \\
wenzelm@13041
   501
  \quad \QED{} \\
wenzelm@12621
   502
  \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
wenzelm@12621
   503
\end{matharray}
wenzelm@12621
   504
wenzelm@12621
   505
Typically, the soundness proof is relatively straight-forward, often just by
wenzelm@13048
   506
canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''.
wenzelm@13048
   507
Accordingly, the ``$that$'' reduction above is declared as simplification and
wenzelm@13048
   508
introduction rule.
wenzelm@12621
   509
wenzelm@12621
   510
In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
wenzelm@12621
   511
meta-logical existential quantifiers and conjunctions.  This concept has a
wenzelm@13041
   512
broad range of useful applications, ranging from plain elimination (or
wenzelm@17864
   513
introduction) of object-level existential and conjunctions, to elimination
wenzelm@12621
   514
over results of symbolic evaluation of recursive definitions, for example.
wenzelm@12621
   515
Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
wenzelm@13041
   516
where the result is treated as a genuine assumption.
wenzelm@12621
   517
wenzelm@18903
   518
An alternative name to be used instead of ``$that$'' above may be
wenzelm@18903
   519
given in parentheses.
wenzelm@18903
   520
wenzelm@17864
   521
\medskip
wenzelm@17864
   522
wenzelm@17864
   523
The improper variant $\isarkeyword{guess}$ is similar to $\OBTAINNAME$, but
wenzelm@17864
   524
derives the obtained statement from the course of reasoning!  The proof starts
wenzelm@17864
   525
with a fixed goal $thesis$.  The subsequent proof may refine this to anything
wenzelm@17864
   526
of the form like $\All{\vec x} \vec\phi \Imp thesis$, but must not introduce
wenzelm@17864
   527
new subgoals.  The final goal state is then used as reduction rule for the
wenzelm@17864
   528
obtain scheme described above.  Obtained parameters $\vec x$ are marked as
wenzelm@17864
   529
internal by default, which prevents the proof context from being polluted by
wenzelm@17864
   530
ad-hoc variables.  The variable names and type constraints given as arguments
wenzelm@17864
   531
for $\isarkeyword{guess}$ specify a prefix of obtained parameters explicitly
wenzelm@17864
   532
in the text.
wenzelm@17864
   533
wenzelm@17864
   534
It is important to note that the facts introduced by $\OBTAINNAME$ and
wenzelm@17864
   535
$\isarkeyword{guess}$ may not be polymorphic: any type-variables occurring
wenzelm@17864
   536
here are fixed in the present context!
wenzelm@17864
   537
wenzelm@12621
   538
wenzelm@12621
   539
\subsection{Calculational reasoning}\label{sec:calculation}
wenzelm@7315
   540
wenzelm@8619
   541
\indexisarcmd{also}\indexisarcmd{finally}
wenzelm@8619
   542
\indexisarcmd{moreover}\indexisarcmd{ultimately}
wenzelm@12976
   543
\indexisarcmd{print-trans-rules}
wenzelm@12976
   544
\indexisaratt{trans}\indexisaratt{sym}\indexisaratt{symmetric}
wenzelm@7315
   545
\begin{matharray}{rcl}
wenzelm@7315
   546
  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7315
   547
  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@8619
   548
  \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@8619
   549
  \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@10154
   550
  \isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\
wenzelm@7315
   551
  trans & : & \isaratt \\
wenzelm@12976
   552
  sym & : & \isaratt \\
wenzelm@12976
   553
  symmetric & : & \isaratt \\
wenzelm@7315
   554
\end{matharray}
wenzelm@7315
   555
wenzelm@7315
   556
Calculational proof is forward reasoning with implicit application of
oheimb@11332
   557
transitivity rules (such those of $=$, $\leq$, $<$).  Isabelle/Isar maintains
wenzelm@7391
   558
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
wenzelm@7897
   559
results obtained by transitivity composed with the current result.  Command
wenzelm@7897
   560
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
wenzelm@7897
   561
final $calculation$ by forward chaining towards the next goal statement.  Both
wenzelm@7897
   562
commands require valid current facts, i.e.\ may occur only after commands that
wenzelm@7897
   563
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
wenzelm@8619
   564
$\HAVENAME$, $\SHOWNAME$ etc.  The $\MOREOVER$ and $\ULTIMATELY$ commands are
wenzelm@8619
   565
similar to $\ALSO$ and $\FINALLY$, but only collect further results in
wenzelm@8619
   566
$calculation$ without applying any rules yet.
wenzelm@7315
   567
wenzelm@13041
   568
Also note that the implicit term abbreviation ``$\dots$'' has its canonical
wenzelm@13041
   569
application with calculational proofs.  It refers to the argument of the
wenzelm@13041
   570
preceding statement. (The argument of a curried infix expression happens to be
wenzelm@13041
   571
its right-hand side.)
wenzelm@7315
   572
wenzelm@7315
   573
Isabelle/Isar calculations are implicitly subject to block structure in the
wenzelm@7315
   574
sense that new threads of calculational reasoning are commenced for any new
wenzelm@7315
   575
block (as opened by a local goal, for example).  This means that, apart from
wenzelm@7315
   576
being able to nest calculations, there is no separate \emph{begin-calculation}
wenzelm@7315
   577
command required.
wenzelm@7315
   578
wenzelm@8619
   579
\medskip
wenzelm@8619
   580
wenzelm@13041
   581
The Isar calculation proof commands may be defined as follows:\footnote{We
wenzelm@13041
   582
  suppress internal bookkeeping such as proper handling of block-structure.}
wenzelm@8619
   583
\begin{matharray}{rcl}
wenzelm@8619
   584
  \ALSO@0 & \equiv & \NOTE{calculation}{this} \\
wenzelm@9606
   585
  \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]
wenzelm@8619
   586
  \FINALLY & \equiv & \ALSO~\FROM{calculation} \\
wenzelm@8619
   587
  \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
wenzelm@8619
   588
  \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
wenzelm@8619
   589
\end{matharray}
wenzelm@8619
   590
wenzelm@7315
   591
\begin{rail}
wenzelm@13024
   592
  ('also' | 'finally') ('(' thmrefs ')')?
wenzelm@8619
   593
  ;
wenzelm@8507
   594
  'trans' (() | 'add' | 'del')
wenzelm@7315
   595
  ;
wenzelm@7315
   596
\end{rail}
wenzelm@7315
   597
wenzelm@7315
   598
\begin{descr}
wenzelm@13041
   599
wenzelm@8547
   600
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
wenzelm@7315
   601
  follows.  The first occurrence of $\ALSO$ in some calculational thread
wenzelm@7905
   602
  initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
wenzelm@7335
   603
  level of block-structure updates $calculation$ by some transitivity rule
wenzelm@7458
   604
  applied to $calculation$ and $this$ (in that order).  Transitivity rules are
wenzelm@11095
   605
  picked from the current context, unless alternative rules are given as
wenzelm@11095
   606
  explicit arguments.
wenzelm@9614
   607
wenzelm@8547
   608
\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
wenzelm@7315
   609
  $\ALSO$, and concludes the current calculational thread.  The final result
wenzelm@7315
   610
  is exhibited as fact for forward chaining towards the next goal. Basically,
wenzelm@7987
   611
  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that
wenzelm@7987
   612
  ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
wenzelm@7987
   613
  ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
wenzelm@7987
   614
  calculational proofs.
wenzelm@9614
   615
wenzelm@8619
   616
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
wenzelm@8619
   617
  but collect results only, without applying rules.
wenzelm@13041
   618
wenzelm@13024
   619
\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
wenzelm@13024
   620
  rules (for calculational commands $\ALSO$ and $\FINALLY$) and symmetry rules
wenzelm@13024
   621
  (for the $symmetric$ operation and single step elimination patters) of the
wenzelm@13024
   622
  current context.
wenzelm@13041
   623
wenzelm@8547
   624
\item [$trans$] declares theorems as transitivity rules.
wenzelm@13041
   625
wenzelm@13024
   626
\item [$sym$] declares symmetry rules.
wenzelm@13041
   627
wenzelm@12976
   628
\item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the
wenzelm@12976
   629
  current context.  For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a
wenzelm@12976
   630
  swapped fact derived from that assumption.
wenzelm@13041
   631
wenzelm@13024
   632
  In structured proof texts it is often more appropriate to use an explicit
wenzelm@13024
   633
  single-step elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y =
wenzelm@13041
   634
    x}~\DDOT$''.  The very same rules known to $symmetric$ are declared as
wenzelm@13041
   635
  $elim?$ as well.
wenzelm@13027
   636
wenzelm@7315
   637
\end{descr}
wenzelm@7315
   638
wenzelm@7315
   639
wenzelm@13041
   640
\section{Proof tools}
wenzelm@8517
   641
wenzelm@12618
   642
\subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att}
wenzelm@8517
   643
wenzelm@9606
   644
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
wenzelm@8517
   645
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
wenzelm@8517
   646
\indexisarmeth{fail}\indexisarmeth{succeed}
wenzelm@8517
   647
\begin{matharray}{rcl}
wenzelm@8517
   648
  unfold & : & \isarmeth \\
wenzelm@10741
   649
  fold & : & \isarmeth \\
wenzelm@10741
   650
  insert & : & \isarmeth \\[0.5ex]
wenzelm@8517
   651
  erule^* & : & \isarmeth \\
wenzelm@8517
   652
  drule^* & : & \isarmeth \\
wenzelm@13024
   653
  frule^* & : & \isarmeth \\
wenzelm@8517
   654
  succeed & : & \isarmeth \\
wenzelm@8517
   655
  fail & : & \isarmeth \\
wenzelm@8517
   656
\end{matharray}
wenzelm@7135
   657
wenzelm@7135
   658
\begin{rail}
wenzelm@10741
   659
  ('fold' | 'unfold' | 'insert') thmrefs
wenzelm@10741
   660
  ;
wenzelm@10741
   661
  ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
wenzelm@7135
   662
  ;
wenzelm@7135
   663
\end{rail}
wenzelm@7135
   664
wenzelm@7167
   665
\begin{descr}
wenzelm@13041
   666
wenzelm@13024
   667
\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the
wenzelm@13024
   668
  given meta-level definitions throughout all goals; any chained facts
wenzelm@13024
   669
  provided are inserted into the goal and subject to rewriting as well.
wenzelm@13041
   670
wenzelm@10741
   671
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
wenzelm@10741
   672
  state.  Note that current facts indicated for forward chaining are ignored.
wenzelm@13024
   673
wenzelm@8547
   674
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
wenzelm@8547
   675
  basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
wenzelm@8517
   676
  elim-resolution, destruct-resolution, and forward-resolution, respectively
wenzelm@10741
   677
  \cite{isabelle-ref}.  The optional natural number argument (default $0$)
wenzelm@13041
   678
  specifies additional assumption steps to be performed here.
wenzelm@13041
   679
wenzelm@10741
   680
  Note that these methods are improper ones, mainly serving for
wenzelm@10741
   681
  experimentation and tactic script emulation.  Different modes of basic rule
wenzelm@10741
   682
  application are usually expressed in Isar at the proof language level,
wenzelm@10741
   683
  rather than via implicit proof state manipulations.  For example, a proper
wenzelm@13041
   684
  single-step elimination would be done using the plain $rule$ method, with
wenzelm@10741
   685
  forward chaining of current facts.
wenzelm@13024
   686
wenzelm@8517
   687
\item [$succeed$] yields a single (unchanged) result; it is the identity of
wenzelm@8517
   688
  the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
wenzelm@13024
   689
wenzelm@8517
   690
\item [$fail$] yields an empty result sequence; it is the identity of the
wenzelm@8517
   691
  ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
wenzelm@13024
   692
wenzelm@7167
   693
\end{descr}
wenzelm@7135
   694
wenzelm@10318
   695
\indexisaratt{tagged}\indexisaratt{untagged}
wenzelm@9614
   696
\indexisaratt{THEN}\indexisaratt{COMP}
ballarin@14175
   697
\indexisaratt{unfolded}\indexisaratt{folded}
wenzelm@13027
   698
\indexisaratt{standard}\indexisarattof{Pure}{elim-format}
wenzelm@13024
   699
\indexisaratt{no-vars}
wenzelm@8517
   700
\begin{matharray}{rcl}
wenzelm@9905
   701
  tagged & : & \isaratt \\
wenzelm@9905
   702
  untagged & : & \isaratt \\[0.5ex]
wenzelm@9614
   703
  THEN & : & \isaratt \\
wenzelm@8517
   704
  COMP & : & \isaratt \\[0.5ex]
wenzelm@9905
   705
  unfolded & : & \isaratt \\
wenzelm@9905
   706
  folded & : & \isaratt \\[0.5ex]
wenzelm@9941
   707
  elim_format & : & \isaratt \\
wenzelm@13041
   708
  standard^* & : & \isaratt \\
wenzelm@9936
   709
  no_vars^* & : & \isaratt \\
wenzelm@8517
   710
\end{matharray}
wenzelm@8517
   711
wenzelm@8517
   712
\begin{rail}
wenzelm@9905
   713
  'tagged' (nameref+)
wenzelm@8517
   714
  ;
wenzelm@9905
   715
  'untagged' name
wenzelm@8517
   716
  ;
wenzelm@10154
   717
  ('THEN' | 'COMP') ('[' nat ']')? thmref
wenzelm@8517
   718
  ;
wenzelm@9905
   719
  ('unfolded' | 'folded') thmrefs
wenzelm@8517
   720
  ;
wenzelm@8517
   721
\end{rail}
wenzelm@8517
   722
wenzelm@8517
   723
\begin{descr}
wenzelm@13041
   724
wenzelm@9905
   725
\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
wenzelm@8517
   726
  theorem.  Tags may be any list of strings that serve as comment for some
wenzelm@8517
   727
  tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
wenzelm@8517
   728
  result).  The first string is considered the tag name, the rest its
wenzelm@8517
   729
  arguments.  Note that untag removes any tags of the same name.
wenzelm@13041
   730
wenzelm@13041
   731
\item [$THEN~a$ and $COMP~a$] compose rules by resolution.  $THEN$ resolves
wenzelm@13041
   732
  with the first premise of $a$ (an alternative position may be also
wenzelm@13041
   733
  specified); the $COMP$ version skips the automatic lifting process that is
wenzelm@13041
   734
  normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
wenzelm@8547
   735
  \cite[\S5]{isabelle-ref}).
wenzelm@13041
   736
wenzelm@9905
   737
\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
wenzelm@9905
   738
  given meta-level definitions throughout a rule.
wenzelm@13041
   739
wenzelm@13027
   740
\item [$elim_format$] turns a destruction rule into elimination rule format,
wenzelm@13027
   741
  by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
wenzelm@13027
   742
  B$.
wenzelm@13048
   743
  
wenzelm@13048
   744
  Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own
wenzelm@13048
   745
  version of this operation.
wenzelm@13041
   746
wenzelm@13041
   747
\item [$standard$] puts a theorem into the standard form of object-rules at
wenzelm@13041
   748
  the outermost theory level.  Note that this operation violates the local
wenzelm@13041
   749
  proof context (including active locales).
wenzelm@13041
   750
wenzelm@9232
   751
\item [$no_vars$] replaces schematic variables by free ones; this is mainly
wenzelm@9232
   752
  for tuning output of pretty printed theorems.
wenzelm@13027
   753
wenzelm@8517
   754
\end{descr}
wenzelm@7135
   755
wenzelm@7135
   756
wenzelm@12621
   757
\subsection{Further tactic emulations}\label{sec:tactics}
wenzelm@9606
   758
wenzelm@9606
   759
The following improper proof methods emulate traditional tactics.  These admit
wenzelm@9606
   760
direct access to the goal state, which is normally considered harmful!  In
wenzelm@9606
   761
particular, this may involve both numbered goal addressing (default 1), and
wenzelm@9606
   762
dynamic instantiation within the scope of some subgoal.
wenzelm@9606
   763
wenzelm@9606
   764
\begin{warn}
ballarin@14175
   765
  Dynamic instantiations refer to universally quantified parameters of
ballarin@14175
   766
  a subgoal (the dynamic context) rather than fixed variables and term
ballarin@14175
   767
  abbreviations of a (static) Isar context.
wenzelm@9606
   768
\end{warn}
wenzelm@9606
   769
ballarin@14175
   770
Tactic emulation methods, unlike their ML counterparts, admit
ballarin@14175
   771
simultaneous instantiation from both dynamic and static contexts.  If
ballarin@14175
   772
names occur in both contexts goal parameters hide locally fixed
ballarin@14175
   773
variables.  Likewise, schematic variables refer to term abbreviations,
ballarin@14175
   774
if present in the static context.  Otherwise the schematic variable is
ballarin@14175
   775
interpreted as a schematic variable and left to be solved by unification
ballarin@14175
   776
with certain parts of the subgoal.
ballarin@14175
   777
wenzelm@9606
   778
Note that the tactic emulation proof methods in Isabelle/Isar are consistently
ballarin@14175
   779
named $foo_tac$.  Note also that variable names occurring on left hand sides
ballarin@14212
   780
of instantiations must be preceded by a question mark if they coincide with
ballarin@14212
   781
a keyword or contain dots.
ballarin@14175
   782
This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}).
wenzelm@9606
   783
wenzelm@9606
   784
\indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
wenzelm@9606
   785
\indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
wenzelm@9606
   786
\indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
wenzelm@9642
   787
\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
wenzelm@9614
   788
\indexisarmeth{rotate-tac}\indexisarmeth{tactic}
wenzelm@9606
   789
\begin{matharray}{rcl}
wenzelm@9606
   790
  rule_tac^* & : & \isarmeth \\
wenzelm@9606
   791
  erule_tac^* & : & \isarmeth \\
wenzelm@9606
   792
  drule_tac^* & : & \isarmeth \\
wenzelm@9606
   793
  frule_tac^* & : & \isarmeth \\
wenzelm@9606
   794
  cut_tac^* & : & \isarmeth \\
wenzelm@9606
   795
  thin_tac^* & : & \isarmeth \\
wenzelm@9606
   796
  subgoal_tac^* & : & \isarmeth \\
wenzelm@9614
   797
  rename_tac^* & : & \isarmeth \\
wenzelm@9614
   798
  rotate_tac^* & : & \isarmeth \\
wenzelm@9606
   799
  tactic^* & : & \isarmeth \\
wenzelm@9606
   800
\end{matharray}
wenzelm@9606
   801
wenzelm@9606
   802
\railalias{ruletac}{rule\_tac}
wenzelm@9606
   803
\railterm{ruletac}
wenzelm@9606
   804
wenzelm@9606
   805
\railalias{eruletac}{erule\_tac}
wenzelm@9606
   806
\railterm{eruletac}
wenzelm@9606
   807
wenzelm@9606
   808
\railalias{druletac}{drule\_tac}
wenzelm@9606
   809
\railterm{druletac}
wenzelm@9606
   810
wenzelm@9606
   811
\railalias{fruletac}{frule\_tac}
wenzelm@9606
   812
\railterm{fruletac}
wenzelm@9606
   813
wenzelm@9606
   814
\railalias{cuttac}{cut\_tac}
wenzelm@9606
   815
\railterm{cuttac}
wenzelm@9606
   816
wenzelm@9606
   817
\railalias{thintac}{thin\_tac}
wenzelm@9606
   818
\railterm{thintac}
wenzelm@9606
   819
wenzelm@9606
   820
\railalias{subgoaltac}{subgoal\_tac}
wenzelm@9606
   821
\railterm{subgoaltac}
wenzelm@9606
   822
wenzelm@9614
   823
\railalias{renametac}{rename\_tac}
wenzelm@9614
   824
\railterm{renametac}
wenzelm@9614
   825
wenzelm@9614
   826
\railalias{rotatetac}{rotate\_tac}
wenzelm@9614
   827
\railterm{rotatetac}
wenzelm@9614
   828
wenzelm@9606
   829
\begin{rail}
wenzelm@9606
   830
  ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
wenzelm@9606
   831
  ( insts thmref | thmrefs )
wenzelm@9606
   832
  ;
wenzelm@9606
   833
  subgoaltac goalspec? (prop +)
wenzelm@9606
   834
  ;
wenzelm@9614
   835
  renametac goalspec? (name +)
wenzelm@9614
   836
  ;
wenzelm@9614
   837
  rotatetac goalspec? int?
wenzelm@9614
   838
  ;
wenzelm@9606
   839
  'tactic' text
wenzelm@9606
   840
  ;
wenzelm@9606
   841
wenzelm@9606
   842
  insts: ((name '=' term) + 'and') 'in'
wenzelm@9606
   843
  ;
wenzelm@9606
   844
\end{rail}
wenzelm@9606
   845
wenzelm@9606
   846
\begin{descr}
wenzelm@13041
   847
wenzelm@9606
   848
\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
wenzelm@9606
   849
  This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
wenzelm@9606
   850
  \cite[\S3]{isabelle-ref}).
wenzelm@13041
   851
wenzelm@13041
   852
  Multiple rules may be only given if there is no instantiation; then
wenzelm@9606
   853
  $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
wenzelm@9606
   854
  \cite[\S3]{isabelle-ref}).
wenzelm@13041
   855
wenzelm@9606
   856
\item [$cut_tac$] inserts facts into the proof state as assumption of a
wenzelm@9606
   857
  subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note
wenzelm@13027
   858
  that the scope of schematic variables is spread over the main goal
wenzelm@13027
   859
  statement.  Instantiations may be given as well, see also ML tactic
wenzelm@9606
   860
  \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
wenzelm@13041
   861
wenzelm@9606
   862
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
wenzelm@9606
   863
  that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in
wenzelm@9606
   864
  \cite[\S3]{isabelle-ref}.
wenzelm@13041
   865
wenzelm@9606
   866
\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See
wenzelm@9606
   867
  also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
wenzelm@9606
   868
  \cite[\S3]{isabelle-ref}.
wenzelm@13041
   869
wenzelm@9614
   870
\item [$rename_tac~\vec x$] renames parameters of a goal according to the list
wenzelm@9614
   871
  $\vec x$, which refers to the \emph{suffix} of variables.
wenzelm@13041
   872
wenzelm@9614
   873
\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
wenzelm@9614
   874
  from right to left if $n$ is positive, and from left to right if $n$ is
wenzelm@9614
   875
  negative; the default value is $1$.  See also \texttt{rotate_tac} in
wenzelm@9614
   876
  \cite[\S3]{isabelle-ref}.
wenzelm@13041
   877
wenzelm@9606
   878
\item [$tactic~text$] produces a proof method from any ML text of type
wenzelm@9606
   879
  \texttt{tactic}.  Apart from the usual ML environment and the current
wenzelm@9606
   880
  implicit theory context, the ML code may refer to the following locally
wenzelm@9606
   881
  bound values:
wenzelm@9606
   882
wenzelm@9606
   883
{\footnotesize\begin{verbatim}
wenzelm@9606
   884
val ctxt  : Proof.context
wenzelm@9606
   885
val facts : thm list
wenzelm@9606
   886
val thm   : string -> thm
wenzelm@9606
   887
val thms  : string -> thm list
wenzelm@9606
   888
\end{verbatim}}
wenzelm@9606
   889
  Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
wenzelm@9606
   890
  indicates any current facts for forward-chaining, and
wenzelm@9606
   891
  \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
wenzelm@9606
   892
  theorems) from the context.
wenzelm@9606
   893
\end{descr}
wenzelm@9606
   894
wenzelm@9606
   895
wenzelm@12621
   896
\subsection{The Simplifier}\label{sec:simplifier}
wenzelm@12621
   897
wenzelm@13048
   898
\subsubsection{Simplification methods}
wenzelm@12618
   899
wenzelm@8483
   900
\indexisarmeth{simp}\indexisarmeth{simp-all}
wenzelm@7315
   901
\begin{matharray}{rcl}
wenzelm@7315
   902
  simp & : & \isarmeth \\
wenzelm@8483
   903
  simp_all & : & \isarmeth \\
wenzelm@7315
   904
\end{matharray}
wenzelm@7315
   905
wenzelm@8483
   906
\railalias{simpall}{simp\_all}
wenzelm@8483
   907
\railterm{simpall}
wenzelm@8483
   908
wenzelm@8704
   909
\railalias{noasm}{no\_asm}
wenzelm@8704
   910
\railterm{noasm}
wenzelm@8704
   911
wenzelm@8704
   912
\railalias{noasmsimp}{no\_asm\_simp}
wenzelm@8704
   913
\railterm{noasmsimp}
wenzelm@8704
   914
wenzelm@8704
   915
\railalias{noasmuse}{no\_asm\_use}
wenzelm@8704
   916
\railterm{noasmuse}
wenzelm@8704
   917
berghofe@13617
   918
\railalias{asmlr}{asm\_lr}
berghofe@13617
   919
\railterm{asmlr}
berghofe@13617
   920
wenzelm@11128
   921
\indexouternonterm{simpmod}
wenzelm@7315
   922
\begin{rail}
wenzelm@13027
   923
  ('simp' | simpall) ('!' ?) opt? (simpmod *)
wenzelm@7315
   924
  ;
wenzelm@7315
   925
berghofe@13617
   926
  opt: '(' (noasm | noasmsimp | noasmuse | asmlr) ')'
wenzelm@8704
   927
  ;
wenzelm@9711
   928
  simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
wenzelm@9847
   929
    'split' (() | 'add' | 'del')) ':' thmrefs
wenzelm@7315
   930
  ;
wenzelm@7315
   931
\end{rail}
wenzelm@7315
   932
wenzelm@7321
   933
\begin{descr}
wenzelm@13015
   934
wenzelm@8547
   935
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
wenzelm@8594
   936
  according to the arguments given.  Note that the \railtterm{only} modifier
wenzelm@8547
   937
  first removes all other rewrite rules, congruences, and looper tactics
wenzelm@8594
   938
  (including splits), and then behaves like \railtterm{add}.
wenzelm@13041
   939
wenzelm@9711
   940
  \medskip The \railtterm{cong} modifiers add or delete Simplifier congruence
wenzelm@9711
   941
  rules (see also \cite{isabelle-ref}), the default is to add.
wenzelm@13041
   942
wenzelm@9711
   943
  \medskip The \railtterm{split} modifiers add or delete rules for the
wenzelm@9711
   944
  Splitter (see also \cite{isabelle-ref}), the default is to add.  This works
wenzelm@9711
   945
  only if the Simplifier method has been properly setup to include the
wenzelm@9711
   946
  Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
wenzelm@13041
   947
wenzelm@13015
   948
\item [$simp_all$] is similar to $simp$, but acts on all goals (backwards from
wenzelm@13015
   949
  the last to the first one).
wenzelm@13015
   950
wenzelm@7321
   951
\end{descr}
wenzelm@7321
   952
wenzelm@13015
   953
By default the Simplifier methods take local assumptions fully into account,
wenzelm@13015
   954
using equational assumptions in the subsequent normalization process, or
wenzelm@13024
   955
simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in
wenzelm@13015
   956
\cite[\S10]{isabelle-ref}).  In structured proofs this is usually quite well
wenzelm@13015
   957
behaved in practice: just the local premises of the actual goal are involved,
wenzelm@13041
   958
additional facts may be inserted via explicit forward-chaining (using $\THEN$,
wenzelm@13015
   959
$\FROMNAME$ etc.).  The full context of assumptions is only included if the
wenzelm@13015
   960
``$!$'' (bang) argument is given, which should be used with some care, though.
wenzelm@7321
   961
wenzelm@13015
   962
Additional Simplifier options may be specified to tune the behavior further
wenzelm@13041
   963
(mostly for unstructured scripts with many accidental local facts):
wenzelm@13041
   964
``$(no_asm)$'' means assumptions are ignored completely (cf.\
wenzelm@13041
   965
\texttt{simp_tac}), ``$(no_asm_simp)$'' means assumptions are used in the
wenzelm@13041
   966
simplification of the conclusion but are not themselves simplified (cf.\
wenzelm@13041
   967
\texttt{asm_simp_tac}), and ``$(no_asm_use)$'' means assumptions are
wenzelm@13041
   968
simplified but are not used in the simplification of each other or the
wenzelm@13041
   969
conclusion (cf.\ \texttt{full_simp_tac}).
berghofe@13617
   970
For compatibility reasons, there is also an option ``$(asm_lr)$'',
berghofe@13617
   971
which means that an assumption is only used for simplifying assumptions
berghofe@13617
   972
which are to the right of it (cf.\ \texttt{asm_lr_simp_tac}).
wenzelm@8704
   973
wenzelm@8704
   974
\medskip
wenzelm@8704
   975
wenzelm@8704
   976
The Splitter package is usually configured to work as part of the Simplifier.
wenzelm@9711
   977
The effect of repeatedly applying \texttt{split_tac} can be simulated by
wenzelm@13041
   978
``$(simp~only\colon~split\colon~\vec a)$''.  There is also a separate $split$
wenzelm@13041
   979
method available for single-step case splitting.
wenzelm@8483
   980
wenzelm@8483
   981
wenzelm@12621
   982
\subsubsection{Declaring rules}
wenzelm@8483
   983
wenzelm@8667
   984
\indexisarcmd{print-simpset}
wenzelm@8638
   985
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
wenzelm@7321
   986
\begin{matharray}{rcl}
wenzelm@13024
   987
  \isarcmd{print_simpset}^* & : & \isarkeep{theory~|~proof} \\
wenzelm@7321
   988
  simp & : & \isaratt \\
wenzelm@9711
   989
  cong & : & \isaratt \\
wenzelm@8483
   990
  split & : & \isaratt \\
wenzelm@7321
   991
\end{matharray}
wenzelm@7321
   992
wenzelm@7321
   993
\begin{rail}
wenzelm@9711
   994
  ('simp' | 'cong' | 'split') (() | 'add' | 'del')
wenzelm@7321
   995
  ;
wenzelm@7321
   996
\end{rail}
wenzelm@7321
   997
wenzelm@7321
   998
\begin{descr}
wenzelm@13024
   999
wenzelm@13024
  1000
\item [$\isarcmd{print_simpset}$] prints the collection of rules declared to
wenzelm@13024
  1001
  the Simplifier, which is also known as ``simpset'' internally
wenzelm@8667
  1002
  \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
wenzelm@13024
  1003
wenzelm@8547
  1004
\item [$simp$] declares simplification rules.
wenzelm@13024
  1005
wenzelm@8638
  1006
\item [$cong$] declares congruence rules.
wenzelm@13024
  1007
wenzelm@9711
  1008
\item [$split$] declares case split rules.
wenzelm@13024
  1009
wenzelm@7321
  1010
\end{descr}
wenzelm@7319
  1011
wenzelm@7315
  1012
wenzelm@12621
  1013
\subsubsection{Forward simplification}
wenzelm@12621
  1014
wenzelm@9905
  1015
\indexisaratt{simplified}
wenzelm@7315
  1016
\begin{matharray}{rcl}
wenzelm@9905
  1017
  simplified & : & \isaratt \\
wenzelm@7315
  1018
\end{matharray}
wenzelm@7315
  1019
wenzelm@9905
  1020
\begin{rail}
wenzelm@13015
  1021
  'simplified' opt? thmrefs?
wenzelm@9905
  1022
  ;
wenzelm@9905
  1023
wenzelm@9905
  1024
  opt: '(' (noasm | noasmsimp | noasmuse) ')'
wenzelm@9905
  1025
  ;
wenzelm@9905
  1026
\end{rail}
wenzelm@7905
  1027
wenzelm@9905
  1028
\begin{descr}
wenzelm@13048
  1029
  
wenzelm@13015
  1030
\item [$simplified~\vec a$] causes a theorem to be simplified, either by
wenzelm@13015
  1031
  exactly the specified rules $\vec a$, or the implicit Simplifier context if
wenzelm@13015
  1032
  no arguments are given.  The result is fully simplified by default,
wenzelm@13015
  1033
  including assumptions and conclusion; the options $no_asm$ etc.\ tune the
wenzelm@13048
  1034
  Simplifier in the same way as the for the $simp$ method.
wenzelm@13041
  1035
wenzelm@13015
  1036
  Note that forward simplification restricts the simplifier to its most basic
wenzelm@13015
  1037
  operation of term rewriting; solver and looper tactics \cite{isabelle-ref}
wenzelm@13015
  1038
  are \emph{not} involved here.  The $simplified$ attribute should be only
wenzelm@13015
  1039
  rarely required under normal circumstances.
wenzelm@13015
  1040
wenzelm@9905
  1041
\end{descr}
wenzelm@7315
  1042
wenzelm@7315
  1043
wenzelm@13048
  1044
\subsubsection{Low-level equational reasoning}
wenzelm@9614
  1045
wenzelm@12976
  1046
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}
wenzelm@9614
  1047
\begin{matharray}{rcl}
wenzelm@13015
  1048
  subst^* & : & \isarmeth \\
wenzelm@9614
  1049
  hypsubst^* & : & \isarmeth \\
wenzelm@13015
  1050
  split^* & : & \isarmeth \\
wenzelm@9614
  1051
\end{matharray}
wenzelm@9614
  1052
wenzelm@9614
  1053
\begin{rail}
nipkow@15995
  1054
  'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
wenzelm@9614
  1055
  ;
wenzelm@9799
  1056
  'split' ('(' 'asm' ')')? thmrefs
wenzelm@9703
  1057
  ;
wenzelm@9614
  1058
\end{rail}
wenzelm@9614
  1059
wenzelm@13015
  1060
These methods provide low-level facilities for equational reasoning that are
wenzelm@13015
  1061
intended for specialized applications only.  Normally, single step
wenzelm@13015
  1062
calculations would be performed in a structured text (see also
wenzelm@13015
  1063
\S\ref{sec:calculation}), while the Simplifier methods provide the canonical
wenzelm@13015
  1064
way for automated normalization (see \S\ref{sec:simplifier}).
wenzelm@9614
  1065
wenzelm@9614
  1066
\begin{descr}
wenzelm@13041
  1067
nipkow@15995
  1068
\item [$subst~eq$] performs a single substitution step using rule $eq$, which
wenzelm@13041
  1069
  may be either a meta or object equality.
wenzelm@13041
  1070
nipkow@15995
  1071
\item [$subst~(asm)~eq$] substitutes in an assumption.
nipkow@15995
  1072
nipkow@15995
  1073
\item [$subst~(i \dots j)~eq$] performs several substitutions in the
nipkow@15995
  1074
conclusion. The numbers $i$ to $j$ indicate the positions to substitute at.
nipkow@15995
  1075
Positions are ordered from the top of the term tree moving down from left to
nipkow@15995
  1076
right. For example, in $(a+b)+(c+d)$ there are three positions where
nipkow@15995
  1077
commutativity of $+$ is applicable: 1 refers to the whole term, 2 to $a+b$
nipkow@15995
  1078
and 3 to $c+d$. If the positions in the list $(i \dots j)$ are
nipkow@15995
  1079
non-overlapping (e.g. $(2~3)$ in $(a+b)+(c+d)$) you may assume all
nipkow@15995
  1080
substitutions are performed simultaneously. Otherwise the behaviour of
nipkow@15995
  1081
$subst$ is not specified.
nipkow@15995
  1082
nipkow@15995
  1083
\item [$subst~(asm)~(i \dots j)~eq$] performs the substitutions in the
nipkow@16010
  1084
assumptions. Positions $1 \dots i@1$ refer
nipkow@16010
  1085
to assumption 1, positions $i@1+1 \dots i@2$ to assumption 2, and so on.
nipkow@15995
  1086
wenzelm@13041
  1087
\item [$hypsubst$] performs substitution using some assumption; this only
wenzelm@13041
  1088
  works for equations of the form $x = t$ where $x$ is a free or bound
wenzelm@13041
  1089
  variable.
wenzelm@13041
  1090
wenzelm@13041
  1091
\item [$split~\vec a$] performs single-step case splitting using rules $thms$.
wenzelm@9799
  1092
  By default, splitting is performed in the conclusion of a goal; the $asm$
wenzelm@9799
  1093
  option indicates to operate on assumptions instead.
wenzelm@13048
  1094
  
wenzelm@9703
  1095
  Note that the $simp$ method already involves repeated application of split
wenzelm@13048
  1096
  rules as declared in the current context.
wenzelm@9614
  1097
\end{descr}
wenzelm@9614
  1098
wenzelm@9614
  1099
wenzelm@12621
  1100
\subsection{The Classical Reasoner}\label{sec:classical}
wenzelm@7135
  1101
wenzelm@13048
  1102
\subsubsection{Basic methods}
wenzelm@7321
  1103
wenzelm@13024
  1104
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
wenzelm@13024
  1105
\indexisarmeth{intro}\indexisarmeth{elim}
wenzelm@7321
  1106
\begin{matharray}{rcl}
wenzelm@7321
  1107
  rule & : & \isarmeth \\
wenzelm@13024
  1108
  contradiction & : & \isarmeth \\
wenzelm@7321
  1109
  intro & : & \isarmeth \\
wenzelm@7321
  1110
  elim & : & \isarmeth \\
wenzelm@7321
  1111
\end{matharray}
wenzelm@7321
  1112
wenzelm@7321
  1113
\begin{rail}
wenzelm@8547
  1114
  ('rule' | 'intro' | 'elim') thmrefs?
wenzelm@7321
  1115
  ;
wenzelm@7321
  1116
\end{rail}
wenzelm@7321
  1117
wenzelm@7321
  1118
\begin{descr}
wenzelm@13041
  1119
wenzelm@7466
  1120
\item [$rule$] as offered by the classical reasoner is a refinement over the
wenzelm@13024
  1121
  primitive one (see \S\ref{sec:pure-meth-att}).  Both versions essentially
wenzelm@13024
  1122
  work the same, but the classical version observes the classical rule context
wenzelm@13041
  1123
  in addition to that of Isabelle/Pure.
wenzelm@13041
  1124
wenzelm@13041
  1125
  Common object logics (HOL, ZF, etc.) declare a rich collection of classical
wenzelm@13041
  1126
  rules (even if these would qualify as intuitionistic ones), but only few
wenzelm@13041
  1127
  declarations to the rule context of Isabelle/Pure
wenzelm@13041
  1128
  (\S\ref{sec:pure-meth-att}).
wenzelm@13041
  1129
wenzelm@13024
  1130
\item [$contradiction$] solves some goal by contradiction, deriving any result
wenzelm@13041
  1131
  from both $\neg A$ and $A$.  Chained facts, which are guaranteed to
wenzelm@13041
  1132
  participate, may appear in either order.
wenzelm@9614
  1133
wenzelm@7466
  1134
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
wenzelm@13041
  1135
  elim-resolution, after having inserted any chained facts.  Exactly the rules
wenzelm@13041
  1136
  given as arguments are taken into account; this allows fine-tuned
wenzelm@13041
  1137
  decomposition of a proof problem, in contrast to common automated tools.
wenzelm@13041
  1138
wenzelm@7321
  1139
\end{descr}
wenzelm@7321
  1140
wenzelm@7321
  1141
wenzelm@13048
  1142
\subsubsection{Automated methods}
wenzelm@7315
  1143
wenzelm@9799
  1144
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
wenzelm@9799
  1145
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
wenzelm@7321
  1146
\begin{matharray}{rcl}
wenzelm@9780
  1147
  blast & : & \isarmeth \\
wenzelm@9780
  1148
  fast & : & \isarmeth \\
wenzelm@9799
  1149
  slow & : & \isarmeth \\
wenzelm@9780
  1150
  best & : & \isarmeth \\
wenzelm@9780
  1151
  safe & : & \isarmeth \\
wenzelm@9780
  1152
  clarify & : & \isarmeth \\
wenzelm@7321
  1153
\end{matharray}
wenzelm@7321
  1154
wenzelm@11128
  1155
\indexouternonterm{clamod}
wenzelm@7321
  1156
\begin{rail}
wenzelm@13027
  1157
  'blast' ('!' ?) nat? (clamod *)
wenzelm@7321
  1158
  ;
wenzelm@13027
  1159
  ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
wenzelm@7321
  1160
  ;
wenzelm@7321
  1161
wenzelm@9408
  1162
  clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
wenzelm@7321
  1163
  ;
wenzelm@7321
  1164
\end{rail}
wenzelm@7321
  1165
wenzelm@7321
  1166
\begin{descr}
wenzelm@7321
  1167
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
wenzelm@7335
  1168
  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
wenzelm@10858
  1169
  user-supplied search bound (default 20).
wenzelm@9799
  1170
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
wenzelm@9799
  1171
  classical reasoner.  See \texttt{fast_tac}, \texttt{slow_tac},
wenzelm@9799
  1172
  \texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
wenzelm@9799
  1173
  \cite[\S11]{isabelle-ref} for more information.
wenzelm@7321
  1174
\end{descr}
wenzelm@7321
  1175
wenzelm@13041
  1176
Any of the above methods support additional modifiers of the context of
wenzelm@13041
  1177
classical rules.  Their semantics is analogous to the attributes given before.
wenzelm@13041
  1178
Facts provided by forward chaining are inserted into the goal before
wenzelm@13041
  1179
commencing proof search.  The ``!''~argument causes the full context of
wenzelm@13041
  1180
assumptions to be included as well.
wenzelm@7321
  1181
wenzelm@7315
  1182
wenzelm@12621
  1183
\subsubsection{Combined automated methods}\label{sec:clasimp}
wenzelm@7315
  1184
wenzelm@9799
  1185
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
wenzelm@9799
  1186
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
wenzelm@7321
  1187
\begin{matharray}{rcl}
wenzelm@9606
  1188
  auto & : & \isarmeth \\
wenzelm@7321
  1189
  force & : & \isarmeth \\
wenzelm@9438
  1190
  clarsimp & : & \isarmeth \\
wenzelm@9606
  1191
  fastsimp & : & \isarmeth \\
wenzelm@9799
  1192
  slowsimp & : & \isarmeth \\
wenzelm@9799
  1193
  bestsimp & : & \isarmeth \\
wenzelm@7321
  1194
\end{matharray}
wenzelm@7321
  1195
wenzelm@11128
  1196
\indexouternonterm{clasimpmod}
wenzelm@7321
  1197
\begin{rail}
wenzelm@13027
  1198
  'auto' '!'? (nat nat)? (clasimpmod *)
wenzelm@9780
  1199
  ;
wenzelm@13027
  1200
  ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
wenzelm@7321
  1201
  ;
wenzelm@7315
  1202
wenzelm@9711
  1203
  clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
wenzelm@10031
  1204
    ('cong' | 'split') (() | 'add' | 'del') |
wenzelm@10031
  1205
    'iff' (((() | 'add') '?'?) | 'del') |
wenzelm@9408
  1206
    (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
wenzelm@7321
  1207
\end{rail}
wenzelm@7315
  1208
wenzelm@7321
  1209
\begin{descr}
wenzelm@9799
  1210
\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$]
wenzelm@9799
  1211
  provide access to Isabelle's combined simplification and classical reasoning
wenzelm@9799
  1212
  tactics.  These correspond to \texttt{auto_tac}, \texttt{force_tac},
wenzelm@9799
  1213
  \texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
wenzelm@9799
  1214
  added as wrapper, see \cite[\S11]{isabelle-ref} for more information.  The
wenzelm@13048
  1215
  modifier arguments correspond to those given in \S\ref{sec:simplifier} and
wenzelm@13048
  1216
  \S\ref{sec:classical}.  Just note that the ones related to the Simplifier
wenzelm@13048
  1217
  are prefixed by \railtterm{simp} here.
wenzelm@9614
  1218
wenzelm@7987
  1219
  Facts provided by forward chaining are inserted into the goal before doing
wenzelm@7987
  1220
  the search.  The ``!''~argument causes the full context of assumptions to be
wenzelm@7987
  1221
  included as well.
wenzelm@7321
  1222
\end{descr}
wenzelm@7321
  1223
wenzelm@7987
  1224
wenzelm@13048
  1225
\subsubsection{Declaring rules}
wenzelm@7135
  1226
wenzelm@8667
  1227
\indexisarcmd{print-claset}
wenzelm@7391
  1228
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
wenzelm@9936
  1229
\indexisaratt{iff}\indexisaratt{rule}
wenzelm@7321
  1230
\begin{matharray}{rcl}
wenzelm@13024
  1231
  \isarcmd{print_claset}^* & : & \isarkeep{theory~|~proof} \\
wenzelm@7321
  1232
  intro & : & \isaratt \\
wenzelm@7321
  1233
  elim & : & \isaratt \\
wenzelm@7321
  1234
  dest & : & \isaratt \\
wenzelm@9936
  1235
  rule & : & \isaratt \\
wenzelm@7391
  1236
  iff & : & \isaratt \\
wenzelm@7321
  1237
\end{matharray}
wenzelm@7135
  1238
wenzelm@7321
  1239
\begin{rail}
wenzelm@18854
  1240
  ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
wenzelm@7321
  1241
  ;
wenzelm@9936
  1242
  'rule' 'del'
wenzelm@9936
  1243
  ;
wenzelm@10031
  1244
  'iff' (((() | 'add') '?'?) | 'del')
wenzelm@9936
  1245
  ;
wenzelm@7321
  1246
\end{rail}
wenzelm@7135
  1247
wenzelm@7321
  1248
\begin{descr}
wenzelm@13024
  1249
wenzelm@13024
  1250
\item [$\isarcmd{print_claset}$] prints the collection of rules declared to
wenzelm@13024
  1251
  the Classical Reasoner, which is also known as ``simpset'' internally
wenzelm@8667
  1252
  \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
wenzelm@18854
  1253
  
wenzelm@8517
  1254
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
oheimb@11332
  1255
  destruction rules, respectively.  By default, rules are considered as
wenzelm@9408
  1256
  \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
wenzelm@13041
  1257
  single ``!'' classifies as \emph{safe}.  Rule declarations marked by ``?''
wenzelm@18854
  1258
  coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\ 
wenzelm@18854
  1259
  are only applied in single steps of the $rule$ method).  The optional
wenzelm@18854
  1260
  natural number specifies an explicit weight argument, which is ignored by
wenzelm@18854
  1261
  automated tools, but determines the search order of single rule steps.
wenzelm@13024
  1262
oheimb@11332
  1263
\item [$rule~del$] deletes introduction, elimination, or destruction rules from
wenzelm@9936
  1264
  the context.
wenzelm@13041
  1265
wenzelm@13041
  1266
\item [$iff$] declares logical equivalences to the Simplifier and the
wenzelm@13024
  1267
  Classical reasoner at the same time.  Non-conditional rules result in a
wenzelm@13024
  1268
  ``safe'' introduction and elimination pair; conditional ones are considered
wenzelm@13024
  1269
  ``unsafe''.  Rules with negative conclusion are automatically inverted
wenzelm@13041
  1270
  (using $\neg$ elimination internally).
wenzelm@13041
  1271
wenzelm@13041
  1272
  The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only,
wenzelm@13041
  1273
  and omits the Simplifier declaration.
wenzelm@13041
  1274
wenzelm@7321
  1275
\end{descr}
wenzelm@7135
  1276
wenzelm@8203
  1277
wenzelm@13048
  1278
\subsubsection{Classical operations}
wenzelm@13027
  1279
wenzelm@18530
  1280
\indexisaratt{swapped}
wenzelm@13027
  1281
wenzelm@13027
  1282
\begin{matharray}{rcl}
wenzelm@13027
  1283
  swapped & : & \isaratt \\
wenzelm@13027
  1284
\end{matharray}
wenzelm@13027
  1285
wenzelm@13027
  1286
\begin{descr}
wenzelm@13041
  1287
wenzelm@13027
  1288
\item [$swapped$] turns an introduction rule into an elimination, by resolving
wenzelm@13027
  1289
  with the classical swap principle $(\neg B \Imp A) \Imp (\neg A \Imp B)$.
wenzelm@13027
  1290
wenzelm@13027
  1291
\end{descr}
wenzelm@13027
  1292
wenzelm@13027
  1293
wenzelm@12621
  1294
\subsection{Proof by cases and induction}\label{sec:cases-induct}
wenzelm@12618
  1295
wenzelm@13048
  1296
\subsubsection{Rule contexts}
wenzelm@12618
  1297
wenzelm@12618
  1298
\indexisarcmd{case}\indexisarcmd{print-cases}
wenzelm@18232
  1299
\indexisaratt{case-names}\indexisaratt{case-conclusion}
wenzelm@18232
  1300
\indexisaratt{params}\indexisaratt{consumes}
wenzelm@12618
  1301
\begin{matharray}{rcl}
wenzelm@12618
  1302
  \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@12618
  1303
  \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
wenzelm@12618
  1304
  case_names & : & \isaratt \\
wenzelm@18232
  1305
  case_conclusion & : & \isaratt \\
wenzelm@12618
  1306
  params & : & \isaratt \\
wenzelm@12618
  1307
  consumes & : & \isaratt \\
wenzelm@12618
  1308
\end{matharray}
wenzelm@12618
  1309
wenzelm@18232
  1310
The puristic way to build up Isar proof contexts is by explicit language
wenzelm@18232
  1311
elements like $\FIXNAME$, $\ASSUMENAME$, $\LET$ (see
wenzelm@18232
  1312
\S\ref{sec:proof-context}).  This is adequate for plain natural deduction, but
wenzelm@18232
  1313
easily becomes unwieldy in concrete verification tasks, which typically
wenzelm@18232
  1314
involve big induction rules with several cases.
wenzelm@18232
  1315
wenzelm@18232
  1316
The $\CASENAME$ command provides a shorthand to refer to a local context
wenzelm@18232
  1317
symbolically: certain proof methods provide an environment of named ``cases''
wenzelm@18232
  1318
of the form $c\colon \vec x, \vec \phi$; the effect of ``$\CASE{c}$'' is then
wenzelm@18232
  1319
equivalent to ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''.  Term bindings may be
wenzelm@18232
  1320
covered as well, notably $\Var{case}$ for the main conclusion.
wenzelm@18232
  1321
wenzelm@18232
  1322
By default, the ``terminology'' $\vec x$ of a case value is marked as hidden,
wenzelm@18232
  1323
i.e.\ there is no way to refer to such parameters in the subsequent proof
wenzelm@18232
  1324
text.  After all, original rule parameters stem from somewhere outside of the
wenzelm@18232
  1325
current proof text.  By using the explicit form ``$\CASE{(c~\vec y)}$''
wenzelm@18232
  1326
instead, the proof author is able to chose local names that fit nicely into
wenzelm@18232
  1327
the current context.
wenzelm@12618
  1328
wenzelm@12618
  1329
\medskip
wenzelm@12618
  1330
wenzelm@18232
  1331
It is important to note that proper use of $\CASENAME$ does not provide means
wenzelm@18232
  1332
to peek at the current goal state, which is not directly observable in Isar!
wenzelm@18232
  1333
Nonetheless, goal refinement commands do provide named cases $goal@i$ for each
wenzelm@18232
  1334
subgoal $i = 1, \dots, n$ of the resulting goal state.  Using this feature
wenzelm@18232
  1335
requires great care, because some bits of the internal tactical machinery
wenzelm@18232
  1336
intrude the proof text.  In particular, parameter names stemming from the
wenzelm@18232
  1337
left-over of automated reasoning tools are usually quite unpredictable.
wenzelm@12618
  1338
wenzelm@18232
  1339
Under normal circumstances, the text of cases emerge from standard elimination
wenzelm@18232
  1340
or induction rules, which in turn are derived from previous theory
wenzelm@13041
  1341
specifications in a canonical way (say from $\isarkeyword{inductive}$
wenzelm@13041
  1342
definitions).
wenzelm@13027
  1343
wenzelm@18232
  1344
\medskip Proper cases are only available if both the proof method and the
wenzelm@18232
  1345
rules involved support this.  By using appropriate attributes, case names,
wenzelm@18232
  1346
conclusions, and parameters may be also declared by hand.  Thus variant
wenzelm@18232
  1347
versions of rules that have been derived manually become reasy to use in
wenzelm@18232
  1348
advanced case analysis later.
wenzelm@12618
  1349
wenzelm@12618
  1350
\begin{rail}
wenzelm@13041
  1351
  'case' (caseref | '(' caseref ((name | underscore) +) ')')
wenzelm@12618
  1352
  ;
wenzelm@13024
  1353
  caseref: nameref attributes?
wenzelm@13024
  1354
  ;
wenzelm@13024
  1355
wenzelm@18232
  1356
  'case\_names' (name +)
wenzelm@18232
  1357
  ;
wenzelm@18232
  1358
  'case\_conclusion' name (name *)
wenzelm@12618
  1359
  ;
wenzelm@13027
  1360
  'params' ((name *) + 'and')
wenzelm@12618
  1361
  ;
wenzelm@12618
  1362
  'consumes' nat?
wenzelm@12618
  1363
  ;
wenzelm@12618
  1364
\end{rail}
wenzelm@12618
  1365
wenzelm@12618
  1366
\begin{descr}
wenzelm@18232
  1367
  
wenzelm@13041
  1368
\item [$\CASE{(c~\vec x)}$] invokes a named local context $c\colon \vec x,
wenzelm@13041
  1369
  \vec \phi$, as provided by an appropriate proof method (such as $cases$ and
wenzelm@18232
  1370
  $induct$).  The command ``$\CASE{(c~\vec x)}$'' abbreviates ``$\FIX{\vec
wenzelm@18232
  1371
    x}~\ASSUME{c}{\vec\phi}$''.
wenzelm@13041
  1372
wenzelm@12618
  1373
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
wenzelm@12618
  1374
  state, using Isar proof language notation.  This is a diagnostic command;
wenzelm@12618
  1375
  $undo$ does not apply.
wenzelm@18232
  1376
  
wenzelm@12618
  1377
\item [$case_names~\vec c$] declares names for the local contexts of premises
wenzelm@18232
  1378
  of a theorem; $\vec c$ refers to the \emph{suffix} of the list of premises.
wenzelm@18232
  1379
  
wenzelm@18232
  1380
\item [$case_conclusion~c~\vec d$] declares names for the conclusions of a
wenzelm@18232
  1381
  named premise $c$; here $\vec d$ refers to the prefix of arguments of a
wenzelm@18232
  1382
  logical formula built by nesting a binary connective (e.g.\ $\lor$).
wenzelm@18232
  1383
  
wenzelm@18232
  1384
  Note that proof methods such as $induct$ and $coinduct$ already provide a
wenzelm@18232
  1385
  default name for the conclusion as a whole.  The need to name subformulas
wenzelm@18232
  1386
  only arises with cases that split into several sub-cases, as in common
wenzelm@18232
  1387
  co-induction rules.
wenzelm@13041
  1388
wenzelm@12618
  1389
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
wenzelm@12618
  1390
  premises $1, \dots, n$ of some theorem.  An empty list of names may be given
wenzelm@12618
  1391
  to skip positions, leaving the present parameters unchanged.
wenzelm@18232
  1392
  
wenzelm@12618
  1393
  Note that the default usage of case rules does \emph{not} directly expose
wenzelm@18232
  1394
  parameters to the proof context.
wenzelm@18232
  1395
  
wenzelm@12618
  1396
\item [$consumes~n$] declares the number of ``major premises'' of a rule,
wenzelm@12618
  1397
  i.e.\ the number of facts to be consumed when it is applied by an
wenzelm@18232
  1398
  appropriate proof method.  The default value of $consumes$ is $n = 1$, which
wenzelm@18232
  1399
  is appropriate for the usual kind of cases and induction rules for inductive
wenzelm@18232
  1400
  sets (cf.\ \S\ref{sec:hol-inductive}).  Rules without any $consumes$
wenzelm@18232
  1401
  declaration given are treated as if $consumes~0$ had been specified.
wenzelm@18232
  1402
  
wenzelm@12618
  1403
  Note that explicit $consumes$ declarations are only rarely needed; this is
wenzelm@18232
  1404
  already taken care of automatically by the higher-level $cases$, $induct$,
wenzelm@18232
  1405
  and $coinduct$ declarations.
wenzelm@13027
  1406
wenzelm@12618
  1407
\end{descr}
wenzelm@12618
  1408
wenzelm@12618
  1409
wenzelm@18232
  1410
\subsubsection{Proof methods}
wenzelm@11691
  1411
wenzelm@18232
  1412
\indexisarmeth{cases}\indexisarmeth{induct}\indexisarmeth{coinduct}
wenzelm@11691
  1413
\begin{matharray}{rcl}
wenzelm@11691
  1414
  cases & : & \isarmeth \\
wenzelm@11691
  1415
  induct & : & \isarmeth \\
wenzelm@18232
  1416
  coinduct & : & \isarmeth \\
wenzelm@11691
  1417
\end{matharray}
wenzelm@11691
  1418
wenzelm@18232
  1419
The $cases$, $induct$, and $coinduct$ methods provide a uniform interface to
wenzelm@18232
  1420
common proof techniques over datatypes, inductive sets, recursive functions
wenzelm@18232
  1421
etc.  The corresponding rules may be specified and instantiated in a casual
wenzelm@18232
  1422
manner.  Furthermore, these methods provide named local contexts that may be
wenzelm@18232
  1423
invoked via the $\CASENAME$ proof command within the subsequent proof text.
wenzelm@18232
  1424
This accommodates compact proof texts even when reasoning about large
wenzelm@13048
  1425
specifications.
wenzelm@11691
  1426
wenzelm@18232
  1427
The $induct$ method also provides some additional infrastructure in order to
wenzelm@18232
  1428
be applicable to structure statements (either using explicit meta-level
wenzelm@18232
  1429
connectives, or including facts and parameters separately).  This avoids
wenzelm@18232
  1430
cumbersome encoding of ``strengthened'' inductive statements within the
wenzelm@18232
  1431
object-logic.
wenzelm@18232
  1432
wenzelm@11691
  1433
\begin{rail}
wenzelm@18232
  1434
  'cases' open? (insts * 'and') rule?
wenzelm@11691
  1435
  ;
wenzelm@18232
  1436
  'induct' open? (definsts * 'and') \\ fixing? taking? rule?
wenzelm@18232
  1437
  ;
wenzelm@18232
  1438
  'coinduct' open? insts taking rule?
wenzelm@11691
  1439
  ;
wenzelm@11691
  1440
wenzelm@11691
  1441
  open: '(' 'open' ')'
wenzelm@11691
  1442
  ;
wenzelm@18505
  1443
  rule: ('type' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
wenzelm@18232
  1444
  ;
wenzelm@18232
  1445
  definst: name ('==' | equiv) term | inst
wenzelm@11691
  1446
  ;
wenzelm@18232
  1447
  definsts: ( definst *)
wenzelm@18232
  1448
  ;
wenzelm@18232
  1449
  fixing: 'fixing' ':' ((term *) 'and' +)
wenzelm@18232
  1450
  ;
wenzelm@18232
  1451
  taking: 'taking' ':' insts
wenzelm@11691
  1452
  ;
wenzelm@11691
  1453
\end{rail}
wenzelm@11691
  1454
wenzelm@11691
  1455
\begin{descr}
wenzelm@13041
  1456
wenzelm@13041
  1457
\item [$cases~insts~R$] applies method $rule$ with an appropriate case
wenzelm@11691
  1458
  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
wenzelm@11691
  1459
  names are bound according to the rule's local contexts.
wenzelm@13041
  1460
wenzelm@11691
  1461
  The rule is determined as follows, according to the facts and arguments
wenzelm@11691
  1462
  passed to the $cases$ method:
wenzelm@11691
  1463
  \begin{matharray}{llll}
wenzelm@11691
  1464
    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
wenzelm@11691
  1465
                    & cases &           & \Text{classical case split} \\
wenzelm@11691
  1466
                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
wenzelm@11691
  1467
    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
wenzelm@11691
  1468
    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
wenzelm@11691
  1469
  \end{matharray}
wenzelm@13041
  1470
wenzelm@11691
  1471
  Several instantiations may be given, referring to the \emph{suffix} of
wenzelm@11691
  1472
  premises of the case rule; within each premise, the \emph{prefix} of
wenzelm@11691
  1473
  variables is instantiated.  In most situations, only a single term needs to
wenzelm@11691
  1474
  be specified; this refers to the first variable of the last premise (it is
wenzelm@11691
  1475
  usually the same for all cases).
wenzelm@13041
  1476
wenzelm@13041
  1477
  The ``$(open)$'' option causes the parameters of the new local contexts to
wenzelm@13041
  1478
  be exposed to the current proof context.  Thus local variables stemming from
wenzelm@11691
  1479
  distant parts of the theory development may be introduced in an implicit
wenzelm@11691
  1480
  manner, which can be quite confusing to the reader.  Furthermore, this
wenzelm@11691
  1481
  option may cause unwanted hiding of existing local variables, resulting in
wenzelm@11691
  1482
  less robust proof texts.
wenzelm@13041
  1483
wenzelm@13041
  1484
\item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
wenzelm@11691
  1485
  induction rules, which are determined as follows:
wenzelm@11691
  1486
  \begin{matharray}{llll}
wenzelm@11691
  1487
    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
wenzelm@11691
  1488
                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
wenzelm@11691
  1489
    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
wenzelm@11691
  1490
    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
wenzelm@11691
  1491
  \end{matharray}
wenzelm@18505
  1492
  
wenzelm@18505
  1493
  Several instantiations may be given, each referring to some part of
wenzelm@18505
  1494
  a mutual inductive definition or datatype --- only related partial
wenzelm@18505
  1495
  induction rules may be used together, though.  Any of the lists of
wenzelm@18505
  1496
  terms $P, x, \dots$ refers to the \emph{suffix} of variables present
wenzelm@18505
  1497
  in the induction rule.  This enables the writer to specify only
wenzelm@18505
  1498
  induction variables, or both predicates and variables, for example.
wenzelm@18232
  1499
  
wenzelm@18232
  1500
  Instantiations may be definitional: equations $x \equiv t$ introduce local
wenzelm@18232
  1501
  definitions, which are inserted into the claim and discharged after applying
wenzelm@18232
  1502
  the induction rule.  Equalities reappear in the inductive cases, but have
wenzelm@18232
  1503
  been transformed according to the induction principle being involved here.
wenzelm@18232
  1504
  In order to achieve practically useful induction hypotheses, some variables
wenzelm@18232
  1505
  occurring in $t$ need to be fixed (see below).
wenzelm@18232
  1506
  
wenzelm@18232
  1507
  The optional ``$fixing\colon \vec x$'' specification generalizes variables
wenzelm@18232
  1508
  $\vec x$ of the original goal before applying induction.  Thus induction
wenzelm@18232
  1509
  hypotheses may become sufficiently general to get the proof through.
wenzelm@18232
  1510
  Together with definitional instantiations, one may effectively perform
wenzelm@18232
  1511
  induction over expressions of a certain structure.
wenzelm@18232
  1512
  
wenzelm@18232
  1513
  The optional ``$taking\colon \vec t$'' specification provides additional
wenzelm@18232
  1514
  instantiations of a prefix of pending variables in the rule.  Such schematic
wenzelm@18232
  1515
  induction rules rarely occur in practice, though.
wenzelm@18232
  1516
wenzelm@18232
  1517
  The ``$(open)$'' option works the same way as for $cases$.
wenzelm@18232
  1518
wenzelm@18232
  1519
\item [$coinduct~inst~R$] is analogous to the $induct$ method, but refers to
wenzelm@18232
  1520
  coinduction rules, which are determined as follows:
wenzelm@18232
  1521
  \begin{matharray}{llll}
wenzelm@18232
  1522
    \Text{goal}     &          & \Text{arguments} & \Text{rule} \\\hline
wenzelm@18232
  1523
                    & coinduct & x ~ \dots        & \Text{type coinduction (type of $x$)} \\
wenzelm@18232
  1524
    x \in A         & coinduct & \dots            & \Text{set coinduction (of $A$)} \\
wenzelm@18232
  1525
    \dots           & coinduct & \dots ~ R        & \Text{explicit rule $R$} \\
wenzelm@18232
  1526
  \end{matharray}
wenzelm@18232
  1527
  
wenzelm@18232
  1528
  Coinduction is the dual of induction.  Induction essentially eliminates $x
wenzelm@18232
  1529
  \in A$ towards a generic result $P ~ x$, while coinduction introduces $x \in
wenzelm@18232
  1530
  A$ starting with $x \in B$, for a suitable ``bisimulation'' $B$.  The cases
wenzelm@18232
  1531
  of a coinduct rule are typically named after the sets being covered, while
wenzelm@18232
  1532
  the conclusions consist of several alternatives being named after the
wenzelm@18232
  1533
  individual destructor patterns.
wenzelm@18232
  1534
  
wenzelm@18232
  1535
  The given instantiation refers to the \emph{prefix} of variables occurring
wenzelm@18232
  1536
  in the rule's conclusion.  An additional ``$taking: \vec t$'' specification
wenzelm@18232
  1537
  may be required in order to specify the bisimulation to be used in the
wenzelm@18232
  1538
  coinduction step.
wenzelm@13041
  1539
wenzelm@13041
  1540
  The ``$(open)$'' option works the same way as for $cases$.
wenzelm@13027
  1541
wenzelm@11691
  1542
\end{descr}
wenzelm@11691
  1543
wenzelm@13048
  1544
Above methods produce named local contexts, as determined by the instantiated
wenzelm@18232
  1545
rule as given in the text.  Beyond that, the $induct$ and $coinduct$ methods
wenzelm@18232
  1546
guess further instantiations from the goal specification itself.  Any
wenzelm@18232
  1547
persisting unresolved schematic variables of the resulting rule will render
wenzelm@18232
  1548
the the corresponding case invalid.  The term binding
wenzelm@18232
  1549
$\Var{case}$\indexisarvar{case} for the conclusion will be provided with each
wenzelm@18232
  1550
case, provided that term is fully specified.
wenzelm@11691
  1551
wenzelm@13048
  1552
The $\isarkeyword{print_cases}$ command prints all named cases present in the
wenzelm@13048
  1553
current proof state.
wenzelm@11691
  1554
wenzelm@11691
  1555
\medskip
wenzelm@11691
  1556
wenzelm@18232
  1557
Despite the additional infrastructure, both $cases$ and $coinduct$ merely
wenzelm@18232
  1558
apply a certain rule, after instantiation, while conforming due to the usual
wenzelm@18232
  1559
way of monotonic natural deduction: the context of a structured statement
wenzelm@18232
  1560
$\All{\vec x} \vec\phi \Imp \dots$ reappears unchanged after the case split.
wenzelm@11691
  1561
wenzelm@18232
  1562
The $induct$ method is significantly different in this respect: the meta-level
wenzelm@18232
  1563
structure is passed through the ``recursive'' course involved in the
wenzelm@18232
  1564
induction.  Thus the original statement is basically replaced by separate
wenzelm@18232
  1565
copies, corresponding to the induction hypotheses and conclusion; the original
wenzelm@18232
  1566
goal context is no longer available.  Thus local assumptions, fixed parameters
wenzelm@18232
  1567
and definitions effectively participate in the inductive rephrasing of the
wenzelm@18232
  1568
original statement.
wenzelm@11691
  1569
wenzelm@13425
  1570
In induction proofs, local assumptions introduced by cases are split into two
wenzelm@13425
  1571
different kinds: $hyps$ stemming from the rule and $prems$ from the goal
wenzelm@13425
  1572
statement.  This is reflected in the extracted cases accordingly, so invoking
wenzelm@13425
  1573
``$\isarcmd{case}~c$'' will provide separate facts $c\mathord.hyps$ and
wenzelm@13425
  1574
$c\mathord.prems$, as well as fact $c$ to hold the all-inclusive list.
wenzelm@13425
  1575
wenzelm@11691
  1576
\medskip
wenzelm@11691
  1577
wenzelm@11691
  1578
Facts presented to either method are consumed according to the number of
wenzelm@18232
  1579
``major premises'' of the rule involved, which is usually $0$ for plain cases
wenzelm@18232
  1580
and induction rules of datatypes etc.\ and $1$ for rules of inductive sets and
wenzelm@18232
  1581
the like.  The remaining facts are inserted into the goal verbatim before the
wenzelm@18232
  1582
actual $cases$, $induct$, or $coinduct$ rule is applied.
wenzelm@11691
  1583
wenzelm@11691
  1584
wenzelm@18232
  1585
\subsubsection{Declaring rules}
wenzelm@11691
  1586
wenzelm@18232
  1587
\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}\indexisaratt{coinduct}
wenzelm@11691
  1588
\begin{matharray}{rcl}
wenzelm@11691
  1589
  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
wenzelm@11691
  1590
  cases & : & \isaratt \\
wenzelm@11691
  1591
  induct & : & \isaratt \\
wenzelm@18232
  1592
  coinduct & : & \isaratt \\
wenzelm@11691
  1593
\end{matharray}
wenzelm@11691
  1594
wenzelm@11691
  1595
\begin{rail}
wenzelm@11691
  1596
  'cases' spec
wenzelm@11691
  1597
  ;
wenzelm@11691
  1598
  'induct' spec
wenzelm@11691
  1599
  ;
wenzelm@18232
  1600
  'coinduct' spec
wenzelm@18232
  1601
  ;
wenzelm@11691
  1602
wenzelm@11691
  1603
  spec: ('type' | 'set') ':' nameref
wenzelm@11691
  1604
  ;
wenzelm@11691
  1605
\end{rail}
wenzelm@11691
  1606
wenzelm@13024
  1607
\begin{descr}
wenzelm@13041
  1608
wenzelm@13024
  1609
\item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for
wenzelm@13024
  1610
  sets and types of the current context.
wenzelm@13048
  1611
  
wenzelm@18232
  1612
\item [$cases$, $induct$, and $coinduct$] (as attributes) augment the
wenzelm@18232
  1613
  corresponding context of rules for reasoning about (co)inductive sets and
wenzelm@18232
  1614
  types, using the corresponding methods of the same name.  Certain
wenzelm@18232
  1615
  definitional packages of object-logics usually declare emerging cases and
wenzelm@18232
  1616
  induction rules as expected, so users rarely need to intervene.
wenzelm@18232
  1617
  
wenzelm@18232
  1618
  Manual rule declarations usually refer to the $case_names$ and $params$
wenzelm@18232
  1619
  attributes to adjust names of cases and parameters of a rule; the $consumes$
wenzelm@18232
  1620
  declaration is taken care of automatically: $consumes~0$ is specified for
wenzelm@18232
  1621
  ``type'' rules and $consumes~1$ for ``set'' rules.
wenzelm@13041
  1622
wenzelm@13024
  1623
\end{descr}
wenzelm@11691
  1624
wenzelm@9614
  1625
%%% Local Variables:
wenzelm@7135
  1626
%%% mode: latex
wenzelm@7135
  1627
%%% TeX-master: "isar-ref"
wenzelm@9614
  1628
%%% End: