--- a/Quot/Examples/FSet3.thy	Tue Jan 05 18:10:20 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Wed Jan 06 08:24:37 2010 +0100
@@ -234,10 +234,11 @@
 as
  "concat"
 
-lemma fconcat_rsp[quot_respect]:
+(*lemma fconcat_rsp[quot_respect]:
   shows "((list_rel op \<approx>) ===> op \<approx>) concat concat"
 apply(auto)
 sorry
+*)
 
 (* PROBLEM: these lemmas needs to be restated, since  *)
 (* concat.simps(1) and concat.simps(2) contain the    *)
@@ -251,17 +252,42 @@
   shows "concat (x # xs) \<approx>  x @ concat xs"
 by (simp)
 
+lemma concat_rsp[quot_respect]:
+  shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat"
+sorry
+
+lemma nil_rsp2: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []"
+sledgehammer
+apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
+atp_minimize [atp=remote_vampire] FSet3.nil_rsp list_rel.simps(1) pred_comp.intros
+thm pred_comp_def
+
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
 apply(lifting_setup concat1)
 apply(regularize)
-apply(injection)
 defer
 apply(cleaning)
 apply(simp add: comp_def)
 apply(cleaning)
 apply(fold fempty_def[simplified id_simps])
 apply(rule refl)
+apply(injection)
+apply(rule apply_rsp[of "(list_rel (op \<approx>)) OO (op \<approx>) OO (list_rel (op \<approx>))" _ _ "op \<approx>" "concat" _ "[]" "((map rep_fset \<circ> rep_fset) ((abs_fset \<circ> map abs_fset) []))"])
+prefer 2
+ML_prf {* fun dest_comb (f $ a) = (f, a) *}
+apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (fst o dest_comb) 1 *})
+prefer 3
+apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (snd o dest_comb) 1 *})
+apply(rule rep_abs_rsp[of _ "(abs_fset \<circ> map abs_fset)" "(map rep_fset \<circ> rep_fset)"])
+prefer 3
+apply(rule rep_abs_rsp[of _ "((map rep_fset \<circ> rep_fset) ---> abs_fset)" "(abs_fset \<circ> map abs_fset) ---> rep_fset"])
+prefer 2
+apply(rule concat_rsp)
+prefer 3
+thm nil_rsp
+apply(tactic {* rep_abs_rsp_tac @{context} 1 *})
+apply(rule rep_abs_rsp)
 sorry
 
 lemma fconcat_insert:

--- a/Quot/quotient_tacs.ML	Tue Jan 05 18:10:20 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 06 08:24:37 2010 +0100
@@ -1,11 +1,13 @@
 signature QUOTIENT_TACS =
 sig
     val regularize_tac: Proof.context -> int -> tactic
+    val injection_tac: Proof.context -> int -> tactic
     val all_injection_tac: Proof.context -> int -> tactic
     val clean_tac: Proof.context -> int -> tactic
     val procedure_tac: Proof.context -> thm -> int -> tactic
     val lift_tac: Proof.context -> thm -> int -> tactic
     val quotient_tac: Proof.context -> int -> tactic
+    val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
 end;
 
 structure Quotient_Tacs: QUOTIENT_TACS =
@@ -637,4 +639,4 @@
       (all_injection_tac ctxt, msg2),
       (clean_tac ctxt, msg3)]
 
-end; (* structure *)
\ No newline at end of file
+end; (* structure *)