doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Mon Jan 02 20:16:52 2006 +0100 (2006-01-02)
changeset 18537 2681f9e34390
child 20437 0eb5e30fd620
permissions -rw-r--r--
"The Isabelle/Isar Implementation" manual;
     1 
     2 (* $Id$ *)
     3 
     4 theory logic imports base begin
     5 
     6 chapter {* Pure logic *}
     7 
     8 section {* Syntax *}
     9 
    10 subsection {* Simply-typed lambda calculus *}
    11 
    12 text {*
    13 
    14 FIXME
    15 
    16 \glossary{Type}{FIXME}
    17 \glossary{Term}{FIXME}
    18 
    19 *}
    20 
    21 subsection {* The order-sorted algebra of types *}
    22 
    23 text {*
    24 
    25 FIXME
    26 
    27 \glossary{Type constructor}{FIXME}
    28 
    29 \glossary{Type class}{FIXME}
    30 
    31 \glossary{Type arity}{FIXME}
    32 
    33 \glossary{Sort}{FIXME}
    34 
    35 *}
    36 
    37 
    38 subsection {* Type-inference and schematic polymorphism *}
    39 
    40 text {*
    41 
    42 FIXME
    43 
    44 \glossary{Schematic polymorphism}{FIXME}
    45 
    46 \glossary{Type variable}{FIXME}
    47 
    48 *}
    49 
    50 
    51 section {* Theory *}
    52 
    53 text {*
    54 
    55 FIXME
    56 
    57 \glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
    58 theory context, but slightly more flexible since it may be used at
    59 different type-instances, due to \seeglossary{schematic
    60 polymorphism.}}
    61 
    62 *}
    63 
    64 
    65 section {* Deduction *}
    66 
    67 text {*
    68 
    69   FIXME
    70 
    71 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
    72 @{text "prop"}.  Internally, there is nothing special about
    73 propositions apart from their type, but the concrete syntax enforces a
    74 clear distinction.  Propositions are structured via implication @{text
    75 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
    76 else is considered atomic.  The canonical form for propositions is
    77 that of a \seeglossary{Hereditary Harrop Formula}.}
    78 
    79 \glossary{Theorem}{A proven proposition within a certain theory and
    80 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
    81 rarely spelled out explicitly.  Theorems are usually normalized
    82 according to the \seeglossary{HHF} format.}
    83 
    84 \glossary{Fact}{Sometimes used interchangably for
    85 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
    86 essentially an extra-logical conjunction.  Facts emerge either as
    87 local assumptions, or as results of local goal statements --- both may
    88 be simultaneous, hence the list representation.}
    89 
    90 \glossary{Schematic variable}{FIXME}
    91 
    92 \glossary{Fixed variable}{A variable that is bound within a certain
    93 proof context; an arbitrary-but-fixed entity within a portion of proof
    94 text.}
    95 
    96 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
    97 
    98 \glossary{Bound variable}{FIXME}
    99 
   100 \glossary{Variable}{See \seeglossary{schematic variable},
   101 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
   102 \seeglossary{type variable}.  The distinguishing feature of different
   103 variables is their binding scope.}
   104 
   105 *}
   106 
   107 subsection {* Primitive inferences *}
   108 
   109 text FIXME
   110 
   111 subsection {* Higher-order resolution *}
   112 
   113 text {*
   114 
   115 FIXME
   116 
   117 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   118 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   119 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   120 Any proposition may be put into HHF form by normalizing with the rule
   121 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
   122 quantifier prefix is represented via \seeglossary{schematic
   123 variables}, such that the top-level structure is merely that of a
   124 \seeglossary{Horn Clause}}.
   125 
   126 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   127 
   128 *}
   129 
   130 subsection {* Equational reasoning *}
   131 
   132 text FIXME
   133 
   134 
   135 section {* Proof terms *}
   136 
   137 text FIXME
   138 
   139 end