doc-src/IsarImplementation/Thy/Logic.thy
 author wenzelm Mon Feb 16 20:47:44 2009 +0100 (2009-02-16) changeset 29755 d66b34e46bdf parent 29615 doc-src/IsarImplementation/Thy/logic.thy@24a58ae5dc0e child 29758 7a3b5bbed313 permissions -rw-r--r--
observe usual theory naming conventions;
 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@20480  189 wenzelm@20451  190 section {* Terms \label{sec:terms} *}  wenzelm@18537  191 wenzelm@18537  192 text {*  wenzelm@20451  193  \glossary{Term}{FIXME}  wenzelm@18537  194 wenzelm@20491  195  The language of terms is that of simply-typed @{text "\"}-calculus  wenzelm@20520  196  with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}  wenzelm@20537  197  or \cite{paulson-ml2}), with the types being determined determined  wenzelm@20537  198  by the corresponding binders. In contrast, free variables and  wenzelm@20537  199  constants are have an explicit name and type in each occurrence.  wenzelm@20514  200 wenzelm@20514  201  \medskip A \emph{bound variable} is a natural number @{text "b"},  wenzelm@20537  202  which accounts for the number of intermediate binders between the  wenzelm@20537  203  variable occurrence in the body and its binding position. For  wenzelm@20543  204  example, the de-Bruijn term @{text  wenzelm@20543  205  "\\<^bsub>nat\<^esub>. \\<^bsub>nat\<^esub>. 1 + 0"} would  wenzelm@20543  206  correspond to @{text  wenzelm@20543  207  "\x\<^bsub>nat\<^esub>. \y\<^bsub>nat\<^esub>. x + y"} in a named  wenzelm@20543  208  representation. Note that a bound variable may be represented by  wenzelm@20543  209  different de-Bruijn indices at different occurrences, depending on  wenzelm@20543  210  the nesting of abstractions.  wenzelm@20537  211 wenzelm@20543  212  A \emph{loose variable} is a bound variable that is outside the  wenzelm@20537  213  scope of local binders. The types (and names) for loose variables  wenzelm@20543  214  can be managed as a separate context, that is maintained as a stack  wenzelm@20543  215  of hypothetical binders. The core logic operates on closed terms,  wenzelm@20543  216  without any loose variables.  wenzelm@20514  217 wenzelm@20537  218  A \emph{fixed variable} is a pair of a basic name and a type, e.g.\  wenzelm@20537  219  @{text "(x, \)"} which is usually printed @{text "x\<^isub>\"}. A  wenzelm@20537  220  \emph{schematic variable} is a pair of an indexname and a type,  wenzelm@20537  221  e.g.\ @{text "((x, 0), \)"} which is usually printed as @{text  wenzelm@20537  222  "?x\<^isub>\"}.  wenzelm@20491  223 wenzelm@20537  224  \medskip A \emph{constant} is a pair of a basic name and a type,  wenzelm@20537  225  e.g.\ @{text "(c, \)"} which is usually printed as @{text  wenzelm@20537  226  "c\<^isub>\"}. Constants are declared in the context as polymorphic  wenzelm@20543  227  families @{text "c :: \"}, meaning that all substitution instances  wenzelm@20543  228  @{text "c\<^isub>\"} for @{text "\ = \\"} are valid.  wenzelm@20514  229 wenzelm@20537  230  The vector of \emph{type arguments} of constant @{text "c\<^isub>\"}  wenzelm@20537  231  wrt.\ the declaration @{text "c :: \"} is defined as the codomain of  wenzelm@20537  232  the matcher @{text "\ = {?\\<^isub>1 \ \\<^isub>1, \,  wenzelm@20537  233  ?\\<^isub>n \ \\<^isub>n}"} presented in canonical order @{text  wenzelm@20537  234  "(\\<^isub>1, \, \\<^isub>n)"}. Within a given theory context,  wenzelm@20537  235  there is a one-to-one correspondence between any constant @{text  wenzelm@20537  236  "c\<^isub>\"} and the application @{text "c(\\<^isub>1, \,  wenzelm@20537  237  \\<^isub>n)"} of its type arguments. For example, with @{text "plus  wenzelm@20537  238  :: \ \ \ \ \"}, the instance @{text "plus\<^bsub>nat \ nat \  wenzelm@20537  239  nat\<^esub>"} corresponds to @{text "plus(nat)"}.  wenzelm@20480  240 wenzelm@20514  241  Constant declarations @{text "c :: \"} may contain sort constraints  wenzelm@20514  242  for type variables in @{text "\"}. These are observed by  wenzelm@20514  243  type-inference as expected, but \emph{ignored} by the core logic.  wenzelm@20514  244  This means the primitive logic is able to reason with instances of  wenzelm@20537  245  polymorphic constants that the user-level type-checker would reject  wenzelm@20537  246  due to violation of type class restrictions.  wenzelm@20480  247 wenzelm@20543  248  \medskip An \emph{atomic} term is either a variable or constant. A  wenzelm@20543  249  \emph{term} is defined inductively over atomic terms, with  wenzelm@20543  250  abstraction and application as follows: @{text "t = b | x\<^isub>\ |  wenzelm@20543  251  ?x\<^isub>\ | c\<^isub>\ | \\<^isub>\. t | t\<^isub>1 t\<^isub>2"}.  wenzelm@20543  252  Parsing and printing takes care of converting between an external  wenzelm@20543  253  representation with named bound variables. Subsequently, we shall  wenzelm@20543  254  use the latter notation instead of internal de-Bruijn  wenzelm@20543  255  representation.  wenzelm@20498  256 wenzelm@20537  257  The inductive relation @{text "t :: \"} assigns a (unique) type to a  wenzelm@20537  258  term according to the structure of atomic terms, abstractions, and  wenzelm@20537  259  applicatins:  wenzelm@20498  260  $ wenzelm@20501  261  \infer{@{text "a\<^isub>\ :: \"}}{}  wenzelm@20498  262  \qquad  wenzelm@20501  263  \infer{@{text "(\x\<^sub>\. t) :: \ \ \"}}{@{text "t :: \"}}  wenzelm@20501  264  \qquad  wenzelm@20501  265  \infer{@{text "t u :: \"}}{@{text "t :: \ \ \"} & @{text "u :: \"}}  wenzelm@20498  266 $  wenzelm@20514  267  A \emph{well-typed term} is a term that can be typed according to these rules.  wenzelm@20498  268 wenzelm@20514  269  Typing information can be omitted: type-inference is able to  wenzelm@20514  270  reconstruct the most general type of a raw term, while assigning  wenzelm@20514  271  most general types to all of its variables and constants.  wenzelm@20514  272  Type-inference depends on a context of type constraints for fixed  wenzelm@20514  273  variables, and declarations for polymorphic constants.  wenzelm@20514  274 wenzelm@20537  275  The identity of atomic terms consists both of the name and the type  wenzelm@20537  276  component. This means that different variables @{text  wenzelm@20537  277  "x\<^bsub>\\<^isub>1\<^esub>"} and @{text  wenzelm@20537  278  "x\<^bsub>\\<^isub>2\<^esub>"} may become the same after type  wenzelm@20537  279  instantiation. Some outer layers of the system make it hard to  wenzelm@20537  280  produce variables of the same name, but different types. In  wenzelm@20543  281  contrast, mixed instances of polymorphic constants occur frequently.  wenzelm@20514  282 wenzelm@20514  283  \medskip The \emph{hidden polymorphism} of a term @{text "t :: \"}  wenzelm@20514  284  is the set of type variables occurring in @{text "t"}, but not in  wenzelm@20537  285  @{text "\"}. This means that the term implicitly depends on type  wenzelm@20543  286  arguments that are not accounted in the result type, i.e.\ there are  wenzelm@20537  287  different type instances @{text "t\ :: \"} and @{text  wenzelm@20537  288  "t\' :: \"} with the same type. This slightly  wenzelm@20543  289  pathological situation notoriously demands additional care.  wenzelm@20514  290 wenzelm@20514  291  \medskip A \emph{term abbreviation} is a syntactic definition @{text  wenzelm@20537  292  "c\<^isub>\ \ t"} of a closed term @{text "t"} of type @{text "\"},  wenzelm@20537  293  without any hidden polymorphism. A term abbreviation looks like a  wenzelm@20543  294  constant in the syntax, but is expanded before entering the logical  wenzelm@20543  295  core. Abbreviations are usually reverted when printing terms, using  wenzelm@20543  296  @{text "t \ c\<^isub>\"} as rules for higher-order rewriting.  wenzelm@20519  297 wenzelm@20519  298  \medskip Canonical operations on @{text "\"}-terms include @{text  wenzelm@20537  299  "\\\"}-conversion: @{text "\"}-conversion refers to capture-free  wenzelm@20519  300  renaming of bound variables; @{text "\"}-conversion contracts an  wenzelm@20537  301  abstraction applied to an argument term, substituting the argument  wenzelm@20519  302  in the body: @{text "(\x. b)a"} becomes @{text "b[a/x]"}; @{text  wenzelm@20519  303  "\"}-conversion contracts vacuous application-abstraction: @{text  wenzelm@20519  304  "\x. f x"} becomes @{text "f"}, provided that the bound variable  wenzelm@20537  305  does not occur in @{text "f"}.  wenzelm@20519  306 wenzelm@20537  307  Terms are normally treated modulo @{text "\"}-conversion, which is  wenzelm@20537  308  implicit in the de-Bruijn representation. Names for bound variables  wenzelm@20537  309  in abstractions are maintained separately as (meaningless) comments,  wenzelm@20537  310  mostly for parsing and printing. Full @{text "\\\"}-conversion is  wenzelm@28784  311  commonplace in various standard operations (\secref{sec:obj-rules})  wenzelm@28784  312  that are based on higher-order unification and matching.  wenzelm@18537  313 *}  wenzelm@18537  314 wenzelm@20514  315 text %mlref {*  wenzelm@20514  316  \begin{mldecls}  wenzelm@20514  317  @{index_ML_type term} \\  wenzelm@20519  318  @{index_ML "op aconv": "term * term -> bool"} \\  wenzelm@20547  319  @{index_ML map_types: "(typ -> typ) -> term -> term"} \\  wenzelm@20519  320  @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\  wenzelm@20514  321  @{index_ML map_aterms: "(term -> term) -> term -> term"} \\  wenzelm@20514  322  @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\  wenzelm@20547  323  \end{mldecls}  wenzelm@20547  324  \begin{mldecls}  wenzelm@20514  325  @{index_ML fastype_of: "term -> typ"} \\  wenzelm@20519  326  @{index_ML lambda: "term -> term -> term"} \\  wenzelm@20519  327  @{index_ML betapply: "term * term -> term"} \\  haftmann@29581  328  @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->  wenzelm@24972  329  theory -> term * theory"} \\  haftmann@29581  330  @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->  wenzelm@24972  331  theory -> (term * term) * theory"} \\  wenzelm@20519  332  @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\  wenzelm@20519  333  @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\  wenzelm@20514  334  \end{mldecls}  wenzelm@18537  335 wenzelm@20514  336  \begin{description}  wenzelm@18537  337 wenzelm@20537  338  \item @{ML_type term} represents de-Bruijn terms, with comments in  wenzelm@20537  339  abstractions, and explicitly named free variables and constants;  wenzelm@20537  340  this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML  wenzelm@20537  341  Var}, @{ML Const}, @{ML Abs}, @{ML "op \$"}.  wenzelm@20519  342 wenzelm@20519  343  \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text  wenzelm@20519  344  "\"}-equivalence of two terms. This is the basic equality relation  wenzelm@20519  345  on type @{ML_type term}; raw datatype equality should only be used  wenzelm@20519  346  for operations related to parsing or printing!  wenzelm@20519  347 wenzelm@20547  348  \item @{ML map_types}~@{text "f t"} applies the mapping @{text  wenzelm@20537  349  "f"} to all types occurring in @{text "t"}.  wenzelm@20537  350 wenzelm@20537  351  \item @{ML fold_types}~@{text "f t"} iterates the operation @{text  wenzelm@20537  352  "f"} over all occurrences of types in @{text "t"}; the term  wenzelm@20537  353  structure is traversed from left to right.  wenzelm@20519  354 wenzelm@20537  355  \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}  wenzelm@20537  356  to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML  wenzelm@20537  357  Const}) occurring in @{text "t"}.  wenzelm@20537  358 wenzelm@20537  359  \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text  wenzelm@20537  360  "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},  wenzelm@20537  361  @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is  wenzelm@20519  362  traversed from left to right.  wenzelm@20519  363 wenzelm@20537  364  \item @{ML fastype_of}~@{text "t"} determines the type of a  wenzelm@20537  365  well-typed term. This operation is relatively slow, despite the  wenzelm@20537  366  omission of any sanity checks.  wenzelm@20519  367 wenzelm@20519  368  \item @{ML lambda}~@{text "a b"} produces an abstraction @{text  wenzelm@20537  369  "\a. b"}, where occurrences of the atomic term @{text "a"} in the  wenzelm@20537  370  body @{text "b"} are replaced by bound variables.  wenzelm@20519  371 wenzelm@20537  372  \item @{ML betapply}~@{text "(t, u)"} produces an application @{text  wenzelm@20537  373  "t u"}, with topmost @{text "\"}-conversion if @{text "t"} is an  wenzelm@20537  374  abstraction.  wenzelm@20519  375 wenzelm@28110  376  \item @{ML Sign.declare_const}~@{text "properties ((c, \), mx)"}  wenzelm@24972  377  declares a new constant @{text "c :: \"} with optional mixfix  wenzelm@24972  378  syntax.  wenzelm@20519  379 wenzelm@24828  380  \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}  wenzelm@21827  381  introduces a new term abbreviation @{text "c \ t"}.  wenzelm@20519  382 wenzelm@20520  383  \item @{ML Sign.const_typargs}~@{text "thy (c, \)"} and @{ML  wenzelm@20520  384  Sign.const_instance}~@{text "thy (c, [\\<^isub>1, \, \\<^isub>n])"}  wenzelm@20543  385  convert between two representations of polymorphic constants: full  wenzelm@20543  386  type instance vs.\ compact type arguments form.  wenzelm@18537  387 wenzelm@20514  388  \end{description}  wenzelm@18537  389 *}  wenzelm@18537  390 wenzelm@18537  391 wenzelm@20451  392 section {* Theorems \label{sec:thms} *}  wenzelm@18537  393 wenzelm@18537  394 text {*  wenzelm@20521  395  \glossary{Proposition}{FIXME A \seeglossary{term} of  wenzelm@20521  396  \seeglossary{type} @{text "prop"}. Internally, there is nothing  wenzelm@20521  397  special about propositions apart from their type, but the concrete  wenzelm@20521  398  syntax enforces a clear distinction. Propositions are structured  wenzelm@20521  399  via implication @{text "A \ B"} or universal quantification @{text  wenzelm@20521  400  "\x. B x"} --- anything else is considered atomic. The canonical  wenzelm@20521  401  form for propositions is that of a \seeglossary{Hereditary Harrop  wenzelm@20521  402  Formula}. FIXME}  wenzelm@20480  403 wenzelm@20501  404  \glossary{Theorem}{A proven proposition within a certain theory and  wenzelm@20501  405  proof context, formally @{text "\ \\<^sub>\ \"}; both contexts are  wenzelm@20501  406  rarely spelled out explicitly. Theorems are usually normalized  wenzelm@20501  407  according to the \seeglossary{HHF} format. FIXME}  wenzelm@20480  408 wenzelm@20519  409  \glossary{Fact}{Sometimes used interchangeably for  wenzelm@20501  410  \seeglossary{theorem}. Strictly speaking, a list of theorems,  wenzelm@20501  411  essentially an extra-logical conjunction. Facts emerge either as  wenzelm@20501  412  local assumptions, or as results of local goal statements --- both  wenzelm@20501  413  may be simultaneous, hence the list representation. FIXME}  wenzelm@18537  414 wenzelm@20501  415  \glossary{Schematic variable}{FIXME}  wenzelm@20501  416 wenzelm@20501  417  \glossary{Fixed variable}{A variable that is bound within a certain  wenzelm@20501  418  proof context; an arbitrary-but-fixed entity within a portion of  wenzelm@20501  419  proof text. FIXME}  wenzelm@18537  420 wenzelm@20501  421  \glossary{Free variable}{Synonymous for \seeglossary{fixed  wenzelm@20501  422  variable}. FIXME}  wenzelm@20501  423 wenzelm@20501  424  \glossary{Bound variable}{FIXME}  wenzelm@18537  425 wenzelm@20501  426  \glossary{Variable}{See \seeglossary{schematic variable},  wenzelm@20501  427  \seeglossary{fixed variable}, \seeglossary{bound variable}, or  wenzelm@20501  428  \seeglossary{type variable}. The distinguishing feature of  wenzelm@20501  429  different variables is their binding scope. FIXME}  wenzelm@18537  430 wenzelm@20543  431  A \emph{proposition} is a well-typed term of type @{text "prop"}, a  wenzelm@20521  432  \emph{theorem} is a proven proposition (depending on a context of  wenzelm@20521  433  hypotheses and the background theory). Primitive inferences include  wenzelm@20521  434  plain natural deduction rules for the primary connectives @{text  wenzelm@20537  435  "\"} and @{text "\"} of the framework. There is also a builtin  wenzelm@20537  436  notion of equality/equivalence @{text "\"}.  wenzelm@20521  437 *}  wenzelm@20521  438 wenzelm@26872  439 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}  wenzelm@18537  440 wenzelm@20521  441 text {*  wenzelm@20543  442  The theory @{text "Pure"} contains constant declarations for the  wenzelm@20543  443  primitive connectives @{text "\"}, @{text "\"}, and @{text "\"} of  wenzelm@20543  444  the logical framework, see \figref{fig:pure-connectives}. The  wenzelm@20543  445  derivability judgment @{text "A\<^isub>1, \, A\<^isub>n \ B"} is  wenzelm@20543  446  defined inductively by the primitive inferences given in  wenzelm@20543  447  \figref{fig:prim-rules}, with the global restriction that the  wenzelm@20543  448  hypotheses must \emph{not} contain any schematic variables. The  wenzelm@20543  449  builtin equality is conceptually axiomatized as shown in  wenzelm@20521  450  \figref{fig:pure-equality}, although the implementation works  wenzelm@20543  451  directly with derived inferences.  wenzelm@20521  452 wenzelm@20521  453  \begin{figure}[htb]  wenzelm@20521  454  \begin{center}  wenzelm@20501  455  \begin{tabular}{ll}  wenzelm@20501  456  @{text "all :: (\ \ prop) \ prop"} & universal quantification (binder @{text "\"}) \\  wenzelm@20501  457  @{text "\ :: prop \ prop \ prop"} & implication (right associative infix) \\  wenzelm@20521  458  @{text "\ :: \ \ \ \ prop"} & equality relation (infix) \\  wenzelm@20501  459  \end{tabular}  wenzelm@20537  460  \caption{Primitive connectives of Pure}\label{fig:pure-connectives}  wenzelm@20521  461  \end{center}  wenzelm@20521  462  \end{figure}  wenzelm@18537  463 wenzelm@20501  464  \begin{figure}[htb]  wenzelm@20501  465  \begin{center}  wenzelm@20498  466  $ wenzelm@20498  467  \infer[@{text "(axiom)"}]{@{text "\ A"}}{@{text "A \ \"}}  wenzelm@20498  468  \qquad  wenzelm@20498  469  \infer[@{text "(assume)"}]{@{text "A \ A"}}{}  wenzelm@20498  470 $  wenzelm@20498  471  $ wenzelm@20537  472  \infer[@{text "(\_intro)"}]{@{text "\ \ \x. b[x]"}}{@{text "\ \ b[x]"} & @{text "x \ \"}}  wenzelm@20498  473  \qquad  wenzelm@20537  474  \infer[@{text "(\_elim)"}]{@{text "\ \ b[a]"}}{@{text "\ \ \x. b[x]"}}  wenzelm@20498  475 $  wenzelm@20498  476  $ wenzelm@20498  477  \infer[@{text "(\_intro)"}]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}}  wenzelm@20498  478  \qquad  wenzelm@20498  479  \infer[@{text "(\_elim)"}]{@{text "\\<^sub>1 \ \\<^sub>2 \ B"}}{@{text "\\<^sub>1 \ A \ B"} & @{text "\\<^sub>2 \ A"}}  wenzelm@20498  480 $  wenzelm@20521  481  \caption{Primitive inferences of Pure}\label{fig:prim-rules}  wenzelm@20521  482  \end{center}  wenzelm@20521  483  \end{figure}  wenzelm@20521  484 wenzelm@20521  485  \begin{figure}[htb]  wenzelm@20521  486  \begin{center}  wenzelm@20521  487  \begin{tabular}{ll}  wenzelm@20537  488  @{text "\ (\x. b[x]) a \ b[a]"} & @{text "\"}-conversion \\  wenzelm@20521  489  @{text "\ x \ x"} & reflexivity \\  wenzelm@20521  490  @{text "\ x \ y \ P x \ P y"} & substitution \\  wenzelm@20521  491  @{text "\ (\x. f x \ g x) \ f \ g"} & extensionality \\  wenzelm@20537  492  @{text "\ (A \ B) \ (B \ A) \ A \ B"} & logical equivalence \\  wenzelm@20521  493  \end{tabular}  wenzelm@20542  494  \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}  wenzelm@20501  495  \end{center}  wenzelm@20501  496  \end{figure}  wenzelm@18537  497 wenzelm@20501  498  The introduction and elimination rules for @{text "\"} and @{text  wenzelm@20537  499  "\"} are analogous to formation of dependently typed @{text  wenzelm@20501  500  "\"}-terms representing the underlying proof objects. Proof terms  wenzelm@20543  501  are irrelevant in the Pure logic, though; they cannot occur within  wenzelm@20543  502  propositions. The system provides a runtime option to record  wenzelm@20537  503  explicit proof terms for primitive inferences. Thus all three  wenzelm@20537  504  levels of @{text "\"}-calculus become explicit: @{text "\"} for  wenzelm@20537  505  terms, and @{text "\/\"} for proofs (cf.\  wenzelm@20537  506  \cite{Berghofer-Nipkow:2000:TPHOL}).  wenzelm@20491  507 wenzelm@20537  508  Observe that locally fixed parameters (as in @{text "\_intro"}) need  wenzelm@20537  509  not be recorded in the hypotheses, because the simple syntactic  wenzelm@20543  510  types of Pure are always inhabitable. Assumptions'' @{text "x ::  wenzelm@20543  511  \"} for type-membership are only present as long as some @{text  wenzelm@20543  512  "x\<^isub>\"} occurs in the statement body.\footnote{This is the key  wenzelm@20543  513  difference to @{text "\HOL"}'' in the PTS framework  wenzelm@20543  514  \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are  wenzelm@20543  515  treated uniformly for propositions and types.}  wenzelm@20501  516 wenzelm@20501  517  \medskip The axiomatization of a theory is implicitly closed by  wenzelm@20537  518  forming all instances of type and term variables: @{text "\  wenzelm@20537  519  A\"} holds for any substitution instance of an axiom  wenzelm@20543  520  @{text "\ A"}. By pushing substitutions through derivations  wenzelm@20543  521  inductively, we also get admissible @{text "generalize"} and @{text  wenzelm@20543  522  "instance"} rules as shown in \figref{fig:subst-rules}.  wenzelm@20501  523 wenzelm@20501  524  \begin{figure}[htb]  wenzelm@20501  525  \begin{center}  wenzelm@20498  526  $ wenzelm@20501  527  \infer{@{text "\ \ B[?$"}}{@{text "\ \ B[\]"} & @{text "\ \ \"}}  wenzelm@20501  528  \quad  wenzelm@20501  529  \infer[\quad@{text "(generalize)"}]{@{text "\ \ B[?x]"}}{@{text "\ \ B[x]"} & @{text "x \ \"}}  wenzelm@20498  530  \]  wenzelm@20498  531  $ wenzelm@20501  532  \infer{@{text "\ \ B[$"}}{@{text "\ \ B[?\]"}}  wenzelm@20501  533  \quad  wenzelm@20501  534  \infer[\quad@{text "(instantiate)"}]{@{text "\ \ B[t]"}}{@{text "\ \ B[?x]"}}  wenzelm@20498  535  \]  wenzelm@20501  536  \caption{Admissible substitution rules}\label{fig:subst-rules}  wenzelm@20501  537  \end{center}  wenzelm@20501  538  \end{figure}  wenzelm@18537  539 wenzelm@20537  540  Note that @{text "instantiate"} does not require an explicit  wenzelm@20537  541  side-condition, because @{text "\"} may never contain schematic  wenzelm@20537  542  variables.  wenzelm@20537  543 wenzelm@20537  544  In principle, variables could be substituted in hypotheses as well,  wenzelm@20543  545  but this would disrupt the monotonicity of reasoning: deriving  wenzelm@20543  546  @{text "\\ \ B\"} from @{text "\ \ B"} is  wenzelm@20543  547  correct, but @{text "\\ \ \"} does not necessarily hold:  wenzelm@20543  548  the result belongs to a different proof context.  wenzelm@20542  549 wenzelm@20543  550  \medskip An \emph{oracle} is a function that produces axioms on the  wenzelm@20543  551  fly. Logically, this is an instance of the @{text "axiom"} rule  wenzelm@20543  552  (\figref{fig:prim-rules}), but there is an operational difference.  wenzelm@20543  553  The system always records oracle invocations within derivations of  wenzelm@20543  554  theorems. Tracing plain axioms (and named theorems) is optional.  wenzelm@20542  555 wenzelm@20542  556  Axiomatizations should be limited to the bare minimum, typically as  wenzelm@20542  557  part of the initial logical basis of an object-logic formalization.  wenzelm@20543  558  Later on, theories are usually developed in a strictly definitional  wenzelm@20543  559  fashion, by stating only certain equalities over new constants.  wenzelm@20542  560 wenzelm@20542  561  A \emph{simple definition} consists of a constant declaration @{text  wenzelm@20543  562  "c :: \"} together with an axiom @{text "\ c \ t"}, where @{text "t  wenzelm@20543  563  :: \"} is a closed term without any hidden polymorphism. The RHS  wenzelm@20543  564  may depend on further defined constants, but not @{text "c"} itself.  wenzelm@20543  565  Definitions of functions may be presented as @{text "c \<^vec>x \  wenzelm@20543  566  t"} instead of the puristic @{text "c \ \\<^vec>x. t"}.  wenzelm@20542  567 wenzelm@20543  568  An \emph{overloaded definition} consists of a collection of axioms  wenzelm@20543  569  for the same constant, with zero or one equations @{text  wenzelm@20543  570  "c((\<^vec>\)\) \ t"} for each type constructor @{text "\"} (for  wenzelm@20543  571  distinct variables @{text "\<^vec>\"}). The RHS may mention  wenzelm@20543  572  previously defined constants as above, or arbitrary constants @{text  wenzelm@20543  573  "d(\\<^isub>i)"} for some @{text "\\<^isub>i"} projected from @{text  wenzelm@20543  574  "\<^vec>\"}. Thus overloaded definitions essentially work by  wenzelm@20543  575  primitive recursion over the syntactic structure of a single type  wenzelm@20543  576  argument.  wenzelm@20521  577 *}  wenzelm@20498  578 wenzelm@20521  579 text %mlref {*  wenzelm@20521  580  \begin{mldecls}  wenzelm@20521  581  @{index_ML_type ctyp} \\  wenzelm@20521  582  @{index_ML_type cterm} \\  wenzelm@20547  583  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\  wenzelm@20547  584  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\  wenzelm@20547  585  \end{mldecls}  wenzelm@20547  586  \begin{mldecls}  wenzelm@20521  587  @{index_ML_type thm} \\  wenzelm@20542  588  @{index_ML proofs: "int ref"} \\  wenzelm@20542  589  @{index_ML Thm.assume: "cterm -> thm"} \\  wenzelm@20542  590  @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\  wenzelm@20542  591  @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\  wenzelm@20542  592  @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\  wenzelm@20542  593  @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\  wenzelm@20542  594  @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\  wenzelm@20542  595  @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\  wenzelm@28674  596  @{index_ML Thm.axiom: "theory -> string -> thm"} \\  wenzelm@28290  597  @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory  wenzelm@28290  598  -> (string * ('a -> thm)) * theory"} \\  wenzelm@20547  599  \end{mldecls}  wenzelm@20547  600  \begin{mldecls}  haftmann@29615  601  @{index_ML Theory.add_axioms_i: "(binding * term) list -> theory -> theory"} \\  wenzelm@20542  602  @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\  haftmann@29615  603  @{index_ML Theory.add_defs_i: "bool -> bool -> (binding * term) list -> theory -> theory"} \\  wenzelm@20521  604  \end{mldecls}  wenzelm@20521  605 wenzelm@20521  606  \begin{description}  wenzelm@20521  607 wenzelm@20542  608  \item @{ML_type ctyp} and @{ML_type cterm} represent certified types  wenzelm@20542  609  and terms, respectively. These are abstract datatypes that  wenzelm@20542  610  guarantee that its values have passed the full well-formedness (and  wenzelm@20542  611  well-typedness) checks, relative to the declarations of type  wenzelm@20542  612  constructors, constants etc. in the theory.  wenzelm@20542  613 wenzelm@20547  614  \item @{ML ctyp_of}~@{text "thy \"} and @{ML cterm_of}~@{text "thy  wenzelm@20547  615  t"} explicitly checks types and terms, respectively. This also  wenzelm@20547  616  involves some basic normalizations, such expansion of type and term  wenzelm@20547  617  abbreviations from the theory context.  wenzelm@20547  618 wenzelm@20547  619  Re-certification is relatively slow and should be avoided in tight  wenzelm@20547  620  reasoning loops. There are separate operations to decompose  wenzelm@20547  621  certified entities (including actual theorems).  wenzelm@20542  622 wenzelm@20542  623  \item @{ML_type thm} represents proven propositions. This is an  wenzelm@20542  624  abstract datatype that guarantees that its values have been  wenzelm@20542  625  constructed by basic principles of the @{ML_struct Thm} module.  wenzelm@20543  626  Every @{ML thm} value contains a sliding back-reference to the  wenzelm@20543  627  enclosing theory, cf.\ \secref{sec:context-theory}.  wenzelm@20542  628 wenzelm@20543  629  \item @{ML proofs} determines the detail of proof recording within  wenzelm@20543  630  @{ML_type thm} values: @{ML 0} records only oracles, @{ML 1} records  wenzelm@20543  631  oracles, axioms and named theorems, @{ML 2} records full proof  wenzelm@20543  632  terms.  wenzelm@20542  633 wenzelm@20542  634  \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML  wenzelm@20542  635  Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}  wenzelm@20542  636  correspond to the primitive inferences of \figref{fig:prim-rules}.  wenzelm@20542  637 wenzelm@20542  638  \item @{ML Thm.generalize}~@{text "(\<^vec>\, \<^vec>x)"}  wenzelm@20542  639  corresponds to the @{text "generalize"} rules of  wenzelm@20543  640  \figref{fig:subst-rules}. Here collections of type and term  wenzelm@20543  641  variables are generalized simultaneously, specified by the given  wenzelm@20543  642  basic names.  wenzelm@20521  643 wenzelm@20542  644  \item @{ML Thm.instantiate}~@{text "(\<^vec>\\<^isub>s,  wenzelm@20542  645  \<^vec>x\<^isub>\)"} corresponds to the @{text "instantiate"} rules  wenzelm@20542  646  of \figref{fig:subst-rules}. Type variables are substituted before  wenzelm@20542  647  term variables. Note that the types in @{text "\<^vec>x\<^isub>\"}  wenzelm@20542  648  refer to the instantiated versions.  wenzelm@20542  649 wenzelm@28674  650  \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named  wenzelm@20542  651  axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.  wenzelm@20542  652 wenzelm@28290  653  \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named  wenzelm@28290  654  oracle rule, essentially generating arbitrary axioms on the fly,  wenzelm@28290  655  cf.\ @{text "axiom"} in \figref{fig:prim-rules}.  wenzelm@20521  656 wenzelm@20543  657  \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \]"} declares  wenzelm@20543  658  arbitrary propositions as axioms.  wenzelm@20542  659 wenzelm@20542  660  \item @{ML Theory.add_deps}~@{text "name c\<^isub>\  wenzelm@20543  661  \<^vec>d\<^isub>\"} declares dependencies of a named specification  wenzelm@20543  662  for constant @{text "c\<^isub>\"}, relative to existing  wenzelm@20543  663  specifications for constants @{text "\<^vec>d\<^isub>\"}.  wenzelm@20542  664 wenzelm@20542  665  \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c  wenzelm@20543  666  \<^vec>x \ t), \]"} states a definitional axiom for an existing  wenzelm@20543  667  constant @{text "c"}. Dependencies are recorded (cf.\ @{ML  wenzelm@20543  668  Theory.add_deps}), unless the @{text "unchecked"} option is set.  wenzelm@20521  669 wenzelm@20521  670  \end{description}  wenzelm@20521  671 *}  wenzelm@20521  672 wenzelm@20521  673 wenzelm@20543  674 subsection {* Auxiliary definitions *}  wenzelm@20521  675 wenzelm@20521  676 text {*  wenzelm@20543  677  Theory @{text "Pure"} provides a few auxiliary definitions, see  wenzelm@20543  678  \figref{fig:pure-aux}. These special constants are normally not  wenzelm@20543  679  exposed to the user, but appear in internal encodings.  wenzelm@20501  680 wenzelm@20501  681  \begin{figure}[htb]  wenzelm@20501  682  \begin{center}  wenzelm@20498  683  \begin{tabular}{ll}  wenzelm@20521  684  @{text "conjunction :: prop \ prop \ prop"} & (infix @{text "&"}) \\  wenzelm@20521  685  @{text "\ A & B \ (\C. (A \ B \ C) \ C)"} \$1ex]  wenzelm@20543  686  @{text "prop :: prop \ prop"} & (prefix @{text "#"}, suppressed) \\  wenzelm@20521  687  @{text "#A \ A"} \\[1ex]  wenzelm@20521  688  @{text "term :: \ \ prop"} & (prefix @{text "TERM"}) \\  wenzelm@20521  689  @{text "term x \ (\A. A \ A)"} \\[1ex]  wenzelm@20521  690  @{text "TYPE :: \ itself"} & (prefix @{text "TYPE"}) \\  wenzelm@20521  691  @{text "(unspecified)"} \\  wenzelm@20498  692  \end{tabular}  wenzelm@20521  693  \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}  wenzelm@20501  694  \end{center}  wenzelm@20501  695  \end{figure}  wenzelm@20501  696 wenzelm@20537  697  Derived conjunction rules include introduction @{text "A \ B \ A &  wenzelm@20537  698  B"}, and destructions @{text "A & B \ A"} and @{text "A & B \ B"}.  wenzelm@20537  699  Conjunction allows to treat simultaneous assumptions and conclusions  wenzelm@20537  700  uniformly. For example, multiple claims are intermediately  wenzelm@20543  701  represented as explicit conjunction, but this is refined into  wenzelm@20543  702  separate sub-goals before the user continues the proof; the final  wenzelm@20543  703  result is projected into a list of theorems (cf.\  wenzelm@20537  704  \secref{sec:tactical-goals}).  wenzelm@20498  705 wenzelm@20537  706  The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex  wenzelm@20537  707  propositions appear as atomic, without changing the meaning: @{text  wenzelm@20537  708  "\ \ A"} and @{text "\ \ #A"} are interchangeable. See  wenzelm@20537  709  \secref{sec:tactical-goals} for specific operations.  wenzelm@20521  710 wenzelm@20543  711  The @{text "term"} marker turns any well-typed term into a derivable  wenzelm@20543  712  proposition: @{text "\ TERM t"} holds unconditionally. Although  wenzelm@20543  713  this is logically vacuous, it allows to treat terms and proofs  wenzelm@20543  714  uniformly, similar to a type-theoretic framework.  wenzelm@20498  715 wenzelm@20537  716  The @{text "TYPE"} constructor is the canonical representative of  wenzelm@20537  717  the unspecified type @{text "\ itself"}; it essentially injects the  wenzelm@20537  718  language of types into that of terms. There is specific notation  wenzelm@20537  719  @{text "TYPE(\)"} for @{text "TYPE\<^bsub>\  wenzelm@20521  720  itself\<^esub>"}.  wenzelm@20537  721  Although being devoid of any particular meaning, the @{text  wenzelm@20537  722  "TYPE(\)"} accounts for the type @{text "\"} within the term  wenzelm@20537  723  language. In particular, @{text "TYPE(\)"} may be used as formal  wenzelm@20537  724  argument in primitive definitions, in order to circumvent hidden  wenzelm@20537  725  polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c  wenzelm@20537  726  TYPE(\) \ A[$"} defines @{text "c :: \ itself \ prop"} in terms of  wenzelm@20537  727  a proposition @{text "A"} that depends on an additional type  wenzelm@20537  728  argument, which is essentially a predicate on types.  wenzelm@20521  729 *}  wenzelm@20501  730 wenzelm@20521  731 text %mlref {*  wenzelm@20521  732  \begin{mldecls}  wenzelm@20521  733  @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\  wenzelm@20521  734  @{index_ML Conjunction.elim: "thm -> thm * thm"} \\  wenzelm@20521  735  @{index_ML Drule.mk_term: "cterm -> thm"} \\  wenzelm@20521  736  @{index_ML Drule.dest_term: "thm -> cterm"} \\  wenzelm@20521  737  @{index_ML Logic.mk_type: "typ -> term"} \\  wenzelm@20521  738  @{index_ML Logic.dest_type: "term -> typ"} \\  wenzelm@20521  739  \end{mldecls}  wenzelm@20521  740 wenzelm@20521  741  \begin{description}  wenzelm@20521  742 wenzelm@20542  743  \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text  wenzelm@20542  744  "A"} and @{text "B"}.  wenzelm@20542  745 wenzelm@20543  746  \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}  wenzelm@20542  747  from @{text "A & B"}.  wenzelm@20542  748 wenzelm@20543  749  \item @{ML Drule.mk_term} derives @{text "TERM t"}.  wenzelm@20542  750 wenzelm@20543  751  \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text  wenzelm@20543  752  "TERM t"}.  wenzelm@20542  753 wenzelm@20542  754  \item @{ML Logic.mk_type}~@{text "\"} produces the term @{text  wenzelm@20542  755  "TYPE(\)"}.  wenzelm@20542  756 wenzelm@20542  757  \item @{ML Logic.dest_type}~@{text "TYPE(\)"} recovers the type  wenzelm@20542  758  @{text "\"}.  wenzelm@20521  759 wenzelm@20521  760  \end{description}  wenzelm@20491  761 *}  wenzelm@18537  762 wenzelm@20480  763 wenzelm@28784  764 section {* Object-level rules \label{sec:obj-rules} *}  wenzelm@18537  765 wenzelm@20929  766 text %FIXME {*  wenzelm@18537  767 wenzelm@18537  768 FIXME  wenzelm@18537  769 wenzelm@20491  770  A \emph{rule} is any Pure theorem in HHF normal form; there is a  wenzelm@20491  771  separate calculus for rule composition, which is modeled after  wenzelm@20491  772  Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows  wenzelm@20491  773  rules to be nested arbitrarily, similar to \cite{extensions91}.  wenzelm@20491  774 wenzelm@20491  775  Normally, all theorems accessible to the user are proper rules.  wenzelm@20491  776  Low-level inferences are occasional required internally, but the  wenzelm@20491  777  result should be always presented in canonical form. The higher  wenzelm@20491  778  interfaces of Isabelle/Isar will always produce proper rules. It is  wenzelm@20491  779  important to maintain this invariant in add-on applications!  wenzelm@20491  780 wenzelm@20491  781  There are two main principles of rule composition: @{text  wenzelm@20491  782  "resolution"} (i.e.\ backchaining of rules) and @{text  wenzelm@20491  783  "by-assumption"} (i.e.\ closing a branch); both principles are  wenzelm@20519  784  combined in the variants of @{text "elim-resolution"} and @{text  wenzelm@20491  785  "dest-resolution"}. Raw @{text "composition"} is occasionally  wenzelm@20491  786  useful as well, also it is strictly speaking outside of the proper  wenzelm@20491  787  rule calculus.  wenzelm@20491  788 wenzelm@20491  789  Rules are treated modulo general higher-order unification, which is  wenzelm@20491  790  unification modulo the equational theory of @{text "\\\"}-conversion  wenzelm@20491  791  on @{text "\"}-terms. Moreover, propositions are understood modulo  wenzelm@20491  792  the (derived) equivalence @{text "(A \ (\x. B x)) \ (\x. A \ B x)"}.  wenzelm@20491  793 wenzelm@20491  794  This means that any operations within the rule calculus may be  wenzelm@20491  795  subject to spontaneous @{text "\\\"}-HHF conversions. It is common  wenzelm@20491  796  practice not to contract or expand unnecessarily. Some mechanisms  wenzelm@20491  797  prefer an one form, others the opposite, so there is a potential  wenzelm@20491  798  danger to produce some oscillation!  wenzelm@20491  799 wenzelm@20491  800  Only few operations really work \emph{modulo} HHF conversion, but  wenzelm@20491  801  expect a normal form: quantifiers @{text "\"} before implications  wenzelm@20491  802  @{text "\"} at each level of nesting.  wenzelm@20491  803 wenzelm@18537  804 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF  wenzelm@18537  805 format is defined inductively as @{text "H = (\x\<^sup>*. H\<^sup>* \  wenzelm@18537  806 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.  wenzelm@18537  807 Any proposition may be put into HHF form by normalizing with the rule  wenzelm@18537  808 @{text "(A \ (\x. B x)) \ (\x. A \ B x)"}. In Isabelle, the outermost  wenzelm@18537  809 quantifier prefix is represented via \seeglossary{schematic  wenzelm@18537  810 variables}, such that the top-level structure is merely that of a  wenzelm@18537  811 \seeglossary{Horn Clause}}.  wenzelm@18537  812 wenzelm@18537  813 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}  wenzelm@18537  814 wenzelm@20498  815 wenzelm@20498  816  $ wenzelm@20498  817  \infer[@{text "(assumption)"}]{@{text "C\"}}  wenzelm@20498  818  {@{text "(\\<^vec>x. \<^vec>H \<^vec>x \ A \<^vec>x) \ C"} & @{text "A\ = H\<^sub>i\"}~~\text{(for some~@{text i})}}  wenzelm@20498  819 $  wenzelm@20498  820 wenzelm@20498  821 wenzelm@20498  822  $ wenzelm@20498  823  \infer[@{text "(compose)"}]{@{text "\<^vec>A\ \ C\"}}  wenzelm@20498  824  {@{text "\<^vec>A \ B"} & @{text "B' \ C"} & @{text "B\ = B'\"}}  wenzelm@20498  825 $  wenzelm@20498  826 wenzelm@20498  827 wenzelm@20498  828  $ wenzelm@20498  829  \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  830 $  wenzelm@20498  831  $ wenzelm@20498  832  \infer[@{text "(\_lift)"}]{@{text "(\<^vec>H \ \<^vec>A) \ (\<^vec>H \ B)"}}{@{text "\<^vec>A \ B"}}  wenzelm@20498  833 $  wenzelm@20498  834 wenzelm@20498  835  The @{text resolve} scheme is now acquired from @{text "\_lift"},  wenzelm@20498  836  @{text "\_lift"}, and @{text compose}.  wenzelm@20498  837 wenzelm@20498  838  $ wenzelm@20498  839  \infer[@{text "(resolution)"}]  wenzelm@20498  840  {@{text "(\\<^vec>x. \<^vec>H \<^vec>x \ \<^vec>A (?\<^vec>a \<^vec>x))\ \ C\"}}  wenzelm@20498  841  {\begin{tabular}{l}  wenzelm@20498  842  @{text "\<^vec>A ?\<^vec>a \ B ?\<^vec>a"} \\  wenzelm@20498  843  @{text "(\\<^vec>x. \<^vec>H \<^vec>x \ B' \<^vec>x) \ C"} \\  wenzelm@20498  844  @{text "(\\<^vec>x. B (?\<^vec>a \<^vec>x))\ = B'\"} \\  wenzelm@20498  845  \end{tabular}}  wenzelm@20498  846 $  wenzelm@20498  847 wenzelm@20498  848 wenzelm@20498  849  FIXME @{text "elim_resolution"}, @{text "dest_resolution"}  wenzelm@18537  850 *}  wenzelm@18537  851 wenzelm@18537  852 end