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