doc-src/IsarImplementation/Thy/logic.thy
changeset 18537 2681f9e34390
child 20437 0eb5e30fd620
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,139 @@
+
+(* $Id$ *)
+
+theory logic imports base begin
+
+chapter {* Pure logic *}
+
+section {* Syntax *}
+
+subsection {* Simply-typed lambda calculus *}
+
+text {*
+
+FIXME
+
+\glossary{Type}{FIXME}
+\glossary{Term}{FIXME}
+
+*}
+
+subsection {* The order-sorted algebra of types *}
+
+text {*
+
+FIXME
+
+\glossary{Type constructor}{FIXME}
+
+\glossary{Type class}{FIXME}
+
+\glossary{Type arity}{FIXME}
+
+\glossary{Sort}{FIXME}
+
+*}
+
+
+subsection {* Type-inference and schematic polymorphism *}
+
+text {*
+
+FIXME
+
+\glossary{Schematic polymorphism}{FIXME}
+
+\glossary{Type variable}{FIXME}
+
+*}
+
+
+section {* Theory *}
+
+text {*
+
+FIXME
+
+\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
+theory context, but slightly more flexible since it may be used at
+different type-instances, due to \seeglossary{schematic
+polymorphism.}}
+
+*}
+
+
+section {* Deduction *}
+
+text {*
+
+  FIXME
+
+\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
+@{text "prop"}.  Internally, there is nothing special about
+propositions apart from their type, but the concrete syntax enforces a
+clear distinction.  Propositions are structured via implication @{text
+"A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
+else is considered atomic.  The canonical form for propositions is
+that of a \seeglossary{Hereditary Harrop Formula}.}
+
+\glossary{Theorem}{A proven proposition within a certain theory and
+proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
+rarely spelled out explicitly.  Theorems are usually normalized
+according to the \seeglossary{HHF} format.}
+
+\glossary{Fact}{Sometimes used interchangably for
+\seeglossary{theorem}.  Strictly speaking, a list of theorems,
+essentially an extra-logical conjunction.  Facts emerge either as
+local assumptions, or as results of local goal statements --- both may
+be simultaneous, hence the list representation.}
+
+\glossary{Schematic variable}{FIXME}
+
+\glossary{Fixed variable}{A variable that is bound within a certain
+proof context; an arbitrary-but-fixed entity within a portion of proof
+text.}
+
+\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
+
+\glossary{Bound variable}{FIXME}
+
+\glossary{Variable}{See \seeglossary{schematic variable},
+\seeglossary{fixed variable}, \seeglossary{bound variable}, or
+\seeglossary{type variable}.  The distinguishing feature of different
+variables is their binding scope.}
+
+*}
+
+subsection {* Primitive inferences *}
+
+text FIXME
+
+subsection {* Higher-order resolution *}
+
+text {*
+
+FIXME
+
+\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
+format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
+A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
+Any proposition may be put into HHF form by normalizing with the rule
+@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
+quantifier prefix is represented via \seeglossary{schematic
+variables}, such that the top-level structure is merely that of a
+\seeglossary{Horn Clause}}.
+
+\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
+
+*}
+
+subsection {* Equational reasoning *}
+
+text FIXME
+
+
+section {* Proof terms *}
+
+text FIXME
+
+end