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