--- a/Nominal/FSet.thy	Thu May 27 18:37:52 2010 +0200
+++ b/Nominal/FSet.thy	Thu May 27 18:40:10 2010 +0200
@@ -160,10 +160,14 @@
 
 text {* Respectfullness *}
 
-lemma [quot_respect]:
+lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by auto
 
+lemma append_rsp_unfolded:
+  "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w"
+  by auto
+
 lemma [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
   by (auto simp add: sub_list_def)
@@ -350,7 +354,7 @@
   then show ?thesis using f i by auto
 qed
 
-lemma [quot_respect]:
+lemma concat_rsp[quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 proof (rule fun_relI, elim pred_compE)
   fix a b ba bb
@@ -373,6 +377,31 @@
   then show "concat a \<approx> concat b" by simp
 qed
 
+
+
+lemma concat_rsp_unfolded:
+  "\<lbrakk>list_rel op \<approx> a ba; ba \<approx> bb; list_rel op \<approx> bb b\<rbrakk> \<Longrightarrow> concat a \<approx> concat b"
+proof -
+  fix a b ba bb
+  assume a: "list_rel op \<approx> a ba"
+  assume b: "ba \<approx> bb"
+  assume c: "list_rel op \<approx> bb b"
+  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+    fix x
+    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+    next
+      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+      have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a])
+      have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+      have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c])
+      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+    qed
+  qed
+  then show "concat a \<approx> concat b" by simp
+qed
+
 lemma [quot_respect]:
   "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
   by auto
@@ -597,6 +626,11 @@
   apply auto
   done
 
+lemma insert_preserve2:
+  shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
+         (id ---> rep_fset ---> abs_fset) op #"
+  by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+
 lemma [quot_preserve]:
   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]