Theory Binary_Relations_Clean_Function

✐‹creator "Kevin Kappelmann"›
subsection ‹Clean Functions›
theory Binary_Relations_Clean_Function
  imports
    Binary_Relations_Function_Base
begin

text ‹Clean function relations may not contain further elements outside their specification.›

consts crel_dep_fun :: "'a ⇒ ('b ⇒ 'c) ⇒ 'd ⇒ bool"
consts crel_fun :: "'a ⇒ 'b ⇒ 'c ⇒ bool"

bundle crel_fun_syntax
begin
syntax
  "_crel_fun" :: "'a ⇒ 'b ⇒ 'c ⇒ bool" ("(_) →⇩c (_)" [41, 40] 40)
  "_crel_dep_fun" :: "idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ bool" ("'(_/ :/ _') →⇩c (_)" [41, 41, 40] 40)
end
bundle no_crel_fun_syntax
begin
no_syntax
  "_crel_fun" :: "'a ⇒ 'b ⇒ 'c ⇒ bool" ("(_) →⇩c (_)" [41, 40] 40)
  "_crel_dep_fun" :: "idt ⇒ 'a ⇒ 'b ⇒ 'c ⇒ bool" ("'(_/ :/ _') →⇩c (_)" [41, 41, 40] 40)
end
unbundle crel_fun_syntax
translations
  "A →⇩c B" ⇌ "CONST crel_fun A B"
  "(x : A) →⇩c B" ⇌ "CONST crel_dep_fun A (λx. B)"

definition "crel_dep_fun_pred (A :: 'a ⇒ bool) B R ≡ ((x : A) → B x) R ∧ in_dom R = A"
adhoc_overloading crel_dep_fun crel_dep_fun_pred

definition "crel_fun_pred (A :: 'a ⇒ bool) B ≡ (((_ :: 'a) : A) →⇩c B)"
adhoc_overloading crel_fun crel_fun_pred

lemma crel_fun_eq_crel_dep_fun:
  "(((A :: 'a ⇒ bool) →⇩c (B :: 'b ⇒ bool)) :: ('a ⇒ 'b ⇒ bool) ⇒ bool) = (((_ :: 'a) : A) →⇩c B)"
  by (simp add: crel_fun_pred_def)

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

lemma crel_fun_iff_crel_dep_fun:
  "((A :: 'a ⇒ bool) →⇩c (B :: 'b ⇒ bool)) (R :: 'a ⇒ 'b ⇒ bool) ⟷ (((_ :: 'a) : A) →⇩c B) R"
  by (simp add: crel_fun_pred_def)

lemma crel_dep_funI [intro]:
  assumes "((x : A) → B x) R"
  and "in_dom R ≤ A"
  shows "((x : A) →⇩c B x) R"
  unfolding crel_dep_fun_pred_def using assms
  by (intro conjI antisym le_in_dom_if_left_total_on) auto

lemma crel_dep_funI':
  assumes "left_total_on A R"
  and "right_unique_on A R"
  and "({∑}x : A. B x) R"
  shows "((x : A) →⇩c B x) R"
proof (intro crel_dep_funI rel_dep_funI dep_mono_wrt_predI)
  fix x assume "A x"
  with assms obtain y where "B x y" "R x y" by auto
  moreover with assms have "R`x = y" by (auto intro: eval_eq_if_right_unique_onI)
  ultimately show "B x (R`x)" by simp
qed (use assms in auto)

lemma crel_dep_funE:
  assumes "((x : A) →⇩c B x) R"
  obtains "((x : A) → B x) R" "in_dom R = A"
  using assms unfolding crel_dep_fun_pred_def by auto

lemma crel_dep_funE' [elim]:
  notes crel_dep_funE[elim]
  assumes "((x : A) →⇩c B x) R"
  obtains "((x : A) → B x) R" "({∑}x : A. B x) R"
proof
  show "({∑}x : A. B x) R"
  proof (rule dep_bin_relI)
    fix x y assume "R x y" "A x"
    with assms have "R`x = y" "B x (R`x)" by auto
    then show "B x y" by simp
  qed (use assms in auto)
