1(*:maxLineLen=78:*)
2
3theory Logic
4imports Base
5begin
6
7chapter \<open>Primitive logic \label{ch:logic}\<close>
8
9text \<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
32section \<open>Types \label{sec:types}\<close>
33
34text \<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
103text %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
163text %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
205section \<open>Terms \label{sec:terms}\<close>
206
207text \<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
314text %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
384text %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
422section \<open>Theorems \label{sec:thms}\<close>
423
424text \<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
433subsection \<open>Primitive connectives and rules \label{sec:prim-rules}\<close>
434
435text \<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
565text %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
687text %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
741subsection \<open>Auxiliary connectives \label{sec:logic-aux}\<close>
742
743text \<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
793text %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
817subsection \<open>Sort hypotheses\<close>
818
819text \<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
843text %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
857text %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
862class empty =
863  assumes bad: "\<And>(x::'a) y. x \<noteq> y"
864
865theorem (in empty) false: False
866  using bad by blast
867
868ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
869
870text \<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
877section \<open>Object-level rules \label{sec:obj-rules}\<close>
878
879text \<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
890subsection \<open>Hereditary Harrop Formulae\<close>
891
892text \<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
949text %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
961subsection \<open>Rule composition\<close>
962
963text \<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
1020text %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
1064section \<open>Proof terms \label{sec:proof-terms}\<close>
1065
1066text \<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
1127subsection \<open>Reconstructing and checking proof terms\<close>
1128
1129text \<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
1145subsection \<open>Concrete syntax of proof terms\<close>
1146
1147text \<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
1185text %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
1250text %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
1258end
1259