src/Doc/Implementation/Logic.thy
 author wenzelm Tue Sep 22 22:38:22 2015 +0200 (2015-09-22) changeset 61255 15865e0c5598 parent 61246 077b88f9ec16 child 61261 ddb2da7cb2e4 permissions -rw-r--r--
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
 wenzelm@29755  1 theory Logic  wenzelm@29755  2 imports Base  wenzelm@29755  3 begin  wenzelm@18537  4 wenzelm@58618  5 chapter \Primitive logic \label{ch:logic}\  wenzelm@18537  6 wenzelm@58618  7 text \  wenzelm@20480  8  The logical foundations of Isabelle/Isar are that of the Pure logic,  wenzelm@29774  9  which has been introduced as a Natural Deduction framework in  wenzelm@58555  10  @{cite paulson700}. This is essentially the same logic as @{text  wenzelm@20493  11  "\HOL"}'' in the more abstract setting of Pure Type Systems (PTS)  wenzelm@58555  12  @{cite "Barendregt-Geuvers:2001"}, although there are some key  wenzelm@20491  13  differences in the specific treatment of simple types in  wenzelm@20491  14  Isabelle/Pure.  wenzelm@20480  15 wenzelm@20480  16  Following type-theoretic parlance, the Pure logic consists of three  wenzelm@20543  17  levels of @{text "\"}-calculus with corresponding arrows, @{text  wenzelm@20480  18  "\"} for syntactic function space (terms depending on terms), @{text  wenzelm@20480  19  "\"} for universal quantification (proofs depending on terms), and  wenzelm@20480  20  @{text "\"} for implication (proofs depending on proofs).  wenzelm@20480  21 wenzelm@20537  22  Derivations are relative to a logical theory, which declares type  wenzelm@20537  23  constructors, constants, and axioms. Theory declarations support  wenzelm@20537  24  schematic polymorphism, which is strictly speaking outside the  wenzelm@20537  25  logic.\footnote{This is the deeper logical reason, why the theory  wenzelm@20537  26  context @{text "\"} is separate from the proof context @{text "\"}  wenzelm@34929  27  of the core calculus: type constructors, term constants, and facts  wenzelm@34929  28  (proof constants) may involve arbitrary type schemes, but the type  wenzelm@34929  29  of a locally fixed term parameter is also fixed!}  wenzelm@58618  30 \  wenzelm@20480  31 wenzelm@20480  32 wenzelm@58618  33 section \Types \label{sec:types}\  wenzelm@20437  34 wenzelm@58618  35 text \  wenzelm@20480  36  The language of types is an uninterpreted order-sorted first-order  wenzelm@20480  37  algebra; types are qualified by ordered type classes.  wenzelm@20480  38 wenzelm@20480  39  \medskip A \emph{type class} is an abstract syntactic entity  wenzelm@20480  40  declared in the theory context. The \emph{subclass relation} @{text  wenzelm@53015  41  "c\<^sub>1 \ c\<^sub>2"} is specified by stating an acyclic  wenzelm@20491  42  generating relation; the transitive closure is maintained  wenzelm@20491  43  internally. The resulting relation is an ordering: reflexive,  wenzelm@20491  44  transitive, and antisymmetric.  wenzelm@20451  45 wenzelm@53015  46  A \emph{sort} is a list of type classes written as @{text "s = {c\<^sub>1,  wenzelm@53015  47  \, c\<^sub>m}"}, it represents symbolic intersection. Notationally, the  wenzelm@34929  48  curly braces are omitted for singleton intersections, i.e.\ any  wenzelm@34929  49  class @{text "c"} may be read as a sort @{text "{c}"}. The ordering  wenzelm@34929  50  on type classes is extended to sorts according to the meaning of  wenzelm@53015  51  intersections: @{text "{c\<^sub>1, \ c\<^sub>m} \ {d\<^sub>1, \, d\<^sub>n}"} iff @{text  wenzelm@53015  52  "\j. \i. c\<^sub>i \ d\<^sub>j"}. The empty intersection @{text "{}"} refers to  wenzelm@34929  53  the universal sort, which is the largest element wrt.\ the sort  wenzelm@34929  54  order. Thus @{text "{}"} represents the full sort'', not the  wenzelm@34929  55  empty one! The intersection of all (finitely many) classes declared  wenzelm@34929  56  in the current theory is the least element wrt.\ the sort ordering.  wenzelm@20480  57 wenzelm@20491  58  \medskip A \emph{fixed type variable} is a pair of a basic name  wenzelm@20537  59  (starting with a @{text "'"} character) and a sort constraint, e.g.\  wenzelm@53015  60  @{text "('a, s)"} which is usually printed as @{text "\\<^sub>s"}.  wenzelm@20537  61  A \emph{schematic type variable} is a pair of an indexname and a  wenzelm@20537  62  sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually  wenzelm@53015  63  printed as @{text "?\\<^sub>s"}.  wenzelm@20451  64 wenzelm@20480  65  Note that \emph{all} syntactic components contribute to the identity  wenzelm@34929  66  of type variables: basic name, index, and sort constraint. The core  wenzelm@34929  67  logic handles type variables with the same name but different sorts  wenzelm@34929  68  as different, although the type-inference layer (which is outside  wenzelm@34929  69  the core) rejects anything like that.  wenzelm@20451  70 wenzelm@20493  71  A \emph{type constructor} @{text "\"} is a @{text "k"}-ary operator  wenzelm@20493  72  on types declared in the theory. Type constructor application is  wenzelm@53015  73  written postfix as @{text "(\\<^sub>1, \, \\<^sub>k)\"}. For  wenzelm@20537  74  @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}  wenzelm@20537  75  instead of @{text "()prop"}. For @{text "k = 1"} the parentheses  wenzelm@20537  76  are omitted, e.g.\ @{text "\ list"} instead of @{text "(\)list"}.  wenzelm@20537  77  Further notation is provided for specific constructors, notably the  wenzelm@20537  78  right-associative infix @{text "\ \ \"} instead of @{text "(\,  wenzelm@20537  79  \)fun"}.  wenzelm@20480  80   wenzelm@34929  81  The logical category \emph{type} is defined inductively over type  wenzelm@53015  82  variables and type constructors as follows: @{text "\ = \\<^sub>s | ?\\<^sub>s |  wenzelm@20543  83  (\\<^sub>1, \, \\<^sub>k)\"}.  wenzelm@20451  84 wenzelm@20514  85  A \emph{type abbreviation} is a syntactic definition @{text  wenzelm@20494  86  "(\<^vec>\)\ = \"} of an arbitrary type expression @{text "\"} over  wenzelm@20537  87  variables @{text "\<^vec>\"}. Type abbreviations appear as type  wenzelm@20537  88  constructors in the syntax, but are expanded before entering the  wenzelm@20537  89  logical core.  wenzelm@20480  90 wenzelm@20480  91  A \emph{type arity} declares the image behavior of a type  wenzelm@53015  92  constructor wrt.\ the algebra of sorts: @{text "\ :: (s\<^sub>1, \,  wenzelm@53015  93  s\<^sub>k)s"} means that @{text "(\\<^sub>1, \, \\<^sub>k)\"} is  wenzelm@53015  94  of sort @{text "s"} if every argument type @{text "\\<^sub>i"} is  wenzelm@53015  95  of sort @{text "s\<^sub>i"}. Arity declarations are implicitly  wenzelm@20494  96  completed, i.e.\ @{text "\ :: (\<^vec>s)c"} entails @{text "\ ::  wenzelm@20491  97  (\<^vec>s)c'"} for any @{text "c' \ c"}.  wenzelm@20491  98 wenzelm@20491  99  \medskip The sort algebra is always maintained as \emph{coregular},  wenzelm@20491  100  which means that type arities are consistent with the subclass  wenzelm@20537  101  relation: for any type constructor @{text "\"}, and classes @{text  wenzelm@53015  102  "c\<^sub>1 \ c\<^sub>2"}, and arities @{text "\ ::  wenzelm@53015  103  (\<^vec>s\<^sub>1)c\<^sub>1"} and @{text "\ ::  wenzelm@53015  104  (\<^vec>s\<^sub>2)c\<^sub>2"} holds @{text "\<^vec>s\<^sub>1 \  wenzelm@53015  105  \<^vec>s\<^sub>2"} component-wise.  wenzelm@20451  106 wenzelm@20491  107  The key property of a coregular order-sorted algebra is that sort  wenzelm@20537  108  constraints can be solved in a most general fashion: for each type  wenzelm@20537  109  constructor @{text "\"} and sort @{text "s"} there is a most general  wenzelm@53015  110  vector of argument sorts @{text "(s\<^sub>1, \, s\<^sub>k)"} such  wenzelm@53015  111  that a type scheme @{text "(\\<^bsub>s\<^sub>1\<^esub>, \,  wenzelm@53015  112  \\<^bsub>s\<^sub>k\<^esub>)\"} is of sort @{text "s"}.  wenzelm@20543  113  Consequently, type unification has most general solutions (modulo  wenzelm@20543  114  equivalence of sorts), so type-inference produces primary types as  wenzelm@58555  115  expected @{cite "nipkow-prehofer"}.  wenzelm@58618  116 \  wenzelm@20451  117 wenzelm@58618  118 text %mlref \  wenzelm@20480  119  \begin{mldecls}  wenzelm@34921  120  @{index_ML_type class: string} \\  wenzelm@34921  121  @{index_ML_type sort: "class list"} \\  wenzelm@34921  122  @{index_ML_type arity: "string * sort list * sort"} \\  wenzelm@20480  123  @{index_ML_type typ} \\  wenzelm@39846  124  @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\  wenzelm@39846  125  @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\  wenzelm@20547  126  \end{mldecls}  wenzelm@20547  127  \begin{mldecls}  wenzelm@20480  128  @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\  wenzelm@20480  129  @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\  wenzelm@47174  130  @{index_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\  wenzelm@42401  131  @{index_ML Sign.add_type_abbrev: "Proof.context ->  wenzelm@42401  132  binding * string list * typ -> theory -> theory"} \\  wenzelm@30355  133  @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\  wenzelm@20480  134  @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\  wenzelm@20480  135  @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\  wenzelm@20480  136  \end{mldecls}  wenzelm@20480  137 wenzelm@20480  138  \begin{description}  wenzelm@20480  139 wenzelm@39864  140  \item Type @{ML_type class} represents type classes.  wenzelm@20480  141 wenzelm@39864  142  \item Type @{ML_type sort} represents sorts, i.e.\ finite  wenzelm@39864  143  intersections of classes. The empty list @{ML "[]: sort"} refers to  wenzelm@39864  144  the empty class intersection, i.e.\ the full sort''.  wenzelm@20451  145 wenzelm@39864  146  \item Type @{ML_type arity} represents type arities. A triple  wenzelm@39864  147  @{text "(\, \<^vec>s, s) : arity"} represents @{text "\ ::  wenzelm@39864  148  (\<^vec>s)s"} as described above.  wenzelm@20480  149 wenzelm@39864  150  \item Type @{ML_type typ} represents types; this is a datatype with  wenzelm@20480  151  constructors @{ML TFree}, @{ML TVar}, @{ML Type}.  wenzelm@20480  152 wenzelm@39846  153  \item @{ML Term.map_atyps}~@{text "f \"} applies the mapping @{text  wenzelm@39846  154  "f"} to all atomic types (@{ML TFree}, @{ML TVar}) occurring in  wenzelm@39846  155  @{text "\"}.  wenzelm@20519  156 wenzelm@39846  157  \item @{ML Term.fold_atyps}~@{text "f \"} iterates the operation  wenzelm@39846  158  @{text "f"} over all occurrences of atomic types (@{ML TFree}, @{ML  wenzelm@39846  159  TVar}) in @{text "\"}; the type structure is traversed from left to  wenzelm@39846  160  right.  wenzelm@20494  161 wenzelm@53015  162  \item @{ML Sign.subsort}~@{text "thy (s\<^sub>1, s\<^sub>2)"}  wenzelm@53015  163  tests the subsort relation @{text "s\<^sub>1 \ s\<^sub>2"}.  wenzelm@20480  164 wenzelm@20537  165  \item @{ML Sign.of_sort}~@{text "thy (\, s)"} tests whether type  wenzelm@20537  166  @{text "\"} is of sort @{text "s"}.  wenzelm@20480  167 wenzelm@47174  168  \item @{ML Sign.add_type}~@{text "ctxt (\, k, mx)"} declares a  wenzelm@42401  169  new type constructors @{text "\"} with @{text "k"} arguments and  wenzelm@20480  170  optional mixfix syntax.  wenzelm@20451  171 wenzelm@42401  172  \item @{ML Sign.add_type_abbrev}~@{text "ctxt (\, \<^vec>\, \)"}  wenzelm@42401  173  defines a new type abbreviation @{text "(\<^vec>\)\ = \"}.  wenzelm@20480  174 wenzelm@53015  175  \item @{ML Sign.primitive_class}~@{text "(c, [c\<^sub>1, \,  wenzelm@53015  176  c\<^sub>n])"} declares a new class @{text "c"}, together with class  wenzelm@53015  177  relations @{text "c \ c\<^sub>i"}, for @{text "i = 1, \, n"}.  wenzelm@20480  178 wenzelm@53015  179  \item @{ML Sign.primitive_classrel}~@{text "(c\<^sub>1,  wenzelm@53015  180  c\<^sub>2)"} declares the class relation @{text "c\<^sub>1 \  wenzelm@53015  181  c\<^sub>2"}.  wenzelm@20480  182 wenzelm@20494  183  \item @{ML Sign.primitive_arity}~@{text "(\, \<^vec>s, s)"} declares  wenzelm@20537  184  the arity @{text "\ :: (\<^vec>s)s"}.  wenzelm@20480  185 wenzelm@20480  186  \end{description}  wenzelm@58618  187 \  wenzelm@20437  188 wenzelm@58618  189 text %mlantiq \  wenzelm@39832  190  \begin{matharray}{rcl}  wenzelm@39832  191  @{ML_antiquotation_def "class"} & : & @{text ML_antiquotation} \\  wenzelm@39832  192  @{ML_antiquotation_def "sort"} & : & @{text ML_antiquotation} \\  wenzelm@39832  193  @{ML_antiquotation_def "type_name"} & : & @{text ML_antiquotation} \\  wenzelm@39832  194  @{ML_antiquotation_def "type_abbrev"} & : & @{text ML_antiquotation} \\  wenzelm@39832  195  @{ML_antiquotation_def "nonterminal"} & : & @{text ML_antiquotation} \\  wenzelm@39832  196  @{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\  wenzelm@39832  197  \end{matharray}  wenzelm@39832  198 wenzelm@55112  199  @{rail \  wenzelm@42510  200  @@{ML_antiquotation class} nameref  wenzelm@39832  201  ;  wenzelm@42510  202  @@{ML_antiquotation sort} sort  wenzelm@39832  203  ;  wenzelm@42510  204  (@@{ML_antiquotation type_name} |  wenzelm@42510  205  @@{ML_antiquotation type_abbrev} |  wenzelm@42510  206  @@{ML_antiquotation nonterminal}) nameref  wenzelm@39832  207  ;  wenzelm@42510  208  @@{ML_antiquotation typ} type  wenzelm@55112  209  \}  wenzelm@39832  210 wenzelm@39832  211  \begin{description}  wenzelm@39832  212 wenzelm@39832  213  \item @{text "@{class c}"} inlines the internalized class @{text  wenzelm@39832  214  "c"} --- as @{ML_type string} literal.  wenzelm@39832  215 wenzelm@39832  216  \item @{text "@{sort s}"} inlines the internalized sort @{text "s"}  wenzelm@39832  217  --- as @{ML_type "string list"} literal.  wenzelm@39832  218 wenzelm@39832  219  \item @{text "@{type_name c}"} inlines the internalized type  wenzelm@39832  220  constructor @{text "c"} --- as @{ML_type string} literal.  wenzelm@39832  221 wenzelm@39832  222  \item @{text "@{type_abbrev c}"} inlines the internalized type  wenzelm@39832  223  abbreviation @{text "c"} --- as @{ML_type string} literal.  wenzelm@39832  224 wenzelm@39832  225  \item @{text "@{nonterminal c}"} inlines the internalized syntactic  wenzelm@39832  226  type~/ grammar nonterminal @{text "c"} --- as @{ML_type string}  wenzelm@39832  227  literal.  wenzelm@39832  228 wenzelm@39832  229  \item @{text "@{typ \}"} inlines the internalized type @{text "\"}  wenzelm@39832  230  --- as constructor term for datatype @{ML_type typ}.  wenzelm@39832  231 wenzelm@39832  232  \end{description}  wenzelm@58618  233 \  wenzelm@39832  234 wenzelm@20437  235 wenzelm@58618  236 section \Terms \label{sec:terms}\  wenzelm@18537  237 wenzelm@58618  238 text \  wenzelm@20491  239  The language of terms is that of simply-typed @{text "\"}-calculus  wenzelm@58555  240  with de-Bruijn indices for bound variables (cf.\ @{cite debruijn72}  wenzelm@58555  241  or @{cite "paulson-ml2"}), with the types being determined by the  wenzelm@29761  242  corresponding binders. In contrast, free variables and constants  wenzelm@34929  243  have an explicit name and type in each occurrence.  wenzelm@20514  244 wenzelm@20514  245  \medskip A \emph{bound variable} is a natural number @{text "b"},  wenzelm@20537  246  which accounts for the number of intermediate binders between the  wenzelm@20537  247  variable occurrence in the body and its binding position. For  wenzelm@34929  248  example, the de-Bruijn term @{text "\\<^bsub>bool\<^esub>. \\<^bsub>bool\<^esub>. 1 \ 0"} would  wenzelm@34929  249  correspond to @{text "\x\<^bsub>bool\<^esub>. \y\<^bsub>bool\<^esub>. x \ y"} in a named  wenzelm@20543  250  representation. Note that a bound variable may be represented by  wenzelm@20543  251  different de-Bruijn indices at different occurrences, depending on  wenzelm@20543  252  the nesting of abstractions.  wenzelm@20537  253 wenzelm@20543  254  A \emph{loose variable} is a bound variable that is outside the  wenzelm@20537  255  scope of local binders. The types (and names) for loose variables  wenzelm@20543  256  can be managed as a separate context, that is maintained as a stack  wenzelm@20543  257  of hypothetical binders. The core logic operates on closed terms,  wenzelm@20543  258  without any loose variables.  wenzelm@20514  259 wenzelm@20537  260  A \emph{fixed variable} is a pair of a basic name and a type, e.g.\  wenzelm@53015  261  @{text "(x, \)"} which is usually printed @{text "x\<^sub>\"} here. A  wenzelm@20537  262  \emph{schematic variable} is a pair of an indexname and a type,  wenzelm@34929  263  e.g.\ @{text "((x, 0), \)"} which is likewise printed as @{text  wenzelm@53015  264  "?x\<^sub>\"}.  wenzelm@20491  265 wenzelm@20537  266  \medskip A \emph{constant} is a pair of a basic name and a type,  wenzelm@53015  267  e.g.\ @{text "(c, \)"} which is usually printed as @{text "c\<^sub>\"}  wenzelm@34929  268  here. Constants are declared in the context as polymorphic families  wenzelm@34929  269  @{text "c :: \"}, meaning that all substitution instances @{text  wenzelm@53015  270  "c\<^sub>\"} for @{text "\ = \\"} are valid.  wenzelm@20514  271 wenzelm@53015  272  The vector of \emph{type arguments} of constant @{text "c\<^sub>\"} wrt.\  wenzelm@34929  273  the declaration @{text "c :: \"} is defined as the codomain of the  wenzelm@53015  274  matcher @{text "\ = {?\\<^sub>1 \ \\<^sub>1, \, ?\\<^sub>n \ \\<^sub>n}"} presented in  wenzelm@53015  275  canonical order @{text "(\\<^sub>1, \, \\<^sub>n)"}, corresponding to the  wenzelm@53015  276  left-to-right occurrences of the @{text "\\<^sub>i"} in @{text "\"}.  wenzelm@34929  277  Within a given theory context, there is a one-to-one correspondence  wenzelm@53015  278  between any constant @{text "c\<^sub>\"} and the application @{text "c(\\<^sub>1,  wenzelm@53015  279  \, \\<^sub>n)"} of its type arguments. For example, with @{text "plus :: \  wenzelm@34929  280  \ \ \ \"}, the instance @{text "plus\<^bsub>nat \ nat \ nat\<^esub>"} corresponds to  wenzelm@34929  281  @{text "plus(nat)"}.  wenzelm@20480  282 wenzelm@20514  283  Constant declarations @{text "c :: \"} may contain sort constraints  wenzelm@20514  284  for type variables in @{text "\"}. These are observed by  wenzelm@20514  285  type-inference as expected, but \emph{ignored} by the core logic.  wenzelm@20514  286  This means the primitive logic is able to reason with instances of  wenzelm@20537  287  polymorphic constants that the user-level type-checker would reject  wenzelm@20537  288  due to violation of type class restrictions.  wenzelm@20480  289 wenzelm@39861  290  \medskip An \emph{atomic term} is either a variable or constant.  wenzelm@34929  291  The logical category \emph{term} is defined inductively over atomic  wenzelm@34929  292  terms, with abstraction and application as follows: @{text "t = b |  wenzelm@53015  293  x\<^sub>\ | ?x\<^sub>\ | c\<^sub>\ | \\<^sub>\. t | t\<^sub>1 t\<^sub>2"}. Parsing and printing takes care of  wenzelm@34929  294  converting between an external representation with named bound  wenzelm@34929  295  variables. Subsequently, we shall use the latter notation instead  wenzelm@34929  296  of internal de-Bruijn representation.  wenzelm@20498  297 wenzelm@20537  298  The inductive relation @{text "t :: \"} assigns a (unique) type to a  wenzelm@20537  299  term according to the structure of atomic terms, abstractions, and  wenzelm@56579  300  applications:  wenzelm@20498  301  $ wenzelm@53015  302  \infer{@{text "a\<^sub>\ :: \"}}{}  wenzelm@20498  303  \qquad  wenzelm@20501  304  \infer{@{text "(\x\<^sub>\. t) :: \ \ \"}}{@{text "t :: \"}}  wenzelm@20501  305  \qquad  wenzelm@20501  306  \infer{@{text "t u :: \"}}{@{text "t :: \ \ \"} & @{text "u :: \"}}  wenzelm@20498  307 $  wenzelm@20514  308  A \emph{well-typed term} is a term that can be typed according to these rules.  wenzelm@20498  309 wenzelm@20514  310  Typing information can be omitted: type-inference is able to  wenzelm@20514  311  reconstruct the most general type of a raw term, while assigning  wenzelm@20514  312  most general types to all of its variables and constants.  wenzelm@20514  313  Type-inference depends on a context of type constraints for fixed  wenzelm@20514  314  variables, and declarations for polymorphic constants.  wenzelm@20514  315 wenzelm@20537  316  The identity of atomic terms consists both of the name and the type  wenzelm@20537  317  component. This means that different variables @{text  wenzelm@53015  318  "x\<^bsub>\\<^sub>1\<^esub>"} and @{text "x\<^bsub>\\<^sub>2\<^esub>"} may become the same after  wenzelm@34929  319  type instantiation. Type-inference rejects variables of the same  wenzelm@34929  320  name, but different types. In contrast, mixed instances of  wenzelm@34929  321  polymorphic constants occur routinely.  wenzelm@20514  322 wenzelm@20514  323  \medskip The \emph{hidden polymorphism} of a term @{text "t :: \"}  wenzelm@20514  324  is the set of type variables occurring in @{text "t"}, but not in  wenzelm@34929  325  its type @{text "\"}. This means that the term implicitly depends  wenzelm@34929  326  on type arguments that are not accounted in the result type, i.e.\  wenzelm@34929  327  there are different type instances @{text "t\ :: \"} and  wenzelm@34929  328  @{text "t\' :: \"} with the same type. This slightly  wenzelm@20543  329  pathological situation notoriously demands additional care.  wenzelm@20514  330 wenzelm@20514  331  \medskip A \emph{term abbreviation} is a syntactic definition @{text  wenzelm@53015  332  "c\<^sub>\ \ t"} of a closed term @{text "t"} of type @{text "\"},  wenzelm@20537  333  without any hidden polymorphism. A term abbreviation looks like a  wenzelm@20543  334  constant in the syntax, but is expanded before entering the logical  wenzelm@20543  335  core. Abbreviations are usually reverted when printing terms, using  wenzelm@53015  336  @{text "t \ c\<^sub>\"} as rules for higher-order rewriting.  wenzelm@20519  337 wenzelm@20519  338  \medskip Canonical operations on @{text "\"}-terms include @{text  wenzelm@20537  339  "\\\"}-conversion: @{text "\"}-conversion refers to capture-free  wenzelm@20519  340  renaming of bound variables; @{text "\"}-conversion contracts an  wenzelm@20537  341  abstraction applied to an argument term, substituting the argument  wenzelm@20519  342  in the body: @{text "(\x. b)a"} becomes @{text "b[a/x]"}; @{text  wenzelm@20519  343  "\"}-conversion contracts vacuous application-abstraction: @{text  wenzelm@20519  344  "\x. f x"} becomes @{text "f"}, provided that the bound variable  wenzelm@20537  345  does not occur in @{text "f"}.  wenzelm@20519  346 wenzelm@20537  347  Terms are normally treated modulo @{text "\"}-conversion, which is  wenzelm@20537  348  implicit in the de-Bruijn representation. Names for bound variables  wenzelm@20537  349  in abstractions are maintained separately as (meaningless) comments,  wenzelm@20537  350  mostly for parsing and printing. Full @{text "\\\"}-conversion is  wenzelm@28784  351  commonplace in various standard operations (\secref{sec:obj-rules})  wenzelm@28784  352  that are based on higher-order unification and matching.  wenzelm@58618  353 \  wenzelm@18537  354 wenzelm@58618  355 text %mlref \  wenzelm@20514  356  \begin{mldecls}  wenzelm@20514  357  @{index_ML_type term} \\  wenzelm@46262  358  @{index_ML_op "aconv": "term * term -> bool"} \\  wenzelm@39846  359  @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\  wenzelm@39846  360  @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\  wenzelm@39846  361  @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\  wenzelm@39846  362  @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\  wenzelm@20547  363  \end{mldecls}  wenzelm@20547  364  \begin{mldecls}  wenzelm@20514  365  @{index_ML fastype_of: "term -> typ"} \\  wenzelm@20519  366  @{index_ML lambda: "term -> term -> term"} \\  wenzelm@20519  367  @{index_ML betapply: "term * term -> term"} \\  wenzelm@42934  368  @{index_ML incr_boundvars: "int -> term -> term"} \\  wenzelm@42401  369  @{index_ML Sign.declare_const: "Proof.context ->  wenzelm@42401  370  (binding * typ) * mixfix -> theory -> term * theory"} \\  haftmann@33174  371  @{index_ML Sign.add_abbrev: "string -> binding * term ->  wenzelm@24972  372  theory -> (term * term) * theory"} \\  wenzelm@20519  373  @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\  wenzelm@20519  374  @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\  wenzelm@20514  375  \end{mldecls}  wenzelm@18537  376 wenzelm@20514  377  \begin{description}  wenzelm@18537  378 wenzelm@39864  379  \item Type @{ML_type term} represents de-Bruijn terms, with comments  wenzelm@39864  380  in abstractions, and explicitly named free variables and constants;  wenzelm@52408  381  this is a datatype with constructors @{index_ML Bound}, @{index_ML  wenzelm@52408  382  Free}, @{index_ML Var}, @{index_ML Const}, @{index_ML Abs},  wenzelm@52408  383  @{index_ML_op "$"}.  wenzelm@20519  384 wenzelm@36166  385  \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text  wenzelm@20519  386  "\"}-equivalence of two terms. This is the basic equality relation  wenzelm@20519  387  on type @{ML_type term}; raw datatype equality should only be used  wenzelm@20519  388  for operations related to parsing or printing!  wenzelm@20519  389 wenzelm@39846  390  \item @{ML Term.map_types}~@{text "f t"} applies the mapping @{text  wenzelm@20537  391  "f"} to all types occurring in @{text "t"}.  wenzelm@20537  392 wenzelm@39846  393  \item @{ML Term.fold_types}~@{text "f t"} iterates the operation  wenzelm@39846  394  @{text "f"} over all occurrences of types in @{text "t"}; the term  wenzelm@20537  395  structure is traversed from left to right.  wenzelm@20519  396 wenzelm@39846  397  \item @{ML Term.map_aterms}~@{text "f t"} applies the mapping @{text  wenzelm@39846  398  "f"} to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML  wenzelm@20537  399  Const}) occurring in @{text "t"}.  wenzelm@20537  400 wenzelm@39846  401  \item @{ML Term.fold_aterms}~@{text "f t"} iterates the operation  wenzelm@39846  402  @{text "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML  wenzelm@39846  403  Free}, @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is  wenzelm@20519  404  traversed from left to right.  wenzelm@20519  405 wenzelm@20537  406  \item @{ML fastype_of}~@{text "t"} determines the type of a  wenzelm@20537  407  well-typed term. This operation is relatively slow, despite the  wenzelm@20537  408  omission of any sanity checks.  wenzelm@20519  409 wenzelm@20519  410  \item @{ML lambda}~@{text "a b"} produces an abstraction @{text  wenzelm@20537  411  "\a. b"}, where occurrences of the atomic term @{text "a"} in the  wenzelm@20537  412  body @{text "b"} are replaced by bound variables.  wenzelm@20519  413 wenzelm@20537  414  \item @{ML betapply}~@{text "(t, u)"} produces an application @{text  wenzelm@20537  415  "t u"}, with topmost @{text "\"}-conversion if @{text "t"} is an  wenzelm@20537  416  abstraction.  wenzelm@20519  417 wenzelm@42934  418  \item @{ML incr_boundvars}~@{text "j"} increments a term's dangling  wenzelm@42934  419  bound variables by the offset @{text "j"}. This is required when  wenzelm@42934  420  moving a subterm into a context where it is enclosed by a different  wenzelm@42934  421  number of abstractions. Bound variables with a matching abstraction  wenzelm@42934  422  are unaffected.  wenzelm@42934  423 wenzelm@42401  424  \item @{ML Sign.declare_const}~@{text "ctxt ((c, \), mx)"} declares  wenzelm@42401  425  a new constant @{text "c :: \"} with optional mixfix syntax.  wenzelm@20519  426 haftmann@33174  427  \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}  wenzelm@21827  428  introduces a new term abbreviation @{text "c \ t"}.  wenzelm@20519  429 wenzelm@20520  430  \item @{ML Sign.const_typargs}~@{text "thy (c, \)"} and @{ML  wenzelm@53015  431  Sign.const_instance}~@{text "thy (c, [\\<^sub>1, \, \\<^sub>n])"}  wenzelm@20543  432  convert between two representations of polymorphic constants: full  wenzelm@20543  433  type instance vs.\ compact type arguments form.  wenzelm@18537  434 wenzelm@20514  435  \end{description}  wenzelm@58618  436 \  wenzelm@18537  437 wenzelm@58618  438 text %mlantiq \  wenzelm@39832  439  \begin{matharray}{rcl}  wenzelm@39832  440  @{ML_antiquotation_def "const_name"} & : & @{text ML_antiquotation} \\  wenzelm@39832  441  @{ML_antiquotation_def "const_abbrev"} & : & @{text ML_antiquotation} \\  wenzelm@39832  442  @{ML_antiquotation_def "const"} & : & @{text ML_antiquotation} \\  wenzelm@39832  443  @{ML_antiquotation_def "term"} & : & @{text ML_antiquotation} \\  wenzelm@39832  444  @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\  wenzelm@39832  445  \end{matharray}  wenzelm@39832  446 wenzelm@55112  447  @{rail \  wenzelm@42510  448  (@@{ML_antiquotation const_name} |  wenzelm@42510  449  @@{ML_antiquotation const_abbrev}) nameref  wenzelm@39832  450  ;  wenzelm@42510  451  @@{ML_antiquotation const} ('(' (type + ',') ')')?  wenzelm@39832  452  ;  wenzelm@42510  453  @@{ML_antiquotation term} term  wenzelm@39832  454  ;  wenzelm@42510  455  @@{ML_antiquotation prop} prop  wenzelm@55112  456  \}  wenzelm@39832  457 wenzelm@39832  458  \begin{description}  wenzelm@39832  459 wenzelm@39832  460  \item @{text "@{const_name c}"} inlines the internalized logical  wenzelm@39832  461  constant name @{text "c"} --- as @{ML_type string} literal.  wenzelm@39832  462 wenzelm@39832  463  \item @{text "@{const_abbrev c}"} inlines the internalized  wenzelm@39832  464  abbreviated constant name @{text "c"} --- as @{ML_type string}  wenzelm@39832  465  literal.  wenzelm@39832  466 wenzelm@39832  467  \item @{text "@{const c(\<^vec>\)}"} inlines the internalized  wenzelm@39832  468  constant @{text "c"} with precise type instantiation in the sense of  wenzelm@39832  469  @{ML Sign.const_instance} --- as @{ML Const} constructor term for  wenzelm@39832  470  datatype @{ML_type term}.  wenzelm@39832  471 wenzelm@39832  472  \item @{text "@{term t}"} inlines the internalized term @{text "t"}  wenzelm@39832  473  --- as constructor term for datatype @{ML_type term}.  wenzelm@39832  474 wenzelm@39832  475  \item @{text "@{prop \}"} inlines the internalized proposition  wenzelm@39832  476  @{text "\"} --- as constructor term for datatype @{ML_type term}.  wenzelm@39832  477 wenzelm@39832  478  \end{description}  wenzelm@58618  479 \  wenzelm@39832  480 wenzelm@18537  481 wenzelm@58618  482 section \Theorems \label{sec:thms}\  wenzelm@18537  483 wenzelm@58618  484 text \  wenzelm@20543  485  A \emph{proposition} is a well-typed term of type @{text "prop"}, a  wenzelm@20521  486  \emph{theorem} is a proven proposition (depending on a context of  wenzelm@20521  487  hypotheses and the background theory). Primitive inferences include  wenzelm@29774  488  plain Natural Deduction rules for the primary connectives @{text  wenzelm@20537  489  "\"} and @{text "\"} of the framework. There is also a builtin  wenzelm@20537  490  notion of equality/equivalence @{text "\"}.  wenzelm@58618  491 \  wenzelm@20521  492 wenzelm@29758  493 wenzelm@58618  494 subsection \Primitive connectives and rules \label{sec:prim-rules}\  wenzelm@18537  495 wenzelm@58618  496 text \  wenzelm@20543  497  The theory @{text "Pure"} contains constant declarations for the  wenzelm@20543  498  primitive connectives @{text "\"}, @{text "\"}, and @{text "\"} of  wenzelm@20543  499  the logical framework, see \figref{fig:pure-connectives}. The  wenzelm@53015  500  derivability judgment @{text "A\<^sub>1, \, A\<^sub>n \ B"} is  wenzelm@20543  501  defined inductively by the primitive inferences given in  wenzelm@20543  502  \figref{fig:prim-rules}, with the global restriction that the  wenzelm@20543  503  hypotheses must \emph{not} contain any schematic variables. The  wenzelm@20543  504  builtin equality is conceptually axiomatized as shown in  wenzelm@20521  505  \figref{fig:pure-equality}, although the implementation works  wenzelm@20543  506  directly with derived inferences.  wenzelm@20521  507 wenzelm@20521  508  \begin{figure}[htb]  wenzelm@20521  509  \begin{center}  wenzelm@20501  510  \begin{tabular}{ll}  wenzelm@20501  511  @{text "all :: (\ \ prop) \ prop"} & universal quantification (binder @{text "\"}) \\  wenzelm@20501  512  @{text "\ :: prop \ prop \ prop"} & implication (right associative infix) \\  wenzelm@20521  513  @{text "\ :: \ \ \ \ prop"} & equality relation (infix) \\  wenzelm@20501  514  \end{tabular}  wenzelm@20537  515  \caption{Primitive connectives of Pure}\label{fig:pure-connectives}  wenzelm@20521  516  \end{center}  wenzelm@20521  517  \end{figure}  wenzelm@18537  518 wenzelm@20501  519  \begin{figure}[htb]  wenzelm@20501  520  \begin{center}  wenzelm@20498  521  $ wenzelm@20498  522  \infer[@{text "(axiom)"}]{@{text "\ A"}}{@{text "A \ \"}}  wenzelm@20498  523  \qquad  wenzelm@20498  524  \infer[@{text "(assume)"}]{@{text "A \ A"}}{}  wenzelm@20498  525 $  wenzelm@20498  526  $ wenzelm@52407  527  \infer[@{text "(\\intro)"}]{@{text "\ \ \x. B[x]"}}{@{text "\ \ B[x]"} & @{text "x \ \"}}  wenzelm@20498  528  \qquad  wenzelm@52407  529  \infer[@{text "(\\elim)"}]{@{text "\ \ B[a]"}}{@{text "\ \ \x. B[x]"}}  wenzelm@20498  530 $  wenzelm@20498  531  $ wenzelm@42666  532  \infer[@{text "(\\intro)"}]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}}  wenzelm@20498  533  \qquad  wenzelm@42666  534  \infer[@{text "(\\elim)"}]{@{text "\\<^sub>1 \ \\<^sub>2 \ B"}}{@{text "\\<^sub>1 \ A \ B"} & @{text "\\<^sub>2 \ A"}}  wenzelm@20498  535 $  wenzelm@20521  536  \caption{Primitive inferences of Pure}\label{fig:prim-rules}  wenzelm@20521  537  \end{center}  wenzelm@20521  538  \end{figure}  wenzelm@20521  539 wenzelm@20521  540  \begin{figure}[htb]  wenzelm@20521  541  \begin{center}  wenzelm@20521  542  \begin{tabular}{ll}  wenzelm@20537  543  @{text "\ (\x. b[x]) a \ b[a]"} & @{text "\"}-conversion \\  wenzelm@20521  544  @{text "\ x \ x"} & reflexivity \\  wenzelm@20521  545  @{text "\ x \ y \ P x \ P y"} & substitution \\  wenzelm@20521  546  @{text "\ (\x. f x \ g x) \ f \ g"} & extensionality \\  wenzelm@20537  547  @{text "\ (A \ B) \ (B \ A) \ A \ B"} & logical equivalence \\  wenzelm@20521  548  \end{tabular}  wenzelm@20542  549  \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}  wenzelm@20501  550  \end{center}  wenzelm@20501  551  \end{figure}  wenzelm@18537  552 wenzelm@20501  553  The introduction and elimination rules for @{text "\"} and @{text  wenzelm@20537  554  "\"} are analogous to formation of dependently typed @{text  wenzelm@20501  555  "\"}-terms representing the underlying proof objects. Proof terms  wenzelm@20543  556  are irrelevant in the Pure logic, though; they cannot occur within  wenzelm@20543  557  propositions. The system provides a runtime option to record  wenzelm@52408  558  explicit proof terms for primitive inferences, see also  wenzelm@52408  559  \secref{sec:proof-terms}. Thus all three levels of @{text  wenzelm@52408  560  "\"}-calculus become explicit: @{text "\"} for terms, and @{text  wenzelm@58555  561  "\/\"} for proofs (cf.\ @{cite "Berghofer-Nipkow:2000:TPHOL"}).  wenzelm@20491  562 wenzelm@34929  563  Observe that locally fixed parameters (as in @{text  wenzelm@42666  564  "\\intro"}) need not be recorded in the hypotheses, because  wenzelm@34929  565  the simple syntactic types of Pure are always inhabitable.  wenzelm@34929  566  Assumptions'' @{text "x :: \"} for type-membership are only  wenzelm@53015  567  present as long as some @{text "x\<^sub>\"} occurs in the statement  wenzelm@34929  568  body.\footnote{This is the key difference to @{text "\HOL"}'' in  wenzelm@58555  569  the PTS framework @{cite "Barendregt-Geuvers:2001"}, where hypotheses  wenzelm@34929  570  @{text "x : A"} are treated uniformly for propositions and types.}  wenzelm@20501  571 wenzelm@20501  572  \medskip The axiomatization of a theory is implicitly closed by  wenzelm@20537  573  forming all instances of type and term variables: @{text "\  wenzelm@20537  574  A\"} holds for any substitution instance of an axiom  wenzelm@20543  575  @{text "\ A"}. By pushing substitutions through derivations  wenzelm@20543  576  inductively, we also get admissible @{text "generalize"} and @{text  wenzelm@34929  577  "instantiate"} rules as shown in \figref{fig:subst-rules}.  wenzelm@20501  578 wenzelm@20501  579  \begin{figure}[htb]  wenzelm@20501  580  \begin{center}  wenzelm@20498  581  $ wenzelm@20501  582  \infer{@{text "\ \ B[?$"}}{@{text "\ \ B[\]"} & @{text "\ \ \"}}  wenzelm@20501  583  \quad  wenzelm@20501  584  \infer[\quad@{text "(generalize)"}]{@{text "\ \ B[?x]"}}{@{text "\ \ B[x]"} & @{text "x \ \"}}  wenzelm@20498  585  \]  wenzelm@20498  586  $ wenzelm@20501  587  \infer{@{text "\ \ B[$"}}{@{text "\ \ B[?\]"}}  wenzelm@20501  588  \quad  wenzelm@20501  589  \infer[\quad@{text "(instantiate)"}]{@{text "\ \ B[t]"}}{@{text "\ \ B[?x]"}}  wenzelm@20498  590  \]  wenzelm@20501  591  \caption{Admissible substitution rules}\label{fig:subst-rules}  wenzelm@20501  592  \end{center}  wenzelm@20501  593  \end{figure}  wenzelm@18537  594 wenzelm@20537  595  Note that @{text "instantiate"} does not require an explicit  wenzelm@20537  596  side-condition, because @{text "\"} may never contain schematic  wenzelm@20537  597  variables.  wenzelm@20537  598 wenzelm@20537  599  In principle, variables could be substituted in hypotheses as well,  wenzelm@20543  600  but this would disrupt the monotonicity of reasoning: deriving  wenzelm@20543  601  @{text "\\ \ B\"} from @{text "\ \ B"} is  wenzelm@20543  602  correct, but @{text "\\ \ \"} does not necessarily hold:  wenzelm@20543  603  the result belongs to a different proof context.  wenzelm@20542  604 wenzelm@20543  605  \medskip An \emph{oracle} is a function that produces axioms on the  wenzelm@20543  606  fly. Logically, this is an instance of the @{text "axiom"} rule  wenzelm@20543  607  (\figref{fig:prim-rules}), but there is an operational difference.  wenzelm@20543  608  The system always records oracle invocations within derivations of  wenzelm@29768  609  theorems by a unique tag.  wenzelm@20542  610 wenzelm@20542  611  Axiomatizations should be limited to the bare minimum, typically as  wenzelm@20542  612  part of the initial logical basis of an object-logic formalization.  wenzelm@20543  613  Later on, theories are usually developed in a strictly definitional  wenzelm@20543  614  fashion, by stating only certain equalities over new constants.  wenzelm@20542  615 wenzelm@20542  616  A \emph{simple definition} consists of a constant declaration @{text  wenzelm@20543  617  "c :: \"} together with an axiom @{text "\ c \ t"}, where @{text "t  wenzelm@20543  618  :: \"} is a closed term without any hidden polymorphism. The RHS  wenzelm@20543  619  may depend on further defined constants, but not @{text "c"} itself.  wenzelm@20543  620  Definitions of functions may be presented as @{text "c \<^vec>x \  wenzelm@20543  621  t"} instead of the puristic @{text "c \ \\<^vec>x. t"}.  wenzelm@20542  622 wenzelm@20543  623  An \emph{overloaded definition} consists of a collection of axioms  wenzelm@20543  624  for the same constant, with zero or one equations @{text  wenzelm@20543  625  "c((\<^vec>\)\) \ t"} for each type constructor @{text "\"} (for  wenzelm@20543  626  distinct variables @{text "\<^vec>\"}). The RHS may mention  wenzelm@20543  627  previously defined constants as above, or arbitrary constants @{text  wenzelm@53015  628  "d(\\<^sub>i)"} for some @{text "\\<^sub>i"} projected from @{text  wenzelm@20543  629  "\<^vec>\"}. Thus overloaded definitions essentially work by  wenzelm@20543  630  primitive recursion over the syntactic structure of a single type  wenzelm@58555  631  argument. See also @{cite \\S4.3\ "Haftmann-Wenzel:2006:classes"}.  wenzelm@58618  632 \  wenzelm@20498  633 wenzelm@58618  634 text %mlref \  wenzelm@20521  635  \begin{mldecls}  wenzelm@46253  636  @{index_ML Logic.all: "term -> term -> term"} \\  wenzelm@46253  637  @{index_ML Logic.mk_implies: "term * term -> term"} \\  wenzelm@46253  638  \end{mldecls}  wenzelm@46253  639  \begin{mldecls}  wenzelm@20521  640  @{index_ML_type ctyp} \\  wenzelm@20521  641  @{index_ML_type cterm} \\  wenzelm@59621  642  @{index_ML Thm.ctyp_of: "Proof.context -> typ -> ctyp"} \\  wenzelm@59621  643  @{index_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\  wenzelm@46497  644  @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\  wenzelm@46497  645  @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\  wenzelm@60938  646  @{index_ML Thm.all: "Proof.context -> cterm -> cterm -> cterm"} \\  wenzelm@46253  647  @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\  wenzelm@20547  648  \end{mldecls}  wenzelm@20547  649  \begin{mldecls}  wenzelm@20521  650  @{index_ML_type thm} \\  wenzelm@50126  651  @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\  wenzelm@42933  652  @{index_ML Thm.transfer: "theory -> thm -> thm"} \\  wenzelm@20542  653  @{index_ML Thm.assume: "cterm -> thm"} \\  wenzelm@20542  654  @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\  wenzelm@20542  655  @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\  wenzelm@20542  656  @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\  wenzelm@20542  657  @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\  wenzelm@20542  658  @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\  wenzelm@60642  659  @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list  wenzelm@60642  660  -> thm -> thm"} \\  wenzelm@42401  661  @{index_ML Thm.add_axiom: "Proof.context ->  wenzelm@42401  662  binding * term -> theory -> (string * thm) * theory"} \\  wenzelm@39821  663  @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->  wenzelm@39821  664  (string * ('a -> thm)) * theory"} \\  wenzelm@42401  665  @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->  wenzelm@42401  666  binding * term -> theory -> (string * thm) * theory"} \\  wenzelm@20547  667  \end{mldecls}  wenzelm@20547  668  \begin{mldecls}  wenzelm@42401  669  @{index_ML Theory.add_deps: "Proof.context -> string ->  wenzelm@61255  670  Defs.entry -> Defs.entry list -> theory -> theory"} \\  wenzelm@20521  671  \end{mldecls}  wenzelm@20521  672 wenzelm@20521  673  \begin{description}  wenzelm@20521  674 wenzelm@50126  675  \item @{ML Thm.peek_status}~@{text "thm"} informs about the current  wenzelm@50126  676  status of the derivation object behind the given theorem. This is a  wenzelm@50126  677  snapshot of a potentially ongoing (parallel) evaluation of proofs.  wenzelm@50126  678  The three Boolean values indicate the following: @{verbatim oracle}  wenzelm@50126  679  if the finished part contains some oracle invocation; @{verbatim  wenzelm@50126  680  unfinished} if some future proofs are still pending; @{verbatim  wenzelm@50126  681  failed} if some future proof has failed, rendering the theorem  wenzelm@50126  682  invalid!  wenzelm@50126  683 wenzelm@46253  684  \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification  wenzelm@46253  685  @{text "\a. B"}, where occurrences of the atomic term @{text "a"} in  wenzelm@46253  686  the body proposition @{text "B"} are replaced by bound variables.  wenzelm@46253  687  (See also @{ML lambda} on terms.)  wenzelm@46253  688 wenzelm@46253  689  \item @{ML Logic.mk_implies}~@{text "(A, B)"} produces a Pure  wenzelm@46253  690  implication @{text "A \ B"}.  wenzelm@46253  691 wenzelm@39864  692  \item Types @{ML_type ctyp} and @{ML_type cterm} represent certified  wenzelm@39864  693  types and terms, respectively. These are abstract datatypes that  wenzelm@20542  694  guarantee that its values have passed the full well-formedness (and  wenzelm@20542  695  well-typedness) checks, relative to the declarations of type  wenzelm@46253  696  constructors, constants etc.\ in the background theory. The  wenzelm@46253  697  abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the  wenzelm@46253  698  same inference kernel that is mainly responsible for @{ML_type thm}.  wenzelm@46253  699  Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}  wenzelm@55837  700  are located in the @{ML_structure Thm} module, even though theorems are  wenzelm@46253  701  not yet involved at that stage.  wenzelm@20542  702 wenzelm@59621  703  \item @{ML Thm.ctyp_of}~@{text "ctxt \"} and @{ML  wenzelm@59621  704  Thm.cterm_of}~@{text "ctxt t"} explicitly check types and terms,  wenzelm@29768  705  respectively. This also involves some basic normalizations, such  wenzelm@59621  706  expansion of type and term abbreviations from the underlying  wenzelm@59621  707  theory context.  wenzelm@46253  708  Full re-certification is relatively slow and should be avoided in  wenzelm@46253  709  tight reasoning loops.  wenzelm@20547  710 wenzelm@46497  711  \item @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML  wenzelm@46253  712  Drule.mk_implies} etc.\ compose certified terms (or propositions)  wenzelm@46253  713  incrementally. This is equivalent to @{ML Thm.cterm_of} after  wenzelm@46262  714  unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML  wenzelm@46253  715  Logic.mk_implies} etc., but there can be a big difference in  wenzelm@46253  716  performance when large existing entities are composed by a few extra  wenzelm@46253  717  constructions on top. There are separate operations to decompose  wenzelm@46253  718  certified terms and theorems to produce certified terms again.  wenzelm@20542  719 wenzelm@39864  720  \item Type @{ML_type thm} represents proven propositions. This is  wenzelm@39864  721  an abstract datatype that guarantees that its values have been  wenzelm@55837  722  constructed by basic principles of the @{ML_structure Thm} module.  wenzelm@52788  723  Every @{ML_type thm} value refers its background theory,  wenzelm@52788  724  cf.\ \secref{sec:context-theory}.  wenzelm@20542  725 wenzelm@42933  726  \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given  wenzelm@42933  727  theorem to a \emph{larger} theory, see also \secref{sec:context}.  wenzelm@42933  728  This formal adjustment of the background context has no logical  wenzelm@42933  729  significance, but is occasionally required for formal reasons, e.g.\  wenzelm@42933  730  when theorems that are imported from more basic theories are used in  wenzelm@42933  731  the current situation.  wenzelm@42933  732 wenzelm@20542  733  \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML  wenzelm@20542  734  Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}  wenzelm@20542  735  correspond to the primitive inferences of \figref{fig:prim-rules}.  wenzelm@20542  736 wenzelm@20542  737  \item @{ML Thm.generalize}~@{text "(\<^vec>\, \<^vec>x)"}  wenzelm@20542  738  corresponds to the @{text "generalize"} rules of  wenzelm@20543  739  \figref{fig:subst-rules}. Here collections of type and term  wenzelm@20543  740  variables are generalized simultaneously, specified by the given  wenzelm@20543  741  basic names.  wenzelm@20521  742 wenzelm@53015  743  \item @{ML Thm.instantiate}~@{text "(\<^vec>\\<^sub>s,  wenzelm@53015  744  \<^vec>x\<^sub>\)"} corresponds to the @{text "instantiate"} rules  wenzelm@20542  745  of \figref{fig:subst-rules}. Type variables are substituted before  wenzelm@53015  746  term variables. Note that the types in @{text "\<^vec>x\<^sub>\"}  wenzelm@20542  747  refer to the instantiated versions.  wenzelm@20542  748 wenzelm@42401  749  \item @{ML Thm.add_axiom}~@{text "ctxt (name, A)"} declares an  wenzelm@35927  750  arbitrary proposition as axiom, and retrieves it as a theorem from  wenzelm@35927  751  the resulting theory, cf.\ @{text "axiom"} in  wenzelm@35927  752  \figref{fig:prim-rules}. Note that the low-level representation in  wenzelm@35927  753  the axiom table may differ slightly from the returned theorem.  wenzelm@20542  754 wenzelm@30288  755  \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named  wenzelm@28290  756  oracle rule, essentially generating arbitrary axioms on the fly,  wenzelm@28290  757  cf.\ @{text "axiom"} in \figref{fig:prim-rules}.  wenzelm@20521  758 wenzelm@42401  759  \item @{ML Thm.add_def}~@{text "ctxt unchecked overloaded (name, c  wenzelm@35927  760  \<^vec>x \ t)"} states a definitional axiom for an existing constant  wenzelm@35927  761  @{text "c"}. Dependencies are recorded via @{ML Theory.add_deps},  wenzelm@35927  762  unless the @{text "unchecked"} option is set. Note that the  wenzelm@35927  763  low-level representation in the axiom table may differ slightly from  wenzelm@35927  764  the returned theorem.  wenzelm@20542  765 wenzelm@53015  766  \item @{ML Theory.add_deps}~@{text "ctxt name c\<^sub>\ \<^vec>d\<^sub>\"}  wenzelm@42401  767  declares dependencies of a named specification for constant @{text  wenzelm@53015  768  "c\<^sub>\"}, relative to existing specifications for constants @{text  wenzelm@61255  769  "\<^vec>d\<^sub>\"}. This also works for type constructors.  wenzelm@20542  770 wenzelm@20521  771  \end{description}  wenzelm@58618  772 \  wenzelm@20521  773 wenzelm@20521  774 wenzelm@58618  775 text %mlantiq \  wenzelm@39832  776  \begin{matharray}{rcl}  wenzelm@39832  777  @{ML_antiquotation_def "ctyp"} & : & @{text ML_antiquotation} \\  wenzelm@39832  778  @{ML_antiquotation_def "cterm"} & : & @{text ML_antiquotation} \\  wenzelm@39832  779  @{ML_antiquotation_def "cprop"} & : & @{text ML_antiquotation} \\  wenzelm@39832  780  @{ML_antiquotation_def "thm"} & : & @{text ML_antiquotation} \\  wenzelm@39832  781  @{ML_antiquotation_def "thms"} & : & @{text ML_antiquotation} \\  wenzelm@39832  782  @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\  wenzelm@39832  783  \end{matharray}  wenzelm@39832  784 wenzelm@55112  785  @{rail \  wenzelm@42510  786  @@{ML_antiquotation ctyp} typ  wenzelm@39832  787  ;  wenzelm@42510  788  @@{ML_antiquotation cterm} term  wenzelm@39832  789  ;  wenzelm@42510  790  @@{ML_antiquotation cprop} prop  wenzelm@39832  791  ;  wenzelm@42510  792  @@{ML_antiquotation thm} thmref  wenzelm@42510  793  ;  wenzelm@42510  794  @@{ML_antiquotation thms} thmrefs  wenzelm@39832  795  ;  wenzelm@55029  796  @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \  wenzelm@42517  797  @'by' method method?  wenzelm@55112  798  \}  wenzelm@39832  799 wenzelm@39832  800  \begin{description}  wenzelm@39832  801 wenzelm@39832  802  \item @{text "@{ctyp \}"} produces a certified type wrt.\ the  wenzelm@39832  803  current background theory --- as abstract value of type @{ML_type  wenzelm@39832  804  ctyp}.  wenzelm@39832  805 wenzelm@39832  806  \item @{text "@{cterm t}"} and @{text "@{cprop \}"} produce a  wenzelm@39832  807  certified term wrt.\ the current background theory --- as abstract  wenzelm@39832  808  value of type @{ML_type cterm}.  wenzelm@39832  809 wenzelm@39832  810  \item @{text "@{thm a}"} produces a singleton fact --- as abstract  wenzelm@39832  811  value of type @{ML_type thm}.  wenzelm@39832  812 wenzelm@39832  813  \item @{text "@{thms a}"} produces a general fact --- as abstract  wenzelm@39832  814  value of type @{ML_type "thm list"}.  wenzelm@39832  815 wenzelm@39832  816  \item @{text "@{lemma \ by meth}"} produces a fact that is proven on  wenzelm@39832  817  the spot according to the minimal proof, which imitates a terminal  wenzelm@39832  818  Isar proof. The result is an abstract value of type @{ML_type thm}  wenzelm@39832  819  or @{ML_type "thm list"}, depending on the number of propositions  wenzelm@39832  820  given here.  wenzelm@39832  821 wenzelm@39832  822  The internal derivation object lacks a proper theorem name, but it  wenzelm@39832  823  is formally closed, unless the @{text "(open)"} option is specified  wenzelm@39832  824  (this may impact performance of applications with proof terms).  wenzelm@39832  825 wenzelm@39832  826  Since ML antiquotations are always evaluated at compile-time, there  wenzelm@39832  827  is no run-time overhead even for non-trivial proofs. Nonetheless,  wenzelm@39832  828  the justification is syntactically limited to a single @{command  wenzelm@39832  829  "by"} step. More complex Isar proofs should be done in regular  wenzelm@39832  830  theory source, before compiling the corresponding ML text that uses  wenzelm@39832  831  the result.  wenzelm@39832  832 wenzelm@39832  833  \end{description}  wenzelm@39832  834 wenzelm@58618  835 \  wenzelm@39832  836 wenzelm@39832  837 wenzelm@58618  838 subsection \Auxiliary connectives \label{sec:logic-aux}\  wenzelm@20521  839 wenzelm@58618  840 text \Theory @{text "Pure"} provides a few auxiliary connectives  wenzelm@46254  841  that are defined on top of the primitive ones, see  wenzelm@46254  842  \figref{fig:pure-aux}. These special constants are useful in  wenzelm@46254  843  certain internal encodings, and are normally not directly exposed to  wenzelm@46254  844  the user.  wenzelm@20501  845 wenzelm@20501  846  \begin{figure}[htb]  wenzelm@20501  847  \begin{center}  wenzelm@20498  848  \begin{tabular}{ll}  wenzelm@34929  849  @{text "conjunction :: prop \ prop \ prop"} & (infix @{text "&&&"}) \\  wenzelm@34929  850  @{text "\ A &&& B \ (\C. (A \ B \ C) \ C)"} \$1ex]  wenzelm@20543  851  @{text "prop :: prop \ prop"} & (prefix @{text "#"}, suppressed) \\  wenzelm@20521  852  @{text "#A \ A"} \\[1ex]  wenzelm@20521  853  @{text "term :: \ \ prop"} & (prefix @{text "TERM"}) \\  wenzelm@20521  854  @{text "term x \ (\A. A \ A)"} \\[1ex]  wenzelm@56243  855  @{text "type :: \ itself"} & (prefix @{text "TYPE"}) \\  wenzelm@20521  856  @{text "(unspecified)"} \\  wenzelm@20498  857  \end{tabular}  wenzelm@20521  858  \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}  wenzelm@20501  859  \end{center}  wenzelm@20501  860  \end{figure}  wenzelm@20501  861 wenzelm@34929  862  The introduction @{text "A \ B \ A &&& B"}, and eliminations  wenzelm@34929  863  (projections) @{text "A &&& B \ A"} and @{text "A &&& B \ B"} are  wenzelm@34929  864  available as derived rules. Conjunction allows to treat  wenzelm@34929  865  simultaneous assumptions and conclusions uniformly, e.g.\ consider  wenzelm@34929  866  @{text "A \ B \ C &&& D"}. In particular, the goal mechanism  wenzelm@34929  867  represents multiple claims as explicit conjunction internally, but  wenzelm@34929  868  this is refined (via backwards introduction) into separate sub-goals  wenzelm@34929  869  before the user commences the proof; the final result is projected  wenzelm@34929  870  into a list of theorems using eliminations (cf.\  wenzelm@20537  871  \secref{sec:tactical-goals}).  wenzelm@20498  872 wenzelm@20537  873  The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex  wenzelm@20537  874  propositions appear as atomic, without changing the meaning: @{text  wenzelm@20537  875  "\ \ A"} and @{text "\ \ #A"} are interchangeable. See  wenzelm@20537  876  \secref{sec:tactical-goals} for specific operations.  wenzelm@20521  877 wenzelm@20543  878  The @{text "term"} marker turns any well-typed term into a derivable  wenzelm@20543  879  proposition: @{text "\ TERM t"} holds unconditionally. Although  wenzelm@20543  880  this is logically vacuous, it allows to treat terms and proofs  wenzelm@20543  881  uniformly, similar to a type-theoretic framework.  wenzelm@20498  882 wenzelm@20537  883  The @{text "TYPE"} constructor is the canonical representative of  wenzelm@20537  884  the unspecified type @{text "\ itself"}; it essentially injects the  wenzelm@20537  885  language of types into that of terms. There is specific notation  wenzelm@53071  886  @{text "TYPE(\)"} for @{text "TYPE\<^bsub>\ itself\<^esub>"}.  wenzelm@34929  887  Although being devoid of any particular meaning, the term @{text  wenzelm@20537  888  "TYPE(\)"} accounts for the type @{text "\"} within the term  wenzelm@20537  889  language. In particular, @{text "TYPE(\)"} may be used as formal  wenzelm@20537  890  argument in primitive definitions, in order to circumvent hidden  wenzelm@20537  891  polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c  wenzelm@20537  892  TYPE(\) \ A[$"} defines @{text "c :: \ itself \ prop"} in terms of  wenzelm@20537  893  a proposition @{text "A"} that depends on an additional type  wenzelm@20537  894  argument, which is essentially a predicate on types.  wenzelm@58618  895 \  wenzelm@20501  896 wenzelm@58618  897 text %mlref \  wenzelm@20521  898  \begin{mldecls}  wenzelm@20521  899  @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\  wenzelm@20521  900  @{index_ML Conjunction.elim: "thm -> thm * thm"} \\  wenzelm@20521  901  @{index_ML Drule.mk_term: "cterm -> thm"} \\  wenzelm@20521  902  @{index_ML Drule.dest_term: "thm -> cterm"} \\  wenzelm@20521  903  @{index_ML Logic.mk_type: "typ -> term"} \\  wenzelm@20521  904  @{index_ML Logic.dest_type: "term -> typ"} \\  wenzelm@20521  905  \end{mldecls}  wenzelm@20521  906 wenzelm@20521  907  \begin{description}  wenzelm@20521  908 wenzelm@34929  909  \item @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text  wenzelm@20542  910  "A"} and @{text "B"}.  wenzelm@20542  911 wenzelm@20543  912  \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}  wenzelm@34929  913  from @{text "A &&& B"}.  wenzelm@20542  914 wenzelm@20543  915  \item @{ML Drule.mk_term} derives @{text "TERM t"}.  wenzelm@20542  916 wenzelm@20543  917  \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text  wenzelm@20543  918  "TERM t"}.  wenzelm@20542  919 wenzelm@20542  920  \item @{ML Logic.mk_type}~@{text "\"} produces the term @{text  wenzelm@20542  921  "TYPE(\)"}.  wenzelm@20542  922 wenzelm@20542  923  \item @{ML Logic.dest_type}~@{text "TYPE(\)"} recovers the type  wenzelm@20542  924  @{text "\"}.  wenzelm@20521  925 wenzelm@20521  926  \end{description}  wenzelm@58618  927 \  wenzelm@18537  928 wenzelm@20480  929 wenzelm@58618  930 subsection \Sort hypotheses\  wenzelm@52406  931 wenzelm@58618  932 text \Type variables are decorated with sorts, as explained in  wenzelm@52406  933  \secref{sec:types}. This constrains type instantiation to certain  wenzelm@52406  934  ranges of types: variable @{text "\\<^sub>s"} may only be assigned to types  wenzelm@52406  935  @{text "\"} that belong to sort @{text "s"}. Within the logic, sort  wenzelm@52406  936  constraints act like implicit preconditions on the result @{text  wenzelm@52406  937  "\\\<^sub>1 : s\<^sub>1\, \, \\\<^sub>n : s\<^sub>n\, \ \ \"} where the type variables @{text  wenzelm@52406  938  "\\<^sub>1, \, \\<^sub>n"} cover the propositions @{text "\"}, @{text "\"}, as  wenzelm@52406  939  well as the proof of @{text "\ \ \"}.  wenzelm@52406  940 wenzelm@52406  941  These \emph{sort hypothesis} of a theorem are passed monotonically  wenzelm@52406  942  through further derivations. They are redundant, as long as the  wenzelm@52406  943  statement of a theorem still contains the type variables that are  wenzelm@52406  944  accounted here. The logical significance of sort hypotheses is  wenzelm@52406  945  limited to the boundary case where type variables disappear from the  wenzelm@52406  946  proposition, e.g.\ @{text "\\\<^sub>s : s\ \ \"}. Since such dangling type  wenzelm@52406  947  variables can be renamed arbitrarily without changing the  wenzelm@52406  948  proposition @{text "\"}, the inference kernel maintains sort  wenzelm@52406  949  hypotheses in anonymous form @{text "s \ \"}.  wenzelm@52406  950 wenzelm@52406  951  In most practical situations, such extra sort hypotheses may be  wenzelm@52406  952  stripped in a final bookkeeping step, e.g.\ at the end of a proof:  wenzelm@52406  953  they are typically left over from intermediate reasoning with type  wenzelm@52406  954  classes that can be satisfied by some concrete type @{text "\"} of  wenzelm@52406  955  sort @{text "s"} to replace the hypothetical type variable @{text  wenzelm@58618  956  "\\<^sub>s"}.\  wenzelm@52406  957 wenzelm@58618  958 text %mlref \  wenzelm@52406  959  \begin{mldecls}  wenzelm@52406  960  @{index_ML Thm.extra_shyps: "thm -> sort list"} \\  wenzelm@52406  961  @{index_ML Thm.strip_shyps: "thm -> thm"} \\  wenzelm@52406  962  \end{mldecls}  wenzelm@52406  963 wenzelm@52406  964  \begin{description}  wenzelm@52406  965 wenzelm@52406  966  \item @{ML Thm.extra_shyps}~@{text "thm"} determines the extraneous  wenzelm@52406  967  sort hypotheses of the given theorem, i.e.\ the sorts that are not  wenzelm@52406  968  present within type variables of the statement.  wenzelm@52406  969 wenzelm@52406  970  \item @{ML Thm.strip_shyps}~@{text "thm"} removes any extraneous  wenzelm@52406  971  sort hypotheses that can be witnessed from the type signature.  wenzelm@52406  972 wenzelm@52406  973  \end{description}  wenzelm@58618  974 \  wenzelm@52406  975 wenzelm@58618  976 text %mlex \The following artificial example demonstrates the  wenzelm@52406  977  derivation of @{prop False} with a pending sort hypothesis involving  wenzelm@58618  978  a logically empty sort.\  wenzelm@52406  979 wenzelm@52406  980 class empty =  wenzelm@52406  981  assumes bad: "\(x::'a) y. x \ y"  wenzelm@52406  982 wenzelm@52406  983 theorem (in empty) false: False  wenzelm@52406  984  using bad by blast  wenzelm@52406  985 wenzelm@59902  986 ML_val \@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\  wenzelm@52406  987 wenzelm@58618  988 text \Thanks to the inference kernel managing sort hypothesis  wenzelm@52406  989  according to their logical significance, this example is merely an  wenzelm@52406  990  instance of \emph{ex falso quodlibet consequitur} --- not a collapse  wenzelm@58618  991  of the logical framework!\  wenzelm@52406  992 wenzelm@52406  993 wenzelm@58618  994 section \Object-level rules \label{sec:obj-rules}\  wenzelm@18537  995 wenzelm@58618  996 text \  wenzelm@29768  997  The primitive inferences covered so far mostly serve foundational  wenzelm@29768  998  purposes. User-level reasoning usually works via object-level rules  wenzelm@29768  999  that are represented as theorems of Pure. Composition of rules  wenzelm@29771  1000  involves \emph{backchaining}, \emph{higher-order unification} modulo  wenzelm@29771  1001  @{text "\\\"}-conversion of @{text "\"}-terms, and so-called  wenzelm@29771  1002  \emph{lifting} of rules into a context of @{text "\"} and @{text  wenzelm@29774  1003  "\"} connectives. Thus the full power of higher-order Natural  wenzelm@29774  1004  Deduction in Isabelle/Pure becomes readily available.  wenzelm@58618  1005 \  wenzelm@20491  1006 wenzelm@29769  1007 wenzelm@58618  1008 subsection \Hereditary Harrop Formulae\  wenzelm@29769  1009 wenzelm@58618  1010 text \  wenzelm@29768  1011  The idea of object-level rules is to model Natural Deduction  wenzelm@58555  1012  inferences in the style of Gentzen @{cite "Gentzen:1935"}, but we allow  wenzelm@58555  1013  arbitrary nesting similar to @{cite extensions91}. The most basic  wenzelm@29768  1014  rule format is that of a \emph{Horn Clause}:  wenzelm@29768  1015  $ wenzelm@29768  1016  \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\"} & @{text "A\<^sub>n"}}  wenzelm@29768  1017 $  wenzelm@29768  1018  where @{text "A, A\<^sub>1, \, A\<^sub>n"} are atomic propositions  wenzelm@29768  1019  of the framework, usually of the form @{text "Trueprop B"}, where  wenzelm@29768  1020  @{text "B"} is a (compound) object-level statement. This  wenzelm@29768  1021  object-level inference corresponds to an iterated implication in  wenzelm@29768  1022  Pure like this:  wenzelm@29768  1023  $ wenzelm@29768  1024  @{text "A\<^sub>1 \ \ A\<^sub>n \ A"}  wenzelm@29768  1025 $  wenzelm@29769  1026  As an example consider conjunction introduction: @{text "A \ B \ A \  wenzelm@29769  1027  B"}. Any parameters occurring in such rule statements are  wenzelm@29769  1028  conceptionally treated as arbitrary:  wenzelm@29768  1029  $ wenzelm@29769  1030  @{text "\x\<^sub>1 \ x\<^sub>m. A\<^sub>1 x\<^sub>1 \ x\<^sub>m \ \ A\<^sub>n x\<^sub>1 \ x\<^sub>m \ A x\<^sub>1 \ x\<^sub>m"}  wenzelm@29768  1031 $  wenzelm@20491  1032 wenzelm@29769  1033  Nesting of rules means that the positions of @{text "A\<^sub>i"} may  wenzelm@29770  1034  again hold compound rules, not just atomic propositions.  wenzelm@29769  1035  Propositions of this format are called \emph{Hereditary Harrop  wenzelm@58555  1036  Formulae} in the literature @{cite "Miller:1991"}. Here we give an  wenzelm@29769  1037  inductive characterization as follows:  wenzelm@29768  1038 wenzelm@29768  1039  \medskip  wenzelm@29768  1040  \begin{tabular}{ll}  wenzelm@29768  1041  @{text "\<^bold>x"} & set of variables \\  wenzelm@29768  1042  @{text "\<^bold>A"} & set of atomic propositions \\  wenzelm@29768  1043  @{text "\<^bold>H = \\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \ \<^bold>A"} & set of Hereditary Harrop Formulas \\  wenzelm@29768  1044  \end{tabular}  wenzelm@29768  1045  \medskip  wenzelm@29768  1046 wenzelm@39861  1047  Thus we essentially impose nesting levels on propositions formed  wenzelm@39861  1048  from @{text "\"} and @{text "\"}. At each level there is a prefix  wenzelm@39861  1049  of parameters and compound premises, concluding an atomic  wenzelm@29770  1050  proposition. Typical examples are @{text "\"}-introduction @{text  wenzelm@29770  1051  "(A \ B) \ A \ B"} or mathematical induction @{text "P 0 \ (\n. P n  wenzelm@29770  1052  \ P (Suc n)) \ P n"}. Even deeper nesting occurs in well-founded  wenzelm@29770  1053  induction @{text "(\x. (\y. y \ x \ P y) \ P x) \ P x"}, but this  wenzelm@34929  1054  already marks the limit of rule complexity that is usually seen in  wenzelm@34929  1055  practice.  wenzelm@29769  1056 wenzelm@29770  1057  \medskip Regular user-level inferences in Isabelle/Pure always  wenzelm@29770  1058  maintain the following canonical form of results:  wenzelm@29769  1059 wenzelm@29769  1060  \begin{itemize}  wenzelm@29768  1061 wenzelm@29774  1062  \item Normalization by @{text "(A \ (\x. B x)) \ (\x. A \ B x)"},  wenzelm@29774  1063  which is a theorem of Pure, means that quantifiers are pushed in  wenzelm@29774  1064  front of implication at each level of nesting. The normal form is a  wenzelm@29774  1065  Hereditary Harrop Formula.  wenzelm@29769  1066 wenzelm@29769  1067  \item The outermost prefix of parameters is represented via  wenzelm@29770  1068  schematic variables: instead of @{text "\\<^vec>x. \<^vec>H \<^vec>x  wenzelm@29774  1069  \ A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \ A ?\<^vec>x"}.  wenzelm@29774  1070  Note that this representation looses information about the order of  wenzelm@29774  1071  parameters, and vacuous quantifiers vanish automatically.  wenzelm@29769  1072 wenzelm@29769  1073  \end{itemize}  wenzelm@58618  1074 \  wenzelm@29769  1075 wenzelm@58618  1076 text %mlref \  wenzelm@29771  1077  \begin{mldecls}  wenzelm@54883  1078  @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\  wenzelm@29771  1079  \end{mldecls}  wenzelm@29771  1080 wenzelm@29771  1081  \begin{description}  wenzelm@29771  1082 wenzelm@54883  1083  \item @{ML Simplifier.norm_hhf}~@{text "ctxt thm"} normalizes the given  wenzelm@29771  1084  theorem according to the canonical form specified above. This is  wenzelm@29771  1085  occasionally helpful to repair some low-level tools that do not  wenzelm@29771  1086  handle Hereditary Harrop Formulae properly.  wenzelm@29771  1087 wenzelm@29771  1088  \end{description}  wenzelm@58618  1089 \  wenzelm@29771  1090 wenzelm@29769  1091 wenzelm@58618  1092 subsection \Rule composition\  wenzelm@29769  1093 wenzelm@58618  1094 text \  wenzelm@29771  1095  The rule calculus of Isabelle/Pure provides two main inferences:  wenzelm@29771  1096  @{inference resolution} (i.e.\ back-chaining of rules) and  wenzelm@29771  1097  @{inference assumption} (i.e.\ closing a branch), both modulo  wenzelm@29771  1098  higher-order unification. There are also combined variants, notably  wenzelm@29771  1099  @{inference elim_resolution} and @{inference dest_resolution}.  wenzelm@20491  1100 wenzelm@29771  1101  To understand the all-important @{inference resolution} principle,  wenzelm@29771  1102  we first consider raw @{inference_def composition} (modulo  wenzelm@29771  1103  higher-order unification with substitution @{text "\"}):  wenzelm@20498  1104  $ wenzelm@29771  1105  \infer[(@{inference_def composition})]{@{text "\<^vec>A\ \ C\"}}  wenzelm@20498  1106  {@{text "\<^vec>A \ B"} & @{text "B' \ C"} & @{text "B\ = B'\"}}  wenzelm@20498  1107 $  wenzelm@29771  1108  Here the conclusion of the first rule is unified with the premise of  wenzelm@29771  1109  the second; the resulting rule instance inherits the premises of the  wenzelm@29771  1110  first and conclusion of the second. Note that @{text "C"} can again  wenzelm@29771  1111  consist of iterated implications. We can also permute the premises  wenzelm@29771  1112  of the second rule back-and-forth in order to compose with @{text  wenzelm@29771  1113  "B'"} in any position (subsequently we shall always refer to  wenzelm@29771  1114  position 1 w.l.o.g.).  wenzelm@20498  1115 wenzelm@29774  1116  In @{inference composition} the internal structure of the common  wenzelm@29774  1117  part @{text "B"} and @{text "B'"} is not taken into account. For  wenzelm@29774  1118  proper @{inference resolution} we require @{text "B"} to be atomic,  wenzelm@29774  1119  and explicitly observe the structure @{text "\\<^vec>x. \<^vec>H  wenzelm@29774  1120  \<^vec>x \ B' \<^vec>x"} of the premise of the second rule. The  wenzelm@29774  1121  idea is to adapt the first rule by lifting'' it into this context,  wenzelm@29774  1122  by means of iterated application of the following inferences:  wenzelm@20498  1123  $ wenzelm@29771  1124  \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \ \<^vec>A) \ (\<^vec>H \ B)"}}{@{text "\<^vec>A \ B"}}  wenzelm@20498  1125 $  wenzelm@20498  1126  $ wenzelm@29771  1127  \infer[(@{inference_def all_lift})]{@{text "(\\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \ (\\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \ B ?\<^vec>a"}}  wenzelm@20498  1128 $  wenzelm@29771  1129  By combining raw composition with lifting, we get full @{inference  wenzelm@29771  1130  resolution} as follows:  wenzelm@20498  1131  $ wenzelm@29771  1132  \infer[(@{inference_def resolution})]  wenzelm@20498  1133  {@{text "(\\<^vec>x. \<^vec>H \<^vec>x \ \<^vec>A (?\<^vec>a \<^vec>x))\ \ C\"}}  wenzelm@20498  1134  {\begin{tabular}{l}  wenzelm@20498  1135  @{text "\<^vec>A ?\<^vec>a \ B ?\<^vec>a"} \\  wenzelm@20498  1136  @{text "(\\<^vec>x. \<^vec>H \<^vec>x \ B' \<^vec>x) \ C"} \\  wenzelm@20498  1137  @{text "(\\<^vec>x. B (?\<^vec>a \<^vec>x))\ = B'\"} \\  wenzelm@20498  1138  \end{tabular}}  wenzelm@20498  1139 $  wenzelm@20498  1140 wenzelm@29774  1141  Continued resolution of rules allows to back-chain a problem towards  wenzelm@29774  1142  more and sub-problems. Branches are closed either by resolving with  wenzelm@29774  1143  a rule of 0 premises, or by producing a short-circuit'' within a  wenzelm@29774  1144  solved situation (again modulo unification):  wenzelm@29771  1145  $ wenzelm@29771  1146  \infer[(@{inference_def assumption})]{@{text "C\"}}  wenzelm@29771  1147  {@{text "(\\<^vec>x. \<^vec>H \<^vec>x \ A \<^vec>x) \ C"} & @{text "A\ = H\<^sub>i\"}~~\text{(for some~@{text i})}}  wenzelm@29771  1148 $  wenzelm@20498  1149 wenzelm@52422  1150  %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}  wenzelm@58618  1151 \  wenzelm@18537  1152 wenzelm@58618  1153 text %mlref \  wenzelm@29768  1154  \begin{mldecls}  wenzelm@46262  1155  @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\  wenzelm@46262  1156  @{index_ML_op "RS": "thm * thm -> thm"} \\  wenzelm@46256  1157 wenzelm@46262  1158  @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\  wenzelm@46262  1159  @{index_ML_op "RL": "thm list * thm list -> thm list"} \\  wenzelm@46256  1160 wenzelm@46262  1161  @{index_ML_op "MRS": "thm list * thm -> thm"} \\  wenzelm@46262  1162  @{index_ML_op "OF": "thm * thm list -> thm"} \\  wenzelm@29768  1163  \end{mldecls}  wenzelm@29768  1164 wenzelm@29768  1165  \begin{description}  wenzelm@29768  1166 wenzelm@46256  1167  \item @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of  wenzelm@46256  1168  @{text "rule\<^sub>1"} with the @{text i}-th premise of @{text "rule\<^sub>2"},  wenzelm@46256  1169  according to the @{inference resolution} principle explained above.  wenzelm@46256  1170  Unless there is precisely one resolvent it raises exception @{ML  wenzelm@46256  1171  THM}.  wenzelm@46256  1172 wenzelm@46256  1173  This corresponds to the rule attribute @{attribute THEN} in Isar  wenzelm@46256  1174  source language.  wenzelm@46256  1175 wenzelm@53200  1176  \item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RSN (1,  wenzelm@46256  1177  rule\<^sub>2)"}.  wenzelm@29768  1178 wenzelm@46256  1179  \item @{text "rules\<^sub>1 RLN (i, rules\<^sub>2)"} joins lists of rules. For  wenzelm@46256  1180  every @{text "rule\<^sub>1"} in @{text "rules\<^sub>1"} and @{text "rule\<^sub>2"} in  wenzelm@46256  1181  @{text "rules\<^sub>2"}, it resolves the conclusion of @{text "rule\<^sub>1"} with  wenzelm@46256  1182  the @{text "i"}-th premise of @{text "rule\<^sub>2"}, accumulating multiple  wenzelm@46256  1183  results in one big list. Note that such strict enumerations of  wenzelm@46256  1184  higher-order unifications can be inefficient compared to the lazy  wenzelm@46256  1185  variant seen in elementary tactics like @{ML resolve_tac}.  wenzelm@46256  1186 wenzelm@46256  1187  \item @{text "rules\<^sub>1 RL rules\<^sub>2"} abbreviates @{text "rules\<^sub>1 RLN (1,  wenzelm@46256  1188  rules\<^sub>2)"}.  wenzelm@46256  1189 wenzelm@53015  1190  \item @{text "[rule\<^sub>1, \, rule\<^sub>n] MRS rule"} resolves @{text "rule\<^sub>i"}  wenzelm@46256  1191  against premise @{text "i"} of @{text "rule"}, for @{text "i = n, \,  wenzelm@46256  1192  1"}. By working from right to left, newly emerging premises are  wenzelm@46256  1193  concatenated in the result, without interfering.  wenzelm@46256  1194 wenzelm@47498  1195  \item @{text "rule OF rules"} is an alternative notation for @{text  wenzelm@47498  1196  "rules MRS rule"}, which makes rule composition look more like  wenzelm@47498  1197  function application. Note that the argument @{text "rules"} need  wenzelm@47498  1198  not be atomic.  wenzelm@46256  1199 wenzelm@46256  1200  This corresponds to the rule attribute @{attribute OF} in Isar  wenzelm@46256  1201  source language.  wenzelm@29768  1202 wenzelm@29768  1203  \end{description}  wenzelm@58618  1204 \  wenzelm@30272  1205 wenzelm@52407  1206 wenzelm@58618  1207 section \Proof terms \label{sec:proof-terms}\  wenzelm@52407  1208 wenzelm@58618  1209 text \The Isabelle/Pure inference kernel can record the proof of  wenzelm@52407  1210  each theorem as a proof term that contains all logical inferences in  wenzelm@52407  1211  detail. Rule composition by resolution (\secref{sec:obj-rules}) and  wenzelm@52407  1212  type-class reasoning is broken down to primitive rules of the  wenzelm@52407  1213  logical framework. The proof term can be inspected by a separate  wenzelm@52407  1214  proof-checker, for example.  wenzelm@52407  1215 wenzelm@52407  1216  According to the well-known \emph{Curry-Howard isomorphism}, a proof  wenzelm@52407  1217  can be viewed as a @{text "\"}-term. Following this idea, proofs in  wenzelm@52407  1218  Isabelle are internally represented by a datatype similar to the one  wenzelm@52407  1219  for terms described in \secref{sec:terms}. On top of these  wenzelm@52407  1220  syntactic terms, two more layers of @{text "\"}-calculus are added,  wenzelm@52407  1221  which correspond to @{text "\x :: \. B x"} and @{text "A \ B"}  wenzelm@52407  1222  according to the propositions-as-types principle. The resulting  wenzelm@52407  1223  3-level @{text "\"}-calculus resembles @{text "\HOL"}'' in the  wenzelm@52407  1224  more abstract setting of Pure Type Systems (PTS)  wenzelm@58555  1225  @{cite "Barendregt-Geuvers:2001"}, if some fine points like schematic  wenzelm@52407  1226  polymorphism and type classes are ignored.  wenzelm@52407  1227 wenzelm@52407  1228  \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\x :: \. prf"}  wenzelm@52407  1229  or @{text "\<^bold>\p : A. prf"} correspond to introduction of @{text  wenzelm@52407  1230  "\"}/@{text "\"}, and \emph{proof applications} of the form @{text  wenzelm@52407  1231  "p \ t"} or @{text "p \ q"} correspond to elimination of @{text  wenzelm@52407  1232  "\"}/@{text "\"}. Actual types @{text "\"}, propositions @{text  wenzelm@52407  1233  "A"}, and terms @{text "t"} might be suppressed and reconstructed  wenzelm@52407  1234  from the overall proof term.  wenzelm@52407  1235 wenzelm@52407  1236  \medskip Various atomic proofs indicate special situations within  wenzelm@52407  1237  the proof construction as follows.  wenzelm@52407  1238 wenzelm@52407  1239  A \emph{bound proof variable} is a natural number @{text "b"} that  wenzelm@52407  1240  acts as de-Bruijn index for proof term abstractions.  wenzelm@52407  1241 wenzelm@52407  1242  A \emph{minimal proof} @{text "?"}'' is a dummy proof term. This  wenzelm@52407  1243  indicates some unrecorded part of the proof.  wenzelm@52407  1244 wenzelm@52407  1245  @{text "Hyp A"} refers to some pending hypothesis by giving its  wenzelm@52407  1246  proposition. This indicates an open context of implicit hypotheses,  wenzelm@52407  1247  similar to loose bound variables or free variables within a term  wenzelm@52407  1248  (\secref{sec:terms}).  wenzelm@52407  1249 wenzelm@52407  1250  An \emph{axiom} or \emph{oracle} @{text "a : A[\<^vec>\]"} refers  wenzelm@52407  1251  some postulated @{text "proof constant"}, which is subject to  wenzelm@52407  1252  schematic polymorphism of theory content, and the particular type  wenzelm@52407  1253  instantiation may be given explicitly. The vector of types @{text  wenzelm@52407  1254  "\<^vec>\"} refers to the schematic type variables in the generic  wenzelm@52407  1255  proposition @{text "A"} in canonical order.  wenzelm@52407  1256 wenzelm@52407  1257  A \emph{proof promise} @{text "a : A[\<^vec>\]"} is a placeholder  wenzelm@52407  1258  for some proof of polymorphic proposition @{text "A"}, with explicit  wenzelm@52407  1259  type instantiation as given by the vector @{text "\<^vec>\"}, as  wenzelm@52407  1260  above. Unlike axioms or oracles, proof promises may be  wenzelm@52407  1261  \emph{fulfilled} eventually, by substituting @{text "a"} by some  wenzelm@52407  1262  particular proof @{text "q"} at the corresponding type instance.  wenzelm@52407  1263  This acts like Hindley-Milner @{text "let"}-polymorphism: a generic  wenzelm@52407  1264  local proof definition may get used at different type instances, and  wenzelm@52407  1265  is replaced by the concrete instance eventually.  wenzelm@52407  1266 wenzelm@52407  1267  A \emph{named theorem} wraps up some concrete proof as a closed  wenzelm@52407  1268  formal entity, in the manner of constant definitions for proof  wenzelm@52407  1269  terms. The \emph{proof body} of such boxed theorems involves some  wenzelm@52407  1270  digest about oracles and promises occurring in the original proof.  wenzelm@52407  1271  This allows the inference kernel to manage this critical information  wenzelm@52407  1272  without the full overhead of explicit proof terms.  wenzelm@58618  1273 \  wenzelm@52407  1274 wenzelm@52411  1275 wenzelm@58618  1276 subsection \Reconstructing and checking proof terms\  wenzelm@52411  1277 wenzelm@58618  1278 text \Fully explicit proof terms can be large, but most of this  wenzelm@52411  1279  information is redundant and can be reconstructed from the context.  wenzelm@52411  1280  Therefore, the Isabelle/Pure inference kernel records only  wenzelm@52411  1281  \emph{implicit} proof terms, by omitting all typing information in  wenzelm@52411  1282  terms, all term and type labels of proof abstractions, and some  wenzelm@52411  1283  argument terms of applications @{text "p \ t"} (if possible).  wenzelm@52411  1284 wenzelm@52411  1285  There are separate operations to reconstruct the full proof term  wenzelm@52411  1286  later on, using \emph{higher-order pattern unification}  wenzelm@58555  1287  @{cite "nipkow-patterns" and "Berghofer-Nipkow:2000:TPHOL"}.  wenzelm@52411  1288 wenzelm@52411  1289  The \emph{proof checker} expects a fully reconstructed proof term,  wenzelm@52411  1290  and can turn it into a theorem by replaying its primitive inferences  wenzelm@58618  1291  within the kernel.\  wenzelm@52411  1292 wenzelm@52412  1293 wenzelm@58618  1294 subsection \Concrete syntax of proof terms\  wenzelm@52412  1295 wenzelm@58618  1296 text \The concrete syntax of proof terms is a slight extension of  wenzelm@58555  1297  the regular inner syntax of Isabelle/Pure @{cite "isabelle-isar-ref"}.  wenzelm@52412  1298  Its main syntactic category @{syntax (inner) proof} is defined as  wenzelm@52412  1299  follows:  wenzelm@52412  1300 wenzelm@52412  1301  \begin{center}  wenzelm@52412  1302  \begin{supertabular}{rclr}  wenzelm@52412  1303 wenzelm@52412  1304  @{syntax_def (inner) proof} & = & @{verbatim Lam} @{text params} @{verbatim "."} @{text proof} \\  wenzelm@52486  1305  & @{text "|"} & @{text "\<^bold>\"} @{text "params"} @{verbatim "."} @{text proof} \\  wenzelm@52412  1306  & @{text "|"} & @{text proof} @{verbatim "%"} @{text any} \\  wenzelm@52412  1307  & @{text "|"} & @{text proof} @{text "\"} @{text any} \\  wenzelm@52412  1308  & @{text "|"} & @{text proof} @{verbatim "%%"} @{text proof} \\  wenzelm@52412  1309  & @{text "|"} & @{text proof} @{text "\"} @{text proof} \\  wenzelm@52412  1310  & @{text "|"} & @{text "id | longid"} \\  wenzelm@52412  1311  \\  wenzelm@52412  1312 wenzelm@52412  1313  @{text param} & = & @{text idt} \\  wenzelm@52412  1314  & @{text "|"} & @{text idt} @{verbatim ":"} @{text prop} \\  wenzelm@52412  1315  & @{text "|"} & @{verbatim "("} @{text param} @{verbatim ")"} \\  wenzelm@52412  1316  \\  wenzelm@52412  1317 wenzelm@52412  1318  @{text params} & = & @{text param} \\  wenzelm@52412  1319  & @{text "|"} & @{text param} @{text params} \\  wenzelm@52412  1320 wenzelm@52412  1321  \end{supertabular}  wenzelm@52412  1322  \end{center}  wenzelm@52412  1323 wenzelm@52412  1324  Implicit term arguments in partial proofs are indicated by @{text  wenzelm@52412  1325  "_"}''. Type arguments for theorems and axioms may be specified  wenzelm@52412  1326  using @{text "p \ TYPE(type)"} (they must appear before any other  wenzelm@52412  1327  term argument of a theorem or axiom, but may be omitted altogether).  wenzelm@52412  1328 wenzelm@52412  1329  \medskip There are separate read and print operations for proof  wenzelm@52412  1330  terms, in order to avoid conflicts with the regular term language.  wenzelm@58618  1331 \  wenzelm@52412  1332 wenzelm@58618  1333 text %mlref \  wenzelm@52408  1334  \begin{mldecls}  wenzelm@52408  1335  @{index_ML_type proof} \\  wenzelm@52408  1336  @{index_ML_type proof_body} \\  wenzelm@52487  1337  @{index_ML proofs: "int Unsynchronized.ref"} \\  wenzelm@52411  1338  @{index_ML Reconstruct.reconstruct_proof:  wenzelm@52411  1339  "theory -> term -> proof -> proof"} \\  wenzelm@52411  1340  @{index_ML Reconstruct.expand_proof: "theory ->  wenzelm@52411  1341  (string * term option) list -> proof -> proof"} \\  wenzelm@52412  1342  @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\  wenzelm@52412  1343  @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\  wenzelm@52412  1344  @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\  wenzelm@52408  1345  \end{mldecls}  wenzelm@52408  1346 wenzelm@52408  1347  \begin{description}  wenzelm@52408  1348 wenzelm@52408  1349  \item Type @{ML_type proof} represents proof terms; this is a  wenzelm@52408  1350  datatype with constructors @{index_ML Abst}, @{index_ML AbsP},  wenzelm@52408  1351  @{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound},  wenzelm@52408  1352  @{index_ML MinProof}, @{index_ML Hyp}, @{index_ML PAxm}, @{index_ML  wenzelm@52408  1353  Oracle}, @{index_ML Promise}, @{index_ML PThm} as explained above.  wenzelm@52436  1354  %FIXME OfClass (!?)  wenzelm@52408  1355 wenzelm@52408  1356  \item Type @{ML_type proof_body} represents the nested proof  wenzelm@52408  1357  information of a named theorem, consisting of a digest of oracles  wenzelm@52408  1358  and named theorem over some proof term. The digest only covers the  wenzelm@52408  1359  directly visible part of the proof: in order to get the full  wenzelm@52408  1360  information, the implicit graph of nested theorems needs to be  wenzelm@52408  1361  traversed (e.g.\ using @{ML Proofterm.fold_body_thms}).  wenzelm@52408  1362 wenzelm@52408  1363  \item @{ML Thm.proof_of}~@{text "thm"} and @{ML  wenzelm@52408  1364  Thm.proof_body_of}~@{text "thm"} produce the proof term or proof  wenzelm@52408  1365  body (with digest of oracles and theorems) from a given theorem.  wenzelm@52408  1366  Note that this involves a full join of internal futures that fulfill  wenzelm@52408  1367  pending proof promises, and thus disrupts the natural bottom-up  wenzelm@52408  1368  construction of proofs by introducing dynamic ad-hoc dependencies.  wenzelm@52408  1369  Parallel performance may suffer by inspecting proof terms at  wenzelm@52408  1370  run-time.  wenzelm@52408  1371 wenzelm@52487  1372  \item @{ML proofs} specifies the detail of proof recording within  wenzelm@52487  1373  @{ML_type thm} values produced by the inference kernel: @{ML 0}  wenzelm@52487  1374  records only the names of oracles, @{ML 1} records oracle names and  wenzelm@52487  1375  propositions, @{ML 2} additionally records full proof terms.  wenzelm@52487  1376  Officially named theorems that contribute to a result are recorded  wenzelm@52487  1377  in any case.  wenzelm@52487  1378 wenzelm@52411  1379  \item @{ML Reconstruct.reconstruct_proof}~@{text "thy prop prf"}  wenzelm@52411  1380  turns the implicit proof term @{text "prf"} into a full proof of the  wenzelm@52411  1381  given proposition.  wenzelm@52411  1382 wenzelm@52411  1383  Reconstruction may fail if @{text "prf"} is not a proof of @{text  wenzelm@52411  1384  "prop"}, or if it does not contain sufficient information for  wenzelm@52411  1385  reconstruction. Failure may only happen for proofs that are  wenzelm@52411  1386  constructed manually, but not for those produced automatically by  wenzelm@52411  1387  the inference kernel.  wenzelm@52411  1388 wenzelm@52411  1389  \item @{ML Reconstruct.expand_proof}~@{text "thy [thm\<^sub>1, \, thm\<^sub>n]  wenzelm@52411  1390  prf"} expands and reconstructs the proofs of all specified theorems,  wenzelm@52411  1391  with the given (full) proof. Theorems that are not unique specified  wenzelm@52411  1392  via their name may be disambiguated by giving their proposition.  wenzelm@52411  1393 wenzelm@52411  1394  \item @{ML Proof_Checker.thm_of_proof}~@{text "thy prf"} turns the  wenzelm@52411  1395  given (full) proof into a theorem, by replaying it using only  wenzelm@52411  1396  primitive rules of the inference kernel.  wenzelm@52411  1397 wenzelm@52412  1398  \item @{ML Proof_Syntax.read_proof}~@{text "thy b\<^sub>1 b\<^sub>2 s"} reads in a  wenzelm@52412  1399  proof term. The Boolean flags indicate the use of sort and type  wenzelm@52412  1400  information. Usually, typing information is left implicit and is  wenzelm@52412  1401  inferred during proof reconstruction. %FIXME eliminate flags!?  wenzelm@52412  1402 wenzelm@52412  1403  \item @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"}  wenzelm@52412  1404  pretty-prints the given proof term.  wenzelm@52412  1405 wenzelm@52408  1406  \end{description}  wenzelm@58618  1407 \  wenzelm@52408  1408 wenzelm@58618  1409 text %mlex \Detailed proof information of a theorem may be retrieved  wenzelm@58618  1410  as follows:\  wenzelm@52410  1411 wenzelm@52410  1412 lemma ex: "A \ B \ B \ A"  wenzelm@52410  1413 proof  wenzelm@52410  1414  assume "A \ B"  wenzelm@52410  1415  then obtain B and A ..  wenzelm@52410  1416  then show "B \ A" ..  wenzelm@52410  1417 qed  wenzelm@52410  1418 wenzelm@58618  1419 ML_val \  wenzelm@52410  1420  (*proof body with digest*)  wenzelm@52410  1421  val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});  wenzelm@52410  1422 wenzelm@52410  1423  (*proof term only*)  wenzelm@52410  1424  val prf = Proofterm.proof_of body;  wenzelm@52410  1425  Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);  wenzelm@52410  1426 wenzelm@52410  1427  (*all theorems used in the graph of nested proofs*)  wenzelm@52410  1428  val all_thms =  wenzelm@52410  1429  Proofterm.fold_body_thms  wenzelm@52410  1430  (fn (name, _, _) => insert (op =) name) [body] [];  wenzelm@58618  1431 \  wenzelm@52410  1432 wenzelm@58618  1433 text \The result refers to various basic facts of Isabelle/HOL:  wenzelm@52410  1434  @{thm [source] HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source]  wenzelm@52410  1435  HOL.conjI} etc. The combinator @{ML Proofterm.fold_body_thms}  wenzelm@52410  1436  recursively explores the graph of the proofs of all theorems being  wenzelm@52410  1437  used here.  wenzelm@52410  1438 wenzelm@52410  1439  \medskip Alternatively, we may produce a proof term manually, and  wenzelm@58618  1440  turn it into a theorem as follows:\  wenzelm@52410  1441 wenzelm@58618  1442 ML_val \  wenzelm@52410  1443  val thy = @{theory};  wenzelm@52410  1444  val prf =  wenzelm@52410  1445  Proof_Syntax.read_proof thy true false  wenzelm@52410  1446  "impI \ _ \ _ \ \  wenzelm@52486  1447  \ (\<^bold>\H: _. \  wenzelm@52410  1448  \ conjE \ _ \ _ \ _ \ H \ \  wenzelm@52486  1449  \ (\<^bold>\(H: _) Ha: _. conjI \ _ \ _ \ Ha \ H))";  wenzelm@52410  1450  val thm =  wenzelm@52410  1451  prf  wenzelm@52410  1452  |> Reconstruct.reconstruct_proof thy @{prop "A \ B \ B \ A"}  wenzelm@52410  1453  |> Proof_Checker.thm_of_proof thy  wenzelm@52410  1454  |> Drule.export_without_context;  wenzelm@58618  1455 \  wenzelm@52410  1456 wenzelm@58618  1457 text \\medskip See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"}  wenzelm@52630  1458  for further examples, with export and import of proof terms via  wenzelm@52630  1459  XML/ML data representation.  wenzelm@58618  1460 \  wenzelm@52410  1461 wenzelm@18537  1462 end