doc-src/TutorialI/Types/document/Typedefs.tex
author wenzelm
Mon, 29 Aug 2005 11:44:23 +0200
changeset 17181 5f42dd5e6570
parent 17175 1eced27ee0e1
child 17187 45bee2f6e61f
permissions -rw-r--r--
updated;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     1
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{Typedefs}%
17181
5f42dd5e6570 updated;
wenzelm
parents: 17175
diff changeset
     4
\isamarkupfalse%
17056
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
     5
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
     6
\isadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
     7
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
     8
\endisadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
     9
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
    10
\isatagtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
    11
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
    12
\endisatagtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
    13
{\isafoldtheory}%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
    14
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
    15
\isadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
    16
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
    17
\endisadelimtheory
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    18
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    19
\isamarkupsection{Introducing New Types%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    20
}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    21
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    22
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    23
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    24
\label{sec:adv-typedef}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    25
For most applications, a combination of predefined types like \isa{bool} and
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    26
\isa{{\isasymRightarrow}} with recursive datatypes and records is quite sufficient. Very
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    27
occasionally you may feel the need for a more advanced type.  If you
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    28
are certain that your type is not definable by any of the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    29
standard means, then read on.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    30
\begin{warn}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    31
  Types in HOL must be non-empty; otherwise the quantifier rules would be
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    32
  unsound, because $\exists x.\ x=x$ is a theorem.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    33
