(******************************************************************************)
(* 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"    (‹{(_)}›)
syntax_consts
  "_FinFset" == finsert
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 inj_on_subset)
    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