--- a/Nominal/FSet.thy	Tue Apr 13 15:00:49 2010 +0200
+++ b/Nominal/FSet.thy	Tue Apr 13 15:59:53 2010 +0200
@@ -159,15 +159,15 @@
         apply (simp add: memb_def)
         apply clarify
         by metis
+    next
       case False
-        then have ?thesis using f1 f2 apply -
+      then show ?thesis using f1 f2 apply -
         apply (rule_tac x="a" in exI)
         apply (rule_tac x="xs" in exI)
         apply (simp add: memb_def)
         done
     qed
   qed
-qed
 
 lemma singleton_fcard_1: "set a = {b} \<Longrightarrow> fcard_raw a = Suc 0"
   apply (induct a)
@@ -345,6 +345,36 @@
   apply (simp add: memb_cons_iff rsp_fold_def)
   done
 
+lemma ffold_raw_rsp_pre:
+  "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
+  apply (induct a arbitrary: b)
+  apply (simp add: hd_in_set memb_absorb memb_def none_mem_nil)
+  apply (simp add: ffold_raw.simps)
+  apply (rule conjI)
+  apply (rule_tac [!] impI)
+  apply (rule_tac [!] conjI)
+  apply (rule_tac [!] impI)
+  apply (simp add: in_set_code memb_cons_iff memb_def)
+  apply (metis)
+  apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))
+  defer
+  apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))
+  apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
+  apply (simp only:)
+  apply (rule_tac f="f a1" in arg_cong)
+  apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
+  apply simp
+  apply (simp add: memb_delete_raw)
+  apply (metis memb_cons_iff)
+  apply (erule memb_commute_ffold_raw)
+  apply (drule_tac x="a1" in spec)
+  apply (simp add: memb_cons_iff)
+  done
+
+lemma [quot_respect]:
+  "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
+  by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
+
 primrec
   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
@@ -633,6 +663,11 @@
   "(e |\<in>| (l |\<inter>| r)) = (e |\<in>| l \<and> e |\<in>| r)"
   by (lifting memb_finter_raw)
 
+lemma expand_fset_eq:
+  "(xs = ys) = (\<forall>x. (x |\<in>| xs) = (x |\<in>| ys))"
+  by (lifting list_eq.simps[simplified memb_def[symmetric]])
+
+
 ML {*
 fun dest_fsetT (Type ("FSet.fset", [T])) = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);