Theory Binary_Relations_Reflexive_Closure

✐‹creator "Kevin Kappelmann"›
subsection ‹Reflexive Closure›
theory Binary_Relations_Reflexive_Closure
  imports
    Binary_Relations_Reflexive
    Restricted_Equality
begin

consts refl_closure_on :: "'a ⇒ 'b ⇒ 'b"

overloading
  refl_closure_on_pred ≡ "refl_closure_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool)"
begin
  definition "refl_closure_on_pred (P :: 'a ⇒ bool) (R :: 'a ⇒ 'a ⇒ bool) ≡ R ⊔ (=⇘P⇙)"
end

lemma refl_closure_on_if_pred [intro]:
  assumes "P x"
  shows "refl_closure_on P R x x"
  using assms unfolding refl_closure_on_pred_def by auto

lemma refl_closure_on_if_rel [intro]:
  assumes "(R :: 'a ⇒ 'a ⇒ bool) x y"
  shows "refl_closure_on (P :: 'a ⇒ bool) R x y"
  using assms unfolding refl_closure_on_pred_def by auto

corollary le_refl_closure_on_self: "(R :: 'a ⇒ 'a ⇒ bool) ≤ refl_closure_on (P :: 'a ⇒ bool) R"
  by blast

lemma refl_closure_onE [elim]:
  assumes "refl_closure_on P R x y"
  obtains "P x" "x = y" | "R x y"
  using assms unfolding refl_closure_on_pred_def by auto

lemma reflexive_on_refl_closure_on:
  "reflexive_on (P :: 'a ⇒ bool) (refl_closure_on P (R :: 'a ⇒ 'a ⇒ bool))"
  by fastforce


definition "refl_closure_field R ≡ refl_closure_on (in_field R) R"

open_bundle refl_closure_field_syntax
begin
notation refl_closure_field (‹(_⇧+)› [1000])
end

lemma refl_closure_fieldI [intro]:
  assumes "refl_closure_on (in_field R) R x y"
  shows "R⇧+ x y"
  using assms unfolding refl_closure_field_def by auto

lemma refl_closure_fieldD [dest]:
  assumes "R⇧+ x y"
  shows "refl_closure_on (in_field R) R x y"
  using assms unfolding refl_closure_field_def by auto

lemma refl_closure_field_eq_refl_closure_on_in_field: "R⇧+ = refl_closure_on (in_field R) R"
  by auto


end