--- a/Quot/QuotMain.thy	Tue Dec 08 01:00:21 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 01:25:43 2009 +0100
@@ -147,8 +147,6 @@
 (* Throws now an exception:              *)
 (* declare [[map "option" = (bla, blu)]] *)
 
-
-(* identity quotient is not here as it has to be applied first *)
 lemmas [quotient_thm] =
   fun_quotient prod_quotient
 
@@ -160,19 +158,17 @@
 lemmas [quotient_equiv] =
   identity_equivp prod_equivp
 
-
 (* definition of the quotient types *)
 (* FIXME: should be called quotient_typ.ML *)
 use "quotient.ML"
 
-
 (* lifting of constants *)
 use "quotient_def.ML"
 
 section {* Simset setup *}
 
-(* since HOL_basic_ss is too "big", we need to set up *)
-(* our own minimal simpset                            *)
+(* Since HOL_basic_ss is too "big" for us, *)
+(* we set up our own minimal simpset.      *)
 ML {*
 fun  mk_minimal_ss ctxt =
   Simplifier.context ctxt empty_ss
@@ -181,13 +177,10 @@
 *}
 
 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 *}
+section {* Atomize Infrastructure *}
 
 lemma atomize_eqv[atomize]:
   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
@@ -219,24 +212,20 @@
 end
 *}
 
-section {* infrastructure about id *}
+section {* Infrastructure about id *}
+
+print_attributes
 
 (* TODO: think where should this be *)
 lemma prod_fun_id: "prod_fun id id \<equiv> id"
   by (rule eq_reflection) (simp add: prod_fun_def)
 
-(* FIXME: make it a list and add map_id to it *)
-lemmas id_simps =
+lemmas [id_simps] = 
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
   prod_fun_id
 
-ML {*
-fun simp_ids thm =
-  MetaSimplifier.rewrite_rule @{thms id_simps} thm
-*}
-
 section {* Debugging infrastructure for testing tactics *}
 
 ML {*
@@ -1008,7 +997,7 @@
        val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
        val ti =
          (let
-           val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+           val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
            val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
          in
            Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
@@ -1017,7 +1006,7 @@
            val (insp, inst) = make_inst2 (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 @{thms id_simps} td
+           MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
          end);
        val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then
                   (tracing "lambda_prs";
@@ -1045,8 +1034,8 @@
 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
 (*    and simplification with                                     *)
 thm all_prs ex_prs 
-(* 3. simplification with *)
-thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep
+(* 3. simplification with id_simps and *)
+thm fun_map.simps Quotient_abs_rep Quotient_rel_rep
 (* 4. Test for refl *)
 
 ML {*
@@ -1056,8 +1045,8 @@
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
       (* FIXME: shouldn't the definitions already be varified? *)
     val thms1 = @{thms all_prs ex_prs} @ defs
-    val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
-                @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
+    val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy)
+                @ @{thms Quotient_abs_rep Quotient_rel_rep} 
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [lambda_prs_tac lthy,

--- a/Quot/quotient_info.ML	Tue Dec 08 01:00:21 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 08 01:25:43 2009 +0100
@@ -26,6 +26,7 @@
   val equiv_rules_get: Proof.context -> thm list
   val equiv_rules_add: attribute
   val rsp_rules_get: Proof.context -> thm list  
+  val id_simps_get: Proof.context -> thm list
   val quotient_rules_get: Proof.context -> thm list
   val quotient_rules_add: attribute
 end;
@@ -174,6 +175,9 @@
   OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
+(* FIXME/TODO: check the various lemmas conform *)
+(* with the required shape                      *)
+
 (* equivalence relation theorems *)
 structure EquivRules = Named_Thms
   (val name = "quotient_equiv"
@@ -189,6 +193,13 @@
 
 val rsp_rules_get = RspRules.get
 
+(* respectfulness theorems *)
+structure IdSimps = Named_Thms
+  (val name = "id_simps"
+   val description = "Identity simp rules for maps.")
+
+val id_simps_get = IdSimps.get
+
 (* quotient theorems *)
 structure QuotientRules = Named_Thms
   (val name = "quotient_thm"
@@ -201,6 +212,7 @@
 val _ = Context.>> (Context.map_theory 
     (EquivRules.setup #>
      RspRules.setup #>
+     IdSimps.setup #>
      QuotientRules.setup))
 
 end; (* structure *)