nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:282fe9cc278e
+:27a643e00675
 struct
 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 =
 Simplifier.context ctxt empty_ss
 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']
 end
 (*********************)
 (* Regularize Tactic *)
 (*********************)
 (* 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},
 resolve_tac (quotient_rules_get ctxt)]))
 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
 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)) =
 (cterm_of thy (Var (x, T)), cterm_of thy t)
 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
-(* 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
 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' 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:
 1) theorems 'trans2' from the appropriate Quot_Type
 (***************************)
 (* 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 $ _) =>
 if (member (op=) xs h)
 then Conv.all_conv ctrm
 else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
 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
 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 (*                                                     *)
 (* 5. test for refl                                    *)
 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 *)
 val prs = prs_rules_get lthy
 val ids = id_simps_get lthy
 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
 val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs})
 (* - 2nd prem is the rep/abs injection step              *)
 (* - 3rd prem is the cleaning part                       *)
 (*                                                       *)
 (* 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;
 C = D|] ==> D"
 by (simp add: Quot_True_def)}
 in
 Drule.instantiate' []
 [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
 THEN' gen_frees_tac ctxt

changeset 802	27a643e00675
parent 789	8237786171f1
child 804	ba7e81531c6d