doc-src/IsarRef/generic.tex
changeset 8507 d22fcea34cb7
parent 8483 b437907f9b26
child 8517 062e6cd78534
equal deleted inserted replaced
8506:e2204e3df61b 8507:d22fcea34cb7
    80   export^* & : & \isaratt \\
    80   export^* & : & \isaratt \\
    81   transfer & : & \isaratt \\[0.5ex]
    81   transfer & : & \isaratt \\[0.5ex]
    82 \end{matharray}
    82 \end{matharray}
    83 
    83 
    84 \begin{rail}
    84 \begin{rail}
    85   ('tag' | 'untag') (nameref+)
    85   'tag' (nameref+)
       
    86   ;
       
    87   'untag' name
    86   ;
    88   ;
    87   'OF' thmrefs
    89   'OF' thmrefs
    88   ;
    90   ;
    89   ('RS' | 'COMP') nat? thmref
    91   ('RS' | 'COMP') nat? thmref
    90   ;
    92   ;
    98   inst: underscore | term
   100   inst: underscore | term
    99   ;
   101   ;
   100 \end{rail}
   102 \end{rail}
   101 
   103 
   102 \begin{descr}
   104 \begin{descr}
   103 \item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,
   105 \item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
   104   respectively.  Tags may be any list of strings that serve as comment for
   106   theorem.  Tags may be any list of strings that serve as comment for some
   105   some tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
   107   tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
   106   result).
   108   result).  The first string is considered the tag name, the rest its
       
   109   arguments.  Note that untag removes any tags of the same name.
   107 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
   110 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
   108   $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
   111   $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
   109   the reversed order).  Note that premises may be skipped by including
   112   the reversed order).  Note that premises may be skipped by including
   110   ``$\_$'' (underscore) as argument.
   113   ``$\_$'' (underscore) as argument.
   111   
   114   
   172 command required.
   175 command required.
   173 
   176 
   174 \begin{rail}
   177 \begin{rail}
   175   ('also' | 'finally') transrules? comment?
   178   ('also' | 'finally') transrules? comment?
   176   ;
   179   ;
   177   'trans' (() | 'add' ':' | 'del' ':') thmrefs
   180   'trans' (() | 'add' | 'del')
   178   ;
   181   ;
   179 
   182 
   180   transrules: '(' thmrefs ')' interest?
   183   transrules: '(' thmrefs ')' interest?
   181   ;
   184   ;
   182 \end{rail}
   185 \end{rail}
   228 
   231 
   229 \medskip
   232 \medskip
   230 
   233 
   231 The $\CASENAME$ command provides a shorthand to refer to certain parts of
   234 The $\CASENAME$ command provides a shorthand to refer to certain parts of
   232 logical context symbolically.  Proof methods may provide an environment of
   235 logical context symbolically.  Proof methods may provide an environment of
   233 named ``cases'' of the form $c\colon \vec x, \vec \chi$.  Then the effect of
   236 named ``cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of
   234 $\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
   237 $\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   235 
   238 
   236 It is important to note that $\CASENAME$ does \emph{not} provide any means to
   239 It is important to note that $\CASENAME$ does \emph{not} provide any means to
   237 peek at the current goal state, which is treated as strictly non-observable in
   240 peek at the current goal state, which is treated as strictly non-observable in
   238 Isar!  Instead, the cases considered here usually emerge in a canonical way
   241 Isar!  Instead, the cases considered here usually emerge in a canonical way
   239 from certain pieces of specification that appear in the theory somewhere else
   242 from certain pieces of specification that appear in the theory somewhere else
   259   'params' ((name * ) + 'and')
   262   'params' ((name * ) + 'and')
   260   ;
   263   ;
   261 \end{rail}
   264 \end{rail}
   262 
   265 
   263 \begin{descr}
   266 \begin{descr}
   264 \item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \chi$,
   267 \item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
   265   as provided by an appropriate proof method (such as $cases$ and $induct$,
   268   as provided by an appropriate proof method (such as $cases$ and $induct$,
   266   see \S\ref{sec:induct-method}).  The command $\CASE{c}$ abbreviates
   269   see \S\ref{sec:induct-method}).  The command $\CASE{c}$ abbreviates
   267   $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
   270   $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   268 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
   271 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
   269   goal context, using Isar proof language notation.  This is a diagnostic
   272   goal context, using Isar proof language notation.  This is a diagnostic
   270   command; $undo$ does not apply.
   273   command; $undo$ does not apply.
   271 \item [$case_names~\vec c$] declares names for the local contexts of premises
   274 \item [$case_names~\vec c$] declares names for the local contexts of premises
   272   of some theorem ($\vec c$ refers to the \emph{suffix} of the list premises).
   275   of some theorem ($\vec c$ refers to the \emph{suffix} of the list premises).