doc-src/IsarImplementation/Thy/logic.thy
changeset 20494 99ad217b6974
parent 20493 48fea5e99505
child 20498 825a8d2335ce
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 17:33:05 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 19:44:43 2006 +0200
     1.3 @@ -70,45 +70,46 @@
     1.4  
     1.5    A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
     1.6    on types declared in the theory.  Type constructor application is
     1.7 -  usually written postfix as @{text "(FIXME)\<kappa>"}.  For @{text "k = 0"}
     1.8 -  the argument tuple is omitted, e.g.\ @{text "prop"} instead of
     1.9 -  @{text "()prop"}.  For @{text "k = 1"} the parentheses are omitted,
    1.10 -  e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.  Further
    1.11 -  notation is provided for specific constructors, notably
    1.12 -  right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
    1.13 -  \<beta>)fun"} constructor.
    1.14 +  usually written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.
    1.15 +  For @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text
    1.16 +  "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
    1.17 +  parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text
    1.18 +  "(\<alpha>)list"}.  Further notation is provided for specific constructors,
    1.19 +  notably the right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of
    1.20 +  @{text "(\<alpha>, \<beta>)fun"}.
    1.21    
    1.22    A \emph{type} is defined inductively over type variables and type
    1.23    constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
    1.24 -  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}.
    1.25 +  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.
    1.26  
    1.27 -  A \emph{type abbreviation} is a syntactic abbreviation of an
    1.28 -  arbitrary type expression of the theory.  Type abbreviations looks
    1.29 -  like type constructors at the surface, but are expanded before the
    1.30 -  core logic encounters them.
    1.31 +  A \emph{type abbreviation} is a syntactic abbreviation @{text
    1.32 +  "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
    1.33 +  variables @{text "\<^vec>\<alpha>"}.  Type abbreviations looks like type
    1.34 +  constructors at the surface, but are fully expanded before entering
    1.35 +  the logical core.
    1.36  
    1.37    A \emph{type arity} declares the image behavior of a type
    1.38 -  constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
    1.39 -  s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
    1.40 -  of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
    1.41 -  sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
    1.42 -  completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::
    1.43 +  constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,
    1.44 +  s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is
    1.45 +  of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is
    1.46 +  of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
    1.47 +  completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
    1.48    (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
    1.49  
    1.50    \medskip The sort algebra is always maintained as \emph{coregular},
    1.51    which means that type arities are consistent with the subclass
    1.52 -  relation: for each type constructor @{text "c"} and classes @{text
    1.53 -  "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
    1.54 -  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
    1.55 +  relation: for each type constructor @{text "\<kappa>"} and classes @{text
    1.56 +  "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "\<kappa> ::
    1.57 +  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>
    1.58    :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
    1.59 -  \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
    1.60 +  \<^vec>s\<^isub>2"} holds componentwise.
    1.61  
    1.62    The key property of a coregular order-sorted algebra is that sort
    1.63 -  constraints may be always fulfilled in a most general fashion: for
    1.64 -  each type constructor @{text "c"} and sort @{text "s"} there is a
    1.65 -  most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
    1.66 +  constraints may be always solved in a most general fashion: for each
    1.67 +  type constructor @{text "\<kappa>"} and sort @{text "s"} there is a most
    1.68 +  general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
    1.69    s\<^isub>k)"} such that a type scheme @{text
    1.70 -  "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is
    1.71 +  "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is
    1.72    of sort @{text "s"}.  Consequently, the unification problem on the
    1.73    algebra of types has most general solutions (modulo renaming and
    1.74    equivalence of sorts).  Moreover, the usual type-inference algorithm
    1.75 @@ -119,8 +120,9 @@
    1.76    \begin{mldecls}
    1.77    @{index_ML_type class} \\
    1.78    @{index_ML_type sort} \\
    1.79 +  @{index_ML_type arity} \\
    1.80    @{index_ML_type typ} \\
    1.81 -  @{index_ML_type arity} \\
    1.82 +  @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
    1.83    @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
    1.84    @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
    1.85    @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
    1.86 @@ -140,36 +142,40 @@
    1.87    @{ML_type "class list"}.
    1.88  
    1.89    \item @{ML_type arity} represents type arities; this is an alias for
    1.90 -  triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
    1.91 +  triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
    1.92    (\<^vec>s)s"} described above.
    1.93  
    1.94    \item @{ML_type typ} represents types; this is a datatype with
    1.95    constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
    1.96  
    1.97 +  \item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}
    1.98 +  over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text
    1.99 +  "\<tau>"}; the type structure is traversed from left to right.
   1.100 +
   1.101    \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
   1.102    tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
   1.103  
   1.104    \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
   1.105    is of a given sort.
   1.106  
   1.107 -  \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
   1.108 -  type constructors @{text "c"} with @{text "k"} arguments and
   1.109 +  \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares new
   1.110 +  type constructors @{text "\<kappa>"} with @{text "k"} arguments and
   1.111    optional mixfix syntax.
   1.112  
   1.113 -  \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
   1.114 -  defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with
   1.115 +  \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
   1.116 +  defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
   1.117    optional mixfix syntax.
   1.118  
   1.119    \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
   1.120 -  c\<^isub>n])"} declares new class @{text "c"} derived together with
   1.121 -  class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
   1.122 +  c\<^isub>n])"} declares new class @{text "c"}, together with class
   1.123 +  relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
   1.124  
   1.125    \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   1.126    c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
   1.127    c\<^isub>2"}.
   1.128  
   1.129 -  \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
   1.130 -  arity @{text "c :: (\<^vec>s)s"}.
   1.131 +  \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
   1.132 +  arity @{text "\<kappa> :: (\<^vec>s)s"}.
   1.133  
   1.134    \end{description}
   1.135  *}