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