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