Theory FSet_Extra

(******************************************************************************)
(* Project: Isabelle/UTP Toolkit                                              *)
(* File: FSet_Extra.thy                                                       *)
(* Authors: Frank Zeyda and Simon Foster (University of York, UK)             *)
(* Emails: frank.zeyda@york.ac.uk and simon.foster@york.ac.uk                 *)
(******************************************************************************)

section ‹Finite Sets: extra functions and properties›

theory FSet_Extra
imports
  "HOL-Library.FSet"
  "HOL-Library.Countable_Set_Type"
begin

setup_lifting type_definition_fset

notation fempty ("⦃⦄")
notation fset ("⟨_⟩⇩f")
notation fminus (infixl "-⇩f" 65)

syntax
  "_FinFset" :: "args => 'a fset"    ("⦃(_)⦄")

translations
  "⦃x, xs⦄" == "CONST finsert x ⦃xs⦄"
  "⦃x⦄" == "CONST finsert x ⦃⦄"

term "fBall"

definition FUnion :: "'a fset fset ⇒ 'a fset" ("⋃⇩f_" [90] 90) where
"FUnion xs = Abs_fset (⋃x∈⟨xs⟩⇩f. ⟨x⟩⇩f)"

definition FInter :: "'a fset fset ⇒ 'a fset" ("⋂⇩f_" [90] 90) where
"FInter xs = Abs_fset (⋂x∈⟨xs⟩⇩f. ⟨x⟩⇩f)"

text ‹Finite power set›

definition FinPow :: "'a fset ⇒ 'a fset fset" where
"FinPow xs = Abs_fset (Abs_fset ` Pow ⟨xs⟩⇩f)"

text ‹Set of all finite subsets of a set›

definition Fow :: "'a set ⇒ 'a fset set" where
"Fow A = {x. ⟨x⟩⇩f ⊆ A}"

declare Abs_fset_inverse [simp]

lemma fset_intro:
  "fset x = fset y ⟹ x = y"
  by (simp add:fset_inject)

lemma fset_elim:
  "⟦ x = y; fset x = fset y ⟹ P ⟧ ⟹ P"
  by (auto)

lemma fmember_intro:
  "⟦ x ∈ fset(xs) ⟧ ⟹ x |∈| xs"
  .

lemma fmember_elim:
  "⟦ x |∈| xs; x ∈ fset(xs) ⟹ P ⟧ ⟹ P"
  .

lemma fnmember_intro [intro]:
  "⟦ x ∉ fset(xs) ⟧ ⟹ x |∉| xs"
  .

lemma fnmember_elim [elim]:
  "⟦ x |∉| xs; x ∉ fset(xs) ⟹ P ⟧ ⟹ P"
  .

lemma fsubset_intro [intro]:
  "⟨xs⟩⇩f ⊆ ⟨ys⟩⇩f ⟹ xs |⊆| ys"
  by (metis less_eq_fset.rep_eq)

lemma fsubset_elim [elim]:
  "⟦ xs |⊆| ys; ⟨xs⟩⇩f ⊆ ⟨ys⟩⇩f ⟹ P ⟧ ⟹ P"
  by (metis less_eq_fset.rep_eq)

lemma fBall_intro [intro]:
  "Ball ⟨A⟩⇩f P ⟹ fBall A P"
  by (metis (poly_guards_query) fBallI)

lemma fBall_elim [elim]:
  "⟦ fBall A P; Ball ⟨A⟩⇩f P ⟹ Q ⟧ ⟹ Q"
  by (metis fBallE)

lift_definition finset :: "'a list ⇒ 'a fset" is set ..

context linorder
begin

lemma sorted_list_of_set_inj:
  "⟦ finite xs; finite ys; sorted_list_of_set xs = sorted_list_of_set ys ⟧
   ⟹ xs = ys"
  apply (simp add:sorted_list_of_set_def)
  apply (induct xs rule:finite_induct)
   apply (induct ys rule:finite_induct)
    apply (simp_all)
   apply (metis finite.insertI insert_not_empty sorted_list_of_set_def sorted_list_of_set_empty sorted_list_of_set_eq_Nil_iff)
  apply (metis finite.insertI finite_list set_remdups set_sort sorted_list_of_set_def sorted_list_of_set_sort_remdups)
  done

definition flist :: "'a fset ⇒ 'a list" where
"flist xs = sorted_list_of_set (fset xs)"

lemma flist_inj: "inj flist"
  apply (simp add:flist_def inj_on_def)
  apply (clarify)
  apply (rename_tac x y)
  apply (subgoal_tac "fset x = fset y")
   apply (simp add:fset_inject)
  apply (rule sorted_list_of_set_inj, simp_all)
  done

lemma flist_props [simp]:
  "sorted (flist xs)"
  "distinct (flist xs)"
  by (simp_all add:flist_def)

lemma flist_empty [simp]:
  "flist ⦃⦄ = []"
  by (simp add:flist_def)

lemma flist_inv [simp]: "finset (flist xs) = xs"
  by (simp add:finset_def flist_def fset_inverse)

lemma flist_set [simp]: "set (flist xs) = fset xs"
  by (simp add:finset_def flist_def fset_inverse)

lemma fset_inv [simp]: "⟦ sorted xs; distinct xs ⟧ ⟹ flist (finset xs) = xs"
  apply (simp add:finset_def flist_def fset_inverse)
  apply (metis local.sorted_list_of_set_sort_remdups local.sorted_sort_id remdups_id_iff_distinct)
  done

lemma fcard_flist:
  "fcard xs = length (flist xs)"
  apply (simp add:fcard_def)
  apply (fold flist_set)
  apply (unfold distinct_card[OF flist_props(2)])
  apply (rule refl)
  done

lemma flist_nth:
  "i < fcard vs ⟹ flist vs ! i |∈| vs"
  apply (simp add: flist_def fcard_def)
  apply (metis fcard.rep_eq fcard_flist finset.rep_eq flist_def flist_inv nth_mem)
  done

definition fmax :: "'a fset ⇒ 'a" where
"fmax xs = (if (xs = ⦃⦄) then undefined else last (flist xs))"

end

definition flists :: "'a fset ⇒ 'a list set" where
"flists A = {xs. distinct xs ∧ finset xs = A}"

lemma flists_nonempty: "∃ xs. xs ∈ flists A"
  apply (simp add: flists_def)
  apply (metis Abs_fset_cases Abs_fset_inverse finite_distinct_list finite_fset finset.rep_eq)
  done

lemma flists_elem_uniq: "⟦ x ∈ flists A; x ∈ flists B ⟧ ⟹ A = B"
  by (simp add: flists_def)

definition flist_arb :: "'a fset ⇒ 'a list" where
"flist_arb A = (SOME xs. xs ∈ flists A)"

lemma flist_arb_distinct [simp]: "distinct (flist_arb A)"
  by (metis (mono_tags) flist_arb_def flists_def flists_nonempty mem_Collect_eq someI_ex)

lemma flist_arb_inv [simp]: "finset (flist_arb A) = A"
  by (metis (mono_tags) flist_arb_def flists_def flists_nonempty mem_Collect_eq someI_ex)

lemma flist_arb_inj:
  "inj flist_arb"
  by (metis flist_arb_inv injI)

lemma flist_arb_lists: "flist_arb ` Fow A ⊆ lists A"
  apply (auto simp: Fow_def flist_arb_def flists_def)
  using finset.rep_eq
  by (metis (mono_tags, lifting) finite_distinct_list finite_fset fset_inverse someI_ex subset_eq)

lemma countable_Fow:
  fixes A :: "'a set"
  assumes "countable A"
  shows "countable (Fow A)"
proof -
  from assms obtain to_nat_list :: "'a list ⇒ nat" where "inj_on to_nat_list (lists A)"
    by blast
  thus ?thesis
    apply (simp add: countable_def)
    apply (rule_tac x="to_nat_list ∘ flist_arb" in exI)
    apply (rule comp_inj_on)
     apply (metis flist_arb_inv inj_on_def)
    apply (simp add: flist_arb_lists subset_inj_on)
    done
