summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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