doc-src/IsarImplementation/Thy/Logic.thy
 author wenzelm Fri Feb 20 18:48:58 2009 +0100 (2009-02-20) changeset 29769 03634a9e91ae parent 29768 64a50ff3f308 child 29770 cac2ca7bbc08 permissions -rw-r--r--
improved section on "Hereditary Harrop Formulae";
 wenzelm@29755  1 theory Logic  wenzelm@29755  2 imports Base  wenzelm@29755  3 begin  wenzelm@18537  4 wenzelm@20470  5 chapter {* Primitive logic \label{ch:logic} *}  wenzelm@18537  6 wenzelm@20480  7 text {*  wenzelm@20480  8  The logical foundations of Isabelle/Isar are that of the Pure logic,  wenzelm@20480  9  which has been introduced as a natural-deduction framework in  wenzelm@20480  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@20480  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@20537  27  of the core calculus.}  wenzelm@20480  28 *}  wenzelm@20480  29 wenzelm@20480  30 wenzelm@20451  31 section {* Types \label{sec:types} *}  wenzelm@20437  32 wenzelm@20437  33 text {*  wenzelm@20480  34  The language of types is an uninterpreted order-sorted first-order  wenzelm@20480  35  algebra; types are qualified by ordered type classes.  wenzelm@20480  36 wenzelm@20480  37  \medskip A \emph{type class} is an abstract syntactic entity  wenzelm@20480  38  declared in the theory context. The \emph{subclass relation} @{text  wenzelm@20480  39  "c\<^isub>1 \ c\<^isub>2"} is specified by stating an acyclic  wenzelm@20491  40  generating relation; the transitive closure is maintained  wenzelm@20491  41  internally. The resulting relation is an ordering: reflexive,  wenzelm@20491  42  transitive, and antisymmetric.  wenzelm@20451  43 wenzelm@20537  44  A \emph{sort} is a list of type classes written as @{text "s =  wenzelm@20537  45  {c\<^isub>1, \, c\<^isub>m}"}, which represents symbolic  wenzelm@20480  46  intersection. Notationally, the curly braces are omitted for  wenzelm@20480  47  singleton intersections, i.e.\ any class @{text "c"} may be read as  wenzelm@20480  48  a sort @{text "{c}"}. The ordering on type classes is extended to  wenzelm@20491  49  sorts according to the meaning of intersections: @{text  wenzelm@20491  50  "{c\<^isub>1, \ c\<^isub>m} \ {d\<^isub>1, \, d\<^isub>n}"} iff  wenzelm@20491  51  @{text "\j. \i. c\<^isub>i \ d\<^isub>j"}. The empty intersection  wenzelm@20491  52  @{text "{}"} refers to the universal sort, which is the largest  wenzelm@20491  53  element wrt.\ the sort order. The intersections of all (finitely  wenzelm@20491  54  many) classes declared in the current theory are the minimal  wenzelm@20491  55  elements wrt.\ the sort order.  wenzelm@20480  56 wenzelm@20491  57  \medskip A \emph{fixed type variable} is a pair of a basic name  wenzelm@20537  58  (starting with a @{text "'"} character) and a sort constraint, e.g.\  wenzelm@20537  59  @{text "('a, s)"} which is usually printed as @{text "\\<^isub>s"}.  wenzelm@20537  60  A \emph{schematic type variable} is a pair of an indexname and a  wenzelm@20537  61  sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually  wenzelm@20537  62  printed as @{text "?\\<^isub>s"}.  wenzelm@20451  63 wenzelm@20480  64  Note that \emph{all} syntactic components contribute to the identity  wenzelm@20493  65  of type variables, including the sort constraint. The core logic  wenzelm@20493  66  handles type variables with the same name but different sorts as  wenzelm@20493  67  different, although some outer layers of the system make it hard to  wenzelm@20493  68  produce anything like this.  wenzelm@20451  69 wenzelm@20493  70  A \emph{type constructor} @{text "\"} is a @{text "k"}-ary operator  wenzelm@20493  71  on types declared in the theory. Type constructor application is  wenzelm@20537  72  written postfix as @{text "(\\<^isub>1, \, \\<^isub>k)\"}. For  wenzelm@20537  73  @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}  wenzelm@20537  74  instead of @{text "()prop"}. For @{text "k = 1"} the parentheses  wenzelm@20537  75  are omitted, e.g.\ @{text "\ list"} instead of @{text "(\)list"}.  wenzelm@20537  76  Further notation is provided for specific constructors, notably the  wenzelm@20537  77  right-associative infix @{text "\ \ \"} instead of @{text "(\,  wenzelm@20537  78  \)fun"}.  wenzelm@20480  79   wenzelm@20537  80  A \emph{type} is defined inductively over type variables and type  wenzelm@20537  81  constructors as follows: @{text "\ = \\<^isub>s | ?\\<^isub>s |  wenzelm@20543  82  (\\<^sub>1, \, \\<^sub>k)\"}.  wenzelm@20451  83 wenzelm@20514  84  A \emph{type abbreviation} is a syntactic definition @{text  wenzelm@20494  85  "(\<^vec>\)\ = \"} of an arbitrary type expression @{text "\"} over  wenzelm@20537  86  variables @{text "\<^vec>\"}. Type abbreviations appear as type  wenzelm@20537  87  constructors in the syntax, but are expanded before entering the  wenzelm@20537  88  logical core.  wenzelm@20480  89 wenzelm@20480  90  A \emph{type arity} declares the image behavior of a type  wenzelm@20494  91  constructor wrt.\ the algebra of sorts: @{text "\ :: (s\<^isub>1, \,  wenzelm@20494  92  s\<^isub>k)s"} means that @{text "(\\<^isub>1, \, \\<^isub>k)\"} is  wenzelm@20494  93  of sort @{text "s"} if every argument type @{text "\\<^isub>i"} is  wenzelm@20494  94  of sort @{text "s\<^isub>i"}. Arity declarations are implicitly  wenzelm@20494  95  completed, i.e.\ @{text "\ :: (\<^vec>s)c"} entails @{text "\ ::  wenzelm@20491  96  (\<^vec>s)c'"} for any @{text "c' \ c"}.  wenzelm@20491  97 wenzelm@20491  98  \medskip The sort algebra is always maintained as \emph{coregular},  wenzelm@20491  99  which means that type arities are consistent with the subclass  wenzelm@20537  100  relation: for any type constructor @{text "\"}, and classes @{text  wenzelm@20537  101  "c\<^isub>1 \ c\<^isub>2"}, and arities @{text "\ ::  wenzelm@20537  102  (\<^vec>s\<^isub>1)c\<^isub>1"} and @{text "\ ::  wenzelm@20537  103  (\<^vec>s\<^isub>2)c\<^isub>2"} holds @{text "\<^vec>s\<^isub>1 \  wenzelm@20537  104  \<^vec>s\<^isub>2"} component-wise.  wenzelm@20451  105 wenzelm@20491  106  The key property of a coregular order-sorted algebra is that sort  wenzelm@20537  107  constraints can be solved in a most general fashion: for each type  wenzelm@20537  108  constructor @{text "\"} and sort @{text "s"} there is a most general  wenzelm@20537  109  vector of argument sorts @{text "(s\<^isub>1, \, s\<^isub>k)"} such  wenzelm@20537  110  that a type scheme @{text "(\\<^bsub>s\<^isub>1\<^esub>, \,  wenzelm@20537  111  \\<^bsub>s\<^isub>k\<^esub>)\"} is of sort @{text "s"}.  wenzelm@20543  112  Consequently, type unification has most general solutions (modulo  wenzelm@20543  113  equivalence of sorts), so type-inference produces primary types as  wenzelm@20543  114  expected \cite{nipkow-prehofer}.  wenzelm@20480  115 *}  wenzelm@20451  116 wenzelm@20480  117 text %mlref {*  wenzelm@20480  118  \begin{mldecls}  wenzelm@20480  119  @{index_ML_type class} \\  wenzelm@20480  120  @{index_ML_type sort} \\  wenzelm@20494  121  @{index_ML_type arity} \\  wenzelm@20480  122  @{index_ML_type typ} \\  wenzelm@20519  123  @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\  wenzelm@20494  124  @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\  wenzelm@20547  125  \end{mldecls}  wenzelm@20547  126  \begin{mldecls}  wenzelm@20480  127  @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\  wenzelm@20480  128  @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\  wenzelm@20520  129  @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\  wenzelm@20480  130  @{index_ML Sign.add_tyabbrs_i: "  wenzelm@20520  131  (string * string list * typ * mixfix) list -> theory -> theory"} \\  wenzelm@20480  132  @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\  wenzelm@20480  133  @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\  wenzelm@20480  134  @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\  wenzelm@20480  135  \end{mldecls}  wenzelm@20480  136 wenzelm@20480  137  \begin{description}  wenzelm@20480  138 wenzelm@20480  139  \item @{ML_type class} represents type classes; this is an alias for  wenzelm@20480  140  @{ML_type string}.  wenzelm@20480  141 wenzelm@20480  142  \item @{ML_type sort} represents sorts; this is an alias for  wenzelm@20480  143  @{ML_type "class list"}.  wenzelm@20451  144 wenzelm@20480  145  \item @{ML_type arity} represents type arities; this is an alias for  wenzelm@20494  146  triples of the form @{text "(\, \<^vec>s, s)"} for @{text "\ ::  wenzelm@20480  147  (\<^vec>s)s"} described above.  wenzelm@20480  148 wenzelm@20480  149  \item @{ML_type typ} represents types; this is a datatype with  wenzelm@20480  150  constructors @{ML TFree}, @{ML TVar}, @{ML Type}.  wenzelm@20480  151 wenzelm@20537  152  \item @{ML map_atyps}~@{text "f \"} applies the mapping @{text "f"}  wenzelm@20537  153  to all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text  wenzelm@20537  154  "\"}.  wenzelm@20519  155 wenzelm@20537  156  \item @{ML fold_atyps}~@{text "f \"} iterates the operation @{text  wenzelm@20537  157  "f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar})  wenzelm@20537  158  in @{text "\"}; the type structure is traversed from left to right.  wenzelm@20494  159 wenzelm@20480  160  \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}  wenzelm@20480  161  tests the subsort relation @{text "s\<^isub>1 \ s\<^isub>2"}.  wenzelm@20480  162 wenzelm@20537  163  \item @{ML Sign.of_sort}~@{text "thy (\, s)"} tests whether type  wenzelm@20537  164  @{text "\"} is of sort @{text "s"}.  wenzelm@20480  165 wenzelm@20537  166  \item @{ML Sign.add_types}~@{text "[(\, k, mx), \]"} declares a new  wenzelm@20494  167  type constructors @{text "\"} with @{text "k"} arguments and  wenzelm@20480  168  optional mixfix syntax.  wenzelm@20451  169 wenzelm@20494  170  \item @{ML Sign.add_tyabbrs_i}~@{text "[(\, \<^vec>\, \, mx), \]"}  wenzelm@20494  171  defines a new type abbreviation @{text "(\<^vec>\)\ = \"} with  wenzelm@20491  172  optional mixfix syntax.  wenzelm@20480  173 wenzelm@20480  174  \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \,  wenzelm@20537  175  c\<^isub>n])"} declares a new class @{text "c"}, together with class  wenzelm@20494  176  relations @{text "c \ c\<^isub>i"}, for @{text "i = 1, \, n"}.  wenzelm@20480  177 wenzelm@20480  178  \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,  wenzelm@20543  179  c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \  wenzelm@20480  180  c\<^isub>2"}.  wenzelm@20480  181 wenzelm@20494  182  \item @{ML Sign.primitive_arity}~@{text "(\, \<^vec>s, s)"} declares  wenzelm@20537  183  the arity @{text "\ :: (\<^vec>s)s"}.  wenzelm@20480  184 wenzelm@20480  185  \end{description}  wenzelm@20437  186 *}  wenzelm@20437  187 wenzelm@20437  188 wenzelm@20451  189 section {* Terms \label{sec:terms} *}  wenzelm@18537  190 wenzelm@18537  191 text {*  wenzelm@20491  192  The language of terms is that of simply-typed @{text "\"}-calculus  wenzelm@20520  193  with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}  wenzelm@29761  194  or \cite{paulson-ml2}), with the types being determined by the  wenzelm@29761  195  corresponding binders. In contrast, free variables and constants  wenzelm@29761  196  are have an explicit name and type in each occurrence.  wenzelm@20514  197 wenzelm@20514  198  \medskip A \emph{bound variable} is a natural number @{text "b"},  wenzelm@20537  199  which accounts for the number of intermediate binders between the  wenzelm@20537  200  variable occurrence in the body and its binding position. For  wenzelm@20543  201  example, the de-Bruijn term @{text  wenzelm@20543  202  "\\<^bsub>nat\<^esub>. \\<^bsub>nat\<^esub>. 1 + 0"} would  wenzelm@20543  203  correspond to @{text  wenzelm@20543  204  "\x\<^bsub>nat\<^esub>. \y\<^bsub>nat\<^esub>. x + y"} in a named  wenzelm@20543  205  representation. Note that a bound variable may be represented by  wenzelm@20543  206  different de-Bruijn indices at different occurrences, depending on  wenzelm@20543  207  the nesting of abstractions.  wenzelm@20537  208 wenzelm@20543  209  A \emph{loose variable} is a bound variable that is outside the  wenzelm@20537  210  scope of local binders. The types (and names) for loose variables  wenzelm@20543  211  can be managed as a separate context, that is maintained as a stack  wenzelm@20543  212  of hypothetical binders. The core logic operates on closed terms,  wenzelm@20543  213  without any loose variables.  wenzelm@20514  214 wenzelm@20537  215  A \emph{fixed variable} is a pair of a basic name and a type, e.g.\  wenzelm@20537  216  @{text "(x, \)"} which is usually printed @{text "x\<^isub>\"}. A  wenzelm@20537  217  \emph{schematic variable} is a pair of an indexname and a type,  wenzelm@20537  218  e.g.\ @{text "((x, 0), \)"} which is usually printed as @{text  wenzelm@20537  219  "?x\<^isub>\"}.  wenzelm@20491  220 wenzelm@20537  221  \medskip A \emph{constant} is a pair of a basic name and a type,  wenzelm@20537  222  e.g.\ @{text "(c, \)"} which is usually printed as @{text  wenzelm@20537  223  "c\<^isub>\"}. Constants are declared in the context as polymorphic  wenzelm@20543  224  families @{text "c :: \"}, meaning that all substitution instances  wenzelm@20543  225  @{text "c\<^isub>\"} for @{text "\ = \\"} are valid.  wenzelm@20514  226 wenzelm@20537  227  The vector of \emph{type arguments} of constant @{text "c\<^isub>\"}  wenzelm@20537  228  wrt.\ the declaration @{text "c :: \"} is defined as the codomain of  wenzelm@20537  229  the matcher @{text "\ = {?\\<^isub>1 \ \\<^isub>1, \,  wenzelm@20537  230  ?\\<^isub>n \ \\<^isub>n}"} presented in canonical order @{text  wenzelm@20537  231  "(\\<^isub>1, \, \\<^isub>n)"}. Within a given theory context,  wenzelm@20537  232  there is a one-to-one correspondence between any constant @{text  wenzelm@20537  233  "c\<^isub>\"} and the application @{text "c(\\<^isub>1, \,  wenzelm@20537  234  \\<^isub>n)"} of its type arguments. For example, with @{text "plus  wenzelm@20537  235  :: \ \ \ \ \"}, the instance @{text "plus\<^bsub>nat \ nat \  wenzelm@20537  236  nat\<^esub>"} corresponds to @{text "plus(nat)"}.  wenzelm@20480  237 wenzelm@20514  238  Constant declarations @{text "c :: \"} may contain sort constraints  wenzelm@20514  239  for type variables in @{text "\"}. These are observed by  wenzelm@20514  240  type-inference as expected, but \emph{ignored} by the core logic.  wenzelm@20514  241  This means the primitive logic is able to reason with instances of  wenzelm@20537  242  polymorphic constants that the user-level type-checker would reject  wenzelm@20537  243  due to violation of type class restrictions.  wenzelm@20480  244 wenzelm@20543  245  \medskip An \emph{atomic} term is either a variable or constant. A  wenzelm@20543  246  \emph{term} is defined inductively over atomic terms, with  wenzelm@20543  247  abstraction and application as follows: @{text "t = b | x\<^isub>\ |  wenzelm@20543  248  ?x\<^isub>\ | c\<^isub>\ | \\<^isub>\. t | t\<^isub>1 t\<^isub>2"}.  wenzelm@20543  249  Parsing and printing takes care of converting between an external  wenzelm@20543  250  representation with named bound variables. Subsequently, we shall  wenzelm@20543  251  use the latter notation instead of internal de-Bruijn  wenzelm@20543  252  representation.  wenzelm@20498  253 wenzelm@20537  254  The inductive relation @{text "t :: \"} assigns a (unique) type to a  wenzelm@20537  255  term according to the structure of atomic terms, abstractions, and  wenzelm@20537  256  applicatins:  wenzelm@20498  257  $ wenzelm@20501  258  \infer{@{text "a\<^isub>\ :: \"}}{}  wenzelm@20498  259  \qquad  wenzelm@20501  260  \infer{@{text "(\x\<^sub>\. t) :: \ \ \"}}{@{text "t :: \"}}  wenzelm@20501  261  \qquad  wenzelm@20501  262  \infer{@{text "t u :: \"}}{@{text "t :: \ \ \"} & @{text "u :: \"}}  wenzelm@20498  263 $  wenzelm@20514  264  A \emph{well-typed term} is a term that can be typed according to these rules.  wenzelm@20498  265 wenzelm@20514  266  Typing information can be omitted: type-inference is able to  wenzelm@20514  267  reconstruct the most general type of a raw term, while assigning  wenzelm@20514  268  most general types to all of its variables and constants.  wenzelm@20514  269  Type-inference depends on a context of type constraints for fixed  wenzelm@20514  270  variables, and declarations for polymorphic constants.  wenzelm@20514  271 wenzelm@20537  272  The identity of atomic terms consists both of the name and the type  wenzelm@20537  273  component. This means that different variables @{text  wenzelm@20537  274  "x\<^bsub>\\<^isub>1\<^esub>"} and @{text  wenzelm@20537  275  "x\<^bsub>\\<^isub>2\<^esub>"} may become the same after type  wenzelm@20537  276  instantiation. Some outer layers of the system make it hard to  wenzelm@20537  277  produce variables of the same name, but different types. In  wenzelm@20543  278  contrast, mixed instances of polymorphic constants occur frequently.  wenzelm@20514  279 wenzelm@20514  280  \medskip The \emph{hidden polymorphism} of a term @{text "t :: \"}  wenzelm@20514  281  is the set of type variables occurring in @{text "t"}, but not in  wenzelm@20537  282  @{text "\"}. This means that the term implicitly depends on type  wenzelm@20543  283  arguments that are not accounted in the result type, i.e.\ there are  wenzelm@20537  284  different type instances @{text "t\ :: \"} and @{text  wenzelm@20537  285  "t\' :: \"} with the same type. This slightly  wenzelm@20543  286  pathological situation notoriously demands additional care.  wenzelm@20514  287 wenzelm@20514  288  \medskip A \emph{term abbreviation} is a syntactic definition @{text  wenzelm@20537  289  "c\<^isub>\ \ t"} of a closed term @{text "t"} of type @{text "\"},  wenzelm@20537  290  without any hidden polymorphism. A term abbreviation looks like a  wenzelm@20543  291  constant in the syntax, but is expanded before entering the logical  wenzelm@20543  292  core. Abbreviations are usually reverted when printing terms, using  wenzelm@20543  293  @{text "t \ c\<^isub>\"} as rules for higher-order rewriting.  wenzelm@20519  294 wenzelm@20519  295  \medskip Canonical operations on @{text "\"}-terms include @{text  wenzelm@20537  296  "\\\"}-conversion: @{text "\"}-conversion refers to capture-free  wenzelm@20519  297  renaming of bound variables; @{text "\"}-conversion contracts an  wenzelm@20537  298  abstraction applied to an argument term, substituting the argument  wenzelm@20519  299  in the body: @{text "(\x. b)a"} becomes @{text "b[a/x]"}; @{text  wenzelm@20519  300  "\"}-conversion contracts vacuous application-abstraction: @{text  wenzelm@20519  301  "\x. f x"} becomes @{text "f"}, provided that the bound variable  wenzelm@20537  302  does not occur in @{text "f"}.  wenzelm@20519  303 wenzelm@20537  304  Terms are normally treated modulo @{text "\"}-conversion, which is  wenzelm@20537  305  implicit in the de-Bruijn representation. Names for bound variables  wenzelm@20537  306  in abstractions are maintained separately as (meaningless) comments,  wenzelm@20537  307  mostly for parsing and printing. Full @{text "\\\"}-conversion is  wenzelm@28784  308  commonplace in various standard operations (\secref{sec:obj-rules})  wenzelm@28784  309  that are based on higher-order unification and matching.  wenzelm@18537  310 *}  wenzelm@18537  311 wenzelm@20514  312 text %mlref {*  wenzelm@20514  313  \begin{mldecls}  wenzelm@20514  314  @{index_ML_type term} \\  wenzelm@20519  315  @{index_ML "op aconv": "term * term -> bool"} \\  wenzelm@20547  316  @{index_ML map_types: "(typ -> typ) -> term -> term"} \\  wenzelm@20519  317  @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\  wenzelm@20514  318  @{index_ML map_aterms: "(term -> term) -> term -> term"} \\  wenzelm@20514  319  @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\  wenzelm@20547  320  \end{mldecls}  wenzelm@20547  321  \begin{mldecls}  wenzelm@20514  322  @{index_ML fastype_of: "term -> typ"} \\  wenzelm@20519  323  @{index_ML lambda: "term -> term -> term"} \\  wenzelm@20519  324  @{index_ML betapply: "term * term -> term"} \\  haftmann@29581  325  @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->  wenzelm@24972  326  theory -> term * theory"} \\  haftmann@29581  327  @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->  wenzelm@24972  328  theory -> (term * term) * theory"} \\  wenzelm@20519  329  @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\  wenzelm@20519  330  @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\  wenzelm@20514  331  \end{mldecls}  wenzelm@18537  332 wenzelm@20514  333  \begin{description}  wenzelm@18537  334 wenzelm@20537  335  \item @{ML_type term} represents de-Bruijn terms, with comments in  wenzelm@20537  336  abstractions, and explicitly named free variables and constants;  wenzelm@20537  337  this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML  wenzelm@20537  338  Var}, @{ML Const}, @{ML Abs}, @{ML "op \$"}.  wenzelm@20519  339 wenzelm@20519  340  \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text  wenzelm@20519  341  "\"}-equivalence of two terms. This is the basic equality relation  wenzelm@20519  342  on type @{ML_type term}; raw datatype equality should only be used  wenzelm@20519  343  for operations related to parsing or printing!  wenzelm@20519  344 wenzelm@20547  345  \item @{ML map_types}~@{text "f t"} applies the mapping @{text  wenzelm@20537  346  "f"} to all types occurring in @{text "t"}.  wenzelm@20537  347 wenzelm@20537  348  \item @{ML fold_types}~@{text "f t"} iterates the operation @{text  wenzelm@20537  349  "f"} over all occurrences of types in @{text "t"}; the term  wenzelm@20537  350  structure is traversed from left to right.  wenzelm@20519  351 wenzelm@20537  352  \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}  wenzelm@20537  353  to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML  wenzelm@20537  354  Const}) occurring in @{text "t"}.  wenzelm@20537  355 wenzelm@20537  356  \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text  wenzelm@20537  357  "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},  wenzelm@20537  358  @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is  wenzelm@20519  359  traversed from left to right.  wenzelm@20519  360 wenzelm@20537  361  \item @{ML fastype_of}~@{text "t"} determines the type of a  wenzelm@20537  362  well-typed term. This operation is relatively slow, despite the  wenzelm@20537  363  omission of any sanity checks.  wenzelm@20519  364 wenzelm@20519  365  \item @{ML lambda}~@{text "a b"} produces an abstraction @{text  wenzelm@20537  366  "\a. b"}, where occurrences of the atomic term @{text "a"} in the  wenzelm@20537  367  body @{text "b"} are replaced by bound variables.  wenzelm@20519  368 wenzelm@20537  369  \item @{ML betapply}~@{text "(t, u)"} produces an application @{text  wenzelm@20537  370  "t u"}, with topmost @{text "\"}-conversion if @{text "t"} is an  wenzelm@20537  371  abstraction.  wenzelm@20519  372 wenzelm@28110  373  \item @{ML Sign.declare_const}~@{text "properties ((c, \), mx)"}  wenzelm@24972  374  declares a new constant @{text "c :: \"} with optional mixfix  wenzelm@24972  375  syntax.  wenzelm@20519  376 wenzelm@24828  377  \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}  wenzelm@21827  378  introduces a new term abbreviation @{text "c \ t"}.  wenzelm@20519  379 wenzelm@20520  380  \item @{ML Sign.const_typargs}~@{text "thy (c, \)"} and @{ML  wenzelm@20520  381  Sign.const_instance}~@{text "thy (c, [\\<^isub>1, \, \\<^isub>n])"}  wenzelm@20543  382  convert between two representations of polymorphic constants: full  wenzelm@20543  383  type instance vs.\ compact type arguments form.  wenzelm@18537  384 wenzelm@20514  385  \end{description}  wenzelm@18537  386 *}  wenzelm@18537  387 wenzelm@18537  388 wenzelm@20451  389 section {* Theorems \label{sec:thms} *}  wenzelm@18537  390 wenzelm@18537  391 text {*  wenzelm@20543  392  A \emph{proposition} is a well-typed term of type @{text "prop"}, a  wenzelm@20521  393  \emph{theorem} is a proven proposition (depending on a context of  wenzelm@20521  394  hypotheses and the background theory). Primitive inferences include  wenzelm@20521  395  plain natural deduction rules for the primary connectives @{text  wenzelm@20537  396  "\"} and @{text "\"} of the framework. There is also a builtin  wenzelm@20537  397  notion of equality/equivalence @{text "\"}.  wenzelm@20521  398 *}  wenzelm@20521  399 wenzelm@29758  400 wenzelm@26872  401 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}  wenzelm@18537  402 wenzelm@20521  403 text {*  wenzelm@20543  404  The theory @{text "Pure"} contains constant declarations for the  wenzelm@20543  405  primitive connectives @{text "\"}, @{text "\"}, and @{text "\"} of  wenzelm@20543  406  the logical framework, see \figref{fig:pure-connectives}. The  wenzelm@20543  407  derivability judgment @{text "A\<^isub>1, \, A\<^isub>n \ B"} is  wenzelm@20543  408  defined inductively by the primitive inferences given in  wenzelm@20543  409  \figref{fig:prim-rules}, with the global restriction that the  wenzelm@20543  410  hypotheses must \emph{not} contain any schematic variables. The  wenzelm@20543  411  builtin equality is conceptually axiomatized as shown in  wenzelm@20521  412  \figref{fig:pure-equality}, although the implementation works  wenzelm@20543  413  directly with derived inferences.  wenzelm@20521  414 wenzelm@20521  415  \begin{figure}[htb]  wenzelm@20521  416  \begin{center}  wenzelm@20501  417  \begin{tabular}{ll}  wenzelm@20501  418  @{text "all :: (\ \ prop) \ prop"} & universal quantification (binder @{text "\"}) \\  wenzelm@20501  419  @{text "\ :: prop \ prop \ prop"} & implication (right associative infix) \\  wenzelm@20521  420  @{text "\ :: \ \ \ \ prop"} & equality relation (infix) \\  wenzelm@20501  421  \end{tabular}  wenzelm@20537  422  \caption{Primitive connectives of Pure}\label{fig:pure-connectives}  wenzelm@20521  423  \end{center}  wenzelm@20521  424  \end{figure}  wenzelm@18537  425 wenzelm@20501  426  \begin{figure}[htb]  wenzelm@20501  427  \begin{center}  wenzelm@20498  428  $ wenzelm@20498  429  \infer[@{text "(axiom)"}]{@{text "\ A"}}{@{text "A \ \"}}  wenzelm@20498  430  \qquad  wenzelm@20498  431  \infer[@{text "(assume)"}]{@{text "A \ A"}}{}  wenzelm@20498  432 $  wenzelm@20498  433  $ wenzelm@20537  434  \infer[@{text "(\_intro)"}]{@{text "\ \ \x. b[x]"}}{@{text "\ \ b[x]"} & @{text "x \ \"}}  wenzelm@20498  435  \qquad  wenzelm@20537  436  \infer[@{text "(\_elim)"}]{@{text "\ \ b[a]"}}{@{text "\ \ \x. b[x]"}}  wenzelm@20498  437 $  wenzelm@20498  438  $ wenzelm@20498  439  \infer[@{text "(\_intro)"}]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}}  wenzelm@20498  440  \qquad  wenzelm@20498  441  \infer[@{text "(\_elim)"}]{@{text "\\<^sub>1 \ \\<^sub>2 \ B"}}{@{text "\\<^sub>1 \ A \ B"} & @{text "\\<^sub>2 \ A"}}  wenzelm@20498  442 $  wenzelm@20521  443  \caption{Primitive inferences of Pure}\label{fig:prim-rules}  wenzelm@20521  444  \end{center}  wenzelm@20521  445  \end{figure}  wenzelm@20521  446 wenzelm@20521  447  \begin{figure}[htb]  wenzelm@20521  448  \begin{center}  wenzelm@20521  449  \begin{tabular}{ll}  wenzelm@20537  450  @{text "\ (\x. b[x]) a \ b[a]"} & @{text "\"}-conversion \\  wenzelm@20521  451  @{text "\ x \ x"} & reflexivity \\  wenzelm@20521  452  @{text "\ x \ y \ P x \ P y"} & substitution \\  wenzelm@20521  453  @{text "\ (\x. f x \ g x) \ f \ g"} & extensionality \\  wenzelm@20537  454  @{text "\ (A \ B) \ (B \ A) \ A \ B"} & logical equivalence \\  wenzelm@20521  455  \end{tabular}  wenzelm@20542  456  \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}  wenzelm@20501  457  \end{center}  wenzelm@20501  458  \end{figure}  wenzelm@18537  459 wenzelm@20501  460  The introduction and elimination rules for @{text "\"} and @{text  wenzelm@20537  461  "\"} are analogous to formation of dependently typed @{text  wenzelm@20501  462  "\"}-terms representing the underlying proof objects. Proof terms  wenzelm@20543  463  are irrelevant in the Pure logic, though; they cannot occur within  wenzelm@20543  464  propositions. The system provides a runtime option to record  wenzelm@20537  465  explicit proof terms for primitive inferences. Thus all three  wenzelm@20537  466  levels of @{text "\"}-calculus become explicit: @{text "\"} for  wenzelm@20537  467  terms, and @{text "\/\"} for proofs (cf.\  wenzelm@20537  468  \cite{Berghofer-Nipkow:2000:TPHOL}).  wenzelm@20491  469 wenzelm@20537  470  Observe that locally fixed parameters (as in @{text "\_intro"}) need  wenzelm@20537  471  not be recorded in the hypotheses, because the simple syntactic  wenzelm@20543  472  types of Pure are always inhabitable. Assumptions'' @{text "x ::  wenzelm@20543  473  \"} for type-membership are only present as long as some @{text  wenzelm@20543  474  "x\<^isub>\"} occurs in the statement body.\footnote{This is the key  wenzelm@20543  475  difference to @{text "\HOL"}'' in the PTS framework  wenzelm@20543  476  \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are  wenzelm@20543  477  treated uniformly for propositions and types.}  wenzelm@20501  478 wenzelm@20501  479  \medskip The axiomatization of a theory is implicitly closed by  wenzelm@20537  480  forming all instances of type and term variables: @{text "\  wenzelm@20537  481  A\"} holds for any substitution instance of an axiom  wenzelm@20543  482  @{text "\ A"}. By pushing substitutions through derivations  wenzelm@20543  483  inductively, we also get admissible @{text "generalize"} and @{text  wenzelm@20543  484  "instance"} rules as shown in \figref{fig:subst-rules}.  wenzelm@20501  485 wenzelm@20501  486  \begin{figure}[htb]  wenzelm@20501  487  \begin{center}  wenzelm@20498  488  $ wenzelm@20501  489  \infer{@{text "\ \ B[?$"}}{@{text "\ \ B[\]"} & @{text "\ \ \"}}  wenzelm@20501  490  \quad  wenzelm@20501  491  \infer[\quad@{text "(generalize)"}]{@{text "\ \ B[?x]"}}{@{text "\ \ B[x]"} & @{text "x \ \"}}  wenzelm@20498  492  \]  wenzelm@20498  493  $ wenzelm@20501  494  \infer{@{text "\ \ B[$"}}{@{text "\ \ B[?\]"}}  wenzelm@20501  495  \quad  wenzelm@20501  496  \infer[\quad@{text "(instantiate)"}]{@{text "\ \ B[t]"}}{@{text "\ \ B[?x]"}}  wenzelm@20498  497  \]  wenzelm@20501  498  \caption{Admissible substitution rules}\label{fig:subst-rules}  wenzelm@20501  499  \end{center}  wenzelm@20501  500  \end{figure}  wenzelm@18537  501 wenzelm@20537  502  Note that @{text "instantiate"} does not require an explicit  wenzelm@20537  503  side-condition, because @{text "\"} may never contain schematic  wenzelm@20537  504  variables.  wenzelm@20537  505 wenzelm@20537  506  In principle, variables could be substituted in hypotheses as well,  wenzelm@20543  507  but this would disrupt the monotonicity of reasoning: deriving  wenzelm@20543  508  @{text "\\ \ B\"} from @{text "\ \ B"} is  wenzelm@20543  509  correct, but @{text "\\ \ \"} does not necessarily hold:  wenzelm@20543  510  the result belongs to a different proof context.  wenzelm@20542  511 wenzelm@20543  512  \medskip An \emph{oracle} is a function that produces axioms on the  wenzelm@20543  513  fly. Logically, this is an instance of the @{text "axiom"} rule  wenzelm@20543  514  (\figref{fig:prim-rules}), but there is an operational difference.  wenzelm@20543  515  The system always records oracle invocations within derivations of  wenzelm@29768  516  theorems by a unique tag.  wenzelm@20542  517 wenzelm@20542  518  Axiomatizations should be limited to the bare minimum, typically as  wenzelm@20542  519  part of the initial logical basis of an object-logic formalization.  wenzelm@20543  520  Later on, theories are usually developed in a strictly definitional  wenzelm@20543  521  fashion, by stating only certain equalities over new constants.  wenzelm@20542  522 wenzelm@20542  523  A \emph{simple definition} consists of a constant declaration @{text  wenzelm@20543  524  "c :: \"} together with an axiom @{text "\ c \ t"}, where @{text "t  wenzelm@20543  525  :: \"} is a closed term without any hidden polymorphism. The RHS  wenzelm@20543  526  may depend on further defined constants, but not @{text "c"} itself.  wenzelm@20543  527  Definitions of functions may be presented as @{text "c \<^vec>x \  wenzelm@20543  528  t"} instead of the puristic @{text "c \ \\<^vec>x. t"}.  wenzelm@20542  529 wenzelm@20543  530  An \emph{overloaded definition} consists of a collection of axioms  wenzelm@20543  531  for the same constant, with zero or one equations @{text  wenzelm@20543  532  "c((\<^vec>\)\) \ t"} for each type constructor @{text "\"} (for  wenzelm@20543  533  distinct variables @{text "\<^vec>\"}). The RHS may mention  wenzelm@20543  534  previously defined constants as above, or arbitrary constants @{text  wenzelm@20543  535  "d(\\<^isub>i)"} for some @{text "\\<^isub>i"} projected from @{text  wenzelm@20543  536  "\<^vec>\"}. Thus overloaded definitions essentially work by  wenzelm@20543  537  primitive recursion over the syntactic structure of a single type  wenzelm@20543  538  argument.  wenzelm@20521  539 *}  wenzelm@20498  540 wenzelm@20521  541 text %mlref {*  wenzelm@20521  542  \begin{mldecls}  wenzelm@20521  543  @{index_ML_type ctyp} \\  wenzelm@20521  544  @{index_ML_type cterm} \\  wenzelm@20547  545  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\  wenzelm@20547  546  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\  wenzelm@20547  547  \end{mldecls}  wenzelm@20547  548  \begin{mldecls}  wenzelm@20521  549  @{index_ML_type thm} \\  wenzelm@20542  550  @{index_ML proofs: "int ref"} \\  wenzelm@20542  551  @{index_ML Thm.assume: "cterm -> thm"} \\  wenzelm@20542  552  @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\  wenzelm@20542  553  @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\  wenzelm@20542  554  @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\  wenzelm@20542  555  @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\  wenzelm@20542  556  @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\  wenzelm@20542  557  @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\  wenzelm@28674  558  @{index_ML Thm.axiom: "theory -> string -> thm"} \\  wenzelm@28290  559  @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory  wenzelm@28290  560  -> (string * ('a -> thm)) * theory"} \\  wenzelm@20547  561  \end{mldecls}  wenzelm@20547  562  \begin{mldecls}  haftmann@29615  563  @{index_ML Theory.add_axioms_i: "(binding * term) list -> theory -> theory"} \\  wenzelm@20542  564  @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\  haftmann@29615  565  @{index_ML Theory.add_defs_i: "bool -> bool -> (binding * term) list -> theory -> theory"} \\  wenzelm@20521  566  \end{mldecls}  wenzelm@20521  567 wenzelm@20521  568  \begin{description}  wenzelm@20521  569 wenzelm@20542  570  \item @{ML_type ctyp} and @{ML_type cterm} represent certified types  wenzelm@20542  571  and terms, respectively. These are abstract datatypes that  wenzelm@20542  572  guarantee that its values have passed the full well-formedness (and  wenzelm@20542  573  well-typedness) checks, relative to the declarations of type  wenzelm@20542  574  constructors, constants etc. in the theory.  wenzelm@20542  575 wenzelm@29768  576  \item @{ML Thm.ctyp_of}~@{text "thy \"} and @{ML  wenzelm@29768  577  Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,  wenzelm@29768  578  respectively. This also involves some basic normalizations, such  wenzelm@29768  579  expansion of type and term abbreviations from the theory context.  wenzelm@20547  580 wenzelm@20547  581  Re-certification is relatively slow and should be avoided in tight  wenzelm@20547  582  reasoning loops. There are separate operations to decompose  wenzelm@20547  583  certified entities (including actual theorems).  wenzelm@20542  584 wenzelm@20542  585  \item @{ML_type thm} represents proven propositions. This is an  wenzelm@20542  586  abstract datatype that guarantees that its values have been  wenzelm@20542  587  constructed by basic principles of the @{ML_struct Thm} module.  wenzelm@20543  588  Every @{ML thm} value contains a sliding back-reference to the  wenzelm@20543  589  enclosing theory, cf.\ \secref{sec:context-theory}.  wenzelm@20542  590 wenzelm@20543  591  \item @{ML proofs} determines the detail of proof recording within  wenzelm@29768  592  @{ML_type thm} values: @{ML 0} records only the names of oracles,  wenzelm@29768  593  @{ML 1} records oracle names and propositions, @{ML 2} additionally  wenzelm@29768  594  records full proof terms. Officially named theorems that contribute  wenzelm@29768  595  to a result are always recorded.  wenzelm@20542  596 wenzelm@20542  597  \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML  wenzelm@20542  598  Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}  wenzelm@20542  599  correspond to the primitive inferences of \figref{fig:prim-rules}.  wenzelm@20542  600 wenzelm@20542  601  \item @{ML Thm.generalize}~@{text "(\<^vec>\, \<^vec>x)"}  wenzelm@20542  602  corresponds to the @{text "generalize"} rules of  wenzelm@20543  603  \figref{fig:subst-rules}. Here collections of type and term  wenzelm@20543  604  variables are generalized simultaneously, specified by the given  wenzelm@20543  605  basic names.  wenzelm@20521  606 wenzelm@20542  607  \item @{ML Thm.instantiate}~@{text "(\<^vec>\\<^isub>s,  wenzelm@20542  608  \<^vec>x\<^isub>\)"} corresponds to the @{text "instantiate"} rules  wenzelm@20542  609  of \figref{fig:subst-rules}. Type variables are substituted before  wenzelm@20542  610  term variables. Note that the types in @{text "\<^vec>x\<^isub>\"}  wenzelm@20542  611  refer to the instantiated versions.  wenzelm@20542  612 wenzelm@28674  613  \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named  wenzelm@20542  614  axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.  wenzelm@20542  615 wenzelm@28290  616  \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named  wenzelm@28290  617  oracle rule, essentially generating arbitrary axioms on the fly,  wenzelm@28290  618  cf.\ @{text "axiom"} in \figref{fig:prim-rules}.  wenzelm@20521  619 wenzelm@20543  620  \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \]"} declares  wenzelm@20543  621  arbitrary propositions as axioms.  wenzelm@20542  622 wenzelm@20542  623  \item @{ML Theory.add_deps}~@{text "name c\<^isub>\  wenzelm@20543  624  \<^vec>d\<^isub>\"} declares dependencies of a named specification  wenzelm@20543  625  for constant @{text "c\<^isub>\"}, relative to existing  wenzelm@20543  626  specifications for constants @{text "\<^vec>d\<^isub>\"}.  wenzelm@20542  627 wenzelm@20542  628  \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c  wenzelm@20543  629  \<^vec>x \ t), \]"} states a definitional axiom for an existing  wenzelm@20543  630  constant @{text "c"}. Dependencies are recorded (cf.\ @{ML  wenzelm@20543  631  Theory.add_deps}), unless the @{text "unchecked"} option is set.  wenzelm@20521  632 wenzelm@20521  633  \end{description}  wenzelm@20521  634 *}  wenzelm@20521  635 wenzelm@20521  636 wenzelm@20543  637 subsection {* Auxiliary definitions *}  wenzelm@20521  638 wenzelm@20521  639 text {*  wenzelm@20543  640  Theory @{text "Pure"} provides a few auxiliary definitions, see  wenzelm@20543  641  \figref{fig:pure-aux}. These special constants are normally not  wenzelm@20543  642  exposed to the user, but appear in internal encodings.  wenzelm@20501  643 wenzelm@20501  644  \begin{figure}[htb]  wenzelm@20501  645  \begin{center}  wenzelm@20498  646  \begin{tabular}{ll}  wenzelm@20521  647  @{text "conjunction :: prop \ prop \ prop"} & (infix @{text "&"}) \\  wenzelm@20521  648  @{text "\ A & B \ (\C. (A \ B \ C) \ C)"} \$1ex]  wenzelm@20543  649  @{text "prop :: prop \ prop"} & (prefix @{text "#"}, suppressed) \\  wenzelm@20521  650  @{text "#A \ A"} \\[1ex]  wenzelm@20521  651  @{text "term :: \ \ prop"} & (prefix @{text "TERM"}) \\  wenzelm@20521  652  @{text "term x \ (\A. A \ A)"} \\[1ex]  wenzelm@20521  653  @{text "TYPE :: \ itself"} & (prefix @{text "TYPE"}) \\  wenzelm@20521  654  @{text "(unspecified)"} \\  wenzelm@20498  655  \end{tabular}  wenzelm@20521  656  \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}  wenzelm@20501  657  \end{center}  wenzelm@20501  658  \end{figure}  wenzelm@20501  659 wenzelm@20537  660  Derived conjunction rules include introduction @{text "A \ B \ A &  wenzelm@20537  661  B"}, and destructions @{text "A & B \ A"} and @{text "A & B \ B"}.  wenzelm@20537  662  Conjunction allows to treat simultaneous assumptions and conclusions  wenzelm@20537  663  uniformly. For example, multiple claims are intermediately  wenzelm@20543  664  represented as explicit conjunction, but this is refined into  wenzelm@20543  665  separate sub-goals before the user continues the proof; the final  wenzelm@20543  666  result is projected into a list of theorems (cf.\  wenzelm@20537  667  \secref{sec:tactical-goals}).  wenzelm@20498  668 wenzelm@20537  669  The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex  wenzelm@20537  670  propositions appear as atomic, without changing the meaning: @{text  wenzelm@20537  671  "\ \ A"} and @{text "\ \ #A"} are interchangeable. See  wenzelm@20537  672  \secref{sec:tactical-goals} for specific operations.  wenzelm@20521  673 wenzelm@20543  674  The @{text "term"} marker turns any well-typed term into a derivable  wenzelm@20543  675  proposition: @{text "\ TERM t"} holds unconditionally. Although  wenzelm@20543  676  this is logically vacuous, it allows to treat terms and proofs  wenzelm@20543  677  uniformly, similar to a type-theoretic framework.  wenzelm@20498  678 wenzelm@20537  679  The @{text "TYPE"} constructor is the canonical representative of  wenzelm@20537  680  the unspecified type @{text "\ itself"}; it essentially injects the  wenzelm@20537  681  language of types into that of terms. There is specific notation  wenzelm@20537  682  @{text "TYPE(\)"} for @{text "TYPE\<^bsub>\  wenzelm@20521  683  itself\<^esub>"}.  wenzelm@20537  684  Although being devoid of any particular meaning, the @{text  wenzelm@20537  685  "TYPE(\)"} accounts for the type @{text "\"} within the term  wenzelm@20537  686  language. In particular, @{text "TYPE(\)"} may be used as formal  wenzelm@20537  687  argument in primitive definitions, in order to circumvent hidden  wenzelm@20537  688  polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c  wenzelm@20537  689  TYPE(\) \ A[$"} defines @{text "c :: \ itself \ prop"} in terms of  wenzelm@20537  690  a proposition @{text "A"} that depends on an additional type  wenzelm@20537  691  argument, which is essentially a predicate on types.  wenzelm@20521  692 *}  wenzelm@20501  693 wenzelm@20521  694 text %mlref {*  wenzelm@20521  695  \begin{mldecls}  wenzelm@20521  696  @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\  wenzelm@20521  697  @{index_ML Conjunction.elim: "thm -> thm * thm"} \\  wenzelm@20521  698  @{index_ML Drule.mk_term: "cterm -> thm"} \\  wenzelm@20521  699  @{index_ML Drule.dest_term: "thm -> cterm"} \\  wenzelm@20521  700  @{index_ML Logic.mk_type: "typ -> term"} \\  wenzelm@20521  701  @{index_ML Logic.dest_type: "term -> typ"} \\  wenzelm@20521  702  \end{mldecls}  wenzelm@20521  703 wenzelm@20521  704  \begin{description}  wenzelm@20521  705 wenzelm@20542  706  \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text  wenzelm@20542  707  "A"} and @{text "B"}.  wenzelm@20542  708 wenzelm@20543  709  \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}  wenzelm@20542  710  from @{text "A & B"}.  wenzelm@20542  711 wenzelm@20543  712  \item @{ML Drule.mk_term} derives @{text "TERM t"}.  wenzelm@20542  713 wenzelm@20543  714  \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text  wenzelm@20543  715  "TERM t"}.  wenzelm@20542  716 wenzelm@20542  717  \item @{ML Logic.mk_type}~@{text "\"} produces the term @{text  wenzelm@20542  718  "TYPE(\)"}.  wenzelm@20542  719 wenzelm@20542  720  \item @{ML Logic.dest_type}~@{text "TYPE(\)"} recovers the type  wenzelm@20542  721  @{text "\"}.  wenzelm@20521  722 wenzelm@20521  723  \end{description}  wenzelm@20491  724 *}  wenzelm@18537  725 wenzelm@20480  726 wenzelm@28784  727 section {* Object-level rules \label{sec:obj-rules} *}  wenzelm@18537  728 wenzelm@29768  729 text {*  wenzelm@29768  730  The primitive inferences covered so far mostly serve foundational  wenzelm@29768  731  purposes. User-level reasoning usually works via object-level rules  wenzelm@29768  732  that are represented as theorems of Pure. Composition of rules  wenzelm@29768  733  works via \emph{higher-order backchaining}, which involves  wenzelm@29768  734  unification module @{text "\\\"}-conversion of @{text "\"}-terms,  wenzelm@29768  735  and so-called \emph{lifting} of rules into a context of @{text "\"}  wenzelm@29768  736  and @{text "\"} connectives. Thus the full power of higher-order  wenzelm@29768  737  natural deduction in Isabelle/Pure becomes readily available.  wenzelm@29769  738 *}  wenzelm@20491  739 wenzelm@29769  740 wenzelm@29769  741 subsection {* Hereditary Harrop Formulae *}  wenzelm@29769  742 wenzelm@29769  743 text {*  wenzelm@29768  744  The idea of object-level rules is to model Natural Deduction  wenzelm@29768  745  inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow  wenzelm@29768  746  arbitrary nesting similar to \cite{extensions91}. The most basic  wenzelm@29768  747  rule format is that of a \emph{Horn Clause}:  wenzelm@29768  748  $ wenzelm@29768  749  \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\"} & @{text "A\<^sub>n"}}  wenzelm@29768  750 $  wenzelm@29768  751  where @{text "A, A\<^sub>1, \, A\<^sub>n"} are atomic propositions  wenzelm@29768  752  of the framework, usually of the form @{text "Trueprop B"}, where  wenzelm@29768  753  @{text "B"} is a (compound) object-level statement. This  wenzelm@29768  754  object-level inference corresponds to an iterated implication in  wenzelm@29768  755  Pure like this:  wenzelm@29768  756  $ wenzelm@29768  757  @{text "A\<^sub>1 \ \ A\<^sub>n \ A"}  wenzelm@29768  758 $  wenzelm@29769  759  As an example consider conjunction introduction: @{text "A \ B \ A \  wenzelm@29769  760  B"}. Any parameters occurring in such rule statements are  wenzelm@29769  761  conceptionally treated as arbitrary:  wenzelm@29768  762  $ wenzelm@29769  763  @{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  764 $  wenzelm@20491  765 wenzelm@29769  766  Nesting of rules means that the positions of @{text "A\<^sub>i"} may  wenzelm@29769  767  hold compound rules of the same shape, not just atomic propositions.  wenzelm@29769  768  Propositions of this format are called \emph{Hereditary Harrop  wenzelm@29769  769  Formulae} in the literature \cite{Miller:1991}. Here we give an  wenzelm@29769  770  inductive characterization as follows:  wenzelm@29768  771 wenzelm@29768  772  \medskip  wenzelm@29768  773  \begin{tabular}{ll}  wenzelm@29768  774  @{text "\<^bold>x"} & set of variables \\  wenzelm@29768  775  @{text "\<^bold>A"} & set of atomic propositions \\  wenzelm@29768  776  @{text "\<^bold>H = \\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \ \<^bold>A"} & set of Hereditary Harrop Formulas \\  wenzelm@29768  777  \end{tabular}  wenzelm@29768  778  \medskip  wenzelm@29768  779 wenzelm@29769  780  \noindent Thus we essentially impose nesting levels on Pure  wenzelm@29769  781  propositions. At each level there is a local parameter prefix,  wenzelm@29769  782  followed by premises, and concluding another atomic proposition.  wenzelm@29769  783  Typical examples are implication introduction @{text "(A \ B) \ A \  wenzelm@29769  784  B"} or mathematical induction @{text "P 0 \ (\n. P n \ P (Suc n)) \  wenzelm@29769  785  P n"}. Even deeper nesting occurs in well-founded induction @{text  wenzelm@29769  786  "(\x. (\y. y \ x \ P y) \ P x) \ P x"}, but this already marks the  wenzelm@29769  787  limit of rule complexity seen in practice.  wenzelm@29769  788 wenzelm@29769  789  \medskip The main inference system of Isabelle/Pure always maintains  wenzelm@29769  790  the following canonical form of framework propositions:  wenzelm@29769  791 wenzelm@29769  792  \begin{itemize}  wenzelm@29768  793 wenzelm@29769  794  \item Results are normalized by means of the equivalence @{prop  wenzelm@29769  795  "(PROP A \ (\x. PROP B x)) \ (\x. PROP A \ PROP B x)"}, which is a  wenzelm@29769  796  theorem of Pure. By pushing quantifiers inside conclusions in front  wenzelm@29769  797  of the implication, we arrive at a normal form that is always a  wenzelm@29769  798  Hereditary Harrop Formula.  wenzelm@29769  799 wenzelm@29769  800  \item The outermost prefix of parameters is represented via  wenzelm@29769  801  schematic variables, i.e.\ instead of @{text "\\<^vec>x. \<^vec>H  wenzelm@29769  802  \<^vec>x \ A \<^vec>x"} we always work with @{text "\<^vec>H  wenzelm@29769  803  ?\<^vec>x \ A ?\<^vec>x"}. Note that this representation looses  wenzelm@29769  804  information about the order of parameters, and vacuous quantifiers  wenzelm@29769  805  vanish automatically.  wenzelm@29769  806 wenzelm@29769  807  \end{itemize}  wenzelm@29769  808 *}  wenzelm@29769  809 wenzelm@29769  810 wenzelm@29769  811 subsection {* Rule composition *}  wenzelm@29769  812 wenzelm@29769  813 text {*  wenzelm@29768  814  There are two main principles of rule composition: @{inference  wenzelm@29768  815  resolution} (i.e.\ backchaining of rules) and @{inference  wenzelm@29768  816  assumption} (i.e.\ closing a branch); both principles are combined  wenzelm@29768  817  in the variants of @{inference elim_resolution} and @{inference  wenzelm@29768  818  dest_resolution}. Raw @{inference composition} is occasionally  wenzelm@20491  819  useful as well, also it is strictly speaking outside of the proper  wenzelm@20491  820  rule calculus.  wenzelm@20491  821 wenzelm@20491  822 wenzelm@20491  823  This means that any operations within the rule calculus may be  wenzelm@20491  824  subject to spontaneous @{text "\\\"}-HHF conversions. It is common  wenzelm@20491  825  practice not to contract or expand unnecessarily. Some mechanisms  wenzelm@20491  826  prefer an one form, others the opposite, so there is a potential  wenzelm@20491  827  danger to produce some oscillation!  wenzelm@20491  828 wenzelm@20498  829  $ wenzelm@29768  830  \infer[(@{inference assumption})]{@{text "C\"}}  wenzelm@20498  831  {@{text "(\\<^vec>x. \<^vec>H \<^vec>x \ A \<^vec>x) \ C"} & @{text "A\ = H\<^sub>i\"}~~\text{(for some~@{text i})}}  wenzelm@20498  832 $  wenzelm@20498  833 wenzelm@20498  834 wenzelm@20498  835  $ wenzelm@29768  836  \infer[(@{inference composition})]{@{text "\<^vec>A\ \ C\"}}  wenzelm@20498  837  {@{text "\<^vec>A \ B"} & @{text "B' \ C"} & @{text "B\ = B'\"}}  wenzelm@20498  838 $  wenzelm@20498  839 wenzelm@20498  840 wenzelm@20498  841  $ wenzelm@20498  842  \infer[@{text "(\_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  843 $  wenzelm@20498  844  $ wenzelm@20498  845  \infer[@{text "(\_lift)"}]{@{text "(\<^vec>H \ \<^vec>A) \ (\<^vec>H \ B)"}}{@{text "\<^vec>A \ B"}}  wenzelm@20498  846 $  wenzelm@20498  847 wenzelm@20498  848  The @{text resolve} scheme is now acquired from @{text "\_lift"},  wenzelm@20498  849  @{text "\_lift"}, and @{text compose}.  wenzelm@20498  850 wenzelm@20498  851  $ wenzelm@29768  852  \infer[(@{inference resolution})]  wenzelm@20498  853  {@{text "(\\<^vec>x. \<^vec>H \<^vec>x \ \<^vec>A (?\<^vec>a \<^vec>x))\ \ C\"}}  wenzelm@20498  854  {\begin{tabular}{l}  wenzelm@20498  855  @{text "\<^vec>A ?\<^vec>a \ B ?\<^vec>a"} \\  wenzelm@20498  856  @{text "(\\<^vec>x. \<^vec>H \<^vec>x \ B' \<^vec>x) \ C"} \\  wenzelm@20498  857  @{text "(\\<^vec>x. B (?\<^vec>a \<^vec>x))\ = B'\"} \\  wenzelm@20498  858  \end{tabular}}  wenzelm@20498  859 $  wenzelm@20498  860 wenzelm@20498  861 wenzelm@29768  862  FIXME @{inference elim_resolution}, @{inference dest_resolution}  wenzelm@18537  863 *}  wenzelm@18537  864 wenzelm@29768  865 wenzelm@29768  866 text %mlref {*  wenzelm@29768  867  \begin{mldecls}  wenzelm@29768  868  @{index_ML "op RS": "thm * thm -> thm"} \\  wenzelm@29768  869  @{index_ML "op OF": "thm * thm list -> thm"} \\  wenzelm@29768  870  @{index_ML MetaSimplifier.norm_hhf: "thm -> thm"} \\  wenzelm@29768  871  \end{mldecls}  wenzelm@29768  872 wenzelm@29768  873  \begin{description}  wenzelm@29768  874 wenzelm@29768  875  \item @{text "thm\<^sub>1 RS thm\<^sub>2"} FIXME  wenzelm@29768  876 wenzelm@29768  877  \item @{text "thm OF thms"} FIXME  wenzelm@29768  878 wenzelm@29768  879  \item @{ML MetaSimplifier.norm_hhf}~@{text thm} FIXME  wenzelm@29768  880 wenzelm@29768  881  \end{description}  wenzelm@29768  882 *}  wenzelm@29768  883 wenzelm@29768  884 wenzelm@18537  885 end