doc-src/IsarImplementation/Thy/logic.thy
author haftmann
Wed Feb 14 10:07:17 2007 +0100 (2007-02-14)
changeset 22322 b9924abb8c66
parent 21827 0b1d07f79c1e
child 24828 137c242e7277
permissions -rw-r--r--
continued
     1 
     2 (* $Id$ *)
     3 
     4 theory logic imports base begin
     5 
     6 chapter {* Primitive logic \label{ch:logic} *}
     7 
     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.
    16 
    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).
    22 
    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 *}
    30 
    31 
    32 section {* Types \label{sec:types} *}
    33 
    34 text {*
    35   The language of types is an uninterpreted order-sorted first-order
    36   algebra; types are qualified by ordered type classes.
    37 
    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.
    44 
    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.
    57 
    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"}.
    64 
    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.
    70 
    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"}.
    80   
    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>"}.
    84 
    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.
    90 
    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"}.
    98 
    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.
   106 
   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 *}
   117 
   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}
   137 
   138   \begin{description}
   139 
   140   \item @{ML_type class} represents type classes; this is an alias for
   141   @{ML_type string}.
   142 
   143   \item @{ML_type sort} represents sorts; this is an alias for
   144   @{ML_type "class list"}.
   145 
   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.
   149 
   150   \item @{ML_type typ} represents types; this is a datatype with
   151   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
   152 
   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>"}.
   156 
   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.
   160 
   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"}.
   163 
   164   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
   165   @{text "\<tau>"} is of sort @{text "s"}.
   166 
   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.
   170 
   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.
   174 
   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"}.
   178 
   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"}.
   182 
   183   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
   184   the arity @{text "\<kappa> :: (\<^vec>s)s"}.
   185 
   186   \end{description}
   187 *}
   188 
   189 
   190 
   191 section {* Terms \label{sec:terms} *}
   192 
   193 text {*
   194   \glossary{Term}{FIXME}
   195 
   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.
   201 
   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.
   212 
   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.
   218 
   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>"}.
   224 
   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.
   230 
   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)"}.
   241 
   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.
   248 
   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.
   257 
   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.
   269 
   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.
   275 
   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.
   283 
   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.
   291 
   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.
   298 
   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"}.
   307 
   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 *}
   315 
   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 -> 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}
   334 
   335   \begin{description}
   336 
   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 $"}.
   341 
   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!
   346 
   347   \item @{ML map_types}~@{text "f t"} applies the mapping @{text
   348   "f"} to all types occurring in @{text "t"}.
   349 
   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.
   353 
   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"}.
   357 
   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.
   362 
   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.
   366 
   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.
   370 
   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.
   374 
   375   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
   376   new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
   377 
   378   \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
   379   introduces a new term abbreviation @{text "c \<equiv> t"}.
   380 
   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.
   385 
   386   \end{description}
   387 *}
   388 
   389 
   390 section {* Theorems \label{sec:thms} *}
   391 
   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}
   401 
   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}
   406 
   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}
   412 
   413   \glossary{Schematic variable}{FIXME}
   414 
   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}
   418 
   419   \glossary{Free variable}{Synonymous for \seeglossary{fixed
   420   variable}. FIXME}
   421 
   422   \glossary{Bound variable}{FIXME}
   423 
   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}
   428 
   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 *}
   436 
   437 subsection {* Primitive connectives and rules \label{sec:prim_rules} *}
   438 
   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.
   450 
   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}
   461 
   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}
   482 
   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}
   495 
   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}).
   505 
   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.}
   514 
   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}.
   521 
   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}
   537 
   538   Note that @{text "instantiate"} does not require an explicit
   539   side-condition, because @{text "\<Gamma>"} may never contain schematic
   540   variables.
   541 
   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.
   547 
   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.
   553 
   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.
   558 
   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"}.
   565 
   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 *}
   576 
   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}
   603 
   604   \begin{description}
   605 
   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.
   611 
   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.
   616 
   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).
   620 
   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}.
   626 
   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.
   631 
   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}.
   635 
   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.
   641 
   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.
   647 
   648   \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
   649   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
   650 
   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}.
   654 
   655   \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
   656   arbitrary propositions as axioms.
   657 
   658   \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle
   659   function for generating arbitrary axioms on the fly.
   660 
   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>"}.
   665 
   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.
   670 
   671   \end{description}
   672 *}
   673 
   674 
   675 subsection {* Auxiliary definitions *}
   676 
   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.
   681 
   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}
   697 
   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}).
   706 
   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.
   711 
   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.
   716 
   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 *}
   731 
   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}
   741 
   742   \begin{description}
   743 
   744   \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text
   745   "A"} and @{text "B"}.
   746 
   747   \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}
   748   from @{text "A & B"}.
   749 
   750   \item @{ML Drule.mk_term} derives @{text "TERM t"}.
   751 
   752   \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text
   753   "TERM t"}.
   754 
   755   \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text
   756   "TYPE(\<tau>)"}.
   757 
   758   \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type
   759   @{text "\<tau>"}.
   760 
   761   \end{description}
   762 *}
   763 
   764 
   765 section {* Rules \label{sec:rules} *}
   766 
   767 text %FIXME {*
   768 
   769 FIXME
   770 
   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}.
   775 
   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!
   781 
   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.
   789 
   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)"}.
   794 
   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!
   800 
   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.
   804 
   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}}.
   813 
   814 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   815 
   816 
   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   \]
   821 
   822 
   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   \]
   827 
   828 
   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   \]
   835 
   836   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},
   837   @{text "\<Longrightarrow>_lift"}, and @{text compose}.
   838 
   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   \]
   848 
   849 
   850   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}
   851 *}
   852 
   853 
   854 end