renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
Sun, 21 Oct 2001 19:35:40 +0200
changeset 11858 ca128c9100b6
parent 11857 cc3d971fe66a
child 11859 cb26f3922489
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
--- a/doc-src/TutorialI/IsaMakefile	Sat Oct 20 22:07:44 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Sun Oct 21 19:35:40 2001 +0200
@@ -157,7 +157,7 @@
 HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz
 $(LOG)/HOL-Real-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
-  Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedef.thy \
+  Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   Types/Overloading.thy Types/Axioms.thy
--- a/doc-src/TutorialI/Types/ROOT.ML	Sat Oct 20 22:07:44 2001 +0200
+++ b/doc-src/TutorialI/Types/ROOT.ML	Sun Oct 21 19:35:40 2001 +0200
@@ -3,7 +3,7 @@
 use_thy "Numbers";
 use_thy "Pairs";
 use_thy "Records";
-use_thy "Typedef";
+use_thy "Typedefs";
 use_thy "Overloading0";
 use_thy "Overloading2";
 use_thy "Axioms";
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Typedefs.thy	Sun Oct 21 19:35:40 2001 +0200
@@ -0,0 +1,278 @@
+(*<*)theory Typedefs = 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.
+  Types in HOL must be non-empty; otherwise the quantifier rules would be
+  unsound, because $\exists x.\ x=x$ is a theorem.
+subsection{*Declaring New Types*}
+\index{typedecl@\isacommand {typedecl} (command)}%
+The most trivial way of introducing a new type is by a \textbf{type
+declaration}: *}
+typedecl my_new_type
+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:
+just_one: "\<exists>x::my_new_type. \<forall>y. x = y"
+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.
+subsection{*Defining New Types*}
+\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
+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::nat. n \<le> 2}"
+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:
+Fortunately, this is easy enough to show: take 0 as a witness.
+apply(rule_tac x = 0 in exI)
+by simp
+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:
+@{term three} &::& @{typ"nat set"} \\
+@{term Rep_three} &::& @{typ"three \<Rightarrow> nat"}\\
+@{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
+where constant @{term three} is explicitly defined as the representing set:
+@{thm three_def}\hfill(@{thm[source]three_def})
+The situation is best summarized with the help of the following diagram,
+where squares are types and circles are sets:
+\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(25,14){\makebox(0,0)[tl]{@{term Rep_three}}}
+\put(25,26){\makebox(0,0)[bl]{@{term Abs_three}}}
+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{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
+@{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})
+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:
+\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.
+In our example it suffices to give the three elements of type @{typ three}
+  A:: three
+ "A \<equiv> Abs_three 0"
+  B:: three
+ "B \<equiv> Abs_three 1"
+  C :: three
+ "C \<equiv> Abs_three 2"
+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:
+@{thm Abs_three_inject[no_vars]}
+Another, @{thm[source]Rep_three_inject}, expresses that the representation
+function is also injective:
+@{thm Rep_three_inject[no_vars]}
+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)
+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"
+Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated
+elimination with @{thm[source]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(simp add: three_def numerals)
+apply((erule le_SucE)+)
+apply simp_all
+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"
+We start by replacing the @{term x} by @{term"Abs_three(Rep_three x)"}:
+apply(rule subst[OF Rep_three_inverse])
+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)
+The resulting subgoals are easily solved by simplification:
+apply(simp_all add:A_def B_def C_def Rep_three)
+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
+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:
+\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.
+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)|)}%