--- a/doc-src/IsarRef/Thy/Generic.thy Tue May 06 00:13:01 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Tue May 06 23:33:05 2008 +0200
@@ -2057,4 +2057,85 @@
\end{descr}
*}
+
+section {* General logic setup \label{sec:object-logic} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "judgment"} & : & \isartrans{theory}{theory} \\
+ @{method_def atomize} & : & \isarmeth \\
+ @{attribute_def atomize} & : & \isaratt \\
+ @{attribute_def rule_format} & : & \isaratt \\
+ @{attribute_def 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 @{text prop} that covers universal
+ quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}).
+
+ Common object-logics are sufficiently expressive to internalize rule
+ statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} 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.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}.
+
+ From the following language elements, only the @{method atomize}
+ method and @{attribute 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.
+
+ \begin{rail}
+ 'judgment' constdecl
+ ;
+ 'atomize' ('(' 'full' ')')?
+ ;
+ 'rule\_format' ('(' 'noasm' ')')?
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "judgment"}~@{text "c :: \<sigma> (mx)"}] declares
+ constant @{text c} as the truth judgment of the current
+ object-logic. Its type @{text \<sigma>} should specify a coercion of the
+ category of object-level propositions to @{text prop} of the Pure
+ meta-logic; the mixfix annotation @{text "(mx)"} would typically
+ just link the object language (internally of syntactic category
+ @{text logic}) with that of @{text prop}. Only one @{command
+ "judgment"} declaration may be given in any theory development.
+
+ \item [@{method atomize} (as a method)] rewrites any non-atomic
+ premises of a sub-goal, using the meta-level equations declared via
+ @{attribute atomize} (as an attribute) beforehand. As a result,
+ heavily nested goals become amenable to fundamental operations such
+ as resolution (cf.\ the @{method rule} method). Giving the ``@{text
+ "(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 @{attribute atomize} rules for a particular
+ object-logic would provide an internalization for each of the
+ connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}.
+ Meta-level conjunction should be covered as well (this is
+ particularly important for locales, see \secref{sec:locale}).
+
+ \item [@{attribute rule_format}] rewrites a theorem by the
+ equalities declared as @{attribute rulify} rules in the current
+ object-logic. By default, the result is fully normalized, including
+ assumptions and conclusions at any depth. The @{text "(no_asm)"}
+ option restricts the transformation to the conclusion of a rule.
+
+ In common object-logics (HOL, FOL, ZF), the effect of @{attribute
+ rule_format} is to replace (bounded) universal quantification
+ (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding
+ rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
+
+ \end{descr}
+*}
+
end
--- a/doc-src/IsarRef/Thy/document/Generic.tex Tue May 06 00:13:01 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Tue May 06 23:33:05 2008 +0200
@@ -2038,6 +2038,86 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{General logic setup \label{sec:object-logic}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{command}{judgment}\mbox{\isa{\isacommand{judgment}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{method}{atomize}\mbox{\isa{atomize}} & : & \isarmeth \\
+ \indexdef{}{attribute}{atomize}\mbox{\isa{atomize}} & : & \isaratt \\
+ \indexdef{}{attribute}{rule-format}\mbox{\isa{rule{\isacharunderscore}format}} & : & \isaratt \\
+ \indexdef{}{attribute}{rulify}\mbox{\isa{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 \isa{prop} that covers universal
+ quantification \isa{{\isasymAnd}} and implication \isa{{\isasymLongrightarrow}}).
+
+ Common object-logics are sufficiently expressive to internalize rule
+ statements over \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} 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.\ \isa{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ P\ x} versus \isa{{\isasymforall}x\ {\isasymin}\ A{\isachardot}\ P\ x}.
+
+ From the following language elements, only the \mbox{\isa{atomize}}
+ method and \mbox{\isa{rule{\isacharunderscore}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.
+
+ \begin{rail}
+ 'judgment' constdecl
+ ;
+ 'atomize' ('(' 'full' ')')?
+ ;
+ 'rule\_format' ('(' 'noasm' ')')?
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\mbox{\isa{\isacommand{judgment}}}~\isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isacharparenleft}mx{\isacharparenright}}] declares
+ constant \isa{c} as the truth judgment of the current
+ object-logic. Its type \isa{{\isasymsigma}} should specify a coercion of the
+ category of object-level propositions to \isa{prop} of the Pure
+ meta-logic; the mixfix annotation \isa{{\isacharparenleft}mx{\isacharparenright}} would typically
+ just link the object language (internally of syntactic category
+ \isa{logic}) with that of \isa{prop}. Only one \mbox{\isa{\isacommand{judgment}}} declaration may be given in any theory development.
+
+ \item [\mbox{\isa{atomize}} (as a method)] rewrites any non-atomic
+ premises of a sub-goal, using the meta-level equations declared via
+ \mbox{\isa{atomize}} (as an attribute) beforehand. As a result,
+ heavily nested goals become amenable to fundamental operations such
+ as resolution (cf.\ the \mbox{\isa{rule}} method). Giving the ``\isa{{\isacharparenleft}full{\isacharparenright}}'' 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 \mbox{\isa{atomize}} rules for a particular
+ object-logic would provide an internalization for each of the
+ connectives of \isa{{\isasymAnd}}, \isa{{\isasymLongrightarrow}}, and \isa{{\isasymequiv}}.
+ Meta-level conjunction should be covered as well (this is
+ particularly important for locales, see \secref{sec:locale}).
+
+ \item [\mbox{\isa{rule{\isacharunderscore}format}}] rewrites a theorem by the
+ equalities declared as \mbox{\isa{rulify}} rules in the current
+ object-logic. By default, the result is fully normalized, including
+ assumptions and conclusions at any depth. The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}
+ option restricts the transformation to the conclusion of a rule.
+
+ In common object-logics (HOL, FOL, ZF), the effect of \mbox{\isa{rule{\isacharunderscore}format}} is to replace (bounded) universal quantification
+ (\isa{{\isasymforall}}) and implication (\isa{{\isasymlongrightarrow}}) by the corresponding
+ rule statements over \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}}.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- 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}