--- a/QuotMain.thy	Thu Dec 03 02:53:54 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 11:28:19 2009 +0100
@@ -938,7 +938,7 @@
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-    DT ctxt "1" (resolve_tac trans2),
+    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),
@@ -1063,13 +1063,6 @@
   (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot)
 *}
 
-(* Rewrites the term with LAMBDA_PRS thm.
-
-Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
-    with: f
-
-It proves the QUOTIENT assumptions by calling quotient_tac
- *)
 ML {*
 fun make_inst lhs t =
   let
@@ -1085,9 +1078,24 @@
   in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}
 
+(* It proves the QUOTIENT assumptions by calling quotient_tac *)
 ML {*
-fun lambda_prs_simple_conv quot_thms ctxt ctrm =
-  case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
+fun solve_quotient_assum i quot_thms ctxt thm =
+  let
+    val tac =
+      (compose_tac (false, thm, i)) THEN_ALL_NEW
+      (quotient_tac ctxt quot_thms);
+    val gc = Drule.strip_imp_concl (cprop_of thm);
+  in
+    Goal.prove_internal [] gc (fn _ => tac 1)
+  end
+  handle _ => error "solve_quotient_assum"
+*}
+
+ML {*
+fun lambda_allex_prs_simple_conv quot_thms ctxt ctrm =
+  case (term_of ctrm) of
+    ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
   let
     val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
     val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
@@ -1096,17 +1104,37 @@
     val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
     val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
     val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
-    val tac =
-      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
-      (quotient_tac ctxt quot_thms);
-    val gc = Drule.strip_imp_concl (cprop_of lpi);
-    val t = Goal.prove_internal [] gc (fn _ => tac 1)
-    val te = @{thm eq_reflection} OF [t]
+    val te = @{thm eq_reflection} OF [solve_quotient_assum 2 quot_thms ctxt lpi]
     val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
     val tl = Thm.lhs_of ts;
     val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
     val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
-(*    val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+  in
+    Conv.rewr_conv ti ctrm
+  end
+  | (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $
+    (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
+  let
+    val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf);
+    val thy = ProofContext.theory_of ctxt;
+    val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
+    val tyinst = [SOME cty_a, SOME cty_b];
+    val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
+    val thm = Drule.instantiate' tyinst tinst @{thm all_prs};
+    val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
+  in
+    Conv.rewr_conv ti ctrm
+  end
+  | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $
+    (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
+  let
+    val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf);
+    val thy = ProofContext.theory_of ctxt;
+    val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
+    val tyinst = [SOME cty_a, SOME cty_b];
+    val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
+    val thm = Drule.instantiate' tyinst tinst @{thm ex_prs};
+    val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
   in
     Conv.rewr_conv ti ctrm
   end
@@ -1116,12 +1144,12 @@
 (* quot stands for the QUOTIENT theorems: *)
 (* could be potentially all of them       *)
 ML {*
-fun lambda_prs_conv quot =
-  More_Conv.top_conv (lambda_prs_simple_conv quot) 
+fun lambda_allex_prs_conv quot =
+  More_Conv.top_conv (lambda_allex_prs_simple_conv quot) 
 *}
 
 ML {*
-fun lambda_prs_tac quot ctxt = CONVERSION (lambda_prs_conv quot ctxt)
+fun lambda_allex_prs_tac quot ctxt = CONVERSION (lambda_allex_prs_conv quot ctxt)
 *}
 
 (*
@@ -1150,9 +1178,6 @@
  The rest are a simp_tac and are fast.
 *)
 
-thm all_prs ex_prs
-
-
 ML {*
 fun clean_tac lthy quot defs =
   let
@@ -1164,20 +1189,17 @@
       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
   in
     EVERY' [
-      
       (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f *)
-      DT lthy "a" (TRY o lambda_prs_tac quot lthy),
+      (* \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f *)
+      NDT lthy "a" (TRY o lambda_allex_prs_tac quot lthy),
 
-      (* \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f *)
-      DT lthy "b" (TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot)),
-    
       (* NewConst  ---->  (rep ---> abs) oldConst *)
       (* Abs (Rep x)  ---->  x                    *)
       (* id_simps; fun_map.simps                  *)
-      DT lthy "c" (TRY o simp_tac simp_ctxt),
+      NDT lthy "c" (TRY o simp_tac simp_ctxt),
 
       (* final step *)
-      DT lthy "d" (TRY o rtac refl)
+      NDT lthy "d" (TRY o rtac refl)
     ]
   end
 *}