doc-src/IsarRef/logics.tex
changeset 13024 0461b281c2b5
parent 13016 c039b8ede204
child 13027 ddf235f2384a
     1.1 --- a/doc-src/IsarRef/logics.tex	Tue Mar 05 18:54:55 2002 +0100
     1.2 +++ b/doc-src/IsarRef/logics.tex	Tue Mar 05 18:55:46 2002 +0100
     1.3 @@ -149,7 +149,7 @@
     1.4  \railterm{complete}
     1.5  
     1.6  \begin{rail}
     1.7 -  splitformat (((name * ) + 'and') | ('(' complete ')'))
     1.8 +  splitformat (((name *) + 'and') | ('(' complete ')'))
     1.9    ;
    1.10  \end{rail}
    1.11  
    1.12 @@ -396,12 +396,12 @@
    1.13  \begin{rail}
    1.14    'datatype' (dtspec + 'and')
    1.15    ;
    1.16 -  repdatatype (name * ) dtrules
    1.17 +  repdatatype (name *) dtrules
    1.18    ;
    1.19  
    1.20    dtspec: parname? typespec infix? '=' (cons + '|')
    1.21    ;
    1.22 -  cons: name (type * ) mixfix?
    1.23 +  cons: name (type *) mixfix?
    1.24    ;
    1.25    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    1.26  \end{rail}
    1.27 @@ -421,8 +421,9 @@
    1.28  old-style theory syntax being used there!  Apart from proper proof methods for
    1.29  case-analysis and induction, there are also emulations of ML tactics
    1.30  \texttt{case_tac} and \texttt{induct_tac} available, see
    1.31 -\S\ref{sec:induct_tac}; these admit to refer directly to the internal
    1.32 -structure of subgoals (including internally bound parameters).
    1.33 +\S\ref{sec:hol-induct-tac} or \S\ref{sec:zf-induct-tac}; these admit to refer
    1.34 +directly to the internal structure of subgoals (including internally bound
    1.35 +parameters).
    1.36  
    1.37  
    1.38  \subsection{Recursive functions}\label{sec:recursion}
    1.39 @@ -432,8 +433,7 @@
    1.40    \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
    1.41    \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
    1.42    \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
    1.43 -%FIXME
    1.44 -%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
    1.45 +%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\  %FIXME
    1.46  \end{matharray}
    1.47  
    1.48  \railalias{recdefsimp}{recdef\_simp}
    1.49 @@ -449,16 +449,16 @@
    1.50  \railterm{recdeftc}
    1.51  
    1.52  \begin{rail}
    1.53 -  'primrec' parname? (equation + )
    1.54 +  'primrec' parname? (equation +)
    1.55    ;
    1.56 -  'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
    1.57 +  'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
    1.58    ;
    1.59    recdeftc thmdecl? tc
    1.60    ;
    1.61  
    1.62    equation: thmdecl? prop
    1.63    ;
    1.64 -  hints: '(' 'hints' (recdefmod * ) ')'
    1.65 +  hints: '(' 'hints' (recdefmod *) ')'
    1.66    ;
    1.67    recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
    1.68    ;
    1.69 @@ -467,23 +467,27 @@
    1.70  \end{rail}
    1.71  
    1.72  \begin{descr}
    1.73 +  
    1.74  \item [$\isarkeyword{primrec}$] defines primitive recursive functions over
    1.75 -  datatypes, see also \cite{isabelle-HOL} FIXME.
    1.76 +  datatypes, see also \cite{isabelle-HOL}.
    1.77 +  
    1.78  \item [$\isarkeyword{recdef}$] defines general well-founded recursive
    1.79 -  functions (using the TFL package), see also \cite{isabelle-HOL} FIXME.  The
    1.80 +  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
    1.81    $(permissive)$ option tells TFL to recover from failed proof attempts,
    1.82    returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
    1.83    $recdef_wf$ hints refer to auxiliary rules to be used in the internal
    1.84 -  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\
    1.85 +  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\ 
    1.86    \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
    1.87 -  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
    1.88 +  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 
    1.89    \S\ref{sec:classical}).
    1.90 +  
    1.91  \item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
    1.92    termination condition number $i$ (default $1$) as generated by a
    1.93    $\isarkeyword{recdef}$ definition of constant $c$.
    1.94 -
    1.95 +  
    1.96    Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
    1.97    internal proofs without manual intervention.
    1.98 +
    1.99  \end{descr}
   1.100  
   1.101  Both kinds of recursive definitions accommodate reasoning by induction (cf.\
   1.102 @@ -533,9 +537,6 @@
   1.103    mono & : & \isaratt \\
   1.104  \end{matharray}
   1.105  
   1.106 -\railalias{condefs}{con\_defs}
   1.107 -\railterm{condefs}
   1.108 -
   1.109  \begin{rail}
   1.110    ('inductive' | 'coinductive') sets intros monos?
   1.111    ;
   1.112 @@ -557,8 +558,8 @@
   1.113    automated monotonicity proof of $\isarkeyword{inductive}$.
   1.114  \end{descr}
   1.115  
   1.116 -See \cite{isabelle-HOL} FIXME for further information on inductive definitions
   1.117 -in HOL.
   1.118 +See \cite{isabelle-HOL} for further information on inductive definitions in
   1.119 +HOL, but note that this covers the old-style theory format.
   1.120  
   1.121  
   1.122  \subsection{Arithmetic proof support}
   1.123 @@ -584,7 +585,7 @@
   1.124  performed by the Simplifier.
   1.125  
   1.126  
   1.127 -\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
   1.128 +\subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac}
   1.129  
   1.130  The following important tactical tools of Isabelle/HOL have been ported to
   1.131  Isar.  These should be never used in proper proof texts!
   1.132 @@ -681,7 +682,7 @@
   1.133  
   1.134    dmspec: typespec '=' (cons + '|')
   1.135    ;
   1.136 -  cons: name (type * ) mixfix?
   1.137 +  cons: name (type *) mixfix?
   1.138    ;
   1.139    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
   1.140  \end{rail}
   1.141 @@ -698,11 +699,142 @@
   1.142  
   1.143  \subsection{Type checking}
   1.144  
   1.145 -FIXME
   1.146 +The ZF logic is essentially untyped, so the concept of ``type checking'' is
   1.147 +performed as logical reasoning about set-membership statements.  A special
   1.148 +method assists users in this task; a version of this is already declared as a
   1.149 +``solver'' in the default Simplifier context.
   1.150 +
   1.151 +\indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC}
   1.152 +
   1.153 +\begin{matharray}{rcl}
   1.154 +  \isarcmd{print_tcset}^* & : & \isarkeep{theory~|~proof} \\
   1.155 +  typecheck & : & \isarmeth \\
   1.156 +  TC & : & \isaratt \\
   1.157 +\end{matharray}
   1.158 +
   1.159 +\begin{rail}
   1.160 +  'TC' (() | 'add' | 'del')
   1.161 +  ;
   1.162 +\end{rail}
   1.163 +
   1.164 +\begin{descr}
   1.165 +  
   1.166 +\item [$\isarcmd{print_tcset}$] prints the collection of typechecking rules of
   1.167 +  the current context.
   1.168 +  
   1.169 +  Note that the component built into the Simplifier only knows about those
   1.170 +  rules being declared globally in the theory!
   1.171 +  
   1.172 +\item [$typecheck$] attempts to solve any pending type-checking problems in
   1.173 +  subgoals.
   1.174 +  
   1.175 +\item [$TC$] adds or deletes type-checking rules from the context.
   1.176 +
   1.177 +\end{descr}
   1.178 +
   1.179 +
   1.180 +\subsection{(Co)Inductive sets and datatypes}
   1.181 +
   1.182 +\subsubsection{Set definitions}
   1.183 +
   1.184 +In ZF everything is a set.  The generic inductive package also provides a
   1.185 +specific view for ``datatype'' specifications.  Coinductive definitions are
   1.186 +available as well.
   1.187 +
   1.188 +\indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive}
   1.189 +\indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}
   1.190 +\begin{matharray}{rcl}
   1.191 +  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
   1.192 +  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
   1.193 +  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
   1.194 +  \isarcmd{codatatype} & : & \isartrans{theory}{theory} \\
   1.195 +\end{matharray}
   1.196 +
   1.197 +\railalias{CONDEFS}{con\_defs}
   1.198 +\railterm{CONDEFS}
   1.199 +
   1.200 +\railalias{TYPEINTROS}{type\_intros}
   1.201 +\railterm{TYPEINTROS}
   1.202 +
   1.203 +\railalias{TYPEELIMS}{type\_elims}
   1.204 +\railterm{TYPEELIMS}
   1.205 +
   1.206 +\begin{rail}
   1.207 +  ('inductive' | 'coinductive') domains intros hints
   1.208 +  ;
   1.209  
   1.210 -\subsection{Inductive sets and datatypes}
   1.211 +  domains: 'domains' (term + '+') ('<=' | subseteq) term
   1.212 +  ;
   1.213 +  intros: 'intros' (thmdecl? prop +)
   1.214 +  ;
   1.215 +  hints: monos? condefs? typeintros? typeelims?
   1.216 +  ;
   1.217 +  monos: ('monos' thmrefs)?
   1.218 +  ;
   1.219 +  condefs: (CONDEFS thmrefs)?
   1.220 +  ;
   1.221 +  typeintros: (TYPEINTROS thmrefs)?
   1.222 +  ;
   1.223 +  typeelims: (TYPEELIMS thmrefs)?
   1.224 +  ;
   1.225 +\end{rail}
   1.226 +
   1.227 +In the following diagram $monos$, $typeintros$, and $typeelims$ are the same
   1.228 +as above.
   1.229 +
   1.230 +\begin{rail}
   1.231 +  ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
   1.232 +  ;
   1.233 +
   1.234 +  domain: ('<=' | subseteq) term
   1.235 +  ;
   1.236 +  dtspec: term '=' (con + '|')
   1.237 +  ;
   1.238 +  con: name ('(' (term ',' +) ')')?  
   1.239 +  ;
   1.240 +  hints: monos? typeintros? typeelims?
   1.241 +  ;
   1.242 +\end{rail}
   1.243 +
   1.244 +See \cite{isabelle-ZF} for further information on inductive definitions in
   1.245 +HOL, but note that this covers the old-style theory format.
   1.246  
   1.247 -FIXME
   1.248 +
   1.249 +\subsubsection{Primitive recursive functions}
   1.250 +
   1.251 +\indexisarcmdof{ZF}{primrec}
   1.252 +\begin{matharray}{rcl}
   1.253 +  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
   1.254 +\end{matharray}
   1.255 +
   1.256 +\begin{rail}
   1.257 +  'primrec' (thmdecl? prop +)
   1.258 +  ;
   1.259 +\end{rail}
   1.260 +
   1.261 +
   1.262 +\subsubsection{Cases and induction: emulating tactic scripts}\label{sec:zf-induct-tac}
   1.263 +
   1.264 +The following important tactical tools of Isabelle/ZF have been ported to
   1.265 +Isar.  These should be never used in proper proof texts!
   1.266 +
   1.267 +\indexisarmethof{ZF}{case-tac}\indexisarmethof{ZF}{induct-tac}
   1.268 +\indexisarmethof{ZF}{ind-cases}\indexisarcmdof{ZF}{inductive-cases}
   1.269 +\begin{matharray}{rcl}
   1.270 +  case_tac^* & : & \isarmeth \\
   1.271 +  induct_tac^* & : & \isarmeth \\
   1.272 +  ind_cases^* & : & \isarmeth \\
   1.273 +  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
   1.274 +\end{matharray}
   1.275 +
   1.276 +\begin{rail}
   1.277 +  (casetac | inducttac) goalspec? name
   1.278 +  ;
   1.279 +  indcases (prop +)
   1.280 +  ;
   1.281 +  inductivecases (thmdecl? (prop +) + 'and')
   1.282 +  ;
   1.283 +\end{rail}
   1.284  
   1.285  
   1.286  %%% Local Variables: