--- a/FSet.thy	Fri Dec 04 09:33:32 2009 +0100
+++ b/FSet.thy	Fri Dec 04 10:12:17 2009 +0100
@@ -299,7 +299,7 @@
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply(tactic {* all_inj_repabs_tac' @{context} [rel_refl] [trans2] 1 *})
 apply(tactic {* clean_tac @{context} 1*})
 done
 
@@ -327,7 +327,7 @@
 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac' lthy [rel_refl] [trans2] *}
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
@@ -389,6 +389,9 @@
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 done
 
 lemma list_induct_part:

--- a/LFex.thy	Fri Dec 04 09:33:32 2009 +0100
+++ b/LFex.thy	Fri Dec 04 10:12:17 2009 +0100
@@ -258,10 +258,12 @@
          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 apply - 
-apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
-apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-prefer 2
+apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *})
+(*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
+apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *})
 apply(tactic {* clean_tac @{context} 1 *})
+*)
+(*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)
 (*
 Profiling:
 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
@@ -270,8 +272,6 @@
 ML_prf {* PolyML.profiling 1 *}
 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 *)
-apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *})
-(*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)
 done
 
 (* Does not work:

--- a/QuotMain.thy	Fri Dec 04 09:33:32 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 10:12:17 2009 +0100
@@ -813,6 +813,32 @@
      | _ => no_tac)
 *}
 
+ML {*
+val APPLY_RSP1_TAC =
+  Subgoal.FOCUS (fn {concl, asms, context,...} =>
+    case ((HOLogic.dest_Trueprop (term_of concl))) of
+       ((R2 $ (f $ x) $ (g $ y))) =>
+          let
+            val (asmf, asma) = find_qt_asm (map term_of asms);
+          in
+            if (fastype_of asmf) = (fastype_of f) then no_tac else let
+              val ty_a = fastype_of x;
+              val ty_b = fastype_of asma;
+              val ty_c = range_type (type_of f);
+(*              val ty_d = range_type (type_of asmf);*)
+              val thy = ProofContext.theory_of context;
+              val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c];
+              val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
+              val t_inst = [NONE, NONE, NONE, SOME R2, SOME f, SOME g, SOME x, SOME y];
+              val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP1}
+              (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*)
+            in
+              rtac thm 1
+            end
+          end
+     | _ => no_tac)
+*}
+
 
 ML {*
 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
@@ -1000,8 +1026,8 @@
 fun inj_repabs_tac' ctxt rel_refl trans2 =
   (FIRST' [
     inj_repabs_tac_fast ctxt trans2,
-    NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
-                (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
+    NDT ctxt "A" (APPLY_RSP1_TAC ctxt THEN'
+                (RANGE [SOLVES' (quotient_tac ctxt),
                         quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
     NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),

--- a/QuotScript.thy	Fri Dec 04 09:33:32 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 10:12:17 2009 +0100
@@ -329,9 +329,8 @@
 lemma REP_ABS_RSP_LEFT:
   assumes q: "QUOTIENT R Abs Rep"
   and     a: "R x1 x2"
-  and   "R (Rep (Abs x1)) x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
+using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
@@ -382,6 +381,11 @@
 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto
 
 (* ask peter: no use of q1 q2 *)
+(* Cez: I can answer,
+   In the following theorem R2 can be instantiated with anything,
+   but we know some of the types of the Rep and Abs functions;
+   so by solving QUOTIENT assumptions we can get a unique R2 that
+   will be provable; which is why we need to use APPLY_RSP1 *)
 lemma APPLY_RSP:
   assumes q1: "QUOTIENT R1 Abs1 Rep1"
   and     q2: "QUOTIENT R2 Abs2 Rep2"
@@ -389,6 +393,12 @@
   shows "R2 (f x) (g y)"
 using a by (rule FUN_REL_IMP)
 
+lemma APPLY_RSP1:
+  assumes q: "QUOTIENT R1 Abs1 Rep1"
+  and     a: "(R1 ===> R2) f g" "R1 x y"
+  shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"
+using a by (rule FUN_REL_IMP)
+
 lemma APPLY_RSP2:
   assumes a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"