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