doc-src/IsarRef/generic.tex
 changeset 10548 e8c774c12105 parent 10318 e47c221beded child 10627 dc3eff1b7556
equal inserted replaced
10547:efaba354b7f1 10548:e8c774c12105
   138
   138
   139
   139
   140 \section{Named local contexts (cases)}\label{sec:cases}
   140 \section{Named local contexts (cases)}\label{sec:cases}
   141
   141
   142 \indexisarcmd{case}\indexisarcmd{print-cases}
   142 \indexisarcmd{case}\indexisarcmd{print-cases}
   143 \indexisaratt{case-names}\indexisaratt{params}
   143 \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
   144 \begin{matharray}{rcl}
   144 \begin{matharray}{rcl}
   145   \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
   145   \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
   146   \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
   146   \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
   147   case_names & : & \isaratt \\
   147   case_names & : & \isaratt \\
   148   params & : & \isaratt \\
   148   params & : & \isaratt \\

   149   consumes & : & \isaratt \\
   149 \end{matharray}
   150 \end{matharray}
   150
   151
   151 Basically, Isar proof contexts are built up explicitly using commands like
   152 Basically, Isar proof contexts are built up explicitly using commands like
   152 $\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical
   153 $\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical
   153 verification tasks this can become hard to manage, though.  In particular, a
   154 verification tasks this can become hard to manage, though.  In particular, a
   183   'case' nameref attributes?
   184   'case' nameref attributes?
   184   ;
   185   ;
   185   casenames (name + )
   186   casenames (name + )
   186   ;
   187   ;
   187   'params' ((name * ) + 'and')
   188   'params' ((name * ) + 'and')

   189   ;

   190   'consumes' nat?
   188   ;
   191   ;
   189 \end{rail}
   192 \end{rail}
   190 %FIXME bug in rail
   193 %FIXME bug in rail
   191
   194
   192 \begin{descr}
   195 \begin{descr}
   203   premises $1, \dots, n$ of some theorem.  An empty list of names may be given
   206   premises $1, \dots, n$ of some theorem.  An empty list of names may be given
   204   to skip positions, leaving the present parameters unchanged.
   207   to skip positions, leaving the present parameters unchanged.
   205
   208
   206   Note that the default usage of case rules does \emph{not} directly expose
   209   Note that the default usage of case rules does \emph{not} directly expose
   207   parameters to the proof context (see also \S\ref{sec:induct-method-proper}).
   210   parameters to the proof context (see also \S\ref{sec:induct-method-proper}).

   211 \item [$consumes~n$] declares the number of major premises'' of a rule,

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

   213   appropriate proof method (cf.\ \S\ref{sec:induct-method}).  The default

   214   value of $consumes$ is $n = 1$, which is appropriate for the usual kind of

   215   cases and induction rules for inductive sets (cf.\ \S\ref{sec:inductive}).

   216   Rules without any $consumes$ declaration given are treated as if

   217   $consumes~0$ had been specified.

   218

   219   Note that explicit $consumes$ declarations are only rarely needed; this is

   220   already taken care of automatically by the higher-level $cases$ and $induct$

   221   declarations, see also \S\ref{sec:induct-att}.
   208 \end{descr}
   222 \end{descr}
   209
   223
   210
   224
   211 \section{Generalized existence}\label{sec:obtain}
   225 \section{Generalized existence}\label{sec:obtain}
   212
   226