src/HOL/Tools/inductive.ML
changeset 51717 9e7d1c139569
parent 51658 21c10672633b
child 51798 ad3a241def73
     1.1 --- a/src/HOL/Tools/inductive.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    val mono_del: attribute
     1.5    val mk_cases: Proof.context -> term -> thm
     1.6    val inductive_forall_def: thm
     1.7 -  val rulify: thm -> thm
     1.8 +  val rulify: Proof.context -> thm -> thm
     1.9    val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
    1.10      thm list list * local_theory
    1.11    val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
    1.12 @@ -346,10 +346,10 @@
    1.13      ((binding, att), arule)
    1.14    end;
    1.15  
    1.16 -val rulify =
    1.17 -  hol_simplify inductive_conj
    1.18 -  #> hol_simplify inductive_rulify
    1.19 -  #> hol_simplify inductive_rulify_fallback
    1.20 +fun rulify ctxt =
    1.21 +  hol_simplify ctxt inductive_conj
    1.22 +  #> hol_simplify ctxt inductive_rulify
    1.23 +  #> hol_simplify ctxt inductive_rulify_fallback
    1.24    #> Simplifier.norm_hhf;
    1.25  
    1.26  end;
    1.27 @@ -515,7 +515,7 @@
    1.28                EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') THEN
    1.29                prove_intr2 last_c_intr
    1.30              end))
    1.31 -        |> rulify
    1.32 +        |> rulify ctxt'
    1.33          |> singleton (Proof_Context.export ctxt' ctxt'')
    1.34        end;
    1.35    in
    1.36 @@ -533,15 +533,14 @@
    1.37  val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
    1.38  val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
    1.39  
    1.40 -fun simp_case_tac ss i =
    1.41 -  EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i;
    1.42 +fun simp_case_tac ctxt i =
    1.43 +  EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac] i;
    1.44  
    1.45  in
    1.46  
    1.47  fun mk_cases ctxt prop =
    1.48    let
    1.49      val thy = Proof_Context.theory_of ctxt;
    1.50 -    val ss = simpset_of ctxt;
    1.51  
    1.52      fun err msg =
    1.53        error (Pretty.string_of (Pretty.block
    1.54 @@ -550,7 +549,7 @@
    1.55      val elims = Induct.find_casesP ctxt prop;
    1.56  
    1.57      val cprop = Thm.cterm_of thy prop;
    1.58 -    val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
    1.59 +    val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
    1.60      fun mk_elim rl =
    1.61        Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
    1.62        |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
    1.63 @@ -617,7 +616,7 @@
    1.64          (Term.add_vars (lhs_of eq) []);
    1.65    in
    1.66      Drule.cterm_instantiate inst eq
    1.67 -    |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite (simpset_of ctxt))))
    1.68 +    |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt)))
    1.69      |> singleton (Variable.export ctxt' ctxt)
    1.70    end
    1.71  
    1.72 @@ -822,7 +821,7 @@
    1.73               (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
    1.74        ||> Local_Theory.restore_naming lthy;
    1.75      val fp_def' =
    1.76 -      Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
    1.77 +      Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
    1.78          (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));
    1.79      val specs =
    1.80        if length cs < 2 then []
    1.81 @@ -895,7 +894,7 @@
    1.82          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    1.83        Local_Theory.note
    1.84          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
    1.85 -          map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
    1.86 +          map (Attrib.internal o K) (#2 induct)), [rulify lthy1 (#1 induct)]);
    1.87  
    1.88      val (eqs', lthy3) = lthy2 |>
    1.89        fold_map (fn (name, eq) => Local_Theory.note
    1.90 @@ -963,8 +962,8 @@
    1.91      val eqs =
    1.92        if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1;
    1.93  
    1.94 -    val elims' = map (fn (th, ns, i) => (rulify th, ns, i)) elims;
    1.95 -    val intrs' = map rulify intrs;
    1.96 +    val elims' = map (fn (th, ns, i) => (rulify lthy1 th, ns, i)) elims;
    1.97 +    val intrs' = map (rulify lthy1) intrs;
    1.98  
    1.99      val (intrs'', elims'', eqs', induct, inducts, lthy3) =
   1.100        declare_rules rec_name coind no_ind
   1.101 @@ -974,7 +973,7 @@
   1.102        {preds = preds,
   1.103         intrs = intrs'',
   1.104         elims = elims'',
   1.105 -       raw_induct = rulify raw_induct,
   1.106 +       raw_induct = rulify lthy3 raw_induct,
   1.107         induct = induct,
   1.108         inducts = inducts,
   1.109         eqs = eqs'};