doc-src/IsarRef/generic.tex
changeset 11691 fc9bd420162c
parent 11469 57b072f00626
child 12618 43a97a2155d0
equal deleted 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: