Theory Abstract_Substitution.List_Extra

theory List_Extra ✐‹contributor ‹Balazs Toth›› 
  imports Main
begin

definition set_list :: "'a set ⇒ 'a list" where
  "set_list S ≡ SOME xs. set xs = S ∧ distinct xs"

lemma set_list_empty [simp]: "set_list {} = []"
  unfolding set_list_def
  by auto

lemma set_list_singleton [simp]: "set_list {x} = [x]"
proof (unfold set_list_def, rule some1_equality, intro ex_ex1I)

  show "⋀xs y. ⟦set xs = {x} ∧ distinct xs; set y = {x} ∧ distinct y⟧ ⟹ xs = y"
    by (metis distinct_card replicate_eqI singleton_iff)
qed (auto simp: finite_distinct_list)

lemma set_list_set [simp]:
  assumes "finite S"
  shows "set (set_list S) = S"
  unfolding set_list_def
  by (rule someI2_ex[OF finite_distinct_list[OF assms]]) argo

lemma set_list_distinct [simp]:
  assumes "finite S"
  shows "distinct (set_list S)"
  unfolding set_list_def
  by (rule someI2_ex[OF finite_distinct_list[OF assms]]) argo

end