Theory FSet_Utils

section‹FSet Utilities›
text‹This theory provides various additional lemmas, definitions, and syntax over the fset data type.›
theory FSet_Utils
  imports "HOL-Library.FSet"
begin

notation (latex output)
  "FSet.fempty" ("∅") and
  "FSet.fmember" ("∈")

syntax (ASCII)
  "_fBall"       :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3ALL (_/:_)./ _)" [0, 0, 10] 10)
  "_fBex"        :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3EX (_/:_)./ _)" [0, 0, 10] 10)
  "_fBex1"       :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3EX! (_/:_)./ _)" [0, 0, 10] 10)

syntax (input)
  "_fBall"       :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3! (_/:_)./ _)" [0, 0, 10] 10)
  "_fBex"        :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3? (_/:_)./ _)" [0, 0, 10] 10)
  "_fBex1"       :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3?! (_/:_)./ _)" [0, 0, 10] 10)

syntax
  "_fBall"       :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3∀(_/|∈|_)./ _)" [0, 0, 10] 10)
  "_fBex"        :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3∃(_/|∈|_)./ _)" [0, 0, 10] 10)
  "_fBnex"       :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3∄(_/|∈|_)./ _)" [0, 0, 10] 10)
  "_fBex1"       :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3∃!(_/|∈|_)./ _)" [0, 0, 10] 10)

translations
  "∀x|∈|A. P" ⇌ "CONST fBall A (λx. P)"
  "∃x|∈|A. P" ⇌ "CONST fBex  A (λx. P)"
  "∄x|∈|A. P" ⇌ "CONST fBall A (λx. ¬P)"
  "∃!x|∈|A. P" ⇀ "∃!x. x |∈| A ∧ P"

lemma fset_of_list_remdups [simp]: "fset_of_list (remdups l) = fset_of_list l"
  apply (induct l)
   apply simp
  by (simp add: finsert_absorb fset_of_list_elem)

definition "fSum ≡ fsum (λx. x)"

lemma fset_both_sides: "(Abs_fset s = f) = (fset (Abs_fset s) = fset f)"
  by (simp add: fset_inject)

lemma Abs_ffilter: "(ffilter f s = s') = ({e ∈ (fset s). f e} = (fset s'))"
  by (simp add: ffilter_def fset_both_sides Abs_fset_inverse Set.filter_def)

lemma size_ffilter_card: "size (ffilter f s) = card ({e ∈ (fset s). f e})"
  by (simp add: ffilter_def fset_both_sides Abs_fset_inverse Set.filter_def)

lemma ffilter_empty [simp]: "ffilter f {||} = {||}"
  by auto

lemma ffilter_finsert:
  "ffilter f (finsert a s) = (if f a then finsert a (ffilter f s) else (ffilter f s))"
  apply simp
  apply standard
   apply (simp add: ffilter_def fset_both_sides Abs_fset_inverse)
   apply auto[1]
  apply (simp add: ffilter_def fset_both_sides Abs_fset_inverse)
  by auto

lemma fset_equiv: "(f1 = f2) = (fset f1 = fset f2)"
  by (simp add: fset_inject)

lemma finsert_equiv: "(finsert e f = f') = (insert e (fset f) = (fset f'))"
  by (simp add: finsert_def fset_both_sides Abs_fset_inverse)

lemma filter_elements:
  "x |∈| Abs_fset (Set.filter f (fset s)) = (x ∈ (Set.filter f (fset s)))"
  by (metis ffilter.rep_eq fset_inverse)

lemma sorted_list_of_fempty [simp]: "sorted_list_of_fset {||} = []"
  by (simp add: sorted_list_of_fset_def)

lemma fold_union_ffUnion: "fold (|∪|) l {||} = ffUnion (fset_of_list l)"
by(induct l rule: rev_induct, auto)

lemma filter_filter:
  "ffilter P (ffilter Q xs) = ffilter (λx. Q x ∧ P x) xs"
  by auto

