doc-src/TutorialI/Types/Overloading1.thy

*** empty log message ***

(*<*)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(*>*)