# HG changeset patch # User wenzelm # Date 1003685740 -7200 # Node ID ca128c9100b679cc619086d910d5e2ae3989cc3e # Parent cc3d971fe66ae895cfe72622e5aa2458d552c819 renamed Typedef.thy to Typedefs.thy (former already present in main HOL); diff -r cc3d971fe66a -r ca128c9100b6 doc-src/TutorialI/IsaMakefile --- 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 $(REALUSEDIR) Types diff -r cc3d971fe66a -r ca128c9100b6 doc-src/TutorialI/Types/ROOT.ML --- 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"; diff -r cc3d971fe66a -r ca128c9100b6 doc-src/TutorialI/Types/Typedefs.thy --- /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*} + +text{*\label{sec:adv-typedef} +For most applications, a combination of predefined types like @{typ bool} and +@{text"\"} 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: "\x::my_new_type. \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::nat. n \ 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 \ nat"}\\ +@{term Abs_three} &::& @{typ"nat \ 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} +\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}) +\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\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 \ Abs_three 0" + B:: three + "B \ Abs_three 1" + C :: three + "C \ 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 \ B \ B \ A \ A \ C \ C \ A \ B \ C \ C \ 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 \ 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: "\ Q 0; Q 1; Q 2; n \ three \ \ Q n" + +txt{*\noindent +Expanding @{thm[source]three_def} yields the premise @{prop"n\2"}. Repeated +elimination with @{thm[source]le_SucE} +@{thm[display]le_SucE} +reduces @{prop"n\2"} to the three cases @{prop"n\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 +done + +text{* +Now the case distinction lemma on type @{typ three} is easy to derive if you +know how: +*} + +lemma three_cases: "\ P A; P B; P C \ \ 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"\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(*>*)