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