Theory PAC_Misc

theory PAC_Misc
  imports Main

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)