doc-src/IsarRef/generic.tex
changeset 10548 e8c774c12105
parent 10318 e47c221beded
child 10627 dc3eff1b7556
equal deleted 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