
diff -r 14682786c356 -r 06e54c862a39 QuotMain.thy
--- a/QuotMain.thy	Sun Dec 06 06:39:32 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 06:41:52 2009 +0100
@@ -740,12 +740,17 @@
         then rtrm 
         else mk_repabs lthy (T, T') rtrm
 
-  | (Const (_, T), Const (_, T')) =>
-        if T = T'                    
+  | (_, Const (@{const_name "op ="}, _)) => rtrm
+
+    (* FIXME: check here that rtrm is the corresponding definition for teh const *)
+  | (_, Const (_, T')) =>
+      let
+        val rty = fastype_of rtrm
+      in 
+        if rty = T'                    
         then rtrm
-        else mk_repabs lthy (T, T') rtrm
-  
-  | (_, Const (@{const_name "op ="}, _)) => rtrm
+        else mk_repabs lthy (rty, T') rtrm
+      end   
   
   | _ => raise (LIFT_MATCH "injection")
 *}
@@ -773,6 +778,12 @@
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
+(* solver for the simplifier *)
+ML {*
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
+
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -1041,92 +1052,77 @@
 *}
 
 ML {*
-fun lambda_allex_prs_simple_conv ctxt ctrm =
+fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
-    ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
-    let
-      val (ty_b, ty_a) = dest_fun_type (fastype_of r1);
-      val (ty_c, ty_d) = dest_fun_type (fastype_of a2);
-      val thy = ProofContext.theory_of ctxt;
-      val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_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_assums ctxt (solve_quotient_assums 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);
-      val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
-    in
-      Conv.rewr_conv ti ctrm
-    end
+   ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+     let
+       val thy = ProofContext.theory_of ctxt
+       val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+       val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+       val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_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_assums ctxt (solve_quotient_assums 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)
+       val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+        (*val _ = tracing "lambda_prs"
+          val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)))
+          val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*)
+     in
+       Conv.rewr_conv ti ctrm
+     end
   | _ => Conv.all_conv ctrm
 *}
 
 ML {*
-val lambda_allex_prs_conv =
-  More_Conv.top_conv lambda_allex_prs_simple_conv
+val lambda_prs_conv =
+  More_Conv.top_conv lambda_prs_simple_conv
 
-fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
+fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 *}
 
 (*
- Cleaning the theorem consists of 6 kinds of rewrites.
+ Cleaning the theorem consists of three rewriting steps.
  The first two need to be done before fun_map is unfolded
 
- - lambda_prs:
+ 1) lambda_prs:
      (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f
 
- - all_prs (and the same for exists: ex_prs)
-     \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f
-
- - Rewriting with definitions from the argument defs
-     NewConst  ---->  (rep ---> abs) oldConst
+    Implemented as conversion since it is not a pattern.
 
- - Quotient_rel_rep:
-     Rel (Rep x) (Rep y)  ---->  x = y
+ 2) all_prs (the same for exists):
+     Ball (Respects R) ((abs ---> id) f)  ---->  All f
 
- - ABS_REP
-     Abs (Rep x)  ---->  x
+    Rewriting with definitions from the argument defs
+     (rep ---> abs) oldConst ----> newconst
 
- - id_simps; fun_map.simps
+ 3) Quotient_rel_rep:
+      Rel (Rep x) (Rep y)  ---->  x = y
 
- The first one is implemented as a conversion (fast).
- The second one is an EqSubst (slow).
- The rest are a simp_tac and are fast.
+    Quotient_abs_rep:
+      Abs (Rep x)  ---->  x
+
+    id_simps; fun_map.simps
 *)
 
 ML {*
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-*}
-
-ML {*
 fun clean_tac lthy =
   let
     val thy = ProofContext.theory_of lthy;
     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} 
-    fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver
-    (* FIXME: use of someting smaller than HOL_basic_ss *)
+    fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver
+      (* FIXME: use of someting smaller than HOL_basic_ss *)
   in
-    EVERY' [
-      (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x)))  ---->  f *)
-      NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
-
-      (* Ball (Respects R) ((abs ---> id) f)  ---->  All f *)
-      NDT lthy "b" (simp_tac (simp_ctxt thms1)),
-
-      (* NewConst  ----->  (rep ---> abs) oldConst *)
-      (* abs (rep x)  ----->  x                    *)
-      (* R (Rep x) (Rep y) -----> x = y            *)
-      (* id_simps; fun_map.simps                   *)
-      NDT lthy "c" (simp_tac (simp_ctxt thms2)),
-
-      (* final step *)
-      NDT lthy "d" (TRY o rtac refl)
-    ]
+    EVERY' [lambda_prs_tac lthy,
+            simp_tac (simps thms1),
+            simp_tac (simps thms2),
+            TRY o rtac refl]
   end
 *}
 




