src/Doc/IsarImplementation/Logic.thy
author wenzelm
Mon Jun 17 21:23:49 2013 +0200 (2013-06-17)
changeset 52412 4cfa094da3cb
parent 52411 f192c4ea5b17
child 52422 93f3f9a2ae91
permissions -rw-r--r--
more on concrete syntax of 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 
  1277 subsection {* Reconstructing and checking proof terms *}
  1278 
  1279 text {* Fully explicit proof terms can be large, but most of this
  1280   information is redundant and can be reconstructed from the context.
  1281   Therefore, the Isabelle/Pure inference kernel records only
  1282   \emph{implicit} proof terms, by omitting all typing information in
  1283   terms, all term and type labels of proof abstractions, and some
  1284   argument terms of applications @{text "p \<cdot> t"} (if possible).
  1285 
  1286   There are separate operations to reconstruct the full proof term
  1287   later on, using \emph{higher-order pattern unification}
  1288   \cite{nipkow-patterns,Berghofer-Nipkow:2000:TPHOL}.
  1289 
  1290   The \emph{proof checker} expects a fully reconstructed proof term,
  1291   and can turn it into a theorem by replaying its primitive inferences
  1292   within the kernel.  *}
  1293 
  1294 
  1295 subsection {* Concrete syntax of proof terms *}
  1296 
  1297 text {* The concrete syntax of proof terms is a slight extension of
  1298   the regular inner syntax of Isabelle/Pure \cite{isabelle-isar-ref}.
  1299   Its main syntactic category @{syntax (inner) proof} is defined as
  1300   follows:
  1301 
  1302   \begin{center}
  1303   \begin{supertabular}{rclr}
  1304 
  1305   @{syntax_def (inner) proof} & = & @{verbatim Lam} @{text params} @{verbatim "."} @{text proof} \\
  1306     & @{text "|"} & @{text "\<Lambda>"} @{text "params"} @{verbatim "."} @{text proof} \\
  1307     & @{text "|"} & @{text proof} @{verbatim "%"} @{text any} \\
  1308     & @{text "|"} & @{text proof} @{text "\<cdot>"} @{text any} \\
  1309     & @{text "|"} & @{text proof} @{verbatim "%%"} @{text proof} \\
  1310     & @{text "|"} & @{text proof} @{text "\<bullet>"} @{text proof} \\
  1311     & @{text "|"} & @{text "id  |  longid"} \\
  1312   \\
  1313 
  1314   @{text param} & = & @{text idt} \\
  1315     & @{text "|"} & @{text idt} @{verbatim ":"} @{text prop} \\
  1316     & @{text "|"} & @{verbatim "("} @{text param} @{verbatim ")"} \\
  1317   \\
  1318 
  1319   @{text params} & = & @{text param} \\
  1320     & @{text "|"} & @{text param} @{text params} \\
  1321 
  1322   \end{supertabular}
  1323   \end{center}
  1324 
  1325   Implicit term arguments in partial proofs are indicated by ``@{text
  1326   "_"}''.  Type arguments for theorems and axioms may be specified
  1327   using @{text "p \<cdot> TYPE(type)"} (they must appear before any other
  1328   term argument of a theorem or axiom, but may be omitted altogether).
  1329 
  1330   \medskip There are separate read and print operations for proof
  1331   terms, in order to avoid conflicts with the regular term language.
  1332 *}
  1333 
  1334 text %mlref {*
  1335   \begin{mldecls}
  1336   @{index_ML_type proof} \\
  1337   @{index_ML_type proof_body} \\
  1338   @{index_ML proofs: "int Unsynchronized.ref"} \\
  1339   @{index_ML Reconstruct.reconstruct_proof:
  1340   "theory -> term -> proof -> proof"} \\
  1341   @{index_ML Reconstruct.expand_proof: "theory ->
  1342   (string * term option) list -> proof -> proof"} \\
  1343   @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
  1344   @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
  1345   @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
  1346   \end{mldecls}
  1347 
  1348   \begin{description}
  1349 
  1350   \item Type @{ML_type proof} represents proof terms; this is a
  1351   datatype with constructors @{index_ML Abst}, @{index_ML AbsP},
  1352   @{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound},
  1353   @{index_ML MinProof}, @{index_ML Hyp}, @{index_ML PAxm}, @{index_ML
  1354   Oracle}, @{index_ML Promise}, @{index_ML PThm} as explained above.
  1355 
  1356   \item Type @{ML_type proof_body} represents the nested proof
  1357   information of a named theorem, consisting of a digest of oracles
  1358   and named theorem over some proof term.  The digest only covers the
  1359   directly visible part of the proof: in order to get the full
  1360   information, the implicit graph of nested theorems needs to be
  1361   traversed (e.g.\ using @{ML Proofterm.fold_body_thms}).
  1362 
  1363   \item @{ML Thm.proof_of}~@{text "thm"} and @{ML
  1364   Thm.proof_body_of}~@{text "thm"} produce the proof term or proof
  1365   body (with digest of oracles and theorems) from a given theorem.
  1366   Note that this involves a full join of internal futures that fulfill
  1367   pending proof promises, and thus disrupts the natural bottom-up
  1368   construction of proofs by introducing dynamic ad-hoc dependencies.
  1369   Parallel performance may suffer by inspecting proof terms at
  1370   run-time.
  1371 
  1372   \item @{ML proofs} specifies the detail of proof recording within
  1373   @{ML_type thm} values produced by the inference kernel: @{ML 0}
  1374   records only the names of oracles, @{ML 1} records oracle names and
  1375   propositions, @{ML 2} additionally records full proof terms.
  1376   Officially named theorems that contribute to a result are recorded
  1377   in any case.
  1378 
  1379   \item @{ML Reconstruct.reconstruct_proof}~@{text "thy prop prf"}
  1380   turns the implicit proof term @{text "prf"} into a full proof of the
  1381   given proposition.
  1382 
  1383   Reconstruction may fail if @{text "prf"} is not a proof of @{text
  1384   "prop"}, or if it does not contain sufficient information for
  1385   reconstruction.  Failure may only happen for proofs that are
  1386   constructed manually, but not for those produced automatically by
  1387   the inference kernel.
  1388 
  1389   \item @{ML Reconstruct.expand_proof}~@{text "thy [thm\<^sub>1, \<dots>, thm\<^sub>n]
  1390   prf"} expands and reconstructs the proofs of all specified theorems,
  1391   with the given (full) proof.  Theorems that are not unique specified
  1392   via their name may be disambiguated by giving their proposition.
  1393 
  1394   \item @{ML Proof_Checker.thm_of_proof}~@{text "thy prf"} turns the
  1395   given (full) proof into a theorem, by replaying it using only
  1396   primitive rules of the inference kernel.
  1397 
  1398   \item @{ML Proof_Syntax.read_proof}~@{text "thy b\<^sub>1 b\<^sub>2 s"} reads in a
  1399   proof term. The Boolean flags indicate the use of sort and type
  1400   information.  Usually, typing information is left implicit and is
  1401   inferred during proof reconstruction.  %FIXME eliminate flags!?
  1402 
  1403   \item @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"}
  1404   pretty-prints the given proof term.
  1405 
  1406   \end{description}
  1407 *}
  1408 
  1409 text %mlex {* Detailed proof information of a theorem may be retrieved
  1410   as follows: *}
  1411 
  1412 lemma ex: "A \<and> B \<longrightarrow> B \<and> A"
  1413 proof
  1414   assume "A \<and> B"
  1415   then obtain B and A ..
  1416   then show "B \<and> A" ..
  1417 qed
  1418 
  1419 ML_val {*
  1420   (*proof body with digest*)
  1421   val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});
  1422 
  1423   (*proof term only*)
  1424   val prf = Proofterm.proof_of body;
  1425   Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
  1426 
  1427   (*all theorems used in the graph of nested proofs*)
  1428   val all_thms =
  1429     Proofterm.fold_body_thms
  1430       (fn (name, _, _) => insert (op =) name) [body] [];
  1431 *}
  1432 
  1433 text {* The result refers to various basic facts of Isabelle/HOL:
  1434   @{thm [source] HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source]
  1435   HOL.conjI} etc.  The combinator @{ML Proofterm.fold_body_thms}
  1436   recursively explores the graph of the proofs of all theorems being
  1437   used here.
  1438 
  1439   \medskip Alternatively, we may produce a proof term manually, and
  1440   turn it into a theorem as follows: *}
  1441 
  1442 ML_val {*
  1443   val thy = @{theory};
  1444   val prf =
  1445     Proof_Syntax.read_proof thy true false
  1446       "impI \<cdot> _ \<cdot> _ \<bullet> \
  1447       \   (Lam H: _. \
  1448       \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
  1449       \       (Lam (H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
  1450   val thm =
  1451     prf
  1452     |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
  1453     |> Proof_Checker.thm_of_proof thy
  1454     |> Drule.export_without_context;
  1455 *}
  1456 
  1457 text {* \medskip The subsequent example illustrates the use of various
  1458   key operations on proof terms: the proof term of an existing theorem
  1459   is reconstructed and turned again into a theorem using the proof
  1460   checker; some informative output is printed as well.  *}
  1461 
  1462 ML {*
  1463   fun recheck ctxt0 thm0 =
  1464     let
  1465       (*formal transfer and import -- avoid schematic variables*)
  1466       val thy = Proof_Context.theory_of ctxt0;
  1467       val ((_, [thm]), ctxt) =
  1468         Variable.import true [Thm.transfer thy thm0] ctxt0;
  1469 
  1470       (*main proof information*)
  1471       val prop = Thm.prop_of thm;
  1472       val prf =
  1473         Proofterm.proof_of
  1474           (Proofterm.strip_thm (Thm.proof_body_of thm));
  1475       val full_prf = Reconstruct.reconstruct_proof thy prop prf;
  1476 
  1477       (*informative output*)
  1478       fun pretty_item name prt =
  1479         Pretty.block [Pretty.str name, Pretty.brk 1, prt];
  1480       val _ =
  1481         [pretty_item "proposition:" (Syntax.pretty_term ctxt prop),
  1482          pretty_item "proof:" (Proof_Syntax.pretty_proof ctxt prf),
  1483          pretty_item "full proof:"
  1484           (Proof_Syntax.pretty_proof ctxt full_prf)]
  1485         |> Pretty.chunks |> Pretty.writeln;
  1486     in
  1487       (*rechecked theorem*)
  1488       Proof_Checker.thm_of_proof thy full_prf
  1489       |> singleton (Proof_Context.export ctxt ctxt0)
  1490     end;
  1491 *}
  1492 
  1493 text {* As anticipated, the rechecked theorem establishes the same
  1494   proposition: *}
  1495 
  1496 ML_val {*
  1497   val thm = @{thm ex};
  1498   val thm' = recheck @{context} thm;
  1499   @{assert} (Thm.eq_thm_prop (thm, thm'));
  1500 *}
  1501 
  1502 text {* More precise theorem equality is achieved by adjusting a few
  1503   accidental details of the theorems involved here: *}
  1504 
  1505 ML_val {*
  1506   val thm = Thm.map_tags (K []) @{thm ex};
  1507   val thm' = Thm.strip_shyps (recheck @{context} thm);
  1508   @{assert} (Thm.eq_thm (thm, thm'));
  1509 *}
  1510 
  1511 end