--- a/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 10:24:39 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Wed Apr 21 10:34:10 2010 +0200
@@ -9,47 +9,65 @@
   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by (lifting list.exhaust)
 
-(* PROBLEM: these lemmas needs to be restated, since  *)
-(* concat.simps(1) and concat.simps(2) contain the    *)
-(* type variables ?'a1.0 (which are turned into frees *)
-(* 'a_1                                               *)
-
-lemma concat1:
-  shows "concat [] \<approx> []"
-by (simp)
+lemma list_rel_find_element:
+  assumes a: "x \<in> set a"
+  and b: "list_rel R a b"
+  shows "\<exists>y. (y \<in> set b \<and> R x y)"
+proof -
+  have "length a = length b" using b by (rule list_rel_len)
+  then show ?thesis using a b proof (induct a b rule: list_induct2)
+    case Nil
+    show ?case using Nil.prems by simp
+  next
+    case (Cons x xs y ys)
+    show ?case using Cons by auto
+  qed
+qed
 
-lemma concat2:
-  shows "concat (x # xs) \<approx> x @ concat xs"
-by (simp)
-
-lemma concat_rsp:
-  "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y\<rbrakk> \<Longrightarrow> concat x \<approx> concat y"
-  apply (induct x y arbitrary: x' y' rule: list_induct2')
+lemma concat_rsp_pre:
+  "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y; \<exists>x\<in>set x. xa \<in> set x\<rbrakk> \<Longrightarrow> 
+    \<exists>x\<in>set y. xa \<in> set x"
+  apply clarify
+  apply (frule list_rel_find_element[of _ "x"])
+  apply assumption
+  apply clarify
+  apply (subgoal_tac "ya \<in> set y'")
+  prefer 2
   apply simp
-  defer defer
-  apply (simp only: concat.simps)
-  sorry
+  apply (frule list_rel_find_element[of _ "y'"])
+  apply assumption
+  apply auto
+  done
 
 lemma [quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
   apply (simp only: fun_rel_def)
   apply clarify
-  apply (rule concat_rsp)
+  apply (simp (no_asm))
+  apply rule
+  apply rule
+  apply (erule concat_rsp_pre)
   apply assumption+
+  apply (rule concat_rsp_pre)
+  prefer 4
+  apply assumption
+  apply (rule list_rel_symp[OF list_eq_equivp])
+  apply assumption
+  apply (rule equivp_symp[OF list_eq_equivp])
+  apply assumption
+  apply (rule list_rel_symp[OF list_eq_equivp])
+  apply assumption
   done
 
 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
   by (metis nil_rsp list_rel.simps(1) pred_compI)
 
 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
-  apply (rule eq_reflection)
-  apply auto
-  done
+  by (rule eq_reflection) auto
 
 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
   unfolding list_eq.simps
-  apply(simp only: set_map set_in_eq)
-  done
+  by (simp only: set_map set_in_eq)
 
 lemma quotient_compose_list_pre:
   "(list_rel op \<approx> OOO op \<approx>) r s =
@@ -106,7 +124,7 @@
     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
   unfolding Quotient_def comp_def
   apply (rule)+
-  apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
+  apply (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
   apply (rule)
   apply (rule)
   apply (rule)
@@ -123,7 +141,7 @@
 
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
-  apply(lifting concat1)
+  apply(lifting concat.simps(1))
   apply(cleaning)
   apply(simp add: comp_def bot_fset_def)
   done
@@ -144,10 +162,10 @@
 
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
-  apply(lifting concat2)
-  apply(cleaning)
+  apply (lifting concat.simps(2))
+  apply (cleaning)
   apply (simp add: finsert_def fconcat_def comp_def)
-  apply cleaning
+  apply (cleaning)
   done
 
 (* TBD *)