src/Doc/Tutorial/Types/Typedefs.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 49834 b27bbb021df1
child 58620 7435b6a3f72e
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17914
99ead7a7eb42 fix headers;
wenzelm
parents: 12815
diff changeset
     1
(*<*)theory Typedefs imports Main begin(*>*)
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
     2
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
     3
section{*Introducing New Types*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
     4
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
     5
text{*\label{sec:adv-typedef}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
     6
For most applications, a combination of predefined types like @{typ bool} and
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
     7
@{text"\<Rightarrow>"} with recursive datatypes and records is quite sufficient. Very
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
     8
occasionally you may feel the need for a more advanced type.  If you
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
     9
are certain that your type is not definable by any of the
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    10
standard means, then read on.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    11
\begin{warn}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    12
  Types in HOL must be non-empty; otherwise the quantifier rules would be
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    13
  unsound, because $\exists x.\ x=x$ is a theorem.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    14
\end{warn}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    15
*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    16
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    17
subsection{*Declaring New Types*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    18
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    19
text{*\label{sec:typedecl}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    20
\index{types!declaring|(}%
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    21
\index{typedecl@\isacommand {typedecl} (command)}%
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    22
The most trivial way of introducing a new type is by a \textbf{type
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    23
declaration}: *}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    24
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    25
typedecl my_new_type
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    26
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    27
text{*\noindent
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    28
This does not define @{typ my_new_type} at all but merely introduces its
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    29
name. Thus we know nothing about this type, except that it is
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    30
non-empty. Such declarations without definitions are
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    31
useful if that type can be viewed as a parameter of the theory.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    32
A typical example is given in \S\ref{sec:VMC}, where we define a transition
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    33
relation over an arbitrary type of states.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    34
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    35
In principle we can always get rid of such type declarations by making those
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    36
types parameters of every other type, thus keeping the theory generic. In
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    37
practice, however, the resulting clutter can make types hard to read.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    38
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    39
If you are looking for a quick and dirty way of introducing a new type
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    40
together with its properties: declare the type and state its properties as
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    41
axioms. Example:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    42
*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    43
48994
c84278efa9d5 modernized specifications;
wenzelm
parents: 48985
diff changeset
    44
axiomatization where
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    45
just_one: "\<exists>x::my_new_type. \<forall>y. x = y"
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    46
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    47
text{*\noindent
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    48
However, we strongly discourage this approach, except at explorative stages
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    49
of your development. It is extremely easy to write down contradictory sets of
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    50
axioms, in which case you will be able to prove everything but it will mean
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    51
nothing.  In the example above, the axiomatic approach is
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    52
unnecessary: a one-element type called @{typ unit} is already defined in HOL.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    53
\index{types!declaring|)}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    54
*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    55
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    56
subsection{*Defining New Types*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    57
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    58
text{*\label{sec:typedef}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    59
\index{types!defining|(}%
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    60
\index{typedecl@\isacommand {typedef} (command)|(}%
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    61
Now we come to the most general means of safely introducing a new type, the
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    62
\textbf{type definition}. All other means, for example
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    63
\isacommand{datatype}, are based on it. The principle is extremely simple:
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    64
any non-empty subset of an existing type can be turned into a new type.
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    65
More precisely, the new type is specified to be isomorphic to some
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    66
non-empty subset of an existing type.
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    67
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    68
Let us work a simple example, the definition of a three-element type.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    69
It is easily represented by the first three natural numbers:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    70
*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    71
49834
b27bbb021df1 discontinued obsolete typedef (open) syntax;
wenzelm
parents: 49812
diff changeset
    72
typedef three = "{0::nat, 1, 2}"
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    73
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    74
txt{*\noindent
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    75
In order to enforce that the representing set on the right-hand side is
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    76
non-empty, this definition actually starts a proof to that effect:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    77
@{subgoals[display,indent=0]}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
    78
Fortunately, this is easy enough to show, even \isa{auto} could do it.
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
    79
In general, one has to provide a witness, in our case 0:
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    80
*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    81
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    82
apply(rule_tac x = 0 in exI)
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    83
by simp
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    84
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    85
text{*
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    86
This type definition introduces the new type @{typ three} and asserts
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    87
that it is a copy of the set @{term"{0::nat,1,2}"}. This assertion
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    88
is expressed via a bijection between the \emph{type} @{typ three} and the
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
    89
\emph{set} @{term"{0::nat,1,2}"}. To this end, the command declares the following
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    90
constants behind the scenes:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    91
\begin{center}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    92
\begin{tabular}{rcl}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    93
@{term Rep_three} &::& @{typ"three \<Rightarrow> nat"}\\
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    94
@{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    95
\end{tabular}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    96
\end{center}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    97
The situation is best summarized with the help of the following diagram,
12543
3e355f0f079f New type definition diagram
paulson
parents: 12473
diff changeset
    98
where squares denote types and the irregular region denotes a set:
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
    99
\begin{center}
12628
6a07c3bf4903 include typedef image without path prefix!
wenzelm
parents: 12543
diff changeset
   100
\includegraphics[scale=.8]{typedef}
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   101
\end{center}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   102
Finally, \isacommand{typedef} asserts that @{term Rep_three} is
49812
e3945ddcb9aa eliminated some remaining uses of typedef with implicit set definition;
wenzelm
parents: 48994
diff changeset
   103
surjective on the subset and @{term Abs_three} and @{term
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   104
Rep_three} are inverses of each other:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   105
\begin{center}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   106
\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   107
@{thm Rep_three[no_vars]} & (@{thm[source]Rep_three}) \\
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   108
@{thm Rep_three_inverse[no_vars]} & (@{thm[source]Rep_three_inverse}) \\
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   109
@{thm Abs_three_inverse[no_vars]} & (@{thm[source]Abs_three_inverse})
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   110
\end{tabular}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   111
\end{center}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   112
%
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   113
From this example it should be clear what \isacommand{typedef} does
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   114
in general given a name (here @{text three}) and a set
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   115
(here @{term"{0::nat,1,2}"}).
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   116
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   117
Our next step is to define the basic functions expected on the new type.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   118
Although this depends on the type at hand, the following strategy works well:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   119
\begin{itemize}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   120
\item define a small kernel of basic functions that can express all other
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   121
functions you anticipate.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   122
\item define the kernel in terms of corresponding functions on the
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   123
representing type using @{term Abs} and @{term Rep} to convert between the
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   124
two levels.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   125
\end{itemize}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   126
In our example it suffices to give the three elements of type @{typ three}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   127
names:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   128
*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   129
27027
63f0b638355c *** empty log message ***
nipkow
parents: 17914
diff changeset
   130
definition A :: three where "A \<equiv> Abs_three 0"
63f0b638355c *** empty log message ***
nipkow
parents: 17914
diff changeset
   131
definition B :: three where "B \<equiv> Abs_three 1"
63f0b638355c *** empty log message ***
nipkow
parents: 17914
diff changeset
   132
definition C :: three where "C \<equiv> Abs_three 2"
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   133
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   134
text{*
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   135
So far, everything was easy. But it is clear that reasoning about @{typ
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   136
three} will be hell if we have to go back to @{typ nat} every time. Thus our
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   137
aim must be to raise our level of abstraction by deriving enough theorems
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   138
about type @{typ three} to characterize it completely. And those theorems
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   139
should be phrased in terms of @{term A}, @{term B} and @{term C}, not @{term
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   140
Abs_three} and @{term Rep_three}. Because of the simplicity of the example,
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   141
we merely need to prove that @{term A}, @{term B} and @{term C} are distinct
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   142
and that they exhaust the type.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   143
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   144
In processing our \isacommand{typedef} declaration, 
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   145
Isabelle proves several helpful lemmas. The first two
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   146
express injectivity of @{term Rep_three} and @{term Abs_three}:
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   147
\begin{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   148
\begin{tabular}{@ {}r@ {\qquad}l@ {}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   149
@{thm Rep_three_inject[no_vars]} & (@{thm[source]Rep_three_inject}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   150
\begin{tabular}{@ {}l@ {}}
49812
e3945ddcb9aa eliminated some remaining uses of typedef with implicit set definition;
wenzelm
parents: 48994
diff changeset
   151
@{text"\<lbrakk>x \<in> {0, 1, 2}; y \<in> {0, 1, 2} \<rbrakk>"} \\
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   152
@{text"\<Longrightarrow> (Abs_three x = Abs_three y) = (x = y)"}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   153
\end{tabular} & (@{thm[source]Abs_three_inject}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   154
\end{tabular}
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   155
\end{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   156
The following ones allow to replace some @{text"x::three"} by
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   157
@{text"Abs_three(y::nat)"}, and conversely @{term y} by @{term"Rep_three x"}:
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   158
\begin{center}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   159
\begin{tabular}{@ {}r@ {\qquad}l@ {}}
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   160
@{thm Rep_three_cases[no_vars]} & (@{thm[source]Rep_three_cases}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   161
@{thm Abs_three_cases[no_vars]} & (@{thm[source]Abs_three_cases}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   162
@{thm Rep_three_induct[no_vars]} & (@{thm[source]Rep_three_induct}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   163
@{thm Abs_three_induct[no_vars]} & (@{thm[source]Abs_three_induct}) \\
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   164
\end{tabular}
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   165
\end{center}
49812
e3945ddcb9aa eliminated some remaining uses of typedef with implicit set definition;
wenzelm
parents: 48994
diff changeset
   166
These theorems are proved for any type definition, with @{text three}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   167
replaced by the name of the type in question.
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   168
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   169
Distinctness of @{term A}, @{term B} and @{term C} follows immediately
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   170
if we expand their definitions and rewrite with the injectivity
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   171
of @{term Abs_three}:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   172
*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   173
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   174
lemma "A \<noteq> B \<and> B \<noteq> A \<and> A \<noteq> C \<and> C \<noteq> A \<and> B \<noteq> C \<and> C \<noteq> B"
49812
e3945ddcb9aa eliminated some remaining uses of typedef with implicit set definition;
wenzelm
parents: 48994
diff changeset
   175
by(simp add: Abs_three_inject A_def B_def C_def)
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   176
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   177
text{*\noindent
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   178
Of course we rely on the simplifier to solve goals like @{prop"(0::nat) \<noteq> 1"}.
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   179
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   180
The fact that @{term A}, @{term B} and @{term C} exhaust type @{typ three} is
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   181
best phrased as a case distinction theorem: if you want to prove @{prop"P x"}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   182
(where @{term x} is of type @{typ three}) it suffices to prove @{prop"P A"},
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   183
@{prop"P B"} and @{prop"P C"}: *}
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   184
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   185
lemma three_cases: "\<lbrakk> P A; P B; P C \<rbrakk> \<Longrightarrow> P x"
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   186
27318
5cd16e4df9c2 induct_tac: rule is inferred from types;
wenzelm
parents: 27027
diff changeset
   187
txt{*\noindent Again this follows easily using the induction principle stemming from the type definition:*}
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   188
27318
5cd16e4df9c2 induct_tac: rule is inferred from types;
wenzelm
parents: 27027
diff changeset
   189
apply(induct_tac x)
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   190
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   191
txt{*
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   192
@{subgoals[display,indent=0]}
49812
e3945ddcb9aa eliminated some remaining uses of typedef with implicit set definition;
wenzelm
parents: 48994
diff changeset
   193
Simplification leads to the disjunction @{prop"y
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   194
= 0 \<or> y = 1 \<or> y = (2::nat)"} which \isa{auto} separates into three
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   195
subgoals, each of which is easily solved by simplification: *}
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   196
49812
e3945ddcb9aa eliminated some remaining uses of typedef with implicit set definition;
wenzelm
parents: 48994
diff changeset
   197
apply(auto simp add: A_def B_def C_def)
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   198
done
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   199
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   200
text{*\noindent
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   201
This concludes the derivation of the characteristic theorems for
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   202
type @{typ three}.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   203
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   204
The attentive reader has realized long ago that the
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   205
above lengthy definition can be collapsed into one line:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   206
*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   207
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   208
datatype better_three = A | B | C
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   209
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   210
text{*\noindent
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   211
In fact, the \isacommand{datatype} command performs internally more or less
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   212
the same derivations as we did, which gives you some idea what life would be
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   213
like without \isacommand{datatype}.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   214
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   215
Although @{typ three} could be defined in one line, we have chosen this
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   216
example to demonstrate \isacommand{typedef} because its simplicity makes the
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   217
key concepts particularly easy to grasp. If you would like to see a
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   218
non-trivial example that cannot be defined more directly, we recommend the
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   219
definition of \emph{finite multisets} in the Library~\cite{HOL-Library}.
11858
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   220
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   221
Let us conclude by summarizing the above procedure for defining a new type.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   222
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   223
set of functions $F$, this involves three steps:
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   224
\begin{enumerate}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   225
\item Find an appropriate type $\tau$ and subset $A$ which has the desired
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   226
  properties $P$, and make a type definition based on this representation.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   227
\item Define the required functions $F$ on $ty$ by lifting
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   228
analogous functions on the representation via $Abs_ty$ and $Rep_ty$.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   229
\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   230
\end{enumerate}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   231
You can now forget about the representation and work solely in terms of the
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   232
abstract functions $F$ and properties $P$.%
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   233
\index{typedecl@\isacommand {typedef} (command)|)}%
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   234
\index{types!defining|)}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   235
*}
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   236
ca128c9100b6 renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff changeset
   237
(*<*)end(*>*)