author wenzelm Fri, 20 Feb 2009 18:48:58 +0100 changeset 29769 03634a9e91ae parent 29768 64a50ff3f308 child 29770 cac2ca7bbc08
improved section on "Hereditary Harrop Formulae";
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Thu Feb 19 21:19:49 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Fri Feb 20 18:48:58 2009 +0100
@@ -735,7 +735,12 @@
and so-called \emph{lifting} of rules into a context of @{text "\<And>"}
and @{text "\<Longrightarrow>"} connectives.  Thus the full power of higher-order
natural deduction in Isabelle/Pure becomes readily available.
+*}

+
+subsection {* Hereditary Harrop Formulae *}
+
+text {*
The idea of object-level rules is to model Natural Deduction
inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow
arbitrary nesting similar to \cite{extensions91}.  The most basic
@@ -751,22 +756,18 @@
$@{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}$
-  Any parameters occurring in rule statement are conceptionally
-  treated as arbitrary:
+  As an example consider conjunction introduction: @{text "A \<Longrightarrow> B \<Longrightarrow> A \<and>
+  B"}.  Any parameters occurring in such rule statements are
+  conceptionally treated as arbitrary:
$- @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"} + @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. A\<^sub>1 x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> \<dots> A\<^sub>n x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> A x\<^sub>1 \<dots> x\<^sub>m"}$
-  This outermost quantifier prefix via is represented in Isabelle via
-  schematic variables @{text "?x\<^sub>1, \<dots>, ?x\<^sub>m"} occurring in
-  the statement body.  Note that this representation lacks information
-  about the order of parameters, and vacuous quantifiers disappear
-  automatically.

-  \medskip Nesting of rules means that the positions of @{text
-  "A\<^sub>i"} may hold recursively rules of the same shape, not just
-  atomic propositions.  This format is called \emph{Hereditary Harrop
-  Form} in the literature \cite{Miller:1991} and may be characterized
-  inductively as follows:
+  Nesting of rules means that the positions of @{text "A\<^sub>i"} may
+  hold compound rules of the same shape, not just atomic propositions.
+  Propositions of this format are called \emph{Hereditary Harrop
+  Formulae} in the literature \cite{Miller:1991}.  Here we give an
+  inductive characterization as follows:

\medskip
\begin{tabular}{ll}
@@ -776,13 +777,40 @@
\end{tabular}
\medskip

-  \noindent Due to @{prop "(PROP A \<Longrightarrow> (\<And>x. PROP B x)) \<equiv> (\<And>x. PROP A \<Longrightarrow>
-  PROP B x)"} any Pure proposition can be seen a rule in HHF format.
-  Some operations in Isabelle already work modulo that equivalence, in
-  other places results are explicitly put into canonical form (e.g.\
-  when exporting results, notably at the end of a proof).  Regular
-  user-level results should always be in canonical HHF format.
+  \noindent Thus we essentially impose nesting levels on Pure
+  propositions.  At each level there is a local parameter prefix,
+  followed by premises, and concluding another atomic proposition.
+  Typical examples are implication introduction @{text "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow>
+  B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n)) \<Longrightarrow>
+  P n"}.  Even deeper nesting occurs in well-founded induction @{text
+  "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this already marks the
+  limit of rule complexity seen in practice.
+
+  \medskip The main inference system of Isabelle/Pure always maintains
+  the following canonical form of framework propositions:
+
+  \begin{itemize}

+  \item Results are normalized by means of the equivalence @{prop
+  "(PROP A \<Longrightarrow> (\<And>x. PROP B x)) \<equiv> (\<And>x. PROP A \<Longrightarrow> PROP B x)"}, which is a
+  theorem of Pure.  By pushing quantifiers inside conclusions in front
+  of the implication, we arrive at a normal form that is always a
+  Hereditary Harrop Formula.
+
+  \item The outermost prefix of parameters is represented via
+  schematic variables, i.e.\ instead of @{text "\<And>\<^vec>x. \<^vec>H
+  \<^vec>x \<Longrightarrow> A \<^vec>x"} we always work with @{text "\<^vec>H
+  ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.  Note that this representation looses
+  information about the order of parameters, and vacuous quantifiers
+  vanish automatically.
+
+  \end{itemize}
+*}
+
+
+subsection {* Rule composition *}
+
+text {*
There are two main principles of rule composition: @{inference
resolution} (i.e.\ backchaining of rules) and @{inference
assumption} (i.e.\ closing a branch); both principles are combined