Theory PAC_Misc

theory PAC_Misc
  imports Main
begin

text "I believe this should be added to the simplifier by default..."
lemma Collect_eq_comp':
  "{(x, y). P x y} O {(c, a). c = f a} = {(x, a). P x (f a)}"
  by auto

lemma in_set_conv_iff:
  "x ∈ set (take n xs) ⟷ (∃i<n. i < length xs ∧ xs ! i = x)"
  by (metis in_set_conv_nth length_take min_less_iff_conj nth_take)

lemma in_set_take_conv_nth:
  "x ∈ set (take n xs) ⟷ (∃i<min n (length xs). xs ! i = x)"
  by (simp add: in_set_conv_iff)

lemma in_set_remove1D:
  "a ∈ set (remove1 x xs) ⟹ a ∈ set xs"
  by (meson notin_set_remove1)

end