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