Theory Relational_Properties

section ‹Properties of Binary Relations›

theory Relational_Properties

imports Main

begin

text ‹This is a general-purpose theory for enrichments of Rel, which is still quite basic,
but helpful for developing properties of multirelations.›

notation relcomp (infixl ‹;› 75)
notation converse (‹_⇧⌣› [1000] 999)

type_synonym ('a,'b) rel = "('a × 'b) set"

lemma modular_law: "R ; S ∩ T ⊆ (R ∩ T ; S⇧⌣) ; S"
  by blast

lemma compl_conv: "-(R⇧⌣) = (-R)⇧⌣"
  by fastforce

definition top :: "('a,'b) rel" where
  "top = {(a,b) |a b. True}"

abbreviation "neg R ≡ Id ∩ -R"


subsection ‹Univalence, totality, determinism, and related properties›

definition univalent :: "('a,'b) rel ⇒ bool" where
  "univalent R = (R⇧⌣ ; R ⊆ Id)"

definition total :: "('a,'b) rel ⇒ bool" where
  "total R = (Id ⊆ R ; R⇧⌣)"

definition injective :: "('a,'b) rel ⇒ bool" where
  "injective R = (R ; R⇧⌣ ⊆ Id)"

definition surjective :: "('a,'b) rel ⇒ bool" where
  "surjective R = (Id ⊆ R⇧⌣ ; R)"

definition deterministic :: "('a,'b) rel ⇒ bool" where
  "deterministic R = (univalent R ∧ total R)"

definition bijective :: "('a,'b) rel ⇒ bool" where
  "bijective R = (injective R ∧ surjective R)"

lemma univalent_set: "univalent R = (∀a b c. (a,b) ∈ R ∧ (a,c) ∈ R ⟶ b = c)"
  unfolding univalent_def converse_unfold Id_def by force

text ‹Univalent relations feature as single-valued relations in Main.›

lemma univ_single_valued: "univalent R = single_valued R"
  unfolding univalent_set single_valued_def by auto

lemma total_set: "total R = (∀a. ∃b. (a,b) ∈ R)"
  unfolding total_def converse_unfold Id_def by force

lemma total_var: "total R = (R ; top = top)"
  unfolding total_set top_def by force

lemma deterministic_set: "deterministic R = (∀a . ∃!B . (a,B) ∈ R)"
  unfolding deterministic_def univalent_set total_set by force

lemma deterministic_var1: "deterministic R = (R ; -Id = -R)"
  unfolding deterministic_set Id_def by force

lemma deterministic_var2: "deterministic R = (∀S. R ; -S = -(R ; S))"
  unfolding deterministic_set by (standard, force, blast)

lemma inj_univ: "injective R = univalent (R⇧⌣)"
  by (simp add: injective_def univalent_def)

lemma injective_set: "injective S = (∀a b c. (a,c) ∈ S ∧ (b,c) ∈ S ⟶ a = b)"
  by (meson converseD converseI inj_univ univalent_set)

lemma surj_tot: "surjective R = total (R⇧⌣)"
  by (simp add: surjective_def total_def)

lemma surjective_set: "surjective S = (∀b. ∃a. (a,b) ∈ S)"
  by (simp add: surj_tot total_set)

lemma surj_var: "surjective R = (R⇧⌣ ; top = top)"
  by (simp add: surj_tot total_var)

lemma bij_det: "bijective R = deterministic (R⇧⌣)"
  by (simp add: bijective_def deterministic_def inj_univ surj_tot)

lemma univ_relcomp: "univalent R ⟹ univalent S ⟹ univalent (R ; S)"
  by (simp add: single_valued_relcomp univ_single_valued)

lemma tot_relcomp: "total R ⟹ total S ⟹ total (R ; S)"
  by (meson relcomp.simps total_set)

lemma det_relcomp: "deterministic R ⟹ deterministic S ⟹ deterministic (R ; S)"
  by (simp add: deterministic_def tot_relcomp univ_relcomp)

lemma inj_relcomp: "injective R ⟹ injective S ⟹ injective (R ; S)"
  by (simp add: converse_relcomp inj_univ univ_relcomp)

lemma surj_relcomp: "surjective R ⟹ surjective S ⟹ surjective (R ; S)"
  by (simp add: converse_relcomp surj_tot tot_relcomp)

lemma bij_relcomp: "bijective R ⟹ bijective S ⟹ bijective (R ; S)"
  by (simp add: bijective_def inj_relcomp surj_relcomp)

