--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/logics.tex Thu Jan 03 17:48:02 2002 +0100
@@ -0,0 +1,500 @@
+
+\chapter{Object-logic specific elements}\label{ch:logics}
+
+\section{General logic setup}\label{sec:object-logic}
+
+\indexisarcmd{judgment}
+\indexisarmeth{atomize}\indexisaratt{atomize}
+\indexisaratt{rule-format}\indexisaratt{rulify}
+
+\begin{matharray}{rcl}
+ \isarcmd{judgment} & : & \isartrans{theory}{theory} \\
+ atomize & : & \isarmeth \\
+ atomize & : & \isaratt \\
+ rule_format & : & \isaratt \\
+ rulify & : & \isaratt \\
+\end{matharray}
+
+The very starting point for any Isabelle object-logic is a ``truth judgment''
+that links object-level statements to the meta-logic (with its minimal
+language of $prop$ that covers universal quantification $\Forall$ and
+implication $\Imp$). Common object-logics are sufficiently expressive to
+\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
+language. This is useful in certain situations where a rule needs to be
+viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
+\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
+
+From the following language elements, only the $atomize$ method and
+$rule_format$ attribute are occasionally required by end-users, the rest is
+for those who need to setup their own object-logic. In the latter case
+existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as
+realistic examples.
+
+Generic tools may refer to the information provided by object-logic
+declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
+Reasoner \S\ref{sec:classical}).
+
+\railalias{ruleformat}{rule\_format}
+\railterm{ruleformat}
+
+\begin{rail}
+ 'judgment' constdecl
+ ;
+ ruleformat ('(' noasm ')')?
+ ;
+\end{rail}
+
+\begin{descr}
+
+\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
+ truth judgment of the current object-logic. Its type $\sigma$ should
+ specify a coercion of the category of object-level propositions to $prop$ of
+ the Pure meta-logic; the mixfix annotation $syn$ would typically just link
+ the object language (internally of syntactic category $logic$) with that of
+ $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any
+ theory development.
+
+\item [$atomize$] (as a method) rewrites any non-atomic premises of a
+ sub-goal, using the meta-level equations declared via $atomize$ (as an
+ attribute) beforehand. As a result, heavily nested goals become amenable to
+ fundamental operations such as resolution (cf.\ the $rule$ method) and
+ proof-by-assumption (cf.\ $assumption$).
+
+ A typical collection of $atomize$ rules for a particular object-logic would
+ provide an internalization for each of the connectives of $\Forall$, $\Imp$,
+ and $\equiv$. Meta-level conjunction expressed in the manner of minimal
+ higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$
+ should be covered as well (this is particularly important for locales, see
+ \S\ref{sec:locale}).
+
+\item [$rule_format$] rewrites a theorem by the equalities declared as
+ $rulify$ rules in the current object-logic. By default, the result is fully
+ normalized, including assumptions and conclusions at any depth. The
+ $no_asm$ option restricts the transformation to the conclusion of a rule.
+
+ In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to
+ replace (bounded) universal quantification ($\forall$) and implication
+ ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$.
+
+\end{descr}
+
+
+\section{HOL}
+
+\subsection{Primitive types}\label{sec:typedef}
+
+\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
+\begin{matharray}{rcl}
+ \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
+ \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
+\end{matharray}
+
+\begin{rail}
+ 'typedecl' typespec infix? comment?
+ ;
+ 'typedef' parname? typespec infix? \\ '=' term comment?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
+ $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
+ also declares type arity $t :: (term, \dots, term) term$, making $t$ an
+ actual HOL type constructor.
+\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
+ non-emptiness of the set $A$. After finishing the proof, the theory will be
+ augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL}
+ for more information. Note that user-level theories usually do not directly
+ refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced
+ packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and
+ $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
+\end{descr}
+
+
+\subsection{Low-level tuples}
+
+\indexisarattof{HOL}{split-format}
+\begin{matharray}{rcl}
+ split_format^* & : & \isaratt \\
+\end{matharray}
+
+\railalias{splitformat}{split\_format}
+\railterm{splitformat}
+\railterm{complete}
+
+\begin{rail}
+ splitformat (((name * ) + 'and') | ('(' complete ')'))
+ ;
+\end{rail}
+
+\begin{descr}
+
+\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
+ tuple types into canonical form as specified by the arguments given; $\vec
+ p@i$ refers to occurrences in premise $i$ of the rule. The
+ $split_format~(complete)$ form causes \emph{all} arguments in function
+ applications to be represented canonically according to their tuple type
+ structure.
+
+ Note that these operations tend to invent funny names for new local
+ parameters to be introduced.
+
+\end{descr}
+
+
+\subsection{Records}\label{sec:hol-record}
+
+FIXME proof tools (simp, cases/induct; no split!?);
+
+FIXME mixfix syntax;
+
+\indexisarcmdof{HOL}{record}
+\begin{matharray}{rcl}
+ \isarcmd{record} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+ 'record' typespec '=' (type '+')? (constdecl +)
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
+ defines extensible record type $(\vec\alpha)t$, derived from the optional
+ parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
+ See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on
+ simply-typed extensible records.
+\end{descr}
+
+
+\subsection{Datatypes}\label{sec:hol-datatype}
+
+\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype}
+\begin{matharray}{rcl}
+ \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
+ \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{repdatatype}{rep\_datatype}
+\railterm{repdatatype}
+
+\begin{rail}
+ '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
+ ones, generating the standard infrastructure of derived concepts (primitive
+ recursion etc.).
+\end{descr}
+
+The induction and exhaustion theorems generated provide case names according
+to the constructors involved, while parameters are named after the types (see
+also \S\ref{sec:cases-induct}).
+
+See \cite{isabelle-HOL} for more details on datatypes. Note that the theory
+syntax above has been slightly simplified over the old version, usually
+requiring more quotes and less parentheses. Apart from proper proof methods
+for case-analysis and induction, there are also emulations of ML tactics
+\texttt{case_tac} and \texttt{induct_tac} available, see
+\S\ref{sec:induct_tac}.
+
+
+\subsection{Recursive functions}\label{sec:recursion}
+
+\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
+\begin{matharray}{rcl}
+ \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
+ \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
+ \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
+%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}
+
+\railalias{recdeftc}{recdef\_tc}
+\railterm{recdeftc}
+
+\begin{rail}
+ 'primrec' parname? (equation + )
+ ;
+ 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
+ ;
+ recdeftc thmdecl? tc comment?
+ ;
+
+ equation: thmdecl? eqn
+ ;
+ eqn: prop comment?
+ ;
+ hints: '(' 'hints' (recdefmod * ) ')'
+ ;
+ recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
+ ;
+ tc: nameref ('(' nat ')')?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
+ datatypes, see also \cite{isabelle-HOL}.
+\item [$\isarkeyword{recdef}$] defines general well-founded recursive
+ functions (using the TFL package), see also \cite{isabelle-HOL}. The
+ $(permissive)$ option tells TFL to recover from failed proof attempts,
+ returning unfinished results. The $recdef_simp$, $recdef_cong$, and
+ $recdef_wf$ hints refer to auxiliary rules to be used in the internal
+ automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\
+ \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
+ (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
+ \S\ref{sec:classical}).
+\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
+ termination condition number $i$ (default $1$) as generated by a
+ $\isarkeyword{recdef}$ definition of constant $c$.
+
+ Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
+ internal proofs without manual intervention.
+\end{descr}
+
+Both kinds of recursive definitions accommodate reasoning by induction (cf.\
+\S\ref{sec:cases-induct}): 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$).
+
+The equations provided by these packages may be referred later as theorem list
+$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.
+
+\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
+the following attributes.
+
+\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf}
+\begin{matharray}{rcl}
+ recdef_simp & : & \isaratt \\
+ recdef_cong & : & \isaratt \\
+ recdef_wf & : & \isaratt \\
+\end{matharray}
+
+\railalias{recdefsimp}{recdef\_simp}
+\railterm{recdefsimp}
+
+\railalias{recdefcong}{recdef\_cong}
+\railterm{recdefcong}
+
+\railalias{recdefwf}{recdef\_wf}
+\railterm{recdefwf}
+
+\begin{rail}
+ (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del')
+ ;
+\end{rail}
+
+
+\subsection{(Co)Inductive sets}\label{sec:hol-inductive}
+
+\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}
+\begin{matharray}{rcl}
+ \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
+ \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
+ mono & : & \isaratt \\
+\end{matharray}
+
+\railalias{condefs}{con\_defs}
+\railterm{condefs}
+
+\begin{rail}
+ ('inductive' | 'coinductive') sets intros monos?
+ ;
+ 'mono' (() | 'add' | 'del')
+ ;
+
+ sets: (term comment? +)
+ ;
+ intros: 'intros' (thmdecl? prop comment? +)
+ ;
+ monos: 'monos' thmrefs comment?
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
+ (co)inductive sets from the given introduction rules.
+\item [$mono$] declares monotonicity rules. These rule are involved in the
+ automated monotonicity proof of $\isarkeyword{inductive}$.
+\end{descr}
+
+See \cite{isabelle-HOL} for further information on inductive definitions in
+HOL.
+
+
+\subsection{Arithmetic proof support}
+
+\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split}
+\begin{matharray}{rcl}
+ arith & : & \isarmeth \\
+ arith_split & : & \isaratt \\
+\end{matharray}
+
+\begin{rail}
+ 'arith' '!'?
+ ;
+\end{rail}
+
+The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
+$real$). Any current facts are inserted into the goal before running the
+procedure. The ``!''~argument causes the full context of assumptions to be
+included. The $arith_split$ attribute declares case split rules to be
+expanded before the arithmetic procedure is invoked.
+
+Note that a simpler (but faster) version of arithmetic reasoning is already
+performed by the Simplifier.
+
+
+\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
+
+The following important tactical tools of Isabelle/HOL have been ported to
+Isar. These should be never used in proper proof texts!
+
+\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac}
+\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases}
+\begin{matharray}{rcl}
+ case_tac^* & : & \isarmeth \\
+ induct_tac^* & : & \isarmeth \\
+ ind_cases^* & : & \isarmeth \\
+ \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{casetac}{case\_tac}
+\railterm{casetac}
+
+\railalias{inducttac}{induct\_tac}
+\railterm{inducttac}
+
+\railalias{indcases}{ind\_cases}
+\railterm{indcases}
+
+\railalias{inductivecases}{inductive\_cases}
+\railterm{inductivecases}
+
+\begin{rail}
+ casetac goalspec? term rule?
+ ;
+ inducttac goalspec? (insts * 'and') rule?
+ ;
+ indcases (prop +)
+ ;
+ inductivecases thmdecl? (prop +) comment?
+ ;
+
+ rule: ('rule' ':' thmref)
+ ;
+\end{rail}
+
+\begin{descr}
+\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes
+ only (unless an alternative rule is given explicitly). Furthermore,
+ $case_tac$ does a classical case split on booleans; $induct_tac$ allows only
+ variables to be given as instantiation. These tactic emulations feature
+ both goal addressing and dynamic instantiation. Note that named rule cases
+ are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
+ methods (see \S\ref{sec:cases-induct}).
+
+\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
+ to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted
+ forward manner.
+
+ While $ind_cases$ is a proof method to apply the result immediately as
+ elimination rules, $\isarkeyword{inductive_cases}$ provides case split
+ theorems at the theory level for later use,
+\end{descr}
+
+
+\section{HOLCF}
+
+\subsection{Mixfix syntax for continuous operations}
+
+\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs}
+
+\begin{matharray}{rcl}
+ \isarcmd{consts} & : & \isartrans{theory}{theory} \\
+ \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+HOLCF provides a separate type for continuous functions $\alpha \rightarrow
+\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix
+syntax normally refers directly to the pure meta-level function type $\alpha
+\To \beta$, with application $f\,x$.
+
+The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as
+the pure versions (cf.\ \S\ref{sec:consts}). Internally, declarations
+involving continuous function types are treated specifically, transforming the
+syntax template accordingly and generating syntax translation rules for the
+abstract and concrete representation of application.
+
+The behavior for plain meta-level function types is unchanged. Mixed
+continuous and meta-level application is \emph{not} supported.
+
+\subsection{Recursive domains}
+
+\indexisarcmdof{HOLCF}{domain}
+\begin{matharray}{rcl}
+ \isarcmd{domain} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+ 'domain' parname? (dmspec + 'and')
+ ;
+
+ dmspec: typespec '=' (cons + '|')
+ ;
+ cons: name (type * ) mixfix? comment?
+ ;
+ dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
+\end{rail}
+
+Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
+\S\ref{sec:hol-datatype}). Mutual recursive is supported, but no nesting nor
+arbitrary branching. Domain constructors may be strict (default) or lazy, the
+latter admits to introduce infinitary objects in the typical LCF manner (lazy
+lists etc.).
+
+See also \cite{MuellerNvOS99} for further information HOLCF domains in
+general.
+
+
+\section{ZF}
+
+\subsection{Type checking}
+
+FIXME
+
+\subsection{Inductive sets and datatypes}
+
+FIXME
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "isar-ref"
+%%% End: