doc-src/IsarImplementation/Thy/logic.thy
changeset 18537 2681f9e34390
child 20437 0eb5e30fd620
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Mon Jan 02 20:16:52 2006 +0100
     1.3 @@ -0,0 +1,139 @@
     1.4 +
     1.5 +(* $Id$ *)
     1.6 +
     1.7 +theory logic imports base begin
     1.8 +
     1.9 +chapter {* Pure logic *}
    1.10 +
    1.11 +section {* Syntax *}
    1.12 +
    1.13 +subsection {* Simply-typed lambda calculus *}
    1.14 +
    1.15 +text {*
    1.16 +
    1.17 +FIXME
    1.18 +
    1.19 +\glossary{Type}{FIXME}
    1.20 +\glossary{Term}{FIXME}
    1.21 +
    1.22 +*}
    1.23 +
    1.24 +subsection {* The order-sorted algebra of types *}
    1.25 +
    1.26 +text {*
    1.27 +
    1.28 +FIXME
    1.29 +
    1.30 +\glossary{Type constructor}{FIXME}
    1.31 +
    1.32 +\glossary{Type class}{FIXME}
    1.33 +
    1.34 +\glossary{Type arity}{FIXME}
    1.35 +
    1.36 +\glossary{Sort}{FIXME}
    1.37 +
    1.38 +*}
    1.39 +
    1.40 +
    1.41 +subsection {* Type-inference and schematic polymorphism *}
    1.42 +
    1.43 +text {*
    1.44 +
    1.45 +FIXME
    1.46 +
    1.47 +\glossary{Schematic polymorphism}{FIXME}
    1.48 +
    1.49 +\glossary{Type variable}{FIXME}
    1.50 +
    1.51 +*}
    1.52 +
    1.53 +
    1.54 +section {* Theory *}
    1.55 +
    1.56 +text {*
    1.57 +
    1.58 +FIXME
    1.59 +
    1.60 +\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
    1.61 +theory context, but slightly more flexible since it may be used at
    1.62 +different type-instances, due to \seeglossary{schematic
    1.63 +polymorphism.}}
    1.64 +
    1.65 +*}
    1.66 +
    1.67 +
    1.68 +section {* Deduction *}
    1.69 +
    1.70 +text {*
    1.71 +
    1.72 +  FIXME
    1.73 +
    1.74 +\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
    1.75 +@{text "prop"}.  Internally, there is nothing special about
    1.76 +propositions apart from their type, but the concrete syntax enforces a
    1.77 +clear distinction.  Propositions are structured via implication @{text
    1.78 +"A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
    1.79 +else is considered atomic.  The canonical form for propositions is
    1.80 +that of a \seeglossary{Hereditary Harrop Formula}.}
    1.81 +
    1.82 +\glossary{Theorem}{A proven proposition within a certain theory and
    1.83 +proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
    1.84 +rarely spelled out explicitly.  Theorems are usually normalized
    1.85 +according to the \seeglossary{HHF} format.}
    1.86 +
    1.87 +\glossary{Fact}{Sometimes used interchangably for
    1.88 +\seeglossary{theorem}.  Strictly speaking, a list of theorems,
    1.89 +essentially an extra-logical conjunction.  Facts emerge either as
    1.90 +local assumptions, or as results of local goal statements --- both may
    1.91 +be simultaneous, hence the list representation.}
    1.92 +
    1.93 +\glossary{Schematic variable}{FIXME}
    1.94 +
    1.95 +\glossary{Fixed variable}{A variable that is bound within a certain
    1.96 +proof context; an arbitrary-but-fixed entity within a portion of proof
    1.97 +text.}
    1.98 +
    1.99 +\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
   1.100 +
   1.101 +\glossary{Bound variable}{FIXME}
   1.102 +
   1.103 +\glossary{Variable}{See \seeglossary{schematic variable},
   1.104 +\seeglossary{fixed variable}, \seeglossary{bound variable}, or
   1.105 +\seeglossary{type variable}.  The distinguishing feature of different
   1.106 +variables is their binding scope.}
   1.107 +
   1.108 +*}
   1.109 +
   1.110 +subsection {* Primitive inferences *}
   1.111 +
   1.112 +text FIXME
   1.113 +
   1.114 +subsection {* Higher-order resolution *}
   1.115 +
   1.116 +text {*
   1.117 +
   1.118 +FIXME
   1.119 +
   1.120 +\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   1.121 +format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   1.122 +A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   1.123 +Any proposition may be put into HHF form by normalizing with the rule
   1.124 +@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
   1.125 +quantifier prefix is represented via \seeglossary{schematic
   1.126 +variables}, such that the top-level structure is merely that of a
   1.127 +\seeglossary{Horn Clause}}.
   1.128 +
   1.129 +\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   1.130 +
   1.131 +*}
   1.132 +
   1.133 +subsection {* Equational reasoning *}
   1.134 +
   1.135 +text FIXME
   1.136 +
   1.137 +
   1.138 +section {* Proof terms *}
   1.139 +
   1.140 +text FIXME
   1.141 +
   1.142 +end