theory Nominal2_FSet
imports "../Nominal-General/Nominal2_Base"
        "../Nominal-General/Nominal2_Eqvt" 
        "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet"
begin

lemma permute_fset_rsp[quot_respect]:
  shows "(op = ===> list_eq ===> list_eq) permute permute"
  by (simp add: set_eqvt[symmetric])

instantiation fset :: (pt) pt
begin

quotient_definition
  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
is
  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"

instance 
proof
  fix x :: "'a fset" and p q :: "perm"
  show "0 \<bullet> x = x" by (descending) (simp)
  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
qed

end

lemma permute_fset[simp, eqvt]:
  fixes S::"('a::pt) fset"
  shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
  and   "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
  by (lifting permute_list.simps)

lemma map_fset_eqvt[eqvt]: 
  shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
  by (lifting map_eqvt)

lemma fset_eqvt[eqvt]: 
  shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
  by (lifting set_eqvt)

lemma supp_fset [simp]:
  shows "supp (fset S) = supp S"
  unfolding supp_def
  by (perm_simp) (simp add: fset_cong)

lemma supp_empty_fset [simp]:
  shows "supp {||} = {}"
  unfolding supp_def
  by simp

lemma supp_insert_fset [simp]:
  fixes x::"'a::fs"
  and   S::"'a fset"
  shows "supp (insert_fset x S) = supp x \<union> supp S"
  apply(subst supp_fset[symmetric])
  apply(simp add: supp_fset supp_of_fin_insert)
  done

lemma fset_finite_supp:
  fixes S::"('a::fs) fset"
  shows "finite (supp S)"
  by (induct S) (simp_all add: finite_supp)


subsection {* finite sets are fs-types *}

instance fset :: (fs) fs
  apply (default)
  apply (rule fset_finite_supp)
  done

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_fin_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