--- a/doc-src/IsarRef/logics.tex Tue May 06 00:13:01 2008 +0200
+++ b/doc-src/IsarRef/logics.tex Tue May 06 23:33:05 2008 +0200
@@ -1,89 +1,6 @@
\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 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.
-
-\railalias{ruleformat}{rule\_format}
-\railterm{ruleformat}
-
-\begin{rail}
- 'judgment' constdecl
- ;
- 'atomize' ('(' 'full' ')')?
- ;
- ruleformat ('(' 'noasm' ')')?
- ;
-\end{rail}
-
-\begin{descr}
-
-\item [$\isarkeyword{judgment}~c::\sigma~~(mx)$] 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 $(mx)$ 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$). Giving the ``$(full)$'' option
- here means to turn the whole subgoal into an object-statement (if possible),
- including the outermost parameters and assumptions as well.
-
- 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:hol-typedef}