9 The logical foundations of Isabelle/Isar are that of the Pure logic, |
9 The logical foundations of Isabelle/Isar are that of the Pure logic, |
10 which has been introduced as a natural-deduction framework in |
10 which has been introduced as a natural-deduction framework in |
11 \cite{paulson700}. This is essentially the same logic as ``@{text |
11 \cite{paulson700}. This is essentially the same logic as ``@{text |
12 "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS) |
12 "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS) |
13 \cite{Barendregt-Geuvers:2001}, although there are some key |
13 \cite{Barendregt-Geuvers:2001}, although there are some key |
14 differences in the practical treatment of simple types. |
14 differences in the specific treatment of simple types in |
|
15 Isabelle/Pure. |
15 |
16 |
16 Following type-theoretic parlance, the Pure logic consists of three |
17 Following type-theoretic parlance, the Pure logic consists of three |
17 levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text |
18 levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text |
18 "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text |
19 "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text |
19 "\<And>"} for universal quantification (proofs depending on terms), and |
20 "\<And>"} for universal quantification (proofs depending on terms), and |
20 @{text "\<Longrightarrow>"} for implication (proofs depending on proofs). |
21 @{text "\<Longrightarrow>"} for implication (proofs depending on proofs). |
21 |
22 |
22 Pure derivations are relative to a logical theory, which declares |
23 Pure derivations are relative to a logical theory, which declares |
23 type constructors, term constants, and axioms. Term constants and |
24 type constructors, term constants, and axioms. Theory declarations |
24 axioms support schematic polymorphism. |
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.} |
25 *} |
29 *} |
26 |
30 |
27 |
31 |
28 section {* Types \label{sec:types} *} |
32 section {* Types \label{sec:types} *} |
29 |
33 |
32 algebra; types are qualified by ordered type classes. |
36 algebra; types are qualified by ordered type classes. |
33 |
37 |
34 \medskip A \emph{type class} is an abstract syntactic entity |
38 \medskip A \emph{type class} is an abstract syntactic entity |
35 declared in the theory context. The \emph{subclass relation} @{text |
39 declared in the theory context. The \emph{subclass relation} @{text |
36 "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic |
40 "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic |
37 generating relation; the transitive closure maintained internally. |
41 generating relation; the transitive closure is maintained |
|
42 internally. The resulting relation is an ordering: reflexive, |
|
43 transitive, and antisymmetric. |
38 |
44 |
39 A \emph{sort} is a list of type classes written as @{text |
45 A \emph{sort} is a list of type classes written as @{text |
40 "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic |
46 "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic |
41 intersection. Notationally, the curly braces are omitted for |
47 intersection. Notationally, the curly braces are omitted for |
42 singleton intersections, i.e.\ any class @{text "c"} may be read as |
48 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 |
49 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> |
50 sorts according to the meaning of intersections: @{text |
45 {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> |
51 "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff |
46 d\<^isub>j"}. The empty intersection @{text "{}"} refers to the |
52 @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}. The empty intersection |
47 universal sort, which is the largest element wrt.\ the sort order. |
53 @{text "{}"} refers to the universal sort, which is the largest |
48 The intersections of all (i.e.\ finitely many) classes declared in |
54 element wrt.\ the sort order. The intersections of all (finitely |
49 the current theory are the minimal elements wrt.\ sort order. |
55 many) classes declared in the current theory are the minimal |
50 |
56 elements wrt.\ the sort order. |
51 \medskip A \emph{fixed type variable} is pair of a basic name |
57 |
|
58 \medskip A \emph{fixed type variable} is a pair of a basic name |
52 (starting with @{text "'"} character) and a sort constraint. For |
59 (starting with @{text "'"} character) and a sort constraint. For |
53 example, @{text "('a, s)"} which is usually printed as @{text |
60 example, @{text "('a, s)"} which is usually printed as @{text |
54 "\<alpha>\<^isub>s"}. A \emph{schematic type variable} is a pair of an |
61 "\<alpha>\<^isub>s"}. A \emph{schematic type variable} is a pair of an |
55 indexname and a sort constraint. For example, @{text "(('a, 0), |
62 indexname and a sort constraint. For example, @{text "(('a, 0), |
56 s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}. |
63 s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}. |
57 |
64 |
58 Note that \emph{all} syntactic components contribute to the identity |
65 Note that \emph{all} syntactic components contribute to the identity |
59 of a type variables, including the literal sort constraint. The |
66 of type variables, including the literal sort constraint. The core |
60 core logic handles type variables with the same name but different |
67 logic handles type variables with the same name but different sorts |
61 sorts as different, even though the outer layers of the system make |
68 as different, although some outer layers of the system make it hard |
62 it hard to produce anything like this. |
69 to produce anything like this. |
63 |
70 |
64 A \emph{type constructor} is an @{text "k"}-ary type operator |
71 A \emph{type constructor} is a @{text "k"}-ary operator on types |
65 declared in the theory. |
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. |
66 |
79 |
67 A \emph{type} is defined inductively over type variables and type |
80 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>, |
81 constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | |
69 \<tau>\<^sub>k)c"}. Type constructor application is usually written |
82 (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}. |
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. |
|
77 |
83 |
78 A \emph{type abbreviation} is a syntactic abbreviation of an |
84 A \emph{type abbreviation} is a syntactic abbreviation of an |
79 arbitrary type expression of the theory. Type abbreviations looks |
85 arbitrary type expression of the theory. Type abbreviations looks |
80 like type constructors at the surface, but are expanded before the |
86 like type constructors at the surface, but are expanded before the |
81 core logic encounters them. |
87 core logic encounters them. |
82 |
88 |
83 A \emph{type arity} declares the image behavior of a type |
89 A \emph{type arity} declares the image behavior of a type |
84 constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>, |
90 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 |
91 s\<^isub>k)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 |
92 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 |
93 sort @{text "s\<^isub>i"}. Arity declarations are implicitly |
88 \emph{coregular}, which means that type arities are consistent with |
94 completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c :: |
89 the subclass relation: for each type constructor @{text "c"} and |
95 (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}. |
90 classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "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 :: |
91 (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c |
101 (\<^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> |
102 :: (\<^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. |
103 \<^vec>s\<^isub>2"} holds pointwise for all argument sorts. |
94 |
104 |
95 The key property of the order-sorted algebra of types is that sort |
105 The key property of a coregular order-sorted algebra is that sort |
96 constraints may be always fulfilled in a most general fashion: for |
106 constraints may be always fulfilled in a most general fashion: for |
97 each type constructor @{text "c"} and sort @{text "s"} there is a |
107 each type constructor @{text "c"} and sort @{text "s"} there is a |
98 most general vector of argument sorts @{text "(s\<^isub>1, \<dots>, |
108 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>, |
109 s\<^isub>k)"} such that a type scheme @{text |
100 \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of |
110 "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is |
101 sort @{text "s\<^isub>i"}. This means the unification problem on |
111 of sort @{text "s"}. Consequently, the unification problem on the |
102 the algebra of types has most general solutions (modulo renaming and |
112 algebra of types has most general solutions (modulo renaming and |
103 equivalence of sorts). As a consequence, type-inference is able to |
113 equivalence of sorts). Moreover, the usual type-inference algorithm |
104 produce primary types. |
114 will produce primary types as expected \cite{nipkow-prehofer}. |
105 *} |
115 *} |
106 |
116 |
107 text %mlref {* |
117 text %mlref {* |
108 \begin{mldecls} |
118 \begin{mldecls} |
109 @{index_ML_type class} \\ |
119 @{index_ML_type class} \\ |
137 |
147 |
138 \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"} |
148 \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"}. |
149 tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}. |
140 |
150 |
141 \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type |
151 \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type |
142 expression of of a given sort. |
152 is of a given sort. |
143 |
153 |
144 \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new |
154 \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new |
145 type constructors @{text "c"} with @{text "k"} arguments, and |
155 type constructors @{text "c"} with @{text "k"} arguments and |
146 optional mixfix syntax. |
156 optional mixfix syntax. |
147 |
157 |
148 \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"} |
158 \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"} |
149 defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional |
159 defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with |
150 mixfix syntax) as @{text "\<tau>"}. |
160 optional mixfix syntax. |
151 |
161 |
152 \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>, |
162 \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>, |
153 c\<^isub>n])"} declares new class @{text "c"} derived together with |
163 c\<^isub>n])"} declares new class @{text "c"} derived together with |
154 class relations @{text "c \<subseteq> c\<^isub>i"}. |
164 class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}. |
155 |
165 |
156 \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1, |
166 \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1, |
157 c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq> |
167 c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq> |
158 c\<^isub>2"}. |
168 c\<^isub>2"}. |
159 |
169 |
256 \seeglossary{type variable}. The distinguishing feature of different |
266 \seeglossary{type variable}. The distinguishing feature of different |
257 variables is their binding scope.} |
267 variables is their binding scope.} |
258 |
268 |
259 *} |
269 *} |
260 |
270 |
261 subsection {* Primitive inferences *} |
271 |
262 |
272 section {* Proof terms *} |
263 text FIXME |
273 |
264 |
274 text {* |
265 |
275 FIXME !? |
266 subsection {* Higher-order resolution *} |
276 *} |
|
277 |
|
278 |
|
279 section {* Rules \label{sec:rules} *} |
267 |
280 |
268 text {* |
281 text {* |
269 |
282 |
270 FIXME |
283 FIXME |
|
284 |
|
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. |
271 |
318 |
272 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF |
319 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF |
273 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> |
320 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> |
274 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}. |
321 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}. |
275 Any proposition may be put into HHF form by normalizing with the rule |
322 Any proposition may be put into HHF form by normalizing with the rule |