src/HOL/Tools/inductive.ML
changeset 54742 7a86358a3c0b
parent 53995 1d457fc83f5c
child 54883 dd04a8b654fc
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -396,7 +396,7 @@
     1.4  
     1.5      val intrs = map_index (fn (i, intr) =>
     1.6        Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
     1.7 -       [rewrite_goals_tac rec_preds_defs,
     1.8 +       [rewrite_goals_tac ctxt rec_preds_defs,
     1.9          rtac (unfold RS iffD2) 1,
    1.10          EVERY1 (select_disj (length intr_ts) (i + 1)),
    1.11          (*Not ares_tac, since refl must be tried before any equality assumptions;
    1.12 @@ -440,14 +440,15 @@
    1.13             map mk_elim_prem (map #1 c_intrs)
    1.14        in
    1.15          (Goal.prove_sorry ctxt'' [] prems P
    1.16 -          (fn {prems, ...} => EVERY
    1.17 +          (fn {context = ctxt4, prems} => EVERY
    1.18              [cut_tac (hd prems) 1,
    1.19 -             rewrite_goals_tac rec_preds_defs,
    1.20 +             rewrite_goals_tac ctxt4 rec_preds_defs,
    1.21               dtac (unfold RS iffD1) 1,
    1.22               REPEAT (FIRSTGOAL (eresolve_tac rules1)),
    1.23               REPEAT (FIRSTGOAL (eresolve_tac rules2)),
    1.24               EVERY (map (fn prem =>
    1.25 -               DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
    1.26 +               DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1))
    1.27 +                (tl prems))])
    1.28            |> singleton (Proof_Context.export ctxt'' ctxt'''),
    1.29           map #2 c_intrs, length Ts)
    1.30        end
    1.31 @@ -503,12 +504,12 @@
    1.32            (if null ts andalso null us then rtac intr 1
    1.33             else
    1.34              EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
    1.35 -            Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
    1.36 +            Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
    1.37                let
    1.38                  val (eqs, prems') = chop (length us) prems;
    1.39                  val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
    1.40                in
    1.41 -                rewrite_goal_tac rew_thms 1 THEN
    1.42 +                rewrite_goal_tac ctxt'' rew_thms 1 THEN
    1.43                  rtac intr 1 THEN
    1.44                  EVERY (map (fn p => rtac p 1) prems')
    1.45                end) ctxt' 1);
    1.46 @@ -545,7 +546,7 @@
    1.47  
    1.48  in
    1.49  
    1.50 -fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
    1.51 +fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac ctxt;
    1.52  
    1.53  fun mk_cases ctxt prop =
    1.54    let
    1.55 @@ -598,7 +599,7 @@
    1.56            val props = Syntax.read_props ctxt' raw_props;
    1.57            val ctxt'' = fold Variable.declare_term props ctxt';
    1.58            val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
    1.59 -        in Method.erule 0 rules end))
    1.60 +        in Method.erule ctxt 0 rules end))
    1.61      "dynamic case analysis on predicates";
    1.62  
    1.63  
    1.64 @@ -724,30 +725,30 @@
    1.65      val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct});
    1.66  
    1.67      val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
    1.68 -      (fn {prems, ...} => EVERY
    1.69 -        [rewrite_goals_tac [inductive_conj_def],
    1.70 +      (fn {context = ctxt3, prems} => EVERY
    1.71 +        [rewrite_goals_tac ctxt3 [inductive_conj_def],
    1.72           DETERM (rtac raw_fp_induct 1),
    1.73           REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
    1.74 -         rewrite_goals_tac simp_thms2,
    1.75 +         rewrite_goals_tac ctxt3 simp_thms2,
    1.76           (*This disjE separates out the introduction rules*)
    1.77           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
    1.78           (*Now break down the individual cases.  No disjE here in case
    1.79             some premise involves disjunction.*)
    1.80 -         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')),
    1.81 +         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt3)),
    1.82           REPEAT (FIRSTGOAL
    1.83             (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
    1.84 -         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
    1.85 +         EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
    1.86               (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
    1.87             conjI, refl] 1)) prems)]);
    1.88  
    1.89      val lemma = Goal.prove_sorry ctxt'' [] []
    1.90 -      (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
    1.91 -        [rewrite_goals_tac rec_preds_defs,
    1.92 +      (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY
    1.93 +        [rewrite_goals_tac ctxt3 rec_preds_defs,
    1.94           REPEAT (EVERY
    1.95             [REPEAT (resolve_tac [conjI, impI] 1),
    1.96              REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
    1.97              atac 1,
    1.98 -            rewrite_goals_tac simp_thms1,
    1.99 +            rewrite_goals_tac ctxt3 simp_thms1,
   1.100              atac 1])]);
   1.101  
   1.102    in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
   1.103 @@ -961,9 +962,9 @@
   1.104        (if no_ind then Drule.asm_rl
   1.105         else if coind then
   1.106           singleton (Proof_Context.export lthy2 lthy1)
   1.107 -           (rotate_prems ~1 (Object_Logic.rulify
   1.108 -             (fold_rule rec_preds_defs
   1.109 -               (rewrite_rule simp_thms3
   1.110 +           (rotate_prems ~1 (Object_Logic.rulify lthy2
   1.111 +             (fold_rule lthy2 rec_preds_defs
   1.112 +               (rewrite_rule lthy2 simp_thms3
   1.113                  (mono RS (fp_def RS @{thm def_coinduct}))))))
   1.114         else
   1.115           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def