--- a/Quot/QuotMain.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 21:53:50 2009 +0100
@@ -186,6 +186,8 @@
 ML {*
 (* TODO/FIXME not needed anymore? *)
 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+
+fun OF1 thm1 thm2 = thm2 RS thm1
 *}
 
 section {* atomize *}
@@ -292,36 +294,6 @@
    | _ => false
 *}
 
-section {* Infrastructure for collecting theorems for starting the lifting *}
-
-ML {*
-fun lookup_quot_data lthy qty =
-  let
-    val qty_name = fst (dest_Type qty)
-    val SOME quotdata = quotdata_lookup lthy qty_name
-    (* TODO: Should no longer be needed *)
-    val rty = Logic.unvarifyT (#rtyp quotdata)
-    val rel = #rel quotdata
-    val rel_eqv = #equiv_thm quotdata
-    val rel_refl = @{thm equivp_reflp} OF [rel_eqv]
-  in
-    (rty, rel, rel_refl, rel_eqv)
-  end
-*}
-
-ML {*
-fun lookup_quot_thms lthy qty_name =
-  let
-    val thy = ProofContext.theory_of lthy;
-    val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
-    val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
-    val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
-    val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)
-  in
-    (trans2, reps_same, absrep, quot)
-  end
-*}
-
 section {* Regularization *} 
 
 (*
@@ -703,10 +675,12 @@
 
 ML {*
 fun solve_quotient_assums ctxt thm =
-  let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
-  thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
-  end
-  handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
+let 
+  val goal = hd (Drule.strip_imp_prems (cprop_of thm)) 
+in
+  thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]
+end
+handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
 *}
 
 (* Not used *)
@@ -914,9 +888,9 @@
 
     (* reflexivity of operators arising from Cong_tac *)
 | Const (@{const_name "op ="},_) $ _ $ _ 
-      => rtac @{thm refl} ORELSE'
+      => 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)])
+            quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*)
 
 (* TODO: These patterns should should be somehow combined and generalized... *)
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
@@ -943,29 +917,49 @@
 *}
 
 ML {*
-fun inj_repabs_tac ctxt rel_refl trans2 =
+fun inj_repabs_step_tac ctxt rel_refl trans2 =
   (FIRST' [
-    inj_repabs_tac_match ctxt trans2,
+    NDT ctxt "0" (inj_repabs_tac_match ctxt trans2),
     (* 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)])),
+                 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 *)
-    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
+    NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN'
                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    
     (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    NDT ctxt "D" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    
     (* resolving with R x y assumptions *)
     NDT ctxt "E" (atac),
+    
     (* reflexivity of the basic relations *)
     (* R \<dots> \<dots> *)
-    NDT ctxt "D" (resolve_tac rel_refl)
+    NDT ctxt "F" (resolve_tac rel_refl)
     ])
 *}
 
 ML {*
-fun all_inj_repabs_tac ctxt rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
+fun inj_repabs_tac ctxt =
+let
+  val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt)
+  val trans2 = map (fn x => @{thm equals_rsp} OF [x]) (quotient_rules_get ctxt)
+in
+  inj_repabs_step_tac ctxt rel_refl trans2
+end
+*}
+
+ML {*
+fun all_inj_repabs_tac ctxt =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt)
+(* if this is too slow we can inline the code above *)
 *}
 
 section {* Cleaning of the theorem *}
@@ -1190,24 +1184,19 @@
 *}
 
 ML {*
-(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-
 fun lift_tac ctxt rthm =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac ctxt
-  THEN' CSUBGOAL (fn (gl, i) =>
+  THEN' CSUBGOAL (fn (goal, i) =>
     let
       val rthm' = atomize_thm rthm
-      val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
-      val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt)
-      val quotients = quotient_rules_get ctxt
-      val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
-      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
+      val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
+      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb goal))] @{thm QUOT_TRUE_i}
     in
       (rtac rule THEN'
        RANGE [rtac rthm',
               regularize_tac ctxt,
-              rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2,
+              rtac thm THEN' all_inj_repabs_tac ctxt,
               clean_tac ctxt]) i
     end)
 *}