theory Nominal2_FSet

imports FSet Nominal2_Supp

begin

lemma permute_rsp_fset[quot_respect]:

  "(op = ===> op \<approx> ===> op \<approx>) 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

term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"

quotient_definition

  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

is

  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"

lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"

  by (rule permute_zero)

lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"

  by (lifting permute_list_zero)

lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"

  by (rule permute_plus)

lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"

  by (lifting permute_list_plus)

instance

  apply default

  apply (rule permute_fset_zero)

  apply (rule permute_fset_plus)

  done

end

  "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 map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"

  apply (induct l)

  apply (simp_all)

  apply (simp only: eqvt_apply)

  done

lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"

  by (lifting map_eqvt)

lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"

  by (lifting set_eqvt)

lemma fin_fset_to_set:

  "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:

  "supp (fmap atom x) = supp x"

  apply (simp add: supp_def)

  apply (simp add: eqvts eqvts_raw 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"

  by (simp add: expand_fun_eq permute_fun_def atom_eqvt)

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