--- a/QuotMain.thy	Thu Dec 03 14:02:05 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 15:03:31 2009 +0100
@@ -155,6 +155,9 @@
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, FUN_REL)]]
 
+lemmas [quotient_thm] = 
+  FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT
+
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
 ML {* maps_lookup @{theory} "fun" *}
@@ -730,12 +733,9 @@
 *}
 
 ML {*
-fun quotient_tac ctxt quot_thms =
+fun quotient_tac ctxt =
   REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm FUN_QUOTIENT},
-     resolve_tac quot_thms,
-     rtac @{thm IDENTITY_QUOTIENT},
-     rtac @{thm LIST_QUOTIENT},
+    [resolve_tac (quotient_rules_get ctxt),
      (* For functional identity quotients, (op = ---> op =) *)
      (* TODO: think about the other way around, if we need to shorten the relation *)
      CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
@@ -901,7 +901,7 @@
 
 
 ML {*
-fun inj_repabs_tac ctxt quot_thms rel_refl trans2 =
+fun inj_repabs_tac ctxt rel_refl trans2 =
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
@@ -933,11 +933,11 @@
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *) 
     NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
-                  THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
+                  THEN' (RANGE [SOLVES' (quotient_tac ctxt)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
     NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
-                (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+                (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
                         quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
 
     (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
@@ -961,8 +961,8 @@
 *}
 
 ML {*
-fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2)
+fun all_inj_repabs_tac ctxt rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 *}
 
 section {* Cleaning of the theorem *}
@@ -970,8 +970,8 @@
 
 (* TODO: This is slow *)
 ML {*
-fun allex_prs_tac ctxt quot =
-  (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot)
+fun allex_prs_tac ctxt =
+  (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt)
 *}
 
 ML {*
@@ -991,11 +991,11 @@
 
 (* It proves the QUOTIENT assumptions by calling quotient_tac *)
 ML {*
-fun solve_quotient_assum i quot_thms ctxt thm =
+fun solve_quotient_assum i ctxt thm =
   let
     val tac =
       (compose_tac (false, thm, i)) THEN_ALL_NEW
-      (quotient_tac ctxt quot_thms);
+      (quotient_tac ctxt);
     val gc = Drule.strip_imp_concl (cprop_of thm);
   in
     Goal.prove_internal [] gc (fn _ => tac 1)
@@ -1004,7 +1004,7 @@
 *}
 
 ML {*
-fun lambda_allex_prs_simple_conv quot_thms ctxt ctrm =
+fun lambda_allex_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
   let
@@ -1015,7 +1015,7 @@
     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 te = @{thm eq_reflection} OF [solve_quotient_assum 2 quot_thms ctxt lpi]
+    val te = @{thm eq_reflection} OF [solve_quotient_assum 2 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);
@@ -1032,7 +1032,7 @@
     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];
+    val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm];
   in
     Conv.rewr_conv ti ctrm
   end
@@ -1045,7 +1045,7 @@
     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];
+    val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm];
   in
     Conv.rewr_conv ti ctrm
   end
@@ -1055,12 +1055,12 @@
 (* quot stands for the QUOTIENT theorems: *)
 (* could be potentially all of them       *)
 ML {*
-fun lambda_allex_prs_conv quot =
-  More_Conv.top_conv (lambda_allex_prs_simple_conv quot) 
+val lambda_allex_prs_conv =
+  More_Conv.top_conv lambda_allex_prs_simple_conv 
 *}
 
 ML {*
-fun lambda_allex_prs_tac quot ctxt = CONVERSION (lambda_allex_prs_conv quot ctxt)
+fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
 *}
 
 (*
@@ -1090,13 +1090,14 @@
 *)
 
 ML {*
-fun clean_tac lthy quot =
+fun clean_tac lthy =
   let
     val thy = ProofContext.theory_of lthy;
+    val quotients = quotient_rules_get lthy
     val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
-    val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
+    val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients
     val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
-    val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
+    val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients
     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
@@ -1104,7 +1105,7 @@
     EVERY' [
       (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f *)
       (* \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f *)
-      NDT lthy "a" (TRY o lambda_allex_prs_tac quot lthy),
+      NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
 
       (* NewConst  ---->  (rep ---> abs) oldConst *)
       (* Abs (Rep x)  ---->  x                    *)
@@ -1217,7 +1218,7 @@
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
 
-fun lift_tac lthy rthm rel_eqv quot =
+fun lift_tac lthy rthm rel_eqv =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac lthy
   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
@@ -1232,8 +1233,8 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2,
-               clean_tac lthy quot]]
+               rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2,
+               clean_tac lthy]]
     end) lthy
 *}