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.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.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.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.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.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.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.100    \begin{description}
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.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.113 +  \item @{ML map_term_types}~@{text "f t"} applies mapping @{text "f"}
1.114 +  to all types occurring in @{text "t"}.
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.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.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.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.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.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.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.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.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.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.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.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.