1.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Tue May 06 00:13:01 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Tue May 06 23:33:05 2008 +0200
     1.3 @@ -2038,6 +2038,86 @@
     1.4  \end{isamarkuptext}%
     1.5  \isamarkuptrue%
     1.6  %
     1.7 +\isamarkupsection{General logic setup \label{sec:object-logic}%
     1.8 +}
     1.9 +\isamarkuptrue%
    1.10 +%
    1.11 +\begin{isamarkuptext}%
    1.12 +\begin{matharray}{rcl}
    1.13 +    \indexdef{}{command}{judgment}\mbox{\isa{\isacommand{judgment}}} & : & \isartrans{theory}{theory} \\
    1.14 +    \indexdef{}{method}{atomize}\mbox{\isa{atomize}} & : & \isarmeth \\
    1.15 +    \indexdef{}{attribute}{atomize}\mbox{\isa{atomize}} & : & \isaratt \\
    1.16 +    \indexdef{}{attribute}{rule-format}\mbox{\isa{rule{\isacharunderscore}format}} & : & \isaratt \\
    1.17 +    \indexdef{}{attribute}{rulify}\mbox{\isa{rulify}} & : & \isaratt \\
    1.18 +  \end{matharray}
    1.19 +
    1.20 +  The very starting point for any Isabelle object-logic is a ``truth
    1.21 +  judgment'' that links object-level statements to the meta-logic
    1.22 +  (with its minimal language of \isa{prop} that covers universal
    1.23 +  quantification \isa{{\isasymAnd}} and implication \isa{{\isasymLongrightarrow}}).
    1.24 +
    1.25 +  Common object-logics are sufficiently expressive to internalize rule
    1.26 +  statements over \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} within their own
    1.27 +  language.  This is useful in certain situations where a rule needs
    1.28 +  to be viewed as an atomic statement from the meta-level perspective,
    1.29 +  e.g.\ \isa{{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ P\ x} versus \isa{{\isasymforall}x\ {\isasymin}\ A{\isachardot}\ P\ x}.
    1.30 +
    1.31 +  From the following language elements, only the \mbox{\isa{atomize}}
    1.32 +  method and \mbox{\isa{rule{\isacharunderscore}format}} attribute are occasionally
    1.33 +  required by end-users, the rest is for those who need to setup their
    1.34 +  own object-logic.  In the latter case existing formulations of
    1.35 +  Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
    1.36 +
    1.37 +  Generic tools may refer to the information provided by object-logic
    1.38 +  declarations internally.
    1.39 +
    1.40 +  \begin{rail}
    1.41 +    'judgment' constdecl
    1.42 +    ;
    1.43 +    'atomize' ('(' 'full' ')')?
    1.44 +    ;
    1.45 +    'rule\_format' ('(' 'noasm' ')')?
    1.46 +    ;
    1.47 +  \end{rail}
    1.48 +
    1.49 +  \begin{descr}
    1.50 +  
    1.51 +  \item [\mbox{\isa{\isacommand{judgment}}}~\isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isacharparenleft}mx{\isacharparenright}}] declares
    1.52 +  constant \isa{c} as the truth judgment of the current
    1.53 +  object-logic.  Its type \isa{{\isasymsigma}} should specify a coercion of the
    1.54 +  category of object-level propositions to \isa{prop} of the Pure
    1.55 +  meta-logic; the mixfix annotation \isa{{\isacharparenleft}mx{\isacharparenright}} would typically
    1.56 +  just link the object language (internally of syntactic category
    1.57 +  \isa{logic}) with that of \isa{prop}.  Only one \mbox{\isa{\isacommand{judgment}}} declaration may be given in any theory development.
    1.58 +  
    1.59 +  \item [\mbox{\isa{atomize}} (as a method)] rewrites any non-atomic
    1.60 +  premises of a sub-goal, using the meta-level equations declared via
    1.61 +  \mbox{\isa{atomize}} (as an attribute) beforehand.  As a result,
    1.62 +  heavily nested goals become amenable to fundamental operations such
    1.63 +  as resolution (cf.\ the \mbox{\isa{rule}} method).  Giving the ``\isa{{\isacharparenleft}full{\isacharparenright}}'' option here means to turn the whole subgoal into an
    1.64 +  object-statement (if possible), including the outermost parameters
    1.65 +  and assumptions as well.
    1.66 +
    1.67 +  A typical collection of \mbox{\isa{atomize}} rules for a particular
    1.68 +  object-logic would provide an internalization for each of the
    1.69 +  connectives of \isa{{\isasymAnd}}, \isa{{\isasymLongrightarrow}}, and \isa{{\isasymequiv}}.
    1.70 +  Meta-level conjunction should be covered as well (this is
    1.71 +  particularly important for locales, see \secref{sec:locale}).
    1.72 +
    1.73 +  \item [\mbox{\isa{rule{\isacharunderscore}format}}] rewrites a theorem by the
    1.74 +  equalities declared as \mbox{\isa{rulify}} rules in the current
    1.75 +  object-logic.  By default, the result is fully normalized, including
    1.76 +  assumptions and conclusions at any depth.  The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}
    1.77 +  option restricts the transformation to the conclusion of a rule.
    1.78 +
    1.79 +  In common object-logics (HOL, FOL, ZF), the effect of \mbox{\isa{rule{\isacharunderscore}format}} is to replace (bounded) universal quantification
    1.80 +  (\isa{{\isasymforall}}) and implication (\isa{{\isasymlongrightarrow}}) by the corresponding
    1.81 +  rule statements over \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}}.
    1.82 +
    1.83 +  \end{descr}%
    1.84 +\end{isamarkuptext}%
    1.85 +\isamarkuptrue%
    1.86 +%
    1.87  \isadelimtheory
    1.88  %
    1.89  \endisadelimtheory