author wenzelm Sun, 21 Oct 2001 19:48:19 +0200 changeset 11865 93d5408eb7d9 parent 11864 371ce685b0ec child 11866 fbd097aec213
renamed to Typedefs.thy to avoid conflict with main HOL version;
 doc-src/TutorialI/Types/Typedef.thy file | annotate | diff | comparison | revisions
--- a/doc-src/TutorialI/Types/Typedef.thy	Sun Oct 21 19:44:25 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,278 +0,0 @@
-(*<*)theory Typedef = Main:(*>*)
-
-section{*Introducing New Types*}
-
-For most applications, a combination of predefined types like @{typ bool} and
-@{text"\<Rightarrow>"} with recursive datatypes and records is quite sufficient. Very
-occasionally you may feel the need for a more advanced type.  If you
-are certain that your type is not definable by any of the
-standard means, then read on.
-\begin{warn}
-  Types in HOL must be non-empty; otherwise the quantifier rules would be
-  unsound, because $\exists x.\ x=x$ is a theorem.
-\end{warn}
-*}
-
-subsection{*Declaring New Types*}
-
-text{*\label{sec:typedecl}
-\index{types!declaring|(}%
-\index{typedecl@\isacommand {typedecl} (command)}%
-The most trivial way of introducing a new type is by a \textbf{type
-declaration}: *}
-
-typedecl my_new_type
-
-text{*\noindent
-This does not define @{typ my_new_type} at all but merely introduces its
-name. Thus we know nothing about this type, except that it is
-non-empty. Such declarations without definitions are
-useful if that type can be viewed as a parameter of the theory.
-A typical example is given in \S\ref{sec:VMC}, where we define a transition
-relation over an arbitrary type of states.
-
-In principle we can always get rid of such type declarations by making those
-types parameters of every other type, thus keeping the theory generic. In
-practice, however, the resulting clutter can make types hard to read.
-
-If you are looking for a quick and dirty way of introducing a new type
-together with its properties: declare the type and state its properties as
-axioms. Example:
-*}
-
-axioms
-just_one: "\<exists>x::my_new_type. \<forall>y. x = y"
-
-text{*\noindent
-However, we strongly discourage this approach, except at explorative stages
-of your development. It is extremely easy to write down contradictory sets of
-axioms, in which case you will be able to prove everything but it will mean
-nothing.  In the example above, the axiomatic approach is
-unnecessary: a one-element type called @{typ unit} is already defined in HOL.
-\index{types!declaring|)}
-*}
-
-subsection{*Defining New Types*}
-
-text{*\label{sec:typedef}
-\index{types!defining|(}%
-\index{typedecl@\isacommand {typedef} (command)|(}%
-Now we come to the most general means of safely introducing a new type, the
-\textbf{type definition}. All other means, for example
-\isacommand{datatype}, are based on it. The principle is extremely simple:
-any non-empty subset of an existing type can be turned into a new type.  Thus
-a type definition is merely a notational device: you introduce a new name for
-a subset of an existing type. This does not add any logical power to HOL,
-because you could base all your work directly on the subset of the existing
-type. However, the resulting theories could easily become indigestible
-because instead of implicit types you would have explicit sets in your
-formulae.
-
-Let us work a simple example, the definition of a three-element type.
-It is easily represented by the first three natural numbers:
-*}
-
-typedef three = "{n. n \<le> 2}"
-
-txt{*\noindent
-In order to enforce that the representing set on the right-hand side is
-non-empty, this definition actually starts a proof to that effect:
-@{subgoals[display,indent=0]}
-Fortunately, this is easy enough to show: take 0 as a witness.
-*}
-
-apply(rule_tac x = 0 in exI);
-by simp
-
-text{*
-This type definition introduces the new type @{typ three} and asserts
-that it is a copy of the set @{term"{0,1,2}"}. This assertion
-is expressed via a bijection between the \emph{type} @{typ three} and the
-\emph{set} @{term"{0,1,2}"}. To this end, the command declares the following
-constants behind the scenes:
-\begin{center}
-\begin{tabular}{rcl}
-@{term three} &::& @{typ"nat set"} \\
-@{term Rep_three} &::& @{typ"three \<Rightarrow> nat"}\\
-@{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
-\end{tabular}
-\end{center}
-where constant @{term three} is explicitly defined as the representing set:
-\begin{center}
-@{thm three_def}\hfill(@{thm[source]three_def})
-\end{center}
-The situation is best summarized with the help of the following diagram,
-where squares are types and circles are sets:
-\begin{center}
-\unitlength1mm
-\thicklines
-\begin{picture}(100,40)
-\put(3,13){\framebox(15,15){@{typ three}}}
-\put(55,5){\framebox(30,30){@{term three}}}
-\put(70,32){\makebox(0,0){@{typ nat}}}
-\put(70,20){\circle{40}}
-\put(10,15){\vector(1,0){60}}
-\put(25,14){\makebox(0,0)[tl]{@{term Rep_three}}}
-\put(70,25){\vector(-1,0){60}}
-\put(25,26){\makebox(0,0)[bl]{@{term Abs_three}}}
-\end{picture}
-\end{center}
-Finally, \isacommand{typedef} asserts that @{term Rep_three} is
-surjective on the subset @{term three} and @{term Abs_three} and @{term
-Rep_three} are inverses of each other:
-\begin{center}
-@{thm Rep_three[no_vars]} & (@{thm[source]Rep_three}) \\
-@{thm Rep_three_inverse[no_vars]} & (@{thm[source]Rep_three_inverse}) \\
-@{thm Abs_three_inverse[no_vars]} & (@{thm[source]Abs_three_inverse})
-\end{tabular}
-\end{center}
-%
-From this example it should be clear what \isacommand{typedef} does
-in general given a name (here @{text three}) and a set
-(here @{term"{n. n\<le>2}"}).
-
-Our next step is to define the basic functions expected on the new type.
-Although this depends on the type at hand, the following strategy works well:
-\begin{itemize}
-\item define a small kernel of basic functions that can express all other
-functions you anticipate.
-\item define the kernel in terms of corresponding functions on the
-representing type using @{term Abs} and @{term Rep} to convert between the
-two levels.
-\end{itemize}
-In our example it suffices to give the three elements of type @{typ three}
-names:
-*}
-
-constdefs
-  A:: three
- "A \<equiv> Abs_three 0"
-  B:: three
- "B \<equiv> Abs_three 1"
-  C :: three
- "C \<equiv> Abs_three 2";
-
-text{*
-So far, everything was easy. But it is clear that reasoning about @{typ
-three} will be hell if we have to go back to @{typ nat} every time. Thus our
-aim must be to raise our level of abstraction by deriving enough theorems
-about type @{typ three} to characterize it completely. And those theorems
-should be phrased in terms of @{term A}, @{term B} and @{term C}, not @{term
-Abs_three} and @{term Rep_three}. Because of the simplicity of the example,
-we merely need to prove that @{term A}, @{term B} and @{term C} are distinct
-and that they exhaust the type.
-
-In processing our \isacommand{typedef} declaration,
-Isabelle helpfully proves several lemmas.
-One, @{thm[source]Abs_three_inject},
-expresses that @{term Abs_three} is injective on the representing subset:
-\begin{center}
-@{thm Abs_three_inject[no_vars]}
-\end{center}
-Another, @{thm[source]Rep_three_inject}, expresses that the representation
-function is also injective:
-\begin{center}
-@{thm Rep_three_inject[no_vars]}
-\end{center}
-Distinctness of @{term A}, @{term B} and @{term C} follows immediately
-if we expand their definitions and rewrite with the injectivity
-of @{term Abs_three}:
-*}
-
-lemma "A \<noteq> B \<and> B \<noteq> A \<and> A \<noteq> C \<and> C \<noteq> A \<and> B \<noteq> C \<and> C \<noteq> B";
-by(simp add: Abs_three_inject A_def B_def C_def three_def);
-
-text{*\noindent
-Of course we rely on the simplifier to solve goals like @{prop"0 \<noteq> 1"}.
-
-The fact that @{term A}, @{term B} and @{term C} exhaust type @{typ three} is
-best phrased as a case distinction theorem: if you want to prove @{prop"P x"}
-(where @{term x} is of type @{typ three}) it suffices to prove @{prop"P A"},
-@{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the
-representation: *}
-
-lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n \<in> three \<rbrakk> \<Longrightarrow>  Q n";
-
-txt{*\noindent
-Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated
-elimination with @{thm[source]le_SucE}
-@{thm[display]le_SucE}
-reduces @{prop"n\<le>2"} to the three cases @{prop"n\<le>0"}, @{prop"n=1"} and
-@{prop"n=2"} which are trivial for simplification:
-*}
-
-apply((erule le_SucE)+);
-apply simp_all;
-done
-
-text{*
-Now the case distinction lemma on type @{typ three} is easy to derive if you
-know how:
-*}
-
-lemma three_cases: "\<lbrakk> P A; P B; P C \<rbrakk> \<Longrightarrow> P x";
-
-txt{*\noindent
-We start by replacing the @{term x} by @{term"Abs_three(Rep_three x)"}:
-*}
-
-apply(rule subst[OF Rep_three_inverse]);
-
-txt{*\noindent
-This substitution step worked nicely because there was just a single
-occurrence of a term of type @{typ three}, namely @{term x}.
-When we now apply @{thm[source]cases_lemma}, @{term Q} becomes @{term"\<lambda>n. P(Abs_three
-n)"} because @{term"Rep_three x"} is the only term of type @{typ nat}:
-*}
-
-apply(rule cases_lemma);
-
-txt{*
-@{subgoals[display,indent=0]}
-The resulting subgoals are easily solved by simplification:
-*}
-
-apply(simp_all add:A_def B_def C_def Rep_three);
-done
-
-text{*\noindent
-This concludes the derivation of the characteristic theorems for
-type @{typ three}.
-
-The attentive reader has realized long ago that the
-above lengthy definition can be collapsed into one line:
-*}
-
-datatype three' = A | B | C;
-
-text{*\noindent
-In fact, the \isacommand{datatype} command performs internally more or less
-the same derivations as we did, which gives you some idea what life would be
-like without \isacommand{datatype}.
-
-Although @{typ three} could be defined in one line, we have chosen this
-example to demonstrate \isacommand{typedef} because its simplicity makes the
-key concepts particularly easy to grasp. If you would like to see a
-non-trivial example that cannot be defined more directly, we recommend the
-definition of \emph{finite multisets} in the HOL Library.
-
-Let us conclude by summarizing the above procedure for defining a new type.
-Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
-set of functions $F$, this involves three steps:
-\begin{enumerate}
-\item Find an appropriate type $\tau$ and subset $A$ which has the desired
-  properties $P$, and make a type definition based on this representation.
-\item Define the required functions $F$ on $ty$ by lifting
-analogous functions on the representation via $Abs_ty$ and $Rep_ty$.
-\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
-\end{enumerate}
-You can now forget about the representation and work solely in terms of the
-abstract functions $F$ and properties $P$.%
-\index{typedecl@\isacommand {typedef} (command)|)}%
-\index{types!defining|)}
-*}
-
-(*<*)end(*>*)