Theory HOL_Alignment_Predicates

✐‹creator "Kevin Kappelmann"›
subsection ‹Alignment With Predicate Definitions from HOL›
theory HOL_Alignment_Predicates
  imports
    Main
    HOL_Mem_Of
    Predicates
begin

named_theorems HOL_predicate_alignment

subparagraph ‹Quantifiers›

adhoc_overloading ball ⇌ Ball

lemma Ball_eq_ball_pred [HOL_predicate_alignment]: "∀⇘A⇙ = ∀⇘mem_of A⇙" by auto

lemma Ball_eq_ball_pred_uhint [uhint]:
  assumes "P ≡ mem_of A"
  shows "∀⇘A⇙ = ∀⇘P⇙"
  using assms by (simp add: Ball_eq_ball_pred)

lemma Ball_iff_ball_pred [HOL_predicate_alignment]: "(∀x : A. Q x) ⟷ (∀x : mem_of A. Q x)"
  by (simp add: Ball_eq_ball_pred)

adhoc_overloading bex ⇌ Bex

lemma Bex_eq_bex_pred [HOL_predicate_alignment]: "∃⇘A⇙ = ∃⇘mem_of A⇙" by fast

lemma Bex_eq_bex_pred_uhint [uhint]:
  assumes "P ≡ mem_of A"
  shows "∃⇘A⇙ = ∃⇘P⇙"
  using assms by (simp add: Bex_eq_bex_pred)

lemma Bex_iff_bex_pred [HOL_predicate_alignment]: "(∃x : A. Q x) ⟷ (∃x : mem_of A. Q x)"
  by (simp add: Bex_eq_bex_pred)


end