lemma det_Id: "deterministic Id"
  by (simp add: deterministic_var1)

lemma bij_Id: "bijective Id"
  by (simp add: bij_det det_Id)

lemma tot_top: "total top"
  by (simp add: top_def total_set)

lemma tot_surj: "surjective top"
  by (simp add: surjective_set top_def)

lemma det_meet_distl: "univalent R ⟹ R ; (S ∩ T) = R ; S ∩ R ; T"
  unfolding univalent_set relcomp_def relcompp_apply by force

lemma inj_meet_distr: "injective T ⟹ (R ∩ S) ; T = R ; T ∩ S ; T"
  unfolding injective_def converse_def Id_def relcomp.simps by force

lemma univ_modular: "univalent S ⟹ R ; S ∩ T = (R ∩ T ; S⇧⌣) ; S"
  unfolding univalent_set converse_unfold relcomp.simps by force


subsection ‹Inverse image and the diagonal and graph functors›

definition Invim :: "('a,'b) rel ⇒ 'b set ⇒ 'a set" where
  "Invim R = Image (R⇧⌣)"

definition Delta :: "'a set ⇒ ('a,'a) rel" (‹Δ›) where
  "Δ P = {(p,p) |p. p ∈ P}"

definition Grph :: "('a ⇒ 'b) ⇒ ('a,'b) rel" where
  "Grph f = {(x,y). y = f x}"

lemma Image_Grph [simp]: "Image ∘ Grph = image"
  unfolding Image_def Grph_def image_def by auto

subsection ‹Relational domain, codomain and modalities›

text ‹Domain and codomain (range) maps have been defined in Main, but they return sets instead of relations.›

definition dom :: "('a,'b) rel ⇒ ('a,'a) rel" where
  "dom R = Id ∩ R ; R⇧⌣"

definition cod :: "('a,'b) rel ⇒ ('b,'b) rel" where
  "cod R = dom (R⇧⌣)"

definition rel_fdia :: "('a,'b) rel ⇒ ('b,'b) rel ⇒ ('a,'a) rel" (‹(|_⟩_)› [61,81] 82) where
  "|R⟩ Q = dom (R ; dom Q)"

definition rel_bdia :: "('a,'b) rel ⇒ ('a,'a) rel ⇒ ('b,'b) rel" (‹(⟨_|_)› [61,81] 82) where
  "rel_bdia R = rel_fdia (R⇧⌣)"

definition rel_fbox :: "('a,'b) rel ⇒ ('b,'b) rel ⇒ ('a,'a) rel" (‹(|_]_)› [61,81] 82) where
  "|R]Q = neg (dom (R ; neg (dom Q)))"

