include "relations_to_o-algebra.ma".
definition o_basic_topology_of_basic_topology: basic_topology → Obasic_topology.
- intro;
- constructor 1;
- [ apply (POW' b);
- | apply (A b);
- | apply (J b);
- | apply (A_is_saturation b);
- | apply (J_is_reduction b);
- | apply (compatibility b); ]
+ intros (b); constructor 1;
+ [ apply (POW' b) | apply (A b) | apply (J b);
+ | apply (A_is_saturation b) | apply (J_is_reduction b) | apply (compatibility b) ]
qed.
definition o_continuous_relation_of_continuous_relation:
∀BT1,BT2.continuous_relation BT1 BT2 →
Ocontinuous_relation (o_basic_topology_of_basic_topology BT1) (o_basic_topology_of_basic_topology BT2).
- intros;
- constructor 1;
- [ apply (orelation_of_relation ?? c);
- | apply (reduced ?? c);
- | apply (saturated ?? c); ]
+ intros (BT1 BT2 c); constructor 1;
+ [ apply (orelation_of_relation ?? c) | apply (reduced ?? c) | apply (saturated ?? c) ]
qed.
\ No newline at end of file
notation "A × term 74 B ⇒\sub 3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
notation "B ⇒\sub 2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+notation "B ⇒\sub 1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
+notation "B ⇒\sub 2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
interpretation "'binary_morphism1" 'binary_morphism1 A B C = (binary_morphism1 A B C).
interpretation "'binary_morphism2" 'binary_morphism2 A B C = (binary_morphism2 A B C).
(* USARE L'ESISTENZIALE DEBOLE *)
definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
-notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation > "'If' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation < "'If' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
notation > "hvbox(a break ≤ b)" non associative with precedence 45 for @{oa_leq $a $b}.
oa_zero_bot: ∀p:oa_P.𝟘 ≤ p;
oa_one_top: ∀p:oa_P.p ≤ 𝟙;
oa_overlap_preserves_meet_: ∀p,q:oa_P.p >< q →
- p >< (⋀ { x ∈ BOOL | if x then p else q(*match x with [ true ⇒ p | false ⇒ q ]*) | IF_THEN_ELSE_p oa_P p q });
+ p >< (⋀ { x ∈ BOOL | If x then p else q(*match x with [ true ⇒ p | false ⇒ q ]*) | IF_THEN_ELSE_p oa_P p q });
oa_join_split: ∀I:SET.∀p.∀q:I ⇒_2 oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));
(*oa_base : setoid;
1) enum non e' il nome giusto perche' non e' suriettiva
intros (BP1 BP2 t);
constructor 1;
[ apply (t \sub \f);
- | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+ | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros (U e);
apply sym1;
- apply (.= †(†e));
- change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
- cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
- cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+ apply (.= †(†e));
+ change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩\sub BP1)* U));
+ cut ((t \sub \f ∘ (⊩)) ((⊩\sub BP1)* U) = ((⊩) ∘ t \sub \c) ((⊩\sub BP1)* U)) as COM;[2:
+ cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩\sub BP1)* U));]
apply (.= †COM);
change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
- apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
+ apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩\sub BP1)* U))));
apply (.= COM ^ -1);
- change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
+ change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩\sub BP1)* ) U));
change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
apply (†e^-1);
| apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
apply sym1;
apply (.= †(†e));
- change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
- cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
- cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+ change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩\sub BP1)⎻ U));
+ cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩\sub BP1)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩\sub BP1)⎻ U)) as COM;[2:
+ cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩\sub BP1)⎻ U));]
apply (.= †COM);
change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
- apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
+ apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩\sub BP1)⎻ U))));
apply (.= COM ^ -1);
- change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
+ change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩\sub BP1)⎻ ) U));
change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
apply (†e^-1);]
qed.
include "o-algebra.ma".
include "o-saturations.ma".
-record Obasic_topology: Type2 ≝
- { Ocarrbt:> OA;
- oA: Ocarrbt ⇒_2 Ocarrbt;
- oJ: Ocarrbt ⇒_2 Ocarrbt;
- oA_is_saturation: is_o_saturation ? oA;
- oJ_is_reduction: is_o_reduction ? oJ;
+record Obasic_topology: Type2 ≝ {
+ Ocarrbt:> OA;
+ oA: Ocarrbt ⇒_2 Ocarrbt; oJ: Ocarrbt ⇒_2 Ocarrbt;
+ oA_is_saturation: is_o_saturation ? oA; oJ_is_reduction: is_o_reduction ? oJ;
Ocompatibility: ∀U,V. (oA U >< oJ V) =_1 (U >< oJ V)
}.
-record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝
- { Ocont_rel:> arrows2 OA S T;
- (* reduces uses eq1, saturated uses eq!!! *)
- Oreduced: ∀U. U = oJ ? U → Ocont_rel U = oJ ? (Ocont_rel U);
- Osaturated: ∀U. U = oA ? U → Ocont_rel⎻* U = oA ? (Ocont_rel⎻* U)
+record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝ {
+ Ocont_rel:> arrows2 OA S T;
+ Oreduced: ∀U:S. U = oJ ? U → Ocont_rel U =_1 oJ ? (Ocont_rel U);
+ Osaturated: ∀U:S. U = oA ? U → Ocont_rel⎻* U =_1 oA ? (Ocont_rel⎻* U)
}.
definition Ocontinuous_relation_setoid: Obasic_topology → Obasic_topology → setoid2.
include "o-algebra.ma".
-alias symbol "eq" = "setoid1 eq".
-definition is_o_saturation: ∀C:OA. unary_morphism1 C C → CProp1 ≝
- λC:OA.λA:unary_morphism1 C C.
- ∀U,V. (U ≤ A V) = (A U ≤ A V).
+definition is_o_saturation: ∀C:OA. C ⇒_1 C → CProp1 ≝
+ λC:OA.λA:C ⇒_1 C.∀U,V. (U ≤ A V) =_1 (A U ≤ A V).
-definition is_o_reduction: ∀C:OA. unary_morphism1 C C → CProp1 ≝
- λC:OA.λJ:unary_morphism1 C C.
- ∀U,V. (J U ≤ V) = (J U ≤ J V).
+definition is_o_reduction: ∀C:OA. C ⇒_1 C → CProp1 ≝
+ λC:OA.λJ:C ⇒_1 C.∀U,V. (J U ≤ V) =_1 (J U ≤ J V).
theorem o_saturation_expansive: ∀C,A. is_o_saturation C A → ∀U. U ≤ A U.
intros; apply (fi ?? (i ??)); apply (oa_leq_refl C).
qed.
-theorem o_saturation_monotone:
- ∀C,A. is_o_saturation C A →
- ∀U,V. U ≤ V → A U ≤ A V.
+theorem o_saturation_monotone: ∀C:OA.∀A:C ⇒_1 C. is_o_saturation C A → ∀U,V. U ≤ V → A U ≤ A V.
intros; apply (if ?? (i ??)); apply (oa_leq_trans C);
[apply V|3: apply o_saturation_expansive ]
assumption.
qed.
-theorem o_saturation_idempotent: ∀C,A. is_o_saturation C A → ∀U.
- eq1 C (A (A U)) (A U).
+theorem o_saturation_idempotent: ∀C:OA.∀A:C ⇒_1 C. is_o_saturation C A → ∀U. A (A U) =_1 A U.
intros; apply (oa_leq_antisym C);
[ apply (if ?? (i (A U) U)); apply (oa_leq_refl C).
| apply o_saturation_expansive; assumption]
(* These are only conversions :-) *)
-definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)).
- intros (C t);apply t;
-qed.
+definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)) ≝ λC,t.t.
-definition is_o_saturation_of_is_saturation: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
- is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
- intros; apply i;
-qed.
+definition is_o_saturation_of_is_saturation:
+ ∀C:REL.∀R: Ω^C ⇒_1 Ω^C. is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
+intros (C R i); apply i; qed.
-definition is_o_reduction_of_is_reduction: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
- is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
- intros; apply i;
-qed.
\ No newline at end of file
+definition is_o_reduction_of_is_reduction:
+ ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
+intros (C R i); apply i; qed.
projects / helm.git / commitdiff