doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Thu Sep 18 19:39:44 2008 +0200 (2008-09-18) changeset 28290 4cc2b6046258 parent 28110 9d121b171a0a child 28674 08a77c495dc1 permissions -rw-r--r--
simplified oracle interface;
     1

     2 (* $Id$ *)

     3

     4 theory logic imports base begin

     5

     6 chapter {* Primitive logic \label{ch:logic} *}

     7

     8 text {*

     9   The logical foundations of Isabelle/Isar are that of the Pure logic,

    10   which has been introduced as a natural-deduction framework in

    11   \cite{paulson700}.  This is essentially the same logic as @{text

    12   "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)

    13   \cite{Barendregt-Geuvers:2001}, although there are some key

    14   differences in the specific treatment of simple types in

    15   Isabelle/Pure.

    16

    17   Following type-theoretic parlance, the Pure logic consists of three

    18   levels of @{text "\<lambda>"}-calculus with corresponding arrows, @{text

    19   "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text

    20   "\<And>"} for universal quantification (proofs depending on terms), and

    21   @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).

    22

    23   Derivations are relative to a logical theory, which declares type

    24   constructors, constants, and axioms.  Theory declarations support

    25   schematic polymorphism, which is strictly speaking outside the

    26   logic.\footnote{This is the deeper logical reason, why the theory

    27   context @{text "\<Theta>"} is separate from the proof context @{text "\<Gamma>"}

    28   of the core calculus.}

    29 *}

    30

    31

    32 section {* Types \label{sec:types} *}

    33

    34 text {*

    35   The language of types is an uninterpreted order-sorted first-order

    36   algebra; types are qualified by ordered type classes.

    37

    38   \medskip A \emph{type class} is an abstract syntactic entity

    39   declared in the theory context.  The \emph{subclass relation} @{text

    40   "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic

    41   generating relation; the transitive closure is maintained

    42   internally.  The resulting relation is an ordering: reflexive,

    43   transitive, and antisymmetric.

    44

    45   A \emph{sort} is a list of type classes written as @{text "s =

    46   {c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic

    47   intersection.  Notationally, the curly braces are omitted for

    48   singleton intersections, i.e.\ any class @{text "c"} may be read as

    49   a sort @{text "{c}"}.  The ordering on type classes is extended to

    50   sorts according to the meaning of intersections: @{text

    51   "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff

    52   @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}.  The empty intersection

    53   @{text "{}"} refers to the universal sort, which is the largest

    54   element wrt.\ the sort order.  The intersections of all (finitely

    55   many) classes declared in the current theory are the minimal

    56   elements wrt.\ the sort order.

    57

    58   \medskip A \emph{fixed type variable} is a pair of a basic name

    59   (starting with a @{text "'"} character) and a sort constraint, e.g.\

    60   @{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^isub>s"}.

    61   A \emph{schematic type variable} is a pair of an indexname and a

    62   sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually

    63   printed as @{text "?\<alpha>\<^isub>s"}.

    64

    65   Note that \emph{all} syntactic components contribute to the identity

    66   of type variables, including the sort constraint.  The core logic

    67   handles type variables with the same name but different sorts as

    68   different, although some outer layers of the system make it hard to

    69   produce anything like this.

    70

    71   A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator

    72   on types declared in the theory.  Type constructor application is

    73   written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.  For

    74   @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}

    75   instead of @{text "()prop"}.  For @{text "k = 1"} the parentheses

    76   are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.

    77   Further notation is provided for specific constructors, notably the

    78   right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,

    79   \<beta>)fun"}.

    80

    81   A \emph{type} is defined inductively over type variables and type

    82   constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |

    83   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}.

    84

    85   A \emph{type abbreviation} is a syntactic definition @{text

    86   "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over

    87   variables @{text "\<^vec>\<alpha>"}.  Type abbreviations appear as type

    88   constructors in the syntax, but are expanded before entering the

    89   logical core.

    90

    91   A \emph{type arity} declares the image behavior of a type

    92   constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,

    93   s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is

    94   of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is

    95   of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly

    96   completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::

    97   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.

    98

    99   \medskip The sort algebra is always maintained as \emph{coregular},

   100   which means that type arities are consistent with the subclass

   101   relation: for any type constructor @{text "\<kappa>"}, and classes @{text

   102   "c\<^isub>1 \<subseteq> c\<^isub>2"}, and arities @{text "\<kappa> ::

   103   (\<^vec>s\<^isub>1)c\<^isub>1"} and @{text "\<kappa> ::

   104   (\<^vec>s\<^isub>2)c\<^isub>2"} holds @{text "\<^vec>s\<^isub>1 \<subseteq>

   105   \<^vec>s\<^isub>2"} component-wise.

   106

   107   The key property of a coregular order-sorted algebra is that sort

   108   constraints can be solved in a most general fashion: for each type

   109   constructor @{text "\<kappa>"} and sort @{text "s"} there is a most general

   110   vector of argument sorts @{text "(s\<^isub>1, \<dots>, s\<^isub>k)"} such

   111   that a type scheme @{text "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>,

   112   \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is of sort @{text "s"}.

   113   Consequently, type unification has most general solutions (modulo

   114   equivalence of sorts), so type-inference produces primary types as

   115   expected \cite{nipkow-prehofer}.

   116 *}

   117

   118 text %mlref {*

   119   \begin{mldecls}

   120   @{index_ML_type class} \\

   121   @{index_ML_type sort} \\

   122   @{index_ML_type arity} \\

   123   @{index_ML_type typ} \\

   124   @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\

   125   @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\

   126   \end{mldecls}

   127   \begin{mldecls}

   128   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\

   129   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\

   130   @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\

   131   @{index_ML Sign.add_tyabbrs_i: "

   132   (string * string list * typ * mixfix) list -> theory -> theory"} \\

   133   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\

   134   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\

   135   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\

   136   \end{mldecls}

   137

   138   \begin{description}

   139

   140   \item @{ML_type class} represents type classes; this is an alias for

   141   @{ML_type string}.

   142

   143   \item @{ML_type sort} represents sorts; this is an alias for

   144   @{ML_type "class list"}.

   145

   146   \item @{ML_type arity} represents type arities; this is an alias for

   147   triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::

   148   (\<^vec>s)s"} described above.

   149

   150   \item @{ML_type typ} represents types; this is a datatype with

   151   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.

   152

   153   \item @{ML map_atyps}~@{text "f \<tau>"} applies the mapping @{text "f"}

   154   to all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text

   155   "\<tau>"}.

   156

   157   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates the operation @{text

   158   "f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar})

   159   in @{text "\<tau>"}; the type structure is traversed from left to right.

   160

   161   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}

   162   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.

   163

   164   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type

   165   @{text "\<tau>"} is of sort @{text "s"}.

   166

   167   \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a new

   168   type constructors @{text "\<kappa>"} with @{text "k"} arguments and

   169   optional mixfix syntax.

   170

   171   \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}

   172   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with

   173   optional mixfix syntax.

   174

   175   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,

   176   c\<^isub>n])"} declares a new class @{text "c"}, together with class

   177   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.

   178

   179   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,

   180   c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \<subseteq>

   181   c\<^isub>2"}.

   182

   183   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares

   184   the arity @{text "\<kappa> :: (\<^vec>s)s"}.

   185

   186   \end{description}

   187 *}

   188

   189

   190

   191 section {* Terms \label{sec:terms} *}

   192

   193 text {*

   194   \glossary{Term}{FIXME}

   195

   196   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus

   197   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}

   198   or \cite{paulson-ml2}), with the types being determined determined

   199   by the corresponding binders.  In contrast, free variables and

   200   constants are have an explicit name and type in each occurrence.

   201

   202   \medskip A \emph{bound variable} is a natural number @{text "b"},

   203   which accounts for the number of intermediate binders between the

   204   variable occurrence in the body and its binding position.  For

   205   example, the de-Bruijn term @{text

   206   "\<lambda>\<^bsub>nat\<^esub>. \<lambda>\<^bsub>nat\<^esub>. 1 + 0"} would

   207   correspond to @{text

   208   "\<lambda>x\<^bsub>nat\<^esub>. \<lambda>y\<^bsub>nat\<^esub>. x + y"} in a named

   209   representation.  Note that a bound variable may be represented by

   210   different de-Bruijn indices at different occurrences, depending on

   211   the nesting of abstractions.

   212

   213   A \emph{loose variable} is a bound variable that is outside the

   214   scope of local binders.  The types (and names) for loose variables

   215   can be managed as a separate context, that is maintained as a stack

   216   of hypothetical binders.  The core logic operates on closed terms,

   217   without any loose variables.

   218

   219   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\

   220   @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}.  A

   221   \emph{schematic variable} is a pair of an indexname and a type,

   222   e.g.\ @{text "((x, 0), \<tau>)"} which is usually printed as @{text

   223   "?x\<^isub>\<tau>"}.

   224

   225   \medskip A \emph{constant} is a pair of a basic name and a type,

   226   e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text

   227   "c\<^isub>\<tau>"}.  Constants are declared in the context as polymorphic

   228   families @{text "c :: \<sigma>"}, meaning that all substitution instances

   229   @{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.

   230

   231   The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"}

   232   wrt.\ the declaration @{text "c :: \<sigma>"} is defined as the codomain of

   233   the matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>,

   234   ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in canonical order @{text

   235   "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  Within a given theory context,

   236   there is a one-to-one correspondence between any constant @{text

   237   "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, \<dots>,

   238   \<tau>\<^isub>n)"} of its type arguments.  For example, with @{text "plus

   239   :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow>

   240   nat\<^esub>"} corresponds to @{text "plus(nat)"}.

   241

   242   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints

   243   for type variables in @{text "\<sigma>"}.  These are observed by

   244   type-inference as expected, but \emph{ignored} by the core logic.

   245   This means the primitive logic is able to reason with instances of

   246   polymorphic constants that the user-level type-checker would reject

   247   due to violation of type class restrictions.

   248

   249   \medskip An \emph{atomic} term is either a variable or constant.  A

   250   \emph{term} is defined inductively over atomic terms, with

   251   abstraction and application as follows: @{text "t = b | x\<^isub>\<tau> |

   252   ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.

   253   Parsing and printing takes care of converting between an external

   254   representation with named bound variables.  Subsequently, we shall

   255   use the latter notation instead of internal de-Bruijn

   256   representation.

   257

   258   The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a

   259   term according to the structure of atomic terms, abstractions, and

   260   applicatins:

   261   $  262 \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}   263 \qquad   264 \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}   265 \qquad   266 \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}   267$

   268   A \emph{well-typed term} is a term that can be typed according to these rules.

   269

   270   Typing information can be omitted: type-inference is able to

   271   reconstruct the most general type of a raw term, while assigning

   272   most general types to all of its variables and constants.

   273   Type-inference depends on a context of type constraints for fixed

   274   variables, and declarations for polymorphic constants.

   275

   276   The identity of atomic terms consists both of the name and the type

   277   component.  This means that different variables @{text

   278   "x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text

   279   "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after type

   280   instantiation.  Some outer layers of the system make it hard to

   281   produce variables of the same name, but different types.  In

   282   contrast, mixed instances of polymorphic constants occur frequently.

   283

   284   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}

   285   is the set of type variables occurring in @{text "t"}, but not in

   286   @{text "\<sigma>"}.  This means that the term implicitly depends on type

   287   arguments that are not accounted in the result type, i.e.\ there are

   288   different type instances @{text "t\<vartheta> :: \<sigma>"} and @{text

   289   "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly

   290   pathological situation notoriously demands additional care.

   291

   292   \medskip A \emph{term abbreviation} is a syntactic definition @{text

   293   "c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},

   294   without any hidden polymorphism.  A term abbreviation looks like a

   295   constant in the syntax, but is expanded before entering the logical

   296   core.  Abbreviations are usually reverted when printing terms, using

   297   @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higher-order rewriting.

   298

   299   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text

   300   "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free

   301   renaming of bound variables; @{text "\<beta>"}-conversion contracts an

   302   abstraction applied to an argument term, substituting the argument

   303   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text

   304   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text

   305   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable

   306   does not occur in @{text "f"}.

   307

   308   Terms are normally treated modulo @{text "\<alpha>"}-conversion, which is

   309   implicit in the de-Bruijn representation.  Names for bound variables

   310   in abstractions are maintained separately as (meaningless) comments,

   311   mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is

   312   commonplace in various standard operations (\secref{sec:rules}) that

   313   are based on higher-order unification and matching.

   314 *}

   315

   316 text %mlref {*

   317   \begin{mldecls}

   318   @{index_ML_type term} \\

   319   @{index_ML "op aconv": "term * term -> bool"} \\

   320   @{index_ML map_types: "(typ -> typ) -> term -> term"} \\

   321   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\

   322   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\

   323   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\

   324   \end{mldecls}

   325   \begin{mldecls}

   326   @{index_ML fastype_of: "term -> typ"} \\

   327   @{index_ML lambda: "term -> term -> term"} \\

   328   @{index_ML betapply: "term * term -> term"} \\

   329   @{index_ML Sign.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.get_axiom_i: "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.get_axiom_i}~@{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 {* Rules \label{sec:rules} *}   766   767 text %FIXME {*   768   769 FIXME   770   771 A \emph{rule} is any Pure theorem in HHF normal form; there is a   772 separate calculus for rule composition, which is modeled after   773 Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows   774 rules to be nested arbitrarily, similar to \cite{extensions91}.   775   776 Normally, all theorems accessible to the user are proper rules.   777 Low-level inferences are occasional required internally, but the   778 result should be always presented in canonical form. The higher   779 interfaces of Isabelle/Isar will always produce proper rules. It is   780 important to maintain this invariant in add-on applications!   781   782 There are two main principles of rule composition: @{text   783 "resolution"} (i.e.\ backchaining of rules) and @{text   784 "by-assumption"} (i.e.\ closing a branch); both principles are   785 combined in the variants of @{text "elim-resolution"} and @{text   786 "dest-resolution"}. Raw @{text "composition"} is occasionally   787 useful as well, also it is strictly speaking outside of the proper   788 rule calculus.   789   790 Rules are treated modulo general higher-order unification, which is   791 unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion   792 on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo   793 the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.   794   795 This means that any operations within the rule calculus may be   796 subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common   797 practice not to contract or expand unnecessarily. Some mechanisms   798 prefer an one form, others the opposite, so there is a potential   799 danger to produce some oscillation!   800   801 Only few operations really work \emph{modulo} HHF conversion, but   802 expect a normal form: quantifiers @{text "\<And>"} before implications   803 @{text "\<Longrightarrow>"} at each level of nesting.   804   805 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF   806 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>   807 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.   808 Any proposition may be put into HHF form by normalizing with the rule   809 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost   810 quantifier prefix is represented via \seeglossary{schematic   811 variables}, such that the top-level structure is merely that of a   812 \seeglossary{Horn Clause}}.   813   814 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}   815   816   817 \[   818 \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}   819 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}   820$

   821

   822

   823   $  824 \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}   825 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}   826$

   827

   828

   829   $  830 \infer[@{text "(\<And>_lift)"}]{@{text "(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"}}   831$

   832   $  833 \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}   834$

   835

   836   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},

   837   @{text "\<Longrightarrow>_lift"}, and @{text compose}.

   838

   839   $  840 \infer[@{text "(resolution)"}]   841 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   842 {\begin{tabular}{l}   843 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\   844 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   845 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   846 \end{tabular}}   847$

   848

   849

   850   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}

   851 *}

   852

   853

   854 end