theory Nominal2_FSet
imports "../Nominal-General/Nominal2_Base"
        "../Nominal-General/Nominal2_Eqvt"
begin


lemma atom_map_fset_cong:
  shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"
  apply(rule inj_map_fset_cong)
  apply(simp add: inj_on_def)
  done

lemma supp_map_fset_atom:
  shows "supp (map_fset atom S) = supp S"
  unfolding supp_def
  apply(perm_simp)
  apply(simp add: atom_map_fset_cong)
  done

lemma supp_at_fset:
  fixes S::"('a::at_base) fset"
  shows "supp S = fset (map_fset atom S)"
  apply (induct S)
  apply (simp add: supp_empty_fset)
  apply (simp add: supp_insert_fset)
  apply (simp add: supp_at_base)
  done

lemma fresh_star_atom:
  fixes a::"'a::at_base"
  shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S"
  apply (induct S)
  apply (simp add: fresh_set_empty)
  apply simp
  apply (unfold fresh_def)
  apply (simp add: supp_of_finite_insert)
  apply (rule conjI)
  apply (unfold fresh_star_def)
  apply simp
  apply (unfold fresh_def)
  apply (simp add: supp_at_base supp_atom)
  apply clarify
  apply auto
  done

end