Theory Binary_Relations_Function_Extend

✐‹creator "Kevin Kappelmann"›
subsection ‹Extending Functions›
theory Binary_Relations_Function_Extend
  imports
    Binary_Relations_Clean_Function
begin

lemma left_total_on_sup_eq_extend_if_left_total_on:
  assumes "left_total_on A R"
  shows "left_total_on (A ⊔ (=) x) (extend x y R)"
  using assms by fastforce

lemma right_unique_on_sup_eq_extend_if_not_in_dom_if_right_unique_on:
  assumes "right_unique_on A R"
  and "¬(in_dom R x)"
  shows "right_unique_on (A ⊔ (=) x) (extend x y R)"
  using assms by (intro right_unique_onI) (auto dest: right_unique_onD elim!: extendE)

lemma rel_dep_fun_extend_if_if_rel_dep_funI:
  assumes "((x : A) → B x) R"
  and "¬(in_dom R x)"
  shows "((x' : A ⊔ ((=) x)) → (if x' = x then (=) y else B x')) (extend x y R)"
  using assms by (intro rel_dep_funI left_total_on_sup_eq_extend_if_left_total_on
    right_unique_on_sup_eq_extend_if_not_in_dom_if_right_unique_on dep_mono_wrt_predI)
  auto

lemma rel_dep_fun_extend_if_rel_dep_funI:
  assumes "((x : A) → B x) R"
  and "¬(in_dom R x)"
  and "B x y"
  shows "((x' : A ⊔ ((=) x)) → B x') (extend x y R)"
  by (urule rel_dep_fun_covariant_codom, urule rel_dep_fun_extend_if_if_rel_dep_funI)
  (use assms in ‹force split: if_split_asm›)+

lemma crel_dep_fun_extend_if_if_crel_dep_funI:
  assumes "((x : A) →⇩c B x) R"
  and "¬(in_dom R x)"
  shows "((x' : A ⊔ ((=) x)) →⇩c (if x' = x then (=) y else B x')) (extend x y R)"
  using assms by (intro crel_dep_funI rel_dep_fun_extend_if_if_rel_dep_funI) fastforce+

lemma crel_dep_fun_extend_if_rel_dep_funI:
  assumes "((x : A) →⇩c B x) R"
  and "¬(in_dom R x)"
  and "B x y"
  shows "((x' : A ⊔ ((=) x)) →⇩c B x') (extend x y R)"
  using assms by (intro crel_dep_funI rel_dep_fun_extend_if_rel_dep_funI) fastforce+

context
  fixes ℛ :: "('a ⇒ 'b ⇒ bool) ⇒ bool" and A :: "('a ⇒ 'b ⇒ bool) ⇒ 'a ⇒ bool" and D
  defines [simp]: "D ≡ in_codom_on ℛ A"
begin

lemma rel_dep_fun_glue_if_right_unique_if_rel_dep_fun:
  assumes funs: "⋀R. ℛ R ⟹ ((x : A R) → B x) R"
  and runique: "right_unique_on D (glue ℛ)"
  shows "((x : D) → B x) (glue ℛ)"
proof (intro rel_dep_funI dep_mono_wrt_predI left_total_onI)
  fix x assume "D x"
  with funs obtain R where hyps: "ℛ R" "A R x" "((x : A R) → B x) R" by auto
  then have "B x (R`x)" by (auto elim: rel_dep_fun_relE)
  moreover have "(glue ℛ)`x = R`x"
  proof (intro glue_eval_eqI)
    show "ℛ R" by (fact hyps)
    then have "A R ≤ D" by fastforce
    with runique show "right_unique_on (A R) (glue ℛ)" using antimono_right_unique_on by blast
  qed (use hyps in ‹auto elim: rel_dep_fun_relE›)
  ultimately show "B x (glue ℛ`x)" by simp
qed (use assms in ‹fastforce+›)

lemma crel_dep_fun_glue_if_right_unique_if_crel_dep_fun:
  assumes "⋀R. ℛ R ⟹ ((x : A R) →⇩c B x) R"
  and "right_unique_on D (glue ℛ)"
  shows "((x : D) →⇩c B x) (glue ℛ)"
  using assms by (intro crel_dep_funI rel_dep_fun_glue_if_right_unique_if_rel_dep_fun) fastforce+

end

lemma right_unique_on_sup_if_rel_agree_on_sup_if_right_unique_on:
  assumes "right_unique_on P R" "right_unique_on P R'"
  and "rel_agree_on (P ⊓ in_dom R ⊓ in_dom R') ((=) R ⊔ (=) R')"
  shows "right_unique_on P (R ⊔ R')"
proof (intro right_unique_onI)
  fix x y y' assume "P x" "(R ⊔ R') x y" "(R ⊔ R') x y'"
  then obtain R1 R2 where rels: "R1 x y" "R2 x y'" and ors: "R1 = R ∨ R1 = R'" "R2 = R ∨ R2 = R'" by auto
  then consider (neq) "R1 ≠ R2" | "R1 = R2" by auto
  then show "y = y'"
  proof cases
    case neq
    with rels ors obtain z z' where "R x z" "R' x z'" and yors: "y = z ∨ y = z'" "y' = z ∨ y' = z'"
      by auto
    with ‹P x› have "R' x z" by (intro rel_agree_onD[where ?R=R and ?R'=R' and
      ?P="P ⊓ in_dom R ⊓ in_dom R'" and ?ℛ="(=) R ⊔ (=) R'"] assms)
      auto
    with ‹P x› ‹R' x z'› assms have "z = z'" by (blast dest: right_unique_onD)
    with yors show "y = y'" by auto
  qed (use assms ‹P x› rels ors in ‹auto dest: right_unique_onD›)
qed

lemma crel_dep_fun_sup_if_eval_eq_if_crel_dep_fun:
  assumes dep_funs: "((x : A) →⇩c B x) R" "((x : A') →⇩c B x) R'"
  and "⋀x. A x ⟹ A' x ⟹ R`x = R'`x"
  shows "((x : A ⊔ A') →⇩c B x) (R ⊔ R')"
proof -
  let ?A = "λS. if S = R then A else A'"
  from dep_funs have "A = A'" if "R = R'" using that by (simp only: flip:
    in_dom_eq_if_crel_dep_fun[OF dep_funs(1)] in_dom_eq_if_crel_dep_fun[OF dep_funs(2)])
  then have [uhint]: "in_codom_on ((=) R ⊔ (=) R') ?A = A ⊔ A'"
    by (intro ext iffI) (fastforce split: if_splits)+
  show ?thesis by (urule (rr) crel_dep_fun_glue_if_right_unique_if_crel_dep_fun
    right_unique_on_sup_if_rel_agree_on_sup_if_right_unique_on
    rel_agree_on_if_eval_eq_if_rel_dep_fun)
    (use assms in ‹auto 7 0 intro: rel_dep_fun_contravariant_dom dest: right_unique_onD›)
qed

end