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"}'' 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