Theory Binary_Relations_Bi_Total

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Bi-Total›
theory Binary_Relations_Bi_Total
  imports
    Binary_Relations_Left_Total
    Binary_Relations_Surjective
begin

definition "bi_total_on P Q ≡ left_total_on P ⊓ rel_surjective_at Q"

lemma bi_total_onI [intro]:
  assumes "left_total_on P R"
  and "rel_surjective_at Q R"
  shows "bi_total_on P Q R"
  unfolding bi_total_on_def using assms by auto

lemma bi_total_onE [elim]:
  assumes "bi_total_on P Q R"
  obtains "left_total_on P R" "rel_surjective_at Q R"
  using assms unfolding bi_total_on_def by auto

lemma bi_total_on_restricts_if_Fun_Rel_iff_if_bi_total_on:
  assumes "bi_total_on P Q R"
  and "(R ⇛ (⟷)) P Q"
  shows "bi_total_on P Q R↾⇘P⇙↿⇘Q⇙"
  using assms by force

definition "bi_total ≡ bi_total_on (⊤ :: 'a ⇒ bool) (⊤ :: 'b ⇒ bool) :: ('a ⇒ 'b ⇒ bool) ⇒ bool"

lemma bi_total_eq_bi_total_on:
  "(bi_total :: ('a ⇒ 'b ⇒ bool) ⇒ bool) = bi_total_on (⊤ :: 'a ⇒ bool) (⊤ :: 'b ⇒ bool)"
  unfolding bi_total_def ..

lemma bi_total_eq_bi_total_on_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  and "Q ≡ (⊤ :: 'b ⇒ bool)"
  shows "(bi_total :: ('a ⇒ 'b ⇒ bool) ⇒ bool) ≡ bi_total_on P Q"
  using assms by (simp add: bi_total_eq_bi_total_on)

lemma bi_totalI [intro]:
  assumes "left_total R"
  and "rel_surjective R"
  shows "bi_total R"
  using assms by (urule bi_total_onI)

lemma bi_totalE [elim]:
  assumes "bi_total R"
  obtains "left_total R" "rel_surjective R"
  using assms by (urule (e) bi_total_onE)

end