theory Nominal2_FSet
imports "../Nominal-General/Nominal2_Supp"
        FSet 
begin

lemma permute_rsp_fset[quot_respect]:
  "(op = ===> list_eq ===> list_eq) permute permute"
  apply (simp add: eqvts[symmetric])
  apply clarify
  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 (erule_tac x="- x \<bullet> xb" in allE)
  apply simp
  done

instantiation FSet.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[eqvt]:
  "(p \<bullet> {||}) = ({||} :: 'a::pt fset)"
  "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
  by (lifting permute_list.simps)

lemma fmap_eqvt[eqvt]: 
  shows "p \<bullet> (fmap f l) = fmap (p \<bullet> f) (p \<bullet> l)"
  by (lifting map_eqvt)

lemma fset_to_set_eqvt[eqvt]: 
  shows "p \<bullet> (fset_to_set x) = fset_to_set (p \<bullet> x)"
  by (lifting set_eqvt)

lemma fin_fset_to_set:
  shows "finite (fset_to_set x)"
  by (induct x) (simp_all)

lemma supp_fset_to_set:
  "supp (fset_to_set x) = supp x"
  apply (simp add: supp_def)
  apply (simp add: eqvts)
  apply (simp add: fset_cong)
  done

lemma atom_fmap_cong:
  shows "(fmap atom x = fmap atom y) = (x = y)"
  apply(rule inj_fmap_eq_iff)
  apply(simp add: inj_on_def)
  done

lemma supp_fmap_atom:
  shows "supp (fmap atom x) = supp x"
  unfolding supp_def
  apply (perm_simp)
  apply (simp add: atom_fmap_cong)
  done

lemma supp_atom_insert:
  "finite (xs :: atom set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs"
  apply (simp add: supp_finite_atom_set)
  apply (simp add: supp_atom)
  done

lemma atom_image_cong:
  shows "(atom ` X = atom ` Y) = (X = Y)"
  apply(rule inj_image_eq_iff)
  apply(simp add: inj_on_def)
  done

lemma atom_eqvt_raw:
  fixes p::"perm"
  shows "(p \<bullet> atom) = atom"
  apply(perm_simp)
  apply(simp)
  done

lemma supp_finite_at_set:
  fixes S::"('a :: at) set"
  assumes a: "finite S"
  shows "supp S = atom ` S"
  apply(rule finite_supp_unique)
  apply(simp add: supports_def)
  apply (rule finite_induct[OF a])
  apply (simp add: eqvts)
  apply (simp)
  apply clarify
  apply (subst atom_image_cong[symmetric])
  apply (subst atom_eqvt_raw[symmetric])
  apply (subst eqvts[symmetric])
  apply (rule swap_set_not_in)
  apply simp_all
  apply(rule finite_imageI)
  apply(rule a)
  apply (subst atom_image_cong[symmetric])
  apply (subst atom_eqvt_raw[symmetric])
  apply (subst eqvts[symmetric])
  apply (rule swap_set_in)
  apply simp_all
  done

lemma supp_at_insert:
  "finite (xs :: ('a :: at) set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs"
  apply (simp add: supp_finite_at_set)
  apply (simp add: supp_at_base)
  done

lemma supp_atom_finsert:
  "supp (finsert (x :: atom) S) = supp x \<union> supp S"
  apply (subst supp_fset_to_set[symmetric])
  apply (simp add: supp_finite_atom_set)
  apply (simp add: supp_atom_insert[OF fin_fset_to_set])
  apply (simp add: supp_fset_to_set)
  done

lemma supp_at_finsert:
  "supp (finsert (x :: 'a :: at) S) = supp x \<union> supp S"
  apply (subst supp_fset_to_set[symmetric])
  apply (simp add: supp_finite_atom_set)
  apply (simp add: supp_at_insert[OF fin_fset_to_set])
  apply (simp add: supp_fset_to_set)
  done

lemma supp_fempty:
  "supp {||} = {}"
  by (simp add: supp_def eqvts)

instance fset :: (at) fs
  apply (default)
  apply (induct_tac x rule: fset_induct)
  apply (simp add: supp_fempty)
  apply (simp add: supp_at_finsert)
  apply (simp add: supp_at_base)
  done

lemma supp_at_fset:
  "supp (fset :: 'a :: at fset) = fset_to_set (fmap atom fset)"
  apply (induct fset)
  apply (simp add: supp_fempty)
  apply (simp add: supp_at_finsert)
  apply (simp add: supp_at_base)
  done

end