# HG changeset patch
# User wenzelm
# Date 1235152138 -3600
# Node ID 03634a9e91ae5740bb5b7c50b44af1e380c78c48
# Parent  64a50ff3f3087c6abdd7faf3395bffe90fdaf7c4
improved section on "Hereditary Harrop Formulae";

diff -r 64a50ff3f308 -r 03634a9e91ae doc-src/IsarImplementation/Thy/Logic.thy
--- 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