src/Doc/Implementation/Logic.thy
author wenzelm
Tue Apr 15 00:03:39 2014 +0200 (2014-04-15)
changeset 56579 4c94f631c595
parent 56420 b266e7a86485
child 58555 7975676c08c0
permissions -rw-r--r--
tuned spelling;
     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\<^sub>1 \<subseteq> c\<^sub>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\<^sub>1,
    47   \<dots>, c\<^sub>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\<^sub>1, \<dots> c\<^sub>m} \<subseteq> {d\<^sub>1, \<dots>, d\<^sub>n}"} iff @{text
    52   "\<forall>j. \<exists>i. c\<^sub>i \<subseteq> d\<^sub>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>\<^sub>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>\<^sub>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>\<^sub>1, \<dots>, \<alpha>\<^sub>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>\<^sub>s | ?\<alpha>\<^sub>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\<^sub>1, \<dots>,
    93   s\<^sub>k)s"} means that @{text "(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"} is
    94   of sort @{text "s"} if every argument type @{text "\<tau>\<^sub>i"} is
    95   of sort @{text "s\<^sub>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\<^sub>1 \<subseteq> c\<^sub>2"}, and arities @{text "\<kappa> ::
   103   (\<^vec>s\<^sub>1)c\<^sub>1"} and @{text "\<kappa> ::
   104   (\<^vec>s\<^sub>2)c\<^sub>2"} holds @{text "\<^vec>s\<^sub>1 \<subseteq>
   105   \<^vec>s\<^sub>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\<^sub>1, \<dots>, s\<^sub>k)"} such
   111   that a type scheme @{text "(\<alpha>\<^bsub>s\<^sub>1\<^esub>, \<dots>,
   112   \<alpha>\<^bsub>s\<^sub>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_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\
   131   @{index_ML Sign.add_type_abbrev: "Proof.context ->
   132   binding * string list * typ -> theory -> theory"} \\
   133   @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
   134   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
   135   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   136   \end{mldecls}
   137 
   138   \begin{description}
   139 
   140   \item Type @{ML_type class} represents type classes.
   141 
   142   \item Type @{ML_type sort} represents sorts, i.e.\ finite
   143   intersections of classes.  The empty list @{ML "[]: sort"} refers to
   144   the empty class intersection, i.e.\ the ``full sort''.
   145 
   146   \item Type @{ML_type arity} represents type arities.  A triple
   147   @{text "(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> ::
   148   (\<^vec>s)s"} as described above.
   149 
   150   \item Type @{ML_type typ} represents types; this is a datatype with
   151   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
   152 
   153   \item @{ML Term.map_atyps}~@{text "f \<tau>"} applies the mapping @{text
   154   "f"} to all atomic types (@{ML TFree}, @{ML TVar}) occurring in
   155   @{text "\<tau>"}.
   156 
   157   \item @{ML Term.fold_atyps}~@{text "f \<tau>"} iterates the operation
   158   @{text "f"} over all occurrences of atomic types (@{ML TFree}, @{ML
   159   TVar}) in @{text "\<tau>"}; the type structure is traversed from left to
   160   right.
   161 
   162   \item @{ML Sign.subsort}~@{text "thy (s\<^sub>1, s\<^sub>2)"}
   163   tests the subsort relation @{text "s\<^sub>1 \<subseteq> s\<^sub>2"}.
   164 
   165   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
   166   @{text "\<tau>"} is of sort @{text "s"}.
   167 
   168   \item @{ML Sign.add_type}~@{text "ctxt (\<kappa>, k, mx)"} declares a
   169   new type constructors @{text "\<kappa>"} with @{text "k"} arguments and
   170   optional mixfix syntax.
   171 
   172   \item @{ML Sign.add_type_abbrev}~@{text "ctxt (\<kappa>, \<^vec>\<alpha>, \<tau>)"}
   173   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.
   174 
   175   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^sub>1, \<dots>,
   176   c\<^sub>n])"} declares a new class @{text "c"}, together with class
   177   relations @{text "c \<subseteq> c\<^sub>i"}, for @{text "i = 1, \<dots>, n"}.
   178 
   179   \item @{ML Sign.primitive_classrel}~@{text "(c\<^sub>1,
   180   c\<^sub>2)"} declares the class relation @{text "c\<^sub>1 \<subseteq>
   181   c\<^sub>2"}.
   182 
   183   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
   184   the arity @{text "\<kappa> :: (\<^vec>s)s"}.
   185 
   186   \end{description}
   187 *}
   188 
   189 text %mlantiq {*
   190   \begin{matharray}{rcl}
   191   @{ML_antiquotation_def "class"} & : & @{text ML_antiquotation} \\
   192   @{ML_antiquotation_def "sort"} & : & @{text ML_antiquotation} \\
   193   @{ML_antiquotation_def "type_name"} & : & @{text ML_antiquotation} \\
   194   @{ML_antiquotation_def "type_abbrev"} & : & @{text ML_antiquotation} \\
   195   @{ML_antiquotation_def "nonterminal"} & : & @{text ML_antiquotation} \\
   196   @{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\
   197   \end{matharray}
   198 
   199   @{rail \<open>
   200   @@{ML_antiquotation class} nameref
   201   ;
   202   @@{ML_antiquotation sort} sort
   203   ;
   204   (@@{ML_antiquotation type_name} |
   205    @@{ML_antiquotation type_abbrev} |
   206    @@{ML_antiquotation nonterminal}) nameref
   207   ;
   208   @@{ML_antiquotation typ} type
   209   \<close>}
   210 
   211   \begin{description}
   212 
   213   \item @{text "@{class c}"} inlines the internalized class @{text
   214   "c"} --- as @{ML_type string} literal.
   215 
   216   \item @{text "@{sort s}"} inlines the internalized sort @{text "s"}
   217   --- as @{ML_type "string list"} literal.
   218 
   219   \item @{text "@{type_name c}"} inlines the internalized type
   220   constructor @{text "c"} --- as @{ML_type string} literal.
   221 
   222   \item @{text "@{type_abbrev c}"} inlines the internalized type
   223   abbreviation @{text "c"} --- as @{ML_type string} literal.
   224 
   225   \item @{text "@{nonterminal c}"} inlines the internalized syntactic
   226   type~/ grammar nonterminal @{text "c"} --- as @{ML_type string}
   227   literal.
   228 
   229   \item @{text "@{typ \<tau>}"} inlines the internalized type @{text "\<tau>"}
   230   --- as constructor term for datatype @{ML_type typ}.
   231 
   232   \end{description}
   233 *}
   234 
   235 
   236 section {* Terms \label{sec:terms} *}
   237 
   238 text {*
   239   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
   240   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
   241   or \cite{paulson-ml2}), with the types being determined by the
   242   corresponding binders.  In contrast, free variables and constants
   243   have an explicit name and type in each occurrence.
   244 
   245   \medskip A \emph{bound variable} is a natural number @{text "b"},
   246   which accounts for the number of intermediate binders between the
   247   variable occurrence in the body and its binding position.  For
   248   example, the de-Bruijn term @{text "\<lambda>\<^bsub>bool\<^esub>. \<lambda>\<^bsub>bool\<^esub>. 1 \<and> 0"} would
   249   correspond to @{text "\<lambda>x\<^bsub>bool\<^esub>. \<lambda>y\<^bsub>bool\<^esub>. x \<and> y"} in a named
   250   representation.  Note that a bound variable may be represented by
   251   different de-Bruijn indices at different occurrences, depending on
   252   the nesting of abstractions.
   253 
   254   A \emph{loose variable} is a bound variable that is outside the
   255   scope of local binders.  The types (and names) for loose variables
   256   can be managed as a separate context, that is maintained as a stack
   257   of hypothetical binders.  The core logic operates on closed terms,
   258   without any loose variables.
   259 
   260   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
   261   @{text "(x, \<tau>)"} which is usually printed @{text "x\<^sub>\<tau>"} here.  A
   262   \emph{schematic variable} is a pair of an indexname and a type,
   263   e.g.\ @{text "((x, 0), \<tau>)"} which is likewise printed as @{text
   264   "?x\<^sub>\<tau>"}.
   265 
   266   \medskip A \emph{constant} is a pair of a basic name and a type,
   267   e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text "c\<^sub>\<tau>"}
   268   here.  Constants are declared in the context as polymorphic families
   269   @{text "c :: \<sigma>"}, meaning that all substitution instances @{text
   270   "c\<^sub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
   271 
   272   The vector of \emph{type arguments} of constant @{text "c\<^sub>\<tau>"} wrt.\
   273   the declaration @{text "c :: \<sigma>"} is defined as the codomain of the
   274   matcher @{text "\<vartheta> = {?\<alpha>\<^sub>1 \<mapsto> \<tau>\<^sub>1, \<dots>, ?\<alpha>\<^sub>n \<mapsto> \<tau>\<^sub>n}"} presented in
   275   canonical order @{text "(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n)"}, corresponding to the
   276   left-to-right occurrences of the @{text "\<alpha>\<^sub>i"} in @{text "\<sigma>"}.
   277   Within a given theory context, there is a one-to-one correspondence
   278   between any constant @{text "c\<^sub>\<tau>"} and the application @{text "c(\<tau>\<^sub>1,
   279   \<dots>, \<tau>\<^sub>n)"} of its type arguments.  For example, with @{text "plus :: \<alpha>
   280   \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} corresponds to
   281   @{text "plus(nat)"}.
   282 
   283   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
   284   for type variables in @{text "\<sigma>"}.  These are observed by
   285   type-inference as expected, but \emph{ignored} by the core logic.
   286   This means the primitive logic is able to reason with instances of
   287   polymorphic constants that the user-level type-checker would reject
   288   due to violation of type class restrictions.
   289 
   290   \medskip An \emph{atomic term} is either a variable or constant.
   291   The logical category \emph{term} is defined inductively over atomic
   292   terms, with abstraction and application as follows: @{text "t = b |
   293   x\<^sub>\<tau> | ?x\<^sub>\<tau> | c\<^sub>\<tau> | \<lambda>\<^sub>\<tau>. t | t\<^sub>1 t\<^sub>2"}.  Parsing and printing takes care of
   294   converting between an external representation with named bound
   295   variables.  Subsequently, we shall use the latter notation instead
   296   of internal de-Bruijn representation.
   297 
   298   The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a
   299   term according to the structure of atomic terms, abstractions, and
   300   applications:
   301   \[
   302   \infer{@{text "a\<^sub>\<tau> :: \<tau>"}}{}
   303   \qquad
   304   \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}
   305   \qquad
   306   \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}
   307   \]
   308   A \emph{well-typed term} is a term that can be typed according to these rules.
   309 
   310   Typing information can be omitted: type-inference is able to
   311   reconstruct the most general type of a raw term, while assigning
   312   most general types to all of its variables and constants.
   313   Type-inference depends on a context of type constraints for fixed
   314   variables, and declarations for polymorphic constants.
   315 
   316   The identity of atomic terms consists both of the name and the type
   317   component.  This means that different variables @{text
   318   "x\<^bsub>\<tau>\<^sub>1\<^esub>"} and @{text "x\<^bsub>\<tau>\<^sub>2\<^esub>"} may become the same after
   319   type instantiation.  Type-inference rejects variables of the same
   320   name, but different types.  In contrast, mixed instances of
   321   polymorphic constants occur routinely.
   322 
   323   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
   324   is the set of type variables occurring in @{text "t"}, but not in
   325   its type @{text "\<sigma>"}.  This means that the term implicitly depends
   326   on type arguments that are not accounted in the result type, i.e.\
   327   there are different type instances @{text "t\<vartheta> :: \<sigma>"} and
   328   @{text "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly
   329   pathological situation notoriously demands additional care.
   330 
   331   \medskip A \emph{term abbreviation} is a syntactic definition @{text
   332   "c\<^sub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},
   333   without any hidden polymorphism.  A term abbreviation looks like a
   334   constant in the syntax, but is expanded before entering the logical
   335   core.  Abbreviations are usually reverted when printing terms, using
   336   @{text "t \<rightarrow> c\<^sub>\<sigma>"} as rules for higher-order rewriting.
   337 
   338   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
   339   "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free
   340   renaming of bound variables; @{text "\<beta>"}-conversion contracts an
   341   abstraction applied to an argument term, substituting the argument
   342   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
   343   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
   344   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
   345   does not occur in @{text "f"}.
   346 
   347   Terms are normally treated modulo @{text "\<alpha>"}-conversion, which is
   348   implicit in the de-Bruijn representation.  Names for bound variables
   349   in abstractions are maintained separately as (meaningless) comments,
   350   mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is
   351   commonplace in various standard operations (\secref{sec:obj-rules})
   352   that are based on higher-order unification and matching.
   353 *}
   354 
   355 text %mlref {*
   356   \begin{mldecls}
   357   @{index_ML_type term} \\
   358   @{index_ML_op "aconv": "term * term -> bool"} \\
   359   @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
   360   @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   361   @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
   362   @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   363   \end{mldecls}
   364   \begin{mldecls}
   365   @{index_ML fastype_of: "term -> typ"} \\
   366   @{index_ML lambda: "term -> term -> term"} \\
   367   @{index_ML betapply: "term * term -> term"} \\
   368   @{index_ML incr_boundvars: "int -> term -> term"} \\
   369   @{index_ML Sign.declare_const: "Proof.context ->
   370   (binding * typ) * mixfix -> theory -> term * theory"} \\
   371   @{index_ML Sign.add_abbrev: "string -> binding * term ->
   372   theory -> (term * term) * theory"} \\
   373   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   374   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   375   \end{mldecls}
   376 
   377   \begin{description}
   378 
   379   \item Type @{ML_type term} represents de-Bruijn terms, with comments
   380   in abstractions, and explicitly named free variables and constants;
   381   this is a datatype with constructors @{index_ML Bound}, @{index_ML
   382   Free}, @{index_ML Var}, @{index_ML Const}, @{index_ML Abs},
   383   @{index_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>\<^sub>1, \<dots>, \<tau>\<^sub>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 \<open>
   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   \<close>}
   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\<^sub>1, \<dots>, A\<^sub>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, see also
   559   \secref{sec:proof-terms}.  Thus all three levels of @{text
   560   "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for terms, and @{text
   561   "\<And>/\<Longrightarrow>"} for proofs (cf.\ \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\<^sub>\<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>\<^sub>i)"} for some @{text "\<alpha>\<^sub>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 Logic.all: "term -> term -> term"} \\
   637   @{index_ML Logic.mk_implies: "term * term -> term"} \\
   638   \end{mldecls}
   639   \begin{mldecls}
   640   @{index_ML_type ctyp} \\
   641   @{index_ML_type cterm} \\
   642   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
   643   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
   644   @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\
   645   @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
   646   @{index_ML Thm.all: "cterm -> cterm -> cterm"} \\
   647   @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
   648   \end{mldecls}
   649   \begin{mldecls}
   650   @{index_ML_type thm} \\
   651   @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
   652   @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
   653   @{index_ML Thm.assume: "cterm -> thm"} \\
   654   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   655   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
   656   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   657   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
   658   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   659   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
   660   @{index_ML Thm.add_axiom: "Proof.context ->
   661   binding * term -> theory -> (string * thm) * theory"} \\
   662   @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
   663   (string * ('a -> thm)) * theory"} \\
   664   @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->
   665   binding * term -> theory -> (string * thm) * theory"} \\
   666   \end{mldecls}
   667   \begin{mldecls}
   668   @{index_ML Theory.add_deps: "Proof.context -> string ->
   669   string * typ -> (string * typ) list -> theory -> theory"} \\
   670   \end{mldecls}
   671 
   672   \begin{description}
   673 
   674   \item @{ML Thm.peek_status}~@{text "thm"} informs about the current
   675   status of the derivation object behind the given theorem.  This is a
   676   snapshot of a potentially ongoing (parallel) evaluation of proofs.
   677   The three Boolean values indicate the following: @{verbatim oracle}
   678   if the finished part contains some oracle invocation; @{verbatim
   679   unfinished} if some future proofs are still pending; @{verbatim
   680   failed} if some future proof has failed, rendering the theorem
   681   invalid!
   682 
   683   \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification
   684   @{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in
   685   the body proposition @{text "B"} are replaced by bound variables.
   686   (See also @{ML lambda} on terms.)
   687 
   688   \item @{ML Logic.mk_implies}~@{text "(A, B)"} produces a Pure
   689   implication @{text "A \<Longrightarrow> B"}.
   690 
   691   \item Types @{ML_type ctyp} and @{ML_type cterm} represent certified
   692   types and terms, respectively.  These are abstract datatypes that
   693   guarantee that its values have passed the full well-formedness (and
   694   well-typedness) checks, relative to the declarations of type
   695   constructors, constants etc.\ in the background theory.  The
   696   abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the
   697   same inference kernel that is mainly responsible for @{ML_type thm}.
   698   Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}
   699   are located in the @{ML_structure Thm} module, even though theorems are
   700   not yet involved at that stage.
   701 
   702   \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
   703   Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,
   704   respectively.  This also involves some basic normalizations, such
   705   expansion of type and term abbreviations from the theory context.
   706   Full re-certification is relatively slow and should be avoided in
   707   tight reasoning loops.
   708 
   709   \item @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML
   710   Drule.mk_implies} etc.\ compose certified terms (or propositions)
   711   incrementally.  This is equivalent to @{ML Thm.cterm_of} after
   712   unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML
   713   Logic.mk_implies} etc., but there can be a big difference in
   714   performance when large existing entities are composed by a few extra
   715   constructions on top.  There are separate operations to decompose
   716   certified terms and theorems to produce certified terms again.
   717 
   718   \item Type @{ML_type thm} represents proven propositions.  This is
   719   an abstract datatype that guarantees that its values have been
   720   constructed by basic principles of the @{ML_structure Thm} module.
   721   Every @{ML_type thm} value refers its background theory,
   722   cf.\ \secref{sec:context-theory}.
   723 
   724   \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given
   725   theorem to a \emph{larger} theory, see also \secref{sec:context}.
   726   This formal adjustment of the background context has no logical
   727   significance, but is occasionally required for formal reasons, e.g.\
   728   when theorems that are imported from more basic theories are used in
   729   the current situation.
   730 
   731   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
   732   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
   733   correspond to the primitive inferences of \figref{fig:prim-rules}.
   734 
   735   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
   736   corresponds to the @{text "generalize"} rules of
   737   \figref{fig:subst-rules}.  Here collections of type and term
   738   variables are generalized simultaneously, specified by the given
   739   basic names.
   740 
   741   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^sub>s,
   742   \<^vec>x\<^sub>\<tau>)"} corresponds to the @{text "instantiate"} rules
   743   of \figref{fig:subst-rules}.  Type variables are substituted before
   744   term variables.  Note that the types in @{text "\<^vec>x\<^sub>\<tau>"}
   745   refer to the instantiated versions.
   746 
   747   \item @{ML Thm.add_axiom}~@{text "ctxt (name, A)"} declares an
   748   arbitrary proposition as axiom, and retrieves it as a theorem from
   749   the resulting theory, cf.\ @{text "axiom"} in
   750   \figref{fig:prim-rules}.  Note that the low-level representation in
   751   the axiom table may differ slightly from the returned theorem.
   752 
   753   \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named
   754   oracle rule, essentially generating arbitrary axioms on the fly,
   755   cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
   756 
   757   \item @{ML Thm.add_def}~@{text "ctxt unchecked overloaded (name, c
   758   \<^vec>x \<equiv> t)"} states a definitional axiom for an existing constant
   759   @{text "c"}.  Dependencies are recorded via @{ML Theory.add_deps},
   760   unless the @{text "unchecked"} option is set.  Note that the
   761   low-level representation in the axiom table may differ slightly from
   762   the returned theorem.
   763 
   764   \item @{ML Theory.add_deps}~@{text "ctxt name c\<^sub>\<tau> \<^vec>d\<^sub>\<sigma>"}
   765   declares dependencies of a named specification for constant @{text
   766   "c\<^sub>\<tau>"}, relative to existing specifications for constants @{text
   767   "\<^vec>d\<^sub>\<sigma>"}.
   768 
   769   \end{description}
   770 *}
   771 
   772 
   773 text %mlantiq {*
   774   \begin{matharray}{rcl}
   775   @{ML_antiquotation_def "ctyp"} & : & @{text ML_antiquotation} \\
   776   @{ML_antiquotation_def "cterm"} & : & @{text ML_antiquotation} \\
   777   @{ML_antiquotation_def "cprop"} & : & @{text ML_antiquotation} \\
   778   @{ML_antiquotation_def "thm"} & : & @{text ML_antiquotation} \\
   779   @{ML_antiquotation_def "thms"} & : & @{text ML_antiquotation} \\
   780   @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\
   781   \end{matharray}
   782 
   783   @{rail \<open>
   784   @@{ML_antiquotation ctyp} typ
   785   ;
   786   @@{ML_antiquotation cterm} term
   787   ;
   788   @@{ML_antiquotation cprop} prop
   789   ;
   790   @@{ML_antiquotation thm} thmref
   791   ;
   792   @@{ML_antiquotation thms} thmrefs
   793   ;
   794   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
   795     @'by' method method?
   796   \<close>}
   797 
   798   \begin{description}
   799 
   800   \item @{text "@{ctyp \<tau>}"} produces a certified type wrt.\ the
   801   current background theory --- as abstract value of type @{ML_type
   802   ctyp}.
   803 
   804   \item @{text "@{cterm t}"} and @{text "@{cprop \<phi>}"} produce a
   805   certified term wrt.\ the current background theory --- as abstract
   806   value of type @{ML_type cterm}.
   807 
   808   \item @{text "@{thm a}"} produces a singleton fact --- as abstract
   809   value of type @{ML_type thm}.
   810 
   811   \item @{text "@{thms a}"} produces a general fact --- as abstract
   812   value of type @{ML_type "thm list"}.
   813 
   814   \item @{text "@{lemma \<phi> by meth}"} produces a fact that is proven on
   815   the spot according to the minimal proof, which imitates a terminal
   816   Isar proof.  The result is an abstract value of type @{ML_type thm}
   817   or @{ML_type "thm list"}, depending on the number of propositions
   818   given here.
   819 
   820   The internal derivation object lacks a proper theorem name, but it
   821   is formally closed, unless the @{text "(open)"} option is specified
   822   (this may impact performance of applications with proof terms).
   823 
   824   Since ML antiquotations are always evaluated at compile-time, there
   825   is no run-time overhead even for non-trivial proofs.  Nonetheless,
   826   the justification is syntactically limited to a single @{command
   827   "by"} step.  More complex Isar proofs should be done in regular
   828   theory source, before compiling the corresponding ML text that uses
   829   the result.
   830 
   831   \end{description}
   832 
   833 *}
   834 
   835 
   836 subsection {* Auxiliary connectives \label{sec:logic-aux} *}
   837 
   838 text {* Theory @{text "Pure"} provides a few auxiliary connectives
   839   that are defined on top of the primitive ones, see
   840   \figref{fig:pure-aux}.  These special constants are useful in
   841   certain internal encodings, and are normally not directly exposed to
   842   the user.
   843 
   844   \begin{figure}[htb]
   845   \begin{center}
   846   \begin{tabular}{ll}
   847   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&&&"}) \\
   848   @{text "\<turnstile> A &&& B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
   849   @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\
   850   @{text "#A \<equiv> A"} \\[1ex]
   851   @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
   852   @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
   853   @{text "type :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
   854   @{text "(unspecified)"} \\
   855   \end{tabular}
   856   \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   857   \end{center}
   858   \end{figure}
   859 
   860   The introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &&& B"}, and eliminations
   861   (projections) @{text "A &&& B \<Longrightarrow> A"} and @{text "A &&& B \<Longrightarrow> B"} are
   862   available as derived rules.  Conjunction allows to treat
   863   simultaneous assumptions and conclusions uniformly, e.g.\ consider
   864   @{text "A \<Longrightarrow> B \<Longrightarrow> C &&& D"}.  In particular, the goal mechanism
   865   represents multiple claims as explicit conjunction internally, but
   866   this is refined (via backwards introduction) into separate sub-goals
   867   before the user commences the proof; the final result is projected
   868   into a list of theorems using eliminations (cf.\
   869   \secref{sec:tactical-goals}).
   870 
   871   The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex
   872   propositions appear as atomic, without changing the meaning: @{text
   873   "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable.  See
   874   \secref{sec:tactical-goals} for specific operations.
   875 
   876   The @{text "term"} marker turns any well-typed term into a derivable
   877   proposition: @{text "\<turnstile> TERM t"} holds unconditionally.  Although
   878   this is logically vacuous, it allows to treat terms and proofs
   879   uniformly, similar to a type-theoretic framework.
   880 
   881   The @{text "TYPE"} constructor is the canonical representative of
   882   the unspecified type @{text "\<alpha> itself"}; it essentially injects the
   883   language of types into that of terms.  There is specific notation
   884   @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau> itself\<^esub>"}.
   885   Although being devoid of any particular meaning, the term @{text
   886   "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term
   887   language.  In particular, @{text "TYPE(\<alpha>)"} may be used as formal
   888   argument in primitive definitions, in order to circumvent hidden
   889   polymorphism (cf.\ \secref{sec:terms}).  For example, @{text "c
   890   TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of
   891   a proposition @{text "A"} that depends on an additional type
   892   argument, which is essentially a predicate on types.
   893 *}
   894 
   895 text %mlref {*
   896   \begin{mldecls}
   897   @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
   898   @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
   899   @{index_ML Drule.mk_term: "cterm -> thm"} \\
   900   @{index_ML Drule.dest_term: "thm -> cterm"} \\
   901   @{index_ML Logic.mk_type: "typ -> term"} \\
   902   @{index_ML Logic.dest_type: "term -> typ"} \\
   903   \end{mldecls}
   904 
   905   \begin{description}
   906 
   907   \item @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text
   908   "A"} and @{text "B"}.
   909 
   910   \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}
   911   from @{text "A &&& B"}.
   912 
   913   \item @{ML Drule.mk_term} derives @{text "TERM t"}.
   914 
   915   \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text
   916   "TERM t"}.
   917 
   918   \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text
   919   "TYPE(\<tau>)"}.
   920 
   921   \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type
   922   @{text "\<tau>"}.
   923 
   924   \end{description}
   925 *}
   926 
   927 
   928 subsection {* Sort hypotheses *}
   929 
   930 text {* Type variables are decorated with sorts, as explained in
   931   \secref{sec:types}.  This constrains type instantiation to certain
   932   ranges of types: variable @{text "\<alpha>\<^sub>s"} may only be assigned to types
   933   @{text "\<tau>"} that belong to sort @{text "s"}.  Within the logic, sort
   934   constraints act like implicit preconditions on the result @{text
   935   "\<lparr>\<alpha>\<^sub>1 : s\<^sub>1\<rparr>, \<dots>, \<lparr>\<alpha>\<^sub>n : s\<^sub>n\<rparr>, \<Gamma> \<turnstile> \<phi>"} where the type variables @{text
   936   "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} cover the propositions @{text "\<Gamma>"}, @{text "\<phi>"}, as
   937   well as the proof of @{text "\<Gamma> \<turnstile> \<phi>"}.
   938 
   939   These \emph{sort hypothesis} of a theorem are passed monotonically
   940   through further derivations.  They are redundant, as long as the
   941   statement of a theorem still contains the type variables that are
   942   accounted here.  The logical significance of sort hypotheses is
   943   limited to the boundary case where type variables disappear from the
   944   proposition, e.g.\ @{text "\<lparr>\<alpha>\<^sub>s : s\<rparr> \<turnstile> \<phi>"}.  Since such dangling type
   945   variables can be renamed arbitrarily without changing the
   946   proposition @{text "\<phi>"}, the inference kernel maintains sort
   947   hypotheses in anonymous form @{text "s \<turnstile> \<phi>"}.
   948 
   949   In most practical situations, such extra sort hypotheses may be
   950   stripped in a final bookkeeping step, e.g.\ at the end of a proof:
   951   they are typically left over from intermediate reasoning with type
   952   classes that can be satisfied by some concrete type @{text "\<tau>"} of
   953   sort @{text "s"} to replace the hypothetical type variable @{text
   954   "\<alpha>\<^sub>s"}.  *}
   955 
   956 text %mlref {*
   957   \begin{mldecls}
   958   @{index_ML Thm.extra_shyps: "thm -> sort list"} \\
   959   @{index_ML Thm.strip_shyps: "thm -> thm"} \\
   960   \end{mldecls}
   961 
   962   \begin{description}
   963 
   964   \item @{ML Thm.extra_shyps}~@{text "thm"} determines the extraneous
   965   sort hypotheses of the given theorem, i.e.\ the sorts that are not
   966   present within type variables of the statement.
   967 
   968   \item @{ML Thm.strip_shyps}~@{text "thm"} removes any extraneous
   969   sort hypotheses that can be witnessed from the type signature.
   970 
   971   \end{description}
   972 *}
   973 
   974 text %mlex {* The following artificial example demonstrates the
   975   derivation of @{prop False} with a pending sort hypothesis involving
   976   a logically empty sort.  *}
   977 
   978 class empty =
   979   assumes bad: "\<And>(x::'a) y. x \<noteq> y"
   980 
   981 theorem (in empty) false: False
   982   using bad by blast
   983 
   984 ML {*
   985   @{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])
   986 *}
   987 
   988 text {* Thanks to the inference kernel managing sort hypothesis
   989   according to their logical significance, this example is merely an
   990   instance of \emph{ex falso quodlibet consequitur} --- not a collapse
   991   of the logical framework! *}
   992 
   993 
   994 section {* Object-level rules \label{sec:obj-rules} *}
   995 
   996 text {*
   997   The primitive inferences covered so far mostly serve foundational
   998   purposes.  User-level reasoning usually works via object-level rules
   999   that are represented as theorems of Pure.  Composition of rules
  1000   involves \emph{backchaining}, \emph{higher-order unification} modulo
  1001   @{text "\<alpha>\<beta>\<eta>"}-conversion of @{text "\<lambda>"}-terms, and so-called
  1002   \emph{lifting} of rules into a context of @{text "\<And>"} and @{text
  1003   "\<Longrightarrow>"} connectives.  Thus the full power of higher-order Natural
  1004   Deduction in Isabelle/Pure becomes readily available.
  1005 *}
  1006 
  1007 
  1008 subsection {* Hereditary Harrop Formulae *}
  1009 
  1010 text {*
  1011   The idea of object-level rules is to model Natural Deduction
  1012   inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow
  1013   arbitrary nesting similar to \cite{extensions91}.  The most basic
  1014   rule format is that of a \emph{Horn Clause}:
  1015   \[
  1016   \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}
  1017   \]
  1018   where @{text "A, A\<^sub>1, \<dots>, A\<^sub>n"} are atomic propositions
  1019   of the framework, usually of the form @{text "Trueprop B"}, where
  1020   @{text "B"} is a (compound) object-level statement.  This
  1021   object-level inference corresponds to an iterated implication in
  1022   Pure like this:
  1023   \[
  1024   @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}
  1025   \]
  1026   As an example consider conjunction introduction: @{text "A \<Longrightarrow> B \<Longrightarrow> A \<and>
  1027   B"}.  Any parameters occurring in such rule statements are
  1028   conceptionally treated as arbitrary:
  1029   \[
  1030   @{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"}
  1031   \]
  1032 
  1033   Nesting of rules means that the positions of @{text "A\<^sub>i"} may
  1034   again hold compound rules, not just atomic propositions.
  1035   Propositions of this format are called \emph{Hereditary Harrop
  1036   Formulae} in the literature \cite{Miller:1991}.  Here we give an
  1037   inductive characterization as follows:
  1038 
  1039   \medskip
  1040   \begin{tabular}{ll}
  1041   @{text "\<^bold>x"} & set of variables \\
  1042   @{text "\<^bold>A"} & set of atomic propositions \\
  1043   @{text "\<^bold>H  =  \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\
  1044   \end{tabular}
  1045   \medskip
  1046 
  1047   Thus we essentially impose nesting levels on propositions formed
  1048   from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a prefix
  1049   of parameters and compound premises, concluding an atomic
  1050   proposition.  Typical examples are @{text "\<longrightarrow>"}-introduction @{text
  1051   "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n
  1052   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}.  Even deeper nesting occurs in well-founded
  1053   induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this
  1054   already marks the limit of rule complexity that is usually seen in
  1055   practice.
  1056 
  1057   \medskip Regular user-level inferences in Isabelle/Pure always
  1058   maintain the following canonical form of results:
  1059 
  1060   \begin{itemize}
  1061 
  1062   \item Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"},
  1063   which is a theorem of Pure, means that quantifiers are pushed in
  1064   front of implication at each level of nesting.  The normal form is a
  1065   Hereditary Harrop Formula.
  1066 
  1067   \item The outermost prefix of parameters is represented via
  1068   schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x
  1069   \<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.
  1070   Note that this representation looses information about the order of
  1071   parameters, and vacuous quantifiers vanish automatically.
  1072 
  1073   \end{itemize}
  1074 *}
  1075 
  1076 text %mlref {*
  1077   \begin{mldecls}
  1078   @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\
  1079   \end{mldecls}
  1080 
  1081   \begin{description}
  1082 
  1083   \item @{ML Simplifier.norm_hhf}~@{text "ctxt thm"} normalizes the given
  1084   theorem according to the canonical form specified above.  This is
  1085   occasionally helpful to repair some low-level tools that do not
  1086   handle Hereditary Harrop Formulae properly.
  1087 
  1088   \end{description}
  1089 *}
  1090 
  1091 
  1092 subsection {* Rule composition *}
  1093 
  1094 text {*
  1095   The rule calculus of Isabelle/Pure provides two main inferences:
  1096   @{inference resolution} (i.e.\ back-chaining of rules) and
  1097   @{inference assumption} (i.e.\ closing a branch), both modulo
  1098   higher-order unification.  There are also combined variants, notably
  1099   @{inference elim_resolution} and @{inference dest_resolution}.
  1100 
  1101   To understand the all-important @{inference resolution} principle,
  1102   we first consider raw @{inference_def composition} (modulo
  1103   higher-order unification with substitution @{text "\<vartheta>"}):
  1104   \[
  1105   \infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}
  1106   {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}
  1107   \]
  1108   Here the conclusion of the first rule is unified with the premise of
  1109   the second; the resulting rule instance inherits the premises of the
  1110   first and conclusion of the second.  Note that @{text "C"} can again
  1111   consist of iterated implications.  We can also permute the premises
  1112   of the second rule back-and-forth in order to compose with @{text
  1113   "B'"} in any position (subsequently we shall always refer to
  1114   position 1 w.l.o.g.).
  1115 
  1116   In @{inference composition} the internal structure of the common
  1117   part @{text "B"} and @{text "B'"} is not taken into account.  For
  1118   proper @{inference resolution} we require @{text "B"} to be atomic,
  1119   and explicitly observe the structure @{text "\<And>\<^vec>x. \<^vec>H
  1120   \<^vec>x \<Longrightarrow> B' \<^vec>x"} of the premise of the second rule.  The
  1121   idea is to adapt the first rule by ``lifting'' it into this context,
  1122   by means of iterated application of the following inferences:
  1123   \[
  1124   \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}
  1125   \]
  1126   \[
  1127   \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"}}
  1128   \]
  1129   By combining raw composition with lifting, we get full @{inference
  1130   resolution} as follows:
  1131   \[
  1132   \infer[(@{inference_def resolution})]
  1133   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
  1134   {\begin{tabular}{l}
  1135     @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\
  1136     @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
  1137     @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
  1138    \end{tabular}}
  1139   \]
  1140 
  1141   Continued resolution of rules allows to back-chain a problem towards
  1142   more and sub-problems.  Branches are closed either by resolving with
  1143   a rule of 0 premises, or by producing a ``short-circuit'' within a
  1144   solved situation (again modulo unification):
  1145   \[
  1146   \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}
  1147   {@{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})}}
  1148   \]
  1149 
  1150   %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
  1151 *}
  1152 
  1153 text %mlref {*
  1154   \begin{mldecls}
  1155   @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\
  1156   @{index_ML_op "RS": "thm * thm -> thm"} \\
  1157 
  1158   @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\
  1159   @{index_ML_op "RL": "thm list * thm list -> thm list"} \\
  1160 
  1161   @{index_ML_op "MRS": "thm list * thm -> thm"} \\
  1162   @{index_ML_op "OF": "thm * thm list -> thm"} \\
  1163   \end{mldecls}
  1164 
  1165   \begin{description}
  1166 
  1167   \item @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of
  1168   @{text "rule\<^sub>1"} with the @{text i}-th premise of @{text "rule\<^sub>2"},
  1169   according to the @{inference resolution} principle explained above.
  1170   Unless there is precisely one resolvent it raises exception @{ML
  1171   THM}.
  1172 
  1173   This corresponds to the rule attribute @{attribute THEN} in Isar
  1174   source language.
  1175 
  1176   \item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RSN (1,
  1177   rule\<^sub>2)"}.
  1178 
  1179   \item @{text "rules\<^sub>1 RLN (i, rules\<^sub>2)"} joins lists of rules.  For
  1180   every @{text "rule\<^sub>1"} in @{text "rules\<^sub>1"} and @{text "rule\<^sub>2"} in
  1181   @{text "rules\<^sub>2"}, it resolves the conclusion of @{text "rule\<^sub>1"} with
  1182   the @{text "i"}-th premise of @{text "rule\<^sub>2"}, accumulating multiple
  1183   results in one big list.  Note that such strict enumerations of
  1184   higher-order unifications can be inefficient compared to the lazy
  1185   variant seen in elementary tactics like @{ML resolve_tac}.
  1186 
  1187   \item @{text "rules\<^sub>1 RL rules\<^sub>2"} abbreviates @{text "rules\<^sub>1 RLN (1,
  1188   rules\<^sub>2)"}.
  1189 
  1190   \item @{text "[rule\<^sub>1, \<dots>, rule\<^sub>n] MRS rule"} resolves @{text "rule\<^sub>i"}
  1191   against premise @{text "i"} of @{text "rule"}, for @{text "i = n, \<dots>,
  1192   1"}.  By working from right to left, newly emerging premises are
  1193   concatenated in the result, without interfering.
  1194 
  1195   \item @{text "rule OF rules"} is an alternative notation for @{text
  1196   "rules MRS rule"}, which makes rule composition look more like
  1197   function application.  Note that the argument @{text "rules"} need
  1198   not be atomic.
  1199 
  1200   This corresponds to the rule attribute @{attribute OF} in Isar
  1201   source language.
  1202 
  1203   \end{description}
  1204 *}
  1205 
  1206 
  1207 section {* Proof terms \label{sec:proof-terms} *}
  1208 
  1209 text {* The Isabelle/Pure inference kernel can record the proof of
  1210   each theorem as a proof term that contains all logical inferences in
  1211   detail.  Rule composition by resolution (\secref{sec:obj-rules}) and
  1212   type-class reasoning is broken down to primitive rules of the
  1213   logical framework.  The proof term can be inspected by a separate
  1214   proof-checker, for example.
  1215 
  1216   According to the well-known \emph{Curry-Howard isomorphism}, a proof
  1217   can be viewed as a @{text "\<lambda>"}-term. Following this idea, proofs in
  1218   Isabelle are internally represented by a datatype similar to the one
  1219   for terms described in \secref{sec:terms}.  On top of these
  1220   syntactic terms, two more layers of @{text "\<lambda>"}-calculus are added,
  1221   which correspond to @{text "\<And>x :: \<alpha>. B x"} and @{text "A \<Longrightarrow> B"}
  1222   according to the propositions-as-types principle.  The resulting
  1223   3-level @{text "\<lambda>"}-calculus resembles ``@{text "\<lambda>HOL"}'' in the
  1224   more abstract setting of Pure Type Systems (PTS)
  1225   \cite{Barendregt-Geuvers:2001}, if some fine points like schematic
  1226   polymorphism and type classes are ignored.
  1227 
  1228   \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}
  1229   or @{text "\<^bold>\<lambda>p : A. prf"} correspond to introduction of @{text
  1230   "\<And>"}/@{text "\<Longrightarrow>"}, and \emph{proof applications} of the form @{text
  1231   "p \<cdot> t"} or @{text "p \<bullet> q"} correspond to elimination of @{text
  1232   "\<And>"}/@{text "\<Longrightarrow>"}.  Actual types @{text "\<alpha>"}, propositions @{text
  1233   "A"}, and terms @{text "t"} might be suppressed and reconstructed
  1234   from the overall proof term.
  1235 
  1236   \medskip Various atomic proofs indicate special situations within
  1237   the proof construction as follows.
  1238 
  1239   A \emph{bound proof variable} is a natural number @{text "b"} that
  1240   acts as de-Bruijn index for proof term abstractions.
  1241 
  1242   A \emph{minimal proof} ``@{text "?"}'' is a dummy proof term.  This
  1243   indicates some unrecorded part of the proof.
  1244 
  1245   @{text "Hyp A"} refers to some pending hypothesis by giving its
  1246   proposition.  This indicates an open context of implicit hypotheses,
  1247   similar to loose bound variables or free variables within a term
  1248   (\secref{sec:terms}).
  1249 
  1250   An \emph{axiom} or \emph{oracle} @{text "a : A[\<^vec>\<tau>]"} refers
  1251   some postulated @{text "proof constant"}, which is subject to
  1252   schematic polymorphism of theory content, and the particular type
  1253   instantiation may be given explicitly.  The vector of types @{text
  1254   "\<^vec>\<tau>"} refers to the schematic type variables in the generic
  1255   proposition @{text "A"} in canonical order.
  1256 
  1257   A \emph{proof promise} @{text "a : A[\<^vec>\<tau>]"} is a placeholder
  1258   for some proof of polymorphic proposition @{text "A"}, with explicit
  1259   type instantiation as given by the vector @{text "\<^vec>\<tau>"}, as
  1260   above.  Unlike axioms or oracles, proof promises may be
  1261   \emph{fulfilled} eventually, by substituting @{text "a"} by some
  1262   particular proof @{text "q"} at the corresponding type instance.
  1263   This acts like Hindley-Milner @{text "let"}-polymorphism: a generic
  1264   local proof definition may get used at different type instances, and
  1265   is replaced by the concrete instance eventually.
  1266 
  1267   A \emph{named theorem} wraps up some concrete proof as a closed
  1268   formal entity, in the manner of constant definitions for proof
  1269   terms.  The \emph{proof body} of such boxed theorems involves some
  1270   digest about oracles and promises occurring in the original proof.
  1271   This allows the inference kernel to manage this critical information
  1272   without the full overhead of explicit proof terms.
  1273 *}
  1274 
  1275 
  1276 subsection {* Reconstructing and checking proof terms *}
  1277 
  1278 text {* Fully explicit proof terms can be large, but most of this
  1279   information is redundant and can be reconstructed from the context.
  1280   Therefore, the Isabelle/Pure inference kernel records only
  1281   \emph{implicit} proof terms, by omitting all typing information in
  1282   terms, all term and type labels of proof abstractions, and some
  1283   argument terms of applications @{text "p \<cdot> t"} (if possible).
  1284 
  1285   There are separate operations to reconstruct the full proof term
  1286   later on, using \emph{higher-order pattern unification}
  1287   \cite{nipkow-patterns,Berghofer-Nipkow:2000:TPHOL}.
  1288 
  1289   The \emph{proof checker} expects a fully reconstructed proof term,
  1290   and can turn it into a theorem by replaying its primitive inferences
  1291   within the kernel.  *}
  1292 
  1293 
  1294 subsection {* Concrete syntax of proof terms *}
  1295 
  1296 text {* The concrete syntax of proof terms is a slight extension of
  1297   the regular inner syntax of Isabelle/Pure \cite{isabelle-isar-ref}.
  1298   Its main syntactic category @{syntax (inner) proof} is defined as
  1299   follows:
  1300 
  1301   \begin{center}
  1302   \begin{supertabular}{rclr}
  1303 
  1304   @{syntax_def (inner) proof} & = & @{verbatim Lam} @{text params} @{verbatim "."} @{text proof} \\
  1305     & @{text "|"} & @{text "\<^bold>\<lambda>"} @{text "params"} @{verbatim "."} @{text proof} \\
  1306     & @{text "|"} & @{text proof} @{verbatim "%"} @{text any} \\
  1307     & @{text "|"} & @{text proof} @{text "\<cdot>"} @{text any} \\
  1308     & @{text "|"} & @{text proof} @{verbatim "%%"} @{text proof} \\
  1309     & @{text "|"} & @{text proof} @{text "\<bullet>"} @{text proof} \\
  1310     & @{text "|"} & @{text "id  |  longid"} \\
  1311   \\
  1312 
  1313   @{text param} & = & @{text idt} \\
  1314     & @{text "|"} & @{text idt} @{verbatim ":"} @{text prop} \\
  1315     & @{text "|"} & @{verbatim "("} @{text param} @{verbatim ")"} \\
  1316   \\
  1317 
  1318   @{text params} & = & @{text param} \\
  1319     & @{text "|"} & @{text param} @{text params} \\
  1320 
  1321   \end{supertabular}
  1322   \end{center}
  1323 
  1324   Implicit term arguments in partial proofs are indicated by ``@{text
  1325   "_"}''.  Type arguments for theorems and axioms may be specified
  1326   using @{text "p \<cdot> TYPE(type)"} (they must appear before any other
  1327   term argument of a theorem or axiom, but may be omitted altogether).
  1328 
  1329   \medskip There are separate read and print operations for proof
  1330   terms, in order to avoid conflicts with the regular term language.
  1331 *}
  1332 
  1333 text %mlref {*
  1334   \begin{mldecls}
  1335   @{index_ML_type proof} \\
  1336   @{index_ML_type proof_body} \\
  1337   @{index_ML proofs: "int Unsynchronized.ref"} \\
  1338   @{index_ML Reconstruct.reconstruct_proof:
  1339   "theory -> term -> proof -> proof"} \\
  1340   @{index_ML Reconstruct.expand_proof: "theory ->
  1341   (string * term option) list -> proof -> proof"} \\
  1342   @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
  1343   @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
  1344   @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
  1345   \end{mldecls}
  1346 
  1347   \begin{description}
  1348 
  1349   \item Type @{ML_type proof} represents proof terms; this is a
  1350   datatype with constructors @{index_ML Abst}, @{index_ML AbsP},
  1351   @{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound},
  1352   @{index_ML MinProof}, @{index_ML Hyp}, @{index_ML PAxm}, @{index_ML
  1353   Oracle}, @{index_ML Promise}, @{index_ML PThm} as explained above.
  1354   %FIXME OfClass (!?)
  1355 
  1356   \item Type @{ML_type proof_body} represents the nested proof
  1357   information of a named theorem, consisting of a digest of oracles
  1358   and named theorem over some proof term.  The digest only covers the
  1359   directly visible part of the proof: in order to get the full
  1360   information, the implicit graph of nested theorems needs to be
  1361   traversed (e.g.\ using @{ML Proofterm.fold_body_thms}).
  1362 
  1363   \item @{ML Thm.proof_of}~@{text "thm"} and @{ML
  1364   Thm.proof_body_of}~@{text "thm"} produce the proof term or proof
  1365   body (with digest of oracles and theorems) from a given theorem.
  1366   Note that this involves a full join of internal futures that fulfill
  1367   pending proof promises, and thus disrupts the natural bottom-up
  1368   construction of proofs by introducing dynamic ad-hoc dependencies.
  1369   Parallel performance may suffer by inspecting proof terms at
  1370   run-time.
  1371 
  1372   \item @{ML proofs} specifies the detail of proof recording within
  1373   @{ML_type thm} values produced by the inference kernel: @{ML 0}
  1374   records only the names of oracles, @{ML 1} records oracle names and
  1375   propositions, @{ML 2} additionally records full proof terms.
  1376   Officially named theorems that contribute to a result are recorded
  1377   in any case.
  1378 
  1379   \item @{ML Reconstruct.reconstruct_proof}~@{text "thy prop prf"}
  1380   turns the implicit proof term @{text "prf"} into a full proof of the
  1381   given proposition.
  1382 
  1383   Reconstruction may fail if @{text "prf"} is not a proof of @{text
  1384   "prop"}, or if it does not contain sufficient information for
  1385   reconstruction.  Failure may only happen for proofs that are
  1386   constructed manually, but not for those produced automatically by
  1387   the inference kernel.
  1388 
  1389   \item @{ML Reconstruct.expand_proof}~@{text "thy [thm\<^sub>1, \<dots>, thm\<^sub>n]
  1390   prf"} expands and reconstructs the proofs of all specified theorems,
  1391   with the given (full) proof.  Theorems that are not unique specified
  1392   via their name may be disambiguated by giving their proposition.
  1393 
  1394   \item @{ML Proof_Checker.thm_of_proof}~@{text "thy prf"} turns the
  1395   given (full) proof into a theorem, by replaying it using only
  1396   primitive rules of the inference kernel.
  1397 
  1398   \item @{ML Proof_Syntax.read_proof}~@{text "thy b\<^sub>1 b\<^sub>2 s"} reads in a
  1399   proof term. The Boolean flags indicate the use of sort and type
  1400   information.  Usually, typing information is left implicit and is
  1401   inferred during proof reconstruction.  %FIXME eliminate flags!?
  1402 
  1403   \item @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"}
  1404   pretty-prints the given proof term.
  1405 
  1406   \end{description}
  1407 *}
  1408 
  1409 text %mlex {* Detailed proof information of a theorem may be retrieved
  1410   as follows: *}
  1411 
  1412 lemma ex: "A \<and> B \<longrightarrow> B \<and> A"
  1413 proof
  1414   assume "A \<and> B"
  1415   then obtain B and A ..
  1416   then show "B \<and> A" ..
  1417 qed
  1418 
  1419 ML_val {*
  1420   (*proof body with digest*)
  1421   val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});
  1422 
  1423   (*proof term only*)
  1424   val prf = Proofterm.proof_of body;
  1425   Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
  1426 
  1427   (*all theorems used in the graph of nested proofs*)
  1428   val all_thms =
  1429     Proofterm.fold_body_thms
  1430       (fn (name, _, _) => insert (op =) name) [body] [];
  1431 *}
  1432 
  1433 text {* The result refers to various basic facts of Isabelle/HOL:
  1434   @{thm [source] HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source]
  1435   HOL.conjI} etc.  The combinator @{ML Proofterm.fold_body_thms}
  1436   recursively explores the graph of the proofs of all theorems being
  1437   used here.
  1438 
  1439   \medskip Alternatively, we may produce a proof term manually, and
  1440   turn it into a theorem as follows: *}
  1441 
  1442 ML_val {*
  1443   val thy = @{theory};
  1444   val prf =
  1445     Proof_Syntax.read_proof thy true false
  1446       "impI \<cdot> _ \<cdot> _ \<bullet> \
  1447       \   (\<^bold>\<lambda>H: _. \
  1448       \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
  1449       \       (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
  1450   val thm =
  1451     prf
  1452     |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
  1453     |> Proof_Checker.thm_of_proof thy
  1454     |> Drule.export_without_context;
  1455 *}
  1456 
  1457 text {* \medskip See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"}
  1458   for further examples, with export and import of proof terms via
  1459   XML/ML data representation.
  1460 *}
  1461 
  1462 end