doc-src/IsarImplementation/Thy/logic.thy
changeset 20519 d7ad1217c24a
parent 20514 5ede702cd2ca
child 20520 05fd007bdeb9
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 17:12:51 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 17:23:34 2006 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4    "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "\<kappa> ::
     1.5    (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>
     1.6    :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
     1.7 -  \<^vec>s\<^isub>2"} holds componentwise.
     1.8 +  \<^vec>s\<^isub>2"} holds component-wise.
     1.9  
    1.10    The key property of a coregular order-sorted algebra is that sort
    1.11    constraints may be always solved in a most general fashion: for each
    1.12 @@ -122,6 +122,7 @@
    1.13    @{index_ML_type sort} \\
    1.14    @{index_ML_type arity} \\
    1.15    @{index_ML_type typ} \\
    1.16 +  @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
    1.17    @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
    1.18    @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
    1.19    @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
    1.20 @@ -148,8 +149,11 @@
    1.21    \item @{ML_type typ} represents types; this is a datatype with
    1.22    constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
    1.23  
    1.24 -  \item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}
    1.25 -  over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text
    1.26 +  \item @{ML map_atyps}~@{text "f \<tau>"} applies mapping @{text "f"} to
    1.27 +  all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text "\<tau>"}.
    1.28 +
    1.29 +  \item @{ML fold_atyps}~@{text "f \<tau>"} iterates operation @{text "f"}
    1.30 +  over all occurrences of atoms (@{ML TFree}, @{ML TVar}) in @{text
    1.31    "\<tau>"}; the type structure is traversed from left to right.
    1.32  
    1.33    \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
    1.34 @@ -188,18 +192,18 @@
    1.35    \glossary{Term}{FIXME}
    1.36  
    1.37    The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
    1.38 -  with de-Bruijn indices for bound variables, and named free variables
    1.39 -  and constants.  Terms with loose bound variables are usually
    1.40 -  considered malformed.  The types of variables and constants is
    1.41 -  stored explicitly at each occurrence in the term.
    1.42 +  with de-Bruijn indices for bound variables
    1.43 +  \cite{debruijn72,paulson-ml2}, and named free variables and
    1.44 +  constants.  Terms with loose bound variables are usually considered
    1.45 +  malformed.  The types of variables and constants is stored
    1.46 +  explicitly at each occurrence in the term.
    1.47  
    1.48    \medskip A \emph{bound variable} is a natural number @{text "b"},
    1.49    which refers to the next binder that is @{text "b"} steps upwards
    1.50    from the occurrence of @{text "b"} (counting from zero).  Bindings
    1.51    may be introduced as abstractions within the term, or as a separate
    1.52    context (an inside-out list).  This associates each bound variable
    1.53 -  with a type, and a name that is maintained as a comment for parsing
    1.54 -  and printing.  A \emph{loose variables} is a bound variable that is
    1.55 +  with a type.  A \emph{loose variables} is a bound variable that is
    1.56    outside the current scope of local binders or the context.  For
    1.57    example, the de-Bruijn term @{text "\<lambda>\<^isub>\<tau>. \<lambda>\<^isub>\<tau>. 1 + 0"}
    1.58    corresponds to @{text "\<lambda>x\<^isub>\<tau>. \<lambda>y\<^isub>\<tau>. x + y"} in a named
    1.59 @@ -284,20 +288,96 @@
    1.60    entering the logical core.  Abbreviations are usually reverted when
    1.61    printing terms, using rules @{text "t \<rightarrow> c\<^isub>\<sigma>"} has a
    1.62    higher-order term rewrite system.
    1.63 +
    1.64 +  \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
    1.65 +  "\<alpha>\<beta>\<eta>"}-conversion. @{text "\<alpha>"}-conversion refers to capture-free
    1.66 +  renaming of bound variables; @{text "\<beta>"}-conversion contracts an
    1.67 +  abstraction applied to some argument term, substituting the argument
    1.68 +  in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
    1.69 +  "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
    1.70 +  "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
    1.71 +  @{text "0"} does not occur in @{text "f"}.
    1.72 +
    1.73 +  Terms are almost always treated module @{text "\<alpha>"}-conversion, which
    1.74 +  is implicit in the de-Bruijn representation.  The names in
    1.75 +  abstractions of bound variables are maintained only as a comment for
    1.76 +  parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-equivalence is usually
    1.77 +  taken for granted higher rules (\secref{sec:rules}), anything
    1.78 +  depending on higher-order unification or rewriting.
    1.79  *}
    1.80  
    1.81  text %mlref {*
    1.82    \begin{mldecls}
    1.83    @{index_ML_type term} \\
    1.84 +  @{index_ML "op aconv": "term * term -> bool"} \\
    1.85 +  @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\  %FIXME rename map_types
    1.86 +  @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
    1.87    @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
    1.88    @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
    1.89    @{index_ML fastype_of: "term -> typ"} \\
    1.90 -  @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
    1.91 +  @{index_ML lambda: "term -> term -> term"} \\
    1.92 +  @{index_ML betapply: "term * term -> term"} \\
    1.93 +  @{index_ML Sign.add_consts_i: "(bstring * typ * mixfix) list -> theory -> theory"} \\
    1.94 +  @{index_ML Sign.add_abbrevs: "string * bool ->
    1.95 +  ((bstring * mixfix) * term) list -> theory -> theory"} \\
    1.96 +  @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    1.97 +  @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
    1.98    \end{mldecls}
    1.99  
   1.100    \begin{description}
   1.101  
   1.102 -  \item @{ML_type term} FIXME
   1.103 +  \item @{ML_type term} represents de-Bruijn terms with comments in
   1.104 +  abstractions for bound variable names.  This is a datatype with
   1.105 +  constructors @{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}, @{ML
   1.106 +  Abs}, @{ML "op $"}.
   1.107 +
   1.108 +  \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
   1.109 +  "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
   1.110 +  on type @{ML_type term}; raw datatype equality should only be used
   1.111 +  for operations related to parsing or printing!
   1.112 +
   1.113 +  \item @{ML map_term_types}~@{text "f t"} applies mapping @{text "f"}
   1.114 +  to all types occurring in @{text "t"}.
   1.115 +
   1.116 +  \item @{ML fold_types}~@{text "f t"} iterates operation @{text "f"}
   1.117 +  over all occurrences of types in @{text "t"}; the term structure is
   1.118 +  traversed from left to right.
   1.119 +
   1.120 +  \item @{ML map_aterms}~@{text "f t"} applies mapping @{text "f"} to
   1.121 +  all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const})
   1.122 +  occurring in @{text "t"}.
   1.123 +
   1.124 +  \item @{ML fold_aterms}~@{text "f t"} iterates operation @{text "f"}
   1.125 +  over all occurrences of atomic terms in (@{ML Bound}, @{ML Free},
   1.126 +  @{ML Var}, @{ML Const}) @{text "t"}; the term structure is traversed
   1.127 +  from left to right.
   1.128 +
   1.129 +  \item @{ML fastype_of}~@{text "t"} recomputes the type of a
   1.130 +  well-formed term, while omitting any sanity checks.  This operation
   1.131 +  is relatively slow.
   1.132 +
   1.133 +  \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
   1.134 +  "\<lambda>a. b"}, where occurrences of the original (atomic) term @{text
   1.135 +  "a"} are replaced by bound variables.
   1.136 +
   1.137 +  \item @{ML betapply}~@{text "t u"} produces an application @{text "t
   1.138 +  u"}, with topmost @{text "\<beta>"}-conversion @{text "t"} is an
   1.139 +  abstraction.
   1.140 +
   1.141 +  \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
   1.142 +  new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
   1.143 +
   1.144 +  \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}
   1.145 +  declares a new term abbreviation @{text "c \<equiv> t"} with optional
   1.146 +  mixfix syntax.
   1.147 +
   1.148 +  \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} produces the
   1.149 +  type arguments of the instance @{text "c\<^isub>\<tau>"} wrt.\ its
   1.150 +  declaration in the theory.
   1.151 +
   1.152 +  \item @{ML Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>,
   1.153 +  \<tau>\<^isub>n])"} produces the full instance @{text "c(\<tau>\<^isub>1, \<dots>,
   1.154 +  \<tau>\<^isub>n)"} wrt.\ its declaration in the theory.
   1.155  
   1.156    \end{description}
   1.157  *}
   1.158 @@ -319,7 +399,7 @@
   1.159    rarely spelled out explicitly.  Theorems are usually normalized
   1.160    according to the \seeglossary{HHF} format. FIXME}
   1.161  
   1.162 -  \glossary{Fact}{Sometimes used interchangably for
   1.163 +  \glossary{Fact}{Sometimes used interchangeably for
   1.164    \seeglossary{theorem}.  Strictly speaking, a list of theorems,
   1.165    essentially an extra-logical conjunction.  Facts emerge either as
   1.166    local assumptions, or as results of local goal statements --- both
   1.167 @@ -495,7 +575,7 @@
   1.168    There are two main principles of rule composition: @{text
   1.169    "resolution"} (i.e.\ backchaining of rules) and @{text
   1.170    "by-assumption"} (i.e.\ closing a branch); both principles are
   1.171 -  combined in the variants of @{text "elim-resosultion"} and @{text
   1.172 +  combined in the variants of @{text "elim-resolution"} and @{text
   1.173    "dest-resolution"}.  Raw @{text "composition"} is occasionally
   1.174    useful as well, also it is strictly speaking outside of the proper
   1.175    rule calculus.