--- a/Nominal/FSet.thy	Fri Oct 15 15:24:19 2010 +0900
+++ b/Nominal/FSet.thy	Fri Oct 15 15:52:40 2010 +0900
@@ -256,8 +256,7 @@
 lemma ffold_raw_rsp[quot_respect]:
   shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
   unfolding fun_rel_def
-  apply(auto intro: ffold_raw_rsp_pre)
-  done
+  by(auto intro: ffold_raw_rsp_pre)
 
 lemma concat_rsp_pre:
   assumes a: "list_all2 op \<approx> x x'"
@@ -300,28 +299,7 @@
 qed
 
 
-lemma concat_rsp_unfolded:
-  "\<lbrakk>list_all2 op \<approx> a ba; ba \<approx> bb; list_all2 op \<approx> bb b\<rbrakk> \<Longrightarrow> concat a \<approx> concat b"
-proof -
-  fix a b ba bb
-  assume a: "list_all2 op \<approx> a ba"
-  assume b: "ba \<approx> bb"
-  assume c: "list_all2 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_all2 op \<approx> ba a" by (rule list_all2_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_all2 op \<approx> b bb" by (rule list_all2_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 auto
-qed
+
 
 lemma [quot_respect]:
   shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
@@ -505,11 +483,13 @@
 
 quotient_definition
   "fcard :: 'a fset \<Rightarrow> nat"
-  is fcard_raw
+is
+  fcard_raw
 
 quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-  is map
+is
+  map
 
 quotient_definition
   "fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
@@ -679,14 +659,6 @@
   "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
   by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 
-lemma cons_left_comm:
-  "x # y # xs \<approx> y # x # xs"
-  by auto
-
-lemma cons_left_idem:
-  "x # x # xs \<approx> x # xs"
-  by auto
-
 lemma fset_raw_strong_cases:
   obtains "xs = []"
     | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
@@ -720,7 +692,6 @@
   then show thesis using a c by blast
 qed
 
-
 section {* deletion *}
 
 
@@ -827,7 +798,7 @@
 text {* Lifted theorems *}
 
 lemma not_fin_fnil: "x |\<notin>| {||}"
-  by (lifting not_memb_nil)
+  by (descending) (simp add: memb_def)
 
 lemma fin_finsert_iff[simp]:
   "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
@@ -1025,7 +996,7 @@
   by (induct S) simp_all
 
 lemma inj_fmap_eq_iff:
-  "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
+  "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
   by (lifting inj_map_eq_iff)
 
 lemma fmap_funion: 
@@ -1215,10 +1186,10 @@
 lemma eq_ffilter: 
   shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
   by (descending) (auto simp add: memb_def)
-  
-lemma subset_ffilter: 
-  "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
-unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
+
+lemma subset_ffilter:
+  shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+  unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
 
 
 section {* lemmas transferred from Finite_Set theory *}
@@ -1410,5 +1381,4 @@
 no_notation
   list_eq (infix "\<approx>" 50)
 
-
 end

--- a/Quotient-Paper/Paper.thy	Fri Oct 15 15:24:19 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Fri Oct 15 15:52:40 2010 +0900
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "Quotient"
+imports "Quotient" "Quotient_Syntax"
         "LaTeXsugar"
         "../Nominal/FSet"
 begin
@@ -62,6 +62,29 @@
          (id ---> rep_fset ---> abs_fset) op #"
   by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
 
+lemma concat_rsp_unfolded:
+  "\<lbrakk>list_all2 list_eq a ba; list_eq ba bb; list_all2 list_eq bb b\<rbrakk> \<Longrightarrow> list_eq (concat a) (concat b)"
+proof -
+  fix a b ba bb
+  assume a: "list_all2 list_eq a ba"
+  assume b: "list_eq ba bb"
+  assume c: "list_all2 list_eq 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_all2 list_eq ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
+      have b': "list_eq bb ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+      have c': "list_all2 list_eq b bb" by (rule list_all2_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 "list_eq (concat a) (concat b)" by auto
+qed
+
 (*>*)