doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Tue Sep 12 21:05:39 2006 +0200 (2006-09-12) changeset 20521 189811b39869 parent 20520 05fd007bdeb9 child 20537 b6b49903db7e permissions -rw-r--r--
more on theorems;
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 component-wise.
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 map_atyps: "(typ -> typ) -> typ -> typ"} \\
126   @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
127   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
128   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
129   @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
130   @{index_ML Sign.add_tyabbrs_i: "
131   (string * string list * typ * mixfix) list -> theory -> theory"} \\
132   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
133   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
134   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
135   \end{mldecls}
137   \begin{description}
139   \item @{ML_type class} represents type classes; this is an alias for
140   @{ML_type string}.
142   \item @{ML_type sort} represents sorts; this is an alias for
143   @{ML_type "class list"}.
145   \item @{ML_type arity} represents type arities; this is an alias for
146   triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
147   (\<^vec>s)s"} described above.
149   \item @{ML_type typ} represents types; this is a datatype with
150   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
152   \item @{ML map_atyps}~@{text "f \<tau>"} applies mapping @{text "f"} to
153   all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text "\<tau>"}.
155   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates operation @{text "f"}
156   over all occurrences of atoms (@{ML TFree}, @{ML TVar}) in @{text
157   "\<tau>"}; the type structure is traversed from left to right.
159   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
160   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
162   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
163   is of a given sort.
165   \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares new
166   type constructors @{text "\<kappa>"} with @{text "k"} arguments and
167   optional mixfix syntax.
169   \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
170   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
171   optional mixfix syntax.
173   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
174   c\<^isub>n])"} declares new class @{text "c"}, together with class
175   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
177   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
178   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
179   c\<^isub>2"}.
181   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
182   arity @{text "\<kappa> :: (\<^vec>s)s"}.
184   \end{description}
185 *}
189 section {* Terms \label{sec:terms} *}
191 text {*
192   \glossary{Term}{FIXME}
194   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
195   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
196   or \cite{paulson-ml2}), and named free variables and constants.
197   Terms with loose bound variables are usually considered malformed.
198   The types of variables and constants is stored explicitly at each
199   occurrence in the term.
201   \medskip A \emph{bound variable} is a natural number @{text "b"},
202   which refers to the next binder that is @{text "b"} steps upwards
203   from the occurrence of @{text "b"} (counting from zero).  Bindings
204   may be introduced as abstractions within the term, or as a separate
205   context (an inside-out list).  This associates each bound variable
206   with a type.  A \emph{loose variables} is a bound variable that is
207   outside the current scope of local binders or the context.  For
208   example, the de-Bruijn term @{text "\<lambda>\<^isub>\<tau>. \<lambda>\<^isub>\<tau>. 1 + 0"}
209   corresponds to @{text "\<lambda>x\<^isub>\<tau>. \<lambda>y\<^isub>\<tau>. x + y"} in a named
210   representation.  Also note that the very same bound variable may get
211   different numbers at different occurrences.
213   A \emph{fixed variable} is a pair of a basic name and a type.  For
214   example, @{text "(x, \<tau>)"} which is usually printed @{text
215   "x\<^isub>\<tau>"}.  A \emph{schematic variable} is a pair of an
216   indexname and a type.  For example, @{text "((x, 0), \<tau>)"} which is
217   usually printed as @{text "?x\<^isub>\<tau>"}.
219   \medskip A \emph{constant} is a atomic terms consisting of a basic
220   name and a type.  Constants are declared in the context as
221   polymorphic families @{text "c :: \<sigma>"}, meaning that any @{text
222   "c\<^isub>\<tau>"} is a valid constant for all substitution instances
223   @{text "\<tau> \<le> \<sigma>"}.
225   The list of \emph{type arguments} of @{text "c\<^isub>\<tau>"} wrt.\ the
226   declaration @{text "c :: \<sigma>"} is the codomain of the type matcher
227   presented in canonical order (according to the left-to-right
228   occurrences of type variables in in @{text "\<sigma>"}).  Thus @{text
229   "c\<^isub>\<tau>"} can be represented more compactly as @{text
230   "c(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  For example, the instance @{text
231   "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} of some @{text "plus :: \<alpha> \<Rightarrow> \<alpha>
232   \<Rightarrow> \<alpha>"} has the singleton list @{text "nat"} as type arguments, the
233   constant may be represented as @{text "plus(nat)"}.
235   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
236   for type variables in @{text "\<sigma>"}.  These are observed by
237   type-inference as expected, but \emph{ignored} by the core logic.
238   This means the primitive logic is able to reason with instances of
239   polymorphic constants that the user-level type-checker would reject.
241   \medskip A \emph{term} @{text "t"} is defined inductively over
242   variables and constants, with abstraction and application as
243   follows: @{text "t = b | x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> |
244   \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes
245   care of converting between an external representation with named
246   bound variables.  Subsequently, we shall use the latter notation
247   instead of internal de-Bruijn representation.
249   The subsequent inductive relation @{text "t :: \<tau>"} assigns a
250   (unique) type to a term, using the special type constructor @{text
251   "(\<alpha>, \<beta>)fun"}, which is written @{text "\<alpha> \<Rightarrow> \<beta>"}.
252   $253 \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{} 254 \qquad 255 \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}} 256 \qquad 257 \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}} 258$
259   A \emph{well-typed term} is a term that can be typed according to these rules.
261   Typing information can be omitted: type-inference is able to
262   reconstruct the most general type of a raw term, while assigning
263   most general types to all of its variables and constants.
264   Type-inference depends on a context of type constraints for fixed
265   variables, and declarations for polymorphic constants.
267   The identity of atomic terms consists both of the name and the type.
268   Thus different entities @{text "c\<^bsub>\<tau>\<^isub>1\<^esub>"} and
269   @{text "c\<^bsub>\<tau>\<^isub>2\<^esub>"} may well identified by type
270   instantiation, by mapping @{text "\<tau>\<^isub>1"} and @{text
271   "\<tau>\<^isub>2"} to the same @{text "\<tau>"}.  Although,
272   different type instances of constants of the same basic name are
273   commonplace, this rarely happens for variables: type-inference
274   always demands consistent'' type constraints.
276   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
277   is the set of type variables occurring in @{text "t"}, but not in
278   @{text "\<sigma>"}.  This means that the term implicitly depends on the
279   values of various type variables that are not visible in the overall
280   type, i.e.\ there are different type instances @{text "t\<vartheta>
281   :: \<sigma>"} and @{text "t\<vartheta>' :: \<sigma>"} with the same type.  This
282   slightly pathological situation is apt to cause strange effects.
284   \medskip A \emph{term abbreviation} is a syntactic definition @{text
285   "c\<^isub>\<sigma> \<equiv> t"} of an arbitrary closed term @{text "t"} of type
286   @{text "\<sigma>"} without any hidden polymorphism.  A term abbreviation
287   looks like a constant at the surface, but is fully expanded before
288   entering the logical core.  Abbreviations are usually reverted when
289   printing terms, using rules @{text "t \<rightarrow> c\<^isub>\<sigma>"} has a
290   higher-order term rewrite system.
292   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
293   "\<alpha>\<beta>\<eta>"}-conversion. @{text "\<alpha>"}-conversion refers to capture-free
294   renaming of bound variables; @{text "\<beta>"}-conversion contracts an
295   abstraction applied to some argument term, substituting the argument
296   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
297   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
298   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
299   @{text "0"} does not occur in @{text "f"}.
301   Terms are almost always treated module @{text "\<alpha>"}-conversion, which
302   is implicit in the de-Bruijn representation.  The names in
303   abstractions of bound variables are maintained only as a comment for
304   parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-equivalence is usually
305   taken for granted higher rules (\secref{sec:rules}), anything
306   depending on higher-order unification or rewriting.
307 *}
309 text %mlref {*
310   \begin{mldecls}
311   @{index_ML_type term} \\
312   @{index_ML "op aconv": "term * term -> bool"} \\
313   @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\  %FIXME rename map_types
314   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
315   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
316   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
317   @{index_ML fastype_of: "term -> typ"} \\
318   @{index_ML lambda: "term -> term -> term"} \\
319   @{index_ML betapply: "term * term -> term"} \\
320   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
321   @{index_ML Sign.add_abbrevs: "string * bool ->
322   ((string * mixfix) * term) list -> theory -> theory"} \\
323   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
324   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
325   \end{mldecls}
327   \begin{description}
329   \item @{ML_type term} represents de-Bruijn terms with comments in
330   abstractions for bound variable names.  This is a datatype with
331   constructors @{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}, @{ML
332   Abs}, @{ML "op \$"}.
334   \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
335   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
336   on type @{ML_type term}; raw datatype equality should only be used
337   for operations related to parsing or printing!
339   \item @{ML map_term_types}~@{text "f t"} applies mapping @{text "f"}
340   to all types occurring in @{text "t"}.
342   \item @{ML fold_types}~@{text "f t"} iterates operation @{text "f"}
343   over all occurrences of types in @{text "t"}; the term structure is
344   traversed from left to right.
346   \item @{ML map_aterms}~@{text "f t"} applies mapping @{text "f"} to
347   all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const})
348   occurring in @{text "t"}.
350   \item @{ML fold_aterms}~@{text "f t"} iterates operation @{text "f"}
351   over all occurrences of atomic terms in (@{ML Bound}, @{ML Free},
352   @{ML Var}, @{ML Const}) @{text "t"}; the term structure is traversed
353   from left to right.
355   \item @{ML fastype_of}~@{text "t"} recomputes the type of a
356   well-formed term, while omitting any sanity checks.  This operation
357   is relatively slow.
359   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
360   "\<lambda>a. b"}, where occurrences of the original (atomic) term @{text
361   "a"} in the body @{text "b"} are replaced by bound variables.
363   \item @{ML betapply}~@{text "t u"} produces an application @{text "t
364   u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} happens to
365   be an abstraction.
367   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
368   new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
370   \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}
371   declares a new term abbreviation @{text "c \<equiv> t"} with optional
372   mixfix syntax.
374   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
375   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
376   convert between the two representations of constants, namely full
377   type instance vs.\ compact type arguments form (depending on the
378   most general declaration given in the context).
380   \end{description}
381 *}
384 section {* Theorems \label{sec:thms} *}
386 text {*
387   \glossary{Proposition}{FIXME A \seeglossary{term} of
388   \seeglossary{type} @{text "prop"}.  Internally, there is nothing
389   special about propositions apart from their type, but the concrete
390   syntax enforces a clear distinction.  Propositions are structured
391   via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
392   "\<And>x. B x"} --- anything else is considered atomic.  The canonical
393   form for propositions is that of a \seeglossary{Hereditary Harrop
394   Formula}. FIXME}
396   \glossary{Theorem}{A proven proposition within a certain theory and
397   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
398   rarely spelled out explicitly.  Theorems are usually normalized
399   according to the \seeglossary{HHF} format. FIXME}
401   \glossary{Fact}{Sometimes used interchangeably for
402   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
403   essentially an extra-logical conjunction.  Facts emerge either as
404   local assumptions, or as results of local goal statements --- both
405   may be simultaneous, hence the list representation. FIXME}
407   \glossary{Schematic variable}{FIXME}
409   \glossary{Fixed variable}{A variable that is bound within a certain
410   proof context; an arbitrary-but-fixed entity within a portion of
411   proof text. FIXME}
413   \glossary{Free variable}{Synonymous for \seeglossary{fixed
414   variable}. FIXME}
416   \glossary{Bound variable}{FIXME}
418   \glossary{Variable}{See \seeglossary{schematic variable},
419   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
420   \seeglossary{type variable}.  The distinguishing feature of
421   different variables is their binding scope. FIXME}
423   A \emph{proposition} is a well-formed term of type @{text "prop"}, a
424   \emph{theorem} is a proven proposition (depending on a context of
425   hypotheses and the background theory).  Primitive inferences include
426   plain natural deduction rules for the primary connectives @{text
427   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There are separate (derived)
428   rules for equality/equivalence @{text "\<equiv>"} and internal conjunction
429   @{text "&"}.
430 *}
432 subsection {* Standard connectives and rules *}
434 text {*
435   The basic theory is called @{text "Pure"}, it contains declarations
436   for the standard logical connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and
437   @{text "\<equiv>"} of the framework, see \figref{fig:pure-connectives}.
438   The derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
439   defined inductively by the primitive inferences given in
440   \figref{fig:prim-rules}, with the global syntactic restriction that
441   hypotheses may never contain schematic variables.  The builtin
442   equality is conceptually axiomatized shown in
443   \figref{fig:pure-equality}, although the implementation works
444   directly with (derived) inference rules.
446   \begin{figure}[htb]
447   \begin{center}
448   \begin{tabular}{ll}
449   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
450   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
451   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
452   \end{tabular}
453   \caption{Standard connectives of Pure}\label{fig:pure-connectives}
454   \end{center}
455   \end{figure}
457   \begin{figure}[htb]
458   \begin{center}
459   $460 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}} 461 \qquad 462 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{} 463$
464   $465 \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}{@{text "\<Gamma> \<turnstile> b x"} & @{text "x \<notin> \<Gamma>"}} 466 \qquad 467 \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b a"}}{@{text "\<Gamma> \<turnstile> \<And>x. b x"}} 468$
469   $470 \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 471 \qquad 472 \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"}} 473$
474   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
475   \end{center}
476   \end{figure}
478   \begin{figure}[htb]
479   \begin{center}
480   \begin{tabular}{ll}
481   @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
482   @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
483   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
484   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
485   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
486   \end{tabular}
487   \caption{Conceptual axiomatization of builtin equality}\label{fig:pure-equality}
488   \end{center}
489   \end{figure}
491   The introduction and elimination rules for @{text "\<And>"} and @{text
492   "\<Longrightarrow>"} are analogous to formation of (dependently typed) @{text
493   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
494   are \emph{irrelevant} in the Pure logic, they may never occur within
495   propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow is non-dependent.  The
496   system provides a runtime option to record explicit proof terms for
497   primitive inferences, cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}.  Thus
498   the three-fold @{text "\<lambda>"}-structure can be made explicit.
500   Observe that locally fixed parameters (as used in rule @{text
501   "\<And>_intro"}) need not be recorded in the hypotheses, because the
502   simple syntactic types of Pure are always inhabitable.  The typing
503   assumption'' @{text "x :: \<tau>"} is logically vacuous, it disappears
504   automatically whenever the statement body ceases to mention variable
505   @{text "x\<^isub>\<tau>"}.\footnote{This greatly simplifies many basic
506   reasoning steps, and is the key difference to the formulation of
507   this logic as @{text "\<lambda>HOL"}'' in the PTS framework
508   \cite{Barendregt-Geuvers:2001}.}
510   \medskip FIXME @{text "\<alpha>\<beta>\<eta>"}-equivalence and primitive definitions
512   Since the basic representation of terms already accounts for @{text
513   "\<alpha>"}-conversion, Pure equality essentially acts like @{text
514   "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
516   \medskip The axiomatization of a theory is implicitly closed by
517   forming all instances of type and term variables: @{text "\<turnstile> A\<vartheta>"} for
518   any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing
519   substitution through derivations inductively, we get admissible
520   substitution rules for theorems shown in \figref{fig:subst-rules}.
521   Alternatively, the term substitution rules could be derived from
522   @{text "\<And>_intro/elim"}.  The versions for types are genuine
523   admissible rules, due to the lack of true polymorphism in the logic.
525   \begin{figure}[htb]
526   \begin{center}
527   $528 \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}} 529 \quad 530 \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}} 531$
532   $533 \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}} 534 \quad 535 \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}} 536$
537   \caption{Admissible substitution rules}\label{fig:subst-rules}
538   \end{center}
539   \end{figure}
541   Since @{text "\<Gamma>"} may never contain any schematic variables, the
542   @{text "instantiate"} do not require an explicit side-condition.  In
543   principle, variables could be substituted in hypotheses as well, but
544   this could disrupt monotonicity of the basic calculus: derivations
545   could leave the current proof context.
546 *}
548 text %mlref {*
549   \begin{mldecls}
550   @{index_ML_type ctyp} \\
551   @{index_ML_type cterm} \\
552   @{index_ML_type thm} \\
553   \end{mldecls}
555   \begin{description}
557   \item @{ML_type ctyp} FIXME
559   \item @{ML_type cterm} FIXME
561   \item @{ML_type thm} FIXME
563   \end{description}
564 *}
567 subsection {* Auxiliary connectives *}
569 text {*
570   Pure also provides various auxiliary connectives based on primitive
571   definitions, see \figref{fig:pure-aux}.  These are normally not
572   exposed to the user, but appear in internal encodings only.
574   \begin{figure}[htb]
575   \begin{center}
576   \begin{tabular}{ll}
577   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
578   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \$1ex] 579 @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}) \\ 580 @{text "#A \<equiv> A"} \\[1ex] 581 @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\ 582 @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex] 583 @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\ 584 @{text "(unspecified)"} \\ 585 \end{tabular} 586 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux} 587 \end{center} 588 \end{figure} 590 Conjunction as an explicit connective allows to treat both 591 simultaneous assumptions and conclusions uniformly. The definition 592 allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow> B \<Longrightarrow> A & B"}, 593 and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}. For 594 example, several claims may be stated at the same time, which is 595 intermediately represented as an assumption, but the user only 596 encounters several sub-goals, and several resulting facts in the 597 very end (cf.\ \secref{sec:tactical-goals}). 599 The @{text "#"} marker allows complex propositions (nested @{text 600 "\<And>"} and @{text "\<Longrightarrow>"}) to appear formally as atomic, without changing 601 the meaning: @{text "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are 602 interchangeable. See \secref{sec:tactical-goals} for specific 603 operations. 605 The @{text "TERM"} marker turns any well-formed term into a 606 derivable proposition: @{text "\<turnstile> TERM t"} holds 607 unconditionally. Despite its logically vacous meaning, this is 608 occasionally useful to treat syntactic terms and proven propositions 609 uniformly, as in a type-theoretic framework. 611 The @{text "TYPE"} constructor (which is the canonical 612 representative of the unspecified type @{text "\<alpha> itself"}) injects 613 the language of types into that of terms. There is specific 614 notation @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau> 615 itself\<^esub>"}. 616 Although being devoid of any particular meaning, the term @{text 617 "TYPE(\<tau>)"} is able to carry the type @{text "\<tau>"} formally. @{text 618 "TYPE(\<alpha>)"} may be used as an additional formal argument in primitive 619 definitions, in order to avoid hidden polymorphism (cf.\ 620 \secref{sec:terms}). For example, @{text "c TYPE(\<alpha>) \<equiv> A[\<alpha>]"} turns 621 out as a formally correct definition of some proposition @{text "A"} 622 that depends on an additional type argument. 623 *} 625 text %mlref {* 626 \begin{mldecls} 627 @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\ 628 @{index_ML Conjunction.elim: "thm -> thm * thm"} \\ 629 @{index_ML Drule.mk_term: "cterm -> thm"} \\ 630 @{index_ML Drule.dest_term: "thm -> cterm"} \\ 631 @{index_ML Logic.mk_type: "typ -> term"} \\ 632 @{index_ML Logic.dest_type: "term -> typ"} \\ 633 \end{mldecls} 635 \begin{description} 637 \item FIXME 639 \end{description} 640 *} 643 section {* Rules \label{sec:rules} *} 645 text {* 647 FIXME 649 A \emph{rule} is any Pure theorem in HHF normal form; there is a 650 separate calculus for rule composition, which is modeled after 651 Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows 652 rules to be nested arbitrarily, similar to \cite{extensions91}. 654 Normally, all theorems accessible to the user are proper rules. 655 Low-level inferences are occasional required internally, but the 656 result should be always presented in canonical form. The higher 657 interfaces of Isabelle/Isar will always produce proper rules. It is 658 important to maintain this invariant in add-on applications! 660 There are two main principles of rule composition: @{text 661 "resolution"} (i.e.\ backchaining of rules) and @{text 662 "by-assumption"} (i.e.\ closing a branch); both principles are 663 combined in the variants of @{text "elim-resolution"} and @{text 664 "dest-resolution"}. Raw @{text "composition"} is occasionally 665 useful as well, also it is strictly speaking outside of the proper 666 rule calculus. 668 Rules are treated modulo general higher-order unification, which is 669 unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion 670 on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo 671 the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. 673 This means that any operations within the rule calculus may be 674 subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common 675 practice not to contract or expand unnecessarily. Some mechanisms 676 prefer an one form, others the opposite, so there is a potential 677 danger to produce some oscillation! 679 Only few operations really work \emph{modulo} HHF conversion, but 680 expect a normal form: quantifiers @{text "\<And>"} before implications 681 @{text "\<Longrightarrow>"} at each level of nesting. 683 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF 684 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> 685 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}. 686 Any proposition may be put into HHF form by normalizing with the rule 687 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost 688 quantifier prefix is represented via \seeglossary{schematic 689 variables}, such that the top-level structure is merely that of a 690 \seeglossary{Horn Clause}}. 692 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.} 695 \[ 696 \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}} 697 {@{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})}} 698$
701   $702 \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}} 703 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}} 704$
707   $708 \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"}} 709$
710   $711 \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}} 712$
714   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},
715   @{text "\<Longrightarrow>_lift"}, and @{text compose}.
717   $718 \infer[@{text "(resolution)"}] 719 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}} 720 {\begin{tabular}{l} 721 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\ 722 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\ 723 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\ 724 \end{tabular}} 725$
728   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}
729 *}
732 end