--- a/FSet.thy	Fri Nov 27 07:16:16 2009 +0100
+++ b/FSet.thy	Fri Nov 27 08:15:23 2009 +0100
@@ -304,7 +304,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 ML {* val consts = lookup_quot_consts defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs *}
 
 lemma "IN x EMPTY = False"
 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
@@ -345,10 +345,10 @@
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
 prefer 2
-apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
-apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*})
+apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
+apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 rsp_thms 1*})
 done
 
 quotient_def
@@ -376,7 +376,7 @@
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs *}
 
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
@@ -397,7 +397,7 @@
   done
 
 
-ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
+ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] trans2 rsp_thms *}
 
 
 
@@ -405,7 +405,7 @@
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
-apply (tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *})
+apply (tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
 apply (rule FUN_QUOTIENT)
@@ -454,25 +454,25 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply assumption
 apply (rule refl)
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
+apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
 done
 
 end

--- a/IntEx.thy	Fri Nov 27 07:16:16 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 08:15:23 2009 +0100
@@ -142,7 +142,7 @@
 
 ML {*
 fun lift_tac_fset lthy t =
-  lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs
+  lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs
 *}
 
 lemma "PLUS a b = PLUS b a"
@@ -167,9 +167,12 @@
 lemma map_prs: "map REP_my_int (map ABS_my_int x) = x"
 sorry
 
+lemma foldl_prs: "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl"
+sorry
+
 lemma "foldl PLUS x [] = x"
 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
-apply (simp_all only: map_prs)
+apply (simp_all only: map_prs foldl_prs)
 sorry
 
 (*
@@ -187,8 +190,8 @@
 
 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] trans2 rsp_thms) 1 *})
 oops
 
 

--- a/LFex.thy	Fri Nov 27 07:16:16 2009 +0100
+++ b/LFex.thy	Fri Nov 27 08:15:23 2009 +0100
@@ -180,12 +180,6 @@
 where
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
-ML {* val defs =
-  @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
-    FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
-*}
-ML {* val consts = lookup_quot_consts defs *}
-
 thm akind_aty_atrm.induct
 
 lemma left_ball_regular:
@@ -279,6 +273,10 @@
   end
 *}
 
+ML {* val defs =
+  @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
+    FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
+*}
 
 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K');
  \<And>A A' K x x' K'.
@@ -301,8 +299,15 @@
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 prefer 2
-apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply (tactic {* clean_tac @{context} quot defs reps_same absrep 1 *})
+thm QUOTIENT_TY
+apply (tactic {* clean_tac @{context} @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} defs [] 1 *})
+
+
+print_quotients
+apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*})
+
+
+ML {* val consts = lookup_quot_consts defs *}
 
 ML {*
 val rty_qty_rel =

--- a/LamEx.thy	Fri Nov 27 07:16:16 2009 +0100
+++ b/LamEx.thy	Fri Nov 27 08:15:23 2009 +0100
@@ -179,7 +179,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty [quot] trans2 rsp_thms reps_same absrep defs *}
 
 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})

--- 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
 *}
 

--- a/QuotScript.thy	Fri Nov 27 07:16:16 2009 +0100
+++ b/QuotScript.thy	Fri Nov 27 08:15:23 2009 +0100
@@ -20,8 +20,8 @@
 by (blast)
 
 lemma EQUIV_REFL:
-  shows "EQUIV E ==> REFL E"
-  by (simp add: EQUIV_REFL_SYM_TRANS)
+  shows "EQUIV E \<Longrightarrow> (\<And>x. E x x)"
+  by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
 
 definition
   "PART_EQUIV E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"