Theory Set_Applicative

theory Set_Applicative imports
  Applicative_Lifting.Applicative_Set
begin

subsection ‹Applicative instance for @{typ "'a set"}›

lemma ap_set_conv_bind: "ap_set f x = Set.bind f (λf. Set.bind x (λx. {f x}))"
by(auto simp add: ap_set_def bind_UNION)

context includes applicative_syntax begin

lemma in_ap_setI: "⟦ f' ∈ f; x' ∈ x ⟧ ⟹ f' x' ∈ f ⋄ x"
by(auto simp add: ap_set_def)

lemma in_ap_setE [elim!]:
  "⟦ x ∈ f ⋄ y; ⋀f' y'. ⟦ x = f' y'; f' ∈ f; y' ∈ y ⟧ ⟹ thesis ⟧ ⟹ thesis"
by(auto simp add: ap_set_def)

lemma in_ap_pure_set [iff]: "x ∈ {f} ⋄ y ⟷ (∃y'∈y. x = f y')"
unfolding ap_set_def by auto

end

end