src/HOL/Quot/PER0.thy
 author wenzelm Fri Oct 10 19:02:28 1997 +0200 (1997-10-10) changeset 3842 b55686a7b22c parent 3058 9d6526cacc3c permissions -rw-r--r--
fixed dots;
```     1 (*  Title:      HOL/Quot/PER0.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Oscar Slotosch
```
```     4     Copyright   1997 Technische Universitaet Muenchen
```
```     5
```
```     6 Definition of classes per and er for (partial) equivalence classes
```
```     7 The polymorphic constant eqv is only for the definition of PERs
```
```     8 The characteristic constant === (sim) is available on the class per
```
```     9
```
```    10 *)
```
```    11
```
```    12 PER0 = Set + (* partial equivalence relations *)
```
```    13
```
```    14 consts  (* polymorphic constant for (partial) equivalence relations *)
```
```    15         eqv    :: "'a::term => 'a => bool"
```
```    16
```
```    17 axclass per < term
```
```    18 	(* axioms for partial equivalence relations *)
```
```    19         ax_per_trans    "[|eqv x y; eqv y z|] ==> eqv x z"
```
```    20         ax_per_sym      "eqv x y ==> eqv y x"
```
```    21
```
```    22 axclass er < per
```
```    23 	ax_er_refl	"eqv x x"
```
```    24
```
```    25 consts  (* characteristic constant and Domain for per *)
```
```    26         "==="     :: "'a::per => 'a => bool" (infixl 55)
```
```    27         D         :: "'a::per set"
```
```    28 defs
```
```    29         per_def         "(op ===) == eqv"
```
```    30         Dom             "D=={x. x===x}"
```
```    31 (* define ==== on and function type => *)
```
```    32         fun_per_def     "eqv f g == !x y. x:D & y:D & x===y --> f x === g y"
```
```    33
```
```    34 syntax (symbols)
```
```    35   "op ==="   :: "['a,'a::per] => bool"        (infixl "\\<sim>" 50)
```
```    36
```
```    37 end
```