doc-src/IsarImplementation/Thy/document/logic.tex
author wenzelm
Tue Sep 05 16:42:32 2006 +0200 (2006-09-05 ago)
changeset 20477 e623b0e30541
parent 20472 e993073eda4c
child 20481 c96f80442ce6
permissions -rw-r--r--
tuned;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{logic}%
     4 %
     5 \isadelimtheory
     6 \isanewline
     7 \isanewline
     8 \isanewline
     9 %
    10 \endisadelimtheory
    11 %
    12 \isatagtheory
    13 \isacommand{theory}\isamarkupfalse%
    14 \ logic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
    15 \endisatagtheory
    16 {\isafoldtheory}%
    17 %
    18 \isadelimtheory
    19 %
    20 \endisadelimtheory
    21 %
    22 \isamarkupchapter{Primitive logic \label{ch:logic}%
    23 }
    24 \isamarkuptrue%
    25 %
    26 \isamarkupsection{Types \label{sec:types}%
    27 }
    28 \isamarkuptrue%
    29 %
    30 \begin{isamarkuptext}%
    31 \glossary{Type class}{FIXME}
    32 
    33   \glossary{Type arity}{FIXME}
    34 
    35   \glossary{Sort}{FIXME}
    36 
    37   FIXME classes and sorts
    38 
    39 
    40   \glossary{Type}{FIXME}
    41 
    42   \glossary{Type constructor}{FIXME}
    43 
    44   \glossary{Type variable}{FIXME}
    45 
    46   FIXME simple types%
    47 \end{isamarkuptext}%
    48 \isamarkuptrue%
    49 %
    50 \isamarkupsection{Terms \label{sec:terms}%
    51 }
    52 \isamarkuptrue%
    53 %
    54 \begin{isamarkuptext}%
    55 \glossary{Term}{FIXME}
    56 
    57   FIXME de-Bruijn representation of lambda terms%
    58 \end{isamarkuptext}%
    59 \isamarkuptrue%
    60 %
    61 \begin{isamarkuptext}%
    62 FIXME
    63 
    64 \glossary{Schematic polymorphism}{FIXME}
    65 
    66 \glossary{Type variable}{FIXME}%
    67 \end{isamarkuptext}%
    68 \isamarkuptrue%
    69 %
    70 \isamarkupsection{Proof terms%
    71 }
    72 \isamarkuptrue%
    73 %
    74 \begin{isamarkuptext}%
    75 FIXME%
    76 \end{isamarkuptext}%
    77 \isamarkuptrue%
    78 %
    79 \isamarkupsection{Theorems \label{sec:thms}%
    80 }
    81 \isamarkuptrue%
    82 %
    83 \begin{isamarkuptext}%
    84 FIXME
    85 
    86 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
    87 \isa{prop}.  Internally, there is nothing special about
    88 propositions apart from their type, but the concrete syntax enforces a
    89 clear distinction.  Propositions are structured via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} --- anything
    90 else is considered atomic.  The canonical form for propositions is
    91 that of a \seeglossary{Hereditary Harrop Formula}.}
    92 
    93 \glossary{Theorem}{A proven proposition within a certain theory and
    94 proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are
    95 rarely spelled out explicitly.  Theorems are usually normalized
    96 according to the \seeglossary{HHF} format.}
    97 
    98 \glossary{Fact}{Sometimes used interchangably for
    99 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
   100 essentially an extra-logical conjunction.  Facts emerge either as
   101 local assumptions, or as results of local goal statements --- both may
   102 be simultaneous, hence the list representation.}
   103 
   104 \glossary{Schematic variable}{FIXME}
   105 
   106 \glossary{Fixed variable}{A variable that is bound within a certain
   107 proof context; an arbitrary-but-fixed entity within a portion of proof
   108 text.}
   109 
   110 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
   111 
   112 \glossary{Bound variable}{FIXME}
   113 
   114 \glossary{Variable}{See \seeglossary{schematic variable},
   115 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
   116 \seeglossary{type variable}.  The distinguishing feature of different
   117 variables is their binding scope.}%
   118 \end{isamarkuptext}%
   119 \isamarkuptrue%
   120 %
   121 \isamarkupsubsection{Primitive inferences%
   122 }
   123 \isamarkuptrue%
   124 %
   125 \begin{isamarkuptext}%
   126 FIXME%
   127 \end{isamarkuptext}%
   128 \isamarkuptrue%
   129 %
   130 \isamarkupsubsection{Higher-order resolution%
   131 }
   132 \isamarkuptrue%
   133 %
   134 \begin{isamarkuptext}%
   135 FIXME
   136 
   137 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   138 format is defined inductively as \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x} and atomic propositions \isa{A}.
   139 Any proposition may be put into HHF form by normalizing with the rule
   140 \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}.  In Isabelle, the outermost
   141 quantifier prefix is represented via \seeglossary{schematic
   142 variables}, such that the top-level structure is merely that of a
   143 \seeglossary{Horn Clause}}.
   144 
   145 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}%
   146 \end{isamarkuptext}%
   147 \isamarkuptrue%
   148 %
   149 \isamarkupsubsection{Equational reasoning%
   150 }
   151 \isamarkuptrue%
   152 %
   153 \begin{isamarkuptext}%
   154 FIXME%
   155 \end{isamarkuptext}%
   156 \isamarkuptrue%
   157 %
   158 \isamarkupsection{Raw theories%
   159 }
   160 \isamarkuptrue%
   161 %
   162 \begin{isamarkuptext}%
   163 FIXME
   164 
   165 \glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
   166 theory context, but slightly more flexible since it may be used at
   167 different type-instances, due to \seeglossary{schematic
   168 polymorphism.}}
   169 
   170 \glossary{Axiom}{FIXME}
   171 
   172 \glossary{Primitive definition}{FIXME}%
   173 \end{isamarkuptext}%
   174 \isamarkuptrue%
   175 %
   176 \isadelimtheory
   177 %
   178 \endisadelimtheory
   179 %
   180 \isatagtheory
   181 \isacommand{end}\isamarkupfalse%
   182 %
   183 \endisatagtheory
   184 {\isafoldtheory}%
   185 %
   186 \isadelimtheory
   187 %
   188 \endisadelimtheory
   189 \isanewline
   190 \end{isabellebody}%
   191 %%% Local Variables:
   192 %%% mode: latex
   193 %%% TeX-master: "root"
   194 %%% End: