# HG changeset patch # User wenzelm # Date 1434367797 -7200 # Node ID 9a566f4ac20a91226804635a72dcb73cfa9b6e2b # Parent 932c65dade337f40791a9aeeb61efa8c36ab4899 moved sections; diff -r 932c65dade33 -r 9a566f4ac20a src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Mon Jun 15 10:38:09 2015 +0200 +++ b/src/Doc/Isar_Ref/Proof.thy Mon Jun 15 13:29:57 2015 +0200 @@ -191,28 +191,28 @@ \} \begin{description} - + \item @{command "fix"}~@{text x} introduces a local variable @{text x} that is \emph{arbitrary, but fixed.} - + \item @{command "assume"}~@{text "a: \"} and @{command "presume"}~@{text "a: \"} introduce a local fact @{text "\ \ \"} by assumption. Subsequent results applied to an enclosing goal (e.g.\ by @{command_ref "show"}) are handled as follows: @{command "assume"} expects to be able to unify with existing premises in the goal, while @{command "presume"} leaves @{text \} as new subgoals. - + Several lists of assumptions may be given (separated by @{keyword_ref "and"}; the resulting list of current facts consists of all of these concatenated. - + \item @{command "def"}~@{text "x \ t"} introduces a local (non-polymorphic) definition. In results exported from the context, @{text x} is replaced by @{text t}. Basically, ``@{command "def"}~@{text "x \ t"}'' abbreviates ``@{command "fix"}~@{text x}~@{command "assume"}~@{text "x \ t"}'', with the resulting hypothetical equation solved by reflexivity. - + The default name for the definitional equation is @{text x_def}. Several simultaneous definitions may be given at the same time. @@ -333,19 +333,19 @@ rather than an introduction. Automatic methods usually insert the facts into the goal state before operation. This provides a simple scheme to control relevance of facts in automated proof search. - + \item @{command "from"}~@{text b} abbreviates ``@{command "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is equivalent to ``@{command "from"}~@{text this}''. - + \item @{command "with"}~@{text "b\<^sub>1 \ b\<^sub>n"} abbreviates ``@{command "from"}~@{text "b\<^sub>1 \ b\<^sub>n \ this"}''; thus the forward chaining is from earlier facts together with the current ones. - + \item @{command "using"}~@{text "b\<^sub>1 \ b\<^sub>n"} augments the facts being currently indicated for use by a subsequent refinement step (such as @{command_ref "apply"} or @{command_ref "proof"}). - + \item @{command "unfolding"}~@{text "b\<^sub>1 \ b\<^sub>n"} is structurally similar to @{command "using"}, but unfolds definitional equations @{text "b\<^sub>1, \ b\<^sub>n"} throughout the goal state and facts. @@ -431,7 +431,7 @@ ; @@{command print_statement} @{syntax modes}? @{syntax thmrefs} ; - + stmt: (@{syntax props} + @'and') ; statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \ @@ -446,7 +446,7 @@ \} \begin{description} - + \item @{command "lemma"}~@{text "a: \"} enters proof mode with @{text \} as main goal, eventually resulting in some fact @{text "\ \"} to be put back into the target context. An additional @{syntax @@ -454,7 +454,7 @@ subsequent claim; this includes local definitions and syntax as well, see also @{syntax "includes"} in \secref{sec:bundle} and @{syntax context_elem} in \secref{sec:locale}. - + \item @{command "theorem"}~@{text "a: \"} and @{command "corollary"}~@{text "a: \"} are essentially the same as @{command "lemma"}~@{text "a: \"}, but the facts are internally marked as @@ -472,20 +472,20 @@ With schematic statements, the inherent compositionality of Isar proofs is lost, which also impacts performance, because proof checking is forced into sequential mode. - + \item @{command "have"}~@{text "a: \"} claims a local goal, eventually resulting in a fact within the current logical context. This operation is completely independent of any pending sub-goals of an enclosing goal statements, so @{command "have"} may be freely used for experimental exploration of potential results within a proof body. - + \item @{command "show"}~@{text "a: \"} is like @{command "have"}~@{text "a: \"} plus a second stage to refine some pending sub-goal for each one of the finished result, after having been exported into the corresponding context (at the head of the sub-proof of this @{command "show"} command). - + To accommodate interactive debugging, resulting rules are printed before being applied internally. Even more, interactive execution of @{command "show"} predicts potential failure and displays the @@ -496,16 +496,16 @@ \begin{ttbox} Problem! Local statement will fail to solve any pending goal \end{ttbox} - + \item @{command "hence"} abbreviates ``@{command "then"}~@{command "have"}'', i.e.\ claims a local goal to be proven by forward chaining the current facts. Note that @{command "hence"} is also equivalent to ``@{command "from"}~@{text this}~@{command "have"}''. - + \item @{command "thus"} abbreviates ``@{command "then"}~@{command "show"}''. Note that @{command "thus"} is also equivalent to ``@{command "from"}~@{text this}~@{command "show"}''. - + \item @{command "print_statement"}~@{text a} prints facts from the current theory or proof context in long statement form, according to the syntax for @{command "lemma"} given above. @@ -523,6 +523,117 @@ \ +section \Calculational reasoning \label{sec:calculation}\ + +text \ + \begin{matharray}{rcl} + @{command_def "also"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "finally"} & : & @{text "proof(state) \ proof(chain)"} \\ + @{command_def "moreover"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "ultimately"} & : & @{text "proof(state) \ proof(chain)"} \\ + @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{attribute trans} & : & @{text attribute} \\ + @{attribute sym} & : & @{text attribute} \\ + @{attribute symmetric} & : & @{text attribute} \\ + \end{matharray} + + Calculational proof is forward reasoning with implicit application + of transitivity rules (such those of @{text "="}, @{text "\"}, + @{text "<"}). Isabelle/Isar maintains an auxiliary fact register + @{fact_ref calculation} for accumulating results obtained by + transitivity composed with the current result. Command @{command + "also"} updates @{fact calculation} involving @{fact this}, while + @{command "finally"} exhibits the final @{fact calculation} by + forward chaining towards the next goal statement. Both commands + require valid current facts, i.e.\ may occur only after commands + that produce theorems such as @{command "assume"}, @{command + "note"}, or some finished proof of @{command "have"}, @{command + "show"} etc. The @{command "moreover"} and @{command "ultimately"} + commands are similar to @{command "also"} and @{command "finally"}, + but only collect further results in @{fact calculation} without + applying any rules yet. + + Also note that the implicit term abbreviation ``@{text "\"}'' has + its canonical application with calculational proofs. It refers to + the argument of the preceding statement. (The argument of a curried + infix expression happens to be its right-hand side.) + + Isabelle/Isar calculations are implicitly subject to block structure + in the sense that new threads of calculational reasoning are + commenced for any new block (as opened by a local goal, for + example). This means that, apart from being able to nest + calculations, there is no separate \emph{begin-calculation} command + required. + + \medskip The Isar calculation proof commands may be defined as + follows:\footnote{We suppress internal bookkeeping such as proper + handling of block-structure.} + + \begin{matharray}{rcl} + @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\ + @{command "also"}@{text "\<^sub>n+1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex] + @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex] + @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\ + @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\ + \end{matharray} + + @{rail \ + (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')? + ; + @@{attribute trans} (() | 'add' | 'del') + \} + + \begin{description} + + \item @{command "also"}~@{text "(a\<^sub>1 \ a\<^sub>n)"} maintains the auxiliary + @{fact calculation} register as follows. The first occurrence of + @{command "also"} in some calculational thread initializes @{fact + calculation} by @{fact this}. Any subsequent @{command "also"} on + the same level of block-structure updates @{fact calculation} by + some transitivity rule applied to @{fact calculation} and @{fact + this} (in that order). Transitivity rules are picked from the + current context, unless alternative rules are given as explicit + arguments. + + \item @{command "finally"}~@{text "(a\<^sub>1 \ a\<^sub>n)"} maintaining @{fact + calculation} in the same way as @{command "also"}, and concludes the + current calculational thread. The final result is exhibited as fact + for forward chaining towards the next goal. Basically, @{command + "finally"} just abbreviates @{command "also"}~@{command + "from"}~@{fact calculation}. Typical idioms for concluding + calculational proofs are ``@{command "finally"}~@{command + "show"}~@{text ?thesis}~@{command "."}'' and ``@{command + "finally"}~@{command "have"}~@{text \}~@{command "."}''. + + \item @{command "moreover"} and @{command "ultimately"} are + analogous to @{command "also"} and @{command "finally"}, but collect + results only, without applying rules. + + \item @{command "print_trans_rules"} prints the list of transitivity + rules (for calculational commands @{command "also"} and @{command + "finally"}) and symmetry rules (for the @{attribute symmetric} + operation and single step elimination patters) of the current + context. + + \item @{attribute trans} declares theorems as transitivity rules. + + \item @{attribute sym} declares symmetry rules, as well as + @{attribute "Pure.elim"}@{text "?"} rules. + + \item @{attribute symmetric} resolves a theorem with some rule + declared as @{attribute sym} in the current context. For example, + ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a + swapped fact derived from that assumption. + + In structured proof texts it is often more appropriate to use an + explicit single-step elimination proof, such as ``@{command + "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text + "y = x"}~@{command ".."}''. + + \end{description} +\ + + section \Refinement steps\ subsection \Proof method expressions \label{sec:proof-meth}\ @@ -606,7 +717,7 @@ of sub-goals that are to be solved later. Facts are passed to @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text "proof(chain)"} mode. - + \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text "m\<^sub>2"} is intended to solve remaining goals. No facts are passed to @{text "m\<^sub>2"}. @@ -644,11 +755,11 @@ \} \begin{description} - + \item @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof method @{text "m\<^sub>1"}; facts for forward chaining are passed if so indicated by @{text "proof(chain)"} mode. - + \item @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by proof method @{text "m\<^sub>2"} and concludes the sub-proof by assumption. If the goal had been @{text "show"} (or @{text "thus"}), some @@ -661,7 +772,7 @@ situation might involve temporarily changing @{command "show"} into @{command "have"}, or weakening the local context by replacing occurrences of @{command "assume"} by @{command "presume"}. - + \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal proof}\index{proof!terminal}; it abbreviates @{command "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"}, but with @@ -678,7 +789,7 @@ \item ``@{command "."}'' is a \emph{trivial proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text "this"}. - + \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake} pretending to solve the pending claim without further ado. This only works in interactive development, or if the @{attribute @@ -686,7 +797,7 @@ proofs are not the real thing. Internally, the derivation object is tainted by an oracle invocation, which may be inspected via the theorem status @{cite "isabelle-implementation"}. - + The most important application of @{command "sorry"} is to support experimentation and top-down proof development. @@ -739,7 +850,7 @@ \} \begin{description} - + \item @{command "print_rules"} prints rules declared via attributes @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure) dest} of Isabelle/Pure. @@ -754,7 +865,7 @@ reduction step using the @{method_ref (Pure) rule} method; thus a plain \emph{do-nothing} proof step would be ``@{command "proof"}~@{text "-"}'' rather than @{command "proof"} alone. - + \item @{method "fact"}~@{text "a\<^sub>1 \ a\<^sub>n"} composes some fact from @{text "a\<^sub>1, \, a\<^sub>n"} (or implicitly from the current proof context) modulo unification of schematic type and term variables. The rule @@ -765,7 +876,7 @@ "note"}~@{verbatim "`"}@{text \}@{verbatim "`"}'' provided that @{text "\ \"} is an instance of some known @{text "\ \"} in the proof context. - + \item @{method assumption} solves some goal by a single assumption step. All given facts are guaranteed to participate in the refinement; this means there may be only 0 or 1 in the first place. @@ -773,34 +884,34 @@ concludes any remaining sub-goals by assumption, so structured proofs usually need not quote the @{method assumption} method at all. - + \item @{method this} applies all of the current facts directly as rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command "by"}~@{text this}''. - + \item @{method (Pure) rule}~@{text "a\<^sub>1 \ a\<^sub>n"} applies some rule given as argument in backward manner; facts are used to reduce the rule before applying it to the goal. Thus @{method (Pure) rule} without facts is plain introduction, while with facts it becomes elimination. - + When no arguments are given, the @{method (Pure) rule} method tries to pick appropriate rules automatically, as declared in the current context using the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure) dest} attributes (see below). This is the - default behavior of @{command "proof"} and ``@{command ".."}'' + default behavior of @{command "proof"} and ``@{command ".."}'' (double-dot) steps (see \secref{sec:proof-steps}). - + \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and @{attribute (Pure) dest} declare introduction, elimination, and destruct rules, to be used with method @{method (Pure) rule}, and similar tools. Note that the latter will ignore rules declared with ``@{text "?"}'', while ``@{text "!"}'' are used most aggressively. - + The classical reasoner (see \secref{sec:classical}) introduces its own variants of these attributes; use qualified names to access the present versions of Isabelle/Pure, i.e.\ @{attribute (Pure) "Pure.intro"}. - + \item @{attribute (Pure) rule}~@{text del} undeclares introduction, elimination, or destruct rules. @@ -815,7 +926,7 @@ Argument positions may be effectively skipped by using ``@{text _}'' (underscore), which refers to the propositional identity rule in the Pure theory. - + \item @{attribute of}~@{text "t\<^sub>1 \ t\<^sub>n"} performs positional instantiation of term variables. The terms @{text "t\<^sub>1, \, t\<^sub>n"} are substituted for any schematic variables occurring in a theorem from @@ -826,7 +937,7 @@ An optional context of local variables @{text "\ x\<^sub>1 \ x\<^sub>m"} may be specified: the instantiated theorem is exported, and these variables become schematic (usually with some shifting of indices). - + \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \ \ x\<^sub>n = t\<^sub>n"} performs named instantiation of schematic type and term variables occurring in a theorem. Schematic variables have to be specified on @@ -884,22 +995,22 @@ initial position, but unlike @{command "proof"} it retains ``@{text "proof(prove)"}'' mode. Thus consecutive method applications may be given just as in tactic scripts. - + Facts are passed to @{text m} as indicated by the goal's forward-chain mode, and are \emph{consumed} afterwards. Thus any further @{command "apply"} command would always work in a purely backward manner. - + \item @{command "apply_end"}~@{text "m"} applies proof method @{text m} as if in terminal position. Basically, this simulates a multi-step tactic script for @{command "qed"}, but may be given anywhere within the proof body. - + No facts are passed to @{text m} here. Furthermore, the static context is that of the enclosing goal (as for actual @{command "qed"}). Thus the proof method may not refer to any assumptions introduced in the current body, for example. - + \item @{command "done"} completes a proof script, provided that the current goal state is solved completely. Note that actual structured proof commands (e.g.\ ``@{command "."}'' or @{command @@ -910,13 +1021,13 @@ sub-goal @{text n} to the end of the list (@{text "n = 1"} by default), while @{command "prefer"} brings sub-goal @{text n} to the front. - + \item @{command "back"} does back-tracking over the result sequence of the latest proof command. Any proof command may return multiple results, and this command explores the possibilities step-by-step. It is mainly useful for experimentation and interactive exploration, and should be avoided in finished proofs. - + \end{description} Any proper Isar proof method may be used with tactic script commands @@ -971,6 +1082,411 @@ (*<*)end(*>*) +section \Proof by cases and induction \label{sec:cases-induct}\ + +subsection \Rule contexts\ + +text \ + \begin{matharray}{rcl} + @{command_def "case"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{attribute_def case_names} & : & @{text attribute} \\ + @{attribute_def case_conclusion} & : & @{text attribute} \\ + @{attribute_def params} & : & @{text attribute} \\ + @{attribute_def consumes} & : & @{text attribute} \\ + \end{matharray} + + The puristic way to build up Isar proof contexts is by explicit + language elements like @{command "fix"}, @{command "assume"}, + @{command "let"} (see \secref{sec:proof-context}). This is adequate + for plain natural deduction, but easily becomes unwieldy in concrete + verification tasks, which typically involve big induction rules with + several cases. + + The @{command "case"} command provides a shorthand to refer to a + local context symbolically: certain proof methods provide an + environment of named ``cases'' of the form @{text "c: x\<^sub>1, \, + x\<^sub>m, \\<^sub>1, \, \\<^sub>n"}; the effect of ``@{command + "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text + "x\<^sub>1 \ x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ + \\<^sub>n"}''. Term bindings may be covered as well, notably + @{variable ?case} for the main conclusion. + + By default, the ``terminology'' @{text "x\<^sub>1, \, x\<^sub>m"} of + a case value is marked as hidden, i.e.\ there is no way to refer to + such parameters in the subsequent proof text. After all, original + rule parameters stem from somewhere outside of the current proof + text. By using the explicit form ``@{command "case"}~@{text "(c + y\<^sub>1 \ y\<^sub>m)"}'' instead, the proof author is able to + chose local names that fit nicely into the current context. + + \medskip It is important to note that proper use of @{command + "case"} does not provide means to peek at the current goal state, + which is not directly observable in Isar! Nonetheless, goal + refinement commands do provide named cases @{text "goal\<^sub>i"} + for each subgoal @{text "i = 1, \, n"} of the resulting goal state. + Using this extra feature requires great care, because some bits of + the internal tactical machinery intrude the proof text. In + particular, parameter names stemming from the left-over of automated + reasoning tools are usually quite unpredictable. + + Under normal circumstances, the text of cases emerge from standard + elimination or induction rules, which in turn are derived from + previous theory specifications in a canonical way (say from + @{command "inductive"} definitions). + + \medskip Proper cases are only available if both the proof method + and the rules involved support this. By using appropriate + attributes, case names, conclusions, and parameters may be also + declared by hand. Thus variant versions of rules that have been + derived manually become ready to use in advanced case analysis + later. + + @{rail \ + @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')') + ; + caseref: nameref attributes? + ; + + @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +) + ; + @@{attribute case_conclusion} @{syntax name} (@{syntax name} * ) + ; + @@{attribute params} ((@{syntax name} * ) + @'and') + ; + @@{attribute consumes} @{syntax int}? + \} + + \begin{description} + + \item @{command "case"}~@{text "(c x\<^sub>1 \ x\<^sub>m)"} invokes a named local + context @{text "c: x\<^sub>1, \, x\<^sub>m, \\<^sub>1, \, \\<^sub>m"}, as provided by an + appropriate proof method (such as @{method_ref cases} and + @{method_ref induct}). The command ``@{command "case"}~@{text "(c + x\<^sub>1 \ x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \ + x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ \\<^sub>n"}''. + + \item @{command "print_cases"} prints all local contexts of the + current state, using Isar proof language notation. + + \item @{attribute case_names}~@{text "c\<^sub>1 \ c\<^sub>k"} declares names for + the local contexts of premises of a theorem; @{text "c\<^sub>1, \, c\<^sub>k"} + refers to the \emph{prefix} of the list of premises. Each of the + cases @{text "c\<^sub>i"} can be of the form @{text "c[h\<^sub>1 \ h\<^sub>n]"} where + the @{text "h\<^sub>1 \ h\<^sub>n"} are the names of the hypotheses in case @{text "c\<^sub>i"} + from left to right. + + \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \ d\<^sub>k"} declares + names for the conclusions of a named premise @{text c}; here @{text + "d\<^sub>1, \, d\<^sub>k"} refers to the prefix of arguments of a logical formula + built by nesting a binary connective (e.g.\ @{text "\"}). + + Note that proof methods such as @{method induct} and @{method + coinduct} already provide a default name for the conclusion as a + whole. The need to name subformulas only arises with cases that + split into several sub-cases, as in common co-induction rules. + + \item @{attribute params}~@{text "p\<^sub>1 \ p\<^sub>m \ \ q\<^sub>1 \ q\<^sub>n"} renames + the innermost parameters of premises @{text "1, \, n"} of some + theorem. An empty list of names may be given to skip positions, + leaving the present parameters unchanged. + + Note that the default usage of case rules does \emph{not} directly + expose parameters to the proof context. + + \item @{attribute consumes}~@{text n} declares the number of ``major + premises'' of a rule, i.e.\ the number of facts to be consumed when + it is applied by an appropriate proof method. The default value of + @{attribute consumes} is @{text "n = 1"}, which is appropriate for + the usual kind of cases and induction rules for inductive sets (cf.\ + \secref{sec:hol-inductive}). Rules without any @{attribute + consumes} declaration given are treated as if @{attribute + consumes}~@{text 0} had been specified. + + A negative @{text n} is interpreted relatively to the total number + of premises of the rule in the target context. Thus its absolute + value specifies the remaining number of premises, after subtracting + the prefix of major premises as indicated above. This form of + declaration has the technical advantage of being stable under more + morphisms, notably those that export the result from a nested + @{command_ref context} with additional assumptions. + + Note that explicit @{attribute consumes} declarations are only + rarely needed; this is already taken care of automatically by the + higher-level @{attribute cases}, @{attribute induct}, and + @{attribute coinduct} declarations. + + \end{description} +\ + + +subsection \Proof methods\ + +text \ + \begin{matharray}{rcl} + @{method_def cases} & : & @{text method} \\ + @{method_def induct} & : & @{text method} \\ + @{method_def induction} & : & @{text method} \\ + @{method_def coinduct} & : & @{text method} \\ + \end{matharray} + + The @{method cases}, @{method induct}, @{method induction}, + and @{method coinduct} + methods provide a uniform interface to common proof techniques over + datatypes, inductive predicates (or sets), recursive functions etc. + The corresponding rules may be specified and instantiated in a + casual manner. Furthermore, these methods provide named local + contexts that may be invoked via the @{command "case"} proof command + within the subsequent proof text. This accommodates compact proof + texts even when reasoning about large specifications. + + The @{method induct} method also provides some additional + infrastructure in order to be applicable to structure statements + (either using explicit meta-level connectives, or including facts + and parameters separately). This avoids cumbersome encoding of + ``strengthened'' inductive statements within the object-logic. + + Method @{method induction} differs from @{method induct} only in + the names of the facts in the local context invoked by the @{command "case"} + command. + + @{rail \ + @@{method cases} ('(' 'no_simp' ')')? \ + (@{syntax insts} * @'and') rule? + ; + (@@{method induct} | @@{method induction}) + ('(' 'no_simp' ')')? (definsts * @'and') \ arbitrary? taking? rule? + ; + @@{method coinduct} @{syntax insts} taking rule? + ; + + rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +) + ; + definst: @{syntax name} ('==' | '\') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst} + ; + definsts: ( definst * ) + ; + arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +) + ; + taking: 'taking' ':' @{syntax insts} + \} + + \begin{description} + + \item @{method cases}~@{text "insts R"} applies method @{method + rule} with an appropriate case distinction theorem, instantiated to + the subjects @{text insts}. Symbolic case names are bound according + to the rule's local contexts. + + The rule is determined as follows, according to the facts and + arguments passed to the @{method cases} method: + + \medskip + \begin{tabular}{llll} + facts & & arguments & rule \\\hline + @{text "\ R"} & @{method cases} & & implicit rule @{text R} \\ + & @{method cases} & & classical case split \\ + & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\ + @{text "\ A t"} & @{method cases} & @{text "\"} & inductive predicate/set elimination (of @{text A}) \\ + @{text "\"} & @{method cases} & @{text "\ rule: R"} & explicit rule @{text R} \\ + \end{tabular} + \medskip + + Several instantiations may be given, referring to the \emph{suffix} + of premises of the case rule; within each premise, the \emph{prefix} + of variables is instantiated. In most situations, only a single + term needs to be specified; this refers to the first variable of the + last premise (it is usually the same for all cases). The @{text + "(no_simp)"} option can be used to disable pre-simplification of + cases (see the description of @{method induct} below for details). + + \item @{method induct}~@{text "insts R"} and + @{method induction}~@{text "insts R"} are analogous to the + @{method cases} method, but refer to induction rules, which are + determined as follows: + + \medskip + \begin{tabular}{llll} + facts & & arguments & rule \\\hline + & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\ + @{text "\ A x"} & @{method induct} & @{text "\"} & predicate/set induction (of @{text A}) \\ + @{text "\"} & @{method induct} & @{text "\ rule: R"} & explicit rule @{text R} \\ + \end{tabular} + \medskip + + Several instantiations may be given, each referring to some part of + a mutual inductive definition or datatype --- only related partial + induction rules may be used together, though. Any of the lists of + terms @{text "P, x, \"} refers to the \emph{suffix} of variables + present in the induction rule. This enables the writer to specify + only induction variables, or both predicates and variables, for + example. + + Instantiations may be definitional: equations @{text "x \ t"} + introduce local definitions, which are inserted into the claim and + discharged after applying the induction rule. Equalities reappear + in the inductive cases, but have been transformed according to the + induction principle being involved here. In order to achieve + practically useful induction hypotheses, some variables occurring in + @{text t} need to be fixed (see below). Instantiations of the form + @{text t}, where @{text t} is not a variable, are taken as a + shorthand for \mbox{@{text "x \ t"}}, where @{text x} is a fresh + variable. If this is not intended, @{text t} has to be enclosed in + parentheses. By default, the equalities generated by definitional + instantiations are pre-simplified using a specific set of rules, + usually consisting of distinctness and injectivity theorems for + datatypes. This pre-simplification may cause some of the parameters + of an inductive case to disappear, or may even completely delete + some of the inductive cases, if one of the equalities occurring in + their premises can be simplified to @{text False}. The @{text + "(no_simp)"} option can be used to disable pre-simplification. + Additional rules to be used in pre-simplification can be declared + using the @{attribute_def induct_simp} attribute. + + The optional ``@{text "arbitrary: x\<^sub>1 \ x\<^sub>m"}'' + specification generalizes variables @{text "x\<^sub>1, \, + x\<^sub>m"} of the original goal before applying induction. One can + separate variables by ``@{text "and"}'' to generalize them in other + goals then the first. Thus induction hypotheses may become + sufficiently general to get the proof through. Together with + definitional instantiations, one may effectively perform induction + over expressions of a certain structure. + + The optional ``@{text "taking: t\<^sub>1 \ t\<^sub>n"}'' + specification provides additional instantiations of a prefix of + pending variables in the rule. Such schematic induction rules + rarely occur in practice, though. + + \item @{method coinduct}~@{text "inst R"} is analogous to the + @{method induct} method, but refers to coinduction rules, which are + determined as follows: + + \medskip + \begin{tabular}{llll} + goal & & arguments & rule \\\hline + & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\ + @{text "A x"} & @{method coinduct} & @{text "\"} & predicate/set coinduction (of @{text A}) \\ + @{text "\"} & @{method coinduct} & @{text "\ rule: R"} & explicit rule @{text R} \\ + \end{tabular} + + Coinduction is the dual of induction. Induction essentially + eliminates @{text "A x"} towards a generic result @{text "P x"}, + while coinduction introduces @{text "A x"} starting with @{text "B + x"}, for a suitable ``bisimulation'' @{text B}. The cases of a + coinduct rule are typically named after the predicates or sets being + covered, while the conclusions consist of several alternatives being + named after the individual destructor patterns. + + The given instantiation refers to the \emph{suffix} of variables + occurring in the rule's major premise, or conclusion if unavailable. + An additional ``@{text "taking: t\<^sub>1 \ t\<^sub>n"}'' + specification may be required in order to specify the bisimulation + to be used in the coinduction step. + + \end{description} + + Above methods produce named local contexts, as determined by the + instantiated rule as given in the text. Beyond that, the @{method + induct} and @{method coinduct} methods guess further instantiations + from the goal specification itself. Any persisting unresolved + schematic variables of the resulting rule will render the the + corresponding case invalid. The term binding @{variable ?case} for + the conclusion will be provided with each case, provided that term + is fully specified. + + The @{command "print_cases"} command prints all named cases present + in the current proof state. + + \medskip Despite the additional infrastructure, both @{method cases} + and @{method coinduct} merely apply a certain rule, after + instantiation, while conforming due to the usual way of monotonic + natural deduction: the context of a structured statement @{text + "\x\<^sub>1 \ x\<^sub>m. \\<^sub>1 \ \ \\<^sub>n \ \"} + reappears unchanged after the case split. + + The @{method induct} method is fundamentally different in this + respect: the meta-level structure is passed through the + ``recursive'' course involved in the induction. Thus the original + statement is basically replaced by separate copies, corresponding to + the induction hypotheses and conclusion; the original goal context + is no longer available. Thus local assumptions, fixed parameters + and definitions effectively participate in the inductive rephrasing + of the original statement. + + In @{method induct} proofs, local assumptions introduced by cases are split + into two different kinds: @{text hyps} stemming from the rule and + @{text prems} from the goal statement. This is reflected in the + extracted cases accordingly, so invoking ``@{command "case"}~@{text + c}'' will provide separate facts @{text c.hyps} and @{text c.prems}, + as well as fact @{text c} to hold the all-inclusive list. + + In @{method induction} proofs, local assumptions introduced by cases are + split into three different kinds: @{text IH}, the induction hypotheses, + @{text hyps}, the remaining hypotheses stemming from the rule, and + @{text prems}, the assumptions from the goal statement. The names are + @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above. + + + \medskip Facts presented to either method are consumed according to + the number of ``major premises'' of the rule involved, which is + usually 0 for plain cases and induction rules of datatypes etc.\ and + 1 for rules of inductive predicates or sets and the like. The + remaining facts are inserted into the goal verbatim before the + actual @{text cases}, @{text induct}, or @{text coinduct} rule is + applied. +\ + + +subsection \Declaring rules\ + +text \ + \begin{matharray}{rcl} + @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{attribute_def cases} & : & @{text attribute} \\ + @{attribute_def induct} & : & @{text attribute} \\ + @{attribute_def coinduct} & : & @{text attribute} \\ + \end{matharray} + + @{rail \ + @@{attribute cases} spec + ; + @@{attribute induct} spec + ; + @@{attribute coinduct} spec + ; + + spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del' + \} + + \begin{description} + + \item @{command "print_induct_rules"} prints cases and induct rules + for predicates (or sets) and types of the current context. + + \item @{attribute cases}, @{attribute induct}, and @{attribute + coinduct} (as attributes) declare rules for reasoning about + (co)inductive predicates (or sets) and types, using the + corresponding methods of the same name. Certain definitional + packages of object-logics usually declare emerging cases and + induction rules as expected, so users rarely need to intervene. + + Rules may be deleted via the @{text "del"} specification, which + covers all of the @{text "type"}/@{text "pred"}/@{text "set"} + sub-categories simultaneously. For example, @{attribute + cases}~@{text del} removes any @{attribute cases} rules declared for + some type, predicate, or set. + + Manual rule declarations usually refer to the @{attribute + case_names} and @{attribute params} attributes to adjust names of + cases and parameters of a rule; the @{attribute consumes} + declaration is taken care of automatically: @{attribute + consumes}~@{text 0} is specified for ``type'' rules and @{attribute + consumes}~@{text 1} for ``predicate'' / ``set'' rules. + + \end{description} +\ + + section \Generalized elimination and case splitting \label{sec:obtain}\ text \ @@ -1092,520 +1608,4 @@ fix} and @{command assume} in these constructs. \ - -section \Calculational reasoning \label{sec:calculation}\ - -text \ - \begin{matharray}{rcl} - @{command_def "also"} & : & @{text "proof(state) \ proof(state)"} \\ - @{command_def "finally"} & : & @{text "proof(state) \ proof(chain)"} \\ - @{command_def "moreover"} & : & @{text "proof(state) \ proof(state)"} \\ - @{command_def "ultimately"} & : & @{text "proof(state) \ proof(chain)"} \\ - @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{attribute trans} & : & @{text attribute} \\ - @{attribute sym} & : & @{text attribute} \\ - @{attribute symmetric} & : & @{text attribute} \\ - \end{matharray} - - Calculational proof is forward reasoning with implicit application - of transitivity rules (such those of @{text "="}, @{text "\"}, - @{text "<"}). Isabelle/Isar maintains an auxiliary fact register - @{fact_ref calculation} for accumulating results obtained by - transitivity composed with the current result. Command @{command - "also"} updates @{fact calculation} involving @{fact this}, while - @{command "finally"} exhibits the final @{fact calculation} by - forward chaining towards the next goal statement. Both commands - require valid current facts, i.e.\ may occur only after commands - that produce theorems such as @{command "assume"}, @{command - "note"}, or some finished proof of @{command "have"}, @{command - "show"} etc. The @{command "moreover"} and @{command "ultimately"} - commands are similar to @{command "also"} and @{command "finally"}, - but only collect further results in @{fact calculation} without - applying any rules yet. - - Also note that the implicit term abbreviation ``@{text "\"}'' has - its canonical application with calculational proofs. It refers to - the argument of the preceding statement. (The argument of a curried - infix expression happens to be its right-hand side.) - - Isabelle/Isar calculations are implicitly subject to block structure - in the sense that new threads of calculational reasoning are - commenced for any new block (as opened by a local goal, for - example). This means that, apart from being able to nest - calculations, there is no separate \emph{begin-calculation} command - required. - - \medskip The Isar calculation proof commands may be defined as - follows:\footnote{We suppress internal bookkeeping such as proper - handling of block-structure.} - - \begin{matharray}{rcl} - @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\ - @{command "also"}@{text "\<^sub>n+1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex] - @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex] - @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\ - @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\ - \end{matharray} - - @{rail \ - (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')? - ; - @@{attribute trans} (() | 'add' | 'del') - \} - - \begin{description} - - \item @{command "also"}~@{text "(a\<^sub>1 \ a\<^sub>n)"} maintains the auxiliary - @{fact calculation} register as follows. The first occurrence of - @{command "also"} in some calculational thread initializes @{fact - calculation} by @{fact this}. Any subsequent @{command "also"} on - the same level of block-structure updates @{fact calculation} by - some transitivity rule applied to @{fact calculation} and @{fact - this} (in that order). Transitivity rules are picked from the - current context, unless alternative rules are given as explicit - arguments. - - \item @{command "finally"}~@{text "(a\<^sub>1 \ a\<^sub>n)"} maintaining @{fact - calculation} in the same way as @{command "also"}, and concludes the - current calculational thread. The final result is exhibited as fact - for forward chaining towards the next goal. Basically, @{command - "finally"} just abbreviates @{command "also"}~@{command - "from"}~@{fact calculation}. Typical idioms for concluding - calculational proofs are ``@{command "finally"}~@{command - "show"}~@{text ?thesis}~@{command "."}'' and ``@{command - "finally"}~@{command "have"}~@{text \}~@{command "."}''. - - \item @{command "moreover"} and @{command "ultimately"} are - analogous to @{command "also"} and @{command "finally"}, but collect - results only, without applying rules. - - \item @{command "print_trans_rules"} prints the list of transitivity - rules (for calculational commands @{command "also"} and @{command - "finally"}) and symmetry rules (for the @{attribute symmetric} - operation and single step elimination patters) of the current - context. - - \item @{attribute trans} declares theorems as transitivity rules. - - \item @{attribute sym} declares symmetry rules, as well as - @{attribute "Pure.elim"}@{text "?"} rules. - - \item @{attribute symmetric} resolves a theorem with some rule - declared as @{attribute sym} in the current context. For example, - ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a - swapped fact derived from that assumption. - - In structured proof texts it is often more appropriate to use an - explicit single-step elimination proof, such as ``@{command - "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text - "y = x"}~@{command ".."}''. - - \end{description} -\ - - -section \Proof by cases and induction \label{sec:cases-induct}\ - -subsection \Rule contexts\ - -text \ - \begin{matharray}{rcl} - @{command_def "case"} & : & @{text "proof(state) \ proof(state)"} \\ - @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{attribute_def case_names} & : & @{text attribute} \\ - @{attribute_def case_conclusion} & : & @{text attribute} \\ - @{attribute_def params} & : & @{text attribute} \\ - @{attribute_def consumes} & : & @{text attribute} \\ - \end{matharray} - - The puristic way to build up Isar proof contexts is by explicit - language elements like @{command "fix"}, @{command "assume"}, - @{command "let"} (see \secref{sec:proof-context}). This is adequate - for plain natural deduction, but easily becomes unwieldy in concrete - verification tasks, which typically involve big induction rules with - several cases. - - The @{command "case"} command provides a shorthand to refer to a - local context symbolically: certain proof methods provide an - environment of named ``cases'' of the form @{text "c: x\<^sub>1, \, - x\<^sub>m, \\<^sub>1, \, \\<^sub>n"}; the effect of ``@{command - "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text - "x\<^sub>1 \ x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ - \\<^sub>n"}''. Term bindings may be covered as well, notably - @{variable ?case} for the main conclusion. - - By default, the ``terminology'' @{text "x\<^sub>1, \, x\<^sub>m"} of - a case value is marked as hidden, i.e.\ there is no way to refer to - such parameters in the subsequent proof text. After all, original - rule parameters stem from somewhere outside of the current proof - text. By using the explicit form ``@{command "case"}~@{text "(c - y\<^sub>1 \ y\<^sub>m)"}'' instead, the proof author is able to - chose local names that fit nicely into the current context. - - \medskip It is important to note that proper use of @{command - "case"} does not provide means to peek at the current goal state, - which is not directly observable in Isar! Nonetheless, goal - refinement commands do provide named cases @{text "goal\<^sub>i"} - for each subgoal @{text "i = 1, \, n"} of the resulting goal state. - Using this extra feature requires great care, because some bits of - the internal tactical machinery intrude the proof text. In - particular, parameter names stemming from the left-over of automated - reasoning tools are usually quite unpredictable. - - Under normal circumstances, the text of cases emerge from standard - elimination or induction rules, which in turn are derived from - previous theory specifications in a canonical way (say from - @{command "inductive"} definitions). - - \medskip Proper cases are only available if both the proof method - and the rules involved support this. By using appropriate - attributes, case names, conclusions, and parameters may be also - declared by hand. Thus variant versions of rules that have been - derived manually become ready to use in advanced case analysis - later. - - @{rail \ - @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')') - ; - caseref: nameref attributes? - ; - - @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +) - ; - @@{attribute case_conclusion} @{syntax name} (@{syntax name} * ) - ; - @@{attribute params} ((@{syntax name} * ) + @'and') - ; - @@{attribute consumes} @{syntax int}? - \} - - \begin{description} - - \item @{command "case"}~@{text "(c x\<^sub>1 \ x\<^sub>m)"} invokes a named local - context @{text "c: x\<^sub>1, \, x\<^sub>m, \\<^sub>1, \, \\<^sub>m"}, as provided by an - appropriate proof method (such as @{method_ref cases} and - @{method_ref induct}). The command ``@{command "case"}~@{text "(c - x\<^sub>1 \ x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \ - x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ \\<^sub>n"}''. - - \item @{command "print_cases"} prints all local contexts of the - current state, using Isar proof language notation. - - \item @{attribute case_names}~@{text "c\<^sub>1 \ c\<^sub>k"} declares names for - the local contexts of premises of a theorem; @{text "c\<^sub>1, \, c\<^sub>k"} - refers to the \emph{prefix} of the list of premises. Each of the - cases @{text "c\<^sub>i"} can be of the form @{text "c[h\<^sub>1 \ h\<^sub>n]"} where - the @{text "h\<^sub>1 \ h\<^sub>n"} are the names of the hypotheses in case @{text "c\<^sub>i"} - from left to right. - - \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \ d\<^sub>k"} declares - names for the conclusions of a named premise @{text c}; here @{text - "d\<^sub>1, \, d\<^sub>k"} refers to the prefix of arguments of a logical formula - built by nesting a binary connective (e.g.\ @{text "\"}). - - Note that proof methods such as @{method induct} and @{method - coinduct} already provide a default name for the conclusion as a - whole. The need to name subformulas only arises with cases that - split into several sub-cases, as in common co-induction rules. - - \item @{attribute params}~@{text "p\<^sub>1 \ p\<^sub>m \ \ q\<^sub>1 \ q\<^sub>n"} renames - the innermost parameters of premises @{text "1, \, n"} of some - theorem. An empty list of names may be given to skip positions, - leaving the present parameters unchanged. - - Note that the default usage of case rules does \emph{not} directly - expose parameters to the proof context. - - \item @{attribute consumes}~@{text n} declares the number of ``major - premises'' of a rule, i.e.\ the number of facts to be consumed when - it is applied by an appropriate proof method. The default value of - @{attribute consumes} is @{text "n = 1"}, which is appropriate for - the usual kind of cases and induction rules for inductive sets (cf.\ - \secref{sec:hol-inductive}). Rules without any @{attribute - consumes} declaration given are treated as if @{attribute - consumes}~@{text 0} had been specified. - - A negative @{text n} is interpreted relatively to the total number - of premises of the rule in the target context. Thus its absolute - value specifies the remaining number of premises, after subtracting - the prefix of major premises as indicated above. This form of - declaration has the technical advantage of being stable under more - morphisms, notably those that export the result from a nested - @{command_ref context} with additional assumptions. - - Note that explicit @{attribute consumes} declarations are only - rarely needed; this is already taken care of automatically by the - higher-level @{attribute cases}, @{attribute induct}, and - @{attribute coinduct} declarations. - - \end{description} -\ - - -subsection \Proof methods\ - -text \ - \begin{matharray}{rcl} - @{method_def cases} & : & @{text method} \\ - @{method_def induct} & : & @{text method} \\ - @{method_def induction} & : & @{text method} \\ - @{method_def coinduct} & : & @{text method} \\ - \end{matharray} - - The @{method cases}, @{method induct}, @{method induction}, - and @{method coinduct} - methods provide a uniform interface to common proof techniques over - datatypes, inductive predicates (or sets), recursive functions etc. - The corresponding rules may be specified and instantiated in a - casual manner. Furthermore, these methods provide named local - contexts that may be invoked via the @{command "case"} proof command - within the subsequent proof text. This accommodates compact proof - texts even when reasoning about large specifications. - - The @{method induct} method also provides some additional - infrastructure in order to be applicable to structure statements - (either using explicit meta-level connectives, or including facts - and parameters separately). This avoids cumbersome encoding of - ``strengthened'' inductive statements within the object-logic. - - Method @{method induction} differs from @{method induct} only in - the names of the facts in the local context invoked by the @{command "case"} - command. - - @{rail \ - @@{method cases} ('(' 'no_simp' ')')? \ - (@{syntax insts} * @'and') rule? - ; - (@@{method induct} | @@{method induction}) - ('(' 'no_simp' ')')? (definsts * @'and') \ arbitrary? taking? rule? - ; - @@{method coinduct} @{syntax insts} taking rule? - ; - - rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +) - ; - definst: @{syntax name} ('==' | '\') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst} - ; - definsts: ( definst * ) - ; - arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +) - ; - taking: 'taking' ':' @{syntax insts} - \} - - \begin{description} - - \item @{method cases}~@{text "insts R"} applies method @{method - rule} with an appropriate case distinction theorem, instantiated to - the subjects @{text insts}. Symbolic case names are bound according - to the rule's local contexts. - - The rule is determined as follows, according to the facts and - arguments passed to the @{method cases} method: - - \medskip - \begin{tabular}{llll} - facts & & arguments & rule \\\hline - @{text "\ R"} & @{method cases} & & implicit rule @{text R} \\ - & @{method cases} & & classical case split \\ - & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\ - @{text "\ A t"} & @{method cases} & @{text "\"} & inductive predicate/set elimination (of @{text A}) \\ - @{text "\"} & @{method cases} & @{text "\ rule: R"} & explicit rule @{text R} \\ - \end{tabular} - \medskip - - Several instantiations may be given, referring to the \emph{suffix} - of premises of the case rule; within each premise, the \emph{prefix} - of variables is instantiated. In most situations, only a single - term needs to be specified; this refers to the first variable of the - last premise (it is usually the same for all cases). The @{text - "(no_simp)"} option can be used to disable pre-simplification of - cases (see the description of @{method induct} below for details). - - \item @{method induct}~@{text "insts R"} and - @{method induction}~@{text "insts R"} are analogous to the - @{method cases} method, but refer to induction rules, which are - determined as follows: - - \medskip - \begin{tabular}{llll} - facts & & arguments & rule \\\hline - & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\ - @{text "\ A x"} & @{method induct} & @{text "\"} & predicate/set induction (of @{text A}) \\ - @{text "\"} & @{method induct} & @{text "\ rule: R"} & explicit rule @{text R} \\ - \end{tabular} - \medskip - - Several instantiations may be given, each referring to some part of - a mutual inductive definition or datatype --- only related partial - induction rules may be used together, though. Any of the lists of - terms @{text "P, x, \"} refers to the \emph{suffix} of variables - present in the induction rule. This enables the writer to specify - only induction variables, or both predicates and variables, for - example. - - Instantiations may be definitional: equations @{text "x \ t"} - introduce local definitions, which are inserted into the claim and - discharged after applying the induction rule. Equalities reappear - in the inductive cases, but have been transformed according to the - induction principle being involved here. In order to achieve - practically useful induction hypotheses, some variables occurring in - @{text t} need to be fixed (see below). Instantiations of the form - @{text t}, where @{text t} is not a variable, are taken as a - shorthand for \mbox{@{text "x \ t"}}, where @{text x} is a fresh - variable. If this is not intended, @{text t} has to be enclosed in - parentheses. By default, the equalities generated by definitional - instantiations are pre-simplified using a specific set of rules, - usually consisting of distinctness and injectivity theorems for - datatypes. This pre-simplification may cause some of the parameters - of an inductive case to disappear, or may even completely delete - some of the inductive cases, if one of the equalities occurring in - their premises can be simplified to @{text False}. The @{text - "(no_simp)"} option can be used to disable pre-simplification. - Additional rules to be used in pre-simplification can be declared - using the @{attribute_def induct_simp} attribute. - - The optional ``@{text "arbitrary: x\<^sub>1 \ x\<^sub>m"}'' - specification generalizes variables @{text "x\<^sub>1, \, - x\<^sub>m"} of the original goal before applying induction. One can - separate variables by ``@{text "and"}'' to generalize them in other - goals then the first. Thus induction hypotheses may become - sufficiently general to get the proof through. Together with - definitional instantiations, one may effectively perform induction - over expressions of a certain structure. - - The optional ``@{text "taking: t\<^sub>1 \ t\<^sub>n"}'' - specification provides additional instantiations of a prefix of - pending variables in the rule. Such schematic induction rules - rarely occur in practice, though. - - \item @{method coinduct}~@{text "inst R"} is analogous to the - @{method induct} method, but refers to coinduction rules, which are - determined as follows: - - \medskip - \begin{tabular}{llll} - goal & & arguments & rule \\\hline - & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\ - @{text "A x"} & @{method coinduct} & @{text "\"} & predicate/set coinduction (of @{text A}) \\ - @{text "\"} & @{method coinduct} & @{text "\ rule: R"} & explicit rule @{text R} \\ - \end{tabular} - - Coinduction is the dual of induction. Induction essentially - eliminates @{text "A x"} towards a generic result @{text "P x"}, - while coinduction introduces @{text "A x"} starting with @{text "B - x"}, for a suitable ``bisimulation'' @{text B}. The cases of a - coinduct rule are typically named after the predicates or sets being - covered, while the conclusions consist of several alternatives being - named after the individual destructor patterns. - - The given instantiation refers to the \emph{suffix} of variables - occurring in the rule's major premise, or conclusion if unavailable. - An additional ``@{text "taking: t\<^sub>1 \ t\<^sub>n"}'' - specification may be required in order to specify the bisimulation - to be used in the coinduction step. - - \end{description} - - Above methods produce named local contexts, as determined by the - instantiated rule as given in the text. Beyond that, the @{method - induct} and @{method coinduct} methods guess further instantiations - from the goal specification itself. Any persisting unresolved - schematic variables of the resulting rule will render the the - corresponding case invalid. The term binding @{variable ?case} for - the conclusion will be provided with each case, provided that term - is fully specified. - - The @{command "print_cases"} command prints all named cases present - in the current proof state. - - \medskip Despite the additional infrastructure, both @{method cases} - and @{method coinduct} merely apply a certain rule, after - instantiation, while conforming due to the usual way of monotonic - natural deduction: the context of a structured statement @{text - "\x\<^sub>1 \ x\<^sub>m. \\<^sub>1 \ \ \\<^sub>n \ \"} - reappears unchanged after the case split. - - The @{method induct} method is fundamentally different in this - respect: the meta-level structure is passed through the - ``recursive'' course involved in the induction. Thus the original - statement is basically replaced by separate copies, corresponding to - the induction hypotheses and conclusion; the original goal context - is no longer available. Thus local assumptions, fixed parameters - and definitions effectively participate in the inductive rephrasing - of the original statement. - - In @{method induct} proofs, local assumptions introduced by cases are split - into two different kinds: @{text hyps} stemming from the rule and - @{text prems} from the goal statement. This is reflected in the - extracted cases accordingly, so invoking ``@{command "case"}~@{text - c}'' will provide separate facts @{text c.hyps} and @{text c.prems}, - as well as fact @{text c} to hold the all-inclusive list. - - In @{method induction} proofs, local assumptions introduced by cases are - split into three different kinds: @{text IH}, the induction hypotheses, - @{text hyps}, the remaining hypotheses stemming from the rule, and - @{text prems}, the assumptions from the goal statement. The names are - @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above. - - - \medskip Facts presented to either method are consumed according to - the number of ``major premises'' of the rule involved, which is - usually 0 for plain cases and induction rules of datatypes etc.\ and - 1 for rules of inductive predicates or sets and the like. The - remaining facts are inserted into the goal verbatim before the - actual @{text cases}, @{text induct}, or @{text coinduct} rule is - applied. -\ - - -subsection \Declaring rules\ - -text \ - \begin{matharray}{rcl} - @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{attribute_def cases} & : & @{text attribute} \\ - @{attribute_def induct} & : & @{text attribute} \\ - @{attribute_def coinduct} & : & @{text attribute} \\ - \end{matharray} - - @{rail \ - @@{attribute cases} spec - ; - @@{attribute induct} spec - ; - @@{attribute coinduct} spec - ; - - spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del' - \} - - \begin{description} - - \item @{command "print_induct_rules"} prints cases and induct rules - for predicates (or sets) and types of the current context. - - \item @{attribute cases}, @{attribute induct}, and @{attribute - coinduct} (as attributes) declare rules for reasoning about - (co)inductive predicates (or sets) and types, using the - corresponding methods of the same name. Certain definitional - packages of object-logics usually declare emerging cases and - induction rules as expected, so users rarely need to intervene. - - Rules may be deleted via the @{text "del"} specification, which - covers all of the @{text "type"}/@{text "pred"}/@{text "set"} - sub-categories simultaneously. For example, @{attribute - cases}~@{text del} removes any @{attribute cases} rules declared for - some type, predicate, or set. - - Manual rule declarations usually refer to the @{attribute - case_names} and @{attribute params} attributes to adjust names of - cases and parameters of a rule; the @{attribute consumes} - declaration is taken care of automatically: @{attribute - consumes}~@{text 0} is specified for ``type'' rules and @{attribute - consumes}~@{text 1} for ``predicate'' / ``set'' rules. - - \end{description} -\ - end