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