doc-src/IsarRef/generic.tex
 changeset 11691 fc9bd420162c parent 11469 57b072f00626 child 12618 43a97a2155d0
equal inserted replaced
11690:cb64368fb405 11691:fc9bd420162c
   852   any effect on automated proof tools, but only on simple methods such as
   852   any effect on automated proof tools, but only on simple methods such as
   853   $rule$ (see \S\ref{sec:misc-methods}).
   853   $rule$ (see \S\ref{sec:misc-methods}).
   854 \end{descr}
   854 \end{descr}
   855
   855
   856
   856

   857 \section{Proof by cases and induction}\label{sec:induct-method}

   858

   859 \subsection{Proof methods}\label{sec:induct-method-proper}

   860

   861 \indexisarmeth{cases}\indexisarmeth{induct}

   862 \begin{matharray}{rcl}

   863   cases & : & \isarmeth \\

   864   induct & : & \isarmeth \\

   865 \end{matharray}

   866

   867 The $cases$ and $induct$ methods provide a uniform interface to case analysis

   868 and induction over datatypes, inductive sets, and recursive functions.  The

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

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

   871 via the $\CASENAME$ proof command within the subsequent proof text (cf.\

   872 \S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning

   873 about large specifications.

   874

   875 Note that the full spectrum of this generic functionality is currently only

   876 supported by Isabelle/HOL, when used in conjunction with advanced definitional

   877 packages (see especially \S\ref{sec:datatype} and \S\ref{sec:inductive}).

   878

   879 \begin{rail}

   880   'cases' spec

   881   ;

   882   'induct' spec

   883   ;

   884

   885   spec: open? args rule? params?

   886   ;

   887   open: '(' 'open' ')'

   888   ;

   889   args: (insts * 'and')

   890   ;

   891   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref

   892   ;

   893   params: 'of' ':' insts

   894   ;

   895 \end{rail}

   896

   897 \begin{descr}

   898 \item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case

   899   distinction theorem, instantiated to the subjects $insts$.  Symbolic case

   900   names are bound according to the rule's local contexts.

   901

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

   903   passed to the $cases$ method:

   904   \begin{matharray}{llll}

   905     \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline

   906                     & cases &           & \Text{classical case split} \\

   907                     & cases & t         & \Text{datatype exhaustion (type of $t$)} \\

   908     \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\

   909     \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\

   910   \end{matharray}

   911

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

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

   914   variables is instantiated.  In most situations, only a single term needs to

   915   be specified; this refers to the first variable of the last premise (it is

   916   usually the same for all cases).

   917

   918   Additional parameters may be specified as $ps$; these are applied after the

   919   primary instantiation in the same manner as by the $of$ attribute (cf.\

   920   \S\ref{sec:pure-meth-att}).  This feature is rarely needed in practice; a

   921   typical application would be to specify additional arguments for rules

   922   stemming from parameterized inductive definitions (see also

   923   \S\ref{sec:inductive}).

   924

   925   The $open$ option causes the parameters of the new local contexts to be

   926   exposed to the current proof context.  Thus local variables stemming from

   927   distant parts of the theory development may be introduced in an implicit

   928   manner, which can be quite confusing to the reader.  Furthermore, this

   929   option may cause unwanted hiding of existing local variables, resulting in

   930   less robust proof texts.

   931

   932 \item [$induct~insts~R~ps$] is analogous to the $cases$ method, but refers to

   933   induction rules, which are determined as follows:

   934   \begin{matharray}{llll}

   935     \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline

   936                     & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\

   937     \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\

   938     \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\

   939   \end{matharray}

   940

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

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

   943   may be used together, though.  Any of the lists of terms $P, x, \dots$

   944   refers to the \emph{suffix} of variables present in the induction rule.

   945   This enables the writer to specify only induction variables, or both

   946   predicates and variables, for example.

   947

   948   Additional parameters (including the $open$ option) may be given in the same

   949   way as for $cases$, see above.

   950 \end{descr}

   951

   952 Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as

   953 determined by the instantiated rule \emph{before} it has been applied to the

   954 internal proof state.\footnote{As a general principle, Isar proof text may

   955   never refer to parts of proof states directly.} Thus proper use of symbolic

   956 cases usually require the rule to be instantiated fully, as far as the

   957 emerging local contexts and subgoals are concerned.  In particular, for

   958 induction both the predicates and variables have to be specified.  Otherwise

   959 the $\CASENAME$ command would refuse to invoke cases containing schematic

   960 variables.  Furthermore the resulting local goal statement is bound to the

   961 term variable $\Var{case}$\indexisarvar{case} --- for each case where it is

   962 fully specified.

   963

   964 The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named

   965 cases present in the current proof state.

   966

   967 \medskip

   968

   969 It is important to note that there is a fundamental difference of the $cases$

   970 and $induct$ methods in handling of non-atomic goal statements: $cases$ just

   971 applies a certain rule in backward fashion, splitting the result into new

   972 goals with the local contexts being augmented in a purely monotonic manner.

   973

   974 In contrast, $induct$ passes the full goal statement through the recursive''

   975 course involved in the induction.  Thus the original statement is basically

   976 replaced by separate copies, corresponding to the induction hypotheses and

   977 conclusion; the original goal context is no longer available.  This behavior

   978 allows \emph{strengthened induction predicates} to be expressed concisely as

   979 meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to

   980 indicate variable'' parameters $\vec x$ and recursive'' assumptions

   981 $\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec    982 x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.

   983

   984 \medskip

   985

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

   987 major premises'' of the rule involved (see also \S\ref{sec:induct-att} and

   988 \S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules

   989 of datatypes etc.\ and $1$ for rules of inductive sets and the like.  The

   990 remaining facts are inserted into the goal verbatim before the actual $cases$

   991 or $induct$ rule is applied (thus facts may be even passed through an

   992 induction).

   993

   994 Note that whenever facts are present, the default rule selection scheme would

   995 provide a set'' rule only, with the first fact consumed and the rest

   996 inserted into the goal.  In order to pass all facts into a type'' rule

   997 instead, one would have to specify this explicitly, e.g.\ by appending

   998 $type: name$'' to the method argument.

   999

  1000

  1001 \subsection{Declaring rules}\label{sec:induct-att}

  1002

  1003 \indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}

  1004 \begin{matharray}{rcl}

  1005   \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\

  1006   cases & : & \isaratt \\

  1007   induct & : & \isaratt \\

  1008 \end{matharray}

  1009

  1010 \begin{rail}

  1011   'cases' spec

  1012   ;

  1013   'induct' spec

  1014   ;

  1015

  1016   spec: ('type' | 'set') ':' nameref

  1017   ;

  1018 \end{rail}

  1019

  1020 The $cases$ and $induct$ attributes augment the corresponding context of rules

  1021 for reasoning about inductive sets and types.  The standard rules are already

  1022 declared by advanced definitional packages.  For special applications, these

  1023 may be replaced manually by variant versions.

  1024

  1025 Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to

  1026 adjust names of cases and parameters of a rule.

  1027

  1028 The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of

  1029 automatically (if none had been given already): $consumes~0$ is specified for

  1030 type'' rules and $consumes~1$ for set'' rules.

  1031

  1032
   857 %%% Local Variables:
  1033 %%% Local Variables:
   858 %%% mode: latex
  1034 %%% mode: latex
   859 %%% TeX-master: "isar-ref"
  1035 %%% TeX-master: "isar-ref"
   860 %%% End:
  1036 %%% End: