doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Tue Sep 05 22:05:41 2006 +0200 (2006-09-05) changeset 20480 4e0522d38968 parent 20477 e623b0e30541 child 20491 98ba42f19995 permissions -rw-r--r--
more on types and type classes;
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 framework of Pure Type Systems (PTS)
13   \cite{Barendregt-Geuvers:2001}, although there are some key
14   differences in the practical treatment of simple types.
16   Following type-theoretic parlance, the Pure logic consists of three
17   levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
18   "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
19   "\<And>"} for universal quantification (proofs depending on terms), and
20   @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
22   Pure derivations are relative to a logical theory, which declares
23   type constructors, term constants, and axioms.  Term constants and
24   axioms support schematic polymorphism.
25 *}
28 section {* Types \label{sec:types} *}
30 text {*
31   The language of types is an uninterpreted order-sorted first-order
32   algebra; types are qualified by ordered type classes.
34   \medskip A \emph{type class} is an abstract syntactic entity
35   declared in the theory context.  The \emph{subclass relation} @{text
36   "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
37   generating relation; the transitive closure maintained internally.
39   A \emph{sort} is a list of type classes written as @{text
40   "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
41   intersection.  Notationally, the curly braces are omitted for
42   singleton intersections, i.e.\ any class @{text "c"} may be read as
43   a sort @{text "{c}"}.  The ordering on type classes is extended to
44   sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq>
45   {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq>
46   d\<^isub>j"}.  The empty intersection @{text "{}"} refers to the
47   universal sort, which is the largest element wrt.\ the sort order.
48   The intersections of all (i.e.\ finitely many) classes declared in
49   the current theory are the minimal elements wrt.\ sort order.
51   \medskip A \emph{fixed type variable} is pair of a basic name
52   (starting with @{text "'"} character) and a sort constraint.  For
53   example, @{text "('a, s)"} which is usually printed as @{text
54   "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
55   indexname and a sort constraint.  For example, @{text "(('a, 0),
56   s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}.
58   Note that \emph{all} syntactic components contribute to the identity
59   of a type variables, including the literal sort constraint.  The
60   core logic handles type variables with the same name but different
61   sorts as different, even though the outer layers of the system make
62   it hard to produce anything like this.
64   A \emph{type constructor} is an @{text "k"}-ary type operator
65   declared in the theory.
67   A \emph{type} is defined inductively over type variables and type
68   constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>,
69   \<tau>\<^sub>k)c"}.  Type constructor application is usually written
70   postfix.  For @{text "k = 0"} the argument tuple is omitted, e.g.\
71   @{text "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
72   parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text
73   "(\<tau>) list"}.  Further notation is provided for specific
74   constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow>
75   \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"}
76   constructor.
78   A \emph{type abbreviation} is a syntactic abbreviation of an
79   arbitrary type expression of the theory.  Type abbreviations looks
80   like type constructors at the surface, but are expanded before the
81   core logic encounters them.
83   A \emph{type arity} declares the image behavior of a type
84   constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
85   s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
86   of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
87   sort @{text "s\<^isub>i"}.  The sort algebra is always maintained as
88   \emph{coregular}, which means that type arities are consistent with
89   the subclass relation: for each type constructor @{text "c"} and
90   classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
91   (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
92   :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
93   \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
95   The key property of the order-sorted algebra of types is that sort
96   constraints may be always fulfilled in a most general fashion: for
97   each type constructor @{text "c"} and sort @{text "s"} there is a
98   most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
99   s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
100   \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of
101   sort @{text "s\<^isub>i"}.  This means the unification problem on
102   the algebra of types has most general solutions (modulo renaming and
103   equivalence of sorts).  As a consequence, type-inference is able to
104   produce primary types.
105 *}
107 text %mlref {*
108   \begin{mldecls}
109   @{index_ML_type class} \\
110   @{index_ML_type sort} \\
111   @{index_ML_type typ} \\
112   @{index_ML_type arity} \\
113   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
114   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
115   @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
116   @{index_ML Sign.add_tyabbrs_i: "
117   (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
118   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
119   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
120   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
121   \end{mldecls}
123   \begin{description}
125   \item @{ML_type class} represents type classes; this is an alias for
126   @{ML_type string}.
128   \item @{ML_type sort} represents sorts; this is an alias for
129   @{ML_type "class list"}.
131   \item @{ML_type arity} represents type arities; this is an alias for
132   triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
133   (\<^vec>s)s"} described above.
135   \item @{ML_type typ} represents types; this is a datatype with
136   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
138   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
139   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
141   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
142   expression of of a given sort.
144   \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
145   type constructors @{text "c"} with @{text "k"} arguments, and
146   optional mixfix syntax.
148   \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
149   defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional
150   mixfix syntax) as @{text "\<tau>"}.
152   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
153   c\<^isub>n])"} declares new class @{text "c"} derived together with
154   class relations @{text "c \<subseteq> c\<^isub>i"}.
156   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
157   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
158   c\<^isub>2"}.
160   \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
161   arity @{text "c :: (\<^vec>s)s"}.
163   \end{description}
164 *}
168 section {* Terms \label{sec:terms} *}
170 text {*
171   \glossary{Term}{FIXME}
173   FIXME de-Bruijn representation of lambda terms
175   Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
176   and application @{text "t u"}, while types are usually implicit
177   thanks to type-inference.
179   Terms of type @{text "prop"} are called
180   propositions.  Logical statements are composed via @{text "\<And>x ::
181   \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
182 *}
185 text {*
187 FIXME
189 \glossary{Schematic polymorphism}{FIXME}
191 \glossary{Type variable}{FIXME}
193 *}
196 section {* Proof terms *}
198 text {*
199   FIXME
200 *}
203 section {* Theorems \label{sec:thms} *}
205 text {*
207   Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
208   \<phi>"}, with standard introduction and elimination rules for @{text
209   "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
210   hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The
211   corresponding proof terms are left implicit in the classic
212   LCF-approach'', although they could be exploited separately
213   \cite{Berghofer-Nipkow:2000}.
215   The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
216   \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal
217   conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
218   assumptions and conclusions emerging uniformly as simultaneous
219   statements.
223   FIXME
225 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
226 @{text "prop"}.  Internally, there is nothing special about
227 propositions apart from their type, but the concrete syntax enforces a
228 clear distinction.  Propositions are structured via implication @{text
229 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
230 else is considered atomic.  The canonical form for propositions is
231 that of a \seeglossary{Hereditary Harrop Formula}.}
233 \glossary{Theorem}{A proven proposition within a certain theory and
234 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
235 rarely spelled out explicitly.  Theorems are usually normalized
236 according to the \seeglossary{HHF} format.}
238 \glossary{Fact}{Sometimes used interchangably for
239 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
240 essentially an extra-logical conjunction.  Facts emerge either as
241 local assumptions, or as results of local goal statements --- both may
242 be simultaneous, hence the list representation.}
244 \glossary{Schematic variable}{FIXME}
246 \glossary{Fixed variable}{A variable that is bound within a certain
247 proof context; an arbitrary-but-fixed entity within a portion of proof
248 text.}
250 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
252 \glossary{Bound variable}{FIXME}
254 \glossary{Variable}{See \seeglossary{schematic variable},
255 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
256 \seeglossary{type variable}.  The distinguishing feature of different
257 variables is their binding scope.}
259 *}
261 subsection {* Primitive inferences *}
263 text FIXME
266 subsection {* Higher-order resolution *}
268 text {*
270 FIXME
272 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
273 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
274 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
275 Any proposition may be put into HHF form by normalizing with the rule
276 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
277 quantifier prefix is represented via \seeglossary{schematic
278 variables}, such that the top-level structure is merely that of a
279 \seeglossary{Horn Clause}}.
281 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
283 *}
285 subsection {* Equational reasoning *}
287 text FIXME
290 end