src/Doc/IsarRef/Proof.thy
 author wenzelm Mon Nov 19 20:23:47 2012 +0100 (2012-11-19 ago) changeset 50126 3dec88149176 parent 50109 c13dc0b1841c child 50772 6973b3f41334 permissions -rw-r--r--
theorem status about oracles/futures is no longer printed by default;
renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;
     1 theory Proof

     2 imports Base Main

     3 begin

     4

     5 chapter {* Proofs \label{ch:proofs} *}

     6

     7 text {*

     8   Proof commands perform transitions of Isar/VM machine

     9   configurations, which are block-structured, consisting of a stack of

    10   nodes with three main components: logical proof context, current

    11   facts, and open goals.  Isar/VM transitions are typed according to

    12   the following three different modes of operation:

    13

    14   \begin{description}

    15

    16   \item @{text "proof(prove)"} means that a new goal has just been

    17   stated that is now to be \emph{proven}; the next command may refine

    18   it by some proof method, and enter a sub-proof to establish the

    19   actual result.

    20

    21   \item @{text "proof(state)"} is like a nested theory mode: the

    22   context may be augmented by \emph{stating} additional assumptions,

    23   intermediate results etc.

    24

    25   \item @{text "proof(chain)"} is intermediate between @{text

    26   "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\

    27   the contents of the special @{fact_ref this}'' register) have been

    28   just picked up in order to be used when refining the goal claimed

    29   next.

    30

    31   \end{description}

    32

    33   The proof mode indicator may be understood as an instruction to the

    34   writer, telling what kind of operation may be performed next.  The

    35   corresponding typings of proof commands restricts the shape of

    36   well-formed proof texts to particular command sequences.  So dynamic

    37   arrangements of commands eventually turn out as static texts of a

    38   certain structure.

    39

    40   \Appref{ap:refcard} gives a simplified grammar of the (extensible)

    41   language emerging that way from the different types of proof

    42   commands.  The main ideas of the overall Isar framework are

    43   explained in \chref{ch:isar-framework}.

    44 *}

    45

    46

    47 section {* Proof structure *}

    48

    49 subsection {* Formal notepad *}

    50

    51 text {*

    52   \begin{matharray}{rcl}

    53     @{command_def "notepad"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\

    54   \end{matharray}

    55

    56   @{rail "

    57     @@{command notepad} @'begin'

    58     ;

    59     @@{command end}

    60   "}

    61

    62   \begin{description}

    63

    64   \item @{command "notepad"}~@{keyword "begin"} opens a proof state

    65   without any goal statement.  This allows to experiment with Isar,

    66   without producing any persistent result.

    67

    68   The notepad can be closed by @{command "end"} or discontinued by

    69   @{command "oops"}.

    70

    71   \end{description}

    72 *}

    73

    74

    75 subsection {* Blocks *}

    76

    77 text {*

    78   \begin{matharray}{rcl}

    79     @{command_def "next"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

    80     @{command_def "{"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

    81     @{command_def "}"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

    82   \end{matharray}

    83

    84   While Isar is inherently block-structured, opening and closing

    85   blocks is mostly handled rather casually, with little explicit

    86   user-intervention.  Any local goal statement automatically opens

    87   \emph{two} internal blocks, which are closed again when concluding

    88   the sub-proof (by @{command "qed"} etc.).  Sections of different

    89   context within a sub-proof may be switched via @{command "next"},

    90   which is just a single block-close followed by block-open again.

    91   The effect of @{command "next"} is to reset the local proof context;

    92   there is no goal focus involved here!

    93

    94   For slightly more advanced applications, there are explicit block

    95   parentheses as well.  These typically achieve a stronger forward

    96   style of reasoning.

    97

    98   \begin{description}

    99

   100   \item @{command "next"} switches to a fresh block within a

   101   sub-proof, resetting the local context to the initial one.

   102

   103   \item @{command "{"} and @{command "}"} explicitly open and close

   104   blocks.  Any current facts pass through @{command "{"}''

   105   unchanged, while @{command "}"}'' causes any result to be

   106   \emph{exported} into the enclosing context.  Thus fixed variables

   107   are generalized, assumptions discharged, and local definitions

   108   unfolded (cf.\ \secref{sec:proof-context}).  There is no difference

   109   of @{command "assume"} and @{command "presume"} in this mode of

   110   forward reasoning --- in contrast to plain backward reasoning with

   111   the result exported at @{command "show"} time.

   112

   113   \end{description}

   114 *}

   115

   116

   117 subsection {* Omitting proofs *}

   118

   119 text {*

   120   \begin{matharray}{rcl}

   121     @{command_def "oops"} & : & @{text "proof \<rightarrow> local_theory | theory"} \\

   122   \end{matharray}

   123

   124   The @{command "oops"} command discontinues the current proof

   125   attempt, while considering the partial proof text as properly

   126   processed.  This is conceptually quite different from faking''

   127   actual proofs via @{command_ref "sorry"} (see

   128   \secref{sec:proof-steps}): @{command "oops"} does not observe the

   129   proof structure at all, but goes back right to the theory level.

   130   Furthermore, @{command "oops"} does not produce any result theorem

   131   --- there is no intended claim to be able to complete the proof

   132   in any way.

   133

   134   A typical application of @{command "oops"} is to explain Isar proofs

   135   \emph{within} the system itself, in conjunction with the document

   136   preparation tools of Isabelle described in \chref{ch:document-prep}.

   137   Thus partial or even wrong proof attempts can be discussed in a

   138   logically sound manner.  Note that the Isabelle {\LaTeX} macros can

   139   be easily adapted to print something like @{text "\<dots>"}'' instead of

   140   the keyword @{command "oops"}''.

   141 *}

   142

   143

   144 section {* Statements *}

   145

   146 subsection {* Context elements \label{sec:proof-context} *}

   147

   148 text {*

   149   \begin{matharray}{rcl}

   150     @{command_def "fix"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

   151     @{command_def "assume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

   152     @{command_def "presume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

   153     @{command_def "def"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

   154   \end{matharray}

   155

   156   The logical proof context consists of fixed variables and

   157   assumptions.  The former closely correspond to Skolem constants, or

   158   meta-level universal quantification as provided by the Isabelle/Pure

   159   logical framework.  Introducing some \emph{arbitrary, but fixed}

   160   variable via @{command "fix"}~@{text x}'' results in a local value

   161   that may be used in the subsequent proof as any other variable or

   162   constant.  Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from

   163   the context will be universally closed wrt.\ @{text x} at the

   164   outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal

   165   form using Isabelle's meta-variables).

   166

   167   Similarly, introducing some assumption @{text \<chi>} has two effects.

   168   On the one hand, a local theorem is created that may be used as a

   169   fact in subsequent proof steps.  On the other hand, any result

   170   @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\

   171   the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}.  Thus, solving an enclosing goal

   172   using such a result would basically introduce a new subgoal stemming

   173   from the assumption.  How this situation is handled depends on the

   174   version of assumption command used: while @{command "assume"}

   175   insists on solving the subgoal by unification with some premise of

   176   the goal, @{command "presume"} leaves the subgoal unchanged in order

   177   to be proved later by the user.

   178

   179   Local definitions, introduced by @{command "def"}~@{text "x \<equiv>

   180   t"}'', are achieved by combining @{command "fix"}~@{text x}'' with

   181   another version of assumption that causes any hypothetical equation

   182   @{text "x \<equiv> t"} to be eliminated by the reflexivity rule.  Thus,

   183   exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>

   184   \<phi>[t]"}.

   185

   186   @{rail "

   187     @@{command fix} (@{syntax vars} + @'and')

   188     ;

   189     (@@{command assume} | @@{command presume}) (@{syntax props} + @'and')

   190     ;

   191     @@{command def} (def + @'and')

   192     ;

   193     def: @{syntax thmdecl}? \\ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?

   194   "}

   195

   196   \begin{description}

   197

   198   \item @{command "fix"}~@{text x} introduces a local variable @{text

   199   x} that is \emph{arbitrary, but fixed.}

   200

   201   \item @{command "assume"}~@{text "a: \<phi>"} and @{command

   202   "presume"}~@{text "a: \<phi>"} introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by

   203   assumption.  Subsequent results applied to an enclosing goal (e.g.\

   204   by @{command_ref "show"}) are handled as follows: @{command

   205   "assume"} expects to be able to unify with existing premises in the

   206   goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.

   207

   208   Several lists of assumptions may be given (separated by

   209   @{keyword_ref "and"}; the resulting list of current facts consists

   210   of all of these concatenated.

   211

   212   \item @{command "def"}~@{text "x \<equiv> t"} introduces a local

   213   (non-polymorphic) definition.  In results exported from the context,

   214   @{text x} is replaced by @{text t}.  Basically, @{command

   215   "def"}~@{text "x \<equiv> t"}'' abbreviates @{command "fix"}~@{text

   216   x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting

   217   hypothetical equation solved by reflexivity.

   218

   219   The default name for the definitional equation is @{text x_def}.

   220   Several simultaneous definitions may be given at the same time.

   221

   222   \end{description}

   223

   224   The special name @{fact_ref prems} refers to all assumptions of the

   225   current context as a list of theorems.  This feature should be used

   226   with great care!  It is better avoided in final proof texts.

   227 *}

   228

   229

   230 subsection {* Term abbreviations \label{sec:term-abbrev} *}

   231

   232 text {*

   233   \begin{matharray}{rcl}

   234     @{command_def "let"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

   235     @{keyword_def "is"} & : & syntax \\

   236   \end{matharray}

   237

   238   Abbreviations may be either bound by explicit @{command

   239   "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or

   240   goal statements with a list of patterns @{text "(\<IS> p\<^sub>1 \<dots>

   241   p\<^sub>n)"}''.  In both cases, higher-order matching is invoked to

   242   bind extra-logical term variables, which may be either named

   243   schematic variables of the form @{text ?x}, or nameless dummies

   244   @{variable _}'' (underscore). Note that in the @{command "let"}

   245   form the patterns occur on the left-hand side, while the @{keyword

   246   "is"} patterns are in postfix position.

   247

   248   Polymorphism of term bindings is handled in Hindley-Milner style,

   249   similar to ML.  Type variables referring to local assumptions or

   250   open goal statements are \emph{fixed}, while those of finished

   251   results or bound by @{command "let"} may occur in \emph{arbitrary}

   252   instances later.  Even though actual polymorphism should be rarely

   253   used in practice, this mechanism is essential to achieve proper

   254   incremental type-inference, as the user proceeds to build up the

   255   Isar proof text from left to right.

   256

   257   \medskip Term abbreviations are quite different from local

   258   definitions as introduced via @{command "def"} (see

   259   \secref{sec:proof-context}).  The latter are visible within the

   260   logic as actual equations, while abbreviations disappear during the

   261   input process just after type checking.  Also note that @{command

   262   "def"} does not support polymorphism.

   263

   264   @{rail "

   265     @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')

   266   "}

   267

   268   The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or

   269   @{syntax prop_pat} (see \secref{sec:term-decls}).

   270

   271   \begin{description}

   272

   273   \item @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n"} binds any

   274   text variables in patterns @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous

   275   higher-order matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.

   276

   277   \item @{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"} resembles @{command "let"}, but

   278   matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the preceding statement.  Also

   279   note that @{keyword "is"} is not a separate command, but part of

   280   others (such as @{command "assume"}, @{command "have"} etc.).

   281

   282   \end{description}

   283

   284   Some \emph{implicit} term abbreviations\index{term abbreviations}

   285   for goals and facts are available as well.  For any open goal,

   286   @{variable_ref thesis} refers to its object-level statement,

   287   abstracted over any meta-level parameters (if present).  Likewise,

   288   @{variable_ref this} is bound for fact statements resulting from

   289   assumptions or finished goals.  In case @{variable this} refers to

   290   an object-logic statement that is an application @{text "f t"}, then

   291   @{text t} is bound to the special text variable @{variable "\<dots>"}''

   292   (three dots).  The canonical application of this convenience are

   293   calculational proofs (see \secref{sec:calculation}).

   294 *}

   295

   296

   297 subsection {* Facts and forward chaining \label{sec:proof-facts} *}

   298

   299 text {*

   300   \begin{matharray}{rcl}

   301     @{command_def "note"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

   302     @{command_def "then"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

   303     @{command_def "from"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

   304     @{command_def "with"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

   305     @{command_def "using"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\

   306     @{command_def "unfolding"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\

   307   \end{matharray}

   308

   309   New facts are established either by assumption or proof of local

   310   statements.  Any fact will usually be involved in further proofs,

   311   either as explicit arguments of proof methods, or when forward

   312   chaining towards the next goal via @{command "then"} (and variants);

   313   @{command "from"} and @{command "with"} are composite forms

   314   involving @{command "note"}.  The @{command "using"} elements

   315   augments the collection of used facts \emph{after} a goal has been

   316   stated.  Note that the special theorem name @{fact_ref this} refers

   317   to the most recently established facts, but only \emph{before}

   318   issuing a follow-up claim.

   319

   320   @{rail "

   321     @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')

   322     ;

   323     (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})

   324       (@{syntax thmrefs} + @'and')

   325   "}

   326

   327   \begin{description}

   328

   329   \item @{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} recalls existing facts

   330   @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}.  Note that

   331   attributes may be involved as well, both on the left and right hand

   332   sides.

   333

   334   \item @{command "then"} indicates forward chaining by the current

   335   facts in order to establish the goal to be claimed next.  The

   336   initial proof method invoked to refine that will be offered the

   337   facts to do anything appropriate'' (see also

   338   \secref{sec:proof-steps}).  For example, method @{method (Pure) rule}

   339   (see \secref{sec:pure-meth-att}) would typically do an elimination

   340   rather than an introduction.  Automatic methods usually insert the

   341   facts into the goal state before operation.  This provides a simple

   342   scheme to control relevance of facts in automated proof search.

   343

   344   \item @{command "from"}~@{text b} abbreviates @{command

   345   "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is

   346   equivalent to @{command "from"}~@{text this}''.

   347

   348   \item @{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} abbreviates @{command

   349   "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND> this"}''; thus the forward chaining

   350   is from earlier facts together with the current ones.

   351

   352   \item @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} augments the facts being

   353   currently indicated for use by a subsequent refinement step (such as

   354   @{command_ref "apply"} or @{command_ref "proof"}).

   355

   356   \item @{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is structurally

   357   similar to @{command "using"}, but unfolds definitional equations

   358   @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state and facts.

   359

   360   \end{description}

   361

   362   Forward chaining with an empty list of theorems is the same as not

   363   chaining at all.  Thus @{command "from"}~@{text nothing}'' has no

   364   effect apart from entering @{text "prove(chain)"} mode, since

   365   @{fact_ref nothing} is bound to the empty list of theorems.

   366

   367   Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple

   368   facts to be given in their proper order, corresponding to a prefix

   369   of the premises of the rule involved.  Note that positions may be

   370   easily skipped using something like @{command "from"}~@{text "_

   371   \<AND> a \<AND> b"}, for example.  This involves the trivial rule

   372   @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as

   373   @{fact_ref "_"}'' (underscore).

   374

   375   Automated methods (such as @{method simp} or @{method auto}) just

   376   insert any given facts before their usual operation.  Depending on

   377   the kind of procedure involved, the order of facts is less

   378   significant here.

   379 *}

   380

   381

   382 subsection {* Goals \label{sec:goals} *}

   383

   384 text {*

   385   \begin{matharray}{rcl}

   386     @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   387     @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   388     @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   389     @{command_def "schematic_lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   390     @{command_def "schematic_theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   391     @{command_def "schematic_corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   392     @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\

   393     @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\

   394     @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\

   395     @{command_def "thus"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\

   396     @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

   397   \end{matharray}

   398

   399   From a theory context, proof mode is entered by an initial goal

   400   command such as @{command "lemma"}, @{command "theorem"}, or

   401   @{command "corollary"}.  Within a proof, new claims may be

   402   introduced locally as well; four variants are available here to

   403   indicate whether forward chaining of facts should be performed

   404   initially (via @{command_ref "then"}), and whether the final result

   405   is meant to solve some pending goal.

   406

   407   Goals may consist of multiple statements, resulting in a list of

   408   facts eventually.  A pending multi-goal is internally represented as

   409   a meta-level conjunction (@{text "&&&"}), which is usually

   410   split into the corresponding number of sub-goals prior to an initial

   411   method application, via @{command_ref "proof"}

   412   (\secref{sec:proof-steps}) or @{command_ref "apply"}

   413   (\secref{sec:tactic-commands}).  The @{method_ref induct} method

   414   covered in \secref{sec:cases-induct} acts on multiple claims

   415   simultaneously.

   416

   417   Claims at the theory level may be either in short or long form.  A

   418   short goal merely consists of several simultaneous propositions

   419   (often just one).  A long goal includes an explicit context

   420   specification for the subsequent conclusion, involving local

   421   parameters and assumptions.  Here the role of each part of the

   422   statement is explicitly marked by separate keywords (see also

   423   \secref{sec:locale}); the local assumptions being introduced here

   424   are available as @{fact_ref assms} in the proof.  Moreover, there

   425   are two kinds of conclusions: @{element_def "shows"} states several

   426   simultaneous propositions (essentially a big conjunction), while

   427   @{element_def "obtains"} claims several simultaneous simultaneous

   428   contexts of (essentially a big disjunction of eliminated parameters

   429   and assumptions, cf.\ \secref{sec:obtain}).

   430

   431   @{rail "

   432     (@@{command lemma} | @@{command theorem} | @@{command corollary} |

   433      @@{command schematic_lemma} | @@{command schematic_theorem} |

   434      @@{command schematic_corollary}) @{syntax target}? (goal | longgoal)

   435     ;

   436     (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal

   437     ;

   438     @@{command print_statement} @{syntax modes}? @{syntax thmrefs}

   439     ;

   440

   441     goal: (@{syntax props} + @'and')

   442     ;

   443     longgoal: @{syntax thmdecl}? (@{syntax_ref \"includes\"}?) (@{syntax context_elem} * ) conclusion

   444     ;

   445     conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')

   446     ;

   447     case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')

   448   "}

   449

   450   \begin{description}

   451

   452   \item @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with

   453   @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>

   454   \<phi>"} to be put back into the target context.  An additional @{syntax

   455   context} specification may build up an initial proof context for the

   456   subsequent claim; this includes local definitions and syntax as

   457   well, see also @{syntax "includes"} in \secref{sec:bundle} and

   458   @{syntax context_elem} in \secref{sec:locale}.

   459

   460   \item @{command "theorem"}~@{text "a: \<phi>"} and @{command

   461   "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command

   462   "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as

   463   being of a different kind.  This discrimination acts like a formal

   464   comment.

   465

   466   \item @{command "schematic_lemma"}, @{command "schematic_theorem"},

   467   @{command "schematic_corollary"} are similar to @{command "lemma"},

   468   @{command "theorem"}, @{command "corollary"}, respectively but allow

   469   the statement to contain unbound schematic variables.

   470

   471   Under normal circumstances, an Isar proof text needs to specify

   472   claims explicitly.  Schematic goals are more like goals in Prolog,

   473   where certain results are synthesized in the course of reasoning.

   474   With schematic statements, the inherent compositionality of Isar

   475   proofs is lost, which also impacts performance, because proof

   476   checking is forced into sequential mode.

   477

   478   \item @{command "have"}~@{text "a: \<phi>"} claims a local goal,

   479   eventually resulting in a fact within the current logical context.

   480   This operation is completely independent of any pending sub-goals of

   481   an enclosing goal statements, so @{command "have"} may be freely

   482   used for experimental exploration of potential results within a

   483   proof body.

   484

   485   \item @{command "show"}~@{text "a: \<phi>"} is like @{command

   486   "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending

   487   sub-goal for each one of the finished result, after having been

   488   exported into the corresponding context (at the head of the

   489   sub-proof of this @{command "show"} command).

   490

   491   To accommodate interactive debugging, resulting rules are printed

   492   before being applied internally.  Even more, interactive execution

   493   of @{command "show"} predicts potential failure and displays the

   494   resulting error as a warning beforehand.  Watch out for the

   495   following message:

   496

   497   %FIXME proper antiquitation

   498   \begin{ttbox}

   499   Problem! Local statement will fail to solve any pending goal

   500   \end{ttbox}

   501

   502   \item @{command "hence"} abbreviates @{command "then"}~@{command

   503   "have"}'', i.e.\ claims a local goal to be proven by forward

   504   chaining the current facts.  Note that @{command "hence"} is also

   505   equivalent to @{command "from"}~@{text this}~@{command "have"}''.

   506

   507   \item @{command "thus"} abbreviates @{command "then"}~@{command

   508   "show"}''.  Note that @{command "thus"} is also equivalent to

   509   @{command "from"}~@{text this}~@{command "show"}''.

   510

   511   \item @{command "print_statement"}~@{text a} prints facts from the

   512   current theory or proof context in long statement form, according to

   513   the syntax for @{command "lemma"} given above.

   514

   515   \end{description}

   516

   517   Any goal statement causes some term abbreviations (such as

   518   @{variable_ref "?thesis"}) to be bound automatically, see also

   519   \secref{sec:term-abbrev}.

   520

   521   The optional case names of @{element_ref "obtains"} have a twofold

   522   meaning: (1) during the of this claim they refer to the the local

   523   context introductions, (2) the resulting rule is annotated

   524   accordingly to support symbolic case splits when used with the

   525   @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).

   526 *}

   527

   528

   529 section {* Refinement steps *}

   530

   531 subsection {* Proof method expressions \label{sec:proof-meth} *}

   532

   533 text {* Proof methods are either basic ones, or expressions composed

   534   of methods via @{verbatim ","}'' (sequential composition),

   535   @{verbatim "|"}'' (alternative choices), @{verbatim "?"}''

   536   (try), @{verbatim "+"}'' (repeat at least once), @{verbatim

   537   "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}

   538   sub-goals, with default @{text "n = 1"}).  In practice, proof

   539   methods are usually just a comma separated list of @{syntax

   540   nameref}~@{syntax args} specifications.  Note that parentheses may

   541   be dropped for single method specifications (with no arguments).

   542

   543   @{rail "

   544     @{syntax_def method}:

   545       (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')

   546     ;

   547     methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | '|')

   548   "}

   549

   550   Proper Isar proof methods do \emph{not} admit arbitrary goal

   551   addressing, but refer either to the first sub-goal or all sub-goals

   552   uniformly.  The goal restriction operator @{text "[n]"}''

   553   evaluates a method expression within a sandbox consisting of the

   554   first @{text n} sub-goals (which need to exist).  For example, the

   555   method @{text "simp_all[3]"}'' simplifies the first three

   556   sub-goals, while @{text "(rule foo, simp_all)[]"}'' simplifies all

   557   new goals that emerge from applying rule @{text "foo"} to the

   558   originally first one.

   559

   560   Improper methods, notably tactic emulations, offer a separate

   561   low-level goal addressing scheme as explicit argument to the

   562   individual tactic being involved.  Here @{text "[!]"}'' refers to

   563   all goals, and @{text "[n-]"}'' to all goals starting from @{text

   564   "n"}.

   565

   566   @{rail "

   567     @{syntax_def goal_spec}:

   568       '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'

   569   "}

   570 *}

   571

   572

   573 subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}

   574

   575 text {*

   576   \begin{matharray}{rcl}

   577     @{command_def "proof"} & : & @{text "proof(prove) \<rightarrow> proof(state)"} \\

   578     @{command_def "qed"} & : & @{text "proof(state) \<rightarrow> proof(state) | local_theory | theory"} \\

   579     @{command_def "by"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

   580     @{command_def ".."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

   581     @{command_def "."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

   582     @{command_def "sorry"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

   583   \end{matharray}

   584

   585   Arbitrary goal refinement via tactics is considered harmful.

   586   Structured proof composition in Isar admits proof methods to be

   587   invoked in two places only.

   588

   589   \begin{enumerate}

   590

   591   \item An \emph{initial} refinement step @{command_ref

   592   "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number

   593   of sub-goals that are to be solved later.  Facts are passed to

   594   @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text

   595   "proof(chain)"} mode.

   596

   597   \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text

   598   "m\<^sub>2"} is intended to solve remaining goals.  No facts are

   599   passed to @{text "m\<^sub>2"}.

   600

   601   \end{enumerate}

   602

   603   The only other (proper) way to affect pending goals in a proof body

   604   is by @{command_ref "show"}, which involves an explicit statement of

   605   what is to be solved eventually.  Thus we avoid the fundamental

   606   problem of unstructured tactic scripts that consist of numerous

   607   consecutive goal transformations, with invisible effects.

   608

   609   \medskip As a general rule of thumb for good proof style, initial

   610   proof methods should either solve the goal completely, or constitute

   611   some well-understood reduction to new sub-goals.  Arbitrary

   612   automatic proof tools that are prone leave a large number of badly

   613   structured sub-goals are no help in continuing the proof document in

   614   an intelligible manner.

   615

   616   Unless given explicitly by the user, the default initial method is

   617   @{method_ref (Pure) rule} (or its classical variant @{method_ref

   618   rule}), which applies a single standard elimination or introduction

   619   rule according to the topmost symbol involved.  There is no separate

   620   default terminal method.  Any remaining goals are always solved by

   621   assumption in the very last step.

   622

   623   @{rail "

   624     @@{command proof} method?

   625     ;

   626     @@{command qed} method?

   627     ;

   628     @@{command \"by\"} method method?

   629     ;

   630     (@@{command \".\"} | @@{command \"..\"} | @@{command sorry})

   631   "}

   632

   633   \begin{description}

   634

   635   \item @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof

   636   method @{text "m\<^sub>1"}; facts for forward chaining are passed if so

   637   indicated by @{text "proof(chain)"} mode.

   638

   639   \item @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by

   640   proof method @{text "m\<^sub>2"} and concludes the sub-proof by assumption.

   641   If the goal had been @{text "show"} (or @{text "thus"}), some

   642   pending sub-goal is solved as well by the rule resulting from the

   643   result \emph{exported} into the enclosing goal context.  Thus @{text

   644   "qed"} may fail for two reasons: either @{text "m\<^sub>2"} fails, or the

   645   resulting rule does not fit to any pending goal\footnote{This

   646   includes any additional strong'' assumptions as introduced by

   647   @{command "assume"}.} of the enclosing context.  Debugging such a

   648   situation might involve temporarily changing @{command "show"} into

   649   @{command "have"}, or weakening the local context by replacing

   650   occurrences of @{command "assume"} by @{command "presume"}.

   651

   652   \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal

   653   proof}\index{proof!terminal}; it abbreviates @{command

   654   "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"}, but with

   655   backtracking across both methods.  Debugging an unsuccessful

   656   @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} command can be done by expanding its

   657   definition; in many cases @{command "proof"}~@{text "m\<^sub>1"} (or even

   658   @{text "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the

   659   problem.

   660

   661   \item @{command ".."}'' is a \emph{default

   662   proof}\index{proof!default}; it abbreviates @{command "by"}~@{text

   663   "rule"}.

   664

   665   \item @{command "."}'' is a \emph{trivial

   666   proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text

   667   "this"}.

   668

   669   \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}

   670   pretending to solve the pending claim without further ado.  This

   671   only works in interactive development, or if the @{ML

   672   quick_and_dirty} flag is enabled (in ML).  Facts emerging from fake

   673   proofs are not the real thing.  Internally, the derivation object is

   674   tainted by an oracle invocation, which may be inspected via the

   675   theorem status \cite{isabelle-implementation}.

   676

   677   The most important application of @{command "sorry"} is to support

   678   experimentation and top-down proof development.

   679

   680   \end{description}

   681 *}

   682

   683

   684 subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}

   685

   686 text {*

   687   The following proof methods and attributes refer to basic logical

   688   operations of Isar.  Further methods and attributes are provided by

   689   several generic and object-logic specific tools and packages (see

   690   \chref{ch:gen-tools} and \partref{part:hol}).

   691

   692   \begin{matharray}{rcl}

   693     @{method_def "-"} & : & @{text method} \\

   694     @{method_def "fact"} & : & @{text method} \\

   695     @{method_def "assumption"} & : & @{text method} \\

   696     @{method_def "this"} & : & @{text method} \\

   697     @{method_def (Pure) "rule"} & : & @{text method} \\

   698     @{attribute_def (Pure) "intro"} & : & @{text attribute} \\

   699     @{attribute_def (Pure) "elim"} & : & @{text attribute} \\

   700     @{attribute_def (Pure) "dest"} & : & @{text attribute} \\

   701     @{attribute_def (Pure) "rule"} & : & @{text attribute} \\[0.5ex]

   702     @{attribute_def "OF"} & : & @{text attribute} \\

   703     @{attribute_def "of"} & : & @{text attribute} \\

   704     @{attribute_def "where"} & : & @{text attribute} \\

   705   \end{matharray}

   706

   707   @{rail "

   708     @@{method fact} @{syntax thmrefs}?

   709     ;

   710     @@{method (Pure) rule} @{syntax thmrefs}?

   711     ;

   712     rulemod: ('intro' | 'elim' | 'dest')

   713       ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs}

   714     ;

   715     (@@{attribute intro} | @@{attribute elim} | @@{attribute dest})

   716       ('!' | () | '?') @{syntax nat}?

   717     ;

   718     @@{attribute (Pure) rule} 'del'

   719     ;

   720     @@{attribute OF} @{syntax thmrefs}

   721     ;

   722     @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})?

   723     ;

   724     @@{attribute \"where\"}

   725       ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='

   726       (@{syntax type} | @{syntax term}) * @'and')

   727   "}

   728

   729   \begin{description}

   730

   731   \item @{method "-"}'' (minus) does nothing but insert the forward

   732   chaining facts as premises into the goal.  Note that command

   733   @{command_ref "proof"} without any method actually performs a single

   734   reduction step using the @{method_ref (Pure) rule} method; thus a plain

   735   \emph{do-nothing} proof step would be @{command "proof"}~@{text

   736   "-"}'' rather than @{command "proof"} alone.

   737

   738   \item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from

   739   @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)

   740   modulo unification of schematic type and term variables.  The rule

   741   structure is not taken into account, i.e.\ meta-level implication is

   742   considered atomic.  This is the same principle underlying literal

   743   facts (cf.\ \secref{sec:syn-att}): @{command "have"}~@{text

   744   "\<phi>"}~@{command "by"}~@{text fact}'' is equivalent to @{command

   745   "note"}~@{verbatim ""}@{text \<phi>}@{verbatim ""}'' provided that

   746   @{text "\<turnstile> \<phi>"} is an instance of some known @{text "\<turnstile> \<phi>"} in the

   747   proof context.

   748

   749   \item @{method assumption} solves some goal by a single assumption

   750   step.  All given facts are guaranteed to participate in the

   751   refinement; this means there may be only 0 or 1 in the first place.

   752   Recall that @{command "qed"} (\secref{sec:proof-steps}) already

   753   concludes any remaining sub-goals by assumption, so structured

   754   proofs usually need not quote the @{method assumption} method at

   755   all.

   756

   757   \item @{method this} applies all of the current facts directly as

   758   rules.  Recall that @{command "."}'' (dot) abbreviates @{command

   759   "by"}~@{text this}''.

   760

   761   \item @{method (Pure) rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as

   762   argument in backward manner; facts are used to reduce the rule

   763   before applying it to the goal.  Thus @{method (Pure) rule} without facts

   764   is plain introduction, while with facts it becomes elimination.

   765

   766   When no arguments are given, the @{method (Pure) rule} method tries to pick

   767   appropriate rules automatically, as declared in the current context

   768   using the @{attribute (Pure) intro}, @{attribute (Pure) elim},

   769   @{attribute (Pure) dest} attributes (see below).  This is the

   770   default behavior of @{command "proof"} and @{command ".."}''

   771   (double-dot) steps (see \secref{sec:proof-steps}).

   772

   773   \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and

   774   @{attribute (Pure) dest} declare introduction, elimination, and

   775   destruct rules, to be used with method @{method (Pure) rule}, and similar

   776   tools.  Note that the latter will ignore rules declared with

   777   @{text "?"}'', while @{text "!"}''  are used most aggressively.

   778

   779   The classical reasoner (see \secref{sec:classical}) introduces its

   780   own variants of these attributes; use qualified names to access the

   781   present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)

   782   "Pure.intro"}.

   783

   784   \item @{attribute (Pure) rule}~@{text del} undeclares introduction,

   785   elimination, or destruct rules.

   786

   787   \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some theorem to all

   788   of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"} in canonical right-to-left

   789   order, which means that premises stemming from the @{text "a\<^sub>i"}

   790   emerge in parallel in the result, without interfering with each

   791   other.  In many practical situations, the @{text "a\<^sub>i"} do not have

   792   premises themselves, so @{text "rule [OF a\<^sub>1 \<dots> a\<^sub>n]"} can be actually

   793   read as functional application (modulo unification).

   794

   795   Argument positions may be effectively skipped by using @{text _}''

   796   (underscore), which refers to the propositional identity rule in the

   797   Pure theory.

   798

   799   \item @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional

   800   instantiation of term variables.  The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are

   801   substituted for any schematic variables occurring in a theorem from

   802   left to right; @{text _}'' (underscore) indicates to skip a

   803   position.  Arguments following a @{text "concl:"}'' specification

   804   refer to positions of the conclusion of a rule.

   805

   806   \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}

   807   performs named instantiation of schematic type and term variables

   808   occurring in a theorem.  Schematic variables have to be specified on

   809   the left-hand side (e.g.\ @{text "?x1.3"}).  The question mark may

   810   be omitted if the variable name is a plain identifier without index.

   811   As type instantiations are inferred from term instantiations,

   812   explicit type instantiations are seldom necessary.

   813

   814   \end{description}

   815 *}

   816

   817

   818 subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}

   819

   820 text {*

   821   The Isar provides separate commands to accommodate tactic-style

   822   proof scripts within the same system.  While being outside the

   823   orthodox Isar proof language, these might come in handy for

   824   interactive exploration and debugging, or even actual tactical proof

   825   within new-style theories (to benefit from document preparation, for

   826   example).  See also \secref{sec:tactics} for actual tactics, that

   827   have been encapsulated as proof methods.  Proper proof methods may

   828   be used in scripts, too.

   829

   830   \begin{matharray}{rcl}

   831     @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\

   832     @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

   833     @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

   834     @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\

   835     @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\

   836     @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\

   837   \end{matharray}

   838

   839   @{rail "

   840     ( @@{command apply} | @@{command apply_end} ) @{syntax method}

   841     ;

   842     @@{command defer} @{syntax nat}?

   843     ;

   844     @@{command prefer} @{syntax nat}

   845   "}

   846

   847   \begin{description}

   848

   849   \item @{command "apply"}~@{text m} applies proof method @{text m} in

   850   initial position, but unlike @{command "proof"} it retains @{text

   851   "proof(prove)"}'' mode.  Thus consecutive method applications may be

   852   given just as in tactic scripts.

   853

   854   Facts are passed to @{text m} as indicated by the goal's

   855   forward-chain mode, and are \emph{consumed} afterwards.  Thus any

   856   further @{command "apply"} command would always work in a purely

   857   backward manner.

   858

   859   \item @{command "apply_end"}~@{text "m"} applies proof method @{text

   860   m} as if in terminal position.  Basically, this simulates a

   861   multi-step tactic script for @{command "qed"}, but may be given

   862   anywhere within the proof body.

   863

   864   No facts are passed to @{text m} here.  Furthermore, the static

   865   context is that of the enclosing goal (as for actual @{command

   866   "qed"}).  Thus the proof method may not refer to any assumptions

   867   introduced in the current body, for example.

   868

   869   \item @{command "done"} completes a proof script, provided that the

   870   current goal state is solved completely.  Note that actual

   871   structured proof commands (e.g.\ @{command "."}'' or @{command

   872   "sorry"}) may be used to conclude proof scripts as well.

   873

   874   \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}

   875   shuffle the list of pending goals: @{command "defer"} puts off

   876   sub-goal @{text n} to the end of the list (@{text "n = 1"} by

   877   default), while @{command "prefer"} brings sub-goal @{text n} to the

   878   front.

   879

   880   \item @{command "back"} does back-tracking over the result sequence

   881   of the latest proof command.  Basically, any proof command may

   882   return multiple results.

   883

   884   \end{description}

   885

   886   Any proper Isar proof method may be used with tactic script commands

   887   such as @{command "apply"}.  A few additional emulations of actual

   888   tactics are provided as well; these would be never used in actual

   889   structured proofs, of course.

   890 *}

   891

   892

   893 subsection {* Defining proof methods *}

   894

   895 text {*

   896   \begin{matharray}{rcl}

   897     @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\

   898   \end{matharray}

   899

   900   @{rail "

   901     @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?

   902     ;

   903   "}

   904

   905   \begin{description}

   906

   907   \item @{command "method_setup"}~@{text "name = text description"}

   908   defines a proof method in the current theory.  The given @{text

   909   "text"} has to be an ML expression of type

   910   @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\

   911   basic parsers defined in structure @{ML_struct Args} and @{ML_struct

   912   Attrib}.  There are also combinators like @{ML METHOD} and @{ML

   913   SIMPLE_METHOD} to turn certain tactic forms into official proof

   914   methods; the primed versions refer to tactics with explicit goal

   915   addressing.

   916

   917   Here are some example method definitions:

   918

   919   \end{description}

   920 *}

   921

   922   method_setup my_method1 = {*

   923     Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))

   924   *}  "my first method (without any arguments)"

   925

   926   method_setup my_method2 = {*

   927     Scan.succeed (fn ctxt: Proof.context =>

   928       SIMPLE_METHOD' (fn i: int => no_tac))

   929   *}  "my second method (with context)"

   930

   931   method_setup my_method3 = {*

   932     Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>

   933       SIMPLE_METHOD' (fn i: int => no_tac))

   934   *}  "my third method (with theorem arguments and context)"

   935

   936

   937 section {* Generalized elimination \label{sec:obtain} *}

   938

   939 text {*

   940   \begin{matharray}{rcl}

   941     @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\

   942     @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\

   943   \end{matharray}

   944

   945   Generalized elimination means that additional elements with certain

   946   properties may be introduced in the current context, by virtue of a

   947   locally proven soundness statement''.  Technically speaking, the

   948   @{command "obtain"} language element is like a declaration of

   949   @{command "fix"} and @{command "assume"} (see also see

   950   \secref{sec:proof-context}), together with a soundness proof of its

   951   additional claim.  According to the nature of existential reasoning,

   952   assumptions get eliminated from any result exported from the context

   953   later, provided that the corresponding parameters do \emph{not}

   954   occur in the conclusion.

   955

   956   @{rail "

   957     @@{command obtain} @{syntax parname}? (@{syntax vars} + @'and')

   958       @'where' (@{syntax props} + @'and')

   959     ;

   960     @@{command guess} (@{syntax vars} + @'and')

   961   "}

   962

   963   The derived Isar command @{command "obtain"} is defined as follows

   964   (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)

   965   facts indicated for forward chaining).

   966   \begin{matharray}{l}

   967     @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n  \<langle>proof\<rangle> \<equiv>"} \\[1ex]

   968     \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\

   969     \quad @{command "proof"}~@{method succeed} \\

   970     \qquad @{command "fix"}~@{text thesis} \\

   971     \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\

   972     \qquad @{command "then"}~@{command "show"}~@{text thesis} \\

   973     \quad\qquad @{command "apply"}~@{text -} \\

   974     \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k  \<langle>proof\<rangle>"} \\

   975     \quad @{command "qed"} \\

   976     \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\

   977   \end{matharray}

   978

   979   Typically, the soundness proof is relatively straight-forward, often

   980   just by canonical automated tools such as @{command "by"}~@{text

   981   simp}'' or @{command "by"}~@{text blast}''.  Accordingly, the

   982   @{text that}'' reduction above is declared as simplification and

   983   introduction rule.

   984

   985   In a sense, @{command "obtain"} represents at the level of Isar

   986   proofs what would be meta-logical existential quantifiers and

   987   conjunctions.  This concept has a broad range of useful

   988   applications, ranging from plain elimination (or introduction) of

   989   object-level existential and conjunctions, to elimination over

   990   results of symbolic evaluation of recursive definitions, for

   991   example.  Also note that @{command "obtain"} without parameters acts

   992   much like @{command "have"}, where the result is treated as a

   993   genuine assumption.

   994

   995   An alternative name to be used instead of @{text that}'' above may

   996   be given in parentheses.

   997

   998   \medskip The improper variant @{command "guess"} is similar to

   999   @{command "obtain"}, but derives the obtained statement from the

  1000   course of reasoning!  The proof starts with a fixed goal @{text

  1001   thesis}.  The subsequent proof may refine this to anything of the

  1002   form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>

  1003   \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals.  The

  1004   final goal state is then used as reduction rule for the obtain

  1005   scheme described above.  Obtained parameters @{text "x\<^sub>1, \<dots>,

  1006   x\<^sub>m"} are marked as internal by default, which prevents the

  1007   proof context from being polluted by ad-hoc variables.  The variable

  1008   names and type constraints given as arguments for @{command "guess"}

  1009   specify a prefix of obtained parameters explicitly in the text.

  1010

  1011   It is important to note that the facts introduced by @{command

  1012   "obtain"} and @{command "guess"} may not be polymorphic: any

  1013   type-variables occurring here are fixed in the present context!

  1014 *}

  1015

  1016

  1017 section {* Calculational reasoning \label{sec:calculation} *}

  1018

  1019 text {*

  1020   \begin{matharray}{rcl}

  1021     @{command_def "also"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

  1022     @{command_def "finally"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

  1023     @{command_def "moreover"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

  1024     @{command_def "ultimately"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

  1025     @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1026     @{attribute trans} & : & @{text attribute} \\

  1027     @{attribute sym} & : & @{text attribute} \\

  1028     @{attribute symmetric} & : & @{text attribute} \\

  1029   \end{matharray}

  1030

  1031   Calculational proof is forward reasoning with implicit application

  1032   of transitivity rules (such those of @{text "="}, @{text "\<le>"},

  1033   @{text "<"}).  Isabelle/Isar maintains an auxiliary fact register

  1034   @{fact_ref calculation} for accumulating results obtained by

  1035   transitivity composed with the current result.  Command @{command

  1036   "also"} updates @{fact calculation} involving @{fact this}, while

  1037   @{command "finally"} exhibits the final @{fact calculation} by

  1038   forward chaining towards the next goal statement.  Both commands

  1039   require valid current facts, i.e.\ may occur only after commands

  1040   that produce theorems such as @{command "assume"}, @{command

  1041   "note"}, or some finished proof of @{command "have"}, @{command

  1042   "show"} etc.  The @{command "moreover"} and @{command "ultimately"}

  1043   commands are similar to @{command "also"} and @{command "finally"},

  1044   but only collect further results in @{fact calculation} without

  1045   applying any rules yet.

  1046

  1047   Also note that the implicit term abbreviation @{text "\<dots>"}'' has

  1048   its canonical application with calculational proofs.  It refers to

  1049   the argument of the preceding statement. (The argument of a curried

  1050   infix expression happens to be its right-hand side.)

  1051

  1052   Isabelle/Isar calculations are implicitly subject to block structure

  1053   in the sense that new threads of calculational reasoning are

  1054   commenced for any new block (as opened by a local goal, for

  1055   example).  This means that, apart from being able to nest

  1056   calculations, there is no separate \emph{begin-calculation} command

  1057   required.

  1058

  1059   \medskip The Isar calculation proof commands may be defined as

  1060   follows:\footnote{We suppress internal bookkeeping such as proper

  1061   handling of block-structure.}

  1062

  1063   \begin{matharray}{rcl}

  1064     @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\

  1065     @{command "also"}@{text "\<^sub>n+1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]

  1066     @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]

  1067     @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\

  1068     @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\

  1069   \end{matharray}

  1070

  1071   @{rail "

  1072     (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')?

  1073     ;

  1074     @@{attribute trans} (() | 'add' | 'del')

  1075   "}

  1076

  1077   \begin{description}

  1078

  1079   \item @{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintains the auxiliary

  1080   @{fact calculation} register as follows.  The first occurrence of

  1081   @{command "also"} in some calculational thread initializes @{fact

  1082   calculation} by @{fact this}. Any subsequent @{command "also"} on

  1083   the same level of block-structure updates @{fact calculation} by

  1084   some transitivity rule applied to @{fact calculation} and @{fact

  1085   this} (in that order).  Transitivity rules are picked from the

  1086   current context, unless alternative rules are given as explicit

  1087   arguments.

  1088

  1089   \item @{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintaining @{fact

  1090   calculation} in the same way as @{command "also"}, and concludes the

  1091   current calculational thread.  The final result is exhibited as fact

  1092   for forward chaining towards the next goal. Basically, @{command

  1093   "finally"} just abbreviates @{command "also"}~@{command

  1094   "from"}~@{fact calculation}.  Typical idioms for concluding

  1095   calculational proofs are @{command "finally"}~@{command

  1096   "show"}~@{text ?thesis}~@{command "."}'' and @{command

  1097   "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.

  1098

  1099   \item @{command "moreover"} and @{command "ultimately"} are

  1100   analogous to @{command "also"} and @{command "finally"}, but collect

  1101   results only, without applying rules.

  1102

  1103   \item @{command "print_trans_rules"} prints the list of transitivity

  1104   rules (for calculational commands @{command "also"} and @{command

  1105   "finally"}) and symmetry rules (for the @{attribute symmetric}

  1106   operation and single step elimination patters) of the current

  1107   context.

  1108

  1109   \item @{attribute trans} declares theorems as transitivity rules.

  1110

  1111   \item @{attribute sym} declares symmetry rules, as well as

  1112   @{attribute "Pure.elim"}@{text "?"} rules.

  1113

  1114   \item @{attribute symmetric} resolves a theorem with some rule

  1115   declared as @{attribute sym} in the current context.  For example,

  1116   @{command "assume"}~@{text "[symmetric]: x = y"}'' produces a

  1117   swapped fact derived from that assumption.

  1118

  1119   In structured proof texts it is often more appropriate to use an

  1120   explicit single-step elimination proof, such as @{command

  1121   "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text

  1122   "y = x"}~@{command ".."}''.

  1123

  1124   \end{description}

  1125 *}

  1126

  1127

  1128 section {* Proof by cases and induction \label{sec:cases-induct} *}

  1129

  1130 subsection {* Rule contexts *}

  1131

  1132 text {*

  1133   \begin{matharray}{rcl}

  1134     @{command_def "case"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

  1135     @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1136     @{attribute_def case_names} & : & @{text attribute} \\

  1137     @{attribute_def case_conclusion} & : & @{text attribute} \\

  1138     @{attribute_def params} & : & @{text attribute} \\

  1139     @{attribute_def consumes} & : & @{text attribute} \\

  1140   \end{matharray}

  1141

  1142   The puristic way to build up Isar proof contexts is by explicit

  1143   language elements like @{command "fix"}, @{command "assume"},

  1144   @{command "let"} (see \secref{sec:proof-context}).  This is adequate

  1145   for plain natural deduction, but easily becomes unwieldy in concrete

  1146   verification tasks, which typically involve big induction rules with

  1147   several cases.

  1148

  1149   The @{command "case"} command provides a shorthand to refer to a

  1150   local context symbolically: certain proof methods provide an

  1151   environment of named cases'' of the form @{text "c: x\<^sub>1, \<dots>,

  1152   x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of @{command

  1153   "case"}~@{text c}'' is then equivalent to @{command "fix"}~@{text

  1154   "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>

  1155   \<phi>\<^sub>n"}''.  Term bindings may be covered as well, notably

  1156   @{variable ?case} for the main conclusion.

  1157

  1158   By default, the terminology'' @{text "x\<^sub>1, \<dots>, x\<^sub>m"} of

  1159   a case value is marked as hidden, i.e.\ there is no way to refer to

  1160   such parameters in the subsequent proof text.  After all, original

  1161   rule parameters stem from somewhere outside of the current proof

  1162   text.  By using the explicit form @{command "case"}~@{text "(c

  1163   y\<^sub>1 \<dots> y\<^sub>m)"}'' instead, the proof author is able to

  1164   chose local names that fit nicely into the current context.

  1165

  1166   \medskip It is important to note that proper use of @{command

  1167   "case"} does not provide means to peek at the current goal state,

  1168   which is not directly observable in Isar!  Nonetheless, goal

  1169   refinement commands do provide named cases @{text "goal\<^sub>i"}

  1170   for each subgoal @{text "i = 1, \<dots>, n"} of the resulting goal state.

  1171   Using this extra feature requires great care, because some bits of

  1172   the internal tactical machinery intrude the proof text.  In

  1173   particular, parameter names stemming from the left-over of automated

  1174   reasoning tools are usually quite unpredictable.

  1175

  1176   Under normal circumstances, the text of cases emerge from standard

  1177   elimination or induction rules, which in turn are derived from

  1178   previous theory specifications in a canonical way (say from

  1179   @{command "inductive"} definitions).

  1180

  1181   \medskip Proper cases are only available if both the proof method

  1182   and the rules involved support this.  By using appropriate

  1183   attributes, case names, conclusions, and parameters may be also

  1184   declared by hand.  Thus variant versions of rules that have been

  1185   derived manually become ready to use in advanced case analysis

  1186   later.

  1187

  1188   @{rail "

  1189     @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) +) ')')

  1190     ;

  1191     caseref: nameref attributes?

  1192     ;

  1193

  1194     @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)

  1195     ;

  1196     @@{attribute case_conclusion} @{syntax name} (@{syntax name} * )

  1197     ;

  1198     @@{attribute params} ((@{syntax name} * ) + @'and')

  1199     ;

  1200     @@{attribute consumes} @{syntax nat}?

  1201   "}

  1202

  1203   \begin{description}

  1204

  1205   \item @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local

  1206   context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an

  1207   appropriate proof method (such as @{method_ref cases} and

  1208   @{method_ref induct}).  The command @{command "case"}~@{text "(c

  1209   x\<^sub>1 \<dots> x\<^sub>m)"}'' abbreviates @{command "fix"}~@{text "x\<^sub>1 \<dots>

  1210   x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''.

  1211

  1212   \item @{command "print_cases"} prints all local contexts of the

  1213   current state, using Isar proof language notation.

  1214

  1215   \item @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for

  1216   the local contexts of premises of a theorem; @{text "c\<^sub>1, \<dots>, c\<^sub>k"}

  1217   refers to the \emph{prefix} of the list of premises. Each of the

  1218   cases @{text "c\<^isub>i"} can be of the form @{text "c[h\<^isub>1 \<dots> h\<^isub>n]"} where

  1219   the @{text "h\<^isub>1 \<dots> h\<^isub>n"} are the names of the hypotheses in case @{text "c\<^isub>i"}

  1220   from left to right.

  1221

  1222   \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares

  1223   names for the conclusions of a named premise @{text c}; here @{text

  1224   "d\<^sub>1, \<dots>, d\<^sub>k"} refers to the prefix of arguments of a logical formula

  1225   built by nesting a binary connective (e.g.\ @{text "\<or>"}).

  1226

  1227   Note that proof methods such as @{method induct} and @{method

  1228   coinduct} already provide a default name for the conclusion as a

  1229   whole.  The need to name subformulas only arises with cases that

  1230   split into several sub-cases, as in common co-induction rules.

  1231

  1232   \item @{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n"} renames

  1233   the innermost parameters of premises @{text "1, \<dots>, n"} of some

  1234   theorem.  An empty list of names may be given to skip positions,

  1235   leaving the present parameters unchanged.

  1236

  1237   Note that the default usage of case rules does \emph{not} directly

  1238   expose parameters to the proof context.

  1239

  1240   \item @{attribute consumes}~@{text n} declares the number of major

  1241   premises'' of a rule, i.e.\ the number of facts to be consumed when

  1242   it is applied by an appropriate proof method.  The default value of

  1243   @{attribute consumes} is @{text "n = 1"}, which is appropriate for

  1244   the usual kind of cases and induction rules for inductive sets (cf.\

  1245   \secref{sec:hol-inductive}).  Rules without any @{attribute

  1246   consumes} declaration given are treated as if @{attribute

  1247   consumes}~@{text 0} had been specified.

  1248

  1249   Note that explicit @{attribute consumes} declarations are only

  1250   rarely needed; this is already taken care of automatically by the

  1251   higher-level @{attribute cases}, @{attribute induct}, and

  1252   @{attribute coinduct} declarations.

  1253

  1254   \end{description}

  1255 *}

  1256

  1257

  1258 subsection {* Proof methods *}

  1259

  1260 text {*

  1261   \begin{matharray}{rcl}

  1262     @{method_def cases} & : & @{text method} \\

  1263     @{method_def induct} & : & @{text method} \\

  1264     @{method_def induction} & : & @{text method} \\

  1265     @{method_def coinduct} & : & @{text method} \\

  1266   \end{matharray}

  1267

  1268   The @{method cases}, @{method induct}, @{method induction},

  1269   and @{method coinduct}

  1270   methods provide a uniform interface to common proof techniques over

  1271   datatypes, inductive predicates (or sets), recursive functions etc.

  1272   The corresponding rules may be specified and instantiated in a

  1273   casual manner.  Furthermore, these methods provide named local

  1274   contexts that may be invoked via the @{command "case"} proof command

  1275   within the subsequent proof text.  This accommodates compact proof

  1276   texts even when reasoning about large specifications.

  1277

  1278   The @{method induct} method also provides some additional

  1279   infrastructure in order to be applicable to structure statements

  1280   (either using explicit meta-level connectives, or including facts

  1281   and parameters separately).  This avoids cumbersome encoding of

  1282   strengthened'' inductive statements within the object-logic.

  1283

  1284   Method @{method induction} differs from @{method induct} only in

  1285   the names of the facts in the local context invoked by the @{command "case"}

  1286   command.

  1287

  1288   @{rail "

  1289     @@{method cases} ('(' 'no_simp' ')')? \\

  1290       (@{syntax insts} * @'and') rule?

  1291     ;

  1292     (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?

  1293     ;

  1294     @@{method coinduct} @{syntax insts} taking rule?

  1295     ;

  1296

  1297     rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)

  1298     ;

  1299     definst: @{syntax name} ('==' | '\<equiv>') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst}

  1300     ;

  1301     definsts: ( definst * )

  1302     ;

  1303     arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)

  1304     ;

  1305     taking: 'taking' ':' @{syntax insts}

  1306   "}

  1307

  1308   \begin{description}

  1309

  1310   \item @{method cases}~@{text "insts R"} applies method @{method

  1311   rule} with an appropriate case distinction theorem, instantiated to

  1312   the subjects @{text insts}.  Symbolic case names are bound according

  1313   to the rule's local contexts.

  1314

  1315   The rule is determined as follows, according to the facts and

  1316   arguments passed to the @{method cases} method:

  1317

  1318   \medskip

  1319   \begin{tabular}{llll}

  1320     facts           &                 & arguments   & rule \\\hline

  1321                     & @{method cases} &             & classical case split \\

  1322                     & @{method cases} & @{text t}   & datatype exhaustion (type of @{text t}) \\

  1323     @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\

  1324     @{text "\<dots>"}     & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\

  1325   \end{tabular}

  1326   \medskip

  1327

  1328   Several instantiations may be given, referring to the \emph{suffix}

  1329   of premises of the case rule; within each premise, the \emph{prefix}

  1330   of variables is instantiated.  In most situations, only a single

  1331   term needs to be specified; this refers to the first variable of the

  1332   last premise (it is usually the same for all cases).  The @{text

  1333   "(no_simp)"} option can be used to disable pre-simplification of

  1334   cases (see the description of @{method induct} below for details).

  1335

  1336   \item @{method induct}~@{text "insts R"} and

  1337   @{method induction}~@{text "insts R"} are analogous to the

  1338   @{method cases} method, but refer to induction rules, which are

  1339   determined as follows:

  1340

  1341   \medskip

  1342   \begin{tabular}{llll}

  1343     facts           &                  & arguments            & rule \\\hline

  1344                     & @{method induct} & @{text "P x"}        & datatype induction (type of @{text x}) \\

  1345     @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"}          & predicate/set induction (of @{text A}) \\

  1346     @{text "\<dots>"}     & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\

  1347   \end{tabular}

  1348   \medskip

  1349

  1350   Several instantiations may be given, each referring to some part of

  1351   a mutual inductive definition or datatype --- only related partial

  1352   induction rules may be used together, though.  Any of the lists of

  1353   terms @{text "P, x, \<dots>"} refers to the \emph{suffix} of variables

  1354   present in the induction rule.  This enables the writer to specify

  1355   only induction variables, or both predicates and variables, for

  1356   example.

  1357

  1358   Instantiations may be definitional: equations @{text "x \<equiv> t"}

  1359   introduce local definitions, which are inserted into the claim and

  1360   discharged after applying the induction rule.  Equalities reappear

  1361   in the inductive cases, but have been transformed according to the

  1362   induction principle being involved here.  In order to achieve

  1363   practically useful induction hypotheses, some variables occurring in

  1364   @{text t} need to be fixed (see below).  Instantiations of the form

  1365   @{text t}, where @{text t} is not a variable, are taken as a

  1366   shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is a fresh

  1367   variable. If this is not intended, @{text t} has to be enclosed in

  1368   parentheses.  By default, the equalities generated by definitional

  1369   instantiations are pre-simplified using a specific set of rules,

  1370   usually consisting of distinctness and injectivity theorems for

  1371   datatypes. This pre-simplification may cause some of the parameters

  1372   of an inductive case to disappear, or may even completely delete

  1373   some of the inductive cases, if one of the equalities occurring in

  1374   their premises can be simplified to @{text False}.  The @{text

  1375   "(no_simp)"} option can be used to disable pre-simplification.

  1376   Additional rules to be used in pre-simplification can be declared

  1377   using the @{attribute_def induct_simp} attribute.

  1378

  1379   The optional @{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''

  1380   specification generalizes variables @{text "x\<^sub>1, \<dots>,

  1381   x\<^sub>m"} of the original goal before applying induction.  One can

  1382   separate variables by @{text "and"}'' to generalize them in other

  1383   goals then the first. Thus induction hypotheses may become

  1384   sufficiently general to get the proof through.  Together with

  1385   definitional instantiations, one may effectively perform induction

  1386   over expressions of a certain structure.

  1387

  1388   The optional @{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''

  1389   specification provides additional instantiations of a prefix of

  1390   pending variables in the rule.  Such schematic induction rules

  1391   rarely occur in practice, though.

  1392

  1393   \item @{method coinduct}~@{text "inst R"} is analogous to the

  1394   @{method induct} method, but refers to coinduction rules, which are

  1395   determined as follows:

  1396

  1397   \medskip

  1398   \begin{tabular}{llll}

  1399     goal          &                    & arguments & rule \\\hline

  1400                   & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\

  1401     @{text "A x"} & @{method coinduct} & @{text "\<dots>"} & predicate/set coinduction (of @{text A}) \\

  1402     @{text "\<dots>"}   & @{method coinduct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\

  1403   \end{tabular}

  1404

  1405   Coinduction is the dual of induction.  Induction essentially

  1406   eliminates @{text "A x"} towards a generic result @{text "P x"},

  1407   while coinduction introduces @{text "A x"} starting with @{text "B

  1408   x"}, for a suitable bisimulation'' @{text B}.  The cases of a

  1409   coinduct rule are typically named after the predicates or sets being

  1410   covered, while the conclusions consist of several alternatives being

  1411   named after the individual destructor patterns.

  1412

  1413   The given instantiation refers to the \emph{suffix} of variables

  1414   occurring in the rule's major premise, or conclusion if unavailable.

  1415   An additional @{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''

  1416   specification may be required in order to specify the bisimulation

  1417   to be used in the coinduction step.

  1418

  1419   \end{description}

  1420

  1421   Above methods produce named local contexts, as determined by the

  1422   instantiated rule as given in the text.  Beyond that, the @{method

  1423   induct} and @{method coinduct} methods guess further instantiations

  1424   from the goal specification itself.  Any persisting unresolved

  1425   schematic variables of the resulting rule will render the the

  1426   corresponding case invalid.  The term binding @{variable ?case} for

  1427   the conclusion will be provided with each case, provided that term

  1428   is fully specified.

  1429

  1430   The @{command "print_cases"} command prints all named cases present

  1431   in the current proof state.

  1432

  1433   \medskip Despite the additional infrastructure, both @{method cases}

  1434   and @{method coinduct} merely apply a certain rule, after

  1435   instantiation, while conforming due to the usual way of monotonic

  1436   natural deduction: the context of a structured statement @{text

  1437   "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>"}

  1438   reappears unchanged after the case split.

  1439

  1440   The @{method induct} method is fundamentally different in this

  1441   respect: the meta-level structure is passed through the

  1442   recursive'' course involved in the induction.  Thus the original

  1443   statement is basically replaced by separate copies, corresponding to

  1444   the induction hypotheses and conclusion; the original goal context

  1445   is no longer available.  Thus local assumptions, fixed parameters

  1446   and definitions effectively participate in the inductive rephrasing

  1447   of the original statement.

  1448

  1449   In @{method induct} proofs, local assumptions introduced by cases are split

  1450   into two different kinds: @{text hyps} stemming from the rule and

  1451   @{text prems} from the goal statement.  This is reflected in the

  1452   extracted cases accordingly, so invoking @{command "case"}~@{text

  1453   c}'' will provide separate facts @{text c.hyps} and @{text c.prems},

  1454   as well as fact @{text c} to hold the all-inclusive list.

  1455

  1456   In @{method induction} proofs, local assumptions introduced by cases are

  1457   split into three different kinds: @{text IH}, the induction hypotheses,

  1458   @{text hyps}, the remaining hypotheses stemming from the rule, and

  1459   @{text prems}, the assumptions from the goal statement. The names are

  1460   @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above.

  1461

  1462

  1463   \medskip Facts presented to either method are consumed according to

  1464   the number of major premises'' of the rule involved, which is

  1465   usually 0 for plain cases and induction rules of datatypes etc.\ and

  1466   1 for rules of inductive predicates or sets and the like.  The

  1467   remaining facts are inserted into the goal verbatim before the

  1468   actual @{text cases}, @{text induct}, or @{text coinduct} rule is

  1469   applied.

  1470 *}

  1471

  1472

  1473 subsection {* Declaring rules *}

  1474

  1475 text {*

  1476   \begin{matharray}{rcl}

  1477     @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

  1478     @{attribute_def cases} & : & @{text attribute} \\

  1479     @{attribute_def induct} & : & @{text attribute} \\

  1480     @{attribute_def coinduct} & : & @{text attribute} \\

  1481   \end{matharray}

  1482

  1483   @{rail "

  1484     @@{attribute cases} spec

  1485     ;

  1486     @@{attribute induct} spec

  1487     ;

  1488     @@{attribute coinduct} spec

  1489     ;

  1490

  1491     spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'

  1492   "}

  1493

  1494   \begin{description}

  1495

  1496   \item @{command "print_induct_rules"} prints cases and induct rules

  1497   for predicates (or sets) and types of the current context.

  1498

  1499   \item @{attribute cases}, @{attribute induct}, and @{attribute

  1500   coinduct} (as attributes) declare rules for reasoning about

  1501   (co)inductive predicates (or sets) and types, using the

  1502   corresponding methods of the same name.  Certain definitional

  1503   packages of object-logics usually declare emerging cases and

  1504   induction rules as expected, so users rarely need to intervene.

  1505

  1506   Rules may be deleted via the @{text "del"} specification, which

  1507   covers all of the @{text "type"}/@{text "pred"}/@{text "set"}

  1508   sub-categories simultaneously.  For example, @{attribute

  1509   cases}~@{text del} removes any @{attribute cases} rules declared for

  1510   some type, predicate, or set.

  1511

  1512   Manual rule declarations usually refer to the @{attribute

  1513   case_names} and @{attribute params} attributes to adjust names of

  1514   cases and parameters of a rule; the @{attribute consumes}

  1515   declaration is taken care of automatically: @{attribute

  1516   consumes}~@{text 0} is specified for type'' rules and @{attribute

  1517   consumes}~@{text 1} for predicate'' / set'' rules.

  1518

  1519   \end{description}

  1520 *}

  1521

  1522 end