Theory FSet_More

theory FSet_More
imports  "HOL-Library.FSet"
begin

lemma Suc_pred_image[simp]: "0 ∉ P ⟹ (λx. Suc (x - Suc 0)) ` P = P"
    unfolding image_def by safe (metis Suc_pred neq0_conv)+

context includes fset.lifting begin

lemmas Suc_pred_fimage[simp] = Suc_pred_image[Transfer.transferred]

end

lemma ffilter_eq_fempty_iff:
  "ffilter P X = {||} ⟷ (∀x. x |∈| X ⟶ ¬ P x)"
  "{||} = ffilter P X ⟷ (∀x. x |∈| X ⟶ ¬ P x)"
  by auto

lemma max_ffilter_below[simp]: "⟦x |∈| P; x < n⟧ ⟹
  max n (Suc (fMax (ffilter (λi. i < n) P))) = n"
  by (metis max.absorb1 Suc_leI fMax_in fempty_iff ffmember_filter)

lemma fMax_boundedD:
  "⟦fMax P < n; x |∈| P⟧ ⟹ x < n"
  "⟦fMax P ≤ n; n |∉| P; x |∈| P⟧ ⟹ x < n"
  by (metis fMax_ge le_less_trans, metis fMax_ge leD neqE order.strict_trans2)

lemma fMax_ffilter_less: "x |∈| P ⟹ x < n ⟹ fMax (ffilter (λi. i < n) P) < n"
  by (metis fMax_in ffilter_eq_fempty_iff(2) ffmember_filter)

end