src/HOL/Quot/PER0.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/PER0.thy	Fri Apr 04 16:01:14 1997 +0200
@@ -0,0 +1,37 @@
+(*  Title:      HOL/Quot/PER0.thy
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+Definition of classes per and er for (partial) equivalence classes
+The polymorphic constant eqv is only for the definition of PERs
+The characteristic constant === (sim) is available on the class per
+
+*)
+
+PER0 = Set + (* partial equivalence relations *)
+
+consts  (* polymorphic constant for (partial) equivalence relations *)
+        eqv    :: "'a::term => 'a => bool" 
+
+axclass per < term
+	(* axioms for partial equivalence relations *)
+        ax_per_sym      "eqv x y ==> eqv y x"
+        ax_per_trans    "[|eqv x y; eqv y z|] ==> eqv x z"
+
+axclass er < per
+	ax_er_refl	"eqv x x"
+
+consts  (* characteristic constant and Domain for per *)
+        "==="     :: "'a::per => 'a => bool" (infixl 55)
+        D         :: "'a::per set"
+defs
+        per_def         "(op ===) == eqv"
+        Domain          "D=={x.x===x}"
+(* define ==== on and function type => *)
+        fun_per_def     "eqv f g == !x y.x:D & y:D & x===y --> f x === g y"
+
+syntax (symbols)
+  "op ==="   :: "['a,'a::per] => bool"        (infixl "\\<sim>" 50)
+
+end