\end{warn}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    34
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    35
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    36
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    37
\isamarkupsubsection{Declaring New Types%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    38
}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    39
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    40
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    41
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    42
\label{sec:typedecl}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    43
\index{types!declaring|(}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    44
\index{typedecl@\isacommand {typedecl} (command)}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    45
The most trivial way of introducing a new type is by a \textbf{type
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    46
declaration}:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    47
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    48
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    49
\isacommand{typedecl}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    50
\ my{\isacharunderscore}new{\isacharunderscore}type%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    51
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    52
\noindent
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    53
This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    54
name. Thus we know nothing about this type, except that it is
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    55
non-empty. Such declarations without definitions are
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    56
useful if that type can be viewed as a parameter of the theory.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    57
A typical example is given in \S\ref{sec:VMC}, where we define a transition
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    58
relation over an arbitrary type of states.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    59
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    60
In principle we can always get rid of such type declarations by making those
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    61
types parameters of every other type, thus keeping the theory generic. In
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    62
practice, however, the resulting clutter can make types hard to read.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    63
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    64
If you are looking for a quick and dirty way of introducing a new type
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    65
together with its properties: declare the type and state its properties as
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    66
axioms. Example:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    67
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    68
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    69
\isacommand{axioms}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    70
\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
    71
just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ {\isasymforall}y{\isachardot}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    72
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    73
\noindent
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    74
However, we strongly discourage this approach, except at explorative stages
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    75
of your development. It is extremely easy to write down contradictory sets of
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    76
axioms, in which case you will be able to prove everything but it will mean
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    77
nothing.  In the example above, the axiomatic approach is
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    78
unnecessary: a one-element type called \isa{unit} is already defined in HOL.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    79
\index{types!declaring|)}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    80
\end{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    81
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    82
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    83
\isamarkupsubsection{Defining New Types%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    84
}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    85
\isamarkuptrue%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    86
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    87
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    88
\label{sec:typedef}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    89
\index{types!defining|(}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    90
\index{typedecl@\isacommand {typedef} (command)|(}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    91
Now we come to the most general means of safely introducing a new type, the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    92
\textbf{type definition}. All other means, for example
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    93
\isacommand{datatype}, are based on it. The principle is extremely simple:
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    94
any non-empty subset of an existing type can be turned into a new type.
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    95
More precisely, the new type is specified to be isomorphic to some
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    96
non-empty subset of an existing type.
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    97
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    98
Let us work a simple example, the definition of a three-element type.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
    99
It is easily represented by the first three natural numbers:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   100
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   101
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   102
\isacommand{typedef}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   103
\ three\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}%
17056
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   104
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   105
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   106
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   107
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   108
\isatagproof
16353
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   109
%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   110
\begin{isamarkuptxt}%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   111
\noindent
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   112
In order to enforce that the representing set on the right-hand side is
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   113
non-empty, this definition actually starts a proof to that effect:
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   114
\begin{isabelle}%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   115
\ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   116
\end{isabelle}
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   117
Fortunately, this is easy enough to show, even \isa{auto} could do it.
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   118
In general, one has to provide a witness, in our case 0:%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   119
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   120
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   121
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   122
{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isadigit{0}}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   123
\isacommand{by}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   124
\ simp%
17056
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   125
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   126
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   127
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   128
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   129
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   130
\endisadelimproof
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   131
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   132
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   133
This type definition introduces the new type \isa{three} and asserts
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   134
that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. This assertion
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   135
is expressed via a bijection between the \emph{type} \isa{three} and the
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   136
\emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. To this end, the command declares the following
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   137
constants behind the scenes:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   138
\begin{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   139
\begin{tabular}{rcl}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   140
\isa{three} &::& \isa{nat\ set} \\
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   141
\isa{Rep{\isacharunderscore}three} &::& \isa{three\ {\isasymRightarrow}\ nat}\\
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   142
\isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   143
\end{tabular}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   144
\end{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   145
where constant \isa{three} is explicitly defined as the representing set:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   146
\begin{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   147
\isa{three\ {\isasymequiv}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def})
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   148
\end{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   149
The situation is best summarized with the help of the following diagram,
12543
3e355f0f079f New type definition diagram
paulson
parents: 12473
diff changeset
   150
where squares denote types and the irregular region denotes a set:
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   151
\begin{center}
12627
08eee994bf99 updated;
wenzelm
parents: 12543
diff changeset
   152
\includegraphics[scale=.8]{typedef}
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   153
\end{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   154
Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   155
surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   156
\begin{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   157
\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   158
\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} & (\isa{Rep{\isacharunderscore}three}) \\
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   159
\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   160
\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   161
\end{tabular}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   162
\end{center}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   163
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   164
From this example it should be clear what \isacommand{typedef} does
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   165
in general given a name (here \isa{three}) and a set
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   166
(here \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}).
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   167
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   168
Our next step is to define the basic functions expected on the new type.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   169
Although this depends on the type at hand, the following strategy works well:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   170
\begin{itemize}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   171
\item define a small kernel of basic functions that can express all other
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   172
functions you anticipate.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   173
\item define the kernel in terms of corresponding functions on the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   174
representing type using \isa{Abs} and \isa{Rep} to convert between the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   175
two levels.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   176
\end{itemize}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   177
In our example it suffices to give the three elements of type \isa{three}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   178
names:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   179
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   180
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   181
\isacommand{constdefs}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   182
\isanewline
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   183
\ \ A{\isacharcolon}{\isacharcolon}\ three\isanewline
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   184
\ {\isachardoublequoteopen}A\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   185
\ \ B{\isacharcolon}{\isacharcolon}\ three\isanewline
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   186
\ {\isachardoublequoteopen}B\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   187
\ \ C\ {\isacharcolon}{\isacharcolon}\ three\isanewline
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   188
\ {\isachardoublequoteopen}C\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{2}}{\isachardoublequoteclose}%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   189
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   190
So far, everything was easy. But it is clear that reasoning about \isa{three} will be hell if we have to go back to \isa{nat} every time. Thus our
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   191
aim must be to raise our level of abstraction by deriving enough theorems
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   192
about type \isa{three} to characterize it completely. And those theorems
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   193
should be phrased in terms of \isa{A}, \isa{B} and \isa{C}, not \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three}. Because of the simplicity of the example,
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   194
we merely need to prove that \isa{A}, \isa{B} and \isa{C} are distinct
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   195
and that they exhaust the type.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   196
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   197
In processing our \isacommand{typedef} declaration, 
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   198
Isabelle proves several helpful lemmas. The first two
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   199
express injectivity of \isa{Rep{\isacharunderscore}three} and \isa{Abs{\isacharunderscore}three}:
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   200
\begin{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   201
\begin{tabular}{@ {}r@ {\qquad}l@ {}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   202
\isa{{\isacharparenleft}Rep{\isacharunderscore}three\ x\ {\isacharequal}\ Rep{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inject}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   203
\begin{tabular}{@ {}l@ {}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   204
\isa{{\isasymlbrakk}x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three\ {\isasymrbrakk}} \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   205
\isa{{\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   206
\end{tabular} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inject}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   207
\end{tabular}
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   208
\end{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   209
The following ones allow to replace some \isa{x{\isacharcolon}{\isacharcolon}three} by
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   210
\isa{Abs{\isacharunderscore}three{\isacharparenleft}y{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}, and conversely \isa{y} by \isa{Rep{\isacharunderscore}three\ x}:
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   211
\begin{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   212
\begin{tabular}{@ {}r@ {\qquad}l@ {}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   213
\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ y\ {\isacharequal}\ Rep{\isacharunderscore}three\ x\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}cases}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   214
\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}cases}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   215
\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}induct}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   216
\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}induct}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   217
\end{tabular}
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   218
\end{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   219
These theorems are proved for any type definition, with \isa{three}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   220
replaced by the name of the type in question.
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   221
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   222
Distinctness of \isa{A}, \isa{B} and \isa{C} follows immediately
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   223
if we expand their definitions and rewrite with the injectivity
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   224
of \isa{Abs{\isacharunderscore}three}:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   225
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   226
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   227
\isacommand{lemma}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   228
\ {\isachardoublequoteopen}A\ {\isasymnoteq}\ B\ {\isasymand}\ B\ {\isasymnoteq}\ A\ {\isasymand}\ A\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ A\ {\isasymand}\ B\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ B{\isachardoublequoteclose}\isanewline
17056
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   229
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   230
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   231
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   232
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   233
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   234
\isatagproof
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   235
\isacommand{by}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   236
{\isacharparenleft}simp\ add{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}inject\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ three{\isacharunderscore}def{\isacharparenright}%
17056
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   237
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   238
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   239
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   240
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   241
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   242
\endisadelimproof
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   243
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   244
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   245
\noindent
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   246
Of course we rely on the simplifier to solve goals like \isa{{\isadigit{0}}\ {\isasymnoteq}\ {\isadigit{1}}}.
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   247
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   248
The fact that \isa{A}, \isa{B} and \isa{C} exhaust type \isa{three} is
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   249
best phrased as a case distinction theorem: if you want to prove \isa{P\ x}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   250
(where \isa{x} is of type \isa{three}) it suffices to prove \isa{P\ A},
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   251
\isa{P\ B} and \isa{P\ C}:%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   252
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   253
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   254
\isacommand{lemma}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   255
\ three{\isacharunderscore}cases{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x{\isachardoublequoteclose}%
17056
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   256
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   257
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   258
\endisadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   259
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   260
\isatagproof
16353
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   261
%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   262
\begin{isamarkuptxt}%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   263
\noindent Again this follows easily from a pre-proved general theorem:%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   264
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   265
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   266
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   267
{\isacharparenleft}induct{\isacharunderscore}tac\ x\ rule{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}%
16353
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   268
\begin{isamarkuptxt}%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   269
\begin{isabelle}%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   270
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}y{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   271
\end{isabelle}
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   272
Simplification with \isa{three{\isacharunderscore}def} leads to the disjunction \isa{y\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{2}}} which \isa{auto} separates into three
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   273
subgoals, each of which is easily solved by simplification:%
94e565ded526 updated;
wenzelm
parents: 15481
diff changeset
   274
\end{isamarkuptxt}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   275
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   276
\isacommand{apply}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   277
{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def{\isacharparenright}\isanewline
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   278
\isacommand{done}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   279
%
17056
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   280
\endisatagproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   281
{\isafoldproof}%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   282
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   283
\isadelimproof
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   284
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   285
\endisadelimproof
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   286
%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   287
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   288
\noindent
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   289
This concludes the derivation of the characteristic theorems for
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   290
type \isa{three}.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   291
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   292
The attentive reader has realized long ago that the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   293
above lengthy definition can be collapsed into one line:%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   294
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   295
\isamarkuptrue%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   296
\isacommand{datatype}\isamarkupfalse%
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   297
\ better{\isacharunderscore}three\ {\isacharequal}\ A\ {\isacharbar}\ B\ {\isacharbar}\ C%
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   298
\begin{isamarkuptext}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   299
\noindent
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   300
In fact, the \isacommand{datatype} command performs internally more or less
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   301
the same derivations as we did, which gives you some idea what life would be
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   302
like without \isacommand{datatype}.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   303
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   304
Although \isa{three} could be defined in one line, we have chosen this
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   305
example to demonstrate \isacommand{typedef} because its simplicity makes the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   306
key concepts particularly easy to grasp. If you would like to see a
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   307
non-trivial example that cannot be defined more directly, we recommend the
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   308
definition of \emph{finite multisets} in the Library~\cite{HOL-Library}.
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   309
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   310
Let us conclude by summarizing the above procedure for defining a new type.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   311
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   312
set of functions $F$, this involves three steps:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   313
\begin{enumerate}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   314
\item Find an appropriate type $\tau$ and subset $A$ which has the desired
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   315
  properties $P$, and make a type definition based on this representation.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   316
\item Define the required functions $F$ on $ty$ by lifting
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   317
analogous functions on the representation via $Abs_ty$ and $Rep_ty$.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   318
\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   319
\end{enumerate}
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   320
You can now forget about the representation and work solely in terms of the
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   321
abstract functions $F$ and properties $P$.%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   322
\index{typedecl@\isacommand {typedef} (command)|)}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   323
\index{types!defining|)}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   324
\end{isamarkuptext}%
17175
1eced27ee0e1 updated;
wenzelm
parents: 17056
diff changeset
   325
\isamarkuptrue%
17056
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   326
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   327
\isadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   328
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   329
\endisadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   330
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   331
\isatagtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   332
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   333
\endisatagtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   334
{\isafoldtheory}%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   335
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   336
\isadelimtheory
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   337
%
05fc32a23b8b updated;
wenzelm
parents: 16353
diff changeset
   338
\endisadelimtheory
11898
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   339
\end{isabellebody}%
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   340
%%% Local Variables:
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   341
%%% mode: latex
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   342
%%% TeX-master: "root"
0844573f4518 *** empty log message ***
wenzelm
parents:
diff changeset
   343
%%% End: