src/Doc/Isar_Ref/Proof.thy
 author wenzelm Sun Dec 03 13:22:09 2017 +0100 (17 months ago) changeset 67119 acb0807ddb56 parent 64926 75ee8475c37e child 69597 ff784d5a5bfb permissions -rw-r--r--
discontinued old 'def' command;
     1 (*:maxLineLen=78:*)

     2

     3 theory Proof

     4   imports Main Base

     5 begin

     6

     7 chapter \<open>Proofs \label{ch:proofs}\<close>

     8

     9 text \<open>

    10   Proof commands perform transitions of Isar/VM machine configurations, which

    11   are block-structured, consisting of a stack of nodes with three main

    12   components: logical proof context, current facts, and open goals. Isar/VM

    13   transitions are typed according to the following three different modes of

    14   operation:

    15

    16     \<^descr> \<open>proof(prove)\<close> means that a new goal has just been stated that is now to

    17     be \<^emph>\<open>proven\<close>; the next command may refine it by some proof method, and

    18     enter a sub-proof to establish the actual result.

    19

    20     \<^descr> \<open>proof(state)\<close> is like a nested theory mode: the context may be

    21     augmented by \<^emph>\<open>stating\<close> additional assumptions, intermediate results etc.

    22

    23     \<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and

    24     \<open>proof(prove)\<close>: existing facts (i.e.\ the contents of the special

    25     @{fact_ref this} register) have been just picked up in order to be used

    26     when refining the goal claimed next.

    27

    28   The proof mode indicator may be understood as an instruction to the writer,

    29   telling what kind of operation may be performed next. The corresponding

    30   typings of proof commands restricts the shape of well-formed proof texts to

    31   particular command sequences. So dynamic arrangements of commands eventually

    32   turn out as static texts of a certain structure.

    33

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

    35   emerging that way from the different types of proof commands. The main ideas

    36   of the overall Isar framework are explained in \chref{ch:isar-framework}.

    37 \<close>

    38

    39

    40 section \<open>Proof structure\<close>

    41

    42 subsection \<open>Formal notepad\<close>

    43

    44 text \<open>

    45   \begin{matharray}{rcl}

    46     @{command_def "notepad"} & : & \<open>local_theory \<rightarrow> proof(state)\<close> \\

    47   \end{matharray}

    48

    49   @{rail \<open>

    50     @@{command notepad} @'begin'

    51     ;

    52     @@{command end}

    53   \<close>}

    54

    55   \<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without any

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

    57   persistent result. The notepad is closed by @{command "end"}.

    58 \<close>

    59

    60

    61 subsection \<open>Blocks\<close>

    62

    63 text \<open>

    64   \begin{matharray}{rcl}

    65     @{command_def "next"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

    66     @{command_def "{"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

    67     @{command_def "}"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

    68   \end{matharray}

    69

    70   While Isar is inherently block-structured, opening and closing blocks is

    71   mostly handled rather casually, with little explicit user-intervention. Any

    72   local goal statement automatically opens \<^emph>\<open>two\<close> internal blocks, which are

    73   closed again when concluding the sub-proof (by @{command "qed"} etc.).

    74   Sections of different context within a sub-proof may be switched via

    75   @{command "next"}, which is just a single block-close followed by block-open

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

    77   there is no goal focus involved here!

    78

    79   For slightly more advanced applications, there are explicit block

    80   parentheses as well. These typically achieve a stronger forward style of

    81   reasoning.

    82

    83   \<^descr> @{command "next"} switches to a fresh block within a sub-proof, resetting

    84   the local context to the initial one.

    85

    86   \<^descr> @{command "{"} and @{command "}"} explicitly open and close blocks. Any

    87   current facts pass through @{command "{"}'' unchanged, while @{command

    88   "}"}'' causes any result to be \<^emph>\<open>exported\<close> into the enclosing context. Thus

    89   fixed variables are generalized, assumptions discharged, and local

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

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

    92   forward reasoning --- in contrast to plain backward reasoning with the

    93   result exported at @{command "show"} time.

    94 \<close>

    95

    96

    97 subsection \<open>Omitting proofs\<close>

    98

    99 text \<open>

   100   \begin{matharray}{rcl}

   101     @{command_def "oops"} & : & \<open>proof \<rightarrow> local_theory | theory\<close> \\

   102   \end{matharray}

   103

   104   The @{command "oops"} command discontinues the current proof attempt, while

   105   considering the partial proof text as properly processed. This is

   106   conceptually quite different from faking'' actual proofs via @{command_ref

   107   "sorry"} (see \secref{sec:proof-steps}): @{command "oops"} does not observe

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

   109   Furthermore, @{command "oops"} does not produce any result theorem --- there

   110   is no intended claim to be able to complete the proof in any way.

   111

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

   113   \<^emph>\<open>within\<close> the system itself, in conjunction with the document preparation

   114   tools of Isabelle described in \chref{ch:document-prep}. Thus partial or

   115   even wrong proof attempts can be discussed in a logically sound manner. Note

   116   that the Isabelle {\LaTeX} macros can be easily adapted to print something

   117   like \<open>\<dots>\<close>'' instead of the keyword @{command "oops"}''.

   118 \<close>

   119

   120

   121 section \<open>Statements\<close>

   122

   123 subsection \<open>Context elements \label{sec:proof-context}\<close>

   124

   125 text \<open>

   126   \begin{matharray}{rcl}

   127     @{command_def "fix"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

   128     @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

   129     @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

   130     @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

   131   \end{matharray}

   132

   133   The logical proof context consists of fixed variables and assumptions. The

   134   former closely correspond to Skolem constants, or meta-level universal

   135   quantification as provided by the Isabelle/Pure logical framework.

   136   Introducing some \<^emph>\<open>arbitrary, but fixed\<close> variable via @{command

   137   "fix"}~\<open>x\<close>'' results in a local value that may be used in the subsequent

   138   proof as any other variable or constant. Furthermore, any result \<open>\<turnstile> \<phi>[x]\<close>

   139   exported from the context will be universally closed wrt.\ \<open>x\<close> at the

   140   outermost level: \<open>\<turnstile> \<And>x. \<phi>[x]\<close> (this is expressed in normal form using

   141   Isabelle's meta-variables).

   142

   143   Similarly, introducing some assumption \<open>\<chi>\<close> has two effects. On the one hand,

   144   a local theorem is created that may be used as a fact in subsequent proof

   145   steps. On the other hand, any result \<open>\<chi> \<turnstile> \<phi>\<close> exported from the context

   146   becomes conditional wrt.\ the assumption: \<open>\<turnstile> \<chi> \<Longrightarrow> \<phi>\<close>. Thus, solving an

   147   enclosing goal using such a result would basically introduce a new subgoal

   148   stemming from the assumption. How this situation is handled depends on the

   149   version of assumption command used: while @{command "assume"} insists on

   150   solving the subgoal by unification with some premise of the goal, @{command

   151   "presume"} leaves the subgoal unchanged in order to be proved later by the

   152   user.

   153

   154   Local definitions, introduced by \<^theory_text>\<open>define x where x = t\<close>'', are achieved

   155   by combining @{command "fix"}~\<open>x\<close>'' with another version of assumption

   156   that causes any hypothetical equation \<open>x \<equiv> t\<close> to be eliminated by the

   157   reflexivity rule. Thus, exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>

   158   \<phi>[t]\<close>.

   159

   160   @{rail \<open>

   161     @@{command fix} @{syntax vars}

   162     ;

   163     (@@{command assume} | @@{command presume}) concl prems @{syntax for_fixes}

   164     ;

   165     concl: (@{syntax props} + @'and')

   166     ;

   167     prems: (@'if' (@{syntax props'} + @'and'))?

   168     ;

   169     @@{command define} @{syntax vars} @'where'

   170       (@{syntax props} + @'and') @{syntax for_fixes}

   171   \<close>}

   172

   173   \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary,

   174   but fixed\<close>.

   175

   176   \<^descr> @{command "assume"}~\<open>a: \<phi>\<close> and @{command "presume"}~\<open>a: \<phi>\<close> introduce a

   177   local fact \<open>\<phi> \<turnstile> \<phi>\<close> by assumption. Subsequent results applied to an enclosing

   178   goal (e.g.\ by @{command_ref "show"}) are handled as follows: @{command

   179   "assume"} expects to be able to unify with existing premises in the goal,

   180   while @{command "presume"} leaves \<open>\<phi>\<close> as new subgoals.

   181

   182   Several lists of assumptions may be given (separated by @{keyword_ref

   183   "and"}; the resulting list of current facts consists of all of these

   184   concatenated.

   185

   186   A structured assumption like \<^theory_text>\<open>assume "B x" if "A x" for x\<close> is equivalent to

   187   \<^theory_text>\<open>assume "\<And>x. A x \<Longrightarrow> B x"\<close>, but vacuous quantification is avoided: a

   188   for-context only effects propositions according to actual use of variables.

   189

   190   \<^descr> \<^theory_text>\<open>define x where "x = t"\<close> introduces a local (non-polymorphic) definition.

   191   In results that are exported from the context, \<open>x\<close> is replaced by \<open>t\<close>.

   192

   193   Internally, equational assumptions are added to the context in Pure form,

   194   using \<open>x \<equiv> t\<close> instead of \<open>x = t\<close> or \<open>x \<longleftrightarrow> t\<close> from the object-logic. When

   195   exporting results from the context, \<open>x\<close> is generalized and the assumption

   196   discharged by reflexivity, causing the replacement by \<open>t\<close>.

   197

   198   The default name for the definitional fact is \<open>x_def\<close>. Several simultaneous

   199   definitions may be given as well, with a collective default name.

   200

   201   \<^medskip>

   202   It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f

   203   :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>.

   204 \<close>

   205

   206

   207 subsection \<open>Term abbreviations \label{sec:term-abbrev}\<close>

   208

   209 text \<open>

   210   \begin{matharray}{rcl}

   211     @{command_def "let"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

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

   213   \end{matharray}

   214

   215   Abbreviations may be either bound by explicit @{command "let"}~\<open>p \<equiv> t\<close>

   216   statements, or by annotating assumptions or goal statements with a list of

   217   patterns \<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>''. In both cases, higher-order matching is

   218   invoked to bind extra-logical term variables, which may be either named

   219   schematic variables of the form \<open>?x\<close>, or nameless dummies @{variable _}''

   220   (underscore). Note that in the @{command "let"} form the patterns occur on

   221   the left-hand side, while the @{keyword "is"} patterns are in postfix

   222   position.

   223

   224   Polymorphism of term bindings is handled in Hindley-Milner style, similar to

   225   ML. Type variables referring to local assumptions or open goal statements

   226   are \<^emph>\<open>fixed\<close>, while those of finished results or bound by @{command "let"}

   227   may occur in \<^emph>\<open>arbitrary\<close> instances later. Even though actual polymorphism

   228   should be rarely used in practice, this mechanism is essential to achieve

   229   proper incremental type-inference, as the user proceeds to build up the Isar

   230   proof text from left to right.

   231

   232   \<^medskip>

   233   Term abbreviations are quite different from local definitions as introduced

   234   via @{command "define"} (see \secref{sec:proof-context}). The latter are

   235   visible within the logic as actual equations, while abbreviations disappear

   236   during the input process just after type checking. Also note that @{command

   237   "define"} does not support polymorphism.

   238

   239   @{rail \<open>

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

   241   \<close>}

   242

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

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

   245

   246     \<^descr> \<^theory_text>\<open>let p\<^sub>1 = t\<^sub>1 and \<dots> p\<^sub>n = t\<^sub>n\<close> binds any text variables in patterns

   247     \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous higher-order matching against terms \<open>t\<^sub>1, \<dots>,

   248     t\<^sub>n\<close>.

   249

   250     \<^descr> \<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but matches \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close>

   251     against the preceding statement. Also note that @{keyword "is"} is not a

   252     separate command, but part of others (such as @{command "assume"},

   253     @{command "have"} etc.).

   254

   255   Some \<^emph>\<open>implicit\<close> term abbreviations\index{term abbreviations} for goals and

   256   facts are available as well. For any open goal, @{variable_ref thesis}

   257   refers to its object-level statement, abstracted over any meta-level

   258   parameters (if present). Likewise, @{variable_ref this} is bound for fact

   259   statements resulting from assumptions or finished goals. In case @{variable

   260   this} refers to an object-logic statement that is an application \<open>f t\<close>, then

   261   \<open>t\<close> is bound to the special text variable @{variable "\<dots>"}'' (three dots).

   262   The canonical application of this convenience are calculational proofs (see

   263   \secref{sec:calculation}).

   264 \<close>

   265

   266

   267 subsection \<open>Facts and forward chaining \label{sec:proof-facts}\<close>

   268

   269 text \<open>

   270   \begin{matharray}{rcl}

   271     @{command_def "note"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

   272     @{command_def "then"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

   273     @{command_def "from"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

   274     @{command_def "with"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

   275     @{command_def "using"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\

   276     @{command_def "unfolding"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\

   277     @{method_def "use"} & : & \<open>method\<close> \\

   278     @{fact_def "method_facts"} & : & \<open>fact\<close> \\

   279   \end{matharray}

   280

   281   New facts are established either by assumption or proof of local statements.

   282   Any fact will usually be involved in further proofs, either as explicit

   283   arguments of proof methods, or when forward chaining towards the next goal

   284   via @{command "then"} (and variants); @{command "from"} and @{command

   285   "with"} are composite forms involving @{command "note"}. The @{command

   286   "using"} elements augments the collection of used facts \<^emph>\<open>after\<close> a goal has

   287   been stated. Note that the special theorem name @{fact_ref this} refers to

   288   the most recently established facts, but only \<^emph>\<open>before\<close> issuing a follow-up

   289   claim.

   290

   291   @{rail \<open>

   292     @@{command note} (@{syntax thmdef}? @{syntax thms} + @'and')

   293     ;

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

   295       (@{syntax thms} + @'and')

   296     ;

   297     @{method use} @{syntax thms} @'in' @{syntax method}

   298   \<close>}

   299

   300   \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>,

   301   binding the result as \<open>a\<close>. Note that attributes may be involved as well,

   302   both on the left and right hand sides.

   303

   304   \<^descr> @{command "then"} indicates forward chaining by the current facts in order

   305   to establish the goal to be claimed next. The initial proof method invoked

   306   to refine that will be offered the facts to do anything appropriate'' (see

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

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

   309   than an introduction. Automatic methods usually insert the facts into the

   310   goal state before operation. This provides a simple scheme to control

   311   relevance of facts in automated proof search.

   312

   313   \<^descr> @{command "from"}~\<open>b\<close> abbreviates @{command "note"}~\<open>b\<close>~@{command

   314   "then"}''; thus @{command "then"} is equivalent to @{command

   315   "from"}~\<open>this\<close>''.

   316

   317   \<^descr> @{command "with"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> abbreviates @{command "from"}~\<open>b\<^sub>1 \<dots> b\<^sub>n

   318   \<AND> this\<close>''; thus the forward chaining is from earlier facts together

   319   with the current ones.

   320

   321   \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts to be used by a

   322   subsequent refinement step (such as @{command_ref "apply"} or @{command_ref

   323   "proof"}).

   324

   325   \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command

   326   "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the goal

   327   state and facts. See also the proof method @{method_ref unfold}.

   328

   329   \<^descr> \<^theory_text>\<open>(use b\<^sub>1 \<dots> b\<^sub>n in method)\<close> uses the facts in the given method

   330   expression. The facts provided by the proof state (via @{command "using"}

   331   etc.) are ignored, but it is possible to refer to @{fact method_facts}

   332   explicitly.

   333

   334   \<^descr> @{fact method_facts} is a dynamic fact that refers to the currently used

   335   facts of the goal state.

   336

   337

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

   339   at all. Thus @{command "from"}~\<open>nothing\<close>'' has no effect apart from

   340   entering \<open>prove(chain)\<close> mode, since @{fact_ref nothing} is bound to the

   341   empty list of theorems.

   342

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

   344   facts to be given in their proper order, corresponding to a prefix of the

   345   premises of the rule involved. Note that positions may be easily skipped

   346   using something like @{command "from"}~\<open>_ \<AND> a \<AND> b\<close>, for example.

   347   This involves the trivial rule \<open>PROP \<psi> \<Longrightarrow> PROP \<psi>\<close>, which is bound in

   348   Isabelle/Pure as @{fact_ref "_"}'' (underscore).

   349

   350   Automated methods (such as @{method simp} or @{method auto}) just insert any

   351   given facts before their usual operation. Depending on the kind of procedure

   352   involved, the order of facts is less significant here.

   353 \<close>

   354

   355

   356 subsection \<open>Goals \label{sec:goals}\<close>

   357

   358 text \<open>

   359   \begin{matharray}{rcl}

   360     @{command_def "lemma"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

   361     @{command_def "theorem"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

   362     @{command_def "corollary"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

   363     @{command_def "proposition"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

   364     @{command_def "schematic_goal"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

   365     @{command_def "have"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\

   366     @{command_def "show"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\

   367     @{command_def "hence"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\

   368     @{command_def "thus"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\

   369     @{command_def "print_statement"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   370   \end{matharray}

   371

   372   From a theory context, proof mode is entered by an initial goal command such

   373   as @{command "lemma"}. Within a proof context, new claims may be introduced

   374   locally; there are variants to interact with the overall proof structure

   375   specifically, such as @{command have} or @{command show}.

   376

   377   Goals may consist of multiple statements, resulting in a list of facts

   378   eventually. A pending multi-goal is internally represented as a meta-level

   379   conjunction (\<open>&&&\<close>), which is usually split into the corresponding number of

   380   sub-goals prior to an initial method application, via @{command_ref "proof"}

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

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

   383   \secref{sec:cases-induct} acts on multiple claims simultaneously.

   384

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

   386   merely consists of several simultaneous propositions (often just one). A

   387   long goal includes an explicit context specification for the subsequent

   388   conclusion, involving local parameters and assumptions. Here the role of

   389   each part of the statement is explicitly marked by separate keywords (see

   390   also \secref{sec:locale}); the local assumptions being introduced here are

   391   available as @{fact_ref assms} in the proof. Moreover, there are two kinds

   392   of conclusions: @{element_def "shows"} states several simultaneous

   393   propositions (essentially a big conjunction), while @{element_def "obtains"}

   394   claims several simultaneous simultaneous contexts of (essentially a big

   395   disjunction of eliminated parameters and assumptions, cf.\

   396   \secref{sec:obtain}).

   397

   398   @{rail \<open>

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

   400      @@{command proposition} | @@{command schematic_goal})

   401       (long_statement | short_statement)

   402     ;

   403     (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})

   404       stmt cond_stmt @{syntax for_fixes}

   405     ;

   406     @@{command print_statement} @{syntax modes}? @{syntax thms}

   407     ;

   408

   409     stmt: (@{syntax props} + @'and')

   410     ;

   411     cond_stmt: ((@'if' | @'when') stmt)?

   412     ;

   413     short_statement: stmt (@'if' stmt)? @{syntax for_fixes}

   414     ;

   415     long_statement: @{syntax thmdecl}? context conclusion

   416     ;

   417     context: (@{syntax_ref "includes"}?) (@{syntax context_elem} *)

   418     ;

   419     conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}

   420     ;

   421     @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')

   422     ;

   423     @{syntax_def obtain_case}: @{syntax vars} @'where'

   424       (@{syntax thmdecl}? (@{syntax prop}+) + @'and')

   425   \<close>}

   426

   427   \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with \<open>\<phi>\<close> as main goal,

   428   eventually resulting in some fact \<open>\<turnstile> \<phi>\<close> to be put back into the target

   429   context.

   430

   431   A @{syntax long_statement} may build up an initial proof context for the

   432   subsequent claim, potentially including local definitions and syntax; see

   433   also @{syntax "includes"} in \secref{sec:bundle} and @{syntax context_elem}

   434   in \secref{sec:locale}.

   435

   436   A @{syntax short_statement} consists of propositions as conclusion, with an

   437   option context of premises and parameters, via \<^verbatim>\<open>if\<close>/\<^verbatim>\<open>for\<close> in postfix

   438   notation, corresponding to \<^verbatim>\<open>assumes\<close>/\<^verbatim>\<open>fixes\<close> in the long prefix notation.

   439

   440   Local premises (if present) are called \<open>assms\<close>'' for @{syntax

   441   long_statement}, and \<open>that\<close>'' for @{syntax short_statement}.

   442

   443   \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command "proposition"}

   444   are the same as @{command "lemma"}. The different command names merely serve

   445   as a formal comment in the theory source.

   446

   447   \<^descr> @{command "schematic_goal"} is similar to @{command "theorem"}, but allows

   448   the statement to contain unbound schematic variables.

   449

   450   Under normal circumstances, an Isar proof text needs to specify claims

   451   explicitly. Schematic goals are more like goals in Prolog, where certain

   452   results are synthesized in the course of reasoning. With schematic

   453   statements, the inherent compositionality of Isar proofs is lost, which also

   454   impacts performance, because proof checking is forced into sequential mode.

   455

   456   \<^descr> @{command "have"}~\<open>a: \<phi>\<close> claims a local goal, eventually resulting in a

   457   fact within the current logical context. This operation is completely

   458   independent of any pending sub-goals of an enclosing goal statements, so

   459   @{command "have"} may be freely used for experimental exploration of

   460   potential results within a proof body.

   461

   462   \<^descr> @{command "show"}~\<open>a: \<phi>\<close> is like @{command "have"}~\<open>a: \<phi>\<close> plus a second

   463   stage to refine some pending sub-goal for each one of the finished result,

   464   after having been exported into the corresponding context (at the head of

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

   466

   467   To accommodate interactive debugging, resulting rules are printed before

   468   being applied internally. Even more, interactive execution of @{command

   469   "show"} predicts potential failure and displays the resulting error as a

   470   warning beforehand. Watch out for the following message:

   471   @{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>}

   472

   473   \<^descr> @{command "hence"} expands to @{command "then"}~@{command "have"}'' and

   474   @{command "thus"} expands to @{command "then"}~@{command "show"}''. These

   475   conflations are left-over from early history of Isar. The expanded syntax is

   476   more orthogonal and improves readability and maintainability of proofs.

   477

   478   \<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the current theory or

   479   proof context in long statement form, according to the syntax for @{command

   480   "lemma"} given above.

   481

   482

   483   Any goal statement causes some term abbreviations (such as @{variable_ref

   484   "?thesis"}) to be bound automatically, see also \secref{sec:term-abbrev}.

   485

   486   Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref

   487   "when"} define the special fact @{fact_ref that} to refer to these

   488   assumptions in the proof body. The user may provide separate names according

   489   to the syntax of the statement.

   490 \<close>

   491

   492

   493 section \<open>Calculational reasoning \label{sec:calculation}\<close>

   494

   495 text \<open>

   496   \begin{matharray}{rcl}

   497     @{command_def "also"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

   498     @{command_def "finally"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

   499     @{command_def "moreover"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

   500     @{command_def "ultimately"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

   501     @{command_def "print_trans_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   502     @{attribute trans} & : & \<open>attribute\<close> \\

   503     @{attribute sym} & : & \<open>attribute\<close> \\

   504     @{attribute symmetric} & : & \<open>attribute\<close> \\

   505   \end{matharray}

   506

   507   Calculational proof is forward reasoning with implicit application of

   508   transitivity rules (such those of \<open>=\<close>, \<open>\<le>\<close>, \<open><\<close>). Isabelle/Isar maintains an

   509   auxiliary fact register @{fact_ref calculation} for accumulating results

   510   obtained by transitivity composed with the current result. Command @{command

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

   512   "finally"} exhibits the final @{fact calculation} by forward chaining

   513   towards the next goal statement. Both commands require valid current facts,

   514   i.e.\ may occur only after commands that produce theorems such as @{command

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

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

   517   commands are similar to @{command "also"} and @{command "finally"}, but only

   518   collect further results in @{fact calculation} without applying any rules

   519   yet.

   520

   521   Also note that the implicit term abbreviation \<open>\<dots>\<close>'' has its canonical

   522   application with calculational proofs. It refers to the argument of the

   523   preceding statement. (The argument of a curried infix expression happens to

   524   be its right-hand side.)

   525

   526   Isabelle/Isar calculations are implicitly subject to block structure in the

   527   sense that new threads of calculational reasoning are commenced for any new

   528   block (as opened by a local goal, for example). This means that, apart from

   529   being able to nest calculations, there is no separate \<^emph>\<open>begin-calculation\<close>

   530   command required.

   531

   532   \<^medskip>

   533   The Isar calculation proof commands may be defined as follows:\<^footnote>\<open>We suppress

   534   internal bookkeeping such as proper handling of block-structure.\<close>

   535

   536   \begin{matharray}{rcl}

   537     @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\

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

   539     @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\[0.5ex]

   540     @{command "moreover"} & \equiv & @{command "note"}~\<open>calculation = calculation this\<close> \\

   541     @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~\<open>calculation\<close> \\

   542   \end{matharray}

   543

   544   @{rail \<open>

   545     (@@{command also} | @@{command finally}) ('(' @{syntax thms} ')')?

   546     ;

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

   548   \<close>}

   549

   550   \<^descr> @{command "also"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains the auxiliary @{fact

   551   calculation} register as follows. The first occurrence of @{command "also"}

   552   in some calculational thread initializes @{fact calculation} by @{fact

   553   this}. Any subsequent @{command "also"} on the same level of block-structure

   554   updates @{fact calculation} by some transitivity rule applied to @{fact

   555   calculation} and @{fact this} (in that order). Transitivity rules are picked

   556   from the current context, unless alternative rules are given as explicit

   557   arguments.

   558

   559   \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains @{fact calculation} in the

   560   same way as @{command "also"} and then concludes the current calculational

   561   thread. The final result is exhibited as fact for forward chaining towards

   562   the next goal. Basically, @{command "finally"} abbreviates @{command

   563   "also"}~@{command "from"}~@{fact calculation}. Typical idioms for concluding

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

   565   "show"}~\<open>?thesis\<close>~@{command "."}'' and @{command "finally"}~@{command

   566   "have"}~\<open>\<phi>\<close>~@{command "."}''.

   567

   568   \<^descr> @{command "moreover"} and @{command "ultimately"} are analogous to

   569   @{command "also"} and @{command "finally"}, but collect results only,

   570   without applying rules.

   571

   572   \<^descr> @{command "print_trans_rules"} prints the list of transitivity rules (for

   573   calculational commands @{command "also"} and @{command "finally"}) and

   574   symmetry rules (for the @{attribute symmetric} operation and single step

   575   elimination patters) of the current context.

   576

   577   \<^descr> @{attribute trans} declares theorems as transitivity rules.

   578

   579   \<^descr> @{attribute sym} declares symmetry rules, as well as @{attribute

   580   "Pure.elim"}\<open>?\<close> rules.

   581

   582   \<^descr> @{attribute symmetric} resolves a theorem with some rule declared as

   583   @{attribute sym} in the current context. For example, @{command

   584   "assume"}~\<open>[symmetric]: x = y\<close>'' produces a swapped fact derived from that

   585   assumption.

   586

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

   588   single-step elimination proof, such as @{command "assume"}~\<open>x =

   589   y\<close>~@{command "then"}~@{command "have"}~\<open>y = x\<close>~@{command ".."}''.

   590 \<close>

   591

   592

   593 section \<open>Refinement steps\<close>

   594

   595 subsection \<open>Proof method expressions \label{sec:proof-meth}\<close>

   596

   597 text \<open>

   598   Proof methods are either basic ones, or expressions composed of methods via

   599   \<^verbatim>\<open>,\<close>'' (sequential composition), \<^verbatim>\<open>;\<close>'' (structural composition),

   600   \<^verbatim>\<open>|\<close>'' (alternative choices), \<^verbatim>\<open>?\<close>'' (try), \<^verbatim>\<open>+\<close>'' (repeat at least

   601   once), \<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first \<open>n\<close> subgoals). In practice,

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

   603   name}~@{syntax args} specifications. Note that parentheses may be dropped

   604   for single method specifications (with no arguments). The syntactic

   605   precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close> \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low

   606   to high).

   607

   608   @{rail \<open>

   609     @{syntax_def method}:

   610       (@{syntax name} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')

   611     ;

   612     methods: (@{syntax name} @{syntax args} | @{syntax method}) + (',' | ';' | '|')

   613   \<close>}

   614

   615   Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but refer

   616   to the first subgoal or to all subgoals uniformly. Nonetheless, the

   617   subsequent mechanisms allow to imitate the effect of subgoal addressing that

   618   is known from ML tactics.

   619

   620   \<^medskip>

   621   Goal \<^emph>\<open>restriction\<close> means the proof state is wrapped-up in a way that

   622   certain subgoals are exposed, and other subgoals are parked'' elsewhere.

   623   Thus a proof method has no other chance than to operate on the subgoals that

   624   are presently exposed.

   625

   626   Structural composition \<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means that method \<open>m\<^sub>1\<close> is

   627   applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied

   628   consecutively with restriction to each subgoal that has newly emerged due to

   629   \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator @{ML_op THEN_ALL_NEW} in

   630   Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule

   631   r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.

   632

   633   Moreover, the explicit goal restriction operator \<open>[n]\<close>'' exposes only the

   634   first \<open>n\<close> subgoals (which need to exist), with default \<open>n = 1\<close>. For example,

   635   the method expression \<open>simp_all[3]\<close>'' simplifies the first three subgoals,

   636   while \<open>(rule r, simp_all)[]\<close>'' simplifies all new goals that emerge from

   637   applying rule \<open>r\<close> to the originally first one.

   638

   639   \<^medskip>

   640   Improper methods, notably tactic emulations, offer low-level goal addressing

   641   as explicit argument to the individual tactic being involved. Here \<open>[!]\<close>''

   642   refers to all goals, and \<open>[n-]\<close>'' to all goals starting from \<open>n\<close>.

   643

   644   @{rail \<open>

   645     @{syntax_def goal_spec}:

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

   647   \<close>}

   648 \<close>

   649

   650

   651 subsection \<open>Initial and terminal proof steps \label{sec:proof-steps}\<close>

   652

   653 text \<open>

   654   \begin{matharray}{rcl}

   655     @{command_def "proof"} & : & \<open>proof(prove) \<rightarrow> proof(state)\<close> \\

   656     @{command_def "qed"} & : & \<open>proof(state) \<rightarrow> proof(state) | local_theory | theory\<close> \\

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

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

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

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

   661     @{method_def standard} & : & \<open>method\<close> \\

   662   \end{matharray}

   663

   664   Arbitrary goal refinement via tactics is considered harmful. Structured

   665   proof composition in Isar admits proof methods to be invoked in two places

   666   only.

   667

   668     \<^enum> An \<^emph>\<open>initial\<close> refinement step @{command_ref "proof"}~\<open>m\<^sub>1\<close> reduces a

   669     newly stated goal to a number of sub-goals that are to be solved later.

   670     Facts are passed to \<open>m\<^sub>1\<close> for forward chaining, if so indicated by

   671     \<open>proof(chain)\<close> mode.

   672

   673     \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~\<open>m\<^sub>2\<close> is intended to

   674     solve remaining goals. No facts are passed to \<open>m\<^sub>2\<close>.

   675

   676   The only other (proper) way to affect pending goals in a proof body is by

   677   @{command_ref "show"}, which involves an explicit statement of what is to be

   678   solved eventually. Thus we avoid the fundamental problem of unstructured

   679   tactic scripts that consist of numerous consecutive goal transformations,

   680   with invisible effects.

   681

   682   \<^medskip>

   683   As a general rule of thumb for good proof style, initial proof methods

   684   should either solve the goal completely, or constitute some well-understood

   685   reduction to new sub-goals. Arbitrary automatic proof tools that are prone

   686   leave a large number of badly structured sub-goals are no help in continuing

   687   the proof document in an intelligible manner.

   688

   689   Unless given explicitly by the user, the default initial method is @{method

   690   standard}, which subsumes at least @{method_ref (Pure) rule} or its

   691   classical variant @{method_ref (HOL) rule}. These methods apply a single

   692   standard elimination or introduction rule according to the topmost logical

   693   connective involved. There is no separate default terminal method. Any

   694   remaining goals are always solved by assumption in the very last step.

   695

   696   @{rail \<open>

   697     @@{command proof} method?

   698     ;

   699     @@{command qed} method?

   700     ;

   701     @@{command "by"} method method?

   702     ;

   703     (@@{command "."} | @@{command ".."} | @@{command sorry})

   704   \<close>}

   705

   706   \<^descr> @{command "proof"}~\<open>m\<^sub>1\<close> refines the goal by proof method \<open>m\<^sub>1\<close>; facts for

   707   forward chaining are passed if so indicated by \<open>proof(chain)\<close> mode.

   708

   709   \<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by proof method \<open>m\<^sub>2\<close>

   710   and concludes the sub-proof by assumption. If the goal had been \<open>show\<close>, some

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

   712   \<^emph>\<open>exported\<close> into the enclosing goal context. Thus \<open>qed\<close> may fail for two

   713   reasons: either \<open>m\<^sub>2\<close> fails, or the resulting rule does not fit to any

   714   pending goal\<^footnote>\<open>This includes any additional strong'' assumptions as

   715   introduced by @{command "assume"}.\<close> of the enclosing context. Debugging such

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

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

   718   of @{command "assume"} by @{command "presume"}.

   719

   720   \<^descr> @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> is a \<^emph>\<open>terminal proof\<close>\index{proof!terminal}; it

   721   abbreviates @{command "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close>, but with

   722   backtracking across both methods. Debugging an unsuccessful @{command

   723   "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> command can be done by expanding its definition; in many

   724   cases @{command "proof"}~\<open>m\<^sub>1\<close> (or even \<open>apply\<close>~\<open>m\<^sub>1\<close>) is already sufficient

   725   to see the problem.

   726

   727   \<^descr> @{command ".."}'' is a \<^emph>\<open>standard proof\<close>\index{proof!standard}; it

   728   abbreviates @{command "by"}~\<open>standard\<close>.

   729

   730   \<^descr> @{command "."}'' is a \<^emph>\<open>trivial proof\<close>\index{proof!trivial}; it

   731   abbreviates @{command "by"}~\<open>this\<close>.

   732

   733   \<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake} pretending to

   734   solve the pending claim without further ado. This only works in interactive

   735   development, or if the @{attribute quick_and_dirty} is enabled. Facts

   736   emerging from fake proofs are not the real thing. Internally, the derivation

   737   object is tainted by an oracle invocation, which may be inspected via the

   738   theorem status @{cite "isabelle-implementation"}.

   739

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

   741   experimentation and top-down proof development.

   742

   743   \<^descr> @{method standard} refers to the default refinement step of some Isar

   744   language elements (notably @{command proof} and @{command ".."}''). It is

   745   \<^emph>\<open>dynamically scoped\<close>, so the behaviour depends on the application

   746   environment.

   747

   748   In Isabelle/Pure, @{method standard} performs elementary introduction~/

   749   elimination steps (@{method_ref (Pure) rule}), introduction of type classes

   750   (@{method_ref intro_classes}) and locales (@{method_ref intro_locales}).

   751

   752   In Isabelle/HOL, @{method standard} also takes classical rules into account

   753   (cf.\ \secref{sec:classical}).

   754 \<close>

   755

   756

   757 subsection \<open>Fundamental methods and attributes \label{sec:pure-meth-att}\<close>

   758

   759 text \<open>

   760   The following proof methods and attributes refer to basic logical operations

   761   of Isar. Further methods and attributes are provided by several generic and

   762   object-logic specific tools and packages (see \chref{ch:gen-tools} and

   763   \partref{part:hol}).

   764

   765   \begin{matharray}{rcl}

   766     @{command_def "print_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\[0.5ex]

   767     @{method_def "-"} & : & \<open>method\<close> \\

   768     @{method_def "goal_cases"} & : & \<open>method\<close> \\

   769     @{method_def "fact"} & : & \<open>method\<close> \\

   770     @{method_def "assumption"} & : & \<open>method\<close> \\

   771     @{method_def "this"} & : & \<open>method\<close> \\

   772     @{method_def (Pure) "rule"} & : & \<open>method\<close> \\

   773     @{attribute_def (Pure) "intro"} & : & \<open>attribute\<close> \\

   774     @{attribute_def (Pure) "elim"} & : & \<open>attribute\<close> \\

   775     @{attribute_def (Pure) "dest"} & : & \<open>attribute\<close> \\

   776     @{attribute_def (Pure) "rule"} & : & \<open>attribute\<close> \\[0.5ex]

   777     @{attribute_def "OF"} & : & \<open>attribute\<close> \\

   778     @{attribute_def "of"} & : & \<open>attribute\<close> \\

   779     @{attribute_def "where"} & : & \<open>attribute\<close> \\

   780   \end{matharray}

   781

   782   @{rail \<open>

   783     @@{method goal_cases} (@{syntax name}*)

   784     ;

   785     @@{method fact} @{syntax thms}?

   786     ;

   787     @@{method (Pure) rule} @{syntax thms}?

   788     ;

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

   790       ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thms}

   791     ;

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

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

   794     ;

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

   796     ;

   797     @@{attribute OF} @{syntax thms}

   798     ;

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

   800     ;

   801     @@{attribute "where"} @{syntax named_insts} @{syntax for_fixes}

   802   \<close>}

   803

   804   \<^descr> @{command "print_rules"} prints rules declared via attributes @{attribute

   805   (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure) dest} of

   806   Isabelle/Pure.

   807

   808   See also the analogous @{command "print_claset"} command for similar rule

   809   declarations of the classical reasoner (\secref{sec:classical}).

   810

   811   \<^descr> @{method "-"}'' (minus) inserts the forward chaining facts as premises

   812   into the goal, and nothing else.

   813

   814   Note that command @{command_ref "proof"} without any method actually

   815   performs a single reduction step using the @{method_ref (Pure) rule} method;

   816   thus a plain \<^emph>\<open>do-nothing\<close> proof step would be @{command "proof"}~\<open>-\<close>''

   817   rather than @{command "proof"} alone.

   818

   819   \<^descr> @{method "goal_cases"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> turns the current subgoals into cases

   820   within the context (see also \secref{sec:cases-induct}). The specified case

   821   names are used if present; otherwise cases are numbered starting from 1.

   822

   823   Invoking cases in the subsequent proof body via the @{command_ref case}

   824   command will @{command fix} goal parameters, @{command assume} goal

   825   premises, and @{command let} variable @{variable_ref ?case} refer to the

   826   conclusion.

   827

   828   \<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or

   829   implicitly from the current proof context) modulo unification of schematic

   830   type and term variables. The rule structure is not taken into account, i.e.\

   831   meta-level implication is considered atomic. This is the same principle

   832   underlying literal facts (cf.\ \secref{sec:syn-att}): @{command

   833   "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to @{command

   834   "note"}~\<^verbatim>\<open>\<close>\<open>\<phi>\<close>\<^verbatim>\<open>\<close>'' provided that \<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close>

   835   in the proof context.

   836

   837   \<^descr> @{method assumption} solves some goal by a single assumption step. All

   838   given facts are guaranteed to participate in the refinement; this means

   839   there may be only 0 or 1 in the first place. Recall that @{command "qed"}

   840   (\secref{sec:proof-steps}) already concludes any remaining sub-goals by

   841   assumption, so structured proofs usually need not quote the @{method

   842   assumption} method at all.

   843

   844   \<^descr> @{method this} applies all of the current facts directly as rules. Recall

   845   that @{command "."}'' (dot) abbreviates @{command "by"}~\<open>this\<close>''.

   846

   847   \<^descr> @{method (Pure) rule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some rule given as argument in

   848   backward manner; facts are used to reduce the rule before applying it to the

   849   goal. Thus @{method (Pure) rule} without facts is plain introduction, while

   850   with facts it becomes elimination.

   851

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

   853   appropriate rules automatically, as declared in the current context using

   854   the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure)

   855   dest} attributes (see below). This is included in the standard behaviour of

   856   @{command "proof"} and @{command ".."}'' (double-dot) steps (see

   857   \secref{sec:proof-steps}).

   858

   859   \<^descr> @{attribute (Pure) intro}, @{attribute (Pure) elim}, and @{attribute

   860   (Pure) dest} declare introduction, elimination, and destruct rules, to be

   861   used with method @{method (Pure) rule}, and similar tools. Note that the

   862   latter will ignore rules declared with \<open>?\<close>'', while \<open>!\<close>'' are used most

   863   aggressively.

   864

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

   866   variants of these attributes; use qualified names to access the present

   867   versions of Isabelle/Pure, i.e.\ @{attribute (Pure) "Pure.intro"}.

   868

   869   \<^descr> @{attribute (Pure) rule}~\<open>del\<close> undeclares introduction, elimination, or

   870   destruct rules.

   871

   872   \<^descr> @{attribute OF}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some theorem to all of the given rules

   873   \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> in canonical right-to-left order, which means that premises

   874   stemming from the \<open>a\<^sub>i\<close> emerge in parallel in the result, without

   875   interfering with each other. In many practical situations, the \<open>a\<^sub>i\<close> do not

   876   have premises themselves, so \<open>rule [OF a\<^sub>1 \<dots> a\<^sub>n]\<close> can be actually read as

   877   functional application (modulo unification).

   878

   879   Argument positions may be effectively skipped by using \<open>_\<close>'' (underscore),

   880   which refers to the propositional identity rule in the Pure theory.

   881

   882   \<^descr> @{attribute of}~\<open>t\<^sub>1 \<dots> t\<^sub>n\<close> performs positional instantiation of term

   883   variables. The terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> are substituted for any schematic

   884   variables occurring in a theorem from left to right; \<open>_\<close>'' (underscore)

   885   indicates to skip a position. Arguments following a \<open>concl:\<close>''

   886   specification refer to positions of the conclusion of a rule.

   887

   888   An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified:

   889   the instantiated theorem is exported, and these variables become schematic

   890   (usually with some shifting of indices).

   891

   892   \<^descr> @{attribute "where"}~\<open>x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n\<close> performs named

   893   instantiation of schematic type and term variables occurring in a theorem.

   894   Schematic variables have to be specified on the left-hand side (e.g.\

   895   \<open>?x1.3\<close>). The question mark may be omitted if the variable name is a plain

   896   identifier without index. As type instantiations are inferred from term

   897   instantiations, explicit type instantiations are seldom necessary.

   898

   899   An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified

   900   as for @{attribute "of"} above.

   901 \<close>

   902

   903

   904 subsection \<open>Defining proof methods\<close>

   905

   906 text \<open>

   907   \begin{matharray}{rcl}

   908     @{command_def "method_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

   909   \end{matharray}

   910

   911   @{rail \<open>

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

   913   \<close>}

   914

   915   \<^descr> @{command "method_setup"}~\<open>name = text description\<close> defines a proof method

   916   in the current context. The given \<open>text\<close> has to be an ML expression of type

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

   918   parsers defined in structure @{ML_structure Args} and @{ML_structure

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

   920   SIMPLE_METHOD} to turn certain tactic forms into official proof methods; the

   921   primed versions refer to tactics with explicit goal addressing.

   922

   923   Here are some example method definitions:

   924 \<close>

   925

   926 (*<*)experiment begin(*>*)

   927   method_setup my_method1 =

   928     \<open>Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))\<close>

   929     "my first method (without any arguments)"

   930

   931   method_setup my_method2 =

   932     \<open>Scan.succeed (fn ctxt: Proof.context =>

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

   934     "my second method (with context)"

   935

   936   method_setup my_method3 =

   937     \<open>Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>

   938       SIMPLE_METHOD' (fn i: int => no_tac))\<close>

   939     "my third method (with theorem arguments and context)"

   940 (*<*)end(*>*)

   941

   942

   943 section \<open>Proof by cases and induction \label{sec:cases-induct}\<close>

   944

   945 subsection \<open>Rule contexts\<close>

   946

   947 text \<open>

   948   \begin{matharray}{rcl}

   949     @{command_def "case"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

   950     @{command_def "print_cases"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   951     @{attribute_def case_names} & : & \<open>attribute\<close> \\

   952     @{attribute_def case_conclusion} & : & \<open>attribute\<close> \\

   953     @{attribute_def params} & : & \<open>attribute\<close> \\

   954     @{attribute_def consumes} & : & \<open>attribute\<close> \\

   955   \end{matharray}

   956

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

   958   elements like @{command "fix"}, @{command "assume"}, @{command "let"} (see

   959   \secref{sec:proof-context}). This is adequate for plain natural deduction,

   960   but easily becomes unwieldy in concrete verification tasks, which typically

   961   involve big induction rules with several cases.

   962

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

   964   context symbolically: certain proof methods provide an environment of named

   965   cases'' of the form \<open>c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n\<close>; the effect of

   966   @{command "case"}~\<open>c\<close>'' is then equivalent to @{command "fix"}~\<open>x\<^sub>1 \<dots>

   967   x\<^sub>m\<close>~@{command "assume"}~\<open>c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Term bindings may be covered as

   968   well, notably @{variable ?case} for the main conclusion.

   969

   970   By default, the terminology'' \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of a case value is marked as

   971   hidden, i.e.\ there is no way to refer to such parameters in the subsequent

   972   proof text. After all, original rule parameters stem from somewhere outside

   973   of the current proof text. By using the explicit form @{command

   974   "case"}~\<open>(c y\<^sub>1 \<dots> y\<^sub>m)\<close>'' instead, the proof author is able to chose local

   975   names that fit nicely into the current context.

   976

   977   \<^medskip>

   978   It is important to note that proper use of @{command "case"} does not

   979   provide means to peek at the current goal state, which is not directly

   980   observable in Isar! Nonetheless, goal refinement commands do provide named

   981   cases \<open>goal\<^sub>i\<close> for each subgoal \<open>i = 1, \<dots>, n\<close> of the resulting goal state.

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

   983   internal tactical machinery intrude the proof text. In particular, parameter

   984   names stemming from the left-over of automated reasoning tools are usually

   985   quite unpredictable.

   986

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

   988   elimination or induction rules, which in turn are derived from previous

   989   theory specifications in a canonical way (say from @{command "inductive"}

   990   definitions).

   991

   992   \<^medskip>

   993   Proper cases are only available if both the proof method and the rules

   994   involved support this. By using appropriate attributes, case names,

   995   conclusions, and parameters may be also declared by hand. Thus variant

   996   versions of rules that have been derived manually become ready to use in

   997   advanced case analysis later.

   998

   999   @{rail \<open>

  1000     @@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')')

  1001     ;

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

  1003     ;

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

  1005     ;

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

  1007     ;

  1008     @@{attribute consumes} @{syntax int}?

  1009   \<close>}

  1010

  1011   \<^descr> @{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close> invokes a named local context \<open>c:

  1012   x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m\<close>, as provided by an appropriate proof method (such

  1013   as @{method_ref cases} and @{method_ref induct}). The command @{command

  1014   "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>'' abbreviates @{command "fix"}~\<open>x\<^sub>1 \<dots>

  1015   x\<^sub>m\<close>~@{command "assume"}~\<open>a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Each local fact is qualified by

  1016   the prefix \<open>a\<close>, and all such facts are collectively bound to the name \<open>a\<close>.

  1017

  1018   The fact name is specification \<open>a\<close> is optional, the default is to re-use

  1019   \<open>c\<close>. So @{command "case"}~\<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> is the same as @{command

  1020   "case"}~\<open>c: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>.

  1021

  1022   \<^descr> @{command "print_cases"} prints all local contexts of the current state,

  1023   using Isar proof language notation.

  1024

  1025   \<^descr> @{attribute case_names}~\<open>c\<^sub>1 \<dots> c\<^sub>k\<close> declares names for the local contexts

  1026   of premises of a theorem; \<open>c\<^sub>1, \<dots>, c\<^sub>k\<close> refers to the \<^emph>\<open>prefix\<close> of the list

  1027   of premises. Each of the cases \<open>c\<^sub>i\<close> can be of the form \<open>c[h\<^sub>1 \<dots> h\<^sub>n]\<close> where

  1028   the \<open>h\<^sub>1 \<dots> h\<^sub>n\<close> are the names of the hypotheses in case \<open>c\<^sub>i\<close> from left to

  1029   right.

  1030

  1031   \<^descr> @{attribute case_conclusion}~\<open>c d\<^sub>1 \<dots> d\<^sub>k\<close> declares names for the

  1032   conclusions of a named premise \<open>c\<close>; here \<open>d\<^sub>1, \<dots>, d\<^sub>k\<close> refers to the prefix

  1033   of arguments of a logical formula built by nesting a binary connective

  1034   (e.g.\ \<open>\<or>\<close>).

  1035

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

  1037   already provide a default name for the conclusion as a whole. The need to

  1038   name subformulas only arises with cases that split into several sub-cases,

  1039   as in common co-induction rules.

  1040

  1041   \<^descr> @{attribute params}~\<open>p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n\<close> renames the innermost

  1042   parameters of premises \<open>1, \<dots>, n\<close> of some theorem. An empty list of names may

  1043   be given to skip positions, leaving the present parameters unchanged.

  1044

  1045   Note that the default usage of case rules does \<^emph>\<open>not\<close> directly expose

  1046   parameters to the proof context.

  1047

  1048   \<^descr> @{attribute consumes}~\<open>n\<close> declares the number of major premises'' of a

  1049   rule, i.e.\ the number of facts to be consumed when it is applied by an

  1050   appropriate proof method. The default value of @{attribute consumes} is \<open>n =

  1051   1\<close>, which is appropriate for the usual kind of cases and induction rules for

  1052   inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any

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

  1054   consumes}~\<open>0\<close> had been specified.

  1055

  1056   A negative \<open>n\<close> is interpreted relatively to the total number of premises of

  1057   the rule in the target context. Thus its absolute value specifies the

  1058   remaining number of premises, after subtracting the prefix of major premises

  1059   as indicated above. This form of declaration has the technical advantage of

  1060   being stable under more morphisms, notably those that export the result from

  1061   a nested @{command_ref context} with additional assumptions.

  1062

  1063   Note that explicit @{attribute consumes} declarations are only rarely

  1064   needed; this is already taken care of automatically by the higher-level

  1065   @{attribute cases}, @{attribute induct}, and @{attribute coinduct}

  1066   declarations.

  1067 \<close>

  1068

  1069

  1070 subsection \<open>Proof methods\<close>

  1071

  1072 text \<open>

  1073   \begin{matharray}{rcl}

  1074     @{method_def cases} & : & \<open>method\<close> \\

  1075     @{method_def induct} & : & \<open>method\<close> \\

  1076     @{method_def induction} & : & \<open>method\<close> \\

  1077     @{method_def coinduct} & : & \<open>method\<close> \\

  1078   \end{matharray}

  1079

  1080   The @{method cases}, @{method induct}, @{method induction}, and @{method

  1081   coinduct} methods provide a uniform interface to common proof techniques

  1082   over datatypes, inductive predicates (or sets), recursive functions etc. The

  1083   corresponding rules may be specified and instantiated in a casual manner.

  1084   Furthermore, these methods provide named local contexts that may be invoked

  1085   via the @{command "case"} proof command within the subsequent proof text.

  1086   This accommodates compact proof texts even when reasoning about large

  1087   specifications.

  1088

  1089   The @{method induct} method also provides some additional infrastructure in

  1090   order to be applicable to structure statements (either using explicit

  1091   meta-level connectives, or including facts and parameters separately). This

  1092   avoids cumbersome encoding of strengthened'' inductive statements within

  1093   the object-logic.

  1094

  1095   Method @{method induction} differs from @{method induct} only in the names

  1096   of the facts in the local context invoked by the @{command "case"} command.

  1097

  1098   @{rail \<open>

  1099     @@{method cases} ('(' 'no_simp' ')')? \<newline>

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

  1101     ;

  1102     (@@{method induct} | @@{method induction})

  1103       ('(' 'no_simp' ')')? (definsts * @'and') \<newline> arbitrary? taking? rule?

  1104     ;

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

  1106     ;

  1107

  1108     rule: ('type' | 'pred' | 'set') ':' (@{syntax name} +) | 'rule' ':' (@{syntax thm} +)

  1109     ;

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

  1111     ;

  1112     definsts: ( definst * )

  1113     ;

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

  1115     ;

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

  1117   \<close>}

  1118

  1119   \<^descr> @{method cases}~\<open>insts R\<close> applies method @{method rule} with an

  1120   appropriate case distinction theorem, instantiated to the subjects \<open>insts\<close>.

  1121   Symbolic case names are bound according to the rule's local contexts.

  1122

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

  1124   passed to the @{method cases} method:

  1125

  1126   \<^medskip>

  1127   \begin{tabular}{llll}

  1128     facts           &                 & arguments   & rule \\\hline

  1129     \<open>\<turnstile> R\<close>   & @{method cases} &             & implicit rule \<open>R\<close> \\

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

  1131                     & @{method cases} & \<open>t\<close>   & datatype exhaustion (type of \<open>t\<close>) \\

  1132     \<open>\<turnstile> A t\<close> & @{method cases} & \<open>\<dots>\<close> & inductive predicate/set elimination (of \<open>A\<close>) \\

  1133     \<open>\<dots>\<close>     & @{method cases} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\

  1134   \end{tabular}

  1135   \<^medskip>

  1136

  1137   Several instantiations may be given, referring to the \<^emph>\<open>suffix\<close> of premises

  1138   of the case rule; within each premise, the \<^emph>\<open>prefix\<close> of variables is

  1139   instantiated. In most situations, only a single term needs to be specified;

  1140   this refers to the first variable of the last premise (it is usually the

  1141   same for all cases). The \<open>(no_simp)\<close> option can be used to disable

  1142   pre-simplification of cases (see the description of @{method induct} below

  1143   for details).

  1144

  1145   \<^descr> @{method induct}~\<open>insts R\<close> and @{method induction}~\<open>insts R\<close> are analogous

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

  1147   determined as follows:

  1148

  1149   \<^medskip>

  1150   \begin{tabular}{llll}

  1151     facts           &                  & arguments            & rule \\\hline

  1152                     & @{method induct} & \<open>P x\<close>        & datatype induction (type of \<open>x\<close>) \\

  1153     \<open>\<turnstile> A x\<close> & @{method induct} & \<open>\<dots>\<close>          & predicate/set induction (of \<open>A\<close>) \\

  1154     \<open>\<dots>\<close>     & @{method induct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\

  1155   \end{tabular}

  1156   \<^medskip>

  1157

  1158   Several instantiations may be given, each referring to some part of a mutual

  1159   inductive definition or datatype --- only related partial induction rules

  1160   may be used together, though. Any of the lists of terms \<open>P, x, \<dots>\<close> refers to

  1161   the \<^emph>\<open>suffix\<close> of variables present in the induction rule. This enables the

  1162   writer to specify only induction variables, or both predicates and

  1163   variables, for example.

  1164

  1165   Instantiations may be definitional: equations \<open>x \<equiv> t\<close> introduce local

  1166   definitions, which are inserted into the claim and discharged after applying

  1167   the induction rule. Equalities reappear in the inductive cases, but have

  1168   been transformed according to the induction principle being involved here.

  1169   In order to achieve practically useful induction hypotheses, some variables

  1170   occurring in \<open>t\<close> need to be fixed (see below). Instantiations of the form

  1171   \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a shorthand for \<open>x \<equiv> t\<close>,

  1172   where \<open>x\<close> is a fresh variable. If this is not intended, \<open>t\<close> has to be

  1173   enclosed in parentheses. By default, the equalities generated by

  1174   definitional instantiations are pre-simplified using a specific set of

  1175   rules, usually consisting of distinctness and injectivity theorems for

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

  1177   inductive case to disappear, or may even completely delete some of the

  1178   inductive cases, if one of the equalities occurring in their premises can be

  1179   simplified to \<open>False\<close>. The \<open>(no_simp)\<close> option can be used to disable

  1180   pre-simplification. Additional rules to be used in pre-simplification can be

  1181   declared using the @{attribute_def induct_simp} attribute.

  1182

  1183   The optional \<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>'' specification generalizes variables

  1184   \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. One can

  1185   separate variables by \<open>and\<close>'' to generalize them in other goals then the

  1186   first. Thus induction hypotheses may become sufficiently general to get the

  1187   proof through. Together with definitional instantiations, one may

  1188   effectively perform induction over expressions of a certain structure.

  1189

  1190   The optional \<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification provides additional

  1191   instantiations of a prefix of pending variables in the rule. Such schematic

  1192   induction rules rarely occur in practice, though.

  1193

  1194   \<^descr> @{method coinduct}~\<open>inst R\<close> is analogous to the @{method induct} method,

  1195   but refers to coinduction rules, which are determined as follows:

  1196

  1197   \<^medskip>

  1198   \begin{tabular}{llll}

  1199     goal          &                    & arguments & rule \\\hline

  1200                   & @{method coinduct} & \<open>x\<close> & type coinduction (type of \<open>x\<close>) \\

  1201     \<open>A x\<close> & @{method coinduct} & \<open>\<dots>\<close> & predicate/set coinduction (of \<open>A\<close>) \\

  1202     \<open>\<dots>\<close>   & @{method coinduct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\

  1203   \end{tabular}

  1204   \<^medskip>

  1205

  1206   Coinduction is the dual of induction. Induction essentially eliminates \<open>A x\<close>

  1207   towards a generic result \<open>P x\<close>, while coinduction introduces \<open>A x\<close> starting

  1208   with \<open>B x\<close>, for a suitable bisimulation'' \<open>B\<close>. The cases of a coinduct

  1209   rule are typically named after the predicates or sets being covered, while

  1210   the conclusions consist of several alternatives being named after the

  1211   individual destructor patterns.

  1212

  1213   The given instantiation refers to the \<^emph>\<open>suffix\<close> of variables occurring in

  1214   the rule's major premise, or conclusion if unavailable. An additional

  1215   \<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification may be required in order to specify

  1216   the bisimulation to be used in the coinduction step.

  1217

  1218

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

  1220   instantiated rule as given in the text. Beyond that, the @{method induct}

  1221   and @{method coinduct} methods guess further instantiations from the goal

  1222   specification itself. Any persisting unresolved schematic variables of the

  1223   resulting rule will render the the corresponding case invalid. The term

  1224   binding @{variable ?case} for the conclusion will be provided with each

  1225   case, provided that term is fully specified.

  1226

  1227   The @{command "print_cases"} command prints all named cases present in the

  1228   current proof state.

  1229

  1230   \<^medskip>

  1231   Despite the additional infrastructure, both @{method cases} and @{method

  1232   coinduct} merely apply a certain rule, after instantiation, while conforming

  1233   due to the usual way of monotonic natural deduction: the context of a

  1234   structured statement \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>\<close> reappears unchanged after

  1235   the case split.

  1236

  1237   The @{method induct} method is fundamentally different in this respect: the

  1238   meta-level structure is passed through the recursive'' course involved in

  1239   the induction. Thus the original statement is basically replaced by separate

  1240   copies, corresponding to the induction hypotheses and conclusion; the

  1241   original goal context is no longer available. Thus local assumptions, fixed

  1242   parameters and definitions effectively participate in the inductive

  1243   rephrasing of the original statement.

  1244

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

  1246   into two different kinds: \<open>hyps\<close> stemming from the rule and \<open>prems\<close> from the

  1247   goal statement. This is reflected in the extracted cases accordingly, so

  1248   invoking @{command "case"}~\<open>c\<close>'' will provide separate facts \<open>c.hyps\<close> and

  1249   \<open>c.prems\<close>, as well as fact \<open>c\<close> to hold the all-inclusive list.

  1250

  1251   In @{method induction} proofs, local assumptions introduced by cases are

  1252   split into three different kinds: \<open>IH\<close>, the induction hypotheses, \<open>hyps\<close>,

  1253   the remaining hypotheses stemming from the rule, and \<open>prems\<close>, the

  1254   assumptions from the goal statement. The names are \<open>c.IH\<close>, \<open>c.hyps\<close> and

  1255   \<open>c.prems\<close>, as above.

  1256

  1257   \<^medskip>

  1258   Facts presented to either method are consumed according to the number of

  1259   major premises'' of the rule involved, which is usually 0 for plain cases

  1260   and induction rules of datatypes etc.\ and 1 for rules of inductive

  1261   predicates or sets and the like. The remaining facts are inserted into the

  1262   goal verbatim before the actual \<open>cases\<close>, \<open>induct\<close>, or \<open>coinduct\<close> rule is

  1263   applied.

  1264 \<close>

  1265

  1266

  1267 subsection \<open>Declaring rules\<close>

  1268

  1269 text \<open>

  1270   \begin{matharray}{rcl}

  1271     @{command_def "print_induct_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

  1272     @{attribute_def cases} & : & \<open>attribute\<close> \\

  1273     @{attribute_def induct} & : & \<open>attribute\<close> \\

  1274     @{attribute_def coinduct} & : & \<open>attribute\<close> \\

  1275   \end{matharray}

  1276

  1277   @{rail \<open>

  1278     @@{attribute cases} spec

  1279     ;

  1280     @@{attribute induct} spec

  1281     ;

  1282     @@{attribute coinduct} spec

  1283     ;

  1284

  1285     spec: (('type' | 'pred' | 'set') ':' @{syntax name}) | 'del'

  1286   \<close>}

  1287

  1288   \<^descr> @{command "print_induct_rules"} prints cases and induct rules for

  1289   predicates (or sets) and types of the current context.

  1290

  1291   \<^descr> @{attribute cases}, @{attribute induct}, and @{attribute coinduct} (as

  1292   attributes) declare rules for reasoning about (co)inductive predicates (or

  1293   sets) and types, using the corresponding methods of the same name. Certain

  1294   definitional packages of object-logics usually declare emerging cases and

  1295   induction rules as expected, so users rarely need to intervene.

  1296

  1297   Rules may be deleted via the \<open>del\<close> specification, which covers all of the

  1298   \<open>type\<close>/\<open>pred\<close>/\<open>set\<close> sub-categories simultaneously. For example, @{attribute

  1299   cases}~\<open>del\<close> removes any @{attribute cases} rules declared for some type,

  1300   predicate, or set.

  1301

  1302   Manual rule declarations usually refer to the @{attribute case_names} and

  1303   @{attribute params} attributes to adjust names of cases and parameters of a

  1304   rule; the @{attribute consumes} declaration is taken care of automatically:

  1305   @{attribute consumes}~\<open>0\<close> is specified for type'' rules and @{attribute

  1306   consumes}~\<open>1\<close> for predicate'' / set'' rules.

  1307 \<close>

  1308

  1309

  1310 section \<open>Generalized elimination and case splitting \label{sec:obtain}\<close>

  1311

  1312 text \<open>

  1313   \begin{matharray}{rcl}

  1314     @{command_def "consider"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\

  1315     @{command_def "obtain"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\

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

  1317   \end{matharray}

  1318

  1319   Generalized elimination means that hypothetical parameters and premises may

  1320   be introduced in the current context, potentially with a split into cases.

  1321   This works by virtue of a locally proven rule that establishes the soundness

  1322   of this temporary context extension. As representative examples, one may

  1323   think of standard rules from Isabelle/HOL like this:

  1324

  1325   \<^medskip>

  1326   \begin{tabular}{ll}

  1327   \<open>\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\

  1328   \<open>A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\

  1329   \<open>A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\

  1330   \end{tabular}

  1331   \<^medskip>

  1332

  1333   In general, these particular rules and connectives need to get involved at

  1334   all: this concept works directly in Isabelle/Pure via Isar commands defined

  1335   below. In particular, the logic of elimination and case splitting is

  1336   delegated to an Isar proof, which often involves automated tools.

  1337

  1338   @{rail \<open>

  1339     @@{command consider} @{syntax obtain_clauses}

  1340     ;

  1341     @@{command obtain} @{syntax par_name}? @{syntax vars} \<newline>

  1342       @'where' concl prems @{syntax for_fixes}

  1343     ;

  1344     concl: (@{syntax props} + @'and')

  1345     ;

  1346     prems: (@'if' (@{syntax props'} + @'and'))?

  1347     ;

  1348     @@{command guess} @{syntax vars}

  1349   \<close>}

  1350

  1351   \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)

  1352   \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case splitting

  1353   into separate subgoals, such that each case involves new parameters and

  1354   premises. After the proof is finished, the resulting rule may be used

  1355   directly with the @{method cases} proof method (\secref{sec:cases-induct}),

  1356   in order to perform actual case-splitting of the proof text via @{command

  1357   case} and @{command next} as usual.

  1358

  1359   Optional names in round parentheses refer to case names: in the proof of the

  1360   rule this is a fact name, in the resulting rule it is used as annotation

  1361   with the @{attribute_ref case_names} attribute.

  1362

  1363   \<^medskip>

  1364   Formally, the command @{command consider} is defined as derived Isar

  1365   language element as follows:

  1366

  1367   \begin{matharray}{l}

  1368     @{command "consider"}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>\<close> \\[1ex]

  1369     \quad @{command "have"}~\<open>[case_names a b \<dots>]: thesis\<close> \\

  1370     \qquad \<open>\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\

  1371     \qquad \<open>\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis\<close> \\

  1372     \qquad \<open>\<AND> \<dots>\<close> \\

  1373     \qquad \<open>\<FOR> thesis\<close> \\

  1374     \qquad @{command "apply"}~\<open>(insert a b \<dots>)\<close> \\

  1375   \end{matharray}

  1376

  1377   See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal

  1378   statements, as well as @{command print_statement} to print existing rules in

  1379   a similar format.

  1380

  1381   \<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close> states a

  1382   generalized elimination rule with exactly one case. After the proof is

  1383   finished, it is activated for the subsequent proof text: the context is

  1384   augmented via @{command fix}~\<open>\<^vec>x\<close> @{command assume}~\<open>\<^vec>A

  1385   \<^vec>x\<close>, with special provisions to export later results by discharging

  1386   these assumptions again.

  1387

  1388   Note that according to the parameter scopes within the elimination rule,

  1389   results \<^emph>\<open>must not\<close> refer to hypothetical parameters; otherwise the export

  1390   will fail! This restriction conforms to the usual manner of existential

  1391   reasoning in Natural Deduction.

  1392

  1393   \<^medskip>

  1394   Formally, the command @{command obtain} is defined as derived Isar language

  1395   element as follows, using an instrumented variant of @{command assume}:

  1396

  1397   \begin{matharray}{l}

  1398     @{command "obtain"}~\<open>\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>\<close> \\[1ex]

  1399     \quad @{command "have"}~\<open>thesis\<close> \\

  1400     \qquad \<open>\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\

  1401     \qquad \<open>\<FOR> thesis\<close> \\

  1402     \qquad @{command "apply"}~\<open>(insert that)\<close> \\

  1403     \qquad \<open>\<langle>proof\<rangle>\<close> \\

  1404     \quad @{command "fix"}~\<open>\<^vec>x\<close>~@{command "assume"}\<open>\<^sup>* a: \<^vec>A \<^vec>x\<close> \\

  1405   \end{matharray}

  1406

  1407   \<^descr> @{command guess} is similar to @{command obtain}, but it derives the

  1408   obtained context elements from the course of tactical reasoning in the

  1409   proof. Thus it can considerably obscure the proof: it is classified as

  1410   \<^emph>\<open>improper\<close>.

  1411

  1412   A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The

  1413   subsequent refinement steps may turn this to anything of the form

  1414   \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new

  1415   subgoals. The final goal state is then used as reduction rule for the obtain

  1416   pattern described above. Obtained parameters \<open>\<^vec>x\<close> are marked as

  1417   internal by default, and thus inaccessible in the proof text. The variable

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

  1419   a prefix of accessible parameters.

  1420

  1421

  1422   In the proof of @{command consider} and @{command obtain} the local premises

  1423   are always bound to the fact name @{fact_ref that}, according to structured

  1424   Isar statements involving @{keyword_ref "if"} (\secref{sec:goals}).

  1425

  1426   Facts that are established by @{command "obtain"} and @{command "guess"} may

  1427   not be polymorphic: any type-variables occurring here are fixed in the

  1428   present context. This is a natural consequence of the role of @{command fix}

  1429   and @{command assume} in these constructs.

  1430 \<close>

  1431

  1432 end