doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Fri Sep 08 17:33:05 2006 +0200 (2006-09-08) changeset 20493 48fea5e99505 parent 20491 98ba42f19995 child 20494 99ad217b6974 permissions -rw-r--r--
tuned;
2 (* $Id$ *)
4 theory logic imports base begin
6 chapter {* Primitive logic \label{ch:logic} *}
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 setting of Pure Type Systems (PTS)
13   \cite{Barendregt-Geuvers:2001}, although there are some key
14   differences in the specific treatment of simple types in
15   Isabelle/Pure.
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).
23   Pure derivations are relative to a logical theory, which declares
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.}
29 *}
32 section {* Types \label{sec:types} *}
34 text {*
35   The language of types is an uninterpreted order-sorted first-order
36   algebra; types are qualified by ordered type classes.
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
41   generating relation; the transitive closure is maintained
42   internally.  The resulting relation is an ordering: reflexive,
43   transitive, and antisymmetric.
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
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.
58   \medskip A \emph{fixed type variable} is a pair of a basic name
59   (starting with a @{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),
63   s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}.
65   Note that \emph{all} syntactic components contribute to the identity
66   of type variables, including the sort constraint.  The core logic
67   handles type variables with the same name but different sorts as
68   different, although some outer layers of the system make it hard to
69   produce anything like this.
71   A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
72   on types declared in the theory.  Type constructor application is
73   usually written postfix as @{text "(FIXME)\<kappa>"}.  For @{text "k = 0"}
74   the argument tuple is omitted, e.g.\ @{text "prop"} instead of
75   @{text "()prop"}.  For @{text "k = 1"} the parentheses are omitted,
76   e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.  Further
77   notation is provided for specific constructors, notably
78   right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
79   \<beta>)fun"} constructor.
81   A \emph{type} is defined inductively over type variables and type
82   constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
83   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}.
85   A \emph{type abbreviation} is a syntactic abbreviation of an
86   arbitrary type expression of the theory.  Type abbreviations looks
87   like type constructors at the surface, but are expanded before the
88   core logic encounters them.
90   A \emph{type arity} declares the image behavior of a type
91   constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
92   s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
93   of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
94   sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
95   completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::
96   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
98   \medskip The sort algebra is always maintained as \emph{coregular},
99   which means that type arities are consistent with the subclass
100   relation: for each type constructor @{text "c"} and classes @{text
101   "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
102   (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
103   :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
104   \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
106   The key property of a coregular order-sorted algebra is that sort
107   constraints may be always fulfilled in a most general fashion: for
108   each type constructor @{text "c"} and sort @{text "s"} there is a
109   most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
110   s\<^isub>k)"} such that a type scheme @{text
111   "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is
112   of sort @{text "s"}.  Consequently, the unification problem on the
113   algebra of types has most general solutions (modulo renaming and
114   equivalence of sorts).  Moreover, the usual type-inference algorithm
115   will produce primary types as expected \cite{nipkow-prehofer}.
116 *}
118 text %mlref {*
119   \begin{mldecls}
120   @{index_ML_type class} \\
121   @{index_ML_type sort} \\
122   @{index_ML_type typ} \\
123   @{index_ML_type arity} \\
124   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
125   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
126   @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
127   @{index_ML Sign.add_tyabbrs_i: "
128   (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
129   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
130   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
131   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
132   \end{mldecls}
134   \begin{description}
136   \item @{ML_type class} represents type classes; this is an alias for
137   @{ML_type string}.
139   \item @{ML_type sort} represents sorts; this is an alias for
140   @{ML_type "class list"}.
142   \item @{ML_type arity} represents type arities; this is an alias for
143   triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
144   (\<^vec>s)s"} described above.
146   \item @{ML_type typ} represents types; this is a datatype with
147   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
149   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
150   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
152   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
153   is of a given sort.
155   \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
156   type constructors @{text "c"} with @{text "k"} arguments and
157   optional mixfix syntax.
159   \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
160   defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with
161   optional mixfix syntax.
163   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
164   c\<^isub>n])"} declares new class @{text "c"} derived together with
165   class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
167   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
168   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
169   c\<^isub>2"}.
171   \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
172   arity @{text "c :: (\<^vec>s)s"}.
174   \end{description}
175 *}
179 section {* Terms \label{sec:terms} *}
181 text {*
182   \glossary{Term}{FIXME}
184   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
185   with de-Bruijn indices for bound variables, and named free
186   variables, and constants.  Terms with loose bound variables are
187   usually considered malformed.  The types of variables and constants
188   is stored explicitly at each occurrence in the term (which is a
189   known performance issue).
191   FIXME de-Bruijn representation of lambda terms
193   Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
194   and application @{text "t u"}, while types are usually implicit
195   thanks to type-inference.
197   Terms of type @{text "prop"} are called
198   propositions.  Logical statements are composed via @{text "\<And>x ::
199   \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
200 *}
203 text {*
205 FIXME
207 \glossary{Schematic polymorphism}{FIXME}
209 \glossary{Type variable}{FIXME}
211 *}
214 section {* Theorems \label{sec:thms} *}
216 text {*
218   Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
219   \<phi>"}, with standard introduction and elimination rules for @{text
220   "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
221   hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The
222   corresponding proof terms are left implicit in the classic
223   LCF-approach'', although they could be exploited separately
224   \cite{Berghofer-Nipkow:2000}.
226   The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
227   \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal
228   conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
229   assumptions and conclusions emerging uniformly as simultaneous
230   statements.
234   FIXME
236 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
237 @{text "prop"}.  Internally, there is nothing special about
238 propositions apart from their type, but the concrete syntax enforces a
239 clear distinction.  Propositions are structured via implication @{text
240 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
241 else is considered atomic.  The canonical form for propositions is
242 that of a \seeglossary{Hereditary Harrop Formula}.}
244 \glossary{Theorem}{A proven proposition within a certain theory and
245 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
246 rarely spelled out explicitly.  Theorems are usually normalized
247 according to the \seeglossary{HHF} format.}
249 \glossary{Fact}{Sometimes used interchangably for
250 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
251 essentially an extra-logical conjunction.  Facts emerge either as
252 local assumptions, or as results of local goal statements --- both may
253 be simultaneous, hence the list representation.}
255 \glossary{Schematic variable}{FIXME}
257 \glossary{Fixed variable}{A variable that is bound within a certain
258 proof context; an arbitrary-but-fixed entity within a portion of proof
259 text.}
261 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
263 \glossary{Bound variable}{FIXME}
265 \glossary{Variable}{See \seeglossary{schematic variable},
266 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
267 \seeglossary{type variable}.  The distinguishing feature of different
268 variables is their binding scope.}
270 *}
273 section {* Proof terms *}
275 text {*
276   FIXME !?
277 *}
280 section {* Rules \label{sec:rules} *}
282 text {*
284 FIXME
286   A \emph{rule} is any Pure theorem in HHF normal form; there is a
287   separate calculus for rule composition, which is modeled after
288   Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
289   rules to be nested arbitrarily, similar to \cite{extensions91}.
291   Normally, all theorems accessible to the user are proper rules.
292   Low-level inferences are occasional required internally, but the
293   result should be always presented in canonical form.  The higher
294   interfaces of Isabelle/Isar will always produce proper rules.  It is
295   important to maintain this invariant in add-on applications!
297   There are two main principles of rule composition: @{text
298   "resolution"} (i.e.\ backchaining of rules) and @{text
299   "by-assumption"} (i.e.\ closing a branch); both principles are
300   combined in the variants of @{text "elim-resosultion"} and @{text
301   "dest-resolution"}.  Raw @{text "composition"} is occasionally
302   useful as well, also it is strictly speaking outside of the proper
303   rule calculus.
305   Rules are treated modulo general higher-order unification, which is
306   unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
307   on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo
308   the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
310   This means that any operations within the rule calculus may be
311   subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common
312   practice not to contract or expand unnecessarily.  Some mechanisms
313   prefer an one form, others the opposite, so there is a potential
314   danger to produce some oscillation!
316   Only few operations really work \emph{modulo} HHF conversion, but
317   expect a normal form: quantifiers @{text "\<And>"} before implications
318   @{text "\<Longrightarrow>"} at each level of nesting.
320 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
321 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
322 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
323 Any proposition may be put into HHF form by normalizing with the rule
324 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
325 quantifier prefix is represented via \seeglossary{schematic
326 variables}, such that the top-level structure is merely that of a
327 \seeglossary{Horn Clause}}.
329 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
331 *}
333 end