summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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