--- a/doc-src/TutorialI/Advanced/Partial.thy Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy Fri Nov 30 17:55:13 2001 +0100
@@ -62,9 +62,9 @@
*}
consts divi :: "nat \<times> nat \<Rightarrow> nat"
-recdef (permissive) divi "measure(\<lambda>(m,n). m)"
- "divi(m,n) = (if n = 0 then arbitrary else
- if m < n then 0 else divi(m-n,n)+1)" (* FIXME hide permissive!? *)
+recdef divi "measure(\<lambda>(m,n). m)"
+ "divi(m,0) = arbitrary"
+ "divi(m,n) = (if m < n then 0 else divi(m-n,n)+1)"
text{*\noindent Of course we could also have defined
@{term"divi(m,0)"} to be some specific number, for example 0. The
@@ -75,12 +75,12 @@
As a more substantial example we consider the problem of searching a graph.
For simplicity our graph is given by a function @{term f} of
type @{typ"'a \<Rightarrow> 'a"} which
-maps each node to its successor; the graph is really a tree.
+maps each node to its successor; the graph has out-degree 1.
The task is to find the end of a chain, modelled by a node pointing to
itself. Here is a first attempt:
@{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}
-This may be viewed as a fixed point finder or as one half of the well known
-\emph{Union-Find} algorithm.
+This may be viewed as a fixed point finder or as the second half of the well
+known \emph{Union-Find} algorithm.
The snag is that it may not terminate if @{term f} has non-trivial cycles.
Phrased differently, the relation
*}
--- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Fri Nov 30 17:55:13 2001 +0100
@@ -74,9 +74,9 @@
\isamarkuptrue%
\isacommand{consts}\ divi\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{recdef}\ {\isacharparenleft}\isakeyword{permissive}{\isacharparenright}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ arbitrary\ else\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isacommand{recdef}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ arbitrary{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Of course we could also have defined
@@ -88,14 +88,14 @@
As a more substantial example we consider the problem of searching a graph.
For simplicity our graph is given by a function \isa{f} of
type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which
-maps each node to its successor; the graph is really a tree.
+maps each node to its successor; the graph has out-degree 1.
The task is to find the end of a chain, modelled by a node pointing to
itself. Here is a first attempt:
\begin{isabelle}%
\ \ \ \ \ find\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find\ {\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}%
\end{isabelle}
-This may be viewed as a fixed point finder or as one half of the well known
-\emph{Union-Find} algorithm.
+This may be viewed as a fixed point finder or as the second half of the well
+known \emph{Union-Find} algorithm.
The snag is that it may not terminate if \isa{f} has non-trivial cycles.
Phrased differently, the relation%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/CTL/CTL.thy Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Fri Nov 30 17:55:13 2001 +0100
@@ -455,17 +455,16 @@
done
*)
(*>*)
-text{*
-Let us close this section with a few words about the executability of our model checkers.
-It is clear that if all sets are finite, they can be represented as lists and the usual
-set operations are easily implemented. Only @{term lfp} requires a little thought.
-Fortunately, the
-Library\footnote{See theory \isa{While_Combinator}.}~\cite{isabelle-HOL-lib}
-provides a theorem stating that
-in the case of finite sets and a monotone function~@{term F},
-the value of \mbox{@{term"lfp F"}} can be computed by iterated application of @{term F} to~@{term"{}"} until
-a fixed point is reached. It is actually possible to generate executable functional programs
+
+text{* Let us close this section with a few words about the executability of
+our model checkers. It is clear that if all sets are finite, they can be
+represented as lists and the usual set operations are easily
+implemented. Only @{term lfp} requires a little thought. Fortunately, theory
+@{text While_Combinator} in the Library~\cite{isabelle-HOL-lib} provides a
+theorem stating that in the case of finite sets and a monotone
+function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by
+iterated application of @{term F} to~@{term"{}"} until a fixed point is
+reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.%
-\index{CTL|)}
-*}
+\index{CTL|)} *}
(*<*)end(*>*)
--- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Nov 30 17:55:13 2001 +0100
@@ -465,15 +465,15 @@
\isamarkupfalse%
%
\begin{isamarkuptext}%
-Let us close this section with a few words about the executability of our model checkers.
-It is clear that if all sets are finite, they can be represented as lists and the usual
-set operations are easily implemented. Only \isa{lfp} requires a little thought.
-Fortunately, the
-Library\footnote{See theory \isa{While_Combinator}.}~\cite{isabelle-HOL-lib}
-provides a theorem stating that
-in the case of finite sets and a monotone function~\isa{F},
-the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
-a fixed point is reached. It is actually possible to generate executable functional programs
+Let us close this section with a few words about the executability of
+our model checkers. It is clear that if all sets are finite, they can be
+represented as lists and the usual set operations are easily
+implemented. Only \isa{lfp} requires a little thought. Fortunately, theory
+\isa{While{\isacharunderscore}Combinator} in the Library~\cite{isabelle-HOL-lib} provides a
+theorem stating that in the case of finite sets and a monotone
+function~\isa{F}, the value of \mbox{\isa{lfp\ F}} can be computed by
+iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is
+reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.%
\index{CTL|)}%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Datatype/ABexpr.thy Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy Fri Nov 30 17:55:13 2001 +0100
@@ -123,9 +123,50 @@
Prove that @{text"norma"}
preserves the value of an expression and that the result of @{text"norma"}
is really normal, i.e.\ no more @{term"And"}s and @{term"Neg"}s occur in
- it. ({\em Hint:} proceed as in \S\ref{sec:boolex}).
+ it. ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion
+ of type annotations following lemma @{text subst_id} below).
\end{exercise}
*}
-(*<*)
+(*<*)
+consts norma :: "'a aexp \<Rightarrow> 'a aexp"
+ normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp"
+
+primrec
+"norma (IF b t e) = (normb b (norma t) (norma e))"
+"norma (Sum a1 a2) = Sum (norma a1) (norma a2)"
+"norma (Diff a1 a2) = Diff (norma a1) (norma a2)"
+"norma (Var v) = Var v"
+"norma (Num n) = Num n"
+
+"normb (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e"
+"normb (And b1 b2) t e = normb b1 (normb b2 t e) e"
+"normb (Neg b) t e = normb b e t"
+
+lemma " evala (norma a) env = evala a env
+ \<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)"
+apply (induct_tac a and b)
+apply (simp_all)
+done
+
+consts normala :: "'a aexp \<Rightarrow> bool"
+ normalb :: "'b bexp \<Rightarrow> bool"
+
+primrec
+"normala (IF b t e) = (normalb b \<and> normala t \<and> normala e)"
+"normala (Sum a1 a2) = (normala a1 \<and> normala a2)"
+"normala (Diff a1 a2) = (normala a1 \<and> normala a2)"
+"normala (Var v) = True"
+"normala (Num n) = True"
+
+"normalb (Less a1 a2) = (normala a1 \<and> normala a2)"
+"normalb (And b1 b2) = False"
+"normalb (Neg b) = False"
+
+lemma "normala (norma (a::'a aexp)) \<and>
+ (\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))"
+apply (induct_tac a and b)
+apply (auto)
+done
+
end
(*>*)
--- a/doc-src/TutorialI/Datatype/Nested.thy Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Nov 30 17:55:13 2001 +0100
@@ -66,8 +66,8 @@
strengthened and proved as follows:
*}
-lemma "subst Var t = (t ::('v,'f)term) \<and>
- substs Var ts = (ts::('v,'f)term list)";
+lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst Var t = (t ::('v,'f)term) \<and>
+ substs Var ts = (ts::('v,'f)term list)";
apply(induct_tac t and ts, simp_all);
done
@@ -102,6 +102,34 @@
insists on the conjunctive format. Fortunately, we can easily \emph{prove}
that the suggested equation holds:
*}
+(*<*)
+(* Exercise 1: *)
+lemma "subst ((subst f) \<circ> g) t = subst f (subst g t) \<and>
+ substs ((subst f) \<circ> g) ts = substs f (substs g ts)"
+apply (induct_tac t and ts)
+apply (simp_all)
+done
+
+(* Exercise 2: *)
+
+consts trev :: "('v,'f) term \<Rightarrow> ('v,'f) term"
+ trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list"
+primrec
+"trev (Var v) = Var v"
+"trev (App f ts) = App f (trevs ts)"
+
+"trevs [] = []"
+"trevs (t#ts) = (trevs ts) @ [(trev t)]"
+
+lemma [simp]: "\<forall> ys. trevs (xs @ ys) = (trevs ys) @ (trevs xs)"
+apply (induct_tac xs, auto)
+done
+
+lemma "trev (trev t) = (t::('v,'f)term) \<and>
+ trevs (trevs ts) = (ts::('v,'f)term list)"
+apply (induct_tac t and ts, simp_all)
+done
+(*>*)
lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
apply(induct_tac ts, simp_all)
@@ -130,6 +158,4 @@
constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.
*}
-(*<*)
-end
-(*>*)
+(*<*)end(*>*)
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri Nov 30 17:55:13 2001 +0100
@@ -130,11 +130,24 @@
Prove that \isa{norma}
preserves the value of an expression and that the result of \isa{norma}
is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in
- it. ({\em Hint:} proceed as in \S\ref{sec:boolex}).
+ it. ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion
+ of type annotations following lemma \isa{subst{\isacharunderscore}id} below).
\end{exercise}%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Fri Nov 30 17:55:13 2001 +0100
@@ -70,8 +70,8 @@
strengthened and proved as follows:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
-\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ subst{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\isamarkupfalse%
@@ -114,6 +114,19 @@
that the suggested equation holds:%
\end{isamarkuptext}%
\isamarkuptrue%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isamarkupfalse%
+\isanewline
+\isamarkupfalse%
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
--- a/doc-src/TutorialI/Types/Overloading2.thy Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy Fri Nov 30 17:55:13 2001 +0100
@@ -19,8 +19,8 @@
\begin{warn}
A type constructor can be instantiated in only one way to
-a given type class. For example, our two instantiations of \isa{list} must
-reside in separate theories with disjoint scopes.\REMARK{Tobias, please check}
+a given type class. For example, our two instantiations of @{text list} must
+reside in separate theories with disjoint scopes.
\end{warn}
*}
--- a/doc-src/TutorialI/Types/Typedefs.thy Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Types/Typedefs.thy Fri Nov 30 17:55:13 2001 +0100
@@ -61,13 +61,9 @@
Now we come to the most general means of safely introducing a new type, the
\textbf{type definition}. All other means, for example
\isacommand{datatype}, are based on it. The principle is extremely simple:
-any non-empty subset of an existing type can be turned into a new type. Thus
-a type definition is merely a notational device: you introduce a new name for
-a subset of an existing type. This does not add any logical power to HOL,
-because you could base all your work directly on the subset of the existing
-type. However, the resulting theories could easily become indigestible
-because instead of implicit types you would have explicit sets in your
-formulae.
+any non-empty subset of an existing type can be turned into a new type.
+More precisely, the new type is specified to be isomorphic to some
+non-empty subset of an existing type.
Let us work a simple example, the definition of a three-element type.
It is easily represented by the first three natural numbers:
@@ -87,9 +83,9 @@
text{*
This type definition introduces the new type @{typ three} and asserts
-that it is a copy of the set @{term"{0,1,2}"}. This assertion
+that it is a copy of the set @{term"{0::nat,1,2}"}. This assertion
is expressed via a bijection between the \emph{type} @{typ three} and the
-\emph{set} @{term"{0,1,2}"}. To this end, the command declares the following
+\emph{set} @{term"{0::nat,1,2}"}. To this end, the command declares the following
constants behind the scenes:
\begin{center}
\begin{tabular}{rcl}
@@ -131,7 +127,7 @@
%
From this example it should be clear what \isacommand{typedef} does
in general given a name (here @{text three}) and a set
-(here @{term"{n. n\<le>2}"}).
+(here @{term"{n::nat. n\<le>2}"}).
Our next step is to define the basic functions expected on the new type.
Although this depends on the type at hand, the following strategy works well:
@@ -246,7 +242,7 @@
above lengthy definition can be collapsed into one line:
*}
-datatype three' = A | B | C
+datatype better_three = A | B | C
text{*\noindent
In fact, the \isacommand{datatype} command performs internally more or less
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Fri Nov 30 17:55:13 2001 +0100
@@ -26,7 +26,7 @@
\begin{warn}
A type constructor can be instantiated in only one way to
a given type class. For example, our two instantiations of \isa{list} must
-reside in separate theories with disjoint scopes.\REMARK{Tobias, please check}
+reside in separate theories with disjoint scopes.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/Types/document/Typedefs.tex Fri Nov 30 12:18:14 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex Fri Nov 30 17:55:13 2001 +0100
@@ -78,13 +78,9 @@
Now we come to the most general means of safely introducing a new type, the
\textbf{type definition}. All other means, for example
\isacommand{datatype}, are based on it. The principle is extremely simple:
-any non-empty subset of an existing type can be turned into a new type. Thus
-a type definition is merely a notational device: you introduce a new name for
-a subset of an existing type. This does not add any logical power to HOL,
-because you could base all your work directly on the subset of the existing
-type. However, the resulting theories could easily become indigestible
-because instead of implicit types you would have explicit sets in your
-formulae.
+any non-empty subset of an existing type can be turned into a new type.
+More precisely, the new type is specified to be isomorphic to some
+non-empty subset of an existing type.
Let us work a simple example, the definition of a three-element type.
It is easily represented by the first three natural numbers:%
@@ -108,9 +104,9 @@
%
\begin{isamarkuptext}%
This type definition introduces the new type \isa{three} and asserts
-that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharbraceright}}. This assertion
+that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. This assertion
is expressed via a bijection between the \emph{type} \isa{three} and the
-\emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharcomma}\ {\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharbraceright}}. To this end, the command declares the following
+\emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. To this end, the command declares the following
constants behind the scenes:
\begin{center}
\begin{tabular}{rcl}
@@ -151,7 +147,7 @@
%
From this example it should be clear what \isacommand{typedef} does
in general given a name (here \isa{three}) and a set
-(here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharbraceright}}).
+(here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}).
Our next step is to define the basic functions expected on the new type.
Although this depends on the type at hand, the following strategy works well:
@@ -281,7 +277,7 @@
above lengthy definition can be collapsed into one line:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{datatype}\ three{\isacharprime}\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isamarkupfalse%
+\isacommand{datatype}\ better{\isacharunderscore}three\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent