doc-src/TutorialI/Types/Overloading1.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Overloading1.thy	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,41 @@
+(*<*)theory Overloading1 = Main:(*>*)
+
+subsubsection{*Controlled overloading with type classes*}
+
+text{*
+We now start with the theory of ordering relations, which we want to phrase
+in terms of the two binary symbols @{text"<<"} and @{text"<<="}: they have
+been chosen to avoid clashes with @{text"\<le>"} and @{text"<"} in theory @{text
+Main}. To restrict the application of @{text"<<"} and @{text"<<="} we
+introduce the class @{text ordrel}:
+*}
+
+axclass ordrel < "term"
+
+text{*\noindent
+This is a degenerate form of axiomatic type class without any axioms.
+Its sole purpose is to restrict the use of overloaded constants to meaningful
+instances:
+*}
+
+consts
+  "<<"        :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"             (infixl 50)
+  "<<="       :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"             (infixl 50)
+
+instance bool :: ordrel
+by intro_classes
+
+defs (overloaded)
+le_bool_def:  "P <<= Q \<equiv> P \<longrightarrow> Q"
+less_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
+
+text{*
+Now @{prop"False <<= False"} is provable
+*}
+
+lemma "False <<= False"
+by(simp add: le_bool_def)
+
+text{*\noindent
+whereas @{text"[] <<= []"} is not even welltyped. In order to make it welltyped
+we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)