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

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

lemma fset_both_sides: "(Abs_fset s = f) = (fset (Abs_fset s) = fset f)"

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)"

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 {||} = []"

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"

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)"

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

lemma sorted_list_of_fset_Cons:
"∃h t. (sorted_list_of_fset (finsert s ss)) = h#t"
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)"

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"

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)|}"
by (metis fset_inverse fset_simps(1) fset_simps(2))

lemma fprod_equiv:
"(fset (f |×| f') = s) = (((fset f) × (fset f')) = s)"

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|}"

lemma not_singleton_empty [simp]: "¬ fis_singleton {||}"

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

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

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

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
```