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