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