src/Doc/Implementation/Logic.thy
 author wenzelm Wed Dec 06 15:46:35 2017 +0100 (18 months ago) changeset 67146 909dcdec2122 parent 65446 ed18feb34c07 child 68540 000a0e062529 permissions -rw-r--r--
more embedded cartouche arguments;
more uniform LaTeX output for control symbols;
     1 (*:maxLineLen=78:*)

     2

     3 theory Logic

     4 imports Base

     5 begin

     6

     7 chapter \<open>Primitive logic \label{ch:logic}\<close>

     8

     9 text \<open>

    10   The logical foundations of Isabelle/Isar are that of the Pure logic, which

    11   has been introduced as a Natural Deduction framework in @{cite paulson700}.

    12   This is essentially the same logic as \<open>\<lambda>HOL\<close>'' in the more abstract

    13   setting of Pure Type Systems (PTS) @{cite "Barendregt-Geuvers:2001"},

    14   although there are some key differences in the specific treatment of simple

    15   types in Isabelle/Pure.

    16

    17   Following type-theoretic parlance, the Pure logic consists of three levels

    18   of \<open>\<lambda>\<close>-calculus with corresponding arrows, \<open>\<Rightarrow>\<close> for syntactic function space

    19   (terms depending on terms), \<open>\<And>\<close> for universal quantification (proofs

    20   depending on terms), and \<open>\<Longrightarrow>\<close> for implication (proofs depending on proofs).

    21

    22   Derivations are relative to a logical theory, which declares type

    23   constructors, constants, and axioms. Theory declarations support schematic

    24   polymorphism, which is strictly speaking outside the logic.\<^footnote>\<open>This is the

    25   deeper logical reason, why the theory context \<open>\<Theta>\<close> is separate from the proof

    26   context \<open>\<Gamma>\<close> of the core calculus: type constructors, term constants, and

    27   facts (proof constants) may involve arbitrary type schemes, but the type of

    28   a locally fixed term parameter is also fixed!\<close>

    29 \<close>

    30

    31

    32 section \<open>Types \label{sec:types}\<close>

    33

    34 text \<open>

    35   The language of types is an uninterpreted order-sorted first-order algebra;

    36   types are qualified by ordered type classes.

    37

    38   \<^medskip>

    39   A \<^emph>\<open>type class\<close> is an abstract syntactic entity declared in the theory

    40   context. The \<^emph>\<open>subclass relation\<close> \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close> is specified by stating an

    41   acyclic generating relation; the transitive closure is maintained

    42   internally. The resulting relation is an ordering: reflexive, transitive,

    43   and antisymmetric.

    44

    45   A \<^emph>\<open>sort\<close> is a list of type classes written as \<open>s = {c\<^sub>1, \<dots>, c\<^sub>m}\<close>, it

    46   represents symbolic intersection. Notationally, the curly braces are omitted

    47   for singleton intersections, i.e.\ any class \<open>c\<close> may be read as a sort

    48   \<open>{c}\<close>. The ordering on type classes is extended to sorts according to the

    49   meaning of intersections: \<open>{c\<^sub>1, \<dots> c\<^sub>m} \<subseteq> {d\<^sub>1, \<dots>, d\<^sub>n}\<close> iff \<open>\<forall>j. \<exists>i. c\<^sub>i \<subseteq>

    50   d\<^sub>j\<close>. The empty intersection \<open>{}\<close> refers to the universal sort, which is the

    51   largest element wrt.\ the sort order. Thus \<open>{}\<close> represents the full

    52   sort'', not the empty one! The intersection of all (finitely many) classes

    53   declared in the current theory is the least element wrt.\ the sort ordering.

    54

    55   \<^medskip>

    56   A \<^emph>\<open>fixed type variable\<close> is a pair of a basic name (starting with a \<open>'\<close>

    57   character) and a sort constraint, e.g.\ \<open>('a, s)\<close> which is usually printed

    58   as \<open>\<alpha>\<^sub>s\<close>. A \<^emph>\<open>schematic type variable\<close> is a pair of an indexname and a sort

    59   constraint, e.g.\ \<open>(('a, 0), s)\<close> which is usually printed as \<open>?\<alpha>\<^sub>s\<close>.

    60

    61   Note that \<^emph>\<open>all\<close> syntactic components contribute to the identity of type

    62   variables: basic name, index, and sort constraint. The core logic handles

    63   type variables with the same name but different sorts as different, although

    64   the type-inference layer (which is outside the core) rejects anything like

    65   that.

    66

    67   A \<^emph>\<open>type constructor\<close> \<open>\<kappa>\<close> is a \<open>k\<close>-ary operator on types declared in the

    68   theory. Type constructor application is written postfix as \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>k)\<kappa>\<close>.

    69   For \<open>k = 0\<close> the argument tuple is omitted, e.g.\ \<open>prop\<close> instead of \<open>()prop\<close>.

    70   For \<open>k = 1\<close> the parentheses are omitted, e.g.\ \<open>\<alpha> list\<close> instead of

    71   \<open>(\<alpha>)list\<close>. Further notation is provided for specific constructors, notably

    72   the right-associative infix \<open>\<alpha> \<Rightarrow> \<beta>\<close> instead of \<open>(\<alpha>, \<beta>)fun\<close>.

    73

    74   The logical category \<^emph>\<open>type\<close> is defined inductively over type variables and

    75   type constructors as follows: \<open>\<tau> = \<alpha>\<^sub>s | ?\<alpha>\<^sub>s | (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>\<close>.

    76

    77   A \<^emph>\<open>type abbreviation\<close> is a syntactic definition \<open>(\<^vec>\<alpha>)\<kappa> = \<tau>\<close> of an

    78   arbitrary type expression \<open>\<tau>\<close> over variables \<open>\<^vec>\<alpha>\<close>. Type abbreviations

    79   appear as type constructors in the syntax, but are expanded before entering

    80   the logical core.

    81

    82   A \<^emph>\<open>type arity\<close> declares the image behavior of a type constructor wrt.\ the

    83   algebra of sorts: \<open>\<kappa> :: (s\<^sub>1, \<dots>, s\<^sub>k)s\<close> means that \<open>(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>\<close> is of

    84   sort \<open>s\<close> if every argument type \<open>\<tau>\<^sub>i\<close> is of sort \<open>s\<^sub>i\<close>. Arity declarations

    85   are implicitly completed, i.e.\ \<open>\<kappa> :: (\<^vec>s)c\<close> entails \<open>\<kappa> ::

    86   (\<^vec>s)c'\<close> for any \<open>c' \<supseteq> c\<close>.

    87

    88   \<^medskip>

    89   The sort algebra is always maintained as \<^emph>\<open>coregular\<close>, which means that type

    90   arities are consistent with the subclass relation: for any type constructor

    91   \<open>\<kappa>\<close>, and classes \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close>, and arities \<open>\<kappa> :: (\<^vec>s\<^sub>1)c\<^sub>1\<close> and \<open>\<kappa> ::

    92   (\<^vec>s\<^sub>2)c\<^sub>2\<close> holds \<open>\<^vec>s\<^sub>1 \<subseteq> \<^vec>s\<^sub>2\<close> component-wise.

    93

    94   The key property of a coregular order-sorted algebra is that sort

    95   constraints can be solved in a most general fashion: for each type

    96   constructor \<open>\<kappa>\<close> and sort \<open>s\<close> there is a most general vector of argument

    97   sorts \<open>(s\<^sub>1, \<dots>, s\<^sub>k)\<close> such that a type scheme \<open>(\<alpha>\<^bsub>s\<^sub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^sub>k\<^esub>)\<kappa>\<close> is of

    98   sort \<open>s\<close>. Consequently, type unification has most general solutions (modulo

    99   equivalence of sorts), so type-inference produces primary types as expected

   100   @{cite "nipkow-prehofer"}.

   101 \<close>

   102

   103 text %mlref \<open>

   104   \begin{mldecls}

   105   @{index_ML_type class: string} \\

   106   @{index_ML_type sort: "class list"} \\

   107   @{index_ML_type arity: "string * sort list * sort"} \\

   108   @{index_ML_type typ} \\

   109   @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\

   110   @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\

   111   \end{mldecls}

   112   \begin{mldecls}

   113   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\

   114   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\

   115   @{index_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\

   116   @{index_ML Sign.add_type_abbrev: "Proof.context ->

   117   binding * string list * typ -> theory -> theory"} \\

   118   @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\

   119   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\

   120   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\

   121   \end{mldecls}

   122

   123   \<^descr> Type @{ML_type class} represents type classes.

   124

   125   \<^descr> Type @{ML_type sort} represents sorts, i.e.\ finite intersections of

   126   classes. The empty list @{ML "[]: sort"} refers to the empty class

   127   intersection, i.e.\ the full sort''.

   128

   129   \<^descr> Type @{ML_type arity} represents type arities. A triple \<open>(\<kappa>, \<^vec>s, s)

   130   : arity\<close> represents \<open>\<kappa> :: (\<^vec>s)s\<close> as described above.

   131

   132   \<^descr> Type @{ML_type typ} represents types; this is a datatype with constructors

   133   @{ML TFree}, @{ML TVar}, @{ML Type}.

   134

   135   \<^descr> @{ML Term.map_atyps}~\<open>f \<tau>\<close> applies the mapping \<open>f\<close> to all atomic types

   136   (@{ML TFree}, @{ML TVar}) occurring in \<open>\<tau>\<close>.

   137

   138   \<^descr> @{ML Term.fold_atyps}~\<open>f \<tau>\<close> iterates the operation \<open>f\<close> over all

   139   occurrences of atomic types (@{ML TFree}, @{ML TVar}) in \<open>\<tau>\<close>; the type

   140   structure is traversed from left to right.

   141

   142   \<^descr> @{ML Sign.subsort}~\<open>thy (s\<^sub>1, s\<^sub>2)\<close> tests the subsort relation \<open>s\<^sub>1 \<subseteq>

   143   s\<^sub>2\<close>.

   144

   145   \<^descr> @{ML Sign.of_sort}~\<open>thy (\<tau>, s)\<close> tests whether type \<open>\<tau>\<close> is of sort \<open>s\<close>.

   146

   147   \<^descr> @{ML Sign.add_type}~\<open>ctxt (\<kappa>, k, mx)\<close> declares a new type constructors \<open>\<kappa>\<close>

   148   with \<open>k\<close> arguments and optional mixfix syntax.

   149

   150   \<^descr> @{ML Sign.add_type_abbrev}~\<open>ctxt (\<kappa>, \<^vec>\<alpha>, \<tau>)\<close> defines a new type

   151   abbreviation \<open>(\<^vec>\<alpha>)\<kappa> = \<tau>\<close>.

   152

   153   \<^descr> @{ML Sign.primitive_class}~\<open>(c, [c\<^sub>1, \<dots>, c\<^sub>n])\<close> declares a new class \<open>c\<close>,

   154   together with class relations \<open>c \<subseteq> c\<^sub>i\<close>, for \<open>i = 1, \<dots>, n\<close>.

   155

   156   \<^descr> @{ML Sign.primitive_classrel}~\<open>(c\<^sub>1, c\<^sub>2)\<close> declares the class relation

   157   \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close>.

   158

   159   \<^descr> @{ML Sign.primitive_arity}~\<open>(\<kappa>, \<^vec>s, s)\<close> declares the arity \<open>\<kappa> ::

   160   (\<^vec>s)s\<close>.

   161 \<close>

   162

   163 text %mlantiq \<open>

   164   \begin{matharray}{rcl}

   165   @{ML_antiquotation_def "class"} & : & \<open>ML_antiquotation\<close> \\

   166   @{ML_antiquotation_def "sort"} & : & \<open>ML_antiquotation\<close> \\

   167   @{ML_antiquotation_def "type_name"} & : & \<open>ML_antiquotation\<close> \\

   168   @{ML_antiquotation_def "type_abbrev"} & : & \<open>ML_antiquotation\<close> \\

   169   @{ML_antiquotation_def "nonterminal"} & : & \<open>ML_antiquotation\<close> \\

   170   @{ML_antiquotation_def "typ"} & : & \<open>ML_antiquotation\<close> \\

   171   \end{matharray}

   172

   173   @{rail \<open>

   174   @@{ML_antiquotation class} embedded

   175   ;

   176   @@{ML_antiquotation sort} sort

   177   ;

   178   (@@{ML_antiquotation type_name} |

   179    @@{ML_antiquotation type_abbrev} |

   180    @@{ML_antiquotation nonterminal}) embedded

   181   ;

   182   @@{ML_antiquotation typ} type

   183   \<close>}

   184

   185   \<^descr> \<open>@{class c}\<close> inlines the internalized class \<open>c\<close> --- as @{ML_type string}

   186   literal.

   187

   188   \<^descr> \<open>@{sort s}\<close> inlines the internalized sort \<open>s\<close> --- as @{ML_type "string

   189   list"} literal.

   190

   191   \<^descr> \<open>@{type_name c}\<close> inlines the internalized type constructor \<open>c\<close> --- as

   192   @{ML_type string} literal.

   193

   194   \<^descr> \<open>@{type_abbrev c}\<close> inlines the internalized type abbreviation \<open>c\<close> --- as

   195   @{ML_type string} literal.

   196

   197   \<^descr> \<open>@{nonterminal c}\<close> inlines the internalized syntactic type~/ grammar

   198   nonterminal \<open>c\<close> --- as @{ML_type string} literal.

   199

   200   \<^descr> \<open>@{typ \<tau>}\<close> inlines the internalized type \<open>\<tau>\<close> --- as constructor term for

   201   datatype @{ML_type typ}.

   202 \<close>

   203

   204

   205 section \<open>Terms \label{sec:terms}\<close>

   206

   207 text \<open>

   208   The language of terms is that of simply-typed \<open>\<lambda>\<close>-calculus with de-Bruijn

   209   indices for bound variables (cf.\ @{cite debruijn72} or @{cite

   210   "paulson-ml2"}), with the types being determined by the corresponding

   211   binders. In contrast, free variables and constants have an explicit name and

   212   type in each occurrence.

   213

   214   \<^medskip>

   215   A \<^emph>\<open>bound variable\<close> is a natural number \<open>b\<close>, which accounts for the number

   216   of intermediate binders between the variable occurrence in the body and its

   217   binding position. For example, the de-Bruijn term \<open>\<lambda>\<^bsub>bool\<^esub>. \<lambda>\<^bsub>bool\<^esub>. 1 \<and> 0\<close>

   218   would correspond to \<open>\<lambda>x\<^bsub>bool\<^esub>. \<lambda>y\<^bsub>bool\<^esub>. x \<and> y\<close> in a named representation.

   219   Note that a bound variable may be represented by different de-Bruijn indices

   220   at different occurrences, depending on the nesting of abstractions.

   221

   222   A \<^emph>\<open>loose variable\<close> is a bound variable that is outside the scope of local

   223   binders. The types (and names) for loose variables can be managed as a

   224   separate context, that is maintained as a stack of hypothetical binders. The

   225   core logic operates on closed terms, without any loose variables.

   226

   227   A \<^emph>\<open>fixed variable\<close> is a pair of a basic name and a type, e.g.\ \<open>(x, \<tau>)\<close>

   228   which is usually printed \<open>x\<^sub>\<tau>\<close> here. A \<^emph>\<open>schematic variable\<close> is a pair of an

   229   indexname and a type, e.g.\ \<open>((x, 0), \<tau>)\<close> which is likewise printed as

   230   \<open>?x\<^sub>\<tau>\<close>.

   231

   232   \<^medskip>

   233   A \<^emph>\<open>constant\<close> is a pair of a basic name and a type, e.g.\ \<open>(c, \<tau>)\<close> which is

   234   usually printed as \<open>c\<^sub>\<tau>\<close> here. Constants are declared in the context as

   235   polymorphic families \<open>c :: \<sigma>\<close>, meaning that all substitution instances \<open>c\<^sub>\<tau>\<close>

   236   for \<open>\<tau> = \<sigma>\<vartheta>\<close> are valid.

   237

   238   The vector of \<^emph>\<open>type arguments\<close> of constant \<open>c\<^sub>\<tau>\<close> wrt.\ the declaration \<open>c

   239   :: \<sigma>\<close> is defined as the codomain of the matcher \<open>\<vartheta> = {?\<alpha>\<^sub>1 \<mapsto> \<tau>\<^sub>1,

   240   \<dots>, ?\<alpha>\<^sub>n \<mapsto> \<tau>\<^sub>n}\<close> presented in canonical order \<open>(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n)\<close>, corresponding

   241   to the left-to-right occurrences of the \<open>\<alpha>\<^sub>i\<close> in \<open>\<sigma>\<close>. Within a given theory

   242   context, there is a one-to-one correspondence between any constant \<open>c\<^sub>\<tau>\<close> and

   243   the application \<open>c(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n)\<close> of its type arguments. For example, with

   244   \<open>plus :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>\<close>, the instance \<open>plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>\<close> corresponds to

   245   \<open>plus(nat)\<close>.

   246

   247   Constant declarations \<open>c :: \<sigma>\<close> may contain sort constraints for type

   248   variables in \<open>\<sigma>\<close>. These are observed by type-inference as expected, but

   249   \<^emph>\<open>ignored\<close> by the core logic. This means the primitive logic is able to

   250   reason with instances of polymorphic constants that the user-level

   251   type-checker would reject due to violation of type class restrictions.

   252

   253   \<^medskip>

   254   An \<^emph>\<open>atomic term\<close> is either a variable or constant. The logical category

   255   \<^emph>\<open>term\<close> is defined inductively over atomic terms, with abstraction and

   256   application as follows: \<open>t = b | x\<^sub>\<tau> | ?x\<^sub>\<tau> | c\<^sub>\<tau> | \<lambda>\<^sub>\<tau>. t | t\<^sub>1 t\<^sub>2\<close>.

   257   Parsing and printing takes care of converting between an external

   258   representation with named bound variables. Subsequently, we shall use the

   259   latter notation instead of internal de-Bruijn representation.

   260

   261   The inductive relation \<open>t :: \<tau>\<close> assigns a (unique) type to a term according

   262   to the structure of atomic terms, abstractions, and applications:

   263   $  264 \infer{\<open>a\<^sub>\<tau> :: \<tau>\<close>}{}   265 \qquad   266 \infer{\<open>(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>\<close>}{\<open>t :: \<sigma>\<close>}   267 \qquad   268 \infer{\<open>t u :: \<sigma>\<close>}{\<open>t :: \<tau> \<Rightarrow> \<sigma>\<close> & \<open>u :: \<tau>\<close>}   269$

   270   A \<^emph>\<open>well-typed term\<close> is a term that can be typed according to these rules.

   271

   272   Typing information can be omitted: type-inference is able to reconstruct the

   273   most general type of a raw term, while assigning most general types to all

   274   of its variables and constants. Type-inference depends on a context of type

   275   constraints for fixed variables, and declarations for polymorphic constants.

   276

   277   The identity of atomic terms consists both of the name and the type

   278   component. This means that different variables \<open>x\<^bsub>\<tau>\<^sub>1\<^esub>\<close> and \<open>x\<^bsub>\<tau>\<^sub>2\<^esub>\<close> may

   279   become the same after type instantiation. Type-inference rejects variables

   280   of the same name, but different types. In contrast, mixed instances of

   281   polymorphic constants occur routinely.

   282

   283   \<^medskip>

   284   The \<^emph>\<open>hidden polymorphism\<close> of a term \<open>t :: \<sigma>\<close> is the set of type variables

   285   occurring in \<open>t\<close>, but not in its type \<open>\<sigma>\<close>. This means that the term

   286   implicitly depends on type arguments that are not accounted in the result

   287   type, i.e.\ there are different type instances \<open>t\<vartheta> :: \<sigma>\<close> and

   288   \<open>t\<vartheta>' :: \<sigma>\<close> with the same type. This slightly pathological

   289   situation notoriously demands additional care.

   290

   291   \<^medskip>

   292   A \<^emph>\<open>term abbreviation\<close> is a syntactic definition \<open>c\<^sub>\<sigma> \<equiv> t\<close> of a closed term

   293   \<open>t\<close> of type \<open>\<sigma>\<close>, without any hidden polymorphism. A term abbreviation looks

   294   like a constant in the syntax, but is expanded before entering the logical

   295   core. Abbreviations are usually reverted when printing terms, using \<open>t \<rightarrow>

   296   c\<^sub>\<sigma>\<close> as rules for higher-order rewriting.

   297

   298   \<^medskip>

   299   Canonical operations on \<open>\<lambda>\<close>-terms include \<open>\<alpha>\<beta>\<eta>\<close>-conversion: \<open>\<alpha>\<close>-conversion

   300   refers to capture-free renaming of bound variables; \<open>\<beta>\<close>-conversion contracts

   301   an abstraction applied to an argument term, substituting the argument in the

   302   body: \<open>(\<lambda>x. b)a\<close> becomes \<open>b[a/x]\<close>; \<open>\<eta>\<close>-conversion contracts vacuous

   303   application-abstraction: \<open>\<lambda>x. f x\<close> becomes \<open>f\<close>, provided that the bound

   304   variable does not occur in \<open>f\<close>.

   305

   306   Terms are normally treated modulo \<open>\<alpha>\<close>-conversion, which is implicit in the

   307   de-Bruijn representation. Names for bound variables in abstractions are

   308   maintained separately as (meaningless) comments, mostly for parsing and

   309   printing. Full \<open>\<alpha>\<beta>\<eta>\<close>-conversion is commonplace in various standard

   310   operations (\secref{sec:obj-rules}) that are based on higher-order

   311   unification and matching.

   312 \<close>

   313

   314 text %mlref \<open>

   315   \begin{mldecls}

   316   @{index_ML_type term} \\

   317   @{index_ML_op "aconv": "term * term -> bool"} \\

   318   @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\

   319   @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\

   320   @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\

   321   @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\

   322   \end{mldecls}

   323   \begin{mldecls}

   324   @{index_ML fastype_of: "term -> typ"} \\

   325   @{index_ML lambda: "term -> term -> term"} \\

   326   @{index_ML betapply: "term * term -> term"} \\

   327   @{index_ML incr_boundvars: "int -> term -> term"} \\

   328   @{index_ML Sign.declare_const: "Proof.context ->

   329   (binding * typ) * mixfix -> theory -> term * theory"} \\

   330   @{index_ML Sign.add_abbrev: "string -> binding * term ->

   331   theory -> (term * term) * theory"} \\

   332   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\

   333   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\

   334   \end{mldecls}

   335

   336   \<^descr> Type @{ML_type term} represents de-Bruijn terms, with comments in

   337   abstractions, and explicitly named free variables and constants; this is a

   338   datatype with constructors @{index_ML Bound}, @{index_ML Free}, @{index_ML

   339   Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_op "$"}.   340   341 \<^descr> \<open>t\<close>~@{ML_text aconv}~\<open>u\<close> checks \<open>\<alpha>\<close>-equivalence of two terms. This is the   342 basic equality relation on type @{ML_type term}; raw datatype equality   343 should only be used for operations related to parsing or printing!   344   345 \<^descr> @{ML Term.map_types}~\<open>f t\<close> applies the mapping \<open>f\<close> to all types occurring   346 in \<open>t\<close>.   347   348 \<^descr> @{ML Term.fold_types}~\<open>f t\<close> iterates the operation \<open>f\<close> over all   349 occurrences of types in \<open>t\<close>; the term structure is traversed from left to   350 right.   351   352 \<^descr> @{ML Term.map_aterms}~\<open>f t\<close> applies the mapping \<open>f\<close> to all atomic terms   353 (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}) occurring in \<open>t\<close>.   354   355 \<^descr> @{ML Term.fold_aterms}~\<open>f t\<close> iterates the operation \<open>f\<close> over all   356 occurrences of atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML   357 Const}) in \<open>t\<close>; the term structure is traversed from left to right.   358   359 \<^descr> @{ML fastype_of}~\<open>t\<close> determines the type of a well-typed term. This   360 operation is relatively slow, despite the omission of any sanity checks.   361   362 \<^descr> @{ML lambda}~\<open>a b\<close> produces an abstraction \<open>\<lambda>a. b\<close>, where occurrences of   363 the atomic term \<open>a\<close> in the body \<open>b\<close> are replaced by bound variables.   364   365 \<^descr> @{ML betapply}~\<open>(t, u)\<close> produces an application \<open>t u\<close>, with topmost   366 \<open>\<beta>\<close>-conversion if \<open>t\<close> is an abstraction.   367   368 \<^descr> @{ML incr_boundvars}~\<open>j\<close> increments a term's dangling bound variables by   369 the offset \<open>j\<close>. This is required when moving a subterm into a context where   370 it is enclosed by a different number of abstractions. Bound variables with a   371 matching abstraction are unaffected.   372   373 \<^descr> @{ML Sign.declare_const}~\<open>ctxt ((c, \<sigma>), mx)\<close> declares a new constant \<open>c ::   374 \<sigma>\<close> with optional mixfix syntax.   375   376 \<^descr> @{ML Sign.add_abbrev}~\<open>print_mode (c, t)\<close> introduces a new term   377 abbreviation \<open>c \<equiv> t\<close>.   378   379 \<^descr> @{ML Sign.const_typargs}~\<open>thy (c, \<tau>)\<close> and @{ML Sign.const_instance}~\<open>thy   380 (c, [\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n])\<close> convert between two representations of polymorphic   381 constants: full type instance vs.\ compact type arguments form.   382 \<close>   383   384 text %mlantiq \<open>   385 \begin{matharray}{rcl}   386 @{ML_antiquotation_def "const_name"} & : & \<open>ML_antiquotation\<close> \\   387 @{ML_antiquotation_def "const_abbrev"} & : & \<open>ML_antiquotation\<close> \\   388 @{ML_antiquotation_def "const"} & : & \<open>ML_antiquotation\<close> \\   389 @{ML_antiquotation_def "term"} & : & \<open>ML_antiquotation\<close> \\   390 @{ML_antiquotation_def "prop"} & : & \<open>ML_antiquotation\<close> \\   391 \end{matharray}   392   393 @{rail \<open>   394 (@@{ML_antiquotation const_name} |   395 @@{ML_antiquotation const_abbrev}) embedded   396 ;   397 @@{ML_antiquotation const} ('(' (type + ',') ')')?   398 ;   399 @@{ML_antiquotation term} term   400 ;   401 @@{ML_antiquotation prop} prop   402 \<close>}   403   404 \<^descr> \<open>@{const_name c}\<close> inlines the internalized logical constant name \<open>c\<close> ---   405 as @{ML_type string} literal.   406   407 \<^descr> \<open>@{const_abbrev c}\<close> inlines the internalized abbreviated constant name \<open>c\<close>   408 --- as @{ML_type string} literal.   409   410 \<^descr> \<open>@{const c(\<^vec>\<tau>)}\<close> inlines the internalized constant \<open>c\<close> with precise   411 type instantiation in the sense of @{ML Sign.const_instance} --- as @{ML   412 Const} constructor term for datatype @{ML_type term}.   413   414 \<^descr> \<open>@{term t}\<close> inlines the internalized term \<open>t\<close> --- as constructor term for   415 datatype @{ML_type term}.   416   417 \<^descr> \<open>@{prop \<phi>}\<close> inlines the internalized proposition \<open>\<phi>\<close> --- as constructor   418 term for datatype @{ML_type term}.   419 \<close>   420   421   422 section \<open>Theorems \label{sec:thms}\<close>   423   424 text \<open>   425 A \<^emph>\<open>proposition\<close> is a well-typed term of type \<open>prop\<close>, a \<^emph>\<open>theorem\<close> is a   426 proven proposition (depending on a context of hypotheses and the background   427 theory). Primitive inferences include plain Natural Deduction rules for the   428 primary connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> of the framework. There is also a builtin   429 notion of equality/equivalence \<open>\<equiv>\<close>.   430 \<close>   431   432   433 subsection \<open>Primitive connectives and rules \label{sec:prim-rules}\<close>   434   435 text \<open>   436 The theory \<open>Pure\<close> contains constant declarations for the primitive   437 connectives \<open>\<And>\<close>, \<open>\<Longrightarrow>\<close>, and \<open>\<equiv>\<close> of the logical framework, see   438 \figref{fig:pure-connectives}. The derivability judgment \<open>A\<^sub>1, \<dots>, A\<^sub>n \<turnstile> B\<close>   439 is defined inductively by the primitive inferences given in   440 \figref{fig:prim-rules}, with the global restriction that the hypotheses   441 must \<^emph>\<open>not\<close> contain any schematic variables. The builtin equality is   442 conceptually axiomatized as shown in \figref{fig:pure-equality}, although   443 the implementation works directly with derived inferences.   444   445 \begin{figure}[htb]   446 \begin{center}   447 \begin{tabular}{ll}   448 \<open>all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop\<close> & universal quantification (binder \<open>\<And>\<close>) \\   449 \<open>\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop\<close> & implication (right associative infix) \\   450 \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> & equality relation (infix) \\   451 \end{tabular}   452 \caption{Primitive connectives of Pure}\label{fig:pure-connectives}   453 \end{center}   454 \end{figure}   455   456 \begin{figure}[htb]   457 \begin{center}   458 $  459 \infer[\<open>(axiom)\<close>]{\<open>\<turnstile> A\<close>}{\<open>A \<in> \<Theta>\<close>}   460 \qquad   461 \infer[\<open>(assume)\<close>]{\<open>A \<turnstile> A\<close>}{}   462$   463 $  464 \infer[\<open>(\<And>\<hyphen>intro)\<close>]{\<open>\<Gamma> \<turnstile> \<And>x. B[x]\<close>}{\<open>\<Gamma> \<turnstile> B[x]\<close> & \<open>x \<notin> \<Gamma>\<close>}   465 \qquad   466 \infer[\<open>(\<And>\<hyphen>elim)\<close>]{\<open>\<Gamma> \<turnstile> B[a]\<close>}{\<open>\<Gamma> \<turnstile> \<And>x. B[x]\<close>}   467$   468 $  469 \infer[\<open>(\<Longrightarrow>\<hyphen>intro)\<close>]{\<open>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>}   470 \qquad   471 \infer[\<open>(\<Longrightarrow>\<hyphen>elim)\<close>]{\<open>\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B\<close>}{\<open>\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B\<close> & \<open>\<Gamma>\<^sub>2 \<turnstile> A\<close>}   472$   473 \caption{Primitive inferences of Pure}\label{fig:prim-rules}   474 \end{center}   475 \end{figure}   476   477 \begin{figure}[htb]   478 \begin{center}   479 \begin{tabular}{ll}   480 \<open>\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]\<close> & \<open>\<beta>\<close>-conversion \\   481 \<open>\<turnstile> x \<equiv> x\<close> & reflexivity \\   482 \<open>\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y\<close> & substitution \\   483 \<open>\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g\<close> & extensionality \\   484 \<open>\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B\<close> & logical equivalence \\   485 \end{tabular}   486 \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}   487 \end{center}   488 \end{figure}   489   490 The introduction and elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> are analogous to   491 formation of dependently typed \<open>\<lambda>\<close>-terms representing the underlying proof   492 objects. Proof terms are irrelevant in the Pure logic, though; they cannot   493 occur within propositions. The system provides a runtime option to record   494 explicit proof terms for primitive inferences, see also   495 \secref{sec:proof-terms}. Thus all three levels of \<open>\<lambda>\<close>-calculus become   496 explicit: \<open>\<Rightarrow>\<close> for terms, and \<open>\<And>/\<Longrightarrow>\<close> for proofs (cf.\ @{cite   497 "Berghofer-Nipkow:2000:TPHOL"}).   498   499 Observe that locally fixed parameters (as in \<open>\<And>\<hyphen>intro\<close>) need not be recorded   500 in the hypotheses, because the simple syntactic types of Pure are always   501 inhabitable. Assumptions'' \<open>x :: \<tau>\<close> for type-membership are only present   502 as long as some \<open>x\<^sub>\<tau>\<close> occurs in the statement body.\<^footnote>\<open>This is the key   503 difference to \<open>\<lambda>HOL\<close>'' in the PTS framework @{cite   504 "Barendregt-Geuvers:2001"}, where hypotheses \<open>x : A\<close> are treated uniformly   505 for propositions and types.\<close>   506   507 \<^medskip>   508 The axiomatization of a theory is implicitly closed by forming all instances   509 of type and term variables: \<open>\<turnstile> A\<vartheta>\<close> holds for any substitution   510 instance of an axiom \<open>\<turnstile> A\<close>. By pushing substitutions through derivations   511 inductively, we also get admissible \<open>generalize\<close> and \<open>instantiate\<close> rules as   512 shown in \figref{fig:subst-rules}.   513   514 \begin{figure}[htb]   515 \begin{center}   516 $  517 \infer{\<open>\<Gamma> \<turnstile> B[?\<alpha>]\<close>}{\<open>\<Gamma> \<turnstile> B[\<alpha>]\<close> & \<open>\<alpha> \<notin> \<Gamma>\<close>}   518 \quad   519 \infer[\quad\<open>(generalize)\<close>]{\<open>\<Gamma> \<turnstile> B[?x]\<close>}{\<open>\<Gamma> \<turnstile> B[x]\<close> & \<open>x \<notin> \<Gamma>\<close>}   520$   521 $  522 \infer{\<open>\<Gamma> \<turnstile> B[\<tau>]\<close>}{\<open>\<Gamma> \<turnstile> B[?\<alpha>]\<close>}   523 \quad   524 \infer[\quad\<open>(instantiate)\<close>]{\<open>\<Gamma> \<turnstile> B[t]\<close>}{\<open>\<Gamma> \<turnstile> B[?x]\<close>}   525$   526 \caption{Admissible substitution rules}\label{fig:subst-rules}   527 \end{center}   528 \end{figure}   529   530 Note that \<open>instantiate\<close> does not require an explicit side-condition, because   531 \<open>\<Gamma>\<close> may never contain schematic variables.   532   533 In principle, variables could be substituted in hypotheses as well, but this   534 would disrupt the monotonicity of reasoning: deriving \<open>\<Gamma>\<vartheta> \<turnstile>   535 B\<vartheta>\<close> from \<open>\<Gamma> \<turnstile> B\<close> is correct, but \<open>\<Gamma>\<vartheta> \<supseteq> \<Gamma>\<close> does not   536 necessarily hold: the result belongs to a different proof context.   537   538 \<^medskip>   539 An \<^emph>\<open>oracle\<close> is a function that produces axioms on the fly. Logically, this   540 is an instance of the \<open>axiom\<close> rule (\figref{fig:prim-rules}), but there is   541 an operational difference. The system always records oracle invocations   542 within derivations of theorems by a unique tag.   543   544 Axiomatizations should be limited to the bare minimum, typically as part of   545 the initial logical basis of an object-logic formalization. Later on,   546 theories are usually developed in a strictly definitional fashion, by   547 stating only certain equalities over new constants.   548   549 A \<^emph>\<open>simple definition\<close> consists of a constant declaration \<open>c :: \<sigma>\<close> together   550 with an axiom \<open>\<turnstile> c \<equiv> t\<close>, where \<open>t :: \<sigma>\<close> is a closed term without any hidden   551 polymorphism. The RHS may depend on further defined constants, but not \<open>c\<close>   552 itself. Definitions of functions may be presented as \<open>c \<^vec>x \<equiv> t\<close>   553 instead of the puristic \<open>c \<equiv> \<lambda>\<^vec>x. t\<close>.   554   555 An \<^emph>\<open>overloaded definition\<close> consists of a collection of axioms for the same   556 constant, with zero or one equations \<open>c((\<^vec>\<alpha>)\<kappa>) \<equiv> t\<close> for each type   557 constructor \<open>\<kappa>\<close> (for distinct variables \<open>\<^vec>\<alpha>\<close>). The RHS may mention   558 previously defined constants as above, or arbitrary constants \<open>d(\<alpha>\<^sub>i)\<close> for   559 some \<open>\<alpha>\<^sub>i\<close> projected from \<open>\<^vec>\<alpha>\<close>. Thus overloaded definitions   560 essentially work by primitive recursion over the syntactic structure of a   561 single type argument. See also @{cite \<open>\S4.3\<close>   562 "Haftmann-Wenzel:2006:classes"}.   563 \<close>   564   565 text %mlref \<open>   566 \begin{mldecls}   567 @{index_ML Logic.all: "term -> term -> term"} \\   568 @{index_ML Logic.mk_implies: "term * term -> term"} \\   569 \end{mldecls}   570 \begin{mldecls}   571 @{index_ML_type ctyp} \\   572 @{index_ML_type cterm} \\   573 @{index_ML Thm.ctyp_of: "Proof.context -> typ -> ctyp"} \\   574 @{index_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\   575 @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\   576 @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\   577 @{index_ML Thm.all: "Proof.context -> cterm -> cterm -> cterm"} \\   578 @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\   579 \end{mldecls}   580 \begin{mldecls}   581 @{index_ML_type thm} \\   582 @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\   583 @{index_ML Thm.transfer: "theory -> thm -> thm"} \\   584 @{index_ML Thm.assume: "cterm -> thm"} \\   585 @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\   586 @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\   587 @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\   588 @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\   589 @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\   590 @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list   591 -> thm -> thm"} \\   592 @{index_ML Thm.add_axiom: "Proof.context ->   593 binding * term -> theory -> (string * thm) * theory"} \\   594 @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->   595 (string * ('a -> thm)) * theory"} \\   596 @{index_ML Thm.add_def: "Defs.context -> bool -> bool ->   597 binding * term -> theory -> (string * thm) * theory"} \\   598 \end{mldecls}   599 \begin{mldecls}   600 @{index_ML Theory.add_deps: "Defs.context -> string ->   601 Defs.entry -> Defs.entry list -> theory -> theory"} \\   602 \end{mldecls}   603   604 \<^descr> @{ML Thm.peek_status}~\<open>thm\<close> informs about the current status of the   605 derivation object behind the given theorem. This is a snapshot of a   606 potentially ongoing (parallel) evaluation of proofs. The three Boolean   607 values indicate the following: \<^verbatim>\<open>oracle\<close> if the finished part contains some   608 oracle invocation; \<^verbatim>\<open>unfinished\<close> if some future proofs are still pending;   609 \<^verbatim>\<open>failed\<close> if some future proof has failed, rendering the theorem invalid!   610   611 \<^descr> @{ML Logic.all}~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where   612 occurrences of the atomic term \<open>a\<close> in the body proposition \<open>B\<close> are replaced   613 by bound variables. (See also @{ML lambda} on terms.)   614   615 \<^descr> @{ML Logic.mk_implies}~\<open>(A, B)\<close> produces a Pure implication \<open>A \<Longrightarrow> B\<close>.   616   617 \<^descr> Types @{ML_type ctyp} and @{ML_type cterm} represent certified types and   618 terms, respectively. These are abstract datatypes that guarantee that its   619 values have passed the full well-formedness (and well-typedness) checks,   620 relative to the declarations of type constructors, constants etc.\ in the   621 background theory. The abstract types @{ML_type ctyp} and @{ML_type cterm}   622 are part of the same inference kernel that is mainly responsible for   623 @{ML_type thm}. Thus syntactic operations on @{ML_type ctyp} and @{ML_type   624 cterm} are located in the @{ML_structure Thm} module, even though theorems   625 are not yet involved at that stage.   626   627 \<^descr> @{ML Thm.ctyp_of}~\<open>ctxt \<tau>\<close> and @{ML Thm.cterm_of}~\<open>ctxt t\<close> explicitly   628 check types and terms, respectively. This also involves some basic   629 normalizations, such expansion of type and term abbreviations from the   630 underlying theory context. Full re-certification is relatively slow and   631 should be avoided in tight reasoning loops.   632   633 \<^descr> @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML Drule.mk_implies}   634 etc.\ compose certified terms (or propositions) incrementally. This is   635 equivalent to @{ML Thm.cterm_of} after unchecked @{ML_op "$"}, @{ML lambda},

   636   @{ML Logic.all}, @{ML Logic.mk_implies} etc., but there can be a big

   637   difference in performance when large existing entities are composed by a few

   638   extra constructions on top. There are separate operations to decompose

   639   certified terms and theorems to produce certified terms again.

   640

   641   \<^descr> Type @{ML_type thm} represents proven propositions. This is an abstract

   642   datatype that guarantees that its values have been constructed by basic

   643   principles of the @{ML_structure Thm} module. Every @{ML_type thm} value

   644   refers its background theory, cf.\ \secref{sec:context-theory}.

   645

   646   \<^descr> @{ML Thm.transfer}~\<open>thy thm\<close> transfers the given theorem to a \<^emph>\<open>larger\<close>

   647   theory, see also \secref{sec:context}. This formal adjustment of the

   648   background context has no logical significance, but is occasionally required

   649   for formal reasons, e.g.\ when theorems that are imported from more basic

   650   theories are used in the current situation.

   651

   652   \<^descr> @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML Thm.forall_elim}, @{ML

   653   Thm.implies_intr}, and @{ML Thm.implies_elim} correspond to the primitive

   654   inferences of \figref{fig:prim-rules}.

   655

   656   \<^descr> @{ML Thm.generalize}~\<open>(\<^vec>\<alpha>, \<^vec>x)\<close> corresponds to the

   657   \<open>generalize\<close> rules of \figref{fig:subst-rules}. Here collections of type and

   658   term variables are generalized simultaneously, specified by the given basic

   659   names.

   660

   661   \<^descr> @{ML Thm.instantiate}~\<open>(\<^vec>\<alpha>\<^sub>s, \<^vec>x\<^sub>\<tau>)\<close> corresponds to the

   662   \<open>instantiate\<close> rules of \figref{fig:subst-rules}. Type variables are

   663   substituted before term variables. Note that the types in \<open>\<^vec>x\<^sub>\<tau>\<close> refer

   664   to the instantiated versions.

   665

   666   \<^descr> @{ML Thm.add_axiom}~\<open>ctxt (name, A)\<close> declares an arbitrary proposition as

   667   axiom, and retrieves it as a theorem from the resulting theory, cf.\ \<open>axiom\<close>

   668   in \figref{fig:prim-rules}. Note that the low-level representation in the

   669   axiom table may differ slightly from the returned theorem.

   670

   671   \<^descr> @{ML Thm.add_oracle}~\<open>(binding, oracle)\<close> produces a named oracle rule,

   672   essentially generating arbitrary axioms on the fly, cf.\ \<open>axiom\<close> in

   673   \figref{fig:prim-rules}.

   674

   675   \<^descr> @{ML Thm.add_def}~\<open>ctxt unchecked overloaded (name, c \<^vec>x \<equiv> t)\<close>

   676   states a definitional axiom for an existing constant \<open>c\<close>. Dependencies are

   677   recorded via @{ML Theory.add_deps}, unless the \<open>unchecked\<close> option is set.

   678   Note that the low-level representation in the axiom table may differ

   679   slightly from the returned theorem.

   680

   681   \<^descr> @{ML Theory.add_deps}~\<open>ctxt name c\<^sub>\<tau> \<^vec>d\<^sub>\<sigma>\<close> declares dependencies of

   682   a named specification for constant \<open>c\<^sub>\<tau>\<close>, relative to existing

   683   specifications for constants \<open>\<^vec>d\<^sub>\<sigma>\<close>. This also works for type

   684   constructors.

   685 \<close>

   686

   687 text %mlantiq \<open>

   688   \begin{matharray}{rcl}

   689   @{ML_antiquotation_def "ctyp"} & : & \<open>ML_antiquotation\<close> \\

   690   @{ML_antiquotation_def "cterm"} & : & \<open>ML_antiquotation\<close> \\

   691   @{ML_antiquotation_def "cprop"} & : & \<open>ML_antiquotation\<close> \\

   692   @{ML_antiquotation_def "thm"} & : & \<open>ML_antiquotation\<close> \\

   693   @{ML_antiquotation_def "thms"} & : & \<open>ML_antiquotation\<close> \\

   694   @{ML_antiquotation_def "lemma"} & : & \<open>ML_antiquotation\<close> \\

   695   \end{matharray}

   696

   697   @{rail \<open>

   698   @@{ML_antiquotation ctyp} typ

   699   ;

   700   @@{ML_antiquotation cterm} term

   701   ;

   702   @@{ML_antiquotation cprop} prop

   703   ;

   704   @@{ML_antiquotation thm} thm

   705   ;

   706   @@{ML_antiquotation thms} thms

   707   ;

   708   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>

   709     @'by' method method?

   710   \<close>}

   711

   712   \<^descr> \<open>@{ctyp \<tau>}\<close> produces a certified type wrt.\ the current background theory

   713   --- as abstract value of type @{ML_type ctyp}.

   714

   715   \<^descr> \<open>@{cterm t}\<close> and \<open>@{cprop \<phi>}\<close> produce a certified term wrt.\ the current

   716   background theory --- as abstract value of type @{ML_type cterm}.

   717

   718   \<^descr> \<open>@{thm a}\<close> produces a singleton fact --- as abstract value of type

   719   @{ML_type thm}.

   720

   721   \<^descr> \<open>@{thms a}\<close> produces a general fact --- as abstract value of type

   722   @{ML_type "thm list"}.

   723

   724   \<^descr> \<open>@{lemma \<phi> by meth}\<close> produces a fact that is proven on the spot according

   725   to the minimal proof, which imitates a terminal Isar proof. The result is an

   726   abstract value of type @{ML_type thm} or @{ML_type "thm list"}, depending on

   727   the number of propositions given here.

   728

   729   The internal derivation object lacks a proper theorem name, but it is

   730   formally closed, unless the \<open>(open)\<close> option is specified (this may impact

   731   performance of applications with proof terms).

   732

   733   Since ML antiquotations are always evaluated at compile-time, there is no

   734   run-time overhead even for non-trivial proofs. Nonetheless, the

   735   justification is syntactically limited to a single @{command "by"} step.

   736   More complex Isar proofs should be done in regular theory source, before

   737   compiling the corresponding ML text that uses the result.

   738 \<close>

   739

   740

   741 subsection \<open>Auxiliary connectives \label{sec:logic-aux}\<close>

   742

   743 text \<open>

   744   Theory \<open>Pure\<close> provides a few auxiliary connectives that are defined on top

   745   of the primitive ones, see \figref{fig:pure-aux}. These special constants

   746   are useful in certain internal encodings, and are normally not directly

   747   exposed to the user.

   748

   749   \begin{figure}[htb]

   750   \begin{center}

   751   \begin{tabular}{ll}

   752   \<open>conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop\<close> & (infix \<open>&&&\<close>) \\

   753   \<open>\<turnstile> A &&& B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)\<close> \$1ex]   754 \<open>prop :: prop \<Rightarrow> prop\<close> & (prefix \<open>#\<close>, suppressed) \\   755 \<open>#A \<equiv> A\<close> \\[1ex]   756 \<open>term :: \<alpha> \<Rightarrow> prop\<close> & (prefix \<open>TERM\<close>) \\   757 \<open>term x \<equiv> (\<And>A. A \<Longrightarrow> A)\<close> \\[1ex]   758 \<open>type :: \<alpha> itself\<close> & (prefix \<open>TYPE\<close>) \\   759 \<open>(unspecified)\<close> \\   760 \end{tabular}   761 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}   762 \end{center}   763 \end{figure}   764   765 The introduction \<open>A \<Longrightarrow> B \<Longrightarrow> A &&& B\<close>, and eliminations (projections) \<open>A &&& B   766 \<Longrightarrow> A\<close> and \<open>A &&& B \<Longrightarrow> B\<close> are available as derived rules. Conjunction allows to   767 treat simultaneous assumptions and conclusions uniformly, e.g.\ consider \<open>A   768 \<Longrightarrow> B \<Longrightarrow> C &&& D\<close>. In particular, the goal mechanism represents multiple claims   769 as explicit conjunction internally, but this is refined (via backwards   770 introduction) into separate sub-goals before the user commences the proof;   771 the final result is projected into a list of theorems using eliminations   772 (cf.\ \secref{sec:tactical-goals}).   773   774 The \<open>prop\<close> marker (\<open>#\<close>) makes arbitrarily complex propositions appear as   775 atomic, without changing the meaning: \<open>\<Gamma> \<turnstile> A\<close> and \<open>\<Gamma> \<turnstile> #A\<close> are   776 interchangeable. See \secref{sec:tactical-goals} for specific operations.   777   778 The \<open>term\<close> marker turns any well-typed term into a derivable proposition: \<open>\<turnstile>   779 TERM t\<close> holds unconditionally. Although this is logically vacuous, it allows   780 to treat terms and proofs uniformly, similar to a type-theoretic framework.   781   782 The \<open>TYPE\<close> constructor is the canonical representative of the unspecified   783 type \<open>\<alpha> itself\<close>; it essentially injects the language of types into that of   784 terms. There is specific notation \<open>TYPE(\<tau>)\<close> for \<open>TYPE\<^bsub>\<tau> itself\<^esub>\<close>. Although   785 being devoid of any particular meaning, the term \<open>TYPE(\<tau>)\<close> accounts for the   786 type \<open>\<tau>\<close> within the term language. In particular, \<open>TYPE(\<alpha>)\<close> may be used as   787 formal argument in primitive definitions, in order to circumvent hidden   788 polymorphism (cf.\ \secref{sec:terms}). For example, \<open>c TYPE(\<alpha>) \<equiv> A[\<alpha>]\<close>   789 defines \<open>c :: \<alpha> itself \<Rightarrow> prop\<close> in terms of a proposition \<open>A\<close> that depends on   790 an additional type argument, which is essentially a predicate on types.   791 \<close>   792   793 text %mlref \<open>   794 \begin{mldecls}   795 @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\   796 @{index_ML Conjunction.elim: "thm -> thm * thm"} \\   797 @{index_ML Drule.mk_term: "cterm -> thm"} \\   798 @{index_ML Drule.dest_term: "thm -> cterm"} \\   799 @{index_ML Logic.mk_type: "typ -> term"} \\   800 @{index_ML Logic.dest_type: "term -> typ"} \\   801 \end{mldecls}   802   803 \<^descr> @{ML Conjunction.intr} derives \<open>A &&& B\<close> from \<open>A\<close> and \<open>B\<close>.   804   805 \<^descr> @{ML Conjunction.elim} derives \<open>A\<close> and \<open>B\<close> from \<open>A &&& B\<close>.   806   807 \<^descr> @{ML Drule.mk_term} derives \<open>TERM t\<close>.   808   809 \<^descr> @{ML Drule.dest_term} recovers term \<open>t\<close> from \<open>TERM t\<close>.   810   811 \<^descr> @{ML Logic.mk_type}~\<open>\<tau>\<close> produces the term \<open>TYPE(\<tau>)\<close>.   812   813 \<^descr> @{ML Logic.dest_type}~\<open>TYPE(\<tau>)\<close> recovers the type \<open>\<tau>\<close>.   814 \<close>   815   816   817 subsection \<open>Sort hypotheses\<close>   818   819 text \<open>   820 Type variables are decorated with sorts, as explained in \secref{sec:types}.   821 This constrains type instantiation to certain ranges of types: variable   822 \<open>\<alpha>\<^sub>s\<close> may only be assigned to types \<open>\<tau>\<close> that belong to sort \<open>s\<close>. Within the   823 logic, sort constraints act like implicit preconditions on the result \<open>\<lparr>\<alpha>\<^sub>1   824 : s\<^sub>1\<rparr>, \<dots>, \<lparr>\<alpha>\<^sub>n : s\<^sub>n\<rparr>, \<Gamma> \<turnstile> \<phi>\<close> where the type variables \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n\<close> cover   825 the propositions \<open>\<Gamma>\<close>, \<open>\<phi>\<close>, as well as the proof of \<open>\<Gamma> \<turnstile> \<phi>\<close>.   826   827 These \<^emph>\<open>sort hypothesis\<close> of a theorem are passed monotonically through   828 further derivations. They are redundant, as long as the statement of a   829 theorem still contains the type variables that are accounted here. The   830 logical significance of sort hypotheses is limited to the boundary case   831 where type variables disappear from the proposition, e.g.\ \<open>\<lparr>\<alpha>\<^sub>s : s\<rparr> \<turnstile> \<phi>\<close>.   832 Since such dangling type variables can be renamed arbitrarily without   833 changing the proposition \<open>\<phi>\<close>, the inference kernel maintains sort hypotheses   834 in anonymous form \<open>s \<turnstile> \<phi>\<close>.   835   836 In most practical situations, such extra sort hypotheses may be stripped in   837 a final bookkeeping step, e.g.\ at the end of a proof: they are typically   838 left over from intermediate reasoning with type classes that can be   839 satisfied by some concrete type \<open>\<tau>\<close> of sort \<open>s\<close> to replace the hypothetical   840 type variable \<open>\<alpha>\<^sub>s\<close>.   841 \<close>   842   843 text %mlref \<open>   844 \begin{mldecls}   845 @{index_ML Thm.extra_shyps: "thm -> sort list"} \\   846 @{index_ML Thm.strip_shyps: "thm -> thm"} \\   847 \end{mldecls}   848   849 \<^descr> @{ML Thm.extra_shyps}~\<open>thm\<close> determines the extraneous sort hypotheses of   850 the given theorem, i.e.\ the sorts that are not present within type   851 variables of the statement.   852   853 \<^descr> @{ML Thm.strip_shyps}~\<open>thm\<close> removes any extraneous sort hypotheses that   854 can be witnessed from the type signature.   855 \<close>   856   857 text %mlex \<open>   858 The following artificial example demonstrates the derivation of @{prop   859 False} with a pending sort hypothesis involving a logically empty sort.   860 \<close>   861   862 class empty =   863 assumes bad: "\<And>(x::'a) y. x \<noteq> y"   864   865 theorem (in empty) false: False   866 using bad by blast   867   868 ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>   869   870 text \<open>   871 Thanks to the inference kernel managing sort hypothesis according to their   872 logical significance, this example is merely an instance of \<^emph>\<open>ex falso   873 quodlibet consequitur\<close> --- not a collapse of the logical framework!   874 \<close>   875   876   877 section \<open>Object-level rules \label{sec:obj-rules}\<close>   878   879 text \<open>   880 The primitive inferences covered so far mostly serve foundational purposes.   881 User-level reasoning usually works via object-level rules that are   882 represented as theorems of Pure. Composition of rules involves   883 \<^emph>\<open>backchaining\<close>, \<^emph>\<open>higher-order unification\<close> modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion of   884 \<open>\<lambda>\<close>-terms, and so-called \<^emph>\<open>lifting\<close> of rules into a context of \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>   885 connectives. Thus the full power of higher-order Natural Deduction in   886 Isabelle/Pure becomes readily available.   887 \<close>   888   889   890 subsection \<open>Hereditary Harrop Formulae\<close>   891   892 text \<open>   893 The idea of object-level rules is to model Natural Deduction inferences in   894 the style of Gentzen @{cite "Gentzen:1935"}, but we allow arbitrary nesting   895 similar to @{cite extensions91}. The most basic rule format is that of a   896 \<^emph>\<open>Horn Clause\<close>:   897 \[   898 \infer{\<open>A\<close>}{\<open>A\<^sub>1\<close> & \<open>\<dots>\<close> & \<open>A\<^sub>n\<close>}   899$

   900   where \<open>A, A\<^sub>1, \<dots>, A\<^sub>n\<close> are atomic propositions of the framework, usually of

   901   the form \<open>Trueprop B\<close>, where \<open>B\<close> is a (compound) object-level statement.

   902   This object-level inference corresponds to an iterated implication in Pure

   903   like this:

   904   $  905 \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close>   906$

   907   As an example consider conjunction introduction: \<open>A \<Longrightarrow> B \<Longrightarrow> A \<and> B\<close>. Any

   908   parameters occurring in such rule statements are conceptionally treated as

   909   arbitrary:

   910   $  911 \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. A\<^sub>1 x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> \<dots> A\<^sub>n x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> A x\<^sub>1 \<dots> x\<^sub>m\<close>   912$

   913

   914   Nesting of rules means that the positions of \<open>A\<^sub>i\<close> may again hold compound

   915   rules, not just atomic propositions. Propositions of this format are called

   916   \<^emph>\<open>Hereditary Harrop Formulae\<close> in the literature @{cite "Miller:1991"}. Here

   917   we give an inductive characterization as follows:

   918

   919   \<^medskip>

   920   \begin{tabular}{ll}

   921   \<open>\<^bold>x\<close> & set of variables \\

   922   \<open>\<^bold>A\<close> & set of atomic propositions \\

   923   \<open>\<^bold>H  =  \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A\<close> & set of Hereditary Harrop Formulas \\

   924   \end{tabular}

   925   \<^medskip>

   926

   927   Thus we essentially impose nesting levels on propositions formed from \<open>\<And>\<close>

   928   and \<open>\<Longrightarrow>\<close>. At each level there is a prefix of parameters and compound

   929   premises, concluding an atomic proposition. Typical examples are

   930   \<open>\<longrightarrow>\<close>-introduction \<open>(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B\<close> or mathematical induction \<open>P 0 \<Longrightarrow> (\<And>n. P n

   931   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n\<close>. Even deeper nesting occurs in well-founded induction

   932   \<open>(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x\<close>, but this already marks the limit of

   933   rule complexity that is usually seen in practice.

   934

   935   \<^medskip>

   936   Regular user-level inferences in Isabelle/Pure always maintain the following

   937   canonical form of results:

   938

   939   \<^item> Normalization by \<open>(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)\<close>, which is a theorem of

   940   Pure, means that quantifiers are pushed in front of implication at each

   941   level of nesting. The normal form is a Hereditary Harrop Formula.

   942

   943   \<^item> The outermost prefix of parameters is represented via schematic variables:

   944   instead of \<open>\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x\<close> we have \<open>\<^vec>H

   945   ?\<^vec>x \<Longrightarrow> A ?\<^vec>x\<close>. Note that this representation looses information

   946   about the order of parameters, and vacuous quantifiers vanish automatically.

   947 \<close>

   948

   949 text %mlref \<open>

   950   \begin{mldecls}

   951   @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\

   952   \end{mldecls}

   953

   954   \<^descr> @{ML Simplifier.norm_hhf}~\<open>ctxt thm\<close> normalizes the given theorem

   955   according to the canonical form specified above. This is occasionally

   956   helpful to repair some low-level tools that do not handle Hereditary Harrop

   957   Formulae properly.

   958 \<close>

   959

   960

   961 subsection \<open>Rule composition\<close>

   962

   963 text \<open>

   964   The rule calculus of Isabelle/Pure provides two main inferences: @{inference

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

   966   (i.e.\ closing a branch), both modulo higher-order unification. There are

   967   also combined variants, notably @{inference elim_resolution} and @{inference

   968   dest_resolution}.

   969

   970   To understand the all-important @{inference resolution} principle, we first

   971   consider raw @{inference_def composition} (modulo higher-order unification

   972   with substitution \<open>\<vartheta>\<close>):

   973   $  974 \infer[(@{inference_def composition})]{\<open>\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}   975 {\<open>\<^vec>A \<Longrightarrow> B\<close> & \<open>B' \<Longrightarrow> C\<close> & \<open>B\<vartheta> = B'\<vartheta>\<close>}   976$

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

   978   second; the resulting rule instance inherits the premises of the first and

   979   conclusion of the second. Note that \<open>C\<close> can again consist of iterated

   980   implications. We can also permute the premises of the second rule

   981   back-and-forth in order to compose with \<open>B'\<close> in any position (subsequently

   982   we shall always refer to position 1 w.l.o.g.).

   983

   984   In @{inference composition} the internal structure of the common part \<open>B\<close>

   985   and \<open>B'\<close> is not taken into account. For proper @{inference resolution} we

   986   require \<open>B\<close> to be atomic, and explicitly observe the structure \<open>\<And>\<^vec>x.

   987   \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x\<close> of the premise of the second rule. The idea

   988   is to adapt the first rule by lifting'' it into this context, by means of

   989   iterated application of the following inferences:

   990   $  991 \infer[(@{inference_def imp_lift})]{\<open>(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)\<close>}{\<open>\<^vec>A \<Longrightarrow> B\<close>}   992$

   993   $  994 \infer[(@{inference_def all_lift})]{\<open>(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))\<close>}{\<open>\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a\<close>}   995$

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

   997   resolution} as follows:

   998   $  999 \infer[(@{inference_def resolution})]   1000 {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}   1001 {\begin{tabular}{l}   1002 \<open>\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a\<close> \\   1003 \<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\   1004 \<open>(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\   1005 \end{tabular}}   1006$

  1007

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

  1009   and sub-problems. Branches are closed either by resolving with a rule of 0

  1010   premises, or by producing a short-circuit'' within a solved situation

  1011   (again modulo unification):

  1012   $  1013 \infer[(@{inference_def assumption})]{\<open>C\<vartheta>\<close>}   1014 {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{(for some~\<open>i\<close>)}}   1015$

  1016

  1017   %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}

  1018 \<close>

  1019

  1020 text %mlref \<open>

  1021   \begin{mldecls}

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

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

  1024

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

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

  1027

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

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

  1030   \end{mldecls}

  1031

  1032   \<^descr> \<open>rule\<^sub>1 RSN (i, rule\<^sub>2)\<close> resolves the conclusion of \<open>rule\<^sub>1\<close> with the

  1033   \<open>i\<close>-th premise of \<open>rule\<^sub>2\<close>, according to the @{inference resolution}

  1034   principle explained above. Unless there is precisely one resolvent it raises

  1035   exception @{ML THM}.

  1036

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

  1038   language.

  1039

  1040   \<^descr> \<open>rule\<^sub>1 RS rule\<^sub>2\<close> abbreviates \<open>rule\<^sub>1 RSN (1, rule\<^sub>2)\<close>.

  1041

  1042   \<^descr> \<open>rules\<^sub>1 RLN (i, rules\<^sub>2)\<close> joins lists of rules. For every \<open>rule\<^sub>1\<close> in

  1043   \<open>rules\<^sub>1\<close> and \<open>rule\<^sub>2\<close> in \<open>rules\<^sub>2\<close>, it resolves the conclusion of \<open>rule\<^sub>1\<close>

  1044   with the \<open>i\<close>-th premise of \<open>rule\<^sub>2\<close>, accumulating multiple results in one

  1045   big list. Note that such strict enumerations of higher-order unifications

  1046   can be inefficient compared to the lazy variant seen in elementary tactics

  1047   like @{ML resolve_tac}.

  1048

  1049   \<^descr> \<open>rules\<^sub>1 RL rules\<^sub>2\<close> abbreviates \<open>rules\<^sub>1 RLN (1, rules\<^sub>2)\<close>.

  1050

  1051   \<^descr> \<open>[rule\<^sub>1, \<dots>, rule\<^sub>n] MRS rule\<close> resolves \<open>rule\<^sub>i\<close> against premise \<open>i\<close> of

  1052   \<open>rule\<close>, for \<open>i = n, \<dots>, 1\<close>. By working from right to left, newly emerging

  1053   premises are concatenated in the result, without interfering.

  1054

  1055   \<^descr> \<open>rule OF rules\<close> is an alternative notation for \<open>rules MRS rule\<close>, which

  1056   makes rule composition look more like function application. Note that the

  1057   argument \<open>rules\<close> need not be atomic.

  1058

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

  1060   language.

  1061 \<close>

  1062

  1063

  1064 section \<open>Proof terms \label{sec:proof-terms}\<close>

  1065

  1066 text \<open>

  1067   The Isabelle/Pure inference kernel can record the proof of each theorem as a

  1068   proof term that contains all logical inferences in detail. Rule composition

  1069   by resolution (\secref{sec:obj-rules}) and type-class reasoning is broken

  1070   down to primitive rules of the logical framework. The proof term can be

  1071   inspected by a separate proof-checker, for example.

  1072

  1073   According to the well-known \<^emph>\<open>Curry-Howard isomorphism\<close>, a proof can be

  1074   viewed as a \<open>\<lambda>\<close>-term. Following this idea, proofs in Isabelle are internally

  1075   represented by a datatype similar to the one for terms described in

  1076   \secref{sec:terms}. On top of these syntactic terms, two more layers of

  1077   \<open>\<lambda>\<close>-calculus are added, which correspond to \<open>\<And>x :: \<alpha>. B x\<close> and \<open>A \<Longrightarrow> B\<close>

  1078   according to the propositions-as-types principle. The resulting 3-level

  1079   \<open>\<lambda>\<close>-calculus resembles \<open>\<lambda>HOL\<close>'' in the more abstract setting of Pure Type

  1080   Systems (PTS) @{cite "Barendregt-Geuvers:2001"}, if some fine points like

  1081   schematic polymorphism and type classes are ignored.

  1082

  1083   \<^medskip>

  1084   \<^emph>\<open>Proof abstractions\<close> of the form \<open>\<^bold>\<lambda>x :: \<alpha>. prf\<close> or \<open>\<^bold>\<lambda>p : A. prf\<close>

  1085   correspond to introduction of \<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>, and \<^emph>\<open>proof applications\<close> of the form

  1086   \<open>p \<cdot> t\<close> or \<open>p \<bullet> q\<close> correspond to elimination of \<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>. Actual types \<open>\<alpha>\<close>,

  1087   propositions \<open>A\<close>, and terms \<open>t\<close> might be suppressed and reconstructed from

  1088   the overall proof term.

  1089

  1090   \<^medskip>

  1091   Various atomic proofs indicate special situations within the proof

  1092   construction as follows.

  1093

  1094   A \<^emph>\<open>bound proof variable\<close> is a natural number \<open>b\<close> that acts as de-Bruijn

  1095   index for proof term abstractions.

  1096

  1097   A \<^emph>\<open>minimal proof\<close> \<open>?\<close>'' is a dummy proof term. This indicates some

  1098   unrecorded part of the proof.

  1099

  1100   \<open>Hyp A\<close> refers to some pending hypothesis by giving its proposition. This

  1101   indicates an open context of implicit hypotheses, similar to loose bound

  1102   variables or free variables within a term (\secref{sec:terms}).

  1103

  1104   An \<^emph>\<open>axiom\<close> or \<^emph>\<open>oracle\<close> \<open>a : A[\<^vec>\<tau>]\<close> refers some postulated \<open>proof

  1105   constant\<close>, which is subject to schematic polymorphism of theory content, and

  1106   the particular type instantiation may be given explicitly. The vector of

  1107   types \<open>\<^vec>\<tau>\<close> refers to the schematic type variables in the generic

  1108   proposition \<open>A\<close> in canonical order.

  1109

  1110   A \<^emph>\<open>proof promise\<close> \<open>a : A[\<^vec>\<tau>]\<close> is a placeholder for some proof of

  1111   polymorphic proposition \<open>A\<close>, with explicit type instantiation as given by

  1112   the vector \<open>\<^vec>\<tau>\<close>, as above. Unlike axioms or oracles, proof promises

  1113   may be \<^emph>\<open>fulfilled\<close> eventually, by substituting \<open>a\<close> by some particular proof

  1114   \<open>q\<close> at the corresponding type instance. This acts like Hindley-Milner

  1115   \<open>let\<close>-polymorphism: a generic local proof definition may get used at

  1116   different type instances, and is replaced by the concrete instance

  1117   eventually.

  1118

  1119   A \<^emph>\<open>named theorem\<close> wraps up some concrete proof as a closed formal entity,

  1120   in the manner of constant definitions for proof terms. The \<^emph>\<open>proof body\<close> of

  1121   such boxed theorems involves some digest about oracles and promises

  1122   occurring in the original proof. This allows the inference kernel to manage

  1123   this critical information without the full overhead of explicit proof terms.

  1124 \<close>

  1125

  1126

  1127 subsection \<open>Reconstructing and checking proof terms\<close>

  1128

  1129 text \<open>

  1130   Fully explicit proof terms can be large, but most of this information is

  1131   redundant and can be reconstructed from the context. Therefore, the

  1132   Isabelle/Pure inference kernel records only \<^emph>\<open>implicit\<close> proof terms, by

  1133   omitting all typing information in terms, all term and type labels of proof

  1134   abstractions, and some argument terms of applications \<open>p \<cdot> t\<close> (if possible).

  1135

  1136   There are separate operations to reconstruct the full proof term later on,

  1137   using \<^emph>\<open>higher-order pattern unification\<close> @{cite "nipkow-patterns" and

  1138   "Berghofer-Nipkow:2000:TPHOL"}.

  1139

  1140   The \<^emph>\<open>proof checker\<close> expects a fully reconstructed proof term, and can turn

  1141   it into a theorem by replaying its primitive inferences within the kernel.

  1142 \<close>

  1143

  1144

  1145 subsection \<open>Concrete syntax of proof terms\<close>

  1146

  1147 text \<open>

  1148   The concrete syntax of proof terms is a slight extension of the regular

  1149   inner syntax of Isabelle/Pure @{cite "isabelle-isar-ref"}. Its main

  1150   syntactic category @{syntax (inner) proof} is defined as follows:

  1151

  1152   \begin{center}

  1153   \begin{supertabular}{rclr}

  1154

  1155   @{syntax_def (inner) proof} & = & \<^verbatim>\<open>Lam\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\

  1156     & \<open>|\<close> & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\

  1157     & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%\<close> \<open>any\<close> \\

  1158     & \<open>|\<close> & \<open>proof\<close> \<open>\<cdot>\<close> \<open>any\<close> \\

  1159     & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%%\<close> \<open>proof\<close> \\

  1160     & \<open>|\<close> & \<open>proof\<close> \<open>\<bullet>\<close> \<open>proof\<close> \\

  1161     & \<open>|\<close> & \<open>id  |  longid\<close> \\

  1162   \\

  1163

  1164   \<open>param\<close> & = & \<open>idt\<close> \\

  1165     & \<open>|\<close> & \<open>idt\<close> \<^verbatim>\<open>:\<close> \<open>prop\<close> \\

  1166     & \<open>|\<close> & \<^verbatim>\<open>(\<close> \<open>param\<close> \<^verbatim>\<open>)\<close> \\

  1167   \\

  1168

  1169   \<open>params\<close> & = & \<open>param\<close> \\

  1170     & \<open>|\<close> & \<open>param\<close> \<open>params\<close> \\

  1171

  1172   \end{supertabular}

  1173   \end{center}

  1174

  1175   Implicit term arguments in partial proofs are indicated by \<open>_\<close>''. Type

  1176   arguments for theorems and axioms may be specified using \<open>p \<cdot> TYPE(type)\<close>

  1177   (they must appear before any other term argument of a theorem or axiom, but

  1178   may be omitted altogether).

  1179

  1180   \<^medskip>

  1181   There are separate read and print operations for proof terms, in order to

  1182   avoid conflicts with the regular term language.

  1183 \<close>

  1184

  1185 text %mlref \<open>

  1186   \begin{mldecls}

  1187   @{index_ML_type proof} \\

  1188   @{index_ML_type proof_body} \\

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

  1190   @{index_ML Reconstruct.reconstruct_proof:

  1191   "Proof.context -> term -> proof -> proof"} \\

  1192   @{index_ML Reconstruct.expand_proof: "Proof.context ->

  1193   (string * term option) list -> proof -> proof"} \\

  1194   @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\

  1195   @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\

  1196   @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\

  1197   \end{mldecls}

  1198

  1199   \<^descr> Type @{ML_type proof} represents proof terms; this is a datatype with

  1200   constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"},

  1201   @{index_ML_op "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML

  1202   Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML Promise}, @{index_ML

  1203   PThm} as explained above. %FIXME OfClass (!?)

  1204

  1205   \<^descr> Type @{ML_type proof_body} represents the nested proof information of a

  1206   named theorem, consisting of a digest of oracles and named theorem over some

  1207   proof term. The digest only covers the directly visible part of the proof:

  1208   in order to get the full information, the implicit graph of nested theorems

  1209   needs to be traversed (e.g.\ using @{ML Proofterm.fold_body_thms}).

  1210

  1211   \<^descr> @{ML Thm.proof_of}~\<open>thm\<close> and @{ML Thm.proof_body_of}~\<open>thm\<close> produce the

  1212   proof term or proof body (with digest of oracles and theorems) from a given

  1213   theorem. Note that this involves a full join of internal futures that

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

  1215   construction of proofs by introducing dynamic ad-hoc dependencies. Parallel

  1216   performance may suffer by inspecting proof terms at run-time.

  1217

  1218   \<^descr> @{ML Proofterm.proofs} specifies the detail of proof recording within

  1219   @{ML_type thm} values produced by the inference kernel: @{ML 0} records only

  1220   the names of oracles, @{ML 1} records oracle names and propositions, @{ML 2}

  1221   additionally records full proof terms. Officially named theorems that

  1222   contribute to a result are recorded in any case.

  1223

  1224   \<^descr> @{ML Reconstruct.reconstruct_proof}~\<open>ctxt prop prf\<close> turns the implicit

  1225   proof term \<open>prf\<close> into a full proof of the given proposition.

  1226

  1227   Reconstruction may fail if \<open>prf\<close> is not a proof of \<open>prop\<close>, or if it does not

  1228   contain sufficient information for reconstruction. Failure may only happen

  1229   for proofs that are constructed manually, but not for those produced

  1230   automatically by the inference kernel.

  1231

  1232   \<^descr> @{ML Reconstruct.expand_proof}~\<open>ctxt [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and

  1233   reconstructs the proofs of all specified theorems, with the given (full)

  1234   proof. Theorems that are not unique specified via their name may be

  1235   disambiguated by giving their proposition.

  1236

  1237   \<^descr> @{ML Proof_Checker.thm_of_proof}~\<open>thy prf\<close> turns the given (full) proof

  1238   into a theorem, by replaying it using only primitive rules of the inference

  1239   kernel.

  1240

  1241   \<^descr> @{ML Proof_Syntax.read_proof}~\<open>thy b\<^sub>1 b\<^sub>2 s\<close> reads in a proof term. The

  1242   Boolean flags indicate the use of sort and type information. Usually, typing

  1243   information is left implicit and is inferred during proof reconstruction.

  1244   %FIXME eliminate flags!?

  1245

  1246   \<^descr> @{ML Proof_Syntax.pretty_proof}~\<open>ctxt prf\<close> pretty-prints the given proof

  1247   term.

  1248 \<close>

  1249

  1250 text %mlex \<open>

  1251   \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close> provides basic examples involving

  1252   proof terms.

  1253

  1254   \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/XML_Data.thy\<close> demonstrates export and import of

  1255   proof terms via XML/ML data representation.

  1256 \<close>

  1257

  1258 end