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