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