try assumption; apply I]
qed.
-definition setoid_OF_SET: objs1 SET → setoid.
- intros; apply o; qed.
-
-coercion setoid_OF_SET.
-
lemma IF_THEN_ELSE_p :
∀S:setoid.∀a,b:S.∀x,y:BOOL.x = y →
(λm.match m with [ true ⇒ a | false ⇒ b ]) x =
oa_join_sup: ∀I.∀p_i.∀p:oa_P.oa_leq (oa_join I p_i) p → ∀i:I.oa_leq (p_i i) p;
oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
oa_one_top: ∀p:oa_P.oa_leq p oa_one;
- oa_overlap_preservers_meet:
+ oa_overlap_preservers_meet_:
∀p,q.oa_overlap p q → oa_overlap p
(oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
oa_join_split:
non associative with precedence 50 for @{ 'oa_meet $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈ I) break term 90 p)"
non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
+
+(*
notation < "hovbox(a ∧ b)" left associative with precedence 35
for @{ 'oa_meet_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
-
+*)
notation > "hovbox(∧ f)" non associative with precedence 60
for @{ 'oa_meet $f }.
+(*
notation > "hovbox(a ∧ b)" left associative with precedence 50
for @{ 'oa_meet (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
-
+*)
interpretation "o-algebra meet" 'oa_meet f =
(fun_1 __ (oa_meet __) f).
interpretation "o-algebra meet with explicit function" 'oa_meet_mk f =
(fun_1 __ (oa_meet __) (mk_unary_morphism _ _ f _)).
+definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
+intros; split;
+[ intros (p q);
+ apply (∧ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
+| intros; apply (prop_1 ?? (oa_meet O BOOL)); intro x; simplify;
+ cases x; simplify; assumption;]
+qed.
+
+notation "hovbox(a ∧ b)" left associative with precedence 35
+for @{ 'oa_meet_bin $a $b }.
+interpretation "o-algebra binary meet" 'oa_meet_bin a b =
+ (fun1 ___ (binary_meet _) a b).
+
+lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q).
+intros; lapply (oa_overlap_preservers_meet_ O p q f);
+lapply (prop1 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?);
+[3: apply (if ?? (Hletin1)); apply Hletin;|skip] apply refl1;
+qed.
+
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)"
non associative with precedence 49 for @{ 'oa_join $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈ I) break term 90 p)"
| apply ((comp_assoc1 ????? H* G* F* ));]
| intros; split; unfold ORelation_composition; simplify; apply id_neutral_left1;
| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right1;]
-qed.
\ No newline at end of file
+qed.