Theory Binary_Relations_Left_Total

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Left Total›
theory Binary_Relations_Left_Total
  imports
    Functions_Monotone
begin

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

overloading
  left_total_on_pred ≡ "left_total_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool"
begin
  definition "left_total_on_pred P R ≡ ∀x : P. in_dom R x"
end

lemma left_total_onI [intro]:
  assumes "⋀x. P x ⟹ in_dom R x"
  shows "left_total_on P R"
  unfolding left_total_on_pred_def using assms by blast

lemma left_total_onE [elim]:
  assumes "left_total_on P R"
  and "P x"
  obtains y where "R x y"
  using assms unfolding left_total_on_pred_def by blast

lemma le_in_dom_if_left_total_on:
  assumes "left_total_on P R"
  shows "P ≤ in_dom R"
  using assms by force

lemma left_total_on_if_le_in_dom:
  assumes "P ≤ in_dom R"
  shows "left_total_on P R"
  using assms by fastforce

lemma mono_left_total_on:
  "((≥) ⇒ (≤) ⇛ (≤)) (left_total_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool)"
  by fastforce

lemma le_in_dom_iff_left_total_on: "P ≤ in_dom R ⟷ left_total_on P R"
  using le_in_dom_if_left_total_on left_total_on_if_le_in_dom by auto

lemma mono_left_total_on_top_left_total_on_inf_rel_restrict_left:
  "((R : left_total_on P) ⇒ (P' : ⊤) ⇒ left_total_on (P ⊓ P')) rel_restrict_left"
  by fast

lemma mono_left_total_on_comp:
  "((R : left_total_on P) ⇒ left_total_on (in_codom (R↾⇘P⇙)) ⇒ left_total_on P) (∘∘)"
  by fast

consts left_total :: "'a ⇒ bool"

overloading
  left_total ≡ "left_total :: ('a ⇒ 'b ⇒ bool) ⇒ bool"
begin
  definition "(left_total :: ('a ⇒ 'b ⇒ bool) ⇒ bool) ≡ left_total_on (⊤ :: 'a ⇒ bool)"
end

lemma left_total_eq_left_total_on:
  "(left_total :: ('a ⇒ 'b ⇒ bool) ⇒ _) = left_total_on (⊤ :: 'a ⇒ bool)"
  unfolding left_total_def ..

lemma left_total_eq_left_total_on_uhint [uhint]:
  assumes "P ≡ ⊤ :: 'a ⇒ bool"
  shows "left_total :: ('a ⇒ 'b ⇒ bool) ⇒ _ ≡ left_total_on P"
  using assms by (simp add: left_total_eq_left_total_on)

lemma left_totalI [intro]:
  assumes "⋀x. in_dom R x"
  shows "left_total R"
  using assms by (urule left_total_onI)

lemma left_totalE:
  assumes "left_total R"
  obtains y where "R x y"
  using assms by (urule (e) left_total_onE where chained = insert) simp

lemma in_dom_if_left_total:
  assumes "left_total R"
  shows "in_dom R x"
  using assms by (blast elim: left_totalE)

lemma left_total_on_if_left_total:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'b ⇒ bool"
  assumes "left_total R"
  shows "left_total_on P R"
  using assms by (intro left_total_onI) (blast dest: in_dom_if_left_total)


end