doc-src/IsarImplementation/Thy/Logic.thy
changeset 29758 7a3b5bbed313
parent 29755 d66b34e46bdf
child 29761 2b658e50683a
equal deleted inserted replaced
29757:ce2b8e6502f9 29758:7a3b5bbed313
   184 
   184 
   185   \end{description}
   185   \end{description}
   186 *}
   186 *}
   187 
   187 
   188 
   188 
   189 
       
   190 section {* Terms \label{sec:terms} *}
   189 section {* Terms \label{sec:terms} *}
   191 
   190 
   192 text {*
   191 text {*
   193   \glossary{Term}{FIXME}
       
   194 
       
   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 {*
   395   \glossary{Proposition}{FIXME A \seeglossary{term} of
       
   396   \seeglossary{type} @{text "prop"}.  Internally, there is nothing
       
   397   special about propositions apart from their type, but the concrete
       
   398   syntax enforces a clear distinction.  Propositions are structured
       
   399   via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
       
   400   "\<And>x. B x"} --- anything else is considered atomic.  The canonical
       
   401   form for propositions is that of a \seeglossary{Hereditary Harrop
       
   402   Formula}. FIXME}
       
   403 
       
   404   \glossary{Theorem}{A proven proposition within a certain theory and
       
   405   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
       
   406   rarely spelled out explicitly.  Theorems are usually normalized
       
   407   according to the \seeglossary{HHF} format. FIXME}
       
   408 
       
   409   \glossary{Fact}{Sometimes used interchangeably for
       
   410   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
       
   411   essentially an extra-logical conjunction.  Facts emerge either as
       
   412   local assumptions, or as results of local goal statements --- both
       
   413   may be simultaneous, hence the list representation. FIXME}
       
   414 
       
   415   \glossary{Schematic variable}{FIXME}
       
   416 
       
   417   \glossary{Fixed variable}{A variable that is bound within a certain
       
   418   proof context; an arbitrary-but-fixed entity within a portion of
       
   419   proof text. FIXME}
       
   420 
       
   421   \glossary{Free variable}{Synonymous for \seeglossary{fixed
       
   422   variable}. FIXME}
       
   423 
       
   424   \glossary{Bound variable}{FIXME}
       
   425 
       
   426   \glossary{Variable}{See \seeglossary{schematic variable},
       
   427   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
       
   428   \seeglossary{type variable}.  The distinguishing feature of
       
   429   different variables is their binding scope. FIXME}
       
   430 
       
   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})}}