src/Doc/Isar_Ref/Proof.thy
author wenzelm
Sun Dec 03 13:22:09 2017 +0100 (17 months ago)
changeset 67119 acb0807ddb56
parent 64926 75ee8475c37e
child 69597 ff784d5a5bfb
permissions -rw-r--r--
discontinued old 'def' command;
wenzelm@61656
     1
(*:maxLineLen=78:*)
wenzelm@61656
     2
wenzelm@26869
     3
theory Proof
wenzelm@63531
     4
  imports Main Base
wenzelm@26869
     5
begin
wenzelm@26869
     6
wenzelm@58618
     7
chapter \<open>Proofs \label{ch:proofs}\<close>
wenzelm@26869
     8
wenzelm@58618
     9
text \<open>
wenzelm@61657
    10
  Proof commands perform transitions of Isar/VM machine configurations, which
wenzelm@61657
    11
  are block-structured, consisting of a stack of nodes with three main
wenzelm@61657
    12
  components: logical proof context, current facts, and open goals. Isar/VM
wenzelm@61657
    13
  transitions are typed according to the following three different modes of
wenzelm@61657
    14
  operation:
wenzelm@26870
    15
wenzelm@61657
    16
    \<^descr> \<open>proof(prove)\<close> means that a new goal has just been stated that is now to
wenzelm@61657
    17
    be \<^emph>\<open>proven\<close>; the next command may refine it by some proof method, and
wenzelm@61657
    18
    enter a sub-proof to establish the actual result.
wenzelm@64926
    19
wenzelm@61657
    20
    \<^descr> \<open>proof(state)\<close> is like a nested theory mode: the context may be
wenzelm@61657
    21
    augmented by \<^emph>\<open>stating\<close> additional assumptions, intermediate results etc.
wenzelm@64926
    22
wenzelm@61657
    23
    \<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and
wenzelm@61657
    24
    \<open>proof(prove)\<close>: existing facts (i.e.\ the contents of the special
wenzelm@61657
    25
    @{fact_ref this} register) have been just picked up in order to be used
wenzelm@61657
    26
    when refining the goal claimed next.
wenzelm@26870
    27
wenzelm@61657
    28
  The proof mode indicator may be understood as an instruction to the writer,
wenzelm@61657
    29
  telling what kind of operation may be performed next. The corresponding
wenzelm@61657
    30
  typings of proof commands restricts the shape of well-formed proof texts to
wenzelm@61657
    31
  particular command sequences. So dynamic arrangements of commands eventually
wenzelm@61657
    32
  turn out as static texts of a certain structure.
wenzelm@29741
    33
wenzelm@61657
    34
  \Appref{ap:refcard} gives a simplified grammar of the (extensible) language
wenzelm@61657
    35
  emerging that way from the different types of proof commands. The main ideas
wenzelm@61657
    36
  of the overall Isar framework are explained in \chref{ch:isar-framework}.
wenzelm@58618
    37
\<close>
wenzelm@26870
    38
wenzelm@26870
    39
wenzelm@58618
    40
section \<open>Proof structure\<close>
wenzelm@28755
    41
wenzelm@58618
    42
subsection \<open>Formal notepad\<close>
wenzelm@36356
    43
wenzelm@58618
    44
text \<open>
wenzelm@36356
    45
  \begin{matharray}{rcl}
wenzelm@61493
    46
    @{command_def "notepad"} & : & \<open>local_theory \<rightarrow> proof(state)\<close> \\
wenzelm@36356
    47
  \end{matharray}
wenzelm@36356
    48
wenzelm@55112
    49
  @{rail \<open>
wenzelm@42596
    50
    @@{command notepad} @'begin'
wenzelm@40965
    51
    ;
wenzelm@42596
    52
    @@{command end}
wenzelm@55112
    53
  \<close>}
wenzelm@40965
    54
wenzelm@61657
    55
  \<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without any
wenzelm@61657
    56
  goal statement. This allows to experiment with Isar, without producing any
wenzelm@61657
    57
  persistent result. The notepad is closed by @{command "end"}.
wenzelm@58618
    58
\<close>
wenzelm@36356
    59
wenzelm@36356
    60
wenzelm@58618
    61
subsection \<open>Blocks\<close>
wenzelm@28755
    62
wenzelm@58618
    63
text \<open>
wenzelm@28755
    64
  \begin{matharray}{rcl}
