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