(*:maxLineLen=78:*) theory Logicimports Basebegin chapter ‹ Primitive logic \label {ch:logic}› text ‹ cite ‹ paulson700› .‹ λHOL› '' in the more abstractcite ‹ "Barendregt-Geuvers:2001"› ,‹ λ› -calculus with corresponding arrows, ‹ ==> › for syntactic function space‹ ∧ › for universal quantification (proofs‹ ==> › for implication (proofs depending on proofs).🪙 ‹ This is the‹ Θ› is separate from the proof‹ Γ› of the core calculus: type constructors, term constants, and› › section ‹ Types \label {sec:types}› text ‹ 🪙 🪙 ‹ type class› is an abstract syntactic entity declared in the theory🪙 ‹ subclass relation› ‹ c1 ⊆ c2 › is specified by stating an🪙 ‹ sort› is a list of type classes written as ‹ s = {c1 … , cm › , it\ any class ‹ c› may be read as a sort‹ {c}› . The ordering on type classes is extended to sorts according to the‹ {c1 … cm ⊆ {d1 … , dn › iff ‹ ∀ j. ∃ i. ci ⊆ j › . The empty intersection ‹ {}› refers to the universal sort, which is the\ the sort order. Thus ‹ {}› represents the ``full\ the sort ordering.🪙 🪙 ‹ fixed type variable› is a pair of a basic name (starting with a ‹ '› \ ‹ ('a, s)› which is usually printed‹ αs › . A 🪙 ‹ schematic type variable› is a pair of an indexname and a sort\ ‹ (('a, 0), s)› which is usually printed as ‹ ?αs › .🪙 ‹ all› syntactic components contribute to the identity of type🪙 ‹ type constructor› ‹ κ› is a ‹ k› -ary operator on types declared in the‹ (α1 … , αk › .‹ k = 0› the argument tuple is omitted, e.g.\ ‹ prop› instead of ‹ ()prop› .‹ k = 1› the parentheses are omitted, e.g.\ ‹ α list› instead of‹ (α)list› . Further notation is provided for specific constructors, notably‹ α ==> › instead of ‹ (α, β)fun› .🪙 ‹ type› is defined inductively over type variables and‹ τ = αs s 1 … , τk › .🪙 ‹ type abbreviation› is a syntactic definition ‹ (🪙 α)κ = τ› of an‹ τ› over variables ‹ 🪙 α› . Type abbreviations🪙 ‹ type arity› declares the image behavior of a type constructor wrt.\ the‹ κ :: (s1 … , sk › means that ‹ (τ1 … , τk › is of‹ s› if every argument type ‹ τi › is of sort ‹ si › . Arity declarations\ ‹ κ :: (🪙 s)c› entails ‹ κ ::🪙 s)c'› for any ‹ c' 🪙 c› .🪙 🪙 ‹ coregular› , which means that type‹ κ› , and classes ‹ c1 ⊆ c2 › , and arities ‹ κ :: (🪙 s1 1 › and ‹ κ ::🪙 s2 2 › holds ‹ 🪙 s1 ⊆ 🪙 s2 › component-wise.‹ κ› and sort ‹ s› there is a most general vector of argument‹ (s1 … , sk › such that a type scheme ‹ (α1 … , αk › is of‹ s› . Consequently, type unification has most general solutions (modulocite ‹ "nipkow-prehofer"› .› text %mlref ‹ \begin {mldecls}\\ \\ \\ \\ \\ \\ \end {mldecls}\begin {mldecls}\\ \\ theory"} \\ \\ \\ \\ \\ \end {mldecls}🪙 Type 🪙 ‹ class› represents type classes.🪙 Type 🪙 ‹ sort› represents sorts, i.e.\ finite intersections of🪙 ‹ []: sort› refers to the empty class\ the ``full sort''.🪙 Type 🪙 ‹ arity› represents type arities. A triple ‹ (κ, 🪙 s, s)› represents ‹ κ :: (🪙 s)s› as described above.🪙 Type 🪙 ‹ typ› represents types; this is a datatype with constructors🪙 ‹ TFree› , 🪙 ‹ TVar› , 🪙 ‹ Type› .🪙 🪙 ‹ Term.map_atyps› ~‹ f τ› applies the mapping ‹ f› to all atomic types🪙 ‹ TFree› , 🪙 ‹ TVar› ) occurring in ‹ τ› .🪙 🪙 ‹ Term.fold_atyps› ~‹ f τ› iterates the operation ‹ f› over all🪙 ‹ TFree› , 🪙 ‹ TVar› ) in ‹ τ› ; the type🪙 🪙 ‹ Sign.subsort› ~‹ thy (s1 2 › tests the subsort relation ‹ s1 ⊆ 2 › .🪙 🪙 ‹ Sign.of_sort› ~‹ thy (τ, s)› tests whether type ‹ τ› is of sort ‹ s› .🪙 🪙 ‹ Sign.add_type› ~‹ ctxt (κ, k, mx)› declares a new type constructors ‹ κ› ‹ k› arguments and optional mixfix syntax.🪙 🪙 ‹ Sign.add_type_abbrev› ~‹ ctxt (κ, 🪙 α, τ)› defines a new type‹ (🪙 α)κ = τ› .🪙 🪙 ‹ Sign.primitive_class› ~‹ (c, [c1 … , cn › declares a new class ‹ c› ,‹ c ⊆ ci › , for ‹ i = 1, … , n› .🪙 🪙 ‹ Sign.primitive_classrel› ~‹ (c1 2 › declares the class relation‹ c1 ⊆ c2 › .🪙 🪙 ‹ Sign.primitive_arity› ~‹ (κ, 🪙 s, s)› declares the arity ‹ κ ::🪙 s)s› . › text %mlantiq ‹ \begin {matharray}{rcl}‹ ML_antiquotation› \\ ‹ ML_antiquotation› \\ ‹ ML_antiquotation› \\ ‹ ML_antiquotation› \\ ‹ ML_antiquotation› \\ ‹ ML_antiquotation› \\ ‹ ML_antiquotation› \\ ‹ ML_antiquotation› \\ \end {matharray}🪙 ‹ › 🪙 ‹ @{class c}› inlines the internalized class ‹ c› --- as 🪙 ‹ string› 🪙 ‹ @{sort s}› inlines the internalized sort ‹ s› --- as 🪙 ‹ string› literal.🪙 ‹ @{type_name c}› inlines the internalized type constructor ‹ c› --- as🪙 ‹ string› literal.🪙 ‹ @{type_abbrev c}› inlines the internalized type abbreviation ‹ c› --- as🪙 ‹ string› literal.🪙 ‹ @{nonterminal c}› inlines the internalized syntactic type~/ grammar‹ c› --- as 🪙 ‹ string› literal.🪙 ‹ @{typ τ}› inlines the internalized type ‹ τ› --- as constructor term for🪙 ‹ typ› .🪙 ‹ @{Type source}› refers to embedded source text to produce a type‹ source› follows the syntax category @{syntax type_const}🪙 ‹ @{Type_fn source}› is similar to ‹ @{Type source}› , but produces a partial🪙 ‹ syntax type_const} @'=>' @{syntax embedded_ml}syntax embedded} | @{syntax control_symbol} @{syntax embedded}› text provided as @{syntax embedded_ml} is treated as regular Isabelle/MLwith nested antiquotations. ML text that only consists of ain compact control-cartouche notation , can be writtentext (see the last example› text %mlex ‹ Here are some minimal examples for type constructor antiquotations . \ < close > ML \ < open > \ < comment > \ < open > type constructor without arguments : \ < close > val natT = \ < ^ Type > \ < open > nat \ < close > ; \ < comment > \ < open > type constructor with arguments : \ < close > fun mk_funT ( A , B ) = \ < ^ Type > \ < open > fun A B \ < close > ; \ < comment > \ < open > type constructor decomposition as partial function : \ < close > val dest_funT = \ < ^ Type_fn > \ < open > fun A B = > \ < open > ( A , B ) \ < close > \ < close > ; \ < comment > \ < open > nested type constructors : \ < close > fun mk_relT A = \ < ^ Type > \ < open > fun A \ < ^ Type > \ < open > fun A \ < ^ Type > \ < open > bool \ < close > \ < close > \ < close > ; \ < ^ assert > ( mk_relT natT = \ < ^ typ > \ < open > nat \ < Rightarrow > nat \ < Rightarrow > bool \ < close > ) ; \ < close > section \ < open > Terms \ label { sec : terms } \ < close > text \ < open > The language of terms is that of simply - typed \ < open > \ < lambda > \ < close > - calculus with de - Bruijn indices for bound variables ( cf . \ \ < ^ cite > \ < open > debruijn72 \ < close > or \ < ^ cite > \ < open > " paulson - ml2 " \ < close > ) , with the types being determined by the corresponding binders . In contrast , free variables and constants have an explicit name and type in each occurrence . \ < ^ medskip > A \ < ^ emph > \ < open > bound variable \ < close > is a natural number \ < open > b \ < close > , which accounts for the number of intermediate binders between the variable occurrence in the body and its binding position . For example , the de - Bruijn term \ < open > \ < lambda > \ < ^ bsub > bool \ < ^ esub > . \ < lambda > \ < ^ bsub > bool \ < ^ esub > . 1 \ < and > 0 \ < close > would correspond to \ < open > \ < lambda > x \ < ^ bsub > bool \ < ^ esub > . \ < lambda > y \ < ^ bsub > bool \ < ^ esub > . x \ < and > y \ < close > in a named representation . Note that a bound variable may be represented by different de - Bruijn indices at different occurrences , depending on the nesting of abstractions . A \ < ^ emph > \ < open > loose variable \ < close > is a bound variable that is outside the scope of local binders . The types ( and names ) for loose variables can be managed as a separate context , that is maintained as a stack of hypothetical binders . The core logic operates on closed terms , without any loose variables . A \ < ^ emph > \ < open > fixed variable \ < close > is a pair of a basic name and a type , e . g . \ \ < open > ( x , \ < tau > ) \ < close > which is usually printed \ < open > x \ < ^ sub > \ < tau > \ < close > here . A \ < ^ emph > \ < open > schematic variable \ < close > is a pair of an indexname and a type , e . g . \ \ < open > ( ( x , 0 ) , \ < tau > ) \ < close > which is likewise printed as \ < open > ? x \ < ^ sub > \ < tau > \ < close > . \ < ^ medskip > A \ < ^ emph > \ < open > constant \ < close > is a pair of a basic name and a type , e . g . \ \ < open > ( c , \ < tau > ) \ < close > which is usually printed as \ < open > c \ < ^ sub > \ < tau > \ < close > here . Constants are declared in the context as polymorphic families \ < open > c : : \ < sigma > \ < close > , meaning that all substitution instances \ < open > c \ < ^ sub > \ < tau > \ < close > for \ < open > \ < tau > = \ < sigma > \ < vartheta > \ < close > are valid . The vector of \ < ^ emph > \ < open > type arguments \ < close > of constant \ < open > c \ < ^ sub > \ < tau > \ < close > wrt . \ the declaration \ < open > c : : \ < sigma > \ < close > is defined as the codomain of the matcher \ < open > \ < vartheta > = { ? \ < alpha > \ < ^ sub > 1 \ < mapsto > \ < tau > \ < ^ sub > 1 , \ < dots > , ? \ < alpha > \ < ^ sub > n \ < mapsto > \ < tau > \ < ^ sub > n } \ < close > presented in canonical order \ < open > ( \ < tau > \ < ^ sub > 1 , \ < dots > , \ < tau > \ < ^ sub > n ) \ < close > , corresponding to the left - to - right occurrences of the \ < open > \ < alpha > \ < ^ sub > i \ < close > in \ < open > \ < sigma > \ < close > . Within a given theory context , there is a one - to - one correspondence between any constant \ < open > c \ < ^ sub > \ < tau > \ < close > and the application \ < open > c ( \ < tau > \ < ^ sub > 1 , \ < dots > , \ < tau > \ < ^ sub > n ) \ < close > of its type arguments . For example , with \ < open > plus : : \ < alpha > \ < Rightarrow > \ < alpha > \ < Rightarrow > \ < alpha > \ < close > , the instance \ < open > plus \ < ^ bsub > nat \ < Rightarrow > nat \ < Rightarrow > nat \ < ^ esub > \ < close > corresponds to \ < open > plus ( nat ) \ < close > . Constant declarations \ < open > c : : \ < sigma > \ < close > may contain sort constraints for type variables in \ < open > \ < sigma > \ < close > . These are observed by type - inference as expected , but \ < ^ emph > \ < open > ignored \ < close > by the core logic . This means the primitive logic is able to reason with instances of polymorphic constants that the user - level type - checker would reject due to violation of type class restrictions . \ < ^ medskip > An \ < ^ emph > \ < open > atomic term \ < close > is either a variable or constant . The logical category \ < ^ emph > \ < open > term \ < close > is defined inductively over atomic terms , with abstraction and 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 > . Parsing and printing takes care of converting between an external representation with named bound variables . Subsequently , we shall use the latter notation instead of internal de - Bruijn representation . The inductive relation \ < open > t : : \ < tau > \ < close > assigns a ( unique ) type to a term according to the structure of atomic terms , abstractions , and applications : \ [ \ infer { \ < open > a \ < ^ sub > \ < tau > : : \ < tau > \ < close > } { } \ qquad \ infer { \ < open > ( \ < lambda > x \ < ^ sub > \ < tau > . t ) : : \ < tau > \ < Rightarrow > \ < sigma > \ < close > } { \ < open > t : : \ < sigma > \ < close > } \ qquad \ infer { \ < open > t u : : \ < sigma > \ < close > } { \ < open > t : : \ < tau > \ < Rightarrow > \ < sigma > \ < close > & \ < open > u : : \ < tau > \ < close > } \ ] A \ < ^ emph > \ < open > well - typed term \ < close > is a term that can be typed according to these rules . Typing information can be omitted : type - inference is able to reconstruct the most general type of a raw term , while assigning most general types to all of its variables and constants . Type - inference depends on a context of type constraints for fixed variables , and declarations for polymorphic constants . The identity of atomic terms consists both of the name and the type component . This means that different variables \ < open > x \ < ^ bsub > \ < tau > \ < ^ sub > 1 \ < ^ esub > \ < close > and \ < open > x \ < ^ bsub > \ < tau > \ < ^ sub > 2 \ < ^ esub > \ < close > may become the same after type instantiation . Type - inference rejects variables of the same name , but different types . In contrast , mixed instances of polymorphic constants occur routinely . \ < ^ medskip > The \ < ^ emph > \ < open > hidden polymorphism \ < close > of a term \ < open > t : : \ < sigma > \ < close > is the set of type variables occurring in \ < open > t \ < close > , but not in its type \ < open > \ < sigma > \ < close > . This means that the term implicitly depends on type arguments that are not accounted in the result type , i . e . \ there are different type instances \ < open > t \ < vartheta > : : \ < sigma > \ < close > and \ < open > t \ < vartheta > ' : : \ < sigma > \ < close > with the same type . This slightly pathological situation notoriously demands additional care . \ < ^ medskip > A \ < ^ emph > \ < open > term abbreviation \ < close > is a syntactic definition \ < open > c \ < ^ sub > \ < sigma > \ < equiv > t \ < close > of a closed term \ < open > t \ < close > of type \ < open > \ < sigma > \ < close > , without any hidden polymorphism . A term abbreviation looks like a constant in the syntax , but is expanded before entering the logical core . Abbreviations are usually reverted when printing terms , using \ < open > t \ < rightarrow > c \ < ^ sub > \ < sigma > \ < close > as rules for higher - order rewriting . \ < ^ medskip > Canonical operations on \ < open > \ < lambda > \ < close > - terms include \ < open > \ < alpha > \ < beta > \ < eta > \ < close > - conversion : \ < open > \ < alpha > \ < close > - conversion refers to capture - free renaming of bound variables ; \ < open > \ < beta > \ < close > - conversion contracts an abstraction applied to an argument term , substituting the argument in the body : \ < open > ( \ < lambda > x . b ) a \ < close > becomes \ < open > b [ a / x ] \ < close > ; \ < open > \ < eta > \ < close > - conversion contracts vacuous application - abstraction : \ < open > \ < lambda > x . f x \ < close > becomes \ < open > f \ < close > , provided that the bound variable does not occur in \ < open > f \ < close > . Terms are normally treated modulo \ < open > \ < alpha > \ < close > - conversion , which is implicit in the de - Bruijn representation . Names for bound variables in abstractions are maintained separately as ( meaningless ) comments , mostly for parsing and printing . Full \ < open > \ < alpha > \ < beta > \ < eta > \ < close > - conversion is commonplace in various standard operations ( \ secref { sec : obj - rules } ) that are based on higher - order unification and matching . \ < close > text % mlref \ < open > \ begin { mldecls } @ { define_ML_type term } \ \ @ { define_ML_infix " aconv " : " term * term - > bool " } \ \ @ { define_ML Term . map_types : " ( typ - > typ ) - > term - > term " } \ \ @ { define_ML Term . fold_types : " ( typ - > ' a - > ' a ) - > term - > ' a - > ' a " } \ \ @ { define_ML Term . map_aterms : " ( term - > term ) - > term - > term " } \ \ @ { define_ML Term . fold_aterms : " ( term - > ' a - > ' a ) - > term - > ' a - > ' a " } \ \ \ end { mldecls } \ begin { mldecls } @ { define_ML fastype_of : " term - > typ " } \ \ @ { define_ML lambda : " term - > term - > term " } \ \ @ { define_ML betapply : " term * term - > term " } \ \ @ { define_ML incr_boundvars : " int - > term - > term " } \ \ @ { define_ML Sign . declare_const : " Proof . context - > ( binding * typ ) * mixfix - > theory - > term * theory " } \ \ @ { define_ML Sign . add_abbrev : " string - > binding * term - > theory - > ( term * term ) * theory " } \ \ @ { define_ML Sign . const_typargs : " theory - > string * typ - > typ list " } \ \ @ { define_ML Sign . const_instance : " theory - > string * typ list - > typ " } \ \ \ end { mldecls } \ < ^ descr > Type \ < ^ ML_type > \ < open > term \ < close > represents de - Bruijn terms , with comments in abstractions , and explicitly named free variables and constants ; this is a datatype with constructors @ { define_ML Bound } , @ { define_ML Free } , @ { define_ML Var } , @ { define_ML Const } , @ { define_ML Abs } , @ { define_ML_infix " $ " } . \ < ^ descr > \ < open > t \ < close > ~ \ < ^ ML_text > \ < open > aconv \ < close > ~ \ < open > u \ < close > checks \ < open > \ < alpha > \ < close > - equivalence of two terms . This is the basic equality relation on type \ < ^ ML_type > \ < open > term \ < close > ; raw datatype equality should only be used for operations related to parsing or printing ! \ < ^ descr > \ < ^ ML > \ < open > Term . map_types \ < close > ~ \ < open > f t \ < close > applies the mapping \ < open > f \ < close > to all types occurring in \ < open > t \ < close > . \ < ^ descr > \ < ^ ML > \ < open > Term . fold_types \ < close > ~ \ < open > f t \ < close > iterates the operation \ < open > f \ < close > over all occurrences of types in \ < open > t \ < close > ; the term structure is traversed from left to right . \ < ^ descr > \ < ^ ML > \ < open > Term . map_aterms \ < close > ~ \ < open > f t \ < close > applies the mapping \ < open > f \ < close > to all atomic terms ( \ < ^ ML > \ < open > Bound \ < close > , \ < ^ ML > \ < open > Free \ < close > , \ < ^ ML > \ < open > Var \ < close > , \ < ^ ML > \ < open > Const \ < close > ) occurring in \ < open > t \ < close > . \ < ^ descr > \ < ^ ML > \ < open > Term . fold_aterms \ < close > ~ \ < open > f t \ < close > iterates the operation \ < open > f \ < close > over all occurrences of atomic terms ( \ < ^ ML > \ < open > Bound \ < close > , \ < ^ ML > \ < open > Free \ < close > , \ < ^ ML > \ < open > Var \ < close > , \ < ^ ML > \ < open > Const \ < close > ) in \ < open > t \ < close > ; the term structure is traversed from left to right . \ < ^ descr > \ < ^ ML > \ < open > fastype_of \ < close > ~ \ < open > t \ < close > determines the type of a well - typed term . This operation is relatively slow , despite the omission of any sanity checks . \ < ^ descr > \ < ^ ML > \ < open > lambda \ < close > ~ \ < open > a b \ < close > produces an abstraction \ < open > \ < lambda > a . b \ < close > , where occurrences of the atomic term \ < open > a \ < close > in the body \ < open > b \ < close > are replaced by bound variables . \ < ^ descr > \ < ^ ML > \ < open > betapply \ < close > ~ \ < open > ( t , u ) \ < close > produces an application \ < open > t u \ < close > , with topmost \ < open > \ < beta > \ < close > - conversion if \ < open > t \ < close > is an abstraction . \ < ^ descr > \ < ^ ML > \ < open > incr_boundvars \ < close > ~ \ < open > j \ < close > increments a term ' s dangling bound variables by the offset \ < open > j \ < close > . This is required when moving a subterm into a context where it is enclosed by a different number of abstractions . Bound variables with a matching abstraction are unaffected . \ < ^ descr > \ < ^ ML > \ < open > Sign . declare_const \ < close > ~ \ < open > ctxt ( ( c , \ < sigma > ) , mx ) \ < close > declares a new constant \ < open > c : : \ < sigma > \ < close > with optional mixfix syntax . \ < ^ descr > \ < ^ ML > \ < open > Sign . add_abbrev \ < close > ~ \ < open > print_mode ( c , t ) \ < close > introduces a new term abbreviation \ < open > c \ < equiv > t \ < close > . \ < ^ descr > \ < ^ ML > \ < open > Sign . const_typargs \ < close > ~ \ < open > thy ( c , \ < tau > ) \ < close > and \ < ^ ML > \ < open > Sign . const_instance \ < close > ~ \ < open > thy ( c , [ \ < tau > \ < ^ sub > 1 , \ < dots > , \ < tau > \ < ^ sub > n ] ) \ < close > convert between two representations of polymorphic constants : full type instance vs . \ compact type arguments form . \ < close > text % mlantiq \ < open > \ begin { matharray } { rcl } @ { ML_antiquotation_def " const_name " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " const_abbrev " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " const " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " term " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " prop " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " Const " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " Const_ " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " Const_fn " } & : & \ < open > ML_antiquotation \ < close > \ \ \ end { matharray } \ < ^ rail > \ < open > ( @ @ { ML_antiquotation const_name } | @ @ { ML_antiquotation const_abbrev } ) embedded ; @ @ { ML_antiquotation const } ( ' ( ' ( type + ' , ' ) ' ) ' ) ? ; @ @ { ML_antiquotation term } term ; @ @ { ML_antiquotation prop } prop ; ( @ @ { ML_antiquotation Const } | @ @ { ML_antiquotation Const_ } | @ @ { ML_antiquotation Const_fn } ) embedded \ < close > \ < ^ descr > \ < open > @ { const_name c } \ < close > inlines the internalized logical constant name \ < open > c \ < close > - - - as \ < ^ ML_type > \ < open > string \ < close > literal . \ < ^ descr > \ < open > @ { const_abbrev c } \ < close > inlines the internalized abbreviated constant name \ < open > c \ < close > - - - as \ < ^ ML_type > \ < open > string \ < close > literal . \ < ^ descr > \ < open > @ { const c ( \ < ^ vec > \ < tau > ) } \ < close > inlines the internalized constant \ < open > c \ < close > with precise type instantiation in the sense of \ < ^ ML > \ < open > Sign . const_instance \ < close > - - - as \ < ^ ML > \ < open > Const \ < close > constructor term for datatype \ < ^ ML_type > \ < open > term \ < close > . \ < ^ descr > \ < open > @ { term t } \ < close > inlines the internalized term \ < open > t \ < close > - - - as constructor term for datatype \ < ^ ML_type > \ < open > term \ < close > . \ < ^ descr > \ < open > @ { prop \ < phi > } \ < close > inlines the internalized proposition \ < open > \ < phi > \ < close > - - - as constructor term for datatype \ < ^ ML_type > \ < open > term \ < close > . \ < ^ descr > \ < open > @ { Const source } \ < close > refers to embedded source text to produce a term constructor with name ( formally checked ) , type arguments and term arguments ( inlined ML text ) . The embedded \ < open > source \ < close > follows the syntax category @ { syntax term_const } defined below , using @ { syntax embedded_ml } from antiquotation @ { ML_antiquotation Type } ( \ secref { sec : types } ) . \ < ^ descr > \ < open > @ { Const_ source } \ < close > is similar to \ < open > @ { Const source } \ < close > for patterns instead of closed values . This distinction is required due to redundant type information within term constants : subtrees with duplicate ML pattern variable need to be suppressed ( replaced by dummy patterns ) . The embedded \ < open > source \ < close > follows the syntax category @ { syntax term_const } defined below . \ < ^ descr > \ < open > @ { Const_fn source } \ < close > is similar to \ < open > @ { Const_ source } \ < close > , but produces a proper \ < ^ verbatim > \ < open > fn \ < close > expression with function body . The embedded \ < open > source \ < close > follows the syntax category @ { syntax term_const_fn } defined below . \ < ^ rail > \ < open > @ { syntax_def term_const } : syntax for_args})?syntax term_const} @'=>' @{syntax embedded_ml}for ' (@{syntax embedded_ml}+)› › text %mlex ‹ Here are some minimal examples for term constant antiquotations . Type arguments for constants are analogous to type constructors ( \ secref { sec : types } ) . Term arguments are different : a flexible number of arguments is inserted via curried applications ( \ < ^ ML > \ < open > op $ \ < close > ) . \ < close > ML \ < open > \ < comment > \ < open > constant without type argument : \ < close > fun mk_conj ( A , B ) = \ < ^ Const > \ < open > conj for A B \ < close > ; val dest_conj = \ < ^ Const_fn > \ < open > conj for A B = > \ < open > ( A , B ) \ < close > \ < close > ; \ < comment > \ < open > constant with type argument : \ < close > fun mk_eq T ( t , u ) = \ < ^ Const > \ < open > HOL . eq T for t u \ < close > ; val dest_eq = \ < ^ Const_fn > \ < open > HOL . eq T for t u = > \ < open > ( T , ( t , u ) ) \ < close > \ < close > ; \ < comment > \ < open > constant with variable number of term arguments : \ < close > val c = Const ( \ < ^ const_name > \ < open > conj \ < close > , \ < ^ typ > \ < open > bool \ < Rightarrow > bool \ < Rightarrow > bool \ < close > ) ; val P = \ < ^ term > \ < open > P : : bool \ < close > ; val Q = \ < ^ term > \ < open > Q : : bool \ < close > ; \ < ^ assert > ( \ < ^ Const > \ < open > conj \ < close > = c ) ; \ < ^ assert > ( \ < ^ Const > \ < open > conj for P \ < close > = c $ P ) ; \ < ^ assert > ( \ < ^ Const > \ < open > conj for P Q \ < close > = c $ P $ Q ) ; \ < close > section \ < open > Theorems \ label { sec : thms } \ < close > text \ < open > A \ < ^ emph > \ < open > proposition \ < close > is a well - typed term of type \ < open > prop \ < close > , a \ < ^ emph > \ < open > theorem \ < close > is a proven proposition ( depending on a context of hypotheses and the background theory ) . Primitive inferences include plain Natural Deduction rules for the primary connectives \ < open > \ < And > \ < close > and \ < open > \ < Longrightarrow > \ < close > of the framework . There is also a builtin notion of equality / equivalence \ < open > \ < equiv > \ < close > . \ < close > subsection \ < open > Primitive connectives and rules \ label { sec : prim - rules } \ < close > text \ < open > The theory \ < open > Pure \ < close > contains constant declarations for the primitive connectives \ < open > \ < And > \ < close > , \ < open > \ < Longrightarrow > \ < close > , and \ < open > \ < equiv > \ < close > of the logical framework , see \ figref { fig : pure - connectives } . The derivability judgment \ < open > A \ < ^ sub > 1 , \ < dots > , A \ < ^ sub > n \ < turnstile > B \ < close > is defined inductively by the primitive inferences given in \ figref { fig : prim - rules } , with the global restriction that the hypotheses must \ < ^ emph > \ < open > not \ < close > contain any schematic variables . The builtin equality is conceptually axiomatized as shown in \ figref { fig : pure - equality } , although the implementation works directly with derived inferences . \ begin { figure } [ htb ] \ begin { center } \ begin { tabular } { ll } \ < open > all : : ( \ < alpha > \ < Rightarrow > prop ) \ < Rightarrow > prop \ < close > & universal quantification ( binder \ < open > \ < And > \ < close > ) \ \ \ < open > \ < Longrightarrow > : : prop \ < Rightarrow > prop \ < Rightarrow > prop \ < close > & implication ( right associative infix ) \ \ \ < open > \ < equiv > : : \ < alpha > \ < Rightarrow > \ < alpha > \ < Rightarrow > prop \ < close > & equality relation ( infix ) \ \ \ end { tabular } \ caption { Primitive connectives of Pure } \ label { fig : pure - connectives } \ end { center } \ end { figure } \ begin { figure } [ htb ] \ begin { center } \ [ \ infer [ \ < open > ( axiom ) \ < close > ] { \ < open > \ < turnstile > A \ < close > } { \ < open > A \ < in > \ < Theta > \ < close > } \ qquad \ infer [ \ < open > ( assume ) \ < close > ] { \ < open > A \ < turnstile > A \ < close > } { } \ ] \ [ \ 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 > } \ qquad \ infer [ \ < open > ( \ < And > \ < hyphen > elim ) \ < close > ] { \ < open > \ < Gamma > \ < turnstile > B [ a ] \ < close > } { \ < open > \ < Gamma > \ < turnstile > \ < And > x . B [ x ] \ < close > } \ ] \ [ \ infer [ \ < open > ( \ < Longrightarrow > \ < hyphen > intro ) \ < close > ] { \ < open > \ < Gamma > - A \ < turnstile > A \ < Longrightarrow > B \ < close > } { \ < open > \ < Gamma > \ < turnstile > B \ < close > } \ qquad \ 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 > } \ ] \ caption { Primitive inferences of Pure } \ label { fig : prim - rules } \ end { center } \ end { figure } \ begin { figure } [ htb ] \ begin { center } \ begin { tabular } { ll } \ < open > \ < turnstile > ( \ < lambda > x . b [ x ] ) a \ < equiv > b [ a ] \ < close > & \ < open > \ < beta > \ < close > - conversion \ \ \ < open > \ < turnstile > x \ < equiv > x \ < close > & reflexivity \ \ \ < open > \ < turnstile > x \ < equiv > y \ < Longrightarrow > P x \ < Longrightarrow > P y \ < close > & substitution \ \ \ < open > \ < turnstile > ( \ < And > x . f x \ < equiv > g x ) \ < Longrightarrow > f \ < equiv > g \ < close > & extensionality \ \ \ < open > \ < turnstile > ( A \ < Longrightarrow > B ) \ < Longrightarrow > ( B \ < Longrightarrow > A ) \ < Longrightarrow > A \ < equiv > B \ < close > & logical equivalence \ \ \ end { tabular } \ caption { Conceptual axiomatization of Pure equality } \ label { fig : pure - equality } \ end { center } \ end { figure } The introduction and elimination rules for \ < open > \ < And > \ < close > and \ < open > \ < Longrightarrow > \ < close > are analogous to formation of dependently typed \ < open > \ < lambda > \ < close > - terms representing the underlying proof objects . Proof terms are irrelevant in the Pure logic , though ; they cannot occur within propositions . The system provides a runtime option to record explicit proof terms for primitive inferences , see also \ secref { sec : proof - terms } . Thus all three levels of \ < open > \ < lambda > \ < close > - calculus become explicit : \ < open > \ < Rightarrow > \ < close > for terms , and \ < open > \ < And > / \ < Longrightarrow > \ < close > for proofs ( cf . \ \ < ^ cite > \ < open > " Berghofer - Nipkow : 2000 : TPHOL " \ < close > ) . Observe that locally fixed parameters ( as in \ < open > \ < And > \ < hyphen > intro \ < close > ) need not be recorded in the hypotheses , because the simple syntactic types of Pure are always inhabitable . ` ` Assumptions ' ' \ < open > x : : \ < tau > \ < close > for type - membership are only present as long as some \ < open > x \ < ^ sub > \ < tau > \ < close > occurs in the statement body . \ < ^ footnote > \ < open > This is the key difference to ` ` \ < open > \ < lambda > HOL \ < close > ' ' in the PTS framework \ < ^ cite > \ < open > " Barendregt - Geuvers : 2001 " \ < close > , where hypotheses \ < open > x : A \ < close > are treated uniformly for propositions and types . \ < close > \ < ^ medskip > The axiomatization of a theory is implicitly closed by forming all instances of type and term variables : \ < open > \ < turnstile > A \ < vartheta > \ < close > holds for any substitution instance of an axiom \ < open > \ < turnstile > A \ < close > . By pushing substitutions through derivations inductively , we also get admissible \ < open > generalize \ < close > and \ < open > instantiate \ < close > rules as shown in \ figref { fig : subst - rules } . \ begin { figure } [ htb ] \ begin { center } \ [ \ infer { \ < open > \ < Gamma > \ < turnstile > B [ ? \ < alpha > ] \ < close > } { \ < open > \ < Gamma > \ < turnstile > B [ \ < alpha > ] \ < close > & \ < open > \ < alpha > \ < notin > \ < Gamma > \ < close > } \ quad \ infer [ \ quad \ < open > ( generalize ) \ < close > ] { \ < open > \ < Gamma > \ < turnstile > B [ ? x ] \ < close > } { \ < open > \ < Gamma > \ < turnstile > B [ x ] \ < close > & \ < open > x \ < notin > \ < Gamma > \ < close > } \ ] \ [ \ infer { \ < open > \ < Gamma > \ < turnstile > B [ \ < tau > ] \ < close > } { \ < open > \ < Gamma > \ < turnstile > B [ ? \ < alpha > ] \ < close > } \ quad \ infer [ \ quad \ < open > ( instantiate ) \ < close > ] { \ < open > \ < Gamma > \ < turnstile > B [ t ] \ < close > } { \ < open > \ < Gamma > \ < turnstile > B [ ? x ] \ < close > } \ ] \ caption { Admissible substitution rules } \ label { fig : subst - rules } \ end { center } \ end { figure } Note that \ < open > instantiate \ < close > does not require an explicit side - condition , because \ < open > \ < Gamma > \ < close > may never contain schematic variables . In principle , variables could be substituted in hypotheses as well , but this would disrupt the monotonicity of reasoning : deriving \ < open > \ < Gamma > \ < vartheta > \ < turnstile > B \ < vartheta > \ < close > from \ < open > \ < Gamma > \ < turnstile > B \ < close > is correct , but \ < open > \ < Gamma > \ < vartheta > \ < supseteq > \ < Gamma > \ < close > does not necessarily hold : the result belongs to a different proof context . \ < ^ medskip > An \ < ^ emph > \ < open > oracle \ < close > is a function that produces axioms on the fly . Logically , this is an instance of the \ < open > axiom \ < close > rule ( \ figref { fig : prim - rules } ) , but there is an operational difference . The inference kernel records oracle invocations within derivations of theorems by a unique tag . This also includes implicit type - class reasoning via the order - sorted algebra of class relations and type arities ( see also @ { command_ref instantiation } and @ { command_ref instance } ) . Axiomatizations should be limited to the bare minimum , typically as part of the initial logical basis of an object - logic formalization . Later on , theories are usually developed in a strictly definitional fashion , by stating only certain equalities over new constants . A \ < ^ emph > \ < open > simple definition \ < close > consists of a constant declaration \ < open > c : : \ < sigma > \ < close > together with an axiom \ < open > \ < turnstile > c \ < equiv > t \ < close > , where \ < open > t : : \ < sigma > \ < close > is a closed term without any hidden polymorphism . The RHS may depend on further defined constants , but not \ < open > c \ < close > itself . Definitions of functions may be presented as \ < open > c \ < ^ vec > x \ < equiv > t \ < close > instead of the puristic \ < open > c \ < equiv > \ < lambda > \ < ^ vec > x . t \ < close > . An \ < ^ emph > \ < open > overloaded definition \ < close > consists of a collection of axioms for the same constant , with zero or one equations \ < open > c ( ( \ < ^ vec > \ < alpha > ) \ < kappa > ) \ < equiv > t \ < close > for each type constructor \ < open > \ < kappa > \ < close > ( for distinct variables \ < open > \ < ^ vec > \ < alpha > \ < close > ) . The RHS may mention previously defined constants as above , or arbitrary constants \ < open > d ( \ < alpha > \ < ^ sub > i ) \ < close > for some \ < open > \ < alpha > \ < ^ sub > i \ < close > projected from \ < open > \ < ^ vec > \ < alpha > \ < close > . Thus overloaded definitions essentially work by primitive recursion over the syntactic structure of a single type argument . See also \ < ^ cite > \ < open > \ < open > \ S4 . 3 \ < close > in " Haftmann - Wenzel : 2006 : classes " \ < close > . \ < close > text % mlref \ < open > \ begin { mldecls } @ { define_ML Logic . all : " term - > term - > term " } \ \ @ { define_ML Logic . mk_implies : " term * term - > term " } \ \ \ end { mldecls } \ begin { mldecls } @ { define_ML_type ctyp } \ \ @ { define_ML_type cterm } \ \ @ { define_ML Thm . ctyp_of : " Proof . context - > typ - > ctyp " } \ \ @ { define_ML Thm . cterm_of : " Proof . context - > term - > cterm " } \ \ @ { define_ML Thm . apply : " cterm - > cterm - > cterm " } \ \ @ { define_ML Thm . lambda : " cterm - > cterm - > cterm " } \ \ @ { define_ML Thm . all : " Proof . context - > cterm - > cterm - > cterm " } \ \ @ { define_ML Drule . mk_implies : " cterm * cterm - > cterm " } \ \ \ end { mldecls } \ begin { mldecls } @ { define_ML_type thm } \ \ @ { define_ML Thm . transfer : " theory - > thm - > thm " } \ \ @ { define_ML Thm . assume : " cterm - > thm " } \ \ @ { define_ML Thm . forall_intr : " cterm - > thm - > thm " } \ \ @ { define_ML Thm . forall_elim : " cterm - > thm - > thm " } \ \ @ { define_ML Thm . implies_intr : " cterm - > thm - > thm " } \ \ @ { define_ML Thm . implies_elim : " thm - > thm - > thm " } \ \ @ { define_ML Thm . generalize : " Names . set * Names . set - > int - > thm - > thm " } \ \ @ { define_ML Thm . instantiate : " ctyp TVars . table * cterm Vars . table - > thm - > thm " } \ \ @ { define_ML Thm . add_axiom : " Proof . context - > binding * term - > theory - > ( string * thm ) * theory " } \ \ @ { define_ML Thm . add_oracle : " binding * ( ' a - > cterm ) - > theory - > ( string * ( ' a - > thm ) ) * theory " } \ \ @ { define_ML Thm . add_def : " Defs . context - > bool - > bool - > binding * term - > theory - > ( string * thm ) * theory " } \ \ \ end { mldecls } \ begin { mldecls } @ { define_ML Theory . add_deps : " Defs . context - > string - > Defs . entry - > Defs . entry list - > theory - > theory " } \ \ @ { define_ML Thm_Deps . all_oracles : " thm list - > Proofterm . oracle list " } \ \ \ end { mldecls } \ < ^ descr > \ < ^ ML > \ < open > Logic . all \ < close > ~ \ < open > a B \ < close > produces a Pure quantification \ < open > \ < And > a . B \ < close > , where occurrences of the atomic term \ < open > a \ < close > in the body proposition \ < open > B \ < close > are replaced by bound variables . ( See also \ < ^ ML > \ < open > lambda \ < close > on terms . ) \ < ^ descr > \ < ^ ML > \ < open > Logic . mk_implies \ < close > ~ \ < open > ( A , B ) \ < close > produces a Pure implication \ < open > A \ < Longrightarrow > B \ < close > . \ < ^ descr > Types \ < ^ ML_type > \ < open > ctyp \ < close > and \ < ^ ML_type > \ < open > cterm \ < close > represent certified types and terms , respectively . These are abstract datatypes that guarantee that its values have passed the full well - formedness ( and well - typedness ) checks , relative to the declarations of type constructors , constants etc . \ in the background theory . The abstract types \ < ^ ML_type > \ < open > ctyp \ < close > and \ < ^ ML_type > \ < open > cterm \ < close > are part of the same inference kernel that is mainly responsible for \ < ^ ML_type > \ < open > thm \ < close > . Thus syntactic operations on \ < ^ ML_type > \ < open > ctyp \ < close > and \ < ^ ML_type > \ < open > cterm \ < close > are located in the \ < ^ ML_structure > \ < open > Thm \ < close > module , even though theorems are not yet involved at that stage . \ < ^ descr > \ < ^ ML > \ < open > Thm . ctyp_of \ < close > ~ \ < open > ctxt \ < tau > \ < close > and \ < ^ ML > \ < open > Thm . cterm_of \ < close > ~ \ < open > ctxt t \ < close > explicitly check types and terms , respectively . This also involves some basic normalizations , such expansion of type and term abbreviations from the underlying theory context . Full re - certification is relatively slow and should be avoided in tight reasoning loops . \ < ^ descr > \ < ^ ML > \ < open > Thm . apply \ < close > , \ < ^ ML > \ < open > Thm . lambda \ < close > , \ < ^ ML > \ < open > Thm . all \ < close > , \ < ^ ML > \ < open > Drule . mk_implies \ < close > etc . \ compose certified terms ( or propositions ) incrementally . This is equivalent to \ < ^ ML > \ < open > Thm . cterm_of \ < close > after unchecked \ < ^ ML_infix > \ < open > $ \ < close > , \ < ^ ML > \ < open > lambda \ < close > , \ < ^ ML > \ < open > Logic . all \ < close > , \ < ^ ML > \ < open > Logic . mk_implies \ < close > etc . , but there can be a big difference in performance when large existing entities are composed by a few extra constructions on top . There are separate operations to decompose certified terms and theorems to produce certified terms again . \ < ^ descr > Type \ < ^ ML_type > \ < open > thm \ < close > represents proven propositions . This is an abstract datatype that guarantees that its values have been constructed by basic principles of the \ < ^ ML_structure > \ < open > Thm \ < close > module . Every \ < ^ ML_type > \ < open > thm \ < close > value refers its background theory , cf . \ \ secref { sec : context - theory } . \ < ^ descr > \ < ^ ML > \ < open > Thm . transfer \ < close > ~ \ < open > thy thm \ < close > transfers the given theorem to a \ < ^ emph > \ < open > larger \ < close > theory , see also \ secref { sec : context } . This formal adjustment of the background context has no logical significance , but is occasionally required for formal reasons , e . g . \ when theorems that are imported from more basic theories are used in the current situation . \ < ^ descr > \ < ^ ML > \ < open > Thm . assume \ < close > , \ < ^ ML > \ < open > Thm . forall_intr \ < close > , \ < ^ ML > \ < open > Thm . forall_elim \ < close > , \ < ^ ML > \ < open > Thm . implies_intr \ < close > , and \ < ^ ML > \ < open > Thm . implies_elim \ < close > correspond to the primitive inferences of \ figref { fig : prim - rules } . \ < ^ descr > \ < ^ ML > \ < open > Thm . generalize \ < close > ~ \ < open > ( \ < ^ vec > \ < alpha > , \ < ^ vec > x ) \ < close > corresponds to the \ < open > generalize \ < close > rules of \ figref { fig : subst - rules } . Here collections of type and term variables are generalized simultaneously , specified by the given sets of basic names . \ < ^ descr > \ < ^ ML > \ < open > Thm . instantiate \ < close > ~ \ < open > ( \ < ^ vec > \ < alpha > \ < ^ sub > s , \ < ^ vec > x \ < ^ sub > \ < tau > ) \ < close > corresponds to the \ < open > instantiate \ < close > rules of \ figref { fig : subst - rules } . Type variables are substituted before term variables . Note that the types in \ < open > \ < ^ vec > x \ < ^ sub > \ < tau > \ < close > refer to the instantiated versions . \ < ^ descr > \ < ^ ML > \ < open > Thm . add_axiom \ < close > ~ \ < open > ctxt ( name , A ) \ < close > declares an arbitrary proposition as axiom , and retrieves it as a theorem from the resulting theory , cf . \ \ < open > axiom \ < close > in \ figref { fig : prim - rules } . Note that the low - level representation in the axiom table may differ slightly from the returned theorem . \ < ^ descr > \ < ^ ML > \ < open > Thm . add_oracle \ < close > ~ \ < open > ( binding , oracle ) \ < close > produces a named oracle rule , essentially generating arbitrary axioms on the fly , cf . \ \ < open > axiom \ < close > in \ figref { fig : prim - rules } . \ < ^ descr > \ < ^ ML > \ < open > Thm . add_def \ < close > ~ \ < open > ctxt unchecked overloaded ( name , c \ < ^ vec > x \ < equiv > t ) \ < close > states a definitional axiom for an existing constant \ < open > c \ < close > . Dependencies are recorded via \ < ^ ML > \ < open > Theory . add_deps \ < close > , unless the \ < open > unchecked \ < close > option is set . Note that the low - level representation in the axiom table may differ slightly from the returned theorem . \ < ^ descr > \ < ^ ML > \ < open > Theory . add_deps \ < close > ~ \ < open > ctxt name c \ < ^ sub > \ < tau > \ < ^ vec > d \ < ^ sub > \ < sigma > \ < close > declares dependencies of a named specification for constant \ < open > c \ < ^ sub > \ < tau > \ < close > , relative to existing specifications for constants \ < open > \ < ^ vec > d \ < ^ sub > \ < sigma > \ < close > . This also works for type constructors . \ < ^ descr > \ < ^ ML > \ < open > Thm_Deps . all_oracles \ < close > ~ \ < open > thms \ < close > returns all oracles used in the internal derivation of the given theorems ; this covers the full graph of transitive dependencies . The result contains an authentic oracle name ; if @ { ML Proofterm . proofs } was at least @ { ML 1 } during the oracle inference , it also contains the position of the oracle invocation and its proposition . See also the command @ { command_ref " thm_oracles " } . \ < close > text % mlantiq \ < open > \ begin { matharray } { rcl } @ { ML_antiquotation_def " ctyp " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " cterm " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " cprop " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " thm " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " thms " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " lemma " } & : & \ < open > ML_antiquotation \ < close > \ \ @ { ML_antiquotation_def " oracle_name " } & : & \ < open > ML_antiquotation \ < close > \ \ \ end { matharray } \ < ^ rail > \ < open > @ @ { ML_antiquotation ctyp } typ ; @ @ { ML_antiquotation cterm } term ; @ @ { ML_antiquotation cprop } prop ; @ @ { ML_antiquotation thm } thm ; @ @ { ML_antiquotation thms } thms ; @ @ { ML_antiquotation lemma } @ { syntax embedded_lemma } ; @ { syntax_def embedded_lemma } ( ' ( ' @ ' open ' ' ) ' ) ? ( ( prop + ) + @ ' and ' ) \ < newline > @ { syntax for_fixes } @ ' by ' method method ? ; @ @ { ML_antiquotation oracle_name } embedded \ < close > \ < ^ descr > \ < open > @ { ctyp \ < tau > } \ < close > produces a certified type wrt . \ the current background theory - - - as abstract value of type \ < ^ ML_type > \ < open > ctyp \ < close > . \ < ^ descr > \ < open > @ { cterm t } \ < close > and \ < open > @ { cprop \ < phi > } \ < close > produce a certified term wrt . \ the current background theory - - - as abstract value of type \ < ^ ML_type > \ < open > cterm \ < close > . \ < ^ descr > \ < open > @ { thm a } \ < close > produces a singleton fact - - - as abstract value of type \ < ^ ML_type > \ < open > thm \ < close > . \ < ^ descr > \ < open > @ { thms a } \ < close > produces a general fact - - - as abstract value of type \ < ^ ML_type > \ < open > thm list \ < close > . \ < ^ descr > \ < open > @ { lemma \ < phi > by meth } \ < close > produces a fact that is proven on the spot according to the minimal proof , which imitates a terminal Isar proof . The result is an abstract value of type \ < ^ ML_type > \ < open > thm \ < close > or \ < ^ ML_type > \ < open > thm list \ < close > , depending on the number of propositions given here . The internal derivation object lacks a proper theorem name , but it is formally closed , unless the \ < open > ( open ) \ < close > option is specified ( this may impact performance of applications with proof terms ) . Since ML antiquotations are always evaluated at compile - time , there is no run - time overhead even for non - trivial proofs . Nonetheless , the justification is syntactically limited to a single @ { command " by " } step . More complex Isar proofs should be done in regular theory source , before compiling the corresponding ML text that uses the result . \ < ^ descr > \ < open > @ { oracle_name a } \ < close > inlines the internalized oracle name \ < open > a \ < close > - - - as \ < ^ ML_type > \ < open > string \ < close > literal . \ < close > subsection \ < open > Auxiliary connectives \ label { sec : logic - aux } \ < close > text \ < open > Theory \ < open > Pure \ < close > provides a few auxiliary connectives that are defined on top of the primitive ones , see \ figref { fig : pure - aux } . These special constants are useful in certain internal encodings , and are normally not directly exposed to the user . \ begin { figure } [ htb ] \ begin { center } \ begin { tabular } { ll } \ < open > conjunction : : prop \ < Rightarrow > prop \ < Rightarrow > prop \ < close > & ( infix \ < open > &>& & \ < close > ) \ \ \ < open > \ < turnstile > A & & & B \ < equiv > ( \ < And > C . ( A \ < Longrightarrow > B \ < Longrightarrow > C ) \ < Longrightarrow > C ) \ < close > \ \ [ 1 ex ] \ < open > prop : : prop \ < Rightarrow > prop \ < close > & ( prefix \ < open > # \ < close > , suppressed ) \ \ \ < open > # A \ < equiv > A \ < close > \ \ [ 1 ex ] \ < open > term : : \ < alpha > \ < Rightarrow > prop \ < close > & ( prefix \ < open > TERM \ < close > ) \ \ \ < open > term x \ < equiv > ( \ < And > A . A \ < Longrightarrow > A ) \ < close > \ \ [ 1 ex ] \ < open > type : : \ < alpha > itself \ < close > & ( prefix \ < open > TYPE \ < close > ) \ \ \ < open > ( unspecified ) \ < close > \ \ \ end { tabular } \ caption { Definitions of auxiliary connectives } \ label { fig : pure - aux } \ end { center } \ end { figure } The introduction \ < open > A \ < Longrightarrow > B \ < Longrightarrow > A & & & B \ < close > , and eliminations ( projections ) \ < open > A & & & B \ < Longrightarrow > A \ < close > and \ < open > A & & & B \ < Longrightarrow > B \ < close > are available as derived rules . Conjunction allows to treat simultaneous assumptions and conclusions uniformly , e . g . \ consider \ < open > A \ < Longrightarrow > B \ < Longrightarrow > C & & & D \ < close > . In particular , the goal mechanism represents multiple claims as explicit conjunction internally , but this is refined ( via backwards introduction ) into separate sub - goals before the user commences the proof ; the final result is projected into a list of theorems using eliminations ( cf . \ \ secref { sec : tactical - goals } ) . The \ < open > prop \ < close > marker ( \ < open > # \ < close > ) makes arbitrarily complex propositions appear as atomic , without changing the meaning : \ < open > \ < Gamma > \ < turnstile > A \ < close > and \ < open > \ < Gamma > \ < turnstile > # A \ < close > are interchangeable . See \ secref { sec : tactical - goals } for specific operations . The \ < open > term \ < close > marker turns any well - typed term into a derivable proposition : \ < open > \ < turnstile > TERM t \ < close > holds unconditionally . Although this is logically vacuous , it allows to treat terms and proofs uniformly , similar to a type - theoretic framework . The \ < open > TYPE \ < close > constructor is the canonical representative of the unspecified type \ < open > \ < alpha > itself \ < close > ; it essentially injects the language of types into that of terms . There is specific notation \ < open > TYPE ( \ < tau > ) \ < close > for \ < open > TYPE \ < ^ bsub > \ < tau > itself \ < ^ esub > \ < close > . Although being devoid of any particular meaning , the term \ < open > TYPE ( \ < tau > ) \ < close > accounts for the type \ < open > \ < tau > \ < close > within the term language . In particular , \ < open > TYPE ( \ < alpha > ) \ < close > may be used as formal argument in primitive definitions , in order to circumvent hidden polymorphism ( cf . \ \ secref { sec : terms } ) . For example , \ < open > c TYPE ( \ < alpha > ) \ < equiv > A [ \ < alpha > ] \ < close > defines \ < open > c : : \ < alpha > itself \ < Rightarrow > prop \ < close > in terms of a proposition \ < open > A \ < close > that depends on an additional type argument , which is essentially a predicate on types . \ < close > text % mlref \ < open > \ begin { mldecls } @ { define_ML Conjunction . intr : " thm - > thm - > thm " } \ \ @ { define_ML Conjunction . elim : " thm - > thm * thm " } \ \ @ { define_ML Drule . mk_term : " cterm - > thm " } \ \ @ { define_ML Drule . dest_term : " thm - > cterm " } \ \ @ { define_ML Logic . mk_type : " typ - > term " } \ \ @ { define_ML Logic . dest_type : " term - > typ " } \ \ \ end { mldecls } \ < ^ descr > \ < ^ ML > \ < open > Conjunction . intr \ < close > derives \ < open > A & & & B \ < close > from \ < open > A \ < close > and \ < open > B \ < close > . \ < ^ descr > \ < ^ ML > \ < open > Conjunction . elim \ < close > derives \ < open > A \ < close > and \ < open > B \ < close > from \ < open > A & & & B \ < close > . \ < ^ descr > \ < ^ ML > \ < open > Drule . mk_term \ < close > derives \ < open > TERM t \ < close > . \ < ^ descr > \ < ^ ML > \ < open > Drule . dest_term \ < close > recovers term \ < open > t \ < close > from \ < open > TERM t \ < close > . \ < ^ descr > \ < ^ ML > \ < open > Logic . mk_type \ < close > ~ \ < open > \ < tau > \ < close > produces the term \ < open > TYPE ( \ < tau > ) \ < close > . \ < ^ descr > \ < ^ ML > \ < open > Logic . dest_type \ < close > ~ \ < open > TYPE ( \ < tau > ) \ < close > recovers the type \ < open > \ < tau > \ < close > . \ < close > subsection \ < open > Sort hypotheses \ < close > text \ < open > Type variables are decorated with sorts , as explained in \ secref { sec : types } . This constrains type instantiation to certain ranges of types : variable \ < open > \ < alpha > \ < ^ sub > s \ < close > may only be assigned to types \ < open > \ < tau > \ < close > that belong to sort \ < open > s \ < close > . Within the logic , sort constraints act like implicit preconditions on the result \ < open > \ < lparr > \ < alpha > \ < ^ sub > 1 : 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 the propositions \ < open > \ < Gamma > \ < close > , \ < open > \ < phi > \ < close > , as well as the proof of \ < open > \ < Gamma > \ < turnstile > \ < phi > \ < close > . These \ < ^ emph > \ < open > sort hypothesis \ < close > of a theorem are passed monotonically through further derivations . They are redundant , as long as the statement of a theorem still contains the type variables that are accounted here . The logical significance of sort hypotheses is limited to the boundary case where type variables disappear from the proposition , e . g . \ \ < open > \ < lparr > \ < alpha > \ < ^ sub > s : s \ < rparr > \ < turnstile > \ < phi > \ < close > . Since such dangling type variables can be renamed arbitrarily without changing the proposition \ < open > \ < phi > \ < close > , the inference kernel maintains sort hypotheses in anonymous form \ < open > s \ < turnstile > \ < phi > \ < close > . In most practical situations , such extra sort hypotheses may be stripped in a final bookkeeping step , e . g . \ at the end of a proof : they are typically left over from intermediate reasoning with type classes that can be satisfied by some concrete type \ < open > \ < tau > \ < close > of sort \ < open > s \ < close > to replace the hypothetical type variable \ < open > \ < alpha > \ < ^ sub > s \ < close > . \ < close > text % mlref \ < open > \ begin { mldecls } @ { define_ML Thm . extra_shyps : " thm - > sort list " } \ \ @ { define_ML Thm . strip_shyps : " thm - > thm " } \ \ \ end { mldecls } \ < ^ descr > \ < ^ ML > \ < open > Thm . extra_shyps \ < close > ~ \ < open > thm \ < close > determines the extraneous sort hypotheses of the given theorem , i . e . \ the sorts that are not present within type variables of the statement . \ < ^ descr > \ < ^ ML > \ < open > Thm . strip_shyps \ < close > ~ \ < open > thm \ < close > removes any extraneous sort hypotheses that can be witnessed from the type signature . \ < close > text % mlex \ < open > The following artificial example demonstrates the derivation of \ < ^ prop > \ < open > False \ < close > with a pending sort hypothesis involving a logically empty sort . \ < close > class empty = assumes bad : " \ < And > ( x : : ' a ) y . x \ < noteq > y " theorem ( in empty ) false : False using bad by blast ML_val \ < open > \ < ^ assert > ( Thm . extra_shyps @ { thm false } = [ \ < ^ sort > \ < open > empty \ < close > ] ) \ < close > text \ < open > Thanks to the inference kernel managing sort hypothesis according to their logical significance , this example is merely an instance of \ < ^ emph > \ < open > ex falso quodlibet consequitur \ < close > - - - not a collapse of the logical framework ! \ < close > section \ < open > Object - level rules \ label { sec : obj - rules } \ < close > text \ < open > The primitive inferences covered so far mostly serve foundational purposes . User - level reasoning usually works via object - level rules that are represented as theorems of Pure . Composition of rules involves \ < ^ emph > \ < open > backchaining \ < close > , \ < ^ emph > \ < open > higher - order unification \ < close > modulo \ < open > \ < alpha > \ < beta > \ < eta > \ < close > - conversion of \ < open > \ < lambda > \ < close > - terms , and so - called \ < ^ emph > \ < open > lifting \ < close > of rules into a context of \ < open > \ < And > \ < close > and \ < open > \ < Longrightarrow > \ < close > connectives . Thus the full power of higher - order Natural Deduction in Isabelle / Pure becomes readily available . \ < close > subsection \ < open > Hereditary Harrop Formulae \ < close > text \ < open > The idea of object - level rules is to model Natural Deduction inferences in the style of Gentzen \ < ^ cite > \ < open > " Gentzen : 1935 " \ < close > , but we allow arbitrary nesting similar to \ < ^ cite > \ < open > " Schroeder - Heister : 1984 " \ < close > . The most basic rule format is that of a \ < ^ emph > \ < open > Horn Clause \ < close > : \ [ \ infer { \ < open > A \ < close > } { \ < open > A \ < ^ sub > 1 \ < close > & \ < open > \ < dots > \ < close > & \ < open > A \ < ^ sub > n \ < close > } \ ] where \ < open > A , A \ < ^ sub > 1 , \ < dots > , A \ < ^ sub > n \ < close > are atomic propositions of the framework , usually of the form \ < open > Trueprop B \ < close > , where \ < open > B \ < close > is a ( compound ) object - level statement . This object - level inference corresponds to an iterated implication in Pure like this : \ [ \ < open > A \ < ^ sub > 1 \ < Longrightarrow > \ < dots > A \ < ^ sub > n \ < Longrightarrow > A \ < close > \ ] As an example consider conjunction introduction : \ < open > A \ < Longrightarrow > B \ < Longrightarrow > A \ < and > B \ < close > . Any parameters occurring in such rule statements are conceptionally treated as arbitrary : \ [ \ < 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 > \ ] Nesting of rules means that the positions of \ < open > A \ < ^ sub > i \ < close > may again hold compound rules , not just atomic propositions . Propositions of this format are called \ < ^ emph > \ < open > Hereditary Harrop Formulae \ < close > in the literature \ < ^ cite > \ < open > " Miller : 1991 " \ < close > . Here we give an inductive characterization as follows : \ < ^ medskip > \ begin { tabular } { ll } \ < open > \ < ^ bold > x \ < close > & set of variables \ \ \ < open > \ < ^ bold > A \ < close > & set of atomic propositions \ \ \ < open > \ < ^ bold > H = \ < And > \ < ^ bold > x \ < ^ sup > * . \ < ^ bold > H \ < ^ sup > * \ < Longrightarrow > \ < ^ bold > A \ < close > & set of Hereditary Harrop Formulas \ \ \ end { tabular } \ < ^ medskip > Thus we essentially impose nesting levels on propositions formed from \ < open > \ < And > \ < close > and \ < open > \ < Longrightarrow > \ < close > . At each level there is a prefix of parameters and compound premises , concluding an atomic proposition . Typical examples are \ < open > \ < longrightarrow > \ < close > - introduction \ < open > ( A \ < Longrightarrow > B ) \ < Longrightarrow > A \ < longrightarrow > B \ < close > or mathematical induction \ < open > P 0 \ < Longrightarrow > ( \ < And > n . P n \ < Longrightarrow > P ( Suc n ) ) \ < Longrightarrow > P n \ < close > . Even deeper nesting occurs in well - founded induction \ < 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 rule complexity that is usually seen in practice . \ < ^ medskip > Regular user - level inferences in Isabelle / Pure always maintain the following canonical form of results : \ < ^ item > Normalization by \ < open > ( A \ < Longrightarrow > ( \ < And > x . B x ) ) \ < equiv > ( \ < And > x . A \ < Longrightarrow > B x ) \ < close > , which is a theorem of Pure , means that quantifiers are pushed in front of implication at each level of nesting . The normal form is a Hereditary Harrop Formula . \ < ^ item > The outermost prefix of parameters is represented via schematic variables : instead of \ < open > \ < And > \ < ^ vec > x . \ < ^ vec > H \ < ^ vec > x \ < Longrightarrow > A \ < ^ vec > x \ < close > we have \ < open > \ < ^ vec > H ? \ < ^ vec > x \ < Longrightarrow > A ? \ < ^ vec > x \ < close > . Note that this representation looses information about the order of parameters , and vacuous quantifiers vanish automatically . \ < close > text % mlref \ < open > \ begin { mldecls } @ { define_ML Simplifier . norm_hhf : " Proof . context - > thm - > thm " } \ \ \ end { mldecls } \ < ^ descr > \ < ^ ML > \ < open > Simplifier . norm_hhf \ < close > ~ \ < open > ctxt thm \ < close > normalizes the given theorem according to the canonical form specified above . This is occasionally helpful to repair some low - level tools that do not handle Hereditary Harrop Formulae properly . \ < close > subsection \ < open > Rule composition \ < close > text \ < open > The rule calculus of Isabelle / Pure provides two main inferences : @ { inference resolution } ( i . e . \ back - chaining of rules ) and @ { inference assumption } ( i . e . \ closing a branch ) , both modulo higher - order unification . There are also combined variants , notably @ { inference elim_resolution } and @ { inference dest_resolution } . To understand the all - important @ { inference resolution } principle , we first consider raw @ { inference_def composition } ( modulo higher - order unification with substitution \ < open > \ < vartheta > \ < close > ) : \ [ \ infer [ ( @ { inference_def composition } ) ] { \ < open > \ < ^ vec > A \ < vartheta > \ < Longrightarrow > C \ < vartheta > \ < close > } { \ < open > \ < ^ vec > A \ < Longrightarrow > B \ < close > & \ < open > B ' \ < Longrightarrow > C \ < close > & \ < open > B \ < vartheta > = B ' \ < vartheta > \ < close > } \ ] Here the conclusion of the first rule is unified with the premise of the second ; the resulting rule instance inherits the premises of the first and conclusion of the second . Note that \ < open > C \ < close > can again consist of iterated implications . We can also permute the premises of the second rule back - and - forth in order to compose with \ < open > B ' \ < close > in any position ( subsequently we shall always refer to position 1 w . l . o . g . ) . In @ { inference composition } the internal structure of the common part \ < open > B \ < close > and \ < open > B ' \ < close > is not taken into account . For proper @ { inference resolution } we require \ < open > B \ < close > to be atomic , and explicitly observe the structure \ < open > \ < And > \ < ^ vec > x . \ < ^ vec > H \ < ^ vec > x \ < Longrightarrow > B ' \ < ^ vec > x \ < close > of the premise of the second rule . The idea is to adapt the first rule by ` ` lifting ' ' it into this context , by means of iterated application of the following inferences : \ [ \ infer [ ( @ { inference_def imp_lift } ) ] { \ < open > ( \ < ^ vec > H \ < Longrightarrow > \ < ^ vec > A ) \ < Longrightarrow > ( \ < ^ vec > H \ < Longrightarrow > B ) \ < close > } { \ < open > \ < ^ vec > A \ < Longrightarrow > B \ < close > } \ ] \ [ \ 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 > } \ ] By combining raw composition with lifting , we get full @ { inference resolution } as follows : \ [ \ infer [ ( @ { inference_def resolution } ) ] { \ < open > ( \ < And > \ < ^ vec > x . \ < ^ vec > H \ < ^ vec > x \ < Longrightarrow > \ < ^ vec > A ( ? \ < ^ vec > a \ < ^ vec > x ) ) \ < vartheta > \ < Longrightarrow > C \ < vartheta > \ < close > } { \ begin { tabular } { l } \ < open > \ < ^ vec > A ? \ < ^ vec > a \ < Longrightarrow > B ? \ < ^ vec > a \ < close > \ \ \ < open > ( \ < And > \ < ^ vec > x . \ < ^ vec > H \ < ^ vec > x \ < Longrightarrow > B ' \ < ^ vec > x ) \ < Longrightarrow > C \ < close > \ \ \ < open > ( \ < lambda > \ < ^ vec > x . B ( ? \ < ^ vec > a \ < ^ vec > x ) ) \ < vartheta > = B ' \ < vartheta > \ < close > \ \ \ end { tabular } } \ ] Continued resolution of rules allows to back - chain a problem towards more and sub - problems . Branches are closed either by resolving with a rule of 0 premises , or by producing a ` ` short - circuit ' ' within a solved situation ( again modulo unification ) : \ [ \ infer [ ( @ { inference_def assumption } ) ] { \ < open > C \ < vartheta > \ < close > } { \ < 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 > ) } } \ ] % FIXME @ { inference_def elim_resolution } , @ { inference_def dest_resolution } \ < close > text % mlref \ < open > \ begin { mldecls } @ { define_ML_infix " RSN " : " thm * ( int * thm ) - > thm " } \ \ @ { define_ML_infix " RS " : " thm * thm - > thm " } \ \ @ { define_ML_infix " RLN " : " thm list * ( int * thm list ) - > thm list " } \ \ @ { define_ML_infix " RL " : " thm list * thm list - > thm list " } \ \ @ { define_ML_infix " MRS " : " thm list * thm - > thm " } \ \ @ { define_ML_infix " OF " : " thm * thm list - > thm " } \ \ \ end { mldecls } \ < ^ descr > \ < open > rule \ < ^ sub > 1 RSN ( i , rule \ < ^ sub > 2 ) \ < close > resolves the conclusion of \ < open > rule \ < ^ sub > 1 \ < close > with the \ < open > i \ < close > - th premise of \ < open > rule \ < ^ sub > 2 \ < close > , according to the @ { inference resolution } principle explained above . Unless there is precisely one resolvent it raises exception \ < ^ ML > \ < open > THM \ < close > . This corresponds to the rule attribute @ { attribute THEN } in Isar source language . \ < ^ descr > \ < open > rule \ < ^ sub > 1 RS rule \ < ^ sub > 2 \ < close > abbreviates \ < open > rule \ < ^ sub > 1 RSN ( 1 , rule \ < ^ sub > 2 ) \ < close > . \ < ^ descr > \ < open > rules \ < ^ sub > 1 RLN ( i , rules \ < ^ sub > 2 ) \ < close > joins lists of rules . For every \ < open > rule \ < ^ sub > 1 \ < close > in \ < 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 > with the \ < open > i \ < close > - th premise of \ < open > rule \ < ^ sub > 2 \ < close > , accumulating multiple results in one big list . Note that such strict enumerations of higher - order unifications can be inefficient compared to the lazy variant seen in elementary tactics like \ < ^ ML > \ < open > resolve_tac \ < close > . \ < ^ descr > \ < open > rules \ < ^ sub > 1 RL rules \ < ^ sub > 2 \ < close > abbreviates \ < open > rules \ < ^ sub > 1 RLN ( 1 , rules \ < ^ sub > 2 ) \ < close > . \ < ^ descr > \ < open > [ rule \ < ^ sub > 1 , \ < dots > , rule \ < ^ sub > n ] MRS rule \ < close > resolves \ < open > rule \ < ^ sub > i \ < close > against premise \ < open > i \ < close > of \ < open > rule \ < close > , for \ < open > i = n , \ < dots > , 1 \ < close > . By working from right to left , newly emerging premises are concatenated in the result , without interfering . \ < ^ descr > \ < open > rule OF rules \ < close > is an alternative notation for \ < open > rules MRS rule \ < close > , which makes rule composition look more like function application . Note that the argument \ < open > rules \ < close > need not be atomic . This corresponds to the rule attribute @ { attribute OF } in Isar source language . \ < close > section \ < open > Proof terms \ label { sec : proof - terms } \ < close > text \ < open > The Isabelle / Pure inference kernel can record the proof of each theorem as a proof term that contains all logical inferences in detail . Rule composition by resolution ( \ secref { sec : obj - rules } ) and type - class reasoning is broken down to primitive rules of the logical framework . The proof term can be inspected by a separate proof - checker , for example . According to the well - known \ < ^ emph > \ < open > Curry - Howard isomorphism \ < close > , a proof can be viewed as a \ < open > \ < lambda > \ < close > - term . Following this idea , proofs in Isabelle are internally represented by a datatype similar to the one for terms described in \ secref { sec : terms } . On top of these syntactic terms , two more layers of \ < open > \ < lambda > \ < close > - calculus are added , which correspond to \ < open > \ < And > x : : \ < alpha > . B x \ < close > and \ < open > A \ < Longrightarrow > B \ < close > according to the propositions - as - types principle . The resulting 3 - level \ < open > \ < lambda > \ < close > - calculus resembles ` ` \ < open > \ < lambda > HOL \ < close > ' ' in the more abstract setting of Pure Type Systems ( PTS ) \ < ^ cite > \ < open > " Barendregt - Geuvers : 2001 " \ < close > , if some fine points like schematic polymorphism and type classes are ignored . \ < ^ medskip > \ < ^ emph > \ < open > Proof abstractions \ < close > of the form \ < open > \ < ^ bold > \ < lambda > x : : \ < alpha > . prf \ < close > or \ < open > \ < ^ bold > \ < lambda > p : A . prf \ < close > correspond to introduction of \ < open > \ < And > \ < close > / \ < open > \ < Longrightarrow > \ < close > , and \ < ^ emph > \ < open > proof applications \ < close > of the form \ < 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 > , propositions \ < open > A \ < close > , and terms \ < open > t \ < close > might be suppressed and reconstructed from the overall proof term . \ < ^ medskip > Various atomic proofs indicate special situations within the proof construction as follows . A \ < ^ emph > \ < open > bound proof variable \ < close > is a natural number \ < open > b \ < close > that acts as de - Bruijn index for proof term abstractions . A \ < ^ emph > \ < open > minimal proof \ < close > ` ` \ < open > ? \ < close > ' ' is a dummy proof term . This indicates some unrecorded part of the proof . \ < open > Hyp A \ < close > refers to some pending hypothesis by giving its proposition . This indicates an open context of implicit hypotheses , similar to loose bound variables or free variables within a term ( \ secref { sec : terms } ) . An \ < ^ emph > \ < open > axiom \ < close > or \ < ^ emph > \ < open > oracle \ < close > \ < open > a : A [ \ < ^ vec > \ < tau > ] \ < close > refers some postulated \ < open > proof constant \ < close > , which is subject to schematic polymorphism of theory content , and the particular type instantiation may be given explicitly . The vector of types \ < open > \ < ^ vec > \ < tau > \ < close > refers to the schematic type variables in the generic proposition \ < open > A \ < close > in canonical order . A \ < ^ emph > \ < open > proof promise \ < close > \ < open > a : A [ \ < ^ vec > \ < tau > ] \ < close > is a placeholder for some proof of polymorphic proposition \ < open > A \ < close > , with explicit type instantiation as given by the vector \ < open > \ < ^ vec > \ < tau > \ < close > , as above . Unlike axioms or oracles , proof promises may be \ < ^ emph > \ < open > fulfilled \ < close > eventually , by substituting \ < open > a \ < close > by some particular proof \ < open > q \ < close > at the corresponding type instance . This acts like Hindley - Milner \ < open > let \ < close > - polymorphism : a generic local proof definition may get used at different type instances , and is replaced by the concrete instance eventually . A \ < ^ emph > \ < open > named theorem \ < close > wraps up some concrete proof as a closed formal entity , in the manner of constant definitions for proof terms . The \ < ^ emph > \ < open > proof body \ < close > of such boxed theorems involves some digest about oracles and promises occurring in the original proof . This allows the inference kernel to manage this critical information without the full overhead of explicit proof terms . \ < close > subsection \ < open > Reconstructing and checking proof terms \ < close > text \ < open > Fully explicit proof terms can be large , but most of this information is redundant and can be reconstructed from the context . Therefore , the Isabelle / Pure inference kernel records only \ < ^ emph > \ < open > implicit \ < close > proof terms , by omitting all typing information in terms , all term and type labels of proof abstractions , and some argument terms of applications \ < open > p \ < cdot > t \ < close > ( if possible ) . There are separate operations to reconstruct the full proof term later on , using \ < ^ emph > \ < open > higher - order pattern unification \ < close > \ < ^ cite > \ < open > " nipkow - patterns " and " Berghofer - Nipkow : 2000 : TPHOL " \ < close > . The \ < ^ emph > \ < open > proof checker \ < close > expects a fully reconstructed proof term , and can turn it into a theorem by replaying its primitive inferences within the kernel . \ < close > subsection \ < open > Concrete syntax of proof terms \ < close > text \ < open > The concrete syntax of proof terms is a slight extension of the regular inner syntax of Isabelle / Pure \ < ^ cite > \ < open > " isabelle - isar - ref " \ < close > . Its main syntactic category @ { syntax ( inner ) proof } is defined as follows : \ begin { center } \ begin { supertabular } { rclr } @ { syntax_def ( inner ) proof } & = & \ < open > \ < ^ bold > \ < lambda > \ < close > \ < open > params \ < close > \ < ^ verbatim > \ < open > . \ < close > \ < open > proof \ < close > \ \ & \ < open > | \ < close > & \ < open > proof \ < close > \ < open > \ < cdot > \ < close > \ < open > any \ < close > \ \ & \ < open > | \ < close > & \ < open > proof \ < close > \ < open > \ < bullet > \ < close > \ < open > proof \ < close > \ \ & \ < open > | \ < close > & \ < open > id | longid \ < close > \ \ \ \ \ < open > param \ < close > & = & \ < open > idt \ < close > \ \ & \ < open > | \ < close > & \ < open > idt \ < close > \ < ^ verbatim > \ < open > : \ < close > \ < open > prop \ < close > \ \ & \ < open > | \ < close > & \ < ^ verbatim > \ < open > ( \ < close > \ < open > param \ < close > \ < ^ verbatim > \ < open > ) \ < close > \ \ \ \ \ < open > params \ < close > & = & \ < open > param \ < close > \ \ & \ < open > | \ < close > & \ < open > param \ < close > \ < open > params \ < close > \ \ \ end { supertabular } \ end { center } Implicit term arguments in partial proofs are indicated by ` ` \ < open > _ \ < close > ' ' . Type arguments for theorems and axioms may be specified using \ < open > p \ < cdot > TYPE ( type ) \ < close > ( they must appear before any other term argument of a theorem or axiom , but may be omitted altogether ) . \ < ^ medskip > There are separate read and print operations for proof terms , in order to avoid conflicts with the regular term language . \ < close > text % mlref \ < open > \ begin { mldecls } @ { define_ML_type proof } \ \ @ { define_ML_type proof_body } \ \ @ { define_ML Proofterm . proofs : " int Unsynchronized . ref " } \ \ @ { define_ML Proofterm . reconstruct_proof : " theory - > term - > proof - > proof " } \ \ @ { define_ML Proofterm . expand_proof : " theory - > ( Proofterm . thm_header - > Thm_Name . P option ) - > proof - > proof " } \ \ @ { define_ML Proof_Checker . thm_of_proof : " theory - > proof - > thm " } \ \ @ { define_ML Proof_Syntax . read_proof : " theory - > bool - > bool - > string - > proof " } \ \ @ { define_ML Proof_Syntax . pretty_proof : " Proof . context - > proof - > Pretty . T " } \ \ \ end { mldecls } \ < ^ descr > Type \ < ^ ML_type > \ < open > proof \ < close > represents proof terms ; this is a datatype with constructors @ { define_ML Abst } , @ { define_ML AbsP } , @ { define_ML_infix " % " } , @ { define_ML_infix " % % " } , @ { define_ML PBound } , @ { define_ML MinProof } , @ { define_ML Hyp } , @ { define_ML PAxm } , @ { define_ML Oracle } , @ { define_ML PThm } as explained above . % FIXME PClass ( ! ? ) \ < ^ descr > Type \ < ^ ML_type > \ < open > proof_body \ < close > represents the nested proof information of a named theorem , consisting of a digest of oracles and named theorem over some proof term . The digest only covers the directly visible part of the proof : in order to get the full information , the implicit graph of nested theorems needs to be traversed ( e . g . \ using \ < ^ ML > \ < open > Proofterm . fold_body_thms \ < close > ) . \ < ^ descr > \ < ^ ML > \ < open > Thm . proof_of \ < close > ~ \ < open > thm \ < close > and \ < ^ ML > \ < open > Thm . proof_body_of \ < close > ~ \ < open > thm \ < close > produce the proof term or proof body ( with digest of oracles and theorems ) from a given theorem . Note that this involves a full join of internal futures that fulfill pending proof promises , and thus disrupts the natural bottom - up construction of proofs by introducing dynamic ad - hoc dependencies . Parallel performance may suffer by inspecting proof terms at run - time . \ < ^ descr > \ < ^ ML > \ < open > Proofterm . proofs \ < close > specifies the detail of proof recording within \ < ^ ML_type > \ < open > thm \ < close > values produced by the inference kernel : \ < ^ ML > \ < open > 0 \ < close > records only the names of oracles , \ < ^ ML > \ < open > 1 \ < close > records oracle names and propositions , \ < ^ ML > \ < open > 2 \ < close > additionally records full proof terms . Officially named theorems that contribute to a result are recorded in any case . \ < ^ descr > \ < ^ ML > \ < open > Proofterm . reconstruct_proof \ < close > ~ \ < open > thy prop prf \ < close > turns the implicit proof term \ < open > prf \ < close > into a full proof of the given proposition . Reconstruction may fail if \ < open > prf \ < close > is not a proof of \ < open > prop \ < close > , or if it does not contain sufficient information for reconstruction . Failure may only happen for proofs that are constructed manually , but not for those produced automatically by the inference kernel . \ < ^ descr > \ < ^ ML > \ < open > Proofterm . expand_proof \ < close > ~ \ < open > thy expand prf \ < close > reconstructs and expands the proofs of nested theorems according to the given \ < open > expand \ < close > function : a result of @ { ML \ < open > SOME " " \ < close > } means full expansion , @ { ML \ < open > SOME \ < close > } ~ \ < open > name \ < close > means to keep the theorem node but replace its internal name , @ { ML NONE } means no change . \ < ^ descr > \ < ^ ML > \ < open > Proof_Checker . thm_of_proof \ < close > ~ \ < open > thy prf \ < close > turns the given ( full ) proof into a theorem , by replaying it using only primitive rules of the inference kernel . \ < ^ descr > \ < ^ ML > \ < open > Proof_Syntax . read_proof \ < close > ~ \ < open > thy b \ < ^ sub > 1 b \ < ^ sub > 2 s \ < close > reads in a proof term . The Boolean flags indicate the use of sort and type information . Usually , typing information is left implicit and is inferred during proof reconstruction . % FIXME eliminate flags ! ? \ < ^ descr > \ < ^ ML > \ < open > Proof_Syntax . pretty_proof \ < close > ~ \ < open > ctxt prf \ < close > pretty - prints the given proof term . \ < close > text % mlex \ < open > \ < ^ item > \ < ^ file > \ < open > ~ ~ / src / HOL / Proofs / ex / Proof_Terms . thy \ < close > provides basic examples involving proof terms . \ < ^ item > \ < ^ file > \ < open > ~ ~ / src / HOL / Proofs / ex / XML_Data . thy \ < close > demonstrates export and import of proof terms via XML / ML data representation . \ < close > section \ < open > Instantiation of formal entities \ label { sec : instantiation } \ < close > text \ < open > The construction of formal entities ( types , terms , theorems ) in Isabelle / ML can be tedious , error - prone , and costly at run - time . Repeated certification of types / terms , or proof steps for theorems should be minimized , when performance is relevant . For example , consider a proof - producing decision procedure that refers to certain term schemes and derived rules that need to be applied repeatedly . A reasonably efficient approach is the subsequent separation of Isabelle / ML \ < ^ emph > \ < open > compile - time \ < close > vs . \ < ^ emph > \ < open > run - time \ < close > . Lets say there is an ML module that is loaded into the theory context to provide a tool as proof method , to be used later in a different context . \ < ^ item > At compile - time , the ML module constructs templates for relevant formal entities , e . g . as certified types / terms and proven theorems ( with parameters ) . This uses the source notation for types , terms , propositions , inlined into Isabelle / ML . Formal parameters are taken from the template , and turned into ML names ( as in \ < ^ verbatim > \ < open > let \ < close > expressions ) . \ < ^ item > At run - time , the ML tool takes concrete entities from the application context , and instantiates the above templates accordingly . The formal parameters of the compile - time template get assigned to concrete ML values . ML names and types have already been properly checked by the ML compiler , and the running program cannot go wrong in that respect . ( It \ < ^ emph > \ < open > can \ < close > go wrong , concerning types of the implemented logic , though ) . This approach is supported by ML antiquotations as follows . \ < close > text % mlantiq \ < open > \ begin { matharray } { rcl } @ { ML_antiquotation_def " instantiate " } & : & \ < open > ML_antiquotation \ < close > \ \ \ end { matharray } \ < ^ rail > \ < open > @ @ { ML_antiquotation instantiate } embedded \ < close > \ < ^ descr > \ < open > @ { instantiation source } \ < close > refers to embedded source text to produce an instantiation for a logical entity that is given literally in the text . The content of the @ { syntax embedded } argument follows the syntax category @ { syntax instantiation } defined below , using @ { syntax embedded_ml } from antiquotation @ { ML_antiquotation Type } ( \ secref { sec : types } ) , and @ { syntax embedded_lemma } from antiquotation @ { ML_antiquotation lemma } ( \ secref { sec : thms } ) . \ < ^ rail > \ < open > @ { syntax_def instantiation } : no_beta ? ( inst + @ ' and ' ) @ ' in ' @ { syntax body } ; no_beta : ' ( ' ' no_beta ' ' ) ' ; schematic : ' ( ' ' schematic ' ' ) ' ; inst : ( ( type_ident | name ) ( ( @ ' = ' @ { syntax embedded_ml } ) ) ? ) ; body : body_type | body_term | body_prop | body_lemma ; body_type : ( ' typ ' | ' ctyp ' ) schematic ? embedded ; body_term : ( ' term ' | ' cterm ' ) schematic ? embedded ; body_prop : ( ' prop ' | ' cprop ' ) schematic ? embedded ; body_lemma : ' lemma ' schematic ? @ { syntax embedded_lemma } \ < close > \ < ^ item > An @ { syntax inst } entry assigns a type / term variable to a suitable ML value , given as ML expression in the current program context . The ML type of the expression needs to fit to the situation : \ < ^ verbatim > \ < open > ' a = \ < close > ~ \ < open > ty \ < close > refers to \ < open > ty \ < close > \ < ^ verbatim > \ < open > : typ \ < close > or \ < open > ty \ < close > \ < ^ verbatim > \ < open > : ctyp \ < close > , and \ < ^ verbatim > \ < open > a = \ < close > ~ \ < open > tm \ < close > refers to \ < open > tm \ < close > \ < ^ verbatim > \ < open > : term \ < close > or \ < open > tm \ < close > \ < ^ verbatim > \ < open > : cterm \ < close > . Only a body for uncertified \ < ^ verbatim > \ < open > typ \ < close > / \ < ^ verbatim > \ < open > term \ < close > / \ < ^ verbatim > \ < open > prop \ < close > admits uncertified \ < ^ ML_type > \ < open > typ \ < close > or \ < ^ ML_type > \ < open > term \ < close > parameters . The other cases require certified \ < ^ ML_type > \ < open > ctyp \ < close > or \ < ^ ML_type > \ < open > cterm \ < close > parameters . If the RHS of the @ { syntax inst } entry is omitted , it defaults to the LHS : \ < ^ verbatim > \ < open > a \ < close > becomes \ < ^ verbatim > \ < open > a = a \ < close > . This only works for term variables that happen to be legal ML identifiers , and not for type variables . \ < ^ item > The ` ` \ < open > ( schematic ) \ < close > ' ' option disables the usual check that all LHS names in @ { syntax inst } are exactly those present as free variables in the body entity ( type , term , prop , lemma statement ) . By default , omitted variables cause an error , but with ` ` \ < open > ( schematic ) \ < close > ' ' they remain as schematic variables . The latter needs to be used with care , because unexpected variables may emerge , when the theory name space for constants changes over time . \ < ^ item > The ` ` \ < open > ( no_beta ) \ < close > ' ' option disables the usual \ < open > \ < beta > \ < close > - normalization for \ < open > body_term \ < close > / \ < open > body_prop \ < close > / \ < open > body_lemma \ < close > , but has no effect on \ < open > body_type \ < close > . This is occasionally useful for low - level applications , where \ < open > \ < beta > \ < close > - conversion is treated explicitly in primitive inferences . \ < close > text % mlex \ < open > Below are some examples that demonstrate the antiquotation syntax . Real - world applications may be found in the Isabelle sources , by searching for the literal text ` ` \ < ^ verbatim > \ < open > \ < ^ instantiate > \ < close > ' ' . \ < close > ML \ < open > \ < comment > \ < open > uncertified type parameters \ < close > fun make_assoc_type ( A : typ , B : typ ) : typ = \ < ^ instantiate > \ < open > ' a = A and ' b = B in typ \ < open > ( ' a \ < times > ' b ) list \ < close > \ < close > ; \ < comment > \ < open > uncertified term parameters \ < close > val make_assoc_list : ( term * term ) list - > term list = map ( fn ( x , y ) = > \ < ^ instantiate > \ < open > ' a = \ < open > fastype_of x \ < close > and ' b = \ < open > fastype_of y \ < close > and x and y in term \ < open > ( x , y ) \ < close > for x : : ' a and y : : ' b \ < close > ) ; \ < comment > \ < open > theorem with certified term parameters \ < close > fun symmetry ( x : cterm ) ( y : cterm ) : thm = \ < ^ instantiate > \ < open > ' a = \ < open > Thm . ctyp_of_cterm x \ < close > and x and y in lemma \ < open > x = y \ < Longrightarrow > y = x \ < close > for x y : : ' a by simp \ < close > \ < comment > \ < open > theorem with certified type parameter , and schematic result \ < close > fun symmetry_schematic ( A : ctyp ) : thm = \ < ^ instantiate > \ < open > ' a = A in lemma ( schematic ) \ < open > x = y \ < Longrightarrow > y = x \ < close > for x y : : ' a by simp \ < close > \ < close > end
Messung V0.5 in Prozent C=88 H=94 G=90
¤ Dauer der Verarbeitung: 0.172 Sekunden
¤ *© Formatika GbR, Deutschland
