doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Tue Sep 12 21:05:39 2006 +0200 (2006-09-12) changeset 20521 189811b39869 parent 20520 05fd007bdeb9 child 20537 b6b49903db7e permissions -rw-r--r--
more on theorems;
 wenzelm@18537  1 wenzelm@18537  2 (* $Id$ *)  wenzelm@18537  3 wenzelm@18537  4 theory logic imports base begin  wenzelm@18537  5 wenzelm@20470  6 chapter {* Primitive logic \label{ch:logic} *}  wenzelm@18537  7 wenzelm@20480  8 text {*  wenzelm@20480  9  The logical foundations of Isabelle/Isar are that of the Pure logic,  wenzelm@20480  10  which has been introduced as a natural-deduction framework in  wenzelm@20480  11  \cite{paulson700}. This is essentially the same logic as @{text  wenzelm@20493  12  "\HOL"}'' in the more abstract setting of Pure Type Systems (PTS)  wenzelm@20480  13  \cite{Barendregt-Geuvers:2001}, although there are some key  wenzelm@20491  14  differences in the specific treatment of simple types in  wenzelm@20491  15  Isabelle/Pure.  wenzelm@20480  16 wenzelm@20480  17  Following type-theoretic parlance, the Pure logic consists of three  wenzelm@20480  18  levels of @{text "\"}-calculus with corresponding arrows: @{text  wenzelm@20480  19  "\"} for syntactic function space (terms depending on terms), @{text  wenzelm@20480  20  "\"} for universal quantification (proofs depending on terms), and  wenzelm@20480  21  @{text "\"} for implication (proofs depending on proofs).  wenzelm@20480  22 wenzelm@20480  23  Pure derivations are relative to a logical theory, which declares  wenzelm@20491  24  type constructors, term constants, and axioms. Theory declarations  wenzelm@20491  25  support schematic polymorphism, which is strictly speaking outside  wenzelm@20491  26  the logic.\footnote{Incidently, this is the main logical reason, why  wenzelm@20491  27  the theory context @{text "\"} is separate from the context @{text  wenzelm@20491  28  "\"} of the core calculus.}  wenzelm@20480  29 *}  wenzelm@20480  30 wenzelm@20480  31 wenzelm@20451  32 section {* Types \label{sec:types} *}  wenzelm@20437  33 wenzelm@20437  34 text {*  wenzelm@20480  35  The language of types is an uninterpreted order-sorted first-order  wenzelm@20480  36  algebra; types are qualified by ordered type classes.  wenzelm@20480  37 wenzelm@20480  38  \medskip A \emph{type class} is an abstract syntactic entity  wenzelm@20480  39  declared in the theory context. The \emph{subclass relation} @{text  wenzelm@20480  40  "c\<^isub>1 \ c\<^isub>2"} is specified by stating an acyclic  wenzelm@20491  41  generating relation; the transitive closure is maintained  wenzelm@20491  42  internally. The resulting relation is an ordering: reflexive,  wenzelm@20491  43  transitive, and antisymmetric.  wenzelm@20451  44 wenzelm@20480  45  A \emph{sort} is a list of type classes written as @{text  wenzelm@20480  46  "{c\<^isub>1, \, c\<^isub>m}"}, which represents symbolic  wenzelm@20480  47  intersection. Notationally, the curly braces are omitted for  wenzelm@20480  48  singleton intersections, i.e.\ any class @{text "c"} may be read as  wenzelm@20480  49  a sort @{text "{c}"}. The ordering on type classes is extended to  wenzelm@20491  50  sorts according to the meaning of intersections: @{text  wenzelm@20491  51  "{c\<^isub>1, \ c\<^isub>m} \ {d\<^isub>1, \, d\<^isub>n}"} iff  wenzelm@20491  52  @{text "\j. \i. c\<^isub>i \ d\<^isub>j"}. The empty intersection  wenzelm@20491  53  @{text "{}"} refers to the universal sort, which is the largest  wenzelm@20491  54  element wrt.\ the sort order. The intersections of all (finitely  wenzelm@20491  55  many) classes declared in the current theory are the minimal  wenzelm@20491  56  elements wrt.\ the sort order.  wenzelm@20480  57 wenzelm@20491  58  \medskip A \emph{fixed type variable} is a pair of a basic name  wenzelm@20493  59  (starting with a @{text "'"} character) and a sort constraint. For  wenzelm@20480  60  example, @{text "('a, s)"} which is usually printed as @{text  wenzelm@20480  61  "\\<^isub>s"}. A \emph{schematic type variable} is a pair of an  wenzelm@20480  62  indexname and a sort constraint. For example, @{text "(('a, 0),  wenzelm@20491  63  s)"} which is usually printed as @{text "?\\<^isub>s"}.  wenzelm@20451  64 wenzelm@20480  65  Note that \emph{all} syntactic components contribute to the identity  wenzelm@20493  66  of type variables, including the sort constraint. The core logic  wenzelm@20493  67  handles type variables with the same name but different sorts as  wenzelm@20493  68  different, although some outer layers of the system make it hard to  wenzelm@20493  69  produce anything like this.  wenzelm@20451  70 wenzelm@20493  71  A \emph{type constructor} @{text "\"} is a @{text "k"}-ary operator  wenzelm@20493  72  on types declared in the theory. Type constructor application is  wenzelm@20494  73  usually written postfix as @{text "(\\<^isub>1, \, \\<^isub>k)\"}.  wenzelm@20494  74  For @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text  wenzelm@20494  75  "prop"} instead of @{text "()prop"}. For @{text "k = 1"} the  wenzelm@20494  76  parentheses are omitted, e.g.\ @{text "\ list"} instead of @{text  wenzelm@20494  77  "(\)list"}. Further notation is provided for specific constructors,  wenzelm@20494  78  notably the right-associative infix @{text "\ \ \"} instead of  wenzelm@20494  79  @{text "(\, \)fun"}.  wenzelm@20480  80   wenzelm@20514  81  A \emph{type} @{text "\"} is defined inductively over type variables  wenzelm@20514  82  and type constructors as follows: @{text "\ = \\<^isub>s |  wenzelm@20514  83  ?\\<^isub>s | (\\<^sub>1, \, \\<^sub>k)k"}.  wenzelm@20451  84 wenzelm@20514  85  A \emph{type abbreviation} is a syntactic definition @{text  wenzelm@20494  86  "(\<^vec>\)\ = \"} of an arbitrary type expression @{text "\"} over  wenzelm@20494  87  variables @{text "\<^vec>\"}. Type abbreviations looks like type  wenzelm@20494  88  constructors at the surface, but are fully expanded before entering  wenzelm@20494  89  the logical core.  wenzelm@20480  90 wenzelm@20480  91  A \emph{type arity} declares the image behavior of a type  wenzelm@20494  92  constructor wrt.\ the algebra of sorts: @{text "\ :: (s\<^isub>1, \,  wenzelm@20494  93  s\<^isub>k)s"} means that @{text "(\\<^isub>1, \, \\<^isub>k)\"} is  wenzelm@20494  94  of sort @{text "s"} if every argument type @{text "\\<^isub>i"} is  wenzelm@20494  95  of sort @{text "s\<^isub>i"}. Arity declarations are implicitly  wenzelm@20494  96  completed, i.e.\ @{text "\ :: (\<^vec>s)c"} entails @{text "\ ::  wenzelm@20491  97  (\<^vec>s)c'"} for any @{text "c' \ c"}.  wenzelm@20491  98 wenzelm@20491  99  \medskip The sort algebra is always maintained as \emph{coregular},  wenzelm@20491  100  which means that type arities are consistent with the subclass  wenzelm@20494  101  relation: for each type constructor @{text "\"} and classes @{text  wenzelm@20494  102  "c\<^isub>1 \ c\<^isub>2"}, any arity @{text "\ ::  wenzelm@20494  103  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\  wenzelm@20480  104  :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \  wenzelm@20519  105  \<^vec>s\<^isub>2"} holds component-wise.  wenzelm@20451  106 wenzelm@20491  107  The key property of a coregular order-sorted algebra is that sort  wenzelm@20494  108  constraints may be always solved in a most general fashion: for each  wenzelm@20494  109  type constructor @{text "\"} and sort @{text "s"} there is a most  wenzelm@20494  110  general vector of argument sorts @{text "(s\<^isub>1, \,  wenzelm@20491  111  s\<^isub>k)"} such that a type scheme @{text  wenzelm@20494  112  "(\\<^bsub>s\<^isub>1\<^esub>, \, \\<^bsub>s\<^isub>k\<^esub>)\"} is  wenzelm@20491  113  of sort @{text "s"}. Consequently, the unification problem on the  wenzelm@20491  114  algebra of types has most general solutions (modulo renaming and  wenzelm@20491  115  equivalence of sorts). Moreover, the usual type-inference algorithm  wenzelm@20491  116  will produce primary types as expected \cite{nipkow-prehofer}.  wenzelm@20480  117 *}  wenzelm@20451  118 wenzelm@20480  119 text %mlref {*  wenzelm@20480  120  \begin{mldecls}  wenzelm@20480  121  @{index_ML_type class} \\  wenzelm@20480  122  @{index_ML_type sort} \\  wenzelm@20494  123  @{index_ML_type arity} \\  wenzelm@20480  124  @{index_ML_type typ} \\  wenzelm@20519  125  @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\  wenzelm@20494  126  @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\  wenzelm@20480  127  @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\  wenzelm@20480  128  @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\  wenzelm@20520  129  @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\  wenzelm@20480  130  @{index_ML Sign.add_tyabbrs_i: "  wenzelm@20520  131  (string * string list * typ * mixfix) list -> theory -> theory"} \\  wenzelm@20480  132  @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\  wenzelm@20480  133  @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\  wenzelm@20480  134  @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\  wenzelm@20480  135  \end{mldecls}  wenzelm@20480  136 wenzelm@20480  137  \begin{description}  wenzelm@20480  138 wenzelm@20480  139  \item @{ML_type class} represents type classes; this is an alias for  wenzelm@20480  140  @{ML_type string}.  wenzelm@20480  141 wenzelm@20480  142  \item @{ML_type sort} represents sorts; this is an alias for  wenzelm@20480  143  @{ML_type "class list"}.  wenzelm@20451  144 wenzelm@20480  145  \item @{ML_type arity} represents type arities; this is an alias for  wenzelm@20494  146  triples of the form @{text "(\, \<^vec>s, s)"} for @{text "\ ::  wenzelm@20480  147  (\<^vec>s)s"} described above.  wenzelm@20480  148 wenzelm@20480  149  \item @{ML_type typ} represents types; this is a datatype with  wenzelm@20480  150  constructors @{ML TFree}, @{ML TVar}, @{ML Type}.  wenzelm@20480  151 wenzelm@20519  152  \item @{ML map_atyps}~@{text "f \"} applies mapping @{text "f"} to  wenzelm@20519  153  all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text "\"}.  wenzelm@20519  154 wenzelm@20519  155  \item @{ML fold_atyps}~@{text "f \"} iterates operation @{text "f"}  wenzelm@20519  156  over all occurrences of atoms (@{ML TFree}, @{ML TVar}) in @{text  wenzelm@20494  157  "\"}; the type structure is traversed from left to right.  wenzelm@20494  158 wenzelm@20480  159  \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}  wenzelm@20480  160  tests the subsort relation @{text "s\<^isub>1 \ s\<^isub>2"}.  wenzelm@20480  161 wenzelm@20480  162  \item @{ML Sign.of_sort}~@{text "thy (\, s)"} tests whether a type  wenzelm@20491  163  is of a given sort.  wenzelm@20480  164 wenzelm@20494  165  \item @{ML Sign.add_types}~@{text "[(\, k, mx), \]"} declares new  wenzelm@20494  166  type constructors @{text "\"} with @{text "k"} arguments and  wenzelm@20480  167  optional mixfix syntax.  wenzelm@20451  168 wenzelm@20494  169  \item @{ML Sign.add_tyabbrs_i}~@{text "[(\, \<^vec>\, \, mx), \]"}  wenzelm@20494  170  defines a new type abbreviation @{text "(\<^vec>\)\ = \"} with  wenzelm@20491  171  optional mixfix syntax.  wenzelm@20480  172 wenzelm@20480  173  \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \,  wenzelm@20494  174  c\<^isub>n])"} declares new class @{text "c"}, together with class  wenzelm@20494  175  relations @{text "c \ c\<^isub>i"}, for @{text "i = 1, \, n"}.  wenzelm@20480  176 wenzelm@20480  177  \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,  wenzelm@20480  178  c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \  wenzelm@20480  179  c\<^isub>2"}.  wenzelm@20480  180 wenzelm@20494  181  \item @{ML Sign.primitive_arity}~@{text "(\, \<^vec>s, s)"} declares  wenzelm@20494  182  arity @{text "\ :: (\<^vec>s)s"}.  wenzelm@20480  183 wenzelm@20480  184  \end{description}  wenzelm@20437  185 *}  wenzelm@20437  186 wenzelm@20437  187 wenzelm@20480  188 wenzelm@20451  189 section {* Terms \label{sec:terms} *}  wenzelm@18537  190 wenzelm@18537  191 text {*  wenzelm@20451  192  \glossary{Term}{FIXME}  wenzelm@18537  193 wenzelm@20491  194  The language of terms is that of simply-typed @{text "\"}-calculus  wenzelm@20520  195  with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}  wenzelm@20520  196  or \cite{paulson-ml2}), and named free variables and constants.  wenzelm@20520  197  Terms with loose bound variables are usually considered malformed.  wenzelm@20520  198  The types of variables and constants is stored explicitly at each  wenzelm@20520  199  occurrence in the term.  wenzelm@20514  200 wenzelm@20514  201  \medskip A \emph{bound variable} is a natural number @{text "b"},  wenzelm@20514  202  which refers to the next binder that is @{text "b"} steps upwards  wenzelm@20514  203  from the occurrence of @{text "b"} (counting from zero). Bindings  wenzelm@20514  204  may be introduced as abstractions within the term, or as a separate  wenzelm@20514  205  context (an inside-out list). This associates each bound variable  wenzelm@20519  206  with a type. A \emph{loose variables} is a bound variable that is  wenzelm@20514  207  outside the current scope of local binders or the context. For  wenzelm@20514  208  example, the de-Bruijn term @{text "\\<^isub>\. \\<^isub>\. 1 + 0"}  wenzelm@20514  209  corresponds to @{text "\x\<^isub>\. \y\<^isub>\. x + y"} in a named  wenzelm@20514  210  representation. Also note that the very same bound variable may get  wenzelm@20514  211  different numbers at different occurrences.  wenzelm@20514  212 wenzelm@20514  213  A \emph{fixed variable} is a pair of a basic name and a type. For  wenzelm@20514  214  example, @{text "(x, \)"} which is usually printed @{text  wenzelm@20514  215  "x\<^isub>\"}. A \emph{schematic variable} is a pair of an  wenzelm@20514  216  indexname and a type. For example, @{text "((x, 0), \)"} which is  wenzelm@20514  217  usually printed as @{text "?x\<^isub>\"}.  wenzelm@20491  218 wenzelm@20514  219  \medskip A \emph{constant} is a atomic terms consisting of a basic  wenzelm@20514  220  name and a type. Constants are declared in the context as  wenzelm@20514  221  polymorphic families @{text "c :: \"}, meaning that any @{text  wenzelm@20514  222  "c\<^isub>\"} is a valid constant for all substitution instances  wenzelm@20514  223  @{text "\ \ \"}.  wenzelm@20514  224 wenzelm@20514  225  The list of \emph{type arguments} of @{text "c\<^isub>\"} wrt.\ the  wenzelm@20514  226  declaration @{text "c :: \"} is the codomain of the type matcher  wenzelm@20514  227  presented in canonical order (according to the left-to-right  wenzelm@20514  228  occurrences of type variables in in @{text "\"}). Thus @{text  wenzelm@20514  229  "c\<^isub>\"} can be represented more compactly as @{text  wenzelm@20514  230  "c(\\<^isub>1, \, \\<^isub>n)"}. For example, the instance @{text  wenzelm@20514  231  "plus\<^bsub>nat \ nat \ nat\<^esub>"} of some @{text "plus :: \ \ \  wenzelm@20514  232  \ \"} has the singleton list @{text "nat"} as type arguments, the  wenzelm@20514  233  constant may be represented as @{text "plus(nat)"}.  wenzelm@20480  234 wenzelm@20514  235  Constant declarations @{text "c :: \"} may contain sort constraints  wenzelm@20514  236  for type variables in @{text "\"}. These are observed by  wenzelm@20514  237  type-inference as expected, but \emph{ignored} by the core logic.  wenzelm@20514  238  This means the primitive logic is able to reason with instances of  wenzelm@20514  239  polymorphic constants that the user-level type-checker would reject.  wenzelm@20480  240 wenzelm@20514  241  \medskip A \emph{term} @{text "t"} is defined inductively over  wenzelm@20514  242  variables and constants, with abstraction and application as  wenzelm@20514  243  follows: @{text "t = b | x\<^isub>\ | ?x\<^isub>\ | c\<^isub>\ |  wenzelm@20514  244  \\<^isub>\. t | t\<^isub>1 t\<^isub>2"}. Parsing and printing takes  wenzelm@20514  245  care of converting between an external representation with named  wenzelm@20514  246  bound variables. Subsequently, we shall use the latter notation  wenzelm@20514  247  instead of internal de-Bruijn representation.  wenzelm@20498  248 wenzelm@20514  249  The subsequent inductive relation @{text "t :: \"} assigns a  wenzelm@20514  250  (unique) type to a term, using the special type constructor @{text  wenzelm@20514  251  "(\, \)fun"}, which is written @{text "\ \ \"}.  wenzelm@20498  252  $ wenzelm@20501  253  \infer{@{text "a\<^isub>\ :: \"}}{}  wenzelm@20498  254  \qquad  wenzelm@20501  255  \infer{@{text "(\x\<^sub>\. t) :: \ \ \"}}{@{text "t :: \"}}  wenzelm@20501  256  \qquad  wenzelm@20501  257  \infer{@{text "t u :: \"}}{@{text "t :: \ \ \"} & @{text "u :: \"}}  wenzelm@20498  258 $  wenzelm@20514  259  A \emph{well-typed term} is a term that can be typed according to these rules.  wenzelm@20498  260 wenzelm@20514  261  Typing information can be omitted: type-inference is able to  wenzelm@20514  262  reconstruct the most general type of a raw term, while assigning  wenzelm@20514  263  most general types to all of its variables and constants.  wenzelm@20514  264  Type-inference depends on a context of type constraints for fixed  wenzelm@20514  265  variables, and declarations for polymorphic constants.  wenzelm@20514  266 wenzelm@20514  267  The identity of atomic terms consists both of the name and the type.  wenzelm@20514  268  Thus different entities @{text "c\<^bsub>\\<^isub>1\<^esub>"} and  wenzelm@20514  269  @{text "c\<^bsub>\\<^isub>2\<^esub>"} may well identified by type  wenzelm@20514  270  instantiation, by mapping @{text "\\<^isub>1"} and @{text  wenzelm@20514  271  "\\<^isub>2"} to the same @{text "\"}. Although,  wenzelm@20514  272  different type instances of constants of the same basic name are  wenzelm@20514  273  commonplace, this rarely happens for variables: type-inference  wenzelm@20514  274  always demands consistent'' type constraints.  wenzelm@20514  275 wenzelm@20514  276  \medskip The \emph{hidden polymorphism} of a term @{text "t :: \"}  wenzelm@20514  277  is the set of type variables occurring in @{text "t"}, but not in  wenzelm@20514  278  @{text "\"}. This means that the term implicitly depends on the  wenzelm@20514  279  values of various type variables that are not visible in the overall  wenzelm@20514  280  type, i.e.\ there are different type instances @{text "t\  wenzelm@20514  281  :: \"} and @{text "t\' :: \"} with the same type. This  wenzelm@20514  282  slightly pathological situation is apt to cause strange effects.  wenzelm@20514  283 wenzelm@20514  284  \medskip A \emph{term abbreviation} is a syntactic definition @{text  wenzelm@20514  285  "c\<^isub>\ \ t"} of an arbitrary closed term @{text "t"} of type  wenzelm@20514  286  @{text "\"} without any hidden polymorphism. A term abbreviation  wenzelm@20514  287  looks like a constant at the surface, but is fully expanded before  wenzelm@20514  288  entering the logical core. Abbreviations are usually reverted when  wenzelm@20514  289  printing terms, using rules @{text "t \ c\<^isub>\"} has a  wenzelm@20514  290  higher-order term rewrite system.  wenzelm@20519  291 wenzelm@20519  292  \medskip Canonical operations on @{text "\"}-terms include @{text  wenzelm@20519  293  "\\\"}-conversion. @{text "\"}-conversion refers to capture-free  wenzelm@20519  294  renaming of bound variables; @{text "\"}-conversion contracts an  wenzelm@20519  295  abstraction applied to some argument term, substituting the argument  wenzelm@20519  296  in the body: @{text "(\x. b)a"} becomes @{text "b[a/x]"}; @{text  wenzelm@20519  297  "\"}-conversion contracts vacuous application-abstraction: @{text  wenzelm@20519  298  "\x. f x"} becomes @{text "f"}, provided that the bound variable  wenzelm@20519  299  @{text "0"} does not occur in @{text "f"}.  wenzelm@20519  300 wenzelm@20519  301  Terms are almost always treated module @{text "\"}-conversion, which  wenzelm@20519  302  is implicit in the de-Bruijn representation. The names in  wenzelm@20519  303  abstractions of bound variables are maintained only as a comment for  wenzelm@20519  304  parsing and printing. Full @{text "\\\"}-equivalence is usually  wenzelm@20519  305  taken for granted higher rules (\secref{sec:rules}), anything  wenzelm@20519  306  depending on higher-order unification or rewriting.  wenzelm@18537  307 *}  wenzelm@18537  308 wenzelm@20514  309 text %mlref {*  wenzelm@20514  310  \begin{mldecls}  wenzelm@20514  311  @{index_ML_type term} \\  wenzelm@20519  312  @{index_ML "op aconv": "term * term -> bool"} \\  wenzelm@20519  313  @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\ %FIXME rename map_types  wenzelm@20519  314  @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\  wenzelm@20514  315  @{index_ML map_aterms: "(term -> term) -> term -> term"} \\  wenzelm@20514  316  @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\  wenzelm@20514  317  @{index_ML fastype_of: "term -> typ"} \\  wenzelm@20519  318  @{index_ML lambda: "term -> term -> term"} \\  wenzelm@20519  319  @{index_ML betapply: "term * term -> term"} \\  wenzelm@20520  320  @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\  wenzelm@20519  321  @{index_ML Sign.add_abbrevs: "string * bool ->  wenzelm@20520  322  ((string * mixfix) * term) list -> theory -> theory"} \\  wenzelm@20519  323  @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\  wenzelm@20519  324  @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\  wenzelm@20514  325  \end{mldecls}  wenzelm@18537  326 wenzelm@20514  327  \begin{description}  wenzelm@18537  328 wenzelm@20519  329  \item @{ML_type term} represents de-Bruijn terms with comments in  wenzelm@20519  330  abstractions for bound variable names. This is a datatype with  wenzelm@20519  331  constructors @{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}, @{ML  wenzelm@20519  332  Abs}, @{ML "op \$"}.  wenzelm@20519  333 wenzelm@20519  334  \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text  wenzelm@20519  335  "\"}-equivalence of two terms. This is the basic equality relation  wenzelm@20519  336  on type @{ML_type term}; raw datatype equality should only be used  wenzelm@20519  337  for operations related to parsing or printing!  wenzelm@20519  338 wenzelm@20519  339  \item @{ML map_term_types}~@{text "f t"} applies mapping @{text "f"}  wenzelm@20519  340  to all types occurring in @{text "t"}.  wenzelm@20519  341 wenzelm@20519  342  \item @{ML fold_types}~@{text "f t"} iterates operation @{text "f"}  wenzelm@20519  343  over all occurrences of types in @{text "t"}; the term structure is  wenzelm@20519  344  traversed from left to right.  wenzelm@20519  345 wenzelm@20519  346  \item @{ML map_aterms}~@{text "f t"} applies mapping @{text "f"} to  wenzelm@20519  347  all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const})  wenzelm@20519  348  occurring in @{text "t"}.  wenzelm@20519  349 wenzelm@20519  350  \item @{ML fold_aterms}~@{text "f t"} iterates operation @{text "f"}  wenzelm@20519  351  over all occurrences of atomic terms in (@{ML Bound}, @{ML Free},  wenzelm@20519  352  @{ML Var}, @{ML Const}) @{text "t"}; the term structure is traversed  wenzelm@20519  353  from left to right.  wenzelm@20519  354 wenzelm@20519  355  \item @{ML fastype_of}~@{text "t"} recomputes the type of a  wenzelm@20519  356  well-formed term, while omitting any sanity checks. This operation  wenzelm@20519  357  is relatively slow.  wenzelm@20519  358 wenzelm@20519  359  \item @{ML lambda}~@{text "a b"} produces an abstraction @{text  wenzelm@20519  360  "\a. b"}, where occurrences of the original (atomic) term @{text  wenzelm@20520  361  "a"} in the body @{text "b"} are replaced by bound variables.  wenzelm@20519  362 wenzelm@20519  363  \item @{ML betapply}~@{text "t u"} produces an application @{text "t  wenzelm@20520  364  u"}, with topmost @{text "\"}-conversion if @{text "t"} happens to  wenzelm@20520  365  be an abstraction.  wenzelm@20519  366 wenzelm@20519  367  \item @{ML Sign.add_consts_i}~@{text "[(c, \, mx), \]"} declares a  wenzelm@20519  368  new constant @{text "c :: \"} with optional mixfix syntax.  wenzelm@20519  369 wenzelm@20519  370  \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \]"}  wenzelm@20519  371  declares a new term abbreviation @{text "c \ t"} with optional  wenzelm@20519  372  mixfix syntax.  wenzelm@20519  373 wenzelm@20520  374  \item @{ML Sign.const_typargs}~@{text "thy (c, \)"} and @{ML  wenzelm@20520  375  Sign.const_instance}~@{text "thy (c, [\\<^isub>1, \, \\<^isub>n])"}  wenzelm@20520  376  convert between the two representations of constants, namely full  wenzelm@20520  377  type instance vs.\ compact type arguments form (depending on the  wenzelm@20520  378  most general declaration given in the context).  wenzelm@18537  379 wenzelm@20514  380  \end{description}  wenzelm@18537  381 *}  wenzelm@18537  382 wenzelm@18537  383 wenzelm@20451  384 section {* Theorems \label{sec:thms} *}  wenzelm@18537  385 wenzelm@18537  386 text {*  wenzelm@20521  387  \glossary{Proposition}{FIXME A \seeglossary{term} of  wenzelm@20521  388  \seeglossary{type} @{text "prop"}. Internally, there is nothing  wenzelm@20521  389  special about propositions apart from their type, but the concrete  wenzelm@20521  390  syntax enforces a clear distinction. Propositions are structured  wenzelm@20521  391  via implication @{text "A \ B"} or universal quantification @{text  wenzelm@20521  392  "\x. B x"} --- anything else is considered atomic. The canonical  wenzelm@20521  393  form for propositions is that of a \seeglossary{Hereditary Harrop  wenzelm@20521  394  Formula}. FIXME}  wenzelm@20480  395 wenzelm@20501  396  \glossary{Theorem}{A proven proposition within a certain theory and  wenzelm@20501  397  proof context, formally @{text "\ \\<^sub>\ \"}; both contexts are  wenzelm@20501  398  rarely spelled out explicitly. Theorems are usually normalized  wenzelm@20501  399  according to the \seeglossary{HHF} format. FIXME}  wenzelm@20480  400 wenzelm@20519  401  \glossary{Fact}{Sometimes used interchangeably for  wenzelm@20501  402  \seeglossary{theorem}. Strictly speaking, a list of theorems,  wenzelm@20501  403  essentially an extra-logical conjunction. Facts emerge either as  wenzelm@20501  404  local assumptions, or as results of local goal statements --- both  wenzelm@20501  405  may be simultaneous, hence the list representation. FIXME}  wenzelm@18537  406 wenzelm@20501  407  \glossary{Schematic variable}{FIXME}  wenzelm@20501  408 wenzelm@20501  409  \glossary{Fixed variable}{A variable that is bound within a certain  wenzelm@20501  410  proof context; an arbitrary-but-fixed entity within a portion of  wenzelm@20501  411  proof text. FIXME}  wenzelm@18537  412 wenzelm@20501  413  \glossary{Free variable}{Synonymous for \seeglossary{fixed  wenzelm@20501  414  variable}. FIXME}  wenzelm@20501  415 wenzelm@20501  416  \glossary{Bound variable}{FIXME}  wenzelm@18537  417 wenzelm@20501  418  \glossary{Variable}{See \seeglossary{schematic variable},  wenzelm@20501  419  \seeglossary{fixed variable}, \seeglossary{bound variable}, or  wenzelm@20501  420  \seeglossary{type variable}. The distinguishing feature of  wenzelm@20501  421  different variables is their binding scope. FIXME}  wenzelm@18537  422 wenzelm@20521  423  A \emph{proposition} is a well-formed term of type @{text "prop"}, a  wenzelm@20521  424  \emph{theorem} is a proven proposition (depending on a context of  wenzelm@20521  425  hypotheses and the background theory). Primitive inferences include  wenzelm@20521  426  plain natural deduction rules for the primary connectives @{text  wenzelm@20521  427  "\"} and @{text "\"} of the framework. There are separate (derived)  wenzelm@20521  428  rules for equality/equivalence @{text "\"} and internal conjunction  wenzelm@20521  429  @{text "&"}.  wenzelm@20521  430 *}  wenzelm@20521  431 wenzelm@20521  432 subsection {* Standard connectives and rules *}  wenzelm@18537  433 wenzelm@20521  434 text {*  wenzelm@20521  435  The basic theory is called @{text "Pure"}, it contains declarations  wenzelm@20521  436  for the standard logical connectives @{text "\"}, @{text "\"}, and  wenzelm@20521  437  @{text "\"} of the framework, see \figref{fig:pure-connectives}.  wenzelm@20521  438  The derivability judgment @{text "A\<^isub>1, \, A\<^isub>n \ B"} is  wenzelm@20521  439  defined inductively by the primitive inferences given in  wenzelm@20521  440  \figref{fig:prim-rules}, with the global syntactic restriction that  wenzelm@20521  441  hypotheses may never contain schematic variables. The builtin  wenzelm@20521  442  equality is conceptually axiomatized shown in  wenzelm@20521  443  \figref{fig:pure-equality}, although the implementation works  wenzelm@20521  444  directly with (derived) inference rules.  wenzelm@20521  445 wenzelm@20521  446  \begin{figure}[htb]  wenzelm@20521  447  \begin{center}  wenzelm@20501  448  \begin{tabular}{ll}  wenzelm@20501  449  @{text "all :: (\ \ prop) \ prop"} & universal quantification (binder @{text "\"}) \\  wenzelm@20501  450  @{text "\ :: prop \ prop \ prop"} & implication (right associative infix) \\  wenzelm@20521  451  @{text "\ :: \ \ \ \ prop"} & equality relation (infix) \\  wenzelm@20501  452  \end{tabular}  wenzelm@20521  453  \caption{Standard connectives of Pure}\label{fig:pure-connectives}  wenzelm@20521  454  \end{center}  wenzelm@20521  455  \end{figure}  wenzelm@18537  456 wenzelm@20501  457  \begin{figure}[htb]  wenzelm@20501  458  \begin{center}  wenzelm@20498  459  $ wenzelm@20498  460  \infer[@{text "(axiom)"}]{@{text "\ A"}}{@{text "A \ \"}}  wenzelm@20498  461  \qquad  wenzelm@20498  462  \infer[@{text "(assume)"}]{@{text "A \ A"}}{}  wenzelm@20498  463 $  wenzelm@20498  464  $ wenzelm@20498  465  \infer[@{text "(\_intro)"}]{@{text "\ \ \x. b x"}}{@{text "\ \ b x"} & @{text "x \ \"}}  wenzelm@20498  466  \qquad  wenzelm@20498  467  \infer[@{text "(\_elim)"}]{@{text "\ \ b a"}}{@{text "\ \ \x. b x"}}  wenzelm@20498  468 $  wenzelm@20498  469  $ wenzelm@20498  470  \infer[@{text "(\_intro)"}]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}}  wenzelm@20498  471  \qquad  wenzelm@20498  472  \infer[@{text "(\_elim)"}]{@{text "\\<^sub>1 \ \\<^sub>2 \ B"}}{@{text "\\<^sub>1 \ A \ B"} & @{text "\\<^sub>2 \ A"}}  wenzelm@20498  473 $  wenzelm@20521  474  \caption{Primitive inferences of Pure}\label{fig:prim-rules}  wenzelm@20521  475  \end{center}  wenzelm@20521  476  \end{figure}  wenzelm@20521  477 wenzelm@20521  478  \begin{figure}[htb]  wenzelm@20521  479  \begin{center}  wenzelm@20521  480  \begin{tabular}{ll}  wenzelm@20521  481  @{text "\ (\x. b x) a \ b a"} & @{text "\"}-conversion \\  wenzelm@20521  482  @{text "\ x \ x"} & reflexivity \\  wenzelm@20521  483  @{text "\ x \ y \ P x \ P y"} & substitution \\  wenzelm@20521  484  @{text "\ (\x. f x \ g x) \ f \ g"} & extensionality \\  wenzelm@20521  485  @{text "\ (A \ B) \ (B \ A) \ A \ B"} & coincidence with equivalence \\  wenzelm@20521  486  \end{tabular}  wenzelm@20521  487  \caption{Conceptual axiomatization of builtin equality}\label{fig:pure-equality}  wenzelm@20501  488  \end{center}  wenzelm@20501  489  \end{figure}  wenzelm@18537  490 wenzelm@20501  491  The introduction and elimination rules for @{text "\"} and @{text  wenzelm@20501  492  "\"} are analogous to formation of (dependently typed) @{text  wenzelm@20501  493  "\"}-terms representing the underlying proof objects. Proof terms  wenzelm@20501  494  are \emph{irrelevant} in the Pure logic, they may never occur within  wenzelm@20521  495  propositions, i.e.\ the @{text "\"} arrow is non-dependent. The  wenzelm@20521  496  system provides a runtime option to record explicit proof terms for  wenzelm@20521  497  primitive inferences, cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}. Thus  wenzelm@20521  498  the three-fold @{text "\"}-structure can be made explicit.  wenzelm@20491  499 wenzelm@20521  500  Observe that locally fixed parameters (as used in rule @{text  wenzelm@20521  501  "\_intro"}) need not be recorded in the hypotheses, because the  wenzelm@20521  502  simple syntactic types of Pure are always inhabitable. The typing  wenzelm@20521  503  assumption'' @{text "x :: \"} is logically vacuous, it disappears  wenzelm@20521  504  automatically whenever the statement body ceases to mention variable  wenzelm@20521  505  @{text "x\<^isub>\"}.\footnote{This greatly simplifies many basic  wenzelm@20521  506  reasoning steps, and is the key difference to the formulation of  wenzelm@20521  507  this logic as @{text "\HOL"}'' in the PTS framework  wenzelm@20521  508  \cite{Barendregt-Geuvers:2001}.}  wenzelm@20501  509 wenzelm@20521  510  \medskip FIXME @{text "\\\"}-equivalence and primitive definitions  wenzelm@20521  511 wenzelm@20521  512  Since the basic representation of terms already accounts for @{text  wenzelm@20521  513  "\"}-conversion, Pure equality essentially acts like @{text  wenzelm@20521  514  "\\\"}-equivalence on terms, while coinciding with bi-implication.  wenzelm@20501  515 wenzelm@20501  516  \medskip The axiomatization of a theory is implicitly closed by  wenzelm@20520  517  forming all instances of type and term variables: @{text "\ A\"} for  wenzelm@20514  518  any substitution instance of axiom @{text "\ A"}. By pushing  wenzelm@20501  519  substitution through derivations inductively, we get admissible  wenzelm@20501  520  substitution rules for theorems shown in \figref{fig:subst-rules}.  wenzelm@20521  521  Alternatively, the term substitution rules could be derived from  wenzelm@20521  522  @{text "\_intro/elim"}. The versions for types are genuine  wenzelm@20521  523  admissible rules, due to the lack of true polymorphism in the logic.  wenzelm@20501  524 wenzelm@20501  525  \begin{figure}[htb]  wenzelm@20501  526  \begin{center}  wenzelm@20498  527  $ wenzelm@20501  528  \infer{@{text "\ \ B[?$"}}{@{text "\ \ B[\]"} & @{text "\ \ \"}}  wenzelm@20501  529  \quad  wenzelm@20501  530  \infer[\quad@{text "(generalize)"}]{@{text "\ \ B[?x]"}}{@{text "\ \ B[x]"} & @{text "x \ \"}}  wenzelm@20498  531  \]  wenzelm@20498  532  $ wenzelm@20501  533  \infer{@{text "\ \ B[$"}}{@{text "\ \ B[?\]"}}  wenzelm@20501  534  \quad  wenzelm@20501  535  \infer[\quad@{text "(instantiate)"}]{@{text "\ \ B[t]"}}{@{text "\ \ B[?x]"}}  wenzelm@20498  536  \]  wenzelm@20501  537  \caption{Admissible substitution rules}\label{fig:subst-rules}  wenzelm@20501  538  \end{center}  wenzelm@20501  539  \end{figure}  wenzelm@18537  540 wenzelm@20501  541  Since @{text "\"} may never contain any schematic variables, the  wenzelm@20501  542  @{text "instantiate"} do not require an explicit side-condition. In  wenzelm@20501  543  principle, variables could be substituted in hypotheses as well, but  wenzelm@20501  544  this could disrupt monotonicity of the basic calculus: derivations  wenzelm@20501  545  could leave the current proof context.  wenzelm@20521  546 *}  wenzelm@20498  547 wenzelm@20521  548 text %mlref {*  wenzelm@20521  549  \begin{mldecls}  wenzelm@20521  550  @{index_ML_type ctyp} \\  wenzelm@20521  551  @{index_ML_type cterm} \\  wenzelm@20521  552  @{index_ML_type thm} \\  wenzelm@20521  553  \end{mldecls}  wenzelm@20521  554 wenzelm@20521  555  \begin{description}  wenzelm@20521  556 wenzelm@20521  557  \item @{ML_type ctyp} FIXME  wenzelm@20521  558 wenzelm@20521  559  \item @{ML_type cterm} FIXME  wenzelm@20521  560 wenzelm@20521  561  \item @{ML_type thm} FIXME  wenzelm@20521  562 wenzelm@20521  563  \end{description}  wenzelm@20521  564 *}  wenzelm@20521  565 wenzelm@20521  566 wenzelm@20521  567 subsection {* Auxiliary connectives *}  wenzelm@20521  568 wenzelm@20521  569 text {*  wenzelm@20521  570  Pure also provides various auxiliary connectives based on primitive  wenzelm@20521  571  definitions, see \figref{fig:pure-aux}. These are normally not  wenzelm@20521  572  exposed to the user, but appear in internal encodings only.  wenzelm@20501  573 wenzelm@20501  574  \begin{figure}[htb]  wenzelm@20501  575  \begin{center}  wenzelm@20498  576  \begin{tabular}{ll}  wenzelm@20521  577  @{text "conjunction :: prop \ prop \ prop"} & (infix @{text "&"}) \\  wenzelm@20521  578  @{text "\ A & B \ (\C. (A \ B \ C) \ C)"} \$1ex]  wenzelm@20521  579  @{text "prop :: prop \ prop"} & (prefix @{text "#"}) \\  wenzelm@20521  580  @{text "#A \ A"} \\[1ex]  wenzelm@20521  581  @{text "term :: \ \ prop"} & (prefix @{text "TERM"}) \\  wenzelm@20521  582  @{text "term x \ (\A. A \ A)"} \\[1ex]  wenzelm@20521  583  @{text "TYPE :: \ itself"} & (prefix @{text "TYPE"}) \\  wenzelm@20521  584  @{text "(unspecified)"} \\  wenzelm@20498  585  \end{tabular}  wenzelm@20521  586  \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}  wenzelm@20501  587  \end{center}  wenzelm@20501  588  \end{figure}  wenzelm@20501  589 wenzelm@20521  590  Conjunction as an explicit connective allows to treat both  wenzelm@20521  591  simultaneous assumptions and conclusions uniformly. The definition  wenzelm@20521  592  allows to derive the usual introduction @{text "\ A \ B \ A & B"},  wenzelm@20521  593  and destructions @{text "A & B \ A"} and @{text "A & B \ B"}. For  wenzelm@20521  594  example, several claims may be stated at the same time, which is  wenzelm@20521  595  intermediately represented as an assumption, but the user only  wenzelm@20521  596  encounters several sub-goals, and several resulting facts in the  wenzelm@20521  597  very end (cf.\ \secref{sec:tactical-goals}).  wenzelm@20498  598 wenzelm@20521  599  The @{text "#"} marker allows complex propositions (nested @{text  wenzelm@20521  600  "\"} and @{text "\"}) to appear formally as atomic, without changing  wenzelm@20521  601  the meaning: @{text "\ \ A"} and @{text "\ \ #A"} are  wenzelm@20521  602  interchangeable. See \secref{sec:tactical-goals} for specific  wenzelm@20521  603  operations.  wenzelm@20521  604 wenzelm@20521  605  The @{text "TERM"} marker turns any well-formed term into a  wenzelm@20521  606  derivable proposition: @{text "\ TERM t"} holds  wenzelm@20521  607  unconditionally. Despite its logically vacous meaning, this is  wenzelm@20521  608  occasionally useful to treat syntactic terms and proven propositions  wenzelm@20521  609  uniformly, as in a type-theoretic framework.  wenzelm@20498  610 wenzelm@20521  611  The @{text "TYPE"} constructor (which is the canonical  wenzelm@20521  612  representative of the unspecified type @{text "\ itself"}) injects  wenzelm@20521  613  the language of types into that of terms. There is specific  wenzelm@20521  614  notation @{text "TYPE(\)"} for @{text "TYPE\<^bsub>\  wenzelm@20521  615  itself\<^esub>"}.  wenzelm@20521  616  Although being devoid of any particular meaning, the term @{text  wenzelm@20521  617  "TYPE(\)"} is able to carry the type @{text "\"} formally. @{text  wenzelm@20521  618  "TYPE(\)"} may be used as an additional formal argument in primitive  wenzelm@20521  619  definitions, in order to avoid hidden polymorphism (cf.\  wenzelm@20521  620  \secref{sec:terms}). For example, @{text "c TYPE(\) \ A[$"} turns  wenzelm@20521  621  out as a formally correct definition of some proposition @{text "A"}  wenzelm@20521  622  that depends on an additional type argument.  wenzelm@20521  623 *}  wenzelm@20501  624 wenzelm@20521  625 text %mlref {*  wenzelm@20521  626  \begin{mldecls}  wenzelm@20521  627  @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\  wenzelm@20521  628  @{index_ML Conjunction.elim: "thm -> thm * thm"} \\  wenzelm@20521  629  @{index_ML Drule.mk_term: "cterm -> thm"} \\  wenzelm@20521  630  @{index_ML Drule.dest_term: "thm -> cterm"} \\  wenzelm@20521  631  @{index_ML Logic.mk_type: "typ -> term"} \\  wenzelm@20521  632  @{index_ML Logic.dest_type: "term -> typ"} \\  wenzelm@20521  633  \end{mldecls}  wenzelm@20521  634 wenzelm@20521  635  \begin{description}  wenzelm@20521  636 wenzelm@20521  637  \item FIXME  wenzelm@20521  638 wenzelm@20521  639  \end{description}  wenzelm@20491  640 *}  wenzelm@18537  641 wenzelm@20480  642 wenzelm@20491  643 section {* Rules \label{sec:rules} *}  wenzelm@18537  644 wenzelm@18537  645 text {*  wenzelm@18537  646 wenzelm@18537  647 FIXME  wenzelm@18537  648 wenzelm@20491  649  A \emph{rule} is any Pure theorem in HHF normal form; there is a  wenzelm@20491  650  separate calculus for rule composition, which is modeled after  wenzelm@20491  651  Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows  wenzelm@20491  652  rules to be nested arbitrarily, similar to \cite{extensions91}.  wenzelm@20491  653 wenzelm@20491  654  Normally, all theorems accessible to the user are proper rules.  wenzelm@20491  655  Low-level inferences are occasional required internally, but the  wenzelm@20491  656  result should be always presented in canonical form. The higher  wenzelm@20491  657  interfaces of Isabelle/Isar will always produce proper rules. It is  wenzelm@20491  658  important to maintain this invariant in add-on applications!  wenzelm@20491  659 wenzelm@20491  660  There are two main principles of rule composition: @{text  wenzelm@20491  661  "resolution"} (i.e.\ backchaining of rules) and @{text  wenzelm@20491  662  "by-assumption"} (i.e.\ closing a branch); both principles are  wenzelm@20519  663  combined in the variants of @{text "elim-resolution"} and @{text  wenzelm@20491  664  "dest-resolution"}. Raw @{text "composition"} is occasionally  wenzelm@20491  665  useful as well, also it is strictly speaking outside of the proper  wenzelm@20491  666  rule calculus.  wenzelm@20491  667 wenzelm@20491  668  Rules are treated modulo general higher-order unification, which is  wenzelm@20491  669  unification modulo the equational theory of @{text "\\\"}-conversion  wenzelm@20491  670  on @{text "\"}-terms. Moreover, propositions are understood modulo  wenzelm@20491  671  the (derived) equivalence @{text "(A \ (\x. B x)) \ (\x. A \ B x)"}.  wenzelm@20491  672 wenzelm@20491  673  This means that any operations within the rule calculus may be  wenzelm@20491  674  subject to spontaneous @{text "\\\"}-HHF conversions. It is common  wenzelm@20491  675  practice not to contract or expand unnecessarily. Some mechanisms  wenzelm@20491  676  prefer an one form, others the opposite, so there is a potential  wenzelm@20491  677  danger to produce some oscillation!  wenzelm@20491  678 wenzelm@20491  679  Only few operations really work \emph{modulo} HHF conversion, but  wenzelm@20491  680  expect a normal form: quantifiers @{text "\"} before implications  wenzelm@20491  681  @{text "\"} at each level of nesting.  wenzelm@20491  682 wenzelm@18537  683 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF  wenzelm@18537  684 format is defined inductively as @{text "H = (\x\<^sup>*. H\<^sup>* \  wenzelm@18537  685 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.  wenzelm@18537  686 Any proposition may be put into HHF form by normalizing with the rule  wenzelm@18537  687 @{text "(A \ (\x. B x)) \ (\x. A \ B x)"}. In Isabelle, the outermost  wenzelm@18537  688 quantifier prefix is represented via \seeglossary{schematic  wenzelm@18537  689 variables}, such that the top-level structure is merely that of a  wenzelm@18537  690 \seeglossary{Horn Clause}}.  wenzelm@18537  691 wenzelm@18537  692 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}  wenzelm@18537  693 wenzelm@20498  694 wenzelm@20498  695  $ wenzelm@20498  696  \infer[@{text "(assumption)"}]{@{text "C\"}}  wenzelm@20498  697  {@{text "(\\<^vec>x. \<^vec>H \<^vec>x \ A \<^vec>x) \ C"} & @{text "A\ = H\<^sub>i\"}~~\text{(for some~@{text i})}}  wenzelm@20498  698 $  wenzelm@20498  699 wenzelm@20498  700 wenzelm@20498  701  $ wenzelm@20498  702  \infer[@{text "(compose)"}]{@{text "\<^vec>A\ \ C\"}}  wenzelm@20498  703  {@{text "\<^vec>A \ B"} & @{text "B' \ C"} & @{text "B\ = B'\"}}  wenzelm@20498  704 $  wenzelm@20498  705 wenzelm@20498  706 wenzelm@20498  707  $ wenzelm@20498  708  \infer[@{text "(\_lift)"}]{@{text "(\\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \ (\\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \ B ?\<^vec>a"}}  wenzelm@20498  709 $  wenzelm@20498  710  $ wenzelm@20498  711  \infer[@{text "(\_lift)"}]{@{text "(\<^vec>H \ \<^vec>A) \ (\<^vec>H \ B)"}}{@{text "\<^vec>A \ B"}}  wenzelm@20498  712 $  wenzelm@20498  713 wenzelm@20498  714  The @{text resolve} scheme is now acquired from @{text "\_lift"},  wenzelm@20498  715  @{text "\_lift"}, and @{text compose}.  wenzelm@20498  716 wenzelm@20498  717  $ wenzelm@20498  718  \infer[@{text "(resolution)"}]  wenzelm@20498  719  {@{text "(\\<^vec>x. \<^vec>H \<^vec>x \ \<^vec>A (?\<^vec>a \<^vec>x))\ \ C\"}}  wenzelm@20498  720  {\begin{tabular}{l}  wenzelm@20498  721  @{text "\<^vec>A ?\<^vec>a \ B ?\<^vec>a"} \\  wenzelm@20498  722  @{text "(\\<^vec>x. \<^vec>H \<^vec>x \ B' \<^vec>x) \ C"} \\  wenzelm@20498  723  @{text "(\\<^vec>x. B (?\<^vec>a \<^vec>x))\ = B'\"} \\  wenzelm@20498  724  \end{tabular}}  wenzelm@20498  725 $  wenzelm@20498  726 wenzelm@20498  727 wenzelm@20498  728  FIXME @{text "elim_resolution"}, @{text "dest_resolution"}  wenzelm@18537  729 *}  wenzelm@18537  730 wenzelm@20498  731 wenzelm@18537  732 end