diff -r fe2529a9f250 -r 670131bcba4a Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 14 14:24:08 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 15 15:38:17 2009 +0100
@@ -122,6 +122,22 @@
 fun OF1 thm1 thm2 = thm2 RS thm1
 *}
 
+(* various tactic combinators *)
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
+*}
+
+ML {*
+(* prints warning, if goal is unsolved *)
+fun WARN (tac, msg) i st =
+ case Seq.pull ((SOLVES' tac) i st) of
+     NONE    => (warning msg; Seq.single st)
+   | seqcell => Seq.make (fn () => seqcell)
+
+fun RANGE_WARN xs = RANGE (map WARN xs)
+*}
+
+
 section {* Atomize Infrastructure *}
 
 lemma atomize_eqv[atomize]:
@@ -410,10 +426,11 @@
 by (simp add: equivp_reflp)
 
 ML {*
-fun quotient_tac ctxt =
-  REPEAT_ALL_NEW (DETERM o FIRST'
+(* test whether DETERM makes any difference *)
+fun quotient_tac ctxt = SOLVES'  
+  (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
-     resolve_tac (quotient_rules_get ctxt)])
+     resolve_tac (quotient_rules_get ctxt)]))
 
 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
@@ -431,7 +448,7 @@
 
 
 (* 0. preliminary simplification step according to *)
-thm ball_reg_eqv bex_reg_eqv (* babs_reg_eqv is of no use *)
+thm ball_reg_eqv bex_reg_eqv babs_reg_eqv
     ball_reg_eqv_range bex_reg_eqv_range
 (* 1. eliminating simple Ball/Bex instances*)
 thm ball_reg_right bex_reg_left
@@ -453,8 +470,6 @@
   val simpset = (mk_minimal_ss ctxt) 
                        addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
                        addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver
-  (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
-  (* can this cause loops in equiv_tac ? *)
   val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
 in
   simp_tac simpset THEN'
@@ -557,6 +572,8 @@
   "QUOT_TRUE x \<equiv> True"
 
 ML {*
+(* looks for QUOT_TRUE assumtions, and in case its argument    *)
+(* is an application, it returns the function and the argument *)
 fun find_qt_asm asms =
 let
   fun find_fun trm =
@@ -659,9 +676,9 @@
 *}
 
 ML {*
-(* FIXME / TODO: what is asmf and asma in the code below *)
-(* asmf is the QUOT_TRUE assumption function
-   asma are    QUOT_TRUE assumption arguments *)
+(* we apply apply_rsp only in case if the type needs lifting,      *)
+(* which is the case if the type of the data in the QUOT_TRUE      *)
+(* assumption is different from the corresponding type in the goal *)
 val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
   let
@@ -669,13 +686,13 @@
     val qt_asm = find_qt_asm (map term_of asms)
   in
     case (bare_concl, qt_asm) of
-      (R2 $ (f $ x) $ (g $ y), SOME (asmf, asma)) =>
-         if (fastype_of asmf) = (fastype_of f) 
-         then no_tac 
-         else 
+      (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
+         if (fastype_of qt_fun) = (fastype_of f) 
+         then no_tac                             
+         else                                    
            let
              val ty_x = fastype_of x
-             val ty_b = fastype_of asma
+             val ty_b = fastype_of qt_arg
              val ty_f = range_type (fastype_of f) 
              val thy = ProofContext.theory_of context
              val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
@@ -688,6 +705,8 @@
   end)
 *}
 
+thm equals_rsp
+
 ML {*
 fun equals_rsp_tac R ctxt =
 let
@@ -698,16 +717,13 @@
 in
   rtac thm THEN' quotient_tac ctxt
 end
+(* raised by instantiate' *)
 handle THM _  => K no_tac  
      | TYPE _ => K no_tac    
      | TERM _ => K no_tac
 *}
 
-thm rep_abs_rsp
-
 ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
-
 fun rep_abs_rsp_tac ctxt = 
   SUBGOAL (fn (goal, i) =>
     case (bare_concl goal) of 
@@ -719,7 +735,7 @@
            val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
            val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
          in
-           (rtac inst_thm THEN' SOLVES' (quotient_tac ctxt)) i
+           (rtac inst_thm THEN' quotient_tac ctxt) i
          end
          handle THM _ => no_tac | TYPE _ => no_tac)
     | _ => no_tac)
@@ -906,7 +922,7 @@
            val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
          in
            MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
-         end);
+         end)
        val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then
                   (tracing "lambda_prs";
                    tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
@@ -1062,15 +1078,6 @@
 
 section {* Automatic Proofs *}
 
-ML {*
-(* prints warning, if goal is unsolved *)
-fun WARN (tac, msg) i st =
- case Seq.pull ((SOLVES' tac) i st) of
-     NONE    => (warning msg; Seq.single st)
-   | seqcell => Seq.make (fn () => seqcell)
-
-fun RANGE_WARN xs = RANGE (map WARN xs)
-*}
 
 ML {*
 local