src/Doc/Implementation/Logic.thy
author wenzelm
Wed Dec 06 15:46:35 2017 +0100 (18 months ago)
changeset 67146 909dcdec2122
parent 65446 ed18feb34c07
child 68540 000a0e062529
permissions -rw-r--r--
more embedded cartouche arguments;
more uniform LaTeX output for control symbols;
     1 (*:maxLineLen=78:*)
     2 
     3 theory Logic
     4 imports Base
     5 begin
     6 
     7 chapter \<open>Primitive logic \label{ch:logic}\<close>
     8 
     9 text \<open>
    10   The logical foundations of Isabelle/Isar are that of the Pure logic, which
    11   has been introduced as a Natural Deduction framework in @{cite paulson700}.
    12   This is essentially the same logic as ``\<open>\<lambda>HOL\<close>'' in the more abstract
    13   setting of Pure Type Systems (PTS) @{cite "Barendregt-Geuvers:2001"},
    14   although there are some key differences in the specific treatment of simple
    15   types in Isabelle/Pure.
    16 
    17   Following type-theoretic parlance, the Pure logic consists of three levels
    18   of \<open>\<lambda>\<close>-calculus with corresponding arrows, \<open>\<Rightarrow>\<close> for syntactic function space
    19   (terms depending on terms), \<open>\<And>\<close> for universal quantification (proofs
    20   depending on terms), and \<open>\<Longrightarrow>\<close> 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 schematic
    24   polymorphism, which is strictly speaking outside the logic.\<^footnote>\<open>This is the
    25   deeper logical reason, why the theory context \<open>\<Theta>\<close> is separate from the proof
    26   context \<open>\<Gamma>\<close> of the core calculus: type constructors, term constants, and
    27   facts (proof constants) may involve arbitrary type schemes, but the type of
    28   a locally fixed term parameter is also fixed!\<close>
    29 \<close>
    30 
    31 
    32 section \<open>Types \label{sec:types}\<close>
    33 
    34 text \<open>
    35   The language of types is an uninterpreted order-sorted first-order algebra;
    36   types are qualified by ordered type classes.
    37 
    38   \<^medskip>
    39   A \<^emph>\<open>type class\<close> is an abstract syntactic entity declared in the theory
    40   context. The \<^emph>\<open>subclass relation\<close> \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close> is specified by stating an
    41   acyclic generating relation; the transitive closure is maintained
    42   internally. The resulting relation is an ordering: reflexive, transitive,
    43   and antisymmetric.
    44 
    45   A \<^emph>\<open>sort\<close> is a list of type classes written as \<open>s = {c\<^sub>1, \<dots>, c\<^sub>m}\<close>, it
    46   represents symbolic intersection. Notationally, the curly braces are omitted
    47   for singleton intersections, i.e.\ any class \<open>c\<close> may be read as a sort
    48   \<open>{c}\<close>. The ordering on type classes is extended to sorts according to the
    49   meaning of intersections: \<open>{c\<^sub>1, \<dots> c\<^sub>m} \<subseteq> {d\<^sub>1, \<dots>, d\<^sub>n}\<close> iff \<open>\<forall>j. \<exists>i. c\<^sub>i \<subseteq>
    50   d\<^sub>j\<close>. The empty intersection \<open>{}\<close> refers to the universal sort, which is the
    51   largest element wrt.\ the sort order. Thus \<open>{}\<close> represents the ``full
    52   sort'', not the empty one! The intersection of all (finitely many) classes
    53   declared in the current theory is the least element wrt.\ the sort ordering.
    54 
    55   \<^medskip>
    56   A \<^emph>\<open>fixed type variable\<close> is a pair of a basic name (starting with a \<open>'\<close>
    57   character) and a sort constraint, e.g.\ \<open>('a, s)\<close> which is usually printed
    58   as \<open>\<alpha>\<^sub>s\<close>. A \<^emph>\<open>schematic type variable\<close> is a pair of an indexname and a sort
    59   constraint, e.g.\ \<open>(('a, 0), s)\<close> which is usually printed as \<open>?\<alpha>\<^sub>s\<close>.
    60 
    61   Note that \<^emph>\<open>all\<close> syntactic components contribute to the identity of type
    62   variables: basic name, index, and sort constraint. The core logic handles
    63   type variables with the same name but different sorts as different, although
    64   the type-inference layer (which is outside the core) rejects anything like
    65   that.
    66 
    67   A \<^emph>\<open>type constructor\<close> \<open>\<kappa>\<close> is a \<open>k\<close>-ary operator on types declared in the
    68   theory. Type constructor application is written postfix as \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>k)\<kappa>\<close>.
    69   For \<open>k = 0\<close> the argument tuple is omitted, e.g.\ \<open>prop\<close> instead of \<open>()prop\<close>.
    70   For \<open>k = 1\<close> the parentheses are omitted, e.g.\ \<open>\<alpha> list\<close> instead of
    71   \<open>(\<alpha>)list\<close>. Further notation is provided for specific constructors, notably
    72   the right-associative infix \<open>\<alpha> \<Rightarrow> \<beta>\<close> instead of \<open>(\<alpha>, \<beta>)fun\<close>.
    73 
    74   The logical category \<^emph>\<open>type\<close> is defined inductively over type variables and
    75   type constructors as follows: \<open>\<tau> = \<alpha>\<^sub>s | ?\<alpha>\<^sub>s | (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>\<close>.
    76 
    77   A \<^emph>\<open>type abbreviation\<close> is a syntactic definition \<open>(\<^vec>\<alpha>)\<kappa> = \<tau>\<close> of an
    78   arbitrary type expression \<open>\<tau>\<close> over variables \<open>\<^vec>\<alpha>\<close>. Type abbreviations
    79   appear as type constructors in the syntax, but are expanded before entering
    80   the logical core.
    81 
    82   A \<^emph>\<open>type arity\<close> declares the image behavior of a type constructor wrt.\ the
    83   algebra of sorts: \<open>\<kappa> :: (s\<^sub>1, \<dots>, s\<^sub>k)s\<close> means that \<open>(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>\<close> is of
    84   sort \<open>s\<close> if every argument type \<open>\<tau>\<^sub>i\<close> is of sort \<open>s\<^sub>i\<close>. Arity declarations
    85   are implicitly completed, i.e.\ \<open>\<kappa> :: (\<^vec>s)c\<close> entails \<open>\<kappa> ::
    86   (\<^vec>s)c'\<close> for any \<open>c' \<supseteq> c\<close>.
    87 
    88   \<^medskip>
    89   The sort algebra is always maintained as \<^emph>\<open>coregular\<close>, which means that type
    90   arities are consistent with the subclass relation: for any type constructor
    91   \<open>\<kappa>\<close>, and classes \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close>, and arities \<open>\<kappa> :: (\<^vec>s\<^sub>1)c\<^sub>1\<close> and \<open>\<kappa> ::
    92   (\<^vec>s\<^sub>2)c\<^sub>2\<close> holds \<open>\<^vec>s\<^sub>1 \<subseteq> \<^vec>s\<^sub>2\<close> component-wise.
    93 
    94   The key property of a coregular order-sorted algebra is that sort
    95   constraints can be solved in a most general fashion: for each type
    96   constructor \<open>\<kappa>\<close> and sort \<open>s\<close> there is a most general vector of argument
    97   sorts \<open>(s\<^sub>1, \<dots>, s\<^sub>k)\<close> such that a type scheme \<open>(\<alpha>\<^bsub>s\<^sub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^sub>k\<^esub>)\<kappa>\<close> is of
    98   sort \<open>s\<close>. Consequently, type unification has most general solutions (modulo
    99   equivalence of sorts), so type-inference produces primary types as expected
   100   @{cite "nipkow-prehofer"}.
   101 \<close>
   102 
   103 text %mlref \<open>
   104   \begin{mldecls}
   105   @{index_ML_type class: string} \\
   106   @{index_ML_type sort: "class list"} \\
   107   @{index_ML_type arity: "string * sort list * sort"} \\
   108   @{index_ML_type typ} \\
   109   @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\
   110   @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
   111   \end{mldecls}
   112   \begin{mldecls}
   113   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   114   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   115   @{index_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\
   116   @{index_ML Sign.add_type_abbrev: "Proof.context ->
   117   binding * string list * typ -> theory -> theory"} \\
   118   @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
   119   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
   120   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   121   \end{mldecls}
   122 
   123   \<^descr> Type @{ML_type class} represents type classes.
   124 
   125   \<^descr> Type @{ML_type sort} represents sorts, i.e.\ finite intersections of
   126   classes. The empty list @{ML "[]: sort"} refers to the empty class
   127   intersection, i.e.\ the ``full sort''.
   128 
   129   \<^descr> Type @{ML_type arity} represents type arities. A triple \<open>(\<kappa>, \<^vec>s, s)
   130   : arity\<close> represents \<open>\<kappa> :: (\<^vec>s)s\<close> as described above.
   131 
   132   \<^descr> Type @{ML_type typ} represents types; this is a datatype with constructors
   133   @{ML TFree}, @{ML TVar}, @{ML Type}.
   134 
   135   \<^descr> @{ML Term.map_atyps}~\<open>f \<tau>\<close> applies the mapping \<open>f\<close> to all atomic types
   136   (@{ML TFree}, @{ML TVar}) occurring in \<open>\<tau>\<close>.
   137 
   138   \<^descr> @{ML Term.fold_atyps}~\<open>f \<tau>\<close> iterates the operation \<open>f\<close> over all
   139   occurrences of atomic types (@{ML TFree}, @{ML TVar}) in \<open>\<tau>\<close>; the type
   140   structure is traversed from left to right.
   141 
   142   \<^descr> @{ML Sign.subsort}~\<open>thy (s\<^sub>1, s\<^sub>2)\<close> tests the subsort relation \<open>s\<^sub>1 \<subseteq>
   143   s\<^sub>2\<close>.
   144 
   145   \<^descr> @{ML Sign.of_sort}~\<open>thy (\<tau>, s)\<close> tests whether type \<open>\<tau>\<close> is of sort \<open>s\<close>.
   146 
   147   \<^descr> @{ML Sign.add_type}~\<open>ctxt (\<kappa>, k, mx)\<close> declares a new type constructors \<open>\<kappa>\<close>
   148   with \<open>k\<close> arguments and optional mixfix syntax.
   149 
   150   \<^descr> @{ML Sign.add_type_abbrev}~\<open>ctxt (\<kappa>, \<^vec>\<alpha>, \<tau>)\<close> defines a new type
   151   abbreviation \<open>(\<^vec>\<alpha>)\<kappa> = \<tau>\<close>.
   152 
   153   \<^descr> @{ML Sign.primitive_class}~\<open>(c, [c\<^sub>1, \<dots>, c\<^sub>n])\<close> declares a new class \<open>c\<close>,
   154   together with class relations \<open>c \<subseteq> c\<^sub>i\<close>, for \<open>i = 1, \<dots>, n\<close>.
   155 
   156   \<^descr> @{ML Sign.primitive_classrel}~\<open>(c\<^sub>1, c\<^sub>2)\<close> declares the class relation
   157   \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close>.
   158 
   159   \<^descr> @{ML Sign.primitive_arity}~\<open>(\<kappa>, \<^vec>s, s)\<close> declares the arity \<open>\<kappa> ::
   160   (\<^vec>s)s\<close>.
   161 \<close>
   162 
   163 text %mlantiq \<open>
   164   \begin{matharray}{rcl}
   165   @{ML_antiquotation_def "class"} & : & \<open>ML_antiquotation\<close> \\
   166   @{ML_antiquotation_def "sort"} & : & \<open>ML_antiquotation\<close> \\
   167   @{ML_antiquotation_def "type_name"} & : & \<open>ML_antiquotation\<close> \\
   168   @{ML_antiquotation_def "type_abbrev"} & : & \<open>ML_antiquotation\<close> \\
   169   @{ML_antiquotation_def "nonterminal"} & : & \<open>ML_antiquotation\<close> \\
   170   @{ML_antiquotation_def "typ"} & : & \<open>ML_antiquotation\<close> \\
   171   \end{matharray}
   172 
   173   @{rail \<open>
   174   @@{ML_antiquotation class} embedded
   175   ;
   176   @@{ML_antiquotation sort} sort
   177   ;
   178   (@@{ML_antiquotation type_name} |
   179    @@{ML_antiquotation type_abbrev} |
   180    @@{ML_antiquotation nonterminal}) embedded
   181   ;
   182   @@{ML_antiquotation typ} type
   183   \<close>}
   184 
   185   \<^descr> \<open>@{class c}\<close> inlines the internalized class \<open>c\<close> --- as @{ML_type string}
   186   literal.
   187 
   188   \<^descr> \<open>@{sort s}\<close> inlines the internalized sort \<open>s\<close> --- as @{ML_type "string
   189   list"} literal.
   190 
   191   \<^descr> \<open>@{type_name c}\<close> inlines the internalized type constructor \<open>c\<close> --- as
   192   @{ML_type string} literal.
   193 
   194   \<^descr> \<open>@{type_abbrev c}\<close> inlines the internalized type abbreviation \<open>c\<close> --- as
   195   @{ML_type string} literal.
   196 
   197   \<^descr> \<open>@{nonterminal c}\<close> inlines the internalized syntactic type~/ grammar
   198   nonterminal \<open>c\<close> --- as @{ML_type string} literal.
   199 
   200   \<^descr> \<open>@{typ \<tau>}\<close> inlines the internalized type \<open>\<tau>\<close> --- as constructor term for
   201   datatype @{ML_type typ}.
   202 \<close>
   203 
   204 
   205 section \<open>Terms \label{sec:terms}\<close>
   206 
   207 text \<open>
   208   The language of terms is that of simply-typed \<open>\<lambda>\<close>-calculus with de-Bruijn
   209   indices for bound variables (cf.\ @{cite debruijn72} or @{cite
   210   "paulson-ml2"}), with the types being determined by the corresponding
   211   binders. In contrast, free variables and constants have an explicit name and
   212   type in each occurrence.
   213 
   214   \<^medskip>
   215   A \<^emph>\<open>bound variable\<close> is a natural number \<open>b\<close>, which accounts for the number
   216   of intermediate binders between the variable occurrence in the body and its
   217   binding position. For example, the de-Bruijn term \<open>\<lambda>\<^bsub>bool\<^esub>. \<lambda>\<^bsub>bool\<^esub>. 1 \<and> 0\<close>
   218   would correspond to \<open>\<lambda>x\<^bsub>bool\<^esub>. \<lambda>y\<^bsub>bool\<^esub>. x \<and> y\<close> in a named representation.
   219   Note that a bound variable may be represented by different de-Bruijn indices
   220   at different occurrences, depending on the nesting of abstractions.
   221 
   222   A \<^emph>\<open>loose variable\<close> is a bound variable that is outside the scope of local
   223   binders. The types (and names) for loose variables can be managed as a
   224   separate context, that is maintained as a stack of hypothetical binders. The
   225   core logic operates on closed terms, without any loose variables.
   226 
   227   A \<^emph>\<open>fixed variable\<close> is a pair of a basic name and a type, e.g.\ \<open>(x, \<tau>)\<close>
   228   which is usually printed \<open>x\<^sub>\<tau>\<close> here. A \<^emph>\<open>schematic variable\<close> is a pair of an
   229   indexname and a type, e.g.\ \<open>((x, 0), \<tau>)\<close> which is likewise printed as
   230   \<open>?x\<^sub>\<tau>\<close>.
   231 
   232   \<^medskip>
   233   A \<^emph>\<open>constant\<close> is a pair of a basic name and a type, e.g.\ \<open>(c, \<tau>)\<close> which is
   234   usually printed as \<open>c\<^sub>\<tau>\<close> here. Constants are declared in the context as
   235   polymorphic families \<open>c :: \<sigma>\<close>, meaning that all substitution instances \<open>c\<^sub>\<tau>\<close>
   236   for \<open>\<tau> = \<sigma>\<vartheta>\<close> are valid.
   237 
   238   The vector of \<^emph>\<open>type arguments\<close> of constant \<open>c\<^sub>\<tau>\<close> wrt.\ the declaration \<open>c
   239   :: \<sigma>\<close> is defined as the codomain of the matcher \<open>\<vartheta> = {?\<alpha>\<^sub>1 \<mapsto> \<tau>\<^sub>1,
   240   \<dots>, ?\<alpha>\<^sub>n \<mapsto> \<tau>\<^sub>n}\<close> presented in canonical order \<open>(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n)\<close>, corresponding
   241   to the left-to-right occurrences of the \<open>\<alpha>\<^sub>i\<close> in \<open>\<sigma>\<close>. Within a given theory
   242   context, there is a one-to-one correspondence between any constant \<open>c\<^sub>\<tau>\<close> and
   243   the application \<open>c(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n)\<close> of its type arguments. For example, with
   244   \<open>plus :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>\<close>, the instance \<open>plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>\<close> corresponds to
   245   \<open>plus(nat)\<close>.
   246 
   247   Constant declarations \<open>c :: \<sigma>\<close> may contain sort constraints for type
   248   variables in \<open>\<sigma>\<close>. These are observed by type-inference as expected, but
   249   \<^emph>\<open>ignored\<close> by the core logic. This means the primitive logic is able to
   250   reason with instances of polymorphic constants that the user-level
   251   type-checker would reject due to violation of type class restrictions.
   252 
   253   \<^medskip>
   254   An \<^emph>\<open>atomic term\<close> is either a variable or constant. The logical category
   255   \<^emph>\<open>term\<close> is defined inductively over atomic terms, with abstraction and
   256   application as follows: \<open>t = b | x\<^sub>\<tau> | ?x\<^sub>\<tau> | c\<^sub>\<tau> | \<lambda>\<^sub>\<tau>. t | t\<^sub>1 t\<^sub>2\<close>.
   257   Parsing and printing takes care of converting between an external
   258   representation with named bound variables. Subsequently, we shall use the
   259   latter notation instead of internal de-Bruijn representation.
   260 
   261   The inductive relation \<open>t :: \<tau>\<close> assigns a (unique) type to a term according
   262   to the structure of atomic terms, abstractions, and applications:
   263   \[
   264   \infer{\<open>a\<^sub>\<tau> :: \<tau>\<close>}{}
   265   \qquad
   266   \infer{\<open>(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>\<close>}{\<open>t :: \<sigma>\<close>}
   267   \qquad
   268   \infer{\<open>t u :: \<sigma>\<close>}{\<open>t :: \<tau> \<Rightarrow> \<sigma>\<close> & \<open>u :: \<tau>\<close>}
   269   \]
   270   A \<^emph>\<open>well-typed term\<close> is a term that can be typed according to these rules.
   271 
   272   Typing information can be omitted: type-inference is able to reconstruct the
   273   most general type of a raw term, while assigning most general types to all
   274   of its variables and constants. Type-inference depends on a context of type
   275   constraints for fixed variables, and declarations for polymorphic constants.
   276 
   277   The identity of atomic terms consists both of the name and the type
   278   component. This means that different variables \<open>x\<^bsub>\<tau>\<^sub>1\<^esub>\<close> and \<open>x\<^bsub>\<tau>\<^sub>2\<^esub>\<close> may
   279   become the same after type instantiation. Type-inference rejects variables
   280   of the same name, but different types. In contrast, mixed instances of
   281   polymorphic constants occur routinely.
   282 
   283   \<^medskip>
   284   The \<^emph>\<open>hidden polymorphism\<close> of a term \<open>t :: \<sigma>\<close> is the set of type variables
   285   occurring in \<open>t\<close>, but not in its type \<open>\<sigma>\<close>. This means that the term
   286   implicitly depends on type arguments that are not accounted in the result
   287   type, i.e.\ there are different type instances \<open>t\<vartheta> :: \<sigma>\<close> and
   288   \<open>t\<vartheta>' :: \<sigma>\<close> with the same type. This slightly pathological
   289   situation notoriously demands additional care.
   290 
   291   \<^medskip>
   292   A \<^emph>\<open>term abbreviation\<close> is a syntactic definition \<open>c\<^sub>\<sigma> \<equiv> t\<close> of a closed term
   293   \<open>t\<close> of type \<open>\<sigma>\<close>, without any hidden polymorphism. A term abbreviation looks
   294   like a constant in the syntax, but is expanded before entering the logical
   295   core. Abbreviations are usually reverted when printing terms, using \<open>t \<rightarrow>
   296   c\<^sub>\<sigma>\<close> as rules for higher-order rewriting.
   297 
   298   \<^medskip>
   299   Canonical operations on \<open>\<lambda>\<close>-terms include \<open>\<alpha>\<beta>\<eta>\<close>-conversion: \<open>\<alpha>\<close>-conversion
   300   refers to capture-free renaming of bound variables; \<open>\<beta>\<close>-conversion contracts
   301   an abstraction applied to an argument term, substituting the argument in the
   302   body: \<open>(\<lambda>x. b)a\<close> becomes \<open>b[a/x]\<close>; \<open>\<eta>\<close>-conversion contracts vacuous
   303   application-abstraction: \<open>\<lambda>x. f x\<close> becomes \<open>f\<close>, provided that the bound
   304   variable does not occur in \<open>f\<close>.
   305 
   306   Terms are normally treated modulo \<open>\<alpha>\<close>-conversion, which is implicit in the
   307   de-Bruijn representation. Names for bound variables in abstractions are
   308   maintained separately as (meaningless) comments, mostly for parsing and
   309   printing. Full \<open>\<alpha>\<beta>\<eta>\<close>-conversion is commonplace in various standard
   310   operations (\secref{sec:obj-rules}) that are based on higher-order
   311   unification and matching.
   312 \<close>
   313 
   314 text %mlref \<open>
   315   \begin{mldecls}
   316   @{index_ML_type term} \\
   317   @{index_ML_op "aconv": "term * term -> bool"} \\
   318   @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
   319   @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   320   @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
   321   @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   322   \end{mldecls}
   323   \begin{mldecls}
   324   @{index_ML fastype_of: "term -> typ"} \\
   325   @{index_ML lambda: "term -> term -> term"} \\
   326   @{index_ML betapply: "term * term -> term"} \\
   327   @{index_ML incr_boundvars: "int -> term -> term"} \\
   328   @{index_ML Sign.declare_const: "Proof.context ->
   329   (binding * typ) * mixfix -> theory -> term * theory"} \\
   330   @{index_ML Sign.add_abbrev: "string -> binding * term ->
   331   theory -> (term * term) * theory"} \\
   332   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   333   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   334   \end{mldecls}
   335 
   336   \<^descr> Type @{ML_type term} represents de-Bruijn terms, with comments in
   337   abstractions, and explicitly named free variables and constants; this is a
   338   datatype with constructors @{index_ML Bound}, @{index_ML Free}, @{index_ML
   339   Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_op "$"}.
   340 
   341   \<^descr> \<open>t\<close>~@{ML_text aconv}~\<open>u\<close> checks \<open>\<alpha>\<close>-equivalence of two terms. This is the
   342   basic equality relation on type @{ML_type term}; raw datatype equality
   343   should only be used for operations related to parsing or printing!
   344 
   345   \<^descr> @{ML Term.map_types}~\<open>f t\<close> applies the mapping \<open>f\<close> to all types occurring
   346   in \<open>t\<close>.
   347 
   348   \<^descr> @{ML Term.fold_types}~\<open>f t\<close> iterates the operation \<open>f\<close> over all
   349   occurrences of types in \<open>t\<close>; the term structure is traversed from left to
   350   right.
   351 
   352   \<^descr> @{ML Term.map_aterms}~\<open>f t\<close> applies the mapping \<open>f\<close> to all atomic terms
   353   (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}) occurring in \<open>t\<close>.
   354 
   355   \<^descr> @{ML Term.fold_aterms}~\<open>f t\<close> iterates the operation \<open>f\<close> over all
   356   occurrences of atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
   357   Const}) in \<open>t\<close>; the term structure is traversed from left to right.
   358 
   359   \<^descr> @{ML fastype_of}~\<open>t\<close> determines the type of a well-typed term. This
   360   operation is relatively slow, despite the omission of any sanity checks.
   361 
   362   \<^descr> @{ML lambda}~\<open>a b\<close> produces an abstraction \<open>\<lambda>a. b\<close>, where occurrences of
   363   the atomic term \<open>a\<close> in the body \<open>b\<close> are replaced by bound variables.
   364 
   365   \<^descr> @{ML betapply}~\<open>(t, u)\<close> produces an application \<open>t u\<close>, with topmost
   366   \<open>\<beta>\<close>-conversion if \<open>t\<close> is an abstraction.
   367 
   368   \<^descr> @{ML incr_boundvars}~\<open>j\<close> increments a term's dangling bound variables by
   369   the offset \<open>j\<close>. This is required when moving a subterm into a context where
   370   it is enclosed by a different number of abstractions. Bound variables with a
   371   matching abstraction are unaffected.
   372 
   373   \<^descr> @{ML Sign.declare_const}~\<open>ctxt ((c, \<sigma>), mx)\<close> declares a new constant \<open>c ::
   374   \<sigma>\<close> with optional mixfix syntax.
   375 
   376   \<^descr> @{ML Sign.add_abbrev}~\<open>print_mode (c, t)\<close> introduces a new term
   377   abbreviation \<open>c \<equiv> t\<close>.
   378 
   379   \<^descr> @{ML Sign.const_typargs}~\<open>thy (c, \<tau>)\<close> and @{ML Sign.const_instance}~\<open>thy
   380   (c, [\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n])\<close> convert between two representations of polymorphic
   381   constants: full type instance vs.\ compact type arguments form.
   382 \<close>
   383 
   384 text %mlantiq \<open>
   385   \begin{matharray}{rcl}
   386   @{ML_antiquotation_def "const_name"} & : & \<open>ML_antiquotation\<close> \\
   387   @{ML_antiquotation_def "const_abbrev"} & : & \<open>ML_antiquotation\<close> \\
   388   @{ML_antiquotation_def "const"} & : & \<open>ML_antiquotation\<close> \\
   389   @{ML_antiquotation_def "term"} & : & \<open>ML_antiquotation\<close> \\
   390   @{ML_antiquotation_def "prop"} & : & \<open>ML_antiquotation\<close> \\
   391   \end{matharray}
   392 
   393   @{rail \<open>
   394   (@@{ML_antiquotation const_name} |
   395    @@{ML_antiquotation const_abbrev}) embedded
   396   ;
   397   @@{ML_antiquotation const} ('(' (type + ',') ')')?
   398   ;
   399   @@{ML_antiquotation term} term
   400   ;
   401   @@{ML_antiquotation prop} prop
   402   \<close>}
   403 
   404   \<^descr> \<open>@{const_name c}\<close> inlines the internalized logical constant name \<open>c\<close> ---
   405   as @{ML_type string} literal.
   406 
   407   \<^descr> \<open>@{const_abbrev c}\<close> inlines the internalized abbreviated constant name \<open>c\<close>
   408   --- as @{ML_type string} literal.
   409 
   410   \<^descr> \<open>@{const c(\<^vec>\<tau>)}\<close> inlines the internalized constant \<open>c\<close> with precise
   411   type instantiation in the sense of @{ML Sign.const_instance} --- as @{ML
   412   Const} constructor term for datatype @{ML_type term}.
   413 
   414   \<^descr> \<open>@{term t}\<close> inlines the internalized term \<open>t\<close> --- as constructor term for
   415   datatype @{ML_type term}.
   416 
   417   \<^descr> \<open>@{prop \<phi>}\<close> inlines the internalized proposition \<open>\<phi>\<close> --- as constructor
   418   term for datatype @{ML_type term}.
   419 \<close>
   420 
   421 
   422 section \<open>Theorems \label{sec:thms}\<close>
   423 
   424 text \<open>
   425   A \<^emph>\<open>proposition\<close> is a well-typed term of type \<open>prop\<close>, a \<^emph>\<open>theorem\<close> is a
   426   proven proposition (depending on a context of hypotheses and the background
   427   theory). Primitive inferences include plain Natural Deduction rules for the
   428   primary connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> of the framework. There is also a builtin
   429   notion of equality/equivalence \<open>\<equiv>\<close>.
   430 \<close>
   431 
   432 
   433 subsection \<open>Primitive connectives and rules \label{sec:prim-rules}\<close>
   434 
   435 text \<open>
   436   The theory \<open>Pure\<close> contains constant declarations for the primitive
   437   connectives \<open>\<And>\<close>, \<open>\<Longrightarrow>\<close>, and \<open>\<equiv>\<close> of the logical framework, see
   438   \figref{fig:pure-connectives}. The derivability judgment \<open>A\<^sub>1, \<dots>, A\<^sub>n \<turnstile> B\<close>
   439   is defined inductively by the primitive inferences given in
   440   \figref{fig:prim-rules}, with the global restriction that the hypotheses
   441   must \<^emph>\<open>not\<close> contain any schematic variables. The builtin equality is
   442   conceptually axiomatized as shown in \figref{fig:pure-equality}, although
   443   the implementation works directly with derived inferences.
   444 
   445   \begin{figure}[htb]
   446   \begin{center}
   447   \begin{tabular}{ll}
   448   \<open>all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop\<close> & universal quantification (binder \<open>\<And>\<close>) \\
   449   \<open>\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop\<close> & implication (right associative infix) \\
   450   \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> & equality relation (infix) \\
   451   \end{tabular}
   452   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
   453   \end{center}
   454   \end{figure}
   455 
   456   \begin{figure}[htb]
   457   \begin{center}
   458   \[
   459   \infer[\<open>(axiom)\<close>]{\<open>\<turnstile> A\<close>}{\<open>A \<in> \<Theta>\<close>}
   460   \qquad
   461   \infer[\<open>(assume)\<close>]{\<open>A \<turnstile> A\<close>}{}
   462   \]
   463   \[
   464   \infer[\<open>(\<And>\<hyphen>intro)\<close>]{\<open>\<Gamma> \<turnstile> \<And>x. B[x]\<close>}{\<open>\<Gamma> \<turnstile> B[x]\<close> & \<open>x \<notin> \<Gamma>\<close>}
   465   \qquad
   466   \infer[\<open>(\<And>\<hyphen>elim)\<close>]{\<open>\<Gamma> \<turnstile> B[a]\<close>}{\<open>\<Gamma> \<turnstile> \<And>x. B[x]\<close>}
   467   \]
   468   \[
   469   \infer[\<open>(\<Longrightarrow>\<hyphen>intro)\<close>]{\<open>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>}
   470   \qquad
   471   \infer[\<open>(\<Longrightarrow>\<hyphen>elim)\<close>]{\<open>\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B\<close>}{\<open>\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B\<close> & \<open>\<Gamma>\<^sub>2 \<turnstile> A\<close>}
   472   \]
   473   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
   474   \end{center}
   475   \end{figure}
   476 
   477   \begin{figure}[htb]
   478   \begin{center}
   479   \begin{tabular}{ll}
   480   \<open>\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]\<close> & \<open>\<beta>\<close>-conversion \\
   481   \<open>\<turnstile> x \<equiv> x\<close> & reflexivity \\
   482   \<open>\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y\<close> & substitution \\
   483   \<open>\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g\<close> & extensionality \\
   484   \<open>\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B\<close> & logical equivalence \\
   485   \end{tabular}
   486   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
   487   \end{center}
   488   \end{figure}
   489 
   490   The introduction and elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> are analogous to
   491   formation of dependently typed \<open>\<lambda>\<close>-terms representing the underlying proof
   492   objects. Proof terms are irrelevant in the Pure logic, though; they cannot
   493   occur within propositions. The system provides a runtime option to record
   494   explicit proof terms for primitive inferences, see also
   495   \secref{sec:proof-terms}. Thus all three levels of \<open>\<lambda>\<close>-calculus become
   496   explicit: \<open>\<Rightarrow>\<close> for terms, and \<open>\<And>/\<Longrightarrow>\<close> for proofs (cf.\ @{cite
   497   "Berghofer-Nipkow:2000:TPHOL"}).
   498 
   499   Observe that locally fixed parameters (as in \<open>\<And>\<hyphen>intro\<close>) need not be recorded
   500   in the hypotheses, because the simple syntactic types of Pure are always
   501   inhabitable. ``Assumptions'' \<open>x :: \<tau>\<close> for type-membership are only present
   502   as long as some \<open>x\<^sub>\<tau>\<close> occurs in the statement body.\<^footnote>\<open>This is the key
   503   difference to ``\<open>\<lambda>HOL\<close>'' in the PTS framework @{cite
   504   "Barendregt-Geuvers:2001"}, where hypotheses \<open>x : A\<close> are treated uniformly
   505   for propositions and types.\<close>
   506 
   507   \<^medskip>
   508   The axiomatization of a theory is implicitly closed by forming all instances
   509   of type and term variables: \<open>\<turnstile> A\<vartheta>\<close> holds for any substitution
   510   instance of an axiom \<open>\<turnstile> A\<close>. By pushing substitutions through derivations
   511   inductively, we also get admissible \<open>generalize\<close> and \<open>instantiate\<close> rules as
   512   shown in \figref{fig:subst-rules}.
   513 
   514   \begin{figure}[htb]
   515   \begin{center}
   516   \[
   517   \infer{\<open>\<Gamma> \<turnstile> B[?\<alpha>]\<close>}{\<open>\<Gamma> \<turnstile> B[\<alpha>]\<close> & \<open>\<alpha> \<notin> \<Gamma>\<close>}
   518   \quad
   519   \infer[\quad\<open>(generalize)\<close>]{\<open>\<Gamma> \<turnstile> B[?x]\<close>}{\<open>\<Gamma> \<turnstile> B[x]\<close> & \<open>x \<notin> \<Gamma>\<close>}
   520   \]
   521   \[
   522   \infer{\<open>\<Gamma> \<turnstile> B[\<tau>]\<close>}{\<open>\<Gamma> \<turnstile> B[?\<alpha>]\<close>}
   523   \quad
   524   \infer[\quad\<open>(instantiate)\<close>]{\<open>\<Gamma> \<turnstile> B[t]\<close>}{\<open>\<Gamma> \<turnstile> B[?x]\<close>}
   525   \]
   526   \caption{Admissible substitution rules}\label{fig:subst-rules}
   527   \end{center}
   528   \end{figure}
   529 
   530   Note that \<open>instantiate\<close> does not require an explicit side-condition, because
   531   \<open>\<Gamma>\<close> may never contain schematic variables.
   532 
   533   In principle, variables could be substituted in hypotheses as well, but this
   534   would disrupt the monotonicity of reasoning: deriving \<open>\<Gamma>\<vartheta> \<turnstile>
   535   B\<vartheta>\<close> from \<open>\<Gamma> \<turnstile> B\<close> is correct, but \<open>\<Gamma>\<vartheta> \<supseteq> \<Gamma>\<close> does not
   536   necessarily hold: the result belongs to a different proof context.
   537 
   538   \<^medskip>
   539   An \<^emph>\<open>oracle\<close> is a function that produces axioms on the fly. Logically, this
   540   is an instance of the \<open>axiom\<close> rule (\figref{fig:prim-rules}), but there is
   541   an operational difference. The system always records oracle invocations
   542   within derivations of theorems by a unique tag.
   543 
   544   Axiomatizations should be limited to the bare minimum, typically as part of
   545   the initial logical basis of an object-logic formalization. Later on,
   546   theories are usually developed in a strictly definitional fashion, by
   547   stating only certain equalities over new constants.
   548 
   549   A \<^emph>\<open>simple definition\<close> consists of a constant declaration \<open>c :: \<sigma>\<close> together
   550   with an axiom \<open>\<turnstile> c \<equiv> t\<close>, where \<open>t :: \<sigma>\<close> is a closed term without any hidden
   551   polymorphism. The RHS may depend on further defined constants, but not \<open>c\<close>
   552   itself. Definitions of functions may be presented as \<open>c \<^vec>x \<equiv> t\<close>
   553   instead of the puristic \<open>c \<equiv> \<lambda>\<^vec>x. t\<close>.
   554 
   555   An \<^emph>\<open>overloaded definition\<close> consists of a collection of axioms for the same
   556   constant, with zero or one equations \<open>c((\<^vec>\<alpha>)\<kappa>) \<equiv> t\<close> for each type
   557   constructor \<open>\<kappa>\<close> (for distinct variables \<open>\<^vec>\<alpha>\<close>). The RHS may mention
   558   previously defined constants as above, or arbitrary constants \<open>d(\<alpha>\<^sub>i)\<close> for
   559   some \<open>\<alpha>\<^sub>i\<close> projected from \<open>\<^vec>\<alpha>\<close>. Thus overloaded definitions
   560   essentially work by primitive recursion over the syntactic structure of a
   561   single type argument. See also @{cite \<open>\S4.3\<close>
   562   "Haftmann-Wenzel:2006:classes"}.
   563 \<close>
   564 
   565 text %mlref \<open>
   566   \begin{mldecls}
   567   @{index_ML Logic.all: "term -> term -> term"} \\
   568   @{index_ML Logic.mk_implies: "term * term -> term"} \\
   569   \end{mldecls}
   570   \begin{mldecls}
   571   @{index_ML_type ctyp} \\
   572   @{index_ML_type cterm} \\
   573   @{index_ML Thm.ctyp_of: "Proof.context -> typ -> ctyp"} \\
   574   @{index_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\
   575   @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\
   576   @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
   577   @{index_ML Thm.all: "Proof.context -> cterm -> cterm -> cterm"} \\
   578   @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
   579   \end{mldecls}
   580   \begin{mldecls}
   581   @{index_ML_type thm} \\
   582   @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
   583   @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
   584   @{index_ML Thm.assume: "cterm -> thm"} \\
   585   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   586   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
   587   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   588   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
   589   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   590   @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   591   -> thm -> thm"} \\
   592   @{index_ML Thm.add_axiom: "Proof.context ->
   593   binding * term -> theory -> (string * thm) * theory"} \\
   594   @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
   595   (string * ('a -> thm)) * theory"} \\
   596   @{index_ML Thm.add_def: "Defs.context -> bool -> bool ->
   597   binding * term -> theory -> (string * thm) * theory"} \\
   598   \end{mldecls}
   599   \begin{mldecls}
   600   @{index_ML Theory.add_deps: "Defs.context -> string ->
   601   Defs.entry -> Defs.entry list -> theory -> theory"} \\
   602   \end{mldecls}
   603 
   604   \<^descr> @{ML Thm.peek_status}~\<open>thm\<close> informs about the current status of the
   605   derivation object behind the given theorem. This is a snapshot of a
   606   potentially ongoing (parallel) evaluation of proofs. The three Boolean
   607   values indicate the following: \<^verbatim>\<open>oracle\<close> if the finished part contains some
   608   oracle invocation; \<^verbatim>\<open>unfinished\<close> if some future proofs are still pending;
   609   \<^verbatim>\<open>failed\<close> if some future proof has failed, rendering the theorem invalid!
   610 
   611   \<^descr> @{ML Logic.all}~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where
   612   occurrences of the atomic term \<open>a\<close> in the body proposition \<open>B\<close> are replaced
   613   by bound variables. (See also @{ML lambda} on terms.)
   614 
   615   \<^descr> @{ML Logic.mk_implies}~\<open>(A, B)\<close> produces a Pure implication \<open>A \<Longrightarrow> B\<close>.
   616 
   617   \<^descr> Types @{ML_type ctyp} and @{ML_type cterm} represent certified types and
   618   terms, respectively. These are abstract datatypes that guarantee that its
   619   values have passed the full well-formedness (and well-typedness) checks,
   620   relative to the declarations of type constructors, constants etc.\ in the
   621   background theory. The abstract types @{ML_type ctyp} and @{ML_type cterm}
   622   are part of the same inference kernel that is mainly responsible for
   623   @{ML_type thm}. Thus syntactic operations on @{ML_type ctyp} and @{ML_type
   624   cterm} are located in the @{ML_structure Thm} module, even though theorems
   625   are not yet involved at that stage.
   626 
   627   \<^descr> @{ML Thm.ctyp_of}~\<open>ctxt \<tau>\<close> and @{ML Thm.cterm_of}~\<open>ctxt t\<close> explicitly
   628   check types and terms, respectively. This also involves some basic
   629   normalizations, such expansion of type and term abbreviations from the
   630   underlying theory context. Full re-certification is relatively slow and
   631   should be avoided in tight reasoning loops.
   632 
   633   \<^descr> @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML Drule.mk_implies}
   634   etc.\ compose certified terms (or propositions) incrementally. This is
   635   equivalent to @{ML Thm.cterm_of} after unchecked @{ML_op "$"}, @{ML lambda},
   636   @{ML Logic.all}, @{ML Logic.mk_implies} etc., but there can be a big
   637   difference in performance when large existing entities are composed by a few
   638   extra constructions on top. There are separate operations to decompose
   639   certified terms and theorems to produce certified terms again.
   640 
   641   \<^descr> Type @{ML_type thm} represents proven propositions. This is an abstract
   642   datatype that guarantees that its values have been constructed by basic
   643   principles of the @{ML_structure Thm} module. Every @{ML_type thm} value
   644   refers its background theory, cf.\ \secref{sec:context-theory}.
   645 
   646   \<^descr> @{ML Thm.transfer}~\<open>thy thm\<close> transfers the given theorem to a \<^emph>\<open>larger\<close>
   647   theory, see also \secref{sec:context}. This formal adjustment of the
   648   background context has no logical significance, but is occasionally required
   649   for formal reasons, e.g.\ when theorems that are imported from more basic
   650   theories are used in the current situation.
   651 
   652   \<^descr> @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML Thm.forall_elim}, @{ML
   653   Thm.implies_intr}, and @{ML Thm.implies_elim} correspond to the primitive
   654   inferences of \figref{fig:prim-rules}.
   655 
   656   \<^descr> @{ML Thm.generalize}~\<open>(\<^vec>\<alpha>, \<^vec>x)\<close> corresponds to the
   657   \<open>generalize\<close> rules of \figref{fig:subst-rules}. Here collections of type and
   658   term variables are generalized simultaneously, specified by the given basic
   659   names.
   660 
   661   \<^descr> @{ML Thm.instantiate}~\<open>(\<^vec>\<alpha>\<^sub>s, \<^vec>x\<^sub>\<tau>)\<close> corresponds to the
   662   \<open>instantiate\<close> rules of \figref{fig:subst-rules}. Type variables are
   663   substituted before term variables. Note that the types in \<open>\<^vec>x\<^sub>\<tau>\<close> refer
   664   to the instantiated versions.
   665 
   666   \<^descr> @{ML Thm.add_axiom}~\<open>ctxt (name, A)\<close> declares an arbitrary proposition as
   667   axiom, and retrieves it as a theorem from the resulting theory, cf.\ \<open>axiom\<close>
   668   in \figref{fig:prim-rules}. Note that the low-level representation in the
   669   axiom table may differ slightly from the returned theorem.
   670 
   671   \<^descr> @{ML Thm.add_oracle}~\<open>(binding, oracle)\<close> produces a named oracle rule,
   672   essentially generating arbitrary axioms on the fly, cf.\ \<open>axiom\<close> in
   673   \figref{fig:prim-rules}.
   674 
   675   \<^descr> @{ML Thm.add_def}~\<open>ctxt unchecked overloaded (name, c \<^vec>x \<equiv> t)\<close>
   676   states a definitional axiom for an existing constant \<open>c\<close>. Dependencies are
   677   recorded via @{ML Theory.add_deps}, unless the \<open>unchecked\<close> option is set.
   678   Note that the low-level representation in the axiom table may differ
   679   slightly from the returned theorem.
   680 
   681   \<^descr> @{ML Theory.add_deps}~\<open>ctxt name c\<^sub>\<tau> \<^vec>d\<^sub>\<sigma>\<close> declares dependencies of
   682   a named specification for constant \<open>c\<^sub>\<tau>\<close>, relative to existing
   683   specifications for constants \<open>\<^vec>d\<^sub>\<sigma>\<close>. This also works for type
   684   constructors.
   685 \<close>
   686 
   687 text %mlantiq \<open>
   688   \begin{matharray}{rcl}
   689   @{ML_antiquotation_def "ctyp"} & : & \<open>ML_antiquotation\<close> \\
   690   @{ML_antiquotation_def "cterm"} & : & \<open>ML_antiquotation\<close> \\
   691   @{ML_antiquotation_def "cprop"} & : & \<open>ML_antiquotation\<close> \\
   692   @{ML_antiquotation_def "thm"} & : & \<open>ML_antiquotation\<close> \\
   693   @{ML_antiquotation_def "thms"} & : & \<open>ML_antiquotation\<close> \\
   694   @{ML_antiquotation_def "lemma"} & : & \<open>ML_antiquotation\<close> \\
   695   \end{matharray}
   696 
   697   @{rail \<open>
   698   @@{ML_antiquotation ctyp} typ
   699   ;
   700   @@{ML_antiquotation cterm} term
   701   ;
   702   @@{ML_antiquotation cprop} prop
   703   ;
   704   @@{ML_antiquotation thm} thm
   705   ;
   706   @@{ML_antiquotation thms} thms
   707   ;
   708   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
   709     @'by' method method?
   710   \<close>}
   711 
   712   \<^descr> \<open>@{ctyp \<tau>}\<close> produces a certified type wrt.\ the current background theory
   713   --- as abstract value of type @{ML_type ctyp}.
   714 
   715   \<^descr> \<open>@{cterm t}\<close> and \<open>@{cprop \<phi>}\<close> produce a certified term wrt.\ the current
   716   background theory --- as abstract value of type @{ML_type cterm}.
   717 
   718   \<^descr> \<open>@{thm a}\<close> produces a singleton fact --- as abstract value of type
   719   @{ML_type thm}.
   720 
   721   \<^descr> \<open>@{thms a}\<close> produces a general fact --- as abstract value of type
   722   @{ML_type "thm list"}.
   723 
   724   \<^descr> \<open>@{lemma \<phi> by meth}\<close> produces a fact that is proven on the spot according
   725   to the minimal proof, which imitates a terminal Isar proof. The result is an
   726   abstract value of type @{ML_type thm} or @{ML_type "thm list"}, depending on
   727   the number of propositions given here.
   728 
   729   The internal derivation object lacks a proper theorem name, but it is
   730   formally closed, unless the \<open>(open)\<close> option is specified (this may impact
   731   performance of applications with proof terms).
   732 
   733   Since ML antiquotations are always evaluated at compile-time, there is no
   734   run-time overhead even for non-trivial proofs. Nonetheless, the
   735   justification is syntactically limited to a single @{command "by"} step.
   736   More complex Isar proofs should be done in regular theory source, before
   737   compiling the corresponding ML text that uses the result.
   738 \<close>
   739 
   740 
   741 subsection \<open>Auxiliary connectives \label{sec:logic-aux}\<close>
   742 
   743 text \<open>
   744   Theory \<open>Pure\<close> provides a few auxiliary connectives that are defined on top
   745   of the primitive ones, see \figref{fig:pure-aux}. These special constants
   746   are useful in certain internal encodings, and are normally not directly
   747   exposed to the user.
   748 
   749   \begin{figure}[htb]
   750   \begin{center}
   751   \begin{tabular}{ll}
   752   \<open>conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop\<close> & (infix \<open>&&&\<close>) \\
   753   \<open>\<turnstile> A &&& B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)\<close> \\[1ex]
   754   \<open>prop :: prop \<Rightarrow> prop\<close> & (prefix \<open>#\<close>, suppressed) \\
   755   \<open>#A \<equiv> A\<close> \\[1ex]
   756   \<open>term :: \<alpha> \<Rightarrow> prop\<close> & (prefix \<open>TERM\<close>) \\
   757   \<open>term x \<equiv> (\<And>A. A \<Longrightarrow> A)\<close> \\[1ex]
   758   \<open>type :: \<alpha> itself\<close> & (prefix \<open>TYPE\<close>) \\
   759   \<open>(unspecified)\<close> \\
   760   \end{tabular}
   761   \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   762   \end{center}
   763   \end{figure}
   764 
   765   The introduction \<open>A \<Longrightarrow> B \<Longrightarrow> A &&& B\<close>, and eliminations (projections) \<open>A &&& B
   766   \<Longrightarrow> A\<close> and \<open>A &&& B \<Longrightarrow> B\<close> are available as derived rules. Conjunction allows to
   767   treat simultaneous assumptions and conclusions uniformly, e.g.\ consider \<open>A
   768   \<Longrightarrow> B \<Longrightarrow> C &&& D\<close>. In particular, the goal mechanism represents multiple claims
   769   as explicit conjunction internally, but this is refined (via backwards
   770   introduction) into separate sub-goals before the user commences the proof;
   771   the final result is projected into a list of theorems using eliminations
   772   (cf.\ \secref{sec:tactical-goals}).
   773 
   774   The \<open>prop\<close> marker (\<open>#\<close>) makes arbitrarily complex propositions appear as
   775   atomic, without changing the meaning: \<open>\<Gamma> \<turnstile> A\<close> and \<open>\<Gamma> \<turnstile> #A\<close> are
   776   interchangeable. See \secref{sec:tactical-goals} for specific operations.
   777 
   778   The \<open>term\<close> marker turns any well-typed term into a derivable proposition: \<open>\<turnstile>
   779   TERM t\<close> holds unconditionally. Although this is logically vacuous, it allows
   780   to treat terms and proofs uniformly, similar to a type-theoretic framework.
   781 
   782   The \<open>TYPE\<close> constructor is the canonical representative of the unspecified
   783   type \<open>\<alpha> itself\<close>; it essentially injects the language of types into that of
   784   terms. There is specific notation \<open>TYPE(\<tau>)\<close> for \<open>TYPE\<^bsub>\<tau> itself\<^esub>\<close>. Although
   785   being devoid of any particular meaning, the term \<open>TYPE(\<tau>)\<close> accounts for the
   786   type \<open>\<tau>\<close> within the term language. In particular, \<open>TYPE(\<alpha>)\<close> may be used as
   787   formal argument in primitive definitions, in order to circumvent hidden
   788   polymorphism (cf.\ \secref{sec:terms}). For example, \<open>c TYPE(\<alpha>) \<equiv> A[\<alpha>]\<close>
   789   defines \<open>c :: \<alpha> itself \<Rightarrow> prop\<close> in terms of a proposition \<open>A\<close> that depends on
   790   an additional type argument, which is essentially a predicate on types.
   791 \<close>
   792 
   793 text %mlref \<open>
   794   \begin{mldecls}
   795   @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
   796   @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
   797   @{index_ML Drule.mk_term: "cterm -> thm"} \\
   798   @{index_ML Drule.dest_term: "thm -> cterm"} \\
   799   @{index_ML Logic.mk_type: "typ -> term"} \\
   800   @{index_ML Logic.dest_type: "term -> typ"} \\
   801   \end{mldecls}
   802 
   803   \<^descr> @{ML Conjunction.intr} derives \<open>A &&& B\<close> from \<open>A\<close> and \<open>B\<close>.
   804 
   805   \<^descr> @{ML Conjunction.elim} derives \<open>A\<close> and \<open>B\<close> from \<open>A &&& B\<close>.
   806 
   807   \<^descr> @{ML Drule.mk_term} derives \<open>TERM t\<close>.
   808 
   809   \<^descr> @{ML Drule.dest_term} recovers term \<open>t\<close> from \<open>TERM t\<close>.
   810 
   811   \<^descr> @{ML Logic.mk_type}~\<open>\<tau>\<close> produces the term \<open>TYPE(\<tau>)\<close>.
   812 
   813   \<^descr> @{ML Logic.dest_type}~\<open>TYPE(\<tau>)\<close> recovers the type \<open>\<tau>\<close>.
   814 \<close>
   815 
   816 
   817 subsection \<open>Sort hypotheses\<close>
   818 
   819 text \<open>
   820   Type variables are decorated with sorts, as explained in \secref{sec:types}.
   821   This constrains type instantiation to certain ranges of types: variable
   822   \<open>\<alpha>\<^sub>s\<close> may only be assigned to types \<open>\<tau>\<close> that belong to sort \<open>s\<close>. Within the
   823   logic, sort constraints act like implicit preconditions on the result \<open>\<lparr>\<alpha>\<^sub>1
   824   : s\<^sub>1\<rparr>, \<dots>, \<lparr>\<alpha>\<^sub>n : s\<^sub>n\<rparr>, \<Gamma> \<turnstile> \<phi>\<close> where the type variables \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n\<close> cover
   825   the propositions \<open>\<Gamma>\<close>, \<open>\<phi>\<close>, as well as the proof of \<open>\<Gamma> \<turnstile> \<phi>\<close>.
   826 
   827   These \<^emph>\<open>sort hypothesis\<close> of a theorem are passed monotonically through
   828   further derivations. They are redundant, as long as the statement of a
   829   theorem still contains the type variables that are accounted here. The
   830   logical significance of sort hypotheses is limited to the boundary case
   831   where type variables disappear from the proposition, e.g.\ \<open>\<lparr>\<alpha>\<^sub>s : s\<rparr> \<turnstile> \<phi>\<close>.
   832   Since such dangling type variables can be renamed arbitrarily without
   833   changing the proposition \<open>\<phi>\<close>, the inference kernel maintains sort hypotheses
   834   in anonymous form \<open>s \<turnstile> \<phi>\<close>.
   835 
   836   In most practical situations, such extra sort hypotheses may be stripped in
   837   a final bookkeeping step, e.g.\ at the end of a proof: they are typically
   838   left over from intermediate reasoning with type classes that can be
   839   satisfied by some concrete type \<open>\<tau>\<close> of sort \<open>s\<close> to replace the hypothetical
   840   type variable \<open>\<alpha>\<^sub>s\<close>.
   841 \<close>
   842 
   843 text %mlref \<open>
   844   \begin{mldecls}
   845   @{index_ML Thm.extra_shyps: "thm -> sort list"} \\
   846   @{index_ML Thm.strip_shyps: "thm -> thm"} \\
   847   \end{mldecls}
   848 
   849   \<^descr> @{ML Thm.extra_shyps}~\<open>thm\<close> determines the extraneous sort hypotheses of
   850   the given theorem, i.e.\ the sorts that are not present within type
   851   variables of the statement.
   852 
   853   \<^descr> @{ML Thm.strip_shyps}~\<open>thm\<close> removes any extraneous sort hypotheses that
   854   can be witnessed from the type signature.
   855 \<close>
   856 
   857 text %mlex \<open>
   858   The following artificial example demonstrates the derivation of @{prop
   859   False} with a pending sort hypothesis involving a logically empty sort.
   860 \<close>
   861 
   862 class empty =
   863   assumes bad: "\<And>(x::'a) y. x \<noteq> y"
   864 
   865 theorem (in empty) false: False
   866   using bad by blast
   867 
   868 ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
   869 
   870 text \<open>
   871   Thanks to the inference kernel managing sort hypothesis according to their
   872   logical significance, this example is merely an instance of \<^emph>\<open>ex falso
   873   quodlibet consequitur\<close> --- not a collapse of the logical framework!
   874 \<close>
   875 
   876 
   877 section \<open>Object-level rules \label{sec:obj-rules}\<close>
   878 
   879 text \<open>
   880   The primitive inferences covered so far mostly serve foundational purposes.
   881   User-level reasoning usually works via object-level rules that are
   882   represented as theorems of Pure. Composition of rules involves
   883   \<^emph>\<open>backchaining\<close>, \<^emph>\<open>higher-order unification\<close> modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion of
   884   \<open>\<lambda>\<close>-terms, and so-called \<^emph>\<open>lifting\<close> of rules into a context of \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>
   885   connectives. Thus the full power of higher-order Natural Deduction in
   886   Isabelle/Pure becomes readily available.
   887 \<close>
   888 
   889 
   890 subsection \<open>Hereditary Harrop Formulae\<close>
   891 
   892 text \<open>
   893   The idea of object-level rules is to model Natural Deduction inferences in
   894   the style of Gentzen @{cite "Gentzen:1935"}, but we allow arbitrary nesting
   895   similar to @{cite extensions91}. The most basic rule format is that of a
   896   \<^emph>\<open>Horn Clause\<close>:
   897   \[
   898   \infer{\<open>A\<close>}{\<open>A\<^sub>1\<close> & \<open>\<dots>\<close> & \<open>A\<^sub>n\<close>}
   899   \]
   900   where \<open>A, A\<^sub>1, \<dots>, A\<^sub>n\<close> are atomic propositions of the framework, usually of
   901   the form \<open>Trueprop B\<close>, where \<open>B\<close> is a (compound) object-level statement.
   902   This object-level inference corresponds to an iterated implication in Pure
   903   like this:
   904   \[
   905   \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close>
   906   \]
   907   As an example consider conjunction introduction: \<open>A \<Longrightarrow> B \<Longrightarrow> A \<and> B\<close>. Any
   908   parameters occurring in such rule statements are conceptionally treated as
   909   arbitrary:
   910   \[
   911   \<open>\<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\<close>
   912   \]
   913 
   914   Nesting of rules means that the positions of \<open>A\<^sub>i\<close> may again hold compound
   915   rules, not just atomic propositions. Propositions of this format are called
   916   \<^emph>\<open>Hereditary Harrop Formulae\<close> in the literature @{cite "Miller:1991"}. Here
   917   we give an inductive characterization as follows:
   918 
   919   \<^medskip>
   920   \begin{tabular}{ll}
   921   \<open>\<^bold>x\<close> & set of variables \\
   922   \<open>\<^bold>A\<close> & set of atomic propositions \\
   923   \<open>\<^bold>H  =  \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A\<close> & set of Hereditary Harrop Formulas \\
   924   \end{tabular}
   925   \<^medskip>
   926 
   927   Thus we essentially impose nesting levels on propositions formed from \<open>\<And>\<close>
   928   and \<open>\<Longrightarrow>\<close>. At each level there is a prefix of parameters and compound
   929   premises, concluding an atomic proposition. Typical examples are
   930   \<open>\<longrightarrow>\<close>-introduction \<open>(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B\<close> or mathematical induction \<open>P 0 \<Longrightarrow> (\<And>n. P n
   931   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n\<close>. Even deeper nesting occurs in well-founded induction
   932   \<open>(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x\<close>, but this already marks the limit of
   933   rule complexity that is usually seen in practice.
   934 
   935   \<^medskip>
   936   Regular user-level inferences in Isabelle/Pure always maintain the following
   937   canonical form of results:
   938 
   939   \<^item> Normalization by \<open>(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)\<close>, which is a theorem of
   940   Pure, means that quantifiers are pushed in front of implication at each
   941   level of nesting. The normal form is a Hereditary Harrop Formula.
   942 
   943   \<^item> The outermost prefix of parameters is represented via schematic variables:
   944   instead of \<open>\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x\<close> we have \<open>\<^vec>H
   945   ?\<^vec>x \<Longrightarrow> A ?\<^vec>x\<close>. Note that this representation looses information
   946   about the order of parameters, and vacuous quantifiers vanish automatically.
   947 \<close>
   948 
   949 text %mlref \<open>
   950   \begin{mldecls}
   951   @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\
   952   \end{mldecls}
   953 
   954   \<^descr> @{ML Simplifier.norm_hhf}~\<open>ctxt thm\<close> normalizes the given theorem
   955   according to the canonical form specified above. This is occasionally
   956   helpful to repair some low-level tools that do not handle Hereditary Harrop
   957   Formulae properly.
   958 \<close>
   959 
   960 
   961 subsection \<open>Rule composition\<close>
   962 
   963 text \<open>
   964   The rule calculus of Isabelle/Pure provides two main inferences: @{inference
   965   resolution} (i.e.\ back-chaining of rules) and @{inference assumption}
   966   (i.e.\ closing a branch), both modulo higher-order unification. There are
   967   also combined variants, notably @{inference elim_resolution} and @{inference
   968   dest_resolution}.
   969 
   970   To understand the all-important @{inference resolution} principle, we first
   971   consider raw @{inference_def composition} (modulo higher-order unification
   972   with substitution \<open>\<vartheta>\<close>):
   973   \[
   974   \infer[(@{inference_def composition})]{\<open>\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}
   975   {\<open>\<^vec>A \<Longrightarrow> B\<close> & \<open>B' \<Longrightarrow> C\<close> & \<open>B\<vartheta> = B'\<vartheta>\<close>}
   976   \]
   977   Here the conclusion of the first rule is unified with the premise of the
   978   second; the resulting rule instance inherits the premises of the first and
   979   conclusion of the second. Note that \<open>C\<close> can again consist of iterated
   980   implications. We can also permute the premises of the second rule
   981   back-and-forth in order to compose with \<open>B'\<close> in any position (subsequently
   982   we shall always refer to position 1 w.l.o.g.).
   983 
   984   In @{inference composition} the internal structure of the common part \<open>B\<close>
   985   and \<open>B'\<close> is not taken into account. For proper @{inference resolution} we
   986   require \<open>B\<close> to be atomic, and explicitly observe the structure \<open>\<And>\<^vec>x.
   987   \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x\<close> of the premise of the second rule. The idea
   988   is to adapt the first rule by ``lifting'' it into this context, by means of
   989   iterated application of the following inferences:
   990   \[
   991   \infer[(@{inference_def imp_lift})]{\<open>(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)\<close>}{\<open>\<^vec>A \<Longrightarrow> B\<close>}
   992   \]
   993   \[
   994   \infer[(@{inference_def all_lift})]{\<open>(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))\<close>}{\<open>\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a\<close>}
   995   \]
   996   By combining raw composition with lifting, we get full @{inference
   997   resolution} as follows:
   998   \[
   999   \infer[(@{inference_def resolution})]
  1000   {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}
  1001   {\begin{tabular}{l}
  1002     \<open>\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a\<close> \\
  1003     \<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\
  1004     \<open>(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\
  1005    \end{tabular}}
  1006   \]
  1007 
  1008   Continued resolution of rules allows to back-chain a problem towards more
  1009   and sub-problems. Branches are closed either by resolving with a rule of 0
  1010   premises, or by producing a ``short-circuit'' within a solved situation
  1011   (again modulo unification):
  1012   \[
  1013   \infer[(@{inference_def assumption})]{\<open>C\<vartheta>\<close>}
  1014   {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{(for some~\<open>i\<close>)}}
  1015   \]
  1016 
  1017   %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
  1018 \<close>
  1019 
  1020 text %mlref \<open>
  1021   \begin{mldecls}
  1022   @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\
  1023   @{index_ML_op "RS": "thm * thm -> thm"} \\
  1024 
  1025   @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\
  1026   @{index_ML_op "RL": "thm list * thm list -> thm list"} \\
  1027 
  1028   @{index_ML_op "MRS": "thm list * thm -> thm"} \\
  1029   @{index_ML_op "OF": "thm * thm list -> thm"} \\
  1030   \end{mldecls}
  1031 
  1032   \<^descr> \<open>rule\<^sub>1 RSN (i, rule\<^sub>2)\<close> resolves the conclusion of \<open>rule\<^sub>1\<close> with the
  1033   \<open>i\<close>-th premise of \<open>rule\<^sub>2\<close>, according to the @{inference resolution}
  1034   principle explained above. Unless there is precisely one resolvent it raises
  1035   exception @{ML THM}.
  1036 
  1037   This corresponds to the rule attribute @{attribute THEN} in Isar source
  1038   language.
  1039 
  1040   \<^descr> \<open>rule\<^sub>1 RS rule\<^sub>2\<close> abbreviates \<open>rule\<^sub>1 RSN (1, rule\<^sub>2)\<close>.
  1041 
  1042   \<^descr> \<open>rules\<^sub>1 RLN (i, rules\<^sub>2)\<close> joins lists of rules. For every \<open>rule\<^sub>1\<close> in
  1043   \<open>rules\<^sub>1\<close> and \<open>rule\<^sub>2\<close> in \<open>rules\<^sub>2\<close>, it resolves the conclusion of \<open>rule\<^sub>1\<close>
  1044   with the \<open>i\<close>-th premise of \<open>rule\<^sub>2\<close>, accumulating multiple results in one
  1045   big list. Note that such strict enumerations of higher-order unifications
  1046   can be inefficient compared to the lazy variant seen in elementary tactics
  1047   like @{ML resolve_tac}.
  1048 
  1049   \<^descr> \<open>rules\<^sub>1 RL rules\<^sub>2\<close> abbreviates \<open>rules\<^sub>1 RLN (1, rules\<^sub>2)\<close>.
  1050 
  1051   \<^descr> \<open>[rule\<^sub>1, \<dots>, rule\<^sub>n] MRS rule\<close> resolves \<open>rule\<^sub>i\<close> against premise \<open>i\<close> of
  1052   \<open>rule\<close>, for \<open>i = n, \<dots>, 1\<close>. By working from right to left, newly emerging
  1053   premises are concatenated in the result, without interfering.
  1054 
  1055   \<^descr> \<open>rule OF rules\<close> is an alternative notation for \<open>rules MRS rule\<close>, which
  1056   makes rule composition look more like function application. Note that the
  1057   argument \<open>rules\<close> need not be atomic.
  1058 
  1059   This corresponds to the rule attribute @{attribute OF} in Isar source
  1060   language.
  1061 \<close>
  1062 
  1063 
  1064 section \<open>Proof terms \label{sec:proof-terms}\<close>
  1065 
  1066 text \<open>
  1067   The Isabelle/Pure inference kernel can record the proof of each theorem as a
  1068   proof term that contains all logical inferences in detail. Rule composition
  1069   by resolution (\secref{sec:obj-rules}) and type-class reasoning is broken
  1070   down to primitive rules of the logical framework. The proof term can be
  1071   inspected by a separate proof-checker, for example.
  1072 
  1073   According to the well-known \<^emph>\<open>Curry-Howard isomorphism\<close>, a proof can be
  1074   viewed as a \<open>\<lambda>\<close>-term. Following this idea, proofs in Isabelle are internally
  1075   represented by a datatype similar to the one for terms described in
  1076   \secref{sec:terms}. On top of these syntactic terms, two more layers of
  1077   \<open>\<lambda>\<close>-calculus are added, which correspond to \<open>\<And>x :: \<alpha>. B x\<close> and \<open>A \<Longrightarrow> B\<close>
  1078   according to the propositions-as-types principle. The resulting 3-level
  1079   \<open>\<lambda>\<close>-calculus resembles ``\<open>\<lambda>HOL\<close>'' in the more abstract setting of Pure Type
  1080   Systems (PTS) @{cite "Barendregt-Geuvers:2001"}, if some fine points like
  1081   schematic polymorphism and type classes are ignored.
  1082 
  1083   \<^medskip>
  1084   \<^emph>\<open>Proof abstractions\<close> of the form \<open>\<^bold>\<lambda>x :: \<alpha>. prf\<close> or \<open>\<^bold>\<lambda>p : A. prf\<close>
  1085   correspond to introduction of \<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>, and \<^emph>\<open>proof applications\<close> of the form
  1086   \<open>p \<cdot> t\<close> or \<open>p \<bullet> q\<close> correspond to elimination of \<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>. Actual types \<open>\<alpha>\<close>,
  1087   propositions \<open>A\<close>, and terms \<open>t\<close> might be suppressed and reconstructed from
  1088   the overall proof term.
  1089 
  1090   \<^medskip>
  1091   Various atomic proofs indicate special situations within the proof
  1092   construction as follows.
  1093 
  1094   A \<^emph>\<open>bound proof variable\<close> is a natural number \<open>b\<close> that acts as de-Bruijn
  1095   index for proof term abstractions.
  1096 
  1097   A \<^emph>\<open>minimal proof\<close> ``\<open>?\<close>'' is a dummy proof term. This indicates some
  1098   unrecorded part of the proof.
  1099 
  1100   \<open>Hyp A\<close> refers to some pending hypothesis by giving its proposition. This
  1101   indicates an open context of implicit hypotheses, similar to loose bound
  1102   variables or free variables within a term (\secref{sec:terms}).
  1103 
  1104   An \<^emph>\<open>axiom\<close> or \<^emph>\<open>oracle\<close> \<open>a : A[\<^vec>\<tau>]\<close> refers some postulated \<open>proof
  1105   constant\<close>, which is subject to schematic polymorphism of theory content, and
  1106   the particular type instantiation may be given explicitly. The vector of
  1107   types \<open>\<^vec>\<tau>\<close> refers to the schematic type variables in the generic
  1108   proposition \<open>A\<close> in canonical order.
  1109 
  1110   A \<^emph>\<open>proof promise\<close> \<open>a : A[\<^vec>\<tau>]\<close> is a placeholder for some proof of
  1111   polymorphic proposition \<open>A\<close>, with explicit type instantiation as given by
  1112   the vector \<open>\<^vec>\<tau>\<close>, as above. Unlike axioms or oracles, proof promises
  1113   may be \<^emph>\<open>fulfilled\<close> eventually, by substituting \<open>a\<close> by some particular proof
  1114   \<open>q\<close> at the corresponding type instance. This acts like Hindley-Milner
  1115   \<open>let\<close>-polymorphism: a generic local proof definition may get used at
  1116   different type instances, and is replaced by the concrete instance
  1117   eventually.
  1118 
  1119   A \<^emph>\<open>named theorem\<close> wraps up some concrete proof as a closed formal entity,
  1120   in the manner of constant definitions for proof terms. The \<^emph>\<open>proof body\<close> of
  1121   such boxed theorems involves some digest about oracles and promises
  1122   occurring in the original proof. This allows the inference kernel to manage
  1123   this critical information without the full overhead of explicit proof terms.
  1124 \<close>
  1125 
  1126 
  1127 subsection \<open>Reconstructing and checking proof terms\<close>
  1128 
  1129 text \<open>
  1130   Fully explicit proof terms can be large, but most of this information is
  1131   redundant and can be reconstructed from the context. Therefore, the
  1132   Isabelle/Pure inference kernel records only \<^emph>\<open>implicit\<close> proof terms, by
  1133   omitting all typing information in terms, all term and type labels of proof
  1134   abstractions, and some argument terms of applications \<open>p \<cdot> t\<close> (if possible).
  1135 
  1136   There are separate operations to reconstruct the full proof term later on,
  1137   using \<^emph>\<open>higher-order pattern unification\<close> @{cite "nipkow-patterns" and
  1138   "Berghofer-Nipkow:2000:TPHOL"}.
  1139 
  1140   The \<^emph>\<open>proof checker\<close> expects a fully reconstructed proof term, and can turn
  1141   it into a theorem by replaying its primitive inferences within the kernel.
  1142 \<close>
  1143 
  1144 
  1145 subsection \<open>Concrete syntax of proof terms\<close>
  1146 
  1147 text \<open>
  1148   The concrete syntax of proof terms is a slight extension of the regular
  1149   inner syntax of Isabelle/Pure @{cite "isabelle-isar-ref"}. Its main
  1150   syntactic category @{syntax (inner) proof} is defined as follows:
  1151 
  1152   \begin{center}
  1153   \begin{supertabular}{rclr}
  1154 
  1155   @{syntax_def (inner) proof} & = & \<^verbatim>\<open>Lam\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
  1156     & \<open>|\<close> & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
  1157     & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%\<close> \<open>any\<close> \\
  1158     & \<open>|\<close> & \<open>proof\<close> \<open>\<cdot>\<close> \<open>any\<close> \\
  1159     & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%%\<close> \<open>proof\<close> \\
  1160     & \<open>|\<close> & \<open>proof\<close> \<open>\<bullet>\<close> \<open>proof\<close> \\
  1161     & \<open>|\<close> & \<open>id  |  longid\<close> \\
  1162   \\
  1163 
  1164   \<open>param\<close> & = & \<open>idt\<close> \\
  1165     & \<open>|\<close> & \<open>idt\<close> \<^verbatim>\<open>:\<close> \<open>prop\<close> \\
  1166     & \<open>|\<close> & \<^verbatim>\<open>(\<close> \<open>param\<close> \<^verbatim>\<open>)\<close> \\
  1167   \\
  1168 
  1169   \<open>params\<close> & = & \<open>param\<close> \\
  1170     & \<open>|\<close> & \<open>param\<close> \<open>params\<close> \\
  1171 
  1172   \end{supertabular}
  1173   \end{center}
  1174 
  1175   Implicit term arguments in partial proofs are indicated by ``\<open>_\<close>''. Type
  1176   arguments for theorems and axioms may be specified using \<open>p \<cdot> TYPE(type)\<close>
  1177   (they must appear before any other term argument of a theorem or axiom, but
  1178   may be omitted altogether).
  1179 
  1180   \<^medskip>
  1181   There are separate read and print operations for proof terms, in order to
  1182   avoid conflicts with the regular term language.
  1183 \<close>
  1184 
  1185 text %mlref \<open>
  1186   \begin{mldecls}
  1187   @{index_ML_type proof} \\
  1188   @{index_ML_type proof_body} \\
  1189   @{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\
  1190   @{index_ML Reconstruct.reconstruct_proof:
  1191   "Proof.context -> term -> proof -> proof"} \\
  1192   @{index_ML Reconstruct.expand_proof: "Proof.context ->
  1193   (string * term option) list -> proof -> proof"} \\
  1194   @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
  1195   @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
  1196   @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
  1197   \end{mldecls}
  1198 
  1199   \<^descr> Type @{ML_type proof} represents proof terms; this is a datatype with
  1200   constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"},
  1201   @{index_ML_op "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
  1202   Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML Promise}, @{index_ML
  1203   PThm} as explained above. %FIXME OfClass (!?)
  1204 
  1205   \<^descr> Type @{ML_type proof_body} represents the nested proof information of a
  1206   named theorem, consisting of a digest of oracles and named theorem over some
  1207   proof term. The digest only covers the directly visible part of the proof:
  1208   in order to get the full information, the implicit graph of nested theorems
  1209   needs to be traversed (e.g.\ using @{ML Proofterm.fold_body_thms}).
  1210 
  1211   \<^descr> @{ML Thm.proof_of}~\<open>thm\<close> and @{ML Thm.proof_body_of}~\<open>thm\<close> produce the
  1212   proof term or proof body (with digest of oracles and theorems) from a given
  1213   theorem. Note that this involves a full join of internal futures that
  1214   fulfill pending proof promises, and thus disrupts the natural bottom-up
  1215   construction of proofs by introducing dynamic ad-hoc dependencies. Parallel
  1216   performance may suffer by inspecting proof terms at run-time.
  1217 
  1218   \<^descr> @{ML Proofterm.proofs} specifies the detail of proof recording within
  1219   @{ML_type thm} values produced by the inference kernel: @{ML 0} records only
  1220   the names of oracles, @{ML 1} records oracle names and propositions, @{ML 2}
  1221   additionally records full proof terms. Officially named theorems that
  1222   contribute to a result are recorded in any case.
  1223 
  1224   \<^descr> @{ML Reconstruct.reconstruct_proof}~\<open>ctxt prop prf\<close> turns the implicit
  1225   proof term \<open>prf\<close> into a full proof of the given proposition.
  1226 
  1227   Reconstruction may fail if \<open>prf\<close> is not a proof of \<open>prop\<close>, or if it does not
  1228   contain sufficient information for reconstruction. Failure may only happen
  1229   for proofs that are constructed manually, but not for those produced
  1230   automatically by the inference kernel.
  1231 
  1232   \<^descr> @{ML Reconstruct.expand_proof}~\<open>ctxt [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and
  1233   reconstructs the proofs of all specified theorems, with the given (full)
  1234   proof. Theorems that are not unique specified via their name may be
  1235   disambiguated by giving their proposition.
  1236 
  1237   \<^descr> @{ML Proof_Checker.thm_of_proof}~\<open>thy prf\<close> turns the given (full) proof
  1238   into a theorem, by replaying it using only primitive rules of the inference
  1239   kernel.
  1240 
  1241   \<^descr> @{ML Proof_Syntax.read_proof}~\<open>thy b\<^sub>1 b\<^sub>2 s\<close> reads in a proof term. The
  1242   Boolean flags indicate the use of sort and type information. Usually, typing
  1243   information is left implicit and is inferred during proof reconstruction.
  1244   %FIXME eliminate flags!?
  1245 
  1246   \<^descr> @{ML Proof_Syntax.pretty_proof}~\<open>ctxt prf\<close> pretty-prints the given proof
  1247   term.
  1248 \<close>
  1249 
  1250 text %mlex \<open>
  1251   \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close> provides basic examples involving
  1252   proof terms.
  1253 
  1254   \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/XML_Data.thy\<close> demonstrates export and import of
  1255   proof terms via XML/ML data representation.
  1256 \<close>
  1257 
  1258 end