doc-src/IsarImplementation/Thy/logic.thy
changeset 20494 99ad217b6974
parent 20493 48fea5e99505
child 20498 825a8d2335ce
--- a/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 17:33:05 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 19:44:43 2006 +0200
@@ -70,45 +70,46 @@
 
   A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
   on types declared in the theory.  Type constructor application is
-  usually written postfix as @{text "(FIXME)\<kappa>"}.  For @{text "k = 0"}
-  the argument tuple is omitted, e.g.\ @{text "prop"} instead of
-  @{text "()prop"}.  For @{text "k = 1"} the parentheses are omitted,
-  e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.  Further
-  notation is provided for specific constructors, notably
-  right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
-  \<beta>)fun"} constructor.
+  usually written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.
+  For @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text
+  "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
+  parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text
+  "(\<alpha>)list"}.  Further notation is provided for specific constructors,
+  notably the right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of
+  @{text "(\<alpha>, \<beta>)fun"}.
   
   A \emph{type} is defined inductively over type variables and type
   constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
-  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}.
+  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.
 
-  A \emph{type abbreviation} is a syntactic abbreviation of an
-  arbitrary type expression of the theory.  Type abbreviations looks
-  like type constructors at the surface, but are expanded before the
-  core logic encounters them.
+  A \emph{type abbreviation} is a syntactic abbreviation @{text
+  "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
+  variables @{text "\<^vec>\<alpha>"}.  Type abbreviations looks like type
+  constructors at the surface, but are fully expanded before entering
+  the logical core.
 
   A \emph{type arity} declares the image behavior of a type
-  constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
-  s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
-  of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
-  sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
-  completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::
+  constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,
+  s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is
+  of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is
+  of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
+  completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
 
   \medskip The sort algebra is always maintained as \emph{coregular},
   which means that type arities are consistent with the subclass
-  relation: for each type constructor @{text "c"} and classes @{text
-  "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
-  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
+  relation: for each type constructor @{text "\<kappa>"} and classes @{text
+  "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "\<kappa> ::
+  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>
   :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
-  \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
+  \<^vec>s\<^isub>2"} holds componentwise.
 
   The key property of a coregular order-sorted algebra is that sort
-  constraints may be always fulfilled in a most general fashion: for
-  each type constructor @{text "c"} and sort @{text "s"} there is a
-  most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
+  constraints may be always solved in a most general fashion: for each
+  type constructor @{text "\<kappa>"} and sort @{text "s"} there is a most
+  general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
   s\<^isub>k)"} such that a type scheme @{text
-  "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is
+  "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is
   of sort @{text "s"}.  Consequently, the unification problem on the
   algebra of types has most general solutions (modulo renaming and
   equivalence of sorts).  Moreover, the usual type-inference algorithm
@@ -119,8 +120,9 @@
   \begin{mldecls}
   @{index_ML_type class} \\
   @{index_ML_type sort} \\
+  @{index_ML_type arity} \\
   @{index_ML_type typ} \\
-  @{index_ML_type arity} \\
+  @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
@@ -140,36 +142,40 @@
   @{ML_type "class list"}.
 
   \item @{ML_type arity} represents type arities; this is an alias for
-  triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
+  triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
   (\<^vec>s)s"} described above.
 
   \item @{ML_type typ} represents types; this is a datatype with
   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
 
+  \item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}
+  over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text
+  "\<tau>"}; the type structure is traversed from left to right.
+
   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
 
   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
   is of a given sort.
 
-  \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
-  type constructors @{text "c"} with @{text "k"} arguments and
+  \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares new
+  type constructors @{text "\<kappa>"} with @{text "k"} arguments and
   optional mixfix syntax.
 
-  \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
-  defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with
+  \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
+  defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
   optional mixfix syntax.
 
   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
-  c\<^isub>n])"} declares new class @{text "c"} derived together with
-  class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
+  c\<^isub>n])"} declares new class @{text "c"}, together with class
+  relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
 
   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
   c\<^isub>2"}.
 
-  \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
-  arity @{text "c :: (\<^vec>s)s"}.
+  \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
+  arity @{text "\<kappa> :: (\<^vec>s)s"}.
 
   \end{description}
 *}