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