Theory Indexed_FSet

theory Indexed_FSet

text It is convenient to address the members of a finite set by a natural number, and
also to convert a finite set to a list.

context includes fset.lifting
lift_definition fset_from_list :: "'a list => 'a fset" is set by (rule finite_set)
lemma mem_fset_from_list[simp]: "x |∈| fset_from_list l   x  set l" by transfer rule
lemma fimage_fset_from_list[simp]: "f |`| fset_from_list l = fset_from_list (map f l)"  by transfer auto
lemma fset_fset_from_list[simp]: "fset (fset_from_list l) = set l"  by transfer auto
lemmas fset_simps[simp] = set_simps[Transfer.transferred]
lemma size_fset_from_list[simp]: "distinct l  size (fset_from_list l) = length l"
  by (induction l) auto

definition list_of_fset :: "'a fset  'a list" where
  "list_of_fset s = (SOME l. fset_from_list l = s  distinct l)"

lemma fset_from_list_of_fset[simp]: "fset_from_list (list_of_fset s) = s"
  and distinct_list_of_fset[simp]: "distinct (list_of_fset s)"
  unfolding atomize_conj list_of_fset_def 
  by (transfer, rule someI_ex, rule finite_distinct_list)

lemma length_list_of_fset[simp]: "length (list_of_fset s) = size s"
  by (metis distinct_list_of_fset fset_from_list_of_fset size_fset_from_list)

lemma nth_list_of_fset_mem[simp]: "i < size s  list_of_fset s ! i |∈| s"
  by (metis fset_from_list_of_fset length_list_of_fset mem_fset_from_list nth_mem)

inductive indexed_fmember :: "'a  nat  'a fset  bool" ("_ |∈|⇘_ _" [50,50,50] 50 ) where
  "i < size s  list_of_fset s ! i |∈|⇘is"

lemma indexed_fmember_is_fmember: "x |∈|⇘is  x |∈| s"
proof (induction rule: indexed_fmember.induct)
case (1 i s)
   hence "i < length (list_of_fset s)" by (metis length_list_of_fset)
   hence "list_of_fset s ! i  set (list_of_fset s)" by (rule nth_mem)
   thus "list_of_fset s ! i |∈| s" by (metis mem_fset_from_list fset_from_list_of_fset)

lemma fmember_is_indexed_fmember:
  assumes "x |∈| s"
  shows "i. x |∈|⇘is"
  from assms
  have "x  set (list_of_fset s)" using mem_fset_from_list by fastforce
  then obtain i where "i < length (list_of_fset s)" and "x = list_of_fset s ! i" by (metis in_set_conv_nth)
  hence "x |∈|⇘is"  by (simp add: indexed_fmember.simps)
  thus ?thesis..

lemma indexed_fmember_unique: "x |∈|⇘is  y |∈|⇘js  x = y  i = j"
  by (metis distinct_list_of_fset indexed_fmember.cases length_list_of_fset nth_eq_iff_index_eq)

definition indexed_members :: "'a fset  (nat × 'a) list" where
  "indexed_members s = zip [0..<size s] (list_of_fset s)"

lemma mem_set_indexed_members:
  "(i,x)  set (indexed_members s)  x |∈|⇘is"
  unfolding indexed_members_def indexed_fmember.simps
  by (force simp add: set_zip)

lemma mem_set_indexed_members'[simp]:
  "t  set (indexed_members s)  snd t |∈|⇘fst ts"
  by (cases t, simp add: mem_set_indexed_members)

definition fnth (infixl "|!|" 100)  where
  "s |!| n = list_of_fset s ! n"
lemma fnth_indexed_fmember: "i < size s  s |!| i |∈|⇘is"
  unfolding fnth_def by (rule indexed_fmember.intros)
lemma indexed_fmember_fnth: "x |∈|⇘is  (s |!| i = x  i < size s)"
 unfolding fnth_def by (metis indexed_fmember.simps)

definition fidx :: "'a fset  'a  nat" where
  "fidx s x = (SOME i. x |∈|⇘is)"

lemma fidx_eq[simp]: "x |∈|⇘is  fidx s x = i"
  unfolding fidx_def
  by (rule someI2)(auto simp add: indexed_fmember_fnth fnth_def nth_eq_iff_index_eq)

lemma fidx_inj[simp]: "x |∈| s  y |∈| s  fidx s x = fidx s y  x = y"
  by (auto dest!: fmember_is_indexed_fmember simp add: indexed_fmember_unique)

lemma inj_on_fidx: "inj_on (fidx vertices) (fset vertices)"
  by (rule inj_onI) (auto simp: fmember.rep_eq [symmetric])