Theory Closure_Operators

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Closure Operators›
theory Closure_Operators
  imports
    Order_Functions_Base
begin

consts idempotent_on :: "'a ⇒ 'b ⇒ 'c ⇒ bool"

overloading
  idempotent_on_pred ≡ "idempotent_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool"
begin
  definition "idempotent_on_pred (P :: 'a ⇒ bool) (R :: 'a ⇒ 'a ⇒ bool) (f :: 'a ⇒ 'a) ≡
    rel_equivalence_on P (rel_map f R) f"
end

context
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool" and f :: "'a ⇒ 'a"
begin

lemma idempotent_onI [intro]:
  assumes "⋀x. P x ⟹ f x ≡⇘R⇙ f (f x)"
  shows "idempotent_on P R f"
  unfolding idempotent_on_pred_def using assms by fastforce

lemma idempotent_onE [elim]:
  assumes "idempotent_on P R f"
  and "P x"
  obtains "f x ≡⇘R⇙ f (f x)"
  using assms unfolding idempotent_on_pred_def by fastforce

lemma rel_equivalence_on_rel_map_iff_idempotent_on [iff]:
  "rel_equivalence_on P (rel_map f R) f ⟷ idempotent_on P R f"
  unfolding idempotent_on_pred_def by simp

lemma idempotent_onD:
  assumes "idempotent_on P R f"
  and "P x"
  shows "f x ≡⇘R⇙ f (f x)"
  using assms by blast

end

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

overloading
  idempotent ≡ "idempotent :: ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool"
begin
  definition "(idempotent :: ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool) ≡ idempotent_on (⊤ :: 'a ⇒ bool)"
end

lemma idempotent_eq_idempotent_on:
  "(idempotent :: ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool) = idempotent_on (⊤ :: 'a ⇒ bool)"
  unfolding idempotent_def ..

lemma idempotent_eq_idempotent_on_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "idempotent :: ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool ≡ idempotent_on P"
  using assms by (simp add: idempotent_eq_idempotent_on)

context
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool" and f :: "'a ⇒ 'a"
begin

lemma idempotentI [intro]:
  assumes "⋀x. f x ≡⇘R⇙ f (f x)"
  shows "idempotent R f"
  using assms by (urule idempotent_onI)

lemma idempotentD [dest]:
  assumes "idempotent R f"
  shows "f x ≡⇘R⇙ f (f x)"
  using assms by (urule (e) idempotent_onE where chained = insert) simp

lemma idempotent_on_if_idempotent:
  assumes "idempotent R f"
  shows "idempotent_on P R f"
  using assms by (intro idempotent_onI) auto

end

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

overloading
  closure_operator ≡ "closure_operator :: ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ bool"
begin
definition "closure_operator (R :: 'a ⇒ 'a ⇒ bool) :: ('a ⇒ 'a) ⇒ bool ≡
  (R ⇒ R) ⊓ inflationary_on (in_field R) R ⊓ idempotent_on (in_field R) R"
end

lemma closure_operatorI [intro]:
  assumes "(R ⇒ R) f"
  and "inflationary_on (in_field R) R f"
  and "idempotent_on (in_field R) R f"
  shows "closure_operator R f"
  unfolding closure_operator_def using assms by blast

lemma closure_operatorE [elim]:
  assumes "closure_operator R f"
  obtains "(R ⇒ R) f" "inflationary_on (in_field R) R f"
    "idempotent_on (in_field R) R f"
  using assms unfolding closure_operator_def by blast

lemma mono_wrt_rel_if_closure_operator:
  assumes "closure_operator (R :: 'a ⇒ 'a ⇒ bool) f"
  shows "(R ⇒ R) f"
  using assms by (elim closure_operatorE)

context
  fixes R :: "'a ⇒ 'a ⇒ bool" and f :: "'a ⇒ 'a"
begin

lemma inflationary_on_in_field_if_closure_operator:
  assumes "closure_operator R f"
  shows "inflationary_on (in_field R) R f"
  using assms by (elim closure_operatorE)

lemma idempotent_on_in_field_if_closure_operator:
  assumes "closure_operator R f"
  shows "idempotent_on (in_field R) R f"
  using assms by (elim closure_operatorE)

end

end