src/Doc/Implementation/Logic.thy
 author wenzelm Fri Jun 29 15:54:41 2018 +0200 (17 months ago ago) changeset 68540 000a0e062529 parent 67146 909dcdec2122 child 68559 7aae213d9e69 permissions -rw-r--r--
disallow pending hyps;
disallow pending shyps, with option to override the check;
tuned message;
     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 declare [[pending_shyps]]   866   867 theorem (in empty) false: False   868 using bad by blast   869   870 declare [[pending_shyps = false]]   871   872 ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>   873   874 text \<open>   875 Thanks to the inference kernel managing sort hypothesis according to their   876 logical significance, this example is merely an instance of \<^emph>\<open>ex falso   877 quodlibet consequitur\<close> --- not a collapse of the logical framework!   878 \<close>   879   880   881 section \<open>Object-level rules \label{sec:obj-rules}\<close>   882   883 text \<open>   884 The primitive inferences covered so far mostly serve foundational purposes.   885 User-level reasoning usually works via object-level rules that are   886 represented as theorems of Pure. Composition of rules involves   887 \<^emph>\<open>backchaining\<close>, \<^emph>\<open>higher-order unification\<close> modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion of   888 \<open>\<lambda>\<close>-terms, and so-called \<^emph>\<open>lifting\<close> of rules into a context of \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>   889 connectives. Thus the full power of higher-order Natural Deduction in   890 Isabelle/Pure becomes readily available.   891 \<close>   892   893   894 subsection \<open>Hereditary Harrop Formulae\<close>   895   896 text \<open>   897 The idea of object-level rules is to model Natural Deduction inferences in   898 the style of Gentzen @{cite "Gentzen:1935"}, but we allow arbitrary nesting   899 similar to @{cite extensions91}. The most basic rule format is that of a   900 \<^emph>\<open>Horn Clause\<close>:   901 \[   902 \infer{\<open>A\<close>}{\<open>A\<^sub>1\<close> & \<open>\<dots>\<close> & \<open>A\<^sub>n\<close>}   903$

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

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

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

   907   like this:

   908   $  909 \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close>   910$

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

   912   parameters occurring in such rule statements are conceptionally treated as

   913   arbitrary:

   914   $  915 \<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>   916$

   917

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

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

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

   921   we give an inductive characterization as follows:

   922

   923   \<^medskip>

   924   \begin{tabular}{ll}

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

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

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

   928   \end{tabular}

   929   \<^medskip>

   930

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

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

   933   premises, concluding an atomic proposition. Typical examples are

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

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

   936   \<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

   937   rule complexity that is usually seen in practice.

   938

   939   \<^medskip>

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

   941   canonical form of results:

   942

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

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

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

   946

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

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

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

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

   951 \<close>

   952

   953 text %mlref \<open>

   954   \begin{mldecls}

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

   956   \end{mldecls}

   957

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

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

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

   961   Formulae properly.

   962 \<close>

   963

   964

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

   966

   967 text \<open>

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

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

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

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

   972   dest_resolution}.

   973

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

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

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

   977   $  978 \infer[(@{inference_def composition})]{\<open>\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}   979 {\<open>\<^vec>A \<Longrightarrow> B\<close> & \<open>B' \<Longrightarrow> C\<close> & \<open>B\<vartheta> = B'\<vartheta>\<close>}   980$

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

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

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

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

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

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

   987

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

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

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

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

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

   993   iterated application of the following inferences:

   994   $  995 \infer[(@{inference_def imp_lift})]{\<open>(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)\<close>}{\<open>\<^vec>A \<Longrightarrow> B\<close>}   996$

   997   $  998 \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>}   999$

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

  1001   resolution} as follows:

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

  1011

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

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

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

  1015   (again modulo unification):

  1016   $  1017 \infer[(@{inference_def assumption})]{\<open>C\<vartheta>\<close>}   1018 {\<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>)}}   1019$

  1020

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

  1022 \<close>

  1023

  1024 text %mlref \<open>

  1025   \begin{mldecls}

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

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

  1028

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

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

  1031

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

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

  1034   \end{mldecls}

  1035

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

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

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

  1039   exception @{ML THM}.

  1040

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

  1042   language.

  1043

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

  1045

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

  1047   \<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>

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

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

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

  1051   like @{ML resolve_tac}.

  1052

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

  1054

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

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

  1057   premises are concatenated in the result, without interfering.

  1058

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

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

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

  1062

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

  1064   language.

  1065 \<close>

  1066

  1067

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

  1069

  1070 text \<open>

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

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

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

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

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

  1076

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

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

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

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

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

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

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

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

  1085   schematic polymorphism and type classes are ignored.

  1086

  1087   \<^medskip>

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

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

  1090   \<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>,

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

  1092   the overall proof term.

  1093

  1094   \<^medskip>

  1095   Various atomic proofs indicate special situations within the proof

  1096   construction as follows.

  1097

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

  1099   index for proof term abstractions.

  1100

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

  1102   unrecorded part of the proof.

  1103

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

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

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

  1107

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

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

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

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

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

  1113

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

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

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

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

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

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

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

  1121   eventually.

  1122

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

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

  1125   such boxed theorems involves some digest about oracles and promises

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

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

  1128 \<close>

  1129

  1130

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

  1132

  1133 text \<open>

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

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

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

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

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

  1139

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

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

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

  1143

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

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

  1146 \<close>

  1147

  1148

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

  1150

  1151 text \<open>

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

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

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

  1155

  1156   \begin{center}

  1157   \begin{supertabular}{rclr}

  1158

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

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

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

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

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

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

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

  1166   \\

  1167

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

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

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

  1171   \\

  1172

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

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

  1175

  1176   \end{supertabular}

  1177   \end{center}

  1178

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

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

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

  1182   may be omitted altogether).

  1183

  1184   \<^medskip>

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

  1186   avoid conflicts with the regular term language.

  1187 \<close>

  1188

  1189 text %mlref \<open>

  1190   \begin{mldecls}

  1191   @{index_ML_type proof} \\

  1192   @{index_ML_type proof_body} \\

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

  1194   @{index_ML Reconstruct.reconstruct_proof:

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

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

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

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

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

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

  1201   \end{mldecls}

  1202

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

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

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

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

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

  1208

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

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

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

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

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

  1214

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

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

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

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

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

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

  1221

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

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

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

  1225   additionally records full proof terms. Officially named theorems that

  1226   contribute to a result are recorded in any case.

  1227

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

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

  1230

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

  1232   contain sufficient information for reconstruction. Failure may only happen

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

  1234   automatically by the inference kernel.

  1235

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

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

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

  1239   disambiguated by giving their proposition.

  1240

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

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

  1243   kernel.

  1244

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

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

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

  1248   %FIXME eliminate flags!?

  1249

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

  1251   term.

  1252 \<close>

  1253

  1254 text %mlex \<open>

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

  1256   proof terms.

  1257

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

  1259   proof terms via XML/ML data representation.

  1260 \<close>

  1261

  1262 end