definition rel_bbox :: "('a,'b) rel ⇒ ('a,'a) rel ⇒ ('b,'b) rel" (‹([_|_)› [61,81] 82) where
  "rel_bbox R = rel_fbox (R⇧⌣)"

lemma rel_bdia_def_var: "rel_bdia = rel_fdia ∘ converse"
  unfolding rel_fdia_def fun_eq_iff comp_def rel_bdia_def by simp

lemma dom_set: "dom R = {(a,a) |a. ∃b. (a,b) ∈ R}"
  unfolding dom_def Id_def converse_unfold relcomp_unfold by force

lemma dom_Domain: "dom = Δ ∘ Domain"
  unfolding fun_eq_iff dom_set Delta_def Domain_def by clarsimp blast

lemma cod_set: "cod R = {(b,b) |b. ∃a. (a,b) ∈ R}"
  by (smt (verit) Collect_cong cod_def converseD converseI dom_set)

lemma cod_Range: "cod = Δ ∘ Range"
  unfolding fun_eq_iff cod_set Delta_def Range_def by clarsimp blast

lemma rel_fdia_set: "|R⟩ Q = {(a,a) |a. ∃b. (a,b) ∈ R ∧ (b,b) ∈ dom Q}"
  unfolding rel_fdia_def dom_set relcomp_unfold by force

lemma rel_bdia_set: "⟨R| P = {(b,b) |b. ∃a. (a,b) ∈ R ∧ (a,a) ∈ dom P}"
  by (smt (verit, best) Collect_cong converseD converseI rel_bdia_def rel_fdia_set)

lemma rel_fbox_set: "|R] Q = {(a,a) |a. ∀b. (a,b) ∈ R ⟶ (b,b) ∈ dom Q}"
  unfolding rel_fbox_def dom_set relcomp_unfold by force

lemma rel_bbox_set: "[R| P = {(b,b) |b. ∀a. (a,b) ∈ R ⟶ (a,a) ∈ dom P}"
  by (smt (verit) Collect_cong converseD converseI rel_bbox_def rel_fbox_set)

lemma dom_alt_def: "dom R = Id ∩ R ; top"
  unfolding dom_set top_def Id_def by force

lemma dom_gla: "(dom R ⊆ Id ∩ S) = (R ⊆ (Id ∩ S) ; R)"
  unfolding dom_set Id_def relcomp_unfold by blast

lemma dom_gla_top: "(dom R ⊆ Id ∩ S) = (R ⊆ (Id ∩ S) ; top)"
  unfolding dom_set Id_def top_def relcomp_unfold by blast

lemma dom_subid: "(dom R = R) = (R = Id ∩ R)"
  by (metis (no_types, lifting) Id_O_R R_O_Id dom_alt_def dom_gla_top equalityD1 inf.absorb_iff2 inf.commute inf.idem le_inf_iff relcomp_mono)

lemma dom_cod: "(dom R = R) = (cod R = R)"
  by (metis dom_def cod_def converse_Id converse_Int converse_converse converse_relcomp)

lemma dom_top: "R ; top = dom R ; top"
  unfolding dom_set top_def by blast

lemma top_dom: "dom R = dom (R ; top)"
  unfolding dom_def top_def by blast

lemma cod_top: "cod R = Id ∩ top ; R"
  by (metis dom_def cod_def converse_Id converse_Int converse_converse converse_relcomp dom_alt_def surj_var tot_surj)

lemma dom_conv [simp]: "(dom R)⇧⌣ = dom R"
  by (simp add: dom_def converse_Int converse_relcomp)

lemma total_dom: "total R = (dom R = Id)"
  by (metis dom_def inf.orderE inf_le2 total_def)

lemma surj_cod: "surjective R = (cod R = Id)"
  by (simp add: cod_def surj_tot total_dom)

lemma fdia_demod: "( |R⟩ P ⊆ dom Q) = (R ; dom P ⊆ dom Q ; R)"
  unfolding rel_fdia_set dom_set relcomp_unfold by force

lemma bbox_demod: "(dom P ⊆ [R| Q) = (R ; dom P ⊆ dom Q ; R)"
  unfolding rel_bbox_set dom_def by force

lemma bdia_demod: "(⟨R| P ⊆ dom Q) = (dom P ; R ⊆ R ; dom Q)"
proof -
  have "(⟨R| P ⊆ dom Q) = ( |R⇧⌣⟩ P ⊆ dom Q)"
    by (simp add: rel_bdia_def)
  also have "… = ((R⇧⌣) ; dom P ⊆ dom Q ; (R⇧⌣))"
    by (simp add: fdia_demod)
  also have "… = (((dom P ; R)⇧⌣) ⊆ ((R ; dom Q)⇧⌣))"
    by (simp add: converse_relcomp)
  also have "… = (dom P ; R ⊆ R ; dom Q)"
    by simp
  finally show ?thesis.
qed

lemma fbox_demod: "(dom P ⊆ |R] Q) = (dom P ; R ⊆ R ; dom Q)"
  unfolding rel_fbox_set dom_set relcomp_unfold by force

lemma fdia_demod_top: "( |R⟩ P ⊆ dom Q) = (R ; dom P ; top ⊆ dom Q ; top)"
  by (metis dom_def dom_gla_top rel_fdia_def top_dom)

lemma bbox_demod_top: "(dom P ⊆ [R| Q) = (R ; dom P ; top ⊆ dom Q ; top)"
  unfolding rel_bbox_def rel_fbox_def dom_def top_def by force

lemma fdia_bbox_galois: "( |R⟩ P ⊆ dom Q) = (dom P ⊆ [R| Q)"
  by (meson bbox_demod_top fdia_demod_top)

lemma bdia_fbox_galois: "(⟨R| P ⊆ dom Q) = (dom P ⊆ |R] Q)"
  by (simp add: fdia_bbox_galois rel_bbox_def rel_bdia_def)

lemma fdia_bdia_conjugation: "( |R⟩ P ⊆ neg (dom Q)) = (⟨R| Q ⊆ neg (dom P))"
  unfolding rel_fdia_set rel_bdia_set dom_set by force

lemma bfox_bbox_conjugation: "(neg (dom Q) ⊆ |R] P) = (neg (dom P) ⊆ [R| Q)"
  unfolding rel_fbox_set rel_bbox_set dom_set by clarsimp blast


subsection ‹Residuation›

definition lres :: "('a,'c) rel ⇒ ('b,'c) rel ⇒ ('a,'b) rel" (infixl ‹⫽› 75)
  where "R ⫽ S = {(a,b). ∀c. (b,c) ∈ S ⟶ (a,c) ∈ R}"

definition rres :: "('c,'a) rel ⇒ ('c,'b) rel ⇒ ('a,'b) rel" (infixl ‹∖› 75)
  where "R ∖ S = {(b,a). ∀c. (c,b) ∈ R ⟶ (c,a) ∈ S}"

lemma rres_lres_conv: "R ∖ S = (S⇧⌣ ⫽ R⇧⌣)⇧⌣"
  unfolding rres_def lres_def by clarsimp fastforce

lemma lres_galois: "(R ; S ⊆ T) = (R ⊆ T ⫽ S)"
  unfolding lres_def by blast

lemma rres_galois: "(R ; S ⊆ T) = (S ⊆ R ∖ T)"
  by (metis converse_converse converse_mono converse_relcomp lres_galois rres_lres_conv)

lemma lres_compl: "R ⫽ S = -(-R ; S⇧⌣)"
  unfolding lres_def converse_unfold by force

lemma rres_compl: "R ∖ S = -(R⇧⌣ ; -S)"
  unfolding rres_def converse_unfold by force

lemma lres_simp [simp]: "(R ⫽ R) ; R = R"
  by (metis Id_O_R lres_galois relcomp_mono subsetI subsetI subset_antisym)

lemma rres_simp [simp]: "R ; (R ∖ R) = R"
  by (metis converse_converse converse_relcomp lres_simp rres_lres_conv)

lemma lres_curry: "R ⫽ (T ; S) = (R ⫽ S) ⫽ T"
  by (metis (no_types, opaque_lifting) O_assoc dual_order.refl lres_galois subset_antisym)

lemma rres_curry: "(R ; S) ∖ T = S ∖ (R ∖ T)"
  by (simp add: converse_relcomp lres_curry rres_lres_conv)

lemma lres_Id: "Id ⊆ R ⫽ R"
  unfolding lres_def Id_def by force

lemma det_lres: "deterministic R ⟹ (R ; S) ⫽ S = R ; (S ⫽ S)"
  by (metis (no_types, lifting) O_assoc deterministic_var2 lres_compl)

lemma det_rres: "deterministic (R⇧⌣) ⟹ S ∖ (S ; R) = (S ∖ S) ; R"
  by (simp add: converse_relcomp det_lres rres_lres_conv)

lemma rres_bij: "bijective S ⟹ (R ∖ T) ; S = R ∖ (T ; S)"
  unfolding bijective_def injective_set surjective_set relcomp_unfold cod_def Id_def rres_def by clarsimp blast

lemma lres_bij: "bijective S ⟹ (R ⫽ T⇧⌣) ; S = R ⫽ (T ; S)⇧⌣"
  unfolding bijective_def injective_set surjective_set relcomp_unfold cod_def Id_def lres_def converse_unfold by blast

lemma dom_rres_top: "(dom P ⊆ R ∖ (dom Q ; top)) = (dom P ; top ⊆ R ∖ (dom Q ; top))"
  unfolding dom_def top_def rres_def relcomp_unfold Id_def converse_unfold by clarsimp blast

lemma dom_rres_top_var: "(dom P ⊆ R ∖ (dom Q ; top)) = (P ; top ⊆ R ∖ (Q ; top))"
  by (metis dom_rres_top dom_top)

lemma fdia_rres_top: "( |R⟩P ⊆ dom Q) = (dom P ⊆ R ∖ (dom Q ; top))"
  by (metis dom_alt_def dom_gla_top rel_fdia_def rres_galois)

lemma fdia_rres_top_var: "( |R⟩ P ⊆ dom Q) = (dom P ⊆ R ∖ (Q ; top))"
  by (metis dom_top fdia_rres_top)

lemma dom_galois_var2: "( |R⟩ (Id ∩ P) ⊆ Id ∩ Q) = (Id ∩ P ⊆ R ∖ ((Id ∩ Q) ; top))"
  by (metis dom_subid fdia_rres_top_var inf_sup_aci(4))

lemma rres_top: "R ∖ (dom Q ; top) ; top = R ∖ (dom Q ; top)"
  unfolding rres_def top_def dom_def relcomp_unfold by clarsimp

lemma ddd_var: "( |R⟩ P ⊆ dom Q) = (dom P ⊆ dom ((R ∖ (dom Q ; top)) ; top))"
  unfolding rel_fdia_def dom_def rres_def top_def relcomp_unfold Id_def by force

lemma wlp_prop: "dom ((R ∖ (dom Q ; top)) ; top) = neg (cod (neg (dom Q); R))"
  unfolding rres_def Id_def cod_def dom_def top_def relcomp_unfold by fastforce

lemma wlp_prop_var: "dom ((R ∖ (dom Q ; top))) = neg (cod ((neg (dom Q)); R))"
  by (metis rres_top wlp_prop)

lemma dom_demod: "( |R⟩ (Id ∩ P) ⊆ Id ∩ Q) = (R ; (Id ∩ P) ⊆ (Id ∩ Q) ; R)"
proof
  assume "|R⟩ (Id ∩ P) ⊆ Id ∩ Q"
  hence "R ; (Id ∩ P) ⊆ (Id ∩ Q) ; R ; (Id ∩ P)"
    by (metis O_assoc dom_gla dom_subid inf.absorb_iff2 inf_le1 rel_fdia_def)
  thus "R ; (Id ∩ P) ⊆ (Id ∩ Q) ; R"
    by auto
next
  assume "R ; (Id ∩ P) ⊆ (Id ∩ Q) ; R"
  hence "|R⟩ (Id ∩ P) ⊆ dom ((Id ∩ Q) ; R)"
    by (metis (no_types, lifting) dom_subid dom_top fdia_demod_top inf.absorb_iff2 inf_le1 relcomp_distrib2 sup.order_iff)
  hence "|R⟩ (Id ∩ P) ⊆ (Id ∩ Q) ∩ dom R"
    unfolding dom_def Id_def by blast
  thus "|R⟩ (Id ∩ P) ⊆ Id ∩ Q"
    by blast
qed

lemma fdia_bbox_galois_var: "( |R⟩ (Id ∩ P) ⊆ Id ∩ Q) = (Id ∩ P ⊆ Id ∩ - cod ((Id ∩ -Q); R))"
  unfolding rel_fdia_def dom_def cod_def Id_def by blast

lemma dom_demod_var2: "( |R⟩ (Id ∩ P) ⊆ Id ∩ Q) = (Id ∩ P ⊆ R ∖ ((Id ∩ Q) ; R))"
  by (meson dom_demod rres_galois)


subsection ‹Symmetric quotient›

definition syq :: "('c,'a) rel ⇒ ('c,'b) rel ⇒ ('a,'b) rel" (infixl ‹÷› 75)
  where "R ÷ S = (R ∖ S) ∩ (R⇧⌣ ⫽ S⇧⌣)"

lemma syq_set: "R ÷ S = {(a,b). ∀c. (c,a) ∈ R ⟷ (c,b) ∈ S}"
  unfolding syq_def relcomp_unfold lres_def rres_def by force

lemma converse_syq [simp]: "(R ÷ S)⇧⌣ = S ÷ R"
  unfolding syq_def converse_def rres_def lres_def by blast

lemma syq_compl: "R ÷ S = - (R⇧⌣ ; -S) ∩ - (-(R⇧⌣) ; S)"
  by (simp add: lres_compl rres_compl syq_def)

lemma syq_compl2 [simp]: "-R ÷ -S = R ÷ S"
  unfolding syq_compl by blast

lemma syq_expand1: "R ; (R ÷ S) = S ∩ (top ; (R ÷ S))"
  unfolding syq_set top_def relcomp_unfold by force

lemma syq_expand2: "(R ÷ S) ; S⇧⌣ = R⇧⌣ ∩ ((R ÷ S) ; top)"
  unfolding syq_set top_def relcomp_unfold by force

lemma syq_comp1: "(R ÷ S) ; (S ÷ T) = (R ÷ T) ∩ (top ; (S ÷ T))"
  unfolding syq_set top_def relcomp_unfold by fastforce

lemma syq_comp2: "(R ÷ S) ; (S ÷ T) = (R ÷ T) ∩ ((R ÷ S) ; top)"
  unfolding syq_set top_def relcomp_unfold by fastforce

lemma syq_bij: "bijective T ⟹ (R ÷ S) ; T = R ÷ (S ; T)"
  by (simp add: bijective_def inj_meet_distr lres_bij rres_bij syq_def)

end