--- a/QuotMain.thy	Wed Nov 25 15:43:12 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 21:48:32 2009 +0100
@@ -797,7 +797,9 @@
   (FIRST' [
     rtac trans_thm,
     LAMBDA_RES_TAC ctxt,
+    rtac @{thm RES_FORALL_RSP},
     ball_rsp_tac ctxt,
+    rtac @{thm RES_EXISTS_RSP},
     bex_rsp_tac ctxt,
     FIRST' (map rtac rsp_thms),
     rtac refl,
@@ -908,7 +910,7 @@
 *}
 
 ML {*
-fun applic_prs lthy rty qty absrep ty =
+fun applic_prs_old lthy rty qty absrep ty =
   let
     val rty = Logic.varifyT rty;
     val qty = Logic.varifyT qty;
@@ -941,6 +943,30 @@
   end
 *}
 
+ML {*
+fun applic_prs lthy absrep (rty, qty) =
+  let
+    fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
+    fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
+    val (raty, rgty) = Term.strip_type rty;
+    val (qaty, qgty) = Term.strip_type qty;
+    val vs = map (fn _ => "x") qaty;
+    val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+    val f = Free (fname, qaty ---> qgty);
+    val args = map Free (vfs ~~ qaty);
+    val rhs = list_comb(f, args);
+    val largs = map2 mk_rep (raty ~~ qaty) args;
+    val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
+    val llhs = Syntax.check_term lthy lhs;
+    val eq = Logic.mk_equals (llhs, rhs);
+    val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+    val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply});
+    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+    val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t;
+  in
+    singleton (ProofContext.export lthy' lthy) t_id
+  end
+*}
 
 ML {*
 fun findaps_all rty tm =
@@ -956,6 +982,23 @@
 
 
 ML {*
+fun find_aps_all rtm qtm =
+  case (rtm, qtm) of
+    (Abs(_, T1, s1), Abs(_, T2, s2)) =>
+      find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
+  | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
+      let
+        val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+      in
+        if T1 = T2 then sub else (T1, T2) :: sub
+      end
+  | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+  | _ => [];
+
+fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
+*}
+
+ML {*
 (* FIXME: allex_prs and lambda_prs can be one function *)
 fun allex_prs_tac lthy quot =
   (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
@@ -1048,13 +1091,14 @@
 *}
 
 ML {*
-fun clean_tac lthy quot defs reps_same =
+fun clean_tac lthy quot defs reps_same absrep aps =
   let
     val lower = flat (map (add_lower_defs lthy) defs)
+    val aps_thms = map (applic_prs lthy absrep) aps
   in
     EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), 
             lambda_prs_tac lthy quot,
-            (* TODO: cleaning according to app_prs *)
+            TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
             TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
             simp_tac (HOL_ss addsimps [reps_same])]
   end
@@ -1145,30 +1189,40 @@
   @{thm procedure}
 end
 *}
-  
+
+(* Left for debugging *)
 ML {*
-fun procedure_tac rthm ctxt =
-  ObjectLogic.full_atomize_tac 
-  THEN' gen_frees_tac ctxt
+fun procedure_tac lthy rthm =
+  ObjectLogic.full_atomize_tac
+  THEN' gen_frees_tac lthy
   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
-          let
-            val rthm' = atomize_thm rthm
-            val rule = procedure_inst context (prop_of rthm') (Envir.beta_norm (term_of concl))
-          in
-           EVERY1 [rtac rule, rtac rthm']
-        end) ctxt
+    let
+      val rthm' = atomize_thm rthm
+      val rule = procedure_inst context (prop_of rthm') (term_of concl)
+    in
+      rtac rule THEN' rtac rthm'
+    end 1) lthy
 *}
 
 ML {*
-fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs =
-  procedure_tac thm lthy THEN'
-  RANGE [regularize_tac lthy rel_eqv rel_refl,
-         REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), 
-         clean_tac lthy quot defs reps_same]
+fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs =
+  ObjectLogic.full_atomize_tac
+  THEN' gen_frees_tac lthy
+  THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
+    let
+      val rthm' = atomize_thm rthm
+      val rule = procedure_inst context (prop_of rthm') (term_of concl)
+      val aps = find_aps (prop_of rthm') (term_of concl)
+    in
+      rtac rule THEN' RANGE [
+        rtac rthm',
+        regularize_tac lthy rel_eqv rel_refl,
+        REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
+        clean_tac lthy quot defs reps_same absrep aps
+      ]
+    end 1) lthy
 *}
 
-
-
 end