doc-src/IsarRef/hol.tex

   rulify & : & \isaratt \\
   rulify_prems & : & \isaratt \\
 \end{matharray}
 
 \begin{descr}
-
+  
 \item [$rulify$] puts a theorem into object-rule form, replacing implication
   and universal quantification of HOL by the corresponding meta-logical
-  connectives.  This is the same operation as performed by the
-  \texttt{qed_spec_mp} ML function.
+  connectives.  This is the same operation as performed in
+  \texttt{qed_spec_mp} in ML.
   
 \item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a
   rule.
 
 \end{descr}

 \end{descr}
 
 
 \section{Records}\label{sec:record}
 
-%FIXME record_split method
 \indexisarcmd{record}
 \begin{matharray}{rcl}
   \isarcmd{record} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 

 
 \railalias{repdatatype}{rep\_datatype}
 \railterm{repdatatype}
 
 \begin{rail}
-  'datatype' (parname? typespec infix? \\ '=' (constructor + '|') + 'and')
-  ;
-  repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
-  ;
-
-  constructor: name (type * ) mixfix? comment?
-  ;
+  'datatype' (dtspec + 'and')
+  ;
+  repdatatype (name * ) dtrules
+  ;
+
+  dtspec: parname? typespec infix? '=' (cons + '|')
+  ;
+  cons: name (type * ) mixfix? comment?
+  ;
+  dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
 \end{rail}
 
 \begin{descr}
 \item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
 \item [$\isarkeyword{rep_datatype}$] represents existing types as inductive

 
 
 \section{Recursive functions}
 
 \indexisarcmd{primrec}\indexisarcmd{recdef}
+\indexisaratt{recdef-simp}\indexisaratt{recdef-cong}\indexisaratt{recdef-wf}
 \begin{matharray}{rcl}
   \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
   \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
+  recdef_simp & : & \isaratt \\
+  recdef_cong & : & \isaratt \\
+  recdef_wf & : & \isaratt \\
 %FIXME
 %  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
+\railalias{recdefsimp}{recdef\_simp}
+\railterm{recdefsimp}
+
+\railalias{recdefcong}{recdef\_cong}
+\railterm{recdefcong}
+
+\railalias{recdefwf}{recdef\_wf}
+\railterm{recdefwf}
+
 \begin{rail}
   'primrec' parname? (equation + )
   ;
-  'recdef' name term (equation +) hints
-  ;
-
-  equation: thmdecl? prop comment?
-  ;
-  hints: ('congs' thmrefs)?
+  'recdef' name term (eqn + ) hints?
+  ;
+  (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
+  ;
+
+  equation: thmdecl? eqn
+  ;
+  eqn: prop comment?
+  ;
+  hints: '(' 'hints' (recdefmod * ) ')'
+  ;
+  recdefmod: (('simp' | 'cong' | 'wf' | 'split' | 'iff') (() | 'add' | 'del') ':' thmrefs) | clamod
   ;
 \end{rail}
 
 \begin{descr}
 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over
-  datatypes.
+  datatypes, see also \cite{isabelle-HOL}.
 \item [$\isarkeyword{recdef}$] defines general well-founded recursive
-  functions (using the TFL package).
-\end{descr}
-
-Both definitions accommodate reasoning by induction (cf.\ 
+  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
+  $simp$, $cong$, and $wf$ hints refer to auxiliary rules to be used in the
+  internal automated proof process of TFL; the other declarations refer to the
+  Simplifier and Classical reasoner (\S\ref{sec:simplifier},
+  \S\ref{sec:classical}, \S\ref{sec:clasimp}) that are used internally.
+
+\item [$recdef_simps$, $recdef_cong$, and $recdef_wf$] declare global hints
+  for $\isarkeyword{recdef}$.
+\end{descr}
+
+Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 
 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
 of the function definition) refers to a specific induction rule, with
 parameters named according to the user-specified equations.  Case names of
 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of
 $\isarkeyword{recdef}$ are numbered (starting from $1$).

 $f\mathord.simps$, where $f$ is the (collective) name of the functions
 defined.  Individual equations may be named explicitly as well; note that for
 $\isarkeyword{recdef}$ each specification given by the user may result in
 several theorems.
 
-See \cite{isabelle-HOL} for further information on recursive function
-definitions in HOL.
-
 
 \section{(Co)Inductive sets}
 
 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono}
 \begin{matharray}{rcl}
   \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
-  \isarcmd{coinductive}^* & : & \isartrans{theory}{theory} \\
+  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
   mono & : & \isaratt \\
 \end{matharray}
 
 \railalias{condefs}{con\_defs}
 \railterm{condefs}
 
 \begin{rail}
-  ('inductive' | 'coinductive') (term comment? +) \\
-    'intros' attributes? (thmdecl? prop comment? +) \\
-    'monos' thmrefs comment? \\ condefs thmrefs comment?
+  ('inductive' | 'coinductive') sets intros monos?
   ;
   'mono' (() | 'add' | 'del')
+  ;
+
+  sets: (term comment? +)
+  ;
+  intros: 'intros' attributes? (thmdecl? prop comment? +)
+  ;
+  monos: 'monos' thmrefs comment?
   ;
 \end{rail}
 
 \begin{descr}
 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define

 via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
 \S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
 about large specifications.
 
 \begin{rail}
-  'cases' ('(' 'simplified' ')')? ('(' 'open' ')')? \\ (insts * 'and') rule?  ;
-
-  'induct' ('(' 'stripped' ')')? ('(' 'open' ')')? \\ (insts * 'and') rule?
-  ;
-
+  'cases' simplified? open? args rule?
+  ;
+  'induct' stripped? open? args rule?
+  ;
+
+  simplified: '(' 'simplified' ')'
+  ;
+  stripped: '(' 'stripped' ')'
+  ;
+  open: '(' 'open' ')'
+  ;
+  args: (insts * 'and') 
+  ;
   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
   ;
 \end{rail}
 
 \begin{descr}