doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Tue Sep 12 14:50:11 2006 +0200 (2006-09-12) changeset 20514 5ede702cd2ca parent 20501 de0b523b0d62 child 20519 d7ad1217c24a permissions -rw-r--r--
more on terms;
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 "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.
74   For @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text
75   "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
76   parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text
77   "(\<alpha>)list"}.  Further notation is provided for specific constructors,
78   notably the right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of
79   @{text "(\<alpha>, \<beta>)fun"}.
81   A \emph{type} @{text "\<tau>"} is defined inductively over type variables
82   and type constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s |
83   ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.
85   A \emph{type abbreviation} is a syntactic definition @{text
86   "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
87   variables @{text "\<^vec>\<alpha>"}.  Type abbreviations looks like type
88   constructors at the surface, but are fully expanded before entering
89   the logical core.
91   A \emph{type arity} declares the image behavior of a type
92   constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,
93   s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is
94   of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is
95   of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
96   completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
97   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
99   \medskip The sort algebra is always maintained as \emph{coregular},
100   which means that type arities are consistent with the subclass
101   relation: for each type constructor @{text "\<kappa>"} and classes @{text
102   "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "\<kappa> ::
103   (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>
104   :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
105   \<^vec>s\<^isub>2"} holds componentwise.
107   The key property of a coregular order-sorted algebra is that sort
108   constraints may be always solved in a most general fashion: for each
109   type constructor @{text "\<kappa>"} and sort @{text "s"} there is a most
110   general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
111   s\<^isub>k)"} such that a type scheme @{text
112   "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is
113   of sort @{text "s"}.  Consequently, the unification problem on the
114   algebra of types has most general solutions (modulo renaming and
115   equivalence of sorts).  Moreover, the usual type-inference algorithm
116   will produce primary types as expected \cite{nipkow-prehofer}.
117 *}
119 text %mlref {*
120   \begin{mldecls}
121   @{index_ML_type class} \\
122   @{index_ML_type sort} \\
123   @{index_ML_type arity} \\
124   @{index_ML_type typ} \\
125   @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
126   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
127   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
128   @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
129   @{index_ML Sign.add_tyabbrs_i: "
130   (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
131   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
132   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
133   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
134   \end{mldecls}
136   \begin{description}
138   \item @{ML_type class} represents type classes; this is an alias for
139   @{ML_type string}.
141   \item @{ML_type sort} represents sorts; this is an alias for
142   @{ML_type "class list"}.
144   \item @{ML_type arity} represents type arities; this is an alias for
145   triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
146   (\<^vec>s)s"} described above.
148   \item @{ML_type typ} represents types; this is a datatype with
149   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
151   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}
152   over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text
153   "\<tau>"}; the type structure is traversed from left to right.
155   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
156   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
158   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
159   is of a given sort.
161   \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares new
162   type constructors @{text "\<kappa>"} with @{text "k"} arguments and
163   optional mixfix syntax.
165   \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
166   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
167   optional mixfix syntax.
169   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
170   c\<^isub>n])"} declares new class @{text "c"}, together with class
171   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
173   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
174   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
175   c\<^isub>2"}.
177   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
178   arity @{text "\<kappa> :: (\<^vec>s)s"}.
180   \end{description}
181 *}
185 section {* Terms \label{sec:terms} *}
187 text {*
188   \glossary{Term}{FIXME}
190   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
191   with de-Bruijn indices for bound variables, and named free variables
192   and constants.  Terms with loose bound variables are usually
193   considered malformed.  The types of variables and constants is
194   stored explicitly at each occurrence in the term.
196   \medskip A \emph{bound variable} is a natural number @{text "b"},
197   which refers to the next binder that is @{text "b"} steps upwards
198   from the occurrence of @{text "b"} (counting from zero).  Bindings
199   may be introduced as abstractions within the term, or as a separate
200   context (an inside-out list).  This associates each bound variable
201   with a type, and a name that is maintained as a comment for parsing
202   and printing.  A \emph{loose variables} is a bound variable that is
203   outside the current scope of local binders or the context.  For
204   example, the de-Bruijn term @{text "\<lambda>\<^isub>\<tau>. \<lambda>\<^isub>\<tau>. 1 + 0"}
205   corresponds to @{text "\<lambda>x\<^isub>\<tau>. \<lambda>y\<^isub>\<tau>. x + y"} in a named
206   representation.  Also note that the very same bound variable may get
207   different numbers at different occurrences.
209   A \emph{fixed variable} is a pair of a basic name and a type.  For
210   example, @{text "(x, \<tau>)"} which is usually printed @{text
211   "x\<^isub>\<tau>"}.  A \emph{schematic variable} is a pair of an
212   indexname and a type.  For example, @{text "((x, 0), \<tau>)"} which is
213   usually printed as @{text "?x\<^isub>\<tau>"}.
215   \medskip A \emph{constant} is a atomic terms consisting of a basic
216   name and a type.  Constants are declared in the context as
217   polymorphic families @{text "c :: \<sigma>"}, meaning that any @{text
218   "c\<^isub>\<tau>"} is a valid constant for all substitution instances
219   @{text "\<tau> \<le> \<sigma>"}.
221   The list of \emph{type arguments} of @{text "c\<^isub>\<tau>"} wrt.\ the
222   declaration @{text "c :: \<sigma>"} is the codomain of the type matcher
223   presented in canonical order (according to the left-to-right
224   occurrences of type variables in in @{text "\<sigma>"}).  Thus @{text
225   "c\<^isub>\<tau>"} can be represented more compactly as @{text
226   "c(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  For example, the instance @{text
227   "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} of some @{text "plus :: \<alpha> \<Rightarrow> \<alpha>
228   \<Rightarrow> \<alpha>"} has the singleton list @{text "nat"} as type arguments, the
229   constant may be represented as @{text "plus(nat)"}.
231   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
232   for type variables in @{text "\<sigma>"}.  These are observed by
233   type-inference as expected, but \emph{ignored} by the core logic.
234   This means the primitive logic is able to reason with instances of
235   polymorphic constants that the user-level type-checker would reject.
237   \medskip A \emph{term} @{text "t"} is defined inductively over
238   variables and constants, with abstraction and application as
239   follows: @{text "t = b | x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> |
240   \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes
241   care of converting between an external representation with named
242   bound variables.  Subsequently, we shall use the latter notation
243   instead of internal de-Bruijn representation.
245   The subsequent inductive relation @{text "t :: \<tau>"} assigns a
246   (unique) type to a term, using the special type constructor @{text
247   "(\<alpha>, \<beta>)fun"}, which is written @{text "\<alpha> \<Rightarrow> \<beta>"}.
248   $249 \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{} 250 \qquad 251 \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}} 252 \qquad 253 \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}} 254$
255   A \emph{well-typed term} is a term that can be typed according to these rules.
257   Typing information can be omitted: type-inference is able to
258   reconstruct the most general type of a raw term, while assigning
259   most general types to all of its variables and constants.
260   Type-inference depends on a context of type constraints for fixed
261   variables, and declarations for polymorphic constants.
263   The identity of atomic terms consists both of the name and the type.
264   Thus different entities @{text "c\<^bsub>\<tau>\<^isub>1\<^esub>"} and
265   @{text "c\<^bsub>\<tau>\<^isub>2\<^esub>"} may well identified by type
266   instantiation, by mapping @{text "\<tau>\<^isub>1"} and @{text
267   "\<tau>\<^isub>2"} to the same @{text "\<tau>"}.  Although,
268   different type instances of constants of the same basic name are
269   commonplace, this rarely happens for variables: type-inference
270   always demands consistent'' type constraints.
272   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
273   is the set of type variables occurring in @{text "t"}, but not in
274   @{text "\<sigma>"}.  This means that the term implicitly depends on the
275   values of various type variables that are not visible in the overall
276   type, i.e.\ there are different type instances @{text "t\<vartheta>
277   :: \<sigma>"} and @{text "t\<vartheta>' :: \<sigma>"} with the same type.  This
278   slightly pathological situation is apt to cause strange effects.
280   \medskip A \emph{term abbreviation} is a syntactic definition @{text
281   "c\<^isub>\<sigma> \<equiv> t"} of an arbitrary closed term @{text "t"} of type
282   @{text "\<sigma>"} without any hidden polymorphism.  A term abbreviation
283   looks like a constant at the surface, but is fully expanded before
284   entering the logical core.  Abbreviations are usually reverted when
285   printing terms, using rules @{text "t \<rightarrow> c\<^isub>\<sigma>"} has a
286   higher-order term rewrite system.
287 *}
289 text %mlref {*
290   \begin{mldecls}
291   @{index_ML_type term} \\
292   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
293   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
294   @{index_ML fastype_of: "term -> typ"} \\
295   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
296   \end{mldecls}
298   \begin{description}
300   \item @{ML_type term} FIXME
302   \end{description}
303 *}
306 section {* Theorems \label{sec:thms} *}
308 text {*
309   \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
310   @{text "prop"}.  Internally, there is nothing special about
311   propositions apart from their type, but the concrete syntax enforces
312   a clear distinction.  Propositions are structured via implication
313   @{text "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} ---
314   anything else is considered atomic.  The canonical form for
315   propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}
317   \glossary{Theorem}{A proven proposition within a certain theory and
318   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
319   rarely spelled out explicitly.  Theorems are usually normalized
320   according to the \seeglossary{HHF} format. FIXME}
322   \glossary{Fact}{Sometimes used interchangably for
323   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
324   essentially an extra-logical conjunction.  Facts emerge either as
325   local assumptions, or as results of local goal statements --- both
326   may be simultaneous, hence the list representation. FIXME}
328   \glossary{Schematic variable}{FIXME}
330   \glossary{Fixed variable}{A variable that is bound within a certain
331   proof context; an arbitrary-but-fixed entity within a portion of
332   proof text. FIXME}
334   \glossary{Free variable}{Synonymous for \seeglossary{fixed
335   variable}. FIXME}
337   \glossary{Bound variable}{FIXME}
339   \glossary{Variable}{See \seeglossary{schematic variable},
340   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
341   \seeglossary{type variable}.  The distinguishing feature of
342   different variables is their binding scope. FIXME}
344   A \emph{proposition} is a well-formed term of type @{text "prop"}.
345   The connectives of minimal logic are declared as constants of the
346   basic theory:
348   \smallskip
349   \begin{tabular}{ll}
350   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
351   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
352   \end{tabular}
354   \medskip A \emph{theorem} is a proven proposition, depending on a
355   collection of assumptions, and axioms from the theory context.  The
356   judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is defined
357   inductively by the primitive inferences given in
358   \figref{fig:prim-rules}; there is a global syntactic restriction
359   that the hypotheses may not contain schematic variables.
361   \begin{figure}[htb]
362   \begin{center}
363   $364 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}} 365 \qquad 366 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{} 367$
368   $369 \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}{@{text "\<Gamma> \<turnstile> b x"} & @{text "x \<notin> \<Gamma>"}} 370 \qquad 371 \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b a"}}{@{text "\<Gamma> \<turnstile> \<And>x. b x"}} 372$
373   $374 \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 375 \qquad 376 \infer[@{text "(\<Longrightarrow>_elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}} 377$
378   \caption{Primitive inferences of the Pure logic}\label{fig:prim-rules}
379   \end{center}
380   \end{figure}
382   The introduction and elimination rules for @{text "\<And>"} and @{text
383   "\<Longrightarrow>"} are analogous to formation of (dependently typed) @{text
384   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
385   are \emph{irrelevant} in the Pure logic, they may never occur within
386   propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow of the framework is a
387   non-dependent one.
389   Also note that fixed parameters as in @{text "\<And>_intro"} need not be
390   recorded in the context @{text "\<Gamma>"}, since syntactic types are
391   always inhabitable.  An assumption'' @{text "x :: \<tau>"} is logically
392   vacuous, because @{text "\<tau>"} is always non-empty.  This is the deeper
393   reason why @{text "\<Gamma>"} only consists of hypothetical proofs, but no
394   hypothetical terms.
396   The corresponding proof terms are left implicit in the classic
397   LCF-approach'', although they could be exploited separately
398   \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime
399   option to control the generation of full proof terms.
401   \medskip The axiomatization of a theory is implicitly closed by
402   forming all instances of type and term variables: @{text "\<turnstile> A\<theta>"} for
403   any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing
404   substitution through derivations inductively, we get admissible
405   substitution rules for theorems shown in \figref{fig:subst-rules}.
407   \begin{figure}[htb]
408   \begin{center}
409   $410 \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}} 411 \quad 412 \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}} 413$
414   $415 \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}} 416 \quad 417 \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}} 418$
419   \caption{Admissible substitution rules}\label{fig:subst-rules}
420   \end{center}
421   \end{figure}
423   Note that @{text "instantiate_term"} could be derived using @{text
424   "\<And>_intro/elim"}, but this is not how it is implemented.  The type
425   instantiation rule is a genuine admissible one, due to the lack of
426   true polymorphism in the logic.
428   Since @{text "\<Gamma>"} may never contain any schematic variables, the
429   @{text "instantiate"} do not require an explicit side-condition.  In
430   principle, variables could be substituted in hypotheses as well, but
431   this could disrupt monotonicity of the basic calculus: derivations
432   could leave the current proof context.
434   \medskip The framework also provides builtin equality @{text "\<equiv>"},
435   which is conceptually axiomatized shown in \figref{fig:equality},
436   although the implementation provides derived rules directly:
438   \begin{figure}[htb]
439   \begin{center}
440   \begin{tabular}{ll}
441   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
442   @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
443   @{text "\<turnstile> x \<equiv> x"} & reflexivity law \\
444   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution law \\
445   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
446   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
447   \end{tabular}
448   \caption{Conceptual axiomatization of equality.}\label{fig:equality}
449   \end{center}
450   \end{figure}
452   Since the basic representation of terms already accounts for @{text
453   "\<alpha>"}-conversion, Pure equality essentially acts like @{text
454   "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
457   \medskip Conjunction is defined in Pure as a derived connective, see
458   \figref{fig:conjunction}.  This is occasionally useful to represent
459   simultaneous statements behind the scenes --- framework conjunction
460   is usually not exposed to the user.
462   \begin{figure}[htb]
463   \begin{center}
464   \begin{tabular}{ll}
465   @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} & conjunction (hidden) \\
466   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\
467   \end{tabular}
468   \caption{Definition of conjunction.}\label{fig:equality}
469   \end{center}
470   \end{figure}
472   The definition allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow>
473   B \<Longrightarrow> A & B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B
474   \<Longrightarrow> B"}.
475 *}
478 section {* Rules \label{sec:rules} *}
480 text {*
482 FIXME
484   A \emph{rule} is any Pure theorem in HHF normal form; there is a
485   separate calculus for rule composition, which is modeled after
486   Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
487   rules to be nested arbitrarily, similar to \cite{extensions91}.
489   Normally, all theorems accessible to the user are proper rules.
490   Low-level inferences are occasional required internally, but the
491   result should be always presented in canonical form.  The higher
492   interfaces of Isabelle/Isar will always produce proper rules.  It is
493   important to maintain this invariant in add-on applications!
495   There are two main principles of rule composition: @{text
496   "resolution"} (i.e.\ backchaining of rules) and @{text
497   "by-assumption"} (i.e.\ closing a branch); both principles are
498   combined in the variants of @{text "elim-resosultion"} and @{text
499   "dest-resolution"}.  Raw @{text "composition"} is occasionally
500   useful as well, also it is strictly speaking outside of the proper
501   rule calculus.
503   Rules are treated modulo general higher-order unification, which is
504   unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
505   on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo
506   the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
508   This means that any operations within the rule calculus may be
509   subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common
510   practice not to contract or expand unnecessarily.  Some mechanisms
511   prefer an one form, others the opposite, so there is a potential
512   danger to produce some oscillation!
514   Only few operations really work \emph{modulo} HHF conversion, but
515   expect a normal form: quantifiers @{text "\<And>"} before implications
516   @{text "\<Longrightarrow>"} at each level of nesting.
518 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
519 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
520 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
521 Any proposition may be put into HHF form by normalizing with the rule
522 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
523 quantifier prefix is represented via \seeglossary{schematic
524 variables}, such that the top-level structure is merely that of a
525 \seeglossary{Horn Clause}}.
527 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
530   $531 \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}} 532 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}} 533$
536   $537 \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}} 538 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}} 539$
542   $543 \infer[@{text "(\<And>_lift)"}]{@{text "(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"}} 544$
545   $546 \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}} 547$
549   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},
550   @{text "\<Longrightarrow>_lift"}, and @{text compose}.
552   $553 \infer[@{text "(resolution)"}] 554 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}} 555 {\begin{tabular}{l} 556 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\ 557 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\ 558 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\ 559 \end{tabular}} 560$
563   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}
564 *}
567 end