--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Nominal2_FSet.thy	Fri Mar 19 08:31:43 2010 +0100
@@ -0,0 +1,107 @@
+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
+
+lemma permute_fset[simp,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 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 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 "\<not> (memb x S) \<Longrightarrow> \<not> (memb y T) \<Longrightarrow> ((x # S) \<approx> (y # T)) = (x = y \<and> S \<approx> T)"*)
+
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
+lemma supp_insert: "supp (insert (x :: 'a :: fs) xs) = supp x \<union> supp xs"
+  oops
+
+lemma supp_finsert:
+  "supp (finsert (x :: 'a :: fs) S) = supp x \<union> supp S"
+  apply (subst supp_fset_to_set[symmetric])
+  apply simp
+  (* apply (simp add: supp_insert supp_fset_to_set) *)
+  oops
+
+instance fset :: (fs) fs
+  apply (default)
+  apply (induct_tac x rule: fset_induct)
+  apply (simp add: supp_def eqvts)
+  (* apply (simp add: supp_finsert) *)
+  (* apply default ? *)
+  oops
+
+end