1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarRef/logics.tex Thu Jan 03 17:48:02 2002 +0100
1.3 @@ -0,0 +1,500 @@
1.4 +
1.5 +\chapter{Object-logic specific elements}\label{ch:logics}
1.6 +
1.7 +\section{General logic setup}\label{sec:object-logic}
1.8 +
1.9 +\indexisarcmd{judgment}
1.10 +\indexisarmeth{atomize}\indexisaratt{atomize}
1.11 +\indexisaratt{rule-format}\indexisaratt{rulify}
1.12 +
1.13 +\begin{matharray}{rcl}
1.14 + \isarcmd{judgment} & : & \isartrans{theory}{theory} \\
1.15 + atomize & : & \isarmeth \\
1.16 + atomize & : & \isaratt \\
1.17 + rule_format & : & \isaratt \\
1.18 + rulify & : & \isaratt \\
1.19 +\end{matharray}
1.20 +
1.21 +The very starting point for any Isabelle object-logic is a ``truth judgment''
1.22 +that links object-level statements to the meta-logic (with its minimal
1.23 +language of $prop$ that covers universal quantification $\Forall$ and
1.24 +implication $\Imp$). Common object-logics are sufficiently expressive to
1.25 +\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
1.26 +language. This is useful in certain situations where a rule needs to be
1.27 +viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
1.28 +\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
1.29 +
1.30 +From the following language elements, only the $atomize$ method and
1.31 +$rule_format$ attribute are occasionally required by end-users, the rest is
1.32 +for those who need to setup their own object-logic. In the latter case
1.33 +existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
1.34 +realistic examples.
1.35 +
1.36 +Generic tools may refer to the information provided by object-logic
1.37 +declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
1.38 +Reasoner \S\ref{sec:classical}).
1.39 +
1.40 +\railalias{ruleformat}{rule\_format}
1.41 +\railterm{ruleformat}
1.42 +
1.43 +\begin{rail}
1.44 + 'judgment' constdecl
1.45 + ;
1.46 + ruleformat ('(' noasm ')')?
1.47 + ;
1.48 +\end{rail}
1.49 +
1.50 +\begin{descr}
1.51 +
1.52 +\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
1.53 + truth judgment of the current object-logic. Its type $\sigma$ should
1.54 + specify a coercion of the category of object-level propositions to $prop$ of
1.55 + the Pure meta-logic; the mixfix annotation $syn$ would typically just link
1.56 + the object language (internally of syntactic category $logic$) with that of
1.57 + $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any
1.58 + theory development.
1.59 +
1.60 +\item [$atomize$] (as a method) rewrites any non-atomic premises of a
1.61 + sub-goal, using the meta-level equations declared via $atomize$ (as an
1.62 + attribute) beforehand. As a result, heavily nested goals become amenable to
1.63 + fundamental operations such as resolution (cf.\ the $rule$ method) and
1.64 + proof-by-assumption (cf.\ $assumption$).
1.65 +
1.66 + A typical collection of $atomize$ rules for a particular object-logic would
1.67 + provide an internalization for each of the connectives of $\Forall$, $\Imp$,
1.68 + and $\equiv$. Meta-level conjunction expressed in the manner of minimal
1.69 + higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$
1.70 + should be covered as well (this is particularly important for locales, see
1.71 + \S\ref{sec:locale}).
1.72 +
1.73 +\item [$rule_format$] rewrites a theorem by the equalities declared as
1.74 + $rulify$ rules in the current object-logic. By default, the result is fully
1.75 + normalized, including assumptions and conclusions at any depth. The
1.76 + $no_asm$ option restricts the transformation to the conclusion of a rule.
1.77 +
1.78 + In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
1.79 + replace (bounded) universal quantification ($\forall$) and implication
1.80 + ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
1.81 +
1.82 +\end{descr}
1.83 +
1.84 +
1.85 +\section{HOL}
1.86 +
1.87 +\subsection{Primitive types}\label{sec:typedef}
1.88 +
1.89 +\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
1.90 +\begin{matharray}{rcl}
1.91 + \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
1.92 + \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
1.93 +\end{matharray}
1.94 +
1.95 +\begin{rail}
1.96 + 'typedecl' typespec infix? comment?
1.97 + ;
1.98 + 'typedef' parname? typespec infix? \\ '=' term comment?
1.99 + ;
1.100 +\end{rail}
1.101 +
1.102 +\begin{descr}
1.103 +\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
1.104 + $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
1.105 + also declares type arity $t :: (term, \dots, term) term$, making $t$ an
1.106 + actual HOL type constructor.
1.107 +\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
1.108 + non-emptiness of the set $A$. After finishing the proof, the theory will be
1.109 + augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL}
1.110 + for more information. Note that user-level theories usually do not directly
1.111 + refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
1.112 + packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and
1.113 + $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
1.114 +\end{descr}
1.115 +
1.116 +
1.117 +\subsection{Low-level tuples}
1.118 +
1.119 +\indexisarattof{HOL}{split-format}
1.120 +\begin{matharray}{rcl}
1.121 + split_format^* & : & \isaratt \\
1.122 +\end{matharray}
1.123 +
1.124 +\railalias{splitformat}{split\_format}
1.125 +\railterm{splitformat}
1.126 +\railterm{complete}
1.127 +
1.128 +\begin{rail}
1.129 + splitformat (((name * ) + 'and') | ('(' complete ')'))
1.130 + ;
1.131 +\end{rail}
1.132 +
1.133 +\begin{descr}
1.134 +
1.135 +\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
1.136 + tuple types into canonical form as specified by the arguments given; $\vec
1.137 + p@i$ refers to occurrences in premise $i$ of the rule. The
1.138 + $split_format~(complete)$ form causes \emph{all} arguments in function
1.139 + applications to be represented canonically according to their tuple type
1.140 + structure.
1.141 +
1.142 + Note that these operations tend to invent funny names for new local
1.143 + parameters to be introduced.
1.144 +
1.145 +\end{descr}
1.146 +
1.147 +
1.148 +\subsection{Records}\label{sec:hol-record}
1.149 +
1.150 +FIXME proof tools (simp, cases/induct; no split!?);
1.151 +
1.152 +FIXME mixfix syntax;
1.153 +
1.154 +\indexisarcmdof{HOL}{record}
1.155 +\begin{matharray}{rcl}
1.156 + \isarcmd{record} & : & \isartrans{theory}{theory} \\
1.157 +\end{matharray}
1.158 +
1.159 +\begin{rail}
1.160 + 'record' typespec '=' (type '+')? (constdecl +)
1.161 + ;
1.162 +\end{rail}
1.163 +
1.164 +\begin{descr}
1.165 +\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
1.166 + defines extensible record type $(\vec\alpha)t$, derived from the optional
1.167 + parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
1.168 + See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on
1.169 + simply-typed extensible records.
1.170 +\end{descr}
1.171 +
1.172 +
1.173 +\subsection{Datatypes}\label{sec:hol-datatype}
1.174 +
1.175 +\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
1.176 +\begin{matharray}{rcl}
1.177 + \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
1.178 + \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
1.179 +\end{matharray}
1.180 +
1.181 +\railalias{repdatatype}{rep\_datatype}
1.182 +\railterm{repdatatype}
1.183 +
1.184 +\begin{rail}
1.185 + 'datatype' (dtspec + 'and')
1.186 + ;
1.187 + repdatatype (name * ) dtrules
1.188 + ;
1.189 +
1.190 + dtspec: parname? typespec infix? '=' (cons + '|')
1.191 + ;
1.192 + cons: name (type * ) mixfix? comment?
1.193 + ;
1.194 + dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
1.195 +\end{rail}
1.196 +
1.197 +\begin{descr}
1.198 +\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL.
1.199 +\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive
1.200 + ones, generating the standard infrastructure of derived concepts (primitive
1.201 + recursion etc.).
1.202 +\end{descr}
1.203 +
1.204 +The induction and exhaustion theorems generated provide case names according
1.205 +to the constructors involved, while parameters are named after the types (see
1.206 +also \S\ref{sec:cases-induct}).
1.207 +
1.208 +See \cite{isabelle-HOL} for more details on datatypes. Note that the theory
1.209 +syntax above has been slightly simplified over the old version, usually
1.210 +requiring more quotes and less parentheses. Apart from proper proof methods
1.211 +for case-analysis and induction, there are also emulations of ML tactics
1.212 +\texttt{case_tac} and \texttt{induct_tac} available, see
1.213 +\S\ref{sec:induct_tac}.
1.214 +
1.215 +
1.216 +\subsection{Recursive functions}\label{sec:recursion}
1.217 +
1.218 +\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
1.219 +\begin{matharray}{rcl}
1.220 + \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
1.221 + \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
1.222 + \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
1.223 +%FIXME
1.224 +% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
1.225 +\end{matharray}
1.226 +
1.227 +\railalias{recdefsimp}{recdef\_simp}
1.228 +\railterm{recdefsimp}
1.229 +
1.230 +\railalias{recdefcong}{recdef\_cong}
1.231 +\railterm{recdefcong}
1.232 +
1.233 +\railalias{recdefwf}{recdef\_wf}
1.234 +\railterm{recdefwf}
1.235 +
1.236 +\railalias{recdeftc}{recdef\_tc}
1.237 +\railterm{recdeftc}
1.238 +
1.239 +\begin{rail}
1.240 + 'primrec' parname? (equation + )
1.241 + ;
1.242 + 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
1.243 + ;
1.244 + recdeftc thmdecl? tc comment?
1.245 + ;
1.246 +
1.247 + equation: thmdecl? eqn
1.248 + ;
1.249 + eqn: prop comment?
1.250 + ;
1.251 + hints: '(' 'hints' (recdefmod * ) ')'
1.252 + ;
1.253 + recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
1.254 + ;
1.255 + tc: nameref ('(' nat ')')?
1.256 + ;
1.257 +\end{rail}
1.258 +
1.259 +\begin{descr}
1.260 +\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
1.261 + datatypes, see also \cite{isabelle-HOL}.
1.262 +\item [$\isarkeyword{recdef}$] defines general well-founded recursive
1.263 + functions (using the TFL package), see also \cite{isabelle-HOL}. The
1.264 + $(permissive)$ option tells TFL to recover from failed proof attempts,
1.265 + returning unfinished results. The $recdef_simp$, $recdef_cong$, and
1.266 + $recdef_wf$ hints refer to auxiliary rules to be used in the internal
1.267 + automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\
1.268 + \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
1.269 + (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
1.270 + \S\ref{sec:classical}).
1.271 +\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
1.272 + termination condition number $i$ (default $1$) as generated by a
1.273 + $\isarkeyword{recdef}$ definition of constant $c$.
1.274 +
1.275 + Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
1.276 + internal proofs without manual intervention.
1.277 +\end{descr}
1.278 +
1.279 +Both kinds of recursive definitions accommodate reasoning by induction (cf.\
1.280 +\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
1.281 +the function definition) refers to a specific induction rule, with parameters
1.282 +named according to the user-specified equations. Case names of
1.283 +$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
1.284 +$\isarkeyword{recdef}$ are numbered (starting from $1$).
1.285 +
1.286 +The equations provided by these packages may be referred later as theorem list
1.287 +$f\mathord.simps$, where $f$ is the (collective) name of the functions
1.288 +defined. Individual equations may be named explicitly as well; note that for
1.289 +$\isarkeyword{recdef}$ each specification given by the user may result in
1.290 +several theorems.
1.291 +
1.292 +\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
1.293 +the following attributes.
1.294 +
1.295 +\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
1.296 +\begin{matharray}{rcl}
1.297 + recdef_simp & : & \isaratt \\
1.298 + recdef_cong & : & \isaratt \\
1.299 + recdef_wf & : & \isaratt \\
1.300 +\end{matharray}
1.301 +
1.302 +\railalias{recdefsimp}{recdef\_simp}
1.303 +\railterm{recdefsimp}
1.304 +
1.305 +\railalias{recdefcong}{recdef\_cong}
1.306 +\railterm{recdefcong}
1.307 +
1.308 +\railalias{recdefwf}{recdef\_wf}
1.309 +\railterm{recdefwf}
1.310 +
1.311 +\begin{rail}
1.312 + (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
1.313 + ;
1.314 +\end{rail}
1.315 +
1.316 +
1.317 +\subsection{(Co)Inductive sets}\label{sec:hol-inductive}
1.318 +
1.319 +\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
1.320 +\begin{matharray}{rcl}
1.321 + \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
1.322 + \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
1.323 + mono & : & \isaratt \\
1.324 +\end{matharray}
1.325 +
1.326 +\railalias{condefs}{con\_defs}
1.327 +\railterm{condefs}
1.328 +
1.329 +\begin{rail}
1.330 + ('inductive' | 'coinductive') sets intros monos?
1.331 + ;
1.332 + 'mono' (() | 'add' | 'del')
1.333 + ;
1.334 +
1.335 + sets: (term comment? +)
1.336 + ;
1.337 + intros: 'intros' (thmdecl? prop comment? +)
1.338 + ;
1.339 + monos: 'monos' thmrefs comment?
1.340 + ;
1.341 +\end{rail}
1.342 +
1.343 +\begin{descr}
1.344 +\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
1.345 + (co)inductive sets from the given introduction rules.
1.346 +\item [$mono$] declares monotonicity rules. These rule are involved in the
1.347 + automated monotonicity proof of $\isarkeyword{inductive}$.
1.348 +\end{descr}
1.349 +
1.350 +See \cite{isabelle-HOL} for further information on inductive definitions in
1.351 +HOL.
1.352 +
1.353 +
1.354 +\subsection{Arithmetic proof support}
1.355 +
1.356 +\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
1.357 +\begin{matharray}{rcl}
1.358 + arith & : & \isarmeth \\
1.359 + arith_split & : & \isaratt \\
1.360 +\end{matharray}
1.361 +
1.362 +\begin{rail}
1.363 + 'arith' '!'?
1.364 + ;
1.365 +\end{rail}
1.366 +
1.367 +The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
1.368 +$real$). Any current facts are inserted into the goal before running the
1.369 +procedure. The ``!''~argument causes the full context of assumptions to be
1.370 +included. The $arith_split$ attribute declares case split rules to be
1.371 +expanded before the arithmetic procedure is invoked.
1.372 +
1.373 +Note that a simpler (but faster) version of arithmetic reasoning is already
1.374 +performed by the Simplifier.
1.375 +
1.376 +
1.377 +\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
1.378 +
1.379 +The following important tactical tools of Isabelle/HOL have been ported to
1.380 +Isar. These should be never used in proper proof texts!
1.381 +
1.382 +\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
1.383 +\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
1.384 +\begin{matharray}{rcl}
1.385 + case_tac^* & : & \isarmeth \\
1.386 + induct_tac^* & : & \isarmeth \\
1.387 + ind_cases^* & : & \isarmeth \\
1.388 + \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
1.389 +\end{matharray}
1.390 +
1.391 +\railalias{casetac}{case\_tac}
1.392 +\railterm{casetac}
1.393 +
1.394 +\railalias{inducttac}{induct\_tac}
1.395 +\railterm{inducttac}
1.396 +
1.397 +\railalias{indcases}{ind\_cases}
1.398 +\railterm{indcases}
1.399 +
1.400 +\railalias{inductivecases}{inductive\_cases}
1.401 +\railterm{inductivecases}
1.402 +
1.403 +\begin{rail}
1.404 + casetac goalspec? term rule?
1.405 + ;
1.406 + inducttac goalspec? (insts * 'and') rule?
1.407 + ;
1.408 + indcases (prop +)
1.409 + ;
1.410 + inductivecases thmdecl? (prop +) comment?
1.411 + ;
1.412 +
1.413 + rule: ('rule' ':' thmref)
1.414 + ;
1.415 +\end{rail}
1.416 +
1.417 +\begin{descr}
1.418 +\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
1.419 + only (unless an alternative rule is given explicitly). Furthermore,
1.420 + $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
1.421 + variables to be given as instantiation. These tactic emulations feature
1.422 + both goal addressing and dynamic instantiation. Note that named rule cases
1.423 + are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
1.424 + methods (see \S\ref{sec:cases-induct}).
1.425 +
1.426 +\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
1.427 + to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted
1.428 + forward manner.
1.429 +
1.430 + While $ind_cases$ is a proof method to apply the result immediately as
1.431 + elimination rules, $\isarkeyword{inductive_cases}$ provides case split
1.432 + theorems at the theory level for later use,
1.433 +\end{descr}
1.434 +
1.435 +
1.436 +\section{HOLCF}
1.437 +
1.438 +\subsection{Mixfix syntax for continuous operations}
1.439 +
1.440 +\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}
1.441 +
1.442 +\begin{matharray}{rcl}
1.443 + \isarcmd{consts} & : & \isartrans{theory}{theory} \\
1.444 + \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
1.445 +\end{matharray}
1.446 +
1.447 +HOLCF provides a separate type for continuous functions $\alpha \rightarrow
1.448 +\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix
1.449 +syntax normally refers directly to the pure meta-level function type $\alpha
1.450 +\To \beta$, with application $f\,x$.
1.451 +
1.452 +The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as
1.453 +the pure versions (cf.\ \S\ref{sec:consts}). Internally, declarations
1.454 +involving continuous function types are treated specifically, transforming the
1.455 +syntax template accordingly and generating syntax translation rules for the
1.456 +abstract and concrete representation of application.
1.457 +
1.458 +The behavior for plain meta-level function types is unchanged. Mixed
1.459 +continuous and meta-level application is \emph{not} supported.
1.460 +
1.461 +\subsection{Recursive domains}
1.462 +
1.463 +\indexisarcmdof{HOLCF}{domain}
1.464 +\begin{matharray}{rcl}
1.465 + \isarcmd{domain} & : & \isartrans{theory}{theory} \\
1.466 +\end{matharray}
1.467 +
1.468 +\begin{rail}
1.469 + 'domain' parname? (dmspec + 'and')
1.470 + ;
1.471 +
1.472 + dmspec: typespec '=' (cons + '|')
1.473 + ;
1.474 + cons: name (type * ) mixfix? comment?
1.475 + ;
1.476 + dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
1.477 +\end{rail}
1.478 +
1.479 +Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
1.480 +\S\ref{sec:hol-datatype}). Mutual recursive is supported, but no nesting nor
1.481 +arbitrary branching. Domain constructors may be strict (default) or lazy, the
1.482 +latter admits to introduce infinitary objects in the typical LCF manner (lazy
1.483 +lists etc.).
1.484 +
1.485 +See also \cite{MuellerNvOS99} for further information HOLCF domains in
1.486 +general.
1.487 +
1.488 +
1.489 +\section{ZF}
1.490 +
1.491 +\subsection{Type checking}
1.492 +
1.493 +FIXME
1.494 +
1.495 +\subsection{Inductive sets and datatypes}
1.496 +
1.497 +FIXME
1.498 +
1.499 +
1.500 +%%% Local Variables:
1.501 +%%% mode: latex
1.502 +%%% TeX-master: "isar-ref"
1.503 +%%% End: