1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat May 21 11:31:59 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 25 22:12:46 2011 +0200
1.3 @@ -27,7 +27,26 @@
1.4 \isamarkuptrue%
1.5 %
1.6 \begin{isamarkuptext}%
1.7 -\begin{matharray}{rcl}
1.8 +A Gordon/HOL-style type definition is a certain axiom scheme
1.9 + that identifies a new type with a subset of an existing type. More
1.10 + precisely, the new type is defined by exhibiting an existing type
1.11 + \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, a set \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ set{\isaliteral{22}{\isachardoublequote}}}, and a theorem that proves
1.12 + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequote}}}. Thus \isa{A} is a non-empty subset of \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, and the new type denotes this subset. New functions are
1.13 + postulated that establish an isomorphism between the new type and
1.14 + the subset. In general, the type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} may involve type
1.15 + variables \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} which means that the type definition
1.16 + produces a type constructor \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} depending on
1.17 + those type arguments.
1.18 +
1.19 + The axiomatization can be considered a ``definition'' in the sense
1.20 + of the particular set-theoretic interpretation of HOL
1.21 + \cite{pitts93}, where the universe of types is required to be
1.22 + downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely
1.23 + new types introduced by \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} stay within the range
1.24 + of HOL models by construction. Note that \indexref{}{command}{type\_synonym}\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}} from Isabelle/Pure merely introduces syntactic
1.25 + abbreviations, without any logical significance.
1.26 +
1.27 + \begin{matharray}{rcl}
1.28 \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
1.29 \end{matharray}
1.30
1.31 @@ -36,13 +55,13 @@
1.32 \rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
1.33 \rail@bar
1.34 \rail@nextbar{1}
1.35 -\rail@nont{\isa{altname}}[]
1.36 +\rail@nont{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}[]
1.37 \rail@endbar
1.38 -\rail@nont{\isa{abstype}}[]
1.39 +\rail@nont{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}[]
1.40 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.41 -\rail@nont{\isa{repset}}[]
1.42 +\rail@nont{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}[]
1.43 \rail@end
1.44 -\rail@begin{3}{\isa{altname}}
1.45 +\rail@begin{3}{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}
1.46 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1.47 \rail@bar
1.48 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.49 @@ -54,14 +73,14 @@
1.50 \rail@endbar
1.51 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.52 \rail@end
1.53 -\rail@begin{2}{\isa{abstype}}
1.54 +\rail@begin{2}{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}
1.55 \rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
1.56 \rail@bar
1.57 \rail@nextbar{1}
1.58 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.59 \rail@endbar
1.60 \rail@end
1.61 -\rail@begin{2}{\isa{repset}}
1.62 +\rail@begin{2}{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}
1.63 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.64 \rail@bar
1.65 \rail@nextbar{1}
1.66 @@ -76,40 +95,161 @@
1.67 \begin{description}
1.68
1.69 \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{22}{\isachardoublequote}}}
1.70 - axiomatizes a Gordon/HOL-style type definition in the background
1.71 - theory of the current context, depending on a non-emptiness result
1.72 - of the set \isa{A} (which needs to be proven interactively).
1.73 + axiomatizes a type definition in the background theory of the
1.74 + current context, depending on a non-emptiness result of the set
1.75 + \isa{A} that needs to be proven here. The set \isa{A} may
1.76 + contain type variables \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} as specified on the LHS,
1.77 + but no term variables.
1.78
1.79 - The raw type may not depend on parameters or assumptions of the
1.80 - context --- this is logically impossible in Isabelle/HOL --- but the
1.81 - non-emptiness property can be local, potentially resulting in
1.82 - multiple interpretations in target contexts. Thus the established
1.83 - bijection between the representing set \isa{A} and the new type
1.84 - \isa{t} may semantically depend on local assumptions.
1.85 + Even though a local theory specification, the newly introduced type
1.86 + constructor cannot depend on parameters or assumptions of the
1.87 + context: this is structurally impossible in HOL. In contrast, the
1.88 + non-emptiness proof may use local assumptions in unusual situations,
1.89 + which could result in different interpretations in target contexts:
1.90 + the meaning of the bijection between the representing set \isa{A}
1.91 + and the new type \isa{t} may then change in different application
1.92 + contexts.
1.93
1.94 - By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t}
1.95 - and a set (term constant) of the same name, unless an alternative
1.96 - base name is given in parentheses, or the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}''
1.97 - declaration is used to suppress a separate constant definition
1.98 + By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type
1.99 + constructor \isa{t} for the new type, and a term constant \isa{t} for the representing set within the old type. Use the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option to suppress a separate constant definition
1.100 altogether. The injection from type to set is called \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t},
1.101 - its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t} --- this may be changed via an explicit
1.102 - \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
1.103 + its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t}, unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
1.104
1.105 - Theorems \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t}, \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse} provide the most basic characterization as a
1.106 - corresponding injection/surjection pair (in both directions). Rules
1.107 - \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} provide a slightly
1.108 - more convenient view on the injectivity part, suitable for automated
1.109 - proof tools (e.g.\ in \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}
1.110 - declarations). Rules \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct}, and
1.111 - \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views
1.112 - on surjectivity; these are already declared as set or type rules for
1.113 - the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
1.114 + The core axiomatization uses the locale predicate \isa{type{\isaliteral{5F}{\isacharunderscore}}definition} as defined in Isabelle/HOL. Various basic
1.115 + consequences of that are instantiated accordingly, re-using the
1.116 + locale facts with names derived from the new type constructor. Thus
1.117 + the generic \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep} is turned into the specific
1.118 + \isa{{\isaliteral{22}{\isachardoublequote}}Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{22}{\isachardoublequote}}}, for example.
1.119 +
1.120 + Theorems \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep}, \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}inverse}
1.121 + provide the most basic characterization as a corresponding
1.122 + injection/surjection pair (in both directions). The derived rules
1.123 + \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}inject} provide a more convenient version of
1.124 + injectivity, suitable for automated proof tools (e.g.\ in
1.125 + declarations involving \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}).
1.126 + Furthermore, the rules \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}cases}~/ \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}induct}, and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}cases}~/
1.127 + \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views on
1.128 + surjectivity. These rules are already declared as set or type rules
1.129 + for the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods,
1.130 + respectively.
1.131
1.132 An alternative name for the set definition (and other derived
1.133 entities) may be specified in parentheses; the default is to use
1.134 - \isa{t} as indicated before.
1.135 + \isa{t} directly.
1.136
1.137 - \end{description}%
1.138 + \end{description}
1.139 +
1.140 + \begin{warn}
1.141 + If you introduce a new type axiomatically, i.e.\ via \indexref{}{command}{typedecl}\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} and \indexref{}{command}{axiomatization}\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}, the minimum requirement
1.142 + is that it has a non-empty model, to avoid immediate collapse of the
1.143 + HOL logic. Moreover, one needs to demonstrate that the
1.144 + interpretation of such free-form axiomatizations can coexist with
1.145 + that of the regular \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}} scheme, and any extension
1.146 + that other people might have introduced elsewhere (e.g.\ in HOLCF
1.147 + \cite{MuellerNvOS99}).
1.148 + \end{warn}%
1.149 +\end{isamarkuptext}%
1.150 +\isamarkuptrue%
1.151 +%
1.152 +\isamarkupsubsubsection{Examples%
1.153 +}
1.154 +\isamarkuptrue%
1.155 +%
1.156 +\begin{isamarkuptext}%
1.157 +Type definitions permit the introduction of abstract data
1.158 + types in a safe way, namely by providing models based on already
1.159 + existing types. Given some abstract axiomatic description \isa{P}
1.160 + of a type, this involves two steps:
1.161 +
1.162 + \begin{enumerate}
1.163 +
1.164 + \item Find an appropriate type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} and subset \isa{A} which
1.165 + has the desired properties \isa{P}, and make a type definition
1.166 + based on this representation.
1.167 +
1.168 + \item Prove that \isa{P} holds for \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} by lifting \isa{P}
1.169 + from the representation.
1.170 +
1.171 + \end{enumerate}
1.172 +
1.173 + You can later forget about the representation and work solely in
1.174 + terms of the abstract properties \isa{P}.
1.175 +
1.176 + \medskip The following trivial example pulls a three-element type
1.177 + into existence within the formal logical environment of HOL.%
1.178 +\end{isamarkuptext}%
1.179 +\isamarkuptrue%
1.180 +\isacommand{typedef}\isamarkupfalse%
1.181 +\ three\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}False{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.182 +%
1.183 +\isadelimproof
1.184 +\ \ %
1.185 +\endisadelimproof
1.186 +%
1.187 +\isatagproof
1.188 +\isacommand{by}\isamarkupfalse%
1.189 +\ blast%
1.190 +\endisatagproof
1.191 +{\isafoldproof}%
1.192 +%
1.193 +\isadelimproof
1.194 +\isanewline
1.195 +%
1.196 +\endisadelimproof
1.197 +\isanewline
1.198 +\isacommand{definition}\isamarkupfalse%
1.199 +\ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.200 +\isacommand{definition}\isamarkupfalse%
1.201 +\ {\isaliteral{22}{\isachardoublequoteopen}}Two\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.202 +\isacommand{definition}\isamarkupfalse%
1.203 +\ {\isaliteral{22}{\isachardoublequoteopen}}Three\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}False{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.204 +\isanewline
1.205 +\isacommand{lemma}\isamarkupfalse%
1.206 +\ three{\isaliteral{5F}{\isacharunderscore}}distinct{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Two{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}Two\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.207 +%
1.208 +\isadelimproof
1.209 +\ \ %
1.210 +\endisadelimproof
1.211 +%
1.212 +\isatagproof
1.213 +\isacommand{by}\isamarkupfalse%
1.214 +\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ One{\isaliteral{5F}{\isacharunderscore}}def\ Two{\isaliteral{5F}{\isacharunderscore}}def\ Three{\isaliteral{5F}{\isacharunderscore}}def\ Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject\ three{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
1.215 +\endisatagproof
1.216 +{\isafoldproof}%
1.217 +%
1.218 +\isadelimproof
1.219 +\isanewline
1.220 +%
1.221 +\endisadelimproof
1.222 +\isanewline
1.223 +\isacommand{lemma}\isamarkupfalse%
1.224 +\ three{\isaliteral{5F}{\isacharunderscore}}cases{\isaliteral{3A}{\isacharcolon}}\isanewline
1.225 +\ \ \isakeyword{fixes}\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ three\ \isakeyword{obtains}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ One{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Two{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.226 +%
1.227 +\isadelimproof
1.228 +\ \ %
1.229 +\endisadelimproof
1.230 +%
1.231 +\isatagproof
1.232 +\isacommand{by}\isamarkupfalse%
1.233 +\ {\isaliteral{28}{\isacharparenleft}}cases\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}auto\ simp{\isaliteral{3A}{\isacharcolon}}\ One{\isaliteral{5F}{\isacharunderscore}}def\ Two{\isaliteral{5F}{\isacharunderscore}}def\ Three{\isaliteral{5F}{\isacharunderscore}}def\ Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject\ three{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
1.234 +\endisatagproof
1.235 +{\isafoldproof}%
1.236 +%
1.237 +\isadelimproof
1.238 +%
1.239 +\endisadelimproof
1.240 +%
1.241 +\begin{isamarkuptext}%
1.242 +Note that such trivial constructions are better done with
1.243 + derived specification mechanisms such as \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}:%
1.244 +\end{isamarkuptext}%
1.245 +\isamarkuptrue%
1.246 +\isacommand{datatype}\isamarkupfalse%
1.247 +\ three{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ One{\isaliteral{27}{\isacharprime}}\ {\isaliteral{7C}{\isacharbar}}\ Two{\isaliteral{27}{\isacharprime}}\ {\isaliteral{7C}{\isacharbar}}\ Three{\isaliteral{27}{\isacharprime}}%
1.248 +\begin{isamarkuptext}%
1.249 +This avoids re-doing basic definitions and proofs from the
1.250 + primitive \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} above.%
1.251 \end{isamarkuptext}%
1.252 \isamarkuptrue%
1.253 %