--- a/IntEx.thy	Thu Dec 03 11:28:19 2009 +0100
+++ b/IntEx.thy	Thu Dec 03 11:33:24 2009 +0100
@@ -259,12 +259,34 @@
   "(LIST_REL R) [] []"
 by simp
 
+thm LAMBDA_PRS[no_vars]
+thm all_prs[no_vars]
+
+lemma test_all_prs:
+  "\<lbrakk>QUOTIENT R absf repf; f = g\<rbrakk> \<Longrightarrow> Ball (Respects R) ((absf ---> id) f) = All g"
+apply(drule all_prs)
+apply(simp)
+done
+
+lemma test:
+  "\<lbrakk>QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2; 
+    (\<lambda>x. Rep2 (f (Abs1 x))) = lhs \<rbrakk> \<Longrightarrow> (Rep1 ---> Abs2) lhs = f"
+apply -
+thm LAMBDA_PRS
+apply(drule LAMBDA_PRS)
+apply(assumption)
+apply(auto)
+done
+
+
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
 apply(simp only: nil_prs)
+apply(rule test_all_prs)
+apply(tactic {* rtac quot 1 *})
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done
 

--- a/QuotMain.thy	Thu Dec 03 11:28:19 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 11:33:24 2009 +0100
@@ -754,15 +754,6 @@
 *}
 
 ML {*
-val weak_lambda_rsp_tac =
-  SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
-       (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i
-     | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i
-     | _ => no_tac)
-*}
-
-ML {*
 val ball_rsp_tac = 
   SUBGOAL (fn (goal, i) =>
     case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
@@ -918,10 +909,9 @@
 *}
 
 ML {*
-fun quot_true_tac ctxt fnctn = CSUBGOAL (fn (goal, i) =>
-  CONVERSION
-    (Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn))) ctxt) i)
+fun quot_true_tac ctxt fnctn = CONVERSION
+    ((Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
 *}
 
 ML {* fun dest_comb (f $ a) = (f, a) *}
@@ -933,61 +923,6 @@
     (Abs a) => snd (Term.dest_abs a)
   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))  *}
 
-ML {*
-fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 =
-  (FIRST' [
-    (* "cong" rule of the of the relation / transitivity*)
-    (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-    NDT ctxt "1" (resolve_tac trans2),
-
-    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    NDT ctxt "2" (lambda_rsp_tac),
-
-    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "3" (rtac @{thm ball_rsp}),
-
-    (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
-    NDT ctxt "4" (ball_rsp_tac),
-
-    (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "5" (rtac @{thm bex_rsp}),
-
-    (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
-    NDT ctxt "6" (bex_rsp_tac),
-
-    (* respectfulness of constants *)
-    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
-
-    (* reflexivity of operators arising from Cong_tac *)
-    NDT ctxt "8" (rtac @{thm refl}),
-
-    (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
-    (* observe ---> *) 
-    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
-                  THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
-
-    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
-    NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
-                (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms)]))),
-
-    (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
-    (* merge with previous tactic *)
-    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
-
-    (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "C" (rtac @{thm ext}),
-    
-    (* reflexivity of the basic relations *)
-    (* R \<dots> \<dots> *)
-    NDT ctxt "D" (resolve_tac rel_refl),
-
-    (* resolving with R x y assumptions *)
-    NDT ctxt "E" (atac),
-
-    (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
-    (* global simplification *)
-    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
-*}
 
 ML {*
 fun inj_repabs_tac ctxt quot_thms rel_refl trans2 =