doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Thu Sep 14 22:48:37 2006 +0200 (2006-09-14) changeset 20542 a54ca4e90874 parent 20537 b6b49903db7e child 20543 dc294418ff17 permissions -rw-r--r--
more on theorems;
2 (* $Id$ *)
4 theory logic imports base begin
6 chapter {* Primitive logic \label{ch:logic} *}
8 text {*
9   The logical foundations of Isabelle/Isar are that of the Pure logic,
10   which has been introduced as a natural-deduction framework in
11   \cite{paulson700}.  This is essentially the same logic as @{text
12   "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)
13   \cite{Barendregt-Geuvers:2001}, although there are some key
14   differences in the specific treatment of simple types in
15   Isabelle/Pure.
17   Following type-theoretic parlance, the Pure logic consists of three
18   levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
19   "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
20   "\<And>"} for universal quantification (proofs depending on terms), and
21   @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
23   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)k"}.
85   A \emph{type abbreviation} is a syntactic definition @{text
86   "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
87   variables @{text "\<^vec>\<alpha>"}.  Type abbreviations 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, unification on the algebra of types has most general
114   solutions (modulo equivalence of sorts).  This means that
115   type-inference will produce primary types as expected
116   \cite{nipkow-prehofer}.
117 *}
119 text %mlref {*
120   \begin{mldecls}
121   @{index_ML_type class} \\
122   @{index_ML_type sort} \\
123   @{index_ML_type arity} \\
124   @{index_ML_type typ} \\
125   @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
126   @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
127   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
128   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
129   @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
130   @{index_ML Sign.add_tyabbrs_i: "
131   (string * string list * typ * mixfix) list -> theory -> theory"} \\
132   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
133   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
134   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
135   \end{mldecls}
137   \begin{description}
139   \item @{ML_type class} represents type classes; this is an alias for
140   @{ML_type string}.
142   \item @{ML_type sort} represents sorts; this is an alias for
143   @{ML_type "class list"}.
145   \item @{ML_type arity} represents type arities; this is an alias for
146   triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
147   (\<^vec>s)s"} described above.
149   \item @{ML_type typ} represents types; this is a datatype with
150   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
152   \item @{ML map_atyps}~@{text "f \<tau>"} applies the mapping @{text "f"}
153   to all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text
154   "\<tau>"}.
156   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates the operation @{text
157   "f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar})
158   in @{text "\<tau>"}; the type structure is traversed from left to right.
160   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
161   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
163   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
164   @{text "\<tau>"} is of sort @{text "s"}.
166   \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a new
167   type constructors @{text "\<kappa>"} with @{text "k"} arguments and
168   optional mixfix syntax.
170   \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
171   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
172   optional mixfix syntax.
174   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
175   c\<^isub>n])"} declares a new class @{text "c"}, together with class
176   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
178   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
179   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
180   c\<^isub>2"}.
182   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
183   the arity @{text "\<kappa> :: (\<^vec>s)s"}.
185   \end{description}
186 *}
190 section {* Terms \label{sec:terms} *}
192 text {*
193   \glossary{Term}{FIXME}
195   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
196   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
197   or \cite{paulson-ml2}), with the types being determined determined
198   by the corresponding binders.  In contrast, free variables and
199   constants are have an explicit name and type in each occurrence.
201   \medskip A \emph{bound variable} is a natural number @{text "b"},
202   which accounts for the number of intermediate binders between the
203   variable occurrence in the body and its binding position.  For
204   example, the de-Bruijn term @{text "\<lambda>\<^isub>\<tau>. \<lambda>\<^isub>\<tau>. 1 + 0"}
205   would correspond to @{text "\<lambda>x\<^isub>\<tau>. \<lambda>y\<^isub>\<tau>. x + y"} in a
206   named representation.  Note that a bound variable may be represented
207   by different de-Bruijn indices at different occurrences, depending
208   on the nesting of abstractions.
210   A \emph{loose variables} is a bound variable that is outside the
211   scope of local binders.  The types (and names) for loose variables
212   can be managed as a separate context, that is maintained inside-out
213   like a stack of hypothetical binders.  The core logic only operates
214   on closed terms, without any loose variables.
216   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
217   @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}.  A
218   \emph{schematic variable} is a pair of an indexname and a type,
219   e.g.\ @{text "((x, 0), \<tau>)"} which is usually printed as @{text
220   "?x\<^isub>\<tau>"}.
222   \medskip A \emph{constant} is a pair of a basic name and a type,
223   e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text
224   "c\<^isub>\<tau>"}.  Constants are declared in the context as polymorphic
225   families @{text "c :: \<sigma>"}, meaning that valid all substitution
226   instances @{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
228   The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"}
229   wrt.\ the declaration @{text "c :: \<sigma>"} is defined as the codomain of
230   the matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>,
231   ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in canonical order @{text
232   "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  Within a given theory context,
233   there is a one-to-one correspondence between any constant @{text
234   "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, \<dots>,
235   \<tau>\<^isub>n)"} of its type arguments.  For example, with @{text "plus
236   :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow>
237   nat\<^esub>"} corresponds to @{text "plus(nat)"}.
239   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
240   for type variables in @{text "\<sigma>"}.  These are observed by
241   type-inference as expected, but \emph{ignored} by the core logic.
242   This means the primitive logic is able to reason with instances of
243   polymorphic constants that the user-level type-checker would reject
244   due to violation of type class restrictions.
246   \medskip A \emph{term} is defined inductively over variables and
247   constants, with abstraction and application as follows: @{text "t =
248   b | x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t |
249   t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes care of
250   converting between an external representation with named bound
251   variables.  Subsequently, we shall use the latter notation instead
252   of internal de-Bruijn representation.
254   The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a
255   term according to the structure of atomic terms, abstractions, and
256   applicatins:
257   $258 \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{} 259 \qquad 260 \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}} 261 \qquad 262 \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}} 263$
264   A \emph{well-typed term} is a term that can be typed according to these rules.
266   Typing information can be omitted: type-inference is able to
267   reconstruct the most general type of a raw term, while assigning
268   most general types to all of its variables and constants.
269   Type-inference depends on a context of type constraints for fixed
270   variables, and declarations for polymorphic constants.
272   The identity of atomic terms consists both of the name and the type
273   component.  This means that different variables @{text
274   "x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text
275   "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after type
276   instantiation.  Some outer layers of the system make it hard to
277   produce variables of the same name, but different types.  In
278   particular, type-inference always demands consistent'' type
279   constraints for free variables.  In contrast, mixed instances of
280   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 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 demands special 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 fully expanded before entering the
294   logical core.  Abbreviations are usually reverted when printing
295   terms, using the collective @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for
296   higher-order rewriting.
298   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
299   "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free
300   renaming of bound variables; @{text "\<beta>"}-conversion contracts an
301   abstraction applied to an argument term, substituting the argument
302   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
303   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
304   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
305   does not occur in @{text "f"}.
307   Terms are normally treated modulo @{text "\<alpha>"}-conversion, which is
308   implicit in the de-Bruijn representation.  Names for bound variables
309   in abstractions are maintained separately as (meaningless) comments,
310   mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is
311   commonplace in various higher operations (\secref{sec:rules}) that
312   are based on higher-order unification and matching.
313 *}
315 text %mlref {*
316   \begin{mldecls}
317   @{index_ML_type term} \\
318   @{index_ML "op aconv": "term * term -> bool"} \\
319   @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\  %FIXME rename map_types
320   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
321   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
322   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
323   @{index_ML fastype_of: "term -> typ"} \\
324   @{index_ML lambda: "term -> term -> term"} \\
325   @{index_ML betapply: "term * term -> term"} \\
326   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
327   @{index_ML Sign.add_abbrevs: "string * bool ->
328   ((string * mixfix) * term) list -> theory -> theory"} \\
329   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
330   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
331   \end{mldecls}
333   \begin{description}
335   \item @{ML_type term} represents de-Bruijn terms, with comments in
336   abstractions, and explicitly named free variables and constants;
337   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
338   Var}, @{ML Const}, @{ML Abs}, @{ML "op \$"}.
340   \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
341   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
342   on type @{ML_type term}; raw datatype equality should only be used
343   for operations related to parsing or printing!
345   \item @{ML map_term_types}~@{text "f t"} applies the mapping @{text
346   "f"} to all types occurring in @{text "t"}.
348   \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
349   "f"} over all occurrences of types in @{text "t"}; the term
350   structure is traversed from left to right.
352   \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}
353   to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
354   Const}) occurring in @{text "t"}.
356   \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text
357   "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},
358   @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
359   traversed from left to right.
361   \item @{ML fastype_of}~@{text "t"} determines the type of a
362   well-typed term.  This operation is relatively slow, despite the
363   omission of any sanity checks.
365   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
366   "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the
367   body @{text "b"} are replaced by bound variables.
369   \item @{ML betapply}~@{text "(t, u)"} produces an application @{text
370   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
371   abstraction.
373   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
374   new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
376   \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}
377   declares a new term abbreviation @{text "c \<equiv> t"} with optional
378   mixfix syntax.
380   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
381   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
382   convert between the representations of polymorphic constants: the
383   full type instance vs.\ the compact type arguments form (depending
384   on the most general declaration given in the context).
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-formed 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 *}
439 text {*
440   The theory @{text "Pure"} contains declarations for the standard
441   connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of the logical
442   framework, see \figref{fig:pure-connectives}.  The derivability
443   judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is defined
444   inductively by the primitive inferences given in
445   \figref{fig:prim-rules}, with the global restriction that hypotheses
446   @{text "\<Gamma>"} may \emph{not} contain schematic variables.  The builtin
447   equality is conceptually axiomatized as shown in
448   \figref{fig:pure-equality}, although the implementation works
449   directly with derived inference rules.
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 may never occur
500   within 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.  Typing assumptions'' @{text
509   "x :: \<tau>"} are (implicitly) present only with occurrences of @{text
510   "x\<^isub>\<tau>"} in the statement body.\footnote{This is the key
511   difference @{text "\<lambda>HOL"}'' in the PTS framework
512   \cite{Barendregt-Geuvers:2001}, where @{text "x : A"} hypotheses are
513   treated explicitly for types, in the same way as propositions.}
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 substitution through derivations
519   inductively, we get admissible @{text "generalize"} and @{text
520   "instance"} rules 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 monotonicity reasoning: deriving @{text
544   "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is correct, but
545   @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold --- the result
546   belongs to a different proof context.
548   \medskip The system allows axioms to be stated either as plain
549   propositions, or as arbitrary functions (oracles'') that produce
550   propositions depending on given arguments.  It is possible to trace
551   the used of axioms (and defined theorems) in derivations.
552   Invocations of oracles are recorded invariable.
554   Axiomatizations should be limited to the bare minimum, typically as
555   part of the initial logical basis of an object-logic formalization.
556   Normally, theories will be developed definitionally, by stating
557   restricted equalities over 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
561   "t"} is a closed term without any hidden polymorphism.  The RHS may
562   depend on further defined constants, but not @{text "c"} itself.
563   Definitions of constants with function type may be presented
564   liberally as @{text "c \<^vec> \<equiv> t"} instead of the puristic @{text
565   "c \<equiv> \<lambda>\<^vec>x. t"}.
567   An \emph{overloaded definition} consists may give zero or one
568   equality axioms @{text "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type
569   constructor @{text "\<kappa>"}, with distinct variables @{text "\<^vec>\<alpha>"}
570   as formal arguments.  The RHS may mention previously defined
571   constants as above, or arbitrary constants @{text "d(\<alpha>\<^isub>i)"}
572   for some @{text "\<alpha>\<^isub>i"} projected from @{text "\<^vec>\<alpha>"}.
573   Thus overloaded definitions essentially work by primitive recursion
574   over the syntactic structure of a single type argument.
575 *}
577 text %mlref {*
578   \begin{mldecls}
579   @{index_ML_type ctyp} \\
580   @{index_ML_type cterm} \\
581   @{index_ML_type thm} \\
582   @{index_ML proofs: "int ref"} \\
583   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
584   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
585   @{index_ML Thm.assume: "cterm -> thm"} \\
586   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
587   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
588   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
589   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
590   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
591   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
592   @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
593   @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
594   @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
595   @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
596   @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
597   @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
598   \end{mldecls}
600   \begin{description}
602   \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
603   and terms, respectively.  These are abstract datatypes that
604   guarantee that its values have passed the full well-formedness (and
605   well-typedness) checks, relative to the declarations of type
606   constructors, constants etc. in the theory.
608   This representation avoids syntactic rechecking in tight loops of
609   inferences.  There are separate operations to decompose certified
610   entities (including actual theorems).
612   \item @{ML_type thm} represents proven propositions.  This is an
613   abstract datatype that guarantees that its values have been
614   constructed by basic principles of the @{ML_struct Thm} module.
616   \item @{ML proofs} determines the detail of proof recording: @{ML 0}
617   records only oracles, @{ML 1} records oracles, axioms and named
618   theorems, @{ML 2} records full proof terms.
620   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
621   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
622   correspond to the primitive inferences of \figref{fig:prim-rules}.
624   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
625   corresponds to the @{text "generalize"} rules of
626   \figref{fig:subst-rules}.  A collection of type and term variables
627   is generalized simultaneously, according to the given basic names.
629   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
630   \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
631   of \figref{fig:subst-rules}.  Type variables are substituted before
632   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
633   refer to the instantiated versions.
635   \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
636   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
638   \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes the
639   oracle function @{text "name"} of the theory.  Logically, this is
640   just another instance of @{text "axiom"} in \figref{fig:prim-rules},
641   but the system records an explicit trace of oracle invocations with
642   the @{text "thm"} value.
644   \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} adds
645   arbitrary axioms, without any checking of the proposition.
647   \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an
648   oracle, i.e.\ a function for generating arbitrary axioms.
650   \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
651   \<^vec>d\<^isub>\<sigma>"} declares dependencies of a new specification for
652   constant @{text "c\<^isub>\<tau>"} from relative to existing ones for
653   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 already
657   declared constant @{text "c"}.  Dependencies are recorded using @{ML
658   Theory.add_deps}, unless the @{text "unchecked"} option is set.
660   \end{description}
661 *}
664 subsection {* Auxiliary connectives *}
666 text {*
667   Theory @{text "Pure"} also defines a few auxiliary connectives, see
668   \figref{fig:pure-aux}.  These are normally not exposed to the user,
669   but appear in internal encodings only.
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 "#"}, hidden) \\ 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 usually refined 692 into separate sub-goals before the user continues the proof; the 693 final 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-formed term into a 702 derivable proposition: @{text "\<turnstile> TERM t"} holds unconditionally. 703 Although this is logically vacuous, it allows to treat terms and 704 proofs 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.intr} derives @{text "A"} and @{text "B"} 737 from @{text "A & B"}. 739 \item @{ML Drule.mk_term}~@{text "t"} derives @{text "TERM t"}. 741 \item @{ML Drule.dest_term}~@{text "TERM t"} recovers term @{text 742 "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