src/Tools/induct.ML
changeset 51717 9e7d1c139569
parent 51658 21c10672633b
child 52684 8d749ebd9ab8
     1.1 --- a/src/Tools/induct.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/Tools/induct.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4    val coinduct_type: string -> attribute
     1.5    val coinduct_pred: string -> attribute
     1.6    val coinduct_del: attribute
     1.7 -  val map_simpset: (simpset -> simpset) -> Context.generic -> Context.generic
     1.8 +  val map_simpset: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
     1.9    val induct_simp_add: attribute
    1.10    val induct_simp_del: attribute
    1.11    val no_simpN: string
    1.12 @@ -164,8 +164,7 @@
    1.13  val rearrange_eqs_simproc =
    1.14    Simplifier.simproc_global
    1.15      (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
    1.16 -    (fn thy => fn ss => fn t =>
    1.17 -      mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t));
    1.18 +    (fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t));
    1.19  
    1.20  
    1.21  (* rotate k premises to the left by j, skipping over first j premises *)
    1.22 @@ -225,7 +224,8 @@
    1.23      ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
    1.24       (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
    1.25       (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)),
    1.26 -     empty_ss addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]);
    1.27 +     simpset_of (empty_simpset @{context}
    1.28 +      addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]));
    1.29    val extend = I;
    1.30    fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1),
    1.31        ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) =
    1.32 @@ -331,12 +331,11 @@
    1.33  val coinduct_pred = mk_att add_coinductP consumes1;
    1.34  val coinduct_del = del_att map3;
    1.35  
    1.36 -fun map_simpset f = Data.map (map4 f);
    1.37 +fun map_simpset f context =
    1.38 +  context |> (Data.map o map4 o Simplifier.simpset_map (Context.proof_of context)) f;
    1.39  
    1.40  fun induct_simp f =
    1.41 -  Thm.declaration_attribute (fn thm => fn context =>
    1.42 -      map_simpset
    1.43 -        (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context);
    1.44 +  Thm.declaration_attribute (fn thm => map_simpset (fn ctxt => f (ctxt, [thm])));
    1.45  
    1.46  val induct_simp_add = induct_simp (op addsimps);
    1.47  val induct_simp_del = induct_simp (op delsimps);
    1.48 @@ -444,7 +443,7 @@
    1.49  (* simplify *)
    1.50  
    1.51  fun simplify_conv' ctxt =
    1.52 -  Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)));
    1.53 +  Simplifier.full_rewrite (put_simpset (#4 (get_local ctxt)) ctxt);
    1.54  
    1.55  fun simplify_conv ctxt ct =
    1.56    if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) then