26 \begin{isamarkuptext}% |
26 \begin{isamarkuptext}% |
27 The logical foundations of Isabelle/Isar are that of the Pure logic, |
27 The logical foundations of Isabelle/Isar are that of the Pure logic, |
28 which has been introduced as a natural-deduction framework in |
28 which has been introduced as a natural-deduction framework in |
29 \cite{paulson700}. This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract framework of Pure Type Systems (PTS) |
29 \cite{paulson700}. This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract framework of Pure Type Systems (PTS) |
30 \cite{Barendregt-Geuvers:2001}, although there are some key |
30 \cite{Barendregt-Geuvers:2001}, although there are some key |
31 differences in the practical treatment of simple types. |
31 differences in the specific treatment of simple types in |
|
32 Isabelle/Pure. |
32 |
33 |
33 Following type-theoretic parlance, the Pure logic consists of three |
34 Following type-theoretic parlance, the Pure logic consists of three |
34 levels of \isa{{\isasymlambda}}-calculus with corresponding arrows: \isa{{\isasymRightarrow}} for syntactic function space (terms depending on terms), \isa{{\isasymAnd}} for universal quantification (proofs depending on terms), and |
35 levels of \isa{{\isasymlambda}}-calculus with corresponding arrows: \isa{{\isasymRightarrow}} for syntactic function space (terms depending on terms), \isa{{\isasymAnd}} for universal quantification (proofs depending on terms), and |
35 \isa{{\isasymLongrightarrow}} for implication (proofs depending on proofs). |
36 \isa{{\isasymLongrightarrow}} for implication (proofs depending on proofs). |
36 |
37 |
37 Pure derivations are relative to a logical theory, which declares |
38 Pure derivations are relative to a logical theory, which declares |
38 type constructors, term constants, and axioms. Term constants and |
39 type constructors, term constants, and axioms. Theory declarations |
39 axioms support schematic polymorphism.% |
40 support schematic polymorphism, which is strictly speaking outside |
|
41 the logic.\footnote{Incidently, this is the main logical reason, why |
|
42 the theory context \isa{{\isasymTheta}} is separate from the context \isa{{\isasymGamma}} of the core calculus.}% |
40 \end{isamarkuptext}% |
43 \end{isamarkuptext}% |
41 \isamarkuptrue% |
44 \isamarkuptrue% |
42 % |
45 % |
43 \isamarkupsection{Types \label{sec:types}% |
46 \isamarkupsection{Types \label{sec:types}% |
44 } |
47 } |
48 The language of types is an uninterpreted order-sorted first-order |
51 The language of types is an uninterpreted order-sorted first-order |
49 algebra; types are qualified by ordered type classes. |
52 algebra; types are qualified by ordered type classes. |
50 |
53 |
51 \medskip A \emph{type class} is an abstract syntactic entity |
54 \medskip A \emph{type class} is an abstract syntactic entity |
52 declared in the theory context. The \emph{subclass relation} \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}} is specified by stating an acyclic |
55 declared in the theory context. The \emph{subclass relation} \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}} is specified by stating an acyclic |
53 generating relation; the transitive closure maintained internally. |
56 generating relation; the transitive closure is maintained |
|
57 internally. The resulting relation is an ordering: reflexive, |
|
58 transitive, and antisymmetric. |
54 |
59 |
55 A \emph{sort} is a list of type classes written as \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, which represents symbolic |
60 A \emph{sort} is a list of type classes written as \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, which represents symbolic |
56 intersection. Notationally, the curly braces are omitted for |
61 intersection. Notationally, the curly braces are omitted for |
57 singleton intersections, i.e.\ any class \isa{c} may be read as |
62 singleton intersections, i.e.\ any class \isa{c} may be read as |
58 a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}. The ordering on type classes is extended to |
63 a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}. The ordering on type classes is extended to |
59 sorts in the canonical fashion: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the |
64 sorts according to the meaning of intersections: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff |
60 universal sort, which is the largest element wrt.\ the sort order. |
65 \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection |
61 The intersections of all (i.e.\ finitely many) classes declared in |
66 \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the universal sort, which is the largest |
62 the current theory are the minimal elements wrt.\ sort order. |
67 element wrt.\ the sort order. The intersections of all (finitely |
63 |
68 many) classes declared in the current theory are the minimal |
64 \medskip A \emph{fixed type variable} is pair of a basic name |
69 elements wrt.\ the sort order. |
|
70 |
|
71 \medskip A \emph{fixed type variable} is a pair of a basic name |
65 (starting with \isa{{\isacharprime}} character) and a sort constraint. For |
72 (starting with \isa{{\isacharprime}} character) and a sort constraint. For |
66 example, \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}. A \emph{schematic type variable} is a pair of an |
73 example, \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}. A \emph{schematic type variable} is a pair of an |
67 indexname and a sort constraint. For example, \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually printed \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}. |
74 indexname and a sort constraint. For example, \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}. |
68 |
75 |
69 Note that \emph{all} syntactic components contribute to the identity |
76 Note that \emph{all} syntactic components contribute to the identity |
70 of a type variables, including the literal sort constraint. The |
77 of type variables, including the literal sort constraint. The core |
71 core logic handles type variables with the same name but different |
78 logic handles type variables with the same name but different sorts |
72 sorts as different, even though the outer layers of the system make |
79 as different, although some outer layers of the system make it hard |
73 it hard to produce anything like this. |
80 to produce anything like this. |
74 |
81 |
75 A \emph{type constructor} is an \isa{k}-ary type operator |
82 A \emph{type constructor} is a \isa{k}-ary operator on types |
76 declared in the theory. |
83 declared in the theory. Type constructor application is usually |
|
84 written postfix. For \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, |
|
85 e.g.\ \isa{prop} instead of \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of |
|
86 \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}. Further notation is provided for specific |
|
87 constructors, notably right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} |
|
88 instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun} constructor. |
77 |
89 |
78 A \emph{type} is defined inductively over type variables and type |
90 A \emph{type} is defined inductively over type variables and type |
79 constructors: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}. Type constructor application is usually written |
91 constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}. |
80 postfix. For \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ |
|
81 \isa{prop} instead of \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the |
|
82 parentheses are omitted, e.g.\ \isa{{\isasymtau}\ list} instead of \isa{{\isacharparenleft}{\isasymtau}{\isacharparenright}\ list}. Further notation is provided for specific |
|
83 constructors, notably right-associative infix \isa{{\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymtau}\isactrlisub {\isadigit{2}}} instead of \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymtau}\isactrlisub {\isadigit{2}}{\isacharparenright}fun} |
|
84 constructor. |
|
85 |
92 |
86 A \emph{type abbreviation} is a syntactic abbreviation of an |
93 A \emph{type abbreviation} is a syntactic abbreviation of an |
87 arbitrary type expression of the theory. Type abbreviations looks |
94 arbitrary type expression of the theory. Type abbreviations looks |
88 like type constructors at the surface, but are expanded before the |
95 like type constructors at the surface, but are expanded before the |
89 core logic encounters them. |
96 core logic encounters them. |
90 |
97 |
91 A \emph{type arity} declares the image behavior of a type |
98 A \emph{type arity} declares the image behavior of a type |
92 constructor wrt.\ the algebra of sorts: \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub n{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}c} is |
99 constructor wrt.\ the algebra of sorts: \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}c} is |
93 of sort \isa{s} if each argument type \isa{{\isasymtau}\isactrlisub i} is of |
100 of sort \isa{s} if each argument type \isa{{\isasymtau}\isactrlisub i} is of |
94 sort \isa{s\isactrlisub i}. The sort algebra is always maintained as |
101 sort \isa{s\isactrlisub i}. Arity declarations are implicitly |
95 \emph{coregular}, which means that type arities are consistent with |
102 completed, i.e.\ \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c} entails \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}} for any \isa{c{\isacharprime}\ {\isasymsupseteq}\ c}. |
96 the subclass relation: for each type constructor \isa{c} and |
103 |
97 classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds pointwise for all argument sorts. |
104 \medskip The sort algebra is always maintained as \emph{coregular}, |
98 |
105 which means that type arities are consistent with the subclass |
99 The key property of the order-sorted algebra of types is that sort |
106 relation: for each type constructor \isa{c} and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds pointwise for all argument sorts. |
|
107 |
|
108 The key property of a coregular order-sorted algebra is that sort |
100 constraints may be always fulfilled in a most general fashion: for |
109 constraints may be always fulfilled in a most general fashion: for |
101 each type constructor \isa{c} and sort \isa{s} there is a |
110 each type constructor \isa{c} and sort \isa{s} there is a |
102 most general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such that \isa{{\isacharparenleft}{\isasymtau}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}} for arbitrary \isa{{\isasymtau}\isactrlisub i} of |
111 most general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such that a type scheme \isa{{\isacharparenleft}{\isasymalpha}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}c} is |
103 sort \isa{s\isactrlisub i}. This means the unification problem on |
112 of sort \isa{s}. Consequently, the unification problem on the |
104 the algebra of types has most general solutions (modulo renaming and |
113 algebra of types has most general solutions (modulo renaming and |
105 equivalence of sorts). As a consequence, type-inference is able to |
114 equivalence of sorts). Moreover, the usual type-inference algorithm |
106 produce primary types.% |
115 will produce primary types as expected \cite{nipkow-prehofer}.% |
107 \end{isamarkuptext}% |
116 \end{isamarkuptext}% |
108 \isamarkuptrue% |
117 \isamarkuptrue% |
109 % |
118 % |
110 \isadelimmlref |
119 \isadelimmlref |
111 % |
120 % |
145 |
154 |
146 \item \verb|Sign.subsort|~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}} |
155 \item \verb|Sign.subsort|~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}} |
147 tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}. |
156 tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}. |
148 |
157 |
149 \item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether a type |
158 \item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether a type |
150 expression of of a given sort. |
159 is of a given sort. |
151 |
160 |
152 \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares new |
161 \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares new |
153 type constructors \isa{c} with \isa{k} arguments, and |
162 type constructors \isa{c} with \isa{k} arguments and |
154 optional mixfix syntax. |
163 optional mixfix syntax. |
155 |
164 |
156 \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} |
165 \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} |
157 defines type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}c} (with optional |
166 defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}c\ {\isacharequal}\ {\isasymtau}} with |
158 mixfix syntax) as \isa{{\isasymtau}}. |
167 optional mixfix syntax. |
159 |
168 |
160 \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares new class \isa{c} derived together with |
169 \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares new class \isa{c} derived together with |
161 class relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}. |
170 class relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}. |
162 |
171 |
163 \item \verb|Sign.primitive_classrel|~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}. |
172 \item \verb|Sign.primitive_classrel|~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}. |
164 |
173 |
165 \item \verb|Sign.primitive_arity|~\isa{{\isacharparenleft}c{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares |
174 \item \verb|Sign.primitive_arity|~\isa{{\isacharparenleft}c{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares |
166 arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}. |
175 arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}. |
265 \seeglossary{type variable}. The distinguishing feature of different |
272 \seeglossary{type variable}. The distinguishing feature of different |
266 variables is their binding scope.}% |
273 variables is their binding scope.}% |
267 \end{isamarkuptext}% |
274 \end{isamarkuptext}% |
268 \isamarkuptrue% |
275 \isamarkuptrue% |
269 % |
276 % |
270 \isamarkupsubsection{Primitive inferences% |
277 \isamarkupsection{Proof terms% |
271 } |
278 } |
272 \isamarkuptrue% |
279 \isamarkuptrue% |
273 % |
280 % |
274 \begin{isamarkuptext}% |
281 \begin{isamarkuptext}% |
275 FIXME% |
282 FIXME !?% |
276 \end{isamarkuptext}% |
283 \end{isamarkuptext}% |
277 \isamarkuptrue% |
284 \isamarkuptrue% |
278 % |
285 % |
279 \isamarkupsubsection{Higher-order resolution% |
286 \isamarkupsection{Rules \label{sec:rules}% |
280 } |
287 } |
281 \isamarkuptrue% |
288 \isamarkuptrue% |
282 % |
289 % |
283 \begin{isamarkuptext}% |
290 \begin{isamarkuptext}% |
284 FIXME |
291 FIXME |
|
292 |
|
293 A \emph{rule} is any Pure theorem in HHF normal form; there is a |
|
294 separate calculus for rule composition, which is modeled after |
|
295 Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows |
|
296 rules to be nested arbitrarily, similar to \cite{extensions91}. |
|
297 |
|
298 Normally, all theorems accessible to the user are proper rules. |
|
299 Low-level inferences are occasional required internally, but the |
|
300 result should be always presented in canonical form. The higher |
|
301 interfaces of Isabelle/Isar will always produce proper rules. It is |
|
302 important to maintain this invariant in add-on applications! |
|
303 |
|
304 There are two main principles of rule composition: \isa{resolution} (i.e.\ backchaining of rules) and \isa{by{\isacharminus}assumption} (i.e.\ closing a branch); both principles are |
|
305 combined in the variants of \isa{elim{\isacharminus}resosultion} and \isa{dest{\isacharminus}resolution}. Raw \isa{composition} is occasionally |
|
306 useful as well, also it is strictly speaking outside of the proper |
|
307 rule calculus. |
|
308 |
|
309 Rules are treated modulo general higher-order unification, which is |
|
310 unification modulo the equational theory of \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion |
|
311 on \isa{{\isasymlambda}}-terms. Moreover, propositions are understood modulo |
|
312 the (derived) equivalence \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}. |
|
313 |
|
314 This means that any operations within the rule calculus may be |
|
315 subject to spontaneous \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-HHF conversions. It is common |
|
316 practice not to contract or expand unnecessarily. Some mechanisms |
|
317 prefer an one form, others the opposite, so there is a potential |
|
318 danger to produce some oscillation! |
|
319 |
|
320 Only few operations really work \emph{modulo} HHF conversion, but |
|
321 expect a normal form: quantifiers \isa{{\isasymAnd}} before implications |
|
322 \isa{{\isasymLongrightarrow}} at each level of nesting. |
285 |
323 |
286 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF |
324 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF |
287 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}. |
325 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}. |
288 Any proposition may be put into HHF form by normalizing with the rule |
326 Any proposition may be put into HHF form by normalizing with the rule |
289 \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 |
327 \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 |