Theory Transport_Natural_Functors_Order_Equivalence
subsection ‹Order Equivalence›
theory Transport_Natural_Functors_Order_Equivalence
imports
Transport_Natural_Functors_Base
begin
context
fixes R1 :: "'a ⇒ 'a ⇒ bool" and R2 :: "'b ⇒ 'b ⇒ bool" and R3 :: "'c ⇒ 'c ⇒ bool"
and f1 :: "'a ⇒ 'a" and f2 :: "'b ⇒ 'b" and f3 :: "'c ⇒ 'c"
and R :: "('d, 'a, 'b, 'c) F ⇒ ('d, 'a, 'b, 'c) F ⇒ bool"
and f :: "('d, 'a, 'b, 'c) F ⇒ ('d, 'a, 'b, 'c) F"
defines "R ≡ Frel R1 R2 R3" and "f ≡ Fmap f1 f2 f3"
begin
lemma inflationary_on_in_dom_FrelI:
assumes "inflationary_on (in_dom R1) R1 f1"
and "inflationary_on (in_dom R2) R2 f2"
and "inflationary_on (in_dom R3) R3 f3"
shows "inflationary_on (in_dom R) R f"
apply (unfold R_def f_def)
apply (rule inflationary_onI)
apply (subst (asm) in_dom_Frel_eq_Fpred_in_dom)
apply (erule FpredE)
apply (subst Frel_Fmap_eq2)
apply (rule Frel_refl_strong)
apply (rule inflationary_onD[where ?R=R1] inflationary_onD[where ?R=R2]
inflationary_onD[where ?R=R3],
rule assms,
assumption+)+
done
lemma inflationary_on_in_codom_FrelI:
assumes "inflationary_on (in_codom R1) R1 f1"
and "inflationary_on (in_codom R2) R2 f2"
and "inflationary_on (in_codom R3) R3 f3"
shows "inflationary_on (in_codom R) R f"
apply (unfold R_def f_def)
apply (rule inflationary_onI)
apply (subst (asm) in_codom_Frel_eq_Fpred_in_codom)
apply (erule FpredE)
apply (subst Frel_Fmap_eq2)
apply (rule Frel_refl_strong)
apply (rule inflationary_onD[where ?R=R1] inflationary_onD[where ?R=R2]
inflationary_onD[where ?R=R3],
rule assms,
assumption+)+
done
end
context
fixes R1 :: "'a ⇒ 'a ⇒ bool" and R2 :: "'b ⇒ 'b ⇒ bool" and R3 :: "'c ⇒ 'c ⇒ bool"
and f1 :: "'a ⇒ 'a" and f2 :: "'b ⇒ 'b" and f3 :: "'c ⇒ 'c"
and R :: "('d, 'a, 'b, 'c) F ⇒ ('d, 'a, 'b, 'c) F ⇒ bool"
and f :: "('d, 'a, 'b, 'c) F ⇒ ('d, 'a, 'b, 'c) F"
defines "R ≡ Frel R1 R2 R3" and "f ≡ Fmap f1 f2 f3"
begin
lemma inflationary_on_in_field_FrelI:
assumes "inflationary_on (in_field R1) R1 f1"
and "inflationary_on (in_field R2) R2 f2"
and "inflationary_on (in_field R3) R3 f3"
shows "inflationary_on (in_field R) R f"
apply (unfold R_def f_def)
apply (subst in_field_eq_in_dom_sup_in_codom)
apply (subst inflationary_on_sup_eq)
apply (unfold inf_apply)
apply (subst inf_bool_def)
apply (rule conjI;
rule inflationary_on_in_dom_FrelI inflationary_on_in_codom_FrelI;
rule inflationary_on_if_le_pred_if_inflationary_on,
rule assms,
rule le_predI,
rule in_field_if_in_dom in_field_if_in_codom,
assumption)
done
lemma deflationary_on_in_dom_FrelI:
assumes "deflationary_on (in_dom R1) R1 f1"
and "deflationary_on (in_dom R2) R2 f2"
and "deflationary_on (in_dom R3) R3 f3"
shows "deflationary_on (in_dom R) R f"
apply (unfold R_def f_def)
apply (subst deflationary_on_eq_inflationary_on_rel_inv)
apply (subst in_codom_rel_inv_eq_in_dom[symmetric])
apply (unfold Frel_rel_inv_eq_rel_inv_Frel[symmetric])
apply (rule inflationary_on_in_codom_FrelI;
subst deflationary_on_eq_inflationary_on_rel_inv[symmetric],
subst in_codom_rel_inv_eq_in_dom,
rule assms)
done
lemma deflationary_on_in_codom_FrelI:
assumes "deflationary_on (in_codom R1) R1 f1"
and "deflationary_on (in_codom R2) R2 f2"
and "deflationary_on (in_codom R3) R3 f3"
shows "deflationary_on (in_codom R) R f"
apply (unfold R_def f_def)
apply (subst deflationary_on_eq_inflationary_on_rel_inv)
apply (subst in_dom_rel_inv_eq_in_codom[symmetric])
apply (unfold Frel_rel_inv_eq_rel_inv_Frel[symmetric])
apply (rule inflationary_on_in_dom_FrelI;
subst deflationary_on_eq_inflationary_on_rel_inv[symmetric],
subst in_dom_rel_inv_eq_in_codom,
rule assms)
done
end
context
fixes R1 :: "'a ⇒ 'a ⇒ bool" and R2 :: "'b ⇒ 'b ⇒ bool" and R3 :: "'c ⇒ 'c ⇒ bool"
and f1 :: "'a ⇒ 'a" and f2 :: "'b ⇒ 'b" and f3 :: "'c ⇒ 'c"
and R :: "('d, 'a, 'b, 'c) F ⇒ ('d, 'a, 'b, 'c) F ⇒ bool"
and f :: "('d, 'a, 'b, 'c) F ⇒ ('d, 'a, 'b, 'c) F"
defines "R ≡ Frel R1 R2 R3" and "f ≡ Fmap f1 f2 f3"
begin
lemma deflationary_on_in_field_FrelI:
assumes "deflationary_on (in_field R1) R1 f1"
and "deflationary_on (in_field R2) R2 f2"
and "deflationary_on (in_field R3) R3 f3"
shows "deflationary_on (in_field R) R f"
apply (unfold R_def f_def)
apply (subst deflationary_on_eq_inflationary_on_rel_inv)
apply (subst in_field_rel_inv_eq_in_field[symmetric])
apply (unfold Frel_rel_inv_eq_rel_inv_Frel[symmetric])
apply (rule inflationary_on_in_field_FrelI;
subst deflationary_on_eq_inflationary_on_rel_inv[symmetric],
subst in_field_rel_inv_eq_in_field,
rule assms)
done
lemma rel_equivalence_on_in_field_FrelI:
assumes "rel_equivalence_on (in_field R1) R1 f1"
and "rel_equivalence_on (in_field R2) R2 f2"
and "rel_equivalence_on (in_field R3) R3 f3"
shows "rel_equivalence_on (in_field R) R f"
apply (unfold R_def f_def)
apply (subst rel_equivalence_on_eq)
apply (unfold inf_apply)
apply (subst inf_bool_def)
apply (insert assms)
apply (elim rel_equivalence_onE)
apply (rule conjI)
apply (rule inflationary_on_in_field_FrelI; assumption)
apply (fold R_def f_def)
apply (rule deflationary_on_in_field_FrelI; assumption)
done
end
context transport_natural_functor
begin
lemmas inflationary_on_in_field_unitI = inflationary_on_in_field_FrelI
[of L1 "η⇩1" L2 "η⇩2" L3 "η⇩3", folded transport_defs unit_eq_Fmap]
lemmas deflationary_on_in_field_unitI = deflationary_on_in_field_FrelI
[of L1 "η⇩1" L2 "η⇩2" L3 "η⇩3", folded transport_defs unit_eq_Fmap]
lemmas rel_equivalence_on_in_field_unitI = rel_equivalence_on_in_field_FrelI
[of L1 "η⇩1" L2 "η⇩2" L3 "η⇩3", folded transport_defs unit_eq_Fmap]
interpretation flip :
transport_natural_functor R1 L1 r1 l1 R2 L2 r2 l2 R3 L3 r3 l3
rewrites "flip.unit ≡ ε" and "flip.t1.unit ≡ ε⇩1"
and "flip.t2.unit ≡ ε⇩2" and "flip.t3.unit ≡ ε⇩3"
by (simp_all only: order_functors.flip_counit_eq_unit)
lemma order_equivalenceI:
assumes "((≤⇘L1⇙) ≡⇩o (≤⇘R1⇙)) l1 r1"
and "((≤⇘L2⇙) ≡⇩o (≤⇘R2⇙)) l2 r2"
and "((≤⇘L3⇙) ≡⇩o (≤⇘R3⇙)) l3 r3"
shows "((≤⇘L⇙) ≡⇩o (≤⇘R⇙)) l r"
apply (insert assms)
apply (elim order_functors.order_equivalenceE)
apply (rule order_equivalenceI;
rule mono_wrt_rel_leftI
flip.mono_wrt_rel_leftI
rel_equivalence_on_in_field_unitI
flip.rel_equivalence_on_in_field_unitI;
assumption)
done
end
end