doc-src/IsarRef/logics.tex
 changeset 13016 c039b8ede204 parent 13014 3c1c493e6d93 child 13024 0461b281c2b5
     1.1 --- a/doc-src/IsarRef/logics.tex	Mon Mar 04 19:08:15 2002 +0100
1.2 +++ b/doc-src/IsarRef/logics.tex	Mon Mar 04 22:31:21 2002 +0100
1.3 @@ -34,9 +34,6 @@
1.4  declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
1.5  Reasoner \S\ref{sec:classical}).
1.6
1.7 -\railalias{ruleformat}{rule\_format}
1.8 -\railterm{ruleformat}
1.9 -
1.10  \begin{rail}
1.11    'judgment' constdecl
1.12    ;
1.13 @@ -96,7 +93,12 @@
1.14  \begin{rail}
1.15    'typedecl' typespec infix?
1.16    ;
1.17 -  'typedef' parname? typespec infix? '=' term
1.18 +  'typedef' parname? abstype '=' repset
1.19 +  ;
1.20 +
1.21 +  abstype: typespec infix?
1.22 +  ;
1.23 +  repset: term ('morphisms' name name)?
1.24    ;
1.25  \end{rail}
1.26
1.27 @@ -113,17 +115,22 @@
1.28    bijection between the representing set $A$ and the new type $t$.
1.29
1.30    Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term
1.31 -  constant) of the same name.  The injection from type to set is called
1.32 -  $Rep_t$, its inverse $Abs_t$.  Theorems $Rep_t$, $Rep_inverse$, and
1.33 -  $Abs_inverse$ provide the most basic characterization as a corresponding
1.34 -  injection/surjection pair (in both directions).  Rules $Rep_t_inject$ and
1.35 -  $Abs_t_inject$ provide a slightly more comfortable view on the injectivity
1.36 -  part; likewise do $Rep_t_cases$, $Rep_t_induct$, and $Abs_t_cases$,
1.37 -  $Abs_t_induct$ for surjectivity.  The latter rules are already declare as
1.38 -  type or set rules for the generic $cases$ and $induct$ methods.
1.39 +  constant) of the same name (an alternative base name may be given in
1.40 +  parentheses).  The injection from type to set is called $Rep_t$, its inverse
1.41 +  $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$
1.42 +  declaration).
1.43 +
1.44 +  Theorems $Rep_t$, $Rep_inverse$, and $Abs_inverse$ provide the most basic
1.45 +  characterization as a corresponding injection/surjection pair (in both
1.46 +  directions).  Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly
1.47 +  more comfortable view on the injectivity part, suitable for automated proof
1.48 +  tools (e.g.\ in $simp$ or $iff$ declarations).  Rules $Rep_t_cases$,
1.49 +  $Rep_t_induct$, and $Abs_t_cases$, $Abs_t_induct$ provide alternative views
1.50 +  on surjectivity; these are already declared as type or set rules for the
1.51 +  generic $cases$ and $induct$ methods.
1.52  \end{descr}
1.53
1.54 -Raw type declarations are rarely useful in practice.  The main application is
1.55 +Raw type declarations are rarely used in practice; the main application is
1.56  with experimental (or even axiomatic!) theory fragments.  Instead of primitive
1.57  HOL type definitions, user-level theories usually refer to higher-level
1.58  packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or