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 (RP))  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