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 definition hint1: OA → Type ≝ λc:OA.carr (oa_P c).
20 definition hint2: ∀C.hint1 C → carr1 ((λx.x) (setoid1_of_setoid (oa_P C))).
25 alias symbol "eq" = "setoid1 eq".
26 definition is_saturation ≝
28 ∀U,V. (U ≤ A V) = (A U ≤ A V).
30 definition is_reduction ≝
32 ∀U,V. (J U ≤ V) = (J U ≤ J V).
34 theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ≤ A U.
35 intros; apply (fi ?? (H ??)); apply (oa_leq_refl C).
38 theorem saturation_monotone:
39 ∀C,A. is_saturation C A →
40 ∀U,V:C. U ≤ V → A U ≤ A V.
41 intros; apply (if ?? (H ??)); apply (oa_leq_trans C);
42 [apply V|3: apply saturation_expansive ]
46 theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U.
47 eq (oa_P C) (A (A U)) (A U).
48 intros; apply (oa_leq_antisym C);
49 [ apply (if ?? (H (A U) U)); apply (oa_leq_refl C).
50 | apply saturation_expansive; assumption]