doc-src/IsarImplementation/Thy/Logic.thy
author wenzelm
Thu Mar 05 19:48:02 2009 +0100 (2009-03-05)
changeset 30288 a32700e45ab3
parent 30272 2d612824e642
child 30355 8066d80cd51e
permissions -rw-r--r--
Thm.add_oracle interface: replaced old bstring by binding;
     1 theory Logic
     2 imports Base
     3 begin
     4 
     5 chapter {* Primitive logic \label{ch:logic} *}
     6 
     7 text {*
     8   The logical foundations of Isabelle/Isar are that of the Pure logic,
     9   which has been introduced as a Natural Deduction framework in
    10   \cite{paulson700}.  This is essentially the same logic as ``@{text
    11   "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)
    12   \cite{Barendregt-Geuvers:2001}, although there are some key
    13   differences in the specific treatment of simple types in
    14   Isabelle/Pure.
    15 
    16   Following type-theoretic parlance, the Pure logic consists of three
    17   levels of @{text "\<lambda>"}-calculus with corresponding arrows, @{text
    18   "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
    19   "\<And>"} for universal quantification (proofs depending on terms), and
    20   @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
    21 
    22   Derivations are relative to a logical theory, which declares type
    23   constructors, constants, and axioms.  Theory declarations support
    24   schematic polymorphism, which is strictly speaking outside the
    25   logic.\footnote{This is the deeper logical reason, why the theory
    26   context @{text "\<Theta>"} is separate from the proof context @{text "\<Gamma>"}
    27   of the core calculus.}
    28 *}
    29 
    30 
    31 section {* Types \label{sec:types} *}
    32 
    33 text {*
    34   The language of types is an uninterpreted order-sorted first-order
    35   algebra; types are qualified by ordered type classes.
    36 
    37   \medskip A \emph{type class} is an abstract syntactic entity
    38   declared in the theory context.  The \emph{subclass relation} @{text
    39   "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
    40   generating relation; the transitive closure is maintained
    41   internally.  The resulting relation is an ordering: reflexive,
    42   transitive, and antisymmetric.
    43 
    44   A \emph{sort} is a list of type classes written as @{text "s =
    45   {c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
    46   intersection.  Notationally, the curly braces are omitted for
    47   singleton intersections, i.e.\ any class @{text "c"} may be read as
    48   a sort @{text "{c}"}.  The ordering on type classes is extended to
    49   sorts according to the meaning of intersections: @{text
    50   "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff
    51   @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}.  The empty intersection
    52   @{text "{}"} refers to the universal sort, which is the largest
    53   element wrt.\ the sort order.  The intersections of all (finitely
    54   many) classes declared in the current theory are the minimal
    55   elements wrt.\ the sort order.
    56 
    57   \medskip A \emph{fixed type variable} is a pair of a basic name
    58   (starting with a @{text "'"} character) and a sort constraint, e.g.\
    59   @{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^isub>s"}.
    60   A \emph{schematic type variable} is a pair of an indexname and a
    61   sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually
    62   printed as @{text "?\<alpha>\<^isub>s"}.
    63 
    64   Note that \emph{all} syntactic components contribute to the identity
    65   of type variables, including the sort constraint.  The core logic
    66   handles type variables with the same name but different sorts as
    67   different, although some outer layers of the system make it hard to
    68   produce anything like this.
    69 
    70   A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
    71   on types declared in the theory.  Type constructor application is
    72   written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.  For
    73   @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}
    74   instead of @{text "()prop"}.  For @{text "k = 1"} the parentheses
    75   are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.
    76   Further notation is provided for specific constructors, notably the
    77   right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
    78   \<beta>)fun"}.
    79   
    80   A \emph{type} is defined inductively over type variables and type
    81   constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
    82   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}.
    83 
    84   A \emph{type abbreviation} is a syntactic definition @{text
    85   "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
    86   variables @{text "\<^vec>\<alpha>"}.  Type abbreviations appear as type
    87   constructors in the syntax, but are expanded before entering the
    88   logical core.
    89 
    90   A \emph{type arity} declares the image behavior of a type
    91   constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,
    92   s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is
    93   of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is
    94   of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
    95   completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
    96   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
    97 
    98   \medskip The sort algebra is always maintained as \emph{coregular},
    99   which means that type arities are consistent with the subclass
   100   relation: for any type constructor @{text "\<kappa>"}, and classes @{text
   101   "c\<^isub>1 \<subseteq> c\<^isub>2"}, and arities @{text "\<kappa> ::
   102   (\<^vec>s\<^isub>1)c\<^isub>1"} and @{text "\<kappa> ::
   103   (\<^vec>s\<^isub>2)c\<^isub>2"} holds @{text "\<^vec>s\<^isub>1 \<subseteq>
   104   \<^vec>s\<^isub>2"} component-wise.
   105 
   106   The key property of a coregular order-sorted algebra is that sort
   107   constraints can be solved in a most general fashion: for each type
   108   constructor @{text "\<kappa>"} and sort @{text "s"} there is a most general
   109   vector of argument sorts @{text "(s\<^isub>1, \<dots>, s\<^isub>k)"} such
   110   that a type scheme @{text "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
   111   \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is of sort @{text "s"}.
   112   Consequently, type unification has most general solutions (modulo
   113   equivalence of sorts), so type-inference produces primary types as
   114   expected \cite{nipkow-prehofer}.
   115 *}
   116 
   117 text %mlref {*
   118   \begin{mldecls}
   119   @{index_ML_type class} \\
   120   @{index_ML_type sort} \\
   121   @{index_ML_type arity} \\
   122   @{index_ML_type typ} \\
   123   @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
   124   @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
   125   \end{mldecls}
   126   \begin{mldecls}
   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 the 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 section {* Terms \label{sec:terms} *}
   190 
   191 text {*
   192   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
   193   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
   194   or \cite{paulson-ml2}), with the types being determined by the
   195   corresponding binders.  In contrast, free variables and constants
   196   are have an explicit name and type in each occurrence.
   197 
   198   \medskip A \emph{bound variable} is a natural number @{text "b"},
   199   which accounts for the number of intermediate binders between the
   200   variable occurrence in the body and its binding position.  For
   201   example, the de-Bruijn term @{text
   202   "\<lambda>\<^bsub>nat\<^esub>. \<lambda>\<^bsub>nat\<^esub>. 1 + 0"} would
   203   correspond to @{text
   204   "\<lambda>x\<^bsub>nat\<^esub>. \<lambda>y\<^bsub>nat\<^esub>. x + y"} in a named
   205   representation.  Note that a bound variable may be represented by
   206   different de-Bruijn indices at different occurrences, depending on
   207   the nesting of abstractions.
   208 
   209   A \emph{loose variable} is a bound variable that is outside the
   210   scope of local binders.  The types (and names) for loose variables
   211   can be managed as a separate context, that is maintained as a stack
   212   of hypothetical binders.  The core logic operates on closed terms,
   213   without any loose variables.
   214 
   215   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
   216   @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}.  A
   217   \emph{schematic variable} is a pair of an indexname and a type,
   218   e.g.\ @{text "((x, 0), \<tau>)"} which is usually printed as @{text
   219   "?x\<^isub>\<tau>"}.
   220 
   221   \medskip A \emph{constant} is a pair of a basic name and a type,
   222   e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text
   223   "c\<^isub>\<tau>"}.  Constants are declared in the context as polymorphic
   224   families @{text "c :: \<sigma>"}, meaning that all substitution instances
   225   @{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
   226 
   227   The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"}
   228   wrt.\ the declaration @{text "c :: \<sigma>"} is defined as the codomain of
   229   the matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>,
   230   ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in canonical order @{text
   231   "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  Within a given theory context,
   232   there is a one-to-one correspondence between any constant @{text
   233   "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, \<dots>,
   234   \<tau>\<^isub>n)"} of its type arguments.  For example, with @{text "plus
   235   :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow>
   236   nat\<^esub>"} corresponds to @{text "plus(nat)"}.
   237 
   238   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
   239   for type variables in @{text "\<sigma>"}.  These are observed by
   240   type-inference as expected, but \emph{ignored} by the core logic.
   241   This means the primitive logic is able to reason with instances of
   242   polymorphic constants that the user-level type-checker would reject
   243   due to violation of type class restrictions.
   244 
   245   \medskip An \emph{atomic} term is either a variable or constant.  A
   246   \emph{term} is defined inductively over atomic terms, with
   247   abstraction and application as follows: @{text "t = b | x\<^isub>\<tau> |
   248   ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.
   249   Parsing and printing takes care of converting between an external
   250   representation with named bound variables.  Subsequently, we shall
   251   use the latter notation instead of internal de-Bruijn
   252   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   contrast, mixed instances of polymorphic constants occur frequently.
   279 
   280   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
   281   is the set of type variables occurring in @{text "t"}, but not in
   282   @{text "\<sigma>"}.  This means that the term implicitly depends on type
   283   arguments that are not accounted in the result type, i.e.\ there are
   284   different type instances @{text "t\<vartheta> :: \<sigma>"} and @{text
   285   "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly
   286   pathological situation notoriously demands additional care.
   287 
   288   \medskip A \emph{term abbreviation} is a syntactic definition @{text
   289   "c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},
   290   without any hidden polymorphism.  A term abbreviation looks like a
   291   constant in the syntax, but is expanded before entering the logical
   292   core.  Abbreviations are usually reverted when printing terms, using
   293   @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higher-order rewriting.
   294 
   295   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
   296   "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free
   297   renaming of bound variables; @{text "\<beta>"}-conversion contracts an
   298   abstraction applied to an argument term, substituting the argument
   299   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
   300   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
   301   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
   302   does not occur in @{text "f"}.
   303 
   304   Terms are normally treated modulo @{text "\<alpha>"}-conversion, which is
   305   implicit in the de-Bruijn representation.  Names for bound variables
   306   in abstractions are maintained separately as (meaningless) comments,
   307   mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is
   308   commonplace in various standard operations (\secref{sec:obj-rules})
   309   that are based on higher-order unification and matching.
   310 *}
   311 
   312 text %mlref {*
   313   \begin{mldecls}
   314   @{index_ML_type term} \\
   315   @{index_ML "op aconv": "term * term -> bool"} \\
   316   @{index_ML map_types: "(typ -> typ) -> term -> term"} \\
   317   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   318   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
   319   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   320   \end{mldecls}
   321   \begin{mldecls}
   322   @{index_ML fastype_of: "term -> typ"} \\
   323   @{index_ML lambda: "term -> term -> term"} \\
   324   @{index_ML betapply: "term * term -> term"} \\
   325   @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->
   326   theory -> term * theory"} \\
   327   @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->
   328   theory -> (term * term) * 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_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.declare_const}~@{text "properties ((c, \<sigma>), mx)"}
   374   declares a new constant @{text "c :: \<sigma>"} with optional mixfix
   375   syntax.
   376 
   377   \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
   378   introduces a new term abbreviation @{text "c \<equiv> t"}.
   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 two representations of polymorphic constants: full
   383   type instance vs.\ compact type arguments form.
   384 
   385   \end{description}
   386 *}
   387 
   388 
   389 section {* Theorems \label{sec:thms} *}
   390 
   391 text {*
   392   A \emph{proposition} is a well-typed term of type @{text "prop"}, a
   393   \emph{theorem} is a proven proposition (depending on a context of
   394   hypotheses and the background theory).  Primitive inferences include
   395   plain Natural Deduction rules for the primary connectives @{text
   396   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
   397   notion of equality/equivalence @{text "\<equiv>"}.
   398 *}
   399 
   400 
   401 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
   402 
   403 text {*
   404   The theory @{text "Pure"} contains constant declarations for the
   405   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
   406   the logical framework, see \figref{fig:pure-connectives}.  The
   407   derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
   408   defined inductively by the primitive inferences given in
   409   \figref{fig:prim-rules}, with the global restriction that the
   410   hypotheses must \emph{not} contain any schematic variables.  The
   411   builtin equality is conceptually axiomatized as shown in
   412   \figref{fig:pure-equality}, although the implementation works
   413   directly with derived inferences.
   414 
   415   \begin{figure}[htb]
   416   \begin{center}
   417   \begin{tabular}{ll}
   418   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
   419   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
   420   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
   421   \end{tabular}
   422   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
   423   \end{center}
   424   \end{figure}
   425 
   426   \begin{figure}[htb]
   427   \begin{center}
   428   \[
   429   \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}
   430   \qquad
   431   \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
   432   \]
   433   \[
   434   \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
   435   \qquad
   436   \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
   437   \]
   438   \[
   439   \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
   440   \qquad
   441   \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"}}
   442   \]
   443   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
   444   \end{center}
   445   \end{figure}
   446 
   447   \begin{figure}[htb]
   448   \begin{center}
   449   \begin{tabular}{ll}
   450   @{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}-conversion \\
   451   @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
   452   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
   453   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
   454   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
   455   \end{tabular}
   456   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
   457   \end{center}
   458   \end{figure}
   459 
   460   The introduction and elimination rules for @{text "\<And>"} and @{text
   461   "\<Longrightarrow>"} are analogous to formation of dependently typed @{text
   462   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
   463   are irrelevant in the Pure logic, though; they cannot occur within
   464   propositions.  The system provides a runtime option to record
   465   explicit proof terms for primitive inferences.  Thus all three
   466   levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
   467   terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
   468   \cite{Berghofer-Nipkow:2000:TPHOL}).
   469 
   470   Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need
   471   not be recorded in the hypotheses, because the simple syntactic
   472   types of Pure are always inhabitable.  ``Assumptions'' @{text "x ::
   473   \<tau>"} for type-membership are only present as long as some @{text
   474   "x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key
   475   difference to ``@{text "\<lambda>HOL"}'' in the PTS framework
   476   \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are
   477   treated uniformly for propositions and types.}
   478 
   479   \medskip The axiomatization of a theory is implicitly closed by
   480   forming all instances of type and term variables: @{text "\<turnstile>
   481   A\<vartheta>"} holds for any substitution instance of an axiom
   482   @{text "\<turnstile> A"}.  By pushing substitutions through derivations
   483   inductively, we also get admissible @{text "generalize"} and @{text
   484   "instance"} rules as shown in \figref{fig:subst-rules}.
   485 
   486   \begin{figure}[htb]
   487   \begin{center}
   488   \[
   489   \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}
   490   \quad
   491   \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
   492   \]
   493   \[
   494   \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}
   495   \quad
   496   \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}
   497   \]
   498   \caption{Admissible substitution rules}\label{fig:subst-rules}
   499   \end{center}
   500   \end{figure}
   501 
   502   Note that @{text "instantiate"} does not require an explicit
   503   side-condition, because @{text "\<Gamma>"} may never contain schematic
   504   variables.
   505 
   506   In principle, variables could be substituted in hypotheses as well,
   507   but this would disrupt the monotonicity of reasoning: deriving
   508   @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is
   509   correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
   510   the result belongs to a different proof context.
   511 
   512   \medskip An \emph{oracle} is a function that produces axioms on the
   513   fly.  Logically, this is an instance of the @{text "axiom"} rule
   514   (\figref{fig:prim-rules}), but there is an operational difference.
   515   The system always records oracle invocations within derivations of
   516   theorems by a unique tag.
   517 
   518   Axiomatizations should be limited to the bare minimum, typically as
   519   part of the initial logical basis of an object-logic formalization.
   520   Later on, theories are usually developed in a strictly definitional
   521   fashion, by stating only certain equalities over new constants.
   522 
   523   A \emph{simple definition} consists of a constant declaration @{text
   524   "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t
   525   :: \<sigma>"} is a closed term without any hidden polymorphism.  The RHS
   526   may depend on further defined constants, but not @{text "c"} itself.
   527   Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>
   528   t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.
   529 
   530   An \emph{overloaded definition} consists of a collection of axioms
   531   for the same constant, with zero or one equations @{text
   532   "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for
   533   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention
   534   previously defined constants as above, or arbitrary constants @{text
   535   "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text
   536   "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by
   537   primitive recursion over the syntactic structure of a single type
   538   argument.
   539 *}
   540 
   541 text %mlref {*
   542   \begin{mldecls}
   543   @{index_ML_type ctyp} \\
   544   @{index_ML_type cterm} \\
   545   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
   546   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
   547   \end{mldecls}
   548   \begin{mldecls}
   549   @{index_ML_type thm} \\
   550   @{index_ML proofs: "int ref"} \\
   551   @{index_ML Thm.assume: "cterm -> thm"} \\
   552   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   553   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
   554   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   555   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
   556   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   557   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
   558   @{index_ML Thm.axiom: "theory -> string -> thm"} \\
   559   @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory
   560   -> (string * ('a -> thm)) * theory"} \\
   561   \end{mldecls}
   562   \begin{mldecls}
   563   @{index_ML Theory.add_axioms_i: "(binding * term) list -> theory -> theory"} \\
   564   @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
   565   @{index_ML Theory.add_defs_i: "bool -> bool -> (binding * term) list -> theory -> theory"} \\
   566   \end{mldecls}
   567 
   568   \begin{description}
   569 
   570   \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
   571   and terms, respectively.  These are abstract datatypes that
   572   guarantee that its values have passed the full well-formedness (and
   573   well-typedness) checks, relative to the declarations of type
   574   constructors, constants etc. in the theory.
   575 
   576   \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
   577   Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,
   578   respectively.  This also involves some basic normalizations, such
   579   expansion of type and term abbreviations from the theory context.
   580 
   581   Re-certification is relatively slow and should be avoided in tight
   582   reasoning loops.  There are separate operations to decompose
   583   certified entities (including actual theorems).
   584 
   585   \item @{ML_type thm} represents proven propositions.  This is an
   586   abstract datatype that guarantees that its values have been
   587   constructed by basic principles of the @{ML_struct Thm} module.
   588   Every @{ML thm} value contains a sliding back-reference to the
   589   enclosing theory, cf.\ \secref{sec:context-theory}.
   590 
   591   \item @{ML proofs} determines the detail of proof recording within
   592   @{ML_type thm} values: @{ML 0} records only the names of oracles,
   593   @{ML 1} records oracle names and propositions, @{ML 2} additionally
   594   records full proof terms.  Officially named theorems that contribute
   595   to a result are always recorded.
   596 
   597   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
   598   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
   599   correspond to the primitive inferences of \figref{fig:prim-rules}.
   600 
   601   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
   602   corresponds to the @{text "generalize"} rules of
   603   \figref{fig:subst-rules}.  Here collections of type and term
   604   variables are generalized simultaneously, specified by the given
   605   basic names.
   606 
   607   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
   608   \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
   609   of \figref{fig:subst-rules}.  Type variables are substituted before
   610   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
   611   refer to the instantiated versions.
   612 
   613   \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
   614   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
   615 
   616   \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named
   617   oracle rule, essentially generating arbitrary axioms on the fly,
   618   cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
   619 
   620   \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
   621   arbitrary propositions as axioms.
   622 
   623   \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
   624   \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
   625   for constant @{text "c\<^isub>\<tau>"}, relative to existing
   626   specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.
   627 
   628   \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c
   629   \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an existing
   630   constant @{text "c"}.  Dependencies are recorded (cf.\ @{ML
   631   Theory.add_deps}), unless the @{text "unchecked"} option is set.
   632 
   633   \end{description}
   634 *}
   635 
   636 
   637 subsection {* Auxiliary definitions *}
   638 
   639 text {*
   640   Theory @{text "Pure"} provides a few auxiliary definitions, see
   641   \figref{fig:pure-aux}.  These special constants are normally not
   642   exposed to the user, but appear in internal encodings.
   643 
   644   \begin{figure}[htb]
   645   \begin{center}
   646   \begin{tabular}{ll}
   647   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
   648   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
   649   @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\
   650   @{text "#A \<equiv> A"} \\[1ex]
   651   @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
   652   @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
   653   @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
   654   @{text "(unspecified)"} \\
   655   \end{tabular}
   656   \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   657   \end{center}
   658   \end{figure}
   659 
   660   Derived conjunction rules include introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &
   661   B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}.
   662   Conjunction allows to treat simultaneous assumptions and conclusions
   663   uniformly.  For example, multiple claims are intermediately
   664   represented as explicit conjunction, but this is refined into
   665   separate sub-goals before the user continues the proof; the final
   666   result is projected into a list of theorems (cf.\
   667   \secref{sec:tactical-goals}).
   668 
   669   The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex
   670   propositions appear as atomic, without changing the meaning: @{text
   671   "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable.  See
   672   \secref{sec:tactical-goals} for specific operations.
   673 
   674   The @{text "term"} marker turns any well-typed term into a derivable
   675   proposition: @{text "\<turnstile> TERM t"} holds unconditionally.  Although
   676   this is logically vacuous, it allows to treat terms and proofs
   677   uniformly, similar to a type-theoretic framework.
   678 
   679   The @{text "TYPE"} constructor is the canonical representative of
   680   the unspecified type @{text "\<alpha> itself"}; it essentially injects the
   681   language of types into that of terms.  There is specific notation
   682   @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
   683  itself\<^esub>"}.
   684   Although being devoid of any particular meaning, the @{text
   685   "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term
   686   language.  In particular, @{text "TYPE(\<alpha>)"} may be used as formal
   687   argument in primitive definitions, in order to circumvent hidden
   688   polymorphism (cf.\ \secref{sec:terms}).  For example, @{text "c
   689   TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of
   690   a proposition @{text "A"} that depends on an additional type
   691   argument, which is essentially a predicate on types.
   692 *}
   693 
   694 text %mlref {*
   695   \begin{mldecls}
   696   @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
   697   @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
   698   @{index_ML Drule.mk_term: "cterm -> thm"} \\
   699   @{index_ML Drule.dest_term: "thm -> cterm"} \\
   700   @{index_ML Logic.mk_type: "typ -> term"} \\
   701   @{index_ML Logic.dest_type: "term -> typ"} \\
   702   \end{mldecls}
   703 
   704   \begin{description}
   705 
   706   \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text
   707   "A"} and @{text "B"}.
   708 
   709   \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}
   710   from @{text "A & B"}.
   711 
   712   \item @{ML Drule.mk_term} derives @{text "TERM t"}.
   713 
   714   \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text
   715   "TERM t"}.
   716 
   717   \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text
   718   "TYPE(\<tau>)"}.
   719 
   720   \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type
   721   @{text "\<tau>"}.
   722 
   723   \end{description}
   724 *}
   725 
   726 
   727 section {* Object-level rules \label{sec:obj-rules} *}
   728 
   729 text {*
   730   The primitive inferences covered so far mostly serve foundational
   731   purposes.  User-level reasoning usually works via object-level rules
   732   that are represented as theorems of Pure.  Composition of rules
   733   involves \emph{backchaining}, \emph{higher-order unification} modulo
   734   @{text "\<alpha>\<beta>\<eta>"}-conversion of @{text "\<lambda>"}-terms, and so-called
   735   \emph{lifting} of rules into a context of @{text "\<And>"} and @{text
   736   "\<Longrightarrow>"} connectives.  Thus the full power of higher-order Natural
   737   Deduction in Isabelle/Pure becomes readily available.
   738 *}
   739 
   740 
   741 subsection {* Hereditary Harrop Formulae *}
   742 
   743 text {*
   744   The idea of object-level rules is to model Natural Deduction
   745   inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow
   746   arbitrary nesting similar to \cite{extensions91}.  The most basic
   747   rule format is that of a \emph{Horn Clause}:
   748   \[
   749   \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}
   750   \]
   751   where @{text "A, A\<^sub>1, \<dots>, A\<^sub>n"} are atomic propositions
   752   of the framework, usually of the form @{text "Trueprop B"}, where
   753   @{text "B"} is a (compound) object-level statement.  This
   754   object-level inference corresponds to an iterated implication in
   755   Pure like this:
   756   \[
   757   @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}
   758   \]
   759   As an example consider conjunction introduction: @{text "A \<Longrightarrow> B \<Longrightarrow> A \<and>
   760   B"}.  Any parameters occurring in such rule statements are
   761   conceptionally treated as arbitrary:
   762   \[
   763   @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. A\<^sub>1 x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> \<dots> A\<^sub>n x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> A x\<^sub>1 \<dots> x\<^sub>m"}
   764   \]
   765 
   766   Nesting of rules means that the positions of @{text "A\<^sub>i"} may
   767   again hold compound rules, not just atomic propositions.
   768   Propositions of this format are called \emph{Hereditary Harrop
   769   Formulae} in the literature \cite{Miller:1991}.  Here we give an
   770   inductive characterization as follows:
   771 
   772   \medskip
   773   \begin{tabular}{ll}
   774   @{text "\<^bold>x"} & set of variables \\
   775   @{text "\<^bold>A"} & set of atomic propositions \\
   776   @{text "\<^bold>H  =  \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\
   777   \end{tabular}
   778   \medskip
   779 
   780   \noindent Thus we essentially impose nesting levels on propositions
   781   formed from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a
   782   prefix of parameters and compound premises, concluding an atomic
   783   proposition.  Typical examples are @{text "\<longrightarrow>"}-introduction @{text
   784   "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n
   785   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}.  Even deeper nesting occurs in well-founded
   786   induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this
   787   already marks the limit of rule complexity seen in practice.
   788 
   789   \medskip Regular user-level inferences in Isabelle/Pure always
   790   maintain the following canonical form of results:
   791 
   792   \begin{itemize}
   793 
   794   \item Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"},
   795   which is a theorem of Pure, means that quantifiers are pushed in
   796   front of implication at each level of nesting.  The normal form is a
   797   Hereditary Harrop Formula.
   798 
   799   \item The outermost prefix of parameters is represented via
   800   schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x
   801   \<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.
   802   Note that this representation looses information about the order of
   803   parameters, and vacuous quantifiers vanish automatically.
   804 
   805   \end{itemize}
   806 *}
   807 
   808 text %mlref {*
   809   \begin{mldecls}
   810   @{index_ML MetaSimplifier.norm_hhf: "thm -> thm"} \\
   811   \end{mldecls}
   812 
   813   \begin{description}
   814 
   815   \item @{ML MetaSimplifier.norm_hhf}~@{text thm} normalizes the given
   816   theorem according to the canonical form specified above.  This is
   817   occasionally helpful to repair some low-level tools that do not
   818   handle Hereditary Harrop Formulae properly.
   819 
   820   \end{description}
   821 *}
   822 
   823 
   824 subsection {* Rule composition *}
   825 
   826 text {*
   827   The rule calculus of Isabelle/Pure provides two main inferences:
   828   @{inference resolution} (i.e.\ back-chaining of rules) and
   829   @{inference assumption} (i.e.\ closing a branch), both modulo
   830   higher-order unification.  There are also combined variants, notably
   831   @{inference elim_resolution} and @{inference dest_resolution}.
   832 
   833   To understand the all-important @{inference resolution} principle,
   834   we first consider raw @{inference_def composition} (modulo
   835   higher-order unification with substitution @{text "\<vartheta>"}):
   836   \[
   837   \infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}
   838   {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}
   839   \]
   840   Here the conclusion of the first rule is unified with the premise of
   841   the second; the resulting rule instance inherits the premises of the
   842   first and conclusion of the second.  Note that @{text "C"} can again
   843   consist of iterated implications.  We can also permute the premises
   844   of the second rule back-and-forth in order to compose with @{text
   845   "B'"} in any position (subsequently we shall always refer to
   846   position 1 w.l.o.g.).
   847 
   848   In @{inference composition} the internal structure of the common
   849   part @{text "B"} and @{text "B'"} is not taken into account.  For
   850   proper @{inference resolution} we require @{text "B"} to be atomic,
   851   and explicitly observe the structure @{text "\<And>\<^vec>x. \<^vec>H
   852   \<^vec>x \<Longrightarrow> B' \<^vec>x"} of the premise of the second rule.  The
   853   idea is to adapt the first rule by ``lifting'' it into this context,
   854   by means of iterated application of the following inferences:
   855   \[
   856   \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}
   857   \]
   858   \[
   859   \infer[(@{inference_def all_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"}}
   860   \]
   861   By combining raw composition with lifting, we get full @{inference
   862   resolution} as follows:
   863   \[
   864   \infer[(@{inference_def resolution})]
   865   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
   866   {\begin{tabular}{l}
   867     @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\
   868     @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
   869     @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
   870    \end{tabular}}
   871   \]
   872 
   873   Continued resolution of rules allows to back-chain a problem towards
   874   more and sub-problems.  Branches are closed either by resolving with
   875   a rule of 0 premises, or by producing a ``short-circuit'' within a
   876   solved situation (again modulo unification):
   877   \[
   878   \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}
   879   {@{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})}}
   880   \]
   881 
   882   FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
   883 *}
   884 
   885 text %mlref {*
   886   \begin{mldecls}
   887   @{index_ML "op RS": "thm * thm -> thm"} \\
   888   @{index_ML "op OF": "thm * thm list -> thm"} \\
   889   \end{mldecls}
   890 
   891   \begin{description}
   892 
   893   \item @{text "rule\<^sub>1 RS rule\<^sub>2"} resolves @{text
   894   "rule\<^sub>1"} with @{text "rule\<^sub>2"} according to the
   895   @{inference resolution} principle explained above.  Note that the
   896   corresponding attribute in the Isar language is called @{attribute
   897   THEN}.
   898 
   899   \item @{text "rule OF rules"} resolves a list of rules with the
   900   first rule, addressing its premises @{text "1, \<dots>, length rules"}
   901   (operating from last to first).  This means the newly emerging
   902   premises are all concatenated, without interfering.  Also note that
   903   compared to @{text "RS"}, the rule argument order is swapped: @{text
   904   "rule\<^sub>1 RS rule\<^sub>2 = rule\<^sub>2 OF [rule\<^sub>1]"}.
   905 
   906   \end{description}
   907 *}
   908 
   909 end