1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "o-algebra.ma".
17 alias symbol "eq" = "setoid1 eq".
18 definition is_saturation ≝
19 λC:OA.λA:unary_morphism (oa_P C) (oa_P C).
20 ∀U,V. (U ≤ A V) = (A U ≤ A V).
22 definition is_reduction ≝
23 λC:OA.λJ:unary_morphism (oa_P C) (oa_P C).
24 ∀U,V. (J U ≤ V) = (J U ≤ J V).
26 theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ≤ A U.
27 intros; apply (fi ?? (H ??)); apply (oa_leq_refl C).
30 theorem saturation_monotone:
31 ∀C,A. is_saturation C A →
32 ∀U,V. U ≤ V → A U ≤ A V.
33 intros; apply (if ?? (H ??)); apply (oa_leq_trans C);
34 [apply V|3: apply saturation_expansive ]
38 theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U.
39 eq (oa_P C) (A (A U)) (A U).
40 intros; apply (oa_leq_antisym C);
41 [ apply (if ?? (H (A U) U)); apply (oa_leq_refl C).
42 | apply saturation_expansive; assumption]