# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1262317183 -3600
# Node ID 27a643e00675847a13ca14ea1709be903311f9d3
# Parent  282fe9cc278eeb28711d08d57b465037c17aee30
tuned

diff -r 282fe9cc278e -r 27a643e00675 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Fri Jan 01 01:10:38 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Jan 01 04:39:43 2010 +0100
@@ -14,6 +14,8 @@
 open Quotient_Info;
 open Quotient_Term;
 
+(* various helper fuctions *)
+
 (* Since HOL_basic_ss is too "big" for us, we *)
 (* need to set up our own minimal simpset.    *)
 fun  mk_minimal_ss ctxt =
@@ -21,25 +23,23 @@
     setsubgoaler asm_simp_tac
     setmksimps (mksimps [])
 
-(* various helper fuctions *)
-
 (* composition of two theorems, used in maps *)
 fun OF1 thm1 thm2 = thm2 RS thm1
 
 (* makes sure a subgoal is solved *)
 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
 
-(* prints warning, if the subgoal is unsolved *)
+(* prints a warning, if the subgoal is not solved *)
 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)
+fun RANGE_WARN tacs = RANGE (map WARN tacs)
 
 fun atomize_thm thm =
 let
-  val thm' = Thm.freezeT (forall_intr_vars thm)
+  val thm' = Thm.freezeT (forall_intr_vars thm) (* TODO: is this proper Isar-technology? *)
   val thm'' = ObjectLogic.atomize (cprop_of thm')
 in
   @{thm equal_elim_rule1} OF [thm'', thm']
@@ -51,13 +51,16 @@
 (*********************)
 
 (* solvers for equivp and quotient assumptions *)
-fun equiv_tac ctxt =
+(* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *)
+(* FIXME / TODO: none of te examples break if added                    *)
+fun equiv_tac ctxt = 
   REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
 
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
-(* test whether DETERM makes any difference *)
+(* FIXME / TODO: test whether DETERM makes any runtime-difference *)
+(* FIXME / TODO: reason: it might back-track over the two alternatives in FIRST' *)
 fun quotient_tac ctxt = SOLVES'  
   (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
@@ -69,7 +72,7 @@
 fun solve_quotient_assm ctxt thm =
   case Seq.pull (quotient_tac ctxt 1 thm) of
     SOME (t, _) => t
-  | _ => error "solve_quotient_assm failed. Maybe a quotient_thm is missing"
+  | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
 
 
 fun prep_trm thy (x, (T, t)) =
@@ -266,7 +269,8 @@
 in
   rtac thm THEN' quotient_tac ctxt
 end
-(* Are they raised by instantiate'? *)
+(* TODO: Are they raised by instantiate'? *)
+(* TODO: Again, can one specify more concretely when no_tac should be returned? *)
 handle THM _  => K no_tac  
      | TYPE _ => K no_tac    
      | TERM _ => K no_tac
@@ -285,11 +289,11 @@
          in
            (rtac inst_thm THEN' quotient_tac ctxt) i
          end
-         handle THM _ => no_tac | TYPE _ => no_tac)
+         handle THM _ => no_tac | TYPE _ => no_tac) (* TODO: same here *)
     | _ => no_tac)
 
 
-(* FIXME /TODO needs to be adapted *)
+(* FIXME / TODO needs to be adapted *)
 (*
 To prove that the regularised theorem implies the abs/rep injected, 
 we try:
@@ -408,7 +412,8 @@
 (* Cleaning of the Theorem *)
 (***************************)
 
-(* expands all fun_maps, except in front of bound variables *)
+(* expands all fun_maps, except in front of the bound *)
+(* variables listed in xs                             *)
 fun fun_map_simple_conv xs ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
@@ -477,7 +482,7 @@
      in
        Conv.rewr_conv ti ctrm
      end
-     handle _ => Conv.all_conv ctrm)
+     handle _ => Conv.all_conv ctrm) (* TODO: another catch all - can this be improved? *)
   | _ => Conv.all_conv ctrm
 
 
@@ -504,10 +509,10 @@
 
 fun clean_tac_aux lthy =
 let
-  (*FIXME produce defs with lthy, like prs and ids *)
+  (* FIXME/TODO produce defs with lthy, like prs and ids *)
   val thy = ProofContext.theory_of lthy;
   val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
-   (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
+  (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
   val prs = prs_rules_get lthy
   val ids = id_simps_get lthy
   
@@ -570,7 +575,7 @@
 (*                                                       *)
 (* the Quot_True premise in 2 records the lifted theorem *)
 
-val lifting_procedure = 
+val lifting_procedure_thm = 
    @{lemma  "[|A; 
                A --> B; 
                Quot_True D ==> B = C; 
@@ -601,10 +606,9 @@
     [SOME (cterm_of thy rtrm'),
      SOME (cterm_of thy reg_goal),
      NONE,
-     SOME (cterm_of thy inj_goal)] lifting_procedure
+     SOME (cterm_of thy inj_goal)] lifting_procedure_thm
 end
 
-
 (* the tactic leaves three subgoals to be proved *)
 fun procedure_tac ctxt rthm =
   ObjectLogic.full_atomize_tac