src/ZF/Tools/inductive_package.ML
changeset 58838 59203adfc33f
parent 58028 e4250d370657
child 58936 7fbe4436952d
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -189,7 +189,7 @@
     1.4    val bnd_mono =
     1.5      Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
     1.6        (fn _ => EVERY
     1.7 -        [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
     1.8 +        [resolve_tac [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
     1.9           REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
    1.10  
    1.11    val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
    1.12 @@ -218,13 +218,13 @@
    1.13      [DETERM (stac unfold 1),
    1.14       REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1),
    1.15       (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
    1.16 -     rtac disjIn 2,
    1.17 +     resolve_tac [disjIn] 2,
    1.18       (*Not ares_tac, since refl must be tried before equality assumptions;
    1.19         backtracking may occur if the premises have extra variables!*)
    1.20       DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
    1.21       (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
    1.22       rewrite_goals_tac ctxt con_defs,
    1.23 -     REPEAT (rtac @{thm refl} 2),
    1.24 +     REPEAT (resolve_tac @{thms refl} 2),
    1.25       (*Typechecking; this can fail*)
    1.26       if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:"
    1.27       else all_tac,
    1.28 @@ -332,15 +332,15 @@
    1.29             setSolver (mk_solver "minimal"
    1.30                        (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)
    1.31                                     ORELSE' assume_tac
    1.32 -                                   ORELSE' etac @{thm FalseE}));
    1.33 +                                   ORELSE' eresolve_tac @{thms FalseE}));
    1.34  
    1.35       val quant_induct =
    1.36         Goal.prove_global thy1 [] ind_prems
    1.37           (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
    1.38           (fn {context = ctxt, prems} => EVERY
    1.39             [rewrite_goals_tac ctxt part_rec_defs,
    1.40 -            rtac (@{thm impI} RS @{thm allI}) 1,
    1.41 -            DETERM (etac raw_induct 1),
    1.42 +            resolve_tac [@{thm impI} RS @{thm allI}] 1,
    1.43 +            DETERM (eresolve_tac [raw_induct] 1),
    1.44              (*Push Part inside Collect*)
    1.45              full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1,
    1.46              (*This CollectE and disjE separates out the introduction rules*)
    1.47 @@ -470,8 +470,8 @@
    1.48                        (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
    1.49                     THEN
    1.50                     (*unpackage and use "prem" in the corresponding place*)
    1.51 -                   REPEAT (rtac @{thm impI} 1)  THEN
    1.52 -                   rtac (rewrite_rule ctxt all_defs prem) 1  THEN
    1.53 +                   REPEAT (resolve_tac @{thms impI} 1)  THEN
    1.54 +                   resolve_tac [rewrite_rule ctxt all_defs prem] 1  THEN
    1.55                     (*prem must not be REPEATed below: could loop!*)
    1.56                     DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
    1.57                                             eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
    1.58 @@ -483,7 +483,7 @@
    1.59           Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
    1.60             mutual_induct_concl
    1.61             (fn {context = ctxt, prems} => EVERY
    1.62 -             [rtac (quant_induct RS lemma) 1,
    1.63 +             [resolve_tac [quant_induct RS lemma] 1,
    1.64                mutual_ind_tac ctxt (rev prems) (length prems)])
    1.65         else @{thm TrueI};
    1.66