src/Doc/Classes/Classes.thy

   Type classes were introduced by Wadler and Blott @{cite wadler89how}
   into the Haskell language to allow for a reasonable implementation
   of overloading\footnote{throughout this tutorial, we are referring
   to classical Haskell 1.0 type classes, not considering later
   additions in expressiveness}.  As a canonical example, a polymorphic
-  equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
+  equality function @{text "eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
   different types for @{text "\<alpha>"}, which is achieved by splitting
   introduction of the @{text eq} function from its overloaded
   definitions by means of @{text class} and @{text instance}
   declarations: \footnote{syntax here is a kind of isabellized
   Haskell}
 
   \begin{quote}
 
   \noindent@{text "class eq where"} \\
-  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
-
-  \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
+  \hspace*{2ex}@{text "eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+
+  \medskip\noindent@{text "instance nat :: eq where"} \\
   \hspace*{2ex}@{text "eq 0 0 = True"} \\
   \hspace*{2ex}@{text "eq 0 _ = False"} \\
   \hspace*{2ex}@{text "eq _ 0 = False"} \\
   \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
 
-  \medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
+  \medskip\noindent@{text "instance (\<alpha>::eq, \<beta>::eq) pair :: eq where"} \\
   \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
 
   \medskip\noindent@{text "class ord extends eq where"} \\
-  \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
-  \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+  \hspace*{2ex}@{text "less_eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+  \hspace*{2ex}@{text "less :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
 
   \end{quote}
 
   \noindent Type variables are annotated with (finitely many) classes;
   these annotations are assertions that a particular polymorphic type

   symmetry and transitivity:
 
   \begin{quote}
 
   \noindent@{text "class eq where"} \\
-  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+  \hspace*{2ex}@{text "eq :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
   @{text "satisfying"} \\
   \hspace*{2ex}@{text "refl: eq x x"} \\
   \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
   \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
 

   \noindent This @{command class} specification consists of two parts:
   the \qn{operational} part names the class parameter (@{element
   "fixes"}), the \qn{logical} part specifies properties on them
   (@{element "assumes"}).  The local @{element "fixes"} and @{element
   "assumes"} are lifted to the theory toplevel, yielding the global
-  parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
-  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon>
-  \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
+  parameter @{term [source] "mult :: \<alpha>::semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
+  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z ::
+  \<alpha>::semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
 *}
 
 
 subsection {* Class instantiation \label{sec:class_inst} *}
 

 
 instantiation %quote int :: semigroup
 begin
 
 definition %quote
-  mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
+  mult_int_def: "i \<otimes> j = i + (j::int)"
 
 instance %quote proof
   fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
   then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
     unfolding mult_int_def .

 
 instantiation %quote nat :: semigroup
 begin
 
 primrec %quote mult_nat where
-  "(0\<Colon>nat) \<otimes> n = n"
+  "(0::nat) \<otimes> n = n"
   | "Suc m \<otimes> n = Suc (m \<otimes> n)"
 
 instance %quote proof
   fix m n q :: nat 
   show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"

 
 definition %quote
   mult_prod_def: "p\<^sub>1 \<otimes> p\<^sub>2 = (fst p\<^sub>1 \<otimes> fst p\<^sub>2, snd p\<^sub>1 \<otimes> snd p\<^sub>2)"
 
 instance %quote proof
-  fix p\<^sub>1 p\<^sub>2 p\<^sub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+  fix p\<^sub>1 p\<^sub>2 p\<^sub>3 :: "\<alpha>::semigroup \<times> \<beta>::semigroup"
   show "p\<^sub>1 \<otimes> p\<^sub>2 \<otimes> p\<^sub>3 = p\<^sub>1 \<otimes> (p\<^sub>2 \<otimes> p\<^sub>3)"
     unfolding mult_prod_def by (simp add: assoc)
 qed      
 
 end %quote

 
 instantiation %quote nat and int :: monoidl
 begin
 
 definition %quote
-  neutral_nat_def: "\<one> = (0\<Colon>nat)"
+  neutral_nat_def: "\<one> = (0::nat)"
 
 definition %quote
-  neutral_int_def: "\<one> = (0\<Colon>int)"
+  neutral_int_def: "\<one> = (0::int)"
 
 instance %quote proof
   fix n :: nat
   show "\<one> \<otimes> n = n"
     unfolding neutral_nat_def by simp

 
 definition %quote
   neutral_prod_def: "\<one> = (\<one>, \<one>)"
 
 instance %quote proof
-  fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
+  fix p :: "\<alpha>::monoidl \<times> \<beta>::monoidl"
   show "\<one> \<otimes> p = p"
     unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
 qed
 
 end %quote

 
 instantiation %quote prod :: (monoid, monoid) monoid
 begin
 
 instance %quote proof 
-  fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
+  fix p :: "\<alpha>::monoid \<times> \<beta>::monoid"
   show "p \<otimes> \<one> = p"
     unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
 qed
 
 end %quote

 
 instantiation %quote int :: group
 begin
 
 definition %quote
-  inverse_int_def: "i\<div> = - (i\<Colon>int)"
+  inverse_int_def: "i\<div> = - (i::int)"
 
 instance %quote proof
   fix i :: int
   have "-i + i = 0" by simp
   then show "i\<div> \<otimes> i = \<one>"

   primitive type class @{text "idem"}, together with a corresponding
   interpretation:
 *}
 
 interpretation %quote idem_class:
-  idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
+  idem "f :: (\<alpha>::idem) \<Rightarrow> \<alpha>"
 (*<*)sorry(*>*)
 
 text {*
   \noindent This gives you the full power of the Isabelle module system;
   conclusions in locale @{text idem} are implicitly propagated

 
 text {*
   \noindent Here the \qt{@{keyword "in"} @{class group}} target
   specification indicates that the result is recorded within that
   context for later use.  This local theorem is also lifted to the
-  global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon>
-  \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been
+  global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z ::
+  \<alpha>::group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been
   made an instance of @{text "group"} before, we may refer to that
-  fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
+  fact as well: @{prop [source] "\<And>x y z :: int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
   z"}.
 *}
 
 
 subsection {* Derived definitions *}

   | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
 
 text {*
   \noindent If the locale @{text group} is also a class, this local
   definition is propagated onto a global definition of @{term [source]
-  "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems
+  "pow_nat :: nat \<Rightarrow> \<alpha>::monoid \<Rightarrow> \<alpha>::monoid"} with corresponding theorems
 
   @{thm pow_nat.simps [no_vars]}.
 
   \noindent As you can see from this example, for local definitions
   you may use any specification tool which works together with

   "pow_int k x = (if k >= 0
     then pow_nat (nat k) x
     else (pow_nat (nat (- k)) x)\<div>)"
 
 text {*
-  \noindent yields the global definition of @{term [source] "pow_int \<Colon>
-  int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm
+  \noindent yields the global definition of @{term [source] "pow_int ::
+  int \<Rightarrow> \<alpha>::group \<Rightarrow> \<alpha>::group"} with the corresponding theorem @{thm
   pow_int_def [no_vars]}.
 *}
 
 subsection {* A note on syntax *}
 

 
 context %quote semigroup
 begin
 
 term %quote "x \<otimes> y" -- {* example 1 *}
-term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
+term %quote "(x::nat) \<otimes> y" -- {* example 2 *}
 
 end  %quote
 
 term %quote "x \<otimes> y" -- {* example 3 *}
 
 text {*
   \noindent Here in example 1, the term refers to the local class
   operation @{text "mult [\<alpha>]"}, whereas in example 2 the type
   constraint enforces the global class operation @{text "mult [nat]"}.
   In the global context in example 3, the reference is to the
-  polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
+  polymorphic global class operation @{text "mult [?\<alpha> :: semigroup]"}.
 *}
 
 section {* Further issues *}
 
 subsection {* Type classes and code generation *}