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})}} |