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