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