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