src/HOLCF/ex/Classlib.thy

ex_impE was incorrectly listed as Safe

(*  Title:      FOCUS/Classlib.thy
    ID:         $ $
    Author:     Franz Regensburger
    Copyright   1995 Technical University Munich

Introduce various type classes

The 8bit package is needed for this theory

The type void of HOLCF/Void.thy is a witness for all the introduced classes.
Inspect theory Witness.thy for all the proofs. 

the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
the trivial instance for .= and .<=  is LAM x y.(UU::tr)

the class hierarchy is as follows

        pcpo 
         |        
          ----------------
         |               | 
         |      --------------------- 
         |      |       |      |    | 
        per   cplus  cminus ctimes cdvi
         |
       equiv
       /  \
      /    \
     |     |
    qpo    eq
     | 
     |    
  qlinear


*)

Classlib = HOLCF +

(* -------------------------------------------------------------------- *)
(* class cplus with characteristic constant  ++                         *)
 
classes cplus < pcpo	

arities void :: cplus

ops curried 
	"++"	:: "'a::cplus -> 'a -> 'a"		(cinfixl 65)


(* class cplus has no characteristic axioms                             *)
(* -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
(* class cminus with characteristic constant --                         *)
 
classes cminus < pcpo	

arities void :: cminus

ops curried 
	"--"	:: "'a::cminus -> 'a -> 'a"		(cinfixl 65)

(* class cminus has no characteristic axioms                            *)
(* -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
(* class ctimes with characteristic constant **                         *)
 
classes ctimes < pcpo	

arities void :: ctimes

ops curried 
	"**"	:: "'a::ctimes -> 'a -> 'a"		(cinfixl 70)

(* class ctimes has no characteristic axioms                            *)
(* -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
(* class cdiv with characteristic constant //                           *)
 
classes cdiv < pcpo	

arities void :: cdiv

ops curried 
	"//"	:: "'a::cdiv -> 'a -> 'a"		(cinfixl 70)

(* class cdiv has no characteristic axioms                              *)
(* -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
(* class per with characteristic constant .=                            *)
 
classes per < pcpo	

arities void :: per

ops curried 
	".="	:: "'a::per -> 'a -> tr"	(cinfixl 55)
syntax (symbols)
	"op .=" :: "'a::per => 'a => tr"	(infixl "\\<doteq>" 55)

rules 

strict_per	"(UU .= x) = UU & (x .= UU) = UU"
total_per	"[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU"
flat_per	"flat (UU::'a::per)"

sym_per		"(x .= y) = (y .= x)"
trans_per	"[| (x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT"

(* -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
(* class equiv is a refinement of of class per                          *)
 
classes equiv < per 	

arities void :: equiv

rules 

refl_per	"[|(x::'a::equiv) ~= UU|] ==> (x .= x)=TT"

(* -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
(* class eq is a refinement of of class equiv                           *)
 
classes eq < equiv  	

arities void :: eq

rules 

weq	"[| (x::'a::eq) ~= UU; y ~= UU |] ==> 
	 (x = y --> (x .=y) = TT) & (x ~= y --> (x .= y)=FF)"

(* -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
(* class qpo with characteristic constant .<=                           *)
(*  .<= is a partial order wrt an equivalence                           *)
 
classes qpo < equiv	

arities void :: qpo

ops curried 
	".<="	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
syntax (symbols)
	"op .<=":: "'a::qpo => 'a => tr"	(infixl "\\<preceq>" 55)
rules 

strict_qpo	"(UU .<= x) = UU & (x .<= UU) = UU"
total_qpo	"[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU"

refl_qpo	"[|x ~= UU|] ==> (x .<= x)=TT"
antisym_qpo	"[| (x .<= y)=TT; (y .<= x)=TT |] ==> (x .=  y)=TT"
trans_qpo	"[| (x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT"

antisym_qpo_rev	"(x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" 

(* -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
(* irreflexive part .< defined via .<=                                  *)
 
ops curried 
	".<"	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
syntax (symbols)
	"op .<"	:: "'a::qpo => 'a => tr"	(infixl "\\<prec>" 55)

defs

qless_def	"(op .<) Ú LAM x y.If x .= y then FF else x .<= y fi"

(* -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
(* class qlinear is a refinement of of class qpo                        *)
 
classes qlinear < qpo  	

arities void :: qlinear

rules 

qlinear	"[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT Á (y .<= x)=TT "

(* -------------------------------------------------------------------- *)

end