diff -r d23416464f62 -r 2e51e1315839 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 16:35:40 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 16:36:01 2009 +0100
@@ -810,6 +810,18 @@
 *}
 
 ML {*
+fun equals_rsp_tac R ctxt =
+  let
+    val t = domain_type (fastype_of R);
+    val thy = ProofContext.theory_of ctxt
+    val thm = Drule.instantiate' [SOME (ctyp_of thy t)] [SOME (cterm_of thy R)] @{thm equals_rsp}
+  in
+    rtac thm THEN' RANGE [quotient_tac ctxt]
+  end
+  handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac
+*}
+
+ML {*
 fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>
     case (bare_concl goal) of 
@@ -829,7 +841,7 @@
 *}
 
 ML {*
-fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
+fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
 (case (bare_concl goal) of
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
   ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
@@ -864,11 +876,12 @@
     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
 
+| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE'
+    (equals_rsp_tac R ctxt THEN' RANGE [
+       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
+
     (* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name "op ="},_) $ _ $ _ 
-      => rtac @{thm refl} (*ORELSE'
-          (resolve_tac trans2 THEN' RANGE [
-            quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*)
+| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
 
    (* respectfulness of constants; in particular of a simple relation *)
 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
@@ -884,17 +897,13 @@
 *}
 
 ML {*
-fun inj_repabs_step_tac ctxt rel_refl trans2 =
+fun inj_repabs_step_tac ctxt rel_refl =
   (FIRST' [
-    NDT ctxt "0" (inj_repabs_tac_match ctxt trans2),
+    NDT ctxt "0" (inj_repabs_tac_match ctxt),
     (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp   provided type of t needs lifting *)
     
     NDT ctxt "A" (apply_rsp_tac ctxt THEN'
                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]),
-    
-    (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *)
-    NDT ctxt "B" (resolve_tac trans2 THEN' 
-                 RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
 
     (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
     (* merge with previous tactic *)
@@ -917,9 +926,8 @@
 fun inj_repabs_tac ctxt =
 let
   val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
-  val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt)
 in
-  inj_repabs_step_tac ctxt rel_refl trans2
+  inj_repabs_step_tac ctxt rel_refl
 end
 
 fun all_inj_repabs_tac ctxt =
@@ -928,6 +936,10 @@
 
 section {* Cleaning of the Theorem *}
 
+(* Since the patterns for the lhs are different; there are 3 different make-insts *)
+(* 1: does  ? \<rightarrow> id *)
+(* 2: does id \<rightarrow> ? *)
+(* 3: does  ? \<rightarrow> ? *)
 ML {*
 fun make_inst lhs t =
   let
@@ -943,12 +955,25 @@
   in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}
 
-(* Since the patterns for the lhs are different; there are 2 different make-insts *)
 ML {*
 fun make_inst2 lhs t =
   let
     val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
-    val _ = tracing "a";
+    val _ $ (Abs (_, _, (_ $ g))) = t;
+    fun mk_abs i t =
+      if incr_boundvars i u aconv t then Bound i
+      else (case t of
+        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
+      | Bound j => if i = j then error "make_inst" else t
+      | _ => t);
+  in (f, Abs ("x", T, mk_abs 0 g)) end;
+*}
+
+ML {*
+fun make_inst3 lhs t =
+  let
+    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
     val _ $ (Abs (_, _, (_ $ g))) = t;
     fun mk_abs i t =
       if incr_boundvars i u aconv t then Bound i
@@ -972,7 +997,6 @@
        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 te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
-       val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
        val ti =
          (let
            val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
@@ -981,7 +1005,15 @@
            Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
          end handle _ => (* TODO handle only Bind | Error "make_inst" *)
          let
-           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
+           val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+           val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+           val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm)
+         in
+           Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+         end handle _ => (* TODO handle only Bind | Error "make_inst" *)
+         let
+           val (insp, inst) = make_inst3 (term_of (Thm.lhs_of te)) (term_of ctrm)
            val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
          in
            MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
@@ -993,6 +1025,7 @@
                    tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
                    tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
                else ()
+
      in
        Conv.rewr_conv ti ctrm
      end