18537
|
1 |
|
|
2 |
(* $Id$ *)
|
|
3 |
|
|
4 |
theory logic imports base begin
|
|
5 |
|
20470
|
6 |
chapter {* Primitive logic \label{ch:logic} *}
|
18537
|
7 |
|
20480
|
8 |
text {*
|
|
9 |
The logical foundations of Isabelle/Isar are that of the Pure logic,
|
|
10 |
which has been introduced as a natural-deduction framework in
|
|
11 |
\cite{paulson700}. This is essentially the same logic as ``@{text
|
|
12 |
"\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS)
|
|
13 |
\cite{Barendregt-Geuvers:2001}, although there are some key
|
20491
|
14 |
differences in the specific treatment of simple types in
|
|
15 |
Isabelle/Pure.
|
20480
|
16 |
|
|
17 |
Following type-theoretic parlance, the Pure logic consists of three
|
|
18 |
levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
|
|
19 |
"\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
|
|
20 |
"\<And>"} for universal quantification (proofs depending on terms), and
|
|
21 |
@{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
|
|
22 |
|
|
23 |
Pure derivations are relative to a logical theory, which declares
|
20491
|
24 |
type constructors, term constants, and axioms. Theory declarations
|
|
25 |
support schematic polymorphism, which is strictly speaking outside
|
|
26 |
the logic.\footnote{Incidently, this is the main logical reason, why
|
|
27 |
the theory context @{text "\<Theta>"} is separate from the context @{text
|
|
28 |
"\<Gamma>"} of the core calculus.}
|
20480
|
29 |
*}
|
|
30 |
|
|
31 |
|
20451
|
32 |
section {* Types \label{sec:types} *}
|
20437
|
33 |
|
|
34 |
text {*
|
20480
|
35 |
The language of types is an uninterpreted order-sorted first-order
|
|
36 |
algebra; types are qualified by ordered type classes.
|
|
37 |
|
|
38 |
\medskip A \emph{type class} is an abstract syntactic entity
|
|
39 |
declared in the theory context. The \emph{subclass relation} @{text
|
|
40 |
"c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
|
20491
|
41 |
generating relation; the transitive closure is maintained
|
|
42 |
internally. The resulting relation is an ordering: reflexive,
|
|
43 |
transitive, and antisymmetric.
|
20451
|
44 |
|
20480
|
45 |
A \emph{sort} is a list of type classes written as @{text
|
|
46 |
"{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
|
|
47 |
intersection. Notationally, the curly braces are omitted for
|
|
48 |
singleton intersections, i.e.\ any class @{text "c"} may be read as
|
|
49 |
a sort @{text "{c}"}. The ordering on type classes is extended to
|
20491
|
50 |
sorts according to the meaning of intersections: @{text
|
|
51 |
"{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff
|
|
52 |
@{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}. The empty intersection
|
|
53 |
@{text "{}"} refers to the universal sort, which is the largest
|
|
54 |
element wrt.\ the sort order. The intersections of all (finitely
|
|
55 |
many) classes declared in the current theory are the minimal
|
|
56 |
elements wrt.\ the sort order.
|
20480
|
57 |
|
20491
|
58 |
\medskip A \emph{fixed type variable} is a pair of a basic name
|
20480
|
59 |
(starting with @{text "'"} character) and a sort constraint. For
|
|
60 |
example, @{text "('a, s)"} which is usually printed as @{text
|
|
61 |
"\<alpha>\<^isub>s"}. A \emph{schematic type variable} is a pair of an
|
|
62 |
indexname and a sort constraint. For example, @{text "(('a, 0),
|
20491
|
63 |
s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}.
|
20451
|
64 |
|
20480
|
65 |
Note that \emph{all} syntactic components contribute to the identity
|
20491
|
66 |
of type variables, including the literal sort constraint. The core
|
|
67 |
logic handles type variables with the same name but different sorts
|
|
68 |
as different, although some outer layers of the system make it hard
|
|
69 |
to produce anything like this.
|
20451
|
70 |
|
20491
|
71 |
A \emph{type constructor} is a @{text "k"}-ary operator on types
|
|
72 |
declared in the theory. Type constructor application is usually
|
|
73 |
written postfix. For @{text "k = 0"} the argument tuple is omitted,
|
|
74 |
e.g.\ @{text "prop"} instead of @{text "()prop"}. For @{text "k =
|
|
75 |
1"} the parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of
|
|
76 |
@{text "(\<alpha>)list"}. Further notation is provided for specific
|
|
77 |
constructors, notably right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"}
|
|
78 |
instead of @{text "(\<alpha>, \<beta>)fun"} constructor.
|
20480
|
79 |
|
|
80 |
A \emph{type} is defined inductively over type variables and type
|
20491
|
81 |
constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
|
|
82 |
(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}.
|
20451
|
83 |
|
20480
|
84 |
A \emph{type abbreviation} is a syntactic abbreviation of an
|
|
85 |
arbitrary type expression of the theory. Type abbreviations looks
|
|
86 |
like type constructors at the surface, but are expanded before the
|
|
87 |
core logic encounters them.
|
|
88 |
|
|
89 |
A \emph{type arity} declares the image behavior of a type
|
|
90 |
constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
|
20491
|
91 |
s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
|
20480
|
92 |
of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
|
20491
|
93 |
sort @{text "s\<^isub>i"}. Arity declarations are implicitly
|
|
94 |
completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::
|
|
95 |
(\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
|
|
96 |
|
|
97 |
\medskip The sort algebra is always maintained as \emph{coregular},
|
|
98 |
which means that type arities are consistent with the subclass
|
|
99 |
relation: for each type constructor @{text "c"} and classes @{text
|
|
100 |
"c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
|
20480
|
101 |
(\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
|
|
102 |
:: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
|
|
103 |
\<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
|
20451
|
104 |
|
20491
|
105 |
The key property of a coregular order-sorted algebra is that sort
|
20480
|
106 |
constraints may be always fulfilled in a most general fashion: for
|
|
107 |
each type constructor @{text "c"} and sort @{text "s"} there is a
|
|
108 |
most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
|
20491
|
109 |
s\<^isub>k)"} such that a type scheme @{text
|
|
110 |
"(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is
|
|
111 |
of sort @{text "s"}. Consequently, the unification problem on the
|
|
112 |
algebra of types has most general solutions (modulo renaming and
|
|
113 |
equivalence of sorts). Moreover, the usual type-inference algorithm
|
|
114 |
will produce primary types as expected \cite{nipkow-prehofer}.
|
20480
|
115 |
*}
|
20451
|
116 |
|
20480
|
117 |
text %mlref {*
|
|
118 |
\begin{mldecls}
|
|
119 |
@{index_ML_type class} \\
|
|
120 |
@{index_ML_type sort} \\
|
|
121 |
@{index_ML_type typ} \\
|
|
122 |
@{index_ML_type arity} \\
|
|
123 |
@{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
|
|
124 |
@{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
|
|
125 |
@{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
|
|
126 |
@{index_ML Sign.add_tyabbrs_i: "
|
|
127 |
(bstring * string list * typ * mixfix) list -> theory -> theory"} \\
|
|
128 |
@{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
|
|
129 |
@{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
|
|
130 |
@{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
|
|
131 |
\end{mldecls}
|
|
132 |
|
|
133 |
\begin{description}
|
|
134 |
|
|
135 |
\item @{ML_type class} represents type classes; this is an alias for
|
|
136 |
@{ML_type string}.
|
|
137 |
|
|
138 |
\item @{ML_type sort} represents sorts; this is an alias for
|
|
139 |
@{ML_type "class list"}.
|
20451
|
140 |
|
20480
|
141 |
\item @{ML_type arity} represents type arities; this is an alias for
|
|
142 |
triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
|
|
143 |
(\<^vec>s)s"} described above.
|
|
144 |
|
|
145 |
\item @{ML_type typ} represents types; this is a datatype with
|
|
146 |
constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
|
|
147 |
|
|
148 |
\item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
|
|
149 |
tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
|
|
150 |
|
|
151 |
\item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
|
20491
|
152 |
is of a given sort.
|
20480
|
153 |
|
|
154 |
\item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
|
20491
|
155 |
type constructors @{text "c"} with @{text "k"} arguments and
|
20480
|
156 |
optional mixfix syntax.
|
20451
|
157 |
|
20480
|
158 |
\item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
|
20491
|
159 |
defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with
|
|
160 |
optional mixfix syntax.
|
20480
|
161 |
|
|
162 |
\item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
|
|
163 |
c\<^isub>n])"} declares new class @{text "c"} derived together with
|
20491
|
164 |
class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
|
20480
|
165 |
|
|
166 |
\item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
|
|
167 |
c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
|
|
168 |
c\<^isub>2"}.
|
|
169 |
|
|
170 |
\item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
|
|
171 |
arity @{text "c :: (\<^vec>s)s"}.
|
|
172 |
|
|
173 |
\end{description}
|
20437
|
174 |
*}
|
|
175 |
|
|
176 |
|
20480
|
177 |
|
20451
|
178 |
section {* Terms \label{sec:terms} *}
|
18537
|
179 |
|
|
180 |
text {*
|
20451
|
181 |
\glossary{Term}{FIXME}
|
18537
|
182 |
|
20491
|
183 |
The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
|
|
184 |
with de-Bruijn indices for bound variables, and named free
|
|
185 |
variables, and constants. Terms with loose bound variables are
|
|
186 |
usually considered malformed. The types of variables and constants
|
|
187 |
is stored explicitly at each occurrence in the term (which is a
|
|
188 |
known performance issue).
|
|
189 |
|
20451
|
190 |
FIXME de-Bruijn representation of lambda terms
|
20480
|
191 |
|
|
192 |
Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
|
|
193 |
and application @{text "t u"}, while types are usually implicit
|
|
194 |
thanks to type-inference.
|
|
195 |
|
|
196 |
Terms of type @{text "prop"} are called
|
|
197 |
propositions. Logical statements are composed via @{text "\<And>x ::
|
|
198 |
\<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
|
18537
|
199 |
*}
|
|
200 |
|
|
201 |
|
|
202 |
text {*
|
|
203 |
|
|
204 |
FIXME
|
|
205 |
|
|
206 |
\glossary{Schematic polymorphism}{FIXME}
|
|
207 |
|
|
208 |
\glossary{Type variable}{FIXME}
|
|
209 |
|
|
210 |
*}
|
|
211 |
|
|
212 |
|
20451
|
213 |
section {* Theorems \label{sec:thms} *}
|
18537
|
214 |
|
|
215 |
text {*
|
|
216 |
|
20480
|
217 |
Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
|
|
218 |
\<phi>"}, with standard introduction and elimination rules for @{text
|
|
219 |
"\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
|
|
220 |
hypotheses @{text "A"} from the context @{text "\<Gamma>"}. The
|
|
221 |
corresponding proof terms are left implicit in the classic
|
|
222 |
``LCF-approach'', although they could be exploited separately
|
|
223 |
\cite{Berghofer-Nipkow:2000}.
|
|
224 |
|
|
225 |
The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
|
|
226 |
\<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules. The internal
|
|
227 |
conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
|
|
228 |
assumptions and conclusions emerging uniformly as simultaneous
|
|
229 |
statements.
|
|
230 |
|
|
231 |
|
|
232 |
|
18537
|
233 |
FIXME
|
|
234 |
|
|
235 |
\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
|
|
236 |
@{text "prop"}. Internally, there is nothing special about
|
|
237 |
propositions apart from their type, but the concrete syntax enforces a
|
|
238 |
clear distinction. Propositions are structured via implication @{text
|
|
239 |
"A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
|
|
240 |
else is considered atomic. The canonical form for propositions is
|
|
241 |
that of a \seeglossary{Hereditary Harrop Formula}.}
|
|
242 |
|
|
243 |
\glossary{Theorem}{A proven proposition within a certain theory and
|
|
244 |
proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
|
|
245 |
rarely spelled out explicitly. Theorems are usually normalized
|
|
246 |
according to the \seeglossary{HHF} format.}
|
|
247 |
|
|
248 |
\glossary{Fact}{Sometimes used interchangably for
|
|
249 |
\seeglossary{theorem}. Strictly speaking, a list of theorems,
|
|
250 |
essentially an extra-logical conjunction. Facts emerge either as
|
|
251 |
local assumptions, or as results of local goal statements --- both may
|
|
252 |
be simultaneous, hence the list representation.}
|
|
253 |
|
|
254 |
\glossary{Schematic variable}{FIXME}
|
|
255 |
|
|
256 |
\glossary{Fixed variable}{A variable that is bound within a certain
|
|
257 |
proof context; an arbitrary-but-fixed entity within a portion of proof
|
|
258 |
text.}
|
|
259 |
|
|
260 |
\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
|
|
261 |
|
|
262 |
\glossary{Bound variable}{FIXME}
|
|
263 |
|
|
264 |
\glossary{Variable}{See \seeglossary{schematic variable},
|
|
265 |
\seeglossary{fixed variable}, \seeglossary{bound variable}, or
|
|
266 |
\seeglossary{type variable}. The distinguishing feature of different
|
|
267 |
variables is their binding scope.}
|
|
268 |
|
|
269 |
*}
|
|
270 |
|
20491
|
271 |
|
|
272 |
section {* Proof terms *}
|
18537
|
273 |
|
20491
|
274 |
text {*
|
|
275 |
FIXME !?
|
|
276 |
*}
|
18537
|
277 |
|
20480
|
278 |
|
20491
|
279 |
section {* Rules \label{sec:rules} *}
|
18537
|
280 |
|
|
281 |
text {*
|
|
282 |
|
|
283 |
FIXME
|
|
284 |
|
20491
|
285 |
A \emph{rule} is any Pure theorem in HHF normal form; there is a
|
|
286 |
separate calculus for rule composition, which is modeled after
|
|
287 |
Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
|
|
288 |
rules to be nested arbitrarily, similar to \cite{extensions91}.
|
|
289 |
|
|
290 |
Normally, all theorems accessible to the user are proper rules.
|
|
291 |
Low-level inferences are occasional required internally, but the
|
|
292 |
result should be always presented in canonical form. The higher
|
|
293 |
interfaces of Isabelle/Isar will always produce proper rules. It is
|
|
294 |
important to maintain this invariant in add-on applications!
|
|
295 |
|
|
296 |
There are two main principles of rule composition: @{text
|
|
297 |
"resolution"} (i.e.\ backchaining of rules) and @{text
|
|
298 |
"by-assumption"} (i.e.\ closing a branch); both principles are
|
|
299 |
combined in the variants of @{text "elim-resosultion"} and @{text
|
|
300 |
"dest-resolution"}. Raw @{text "composition"} is occasionally
|
|
301 |
useful as well, also it is strictly speaking outside of the proper
|
|
302 |
rule calculus.
|
|
303 |
|
|
304 |
Rules are treated modulo general higher-order unification, which is
|
|
305 |
unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
|
|
306 |
on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo
|
|
307 |
the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
|
|
308 |
|
|
309 |
This means that any operations within the rule calculus may be
|
|
310 |
subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common
|
|
311 |
practice not to contract or expand unnecessarily. Some mechanisms
|
|
312 |
prefer an one form, others the opposite, so there is a potential
|
|
313 |
danger to produce some oscillation!
|
|
314 |
|
|
315 |
Only few operations really work \emph{modulo} HHF conversion, but
|
|
316 |
expect a normal form: quantifiers @{text "\<And>"} before implications
|
|
317 |
@{text "\<Longrightarrow>"} at each level of nesting.
|
|
318 |
|
18537
|
319 |
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
|
|
320 |
format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
|
|
321 |
A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
|
|
322 |
Any proposition may be put into HHF form by normalizing with the rule
|
|
323 |
@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost
|
|
324 |
quantifier prefix is represented via \seeglossary{schematic
|
|
325 |
variables}, such that the top-level structure is merely that of a
|
|
326 |
\seeglossary{Horn Clause}}.
|
|
327 |
|
|
328 |
\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
|
|
329 |
|
|
330 |
*}
|
|
331 |
|
|
332 |
end
|