Theory Binary_Relations_Surjective

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Surjective›
theory Binary_Relations_Surjective
  imports
    Binary_Relations_Left_Total
    HOL_Syntax_Bundles_Lattices
begin

consts rel_surjective_at :: "'a ⇒ 'b ⇒ bool"

overloading
  rel_surjective_at_pred ≡ "rel_surjective_at :: ('a ⇒ bool) ⇒ ('b ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "rel_surjective_at_pred P R ≡ ∀y : P. in_codom R y"
end

lemma rel_surjective_atI [intro]:
  assumes "⋀y. P y ⟹ in_codom R y"
  shows "rel_surjective_at P R"
  unfolding rel_surjective_at_pred_def using assms by blast

lemma rel_surjective_atE [elim]:
  assumes "rel_surjective_at P R"
  and "P y"
  obtains x where "R x y"
  using assms unfolding rel_surjective_at_pred_def by blast

lemma in_codom_if_rel_surjective_at:
  assumes "rel_surjective_at P R"
  and "P y"
  shows "in_codom R y"
  using assms by blast

lemma rel_surjective_at_rel_inv_iff_left_total_on [iff]:
  "rel_surjective_at (P :: 'a ⇒ bool) (R¯ :: 'b ⇒ 'a ⇒ bool) ⟷ left_total_on P R"
  by fast

lemma left_total_on_rel_inv_iff_rel_surjective_at [iff]:
  "left_total_on (P :: 'a ⇒ bool) (R¯ :: 'a ⇒ 'b ⇒ bool) ⟷ rel_surjective_at P R"
  by fast

lemma mono_rel_surjective_at:
  "((≥) ⇒ (≤) ⇛ (≤)) (rel_surjective_at :: ('b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool)"
  by fastforce

lemma rel_surjective_at_iff_le_codom:
  "rel_surjective_at (P :: 'b ⇒ bool) (R :: 'a ⇒ 'b ⇒ bool) ⟷ P ≤ in_codom R"
  by force

lemma rel_surjective_at_compI:
  fixes P :: "'c ⇒ bool" and R :: "'a ⇒ 'b ⇒ bool" and S :: "'b ⇒ 'c ⇒ bool"
  assumes surj_R: "rel_surjective_at (in_dom S) R"
  and surj_S: "rel_surjective_at P S"
  shows "rel_surjective_at P (R ∘∘ S)"
proof (rule rel_surjective_atI)
  fix y assume "P y"
  then obtain x where "S x y" using surj_S by auto
  moreover then have "in_dom S x" by auto
  moreover then obtain z where "R z x" using surj_R by auto
  ultimately show "in_codom (R ∘∘ S) y" by blast
qed

consts rel_surjective :: "'a ⇒ bool"

overloading
  rel_surjective ≡ "rel_surjective :: ('b ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "(rel_surjective :: ('b ⇒ 'a ⇒ bool) ⇒ _) ≡ rel_surjective_at (⊤ :: 'a ⇒ bool)"
end

lemma rel_surjective_eq_rel_surjective_at:
  "(rel_surjective :: ('b ⇒ 'a ⇒ bool) ⇒ _) = rel_surjective_at (⊤ :: 'a ⇒ bool)"
  unfolding rel_surjective_def ..

lemma rel_surjective_eq_rel_surjective_at_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "(rel_surjective :: ('b ⇒ 'a ⇒ bool) ⇒ _) ≡ rel_surjective_at P"
  using assms by (simp add: rel_surjective_eq_rel_surjective_at)

lemma rel_surjectiveI:
  assumes "⋀y. in_codom R y"
  shows "rel_surjective R"
  using assms by (urule rel_surjective_atI)

lemma rel_surjectiveE:
  assumes "rel_surjective R"
  obtains x where "R x y"
  using assms by (urule (e) rel_surjective_atE where chained = insert) simp

lemma in_codom_if_rel_surjective:
  assumes "rel_surjective R"
  shows "in_codom R y"
  using assms by (blast elim: rel_surjectiveE)

lemma rel_surjective_rel_inv_iff_left_total [iff]: "rel_surjective R¯ ⟷ left_total R"
  by (urule rel_surjective_at_rel_inv_iff_left_total_on)

lemma left_total_rel_inv_iff_rel_surjective [iff]: "left_total R¯ ⟷ rel_surjective R"
  by (urule left_total_on_rel_inv_iff_rel_surjective_at)

lemma rel_surjective_at_if_surjective:
  fixes P :: "'a ⇒ bool" and R :: "'b ⇒ 'a ⇒ bool"
  assumes "rel_surjective R"
  shows "rel_surjective_at P R"
  using assms by (intro rel_surjective_atI) (blast dest: in_codom_if_rel_surjective)


end