author | wenzelm |
Wed, 19 Oct 2005 21:52:07 +0200 | |
changeset 17914 | 99ead7a7eb42 |
parent 12815 | 1f073030b97a |
child 27027 | 63f0b638355c |
permissions | -rw-r--r-- |
17914 | 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 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
44 |
axioms |
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 | 64 |
any non-empty subset of an existing type can be turned into a new type. |
65 |
More precisely, the new type is specified to be isomorphic to some |
|
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 |
|
12473 | 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 | 78 |
Fortunately, this is easy enough to show, even \isa{auto} could do it. |
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 | 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 | 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 three} &::& @{typ"nat set"} \\ |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
94 |
@{term Rep_three} &::& @{typ"three \<Rightarrow> nat"}\\ |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
95 |
@{term Abs_three} &::& @{typ"nat \<Rightarrow> three"} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
96 |
\end{tabular} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
97 |
\end{center} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
98 |
where constant @{term three} is explicitly defined as the representing set: |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
99 |
\begin{center} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
100 |
@{thm three_def}\hfill(@{thm[source]three_def}) |
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 |
The situation is best summarized with the help of the following diagram, |
12543 | 103 |
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
|
104 |
\begin{center} |
12628 | 105 |
\includegraphics[scale=.8]{typedef} |
11858
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
106 |
\end{center} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
107 |
Finally, \isacommand{typedef} asserts that @{term Rep_three} is |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
108 |
surjective on the subset @{term three} and @{term Abs_three} and @{term |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
109 |
Rep_three} are inverses of each other: |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
110 |
\begin{center} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
111 |
\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
112 |
@{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
|
113 |
@{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
|
114 |
@{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
|
115 |
\end{tabular} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
116 |
\end{center} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
117 |
% |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
118 |
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
|
119 |
in general given a name (here @{text three}) and a set |
12473 | 120 |
(here @{term"{0::nat,1,2}"}). |
11858
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
121 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
122 |
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
|
123 |
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
|
124 |
\begin{itemize} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
125 |
\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
|
126 |
functions you anticipate. |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
127 |
\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
|
128 |
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
|
129 |
two levels. |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
130 |
\end{itemize} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
131 |
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
|
132 |
names: |
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 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
135 |
constdefs |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
136 |
A:: three |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
137 |
"A \<equiv> Abs_three 0" |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
138 |
B:: three |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
139 |
"B \<equiv> Abs_three 1" |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
140 |
C :: three |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
141 |
"C \<equiv> Abs_three 2" |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
142 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
143 |
text{* |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
144 |
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
|
145 |
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
|
146 |
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
|
147 |
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
|
148 |
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
|
149 |
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
|
150 |
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
|
151 |
and that they exhaust the type. |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
152 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
153 |
In processing our \isacommand{typedef} declaration, |
12473 | 154 |
Isabelle proves several helpful lemmas. The first two |
155 |
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
|
156 |
\begin{center} |
12473 | 157 |
\begin{tabular}{@ {}r@ {\qquad}l@ {}} |
158 |
@{thm Rep_three_inject[no_vars]} & (@{thm[source]Rep_three_inject}) \\ |
|
159 |
\begin{tabular}{@ {}l@ {}} |
|
160 |
@{text"\<lbrakk>x \<in> three; y \<in> three \<rbrakk>"} \\ |
|
161 |
@{text"\<Longrightarrow> (Abs_three x = Abs_three y) = (x = y)"} |
|
162 |
\end{tabular} & (@{thm[source]Abs_three_inject}) \\ |
|
163 |
\end{tabular} |
|
11858
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
164 |
\end{center} |
12473 | 165 |
The following ones allow to replace some @{text"x::three"} by |
166 |
@{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
|
167 |
\begin{center} |
12473 | 168 |
\begin{tabular}{@ {}r@ {\qquad}l@ {}} |
169 |
@{thm Rep_three_cases[no_vars]} & (@{thm[source]Rep_three_cases}) \\ |
|
170 |
@{thm Abs_three_cases[no_vars]} & (@{thm[source]Abs_three_cases}) \\ |
|
171 |
@{thm Rep_three_induct[no_vars]} & (@{thm[source]Rep_three_induct}) \\ |
|
172 |
@{thm Abs_three_induct[no_vars]} & (@{thm[source]Abs_three_induct}) \\ |
|
173 |
\end{tabular} |
|
11858
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
174 |
\end{center} |
12473 | 175 |
These theorems are proved for any type definition, with @{term three} |
176 |
replaced by the name of the type in question. |
|
177 |
||
11858
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
178 |
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
|
179 |
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
|
180 |
of @{term Abs_three}: |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
181 |
*} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
182 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
183 |
lemma "A \<noteq> B \<and> B \<noteq> A \<and> A \<noteq> C \<and> C \<noteq> A \<and> B \<noteq> C \<and> C \<noteq> B" |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
184 |
by(simp add: Abs_three_inject A_def B_def C_def three_def) |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
185 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
186 |
text{*\noindent |
12473 | 187 |
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
|
188 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
189 |
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
|
190 |
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
|
191 |
(where @{term x} is of type @{typ three}) it suffices to prove @{prop"P A"}, |
12473 | 192 |
@{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
|
193 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
194 |
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
|
195 |
|
12473 | 196 |
txt{*\noindent Again this follows easily from a pre-proved general theorem:*} |
11858
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
197 |
|
12815 | 198 |
apply(induct_tac x rule: Abs_three_induct) |
11858
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 |
txt{* |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
201 |
@{subgoals[display,indent=0]} |
12473 | 202 |
Simplification with @{thm[source]three_def} leads to the disjunction @{prop"y |
203 |
= 0 \<or> y = 1 \<or> y = (2::nat)"} which \isa{auto} separates into three |
|
204 |
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
|
205 |
|
12473 | 206 |
apply(auto simp add: three_def A_def B_def C_def) |
11858
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
207 |
done |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
208 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
209 |
text{*\noindent |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
210 |
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
|
211 |
type @{typ three}. |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
212 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
213 |
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
|
214 |
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
|
215 |
*} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
216 |
|
12334 | 217 |
datatype better_three = A | B | C |
11858
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
218 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
219 |
text{*\noindent |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
220 |
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
|
221 |
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
|
222 |
like without \isacommand{datatype}. |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
223 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
224 |
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
|
225 |
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
|
226 |
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
|
227 |
non-trivial example that cannot be defined more directly, we recommend the |
12473 | 228 |
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
|
229 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
230 |
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
|
231 |
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
|
232 |
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
|
233 |
\begin{enumerate} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
234 |
\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
|
235 |
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
|
236 |
\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
|
237 |
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
|
238 |
\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
|
239 |
\end{enumerate} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
240 |
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
|
241 |
abstract functions $F$ and properties $P$.% |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
242 |
\index{typedecl@\isacommand {typedef} (command)|)}% |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
243 |
\index{types!defining|)} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
244 |
*} |
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
245 |
|
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
wenzelm
parents:
diff
changeset
|
246 |
(*<*)end(*>*) |