doc-src/IsarImplementation/Thy/Logic.thy
 changeset 29758 7a3b5bbed313 parent 29755 d66b34e46bdf child 29761 2b658e50683a
equal inserted replaced
29757:ce2b8e6502f9 29758:7a3b5bbed313
   184
   184
   185   \end{description}
   185   \end{description}
   186 *}
   186 *}
   187
   187
   188
   188
   190 section {* Terms \label{sec:terms} *}
   189 section {* Terms \label{sec:terms} *}
   191
   190
   192 text {*
   191 text {*
   195   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
   192   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
   196   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
   193   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
   197   or \cite{paulson-ml2}), with the types being determined determined
   194   or \cite{paulson-ml2}), with the types being determined determined
   198   by the corresponding binders.  In contrast, free variables and
   195   by the corresponding binders.  In contrast, free variables and
   199   constants are have an explicit name and type in each occurrence.
   196   constants are have an explicit name and type in each occurrence.
   390
   387
   391
   388
   392 section {* Theorems \label{sec:thms} *}
   389 section {* Theorems \label{sec:thms} *}
   393
   390
   394 text {*
   391 text {*
   431   A \emph{proposition} is a well-typed term of type @{text "prop"}, a
   392   A \emph{proposition} is a well-typed term of type @{text "prop"}, a
   432   \emph{theorem} is a proven proposition (depending on a context of
   393   \emph{theorem} is a proven proposition (depending on a context of
   433   hypotheses and the background theory).  Primitive inferences include
   394   hypotheses and the background theory).  Primitive inferences include
   434   plain natural deduction rules for the primary connectives @{text
   395   plain natural deduction rules for the primary connectives @{text
   435   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
   396   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
   436   notion of equality/equivalence @{text "\<equiv>"}.
   397   notion of equality/equivalence @{text "\<equiv>"}.
   437 *}
   398 *}

   399
   438
   400
   439 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
   401 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
   440
   402
   441 text {*
   403 text {*
   442   The theory @{text "Pure"} contains constant declarations for the
   404   The theory @{text "Pure"} contains constant declarations for the
   799
   761
   800   Only few operations really work \emph{modulo} HHF conversion, but
   762   Only few operations really work \emph{modulo} HHF conversion, but
   801   expect a normal form: quantifiers @{text "\<And>"} before implications
   763   expect a normal form: quantifiers @{text "\<And>"} before implications
   802   @{text "\<Longrightarrow>"} at each level of nesting.
   764   @{text "\<Longrightarrow>"} at each level of nesting.
   803
   765
   804 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   766   The set of propositions in HHF format is defined inductively as
   805 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   767   @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> A)"}, for variables @{text "x"}
   806 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   768   and atomic propositions @{text "A"}.  Any proposition may be put
   807 Any proposition may be put into HHF form by normalizing with the rule
   769   into HHF form by normalizing with the rule @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv>
   808 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
   770   (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost quantifier prefix is
   809 quantifier prefix is represented via \seeglossary{schematic
   771   represented via schematic variables, such that the top-level
   810 variables}, such that the top-level structure is merely that of a
   772   structure is merely that of a Horn Clause.
   811 \seeglossary{Horn Clause}}.

   812

   813 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}

   814
   773
   815
   774
   816   \[
   775   \[
   817   \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}
   776   \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}
   818   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}
   777   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}