doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Thu Oct 04 13:26:34 2007 +0200 (2007-10-04) changeset 24828 137c242e7277 parent 22322 b9924abb8c66 child 24972 acafb18a47dc permissions -rw-r--r--
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   \end{mldecls}
127   \begin{mldecls}
128   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
129   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
130   @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
131   @{index_ML Sign.add_tyabbrs_i: "
132   (string * string list * typ * mixfix) list -> theory -> theory"} \\
133   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
134   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
135   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
136   \end{mldecls}
138   \begin{description}
140   \item @{ML_type class} represents type classes; this is an alias for
141   @{ML_type string}.
143   \item @{ML_type sort} represents sorts; this is an alias for
144   @{ML_type "class list"}.
146   \item @{ML_type arity} represents type arities; this is an alias for
147   triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
148   (\<^vec>s)s"} described above.
150   \item @{ML_type typ} represents types; this is a datatype with
151   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
153   \item @{ML map_atyps}~@{text "f \<tau>"} applies the mapping @{text "f"}
154   to all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text
155   "\<tau>"}.
157   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates the operation @{text
158   "f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar})
159   in @{text "\<tau>"}; the type structure is traversed from left to right.
161   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
162   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
164   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
165   @{text "\<tau>"} is of sort @{text "s"}.
167   \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a new
168   type constructors @{text "\<kappa>"} with @{text "k"} arguments and
169   optional mixfix syntax.
171   \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
172   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
173   optional mixfix syntax.
175   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
176   c\<^isub>n])"} declares a new class @{text "c"}, together with class
177   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
179   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
180   c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \<subseteq>
181   c\<^isub>2"}.
183   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
184   the arity @{text "\<kappa> :: (\<^vec>s)s"}.
186   \end{description}
187 *}
191 section {* Terms \label{sec:terms} *}
193 text {*
194   \glossary{Term}{FIXME}
196   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
197   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
198   or \cite{paulson-ml2}), with the types being determined determined
199   by the corresponding binders.  In contrast, free variables and
200   constants are have an explicit name and type in each occurrence.
202   \medskip A \emph{bound variable} is a natural number @{text "b"},
203   which accounts for the number of intermediate binders between the
204   variable occurrence in the body and its binding position.  For
205   example, the de-Bruijn term @{text
206   "\<lambda>\<^bsub>nat\<^esub>. \<lambda>\<^bsub>nat\<^esub>. 1 + 0"} would
207   correspond to @{text
208   "\<lambda>x\<^bsub>nat\<^esub>. \<lambda>y\<^bsub>nat\<^esub>. x + y"} in a named
209   representation.  Note that a bound variable may be represented by
210   different de-Bruijn indices at different occurrences, depending on
211   the nesting of abstractions.
213   A \emph{loose variable} is a bound variable that is outside the
214   scope of local binders.  The types (and names) for loose variables
215   can be managed as a separate context, that is maintained as a stack
216   of hypothetical binders.  The core logic operates on closed terms,
217   without any loose variables.
219   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
220   @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}.  A
221   \emph{schematic variable} is a pair of an indexname and a type,
222   e.g.\ @{text "((x, 0), \<tau>)"} which is usually printed as @{text
223   "?x\<^isub>\<tau>"}.
225   \medskip A \emph{constant} is a pair of a basic name and a type,
226   e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text
227   "c\<^isub>\<tau>"}.  Constants are declared in the context as polymorphic
228   families @{text "c :: \<sigma>"}, meaning that all substitution instances
229   @{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
231   The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"}
232   wrt.\ the declaration @{text "c :: \<sigma>"} is defined as the codomain of
233   the matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>,
234   ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in canonical order @{text
235   "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  Within a given theory context,
236   there is a one-to-one correspondence between any constant @{text
237   "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, \<dots>,
238   \<tau>\<^isub>n)"} of its type arguments.  For example, with @{text "plus
239   :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow>
240   nat\<^esub>"} corresponds to @{text "plus(nat)"}.
242   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
243   for type variables in @{text "\<sigma>"}.  These are observed by
244   type-inference as expected, but \emph{ignored} by the core logic.
245   This means the primitive logic is able to reason with instances of
246   polymorphic constants that the user-level type-checker would reject
247   due to violation of type class restrictions.
249   \medskip An \emph{atomic} term is either a variable or constant.  A
250   \emph{term} is defined inductively over atomic terms, with
251   abstraction and application as follows: @{text "t = b | x\<^isub>\<tau> |
252   ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.
253   Parsing and printing takes care of converting between an external
254   representation with named bound variables.  Subsequently, we shall
255   use the latter notation instead of internal de-Bruijn
256   representation.
258   The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a
259   term according to the structure of atomic terms, abstractions, and
260   applicatins:
261   $262 \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{} 263 \qquad 264 \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}} 265 \qquad 266 \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}} 267$
268   A \emph{well-typed term} is a term that can be typed according to these rules.
270   Typing information can be omitted: type-inference is able to
271   reconstruct the most general type of a raw term, while assigning
272   most general types to all of its variables and constants.
273   Type-inference depends on a context of type constraints for fixed
274   variables, and declarations for polymorphic constants.
276   The identity of atomic terms consists both of the name and the type
277   component.  This means that different variables @{text
278   "x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text
279   "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after type
280   instantiation.  Some outer layers of the system make it hard to
281   produce variables of the same name, but different types.  In
282   contrast, mixed instances of polymorphic constants occur frequently.
284   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
285   is the set of type variables occurring in @{text "t"}, but not in
286   @{text "\<sigma>"}.  This means that the term implicitly depends on type
287   arguments that are not accounted in the result type, i.e.\ there are
288   different type instances @{text "t\<vartheta> :: \<sigma>"} and @{text
289   "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly
290   pathological situation notoriously demands additional care.
292   \medskip A \emph{term abbreviation} is a syntactic definition @{text
293   "c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},
294   without any hidden polymorphism.  A term abbreviation looks like a
295   constant in the syntax, but is expanded before entering the logical
296   core.  Abbreviations are usually reverted when printing terms, using
297   @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higher-order rewriting.
299   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
300   "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free
301   renaming of bound variables; @{text "\<beta>"}-conversion contracts an
302   abstraction applied to an argument term, substituting the argument
303   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
304   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
305   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
306   does not occur in @{text "f"}.
308   Terms are normally treated modulo @{text "\<alpha>"}-conversion, which is
309   implicit in the de-Bruijn representation.  Names for bound variables
310   in abstractions are maintained separately as (meaningless) comments,
311   mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is
312   commonplace in various standard operations (\secref{sec:rules}) that
313   are based on higher-order unification and matching.
314 *}
316 text %mlref {*
317   \begin{mldecls}
318   @{index_ML_type term} \\
319   @{index_ML "op aconv": "term * term -> bool"} \\
320   @{index_ML map_types: "(typ -> typ) -> term -> term"} \\
321   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
322   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
323   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
324   \end{mldecls}
325   \begin{mldecls}
326   @{index_ML fastype_of: "term -> typ"} \\
327   @{index_ML lambda: "term -> term -> term"} \\
328   @{index_ML betapply: "term * term -> term"} \\
329   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
330   @{index_ML Sign.add_abbrev: "string -> Markup.property list -> bstring * term -> theory -> (term * term) * theory"} \\
331   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
332   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
333   \end{mldecls}
335   \begin{description}
337   \item @{ML_type term} represents de-Bruijn terms, with comments in
338   abstractions, and explicitly named free variables and constants;
339   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
340   Var}, @{ML Const}, @{ML Abs}, @{ML "op \$"}.
342   \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
343   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
344   on type @{ML_type term}; raw datatype equality should only be used
345   for operations related to parsing or printing!
347   \item @{ML map_types}~@{text "f t"} applies the mapping @{text
348   "f"} to all types occurring in @{text "t"}.
350   \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
351   "f"} over all occurrences of types in @{text "t"}; the term
352   structure is traversed from left to right.
354   \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}
355   to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
356   Const}) occurring in @{text "t"}.
358   \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text
359   "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},
360   @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
361   traversed from left to right.
363   \item @{ML fastype_of}~@{text "t"} determines the type of a
364   well-typed term.  This operation is relatively slow, despite the
365   omission of any sanity checks.
367   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
368   "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the
369   body @{text "b"} are replaced by bound variables.
371   \item @{ML betapply}~@{text "(t, u)"} produces an application @{text
372   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
373   abstraction.
375   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
376   new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
378   \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
379   introduces a new term abbreviation @{text "c \<equiv> t"}.
381   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
382   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
383   convert between two representations of polymorphic constants: full
384   type instance vs.\ compact type arguments form.
386   \end{description}
387 *}
390 section {* Theorems \label{sec:thms} *}
392 text {*
393   \glossary{Proposition}{FIXME A \seeglossary{term} of
394   \seeglossary{type} @{text "prop"}.  Internally, there is nothing
395   special about propositions apart from their type, but the concrete
396   syntax enforces a clear distinction.  Propositions are structured
397   via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
398   "\<And>x. B x"} --- anything else is considered atomic.  The canonical
399   form for propositions is that of a \seeglossary{Hereditary Harrop
400   Formula}. FIXME}
402   \glossary{Theorem}{A proven proposition within a certain theory and
403   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
404   rarely spelled out explicitly.  Theorems are usually normalized
405   according to the \seeglossary{HHF} format. FIXME}
407   \glossary{Fact}{Sometimes used interchangeably for
408   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
409   essentially an extra-logical conjunction.  Facts emerge either as
410   local assumptions, or as results of local goal statements --- both
411   may be simultaneous, hence the list representation. FIXME}
413   \glossary{Schematic variable}{FIXME}
415   \glossary{Fixed variable}{A variable that is bound within a certain
416   proof context; an arbitrary-but-fixed entity within a portion of
417   proof text. FIXME}
419   \glossary{Free variable}{Synonymous for \seeglossary{fixed
420   variable}. FIXME}
422   \glossary{Bound variable}{FIXME}
424   \glossary{Variable}{See \seeglossary{schematic variable},
425   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
426   \seeglossary{type variable}.  The distinguishing feature of
427   different variables is their binding scope. FIXME}
429   A \emph{proposition} is a well-typed term of type @{text "prop"}, a
430   \emph{theorem} is a proven proposition (depending on a context of
431   hypotheses and the background theory).  Primitive inferences include
432   plain natural deduction rules for the primary connectives @{text
433   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
434   notion of equality/equivalence @{text "\<equiv>"}.
435 *}
437 subsection {* Primitive connectives and rules \label{sec:prim_rules} *}
439 text {*
440   The theory @{text "Pure"} contains constant declarations for the
441   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
442   the logical framework, see \figref{fig:pure-connectives}.  The
443   derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
444   defined inductively by the primitive inferences given in
445   \figref{fig:prim-rules}, with the global restriction that the
446   hypotheses must \emph{not} contain any schematic variables.  The
447   builtin equality is conceptually axiomatized as shown in
448   \figref{fig:pure-equality}, although the implementation works
449   directly with derived inferences.
451   \begin{figure}[htb]
452   \begin{center}
453   \begin{tabular}{ll}
454   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
455   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
456   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
457   \end{tabular}
458   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
459   \end{center}
460   \end{figure}
462   \begin{figure}[htb]
463   \begin{center}
464   $465 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}} 466 \qquad 467 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{} 468$
469   $470 \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}} 471 \qquad 472 \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}} 473$
474   $475 \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 476 \qquad 477 \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"}} 478$
479   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
480   \end{center}
481   \end{figure}
483   \begin{figure}[htb]
484   \begin{center}
485   \begin{tabular}{ll}
486   @{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}-conversion \\
487   @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
488   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
489   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
490   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
491   \end{tabular}
492   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
493   \end{center}
494   \end{figure}
496   The introduction and elimination rules for @{text "\<And>"} and @{text
497   "\<Longrightarrow>"} are analogous to formation of dependently typed @{text
498   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
499   are irrelevant in the Pure logic, though; they cannot occur within
500   propositions.  The system provides a runtime option to record
501   explicit proof terms for primitive inferences.  Thus all three
502   levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
503   terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
504   \cite{Berghofer-Nipkow:2000:TPHOL}).
506   Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need
507   not be recorded in the hypotheses, because the simple syntactic
508   types of Pure are always inhabitable.  Assumptions'' @{text "x ::
509   \<tau>"} for type-membership are only present as long as some @{text
510   "x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key
511   difference to @{text "\<lambda>HOL"}'' in the PTS framework
512   \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are
513   treated uniformly for propositions and types.}
515   \medskip The axiomatization of a theory is implicitly closed by
516   forming all instances of type and term variables: @{text "\<turnstile>
517   A\<vartheta>"} holds for any substitution instance of an axiom
518   @{text "\<turnstile> A"}.  By pushing substitutions through derivations
519   inductively, we also get admissible @{text "generalize"} and @{text
520   "instance"} rules as shown in \figref{fig:subst-rules}.
522   \begin{figure}[htb]
523   \begin{center}
524   $525 \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}} 526 \quad 527 \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}} 528$
529   $530 \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}} 531 \quad 532 \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}} 533$
534   \caption{Admissible substitution rules}\label{fig:subst-rules}
535   \end{center}
536   \end{figure}
538   Note that @{text "instantiate"} does not require an explicit
539   side-condition, because @{text "\<Gamma>"} may never contain schematic
540   variables.
542   In principle, variables could be substituted in hypotheses as well,
543   but this would disrupt the monotonicity of reasoning: deriving
544   @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is
545   correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
546   the result belongs to a different proof context.
548   \medskip An \emph{oracle} is a function that produces axioms on the
549   fly.  Logically, this is an instance of the @{text "axiom"} rule
550   (\figref{fig:prim-rules}), but there is an operational difference.
551   The system always records oracle invocations within derivations of
552   theorems.  Tracing plain axioms (and named theorems) is optional.
554   Axiomatizations should be limited to the bare minimum, typically as
555   part of the initial logical basis of an object-logic formalization.
556   Later on, theories are usually developed in a strictly definitional
557   fashion, by stating only certain equalities over new constants.
559   A \emph{simple definition} consists of a constant declaration @{text
560   "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t
561   :: \<sigma>"} is a closed term without any hidden polymorphism.  The RHS
562   may depend on further defined constants, but not @{text "c"} itself.
563   Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>
564   t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.
566   An \emph{overloaded definition} consists of a collection of axioms
567   for the same constant, with zero or one equations @{text
568   "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for
569   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention
570   previously defined constants as above, or arbitrary constants @{text
571   "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text
572   "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by
573   primitive recursion over the syntactic structure of a single type
574   argument.
575 *}
577 text %mlref {*
578   \begin{mldecls}
579   @{index_ML_type ctyp} \\
580   @{index_ML_type cterm} \\
581   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
582   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
583   \end{mldecls}
584   \begin{mldecls}
585   @{index_ML_type thm} \\
586   @{index_ML proofs: "int ref"} \\
587   @{index_ML Thm.assume: "cterm -> thm"} \\
588   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
589   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
590   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
591   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
592   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
593   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
594   @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
595   @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
596   \end{mldecls}
597   \begin{mldecls}
598   @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
599   @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
600   @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
601   @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
602   \end{mldecls}
604   \begin{description}
606   \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
607   and terms, respectively.  These are abstract datatypes that
608   guarantee that its values have passed the full well-formedness (and
609   well-typedness) checks, relative to the declarations of type
610   constructors, constants etc. in the theory.
612   \item @{ML ctyp_of}~@{text "thy \<tau>"} and @{ML cterm_of}~@{text "thy
613   t"} explicitly checks types and terms, respectively.  This also
614   involves some basic normalizations, such expansion of type and term
615   abbreviations from the theory context.
617   Re-certification is relatively slow and should be avoided in tight
618   reasoning loops.  There are separate operations to decompose
619   certified entities (including actual theorems).
621   \item @{ML_type thm} represents proven propositions.  This is an
622   abstract datatype that guarantees that its values have been
623   constructed by basic principles of the @{ML_struct Thm} module.
624   Every @{ML thm} value contains a sliding back-reference to the
625   enclosing theory, cf.\ \secref{sec:context-theory}.
627   \item @{ML proofs} determines the detail of proof recording within
628   @{ML_type thm} values: @{ML 0} records only oracles, @{ML 1} records
629   oracles, axioms and named theorems, @{ML 2} records full proof
630   terms.
632   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
633   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
634   correspond to the primitive inferences of \figref{fig:prim-rules}.
636   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
637   corresponds to the @{text "generalize"} rules of
638   \figref{fig:subst-rules}.  Here collections of type and term
639   variables are generalized simultaneously, specified by the given
640   basic names.
642   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
643   \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
644   of \figref{fig:subst-rules}.  Type variables are substituted before
645   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
646   refer to the instantiated versions.
648   \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
649   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
651   \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a
652   named oracle function, cf.\ @{text "axiom"} in
653   \figref{fig:prim-rules}.
655   \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
656   arbitrary propositions as axioms.
658   \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle
659   function for generating arbitrary axioms on the fly.
661   \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
662   \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
663   for constant @{text "c\<^isub>\<tau>"}, relative to existing
664   specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.
666   \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c
667   \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an existing
668   constant @{text "c"}.  Dependencies are recorded (cf.\ @{ML
669   Theory.add_deps}), unless the @{text "unchecked"} option is set.
671   \end{description}
672 *}
675 subsection {* Auxiliary definitions *}
677 text {*
678   Theory @{text "Pure"} provides a few auxiliary definitions, see
679   \figref{fig:pure-aux}.  These special constants are normally not
680   exposed to the user, but appear in internal encodings.
682   \begin{figure}[htb]
683   \begin{center}
684   \begin{tabular}{ll}
685   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
686   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \$1ex] 687 @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\ 688 @{text "#A \<equiv> A"} \\[1ex] 689 @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\ 690 @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex] 691 @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\ 692 @{text "(unspecified)"} \\ 693 \end{tabular} 694 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux} 695 \end{center} 696 \end{figure} 698 Derived conjunction rules include introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A & 699 B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}. 700 Conjunction allows to treat simultaneous assumptions and conclusions 701 uniformly. For example, multiple claims are intermediately 702 represented as explicit conjunction, but this is refined into 703 separate sub-goals before the user continues the proof; the final 704 result is projected into a list of theorems (cf.\ 705 \secref{sec:tactical-goals}). 707 The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex 708 propositions appear as atomic, without changing the meaning: @{text 709 "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable. See 710 \secref{sec:tactical-goals} for specific operations. 712 The @{text "term"} marker turns any well-typed term into a derivable 713 proposition: @{text "\<turnstile> TERM t"} holds unconditionally. Although 714 this is logically vacuous, it allows to treat terms and proofs 715 uniformly, similar to a type-theoretic framework. 717 The @{text "TYPE"} constructor is the canonical representative of 718 the unspecified type @{text "\<alpha> itself"}; it essentially injects the 719 language of types into that of terms. There is specific notation 720 @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau> 721 itself\<^esub>"}. 722 Although being devoid of any particular meaning, the @{text 723 "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term 724 language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal 725 argument in primitive definitions, in order to circumvent hidden 726 polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c 727 TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of 728 a proposition @{text "A"} that depends on an additional type 729 argument, which is essentially a predicate on types. 730 *} 732 text %mlref {* 733 \begin{mldecls} 734 @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\ 735 @{index_ML Conjunction.elim: "thm -> thm * thm"} \\ 736 @{index_ML Drule.mk_term: "cterm -> thm"} \\ 737 @{index_ML Drule.dest_term: "thm -> cterm"} \\ 738 @{index_ML Logic.mk_type: "typ -> term"} \\ 739 @{index_ML Logic.dest_type: "term -> typ"} \\ 740 \end{mldecls} 742 \begin{description} 744 \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text 745 "A"} and @{text "B"}. 747 \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"} 748 from @{text "A & B"}. 750 \item @{ML Drule.mk_term} derives @{text "TERM t"}. 752 \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text 753 "TERM t"}. 755 \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text 756 "TYPE(\<tau>)"}. 758 \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type 759 @{text "\<tau>"}. 761 \end{description} 762 *} 765 section {* Rules \label{sec:rules} *} 767 text %FIXME {* 769 FIXME 771 A \emph{rule} is any Pure theorem in HHF normal form; there is a 772 separate calculus for rule composition, which is modeled after 773 Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows 774 rules to be nested arbitrarily, similar to \cite{extensions91}. 776 Normally, all theorems accessible to the user are proper rules. 777 Low-level inferences are occasional required internally, but the 778 result should be always presented in canonical form. The higher 779 interfaces of Isabelle/Isar will always produce proper rules. It is 780 important to maintain this invariant in add-on applications! 782 There are two main principles of rule composition: @{text 783 "resolution"} (i.e.\ backchaining of rules) and @{text 784 "by-assumption"} (i.e.\ closing a branch); both principles are 785 combined in the variants of @{text "elim-resolution"} and @{text 786 "dest-resolution"}. Raw @{text "composition"} is occasionally 787 useful as well, also it is strictly speaking outside of the proper 788 rule calculus. 790 Rules are treated modulo general higher-order unification, which is 791 unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion 792 on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo 793 the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. 795 This means that any operations within the rule calculus may be 796 subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common 797 practice not to contract or expand unnecessarily. Some mechanisms 798 prefer an one form, others the opposite, so there is a potential 799 danger to produce some oscillation! 801 Only few operations really work \emph{modulo} HHF conversion, but 802 expect a normal form: quantifiers @{text "\<And>"} before implications 803 @{text "\<Longrightarrow>"} at each level of nesting. 805 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF 806 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> 807 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}. 808 Any proposition may be put into HHF form by normalizing with the rule 809 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost 810 quantifier prefix is represented via \seeglossary{schematic 811 variables}, such that the top-level structure is merely that of a 812 \seeglossary{Horn Clause}}. 814 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.} 817 \[ 818 \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}} 819 {@{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})}} 820$
823   $824 \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}} 825 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}} 826$
829   $830 \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"}} 831$
832   $833 \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}} 834$
836   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},
837   @{text "\<Longrightarrow>_lift"}, and @{text compose}.
839   $840 \infer[@{text "(resolution)"}] 841 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}} 842 {\begin{tabular}{l} 843 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\ 844 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\ 845 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\ 846 \end{tabular}} 847$
850   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}
851 *}
854 end