doc-src/IsarImplementation/Thy/Logic.thy
author wenzelm
Mon Jun 06 19:08:46 2011 +0200 (2011-06-06)
changeset 42934 287182c2f23a
parent 42933 7860ffc5ec08
child 46253 3e427a12f0f3
permissions -rw-r--r--
moved incr_boundvars;
discontinued low-level term operations;
     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: type constructors, term constants, and facts
    28   (proof constants) may involve arbitrary type schemes, but the type
    29   of a locally fixed term parameter is also fixed!}
    30 *}
    31 
    32 
    33 section {* Types \label{sec:types} *}
    34 
    35 text {*
    36   The language of types is an uninterpreted order-sorted first-order
    37   algebra; types are qualified by ordered type classes.
    38 
    39   \medskip A \emph{type class} is an abstract syntactic entity
    40   declared in the theory context.  The \emph{subclass relation} @{text
    41   "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
    42   generating relation; the transitive closure is maintained
    43   internally.  The resulting relation is an ordering: reflexive,
    44   transitive, and antisymmetric.
    45 
    46   A \emph{sort} is a list of type classes written as @{text "s = {c\<^isub>1,
    47   \<dots>, c\<^isub>m}"}, it represents symbolic intersection.  Notationally, the
    48   curly braces are omitted for singleton intersections, i.e.\ any
    49   class @{text "c"} may be read as a sort @{text "{c}"}.  The ordering
    50   on type classes is extended to sorts according to the meaning of
    51   intersections: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text
    52   "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}.  The empty intersection @{text "{}"} refers to
    53   the universal sort, which is the largest element wrt.\ the sort
    54   order.  Thus @{text "{}"} represents the ``full sort'', not the
    55   empty one!  The intersection of all (finitely many) classes declared
    56   in the current theory is the least element wrt.\ the sort ordering.
    57 
    58   \medskip A \emph{fixed type variable} is a pair of a basic name
    59   (starting with a @{text "'"} character) and a sort constraint, e.g.\
    60   @{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^isub>s"}.
    61   A \emph{schematic type variable} is a pair of an indexname and a
    62   sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually
    63   printed as @{text "?\<alpha>\<^isub>s"}.
    64 
    65   Note that \emph{all} syntactic components contribute to the identity
    66   of type variables: basic name, index, and sort constraint.  The core
    67   logic handles type variables with the same name but different sorts
    68   as different, although the type-inference layer (which is outside
    69   the core) rejects anything like that.
    70 
    71   A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
    72   on types declared in the theory.  Type constructor application is
    73   written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.  For
    74   @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}
    75   instead of @{text "()prop"}.  For @{text "k = 1"} the parentheses
    76   are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.
    77   Further notation is provided for specific constructors, notably the
    78   right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
    79   \<beta>)fun"}.
    80   
    81   The logical category \emph{type} is defined inductively over type
    82   variables and type constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
    83   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}.
    84 
    85   A \emph{type abbreviation} is a syntactic definition @{text
    86   "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
    87   variables @{text "\<^vec>\<alpha>"}.  Type abbreviations appear as type
    88   constructors in the syntax, but are expanded before entering the
    89   logical core.
    90 
    91   A \emph{type arity} declares the image behavior of a type
    92   constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,
    93   s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is
    94   of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is
    95   of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
    96   completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
    97   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
    98 
    99   \medskip The sort algebra is always maintained as \emph{coregular},
   100   which means that type arities are consistent with the subclass
   101   relation: for any type constructor @{text "\<kappa>"}, and classes @{text
   102   "c\<^isub>1 \<subseteq> c\<^isub>2"}, and arities @{text "\<kappa> ::
   103   (\<^vec>s\<^isub>1)c\<^isub>1"} and @{text "\<kappa> ::
   104   (\<^vec>s\<^isub>2)c\<^isub>2"} holds @{text "\<^vec>s\<^isub>1 \<subseteq>
   105   \<^vec>s\<^isub>2"} component-wise.
   106 
   107   The key property of a coregular order-sorted algebra is that sort
   108   constraints can be solved in a most general fashion: for each type
   109   constructor @{text "\<kappa>"} and sort @{text "s"} there is a most general
   110   vector of argument sorts @{text "(s\<^isub>1, \<dots>, s\<^isub>k)"} such
   111   that a type scheme @{text "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
   112   \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is of sort @{text "s"}.
   113   Consequently, type unification has most general solutions (modulo
   114   equivalence of sorts), so type-inference produces primary types as
   115   expected \cite{nipkow-prehofer}.
   116 *}
   117 
   118 text %mlref {*
   119   \begin{mldecls}
   120   @{index_ML_type class: string} \\
   121   @{index_ML_type sort: "class list"} \\
   122   @{index_ML_type arity: "string * sort list * sort"} \\
   123   @{index_ML_type typ} \\
   124   @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\
   125   @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
   126   \end{mldecls}
   127   \begin{mldecls}
   128   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   129   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   130   @{index_ML Sign.add_types: "Proof.context ->
   131   (binding * int * mixfix) list -> theory -> theory"} \\
   132   @{index_ML Sign.add_type_abbrev: "Proof.context ->
   133   binding * string list * typ -> theory -> theory"} \\
   134   @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
   135   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
   136   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   137   \end{mldecls}
   138 
   139   \begin{description}
   140 
   141   \item Type @{ML_type class} represents type classes.
   142 
   143   \item Type @{ML_type sort} represents sorts, i.e.\ finite
   144   intersections of classes.  The empty list @{ML "[]: sort"} refers to
   145   the empty class intersection, i.e.\ the ``full sort''.
   146 
   147   \item Type @{ML_type arity} represents type arities.  A triple
   148   @{text "(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> ::
   149   (\<^vec>s)s"} as described above.
   150 
   151   \item Type @{ML_type typ} represents types; this is a datatype with
   152   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
   153 
   154   \item @{ML Term.map_atyps}~@{text "f \<tau>"} applies the mapping @{text
   155   "f"} to all atomic types (@{ML TFree}, @{ML TVar}) occurring in
   156   @{text "\<tau>"}.
   157 
   158   \item @{ML Term.fold_atyps}~@{text "f \<tau>"} iterates the operation
   159   @{text "f"} over all occurrences of atomic types (@{ML TFree}, @{ML
   160   TVar}) in @{text "\<tau>"}; the type structure is traversed from left to
   161   right.
   162 
   163   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
   164   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
   165 
   166   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
   167   @{text "\<tau>"} is of sort @{text "s"}.
   168 
   169   \item @{ML Sign.add_types}~@{text "ctxt [(\<kappa>, k, mx), \<dots>]"} declares a
   170   new type constructors @{text "\<kappa>"} with @{text "k"} arguments and
   171   optional mixfix syntax.
   172 
   173   \item @{ML Sign.add_type_abbrev}~@{text "ctxt (\<kappa>, \<^vec>\<alpha>, \<tau>)"}
   174   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.
   175 
   176   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
   177   c\<^isub>n])"} declares a new class @{text "c"}, together with class
   178   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
   179 
   180   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   181   c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \<subseteq>
   182   c\<^isub>2"}.
   183 
   184   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
   185   the arity @{text "\<kappa> :: (\<^vec>s)s"}.
   186 
   187   \end{description}
   188 *}
   189 
   190 text %mlantiq {*
   191   \begin{matharray}{rcl}
   192   @{ML_antiquotation_def "class"} & : & @{text ML_antiquotation} \\
   193   @{ML_antiquotation_def "sort"} & : & @{text ML_antiquotation} \\
   194   @{ML_antiquotation_def "type_name"} & : & @{text ML_antiquotation} \\
   195   @{ML_antiquotation_def "type_abbrev"} & : & @{text ML_antiquotation} \\
   196   @{ML_antiquotation_def "nonterminal"} & : & @{text ML_antiquotation} \\
   197   @{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\
   198   \end{matharray}
   199 
   200   @{rail "
   201   @@{ML_antiquotation class} nameref
   202   ;
   203   @@{ML_antiquotation sort} sort
   204   ;
   205   (@@{ML_antiquotation type_name} |
   206    @@{ML_antiquotation type_abbrev} |
   207    @@{ML_antiquotation nonterminal}) nameref
   208   ;
   209   @@{ML_antiquotation typ} type
   210   "}
   211 
   212   \begin{description}
   213 
   214   \item @{text "@{class c}"} inlines the internalized class @{text
   215   "c"} --- as @{ML_type string} literal.
   216 
   217   \item @{text "@{sort s}"} inlines the internalized sort @{text "s"}
   218   --- as @{ML_type "string list"} literal.
   219 
   220   \item @{text "@{type_name c}"} inlines the internalized type
   221   constructor @{text "c"} --- as @{ML_type string} literal.
   222 
   223   \item @{text "@{type_abbrev c}"} inlines the internalized type
   224   abbreviation @{text "c"} --- as @{ML_type string} literal.
   225 
   226   \item @{text "@{nonterminal c}"} inlines the internalized syntactic
   227   type~/ grammar nonterminal @{text "c"} --- as @{ML_type string}
   228   literal.
   229 
   230   \item @{text "@{typ \<tau>}"} inlines the internalized type @{text "\<tau>"}
   231   --- as constructor term for datatype @{ML_type typ}.
   232 
   233   \end{description}
   234 *}
   235 
   236 
   237 section {* Terms \label{sec:terms} *}
   238 
   239 text {*
   240   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
   241   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
   242   or \cite{paulson-ml2}), with the types being determined by the
   243   corresponding binders.  In contrast, free variables and constants
   244   have an explicit name and type in each occurrence.
   245 
   246   \medskip A \emph{bound variable} is a natural number @{text "b"},
   247   which accounts for the number of intermediate binders between the
   248   variable occurrence in the body and its binding position.  For
   249   example, the de-Bruijn term @{text "\<lambda>\<^bsub>bool\<^esub>. \<lambda>\<^bsub>bool\<^esub>. 1 \<and> 0"} would
   250   correspond to @{text "\<lambda>x\<^bsub>bool\<^esub>. \<lambda>y\<^bsub>bool\<^esub>. x \<and> y"} in a named
   251   representation.  Note that a bound variable may be represented by
   252   different de-Bruijn indices at different occurrences, depending on
   253   the nesting of abstractions.
   254 
   255   A \emph{loose variable} is a bound variable that is outside the
   256   scope of local binders.  The types (and names) for loose variables
   257   can be managed as a separate context, that is maintained as a stack
   258   of hypothetical binders.  The core logic operates on closed terms,
   259   without any loose variables.
   260 
   261   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
   262   @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"} here.  A
   263   \emph{schematic variable} is a pair of an indexname and a type,
   264   e.g.\ @{text "((x, 0), \<tau>)"} which is likewise printed as @{text
   265   "?x\<^isub>\<tau>"}.
   266 
   267   \medskip A \emph{constant} is a pair of a basic name and a type,
   268   e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text "c\<^isub>\<tau>"}
   269   here.  Constants are declared in the context as polymorphic families
   270   @{text "c :: \<sigma>"}, meaning that all substitution instances @{text
   271   "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
   272 
   273   The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"} wrt.\
   274   the declaration @{text "c :: \<sigma>"} is defined as the codomain of the
   275   matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>, ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in
   276   canonical order @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}, corresponding to the
   277   left-to-right occurrences of the @{text "\<alpha>\<^isub>i"} in @{text "\<sigma>"}.
   278   Within a given theory context, there is a one-to-one correspondence
   279   between any constant @{text "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1,
   280   \<dots>, \<tau>\<^isub>n)"} of its type arguments.  For example, with @{text "plus :: \<alpha>
   281   \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} corresponds to
   282   @{text "plus(nat)"}.
   283 
   284   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
   285   for type variables in @{text "\<sigma>"}.  These are observed by
   286   type-inference as expected, but \emph{ignored} by the core logic.
   287   This means the primitive logic is able to reason with instances of
   288   polymorphic constants that the user-level type-checker would reject
   289   due to violation of type class restrictions.
   290 
   291   \medskip An \emph{atomic term} is either a variable or constant.
   292   The logical category \emph{term} is defined inductively over atomic
   293   terms, with abstraction and application as follows: @{text "t = b |
   294   x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes care of
   295   converting between an external representation with named bound
   296   variables.  Subsequently, we shall use the latter notation instead
   297   of internal de-Bruijn representation.
   298 
   299   The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a
   300   term according to the structure of atomic terms, abstractions, and
   301   applicatins:
   302   \[
   303   \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}
   304   \qquad
   305   \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}
   306   \qquad
   307   \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}
   308   \]
   309   A \emph{well-typed term} is a term that can be typed according to these rules.
   310 
   311   Typing information can be omitted: type-inference is able to
   312   reconstruct the most general type of a raw term, while assigning
   313   most general types to all of its variables and constants.
   314   Type-inference depends on a context of type constraints for fixed
   315   variables, and declarations for polymorphic constants.
   316 
   317   The identity of atomic terms consists both of the name and the type
   318   component.  This means that different variables @{text
   319   "x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after
   320   type instantiation.  Type-inference rejects variables of the same
   321   name, but different types.  In contrast, mixed instances of
   322   polymorphic constants occur routinely.
   323 
   324   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
   325   is the set of type variables occurring in @{text "t"}, but not in
   326   its type @{text "\<sigma>"}.  This means that the term implicitly depends
   327   on type arguments that are not accounted in the result type, i.e.\
   328   there are different type instances @{text "t\<vartheta> :: \<sigma>"} and
   329   @{text "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly
   330   pathological situation notoriously demands additional care.
   331 
   332   \medskip A \emph{term abbreviation} is a syntactic definition @{text
   333   "c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},
   334   without any hidden polymorphism.  A term abbreviation looks like a
   335   constant in the syntax, but is expanded before entering the logical
   336   core.  Abbreviations are usually reverted when printing terms, using
   337   @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higher-order rewriting.
   338 
   339   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
   340   "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free
   341   renaming of bound variables; @{text "\<beta>"}-conversion contracts an
   342   abstraction applied to an argument term, substituting the argument
   343   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
   344   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
   345   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
   346   does not occur in @{text "f"}.
   347 
   348   Terms are normally treated modulo @{text "\<alpha>"}-conversion, which is
   349   implicit in the de-Bruijn representation.  Names for bound variables
   350   in abstractions are maintained separately as (meaningless) comments,
   351   mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is
   352   commonplace in various standard operations (\secref{sec:obj-rules})
   353   that are based on higher-order unification and matching.
   354 *}
   355 
   356 text %mlref {*
   357   \begin{mldecls}
   358   @{index_ML_type term} \\
   359   @{index_ML "op aconv": "term * term -> bool"} \\
   360   @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
   361   @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   362   @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
   363   @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   364   \end{mldecls}
   365   \begin{mldecls}
   366   @{index_ML fastype_of: "term -> typ"} \\
   367   @{index_ML lambda: "term -> term -> term"} \\
   368   @{index_ML betapply: "term * term -> term"} \\
   369   @{index_ML incr_boundvars: "int -> term -> term"} \\
   370   @{index_ML Sign.declare_const: "Proof.context ->
   371   (binding * typ) * mixfix -> theory -> term * theory"} \\
   372   @{index_ML Sign.add_abbrev: "string -> binding * term ->
   373   theory -> (term * term) * theory"} \\
   374   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   375   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   376   \end{mldecls}
   377 
   378   \begin{description}
   379 
   380   \item Type @{ML_type term} represents de-Bruijn terms, with comments
   381   in abstractions, and explicitly named free variables and constants;
   382   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
   383   Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.
   384 
   385   \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text
   386   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
   387   on type @{ML_type term}; raw datatype equality should only be used
   388   for operations related to parsing or printing!
   389 
   390   \item @{ML Term.map_types}~@{text "f t"} applies the mapping @{text
   391   "f"} to all types occurring in @{text "t"}.
   392 
   393   \item @{ML Term.fold_types}~@{text "f t"} iterates the operation
   394   @{text "f"} over all occurrences of types in @{text "t"}; the term
   395   structure is traversed from left to right.
   396 
   397   \item @{ML Term.map_aterms}~@{text "f t"} applies the mapping @{text
   398   "f"} to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
   399   Const}) occurring in @{text "t"}.
   400 
   401   \item @{ML Term.fold_aterms}~@{text "f t"} iterates the operation
   402   @{text "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML
   403   Free}, @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
   404   traversed from left to right.
   405 
   406   \item @{ML fastype_of}~@{text "t"} determines the type of a
   407   well-typed term.  This operation is relatively slow, despite the
   408   omission of any sanity checks.
   409 
   410   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
   411   "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the
   412   body @{text "b"} are replaced by bound variables.
   413 
   414   \item @{ML betapply}~@{text "(t, u)"} produces an application @{text
   415   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
   416   abstraction.
   417 
   418   \item @{ML incr_boundvars}~@{text "j"} increments a term's dangling
   419   bound variables by the offset @{text "j"}.  This is required when
   420   moving a subterm into a context where it is enclosed by a different
   421   number of abstractions.  Bound variables with a matching abstraction
   422   are unaffected.
   423 
   424   \item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares
   425   a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
   426 
   427   \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
   428   introduces a new term abbreviation @{text "c \<equiv> t"}.
   429 
   430   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
   431   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
   432   convert between two representations of polymorphic constants: full
   433   type instance vs.\ compact type arguments form.
   434 
   435   \end{description}
   436 *}
   437 
   438 text %mlantiq {*
   439   \begin{matharray}{rcl}
   440   @{ML_antiquotation_def "const_name"} & : & @{text ML_antiquotation} \\
   441   @{ML_antiquotation_def "const_abbrev"} & : & @{text ML_antiquotation} \\
   442   @{ML_antiquotation_def "const"} & : & @{text ML_antiquotation} \\
   443   @{ML_antiquotation_def "term"} & : & @{text ML_antiquotation} \\
   444   @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\
   445   \end{matharray}
   446 
   447   @{rail "
   448   (@@{ML_antiquotation const_name} |
   449    @@{ML_antiquotation const_abbrev}) nameref
   450   ;
   451   @@{ML_antiquotation const} ('(' (type + ',') ')')?
   452   ;
   453   @@{ML_antiquotation term} term
   454   ;
   455   @@{ML_antiquotation prop} prop
   456   "}
   457 
   458   \begin{description}
   459 
   460   \item @{text "@{const_name c}"} inlines the internalized logical
   461   constant name @{text "c"} --- as @{ML_type string} literal.
   462 
   463   \item @{text "@{const_abbrev c}"} inlines the internalized
   464   abbreviated constant name @{text "c"} --- as @{ML_type string}
   465   literal.
   466 
   467   \item @{text "@{const c(\<^vec>\<tau>)}"} inlines the internalized
   468   constant @{text "c"} with precise type instantiation in the sense of
   469   @{ML Sign.const_instance} --- as @{ML Const} constructor term for
   470   datatype @{ML_type term}.
   471 
   472   \item @{text "@{term t}"} inlines the internalized term @{text "t"}
   473   --- as constructor term for datatype @{ML_type term}.
   474 
   475   \item @{text "@{prop \<phi>}"} inlines the internalized proposition
   476   @{text "\<phi>"} --- as constructor term for datatype @{ML_type term}.
   477 
   478   \end{description}
   479 *}
   480 
   481 
   482 section {* Theorems \label{sec:thms} *}
   483 
   484 text {*
   485   A \emph{proposition} is a well-typed term of type @{text "prop"}, a
   486   \emph{theorem} is a proven proposition (depending on a context of
   487   hypotheses and the background theory).  Primitive inferences include
   488   plain Natural Deduction rules for the primary connectives @{text
   489   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
   490   notion of equality/equivalence @{text "\<equiv>"}.
   491 *}
   492 
   493 
   494 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
   495 
   496 text {*
   497   The theory @{text "Pure"} contains constant declarations for the
   498   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
   499   the logical framework, see \figref{fig:pure-connectives}.  The
   500   derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
   501   defined inductively by the primitive inferences given in
   502   \figref{fig:prim-rules}, with the global restriction that the
   503   hypotheses must \emph{not} contain any schematic variables.  The
   504   builtin equality is conceptually axiomatized as shown in
   505   \figref{fig:pure-equality}, although the implementation works
   506   directly with derived inferences.
   507 
   508   \begin{figure}[htb]
   509   \begin{center}
   510   \begin{tabular}{ll}
   511   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
   512   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
   513   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
   514   \end{tabular}
   515   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
   516   \end{center}
   517   \end{figure}
   518 
   519   \begin{figure}[htb]
   520   \begin{center}
   521   \[
   522   \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}
   523   \qquad
   524   \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
   525   \]
   526   \[
   527   \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
   528   \qquad
   529   \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
   530   \]
   531   \[
   532   \infer[@{text "(\<Longrightarrow>\<hyphen>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
   533   \qquad
   534   \infer[@{text "(\<Longrightarrow>\<hyphen>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"}}
   535   \]
   536   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
   537   \end{center}
   538   \end{figure}
   539 
   540   \begin{figure}[htb]
   541   \begin{center}
   542   \begin{tabular}{ll}
   543   @{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}-conversion \\
   544   @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
   545   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
   546   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
   547   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
   548   \end{tabular}
   549   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
   550   \end{center}
   551   \end{figure}
   552 
   553   The introduction and elimination rules for @{text "\<And>"} and @{text
   554   "\<Longrightarrow>"} are analogous to formation of dependently typed @{text
   555   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
   556   are irrelevant in the Pure logic, though; they cannot occur within
   557   propositions.  The system provides a runtime option to record
   558   explicit proof terms for primitive inferences.  Thus all three
   559   levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
   560   terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
   561   \cite{Berghofer-Nipkow:2000:TPHOL}).
   562 
   563   Observe that locally fixed parameters (as in @{text
   564   "\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because
   565   the simple syntactic types of Pure are always inhabitable.
   566   ``Assumptions'' @{text "x :: \<tau>"} for type-membership are only
   567   present as long as some @{text "x\<^isub>\<tau>"} occurs in the statement
   568   body.\footnote{This is the key difference to ``@{text "\<lambda>HOL"}'' in
   569   the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses
   570   @{text "x : A"} are treated uniformly for propositions and types.}
   571 
   572   \medskip The axiomatization of a theory is implicitly closed by
   573   forming all instances of type and term variables: @{text "\<turnstile>
   574   A\<vartheta>"} holds for any substitution instance of an axiom
   575   @{text "\<turnstile> A"}.  By pushing substitutions through derivations
   576   inductively, we also get admissible @{text "generalize"} and @{text
   577   "instantiate"} rules as shown in \figref{fig:subst-rules}.
   578 
   579   \begin{figure}[htb]
   580   \begin{center}
   581   \[
   582   \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}
   583   \quad
   584   \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
   585   \]
   586   \[
   587   \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}
   588   \quad
   589   \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}
   590   \]
   591   \caption{Admissible substitution rules}\label{fig:subst-rules}
   592   \end{center}
   593   \end{figure}
   594 
   595   Note that @{text "instantiate"} does not require an explicit
   596   side-condition, because @{text "\<Gamma>"} may never contain schematic
   597   variables.
   598 
   599   In principle, variables could be substituted in hypotheses as well,
   600   but this would disrupt the monotonicity of reasoning: deriving
   601   @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is
   602   correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
   603   the result belongs to a different proof context.
   604 
   605   \medskip An \emph{oracle} is a function that produces axioms on the
   606   fly.  Logically, this is an instance of the @{text "axiom"} rule
   607   (\figref{fig:prim-rules}), but there is an operational difference.
   608   The system always records oracle invocations within derivations of
   609   theorems by a unique tag.
   610 
   611   Axiomatizations should be limited to the bare minimum, typically as
   612   part of the initial logical basis of an object-logic formalization.
   613   Later on, theories are usually developed in a strictly definitional
   614   fashion, by stating only certain equalities over new constants.
   615 
   616   A \emph{simple definition} consists of a constant declaration @{text
   617   "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t
   618   :: \<sigma>"} is a closed term without any hidden polymorphism.  The RHS
   619   may depend on further defined constants, but not @{text "c"} itself.
   620   Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>
   621   t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.
   622 
   623   An \emph{overloaded definition} consists of a collection of axioms
   624   for the same constant, with zero or one equations @{text
   625   "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for
   626   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention
   627   previously defined constants as above, or arbitrary constants @{text
   628   "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text
   629   "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by
   630   primitive recursion over the syntactic structure of a single type
   631   argument.  See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.
   632 *}
   633 
   634 text %mlref {*
   635   \begin{mldecls}
   636   @{index_ML_type ctyp} \\
   637   @{index_ML_type cterm} \\
   638   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
   639   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
   640   \end{mldecls}
   641   \begin{mldecls}
   642   @{index_ML_type thm} \\
   643   @{index_ML proofs: "int Unsynchronized.ref"} \\
   644   @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
   645   @{index_ML Thm.assume: "cterm -> thm"} \\
   646   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   647   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
   648   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   649   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
   650   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   651   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
   652   @{index_ML Thm.add_axiom: "Proof.context ->
   653   binding * term -> theory -> (string * thm) * theory"} \\
   654   @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
   655   (string * ('a -> thm)) * theory"} \\
   656   @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->
   657   binding * term -> theory -> (string * thm) * theory"} \\
   658   \end{mldecls}
   659   \begin{mldecls}
   660   @{index_ML Theory.add_deps: "Proof.context -> string ->
   661   string * typ -> (string * typ) list -> theory -> theory"} \\
   662   \end{mldecls}
   663 
   664   \begin{description}
   665 
   666   \item Types @{ML_type ctyp} and @{ML_type cterm} represent certified
   667   types and terms, respectively.  These are abstract datatypes that
   668   guarantee that its values have passed the full well-formedness (and
   669   well-typedness) checks, relative to the declarations of type
   670   constructors, constants etc. in the theory.
   671 
   672   \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
   673   Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,
   674   respectively.  This also involves some basic normalizations, such
   675   expansion of type and term abbreviations from the theory context.
   676 
   677   Re-certification is relatively slow and should be avoided in tight
   678   reasoning loops.  There are separate operations to decompose
   679   certified entities (including actual theorems).
   680 
   681   \item Type @{ML_type thm} represents proven propositions.  This is
   682   an abstract datatype that guarantees that its values have been
   683   constructed by basic principles of the @{ML_struct Thm} module.
   684   Every @{ML_type thm} value contains a sliding back-reference to the
   685   enclosing theory, cf.\ \secref{sec:context-theory}.
   686 
   687   \item @{ML proofs} specifies the detail of proof recording within
   688   @{ML_type thm} values: @{ML 0} records only the names of oracles,
   689   @{ML 1} records oracle names and propositions, @{ML 2} additionally
   690   records full proof terms.  Officially named theorems that contribute
   691   to a result are recorded in any case.
   692 
   693   \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given
   694   theorem to a \emph{larger} theory, see also \secref{sec:context}.
   695   This formal adjustment of the background context has no logical
   696   significance, but is occasionally required for formal reasons, e.g.\
   697   when theorems that are imported from more basic theories are used in
   698   the current situation.
   699 
   700   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
   701   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
   702   correspond to the primitive inferences of \figref{fig:prim-rules}.
   703 
   704   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
   705   corresponds to the @{text "generalize"} rules of
   706   \figref{fig:subst-rules}.  Here collections of type and term
   707   variables are generalized simultaneously, specified by the given
   708   basic names.
   709 
   710   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
   711   \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
   712   of \figref{fig:subst-rules}.  Type variables are substituted before
   713   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
   714   refer to the instantiated versions.
   715 
   716   \item @{ML Thm.add_axiom}~@{text "ctxt (name, A)"} declares an
   717   arbitrary proposition as axiom, and retrieves it as a theorem from
   718   the resulting theory, cf.\ @{text "axiom"} in
   719   \figref{fig:prim-rules}.  Note that the low-level representation in
   720   the axiom table may differ slightly from the returned theorem.
   721 
   722   \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named
   723   oracle rule, essentially generating arbitrary axioms on the fly,
   724   cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
   725 
   726   \item @{ML Thm.add_def}~@{text "ctxt unchecked overloaded (name, c
   727   \<^vec>x \<equiv> t)"} states a definitional axiom for an existing constant
   728   @{text "c"}.  Dependencies are recorded via @{ML Theory.add_deps},
   729   unless the @{text "unchecked"} option is set.  Note that the
   730   low-level representation in the axiom table may differ slightly from
   731   the returned theorem.
   732 
   733   \item @{ML Theory.add_deps}~@{text "ctxt name c\<^isub>\<tau> \<^vec>d\<^isub>\<sigma>"}
   734   declares dependencies of a named specification for constant @{text
   735   "c\<^isub>\<tau>"}, relative to existing specifications for constants @{text
   736   "\<^vec>d\<^isub>\<sigma>"}.
   737 
   738   \end{description}
   739 *}
   740 
   741 
   742 text %mlantiq {*
   743   \begin{matharray}{rcl}
   744   @{ML_antiquotation_def "ctyp"} & : & @{text ML_antiquotation} \\
   745   @{ML_antiquotation_def "cterm"} & : & @{text ML_antiquotation} \\
   746   @{ML_antiquotation_def "cprop"} & : & @{text ML_antiquotation} \\
   747   @{ML_antiquotation_def "thm"} & : & @{text ML_antiquotation} \\
   748   @{ML_antiquotation_def "thms"} & : & @{text ML_antiquotation} \\
   749   @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\
   750   \end{matharray}
   751 
   752   @{rail "
   753   @@{ML_antiquotation ctyp} typ
   754   ;
   755   @@{ML_antiquotation cterm} term
   756   ;
   757   @@{ML_antiquotation cprop} prop
   758   ;
   759   @@{ML_antiquotation thm} thmref
   760   ;
   761   @@{ML_antiquotation thms} thmrefs
   762   ;
   763   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \\
   764     @'by' method method?
   765   "}
   766 
   767   \begin{description}
   768 
   769   \item @{text "@{ctyp \<tau>}"} produces a certified type wrt.\ the
   770   current background theory --- as abstract value of type @{ML_type
   771   ctyp}.
   772 
   773   \item @{text "@{cterm t}"} and @{text "@{cprop \<phi>}"} produce a
   774   certified term wrt.\ the current background theory --- as abstract
   775   value of type @{ML_type cterm}.
   776 
   777   \item @{text "@{thm a}"} produces a singleton fact --- as abstract
   778   value of type @{ML_type thm}.
   779 
   780   \item @{text "@{thms a}"} produces a general fact --- as abstract
   781   value of type @{ML_type "thm list"}.
   782 
   783   \item @{text "@{lemma \<phi> by meth}"} produces a fact that is proven on
   784   the spot according to the minimal proof, which imitates a terminal
   785   Isar proof.  The result is an abstract value of type @{ML_type thm}
   786   or @{ML_type "thm list"}, depending on the number of propositions
   787   given here.
   788 
   789   The internal derivation object lacks a proper theorem name, but it
   790   is formally closed, unless the @{text "(open)"} option is specified
   791   (this may impact performance of applications with proof terms).
   792 
   793   Since ML antiquotations are always evaluated at compile-time, there
   794   is no run-time overhead even for non-trivial proofs.  Nonetheless,
   795   the justification is syntactically limited to a single @{command
   796   "by"} step.  More complex Isar proofs should be done in regular
   797   theory source, before compiling the corresponding ML text that uses
   798   the result.
   799 
   800   \end{description}
   801 
   802 *}
   803 
   804 
   805 subsection {* Auxiliary definitions \label{sec:logic-aux} *}
   806 
   807 text {*
   808   Theory @{text "Pure"} provides a few auxiliary definitions, see
   809   \figref{fig:pure-aux}.  These special constants are normally not
   810   exposed to the user, but appear in internal encodings.
   811 
   812   \begin{figure}[htb]
   813   \begin{center}
   814   \begin{tabular}{ll}
   815   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&&&"}) \\
   816   @{text "\<turnstile> A &&& B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
   817   @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\
   818   @{text "#A \<equiv> A"} \\[1ex]
   819   @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
   820   @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
   821   @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
   822   @{text "(unspecified)"} \\
   823   \end{tabular}
   824   \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   825   \end{center}
   826   \end{figure}
   827 
   828   The introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &&& B"}, and eliminations
   829   (projections) @{text "A &&& B \<Longrightarrow> A"} and @{text "A &&& B \<Longrightarrow> B"} are
   830   available as derived rules.  Conjunction allows to treat
   831   simultaneous assumptions and conclusions uniformly, e.g.\ consider
   832   @{text "A \<Longrightarrow> B \<Longrightarrow> C &&& D"}.  In particular, the goal mechanism
   833   represents multiple claims as explicit conjunction internally, but
   834   this is refined (via backwards introduction) into separate sub-goals
   835   before the user commences the proof; the final result is projected
   836   into a list of theorems using eliminations (cf.\
   837   \secref{sec:tactical-goals}).
   838 
   839   The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex
   840   propositions appear as atomic, without changing the meaning: @{text
   841   "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable.  See
   842   \secref{sec:tactical-goals} for specific operations.
   843 
   844   The @{text "term"} marker turns any well-typed term into a derivable
   845   proposition: @{text "\<turnstile> TERM t"} holds unconditionally.  Although
   846   this is logically vacuous, it allows to treat terms and proofs
   847   uniformly, similar to a type-theoretic framework.
   848 
   849   The @{text "TYPE"} constructor is the canonical representative of
   850   the unspecified type @{text "\<alpha> itself"}; it essentially injects the
   851   language of types into that of terms.  There is specific notation
   852   @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
   853  itself\<^esub>"}.
   854   Although being devoid of any particular meaning, the term @{text
   855   "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term
   856   language.  In particular, @{text "TYPE(\<alpha>)"} may be used as formal
   857   argument in primitive definitions, in order to circumvent hidden
   858   polymorphism (cf.\ \secref{sec:terms}).  For example, @{text "c
   859   TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of
   860   a proposition @{text "A"} that depends on an additional type
   861   argument, which is essentially a predicate on types.
   862 *}
   863 
   864 text %mlref {*
   865   \begin{mldecls}
   866   @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
   867   @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
   868   @{index_ML Drule.mk_term: "cterm -> thm"} \\
   869   @{index_ML Drule.dest_term: "thm -> cterm"} \\
   870   @{index_ML Logic.mk_type: "typ -> term"} \\
   871   @{index_ML Logic.dest_type: "term -> typ"} \\
   872   \end{mldecls}
   873 
   874   \begin{description}
   875 
   876   \item @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text
   877   "A"} and @{text "B"}.
   878 
   879   \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}
   880   from @{text "A &&& B"}.
   881 
   882   \item @{ML Drule.mk_term} derives @{text "TERM t"}.
   883 
   884   \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text
   885   "TERM t"}.
   886 
   887   \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text
   888   "TYPE(\<tau>)"}.
   889 
   890   \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type
   891   @{text "\<tau>"}.
   892 
   893   \end{description}
   894 *}
   895 
   896 
   897 section {* Object-level rules \label{sec:obj-rules} *}
   898 
   899 text {*
   900   The primitive inferences covered so far mostly serve foundational
   901   purposes.  User-level reasoning usually works via object-level rules
   902   that are represented as theorems of Pure.  Composition of rules
   903   involves \emph{backchaining}, \emph{higher-order unification} modulo
   904   @{text "\<alpha>\<beta>\<eta>"}-conversion of @{text "\<lambda>"}-terms, and so-called
   905   \emph{lifting} of rules into a context of @{text "\<And>"} and @{text
   906   "\<Longrightarrow>"} connectives.  Thus the full power of higher-order Natural
   907   Deduction in Isabelle/Pure becomes readily available.
   908 *}
   909 
   910 
   911 subsection {* Hereditary Harrop Formulae *}
   912 
   913 text {*
   914   The idea of object-level rules is to model Natural Deduction
   915   inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow
   916   arbitrary nesting similar to \cite{extensions91}.  The most basic
   917   rule format is that of a \emph{Horn Clause}:
   918   \[
   919   \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}
   920   \]
   921   where @{text "A, A\<^sub>1, \<dots>, A\<^sub>n"} are atomic propositions
   922   of the framework, usually of the form @{text "Trueprop B"}, where
   923   @{text "B"} is a (compound) object-level statement.  This
   924   object-level inference corresponds to an iterated implication in
   925   Pure like this:
   926   \[
   927   @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}
   928   \]
   929   As an example consider conjunction introduction: @{text "A \<Longrightarrow> B \<Longrightarrow> A \<and>
   930   B"}.  Any parameters occurring in such rule statements are
   931   conceptionally treated as arbitrary:
   932   \[
   933   @{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"}
   934   \]
   935 
   936   Nesting of rules means that the positions of @{text "A\<^sub>i"} may
   937   again hold compound rules, not just atomic propositions.
   938   Propositions of this format are called \emph{Hereditary Harrop
   939   Formulae} in the literature \cite{Miller:1991}.  Here we give an
   940   inductive characterization as follows:
   941 
   942   \medskip
   943   \begin{tabular}{ll}
   944   @{text "\<^bold>x"} & set of variables \\
   945   @{text "\<^bold>A"} & set of atomic propositions \\
   946   @{text "\<^bold>H  =  \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\
   947   \end{tabular}
   948   \medskip
   949 
   950   Thus we essentially impose nesting levels on propositions formed
   951   from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a prefix
   952   of parameters and compound premises, concluding an atomic
   953   proposition.  Typical examples are @{text "\<longrightarrow>"}-introduction @{text
   954   "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n
   955   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}.  Even deeper nesting occurs in well-founded
   956   induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this
   957   already marks the limit of rule complexity that is usually seen in
   958   practice.
   959 
   960   \medskip Regular user-level inferences in Isabelle/Pure always
   961   maintain the following canonical form of results:
   962 
   963   \begin{itemize}
   964 
   965   \item Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"},
   966   which is a theorem of Pure, means that quantifiers are pushed in
   967   front of implication at each level of nesting.  The normal form is a
   968   Hereditary Harrop Formula.
   969 
   970   \item The outermost prefix of parameters is represented via
   971   schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x
   972   \<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.
   973   Note that this representation looses information about the order of
   974   parameters, and vacuous quantifiers vanish automatically.
   975 
   976   \end{itemize}
   977 *}
   978 
   979 text %mlref {*
   980   \begin{mldecls}
   981   @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\
   982   \end{mldecls}
   983 
   984   \begin{description}
   985 
   986   \item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given
   987   theorem according to the canonical form specified above.  This is
   988   occasionally helpful to repair some low-level tools that do not
   989   handle Hereditary Harrop Formulae properly.
   990 
   991   \end{description}
   992 *}
   993 
   994 
   995 subsection {* Rule composition *}
   996 
   997 text {*
   998   The rule calculus of Isabelle/Pure provides two main inferences:
   999   @{inference resolution} (i.e.\ back-chaining of rules) and
  1000   @{inference assumption} (i.e.\ closing a branch), both modulo
  1001   higher-order unification.  There are also combined variants, notably
  1002   @{inference elim_resolution} and @{inference dest_resolution}.
  1003 
  1004   To understand the all-important @{inference resolution} principle,
  1005   we first consider raw @{inference_def composition} (modulo
  1006   higher-order unification with substitution @{text "\<vartheta>"}):
  1007   \[
  1008   \infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}
  1009   {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}
  1010   \]
  1011   Here the conclusion of the first rule is unified with the premise of
  1012   the second; the resulting rule instance inherits the premises of the
  1013   first and conclusion of the second.  Note that @{text "C"} can again
  1014   consist of iterated implications.  We can also permute the premises
  1015   of the second rule back-and-forth in order to compose with @{text
  1016   "B'"} in any position (subsequently we shall always refer to
  1017   position 1 w.l.o.g.).
  1018 
  1019   In @{inference composition} the internal structure of the common
  1020   part @{text "B"} and @{text "B'"} is not taken into account.  For
  1021   proper @{inference resolution} we require @{text "B"} to be atomic,
  1022   and explicitly observe the structure @{text "\<And>\<^vec>x. \<^vec>H
  1023   \<^vec>x \<Longrightarrow> B' \<^vec>x"} of the premise of the second rule.  The
  1024   idea is to adapt the first rule by ``lifting'' it into this context,
  1025   by means of iterated application of the following inferences:
  1026   \[
  1027   \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}
  1028   \]
  1029   \[
  1030   \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"}}
  1031   \]
  1032   By combining raw composition with lifting, we get full @{inference
  1033   resolution} as follows:
  1034   \[
  1035   \infer[(@{inference_def resolution})]
  1036   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
  1037   {\begin{tabular}{l}
  1038     @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\
  1039     @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
  1040     @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
  1041    \end{tabular}}
  1042   \]
  1043 
  1044   Continued resolution of rules allows to back-chain a problem towards
  1045   more and sub-problems.  Branches are closed either by resolving with
  1046   a rule of 0 premises, or by producing a ``short-circuit'' within a
  1047   solved situation (again modulo unification):
  1048   \[
  1049   \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}
  1050   {@{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})}}
  1051   \]
  1052 
  1053   FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
  1054 *}
  1055 
  1056 text %mlref {*
  1057   \begin{mldecls}
  1058   @{index_ML "op RS": "thm * thm -> thm"} \\
  1059   @{index_ML "op OF": "thm * thm list -> thm"} \\
  1060   \end{mldecls}
  1061 
  1062   \begin{description}
  1063 
  1064   \item @{text "rule\<^sub>1 RS rule\<^sub>2"} resolves @{text "rule\<^sub>1"} with @{text
  1065   "rule\<^sub>2"} according to the @{inference resolution} principle
  1066   explained above.  Note that the corresponding rule attribute in the
  1067   Isar language is called @{attribute THEN}.
  1068 
  1069   \item @{text "rule OF rules"} resolves a list of rules with the
  1070   first rule, addressing its premises @{text "1, \<dots>, length rules"}
  1071   (operating from last to first).  This means the newly emerging
  1072   premises are all concatenated, without interfering.  Also note that
  1073   compared to @{text "RS"}, the rule argument order is swapped: @{text
  1074   "rule\<^sub>1 RS rule\<^sub>2 = rule\<^sub>2 OF [rule\<^sub>1]"}.
  1075 
  1076   \end{description}
  1077 *}
  1078 
  1079 end