Theory HOL_Mem_Of

✐‹creator "Kevin Kappelmann"›
theory HOL_Mem_Of
  imports
    HOL.Set
    ML_Unification.ML_Unification_HOL_Setup
begin

definition "mem_of A x ≡ x ∈ A"
lemma mem_of_eq: "mem_of = (λA x. x ∈ A)" unfolding mem_of_def by simp
lemma mem_of_iff [iff]: "mem_of A x ⟷ x ∈ A" unfolding mem_of_def by simp

lemma mem_of_eq_mem_uhint [uhint]:
  assumes "x ≡ x'"
  and "A ≡ A'"
  shows "mem_of A x ≡ x' ∈ A'"
  using assms by simp

lemma mem_of_UNIV_eq_top [simp]: "mem_of UNIV = ⊤"
  by auto

lemma mem_of_empty_eq_bot [simp]: "mem_of {} = ⊥"
  by auto


end