# HG changeset patch # User wenzelm # Date 1210109585 -7200 # Node ID e8cc166ba1235fe31cd4378871e5a6dc33761ae5 # Parent fc6d5fa0ca3ca5fa1bc00d8bfdc296cd4be20229 converted "General logic setup"; diff -r fc6d5fa0ca3c -r e8cc166ba123 doc-src/IsarRef/Thy/Generic.thy --- 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 implication @{text "\"}). + + Common object-logics are sufficiently expressive to internalize rule + statements over @{text "\"} and @{text "\"} 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 "\x. x \ A \ P x"} versus @{text "\x \ 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 :: \ (mx)"}] declares + constant @{text c} as the truth judgment of the current + object-logic. Its type @{text \} 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 "\"}, @{text "\"}, and @{text "\"}. + 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 "\"}) and implication (@{text "\"}) by the corresponding + rule statements over @{text "\"} and @{text "\"}. + + \end{descr} +*} + end diff -r fc6d5fa0ca3c -r e8cc166ba123 doc-src/IsarRef/Thy/document/Generic.tex --- 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 diff -r fc6d5fa0ca3c -r e8cc166ba123 doc-src/IsarRef/logics.tex --- 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}