qed (use assms in auto)

lemma crel_dep_fun_cong [cong]:
  assumes "⋀x. A x ⟷ A' x"
  and "⋀x y. A' x ⟹ B x y ⟷ B' x y"
  shows "((x : A) →⇩c B x) = ((x : A') →⇩c B' x)"
  using assms by (intro ext) (auto intro!: crel_dep_funI elim!: crel_dep_funE)

lemma in_dom_eq_if_crel_dep_fun [simp]:
  assumes "((x : A) →⇩c B x) R"
  shows "in_dom R = A"
  using assms by (auto elim: crel_dep_funE)

lemma in_codom_le_in_codom_on_if_crel_dep_fun:
  assumes "((x : A) →⇩c B x) R"
  shows "in_codom R ≤ in_codom_on A B"
  using assms by fast

lemma crel_funI [intro]:
  assumes "(A → B) R"
  and "in_dom R ≤ A"
  shows "(A →⇩c B) R"
  using assms by (urule crel_dep_funI)

lemma crel_funI':
  assumes "left_total_on A R"
  and "right_unique_on A R"
  and "(A {×} B) R"
  shows "(A →⇩c B) R"
  using assms by (urule crel_dep_funI')

lemma crel_funE:
  assumes "(A →⇩c B) R"
  obtains "(A → B) R" "in_dom R = A"
  using assms by (urule (e) crel_dep_funE)

lemma crel_funE' [elim]:
  assumes "(A →⇩c B) R"
  obtains "(A → B) R" "(A {×} B) R"
  using assms by (urule (e) crel_dep_funE')

lemma in_dom_eq_if_crel_fun [simp]:
  assumes "(A →⇩c B) R"
  shows "in_dom R = A"
  using assms by (urule in_dom_eq_if_crel_dep_fun)

lemma eq_if_rel_if_rel_if_crel_dep_funI:
  assumes "((x : A) →⇩c B x) R"
  and "R x y" "R x y'"
  shows "y = y'"
  using assms by (auto intro: eq_if_rel_if_rel_if_rel_dep_funI)

lemma eval_eq_if_rel_if_crel_dep_funI [simp]:
  assumes "((x : A) →⇩c B x) R"
  and "R x y"
  shows "R`x = y"
  using assms by (auto intro: eval_eq_if_rel_if_rel_dep_funI)

lemma crel_dep_fun_relE:
  assumes "((x : A) →⇩c B x) R"
  and "R x y"
  obtains "A x" "B x y" "R`x = y"
  using assms by (auto elim: rel_dep_fun_relE)

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

lemma rel_restrict_left_eq_self_if_crel_dep_fun [simp]:
  assumes "((x : A) →⇩c B x) R"
  shows "R↾⇘A⇙ = R"
  using assms by auto

text ‹Note: clean function relations are not contravariant on their domain.›

lemma crel_dep_fun_covariant_codom:
  assumes "((x : A) →⇩c B x) R"
  and "⋀x. A x ⟹ B x (R`x) ⟹ B' x (R`x)"
  shows "((x : A) →⇩c B' x) R"
  using assms by (force intro: rel_dep_fun_covariant_codom)

lemma comp_eq_eval_restrict_left_le_if_crel_dep_fun:
  assumes [uhint]: "((x : A) →⇩c B x) R"
  shows "((=) ∘ eval R)↾⇘A⇙ ≤ R"
  supply rel_restrict_left_eq_self_if_crel_dep_fun[uhint]
  by (urule comp_eq_eval_restrict_left_le_if_rel_dep_fun) (use assms in auto)

lemma le_comp_eq_eval_restrict_left_if_rel_dep_fun:
  assumes [uhint]: "((x : A) →⇩c B x) R"
  shows "R ≤ ((=) ∘ eval R)↾⇘A⇙"
  supply rel_restrict_left_eq_self_if_crel_dep_fun[uhint]
  by (urule restrict_left_le_comp_eq_eval_restrict_left_if_rel_dep_fun) (use assms in auto)

corollary restrict_left_eq_comp_eq_eval_if_crel_dep_fun:
  assumes "((x : A) →⇩c B x) R"
  shows "R = ((=) ∘ eval R)↾⇘A⇙"
  using assms comp_eq_eval_restrict_left_le_if_crel_dep_fun
    le_comp_eq_eval_restrict_left_if_rel_dep_fun
  by (intro antisym) auto

lemma eval_eq_if_crel_dep_fun_if_rel_dep_funI:
  fixes R :: "'a ⇒ 'b ⇒ bool"
  assumes "((x : A) → B x) R" "((x : A') →⇩c B' x) R'"
  and "R ≤ R'"
  and "A x"
  shows "R`x = R'`x"
proof -
  from assms have "A' x" by (blast elim: crel_dep_fun_relE)
  with assms show ?thesis by (blast intro: eval_eq_if_rel_dep_funI)
qed

lemma crel_dep_fun_ext:
  assumes "((x : A) →⇩c B x) R" "((x : A) →⇩c B' x) R'"
  and "⋀x. A x ⟹ R`x = R'`x"
  shows "R = R'"
  using assms
  by (intro eq_if_rel_agree_on_if_dep_bin_relI[where ?A=A and ?B=B and ?ℛ="(=) R ⊔ (=) R'"]
    rel_agree_on_if_eval_eq_if_rel_dep_fun)
  auto

lemma eq_if_le_if_crel_dep_fun_if_rel_dep_fun:
  assumes "((x : A) → B x) R" "((x : A) →⇩c B' x) R'"
  and "R ≤ R'"
  shows "R = R'"
proof (intro ext iffI)
  fix x y assume "R' x y"
  with assms have "R'`x = y" "A x" by auto
  moreover with assms have "R`x = R'`x" by (blast intro: eval_eq_if_crel_dep_fun_if_rel_dep_funI)
  ultimately show "R x y" using assms by (auto intro: rel_if_eval_eq_if_rel_dep_funI)
qed (use assms in auto)

lemma ex_dom_crel_dep_fun_iff_crel_dep_fun_in_dom:
  "(∃(A :: 'a ⇒ bool). ((x : A) →⇩c B x) R) ⟷ (((x : in_dom R) →⇩c B x) R)"
  by auto

lemma crel_fun_bottom_bottom: "((⊥ :: 'a ⇒ bool) →⇩c A) (⊥ :: 'a ⇒ 'b ⇒ bool)"
  by fastforce

lemma crel_dep_fun_bottom_iff_eq_bottom [iff]: "((x : (⊥ :: 'a ⇒ bool)) →⇩c B x) R ⟷ R = ⊥"
  by fastforce

lemma mono_crel_dep_fun_top_crel_dep_fun_inf_rel_restrict_left:
  "(((x : A) →⇩c B x) ⇛⇩m (A' : ⊤) ⇛⇩m (x : A ⊓ A') →⇩c B x) rel_restrict_left"
  by (intro mono_wrt_predI dep_mono_wrt_predI crel_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]
    mono_dep_bin_rel_top_dep_bin_rel_inf_rel_restrict_left
      [THEN mono_wrt_predD, THEN dep_mono_wrt_predD])
  auto

lemma mono_rel_dep_fun_ge_crel_dep_fun_rel_restrict_left:
  "(((x : A) → B x) ⇛⇩m (A' : (≥) A) ⇛⇩m (x : A') →⇩c B x) rel_restrict_left"
proof (intro mono_wrt_predI dep_mono_wrt_predI crel_dep_funI)
  fix A A' :: "'a ⇒ bool" and B and R :: "'a ⇒ 'b ⇒ bool" assume "((x : A) → B x) R"
  with mono_rel_dep_fun_top_rel_dep_fun_inf_rel_restrict_left have "((x : A ⊓ A') → B x) R↾⇘A'⇙"
    by force
  moreover assume "A' ≤ A"
  ultimately show "((x : A') → B x) R↾⇘A'⇙" by (simp only: inf_absorb2)
qed auto

lemma crel_dep_fun_eq_restrict: "((x : (A :: 'a ⇒ bool)) →⇩c (=) x) (=)↾⇘A⇙"
  by fastforce

end