equal
deleted
inserted
replaced
1054 auxiliary classes which specify that (op <=) and |
1054 auxiliary classes which specify that (op <=) and |
1055 Inf are equivariant. Instances for bool and fun are |
1055 Inf are equivariant. Instances for bool and fun are |
1056 given. |
1056 given. |
1057 *} |
1057 *} |
1058 |
1058 |
1059 class le_eqvt = order + |
1059 class le_eqvt = ord + |
1060 assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{pt, order}))))" |
1060 assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{order, pt}))))" |
1061 |
1061 |
1062 class inf_eqvt = complete_lattice + |
1062 class inf_eqvt = Inf + |
1063 assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::('a::{pt, Inf}) set))" |
1063 assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::'a::{complete_lattice, pt} set))" |
1064 |
1064 |
1065 instantiation bool :: le_eqvt |
1065 instantiation bool :: le_eqvt |
1066 begin |
1066 begin |
1067 |
1067 |
1068 instance |
1068 instance |