Theory Binary_Relations_Function_Composition

✐‹creator "Kevin Kappelmann"›
subsection ‹Composing Functions›
theory Binary_Relations_Function_Composition
  imports
    Binary_Relations_Clean_Function
    Restricted_Equality
begin

lemma dep_bin_rel_eval_rel_comp_if_dep_bin_rel_if_crel_dep_fun:
  assumes "((x : A) →⇩c B x) R"
  and "⋀x. A x ⟹ ({∑}y : B x. C x y) R'"
  shows "({∑}x : A. C x (R`x)) (R ∘∘ R')"
  using assms by force

lemma crel_dep_fun_eval_rel_comp_if_rel_dep_fun_if_crel_dep_fun:
  assumes "((x : A) →⇩c B x) R"
  and "⋀x. A x ⟹ ((y : B x) → C x y) R'"
  shows "((x : A) →⇩c C x (R`x)) (R ∘∘ R')"
proof (intro crel_dep_funI' dep_bin_relI
  (*TODO: should be solved by some type-checking automation*)
  mono_left_total_on_comp[THEN dep_mono_wrt_predD, THEN mono_wrt_predD]
  mono_right_unique_on_comp[THEN dep_mono_wrt_predD, THEN mono_wrt_predD])
  from assms show "left_total_on (in_codom R↾⇘A⇙) R'" by force
  from assms show "right_unique_on (in_codom R↾⇘A⇙) R'" by (fast dest: right_unique_onD)
qed (use assms in ‹auto elim: rel_dep_fun_relE crel_dep_fun_relE›)

lemma rel_comp_eval_eq_if_rel_dep_fun_if_crel_dep_funI [simp]:
  assumes "((x : A) →⇩c B x) R"
  and "⋀x. A x ⟹ ((y : B x) → C x y) R'"
  and "A x"
  shows "(R ∘∘ R')`x = R'`(R`x)"
proof (rule eval_eq_if_right_unique_onI)
  from assms have "((x : A) →⇩c C x (R`x)) (R ∘∘ R')"
    by (intro crel_dep_fun_eval_rel_comp_if_rel_dep_fun_if_crel_dep_fun) auto
  then show "right_unique_on A (R ∘∘ R')" by blast
  from assms show "(R ∘∘ R') x (R'`(R`x))" by (blast intro: rel_eval_if_rel_dep_funI)
qed (fact assms)

lemma eq_restrict_comp_eq_if_crel_dep_fun [simp]:
  assumes "((x : A) →⇩c B x) R"
  shows "(=⇘A⇙) ∘∘ R = R"
  using assms by force

lemma comp_eq_restrict_if_crel_dep_fun [simp]:
  assumes "(A →⇩c B) R"
  shows "R ∘∘ (=⇘B⇙) = R"
  using assms by force

end