Theory Binary_Relations_Function_Base

✐‹creator "Kevin Kappelmann"›
subsection ‹Functions as Binary Relations›
theory Binary_Relations_Function_Base
  imports
    Binary_Relations_Function_Evaluation
    Binary_Relations_Left_Total
begin

text ‹Function relations may contain further elements outside their specification.›

consts rel_dep_fun :: "'a ⇒ ('b ⇒ 'c) ⇒ 'd ⇒ bool"
consts rel_fun :: "'a ⇒ 'b ⇒ 'c ⇒ bool"

bundle rel_fun_syntax
begin
syntax
  "_rel_fun" :: "'a ⇒ 'b ⇒ 'c ⇒ bool" ("(_) → (_)" [41, 40] 40)
  "_rel_dep_fun" :: "idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ bool" ("'(_/ :/ _') → (_)" [41, 41, 40] 40)
end
bundle no_rel_fun_syntax
begin
no_syntax
  "_rel_fun" :: "'a ⇒ 'b ⇒ 'c ⇒ bool" ("(_) → (_)" [41, 40] 40)
  "_rel_dep_fun" :: "idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ bool" ("'(_/ :/ _') → (_)" [41, 41, 40] 40)
end
unbundle rel_fun_syntax
translations
  "A → B" ⇌ "CONST rel_fun A B"
  "(x : A) → B" ⇌ "CONST rel_dep_fun A (λx. B)"

definition "rel_dep_fun_pred (A :: 'a ⇒ bool) (B :: 'a ⇒ 'b ⇒ bool) (R :: 'a ⇒ 'b ⇒ bool) ≡
  left_total_on A R ∧ right_unique_on A R ∧ ((x : A) ⇛⇩m B x) (eval R)"
adhoc_overloading rel_dep_fun rel_dep_fun_pred

