111 non-emptiness of the set $A$. After finishing the proof, the theory will be |
113 non-emptiness of the set $A$. After finishing the proof, the theory will be |
112 augmented by a Gordon/HOL-style type definition, which establishes a |
114 augmented by a Gordon/HOL-style type definition, which establishes a |
113 bijection between the representing set $A$ and the new type $t$. |
115 bijection between the representing set $A$ and the new type $t$. |
114 |
116 |
115 Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term |
117 Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term |
116 constant) of the same name. The injection from type to set is called |
118 constant) of the same name (an alternative base name may be given in |
117 $Rep_t$, its inverse $Abs_t$. Theorems $Rep_t$, $Rep_inverse$, and |
119 parentheses). The injection from type to set is called $Rep_t$, its inverse |
118 $Abs_inverse$ provide the most basic characterization as a corresponding |
120 $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$ |
119 injection/surjection pair (in both directions). Rules $Rep_t_inject$ and |
121 declaration). |
120 $Abs_t_inject$ provide a slightly more comfortable view on the injectivity |
122 |
121 part; likewise do $Rep_t_cases$, $Rep_t_induct$, and $Abs_t_cases$, |
123 Theorems $Rep_t$, $Rep_inverse$, and $Abs_inverse$ provide the most basic |
122 $Abs_t_induct$ for surjectivity. The latter rules are already declare as |
124 characterization as a corresponding injection/surjection pair (in both |
123 type or set rules for the generic $cases$ and $induct$ methods. |
125 directions). Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly |
|
126 more comfortable view on the injectivity part, suitable for automated proof |
|
127 tools (e.g.\ in $simp$ or $iff$ declarations). Rules $Rep_t_cases$, |
|
128 $Rep_t_induct$, and $Abs_t_cases$, $Abs_t_induct$ provide alternative views |
|
129 on surjectivity; these are already declared as type or set rules for the |
|
130 generic $cases$ and $induct$ methods. |
124 \end{descr} |
131 \end{descr} |
125 |
132 |
126 Raw type declarations are rarely useful in practice. The main application is |
133 Raw type declarations are rarely used in practice; the main application is |
127 with experimental (or even axiomatic!) theory fragments. Instead of primitive |
134 with experimental (or even axiomatic!) theory fragments. Instead of primitive |
128 HOL type definitions, user-level theories usually refer to higher-level |
135 HOL type definitions, user-level theories usually refer to higher-level |
129 packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or |
136 packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or |
130 $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}). |
137 $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}). |
131 |
138 |