qed

definition flub :: "'a fset set ⇒ 'a fset ⇒ 'a fset" where
"flub A t = (if (∀ a∈A. a |⊆| t) then Abs_fset (⋃x∈A. ⟨x⟩⇩f) else t)"

lemma finite_Union_subsets:
  "⟦ ∀ a ∈ A. a ⊆ b; finite b ⟧ ⟹ finite (⋃A)"
  by (metis Sup_le_iff finite_subset)

lemma finite_UN_subsets:
  "⟦ ∀ a ∈ A. B a ⊆ b; finite b ⟧ ⟹ finite (⋃a∈A. B a)"
  by (metis UN_subset_iff finite_subset)

lemma flub_rep_eq:
  "⟨flub A t⟩⇩f = (if (∀ a∈A. a |⊆| t) then (⋃x∈A. ⟨x⟩⇩f) else ⟨t⟩⇩f)"
  apply (subgoal_tac "(if (∀ a∈A. a |⊆| t) then (⋃x∈A. ⟨x⟩⇩f) else ⟨t⟩⇩f) ∈ {x. finite x}")
   apply (auto simp add:flub_def)
  apply (rule finite_UN_subsets[of _ _ "⟨t⟩⇩f"])
   apply (auto)
  done

definition fglb :: "'a fset set ⇒ 'a fset ⇒ 'a fset" where
"fglb A t = (if (A = {}) then t else Abs_fset (⋂x∈A. ⟨x⟩⇩f))"

lemma fglb_rep_eq:
  "⟨fglb A t⟩⇩f = (if (A = {}) then ⟨t⟩⇩f else (⋂x∈A. ⟨x⟩⇩f))"
  apply (subgoal_tac "(if (A = {}) then ⟨t⟩⇩f else (⋂x∈A. ⟨x⟩⇩f)) ∈ {x. finite x}")
   apply (metis Abs_fset_inverse fglb_def)
  apply (auto)
  apply (metis finite_INT finite_fset)
  done

lemma FinPow_rep_eq [simp]:
  "fset (FinPow xs) = {ys. ys |⊆| xs}"
  apply (subgoal_tac "finite (Abs_fset ` Pow ⟨xs⟩⇩f)")
   apply (auto simp add: FinPow_def)
   apply (rename_tac x' y')
   apply (subgoal_tac "finite x'")
    apply (auto)
   apply (metis finite_fset finite_subset)
  apply (metis (full_types) Pow_iff fset_inverse imageI less_eq_fset.rep_eq)
  done

lemma FUnion_rep_eq [simp]:
  "⟨⋃⇩f xs⟩⇩f = (⋃x∈⟨xs⟩⇩f. ⟨x⟩⇩f)"
  by (simp add:FUnion_def)

lemma FInter_rep_eq [simp]:
  "xs ≠ ⦃⦄ ⟹ ⟨⋂⇩f xs⟩⇩f = (⋂x∈⟨xs⟩⇩f. ⟨x⟩⇩f)"
  apply (simp add:FInter_def)
  apply (subgoal_tac "finite (⋂x∈⟨xs⟩⇩f. ⟨x⟩⇩f)")
   apply (simp)
  apply (metis (poly_guards_query) bot_fset.rep_eq fglb_rep_eq finite_fset fset_inverse)
  done

lemma FUnion_empty [simp]:
  "⋃⇩f ⦃⦄ = ⦃⦄"
  by (auto simp add:FUnion_def)

lemma FinPow_member [simp]:
  "xs |∈| FinPow xs"
  by auto

lemma FUnion_FinPow [simp]:
  "⋃⇩f (FinPow x) = x"
  by (auto simp add: less_eq_fset_def)

lemma Fow_mem [iff]: "x ∈ Fow A ⟷ ⟨x⟩⇩f ⊆ A"
  by (auto simp add:Fow_def)

lemma Fow_UNIV [simp]: "Fow UNIV = UNIV"
  by (simp add:Fow_def)

lift_definition FMax :: "('a::linorder) fset ⇒ 'a" is "Max" .

end