src/Doc/IsarImplementation/Logic.thy
author wenzelm
Tue Aug 28 18:57:32 2012 +0200 (2012-08-28)
changeset 48985 5386df44a037
parent 48938 doc-src/IsarImplementation/Logic.thy@d468d72a458f
child 50126 3dec88149176
permissions -rw-r--r--
renamed doc-src to src/Doc;
renamed TutorialI to Tutorial;
     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 @{ML Bound}, @{ML Free}, @{ML
   382   Var}, @{ML Const}, @{ML Abs}, @{ML_op "$"}.
   383 
   384   \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text
   385   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
   386   on type @{ML_type term}; raw datatype equality should only be used
   387   for operations related to parsing or printing!
   388 
   389   \item @{ML Term.map_types}~@{text "f t"} applies the mapping @{text
   390   "f"} to all types occurring in @{text "t"}.
   391 
   392   \item @{ML Term.fold_types}~@{text "f t"} iterates the operation
   393   @{text "f"} over all occurrences of types in @{text "t"}; the term
   394   structure is traversed from left to right.
   395 
   396   \item @{ML Term.map_aterms}~@{text "f t"} applies the mapping @{text
   397   "f"} to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
   398   Const}) occurring in @{text "t"}.
   399 
   400   \item @{ML Term.fold_aterms}~@{text "f t"} iterates the operation
   401   @{text "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML
   402   Free}, @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
   403   traversed from left to right.
   404 
   405   \item @{ML fastype_of}~@{text "t"} determines the type of a
   406   well-typed term.  This operation is relatively slow, despite the
   407   omission of any sanity checks.
   408 
   409   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
   410   "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the
   411   body @{text "b"} are replaced by bound variables.
   412 
   413   \item @{ML betapply}~@{text "(t, u)"} produces an application @{text
   414   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
   415   abstraction.
   416 
   417   \item @{ML incr_boundvars}~@{text "j"} increments a term's dangling
   418   bound variables by the offset @{text "j"}.  This is required when
   419   moving a subterm into a context where it is enclosed by a different
   420   number of abstractions.  Bound variables with a matching abstraction
   421   are unaffected.
   422 
   423   \item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares
   424   a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
   425 
   426   \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
   427   introduces a new term abbreviation @{text "c \<equiv> t"}.
   428 
   429   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
   430   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
   431   convert between two representations of polymorphic constants: full
   432   type instance vs.\ compact type arguments form.
   433 
   434   \end{description}
   435 *}
   436 
   437 text %mlantiq {*
   438   \begin{matharray}{rcl}
   439   @{ML_antiquotation_def "const_name"} & : & @{text ML_antiquotation} \\
   440   @{ML_antiquotation_def "const_abbrev"} & : & @{text ML_antiquotation} \\
   441   @{ML_antiquotation_def "const"} & : & @{text ML_antiquotation} \\
   442   @{ML_antiquotation_def "term"} & : & @{text ML_antiquotation} \\
   443   @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\
   444   \end{matharray}
   445 
   446   @{rail "
   447   (@@{ML_antiquotation const_name} |
   448    @@{ML_antiquotation const_abbrev}) nameref
   449   ;
   450   @@{ML_antiquotation const} ('(' (type + ',') ')')?
   451   ;
   452   @@{ML_antiquotation term} term
   453   ;
   454   @@{ML_antiquotation prop} prop
   455   "}
   456 
   457   \begin{description}
   458 
   459   \item @{text "@{const_name c}"} inlines the internalized logical
   460   constant name @{text "c"} --- as @{ML_type string} literal.
   461 
   462   \item @{text "@{const_abbrev c}"} inlines the internalized
   463   abbreviated constant name @{text "c"} --- as @{ML_type string}
   464   literal.
   465 
   466   \item @{text "@{const c(\<^vec>\<tau>)}"} inlines the internalized
   467   constant @{text "c"} with precise type instantiation in the sense of
   468   @{ML Sign.const_instance} --- as @{ML Const} constructor term for
   469   datatype @{ML_type term}.
   470 
   471   \item @{text "@{term t}"} inlines the internalized term @{text "t"}
   472   --- as constructor term for datatype @{ML_type term}.
   473 
   474   \item @{text "@{prop \<phi>}"} inlines the internalized proposition
   475   @{text "\<phi>"} --- as constructor term for datatype @{ML_type term}.
   476 
   477   \end{description}
   478 *}
   479 
   480 
   481 section {* Theorems \label{sec:thms} *}
   482 
   483 text {*
   484   A \emph{proposition} is a well-typed term of type @{text "prop"}, a
   485   \emph{theorem} is a proven proposition (depending on a context of
   486   hypotheses and the background theory).  Primitive inferences include
   487   plain Natural Deduction rules for the primary connectives @{text
   488   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
   489   notion of equality/equivalence @{text "\<equiv>"}.
   490 *}
   491 
   492 
   493 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
   494 
   495 text {*
   496   The theory @{text "Pure"} contains constant declarations for the
   497   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
   498   the logical framework, see \figref{fig:pure-connectives}.  The
   499   derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
   500   defined inductively by the primitive inferences given in
   501   \figref{fig:prim-rules}, with the global restriction that the
   502   hypotheses must \emph{not} contain any schematic variables.  The
   503   builtin equality is conceptually axiomatized as shown in
   504   \figref{fig:pure-equality}, although the implementation works
   505   directly with derived inferences.
   506 
   507   \begin{figure}[htb]
   508   \begin{center}
   509   \begin{tabular}{ll}
   510   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
   511   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
   512   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
   513   \end{tabular}
   514   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
   515   \end{center}
   516   \end{figure}
   517 
   518   \begin{figure}[htb]
   519   \begin{center}
   520   \[
   521   \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}
   522   \qquad
   523   \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
   524   \]
   525   \[
   526   \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
   527   \qquad
   528   \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
   529   \]
   530   \[
   531   \infer[@{text "(\<Longrightarrow>\<hyphen>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
   532   \qquad
   533   \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"}}
   534   \]
   535   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
   536   \end{center}
   537   \end{figure}
   538 
   539   \begin{figure}[htb]
   540   \begin{center}
   541   \begin{tabular}{ll}
   542   @{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}-conversion \\
   543   @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
   544   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
   545   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
   546   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\
   547   \end{tabular}
   548   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
   549   \end{center}
   550   \end{figure}
   551 
   552   The introduction and elimination rules for @{text "\<And>"} and @{text
   553   "\<Longrightarrow>"} are analogous to formation of dependently typed @{text
   554   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
   555   are irrelevant in the Pure logic, though; they cannot occur within
   556   propositions.  The system provides a runtime option to record
   557   explicit proof terms for primitive inferences.  Thus all three
   558   levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
   559   terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
   560   \cite{Berghofer-Nipkow:2000:TPHOL}).
   561 
   562   Observe that locally fixed parameters (as in @{text
   563   "\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because
   564   the simple syntactic types of Pure are always inhabitable.
   565   ``Assumptions'' @{text "x :: \<tau>"} for type-membership are only
   566   present as long as some @{text "x\<^isub>\<tau>"} occurs in the statement
   567   body.\footnote{This is the key difference to ``@{text "\<lambda>HOL"}'' in
   568   the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses
   569   @{text "x : A"} are treated uniformly for propositions and types.}
   570 
   571   \medskip The axiomatization of a theory is implicitly closed by
   572   forming all instances of type and term variables: @{text "\<turnstile>
   573   A\<vartheta>"} holds for any substitution instance of an axiom
   574   @{text "\<turnstile> A"}.  By pushing substitutions through derivations
   575   inductively, we also get admissible @{text "generalize"} and @{text
   576   "instantiate"} rules as shown in \figref{fig:subst-rules}.
   577 
   578   \begin{figure}[htb]
   579   \begin{center}
   580   \[
   581   \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}
   582   \quad
   583   \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
   584   \]
   585   \[
   586   \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}
   587   \quad
   588   \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}
   589   \]
   590   \caption{Admissible substitution rules}\label{fig:subst-rules}
   591   \end{center}
   592   \end{figure}
   593 
   594   Note that @{text "instantiate"} does not require an explicit
   595   side-condition, because @{text "\<Gamma>"} may never contain schematic
   596   variables.
   597 
   598   In principle, variables could be substituted in hypotheses as well,
   599   but this would disrupt the monotonicity of reasoning: deriving
   600   @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is
   601   correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
   602   the result belongs to a different proof context.
   603 
   604   \medskip An \emph{oracle} is a function that produces axioms on the
   605   fly.  Logically, this is an instance of the @{text "axiom"} rule
   606   (\figref{fig:prim-rules}), but there is an operational difference.
   607   The system always records oracle invocations within derivations of
   608   theorems by a unique tag.
   609 
   610   Axiomatizations should be limited to the bare minimum, typically as
   611   part of the initial logical basis of an object-logic formalization.
   612   Later on, theories are usually developed in a strictly definitional
   613   fashion, by stating only certain equalities over new constants.
   614 
   615   A \emph{simple definition} consists of a constant declaration @{text
   616   "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t
   617   :: \<sigma>"} is a closed term without any hidden polymorphism.  The RHS
   618   may depend on further defined constants, but not @{text "c"} itself.
   619   Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>
   620   t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.
   621 
   622   An \emph{overloaded definition} consists of a collection of axioms
   623   for the same constant, with zero or one equations @{text
   624   "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for
   625   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention
   626   previously defined constants as above, or arbitrary constants @{text
   627   "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text
   628   "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by
   629   primitive recursion over the syntactic structure of a single type
   630   argument.  See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.
   631 *}
   632 
   633 text %mlref {*
   634   \begin{mldecls}
   635   @{index_ML Logic.all: "term -> term -> term"} \\
   636   @{index_ML Logic.mk_implies: "term * term -> term"} \\
   637   \end{mldecls}
   638   \begin{mldecls}
   639   @{index_ML_type ctyp} \\
   640   @{index_ML_type cterm} \\
   641   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
   642   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
   643   @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\
   644   @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
   645   @{index_ML Thm.all: "cterm -> cterm -> cterm"} \\
   646   @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
   647   \end{mldecls}
   648   \begin{mldecls}
   649   @{index_ML_type thm} \\
   650   @{index_ML proofs: "int Unsynchronized.ref"} \\
   651   @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
   652   @{index_ML Thm.assume: "cterm -> thm"} \\
   653   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   654   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
   655   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   656   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
   657   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   658   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
   659   @{index_ML Thm.add_axiom: "Proof.context ->
   660   binding * term -> theory -> (string * thm) * theory"} \\
   661   @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
   662   (string * ('a -> thm)) * theory"} \\
   663   @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->
   664   binding * term -> theory -> (string * thm) * theory"} \\
   665   \end{mldecls}
   666   \begin{mldecls}
   667   @{index_ML Theory.add_deps: "Proof.context -> string ->
   668   string * typ -> (string * typ) list -> theory -> theory"} \\
   669   \end{mldecls}
   670 
   671   \begin{description}
   672 
   673   \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification
   674   @{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in
   675   the body proposition @{text "B"} are replaced by bound variables.
   676   (See also @{ML lambda} on terms.)
   677 
   678   \item @{ML Logic.mk_implies}~@{text "(A, B)"} produces a Pure
   679   implication @{text "A \<Longrightarrow> B"}.
   680 
   681   \item Types @{ML_type ctyp} and @{ML_type cterm} represent certified
   682   types and terms, respectively.  These are abstract datatypes that
   683   guarantee that its values have passed the full well-formedness (and
   684   well-typedness) checks, relative to the declarations of type
   685   constructors, constants etc.\ in the background theory.  The
   686   abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the
   687   same inference kernel that is mainly responsible for @{ML_type thm}.
   688   Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}
   689   are located in the @{ML_struct Thm} module, even though theorems are
   690   not yet involved at that stage.
   691 
   692   \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML
   693   Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,
   694   respectively.  This also involves some basic normalizations, such
   695   expansion of type and term abbreviations from the theory context.
   696   Full re-certification is relatively slow and should be avoided in
   697   tight reasoning loops.
   698 
   699   \item @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML
   700   Drule.mk_implies} etc.\ compose certified terms (or propositions)
   701   incrementally.  This is equivalent to @{ML Thm.cterm_of} after
   702   unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML
   703   Logic.mk_implies} etc., but there can be a big difference in
   704   performance when large existing entities are composed by a few extra
   705   constructions on top.  There are separate operations to decompose
   706   certified terms and theorems to produce certified terms again.
   707 
   708   \item Type @{ML_type thm} represents proven propositions.  This is
   709   an abstract datatype that guarantees that its values have been
   710   constructed by basic principles of the @{ML_struct Thm} module.
   711   Every @{ML_type thm} value contains a sliding back-reference to the
   712   enclosing theory, cf.\ \secref{sec:context-theory}.
   713 
   714   \item @{ML proofs} specifies the detail of proof recording within
   715   @{ML_type thm} values: @{ML 0} records only the names of oracles,
   716   @{ML 1} records oracle names and propositions, @{ML 2} additionally
   717   records full proof terms.  Officially named theorems that contribute
   718   to a result are recorded in any case.
   719 
   720   \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given
   721   theorem to a \emph{larger} theory, see also \secref{sec:context}.
   722   This formal adjustment of the background context has no logical
   723   significance, but is occasionally required for formal reasons, e.g.\
   724   when theorems that are imported from more basic theories are used in
   725   the current situation.
   726 
   727   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
   728   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
   729   correspond to the primitive inferences of \figref{fig:prim-rules}.
   730 
   731   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}
   732   corresponds to the @{text "generalize"} rules of
   733   \figref{fig:subst-rules}.  Here collections of type and term
   734   variables are generalized simultaneously, specified by the given
   735   basic names.
   736 
   737   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,
   738   \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules
   739   of \figref{fig:subst-rules}.  Type variables are substituted before
   740   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
   741   refer to the instantiated versions.
   742 
   743   \item @{ML Thm.add_axiom}~@{text "ctxt (name, A)"} declares an
   744   arbitrary proposition as axiom, and retrieves it as a theorem from
   745   the resulting theory, cf.\ @{text "axiom"} in
   746   \figref{fig:prim-rules}.  Note that the low-level representation in
   747   the axiom table may differ slightly from the returned theorem.
   748 
   749   \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named
   750   oracle rule, essentially generating arbitrary axioms on the fly,
   751   cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
   752 
   753   \item @{ML Thm.add_def}~@{text "ctxt unchecked overloaded (name, c
   754   \<^vec>x \<equiv> t)"} states a definitional axiom for an existing constant
   755   @{text "c"}.  Dependencies are recorded via @{ML Theory.add_deps},
   756   unless the @{text "unchecked"} option is set.  Note that the
   757   low-level representation in the axiom table may differ slightly from
   758   the returned theorem.
   759 
   760   \item @{ML Theory.add_deps}~@{text "ctxt name c\<^isub>\<tau> \<^vec>d\<^isub>\<sigma>"}
   761   declares dependencies of a named specification for constant @{text
   762   "c\<^isub>\<tau>"}, relative to existing specifications for constants @{text
   763   "\<^vec>d\<^isub>\<sigma>"}.
   764 
   765   \end{description}
   766 *}
   767 
   768 
   769 text %mlantiq {*
   770   \begin{matharray}{rcl}
   771   @{ML_antiquotation_def "ctyp"} & : & @{text ML_antiquotation} \\
   772   @{ML_antiquotation_def "cterm"} & : & @{text ML_antiquotation} \\
   773   @{ML_antiquotation_def "cprop"} & : & @{text ML_antiquotation} \\
   774   @{ML_antiquotation_def "thm"} & : & @{text ML_antiquotation} \\
   775   @{ML_antiquotation_def "thms"} & : & @{text ML_antiquotation} \\
   776   @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\
   777   \end{matharray}
   778 
   779   @{rail "
   780   @@{ML_antiquotation ctyp} typ
   781   ;
   782   @@{ML_antiquotation cterm} term
   783   ;
   784   @@{ML_antiquotation cprop} prop
   785   ;
   786   @@{ML_antiquotation thm} thmref
   787   ;
   788   @@{ML_antiquotation thms} thmrefs
   789   ;
   790   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \\
   791     @'by' method method?
   792   "}
   793 
   794   \begin{description}
   795 
   796   \item @{text "@{ctyp \<tau>}"} produces a certified type wrt.\ the
   797   current background theory --- as abstract value of type @{ML_type
   798   ctyp}.
   799 
   800   \item @{text "@{cterm t}"} and @{text "@{cprop \<phi>}"} produce a
   801   certified term wrt.\ the current background theory --- as abstract
   802   value of type @{ML_type cterm}.
   803 
   804   \item @{text "@{thm a}"} produces a singleton fact --- as abstract
   805   value of type @{ML_type thm}.
   806 
   807   \item @{text "@{thms a}"} produces a general fact --- as abstract
   808   value of type @{ML_type "thm list"}.
   809 
   810   \item @{text "@{lemma \<phi> by meth}"} produces a fact that is proven on
   811   the spot according to the minimal proof, which imitates a terminal
   812   Isar proof.  The result is an abstract value of type @{ML_type thm}
   813   or @{ML_type "thm list"}, depending on the number of propositions
   814   given here.
   815 
   816   The internal derivation object lacks a proper theorem name, but it
   817   is formally closed, unless the @{text "(open)"} option is specified
   818   (this may impact performance of applications with proof terms).
   819 
   820   Since ML antiquotations are always evaluated at compile-time, there
   821   is no run-time overhead even for non-trivial proofs.  Nonetheless,
   822   the justification is syntactically limited to a single @{command
   823   "by"} step.  More complex Isar proofs should be done in regular
   824   theory source, before compiling the corresponding ML text that uses
   825   the result.
   826 
   827   \end{description}
   828 
   829 *}
   830 
   831 
   832 subsection {* Auxiliary connectives \label{sec:logic-aux} *}
   833 
   834 text {* Theory @{text "Pure"} provides a few auxiliary connectives
   835   that are defined on top of the primitive ones, see
   836   \figref{fig:pure-aux}.  These special constants are useful in
   837   certain internal encodings, and are normally not directly exposed to
   838   the user.
   839 
   840   \begin{figure}[htb]
   841   \begin{center}
   842   \begin{tabular}{ll}
   843   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&&&"}) \\
   844   @{text "\<turnstile> A &&& B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
   845   @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\
   846   @{text "#A \<equiv> A"} \\[1ex]
   847   @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
   848   @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
   849   @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
   850   @{text "(unspecified)"} \\
   851   \end{tabular}
   852   \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   853   \end{center}
   854   \end{figure}
   855 
   856   The introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &&& B"}, and eliminations
   857   (projections) @{text "A &&& B \<Longrightarrow> A"} and @{text "A &&& B \<Longrightarrow> B"} are
   858   available as derived rules.  Conjunction allows to treat
   859   simultaneous assumptions and conclusions uniformly, e.g.\ consider
   860   @{text "A \<Longrightarrow> B \<Longrightarrow> C &&& D"}.  In particular, the goal mechanism
   861   represents multiple claims as explicit conjunction internally, but
   862   this is refined (via backwards introduction) into separate sub-goals
   863   before the user commences the proof; the final result is projected
   864   into a list of theorems using eliminations (cf.\
   865   \secref{sec:tactical-goals}).
   866 
   867   The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex
   868   propositions appear as atomic, without changing the meaning: @{text
   869   "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable.  See
   870   \secref{sec:tactical-goals} for specific operations.
   871 
   872   The @{text "term"} marker turns any well-typed term into a derivable
   873   proposition: @{text "\<turnstile> TERM t"} holds unconditionally.  Although
   874   this is logically vacuous, it allows to treat terms and proofs
   875   uniformly, similar to a type-theoretic framework.
   876 
   877   The @{text "TYPE"} constructor is the canonical representative of
   878   the unspecified type @{text "\<alpha> itself"}; it essentially injects the
   879   language of types into that of terms.  There is specific notation
   880   @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
   881  itself\<^esub>"}.
   882   Although being devoid of any particular meaning, the term @{text
   883   "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term
   884   language.  In particular, @{text "TYPE(\<alpha>)"} may be used as formal
   885   argument in primitive definitions, in order to circumvent hidden
   886   polymorphism (cf.\ \secref{sec:terms}).  For example, @{text "c
   887   TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of
   888   a proposition @{text "A"} that depends on an additional type
   889   argument, which is essentially a predicate on types.
   890 *}
   891 
   892 text %mlref {*
   893   \begin{mldecls}
   894   @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
   895   @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
   896   @{index_ML Drule.mk_term: "cterm -> thm"} \\
   897   @{index_ML Drule.dest_term: "thm -> cterm"} \\
   898   @{index_ML Logic.mk_type: "typ -> term"} \\
   899   @{index_ML Logic.dest_type: "term -> typ"} \\
   900   \end{mldecls}
   901 
   902   \begin{description}
   903 
   904   \item @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text
   905   "A"} and @{text "B"}.
   906 
   907   \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}
   908   from @{text "A &&& B"}.
   909 
   910   \item @{ML Drule.mk_term} derives @{text "TERM t"}.
   911 
   912   \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text
   913   "TERM t"}.
   914 
   915   \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text
   916   "TYPE(\<tau>)"}.
   917 
   918   \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type
   919   @{text "\<tau>"}.
   920 
   921   \end{description}
   922 *}
   923 
   924 
   925 section {* Object-level rules \label{sec:obj-rules} *}
   926 
   927 text {*
   928   The primitive inferences covered so far mostly serve foundational
   929   purposes.  User-level reasoning usually works via object-level rules
   930   that are represented as theorems of Pure.  Composition of rules
   931   involves \emph{backchaining}, \emph{higher-order unification} modulo
   932   @{text "\<alpha>\<beta>\<eta>"}-conversion of @{text "\<lambda>"}-terms, and so-called
   933   \emph{lifting} of rules into a context of @{text "\<And>"} and @{text
   934   "\<Longrightarrow>"} connectives.  Thus the full power of higher-order Natural
   935   Deduction in Isabelle/Pure becomes readily available.
   936 *}
   937 
   938 
   939 subsection {* Hereditary Harrop Formulae *}
   940 
   941 text {*
   942   The idea of object-level rules is to model Natural Deduction
   943   inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow
   944   arbitrary nesting similar to \cite{extensions91}.  The most basic
   945   rule format is that of a \emph{Horn Clause}:
   946   \[
   947   \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}
   948   \]
   949   where @{text "A, A\<^sub>1, \<dots>, A\<^sub>n"} are atomic propositions
   950   of the framework, usually of the form @{text "Trueprop B"}, where
   951   @{text "B"} is a (compound) object-level statement.  This
   952   object-level inference corresponds to an iterated implication in
   953   Pure like this:
   954   \[
   955   @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}
   956   \]
   957   As an example consider conjunction introduction: @{text "A \<Longrightarrow> B \<Longrightarrow> A \<and>
   958   B"}.  Any parameters occurring in such rule statements are
   959   conceptionally treated as arbitrary:
   960   \[
   961   @{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"}
   962   \]
   963 
   964   Nesting of rules means that the positions of @{text "A\<^sub>i"} may
   965   again hold compound rules, not just atomic propositions.
   966   Propositions of this format are called \emph{Hereditary Harrop
   967   Formulae} in the literature \cite{Miller:1991}.  Here we give an
   968   inductive characterization as follows:
   969 
   970   \medskip
   971   \begin{tabular}{ll}
   972   @{text "\<^bold>x"} & set of variables \\
   973   @{text "\<^bold>A"} & set of atomic propositions \\
   974   @{text "\<^bold>H  =  \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\
   975   \end{tabular}
   976   \medskip
   977 
   978   Thus we essentially impose nesting levels on propositions formed
   979   from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a prefix
   980   of parameters and compound premises, concluding an atomic
   981   proposition.  Typical examples are @{text "\<longrightarrow>"}-introduction @{text
   982   "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n
   983   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}.  Even deeper nesting occurs in well-founded
   984   induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this
   985   already marks the limit of rule complexity that is usually seen in
   986   practice.
   987 
   988   \medskip Regular user-level inferences in Isabelle/Pure always
   989   maintain the following canonical form of results:
   990 
   991   \begin{itemize}
   992 
   993   \item Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"},
   994   which is a theorem of Pure, means that quantifiers are pushed in
   995   front of implication at each level of nesting.  The normal form is a
   996   Hereditary Harrop Formula.
   997 
   998   \item The outermost prefix of parameters is represented via
   999   schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x
  1000   \<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.
  1001   Note that this representation looses information about the order of
  1002   parameters, and vacuous quantifiers vanish automatically.
  1003 
  1004   \end{itemize}
  1005 *}
  1006 
  1007 text %mlref {*
  1008   \begin{mldecls}
  1009   @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\
  1010   \end{mldecls}
  1011 
  1012   \begin{description}
  1013 
  1014   \item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given
  1015   theorem according to the canonical form specified above.  This is
  1016   occasionally helpful to repair some low-level tools that do not
  1017   handle Hereditary Harrop Formulae properly.
  1018 
  1019   \end{description}
  1020 *}
  1021 
  1022 
  1023 subsection {* Rule composition *}
  1024 
  1025 text {*
  1026   The rule calculus of Isabelle/Pure provides two main inferences:
  1027   @{inference resolution} (i.e.\ back-chaining of rules) and
  1028   @{inference assumption} (i.e.\ closing a branch), both modulo
  1029   higher-order unification.  There are also combined variants, notably
  1030   @{inference elim_resolution} and @{inference dest_resolution}.
  1031 
  1032   To understand the all-important @{inference resolution} principle,
  1033   we first consider raw @{inference_def composition} (modulo
  1034   higher-order unification with substitution @{text "\<vartheta>"}):
  1035   \[
  1036   \infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}
  1037   {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}
  1038   \]
  1039   Here the conclusion of the first rule is unified with the premise of
  1040   the second; the resulting rule instance inherits the premises of the
  1041   first and conclusion of the second.  Note that @{text "C"} can again
  1042   consist of iterated implications.  We can also permute the premises
  1043   of the second rule back-and-forth in order to compose with @{text
  1044   "B'"} in any position (subsequently we shall always refer to
  1045   position 1 w.l.o.g.).
  1046 
  1047   In @{inference composition} the internal structure of the common
  1048   part @{text "B"} and @{text "B'"} is not taken into account.  For
  1049   proper @{inference resolution} we require @{text "B"} to be atomic,
  1050   and explicitly observe the structure @{text "\<And>\<^vec>x. \<^vec>H
  1051   \<^vec>x \<Longrightarrow> B' \<^vec>x"} of the premise of the second rule.  The
  1052   idea is to adapt the first rule by ``lifting'' it into this context,
  1053   by means of iterated application of the following inferences:
  1054   \[
  1055   \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}
  1056   \]
  1057   \[
  1058   \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"}}
  1059   \]
  1060   By combining raw composition with lifting, we get full @{inference
  1061   resolution} as follows:
  1062   \[
  1063   \infer[(@{inference_def resolution})]
  1064   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
  1065   {\begin{tabular}{l}
  1066     @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\
  1067     @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
  1068     @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
  1069    \end{tabular}}
  1070   \]
  1071 
  1072   Continued resolution of rules allows to back-chain a problem towards
  1073   more and sub-problems.  Branches are closed either by resolving with
  1074   a rule of 0 premises, or by producing a ``short-circuit'' within a
  1075   solved situation (again modulo unification):
  1076   \[
  1077   \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}
  1078   {@{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})}}
  1079   \]
  1080 
  1081   FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
  1082 *}
  1083 
  1084 text %mlref {*
  1085   \begin{mldecls}
  1086   @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\
  1087   @{index_ML_op "RS": "thm * thm -> thm"} \\
  1088 
  1089   @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\
  1090   @{index_ML_op "RL": "thm list * thm list -> thm list"} \\
  1091 
  1092   @{index_ML_op "MRS": "thm list * thm -> thm"} \\
  1093   @{index_ML_op "OF": "thm * thm list -> thm"} \\
  1094   \end{mldecls}
  1095 
  1096   \begin{description}
  1097 
  1098   \item @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of
  1099   @{text "rule\<^sub>1"} with the @{text i}-th premise of @{text "rule\<^sub>2"},
  1100   according to the @{inference resolution} principle explained above.
  1101   Unless there is precisely one resolvent it raises exception @{ML
  1102   THM}.
  1103 
  1104   This corresponds to the rule attribute @{attribute THEN} in Isar
  1105   source language.
  1106 
  1107   \item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RS (1,
  1108   rule\<^sub>2)"}.
  1109 
  1110   \item @{text "rules\<^sub>1 RLN (i, rules\<^sub>2)"} joins lists of rules.  For
  1111   every @{text "rule\<^sub>1"} in @{text "rules\<^sub>1"} and @{text "rule\<^sub>2"} in
  1112   @{text "rules\<^sub>2"}, it resolves the conclusion of @{text "rule\<^sub>1"} with
  1113   the @{text "i"}-th premise of @{text "rule\<^sub>2"}, accumulating multiple
  1114   results in one big list.  Note that such strict enumerations of
  1115   higher-order unifications can be inefficient compared to the lazy
  1116   variant seen in elementary tactics like @{ML resolve_tac}.
  1117 
  1118   \item @{text "rules\<^sub>1 RL rules\<^sub>2"} abbreviates @{text "rules\<^sub>1 RLN (1,
  1119   rules\<^sub>2)"}.
  1120 
  1121   \item @{text "[rule\<^sub>1, \<dots>, rule\<^sub>n] MRS rule"} resolves @{text "rule\<^isub>i"}
  1122   against premise @{text "i"} of @{text "rule"}, for @{text "i = n, \<dots>,
  1123   1"}.  By working from right to left, newly emerging premises are
  1124   concatenated in the result, without interfering.
  1125 
  1126   \item @{text "rule OF rules"} is an alternative notation for @{text
  1127   "rules MRS rule"}, which makes rule composition look more like
  1128   function application.  Note that the argument @{text "rules"} need
  1129   not be atomic.
  1130 
  1131   This corresponds to the rule attribute @{attribute OF} in Isar
  1132   source language.
  1133 
  1134   \end{description}
  1135 *}
  1136 
  1137 end