Theory Multirelations
theory Multirelations
imports Power_Allegories_Multirelations
begin
lemma nonempty_set_card:
assumes "finite S"
shows "S ≠ {} ⟷ card S ≥ 1"
using assms card_0_eq by fastforce
no_notation one_class.one (‹1›)
no_notation times_class.times (infixl ‹*› 70)
no_notation rel_fdia (‹(|_⟩_)› [61,81] 82)
no_notation rel_bdia (‹(⟨_|_)› [61,81] 82)
no_notation rel_fbox (‹(|_]_)› [61,81] 82)
no_notation rel_bbox (‹([_|_)› [61,81] 82)
declare s_prod_pa_def [mr_simp]
notation s_prod (infixl ‹*› 70)
notation s_id (‹1›)
lemma sp_oi_subdist:
"(P ∩ Q) * (R ∩ S) ⊆ P * R"
unfolding s_prod_def by blast
lemma sp_oi_subdist_2:
"(P ∩ Q) * (R ∩ S) ⊆ (P * R) ∩ (Q * S)"
unfolding s_prod_def by blast
section ‹Inner Structure›
subsection ‹Inner union, inner intersection and inner complement›
abbreviation "inner_union" (infixl ‹∪∪› 65)
where "inner_union ≡ p_prod"
definition inner_intersection :: "('a,'b) mrel ⇒ ('a,'b) mrel ⇒ ('a,'b) mrel" (infixl ‹∩∩› 65) where
"R ∩∩ S ≡ { (a,B) . ∃C D . B = C ∩ D ∧ (a,C) ∈ R ∧ (a,D) ∈ S }"
definition inner_complement :: "('a,'b) mrel ⇒ ('a,'b) mrel" (‹∼ _› [80] 80) where
"∼R ≡ { (a,B) . (a,-B) ∈ R }"
abbreviation "iu_unit" (‹1⇩∪⇩∪›)
where "1⇩∪⇩∪ ≡ p_id"
definition ii_unit :: "('a,'a) mrel" (‹1⇩∩⇩∩›)
where "1⇩∩⇩∩ ≡ { (a,UNIV) | a . True }"
declare inner_intersection_def [mr_simp] inner_complement_def [mr_simp] ii_unit_def [mr_simp]
lemma iu_assoc:
"(R ∪∪ S) ∪∪ T = R ∪∪ (S ∪∪ T)"
by (simp add: p_prod_assoc)
lemma iu_commute:
"R ∪∪ S = S ∪∪ R"
by (simp add: p_prod_comm)
lemma iu_unit:
"R ∪∪ 1⇩∪⇩∪ = R"
by simp
lemma ii_assoc:
"(R ∩∩ S) ∩∩ T = R ∩∩ (S ∩∩ T)"
apply (clarsimp simp: mr_simp)
by (metis (no_types, opaque_lifting) semilattice_inf_class.inf_assoc)
lemma ii_commute:
"R ∩∩ S = S ∩∩ R"
by (auto simp: mr_simp)
lemma ii_unit [simp]:
"R ∩∩ 1⇩∩⇩∩ = R"
by (simp add: mr_simp)
lemma pa_ic:
"∼(R ⊗ ∼S) = R ⊗ S"
by (clarsimp simp: mr_simp)
lemma ic_involutive [simp]:
"∼∼R = R"
by (simp add: mr_simp)
lemma ic_injective:
"∼R = ∼S ⟹ R = S"
by (metis ic_involutive)
lemma ic_antidist_iu:
"∼(R ∪∪ S) = ∼R ∩∩ ∼S"
apply (clarsimp simp: mr_simp)
by (metis (no_types, opaque_lifting) compl_sup double_compl)
lemma ic_antidist_ii:
"∼(R ∩∩ S) = ∼R ∪∪ ∼S"
by (metis ic_antidist_iu ic_involutive)
lemma ic_iu_unit [simp]:
"∼1⇩∪⇩∪ = 1⇩∩⇩∩"
unfolding ii_unit_def p_id_def inner_complement_def by force
lemma ic_ii_unit [simp]:
"∼1⇩∩⇩∩ = 1⇩∪⇩∪"
by (metis ic_involutive ic_iu_unit)
lemma ii_unit_split_iu [simp]:
"1 ∪∪ ∼1 = 1⇩∩⇩∩"
by (force simp: mr_simp)
lemma aux_1:
"B = {a} ∩ D ⟹ -D = {a} ⟹ B = {}"
by auto
lemma iu_unit_split_ii [simp]:
"1 ∩∩ ∼1 = 1⇩∪⇩∪"
by (metis ic_antidist_iu ic_ii_unit ic_involutive ii_commute ii_unit_split_iu)
lemma iu_right_dist_ou:
"(R ∪ S) ∪∪ T = (R ∪∪ T) ∪ (S ∪∪ T)"
unfolding p_prod_def by auto
lemma ii_right_dist_ou:
"(R ∪ S) ∩∩ T = (R ∩∩ T) ∪ (S ∩∩ T)"
by (auto simp: mr_simp)
lemma iu_left_isotone:
"R ⊆ S ⟹ R ∪∪ T ⊆ S ∪∪ T"
by (metis iu_right_dist_ou subset_Un_eq)
lemma iu_right_isotone:
"R ⊆ S ⟹ T ∪∪ R ⊆ T ∪∪ S"
by (simp add: iu_commute iu_left_isotone)
lemma iu_isotone:
"R ⊆ S ⟹ P ⊆ Q ⟹ R ∪∪ P ⊆ S ∪∪ Q"
by (meson dual_order.trans iu_left_isotone iu_right_isotone)
lemma ii_left_isotone:
"R ⊆ S ⟹ R ∩∩ T ⊆ S ∩∩ T"
by (metis ii_right_dist_ou subset_Un_eq)
lemma ii_right_isotone:
"R ⊆ S ⟹ T ∩∩ R ⊆ T ∩∩ S"
by (simp add: ii_commute ii_left_isotone)
lemma ii_isotone:
"R ⊆ S ⟹ P ⊆ Q ⟹ R ∩∩ P ⊆ S ∩∩ Q"
by (meson ii_left_isotone ii_right_isotone order_trans)
lemma iu_right_subdist_ii:
"(R ∩∩ S) ∪∪ T ⊆ (R ∪∪ T) ∩∩ (S ∪∪ T)"
apply (clarsimp simp: mr_simp)
by (metis sup_inf_distrib2)
lemma ii_right_subdist_iu:
"(R ∪∪ S) ∩∩ T ⊆ (R ∩∩ T) ∪∪ (S ∩∩ T)"
apply (clarsimp simp: mr_simp)
by (metis inf_sup_distrib2)
lemma ic_isotone:
"R ⊆ S ⟹ ∼R ⊆ ∼S"
by (simp add: inner_complement_def subset_eq)
lemma ic_bot [simp]:
"∼{} = {}"
by (simp add: mr_simp)
lemma ic_top [simp]:
"∼U = U"
by (auto simp: mr_simp)
lemma ic_dist_ou:
"∼(R ∪ S) = ∼R ∪ ∼S"
by (auto simp: mr_simp)
lemma ic_dist_oi:
"∼(R ∩ S) = ∼R ∩ ∼S"
by (auto simp: mr_simp)
lemma ic_dist_oc:
"∼-R = -(∼R)"
by (auto simp: mr_simp)
lemma ii_sub_idempotent:
"R ⊆ R ∩∩ R"
unfolding inner_intersection_def by force
definition inner_Union :: "('i ⇒ ('a,'b) mrel) ⇒ 'i set ⇒ ('a,'b) mrel" (‹⋃⋃_|_› [80,80] 80) where
"⋃⋃X|I ≡ { (a,B) . ∃f . B = (⋃i∈I . f i) ∧ (∀i∈I . (a,f i) ∈ X i) }"
definition inner_Intersection :: "('i ⇒ ('a,'b) mrel) ⇒ 'i set ⇒ ('a,'b) mrel" (‹⋂⋂_|_› [80,80] 80) where
"⋂⋂X|I ≡ { (a,B) . ∃f . B = (⋂i∈I . f i) ∧ (∀i∈I . (a,f i) ∈ X i) }"
declare inner_Union_def [mr_simp] inner_Intersection_def [mr_simp]
lemma iU_empty:
"⋃⋃X|{} = 1⇩∪⇩∪"
by (auto simp: mr_simp)
lemma iI_empty:
"⋂⋂X|{} = 1⇩∩⇩∩"
by (auto simp: mr_simp)
lemma ic_antidist_iU:
"∼⋃⋃X|I = ⋂⋂(inner_complement o X)|I"
apply (rule antisym)
apply (clarsimp simp: mr_simp)
apply (metis (mono_tags, lifting) Compl_UN double_compl)
by (clarsimp simp: mr_simp) blast
lemma ic_antidist_iI:
"∼⋂⋂X|I = ⋃⋃(inner_complement o X)|I"
apply (rule antisym)
apply (clarsimp simp: mr_simp)
apply (metis Compl_INT double_complement)
by (clarsimp simp: mr_simp) blast
lemma iu_right_dist_oU:
"⋃X ∪∪ T = (⋃R∈X . R ∪∪ T)"
by (clarsimp simp: mr_simp) blast
lemma ii_right_dist_oU:
"⋃X ∩∩ T = (⋃R∈X . R ∩∩ T)"
by (clarsimp simp: mr_simp) blast
lemma iu_right_subdist_iI:
"⋂⋂X|I ∪∪ T ⊆ ⋂⋂(λi . X i ∪∪ T)|I"
apply (clarsimp simp: mr_simp)
by (metis INT_simps(6))
lemma ii_right_subdist_iU:
"⋃⋃X|I ∩∩ T ⊆ ⋃⋃(λi . X i ∩∩ T)|I"
by (clarsimp simp: mr_simp, metis UN_extend_simps(4))
lemma ic_dist_oU:
"∼⋃X = ⋃(inner_complement ` X)"
by (auto simp: mr_simp)
lemma ic_dist_oI:
"∼⋂X = ⋂(inner_complement ` X)"
by (auto simp: mr_simp)
lemma sp_left_subdist_iU:
"R * (⋃⋃X|I) ⊆ ⋃⋃(λi . R * X i)|I"
apply (clarsimp simp: mr_simp)
subgoal for a B f proof -
assume 1: "(a,B) ∈ R"
assume "∀b∈B . ∃g . f b = ⋃(g ` I) ∧ (∀i∈I . (b,g i) ∈ X i)"
from this obtain g where 2: "∀b∈B . f b = ⋃(g b ` I) ∧ (∀i∈I . (b,g b i) ∈ X i)"
by metis
hence 3: "⋃(f ` B) = (⋃b∈B . ⋃(g b ` I))"
by (meson SUP_cong)
let ?h = "λi . ⋃b∈B . g b i"
have "⋃(f ` B) = ⋃(?h ` I) ∧ (∀i∈I . ∃B . (a,B) ∈ R ∧ (∃f . (∀b∈B . (b,f b) ∈ X i) ∧ ?h i = ⋃(f ` B)))"
using 1 2 3 by (metis SUP_commute)
thus ?thesis
by auto
qed
done
lemma sp_right_subdist_iU:
"(⋃⋃X|I) * R ⊆ ⋃⋃(λi . X i * R)|I"
by (clarsimp simp: mr_simp, blast)
lemma sp_right_dist_iU:
assumes "∀J::'a set . J ≠ {} ⟶ (⋃⋃(λj . R)|J) ⊆ R"
shows "(⋃⋃X|I) * R = ⋃⋃(λi . X i * R)|(I::'a set)"
apply (rule antisym)
using sp_right_subdist_iU apply blast
apply (clarsimp simp: mr_simp)
subgoal for a f proof -
assume "∀i∈I . ∃B . (a,B) ∈ X i ∧ (∃g . (∀b∈B . (b,g b) ∈ R) ∧ f i = ⋃(g ` B))"
from this obtain B g where 1: "∀i∈I . (a,B i) ∈ X i ∧ (∀b∈B i . (b,g i b) ∈ R) ∧ f i = ⋃(g i ` B i)"
by metis
let ?B = "⋃(B ` I)"
let ?g = "λb . ⋃{ g i b | i . i∈I ∧ b ∈ B i }"
have "∀b∈?B . (b,?g b) ∈ R"
proof (rule ballI)
fix b
let ?I = "{ i | i . i∈I ∧ b ∈ B i }"
assume 2: "b ∈ ⋃(B ` I)"
have "(b,?g b) ∈ ⋃⋃(λj . R)|?I"
apply (clarsimp simp: mr_simp)
apply (rule exI[of _ "λi . g i b"])
using 1 by blast
thus "(b,?g b) ∈ R"
using 2 by (smt (verit) assms UN_E empty_Collect_eq subset_iff)
qed
hence "?B = ⋃(B ` I) ∧ (∀i∈I . (a,B i) ∈ X i) ∧ (∀b∈?B . (b,?g b) ∈ R) ∧ ⋃(f ` I) = ⋃(?g ` ?B)"
using 1 by auto
thus "∃B . (∃f . B = ⋃(f ` I) ∧ (∀i∈I . (a,f i) ∈ X i)) ∧ (∃g . (∀b∈B . (b,g b) ∈ R) ∧ ⋃(f ` I) = ⋃(g ` B))"
by (metis (no_types, lifting))
qed
done
subsection ‹Dual›
abbreviation dual :: "('a,'b) mrel ⇒ ('a,'b) mrel" (‹_⇧d› [100] 100)
where "R⇧d ≡ ∼-R"
lemma dual:
"R⇧d = { (a,B) . (a,-B) ∉ R }"
by (simp add: inner_complement_def)
declare dual [mr_simp]
lemma dual_antitone:
"R ⊆ S ⟹ S⇧d ⊆ R⇧d"
by (simp add: ic_isotone)
lemma ic_oc_dual:
"∼R = -R⇧d"
by (simp add: ic_dist_oc)
lemma dual_involutive [simp]:
"R⇧d⇧d = R"
by (simp add: ic_dist_oc)
lemma dual_antidist_ou:
"(R ∪ S)⇧d = R⇧d ∩ S⇧d"
by (simp add: ic_dist_oi)
lemma dual_antidist_oi:
"(R ∩ S)⇧d = R⇧d ∪ S⇧d"
by (simp add: ic_dist_ou)
lemma dual_dist_oc:
"(-R)⇧d = -R⇧d"
by (fact ic_dist_oc)
lemma dual_dist_ic:
"(∼R)⇧d = ∼R⇧d"
by (simp add: ic_dist_oc)
lemma dual_antidist_oU:
"(⋃X)⇧d = ⋂(dual ` X)"
by (simp add: ic_dist_oI uminus_Sup)
lemma dual_antidist_oI:
"(⋂X)⇧d = ⋃(dual ` X)"
by (simp add: ic_dist_oU uminus_Inf)
subsection ‹Co-composition›
definition co_prod :: "('a,'b) mrel ⇒ ('b,'c) mrel ⇒ ('a,'c) mrel" (infixl ‹⊙› 70) where
"R ⊙ S ≡ { (a,C) . ∃B . (a,B) ∈ R ∧ (∃f . (∀b ∈ B . (b,f b) ∈ S) ∧ C = ⋂{ f b | b . b ∈ B }) }"
lemma co_prod_im:
"R ⊙ S = { (a,C) . ∃B . (a,B) ∈ R ∧ (∃f . (∀b ∈ B . (b,f b) ∈ S) ∧ C = ⋂((λx . f x) ` B)) }"
by (auto simp: co_prod_def)
lemma co_prod_iff:
"(a,C) ∈ (R ⊙ S) ⟷ (∃B . (a,B) ∈ R ∧ (∃f . (∀b ∈ B . (b,f b) ∈ S) ∧ C = ⋂{ f b | b . b ∈ B }))"
by (unfold co_prod_im, auto)
declare co_prod_im [mr_simp]
lemma co_prod:
"R ⊙ S = ∼(R * ∼S)"
apply (clarsimp simp: mr_simp)
by (smt (verit) Collect_cong Compl_INT Compl_UN case_prodI2 double_complement old.prod.case)
lemma cp_left_isotone:
"R ⊆ S ⟹ R ⊙ T ⊆ S ⊙ T"
by (simp add: co_prod ic_isotone s_prod_isol)
lemma cp_right_isotone:
"R ⊆ S ⟹ T ⊙ R ⊆ T ⊙ S"
by (smt (verit) co_prod_iff in_mono subrelI)
lemma cp_isotone:
"R ⊆ S ⟹ P ⊆ Q ⟹ R ⊙ P ⊆ S ⊙ Q"
by (meson cp_left_isotone cp_right_isotone order_trans)
lemma ic_dist_cp:
"∼(R ⊙ S) = R * ∼S"
by (simp add: co_prod)
lemma ic_dist_sp:
"∼(R * S) = R ⊙ ∼S"
by (simp add: co_prod)
lemma ic_cp_ic_unit:
"∼R = R ⊙ ∼1"
by (simp add: co_prod)
lemma cp_left_zero [simp]:
"{} ⊙ R = {}"
by (simp add: co_prod_im)
lemma cp_left_unit [simp]:
"1 ⊙ R = R"
by (simp add: co_prod)
lemma cp_ic_unit [simp]:
"∼1 ⊙ ∼1 = 1"
using ic_cp_ic_unit ic_involutive by blast
lemma cp_right_dist_ou:
"(R ∪ S) ⊙ T = (R ⊙ T) ∪ (S ⊙ T)"
by (simp add: co_prod ic_dist_ou s_prod_distr)
lemma cp_left_iu_unit [simp]:
"1⇩∪⇩∪ ⊙ R = 1⇩∩⇩∩"
by (simp add: co_prod)
lemma cp_right_ii_unit:
"R ⊙ 1⇩∩⇩∩ ⊆ R ∪∪ ∼R"
apply (clarsimp simp: mr_simp)
by (metis double_compl sup_compl_top)
lemma sp_right_iu_unit:
"R * 1⇩∪⇩∪ ⊆ R ∩∩ ∼R"
apply (clarsimp simp: mr_simp)
by (metis Compl_disjoint double_complement)
lemma cp_left_subdist_ii:
"R ⊙ (S ∩∩ T) ⊆ (R ⊙ S) ∩∩ (R ⊙ T)"
by (metis cl3 co_prod ic_antidist_ii ic_antidist_iu ic_isotone)
lemma cp_right_subantidist_iu:
"(R ∪∪ S) ⊙ T ⊆ (R ⊙ T) ∩∩ (S ⊙ T)"
by (metis co_prod ic_antidist_iu ic_isotone seq_conc_subdistr)
lemma cp_right_antidist_iu:
assumes "T ∩∩ T ⊆ T"
shows "(R ∪∪ S) ⊙ T = (R ⊙ T) ∩∩ (S ⊙ T)"
by (smt (verit) assms cl4 co_prod cp_right_subantidist_iu ic_antidist_ii ic_involutive ic_isotone subset_antisym)
lemma cp_right_dist_oU:
"⋃X ⊙ T = (⋃R∈X . R ⊙ T)"
by (auto simp: mr_simp)
lemma cp_left_subdist_iI:
"R ⊙ (⋂⋂X|I) ⊆ ⋂⋂(λi . R ⊙ X i)|I"
proof -
have "R ⊙ (⋂⋂X|I) = ∼(R * (⋃⋃(inner_complement o X)|I))"
by (simp add: co_prod ic_antidist_iI)
also have "... ⊆ ∼(⋃⋃(λi . R * ∼(X i))|I)"
apply (rule ic_isotone)
using sp_left_subdist_iU by force
also have "... = ⋂⋂(λi . R ⊙ X i)|I"
apply (subst ic_antidist_iU)
by (metis co_prod comp_apply)
finally show ?thesis
.
qed
lemma cp_right_subantidist_iU:
"(⋃⋃X|I) ⊙ R ⊆ ⋂⋂(λi . X i ⊙ R)|I"
proof -
have "(⋃⋃X|I) ⊙ R = ∼((⋃⋃X|I) * ∼R)"
by (simp add: co_prod)
also have "... ⊆ ∼((⋃⋃(λi . X i * ∼R)|I))"
by (simp add: ic_isotone sp_right_subdist_iU)
also have "... = ⋂⋂(λi . X i ⊙ R)|I"
apply (subst ic_antidist_iU)
by (metis co_prod comp_apply)
finally show ?thesis
.
qed
lemma cp_right_antidist_iU:
assumes "∀J::'a set . J ≠ {} ⟶ (⋂⋂(λj . R)|J) ⊆ R"
shows "(⋃⋃X|I) ⊙ R = ⋂⋂(λi . X i ⊙ R)|(I::'a set)"
proof -
have 1: "⋀J . ⋃⋃(λj. ∼ R)|J = ∼⋂⋂(λj . R)|J"
apply (subst ic_antidist_iI)
by (metis comp_apply)
have "(⋃⋃X|I) ⊙ R = ∼((⋃⋃X|I) * ∼R)"
by (simp add: co_prod)
also have "... = ∼((⋃⋃(λi . X i * ∼R)|I))"
by (simp add: 1 assms sp_right_dist_iU ic_isotone)
also have "... = ⋂⋂(λi . X i ⊙ R)|I"
apply (subst ic_antidist_iU)
by (metis co_prod comp_apply)
finally show ?thesis
.
qed
subsection ‹Inner order›
definition inner_order_iu :: "'a × 'b set ⇒ 'a × 'b set ⇒ bool" (infix ‹≼⇩∪⇩∪› 50) where
"x ≼⇩∪⇩∪ y ≡ fst x = fst y ∧ snd x ⊆ snd y"
definition inner_order_ii :: "'a × 'b set ⇒ 'a × 'b set ⇒ bool" (infix ‹≼⇩∩⇩∩› 50) where
"x ≼⇩∩⇩∩ y ≡ fst x = fst y ∧ snd x ⊇ snd y"
lemma inner_order_dual:
"x ≼⇩∪⇩∪ y ⟷ y ≼⇩∩⇩∩ x"
by (metis inner_order_ii_def inner_order_iu_def)