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