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