doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Fri Sep 15 16:49:41 2006 +0200 (2006-09-15) changeset 20543 dc294418ff17 parent 20542 a54ca4e90874 child 20547 796ae7fa1049 permissions -rw-r--r--
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   Derivations are relative to a logical theory, which declares type
24   constructors, constants, and axioms.  Theory declarations support
25   schematic polymorphism, which is strictly speaking outside the
26   logic.\footnote{This is the deeper logical reason, why the theory
27   context @{text "\<Theta>"} is separate from the proof context @{text "\<Gamma>"}
28   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 "s =
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, e.g.\
60   @{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^isub>s"}.
61   A \emph{schematic type variable} is a pair of an indexname and a
62   sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually
63   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   written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.  For
74   @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}
75   instead of @{text "()prop"}.  For @{text "k = 1"} the parentheses
76   are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.
77   Further notation is provided for specific constructors, notably the
78   right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
79   \<beta>)fun"}.
81   A \emph{type} is defined inductively over type variables and type
82   constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
83   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}.
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 appear as type
88   constructors in the syntax, but are expanded before entering the
89   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 any type constructor @{text "\<kappa>"}, and classes @{text
102   "c\<^isub>1 \<subseteq> c\<^isub>2"}, and arities @{text "\<kappa> ::
103   (\<^vec>s\<^isub>1)c\<^isub>1"} and @{text "\<kappa> ::
104   (\<^vec>s\<^isub>2)c\<^isub>2"} holds @{text "\<^vec>s\<^isub>1 \<subseteq>
105   \<^vec>s\<^isub>2"} component-wise.
107   The key property of a coregular order-sorted algebra is that sort
108   constraints can be solved in a most general fashion: for each type
109   constructor @{text "\<kappa>"} and sort @{text "s"} there is a most general
110   vector of argument sorts @{text "(s\<^isub>1, \<dots>, s\<^isub>k)"} such
111   that a type scheme @{text "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
112   \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is of sort @{text "s"}.
113   Consequently, type unification has most general solutions (modulo
114   equivalence of sorts), so type-inference produces primary types as
115   expected \cite{nipkow-prehofer}.
116 *}
118 text %mlref {*
119   \begin{mldecls}
120   @{index_ML_type class} \\
121   @{index_ML_type sort} \\
122   @{index_ML_type arity} \\
123   @{index_ML_type typ} \\
124   @{index_ML map_atyps: "(typ -> typ) -> typ -> 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: "(string * int * mixfix) list -> theory -> theory"} \\
129   @{index_ML Sign.add_tyabbrs_i: "
130   (string * 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 map_atyps}~@{text "f \<tau>"} applies the mapping @{text "f"}
152   to all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text
153   "\<tau>"}.
155   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates the operation @{text
156   "f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar})
157   in @{text "\<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 type
163   @{text "\<tau>"} is of sort @{text "s"}.
165   \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a 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 a 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 the class relation @{text "c\<^isub>1 \<subseteq>
179   c\<^isub>2"}.
181   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
182   the 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}), with the types being determined determined
197   by the corresponding binders.  In contrast, free variables and
198   constants are have an explicit name and type in each occurrence.
200   \medskip A \emph{bound variable} is a natural number @{text "b"},
201   which accounts for the number of intermediate binders between the
202   variable occurrence in the body and its binding position.  For
203   example, the de-Bruijn term @{text
204   "\<lambda>\<^bsub>nat\<^esub>. \<lambda>\<^bsub>nat\<^esub>. 1 + 0"} would
205   correspond to @{text
206   "\<lambda>x\<^bsub>nat\<^esub>. \<lambda>y\<^bsub>nat\<^esub>. x + y"} in a named
207   representation.  Note that a bound variable may be represented by
208   different de-Bruijn indices at different occurrences, depending on
209   the nesting of abstractions.
211   A \emph{loose variable} is a bound variable that is outside the
212   scope of local binders.  The types (and names) for loose variables
213   can be managed as a separate context, that is maintained as a stack
214   of hypothetical binders.  The core logic operates on closed terms,
215   without any loose variables.
217   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
218   @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}.  A
219   \emph{schematic variable} is a pair of an indexname and a type,
220   e.g.\ @{text "((x, 0), \<tau>)"} which is usually printed as @{text
221   "?x\<^isub>\<tau>"}.
223   \medskip A \emph{constant} is a pair of a basic name and a type,
224   e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text
225   "c\<^isub>\<tau>"}.  Constants are declared in the context as polymorphic
226   families @{text "c :: \<sigma>"}, meaning that all substitution instances
227   @{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
229   The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"}
230   wrt.\ the declaration @{text "c :: \<sigma>"} is defined as the codomain of
231   the matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>,
232   ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in canonical order @{text
233   "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  Within a given theory context,
234   there is a one-to-one correspondence between any constant @{text
235   "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, \<dots>,
236   \<tau>\<^isub>n)"} of its type arguments.  For example, with @{text "plus
237   :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow>
238   nat\<^esub>"} corresponds to @{text "plus(nat)"}.
240   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
241   for type variables in @{text "\<sigma>"}.  These are observed by
242   type-inference as expected, but \emph{ignored} by the core logic.
243   This means the primitive logic is able to reason with instances of
244   polymorphic constants that the user-level type-checker would reject
245   due to violation of type class restrictions.
247   \medskip An \emph{atomic} term is either a variable or constant.  A
248   \emph{term} is defined inductively over atomic terms, with
249   abstraction and application as follows: @{text "t = b | x\<^isub>\<tau> |
250   ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.
251   Parsing and printing takes care of converting between an external
252   representation with named bound variables.  Subsequently, we shall
253   use the latter notation instead of internal de-Bruijn
254   representation.
256   The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a
257   term according to the structure of atomic terms, abstractions, and
258   applicatins:
259   $260 \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{} 261 \qquad 262 \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}} 263 \qquad 264 \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}} 265$
266   A \emph{well-typed term} is a term that can be typed according to these rules.
268   Typing information can be omitted: type-inference is able to
269   reconstruct the most general type of a raw term, while assigning
270   most general types to all of its variables and constants.
271   Type-inference depends on a context of type constraints for fixed
272   variables, and declarations for polymorphic constants.
274   The identity of atomic terms consists both of the name and the type
275   component.  This means that different variables @{text
276   "x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text
277   "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after type
278   instantiation.  Some outer layers of the system make it hard to
279   produce variables of the same name, but different types.  In
280   contrast, mixed instances of polymorphic constants occur frequently.
282   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
283   is the set of type variables occurring in @{text "t"}, but not in
284   @{text "\<sigma>"}.  This means that the term implicitly depends on type
285   arguments that are not accounted in the result type, i.e.\ there are
286   different type instances @{text "t\<vartheta> :: \<sigma>"} and @{text
287   "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly
288   pathological situation notoriously demands additional care.
290   \medskip A \emph{term abbreviation} is a syntactic definition @{text
291   "c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},
292   without any hidden polymorphism.  A term abbreviation looks like a
293   constant in the syntax, but is expanded before entering the logical
294   core.  Abbreviations are usually reverted when printing terms, using
295   @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higher-order rewriting.
297   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
298   "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free
299   renaming of bound variables; @{text "\<beta>"}-conversion contracts an
300   abstraction applied to an argument term, substituting the argument
301   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
302   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
303   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
304   does not occur in @{text "f"}.
306   Terms are normally treated modulo @{text "\<alpha>"}-conversion, which is
307   implicit in the de-Bruijn representation.  Names for bound variables
308   in abstractions are maintained separately as (meaningless) comments,
309   mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is
310   commonplace in various standard operations (\secref{sec:rules}) that
311   are based on higher-order unification and matching.
312 *}
314 text %mlref {*
315   \begin{mldecls}
316   @{index_ML_type term} \\
317   @{index_ML "op aconv": "term * term -> bool"} \\
318   @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\  %FIXME rename map_types
319   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
320   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
321   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
322   @{index_ML fastype_of: "term -> typ"} \\
323   @{index_ML lambda: "term -> term -> term"} \\
324   @{index_ML betapply: "term * term -> term"} \\
325   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
326   @{index_ML Sign.add_abbrevs: "string * bool ->
327   ((string * mixfix) * term) list -> theory -> theory"} \\
328   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
329   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
330   \end{mldecls}
332   \begin{description}
334   \item @{ML_type term} represents de-Bruijn terms, with comments in
335   abstractions, and explicitly named free variables and constants;
336   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
337   Var}, @{ML Const}, @{ML Abs}, @{ML "op \$"}.
339   \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
340   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
341   on type @{ML_type term}; raw datatype equality should only be used
342   for operations related to parsing or printing!
344   \item @{ML map_term_types}~@{text "f t"} applies the mapping @{text
345   "f"} to all types occurring in @{text "t"}.
347   \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
348   "f"} over all occurrences of types in @{text "t"}; the term
349   structure is traversed from left to right.
351   \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}
352   to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
353   Const}) occurring in @{text "t"}.
355   \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text
356   "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},
357   @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
358   traversed from left to right.
360   \item @{ML fastype_of}~@{text "t"} determines the type of a
361   well-typed term.  This operation is relatively slow, despite the
362   omission of any sanity checks.
364   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
365   "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the
366   body @{text "b"} are replaced by bound variables.
368   \item @{ML betapply}~@{text "(t, u)"} produces an application @{text
369   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
370   abstraction.
372   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
373   new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
375   \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}
376   declares a new term abbreviation @{text "c \<equiv> t"} with optional
377   mixfix syntax.
379   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
380   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
381   convert between two representations of polymorphic constants: full
382   type instance vs.\ compact type arguments form.
384   \end{description}
385 *}
388 section {* Theorems \label{sec:thms} *}
390 text {*
391   \glossary{Proposition}{FIXME A \seeglossary{term} of
392   \seeglossary{type} @{text "prop"}.  Internally, there is nothing
393   special about propositions apart from their type, but the concrete
394   syntax enforces a clear distinction.  Propositions are structured
395   via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
396   "\<And>x. B x"} --- anything else is considered atomic.  The canonical
397   form for propositions is that of a \seeglossary{Hereditary Harrop
398   Formula}. FIXME}
400   \glossary{Theorem}{A proven proposition within a certain theory and
401   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
402   rarely spelled out explicitly.  Theorems are usually normalized
403   according to the \seeglossary{HHF} format. FIXME}
405   \glossary{Fact}{Sometimes used interchangeably for
406   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
407   essentially an extra-logical conjunction.  Facts emerge either as
408   local assumptions, or as results of local goal statements --- both
409   may be simultaneous, hence the list representation. FIXME}
411   \glossary{Schematic variable}{FIXME}
413   \glossary{Fixed variable}{A variable that is bound within a certain
414   proof context; an arbitrary-but-fixed entity within a portion of
415   proof text. FIXME}
417   \glossary{Free variable}{Synonymous for \seeglossary{fixed
418   variable}. FIXME}
420   \glossary{Bound variable}{FIXME}
422   \glossary{Variable}{See \seeglossary{schematic variable},
423   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
424   \seeglossary{type variable}.  The distinguishing feature of
425   different variables is their binding scope. FIXME}
427   A \emph{proposition} is a well-typed term of type @{text "prop"}, a
428   \emph{theorem} is a proven proposition (depending on a context of
429   hypotheses and the background theory).  Primitive inferences include
430   plain natural deduction rules for the primary connectives @{text
431   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
432   notion of equality/equivalence @{text "\<equiv>"}.
433 *}
435 subsection {* Primitive connectives and rules *}
437 text {*
438   The theory @{text "Pure"} contains constant declarations for the
439   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
440   the logical framework, see \figref{fig:pure-connectives}.  The
441   derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
442   defined inductively by the primitive inferences given in
443   \figref{fig:prim-rules}, with the global restriction that the
444   hypotheses must \emph{not} contain any schematic variables.  The
445   builtin equality is conceptually axiomatized as shown in
446   \figref{fig:pure-equality}, although the implementation works
447   directly with derived inferences.
449   \begin{figure}[htb]
450   \begin{center}
451   \begin{tabular}{ll}
452   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
453   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
454   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
455   \end{tabular}
456   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
457   \end{center}
458   \end{figure}
460   \begin{figure}[htb]
461   \begin{center}
462   $463 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}} 464 \qquad 465 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{} 466$
467   $468 \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}} 469 \qquad 470 \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}} 471$
472   $473 \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 474 \qquad 475 \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"}} 476$
477   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
478   \end{center}
479   \end{figure}
481   \begin{figure}[htb]
482   \begin{center}
483   \begin{tabular}{ll}
484   @{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}-conversion \\
485   @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
486   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
487   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
488   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
489   \end{tabular}
490   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
491   \end{center}
492   \end{figure}
494   The introduction and elimination rules for @{text "\<And>"} and @{text
495   "\<Longrightarrow>"} are analogous to formation of dependently typed @{text
496   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
497   are irrelevant in the Pure logic, though; they cannot occur within
498   propositions.  The system provides a runtime option to record
499   explicit proof terms for primitive inferences.  Thus all three
500   levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
501   terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
502   \cite{Berghofer-Nipkow:2000:TPHOL}).
504   Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need
505   not be recorded in the hypotheses, because the simple syntactic
506   types of Pure are always inhabitable.  Assumptions'' @{text "x ::
507   \<tau>"} for type-membership are only present as long as some @{text
508   "x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key
509   difference to @{text "\<lambda>HOL"}'' in the PTS framework
510   \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are
511   treated uniformly for propositions and types.}
513   \medskip The axiomatization of a theory is implicitly closed by
514   forming all instances of type and term variables: @{text "\<turnstile>
515   A\<vartheta>"} holds for any substitution instance of an axiom
516   @{text "\<turnstile> A"}.  By pushing substitutions through derivations
517   inductively, we also get admissible @{text "generalize"} and @{text
518   "instance"} rules as shown in \figref{fig:subst-rules}.
520   \begin{figure}[htb]
521   \begin{center}
522   $523 \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}} 524 \quad 525 \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}} 526$
527   $528 \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}} 529 \quad 530 \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}} 531$
532   \caption{Admissible substitution rules}\label{fig:subst-rules}
533   \end{center}
534   \end{figure}
536   Note that @{text "instantiate"} does not require an explicit
537   side-condition, because @{text "\<Gamma>"} may never contain schematic
538   variables.
540   In principle, variables could be substituted in hypotheses as well,
541   but this would disrupt the monotonicity of reasoning: deriving
542   @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is
543   correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
544   the result belongs to a different proof context.
546   \medskip An \emph{oracle} is a function that produces axioms on the
547   fly.  Logically, this is an instance of the @{text "axiom"} rule
548   (\figref{fig:prim-rules}), but there is an operational difference.
549   The system always records oracle invocations within derivations of
550   theorems.  Tracing plain axioms (and named theorems) is optional.
552   Axiomatizations should be limited to the bare minimum, typically as
553   part of the initial logical basis of an object-logic formalization.
554   Later on, theories are usually developed in a strictly definitional
555   fashion, by stating only certain equalities over new constants.
557   A \emph{simple definition} consists of a constant declaration @{text
558   "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t
559   :: \<sigma>"} is a closed term without any hidden polymorphism.  The RHS
560   may depend on further defined constants, but not @{text "c"} itself.
561   Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>
562   t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.
564   An \emph{overloaded definition} consists of a collection of axioms
565   for the same constant, with zero or one equations @{text
566   "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for
567   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention
568   previously defined constants as above, or arbitrary constants @{text
569   "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text
570   "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by
571   primitive recursion over the syntactic structure of a single type
572   argument.
573 *}
575 text %mlref {*
576   \begin{mldecls}
577   @{index_ML_type ctyp} \\
578   @{index_ML_type cterm} \\
579   @{index_ML_type thm} \\
580   @{index_ML proofs: "int ref"} \\
581   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
582   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
583   @{index_ML Thm.assume: "cterm -> thm"} \\
584   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
585   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
586   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
587   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
588   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
589   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
590   @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
591   @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
592   @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
593   @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
594   @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
595   @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
596   \end{mldecls}
598   \begin{description}
600   \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
601   and terms, respectively.  These are abstract datatypes that
602   guarantee that its values have passed the full well-formedness (and
603   well-typedness) checks, relative to the declarations of type
604   constructors, constants etc. in the theory.
606   This representation avoids syntactic rechecking in tight loops of
607   inferences.  There are separate operations to decompose certified
608   entities (including actual theorems).
610   \item @{ML_type thm} represents proven propositions.  This is an
611   abstract datatype that guarantees that its values have been
612   constructed by basic principles of the @{ML_struct Thm} module.
613   Every @{ML thm} value contains a sliding back-reference to the
614   enclosing theory, cf.\ \secref{sec:context-theory}.
616   \item @{ML proofs} determines the detail of proof recording within
617   @{ML_type thm} values: @{ML 0} records only oracles, @{ML 1} records
618   oracles, axioms and named theorems, @{ML 2} records full proof
619   terms.
621   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
622   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
623   correspond to the primitive inferences of \figref{fig:prim-rules}.
625   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
626   corresponds to the @{text "generalize"} rules of
627   \figref{fig:subst-rules}.  Here collections of type and term
628   variables are generalized simultaneously, specified by the given
629   basic names.
631   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
632   \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
633   of \figref{fig:subst-rules}.  Type variables are substituted before
634   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
635   refer to the instantiated versions.
637   \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
638   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
640   \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a
641   named oracle function, cf.\ @{text "axiom"} in
642   \figref{fig:prim-rules}.
644   \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
645   arbitrary propositions as axioms.
647   \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle
648   function for generating arbitrary axioms on the fly.
650   \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
651   \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
652   for constant @{text "c\<^isub>\<tau>"}, relative to existing
653   specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.
655   \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c
656   \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an existing
657   constant @{text "c"}.  Dependencies are recorded (cf.\ @{ML
658   Theory.add_deps}), unless the @{text "unchecked"} option is set.
660   \end{description}
661 *}
664 subsection {* Auxiliary definitions *}
666 text {*
667   Theory @{text "Pure"} provides a few auxiliary definitions, see
668   \figref{fig:pure-aux}.  These special constants are normally not
669   exposed to the user, but appear in internal encodings.
671   \begin{figure}[htb]
672   \begin{center}
673   \begin{tabular}{ll}
674   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
675   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \$1ex] 676 @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\ 677 @{text "#A \<equiv> A"} \\[1ex] 678 @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\ 679 @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex] 680 @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\ 681 @{text "(unspecified)"} \\ 682 \end{tabular} 683 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux} 684 \end{center} 685 \end{figure} 687 Derived conjunction rules include introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A & 688 B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}. 689 Conjunction allows to treat simultaneous assumptions and conclusions 690 uniformly. For example, multiple claims are intermediately 691 represented as explicit conjunction, but this is refined into 692 separate sub-goals before the user continues the proof; the final 693 result is projected into a list of theorems (cf.\ 694 \secref{sec:tactical-goals}). 696 The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex 697 propositions appear as atomic, without changing the meaning: @{text 698 "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable. See 699 \secref{sec:tactical-goals} for specific operations. 701 The @{text "term"} marker turns any well-typed term into a derivable 702 proposition: @{text "\<turnstile> TERM t"} holds unconditionally. Although 703 this is logically vacuous, it allows to treat terms and proofs 704 uniformly, similar to a type-theoretic framework. 706 The @{text "TYPE"} constructor is the canonical representative of 707 the unspecified type @{text "\<alpha> itself"}; it essentially injects the 708 language of types into that of terms. There is specific notation 709 @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau> 710 itself\<^esub>"}. 711 Although being devoid of any particular meaning, the @{text 712 "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term 713 language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal 714 argument in primitive definitions, in order to circumvent hidden 715 polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c 716 TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of 717 a proposition @{text "A"} that depends on an additional type 718 argument, which is essentially a predicate on types. 719 *} 721 text %mlref {* 722 \begin{mldecls} 723 @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\ 724 @{index_ML Conjunction.elim: "thm -> thm * thm"} \\ 725 @{index_ML Drule.mk_term: "cterm -> thm"} \\ 726 @{index_ML Drule.dest_term: "thm -> cterm"} \\ 727 @{index_ML Logic.mk_type: "typ -> term"} \\ 728 @{index_ML Logic.dest_type: "term -> typ"} \\ 729 \end{mldecls} 731 \begin{description} 733 \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text 734 "A"} and @{text "B"}. 736 \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"} 737 from @{text "A & B"}. 739 \item @{ML Drule.mk_term} derives @{text "TERM t"}. 741 \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text 742 "TERM t"}. 744 \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text 745 "TYPE(\<tau>)"}. 747 \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type 748 @{text "\<tau>"}. 750 \end{description} 751 *} 754 section {* Rules \label{sec:rules} *} 756 text {* 758 FIXME 760 A \emph{rule} is any Pure theorem in HHF normal form; there is a 761 separate calculus for rule composition, which is modeled after 762 Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows 763 rules to be nested arbitrarily, similar to \cite{extensions91}. 765 Normally, all theorems accessible to the user are proper rules. 766 Low-level inferences are occasional required internally, but the 767 result should be always presented in canonical form. The higher 768 interfaces of Isabelle/Isar will always produce proper rules. It is 769 important to maintain this invariant in add-on applications! 771 There are two main principles of rule composition: @{text 772 "resolution"} (i.e.\ backchaining of rules) and @{text 773 "by-assumption"} (i.e.\ closing a branch); both principles are 774 combined in the variants of @{text "elim-resolution"} and @{text 775 "dest-resolution"}. Raw @{text "composition"} is occasionally 776 useful as well, also it is strictly speaking outside of the proper 777 rule calculus. 779 Rules are treated modulo general higher-order unification, which is 780 unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion 781 on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo 782 the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. 784 This means that any operations within the rule calculus may be 785 subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common 786 practice not to contract or expand unnecessarily. Some mechanisms 787 prefer an one form, others the opposite, so there is a potential 788 danger to produce some oscillation! 790 Only few operations really work \emph{modulo} HHF conversion, but 791 expect a normal form: quantifiers @{text "\<And>"} before implications 792 @{text "\<Longrightarrow>"} at each level of nesting. 794 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF 795 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> 796 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}. 797 Any proposition may be put into HHF form by normalizing with the rule 798 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost 799 quantifier prefix is represented via \seeglossary{schematic 800 variables}, such that the top-level structure is merely that of a 801 \seeglossary{Horn Clause}}. 803 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.} 806 \[ 807 \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}} 808 {@{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})}} 809$
812   $813 \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}} 814 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}} 815$
818   $819 \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"}} 820$
821   $822 \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}} 823$
825   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},
826   @{text "\<Longrightarrow>_lift"}, and @{text compose}.
828   $829 \infer[@{text "(resolution)"}] 830 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}} 831 {\begin{tabular}{l} 832 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\ 833 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\ 834 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\ 835 \end{tabular}} 836$
839   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}
840 *}
843 end