src/Doc/IsarImplementation/Logic.thy
 author wenzelm Sat Jun 15 21:01:07 2013 +0200 (2013-06-15) changeset 52408 fa2dc6c6c94f parent 52407 e4662afb3483 child 52410 fb1fb867c146 permissions -rw-r--r--
updated operations on proof terms;
     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_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\<^isub>1, s\<^isub>2)"}

   163   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>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\<^isub>1, \<dots>,

   176   c\<^isub>n])"} declares a new class @{text "c"}, together with class

   177   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.

   178

   179   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,

   180   c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \<subseteq>

   181   c\<^isub>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 "

   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   "}

   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\<^isub>\<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\<^isub>\<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\<^isub>\<tau>"}

   268   here.  Constants are declared in the context as polymorphic families

   269   @{text "c :: \<sigma>"}, meaning that all substitution instances @{text

   270   "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.

   271

   272   The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"} wrt.\

   273   the declaration @{text "c :: \<sigma>"} is defined as the codomain of the

   274   matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>, ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in

   275   canonical order @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}, corresponding to the

   276   left-to-right occurrences of the @{text "\<alpha>\<^isub>i"} in @{text "\<sigma>"}.

   277   Within a given theory context, there is a one-to-one correspondence

   278   between any constant @{text "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1,

   279   \<dots>, \<tau>\<^isub>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\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>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   applicatins:

   301   $  302 \infer{@{text "a\<^isub>\<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>\<^isub>1\<^esub>"} and @{text "x\<^bsub>\<tau>\<^isub>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\<^isub>\<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\<^isub>\<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>\<^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, 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\<^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 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_struct 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_struct Thm} module.

   721   Every @{ML_type thm} value contains a sliding back-reference to the

   722   enclosing theory, 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>\<^isub>s,

   742   \<^vec>x\<^isub>\<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\<^isub>\<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\<^isub>\<tau> \<^vec>d\<^isub>\<sigma>"}

   765   declares dependencies of a named specification for constant @{text

   766   "c\<^isub>\<tau>"}, relative to existing specifications for constants @{text

   767   "\<^vec>d\<^isub>\<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 "

   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') \\

   795     @'by' method method?

   796   "}

   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>   885 itself\<^esub>"}.   886 Although being devoid of any particular meaning, the term @{text   887 "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term   888 language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal   889 argument in primitive definitions, in order to circumvent hidden   890 polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c   891 TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of   892 a proposition @{text "A"} that depends on an additional type   893 argument, which is essentially a predicate on types.   894 *}   895   896 text %mlref {*   897 \begin{mldecls}   898 @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\   899 @{index_ML Conjunction.elim: "thm -> thm * thm"} \\   900 @{index_ML Drule.mk_term: "cterm -> thm"} \\   901 @{index_ML Drule.dest_term: "thm -> cterm"} \\   902 @{index_ML Logic.mk_type: "typ -> term"} \\   903 @{index_ML Logic.dest_type: "term -> typ"} \\   904 \end{mldecls}   905   906 \begin{description}   907   908 \item @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text   909 "A"} and @{text "B"}.   910   911 \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}   912 from @{text "A &&& B"}.   913   914 \item @{ML Drule.mk_term} derives @{text "TERM t"}.   915   916 \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text   917 "TERM t"}.   918   919 \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text   920 "TYPE(\<tau>)"}.   921   922 \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type   923 @{text "\<tau>"}.   924   925 \end{description}   926 *}   927   928   929 subsection {* Sort hypotheses *}   930   931 text {* Type variables are decorated with sorts, as explained in   932 \secref{sec:types}. This constrains type instantiation to certain   933 ranges of types: variable @{text "\<alpha>\<^sub>s"} may only be assigned to types   934 @{text "\<tau>"} that belong to sort @{text "s"}. Within the logic, sort   935 constraints act like implicit preconditions on the result @{text   936 "\<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   937 "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} cover the propositions @{text "\<Gamma>"}, @{text "\<phi>"}, as   938 well as the proof of @{text "\<Gamma> \<turnstile> \<phi>"}.   939   940 These \emph{sort hypothesis} of a theorem are passed monotonically   941 through further derivations. They are redundant, as long as the   942 statement of a theorem still contains the type variables that are   943 accounted here. The logical significance of sort hypotheses is   944 limited to the boundary case where type variables disappear from the   945 proposition, e.g.\ @{text "\<lparr>\<alpha>\<^sub>s : s\<rparr> \<turnstile> \<phi>"}. Since such dangling type   946 variables can be renamed arbitrarily without changing the   947 proposition @{text "\<phi>"}, the inference kernel maintains sort   948 hypotheses in anonymous form @{text "s \<turnstile> \<phi>"}.   949   950 In most practical situations, such extra sort hypotheses may be   951 stripped in a final bookkeeping step, e.g.\ at the end of a proof:   952 they are typically left over from intermediate reasoning with type   953 classes that can be satisfied by some concrete type @{text "\<tau>"} of   954 sort @{text "s"} to replace the hypothetical type variable @{text   955 "\<alpha>\<^sub>s"}. *}   956   957 text %mlref {*   958 \begin{mldecls}   959 @{index_ML Thm.extra_shyps: "thm -> sort list"} \\   960 @{index_ML Thm.strip_shyps: "thm -> thm"} \\   961 \end{mldecls}   962   963 \begin{description}   964   965 \item @{ML Thm.extra_shyps}~@{text "thm"} determines the extraneous   966 sort hypotheses of the given theorem, i.e.\ the sorts that are not   967 present within type variables of the statement.   968   969 \item @{ML Thm.strip_shyps}~@{text "thm"} removes any extraneous   970 sort hypotheses that can be witnessed from the type signature.   971   972 \end{description}   973 *}   974   975 text %mlex {* The following artificial example demonstrates the   976 derivation of @{prop False} with a pending sort hypothesis involving   977 a logically empty sort. *}   978   979 class empty =   980 assumes bad: "\<And>(x::'a) y. x \<noteq> y"   981   982 theorem (in empty) false: False   983 using bad by blast   984   985 ML {*   986 @{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])   987 *}   988   989 text {* Thanks to the inference kernel managing sort hypothesis   990 according to their logical significance, this example is merely an   991 instance of \emph{ex falso quodlibet consequitur} --- not a collapse   992 of the logical framework! *}   993   994   995 section {* Object-level rules \label{sec:obj-rules} *}   996   997 text {*   998 The primitive inferences covered so far mostly serve foundational   999 purposes. User-level reasoning usually works via object-level rules   1000 that are represented as theorems of Pure. Composition of rules   1001 involves \emph{backchaining}, \emph{higher-order unification} modulo   1002 @{text "\<alpha>\<beta>\<eta>"}-conversion of @{text "\<lambda>"}-terms, and so-called   1003 \emph{lifting} of rules into a context of @{text "\<And>"} and @{text   1004 "\<Longrightarrow>"} connectives. Thus the full power of higher-order Natural   1005 Deduction in Isabelle/Pure becomes readily available.   1006 *}   1007   1008   1009 subsection {* Hereditary Harrop Formulae *}   1010   1011 text {*   1012 The idea of object-level rules is to model Natural Deduction   1013 inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow   1014 arbitrary nesting similar to \cite{extensions91}. The most basic   1015 rule format is that of a \emph{Horn Clause}:   1016 \[   1017 \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}   1018$

  1019   where @{text "A, A\<^sub>1, \<dots>, A\<^sub>n"} are atomic propositions

  1020   of the framework, usually of the form @{text "Trueprop B"}, where

  1021   @{text "B"} is a (compound) object-level statement.  This

  1022   object-level inference corresponds to an iterated implication in

  1023   Pure like this:

  1024   $  1025 @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}   1026$

  1027   As an example consider conjunction introduction: @{text "A \<Longrightarrow> B \<Longrightarrow> A \<and>

  1028   B"}.  Any parameters occurring in such rule statements are

  1029   conceptionally treated as arbitrary:

  1030   $  1031 @{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"}   1032$

  1033

  1034   Nesting of rules means that the positions of @{text "A\<^sub>i"} may

  1035   again hold compound rules, not just atomic propositions.

  1036   Propositions of this format are called \emph{Hereditary Harrop

  1037   Formulae} in the literature \cite{Miller:1991}.  Here we give an

  1038   inductive characterization as follows:

  1039

  1040   \medskip

  1041   \begin{tabular}{ll}

  1042   @{text "\<^bold>x"} & set of variables \\

  1043   @{text "\<^bold>A"} & set of atomic propositions \\

  1044   @{text "\<^bold>H  =  \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\

  1045   \end{tabular}

  1046   \medskip

  1047

  1048   Thus we essentially impose nesting levels on propositions formed

  1049   from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a prefix

  1050   of parameters and compound premises, concluding an atomic

  1051   proposition.  Typical examples are @{text "\<longrightarrow>"}-introduction @{text

  1052   "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n

  1053   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}.  Even deeper nesting occurs in well-founded

  1054   induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this

  1055   already marks the limit of rule complexity that is usually seen in

  1056   practice.

  1057

  1058   \medskip Regular user-level inferences in Isabelle/Pure always

  1059   maintain the following canonical form of results:

  1060

  1061   \begin{itemize}

  1062

  1063   \item Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"},

  1064   which is a theorem of Pure, means that quantifiers are pushed in

  1065   front of implication at each level of nesting.  The normal form is a

  1066   Hereditary Harrop Formula.

  1067

  1068   \item The outermost prefix of parameters is represented via

  1069   schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x

  1070   \<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.

  1071   Note that this representation looses information about the order of

  1072   parameters, and vacuous quantifiers vanish automatically.

  1073

  1074   \end{itemize}

  1075 *}

  1076

  1077 text %mlref {*

  1078   \begin{mldecls}

  1079   @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\

  1080   \end{mldecls}

  1081

  1082   \begin{description}

  1083

  1084   \item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given

  1085   theorem according to the canonical form specified above.  This is

  1086   occasionally helpful to repair some low-level tools that do not

  1087   handle Hereditary Harrop Formulae properly.

  1088

  1089   \end{description}

  1090 *}

  1091

  1092

  1093 subsection {* Rule composition *}

  1094

  1095 text {*

  1096   The rule calculus of Isabelle/Pure provides two main inferences:

  1097   @{inference resolution} (i.e.\ back-chaining of rules) and

  1098   @{inference assumption} (i.e.\ closing a branch), both modulo

  1099   higher-order unification.  There are also combined variants, notably

  1100   @{inference elim_resolution} and @{inference dest_resolution}.

  1101

  1102   To understand the all-important @{inference resolution} principle,

  1103   we first consider raw @{inference_def composition} (modulo

  1104   higher-order unification with substitution @{text "\<vartheta>"}):

  1105   $  1106 \infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}   1107 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}   1108$

  1109   Here the conclusion of the first rule is unified with the premise of

  1110   the second; the resulting rule instance inherits the premises of the

  1111   first and conclusion of the second.  Note that @{text "C"} can again

  1112   consist of iterated implications.  We can also permute the premises

  1113   of the second rule back-and-forth in order to compose with @{text

  1114   "B'"} in any position (subsequently we shall always refer to

  1115   position 1 w.l.o.g.).

  1116

  1117   In @{inference composition} the internal structure of the common

  1118   part @{text "B"} and @{text "B'"} is not taken into account.  For

  1119   proper @{inference resolution} we require @{text "B"} to be atomic,

  1120   and explicitly observe the structure @{text "\<And>\<^vec>x. \<^vec>H

  1121   \<^vec>x \<Longrightarrow> B' \<^vec>x"} of the premise of the second rule.  The

  1122   idea is to adapt the first rule by lifting'' it into this context,

  1123   by means of iterated application of the following inferences:

  1124   $  1125 \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}   1126$

  1127   $  1128 \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"}}   1129$

  1130   By combining raw composition with lifting, we get full @{inference

  1131   resolution} as follows:

  1132   $  1133 \infer[(@{inference_def resolution})]   1134 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   1135 {\begin{tabular}{l}   1136 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\   1137 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   1138 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   1139 \end{tabular}}   1140$

  1141

  1142   Continued resolution of rules allows to back-chain a problem towards

  1143   more and sub-problems.  Branches are closed either by resolving with

  1144   a rule of 0 premises, or by producing a short-circuit'' within a

  1145   solved situation (again modulo unification):

  1146   $  1147 \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}   1148 {@{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})}}   1149$

  1150

  1151   FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}

  1152 *}

  1153

  1154 text %mlref {*

  1155   \begin{mldecls}

  1156   @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\

  1157   @{index_ML_op "RS": "thm * thm -> thm"} \\

  1158

  1159   @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\

  1160   @{index_ML_op "RL": "thm list * thm list -> thm list"} \\

  1161

  1162   @{index_ML_op "MRS": "thm list * thm -> thm"} \\

  1163   @{index_ML_op "OF": "thm * thm list -> thm"} \\

  1164   \end{mldecls}

  1165

  1166   \begin{description}

  1167

  1168   \item @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of

  1169   @{text "rule\<^sub>1"} with the @{text i}-th premise of @{text "rule\<^sub>2"},

  1170   according to the @{inference resolution} principle explained above.

  1171   Unless there is precisely one resolvent it raises exception @{ML

  1172   THM}.

  1173

  1174   This corresponds to the rule attribute @{attribute THEN} in Isar

  1175   source language.

  1176

  1177   \item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RS (1,

  1178   rule\<^sub>2)"}.

  1179

  1180   \item @{text "rules\<^sub>1 RLN (i, rules\<^sub>2)"} joins lists of rules.  For

  1181   every @{text "rule\<^sub>1"} in @{text "rules\<^sub>1"} and @{text "rule\<^sub>2"} in

  1182   @{text "rules\<^sub>2"}, it resolves the conclusion of @{text "rule\<^sub>1"} with

  1183   the @{text "i"}-th premise of @{text "rule\<^sub>2"}, accumulating multiple

  1184   results in one big list.  Note that such strict enumerations of

  1185   higher-order unifications can be inefficient compared to the lazy

  1186   variant seen in elementary tactics like @{ML resolve_tac}.

  1187

  1188   \item @{text "rules\<^sub>1 RL rules\<^sub>2"} abbreviates @{text "rules\<^sub>1 RLN (1,

  1189   rules\<^sub>2)"}.

  1190

  1191   \item @{text "[rule\<^sub>1, \<dots>, rule\<^sub>n] MRS rule"} resolves @{text "rule\<^isub>i"}

  1192   against premise @{text "i"} of @{text "rule"}, for @{text "i = n, \<dots>,

  1193   1"}.  By working from right to left, newly emerging premises are

  1194   concatenated in the result, without interfering.

  1195

  1196   \item @{text "rule OF rules"} is an alternative notation for @{text

  1197   "rules MRS rule"}, which makes rule composition look more like

  1198   function application.  Note that the argument @{text "rules"} need

  1199   not be atomic.

  1200

  1201   This corresponds to the rule attribute @{attribute OF} in Isar

  1202   source language.

  1203

  1204   \end{description}

  1205 *}

  1206

  1207

  1208 section {* Proof terms \label{sec:proof-terms} *}

  1209

  1210 text {* The Isabelle/Pure inference kernel can record the proof of

  1211   each theorem as a proof term that contains all logical inferences in

  1212   detail.  Rule composition by resolution (\secref{sec:obj-rules}) and

  1213   type-class reasoning is broken down to primitive rules of the

  1214   logical framework.  The proof term can be inspected by a separate

  1215   proof-checker, for example.

  1216

  1217   According to the well-known \emph{Curry-Howard isomorphism}, a proof

  1218   can be viewed as a @{text "\<lambda>"}-term. Following this idea, proofs in

  1219   Isabelle are internally represented by a datatype similar to the one

  1220   for terms described in \secref{sec:terms}.  On top of these

  1221   syntactic terms, two more layers of @{text "\<lambda>"}-calculus are added,

  1222   which correspond to @{text "\<And>x :: \<alpha>. B x"} and @{text "A \<Longrightarrow> B"}

  1223   according to the propositions-as-types principle.  The resulting

  1224   3-level @{text "\<lambda>"}-calculus resembles @{text "\<lambda>HOL"}'' in the

  1225   more abstract setting of Pure Type Systems (PTS)

  1226   \cite{Barendregt-Geuvers:2001}, if some fine points like schematic

  1227   polymorphism and type classes are ignored.

  1228

  1229   \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}

  1230   or @{text "\<^bold>\<lambda>p : A. prf"} correspond to introduction of @{text

  1231   "\<And>"}/@{text "\<Longrightarrow>"}, and \emph{proof applications} of the form @{text

  1232   "p \<cdot> t"} or @{text "p \<bullet> q"} correspond to elimination of @{text

  1233   "\<And>"}/@{text "\<Longrightarrow>"}.  Actual types @{text "\<alpha>"}, propositions @{text

  1234   "A"}, and terms @{text "t"} might be suppressed and reconstructed

  1235   from the overall proof term.

  1236

  1237   \medskip Various atomic proofs indicate special situations within

  1238   the proof construction as follows.

  1239

  1240   A \emph{bound proof variable} is a natural number @{text "b"} that

  1241   acts as de-Bruijn index for proof term abstractions.

  1242

  1243   A \emph{minimal proof} @{text "?"}'' is a dummy proof term.  This

  1244   indicates some unrecorded part of the proof.

  1245

  1246   @{text "Hyp A"} refers to some pending hypothesis by giving its

  1247   proposition.  This indicates an open context of implicit hypotheses,

  1248   similar to loose bound variables or free variables within a term

  1249   (\secref{sec:terms}).

  1250

  1251   An \emph{axiom} or \emph{oracle} @{text "a : A[\<^vec>\<tau>]"} refers

  1252   some postulated @{text "proof constant"}, which is subject to

  1253   schematic polymorphism of theory content, and the particular type

  1254   instantiation may be given explicitly.  The vector of types @{text

  1255   "\<^vec>\<tau>"} refers to the schematic type variables in the generic

  1256   proposition @{text "A"} in canonical order.

  1257

  1258   A \emph{proof promise} @{text "a : A[\<^vec>\<tau>]"} is a placeholder

  1259   for some proof of polymorphic proposition @{text "A"}, with explicit

  1260   type instantiation as given by the vector @{text "\<^vec>\<tau>"}, as

  1261   above.  Unlike axioms or oracles, proof promises may be

  1262   \emph{fulfilled} eventually, by substituting @{text "a"} by some

  1263   particular proof @{text "q"} at the corresponding type instance.

  1264   This acts like Hindley-Milner @{text "let"}-polymorphism: a generic

  1265   local proof definition may get used at different type instances, and

  1266   is replaced by the concrete instance eventually.

  1267

  1268   A \emph{named theorem} wraps up some concrete proof as a closed

  1269   formal entity, in the manner of constant definitions for proof

  1270   terms.  The \emph{proof body} of such boxed theorems involves some

  1271   digest about oracles and promises occurring in the original proof.

  1272   This allows the inference kernel to manage this critical information

  1273   without the full overhead of explicit proof terms.

  1274 *}

  1275

  1276 text %mlref {*

  1277   \begin{mldecls}

  1278   @{index_ML_type proof} \\

  1279   @{index_ML_type proof_body} \\

  1280   @{index_ML proofs: "int Unsynchronized.ref"} \\

  1281   \end{mldecls}

  1282

  1283   \begin{description}

  1284

  1285   \item Type @{ML_type proof} represents proof terms; this is a

  1286   datatype with constructors @{index_ML Abst}, @{index_ML AbsP},

  1287   @{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound},

  1288   @{index_ML MinProof}, @{index_ML Hyp}, @{index_ML PAxm}, @{index_ML

  1289   Oracle}, @{index_ML Promise}, @{index_ML PThm} as explained above.

  1290

  1291   \item Type @{ML_type proof_body} represents the nested proof

  1292   information of a named theorem, consisting of a digest of oracles

  1293   and named theorem over some proof term.  The digest only covers the

  1294   directly visible part of the proof: in order to get the full

  1295   information, the implicit graph of nested theorems needs to be

  1296   traversed (e.g.\ using @{ML Proofterm.fold_body_thms}).

  1297

  1298   \item @{ML Thm.proof_of}~@{text "thm"} and @{ML

  1299   Thm.proof_body_of}~@{text "thm"} produce the proof term or proof

  1300   body (with digest of oracles and theorems) from a given theorem.

  1301   Note that this involves a full join of internal futures that fulfill

  1302   pending proof promises, and thus disrupts the natural bottom-up

  1303   construction of proofs by introducing dynamic ad-hoc dependencies.

  1304   Parallel performance may suffer by inspecting proof terms at

  1305   run-time.

  1306

  1307   \item @{ML proofs} specifies the detail of proof recording within

  1308   @{ML_type thm} values produced by the inference kernel: @{ML 0}

  1309   records only the names of oracles, @{ML 1} records oracle names and

  1310   propositions, @{ML 2} additionally records full proof terms.

  1311   Officially named theorems that contribute to a result are recorded

  1312   in any case.

  1313

  1314   \end{description}

  1315 *}

  1316

  1317 end