lemma fsubset_strict:
  "x2 |⊂| x1 ⟹ ∃e. e |∈| x1 ∧ e |∉| x2"
  by auto

lemma fsubset:
  "x2 |⊂| x1 ⟹ ∄e. e |∈| x2 ∧ e |∉| x1"
  by auto

lemma size_fsubset_elem:
  assumes "∃e. e |∈| x1 ∧ e |∉| x2"
      and "∄e. e |∈| x2 ∧ e |∉| x1"
    shows "size x2 < size x1"
  using assms
  apply simp
  by (metis card_seteq finite_fset linorder_not_le subsetI)

lemma size_fsubset: "x2 |⊂| x1 ⟹ size x2 < size x1"
  by (metis fsubset fsubset_strict size_fsubset_elem)

definition fremove :: "'a ⇒ 'a fset ⇒ 'a fset"
  where [code_abbrev]: "fremove x A = A - {|x|}"

lemma arg_cong_ffilter:
  "∀e |∈| f. p e = p' e ⟹ ffilter p f = ffilter p' f"
  by auto

lemma ffilter_singleton: "f e ⟹ ffilter f {|e|} = {|e|}"
  apply (simp add: ffilter_def fset_both_sides Abs_fset_inverse)
  by auto

lemma fset_eq_alt: "(x = y) = (x |⊆| y ∧ size x = size y)"
  by (metis exists_least_iff le_less size_fsubset)

lemma ffold_empty [simp]: "ffold f b {||} = b"
  by (simp add: ffold_def)

lemma sorted_list_of_fset_sort:
  "sorted_list_of_fset (fset_of_list l) = sort (remdups l)"
  by (simp add: fset_of_list.rep_eq sorted_list_of_fset.rep_eq sorted_list_of_set_sort_remdups)

lemma fMin_Min: "fMin (fset_of_list l) = Min (set l)"
  by (simp add: fMin.F.rep_eq fset_of_list.rep_eq)

lemma sorted_hd_Min:
  "sorted l ⟹
   l ≠ [] ⟹
   hd l = Min (set l)"
  by (metis List.finite_set Min_eqI eq_iff hd_Cons_tl insertE list.set_sel(1) list.simps(15) sorted_simps(2))

lemma hd_sort_Min: "l ≠ [] ⟹ hd (sort l) = Min (set l)"
  by (metis sorted_hd_Min set_empty set_sort sorted_sort)

lemma hd_sort_remdups: "hd (sort (remdups l)) = hd (sort l)"
  by (metis hd_sort_Min remdups_eq_nil_iff set_remdups)

lemma exists_fset_of_list: "∃l. f = fset_of_list l"
  using exists_fset_of_list by fastforce

lemma hd_sorted_list_of_fset:
  "s ≠ {||} ⟹ hd (sorted_list_of_fset s) = (fMin s)"
  apply (insert exists_fset_of_list[of s])
  apply (erule exE)
  apply simp
  apply (simp add: sorted_list_of_fset_sort fMin_Min hd_sort_remdups)
  by (metis fset_of_list_simps(1) hd_sort_Min)

lemma fminus_filter_singleton:
  "fset_of_list l |-| {|x|} = fset_of_list (filter (λe. e ≠ x) l)"
  by auto

lemma card_minus_fMin:
  "s ≠ {||} ⟹ card (fset s - {fMin s}) < card (fset s)"
  by (metis Min_in bot_fset.rep_eq card_Diff1_less fMin.F.rep_eq finite_fset fset_equiv)

(* Provides a deterministic way to fold fsets similar to List.fold that works with the code generator *)
function ffold_ord :: "(('a::linorder) ⇒ 'b ⇒ 'b) ⇒ 'a fset ⇒ 'b ⇒ 'b" where
  "ffold_ord f s b = (
    if s = {||} then
      b
    else
      let
        h = fMin s;
        t = s - {|h|}
      in
        ffold_ord f t (f h b)
  )"
  by auto
