Theory Binary_Relations_Extend

✐‹creator "Kevin Kappelmann"›
subsection ‹Extensions›
theory Binary_Relations_Extend
  imports
    Dependent_Binary_Relations
begin

consts extend :: "'a ⇒ 'b ⇒ 'c ⇒ 'c"

definition "extend_rel x y R x' y' ≡ (x = x' ∧ y = y') ∨ R x' y'"
adhoc_overloading extend extend_rel

lemma extend_leftI [iff]: "(extend x y R) x y"
  unfolding extend_rel_def by blast

lemma extend_rightI [intro]:
  assumes "R x' y'"
  shows "(extend x y R) x' y'"
  unfolding extend_rel_def using assms by blast

lemma extendE [elim]:
  assumes "(extend x y R) x' y'"
  obtains "x = x'" "y = y'" | "x ≠ x' ∨ y ≠ y'" "R x' y'"
  using assms unfolding extend_rel_def by blast

lemma extend_eq_self_if_rel [simp]: "R x y ⟹ extend x y R = R"
  by auto

context
  fixes x :: 'a and y :: 'b and R :: "'a ⇒ 'b ⇒ bool"
begin

lemma in_dom_extend_eq: "in_dom (extend x y R) = in_dom R ⊔ (=) x"
  by (intro ext) auto

lemma in_dom_extend_iff: "in_dom (extend x y R) x' ⟷ in_dom R x' ∨ x = x'"
  by (auto simp: in_dom_extend_eq)

lemma codom_extend_eq: "in_codom (extend x y R) = in_codom R ⊔ (=) y"
  by (intro ext) auto

lemma in_codom_extend_iff: "in_codom (extend x y R) y' ⟷ in_codom R y' ∨ y = y'"
  by (auto simp: codom_extend_eq)

end

lemma in_field_extend_eq: "in_field (extend x y R) = in_field R ⊔ (=) x ⊔ (=) y"
  by (intro ext) auto

lemma in_field_extend_iff: "in_field (extend x y R) z ⟷ in_field R z ∨ z = x ∨ z = y"
  by (auto simp: in_field_extend_eq)

lemma mono_extend: "mono (extend x y :: ('a ⇒ 'b ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool)"
  by (intro monoI) force

lemma dep_mono_dep_bin_rel_extend:
  "((x : A) ⇛⇩m B x ⇛⇩m ({∑}x : A'. B' x) ⇛⇩m ({∑}x : A ⊔ A'. (B ⊔ B') x)) extend"
  by fastforce

consts glue :: "'a ⇒ 'b"

definition "glue_rel (ℛ :: ('a ⇒ 'b ⇒ bool) ⇒ bool) x ≡ in_codom_on ℛ (λR. R x)"
adhoc_overloading glue glue_rel

lemma glue_rel_eq_in_codom_on: "glue ℛ x = in_codom_on ℛ (λR. R x)"
  unfolding glue_rel_def by simp

lemma glueI [intro]:
  assumes "ℛ R"
  and "R x y"
  shows "glue ℛ x y"
  using assms unfolding glue_rel_def by blast

lemma glueE [elim!]:
  assumes "glue ℛ x y"
  obtains R where "ℛ R" "R x y"
  using assms unfolding glue_rel_def by blast

lemma glue_bottom_eq [simp]: "glue (⊥ :: ('a ⇒ 'b ⇒ bool) ⇒ bool) = ⊥"
  by (intro ext) auto

lemma glue_eq_rel_eq_self [simp]: "glue ((=) R) = (R :: 'a ⇒ 'b ⇒ bool)"
  by (intro ext) auto

lemma glue_sup_eq_glue_sup_glue [simp]: "glue (A ⊔ B) = glue A ⊔ glue B"
  supply glue_rel_eq_in_codom_on[simp]
  by (rule ext) (urule in_codom_on_sup_pred_eq_in_codom_on_sup_in_codom_on)

lemma mono_glue: "mono (glue :: (('a ⇒ 'b ⇒ bool) ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool))"
  by auto

lemma dep_bin_rel_glueI:
  fixes ℛ defines [simp]: "D ≡ in_codom_on ℛ in_dom"
  assumes "⋀R. ℛ R ⟹ ∃A. ({∑}x : A. B x) R"
  shows "({∑}x : D. B x) (glue ℛ)"
  using assms by (intro dep_bin_relI) auto


end