doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Thu Oct 11 16:38:42 2007 +0200 (2007-10-11) changeset 24972 acafb18a47dc parent 24828 137c242e7277 child 26872 336dfd860744 permissions -rw-r--r--
replaced Sign.add_consts_i by Sign.declare_const;
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.declare_const: "Markup.property list -> bstring * typ * mixfix ->
330   theory -> term * theory"} \\
331   @{index_ML Sign.add_abbrev: "string -> Markup.property list -> bstring * term ->
332   theory -> (term * term) * theory"} \\
333   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
334   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
335   \end{mldecls}
337   \begin{description}
339   \item @{ML_type term} represents de-Bruijn terms, with comments in
340   abstractions, and explicitly named free variables and constants;
341   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
342   Var}, @{ML Const}, @{ML Abs}, @{ML "op \$"}.
344   \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
345   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
346   on type @{ML_type term}; raw datatype equality should only be used
347   for operations related to parsing or printing!
349   \item @{ML map_types}~@{text "f t"} applies the mapping @{text
350   "f"} to all types occurring in @{text "t"}.
352   \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
353   "f"} over all occurrences of types in @{text "t"}; the term
354   structure is traversed from left to right.
356   \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}
357   to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
358   Const}) occurring in @{text "t"}.
360   \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text
361   "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},
362   @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
363   traversed from left to right.
365   \item @{ML fastype_of}~@{text "t"} determines the type of a
366   well-typed term.  This operation is relatively slow, despite the
367   omission of any sanity checks.
369   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
370   "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the
371   body @{text "b"} are replaced by bound variables.
373   \item @{ML betapply}~@{text "(t, u)"} produces an application @{text
374   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
375   abstraction.
377   \item @{ML Sign.declare_const}~@{text "properties (c, \<sigma>, mx)"}
378   declares a new constant @{text "c :: \<sigma>"} with optional mixfix
379   syntax.
381   \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
382   introduces a new term abbreviation @{text "c \<equiv> t"}.
384   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
385   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
386   convert between two representations of polymorphic constants: full
387   type instance vs.\ compact type arguments form.
389   \end{description}
390 *}
393 section {* Theorems \label{sec:thms} *}
395 text {*
396   \glossary{Proposition}{FIXME A \seeglossary{term} of
397   \seeglossary{type} @{text "prop"}.  Internally, there is nothing
398   special about propositions apart from their type, but the concrete
399   syntax enforces a clear distinction.  Propositions are structured
400   via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
401   "\<And>x. B x"} --- anything else is considered atomic.  The canonical
402   form for propositions is that of a \seeglossary{Hereditary Harrop
403   Formula}. FIXME}
405   \glossary{Theorem}{A proven proposition within a certain theory and
406   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
407   rarely spelled out explicitly.  Theorems are usually normalized
408   according to the \seeglossary{HHF} format. FIXME}
410   \glossary{Fact}{Sometimes used interchangeably for
411   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
412   essentially an extra-logical conjunction.  Facts emerge either as
413   local assumptions, or as results of local goal statements --- both
414   may be simultaneous, hence the list representation. FIXME}
416   \glossary{Schematic variable}{FIXME}
418   \glossary{Fixed variable}{A variable that is bound within a certain
419   proof context; an arbitrary-but-fixed entity within a portion of
420   proof text. FIXME}
422   \glossary{Free variable}{Synonymous for \seeglossary{fixed
423   variable}. FIXME}
425   \glossary{Bound variable}{FIXME}
427   \glossary{Variable}{See \seeglossary{schematic variable},
428   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
429   \seeglossary{type variable}.  The distinguishing feature of
430   different variables is their binding scope. FIXME}
432   A \emph{proposition} is a well-typed term of type @{text "prop"}, a
433   \emph{theorem} is a proven proposition (depending on a context of
434   hypotheses and the background theory).  Primitive inferences include
435   plain natural deduction rules for the primary connectives @{text
436   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
437   notion of equality/equivalence @{text "\<equiv>"}.
438 *}
440 subsection {* Primitive connectives and rules \label{sec:prim_rules} *}
442 text {*
443   The theory @{text "Pure"} contains constant declarations for the
444   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
445   the logical framework, see \figref{fig:pure-connectives}.  The
446   derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
447   defined inductively by the primitive inferences given in
448   \figref{fig:prim-rules}, with the global restriction that the
449   hypotheses must \emph{not} contain any schematic variables.  The
450   builtin equality is conceptually axiomatized as shown in
451   \figref{fig:pure-equality}, although the implementation works
452   directly with derived inferences.
454   \begin{figure}[htb]
455   \begin{center}
456   \begin{tabular}{ll}
457   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
458   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
459   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
460   \end{tabular}
461   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
462   \end{center}
463   \end{figure}
465   \begin{figure}[htb]
466   \begin{center}
467   $468 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}} 469 \qquad 470 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{} 471$
472   $473 \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}} 474 \qquad 475 \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}} 476$
477   $478 \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 479 \qquad 480 \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"}} 481$
482   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
483   \end{center}
484   \end{figure}
486   \begin{figure}[htb]
487   \begin{center}
488   \begin{tabular}{ll}
489   @{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}-conversion \\
490   @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
491   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
492   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
493   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
494   \end{tabular}
495   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
496   \end{center}
497   \end{figure}
499   The introduction and elimination rules for @{text "\<And>"} and @{text
500   "\<Longrightarrow>"} are analogous to formation of dependently typed @{text
501   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
502   are irrelevant in the Pure logic, though; they cannot occur within
503   propositions.  The system provides a runtime option to record
504   explicit proof terms for primitive inferences.  Thus all three
505   levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
506   terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
507   \cite{Berghofer-Nipkow:2000:TPHOL}).
509   Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need
510   not be recorded in the hypotheses, because the simple syntactic
511   types of Pure are always inhabitable.  Assumptions'' @{text "x ::
512   \<tau>"} for type-membership are only present as long as some @{text
513   "x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key
514   difference to @{text "\<lambda>HOL"}'' in the PTS framework
515   \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are
516   treated uniformly for propositions and types.}
518   \medskip The axiomatization of a theory is implicitly closed by
519   forming all instances of type and term variables: @{text "\<turnstile>
520   A\<vartheta>"} holds for any substitution instance of an axiom
521   @{text "\<turnstile> A"}.  By pushing substitutions through derivations
522   inductively, we also get admissible @{text "generalize"} and @{text
523   "instance"} rules as shown in \figref{fig:subst-rules}.
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   Note that @{text "instantiate"} does not require an explicit
542   side-condition, because @{text "\<Gamma>"} may never contain schematic
543   variables.
545   In principle, variables could be substituted in hypotheses as well,
546   but this would disrupt the monotonicity of reasoning: deriving
547   @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is
548   correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
549   the result belongs to a different proof context.
551   \medskip An \emph{oracle} is a function that produces axioms on the
552   fly.  Logically, this is an instance of the @{text "axiom"} rule
553   (\figref{fig:prim-rules}), but there is an operational difference.
554   The system always records oracle invocations within derivations of
555   theorems.  Tracing plain axioms (and named theorems) is optional.
557   Axiomatizations should be limited to the bare minimum, typically as
558   part of the initial logical basis of an object-logic formalization.
559   Later on, theories are usually developed in a strictly definitional
560   fashion, by stating only certain equalities over new constants.
562   A \emph{simple definition} consists of a constant declaration @{text
563   "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t
564   :: \<sigma>"} is a closed term without any hidden polymorphism.  The RHS
565   may depend on further defined constants, but not @{text "c"} itself.
566   Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>
567   t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.
569   An \emph{overloaded definition} consists of a collection of axioms
570   for the same constant, with zero or one equations @{text
571   "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for
572   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention
573   previously defined constants as above, or arbitrary constants @{text
574   "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text
575   "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by
576   primitive recursion over the syntactic structure of a single type
577   argument.
578 *}
580 text %mlref {*
581   \begin{mldecls}
582   @{index_ML_type ctyp} \\
583   @{index_ML_type cterm} \\
584   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
585   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
586   \end{mldecls}
587   \begin{mldecls}
588   @{index_ML_type thm} \\
589   @{index_ML proofs: "int ref"} \\
590   @{index_ML Thm.assume: "cterm -> thm"} \\
591   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
592   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
593   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
594   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
595   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
596   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
597   @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
598   @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
599   \end{mldecls}
600   \begin{mldecls}
601   @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
602   @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
603   @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
604   @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
605   \end{mldecls}
607   \begin{description}
609   \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
610   and terms, respectively.  These are abstract datatypes that
611   guarantee that its values have passed the full well-formedness (and
612   well-typedness) checks, relative to the declarations of type
613   constructors, constants etc. in the theory.
615   \item @{ML ctyp_of}~@{text "thy \<tau>"} and @{ML cterm_of}~@{text "thy
616   t"} explicitly checks types and terms, respectively.  This also
617   involves some basic normalizations, such expansion of type and term
618   abbreviations from the theory context.
620   Re-certification is relatively slow and should be avoided in tight
621   reasoning loops.  There are separate operations to decompose
622   certified entities (including actual theorems).
624   \item @{ML_type thm} represents proven propositions.  This is an
625   abstract datatype that guarantees that its values have been
626   constructed by basic principles of the @{ML_struct Thm} module.
627   Every @{ML thm} value contains a sliding back-reference to the
628   enclosing theory, cf.\ \secref{sec:context-theory}.
630   \item @{ML proofs} determines the detail of proof recording within
631   @{ML_type thm} values: @{ML 0} records only oracles, @{ML 1} records
632   oracles, axioms and named theorems, @{ML 2} records full proof
633   terms.
635   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
636   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
637   correspond to the primitive inferences of \figref{fig:prim-rules}.
639   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
640   corresponds to the @{text "generalize"} rules of
641   \figref{fig:subst-rules}.  Here collections of type and term
642   variables are generalized simultaneously, specified by the given
643   basic names.
645   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
646   \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
647   of \figref{fig:subst-rules}.  Type variables are substituted before
648   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
649   refer to the instantiated versions.
651   \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
652   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
654   \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a
655   named oracle function, cf.\ @{text "axiom"} in
656   \figref{fig:prim-rules}.
658   \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
659   arbitrary propositions as axioms.
661   \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle
662   function for generating arbitrary axioms on the fly.
664   \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
665   \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
666   for constant @{text "c\<^isub>\<tau>"}, relative to existing
667   specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.
669   \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c
670   \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an existing
671   constant @{text "c"}.  Dependencies are recorded (cf.\ @{ML
672   Theory.add_deps}), unless the @{text "unchecked"} option is set.
674   \end{description}
675 *}
678 subsection {* Auxiliary definitions *}
680 text {*
681   Theory @{text "Pure"} provides a few auxiliary definitions, see
682   \figref{fig:pure-aux}.  These special constants are normally not
683   exposed to the user, but appear in internal encodings.
685   \begin{figure}[htb]
686   \begin{center}
687   \begin{tabular}{ll}
688   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
689   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \$1ex] 690 @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\ 691 @{text "#A \<equiv> A"} \\[1ex] 692 @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\ 693 @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex] 694 @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\ 695 @{text "(unspecified)"} \\ 696 \end{tabular} 697 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux} 698 \end{center} 699 \end{figure} 701 Derived conjunction rules include introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A & 702 B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}. 703 Conjunction allows to treat simultaneous assumptions and conclusions 704 uniformly. For example, multiple claims are intermediately 705 represented as explicit conjunction, but this is refined into 706 separate sub-goals before the user continues the proof; the final 707 result is projected into a list of theorems (cf.\ 708 \secref{sec:tactical-goals}). 710 The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex 711 propositions appear as atomic, without changing the meaning: @{text 712 "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable. See 713 \secref{sec:tactical-goals} for specific operations. 715 The @{text "term"} marker turns any well-typed term into a derivable 716 proposition: @{text "\<turnstile> TERM t"} holds unconditionally. Although 717 this is logically vacuous, it allows to treat terms and proofs 718 uniformly, similar to a type-theoretic framework. 720 The @{text "TYPE"} constructor is the canonical representative of 721 the unspecified type @{text "\<alpha> itself"}; it essentially injects the 722 language of types into that of terms. There is specific notation 723 @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau> 724 itself\<^esub>"}. 725 Although being devoid of any particular meaning, the @{text 726 "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term 727 language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal 728 argument in primitive definitions, in order to circumvent hidden 729 polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c 730 TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of 731 a proposition @{text "A"} that depends on an additional type 732 argument, which is essentially a predicate on types. 733 *} 735 text %mlref {* 736 \begin{mldecls} 737 @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\ 738 @{index_ML Conjunction.elim: "thm -> thm * thm"} \\ 739 @{index_ML Drule.mk_term: "cterm -> thm"} \\ 740 @{index_ML Drule.dest_term: "thm -> cterm"} \\ 741 @{index_ML Logic.mk_type: "typ -> term"} \\ 742 @{index_ML Logic.dest_type: "term -> typ"} \\ 743 \end{mldecls} 745 \begin{description} 747 \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text 748 "A"} and @{text "B"}. 750 \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"} 751 from @{text "A & B"}. 753 \item @{ML Drule.mk_term} derives @{text "TERM t"}. 755 \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text 756 "TERM t"}. 758 \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text 759 "TYPE(\<tau>)"}. 761 \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type 762 @{text "\<tau>"}. 764 \end{description} 765 *} 768 section {* Rules \label{sec:rules} *} 770 text %FIXME {* 772 FIXME 774 A \emph{rule} is any Pure theorem in HHF normal form; there is a 775 separate calculus for rule composition, which is modeled after 776 Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows 777 rules to be nested arbitrarily, similar to \cite{extensions91}. 779 Normally, all theorems accessible to the user are proper rules. 780 Low-level inferences are occasional required internally, but the 781 result should be always presented in canonical form. The higher 782 interfaces of Isabelle/Isar will always produce proper rules. It is 783 important to maintain this invariant in add-on applications! 785 There are two main principles of rule composition: @{text 786 "resolution"} (i.e.\ backchaining of rules) and @{text 787 "by-assumption"} (i.e.\ closing a branch); both principles are 788 combined in the variants of @{text "elim-resolution"} and @{text 789 "dest-resolution"}. Raw @{text "composition"} is occasionally 790 useful as well, also it is strictly speaking outside of the proper 791 rule calculus. 793 Rules are treated modulo general higher-order unification, which is 794 unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion 795 on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo 796 the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. 798 This means that any operations within the rule calculus may be 799 subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common 800 practice not to contract or expand unnecessarily. Some mechanisms 801 prefer an one form, others the opposite, so there is a potential 802 danger to produce some oscillation! 804 Only few operations really work \emph{modulo} HHF conversion, but 805 expect a normal form: quantifiers @{text "\<And>"} before implications 806 @{text "\<Longrightarrow>"} at each level of nesting. 808 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF 809 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> 810 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}. 811 Any proposition may be put into HHF form by normalizing with the rule 812 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost 813 quantifier prefix is represented via \seeglossary{schematic 814 variables}, such that the top-level structure is merely that of a 815 \seeglossary{Horn Clause}}. 817 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.} 820 \[ 821 \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}} 822 {@{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})}} 823$
826   $827 \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}} 828 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}} 829$
832   $833 \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"}} 834$
835   $836 \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}} 837$
839   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},
840   @{text "\<Longrightarrow>_lift"}, and @{text compose}.
842   $843 \infer[@{text "(resolution)"}] 844 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}} 845 {\begin{tabular}{l} 846 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\ 847 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\ 848 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\ 849 \end{tabular}} 850$
853   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}
854 *}
857 end