wenzelm@61493
    65
    @{command_def "next"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
    66
    @{command_def "{"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
    67
    @{command_def "}"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@28755
    68
  \end{matharray}
wenzelm@28755
    69
wenzelm@61657
    70
  While Isar is inherently block-structured, opening and closing blocks is
wenzelm@61657
    71
  mostly handled rather casually, with little explicit user-intervention. Any
wenzelm@61657
    72
  local goal statement automatically opens \<^emph>\<open>two\<close> internal blocks, which are
wenzelm@61657
    73
  closed again when concluding the sub-proof (by @{command "qed"} etc.).
wenzelm@61657
    74
  Sections of different context within a sub-proof may be switched via
wenzelm@61657
    75
  @{command "next"}, which is just a single block-close followed by block-open
wenzelm@61657
    76
  again. The effect of @{command "next"} is to reset the local proof context;
wenzelm@28755
    77
  there is no goal focus involved here!
wenzelm@28755
    78
wenzelm@28755
    79
  For slightly more advanced applications, there are explicit block
wenzelm@61657
    80
  parentheses as well. These typically achieve a stronger forward style of
wenzelm@61657
    81
  reasoning.
wenzelm@28755
    82
wenzelm@61657
    83
  \<^descr> @{command "next"} switches to a fresh block within a sub-proof, resetting
wenzelm@61657
    84
  the local context to the initial one.
wenzelm@28755
    85
wenzelm@61657
    86
  \<^descr> @{command "{"} and @{command "}"} explicitly open and close blocks. Any
wenzelm@61657
    87
  current facts pass through ``@{command "{"}'' unchanged, while ``@{command
wenzelm@61657
    88
  "}"}'' causes any result to be \<^emph>\<open>exported\<close> into the enclosing context. Thus
wenzelm@61657
    89
  fixed variables are generalized, assumptions discharged, and local
wenzelm@61657
    90
  definitions unfolded (cf.\ \secref{sec:proof-context}). There is no
wenzelm@61657
    91
  difference of @{command "assume"} and @{command "presume"} in this mode of
wenzelm@61657
    92
  forward reasoning --- in contrast to plain backward reasoning with the
wenzelm@61657
    93
  result exported at @{command "show"} time.
wenzelm@58618
    94
\<close>
wenzelm@28755
    95
wenzelm@28755
    96
wenzelm@58618
    97
subsection \<open>Omitting proofs\<close>
wenzelm@28755
    98
wenzelm@58618
    99
text \<open>
wenzelm@28755
   100
  \begin{matharray}{rcl}
wenzelm@61493
   101
    @{command_def "oops"} & : & \<open>proof \<rightarrow> local_theory | theory\<close> \\
wenzelm@28755
   102
  \end{matharray}
wenzelm@28755
   103
wenzelm@61657
   104
  The @{command "oops"} command discontinues the current proof attempt, while
wenzelm@61657
   105
  considering the partial proof text as properly processed. This is
wenzelm@61657
   106
  conceptually quite different from ``faking'' actual proofs via @{command_ref
wenzelm@61657
   107
  "sorry"} (see \secref{sec:proof-steps}): @{command "oops"} does not observe
wenzelm@61657
   108
  the proof structure at all, but goes back right to the theory level.
wenzelm@61657
   109
  Furthermore, @{command "oops"} does not produce any result theorem --- there
wenzelm@61657
   110
  is no intended claim to be able to complete the proof in any way.
wenzelm@28755
   111
wenzelm@28755
   112
  A typical application of @{command "oops"} is to explain Isar proofs
wenzelm@61657
   113
  \<^emph>\<open>within\<close> the system itself, in conjunction with the document preparation
wenzelm@61657
   114
  tools of Isabelle described in \chref{ch:document-prep}. Thus partial or
wenzelm@61657
   115
  even wrong proof attempts can be discussed in a logically sound manner. Note
wenzelm@61657
   116
  that the Isabelle {\LaTeX} macros can be easily adapted to print something
wenzelm@61657
   117
  like ``\<open>\<dots>\<close>'' instead of the keyword ``@{command "oops"}''.
wenzelm@58618
   118
\<close>
wenzelm@28755
   119
wenzelm@28755
   120
wenzelm@58618
   121
section \<open>Statements\<close>
wenzelm@28754
   122
wenzelm@58618
   123
subsection \<open>Context elements \label{sec:proof-context}\<close>
wenzelm@26870
   124
wenzelm@58618
   125
text \<open>
wenzelm@26870
   126
  \begin{matharray}{rcl}
wenzelm@61493
   127
    @{command_def "fix"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
   128
    @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
   129
    @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@63039
   130
    @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@26870
   131
  \end{matharray}
wenzelm@26870
   132
wenzelm@61657
   133
  The logical proof context consists of fixed variables and assumptions. The
wenzelm@61657
   134
  former closely correspond to Skolem constants, or meta-level universal
wenzelm@61657
   135
  quantification as provided by the Isabelle/Pure logical framework.
wenzelm@61657
   136
  Introducing some \<^emph>\<open>arbitrary, but fixed\<close> variable via ``@{command
wenzelm@61657
   137
  "fix"}~\<open>x\<close>'' results in a local value that may be used in the subsequent
wenzelm@61657
   138
  proof as any other variable or constant. Furthermore, any result \<open>\<turnstile> \<phi>[x]\<close>
wenzelm@61657
   139
  exported from the context will be universally closed wrt.\ \<open>x\<close> at the
wenzelm@61657
   140
  outermost level: \<open>\<turnstile> \<And>x. \<phi>[x]\<close> (this is expressed in normal form using
wenzelm@61657
   141
  Isabelle's meta-variables).
wenzelm@26870
   142
wenzelm@61657
   143
  Similarly, introducing some assumption \<open>\<chi>\<close> has two effects. On the one hand,
wenzelm@61657
   144
  a local theorem is created that may be used as a fact in subsequent proof
wenzelm@61657
   145
  steps. On the other hand, any result \<open>\<chi> \<turnstile> \<phi>\<close> exported from the context
wenzelm@61657
   146
  becomes conditional wrt.\ the assumption: \<open>\<turnstile> \<chi> \<Longrightarrow> \<phi>\<close>. Thus, solving an
wenzelm@61657
   147
  enclosing goal using such a result would basically introduce a new subgoal
wenzelm@61657
   148
  stemming from the assumption. How this situation is handled depends on the
wenzelm@61657
   149
  version of assumption command used: while @{command "assume"} insists on
wenzelm@61657
   150
  solving the subgoal by unification with some premise of the goal, @{command
wenzelm@61657
   151
  "presume"} leaves the subgoal unchanged in order to be proved later by the
wenzelm@61657
   152
  user.
wenzelm@26870
   153
wenzelm@63039
   154
  Local definitions, introduced by ``\<^theory_text>\<open>define x where x = t\<close>'', are achieved
wenzelm@61657
   155
  by combining ``@{command "fix"}~\<open>x\<close>'' with another version of assumption
wenzelm@61657
   156
  that causes any hypothetical equation \<open>x \<equiv> t\<close> to be eliminated by the
wenzelm@61657
   157
  reflexivity rule. Thus, exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>
wenzelm@61493
   158
  \<phi>[t]\<close>.
wenzelm@26870
   159
wenzelm@55112
   160
  @{rail \<open>
wenzelm@63285
   161
    @@{command fix} @{syntax vars}
wenzelm@26870
   162
    ;
wenzelm@61658
   163
    (@@{command assume} | @@{command presume}) concl prems @{syntax for_fixes}
wenzelm@61658
   164
    ;
wenzelm@61658
   165
    concl: (@{syntax props} + @'and')
wenzelm@61658
   166
    ;
wenzelm@61658
   167
    prems: (@'if' (@{syntax props'} + @'and'))?
wenzelm@26870
   168
    ;
wenzelm@63285
   169
    @@{command define} @{syntax vars} @'where'
wenzelm@63285
   170
      (@{syntax props} + @'and') @{syntax for_fixes}
wenzelm@55112
   171
  \<close>}
wenzelm@26870
   172
wenzelm@61657
   173
  \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary,
wenzelm@61657
   174
  but fixed\<close>.
wenzelm@60483
   175
wenzelm@61657
   176
  \<^descr> @{command "assume"}~\<open>a: \<phi>\<close> and @{command "presume"}~\<open>a: \<phi>\<close> introduce a
wenzelm@61657
   177
  local fact \<open>\<phi> \<turnstile> \<phi>\<close> by assumption. Subsequent results applied to an enclosing
wenzelm@61657
   178
  goal (e.g.\ by @{command_ref "show"}) are handled as follows: @{command
wenzelm@61657
   179
  "assume"} expects to be able to unify with existing premises in the goal,
wenzelm@61657
   180
  while @{command "presume"} leaves \<open>\<phi>\<close> as new subgoals.
wenzelm@60483
   181
wenzelm@61657
   182
  Several lists of assumptions may be given (separated by @{keyword_ref
wenzelm@61657
   183
  "and"}; the resulting list of current facts consists of all of these
wenzelm@61657
   184
  concatenated.
wenzelm@60483
   185
wenzelm@63529
   186
  A structured assumption like \<^theory_text>\<open>assume "B x" if "A x" for x\<close> is equivalent to
wenzelm@63529
   187
  \<^theory_text>\<open>assume "\<And>x. A x \<Longrightarrow> B x"\<close>, but vacuous quantification is avoided: a
wenzelm@61658
   188
  for-context only effects propositions according to actual use of variables.
wenzelm@61658
   189
wenzelm@63039
   190
  \<^descr> \<^theory_text>\<open>define x where "x = t"\<close> introduces a local (non-polymorphic) definition.
wenzelm@63039
   191
  In results that are exported from the context, \<open>x\<close> is replaced by \<open>t\<close>.
wenzelm@63039
   192
wenzelm@63039
   193
  Internally, equational assumptions are added to the context in Pure form,
wenzelm@63039
   194
  using \<open>x \<equiv> t\<close> instead of \<open>x = t\<close> or \<open>x \<longleftrightarrow> t\<close> from the object-logic. When
wenzelm@63039
   195
  exporting results from the context, \<open>x\<close> is generalized and the assumption
wenzelm@63039
   196
  discharged by reflexivity, causing the replacement by \<open>t\<close>.
wenzelm@60483
   197
wenzelm@63039
   198
  The default name for the definitional fact is \<open>x_def\<close>. Several simultaneous
wenzelm@63039
   199
  definitions may be given as well, with a collective default name.
wenzelm@63039
   200
wenzelm@63039
   201
  \<^medskip>
wenzelm@63039
   202
  It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f
wenzelm@63039
   203
  :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>.
wenzelm@58618
   204
\<close>
wenzelm@26870
   205
wenzelm@26870
   206
wenzelm@58618
   207
subsection \<open>Term abbreviations \label{sec:term-abbrev}\<close>
wenzelm@28754
   208
wenzelm@58618
   209
text \<open>
wenzelm@28754
   210
  \begin{matharray}{rcl}
wenzelm@61493
   211
    @{command_def "let"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@28754
   212
    @{keyword_def "is"} & : & syntax \\
wenzelm@28754
   213
  \end{matharray}
wenzelm@28754
   214
wenzelm@61657
   215
  Abbreviations may be either bound by explicit @{command "let"}~\<open>p \<equiv> t\<close>
wenzelm@61657
   216
  statements, or by annotating assumptions or goal statements with a list of
wenzelm@62280
   217
  patterns ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>''. In both cases, higher-order matching is
wenzelm@61657
   218
  invoked to bind extra-logical term variables, which may be either named
wenzelm@61657
   219
  schematic variables of the form \<open>?x\<close>, or nameless dummies ``@{variable _}''
wenzelm@61657
   220
  (underscore). Note that in the @{command "let"} form the patterns occur on
wenzelm@61657
   221
  the left-hand side, while the @{keyword "is"} patterns are in postfix
wenzelm@61657
   222
  position.
wenzelm@28754
   223
wenzelm@61657
   224
  Polymorphism of term bindings is handled in Hindley-Milner style, similar to
wenzelm@61657
   225
  ML. Type variables referring to local assumptions or open goal statements
wenzelm@61657
   226
  are \<^emph>\<open>fixed\<close>, while those of finished results or bound by @{command "let"}
wenzelm@61657
   227
  may occur in \<^emph>\<open>arbitrary\<close> instances later. Even though actual polymorphism
wenzelm@61657
   228
  should be rarely used in practice, this mechanism is essential to achieve
wenzelm@61657
   229
  proper incremental type-inference, as the user proceeds to build up the Isar
wenzelm@61657
   230
  proof text from left to right.
wenzelm@28754
   231
wenzelm@61421
   232
  \<^medskip>
wenzelm@61657
   233
  Term abbreviations are quite different from local definitions as introduced
wenzelm@63039
   234
  via @{command "define"} (see \secref{sec:proof-context}). The latter are
wenzelm@61657
   235
  visible within the logic as actual equations, while abbreviations disappear
wenzelm@61657
   236
  during the input process just after type checking. Also note that @{command
wenzelm@63039
   237
  "define"} does not support polymorphism.
wenzelm@28754
   238
wenzelm@55112
   239
  @{rail \<open>
wenzelm@42596
   240
    @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')
wenzelm@55112
   241
  \<close>}
wenzelm@28754
   242
wenzelm@42705
   243
  The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
wenzelm@42705
   244
  @{syntax prop_pat} (see \secref{sec:term-decls}).
wenzelm@28754
   245
wenzelm@62280
   246
    \<^descr> \<^theory_text>\<open>let p\<^sub>1 = t\<^sub>1 and \<dots> p\<^sub>n = t\<^sub>n\<close> binds any text variables in patterns
wenzelm@62280
   247
    \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous higher-order matching against terms \<open>t\<^sub>1, \<dots>,
wenzelm@62280
   248
    t\<^sub>n\<close>.
wenzelm@28754
   249
wenzelm@62280
   250
    \<^descr> \<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but matches \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close>
wenzelm@62280
   251
    against the preceding statement. Also note that @{keyword "is"} is not a
wenzelm@62280
   252
    separate command, but part of others (such as @{command "assume"},
wenzelm@61657
   253
    @{command "have"} etc.).
wenzelm@28754
   254
wenzelm@61657
   255
  Some \<^emph>\<open>implicit\<close> term abbreviations\index{term abbreviations} for goals and
wenzelm@61657
   256
  facts are available as well. For any open goal, @{variable_ref thesis}
wenzelm@61657
   257
  refers to its object-level statement, abstracted over any meta-level
wenzelm@61657
   258
  parameters (if present). Likewise, @{variable_ref this} is bound for fact
wenzelm@61657
   259
  statements resulting from assumptions or finished goals. In case @{variable
wenzelm@61657
   260
  this} refers to an object-logic statement that is an application \<open>f t\<close>, then
wenzelm@61657
   261
  \<open>t\<close> is bound to the special text variable ``@{variable "\<dots>"}'' (three dots).
wenzelm@61657
   262
  The canonical application of this convenience are calculational proofs (see
wenzelm@61657
   263
  \secref{sec:calculation}).
wenzelm@58618
   264
\<close>
wenzelm@28754
   265
wenzelm@28754
   266
wenzelm@58618
   267
subsection \<open>Facts and forward chaining \label{sec:proof-facts}\<close>
wenzelm@26870
   268
wenzelm@58618
   269
text \<open>
wenzelm@26870
   270
  \begin{matharray}{rcl}
wenzelm@61493
   271
    @{command_def "note"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
   272
    @{command_def "then"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
wenzelm@61493
   273
    @{command_def "from"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
wenzelm@61493
   274
    @{command_def "with"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
wenzelm@61493
   275
    @{command_def "using"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   276
    @{command_def "unfolding"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
wenzelm@63527
   277
    @{method_def "use"} & : & \<open>method\<close> \\
wenzelm@63527
   278
    @{fact_def "method_facts"} & : & \<open>fact\<close> \\
wenzelm@26870
   279
  \end{matharray}
wenzelm@26870
   280
wenzelm@61657
   281
  New facts are established either by assumption or proof of local statements.
wenzelm@61657
   282
  Any fact will usually be involved in further proofs, either as explicit
wenzelm@61657
   283
  arguments of proof methods, or when forward chaining towards the next goal
wenzelm@61657
   284
  via @{command "then"} (and variants); @{command "from"} and @{command
wenzelm@61657
   285
  "with"} are composite forms involving @{command "note"}. The @{command
wenzelm@61657
   286
  "using"} elements augments the collection of used facts \<^emph>\<open>after\<close> a goal has
wenzelm@61657
   287
  been stated. Note that the special theorem name @{fact_ref this} refers to
wenzelm@61657
   288
  the most recently established facts, but only \<^emph>\<open>before\<close> issuing a follow-up
wenzelm@61657
   289
  claim.
wenzelm@26870
   290
wenzelm@55112
   291
  @{rail \<open>
wenzelm@62969
   292
    @@{command note} (@{syntax thmdef}? @{syntax thms} + @'and')
wenzelm@26870
   293
    ;
wenzelm@42596
   294
    (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})
wenzelm@62969
   295
      (@{syntax thms} + @'and')
wenzelm@63527
   296
    ;
wenzelm@63527
   297
    @{method use} @{syntax thms} @'in' @{syntax method}
wenzelm@55112
   298
  \<close>}
wenzelm@26870
   299
wenzelm@61657
   300
  \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>,
wenzelm@61657
   301
  binding the result as \<open>a\<close>. Note that attributes may be involved as well,
wenzelm@61657
   302
  both on the left and right hand sides.
wenzelm@26870
   303
wenzelm@61657
   304
  \<^descr> @{command "then"} indicates forward chaining by the current facts in order
wenzelm@61657
   305
  to establish the goal to be claimed next. The initial proof method invoked
wenzelm@61657
   306
  to refine that will be offered the facts to do ``anything appropriate'' (see
wenzelm@61657
   307
  also \secref{sec:proof-steps}). For example, method @{method (Pure) rule}
wenzelm@61657
   308
  (see \secref{sec:pure-meth-att}) would typically do an elimination rather
wenzelm@61657
   309
  than an introduction. Automatic methods usually insert the facts into the
wenzelm@61657
   310
  goal state before operation. This provides a simple scheme to control
wenzelm@61657
   311
  relevance of facts in automated proof search.
wenzelm@60483
   312
wenzelm@61657
   313
  \<^descr> @{command "from"}~\<open>b\<close> abbreviates ``@{command "note"}~\<open>b\<close>~@{command
wenzelm@61657
   314
  "then"}''; thus @{command "then"} is equivalent to ``@{command
wenzelm@61657
   315
  "from"}~\<open>this\<close>''.
wenzelm@60483
   316
wenzelm@61657
   317
  \<^descr> @{command "with"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> abbreviates ``@{command "from"}~\<open>b\<^sub>1 \<dots> b\<^sub>n
wenzelm@61657
   318
  \<AND> this\<close>''; thus the forward chaining is from earlier facts together
wenzelm@61657
   319
  with the current ones.
wenzelm@60483
   320
wenzelm@63527
   321
  \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts to be used by a
wenzelm@63527
   322
  subsequent refinement step (such as @{command_ref "apply"} or @{command_ref
wenzelm@63527
   323
  "proof"}).
wenzelm@60483
   324
wenzelm@61657
   325
  \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command
wenzelm@63821
   326
  "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the goal
wenzelm@63821
   327
  state and facts. See also the proof method @{method_ref unfold}.
wenzelm@26870
   328
wenzelm@63527
   329
  \<^descr> \<^theory_text>\<open>(use b\<^sub>1 \<dots> b\<^sub>n in method)\<close> uses the facts in the given method
wenzelm@63527
   330
  expression. The facts provided by the proof state (via @{command "using"}
wenzelm@63527
   331
  etc.) are ignored, but it is possible to refer to @{fact method_facts}
wenzelm@63527
   332
  explicitly.
wenzelm@63527
   333
wenzelm@63527
   334
  \<^descr> @{fact method_facts} is a dynamic fact that refers to the currently used
wenzelm@63527
   335
  facts of the goal state.
wenzelm@63527
   336
wenzelm@26870
   337
wenzelm@61657
   338
  Forward chaining with an empty list of theorems is the same as not chaining
wenzelm@61657
   339
  at all. Thus ``@{command "from"}~\<open>nothing\<close>'' has no effect apart from
wenzelm@61657
   340
  entering \<open>prove(chain)\<close> mode, since @{fact_ref nothing} is bound to the
wenzelm@61657
   341
  empty list of theorems.
wenzelm@26870
   342
wenzelm@42626
   343
  Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple
wenzelm@61657
   344
  facts to be given in their proper order, corresponding to a prefix of the
wenzelm@61657
   345
  premises of the rule involved. Note that positions may be easily skipped
wenzelm@61657
   346
  using something like @{command "from"}~\<open>_ \<AND> a \<AND> b\<close>, for example.
wenzelm@61657
   347
  This involves the trivial rule \<open>PROP \<psi> \<Longrightarrow> PROP \<psi>\<close>, which is bound in
wenzelm@61657
   348
  Isabelle/Pure as ``@{fact_ref "_"}'' (underscore).
wenzelm@26870
   349
wenzelm@61657
   350
  Automated methods (such as @{method simp} or @{method auto}) just insert any
wenzelm@61657
   351
  given facts before their usual operation. Depending on the kind of procedure
wenzelm@61657
   352
  involved, the order of facts is less significant here.
wenzelm@58618
   353
\<close>
wenzelm@26870
   354
wenzelm@26870
   355
wenzelm@58618
   356
subsection \<open>Goals \label{sec:goals}\<close>
wenzelm@26870
   357
wenzelm@58618
   358
text \<open>
wenzelm@26870
   359
  \begin{matharray}{rcl}
wenzelm@61493
   360
    @{command_def "lemma"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   361
    @{command_def "theorem"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   362
    @{command_def "corollary"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   363
    @{command_def "proposition"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   364
    @{command_def "schematic_goal"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   365
    @{command_def "have"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   366
    @{command_def "show"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   367
    @{command_def "hence"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   368
    @{command_def "thus"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
   369
    @{command_def "print_statement"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@26870
   370
  \end{matharray}
wenzelm@26870
   371
wenzelm@61657
   372
  From a theory context, proof mode is entered by an initial goal command such
wenzelm@61657
   373
  as @{command "lemma"}. Within a proof context, new claims may be introduced
wenzelm@61657
   374
  locally; there are variants to interact with the overall proof structure
wenzelm@61657
   375
  specifically, such as @{command have} or @{command show}.
wenzelm@26870
   376
wenzelm@61657
   377
  Goals may consist of multiple statements, resulting in a list of facts
wenzelm@61657
   378
  eventually. A pending multi-goal is internally represented as a meta-level
wenzelm@61657
   379
  conjunction (\<open>&&&\<close>), which is usually split into the corresponding number of
wenzelm@61657
   380
  sub-goals prior to an initial method application, via @{command_ref "proof"}
wenzelm@26870
   381
  (\secref{sec:proof-steps}) or @{command_ref "apply"}
wenzelm@61657
   382
  (\secref{sec:tactic-commands}). The @{method_ref induct} method covered in
wenzelm@61657
   383
  \secref{sec:cases-induct} acts on multiple claims simultaneously.
wenzelm@26870
   384
wenzelm@61657
   385
  Claims at the theory level may be either in short or long form. A short goal
wenzelm@61657
   386
  merely consists of several simultaneous propositions (often just one). A
wenzelm@61657
   387
  long goal includes an explicit context specification for the subsequent
wenzelm@61657
   388
  conclusion, involving local parameters and assumptions. Here the role of
wenzelm@61657
   389
  each part of the statement is explicitly marked by separate keywords (see
wenzelm@61657
   390
  also \secref{sec:locale}); the local assumptions being introduced here are
wenzelm@61657
   391
  available as @{fact_ref assms} in the proof. Moreover, there are two kinds
wenzelm@61657
   392
  of conclusions: @{element_def "shows"} states several simultaneous
wenzelm@61657
   393
  propositions (essentially a big conjunction), while @{element_def "obtains"}
wenzelm@61657
   394
  claims several simultaneous simultaneous contexts of (essentially a big
wenzelm@61657
   395
  disjunction of eliminated parameters and assumptions, cf.\
wenzelm@61657
   396
  \secref{sec:obtain}).
wenzelm@26870
   397
wenzelm@55112
   398
  @{rail \<open>
wenzelm@42596
   399
    (@@{command lemma} | @@{command theorem} | @@{command corollary} |
wenzelm@63094
   400
     @@{command proposition} | @@{command schematic_goal})
wenzelm@63094
   401
      (long_statement | short_statement)
wenzelm@26870
   402
    ;
wenzelm@60406
   403
    (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
wenzelm@60555
   404
      stmt cond_stmt @{syntax for_fixes}
wenzelm@26870
   405
    ;
wenzelm@62969
   406
    @@{command print_statement} @{syntax modes}? @{syntax thms}
wenzelm@26870
   407
    ;
wenzelm@60483
   408
wenzelm@60406
   409
    stmt: (@{syntax props} + @'and')
wenzelm@26870
   410
    ;
wenzelm@60555
   411
    cond_stmt: ((@'if' | @'when') stmt)?
wenzelm@60555
   412
    ;
wenzelm@63094
   413
    short_statement: stmt (@'if' stmt)? @{syntax for_fixes}
wenzelm@63094
   414
    ;
wenzelm@63094
   415
    long_statement: @{syntax thmdecl}? context conclusion
wenzelm@63094
   416
    ;
wenzelm@63094
   417
    context: (@{syntax_ref "includes"}?) (@{syntax context_elem} *)
wenzelm@26870
   418
    ;
wenzelm@60459
   419
    conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}
wenzelm@26870
   420
    ;
wenzelm@60459
   421
    @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')
wenzelm@60459
   422
    ;
wenzelm@63285
   423
    @{syntax_def obtain_case}: @{syntax vars} @'where'
wenzelm@60459
   424
      (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
wenzelm@55112
   425
  \<close>}
wenzelm@26870
   426
wenzelm@61657
   427
  \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with \<open>\<phi>\<close> as main goal,
wenzelm@61657
   428
  eventually resulting in some fact \<open>\<turnstile> \<phi>\<close> to be put back into the target
wenzelm@63094
   429
  context.
wenzelm@63094
   430
wenzelm@63094
   431
  A @{syntax long_statement} may build up an initial proof context for the
wenzelm@63094
   432
  subsequent claim, potentially including local definitions and syntax; see
wenzelm@63094
   433
  also @{syntax "includes"} in \secref{sec:bundle} and @{syntax context_elem}
wenzelm@63094
   434
  in \secref{sec:locale}.
wenzelm@63094
   435
wenzelm@63094
   436
  A @{syntax short_statement} consists of propositions as conclusion, with an
wenzelm@63094
   437
  option context of premises and parameters, via \<^verbatim>\<open>if\<close>/\<^verbatim>\<open>for\<close> in postfix
wenzelm@63094
   438
  notation, corresponding to \<^verbatim>\<open>assumes\<close>/\<^verbatim>\<open>fixes\<close> in the long prefix notation.
wenzelm@63094
   439
wenzelm@63094
   440
  Local premises (if present) are called ``\<open>assms\<close>'' for @{syntax
wenzelm@63094
   441
  long_statement}, and ``\<open>that\<close>'' for @{syntax short_statement}.
wenzelm@60483
   442
wenzelm@61657
   443
  \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command "proposition"}
wenzelm@61657
   444
  are the same as @{command "lemma"}. The different command names merely serve
wenzelm@61657
   445
  as a formal comment in the theory source.
wenzelm@36320
   446
wenzelm@61657
   447
  \<^descr> @{command "schematic_goal"} is similar to @{command "theorem"}, but allows
wenzelm@61657
   448
  the statement to contain unbound schematic variables.
wenzelm@36320
   449
wenzelm@61657
   450
  Under normal circumstances, an Isar proof text needs to specify claims
wenzelm@61657
   451
  explicitly. Schematic goals are more like goals in Prolog, where certain
wenzelm@61657
   452
  results are synthesized in the course of reasoning. With schematic
wenzelm@61657
   453
  statements, the inherent compositionality of Isar proofs is lost, which also
wenzelm@61657
   454
  impacts performance, because proof checking is forced into sequential mode.
wenzelm@60483
   455
wenzelm@61657
   456
  \<^descr> @{command "have"}~\<open>a: \<phi>\<close> claims a local goal, eventually resulting in a
wenzelm@61657
   457
  fact within the current logical context. This operation is completely
wenzelm@61657
   458
  independent of any pending sub-goals of an enclosing goal statements, so
wenzelm@61657
   459
  @{command "have"} may be freely used for experimental exploration of
wenzelm@61657
   460
  potential results within a proof body.
wenzelm@60483
   461
wenzelm@61657
   462
  \<^descr> @{command "show"}~\<open>a: \<phi>\<close> is like @{command "have"}~\<open>a: \<phi>\<close> plus a second
wenzelm@61657
   463
  stage to refine some pending sub-goal for each one of the finished result,
wenzelm@61657
   464
  after having been exported into the corresponding context (at the head of
wenzelm@61657
   465
  the sub-proof of this @{command "show"} command).
wenzelm@60483
   466
wenzelm@61657
   467
  To accommodate interactive debugging, resulting rules are printed before
wenzelm@61657
   468
  being applied internally. Even more, interactive execution of @{command
wenzelm@61657
   469
  "show"} predicts potential failure and displays the resulting error as a
wenzelm@61657
   470
  warning beforehand. Watch out for the following message:
wenzelm@61408
   471
  @{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>}
wenzelm@60483
   472
wenzelm@62268
   473
  \<^descr> @{command "hence"} expands to ``@{command "then"}~@{command "have"}'' and
wenzelm@62268
   474
  @{command "thus"} expands to ``@{command "then"}~@{command "show"}''. These
wenzelm@62268
   475
  conflations are left-over from early history of Isar. The expanded syntax is
wenzelm@62268
   476
  more orthogonal and improves readability and maintainability of proofs.
wenzelm@60483
   477
wenzelm@61657
   478
  \<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the current theory or
wenzelm@61657
   479
  proof context in long statement form, according to the syntax for @{command
wenzelm@61657
   480
  "lemma"} given above.
wenzelm@26870
   481
wenzelm@26870
   482
wenzelm@61657
   483
  Any goal statement causes some term abbreviations (such as @{variable_ref
wenzelm@61657
   484
  "?thesis"}) to be bound automatically, see also \secref{sec:term-abbrev}.
wenzelm@26870
   485
wenzelm@60555
   486
  Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref
wenzelm@60555
   487
  "when"} define the special fact @{fact_ref that} to refer to these
wenzelm@61657
   488
  assumptions in the proof body. The user may provide separate names according
wenzelm@61657
   489
  to the syntax of the statement.
wenzelm@58618
   490
\<close>
wenzelm@26870
   491
wenzelm@26870
   492
wenzelm@60483
   493
section \<open>Calculational reasoning \label{sec:calculation}\<close>
wenzelm@60483
   494
wenzelm@60483
   495
text \<open>
wenzelm@60483
   496
  \begin{matharray}{rcl}
wenzelm@61493
   497
    @{command_def "also"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
   498
    @{command_def "finally"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
wenzelm@61493
   499
    @{command_def "moreover"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
   500
    @{command_def "ultimately"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
wenzelm@61493
   501
    @{command_def "print_trans_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   502
    @{attribute trans} & : & \<open>attribute\<close> \\
wenzelm@61493
   503
    @{attribute sym} & : & \<open>attribute\<close> \\
wenzelm@61493
   504
    @{attribute symmetric} & : & \<open>attribute\<close> \\
wenzelm@60483
   505
  \end{matharray}
wenzelm@60483
   506
wenzelm@61657
   507
  Calculational proof is forward reasoning with implicit application of
wenzelm@61657
   508
  transitivity rules (such those of \<open>=\<close>, \<open>\<le>\<close>, \<open><\<close>). Isabelle/Isar maintains an
wenzelm@61657
   509
  auxiliary fact register @{fact_ref calculation} for accumulating results
wenzelm@61657
   510
  obtained by transitivity composed with the current result. Command @{command
wenzelm@61657
   511
  "also"} updates @{fact calculation} involving @{fact this}, while @{command
wenzelm@61657
   512
  "finally"} exhibits the final @{fact calculation} by forward chaining
wenzelm@61657
   513
  towards the next goal statement. Both commands require valid current facts,
wenzelm@61657
   514
  i.e.\ may occur only after commands that produce theorems such as @{command
wenzelm@61657
   515
  "assume"}, @{command "note"}, or some finished proof of @{command "have"},
wenzelm@61657
   516
  @{command "show"} etc. The @{command "moreover"} and @{command "ultimately"}
wenzelm@61657
   517
  commands are similar to @{command "also"} and @{command "finally"}, but only
wenzelm@61657
   518
  collect further results in @{fact calculation} without applying any rules
wenzelm@61657
   519
  yet.
wenzelm@60483
   520
wenzelm@61657
   521
  Also note that the implicit term abbreviation ``\<open>\<dots>\<close>'' has its canonical
wenzelm@61657
   522
  application with calculational proofs. It refers to the argument of the
wenzelm@61657
   523
  preceding statement. (The argument of a curried infix expression happens to
wenzelm@61657
   524
  be its right-hand side.)
wenzelm@60483
   525
wenzelm@61657
   526
  Isabelle/Isar calculations are implicitly subject to block structure in the
wenzelm@61657
   527
  sense that new threads of calculational reasoning are commenced for any new
wenzelm@61657
   528
  block (as opened by a local goal, for example). This means that, apart from
wenzelm@61657
   529
  being able to nest calculations, there is no separate \<^emph>\<open>begin-calculation\<close>
wenzelm@61657
   530
  command required.
wenzelm@60483
   531
wenzelm@61421
   532
  \<^medskip>
wenzelm@61657
   533
  The Isar calculation proof commands may be defined as follows:\<^footnote>\<open>We suppress
wenzelm@61657
   534
  internal bookkeeping such as proper handling of block-structure.\<close>
wenzelm@60483
   535
wenzelm@60483
   536
  \begin{matharray}{rcl}
wenzelm@61493
   537
    @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\
wenzelm@64926
   538
    @{command "also"}\<open>\<^sub>n\<^sub>+\<^sub>1\<close> & \equiv & @{command "note"}~\<open>calculation = trans [OF calculation this]\<close> \\[0.5ex]
wenzelm@61493
   539
    @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\[0.5ex]
wenzelm@61493
   540
    @{command "moreover"} & \equiv & @{command "note"}~\<open>calculation = calculation this\<close> \\
wenzelm@61493
   541
    @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~\<open>calculation\<close> \\
wenzelm@60483
   542
  \end{matharray}
wenzelm@60483
   543
wenzelm@60483
   544
  @{rail \<open>
wenzelm@62969
   545
    (@@{command also} | @@{command finally}) ('(' @{syntax thms} ')')?
wenzelm@60483
   546
    ;
wenzelm@60483
   547
    @@{attribute trans} (() | 'add' | 'del')
wenzelm@60483
   548
  \<close>}
wenzelm@60483
   549
wenzelm@61657
   550
  \<^descr> @{command "also"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains the auxiliary @{fact
wenzelm@61657
   551
  calculation} register as follows. The first occurrence of @{command "also"}
wenzelm@61657
   552
  in some calculational thread initializes @{fact calculation} by @{fact
wenzelm@61657
   553
  this}. Any subsequent @{command "also"} on the same level of block-structure
wenzelm@61657
   554
  updates @{fact calculation} by some transitivity rule applied to @{fact
wenzelm@61657
   555
  calculation} and @{fact this} (in that order). Transitivity rules are picked
wenzelm@61657
   556
  from the current context, unless alternative rules are given as explicit
wenzelm@60483
   557
  arguments.
wenzelm@60483
   558
wenzelm@64926
   559
  \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains @{fact calculation} in the
wenzelm@64926
   560
  same way as @{command "also"} and then concludes the current calculational
wenzelm@61657
   561
  thread. The final result is exhibited as fact for forward chaining towards
wenzelm@64926
   562
  the next goal. Basically, @{command "finally"} abbreviates @{command
wenzelm@61657
   563
  "also"}~@{command "from"}~@{fact calculation}. Typical idioms for concluding
wenzelm@60483
   564
  calculational proofs are ``@{command "finally"}~@{command
wenzelm@61657
   565
  "show"}~\<open>?thesis\<close>~@{command "."}'' and ``@{command "finally"}~@{command
wenzelm@61657
   566
  "have"}~\<open>\<phi>\<close>~@{command "."}''.
wenzelm@60483
   567
wenzelm@61657
   568
  \<^descr> @{command "moreover"} and @{command "ultimately"} are analogous to
wenzelm@61657
   569
  @{command "also"} and @{command "finally"}, but collect results only,
wenzelm@61657
   570
  without applying rules.
wenzelm@60483
   571
wenzelm@61657
   572
  \<^descr> @{command "print_trans_rules"} prints the list of transitivity rules (for
wenzelm@61657
   573
  calculational commands @{command "also"} and @{command "finally"}) and
wenzelm@61657
   574
  symmetry rules (for the @{attribute symmetric} operation and single step
wenzelm@61657
   575
  elimination patters) of the current context.
wenzelm@60483
   576
wenzelm@61439
   577
  \<^descr> @{attribute trans} declares theorems as transitivity rules.
wenzelm@60483
   578
wenzelm@61657
   579
  \<^descr> @{attribute sym} declares symmetry rules, as well as @{attribute
wenzelm@61657
   580
  "Pure.elim"}\<open>?\<close> rules.
wenzelm@60483
   581
wenzelm@61657
   582
  \<^descr> @{attribute symmetric} resolves a theorem with some rule declared as
wenzelm@61657
   583
  @{attribute sym} in the current context. For example, ``@{command
wenzelm@61657
   584
  "assume"}~\<open>[symmetric]: x = y\<close>'' produces a swapped fact derived from that
wenzelm@61657
   585
  assumption.
wenzelm@60483
   586
wenzelm@61657
   587
  In structured proof texts it is often more appropriate to use an explicit
wenzelm@61657
   588
  single-step elimination proof, such as ``@{command "assume"}~\<open>x =
wenzelm@61657
   589
  y\<close>~@{command "then"}~@{command "have"}~\<open>y = x\<close>~@{command ".."}''.
wenzelm@60483
   590
\<close>
wenzelm@60483
   591
wenzelm@60483
   592
wenzelm@58618
   593
section \<open>Refinement steps\<close>
wenzelm@28754
   594
wenzelm@58618
   595
subsection \<open>Proof method expressions \label{sec:proof-meth}\<close>
wenzelm@28754
   596
wenzelm@61657
   597
text \<open>
wenzelm@61657
   598
  Proof methods are either basic ones, or expressions composed of methods via
wenzelm@61657
   599
  ``\<^verbatim>\<open>,\<close>'' (sequential composition), ``\<^verbatim>\<open>;\<close>'' (structural composition),
wenzelm@61657
   600
  ``\<^verbatim>\<open>|\<close>'' (alternative choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least
wenzelm@61657
   601
  once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first \<open>n\<close> subgoals). In practice,
wenzelm@61657
   602
  proof methods are usually just a comma separated list of @{syntax
wenzelm@62969
   603
  name}~@{syntax args} specifications. Note that parentheses may be dropped
wenzelm@61657
   604
  for single method specifications (with no arguments). The syntactic
wenzelm@61657
   605
  precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close> \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low
wenzelm@61657
   606
  to high).
wenzelm@28754
   607
wenzelm@55112
   608
  @{rail \<open>
wenzelm@42596
   609
    @{syntax_def method}:
wenzelm@62969
   610
      (@{syntax name} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
wenzelm@28754
   611
    ;
wenzelm@62969
   612
    methods: (@{syntax name} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
wenzelm@55112
   613
  \<close>}
wenzelm@28754
   614
wenzelm@61657
   615
  Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but refer
wenzelm@61657
   616
  to the first subgoal or to all subgoals uniformly. Nonetheless, the
wenzelm@61657
   617
  subsequent mechanisms allow to imitate the effect of subgoal addressing that
wenzelm@61657
   618
  is known from ML tactics.
wenzelm@59660
   619
wenzelm@61421
   620
  \<^medskip>
wenzelm@61657
   621
  Goal \<^emph>\<open>restriction\<close> means the proof state is wrapped-up in a way that
wenzelm@61657
   622
  certain subgoals are exposed, and other subgoals are ``parked'' elsewhere.
wenzelm@61657
   623
  Thus a proof method has no other chance than to operate on the subgoals that
wenzelm@61657
   624
  are presently exposed.
wenzelm@28754
   625
wenzelm@61657
   626
  Structural composition ``\<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means that method \<open>m\<^sub>1\<close> is
wenzelm@61657
   627
  applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied
wenzelm@61657
   628
  consecutively with restriction to each subgoal that has newly emerged due to
wenzelm@61657
   629
  \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator @{ML_op THEN_ALL_NEW} in
wenzelm@61657
   630
  Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule
wenzelm@61657
   631
  r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
wenzelm@59660
   632
wenzelm@61657
   633
  Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes only the
wenzelm@61657
   634
  first \<open>n\<close> subgoals (which need to exist), with default \<open>n = 1\<close>. For example,
wenzelm@61657
   635
  the method expression ``\<open>simp_all[3]\<close>'' simplifies the first three subgoals,
wenzelm@61657
   636
  while ``\<open>(rule r, simp_all)[]\<close>'' simplifies all new goals that emerge from
wenzelm@61493
   637
  applying rule \<open>r\<close> to the originally first one.
wenzelm@59660
   638
wenzelm@61421
   639
  \<^medskip>
wenzelm@61657
   640
  Improper methods, notably tactic emulations, offer low-level goal addressing
wenzelm@61657
   641
  as explicit argument to the individual tactic being involved. Here ``\<open>[!]\<close>''
wenzelm@61657
   642
  refers to all goals, and ``\<open>[n-]\<close>'' to all goals starting from \<open>n\<close>.
wenzelm@28754
   643
wenzelm@55112
   644
  @{rail \<open>
wenzelm@42705
   645
    @{syntax_def goal_spec}:
wenzelm@42596
   646
      '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'
wenzelm@55112
   647
  \<close>}
wenzelm@58618
   648
\<close>
wenzelm@28754
   649
wenzelm@28754
   650
wenzelm@58618
   651
subsection \<open>Initial and terminal proof steps \label{sec:proof-steps}\<close>
wenzelm@26870
   652
wenzelm@58618
   653
text \<open>
wenzelm@26870
   654
  \begin{matharray}{rcl}
wenzelm@61493
   655
    @{command_def "proof"} & : & \<open>proof(prove) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
   656
    @{command_def "qed"} & : & \<open>proof(state) \<rightarrow> proof(state) | local_theory | theory\<close> \\
wenzelm@61493
   657
    @{command_def "by"} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
wenzelm@61493
   658
    @{command_def ".."} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
wenzelm@61493
   659
    @{command_def "."} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
wenzelm@61493
   660
    @{command_def "sorry"} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
wenzelm@61493
   661
    @{method_def standard} & : & \<open>method\<close> \\
wenzelm@26870
   662
  \end{matharray}
wenzelm@26870
   663
wenzelm@61657
   664
  Arbitrary goal refinement via tactics is considered harmful. Structured
wenzelm@61657
   665
  proof composition in Isar admits proof methods to be invoked in two places
wenzelm@61657
   666
  only.
wenzelm@60483
   667
wenzelm@61657
   668
    \<^enum> An \<^emph>\<open>initial\<close> refinement step @{command_ref "proof"}~\<open>m\<^sub>1\<close> reduces a
wenzelm@61657
   669
    newly stated goal to a number of sub-goals that are to be solved later.
wenzelm@61657
   670
    Facts are passed to \<open>m\<^sub>1\<close> for forward chaining, if so indicated by
wenzelm@61657
   671
    \<open>proof(chain)\<close> mode.
wenzelm@64926
   672
wenzelm@61657
   673
    \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~\<open>m\<^sub>2\<close> is intended to
wenzelm@61657
   674
    solve remaining goals. No facts are passed to \<open>m\<^sub>2\<close>.
wenzelm@26870
   675
wenzelm@61657
   676
  The only other (proper) way to affect pending goals in a proof body is by
wenzelm@61657
   677
  @{command_ref "show"}, which involves an explicit statement of what is to be
wenzelm@61657
   678
  solved eventually. Thus we avoid the fundamental problem of unstructured
wenzelm@61657
   679
  tactic scripts that consist of numerous consecutive goal transformations,
wenzelm@61657
   680
  with invisible effects.
wenzelm@26870
   681
wenzelm@61421
   682
  \<^medskip>
wenzelm@61657
   683
  As a general rule of thumb for good proof style, initial proof methods
wenzelm@61657
   684
  should either solve the goal completely, or constitute some well-understood
wenzelm@61657
   685
  reduction to new sub-goals. Arbitrary automatic proof tools that are prone
wenzelm@61657
   686
  leave a large number of badly structured sub-goals are no help in continuing
wenzelm@61657
   687
  the proof document in an intelligible manner.
wenzelm@26870
   688
wenzelm@61657
   689
  Unless given explicitly by the user, the default initial method is @{method
wenzelm@61657
   690
  standard}, which subsumes at least @{method_ref (Pure) rule} or its
wenzelm@61657
   691
  classical variant @{method_ref (HOL) rule}. These methods apply a single
wenzelm@61657
   692
  standard elimination or introduction rule according to the topmost logical
wenzelm@61657
   693
  connective involved. There is no separate default terminal method. Any
wenzelm@61657
   694
  remaining goals are always solved by assumption in the very last step.
wenzelm@26870
   695
wenzelm@55112
   696
  @{rail \<open>
wenzelm@42596
   697
    @@{command proof} method?
wenzelm@26870
   698
    ;
wenzelm@42596
   699
    @@{command qed} method?
wenzelm@26870
   700
    ;
wenzelm@55112
   701
    @@{command "by"} method method?
wenzelm@26870
   702
    ;
wenzelm@55112
   703
    (@@{command "."} | @@{command ".."} | @@{command sorry})
wenzelm@55112
   704
  \<close>}
wenzelm@26870
   705
wenzelm@61657
   706
  \<^descr> @{command "proof"}~\<open>m\<^sub>1\<close> refines the goal by proof method \<open>m\<^sub>1\<close>; facts for
wenzelm@61657
   707
  forward chaining are passed if so indicated by \<open>proof(chain)\<close> mode.
wenzelm@60483
   708
wenzelm@61657
   709
  \<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by proof method \<open>m\<^sub>2\<close>
wenzelm@62268
   710
  and concludes the sub-proof by assumption. If the goal had been \<open>show\<close>, some
wenzelm@62268
   711
  pending sub-goal is solved as well by the rule resulting from the result
wenzelm@62268
   712
  \<^emph>\<open>exported\<close> into the enclosing goal context. Thus \<open>qed\<close> may fail for two
wenzelm@62268
   713
  reasons: either \<open>m\<^sub>2\<close> fails, or the resulting rule does not fit to any
wenzelm@62268
   714
  pending goal\<^footnote>\<open>This includes any additional ``strong'' assumptions as
wenzelm@61657
   715
  introduced by @{command "assume"}.\<close> of the enclosing context. Debugging such
wenzelm@61657
   716
  a situation might involve temporarily changing @{command "show"} into
wenzelm@61657
   717
  @{command "have"}, or weakening the local context by replacing occurrences
wenzelm@61657
   718
  of @{command "assume"} by @{command "presume"}.
wenzelm@60483
   719
wenzelm@61657
   720
  \<^descr> @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> is a \<^emph>\<open>terminal proof\<close>\index{proof!terminal}; it
wenzelm@61657
   721
  abbreviates @{command "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close>, but with
wenzelm@61657
   722
  backtracking across both methods. Debugging an unsuccessful @{command
wenzelm@61657
   723
  "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> command can be done by expanding its definition; in many
wenzelm@61657
   724
  cases @{command "proof"}~\<open>m\<^sub>1\<close> (or even \<open>apply\<close>~\<open>m\<^sub>1\<close>) is already sufficient
wenzelm@61657
   725
  to see the problem.
wenzelm@26870
   726
wenzelm@61657
   727
  \<^descr> ``@{command ".."}'' is a \<^emph>\<open>standard proof\<close>\index{proof!standard}; it
wenzelm@61657
   728
  abbreviates @{command "by"}~\<open>standard\<close>.
wenzelm@26870
   729
wenzelm@61657
   730
  \<^descr> ``@{command "."}'' is a \<^emph>\<open>trivial proof\<close>\index{proof!trivial}; it
wenzelm@61657
   731
  abbreviates @{command "by"}~\<open>this\<close>.
wenzelm@60483
   732
wenzelm@61657
   733
  \<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake} pretending to
wenzelm@61657
   734
  solve the pending claim without further ado. This only works in interactive
wenzelm@61657
   735
  development, or if the @{attribute quick_and_dirty} is enabled. Facts
wenzelm@61657
   736
  emerging from fake proofs are not the real thing. Internally, the derivation
wenzelm@61657
   737
  object is tainted by an oracle invocation, which may be inspected via the
wenzelm@58552
   738
  theorem status @{cite "isabelle-implementation"}.
wenzelm@60483
   739
wenzelm@26870
   740
  The most important application of @{command "sorry"} is to support
wenzelm@26870
   741
  experimentation and top-down proof development.
wenzelm@26870
   742
wenzelm@61657
   743
  \<^descr> @{method standard} refers to the default refinement step of some Isar
wenzelm@61657
   744
  language elements (notably @{command proof} and ``@{command ".."}''). It is
wenzelm@61657
   745
  \<^emph>\<open>dynamically scoped\<close>, so the behaviour depends on the application
wenzelm@61657
   746
  environment.
wenzelm@60618
   747
wenzelm@60618
   748
  In Isabelle/Pure, @{method standard} performs elementary introduction~/
wenzelm@61657
   749
  elimination steps (@{method_ref (Pure) rule}), introduction of type classes
wenzelm@61657
   750
  (@{method_ref intro_classes}) and locales (@{method_ref intro_locales}).
wenzelm@60618
   751
wenzelm@61657
   752
  In Isabelle/HOL, @{method standard} also takes classical rules into account
wenzelm@61657
   753
  (cf.\ \secref{sec:classical}).
wenzelm@58618
   754
\<close>
wenzelm@26870
   755
wenzelm@26870
   756
wenzelm@58618
   757
subsection \<open>Fundamental methods and attributes \label{sec:pure-meth-att}\<close>
wenzelm@26870
   758
wenzelm@58618
   759
text \<open>
wenzelm@61657
   760
  The following proof methods and attributes refer to basic logical operations
wenzelm@61657
   761
  of Isar. Further methods and attributes are provided by several generic and
wenzelm@61657
   762
  object-logic specific tools and packages (see \chref{ch:gen-tools} and
wenzelm@61657
   763
  \partref{part:hol}).
wenzelm@26870
   764
wenzelm@26870
   765
  \begin{matharray}{rcl}
wenzelm@61493
   766
    @{command_def "print_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\[0.5ex]
wenzelm@61493
   767
    @{method_def "-"} & : & \<open>method\<close> \\
wenzelm@61493
   768
    @{method_def "goal_cases"} & : & \<open>method\<close> \\
wenzelm@61493
   769
    @{method_def "fact"} & : & \<open>method\<close> \\
wenzelm@61493
   770
    @{method_def "assumption"} & : & \<open>method\<close> \\
wenzelm@61493
   771
    @{method_def "this"} & : & \<open>method\<close> \\
wenzelm@61493
   772
    @{method_def (Pure) "rule"} & : & \<open>method\<close> \\
wenzelm@61493
   773
    @{attribute_def (Pure) "intro"} & : & \<open>attribute\<close> \\
wenzelm@61493
   774
    @{attribute_def (Pure) "elim"} & : & \<open>attribute\<close> \\
wenzelm@61493
   775
    @{attribute_def (Pure) "dest"} & : & \<open>attribute\<close> \\
wenzelm@61493
   776
    @{attribute_def (Pure) "rule"} & : & \<open>attribute\<close> \\[0.5ex]
wenzelm@61493
   777
    @{attribute_def "OF"} & : & \<open>attribute\<close> \\
wenzelm@61493
   778
    @{attribute_def "of"} & : & \<open>attribute\<close> \\
wenzelm@61493
   779
    @{attribute_def "where"} & : & \<open>attribute\<close> \\
wenzelm@26870
   780
  \end{matharray}
wenzelm@26870
   781
wenzelm@55112
   782
  @{rail \<open>
wenzelm@61166
   783
    @@{method goal_cases} (@{syntax name}*)
wenzelm@60578
   784
    ;
wenzelm@62969
   785
    @@{method fact} @{syntax thms}?
wenzelm@42596
   786
    ;
wenzelm@62969
   787
    @@{method (Pure) rule} @{syntax thms}?
wenzelm@26870
   788
    ;
wenzelm@42596
   789
    rulemod: ('intro' | 'elim' | 'dest')
wenzelm@62969
   790
      ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thms}
wenzelm@26870
   791
    ;
wenzelm@42596
   792
    (@@{attribute intro} | @@{attribute elim} | @@{attribute dest})
wenzelm@42596
   793
      ('!' | () | '?') @{syntax nat}?
wenzelm@26870
   794
    ;
wenzelm@42626
   795
    @@{attribute (Pure) rule} 'del'
wenzelm@26870
   796
    ;
wenzelm@62969
   797
    @@{attribute OF} @{syntax thms}
wenzelm@26870
   798
    ;
wenzelm@59785
   799
    @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes}
wenzelm@26870
   800
    ;
wenzelm@59853
   801
    @@{attribute "where"} @{syntax named_insts} @{syntax for_fixes}
wenzelm@55112
   802
  \<close>}
wenzelm@26870
   803
wenzelm@61657
   804
  \<^descr> @{command "print_rules"} prints rules declared via attributes @{attribute
wenzelm@61657
   805
  (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure) dest} of
wenzelm@61657
   806
  Isabelle/Pure.
wenzelm@51077
   807
wenzelm@61657
   808
  See also the analogous @{command "print_claset"} command for similar rule
wenzelm@61657
   809
  declarations of the classical reasoner (\secref{sec:classical}).
wenzelm@51077
   810
wenzelm@61657
   811
  \<^descr> ``@{method "-"}'' (minus) inserts the forward chaining facts as premises
wenzelm@61657
   812
  into the goal, and nothing else.
wenzelm@60578
   813
wenzelm@60578
   814
  Note that command @{command_ref "proof"} without any method actually
wenzelm@61657
   815
  performs a single reduction step using the @{method_ref (Pure) rule} method;
wenzelm@61657
   816
  thus a plain \<^emph>\<open>do-nothing\<close> proof step would be ``@{command "proof"}~\<open>-\<close>''
wenzelm@61657
   817
  rather than @{command "proof"} alone.
wenzelm@60578
   818
wenzelm@61657
   819
  \<^descr> @{method "goal_cases"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> turns the current subgoals into cases
wenzelm@61657
   820
  within the context (see also \secref{sec:cases-induct}). The specified case
wenzelm@61657
   821
  names are used if present; otherwise cases are numbered starting from 1.
wenzelm@60578
   822
wenzelm@60578
   823
  Invoking cases in the subsequent proof body via the @{command_ref case}
wenzelm@60578
   824
  command will @{command fix} goal parameters, @{command assume} goal
wenzelm@60578
   825
  premises, and @{command let} variable @{variable_ref ?case} refer to the
wenzelm@60578
   826
  conclusion.
wenzelm@60483
   827
wenzelm@61657
   828
  \<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or
wenzelm@61657
   829
  implicitly from the current proof context) modulo unification of schematic
wenzelm@61657
   830
  type and term variables. The rule structure is not taken into account, i.e.\
wenzelm@61657
   831
  meta-level implication is considered atomic. This is the same principle
wenzelm@61657
   832
  underlying literal facts (cf.\ \secref{sec:syn-att}): ``@{command
wenzelm@61657
   833
  "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to ``@{command
wenzelm@61657
   834
  "note"}~\<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close>'' provided that \<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close>
wenzelm@61657
   835
  in the proof context.
wenzelm@60483
   836
wenzelm@61657
   837
  \<^descr> @{method assumption} solves some goal by a single assumption step. All
wenzelm@61657
   838
  given facts are guaranteed to participate in the refinement; this means
wenzelm@61657
   839
  there may be only 0 or 1 in the first place. Recall that @{command "qed"}
wenzelm@61657
   840
  (\secref{sec:proof-steps}) already concludes any remaining sub-goals by
wenzelm@61657
   841
  assumption, so structured proofs usually need not quote the @{method
wenzelm@61657
   842
  assumption} method at all.
wenzelm@60483
   843
wenzelm@61657
   844
  \<^descr> @{method this} applies all of the current facts directly as rules. Recall
wenzelm@61657
   845
  that ``@{command "."}'' (dot) abbreviates ``@{command "by"}~\<open>this\<close>''.
wenzelm@60483
   846
wenzelm@61657
   847
  \<^descr> @{method (Pure) rule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some rule given as argument in
wenzelm@61657
   848
  backward manner; facts are used to reduce the rule before applying it to the
wenzelm@61657
   849
  goal. Thus @{method (Pure) rule} without facts is plain introduction, while
wenzelm@61657
   850
  with facts it becomes elimination.
wenzelm@60483
   851
wenzelm@61657
   852
  When no arguments are given, the @{method (Pure) rule} method tries to pick
wenzelm@61657
   853
  appropriate rules automatically, as declared in the current context using
wenzelm@61657
   854
  the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure)
wenzelm@61657
   855
  dest} attributes (see below). This is included in the standard behaviour of
wenzelm@61657
   856
  @{command "proof"} and ``@{command ".."}'' (double-dot) steps (see
wenzelm@61657
   857
  \secref{sec:proof-steps}).
wenzelm@60483
   858
wenzelm@61657
   859
  \<^descr> @{attribute (Pure) intro}, @{attribute (Pure) elim}, and @{attribute
wenzelm@61657
   860
  (Pure) dest} declare introduction, elimination, and destruct rules, to be
wenzelm@61657
   861
  used with method @{method (Pure) rule}, and similar tools. Note that the
wenzelm@61657
   862
  latter will ignore rules declared with ``\<open>?\<close>'', while ``\<open>!\<close>'' are used most
wenzelm@61657
   863
  aggressively.
wenzelm@60483
   864
wenzelm@61657
   865
  The classical reasoner (see \secref{sec:classical}) introduces its own
wenzelm@61657
   866
  variants of these attributes; use qualified names to access the present
wenzelm@61657
   867
  versions of Isabelle/Pure, i.e.\ @{attribute (Pure) "Pure.intro"}.
wenzelm@60483
   868
wenzelm@61657
   869
  \<^descr> @{attribute (Pure) rule}~\<open>del\<close> undeclares introduction, elimination, or
wenzelm@61657
   870
  destruct rules.
wenzelm@51077
   871
wenzelm@61657
   872
  \<^descr> @{attribute OF}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some theorem to all of the given rules
wenzelm@61657
   873
  \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> in canonical right-to-left order, which means that premises
wenzelm@61657
   874
  stemming from the \<open>a\<^sub>i\<close> emerge in parallel in the result, without
wenzelm@61657
   875
  interfering with each other. In many practical situations, the \<open>a\<^sub>i\<close> do not
wenzelm@61657
   876
  have premises themselves, so \<open>rule [OF a\<^sub>1 \<dots> a\<^sub>n]\<close> can be actually read as
wenzelm@61657
   877
  functional application (modulo unification).
wenzelm@47498
   878
wenzelm@61657
   879
  Argument positions may be effectively skipped by using ``\<open>_\<close>'' (underscore),
wenzelm@61657
   880
  which refers to the propositional identity rule in the Pure theory.
wenzelm@60483
   881
wenzelm@61657
   882
  \<^descr> @{attribute of}~\<open>t\<^sub>1 \<dots> t\<^sub>n\<close> performs positional instantiation of term
wenzelm@61657
   883
  variables. The terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> are substituted for any schematic
wenzelm@61657
   884
  variables occurring in a theorem from left to right; ``\<open>_\<close>'' (underscore)
wenzelm@61657
   885
  indicates to skip a position. Arguments following a ``\<open>concl:\<close>''
wenzelm@61657
   886
  specification refer to positions of the conclusion of a rule.
wenzelm@55143
   887
wenzelm@61657
   888
  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified:
wenzelm@61657
   889
  the instantiated theorem is exported, and these variables become schematic
wenzelm@61657
   890
  (usually with some shifting of indices).
wenzelm@60483
   891
wenzelm@61657
   892
  \<^descr> @{attribute "where"}~\<open>x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n\<close> performs named
wenzelm@61657
   893
  instantiation of schematic type and term variables occurring in a theorem.
wenzelm@61657
   894
  Schematic variables have to be specified on the left-hand side (e.g.\
wenzelm@61657
   895
  \<open>?x1.3\<close>). The question mark may be omitted if the variable name is a plain
wenzelm@61657
   896
  identifier without index. As type instantiations are inferred from term
wenzelm@61657
   897
  instantiations, explicit type instantiations are seldom necessary.
wenzelm@26870
   898
wenzelm@61657
   899
  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified
wenzelm@61657
   900
  as for @{attribute "of"} above.
wenzelm@58618
   901
\<close>
wenzelm@26870
   902
wenzelm@26870
   903
wenzelm@58618
   904
subsection \<open>Defining proof methods\<close>
wenzelm@28757
   905
wenzelm@58618
   906
text \<open>
wenzelm@28757
   907
  \begin{matharray}{rcl}
wenzelm@61493
   908
    @{command_def "method_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
wenzelm@28757
   909
  \end{matharray}
wenzelm@28757
   910
wenzelm@55112
   911
  @{rail \<open>
wenzelm@59783
   912
    @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
wenzelm@55112
   913
  \<close>}
wenzelm@28757
   914
wenzelm@61657
   915
  \<^descr> @{command "method_setup"}~\<open>name = text description\<close> defines a proof method
wenzelm@61657
   916
  in the current context. The given \<open>text\<close> has to be an ML expression of type
wenzelm@61657
   917
  @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\ basic
wenzelm@61657
   918
  parsers defined in structure @{ML_structure Args} and @{ML_structure
wenzelm@61657
   919
  Attrib}. There are also combinators like @{ML METHOD} and @{ML
wenzelm@61657
   920
  SIMPLE_METHOD} to turn certain tactic forms into official proof methods; the
wenzelm@61657
   921
  primed versions refer to tactics with explicit goal addressing.
wenzelm@28757
   922
wenzelm@30547
   923
  Here are some example method definitions:
wenzelm@58618
   924
\<close>
wenzelm@28757
   925
wenzelm@59905
   926
(*<*)experiment begin(*>*)
wenzelm@58619
   927
  method_setup my_method1 =
wenzelm@58619
   928
    \<open>Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))\<close>
wenzelm@58619
   929
    "my first method (without any arguments)"
wenzelm@30547
   930
wenzelm@58619
   931
  method_setup my_method2 =
wenzelm@58619
   932
    \<open>Scan.succeed (fn ctxt: Proof.context =>
wenzelm@58619
   933
      SIMPLE_METHOD' (fn i: int => no_tac))\<close>
wenzelm@58619
   934
    "my second method (with context)"
wenzelm@30547
   935
wenzelm@58619
   936
  method_setup my_method3 =
wenzelm@58619
   937
    \<open>Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
wenzelm@58619
   938
      SIMPLE_METHOD' (fn i: int => no_tac))\<close>
wenzelm@58619
   939
    "my third method (with theorem arguments and context)"
wenzelm@59905
   940
(*<*)end(*>*)
wenzelm@30547
   941
wenzelm@28757
   942
wenzelm@60483
   943
section \<open>Proof by cases and induction \label{sec:cases-induct}\<close>
wenzelm@60483
   944
wenzelm@60483
   945
subsection \<open>Rule contexts\<close>
wenzelm@60483
   946
wenzelm@60483
   947
text \<open>
wenzelm@60483
   948
  \begin{matharray}{rcl}
wenzelm@61493
   949
    @{command_def "case"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
   950
    @{command_def "print_cases"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   951
    @{attribute_def case_names} & : & \<open>attribute\<close> \\
wenzelm@61493
   952
    @{attribute_def case_conclusion} & : & \<open>attribute\<close> \\
wenzelm@61493
   953
    @{attribute_def params} & : & \<open>attribute\<close> \\
wenzelm@61493
   954
    @{attribute_def consumes} & : & \<open>attribute\<close> \\
wenzelm@60483
   955
  \end{matharray}
wenzelm@60483
   956
wenzelm@61657
   957
  The puristic way to build up Isar proof contexts is by explicit language
wenzelm@61657
   958
  elements like @{command "fix"}, @{command "assume"}, @{command "let"} (see
wenzelm@61657
   959
  \secref{sec:proof-context}). This is adequate for plain natural deduction,
wenzelm@61657
   960
  but easily becomes unwieldy in concrete verification tasks, which typically
wenzelm@61657
   961
  involve big induction rules with several cases.
wenzelm@60483
   962
wenzelm@61657
   963
  The @{command "case"} command provides a shorthand to refer to a local
wenzelm@61657
   964
  context symbolically: certain proof methods provide an environment of named
wenzelm@61657
   965
  ``cases'' of the form \<open>c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n\<close>; the effect of
wenzelm@61657
   966
  ``@{command "case"}~\<open>c\<close>'' is then equivalent to ``@{command "fix"}~\<open>x\<^sub>1 \<dots>
wenzelm@61657
   967
  x\<^sub>m\<close>~@{command "assume"}~\<open>c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Term bindings may be covered as
wenzelm@61657
   968
  well, notably @{variable ?case} for the main conclusion.
wenzelm@60483
   969
wenzelm@61657
   970
  By default, the ``terminology'' \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of a case value is marked as
wenzelm@61657
   971
  hidden, i.e.\ there is no way to refer to such parameters in the subsequent
wenzelm@61657
   972
  proof text. After all, original rule parameters stem from somewhere outside
wenzelm@61657
   973
  of the current proof text. By using the explicit form ``@{command
wenzelm@61657
   974
  "case"}~\<open>(c y\<^sub>1 \<dots> y\<^sub>m)\<close>'' instead, the proof author is able to chose local
wenzelm@61657
   975
  names that fit nicely into the current context.
wenzelm@60483
   976
wenzelm@61421
   977
  \<^medskip>
wenzelm@61657
   978
  It is important to note that proper use of @{command "case"} does not
wenzelm@61657
   979
  provide means to peek at the current goal state, which is not directly
wenzelm@61657
   980
  observable in Isar! Nonetheless, goal refinement commands do provide named
wenzelm@61657
   981
  cases \<open>goal\<^sub>i\<close> for each subgoal \<open>i = 1, \<dots>, n\<close> of the resulting goal state.
wenzelm@61657
   982
  Using this extra feature requires great care, because some bits of the
wenzelm@61657
   983
  internal tactical machinery intrude the proof text. In particular, parameter
wenzelm@61657
   984
  names stemming from the left-over of automated reasoning tools are usually
wenzelm@61657
   985
  quite unpredictable.
wenzelm@60483
   986
wenzelm@60483
   987
  Under normal circumstances, the text of cases emerge from standard
wenzelm@61657
   988
  elimination or induction rules, which in turn are derived from previous
wenzelm@61657
   989
  theory specifications in a canonical way (say from @{command "inductive"}
wenzelm@61657
   990
  definitions).
wenzelm@60483
   991
wenzelm@61421
   992
  \<^medskip>
wenzelm@61657
   993
  Proper cases are only available if both the proof method and the rules
wenzelm@61657
   994
  involved support this. By using appropriate attributes, case names,
wenzelm@61657
   995
  conclusions, and parameters may be also declared by hand. Thus variant
wenzelm@61657
   996
  versions of rules that have been derived manually become ready to use in
wenzelm@61657
   997
  advanced case analysis later.
wenzelm@60483
   998
wenzelm@60483
   999
  @{rail \<open>
wenzelm@62969
  1000
    @@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')')
wenzelm@60483
  1001
    ;
wenzelm@63019
  1002
    @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) *) ']' ) ? ) +)
wenzelm@60483
  1003
    ;
wenzelm@60483
  1004
    @@{attribute case_conclusion} @{syntax name} (@{syntax name} * )
wenzelm@60483
  1005
    ;
wenzelm@60483
  1006
    @@{attribute params} ((@{syntax name} * ) + @'and')
wenzelm@60483
  1007
    ;
wenzelm@60483
  1008
    @@{attribute consumes} @{syntax int}?
wenzelm@60483
  1009
  \<close>}
wenzelm@60483
  1010
wenzelm@61657
  1011
  \<^descr> @{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close> invokes a named local context \<open>c:
wenzelm@61657
  1012
  x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m\<close>, as provided by an appropriate proof method (such
wenzelm@61657
  1013
  as @{method_ref cases} and @{method_ref induct}). The command ``@{command
wenzelm@61657
  1014
  "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>'' abbreviates ``@{command "fix"}~\<open>x\<^sub>1 \<dots>
wenzelm@61657
  1015
  x\<^sub>m\<close>~@{command "assume"}~\<open>a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Each local fact is qualified by
wenzelm@61657
  1016
  the prefix \<open>a\<close>, and all such facts are collectively bound to the name \<open>a\<close>.
wenzelm@60565
  1017
wenzelm@61657
  1018
  The fact name is specification \<open>a\<close> is optional, the default is to re-use
wenzelm@61657
  1019
  \<open>c\<close>. So @{command "case"}~\<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> is the same as @{command
wenzelm@61657
  1020
  "case"}~\<open>c: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>.
wenzelm@60483
  1021
wenzelm@61657
  1022
  \<^descr> @{command "print_cases"} prints all local contexts of the current state,
wenzelm@61657
  1023
  using Isar proof language notation.
wenzelm@61657
  1024
wenzelm@61657
  1025
  \<^descr> @{attribute case_names}~\<open>c\<^sub>1 \<dots> c\<^sub>k\<close> declares names for the local contexts
wenzelm@61657
  1026
  of premises of a theorem; \<open>c\<^sub>1, \<dots>, c\<^sub>k\<close> refers to the \<^emph>\<open>prefix\<close> of the list
wenzelm@61657
  1027
  of premises. Each of the cases \<open>c\<^sub>i\<close> can be of the form \<open>c[h\<^sub>1 \<dots> h\<^sub>n]\<close> where
wenzelm@61657
  1028
  the \<open>h\<^sub>1 \<dots> h\<^sub>n\<close> are the names of the hypotheses in case \<open>c\<^sub>i\<close> from left to
wenzelm@61657
  1029
  right.
wenzelm@60483
  1030
wenzelm@61657
  1031
  \<^descr> @{attribute case_conclusion}~\<open>c d\<^sub>1 \<dots> d\<^sub>k\<close> declares names for the
wenzelm@61657
  1032
  conclusions of a named premise \<open>c\<close>; here \<open>d\<^sub>1, \<dots>, d\<^sub>k\<close> refers to the prefix
wenzelm@61657
  1033
  of arguments of a logical formula built by nesting a binary connective
wenzelm@61657
  1034
  (e.g.\ \<open>\<or>\<close>).
wenzelm@60483
  1035
wenzelm@61657
  1036
  Note that proof methods such as @{method induct} and @{method coinduct}
wenzelm@61657
  1037
  already provide a default name for the conclusion as a whole. The need to
wenzelm@61657
  1038
  name subformulas only arises with cases that split into several sub-cases,
wenzelm@61657
  1039
  as in common co-induction rules.
wenzelm@60483
  1040
wenzelm@61657
  1041
  \<^descr> @{attribute params}~\<open>p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n\<close> renames the innermost
wenzelm@61657
  1042
  parameters of premises \<open>1, \<dots>, n\<close> of some theorem. An empty list of names may
wenzelm@61657
  1043
  be given to skip positions, leaving the present parameters unchanged.
wenzelm@60483
  1044
wenzelm@61657
  1045
  Note that the default usage of case rules does \<^emph>\<open>not\<close> directly expose
wenzelm@61657
  1046
  parameters to the proof context.
wenzelm@60483
  1047
wenzelm@61657
  1048
  \<^descr> @{attribute consumes}~\<open>n\<close> declares the number of ``major premises'' of a
wenzelm@61657
  1049
  rule, i.e.\ the number of facts to be consumed when it is applied by an
wenzelm@61657
  1050
  appropriate proof method. The default value of @{attribute consumes} is \<open>n =
wenzelm@61657
  1051
  1\<close>, which is appropriate for the usual kind of cases and induction rules for
wenzelm@61657
  1052
  inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any
wenzelm@61657
  1053
  @{attribute consumes} declaration given are treated as if @{attribute
wenzelm@61493
  1054
  consumes}~\<open>0\<close> had been specified.
wenzelm@60483
  1055
wenzelm@61657
  1056
  A negative \<open>n\<close> is interpreted relatively to the total number of premises of
wenzelm@61657
  1057
  the rule in the target context. Thus its absolute value specifies the
wenzelm@61657
  1058
  remaining number of premises, after subtracting the prefix of major premises
wenzelm@61657
  1059
  as indicated above. This form of declaration has the technical advantage of
wenzelm@61657
  1060
  being stable under more morphisms, notably those that export the result from
wenzelm@61657
  1061
  a nested @{command_ref context} with additional assumptions.
wenzelm@60483
  1062
wenzelm@61657
  1063
  Note that explicit @{attribute consumes} declarations are only rarely
wenzelm@61657
  1064
  needed; this is already taken care of automatically by the higher-level
wenzelm@61657
  1065
  @{attribute cases}, @{attribute induct}, and @{attribute coinduct}
wenzelm@61657
  1066
  declarations.
wenzelm@60483
  1067
\<close>
wenzelm@60483
  1068
wenzelm@60483
  1069
wenzelm@60483
  1070
subsection \<open>Proof methods\<close>
wenzelm@60483
  1071
wenzelm@60483
  1072
text \<open>
wenzelm@60483
  1073
  \begin{matharray}{rcl}
wenzelm@61493
  1074
    @{method_def cases} & : & \<open>method\<close> \\
wenzelm@61493
  1075
    @{method_def induct} & : & \<open>method\<close> \\
wenzelm@61493
  1076
    @{method_def induction} & : & \<open>method\<close> \\
wenzelm@61493
  1077
    @{method_def coinduct} & : & \<open>method\<close> \\
wenzelm@60483
  1078
  \end{matharray}
wenzelm@60483
  1079
wenzelm@61657
  1080
  The @{method cases}, @{method induct}, @{method induction}, and @{method
wenzelm@61657
  1081
  coinduct} methods provide a uniform interface to common proof techniques
wenzelm@61657
  1082
  over datatypes, inductive predicates (or sets), recursive functions etc. The
wenzelm@61657
  1083
  corresponding rules may be specified and instantiated in a casual manner.
wenzelm@61657
  1084
  Furthermore, these methods provide named local contexts that may be invoked
wenzelm@61657
  1085
  via the @{command "case"} proof command within the subsequent proof text.
wenzelm@61657
  1086
  This accommodates compact proof texts even when reasoning about large
wenzelm@61657
  1087
  specifications.
wenzelm@60483
  1088
wenzelm@61657
  1089
  The @{method induct} method also provides some additional infrastructure in
wenzelm@61657
  1090
  order to be applicable to structure statements (either using explicit
wenzelm@61657
  1091
  meta-level connectives, or including facts and parameters separately). This
wenzelm@61657
  1092
  avoids cumbersome encoding of ``strengthened'' inductive statements within
wenzelm@61657
  1093
  the object-logic.
wenzelm@60483
  1094
wenzelm@61657
  1095
  Method @{method induction} differs from @{method induct} only in the names
wenzelm@61657
  1096
  of the facts in the local context invoked by the @{command "case"} command.
wenzelm@60483
  1097
wenzelm@60483
  1098
  @{rail \<open>
wenzelm@60483
  1099
    @@{method cases} ('(' 'no_simp' ')')? \<newline>
wenzelm@60483
  1100
      (@{syntax insts} * @'and') rule?
wenzelm@60483
  1101
    ;
wenzelm@60483
  1102
    (@@{method induct} | @@{method induction})
wenzelm@60483
  1103
      ('(' 'no_simp' ')')? (definsts * @'and') \<newline> arbitrary? taking? rule?
wenzelm@60483
  1104
    ;
wenzelm@60483
  1105
    @@{method coinduct} @{syntax insts} taking rule?
wenzelm@60483
  1106
    ;
wenzelm@60483
  1107
wenzelm@62969
  1108
    rule: ('type' | 'pred' | 'set') ':' (@{syntax name} +) | 'rule' ':' (@{syntax thm} +)
wenzelm@60483
  1109
    ;
wenzelm@60483
  1110
    definst: @{syntax name} ('==' | '\<equiv>') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst}
wenzelm@60483
  1111
    ;
wenzelm@60483
  1112
    definsts: ( definst * )
wenzelm@60483
  1113
    ;
wenzelm@60483
  1114
    arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)
wenzelm@60483
  1115
    ;
wenzelm@60483
  1116
    taking: 'taking' ':' @{syntax insts}
wenzelm@60483
  1117
  \<close>}
wenzelm@60483
  1118
wenzelm@61657
  1119
  \<^descr> @{method cases}~\<open>insts R\<close> applies method @{method rule} with an
wenzelm@61657
  1120
  appropriate case distinction theorem, instantiated to the subjects \<open>insts\<close>.
wenzelm@61657
  1121
  Symbolic case names are bound according to the rule's local contexts.
wenzelm@60483
  1122
wenzelm@61657
  1123
  The rule is determined as follows, according to the facts and arguments
wenzelm@61657
  1124
  passed to the @{method cases} method:
wenzelm@60483
  1125
wenzelm@61421
  1126
  \<^medskip>
wenzelm@60483
  1127
  \begin{tabular}{llll}
wenzelm@60483
  1128
    facts           &                 & arguments   & rule \\\hline
wenzelm@61493
  1129
    \<open>\<turnstile> R\<close>   & @{method cases} &             & implicit rule \<open>R\<close> \\
wenzelm@60483
  1130
                    & @{method cases} &             & classical case split \\
wenzelm@61493
  1131
                    & @{method cases} & \<open>t\<close>   & datatype exhaustion (type of \<open>t\<close>) \\
wenzelm@61493
  1132
    \<open>\<turnstile> A t\<close> & @{method cases} & \<open>\<dots>\<close> & inductive predicate/set elimination (of \<open>A\<close>) \\
wenzelm@61493
  1133
    \<open>\<dots>\<close>     & @{method cases} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\
wenzelm@60483
  1134
  \end{tabular}
wenzelm@61421
  1135
  \<^medskip>
wenzelm@60483
  1136
wenzelm@61657
  1137
  Several instantiations may be given, referring to the \<^emph>\<open>suffix\<close> of premises
wenzelm@61657
  1138
  of the case rule; within each premise, the \<^emph>\<open>prefix\<close> of variables is
wenzelm@61657
  1139
  instantiated. In most situations, only a single term needs to be specified;
wenzelm@61657
  1140
  this refers to the first variable of the last premise (it is usually the
wenzelm@61657
  1141
  same for all cases). The \<open>(no_simp)\<close> option can be used to disable
wenzelm@61657
  1142
  pre-simplification of cases (see the description of @{method induct} below
wenzelm@61657
  1143
  for details).
wenzelm@60483
  1144
wenzelm@61657
  1145
  \<^descr> @{method induct}~\<open>insts R\<close> and @{method induction}~\<open>insts R\<close> are analogous
wenzelm@61657
  1146
  to the @{method cases} method, but refer to induction rules, which are
wenzelm@60483
  1147
  determined as follows:
wenzelm@60483
  1148
wenzelm@61421
  1149
  \<^medskip>
wenzelm@60483
  1150
  \begin{tabular}{llll}
wenzelm@60483
  1151
    facts           &                  & arguments            & rule \\\hline
wenzelm@61493
  1152
                    & @{method induct} & \<open>P x\<close>        & datatype induction (type of \<open>x\<close>) \\
wenzelm@61493
  1153
    \<open>\<turnstile> A x\<close> & @{method induct} & \<open>\<dots>\<close>          & predicate/set induction (of \<open>A\<close>) \\
wenzelm@61493
  1154
    \<open>\<dots>\<close>     & @{method induct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\
wenzelm@60483
  1155
  \end{tabular}
wenzelm@61421
  1156
  \<^medskip>
wenzelm@60483
  1157
wenzelm@61657
  1158
  Several instantiations may be given, each referring to some part of a mutual
wenzelm@61657
  1159
  inductive definition or datatype --- only related partial induction rules
wenzelm@61657
  1160
  may be used together, though. Any of the lists of terms \<open>P, x, \<dots>\<close> refers to
wenzelm@61657
  1161
  the \<^emph>\<open>suffix\<close> of variables present in the induction rule. This enables the
wenzelm@61657
  1162
  writer to specify only induction variables, or both predicates and
wenzelm@61657
  1163
  variables, for example.
wenzelm@60483
  1164
wenzelm@61657
  1165
  Instantiations may be definitional: equations \<open>x \<equiv> t\<close> introduce local
wenzelm@61657
  1166
  definitions, which are inserted into the claim and discharged after applying
wenzelm@61657
  1167
  the induction rule. Equalities reappear in the inductive cases, but have
wenzelm@61657
  1168
  been transformed according to the induction principle being involved here.
wenzelm@61657
  1169
  In order to achieve practically useful induction hypotheses, some variables
wenzelm@61657
  1170
  occurring in \<open>t\<close> need to be fixed (see below). Instantiations of the form
wenzelm@61657
  1171
  \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a shorthand for \<open>x \<equiv> t\<close>,
wenzelm@61657
  1172
  where \<open>x\<close> is a fresh variable. If this is not intended, \<open>t\<close> has to be
wenzelm@61657
  1173
  enclosed in parentheses. By default, the equalities generated by
wenzelm@61657
  1174
  definitional instantiations are pre-simplified using a specific set of
wenzelm@61657
  1175
  rules, usually consisting of distinctness and injectivity theorems for
wenzelm@61657
  1176
  datatypes. This pre-simplification may cause some of the parameters of an
wenzelm@61657
  1177
  inductive case to disappear, or may even completely delete some of the
wenzelm@61657
  1178
  inductive cases, if one of the equalities occurring in their premises can be
wenzelm@61657
  1179
  simplified to \<open>False\<close>. The \<open>(no_simp)\<close> option can be used to disable
wenzelm@61657
  1180
  pre-simplification. Additional rules to be used in pre-simplification can be
wenzelm@61657
  1181
  declared using the @{attribute_def induct_simp} attribute.
wenzelm@60483
  1182
wenzelm@61657
  1183
  The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>'' specification generalizes variables
wenzelm@61657
  1184
  \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. One can
wenzelm@61657
  1185
  separate variables by ``\<open>and\<close>'' to generalize them in other goals then the
wenzelm@61657
  1186
  first. Thus induction hypotheses may become sufficiently general to get the
wenzelm@61657
  1187
  proof through. Together with definitional instantiations, one may
wenzelm@61657
  1188
  effectively perform induction over expressions of a certain structure.
wenzelm@60483
  1189
wenzelm@61657
  1190
  The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification provides additional
wenzelm@61657
  1191
  instantiations of a prefix of pending variables in the rule. Such schematic
wenzelm@61657
  1192
  induction rules rarely occur in practice, though.
wenzelm@60483
  1193
wenzelm@61657
  1194
  \<^descr> @{method coinduct}~\<open>inst R\<close> is analogous to the @{method induct} method,
wenzelm@61657
  1195
  but refers to coinduction rules, which are determined as follows:
wenzelm@60483
  1196
wenzelm@61421
  1197
  \<^medskip>
wenzelm@60483
  1198
  \begin{tabular}{llll}
wenzelm@60483
  1199
    goal          &                    & arguments & rule \\\hline
wenzelm@61493
  1200
                  & @{method coinduct} & \<open>x\<close> & type coinduction (type of \<open>x\<close>) \\
wenzelm@61493
  1201
    \<open>A x\<close> & @{method coinduct} & \<open>\<dots>\<close> & predicate/set coinduction (of \<open>A\<close>) \\
wenzelm@61493
  1202
    \<open>\<dots>\<close>   & @{method coinduct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\
wenzelm@60483
  1203
  \end{tabular}
wenzelm@61421
  1204
  \<^medskip>
wenzelm@60483
  1205
wenzelm@61657
  1206
  Coinduction is the dual of induction. Induction essentially eliminates \<open>A x\<close>
wenzelm@61657
  1207
  towards a generic result \<open>P x\<close>, while coinduction introduces \<open>A x\<close> starting
wenzelm@61657
  1208
  with \<open>B x\<close>, for a suitable ``bisimulation'' \<open>B\<close>. The cases of a coinduct
wenzelm@61657
  1209
  rule are typically named after the predicates or sets being covered, while
wenzelm@61657
  1210
  the conclusions consist of several alternatives being named after the
wenzelm@61657
  1211
  individual destructor patterns.
wenzelm@60483
  1212
wenzelm@61657
  1213
  The given instantiation refers to the \<^emph>\<open>suffix\<close> of variables occurring in
wenzelm@61657
  1214
  the rule's major premise, or conclusion if unavailable. An additional
wenzelm@61657
  1215
  ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification may be required in order to specify
wenzelm@61657
  1216
  the bisimulation to be used in the coinduction step.
wenzelm@60483
  1217
wenzelm@60483
  1218
wenzelm@60483
  1219
  Above methods produce named local contexts, as determined by the
wenzelm@61657
  1220
  instantiated rule as given in the text. Beyond that, the @{method induct}
wenzelm@61657
  1221
  and @{method coinduct} methods guess further instantiations from the goal
wenzelm@61657
  1222
  specification itself. Any persisting unresolved schematic variables of the
wenzelm@61657
  1223
  resulting rule will render the the corresponding case invalid. The term
wenzelm@61657
  1224
  binding @{variable ?case} for the conclusion will be provided with each
wenzelm@61657
  1225
  case, provided that term is fully specified.
wenzelm@60483
  1226
wenzelm@61657
  1227
  The @{command "print_cases"} command prints all named cases present in the
wenzelm@61657
  1228
  current proof state.
wenzelm@60483
  1229
wenzelm@61421
  1230
  \<^medskip>
wenzelm@61657
  1231
  Despite the additional infrastructure, both @{method cases} and @{method
wenzelm@61657
  1232
  coinduct} merely apply a certain rule, after instantiation, while conforming
wenzelm@61657
  1233
  due to the usual way of monotonic natural deduction: the context of a
wenzelm@61657
  1234
  structured statement \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>\<close> reappears unchanged after
wenzelm@61657
  1235
  the case split.
wenzelm@60483
  1236
wenzelm@61657
  1237
  The @{method induct} method is fundamentally different in this respect: the
wenzelm@61657
  1238
  meta-level structure is passed through the ``recursive'' course involved in
wenzelm@61657
  1239
  the induction. Thus the original statement is basically replaced by separate
wenzelm@61657
  1240
  copies, corresponding to the induction hypotheses and conclusion; the
wenzelm@61657
  1241
  original goal context is no longer available. Thus local assumptions, fixed
wenzelm@61657
  1242
  parameters and definitions effectively participate in the inductive
wenzelm@61657
  1243
  rephrasing of the original statement.
wenzelm@60483
  1244
wenzelm@60483
  1245
  In @{method induct} proofs, local assumptions introduced by cases are split
wenzelm@61657
  1246
  into two different kinds: \<open>hyps\<close> stemming from the rule and \<open>prems\<close> from the
wenzelm@61657
  1247
  goal statement. This is reflected in the extracted cases accordingly, so
wenzelm@61657
  1248
  invoking ``@{command "case"}~\<open>c\<close>'' will provide separate facts \<open>c.hyps\<close> and
wenzelm@61657
  1249
  \<open>c.prems\<close>, as well as fact \<open>c\<close> to hold the all-inclusive list.
wenzelm@60483
  1250
wenzelm@60483
  1251
  In @{method induction} proofs, local assumptions introduced by cases are
wenzelm@61657
  1252
  split into three different kinds: \<open>IH\<close>, the induction hypotheses, \<open>hyps\<close>,
wenzelm@61657
  1253
  the remaining hypotheses stemming from the rule, and \<open>prems\<close>, the
wenzelm@61657
  1254
  assumptions from the goal statement. The names are \<open>c.IH\<close>, \<open>c.hyps\<close> and
wenzelm@61657
  1255
  \<open>c.prems\<close>, as above.
wenzelm@60483
  1256
wenzelm@61421
  1257
  \<^medskip>
wenzelm@61657
  1258
  Facts presented to either method are consumed according to the number of
wenzelm@61657
  1259
  ``major premises'' of the rule involved, which is usually 0 for plain cases
wenzelm@61657
  1260
  and induction rules of datatypes etc.\ and 1 for rules of inductive
wenzelm@61657
  1261
  predicates or sets and the like. The remaining facts are inserted into the
wenzelm@61657
  1262
  goal verbatim before the actual \<open>cases\<close>, \<open>induct\<close>, or \<open>coinduct\<close> rule is
wenzelm@60483
  1263
  applied.
wenzelm@60483
  1264
\<close>
wenzelm@60483
  1265
wenzelm@60483
  1266
wenzelm@60483
  1267
subsection \<open>Declaring rules\<close>
wenzelm@60483
  1268
wenzelm@60483
  1269
text \<open>
wenzelm@60483
  1270
  \begin{matharray}{rcl}
wenzelm@61493
  1271
    @{command_def "print_induct_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
  1272
    @{attribute_def cases} & : & \<open>attribute\<close> \\
wenzelm@61493
  1273
    @{attribute_def induct} & : & \<open>attribute\<close> \\
wenzelm@61493
  1274
    @{attribute_def coinduct} & : & \<open>attribute\<close> \\
wenzelm@60483
  1275
  \end{matharray}
wenzelm@60483
  1276
wenzelm@60483
  1277
  @{rail \<open>
wenzelm@60483
  1278
    @@{attribute cases} spec
wenzelm@60483
  1279
    ;
wenzelm@60483
  1280
    @@{attribute induct} spec
wenzelm@60483
  1281
    ;
wenzelm@60483
  1282
    @@{attribute coinduct} spec
wenzelm@60483
  1283
    ;
wenzelm@60483
  1284
wenzelm@62969
  1285
    spec: (('type' | 'pred' | 'set') ':' @{syntax name}) | 'del'
wenzelm@60483
  1286
  \<close>}
wenzelm@60483
  1287
wenzelm@61657
  1288
  \<^descr> @{command "print_induct_rules"} prints cases and induct rules for
wenzelm@61657
  1289
  predicates (or sets) and types of the current context.
wenzelm@60483
  1290
wenzelm@61657
  1291
  \<^descr> @{attribute cases}, @{attribute induct}, and @{attribute coinduct} (as
wenzelm@61657
  1292
  attributes) declare rules for reasoning about (co)inductive predicates (or
wenzelm@61657
  1293
  sets) and types, using the corresponding methods of the same name. Certain
wenzelm@61657
  1294
  definitional packages of object-logics usually declare emerging cases and
wenzelm@60483
  1295
  induction rules as expected, so users rarely need to intervene.
wenzelm@60483
  1296
wenzelm@61657
  1297
  Rules may be deleted via the \<open>del\<close> specification, which covers all of the
wenzelm@61657
  1298
  \<open>type\<close>/\<open>pred\<close>/\<open>set\<close> sub-categories simultaneously. For example, @{attribute
wenzelm@61657
  1299
  cases}~\<open>del\<close> removes any @{attribute cases} rules declared for some type,
wenzelm@61657
  1300
  predicate, or set.
wenzelm@60483
  1301
wenzelm@61657
  1302
  Manual rule declarations usually refer to the @{attribute case_names} and
wenzelm@61657
  1303
  @{attribute params} attributes to adjust names of cases and parameters of a
wenzelm@61657
  1304
  rule; the @{attribute consumes} declaration is taken care of automatically:
wenzelm@61657
  1305
  @{attribute consumes}~\<open>0\<close> is specified for ``type'' rules and @{attribute
wenzelm@61493
  1306
  consumes}~\<open>1\<close> for ``predicate'' / ``set'' rules.
wenzelm@60483
  1307
\<close>
wenzelm@60483
  1308
wenzelm@60483
  1309
wenzelm@60459
  1310
section \<open>Generalized elimination and case splitting \label{sec:obtain}\<close>
wenzelm@26870
  1311
wenzelm@58618
  1312
text \<open>
wenzelm@26870
  1313
  \begin{matharray}{rcl}
wenzelm@61493
  1314
    @{command_def "consider"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
  1315
    @{command_def "obtain"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
  1316
    @{command_def "guess"}\<open>\<^sup>*\<close> & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
wenzelm@26870
  1317
  \end{matharray}
wenzelm@26870
  1318
wenzelm@61657
  1319
  Generalized elimination means that hypothetical parameters and premises may
wenzelm@61657
  1320
  be introduced in the current context, potentially with a split into cases.
wenzelm@61657
  1321
  This works by virtue of a locally proven rule that establishes the soundness
wenzelm@61657
  1322
  of this temporary context extension. As representative examples, one may
wenzelm@61657
  1323
  think of standard rules from Isabelle/HOL like this:
wenzelm@60459
  1324
wenzelm@61421
  1325
  \<^medskip>
wenzelm@60459
  1326
  \begin{tabular}{ll}
wenzelm@61493
  1327
  \<open>\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\
wenzelm@61493
  1328
  \<open>A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\
wenzelm@61493
  1329
  \<open>A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\
wenzelm@60459
  1330
  \end{tabular}
wenzelm@61421
  1331
  \<^medskip>
wenzelm@60459
  1332
wenzelm@60459
  1333
  In general, these particular rules and connectives need to get involved at
wenzelm@61657
  1334
  all: this concept works directly in Isabelle/Pure via Isar commands defined
wenzelm@61657
  1335
  below. In particular, the logic of elimination and case splitting is
wenzelm@61657
  1336
  delegated to an Isar proof, which often involves automated tools.
wenzelm@26870
  1337
wenzelm@55112
  1338
  @{rail \<open>
wenzelm@60459
  1339
    @@{command consider} @{syntax obtain_clauses}
wenzelm@60459
  1340
    ;
wenzelm@63285
  1341
    @@{command obtain} @{syntax par_name}? @{syntax vars} \<newline>
wenzelm@63059
  1342
      @'where' concl prems @{syntax for_fixes}
wenzelm@63059
  1343
    ;
wenzelm@63059
  1344
    concl: (@{syntax props} + @'and')
wenzelm@63059
  1345
    ;
wenzelm@63059
  1346
    prems: (@'if' (@{syntax props'} + @'and'))?
wenzelm@26870
  1347
    ;
wenzelm@63285
  1348
    @@{command guess} @{syntax vars}
wenzelm@55112
  1349
  \<close>}
wenzelm@26870
  1350
wenzelm@61657
  1351
  \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)
wenzelm@61657
  1352
  \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case splitting
wenzelm@61657
  1353
  into separate subgoals, such that each case involves new parameters and
wenzelm@61657
  1354
  premises. After the proof is finished, the resulting rule may be used
wenzelm@61657
  1355
  directly with the @{method cases} proof method (\secref{sec:cases-induct}),
wenzelm@61657
  1356
  in order to perform actual case-splitting of the proof text via @{command
wenzelm@61657
  1357
  case} and @{command next} as usual.
wenzelm@60459
  1358
wenzelm@61657
  1359
  Optional names in round parentheses refer to case names: in the proof of the
wenzelm@61657
  1360
  rule this is a fact name, in the resulting rule it is used as annotation
wenzelm@61657
  1361
  with the @{attribute_ref case_names} attribute.
wenzelm@60459
  1362
wenzelm@61421
  1363
  \<^medskip>
wenzelm@61657
  1364
  Formally, the command @{command consider} is defined as derived Isar
wenzelm@61657
  1365
  language element as follows:
wenzelm@60459
  1366
wenzelm@26870
  1367
  \begin{matharray}{l}
wenzelm@61493
  1368
    @{command "consider"}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>\<close> \\[1ex]
wenzelm@61493
  1369
    \quad @{command "have"}~\<open>[case_names a b \<dots>]: thesis\<close> \\
wenzelm@61493
  1370
    \qquad \<open>\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\
wenzelm@61493
  1371
    \qquad \<open>\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis\<close> \\
wenzelm@61493
  1372
    \qquad \<open>\<AND> \<dots>\<close> \\
wenzelm@61493
  1373
    \qquad \<open>\<FOR> thesis\<close> \\
wenzelm@61493
  1374
    \qquad @{command "apply"}~\<open>(insert a b \<dots>)\<close> \\
wenzelm@26870
  1375
  \end{matharray}
wenzelm@26870
  1376
wenzelm@60459
  1377
  See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal
wenzelm@61657
  1378
  statements, as well as @{command print_statement} to print existing rules in
wenzelm@61657
  1379
  a similar format.
wenzelm@26870
  1380
wenzelm@61657
  1381
  \<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close> states a
wenzelm@61657
  1382
  generalized elimination rule with exactly one case. After the proof is
wenzelm@61657
  1383
  finished, it is activated for the subsequent proof text: the context is
wenzelm@61657
  1384
  augmented via @{command fix}~\<open>\<^vec>x\<close> @{command assume}~\<open>\<^vec>A
wenzelm@61657
  1385
  \<^vec>x\<close>, with special provisions to export later results by discharging
wenzelm@61657
  1386
  these assumptions again.
wenzelm@60459
  1387
wenzelm@60459
  1388
  Note that according to the parameter scopes within the elimination rule,
wenzelm@61657
  1389
  results \<^emph>\<open>must not\<close> refer to hypothetical parameters; otherwise the export
wenzelm@61657
  1390
  will fail! This restriction conforms to the usual manner of existential
wenzelm@61657
  1391
  reasoning in Natural Deduction.
wenzelm@60459
  1392
wenzelm@61421
  1393
  \<^medskip>
wenzelm@61657
  1394
  Formally, the command @{command obtain} is defined as derived Isar language
wenzelm@61657
  1395
  element as follows, using an instrumented variant of @{command assume}:
wenzelm@26870
  1396
wenzelm@60459
  1397
  \begin{matharray}{l}
wenzelm@61493
  1398
    @{command "obtain"}~\<open>\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>\<close> \\[1ex]
wenzelm@61493
  1399
    \quad @{command "have"}~\<open>thesis\<close> \\
wenzelm@61493
  1400
    \qquad \<open>\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\
wenzelm@61493
  1401
    \qquad \<open>\<FOR> thesis\<close> \\
wenzelm@61493
  1402
    \qquad @{command "apply"}~\<open>(insert that)\<close> \\
wenzelm@61493
  1403
    \qquad \<open>\<langle>proof\<rangle>\<close> \\
wenzelm@61493
  1404
    \quad @{command "fix"}~\<open>\<^vec>x\<close>~@{command "assume"}\<open>\<^sup>* a: \<^vec>A \<^vec>x\<close> \\
wenzelm@60459
  1405
  \end{matharray}
wenzelm@60459
  1406
wenzelm@61439
  1407
  \<^descr> @{command guess} is similar to @{command obtain}, but it derives the
wenzelm@60459
  1408
  obtained context elements from the course of tactical reasoning in the
wenzelm@60459
  1409
  proof. Thus it can considerably obscure the proof: it is classified as
wenzelm@61477
  1410
  \<^emph>\<open>improper\<close>.
wenzelm@26870
  1411
wenzelm@61493
  1412
  A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The
wenzelm@61657
  1413
  subsequent refinement steps may turn this to anything of the form
wenzelm@61657
  1414
  \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new
wenzelm@61657
  1415
  subgoals. The final goal state is then used as reduction rule for the obtain
wenzelm@61657
  1416
  pattern described above. Obtained parameters \<open>\<^vec>x\<close> are marked as
wenzelm@61657
  1417
  internal by default, and thus inaccessible in the proof text. The variable
wenzelm@61657
  1418
  names and type constraints given as arguments for @{command "guess"} specify
wenzelm@61657
  1419
  a prefix of accessible parameters.
wenzelm@26870
  1420
wenzelm@60459
  1421
wenzelm@61657
  1422
  In the proof of @{command consider} and @{command obtain} the local premises
wenzelm@61657
  1423
  are always bound to the fact name @{fact_ref that}, according to structured
wenzelm@61657
  1424
  Isar statements involving @{keyword_ref "if"} (\secref{sec:goals}).
wenzelm@60459
  1425
wenzelm@61657
  1426
  Facts that are established by @{command "obtain"} and @{command "guess"} may
wenzelm@61657
  1427
  not be polymorphic: any type-variables occurring here are fixed in the
wenzelm@61657
  1428
  present context. This is a natural consequence of the role of @{command fix}
wenzelm@61657
  1429
  and @{command assume} in these constructs.
wenzelm@58618
  1430
\<close>
wenzelm@26870
  1431
wenzelm@26869
  1432
end