doc-src/TutorialI/Types/Overloading0.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Overloading0.thy	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,40 @@
+(*<*)theory Overloading0 = Main:(*>*)
+
+subsubsection{*An initial example*}
+
+text{* We start with a concept that is required for type classes but already
+useful on its own: \emph{overloading}. Isabelle allows overloading: a
+constant may have multiple definitions at non-overlapping types. For example,
+if we want to introduce the notion of an \emph{inverse} at arbitrary types we
+give it a polymorphic type *}
+
+consts inverse :: "'a \<Rightarrow> 'a"
+
+text{*\noindent
+and provide different definitions at different instances:
+*}
+
+defs (overloaded)
+inverse_bool: "inverse(b::bool) \<equiv> \<not> b"
+inverse_set:  "inverse(A::'a set) \<equiv> -A"
+inverse_pair: "inverse(p) \<equiv> (inverse(fst p), inverse(snd p))"
+
+text{*\noindent
+Isabelle will not complain because the three definitions do not overlap: no
+two of the three types @{typ bool}, @{typ"'a set"} and @{typ"'a \<times> 'b"} have a
+common instance. What is more, the recursion in @{thm[source]inverse_pair} is
+benign because the type of @{term inverse} becomes smaller: on the left it is
+@{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and @{typ"'b \<Rightarrow>
+'b"}. The @{text"(overloaded)"} tells Isabelle that the definitions do
+intentionally define @{term inverse} only at instances of its declared type
+@{typ"'a \<Rightarrow> 'a"} --- this merely supresses warnings to that effect.
+
+However, there is nothing to prevent the user from forming terms such as
+@{term"inverse []"} and proving theorems as @{prop"inverse [] = inverse []"},
+although we never defined inverse on lists. We hasten to say that there is
+nothing wrong with such terms and theorems. But it would be nice if we could
+prevent their formation, simply because it is very likely that the user did
+not mean to write what he did. Thus he had better not waste his time pursuing
+it further. This requires the use of type classes.
+*}
+(*<*)end(*>*)