# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260626879 -3600
# Node ID ac2ed047988d1b5504995623f7c7707875d7a0ca
# Parent  33cd648df179913428abb9216d8f79fd0a20034c
annotated some questions to the code; some simple changes

diff -r 33cd648df179 -r ac2ed047988d Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sat Dec 12 13:54:01 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sat Dec 12 15:07:59 2009 +0100
@@ -280,7 +280,7 @@
 sorry
 
 thm card_raw_cons_gt_0
-thm mem_card_raw_not_0
+(*thm mem_card_raw_not_0*)
 thm not_nil_equiv_cons
 thm delete_raw.simps
 (*thm mem_delete_raw*)
diff -r 33cd648df179 -r ac2ed047988d Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sat Dec 12 13:54:01 2009 +0100
+++ b/Quot/QuotMain.thy	Sat Dec 12 15:07:59 2009 +0100
@@ -399,7 +399,7 @@
 
 ML {*
 fun quotient_tac ctxt =
-  REPEAT_ALL_NEW (FIRST'
+  DETERM o REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
      resolve_tac (quotient_rules_get ctxt)])
 
@@ -407,6 +407,17 @@
 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
 *}
 
+ML {*
+fun solve_quotient_assums ctxt thm =
+let 
+  val goal = hd (Drule.strip_imp_prems (cprop_of thm)) 
+in
+  thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]
+end
+handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
+*}
+
+
 (* 0. preliminary simplification step according to *)
 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)
     ball_reg_eqv_range bex_reg_eqv_range
@@ -530,15 +541,7 @@
 
 section {* Injection Tactic *}
 
-ML {*
-fun solve_quotient_assums ctxt thm =
-let 
-  val goal = hd (Drule.strip_imp_prems (cprop_of thm)) 
-in
-  thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]
-end
-handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
-*}
+
 
 definition
   "QUOT_TRUE x \<equiv> True"
@@ -646,49 +649,57 @@
 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
 *}
 
+thm apply_rsp
+
 ML {*
 val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
     case ((HOLogic.dest_Trueprop (term_of concl))) of
-      ((R2 $ (f $ x) $ (g $ y))) =>
+      (R2 $ (f $ x) $ (g $ y)) =>
         (let
-          val (asmf, asma) = find_qt_asm (map term_of asms);
-        in
-          if (fastype_of asmf) = (fastype_of f) then no_tac else let
-            val ty_a = fastype_of x;
-            val ty_b = fastype_of asma;
-            val ty_c = range_type (type_of f);
-            val thy = ProofContext.theory_of context;
-            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
-            val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
-            val te = solve_quotient_assums context thm
-            val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
-            val thm = Drule.instantiate' [] t_inst te
-          in
-            compose_tac (false, thm, 2) 1
-          end
-        end
+           val (asmf, asma) = find_qt_asm (map term_of asms);
+         in
+           if (fastype_of asmf) = (fastype_of f) (* why is this test necessary *)
+           then no_tac 
+           else 
+             let
+               val ty_a = fastype_of x;
+               val ty_b = fastype_of asma;
+               val ty_c = range_type (type_of f); (* why type_of, not fast_type? *)
+               val thy = ProofContext.theory_of context;
+               val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
+               val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
+               val te = solve_quotient_assums context thm
+               val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; 
+                                                      (* why not instantiate terms 3 lines earlier *)
+               val thm = Drule.instantiate' [] t_inst te
+             in
+               compose_tac (false, thm, 2) 1
+             end
+         end
         handle ERROR "find_qt_asm: no pair" => no_tac)
     | _ => no_tac)
 *}
 
 ML {*
 fun equals_rsp_tac R ctxt =
-  let
-    val ty = domain_type (fastype_of R);
-    val thy = ProofContext.theory_of ctxt
-    val thm = Drule.instantiate' 
-                 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}
-  in
-    rtac thm THEN' quotient_tac ctxt
-  end
-  handle THM _  => K no_tac  
-       | TYPE _ => K no_tac    
-       | TERM _ => K no_tac
+let
+  val ty = domain_type (fastype_of R);
+  val thy = ProofContext.theory_of ctxt
+  val thm = Drule.instantiate' 
+               [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}
+in
+  rtac thm THEN' quotient_tac ctxt
+end
+handle THM _  => K no_tac  
+     | TYPE _ => K no_tac    
+     | TERM _ => K no_tac
 *}
 
+thm rep_abs_rsp
+
 ML {*
-fun rep_abs_rsp_tac ctxt =
+fun rep_abs_rsp_tac ctxt = 
   SUBGOAL (fn (goal, i) =>
     case (bare_concl goal) of 
       (rel $ _ $ (rep $ (abs $ _))) =>
@@ -698,11 +709,10 @@
            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
            val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
            val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
-           val te = solve_quotient_assums ctxt thm
          in
-           rtac te i
+           (rtac thm THEN' quotient_tac ctxt) i
          end
-         handle _ => no_tac)
+         handle _ => no_tac) (* what is the catch for ? *)
     | _ => no_tac)
 *}