theory Nominal2_FSet

imports "../Nominal-General/Nominal2_Supp"

        "../Nominal-General/Nominal2_Atoms" 

        "../Nominal-General/Nominal2_Eqvt" 

        FSet 

begin

lemma permute_rsp_fset[quot_respect]:

  shows "(op = ===> list_eq ===> list_eq) permute permute"

  apply(simp)

  apply(clarify)

  apply(simp add: eqvts[symmetric])  

  apply(subst permute_minus_cancel(1)[symmetric, of "xb"])

  apply(subst mem_eqvt[symmetric])

  apply(subst (2) permute_minus_cancel(1)[symmetric, of "xb"])

  apply(subst mem_eqvt[symmetric])

  apply(simp)

  done

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 (lifting permute_zero [where 'a="'a list"])

  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x"

    by (lifting permute_plus [where 'a="'a list"])

qed

end

lemma permute_fset[simp]:

  fixes S::"('a::pt) fset"

  shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"

  and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"

  by (lifting permute_list.simps)

declare permute_fset[eqvt]

lemma fmap_eqvt[eqvt]: 

  shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"

  by (lifting map_eqvt)

lemma fset_to_set_eqvt [eqvt]: 

  shows "p \<bullet> (fset_to_set S) = fset_to_set (p \<bullet> S)"

  by (lifting set_eqvt)

lemma fin_fset_to_set[simp]:

  shows "finite (fset_to_set S)"

  by (induct S) (simp_all)

lemma supp_fset_to_set:

  shows "supp (fset_to_set S) = supp S"

  unfolding supp_def

  by (perm_simp) (simp add: fset_cong)

lemma supp_fempty:

  shows "supp {||} = {}"

  unfolding supp_def

  by simp

lemma supp_finsert:

  fixes x::"'a::fs"

  shows "supp (finsert x S) = supp x \<union> supp S"

  apply(subst supp_fset_to_set[symmetric])

  apply(simp add: supp_fset_to_set)

  apply(simp add: supp_of_fin_insert)

  apply(simp add: supp_fset_to_set)

  done

instance fset :: (fs) fs

  apply (default)

  apply (induct_tac x rule: fset_induct)

  apply (simp add: supp_fempty)

  apply (simp add: supp_finsert)

  apply (simp add: finite_supp)

  done

lemma atom_fmap_cong:

  shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y"

  apply(rule inj_fmap_eq_iff)

  apply(simp add: inj_on_def)

  done

lemma supp_fmap_atom:

  shows "supp (fmap atom S) = supp S"

  unfolding supp_def

  apply(perm_simp)

  apply(simp add: atom_fmap_cong)

  done

lemma supp_at_fset:

  fixes S::"('a::at_base) fset"

  shows "supp S = fset_to_set (fmap atom S)"

  apply (induct S)

  apply (simp add: supp_fempty)

  apply (simp add: supp_finsert)

  apply (simp add: supp_at_base)

  done

lemma fresh_star_atom:

  fixes a::"'a::at_base"

  shows "fset_to_set S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset_to_set S"

  apply (induct S)

  apply (simp add: fresh_set_empty)

  apply simp

  apply (unfold fresh_def)

  apply (simp add: supp_atom_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