doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Thu Nov 13 22:06:36 2008 +0100 (2008-11-13)
changeset 28784 9495aec512e2
parent 28674 08a77c495dc1
child 28868 4fe0e90080ce
permissions -rw-r--r--
renamed "Rules" to "Object-level rules";
     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:obj-rules})
   313   that 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.declare_const: "Properties.T -> (Name.binding * typ) * mixfix ->
   330   theory -> term * theory"} \\
   331   @{index_ML Sign.add_abbrev: "string -> Properties.T -> bstring * term ->
   332   theory -> (term * term) * theory"} \\
   333   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   334   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   335   \end{mldecls}
   336 
   337   \begin{description}
   338 
   339   \item @{ML_type term} represents de-Bruijn terms, with comments in
   340   abstractions, and explicitly named free variables and constants;
   341   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
   342   Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.
   343 
   344   \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
   345   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
   346   on type @{ML_type term}; raw datatype equality should only be used
   347   for operations related to parsing or printing!
   348 
   349   \item @{ML map_types}~@{text "f t"} applies the mapping @{text
   350   "f"} to all types occurring in @{text "t"}.
   351 
   352   \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
   353   "f"} over all occurrences of types in @{text "t"}; the term
   354   structure is traversed from left to right.
   355 
   356   \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}
   357   to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
   358   Const}) occurring in @{text "t"}.
   359 
   360   \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text
   361   "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},
   362   @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
   363   traversed from left to right.
   364 
   365   \item @{ML fastype_of}~@{text "t"} determines the type of a
   366   well-typed term.  This operation is relatively slow, despite the
   367   omission of any sanity checks.
   368 
   369   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
   370   "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the
   371   body @{text "b"} are replaced by bound variables.
   372 
   373   \item @{ML betapply}~@{text "(t, u)"} produces an application @{text
   374   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
   375   abstraction.
   376 
   377   \item @{ML Sign.declare_const}~@{text "properties ((c, \<sigma>), mx)"}
   378   declares a new constant @{text "c :: \<sigma>"} with optional mixfix
   379   syntax.
   380 
   381   \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
   382   introduces a new term abbreviation @{text "c \<equiv> t"}.
   383 
   384   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
   385   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
   386   convert between two representations of polymorphic constants: full
   387   type instance vs.\ compact type arguments form.
   388 
   389   \end{description}
   390 *}
   391 
   392 
   393 section {* Theorems \label{sec:thms} *}
   394 
   395 text {*
   396   \glossary{Proposition}{FIXME A \seeglossary{term} of
   397   \seeglossary{type} @{text "prop"}.  Internally, there is nothing
   398   special about propositions apart from their type, but the concrete
   399   syntax enforces a clear distinction.  Propositions are structured
   400   via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
   401   "\<And>x. B x"} --- anything else is considered atomic.  The canonical
   402   form for propositions is that of a \seeglossary{Hereditary Harrop
   403   Formula}. FIXME}
   404 
   405   \glossary{Theorem}{A proven proposition within a certain theory and
   406   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
   407   rarely spelled out explicitly.  Theorems are usually normalized
   408   according to the \seeglossary{HHF} format. FIXME}
   409 
   410   \glossary{Fact}{Sometimes used interchangeably for
   411   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
   412   essentially an extra-logical conjunction.  Facts emerge either as
   413   local assumptions, or as results of local goal statements --- both
   414   may be simultaneous, hence the list representation. FIXME}
   415 
   416   \glossary{Schematic variable}{FIXME}
   417 
   418   \glossary{Fixed variable}{A variable that is bound within a certain
   419   proof context; an arbitrary-but-fixed entity within a portion of
   420   proof text. FIXME}
   421 
   422   \glossary{Free variable}{Synonymous for \seeglossary{fixed
   423   variable}. FIXME}
   424 
   425   \glossary{Bound variable}{FIXME}
   426 
   427   \glossary{Variable}{See \seeglossary{schematic variable},
   428   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
   429   \seeglossary{type variable}.  The distinguishing feature of
   430   different variables is their binding scope. FIXME}
   431 
   432   A \emph{proposition} is a well-typed term of type @{text "prop"}, a
   433   \emph{theorem} is a proven proposition (depending on a context of
   434   hypotheses and the background theory).  Primitive inferences include
   435   plain natural deduction rules for the primary connectives @{text
   436   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
   437   notion of equality/equivalence @{text "\<equiv>"}.
   438 *}
   439 
   440 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
   441 
   442 text {*
   443   The theory @{text "Pure"} contains constant declarations for the
   444   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
   445   the logical framework, see \figref{fig:pure-connectives}.  The
   446   derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
   447   defined inductively by the primitive inferences given in
   448   \figref{fig:prim-rules}, with the global restriction that the
   449   hypotheses must \emph{not} contain any schematic variables.  The
   450   builtin equality is conceptually axiomatized as shown in
   451   \figref{fig:pure-equality}, although the implementation works
   452   directly with derived inferences.
   453 
   454   \begin{figure}[htb]
   455   \begin{center}
   456   \begin{tabular}{ll}
   457   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
   458   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
   459   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
   460   \end{tabular}
   461   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
   462   \end{center}
   463   \end{figure}
   464 
   465   \begin{figure}[htb]
   466   \begin{center}
   467   \[
   468   \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}
   469   \qquad
   470   \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
   471   \]
   472   \[
   473   \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
   474   \qquad
   475   \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
   476   \]
   477   \[
   478   \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
   479   \qquad
   480   \infer[@{text "(\<Longrightarrow>_elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
   481   \]
   482   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
   483   \end{center}
   484   \end{figure}
   485 
   486   \begin{figure}[htb]
   487   \begin{center}
   488   \begin{tabular}{ll}
   489   @{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}-conversion \\
   490   @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
   491   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
   492   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
   493   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
   494   \end{tabular}
   495   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
   496   \end{center}
   497   \end{figure}
   498 
   499   The introduction and elimination rules for @{text "\<And>"} and @{text
   500   "\<Longrightarrow>"} are analogous to formation of dependently typed @{text
   501   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
   502   are irrelevant in the Pure logic, though; they cannot occur within
   503   propositions.  The system provides a runtime option to record
   504   explicit proof terms for primitive inferences.  Thus all three
   505   levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
   506   terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
   507   \cite{Berghofer-Nipkow:2000:TPHOL}).
   508 
   509   Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need
   510   not be recorded in the hypotheses, because the simple syntactic
   511   types of Pure are always inhabitable.  ``Assumptions'' @{text "x ::
   512   \<tau>"} for type-membership are only present as long as some @{text
   513   "x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key
   514   difference to ``@{text "\<lambda>HOL"}'' in the PTS framework
   515   \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are
   516   treated uniformly for propositions and types.}
   517 
   518   \medskip The axiomatization of a theory is implicitly closed by
   519   forming all instances of type and term variables: @{text "\<turnstile>
   520   A\<vartheta>"} holds for any substitution instance of an axiom
   521   @{text "\<turnstile> A"}.  By pushing substitutions through derivations
   522   inductively, we also get admissible @{text "generalize"} and @{text
   523   "instance"} rules as shown in \figref{fig:subst-rules}.
   524 
   525   \begin{figure}[htb]
   526   \begin{center}
   527   \[
   528   \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}
   529   \quad
   530   \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
   531   \]
   532   \[
   533   \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}
   534   \quad
   535   \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}
   536   \]
   537   \caption{Admissible substitution rules}\label{fig:subst-rules}
   538   \end{center}
   539   \end{figure}
   540 
   541   Note that @{text "instantiate"} does not require an explicit
   542   side-condition, because @{text "\<Gamma>"} may never contain schematic
   543   variables.
   544 
   545   In principle, variables could be substituted in hypotheses as well,
   546   but this would disrupt the monotonicity of reasoning: deriving
   547   @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is
   548   correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
   549   the result belongs to a different proof context.
   550 
   551   \medskip An \emph{oracle} is a function that produces axioms on the
   552   fly.  Logically, this is an instance of the @{text "axiom"} rule
   553   (\figref{fig:prim-rules}), but there is an operational difference.
   554   The system always records oracle invocations within derivations of
   555   theorems.  Tracing plain axioms (and named theorems) is optional.
   556 
   557   Axiomatizations should be limited to the bare minimum, typically as
   558   part of the initial logical basis of an object-logic formalization.
   559   Later on, theories are usually developed in a strictly definitional
   560   fashion, by stating only certain equalities over new constants.
   561 
   562   A \emph{simple definition} consists of a constant declaration @{text
   563   "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t
   564   :: \<sigma>"} is a closed term without any hidden polymorphism.  The RHS
   565   may depend on further defined constants, but not @{text "c"} itself.
   566   Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>
   567   t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.
   568 
   569   An \emph{overloaded definition} consists of a collection of axioms
   570   for the same constant, with zero or one equations @{text
   571   "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for
   572   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention
   573   previously defined constants as above, or arbitrary constants @{text
   574   "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text
   575   "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by
   576   primitive recursion over the syntactic structure of a single type
   577   argument.
   578 *}
   579 
   580 text %mlref {*
   581   \begin{mldecls}
   582   @{index_ML_type ctyp} \\
   583   @{index_ML_type cterm} \\
   584   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
   585   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
   586   \end{mldecls}
   587   \begin{mldecls}
   588   @{index_ML_type thm} \\
   589   @{index_ML proofs: "int ref"} \\
   590   @{index_ML Thm.assume: "cterm -> thm"} \\
   591   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   592   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
   593   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   594   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
   595   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   596   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
   597   @{index_ML Thm.axiom: "theory -> string -> thm"} \\
   598   @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
   599   -> (string * ('a -> thm)) * theory"} \\
   600   \end{mldecls}
   601   \begin{mldecls}
   602   @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
   603   @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
   604   @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
   605   \end{mldecls}
   606 
   607   \begin{description}
   608 
   609   \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
   610   and terms, respectively.  These are abstract datatypes that
   611   guarantee that its values have passed the full well-formedness (and
   612   well-typedness) checks, relative to the declarations of type
   613   constructors, constants etc. in the theory.
   614 
   615   \item @{ML ctyp_of}~@{text "thy \<tau>"} and @{ML cterm_of}~@{text "thy
   616   t"} explicitly checks types and terms, respectively.  This also
   617   involves some basic normalizations, such expansion of type and term
   618   abbreviations from the theory context.
   619 
   620   Re-certification is relatively slow and should be avoided in tight
   621   reasoning loops.  There are separate operations to decompose
   622   certified entities (including actual theorems).
   623 
   624   \item @{ML_type thm} represents proven propositions.  This is an
   625   abstract datatype that guarantees that its values have been
   626   constructed by basic principles of the @{ML_struct Thm} module.
   627   Every @{ML thm} value contains a sliding back-reference to the
   628   enclosing theory, cf.\ \secref{sec:context-theory}.
   629 
   630   \item @{ML proofs} determines the detail of proof recording within
   631   @{ML_type thm} values: @{ML 0} records only oracles, @{ML 1} records
   632   oracles, axioms and named theorems, @{ML 2} records full proof
   633   terms.
   634 
   635   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
   636   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
   637   correspond to the primitive inferences of \figref{fig:prim-rules}.
   638 
   639   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
   640   corresponds to the @{text "generalize"} rules of
   641   \figref{fig:subst-rules}.  Here collections of type and term
   642   variables are generalized simultaneously, specified by the given
   643   basic names.
   644 
   645   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
   646   \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
   647   of \figref{fig:subst-rules}.  Type variables are substituted before
   648   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
   649   refer to the instantiated versions.
   650 
   651   \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
   652   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
   653 
   654   \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
   655   oracle rule, essentially generating arbitrary axioms on the fly,
   656   cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
   657 
   658   \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
   659   arbitrary propositions as axioms.
   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 {* Object-level rules \label{sec:obj-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