termination
  apply (relation "measures [λ(a, s, ab). size s]")
   apply simp
  by (simp add: card_gt_0_iff fset_equiv)

lemma sorted_list_of_fset_Cons:
  "∃h t. (sorted_list_of_fset (finsert s ss)) = h#t"
  apply (simp add: sorted_list_of_fset_def)
  by (cases "insort s (sorted_list_of_set (fset ss - {s}))", auto)

lemma list_eq_hd_tl:
  "l ≠ [] ⟹
   hd l = h ⟹
   tl l = t ⟹
   l = (h#t)"
  by auto

lemma fset_of_list_sort: "fset_of_list l = fset_of_list (sort l)"
  by (simp add: fset_of_list.abs_eq)

lemma exists_sorted_distinct_fset_of_list:
  "∃l. sorted l ∧ distinct l ∧ f = fset_of_list l"
  by (metis distinct_sorted_list_of_set sorted_list_of_fset.rep_eq sorted_list_of_fset_simps(2) sorted_sorted_list_of_set)

lemma fset_of_list_empty [simp]: "(fset_of_list l = {||}) = (l = [])"
  by (metis fset_of_list.rep_eq fset_of_list_simps(1) set_empty)

lemma ffold_ord_cons: assumes sorted: "sorted (h#t)"
    and distinct: "distinct (h#t)"
  shows "ffold_ord f (fset_of_list (h#t)) b = ffold_ord f (fset_of_list t) (f h b)"
proof-
  have h_is_min: "h = fMin (fset_of_list (h#t))"
    by (metis sorted fMin_Min list.sel(1) list.simps(3) sorted_hd_Min)
  have remove_min: "fset_of_list t = (fset_of_list (h#t)) - {|h|}"
    using distinct fset_of_list_elem by force
  show ?thesis
    apply (simp only: ffold_ord.simps[of f "fset_of_list (h#t)"])
    by (metis h_is_min remove_min fset_of_list_empty list.distinct(1))
qed

lemma sorted_distinct_ffold_ord: assumes "sorted l"
      and "distinct l"
    shows "ffold_ord f (fset_of_list l) b = fold f l b"
  using assms
  apply (induct l arbitrary: b)
   apply simp
  by (metis distinct.simps(2) ffold_ord_cons fold_simps(2) sorted_simps(2))

lemma ffold_ord_fold_sorted: "ffold_ord f s b = fold f (sorted_list_of_fset s) b"
  by (metis exists_sorted_distinct_fset_of_list sorted_distinct_ffold_ord distinct_remdups_id sorted_list_of_fset_sort sorted_sort_id)

context includes fset.lifting begin
  lift_definition fprod  :: "'a fset ⇒ 'b fset ⇒ ('a × 'b) fset " (infixr "|×|" 80) is "λa b. fset a × fset b"
    by simp

  lift_definition fis_singleton :: "'a fset ⇒ bool" is "λA. is_singleton (fset A)".
end

lemma fprod_empty_l: "{||} |×| a = {||}"
  using bot_fset_def fprod.abs_eq by force

lemma fprod_empty_r: "a |×| {||} = {||}"
  by (simp add: fprod_def bot_fset_def Abs_fset_inverse)

lemmas fprod_empty = fprod_empty_l fprod_empty_r

lemma fprod_finsert: "(finsert a as) |×| (finsert b bs) =
   finsert (a, b) (fimage (λb. (a, b)) bs |∪| fimage (λa. (a, b)) as |∪| (as |×| bs))"
  apply (simp add: fprod_def fset_both_sides Abs_fset_inverse)
  by auto

lemma fprod_member:
  "x |∈| xs ⟹
   y |∈| ys ⟹
   (x, y) |∈| xs |×| ys"
  by (simp add: fprod_def Abs_fset_inverse)

lemma fprod_subseteq:
  "x |⊆| x' ∧ y |⊆| y' ⟹ x |×| y |⊆| x' |×| y'"
  apply (simp add: fprod_def less_eq_fset_def Abs_fset_inverse)
  by auto

lemma fimage_fprod:
  "(a, b) |∈| A |×| B ⟹ f a b |∈| (λ(x, y). f x y) |`| (A |×| B)"
  by force

lemma fprod_singletons: "{|a|} |×| {|b|} = {|(a, b)|}"
  apply (simp add: fprod_def)
  by (metis fset_inverse fset_simps(1) fset_simps(2))

lemma fprod_equiv:
  "(fset (f |×| f') = s) = (((fset f) × (fset f')) = s)"
  by (simp add: fprod_def Abs_fset_inverse)

lemma fis_singleton_alt: "fis_singleton f = (∃e. f = {|e|})"
  by (metis fis_singleton.rep_eq fset_inverse fset_simps(1) fset_simps(2) is_singleton_def)

lemma singleton_singleton [simp]: "fis_singleton {|a|}"
  by (simp add: fis_singleton_def)

lemma not_singleton_empty [simp]: "¬ fis_singleton {||}"
  apply (simp add: fis_singleton_def)
  by (simp add: is_singleton_altdef)

lemma fis_singleton_fthe_elem:
  "fis_singleton A ⟷ A = {|fthe_elem A|}"
  by (metis fis_singleton_alt fthe_felem_eq)

lemma fBall_ffilter:
  "∀x |∈| X. f x ⟹ ffilter f X = X"
  by auto

lemma fBall_ffilter2:
  "X = Y ⟹
   ∀x |∈| X. f x ⟹
   ffilter f X = Y"
  by auto

lemma size_fset_of_list: "size (fset_of_list l) = length (remdups l)"
  apply (induct l)
   apply simp
  by (simp add: fset_of_list.rep_eq insert_absorb)

lemma size_fsingleton: "(size f = 1) = (∃e. f = {|e|})"
  apply (insert exists_fset_of_list[of f])
  apply clarify
  apply (simp only: size_fset_of_list)
  apply (simp add: fset_of_list_def fset_both_sides Abs_fset_inverse)
  by (metis List.card_set One_nat_def card.insert card_1_singletonE card.empty empty_iff finite.intros(1))

lemma ffilter_mono: "(ffilter X xs = f) ⟹ ∀x |∈| xs. X x = Y x ⟹ (ffilter Y xs = f)"
  by auto

lemma size_fimage: "size (fimage f s) ≤ size s"
  apply (induct s)
   apply simp
  by (simp add: card_insert_if)

lemma size_ffilter: "size (ffilter P f) ≤ size f"
  apply (induct f)
   apply simp
  apply (simp only: ffilter_finsert)
  apply (case_tac "P x")
   apply simp
  by (simp add: card_insert_if)

lemma fimage_size_le: "⋀f s. size s ≤ n ⟹ size (fimage f s) ≤ n"
  using le_trans size_fimage by blast

lemma ffilter_size_le: "⋀f s. size s ≤ n ⟹ size (ffilter f s) ≤ n"
  using dual_order.trans size_ffilter by blast

lemma set_membership_eq: "A = B ⟷ (λx. Set.member x A) = (λx. Set.member x B)"
  apply standard
   apply simp
  by (meson equalityI subsetI)

lemmas ffilter_eq_iff = Abs_ffilter set_membership_eq fun_eq_iff

lemma size_le_1: "size f ≤ 1 = (f = {||} ∨ (∃e. f = {|e|}))"
  apply standard
   apply (metis bot.not_eq_extremum gr_implies_not0 le_neq_implies_less less_one size_fsingleton size_fsubset)
  by auto

lemma size_gt_1: "1 < size f ⟹ ∃e1 e2 f'. e1 ≠ e2 ∧ f = finsert e1 (finsert e2 f')"
  apply (induct f)
   apply simp
  apply (rule_tac x=x in exI)
  by (metis finsertCI leD not_le_imp_less size_le_1)

end