definition "rel_fun_pred (A :: 'a ⇒ bool) (B :: 'b ⇒ bool) :: ('a ⇒ 'b ⇒ bool) ⇒ bool ≡
  rel_dep_fun_pred A (λ(_ :: 'a). B)"
adhoc_overloading rel_fun rel_fun_pred

lemma rel_fun_eq_rel_dep_fun:
  "(((A :: 'a ⇒ bool) → (B :: 'b ⇒ bool)) :: ('a ⇒ 'b ⇒ bool) ⇒ bool) = (((_ :: 'a) : A) → B)"
  by (simp add: rel_fun_pred_def)

lemma rel_fun_eq_rel_dep_fun_uhint [uhint]:
  assumes "(A :: 'a ⇒ bool) ≡ A'"
  and "B' ≡ (λ(_ :: 'a). (B :: 'b ⇒ bool))"
  shows "(A → B) ≡ ((x : A') → B' x)"
  using assms by (simp add: rel_fun_eq_rel_dep_fun)

lemma rel_fun_iff_rel_dep_fun:
  "((A :: 'a ⇒ bool) → (B :: 'b ⇒ bool)) (R :: 'a ⇒ 'b ⇒ bool) ⟷ (((_ :: 'a) : A) → B) R"
  by (simp add: rel_fun_pred_def)

lemma rel_dep_funI [intro]:
  assumes "left_total_on A R"
  and "right_unique_on A R"
  and "((x : A) ⇛⇩m B x) (eval R)"
  shows "((x : A) → B x) R"
  using assms unfolding rel_dep_fun_pred_def by auto

lemma rel_dep_funE [elim]:
  assumes "((x : A) → B x) R"
  obtains "left_total_on A R" "right_unique_on A R" "((x : A) ⇛⇩m B x) (eval R)"
  using assms unfolding rel_dep_fun_pred_def by auto

lemma rel_dep_fun_cong [cong]:
  assumes "⋀x. A x ⟷ A' x"
  and "⋀x y. A' x ⟹ B x y ⟷ B' x y"
  shows "((x : A) → B x) = ((x : A') → B' x)"
  using assms by (intro ext) (auto intro!: rel_dep_funI left_total_onI
    dep_mono_wrt_predI intro: right_unique_onD elim!: rel_dep_funE)

lemma rel_funI [intro]:
  assumes "left_total_on A R"
  and "right_unique_on A R"
  and "(A ⇛⇩m B) (eval R)"
  shows "(A → B) R"
  using assms by (urule rel_dep_funI)

lemma rel_funE [elim]:
  assumes "(A → B) R"
  obtains "left_total_on A R" "right_unique_on A R" "(A ⇛⇩m B) (eval R)"
  using assms by (urule (e) rel_dep_funE)

lemma mono_rel_dep_fun_mono_wrt_pred_eval: "(((x : A) → B x) ⇛⇩m (x : A) ⇛⇩m B x) eval"
  by auto

lemma ex1_rel_right_if_rel_dep_funI:
  assumes "((x : A) → B x) R"
  and "A x"
  shows "∃!y. R x y"
  using assms by (blast dest: right_unique_onD)

lemma eq_if_rel_if_rel_if_rel_dep_funI:
  assumes "((x : A) → B x) R"
  and "A x"
  and "R x y" "R x y'"
  shows "y = y'"
  using assms by (blast dest: right_unique_onD)

lemma eval_eq_if_rel_if_rel_dep_funI [simp]:
  assumes "((x : A) → B x) R"
  and "A x"
  and "R x y"
  shows "R`x = y"
  using assms by (intro eq_if_rel_if_rel_if_rel_dep_funI[OF assms, symmetric])
  (blast intro!: rel_eval_if_ex1[where ?R=R] ex1_rel_right_if_rel_dep_funI)

lemma rel_if_eval_eq_if_rel_dep_funI:
  assumes "((x : A) → B x) R"
  and "A x"
  and "R`x = y"
  shows "R x y"
  by (rule rel_if_eval_eq_if_in_dom_if_right_unique_on_eq[where ?R=R])
  (use assms in ‹blast dest: right_unique_onD›)+

corollary rel_eval_if_rel_dep_funI:
  assumes "((x : A) → B x) R"
  and "A x"
  shows "R x (R`x)"
  using assms by (rule rel_if_eval_eq_if_rel_dep_funI) simp

corollary rel_iff_eval_eq_if_rel_dep_funI:
  assumes "((x : A) → B x) R"
  and "A x"
  shows "R x y ⟷ R`x = y"
  using assms by (intro iffI; rule eval_eq_if_rel_if_rel_dep_funI rel_if_eval_eq_if_rel_dep_funI)

lemma rel_dep_fun_relE:
  assumes "((x : A) → B x) R"
  and "A x"
  and "R x y"
  obtains "B x y" "R`x = y"
proof
  from assms show "R`x = y" by simp
  with assms show "B x y" by blast
qed

lemma rel_dep_fun_relE':
  assumes "((x : A) → B x) R"
  obtains "⋀x y. A x ⟹ R x y ⟹ B x y ∧ R`x = y"
  using assms by (auto elim: rel_dep_fun_relE)

lemma rel_codom_if_rel_if_pred_if_rel_dep_fun:
  assumes "((x : A) → B x) R"
  and "A x"
  and "R x y"
  shows "B x y"
  using assms by (auto elim: rel_dep_fun_relE)

lemma rel_dep_fun_contravariant_dom:
  assumes "((x : A) → B x) R"
  and [dest]: "⋀x. A' x ⟹ A x"
  shows "((x : A') → B x) R"
  using assms by (fast intro!: rel_dep_funI dest: right_unique_onD)

lemma rel_dep_fun_covariant_codom:
  assumes "((x : A) → B x) R"
  and "⋀x. A x ⟹ B x (R`x) ⟹ B' x (R`x)"
  shows "((x : A) → B' x) R"
  using assms by (fast dest: right_unique_onD)

lemma rel_fun_in_codom_on_if_rel_dep_fun:
  assumes "((x : A) → B x) R"
  shows "(A → in_codom_on A B) R"
  using assms by fastforce

lemma comp_eq_eval_restrict_left_le_if_rel_dep_fun:
  assumes "((x : A) → B x) R"
  shows "((=) ∘ eval R)↾⇘A⇙ ≤ R↾⇘A⇙"
  using assms by (intro le_relI) (force intro: rel_eval_if_rel_dep_funI)

lemma restrict_left_le_comp_eq_eval_restrict_left_if_rel_dep_fun:
  assumes "((x : A) → B x) R"
  shows "R↾⇘A⇙ ≤ ((=) ∘ eval R)↾⇘A⇙"
  using assms by (intro le_relI) force

corollary restrict_left_eq_comp_eq_eval_if_rel_dep_fun:
  assumes "((x : A) → B x) R"
  shows "R↾⇘A⇙ = ((=) ∘ eval R)↾⇘A⇙"
  using assms comp_eq_eval_restrict_left_le_if_rel_dep_fun
    restrict_left_le_comp_eq_eval_restrict_left_if_rel_dep_fun
  by (intro antisym) auto

lemma eval_eq_if_rel_dep_funI:
  fixes R :: "'a ⇒ 'b ⇒ bool"
  assumes "((x : A) → B x) R" "((x : A') → B' x) R'"
  and "R ≤ R'"
  and "(A ⊓ A') x"
  shows "R`x = R'`x"
proof -
  from assms have "R' x (R`x)" "R' x (R'`x)" by (auto intro: rel_eval_if_rel_dep_funI)
  with assms show ?thesis by (intro eval_eq_if_rel_if_rel_dep_funI[symmetric]) force+
qed

lemma rel_agree_on_if_eval_eq_if_rel_dep_fun:
  assumes crel_dep_fun: "⋀R. ℛ R ⟹ ∃B. ((x : A) → B x) R"
  and "⋀R R' x. ℛ R ⟹ ℛ R' ⟹ A x ⟹ R`x = R'`x"
  shows "rel_agree_on A ℛ"
proof (rule rel_agree_onI)
  fix x y R R' assume hyps: "ℛ R" "ℛ R'" "A x" "R x y"
  with crel_dep_fun have "y = R`x" by fastforce
  also from assms hyps have "... = R'`x" by blast
  finally have "y = R'`x" .
  moreover from crel_dep_fun[OF ‹ℛ R'›] obtain B where "((x : A) → B x) R'" by blast
  ultimately show "R' x y" using ‹A x› by (auto intro: rel_eval_if_rel_dep_funI)
qed

lemma mono_rel_dep_fun_top_rel_dep_fun_inf_rel_restrict_left:
  "(((x : A) → B x) ⇛⇩m (A' : ⊤) ⇛⇩m (x : A ⊓ A') → B x) rel_restrict_left"
  by (intro mono_wrt_predI dep_mono_wrt_predI rel_dep_funI
    (*TODO: should be solved by some type-checking automation*)
    mono_right_unique_on_top_right_unique_on_inf_rel_restrict_left
      [THEN dep_mono_wrt_predD, THEN dep_mono_wrt_predD]
    mono_left_total_on_top_left_total_on_inf_rel_restrict_left
      [THEN dep_mono_wrt_predD, THEN dep_mono_wrt_predD])
  auto

end