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