
diff -r 5a9bdf81672d -r 3f3927f793d4 QuotMain.thy
--- a/QuotMain.thy	Fri Nov 27 07:16:16 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 08:15:23 2009 +0100
@@ -293,8 +293,7 @@
     val rty = Logic.unvarifyT (#rtyp quotdata)
     val rel = #rel quotdata
     val rel_eqv = #equiv_thm quotdata
-    val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]
-    val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]
+    val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv]
   in
     (rty, rel, rel_refl, rel_eqv)
   end
@@ -494,7 +493,7 @@
   (ObjectLogic.full_atomize_tac) THEN'
   REPEAT_ALL_NEW (FIRST'
    [(K (print_tac "start")) THEN' (K no_tac),
-    DT ctxt "1" (rtac rel_refl),
+    DT ctxt "1" (FIRST' (map rtac rel_refl)),
     DT ctxt "2" atac,
     DT ctxt "3" (rtac @{thm universal_twice}),
     DT ctxt "4" (rtac @{thm impI} THEN' atac),
@@ -503,7 +502,7 @@
       [(@{thm equiv_res_forall} OF [rel_eqv]),
        (@{thm equiv_res_exists} OF [rel_eqv])]),
     (* For a = b \<longrightarrow> a \<approx> b *)
-    DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+    DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (FIRST' (map rtac rel_refl))),
     DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
   ]);
 *}
@@ -590,7 +589,7 @@
     (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
     rtac @{thm move_forall},
     rtac @{thm move_exists},
-    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl)
+    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' FIRST' (map rtac rel_refl))
   ])
   end
 *}
@@ -720,12 +719,13 @@
 
 
 ML {*
-fun quotient_tac quot_thm =
+fun quotient_tac quot_thms =
   REPEAT_ALL_NEW (FIRST' [
     rtac @{thm FUN_QUOTIENT},
-    rtac quot_thm,
+    FIRST' (map rtac quot_thms),
     rtac @{thm IDENTITY_QUOTIENT},
     (* For functional identity quotients, (op = ---> op =) *)
+    (* TODO: think about the other way around, if we need to shorten the relation *)
     CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))
   ])
 *}
@@ -803,7 +803,7 @@
 *}
 
 ML {*
-fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans_thm rsp_thms =
   (FIRST' [
     rtac trans_thm,
     LAMBDA_RES_TAC ctxt,
@@ -814,12 +814,12 @@
     FIRST' (map rtac rsp_thms),
     rtac refl,
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' 
-         (RANGE [SOLVES' (quotient_tac quot_thm)])),
+         (RANGE [SOLVES' (quotient_tac quot_thms)])),
     (APPLY_RSP_TAC rty ctxt THEN' 
-         (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
+         (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
     Cong_Tac.cong_tac @{thm cong},
     rtac @{thm ext},
-    rtac reflex_thm,
+    FIRST' (map rtac rel_refl),
     atac,
     SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
     WEAK_LAMBDA_RES_TAC ctxt,
@@ -851,7 +851,7 @@
 *)
 
 ML {*
-fun r_mk_comb_tac' ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+fun r_mk_comb_tac' ctxt rty quot_thms reflex_thm trans_thm rsp_thms =
   REPEAT_ALL_NEW (FIRST' [
     (K (print_tac "start")) THEN' (K no_tac), 
     DT ctxt "1" (rtac trans_thm),
@@ -863,9 +863,9 @@
     DT ctxt "7" (FIRST' (map rtac rsp_thms)),
     DT ctxt "8" (rtac refl),
     DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
-                  THEN' (RANGE [SOLVES' (quotient_tac quot_thm)]))),
+                  THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
     DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
-                (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)]))),
+                (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
     DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
     DT ctxt "C" (rtac @{thm ext}),
     DT ctxt "D" (rtac reflex_thm),
@@ -898,7 +898,7 @@
     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 id_simps});
+    val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep);
     val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
     val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;
   in
@@ -950,7 +950,7 @@
 *}
 
 ML {*
-fun lambda_prs_conv1 ctxt quot ctrm =
+fun lambda_prs_conv1 ctxt quot_thms 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);
@@ -962,7 +962,7 @@
     val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
     val tac =
       (compose_tac (false, lpi, 2)) THEN_ALL_NEW
-      (quotient_tac quot);
+      (quotient_tac 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]
@@ -1003,16 +1003,18 @@
 *}
 
 ML {*
-fun clean_tac lthy quot defs reps_same absrep aps =
+fun clean_tac lthy quot defs aps =
   let
     val lower = flat (map (add_lower_defs lthy) defs)
+    val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
+    val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
     val aps_thms = map (applic_prs lthy absrep) aps
   in
-    EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), 
+    EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
             lambda_prs_tac lthy quot,
             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])]
+            simp_tac (HOL_ss addsimps reps_same)]
   end
 *}
 
@@ -1114,7 +1116,7 @@
 
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs =
+fun lift_tac lthy rthm rel_eqv rty quot trans2 rsp_thms defs =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac lthy
   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
@@ -1122,13 +1124,14 @@
       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)
+      val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
     in
       EVERY1 
        [rtac rule, 
         RANGE [rtac rthm',
-               regularize_tac lthy [rel_eqv] rel_refl,
+               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]] 
+               clean_tac lthy quot defs aps]] 
     end) lthy
 *}
 




