simprocs: Simplifier.inherit_bounds;
authorwenzelm
Mon Aug 01 19:20:26 2005 +0200 (2005-08-01)
changeset 16973b2a894562b8f
parent 16972 d3f9abe00712
child 16974 0f8ebabf3163
simprocs: Simplifier.inherit_bounds;
src/HOL/Algebra/abstract/Ring.thy
src/HOL/Fun.thy
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/List.thy
src/HOL/Real/RealDef.thy
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/record_package.ML
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/assoc_fold.ML
src/Provers/Arith/cancel_numeral_factor.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
src/Provers/Arith/extract_common_term.ML
src/ZF/Datatype.ML
src/ZF/Induct/Multiset.thy
src/ZF/Integ/int_arith.ML
src/ZF/arith_data.ML
     1.1 --- a/src/HOL/Algebra/abstract/Ring.thy	Mon Aug 01 19:20:25 2005 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Ring.thy	Mon Aug 01 19:20:26 2005 +0200
     1.3 @@ -163,11 +163,11 @@
     1.4  	 "t - u::'a::ring",
     1.5  	 "t * u::'a::ring",
     1.6  	 "- t::'a::ring"];
     1.7 -    fun proc sg _ t = 
     1.8 +    fun proc sg ss t = 
     1.9        let val rew = Tactic.prove sg [] []
    1.10              (HOLogic.mk_Trueprop
    1.11                (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
    1.12 -                (fn _ => simp_tac ring_ss 1)
    1.13 +                (fn _ => simp_tac (Simplifier.inherit_bounds ss ring_ss) 1)
    1.14              |> mk_meta_eq;
    1.15            val (t', u) = Logic.dest_equals (Thm.prop_of rew);
    1.16        in if t' aconv u 
    1.17 @@ -175,7 +175,7 @@
    1.18          else SOME rew 
    1.19      end;
    1.20    in
    1.21 -    val ring_simproc = Simplifier.simproc (sign_of (the_context ())) "ring" lhss proc;
    1.22 +    val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss proc;
    1.23    end;
    1.24  *}
    1.25  
     2.1 --- a/src/HOL/Fun.thy	Mon Aug 01 19:20:25 2005 +0200
     2.2 +++ b/src/HOL/Fun.thy	Mon Aug 01 19:20:26 2005 +0200
     2.3 @@ -486,15 +486,18 @@
     2.4          | find t = NONE
     2.5      in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
     2.6  
     2.7 -  val ss = simpset ()
     2.8 -  val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1)
     2.9 +  val current_ss = simpset ()
    2.10 +  fun fun_upd_prover ss =
    2.11 +    rtac eq_reflection 1 THEN rtac ext 1 THEN
    2.12 +    simp_tac (Simplifier.inherit_bounds ss current_ss) 1
    2.13  in
    2.14    val fun_upd2_simproc =
    2.15      Simplifier.simproc (Theory.sign_of (the_context ()))
    2.16        "fun_upd2" ["f(v := w, x := y)"]
    2.17 -      (fn sg => fn _ => fn t =>
    2.18 +      (fn sg => fn ss => fn t =>
    2.19          case find_double t of (T, NONE) => NONE
    2.20 -        | (T, SOME rhs) => SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover))
    2.21 +        | (T, SOME rhs) =>
    2.22 +            SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
    2.23  end;
    2.24  Addsimprocs[fun_upd2_simproc];
    2.25  
     3.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Aug 01 19:20:25 2005 +0200
     3.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon Aug 01 19:20:26 2005 +0200
     3.3 @@ -150,7 +150,7 @@
     3.4    ordering is not well-founded.*)
     3.5  fun num_ord (i,j) =
     3.6        (case IntInf.compare (IntInf.abs i, IntInf.abs j) of
     3.7 -            EQUAL => Int.compare (IntInf.sign i, IntInf.sign j) 
     3.8 +            EQUAL => int_ord (IntInf.sign i, IntInf.sign j) 
     3.9            | ord => ord);
    3.10  
    3.11  (*This resembles Term.term_ord, but it puts binary numerals before other
    3.12 @@ -165,7 +165,7 @@
    3.13    | numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
    3.14    | numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
    3.15    | numterm_ord (t, u) =
    3.16 -      (case Int.compare (size_of_term t, size_of_term u) of
    3.17 +      (case int_ord (size_of_term t, size_of_term u) of
    3.18          EQUAL =>
    3.19            let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    3.20              (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    3.21 @@ -308,8 +308,8 @@
    3.22  fun trans_tac NONE      = all_tac
    3.23    | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
    3.24  
    3.25 -fun simplify_meta_eq rules =
    3.26 -    simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
    3.27 +fun simplify_meta_eq rules ss =
    3.28 +    simplify (Simplifier.inherit_bounds ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
    3.29      o mk_meta_eq;
    3.30  
    3.31  structure CancelNumeralsCommon =
    3.32 @@ -319,15 +319,17 @@
    3.33    val mk_coeff          = mk_coeff
    3.34    val dest_coeff        = dest_coeff 1
    3.35    val find_first_coeff  = find_first_coeff []
    3.36 -  val trans_tac         = trans_tac
    3.37 -  val norm_tac =
    3.38 -     ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
    3.39 -                                         diff_simps@minus_simps@add_ac))
    3.40 -     THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
    3.41 -     THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
    3.42 -                                              add_ac@mult_ac))
    3.43 -  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    3.44 -  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
    3.45 +  val trans_tac         = fn _ => trans_tac
    3.46 +  fun norm_tac ss =
    3.47 +    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    3.48 +      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    3.49 +                                         diff_simps @ minus_simps @ add_ac))
    3.50 +      THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
    3.51 +      THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
    3.52 +    end
    3.53 +  fun numeral_simp_tac ss =
    3.54 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    3.55 +  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
    3.56    end;
    3.57  
    3.58  
    3.59 @@ -395,16 +397,17 @@
    3.60    val dest_coeff        = dest_coeff 1
    3.61    val left_distrib      = combine_common_factor RS trans
    3.62    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    3.63 -  val trans_tac          = trans_tac
    3.64 -  val norm_tac =
    3.65 -     ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
    3.66 -                                         diff_simps@minus_simps@add_ac))
    3.67 -     THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
    3.68 -     THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
    3.69 -                                              add_ac@mult_ac))
    3.70 -  val numeral_simp_tac  = ALLGOALS
    3.71 -                    (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    3.72 -  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
    3.73 +  val trans_tac         = fn _ => trans_tac
    3.74 +  fun norm_tac ss =
    3.75 +    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    3.76 +      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    3.77 +                                          diff_simps @ minus_simps @ add_ac))
    3.78 +      THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
    3.79 +      THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
    3.80 +    end
    3.81 +  fun numeral_simp_tac ss =
    3.82 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    3.83 +  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
    3.84    end;
    3.85  
    3.86  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
     4.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Mon Aug 01 19:20:25 2005 +0200
     4.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Mon Aug 01 19:20:26 2005 +0200
     4.3 @@ -42,14 +42,16 @@
     4.4    struct
     4.5    val mk_coeff          = mk_coeff
     4.6    val dest_coeff        = dest_coeff 1
     4.7 -  val trans_tac         = trans_tac
     4.8 -  val norm_tac =
     4.9 -     ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
    4.10 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
    4.11 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
    4.12 -  val numeral_simp_tac  =
    4.13 -         ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
    4.14 -  val simplify_meta_eq  = 
    4.15 +  val trans_tac         = fn _ => trans_tac
    4.16 +  fun norm_tac ss =
    4.17 +    let val HOL_ss' = Simplifier.inherit_bounds ss HOL_ss in
    4.18 +      ALLGOALS (simp_tac (HOL_ss' addsimps minus_from_mult_simps @ mult_1s))
    4.19 +      THEN ALLGOALS (simp_tac (HOL_ss' addsimps bin_simps@mult_minus_simps))
    4.20 +      THEN ALLGOALS (simp_tac (HOL_ss' addsimps mult_ac))
    4.21 +    end
    4.22 +  fun numeral_simp_tac ss =
    4.23 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rel_number_of @ bin_simps))
    4.24 +  val simplify_meta_eq = 
    4.25  	Int_Numeral_Simprocs.simplify_meta_eq
    4.26  	     [add_0, add_0_right,
    4.27  	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
    4.28 @@ -235,8 +237,8 @@
    4.29      Int_Numeral_Simprocs.simplify_meta_eq  
    4.30         [mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1];
    4.31  
    4.32 -fun cancel_simplify_meta_eq cancel_th th =
    4.33 -    simplify_one (([th, cancel_th]) MRS trans);
    4.34 +fun cancel_simplify_meta_eq cancel_th ss th =
    4.35 +    simplify_one ss (([th, cancel_th]) MRS trans);
    4.36  
    4.37  (*At present, long_mk_prod creates Numeral1, so this requires the axclass
    4.38    number_ring*)
    4.39 @@ -247,8 +249,9 @@
    4.40    val mk_coeff          = mk_coeff
    4.41    val dest_coeff        = dest_coeff
    4.42    val find_first        = find_first []
    4.43 -  val trans_tac         = trans_tac
    4.44 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
    4.45 +  val trans_tac         = fn _ => trans_tac
    4.46 +  fun norm_tac ss =
    4.47 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
    4.48    end;
    4.49  
    4.50  (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
     5.1 --- a/src/HOL/Integ/nat_simprocs.ML	Mon Aug 01 19:20:25 2005 +0200
     5.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Mon Aug 01 19:20:26 2005 +0200
     5.3 @@ -168,14 +168,15 @@
     5.4    val mk_coeff          = mk_coeff
     5.5    val dest_coeff        = dest_coeff
     5.6    val find_first_coeff  = find_first_coeff []
     5.7 -  val trans_tac          = trans_tac
     5.8 -  val norm_tac = ALLGOALS
     5.9 -                   (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
    5.10 +  val trans_tac         = fn _ => trans_tac
    5.11 +  fun norm_tac ss =
    5.12 +    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    5.13 +      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    5.14                                  [Suc_eq_add_numeral_1_left] @ add_ac))
    5.15 -                 THEN ALLGOALS (simp_tac
    5.16 -                                (num_ss addsimps bin_simps@add_ac@mult_ac))
    5.17 -  val numeral_simp_tac  = ALLGOALS
    5.18 -                (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    5.19 +      THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
    5.20 +    end
    5.21 +  fun numeral_simp_tac ss =
    5.22 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    5.23    val simplify_meta_eq  = simplify_meta_eq
    5.24    end;
    5.25  
    5.26 @@ -252,14 +253,15 @@
    5.27    val dest_coeff        = dest_coeff
    5.28    val left_distrib      = left_add_mult_distrib RS trans
    5.29    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    5.30 -  val trans_tac          = trans_tac
    5.31 -  val norm_tac = ALLGOALS
    5.32 -                   (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
    5.33 +  val trans_tac         = fn _ => trans_tac
    5.34 +  fun norm_tac ss =
    5.35 +    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    5.36 +      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    5.37                                [Suc_eq_add_numeral_1] @ add_ac))
    5.38 -                 THEN ALLGOALS (simp_tac
    5.39 -                                (num_ss addsimps bin_simps@add_ac@mult_ac))
    5.40 -  val numeral_simp_tac  = ALLGOALS
    5.41 -                (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    5.42 +      THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
    5.43 +    end
    5.44 +  fun numeral_simp_tac ss =
    5.45 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    5.46    val simplify_meta_eq  = simplify_meta_eq
    5.47    end;
    5.48  
    5.49 @@ -275,13 +277,15 @@
    5.50    struct
    5.51    val mk_coeff          = mk_coeff
    5.52    val dest_coeff        = dest_coeff
    5.53 -  val trans_tac         = trans_tac
    5.54 -  val norm_tac = ALLGOALS
    5.55 -                   (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
    5.56 +  val trans_tac         = fn _ => trans_tac
    5.57 +  fun norm_tac ss =
    5.58 +    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    5.59 +      ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    5.60                                  [Suc_eq_add_numeral_1_left] @ add_ac))
    5.61 -                 THEN ALLGOALS (simp_tac
    5.62 -                                (num_ss addsimps bin_simps@add_ac@mult_ac))
    5.63 -  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    5.64 +      THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
    5.65 +    end
    5.66 +  fun numeral_simp_tac ss =
    5.67 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps bin_simps))
    5.68    val simplify_meta_eq  = simplify_meta_eq
    5.69    end
    5.70  
    5.71 @@ -356,8 +360,8 @@
    5.72      Int_Numeral_Simprocs.simplify_meta_eq  
    5.73         [mult_1_left, mult_1_right, div_1, numeral_1_eq_Suc_0];
    5.74  
    5.75 -fun cancel_simplify_meta_eq cancel_th th =
    5.76 -    simplify_one (([th, cancel_th]) MRS trans);
    5.77 +fun cancel_simplify_meta_eq cancel_th ss th =
    5.78 +    simplify_one ss (([th, cancel_th]) MRS trans);
    5.79  
    5.80  structure CancelFactorCommon =
    5.81    struct
    5.82 @@ -366,8 +370,9 @@
    5.83    val mk_coeff          = mk_coeff
    5.84    val dest_coeff        = dest_coeff
    5.85    val find_first        = find_first []
    5.86 -  val trans_tac         = trans_tac
    5.87 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
    5.88 +  val trans_tac         = fn _ => trans_tac
    5.89 +  fun norm_tac ss =
    5.90 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
    5.91    end;
    5.92  
    5.93  structure EqCancelFactor = ExtractCommonTermFun
     6.1 --- a/src/HOL/List.thy	Mon Aug 01 19:20:25 2005 +0200
     6.2 +++ b/src/HOL/List.thy	Mon Aug 01 19:20:26 2005 +0200
     6.3 @@ -415,10 +415,9 @@
     6.4    | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
     6.5    | butlast xs = Const("List.list.Nil",fastype_of xs);
     6.6  
     6.7 -val rearr_tac =
     6.8 -  simp_tac (HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons]);
     6.9 -
    6.10 -fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    6.11 +val rearr_ss = HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons];
    6.12 +
    6.13 +fun list_eq sg ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    6.14    let
    6.15      val lastl = last lhs and lastr = last rhs;
    6.16      fun rearr conv =
    6.17 @@ -429,7 +428,8 @@
    6.18          val app = Const("List.op @",appT)
    6.19          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    6.20          val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
    6.21 -        val thm = Tactic.prove sg [] [] eq (K (rearr_tac 1));
    6.22 +        val thm = Tactic.prove sg [] [] eq
    6.23 +          (K (simp_tac (Simplifier.inherit_bounds ss rearr_ss) 1));
    6.24        in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
    6.25  
    6.26    in
     7.1 --- a/src/HOL/Real/RealDef.thy	Mon Aug 01 19:20:25 2005 +0200
     7.2 +++ b/src/HOL/Real/RealDef.thy	Mon Aug 01 19:20:26 2005 +0200
     7.3 @@ -425,9 +425,9 @@
     7.4                   linorder_not_le [where 'a = preal] 
     7.5                    real_zero_def real_le real_mult)
     7.6    --{*Reduce to the (simpler) @{text "\<le>"} relation *}
     7.7 -apply (auto  dest!: less_add_left_Ex 
     7.8 +apply (auto dest!: less_add_left_Ex
     7.9       simp add: preal_add_ac preal_mult_ac 
    7.10 -          preal_add_mult_distrib2 preal_cancels preal_self_less_add_right)
    7.11 +          preal_add_mult_distrib2 preal_cancels preal_self_less_add_left)
    7.12  done
    7.13  
    7.14  lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
    7.15 @@ -478,7 +478,6 @@
    7.16  apply (auto simp add: real_minus preal_add_ac)
    7.17  apply (cut_tac x = x and y = y in linorder_less_linear)
    7.18  apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc [symmetric])
    7.19 -apply (auto simp add: preal_add_commute)
    7.20  done
    7.21  
    7.22  lemma real_of_preal_leD:
     8.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Aug 01 19:20:25 2005 +0200
     8.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Aug 01 19:20:26 2005 +0200
     8.3 @@ -326,7 +326,7 @@
     8.4  
     8.5  exception ConstrDistinct of term;
     8.6  
     8.7 -fun distinct_proc sg _ (t as Const ("op =", _) $ t1 $ t2) =
     8.8 +fun distinct_proc sg ss (t as Const ("op =", _) $ t1 $ t2) =
     8.9    (case (stripC (0, t1), stripC (0, t2)) of
    8.10       ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
    8.11           (case (stripT (0, T1), stripT (0, T2)) of
    8.12 @@ -347,9 +347,9 @@
    8.13                                 | FewConstrs thms => SOME (Tactic.prove sg [] [] eq_t (K
    8.14                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    8.15                                      atac 2, resolve_tac thms 1, etac FalseE 1])))
    8.16 -                               | ManyConstrs (thm, ss) => SOME (Tactic.prove sg [] [] eq_t (K
    8.17 +                               | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
    8.18                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    8.19 -                                    full_simp_tac ss 1,
    8.20 +                                    full_simp_tac (Simplifier.inherit_bounds ss simpset) 1,
    8.21                                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    8.22                                      eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    8.23                                      etac FalseE 1]))))
     9.1 --- a/src/HOL/Tools/record_package.ML	Mon Aug 01 19:20:25 2005 +0200
     9.2 +++ b/src/HOL/Tools/record_package.ML	Mon Aug 01 19:20:26 2005 +0200
     9.3 @@ -833,7 +833,7 @@
     9.4        else opt ();
     9.5  
     9.6  
     9.7 -fun prove_split_simp sg T prop =
     9.8 +fun prove_split_simp sg ss T prop =
     9.9    let 
    9.10      val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
    9.11      val extsplits = 
    9.12 @@ -844,7 +844,9 @@
    9.13                       all_thm::(case extsplits of [thm] => [] | _ => extsplits)
    9.14                                (* [thm] is the same as all_thm *)
    9.15                   | NONE => extsplits)                                
    9.16 -  in (quick_and_dirty_prove true sg [] prop (fn _ => (simp_tac (simpset addsimps thms) 1)))
    9.17 +  in
    9.18 +    quick_and_dirty_prove true sg [] prop
    9.19 +      (fn _ => simp_tac (Simplifier.inherit_bounds ss simpset addsimps thms) 1)
    9.20    end;
    9.21  
    9.22  
    9.23 @@ -868,7 +870,7 @@
    9.24   *)
    9.25  val record_simproc =
    9.26    Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
    9.27 -    (fn sg => fn _ => fn t =>
    9.28 +    (fn sg => fn ss => fn t =>
    9.29        (case t of (sel as Const (s, Type (_,[domS,rangeS])))$
    9.30                     ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=>
    9.31          (case get_selectors sg s of SOME () =>
    9.32 @@ -908,9 +910,9 @@
    9.33  	      (case mk_eq_terms (upd$k$r) of
    9.34                   SOME (trm,trm',vars,update_s) 
    9.35                   => if update_s 
    9.36 -		    then SOME (prove_split_simp sg domS 
    9.37 +		    then SOME (prove_split_simp sg ss domS 
    9.38                                   (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
    9.39 -                    else SOME (prove_split_simp sg domS 
    9.40 +                    else SOME (prove_split_simp sg ss domS 
    9.41                                   (list_all(vars,(equals rangeS$(sel$trm)$(sel$trm')))))
    9.42                 | NONE => NONE)
    9.43              end
    9.44 @@ -929,7 +931,7 @@
    9.45  *)
    9.46  val record_upd_simproc =
    9.47    Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u k r)"]
    9.48 -    (fn sg => fn _ => fn t =>
    9.49 +    (fn sg => fn ss => fn t =>
    9.50        (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
    9.51   	 let datatype ('a,'b) calc = Init of 'b | Inter of 'a  
    9.52               val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
    9.53 @@ -1020,7 +1022,7 @@
    9.54  
    9.55  	 in (case mk_updterm updates [] t of
    9.56  	       Inter (trm,trm',vars,_)
    9.57 -                => SOME (prove_split_simp sg rT  
    9.58 +                => SOME (prove_split_simp sg ss rT  
    9.59                            (list_all(vars,(equals rT$trm$trm'))))
    9.60               | _ => NONE)
    9.61  	 end
    9.62 @@ -1083,11 +1085,12 @@
    9.63  
    9.64  val record_ex_sel_eq_simproc =
    9.65    Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
    9.66 -    (fn sg => fn _ => fn t =>
    9.67 +    (fn sg => fn ss => fn t =>
    9.68         let 
    9.69 -         fun prove prop = (quick_and_dirty_prove true sg [] prop 
    9.70 -                             (fn _ => (simp_tac ((get_simpset sg) addsimps simp_thms
    9.71 -                                        addsimprocs [record_split_simproc (K ~1)]) 1)));
    9.72 +         fun prove prop =
    9.73 +           quick_and_dirty_prove true sg [] prop
    9.74 +             (fn _ => simp_tac (Simplifier.inherit_bounds ss (get_simpset sg)
    9.75 +               addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
    9.76  
    9.77           fun mkeq (lr,Teq,(sel,Tsel),x) i =
    9.78                (case get_selectors sg sel of SOME () =>
    10.1 --- a/src/Provers/Arith/abel_cancel.ML	Mon Aug 01 19:20:25 2005 +0200
    10.2 +++ b/src/Provers/Arith/abel_cancel.ML	Mon Aug 01 19:20:26 2005 +0200
    10.3 @@ -88,10 +88,10 @@
    10.4  
    10.5  (* A simproc to cancel complementary terms in arbitrary sums. *)
    10.6  
    10.7 -fun sum_proc sg _ t =
    10.8 +fun sum_proc sg ss t =
    10.9     let val t' = cancel sg t
   10.10         val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
   10.11 -                   (fn _ => simp_tac cancel_ss 1)
   10.12 +                   (fn _ => simp_tac (Simplifier.inherit_bounds ss cancel_ss) 1)
   10.13     in SOME thm end
   10.14     handle Cancel => NONE;
   10.15  
   10.16 @@ -108,12 +108,12 @@
   10.17     Reduces the problem to subtraction.
   10.18   *)
   10.19  
   10.20 - fun rel_proc sg _ t =
   10.21 + fun rel_proc sg ss t =
   10.22     let val t' = cancel sg t
   10.23         val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
   10.24                     (fn _ => rtac eq_reflection 1 THEN
   10.25                              resolve_tac eqI_rules 1 THEN
   10.26 -                            simp_tac cancel_ss 1)
   10.27 +                            simp_tac (Simplifier.inherit_bounds ss cancel_ss) 1)
   10.28     in SOME thm end
   10.29     handle Cancel => NONE;
   10.30  
    11.1 --- a/src/Provers/Arith/assoc_fold.ML	Mon Aug 01 19:20:25 2005 +0200
    11.2 +++ b/src/Provers/Arith/assoc_fold.ML	Mon Aug 01 19:20:26 2005 +0200
    11.3 @@ -42,7 +42,7 @@
    11.4   val trace = ref false;
    11.5  
    11.6   (*Make a simproc to combine all literals in a associative nest*)
    11.7 - fun proc thy _ lhs =
    11.8 + fun proc thy ss lhs =
    11.9     let fun show t = string_of_cterm (Thm.cterm_of thy t)
   11.10         val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
   11.11                 else ()
   11.12 @@ -56,7 +56,7 @@
   11.13         val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
   11.14         val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs))
   11.15                     (fn _ => rtac Data.eq_reflection 1 THEN
   11.16 -                            simp_tac assoc_ss 1)
   11.17 +                            simp_tac (Simplifier.inherit_bounds ss assoc_ss) 1)
   11.18     in SOME th end
   11.19     handle Assoc_fail => NONE;
   11.20  
    12.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML	Mon Aug 01 19:20:25 2005 +0200
    12.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML	Mon Aug 01 19:20:26 2005 +0200
    12.3 @@ -29,24 +29,24 @@
    12.4    val neg_exchanges: bool  (*true if a negative coeff swaps the two operands,
    12.5                               as with < and <= but not = and div*)
    12.6    (*proof tools*)
    12.7 -  val prove_conv: tactic list -> Sign.sg -> 
    12.8 +  val prove_conv: tactic list -> theory -> 
    12.9                    thm list -> string list -> term * term -> thm option
   12.10 -  val trans_tac: thm option -> tactic (*applies the initial lemma*)
   12.11 -  val norm_tac: tactic                (*proves the initial lemma*)
   12.12 -  val numeral_simp_tac: tactic        (*proves the final theorem*)
   12.13 -  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
   12.14 +  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
   12.15 +  val norm_tac: simpset -> tactic                (*proves the initial lemma*)
   12.16 +  val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
   12.17 +  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
   12.18  end;
   12.19  
   12.20  
   12.21  functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
   12.22    sig
   12.23 -  val proc: Sign.sg -> simpset -> term -> thm option
   12.24 +  val proc: theory -> simpset -> term -> thm option
   12.25    end 
   12.26  =
   12.27  struct
   12.28  
   12.29  (*the simplification procedure*)
   12.30 -fun proc sg ss t =
   12.31 +fun proc thy ss t =
   12.32    let
   12.33        val hyps = prems_of_ss ss;
   12.34        (*first freeze any Vars in the term to prevent flex-flex problems*)
   12.35 @@ -67,13 +67,13 @@
   12.36                  else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2'))
   12.37        val reshape =  (*Move d to the front and put the rest into standard form
   12.38  		       i * #m * j == #d * (#n * (j * k)) *)
   12.39 -	    Data.prove_conv [Data.norm_tac] sg hyps xs
   12.40 +	    Data.prove_conv [Data.norm_tac ss] thy hyps xs
   12.41  	      (t',   Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
   12.42    in
   12.43 -      Option.map Data.simplify_meta_eq
   12.44 +      Option.map (Data.simplify_meta_eq ss)
   12.45         (Data.prove_conv 
   12.46 -	       [Data.trans_tac reshape, rtac Data.cancel 1,
   12.47 -		Data.numeral_simp_tac] sg hyps xs (t', rhs))
   12.48 +	       [Data.trans_tac ss reshape, rtac Data.cancel 1,
   12.49 +		Data.numeral_simp_tac ss] thy hyps xs (t', rhs))
   12.50    end
   12.51    handle TERM _ => NONE
   12.52         | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    13.1 --- a/src/Provers/Arith/cancel_numerals.ML	Mon Aug 01 19:20:25 2005 +0200
    13.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Mon Aug 01 19:20:26 2005 +0200
    13.3 @@ -36,18 +36,18 @@
    13.4    val bal_add1: thm
    13.5    val bal_add2: thm
    13.6    (*proof tools*)
    13.7 -  val prove_conv: tactic list -> Sign.sg -> 
    13.8 +  val prove_conv: tactic list -> theory -> 
    13.9                    thm list -> string list -> term * term -> thm option
   13.10 -  val trans_tac: thm option -> tactic (*applies the initial lemma*)
   13.11 -  val norm_tac: tactic                (*proves the initial lemma*)
   13.12 -  val numeral_simp_tac: tactic        (*proves the final theorem*)
   13.13 -  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
   13.14 +  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
   13.15 +  val norm_tac: simpset -> tactic                (*proves the initial lemma*)
   13.16 +  val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
   13.17 +  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
   13.18  end;
   13.19  
   13.20  
   13.21  functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
   13.22    sig
   13.23 -  val proc: Sign.sg -> simpset -> term -> thm option
   13.24 +  val proc: theory -> simpset -> term -> thm option
   13.25    end 
   13.26  =
   13.27  struct
   13.28 @@ -69,7 +69,7 @@
   13.29    in  seek terms1 end;
   13.30  
   13.31  (*the simplification procedure*)
   13.32 -fun proc sg ss t =
   13.33 +fun proc thy ss t =
   13.34    let
   13.35        val hyps = prems_of_ss ss;
   13.36        (*first freeze any Vars in the term to prevent flex-flex problems*)
   13.37 @@ -86,22 +86,22 @@
   13.38  		       i + #m + j + k == #m + i + (j + k) *)
   13.39  	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
   13.40  		raise TERM("cancel_numerals", []) 
   13.41 -	    else Data.prove_conv [Data.norm_tac] sg hyps xs
   13.42 +	    else Data.prove_conv [Data.norm_tac ss] thy hyps xs
   13.43  			(t', 
   13.44  			 Data.mk_bal (newshape(n1,terms1'), 
   13.45  				      newshape(n2,terms2')))
   13.46    in
   13.47 -      Option.map Data.simplify_meta_eq
   13.48 +      Option.map (Data.simplify_meta_eq ss)
   13.49         (if n2<=n1 then 
   13.50  	    Data.prove_conv 
   13.51 -	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
   13.52 -		Data.numeral_simp_tac] sg hyps xs
   13.53 +	       [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
   13.54 +		Data.numeral_simp_tac ss] thy hyps xs
   13.55  	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
   13.56  				 Data.mk_sum T terms2'))
   13.57  	else
   13.58  	    Data.prove_conv 
   13.59 -	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
   13.60 -		Data.numeral_simp_tac] sg hyps xs
   13.61 +	       [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
   13.62 +		Data.numeral_simp_tac ss] thy hyps xs
   13.63  	       (t', Data.mk_bal (Data.mk_sum T terms1', 
   13.64  				 newshape(n2-n1,terms2'))))
   13.65    end
    14.1 --- a/src/Provers/Arith/combine_numerals.ML	Mon Aug 01 19:20:25 2005 +0200
    14.2 +++ b/src/Provers/Arith/combine_numerals.ML	Mon Aug 01 19:20:26 2005 +0200
    14.3 @@ -27,17 +27,17 @@
    14.4    (*rules*)
    14.5    val left_distrib: thm
    14.6    (*proof tools*)
    14.7 -  val prove_conv: tactic list -> Sign.sg -> string list -> term * term -> thm option
    14.8 -  val trans_tac: thm option -> tactic (*applies the initial lemma*)
    14.9 -  val norm_tac: tactic                (*proves the initial lemma*)
   14.10 -  val numeral_simp_tac: tactic        (*proves the final theorem*)
   14.11 -  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
   14.12 +  val prove_conv: tactic list -> theory -> string list -> term * term -> thm option
   14.13 +  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
   14.14 +  val norm_tac: simpset -> tactic                (*proves the initial lemma*)
   14.15 +  val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
   14.16 +  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
   14.17  end;
   14.18  
   14.19  
   14.20  functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
   14.21    sig
   14.22 -  val proc: Sign.sg -> simpset -> term -> thm option
   14.23 +  val proc: theory -> simpset -> term -> thm option
   14.24    end 
   14.25  =
   14.26  struct
   14.27 @@ -64,7 +64,7 @@
   14.28  	| NONE => find_repeated (tab, t::past, terms);
   14.29  
   14.30  (*the simplification procedure*)
   14.31 -fun proc sg _ t =
   14.32 +fun proc thy ss t =
   14.33    let (*first freeze any Vars in the term to prevent flex-flex problems*)
   14.34        val (t', xs) = Term.adhoc_freeze_vars t
   14.35        val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
   14.36 @@ -73,15 +73,15 @@
   14.37  		       i + #m + j + k == #m + i + (j + k) *)
   14.38  	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
   14.39  		raise TERM("combine_numerals", []) 
   14.40 -	    else Data.prove_conv [Data.norm_tac] sg xs
   14.41 +	    else Data.prove_conv [Data.norm_tac ss] thy xs
   14.42  			(t', 
   14.43  			 Data.mk_sum T ([Data.mk_coeff(m,u),
   14.44  				         Data.mk_coeff(n,u)] @ terms))
   14.45    in
   14.46 -      Option.map Data.simplify_meta_eq
   14.47 +      Option.map (Data.simplify_meta_eq ss)
   14.48  	 (Data.prove_conv 
   14.49 -	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
   14.50 -	     Data.numeral_simp_tac] sg xs
   14.51 +	    [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
   14.52 +	     Data.numeral_simp_tac ss] thy xs
   14.53  	    (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
   14.54    end
   14.55    handle TERM _ => NONE
    15.1 --- a/src/Provers/Arith/extract_common_term.ML	Mon Aug 01 19:20:25 2005 +0200
    15.2 +++ b/src/Provers/Arith/extract_common_term.ML	Mon Aug 01 19:20:26 2005 +0200
    15.3 @@ -23,34 +23,34 @@
    15.4    val dest_bal: term -> term * term
    15.5    val find_first: term -> term list -> term list
    15.6    (*proof tools*)
    15.7 -  val prove_conv: tactic list -> Sign.sg -> 
    15.8 +  val prove_conv: tactic list -> theory -> 
    15.9                    thm list -> string list -> term * term -> thm option
   15.10 -  val norm_tac: tactic                (*proves the result*)
   15.11 -  val simplify_meta_eq: thm -> thm    (*simplifies the result*)
   15.12 +  val norm_tac: simpset -> tactic                (*proves the result*)
   15.13 +  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the result*)
   15.14  end;
   15.15  
   15.16  
   15.17  functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
   15.18    sig
   15.19 -  val proc: Sign.sg -> simpset -> term -> thm option
   15.20 +  val proc: theory -> simpset -> term -> thm option
   15.21    end 
   15.22  =
   15.23  struct
   15.24  
   15.25  (*Store the term t in the table*)
   15.26 -fun update_by_coeff (tab, t) = Termtab.update ((t, ()), tab);
   15.27 +fun update_by_coeff t tab = Termtab.update ((t, ()), tab);
   15.28  
   15.29  (*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
   15.30  fun find_common (terms1,terms2) =
   15.31 -  let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2)
   15.32 +  let val tab2 = fold update_by_coeff terms2 Termtab.empty
   15.33        fun seek [] = raise TERM("find_common", []) 
   15.34  	| seek (u::terms) =
   15.35 -	      if isSome (Termtab.lookup (tab2, u)) then u
   15.36 +	      if Termtab.defined tab2 u then u
   15.37  	      else seek terms
   15.38 -  in  seek terms1 end;
   15.39 +  in seek terms1 end;
   15.40  
   15.41  (*the simplification procedure*)
   15.42 -fun proc sg ss t =
   15.43 +fun proc thy ss t =
   15.44    let
   15.45        val hyps = prems_of_ss ss;
   15.46        (*first freeze any Vars in the term to prevent flex-flex problems*)
   15.47 @@ -63,12 +63,12 @@
   15.48        and terms2' = Data.find_first u terms2
   15.49        and T = Term.fastype_of u
   15.50        val reshape = 
   15.51 -	    Data.prove_conv [Data.norm_tac] sg hyps xs
   15.52 +	    Data.prove_conv [Data.norm_tac ss] thy hyps xs
   15.53  	        (t', 
   15.54  		 Data.mk_bal (Data.mk_sum T (u::terms1'), 
   15.55  		              Data.mk_sum T (u::terms2')))
   15.56    in
   15.57 -      Option.map Data.simplify_meta_eq reshape
   15.58 +      Option.map (Data.simplify_meta_eq ss) reshape
   15.59    end
   15.60    handle TERM _ => NONE
   15.61         | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    16.1 --- a/src/ZF/Datatype.ML	Mon Aug 01 19:20:25 2005 +0200
    16.2 +++ b/src/ZF/Datatype.ML	Mon Aug 01 19:20:26 2005 +0200
    16.3 @@ -62,9 +62,9 @@
    16.4          fold_bal FOLogic.mk_conj
    16.5                   (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    16.6  
    16.7 - val datatype_ss = simpset_of (the_context ());
    16.8 + val datatype_ss = simpset ();
    16.9  
   16.10 - fun proc sg _ old =
   16.11 + fun proc sg ss old =
   16.12     let val _ = if !trace then writeln ("data_free: OLD = " ^ 
   16.13                                         string_of_cterm (cterm_of sg old))
   16.14                 else ()
   16.15 @@ -88,7 +88,7 @@
   16.16                 else ();
   16.17         val goal = Logic.mk_equals (old, new)
   16.18         val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
   16.19 -           simp_tac (datatype_ss addsimps #free_iffs lcon_info) 1)
   16.20 +           simp_tac (Simplifier.inherit_bounds ss datatype_ss addsimps #free_iffs lcon_info) 1)
   16.21           handle ERROR_MESSAGE msg =>
   16.22           (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
   16.23            raise Match)
   16.24 @@ -96,9 +96,8 @@
   16.25     handle Match => NONE;
   16.26  
   16.27  
   16.28 - val conv = 
   16.29 -     Simplifier.simproc (Theory.sign_of (theory "ZF")) "data_free" 
   16.30 -                        ["(x::i) = y"] proc;
   16.31 + val conv = Simplifier.simproc (theory "ZF") "data_free" ["(x::i) = y"] proc;
   16.32 +
   16.33  end;
   16.34  
   16.35  
    17.1 --- a/src/ZF/Induct/Multiset.thy	Mon Aug 01 19:20:25 2005 +0200
    17.2 +++ b/src/ZF/Induct/Multiset.thy	Mon Aug 01 19:20:26 2005 +0200
    17.3 @@ -483,14 +483,12 @@
    17.4  apply (rule int_of_diff, auto)
    17.5  done
    17.6  
    17.7 -(*FIXME: we should not have to rename x to x' below!  There's a bug in the
    17.8 -  interaction between simproc inteq_cancel_numerals and the simplifier.*)
    17.9  lemma setsum_decr2:
   17.10       "Finite(A)
   17.11        ==> \<forall>M. multiset(M) --> (\<forall>a \<in> mset_of(M).
   17.12 -           setsum(%x'. $# mcount(funrestrict(M, mset_of(M)-{a}), x'), A) =
   17.13 -           (if a \<in> A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a
   17.14 -            else setsum(%x'. $# mcount(M, x'), A)))"
   17.15 +           setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A) =
   17.16 +           (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a
   17.17 +            else setsum(%x. $# mcount(M, x), A)))"
   17.18  apply (simp add: multiset_def)
   17.19  apply (erule Finite_induct)
   17.20  apply (auto simp add: multiset_fun_iff mcount_def mset_of_def)
    18.1 --- a/src/ZF/Integ/int_arith.ML	Mon Aug 01 19:20:25 2005 +0200
    18.2 +++ b/src/ZF/Integ/int_arith.ML	Mon Aug 01 19:20:26 2005 +0200
    18.3 @@ -224,19 +224,21 @@
    18.4    val mk_coeff          = mk_coeff
    18.5    val dest_coeff        = dest_coeff 1
    18.6    val find_first_coeff  = find_first_coeff []
    18.7 -  val trans_tac         = ArithData.gen_trans_tac iff_trans
    18.8 +  fun trans_tac _       = ArithData.gen_trans_tac iff_trans
    18.9    val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
   18.10                                      zminus_simps@zadd_ac
   18.11    val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
   18.12    val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
   18.13                                      zadd_ac@zmult_ac@tc_rules@intifys
   18.14 -  val norm_tac          = ALLGOALS (asm_simp_tac norm_tac_ss1)
   18.15 -                          THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
   18.16 -                          THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
   18.17 -  val numeral_simp_tac  =
   18.18 -         ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
   18.19 -         THEN ALLGOALS Asm_simp_tac
   18.20 -  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
   18.21 +  fun norm_tac ss =
   18.22 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
   18.23 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
   18.24 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss3))
   18.25 +  fun numeral_simp_tac ss =
   18.26 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
   18.27 +      add_0s @ bin_simps @ tc_rules @ intifys))
   18.28 +    THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_bounds ss simpset)))
   18.29 +  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   18.30    end;
   18.31  
   18.32  
   18.33 @@ -298,17 +300,19 @@
   18.34    val dest_coeff        = dest_coeff 1
   18.35    val left_distrib      = left_zadd_zmult_distrib RS trans
   18.36    val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   18.37 -  val trans_tac         = ArithData.gen_trans_tac trans
   18.38 +  fun trans_tac _       = ArithData.gen_trans_tac trans
   18.39    val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
   18.40                                      zminus_simps@zadd_ac@intifys
   18.41    val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
   18.42    val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
   18.43                                      zadd_ac@zmult_ac@tc_rules@intifys
   18.44 -  val norm_tac          = ALLGOALS (asm_simp_tac norm_tac_ss1)
   18.45 -                          THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
   18.46 -                          THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
   18.47 -  val numeral_simp_tac  =
   18.48 -         ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
   18.49 +  fun norm_tac ss =
   18.50 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
   18.51 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
   18.52 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss3))
   18.53 +  fun numeral_simp_tac ss =
   18.54 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
   18.55 +      add_0s @ bin_simps @ tc_rules @ intifys))
   18.56    val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
   18.57    end;
   18.58  
   18.59 @@ -335,14 +339,16 @@
   18.60    fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   18.61    val left_distrib      = zmult_assoc RS sym RS trans
   18.62    val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   18.63 -  val trans_tac         = ArithData.gen_trans_tac trans
   18.64 +  fun trans_tac _       = ArithData.gen_trans_tac trans
   18.65    val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps
   18.66    val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
   18.67                                      bin_simps@zmult_ac@tc_rules@intifys
   18.68 -  val norm_tac          = ALLGOALS (asm_simp_tac norm_tac_ss1)
   18.69 -                          THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
   18.70 -  val numeral_simp_tac  =
   18.71 -         ALLGOALS (simp_tac (ZF_ss addsimps bin_simps@tc_rules@intifys))
   18.72 +  fun norm_tac ss =
   18.73 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
   18.74 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
   18.75 +  fun numeral_simp_tac ss =
   18.76 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
   18.77 +      bin_simps @ tc_rules @ intifys))
   18.78    val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s)
   18.79    end;
   18.80  
    19.1 --- a/src/ZF/arith_data.ML	Mon Aug 01 19:20:25 2005 +0200
    19.2 +++ b/src/ZF/arith_data.ML	Mon Aug 01 19:20:26 2005 +0200
    19.3 @@ -14,7 +14,7 @@
    19.4    val gen_trans_tac: thm -> thm option -> tactic
    19.5    val prove_conv: string -> tactic list -> Sign.sg ->
    19.6                    thm list -> string list -> term * term -> thm option
    19.7 -  val simplify_meta_eq: thm list -> thm -> thm
    19.8 +  val simplify_meta_eq: thm list -> simpset -> thm -> thm
    19.9    (*debugging*)
   19.10    structure EqCancelNumeralsData   : CANCEL_NUMERALS_DATA
   19.11    structure LessCancelNumeralsData : CANCEL_NUMERALS_DATA
   19.12 @@ -128,9 +128,9 @@
   19.13                 diff_natify1, diff_natify2];
   19.14  
   19.15  (*Final simplification: cancel + and **)
   19.16 -fun simplify_meta_eq rules =
   19.17 +fun simplify_meta_eq rules ss =
   19.18      mk_meta_eq o
   19.19 -    simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2]
   19.20 +    simplify (Simplifier.inherit_bounds ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
   19.21                       delsimps iff_simps (*these could erase the whole rule!*)
   19.22                       addsimps rules);
   19.23  
   19.24 @@ -143,13 +143,14 @@
   19.25    val mk_coeff          = mk_coeff
   19.26    val dest_coeff        = dest_coeff
   19.27    val find_first_coeff  = find_first_coeff []
   19.28 -  val norm_tac_ss1 = ZF_ss addsimps add_0s@add_succs@mult_1s@add_ac
   19.29 -  val norm_tac_ss2 = ZF_ss addsimps add_0s@mult_1s@
   19.30 -                                    add_ac@mult_ac@tc_rules@natifys
   19.31 -  val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
   19.32 -                 THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
   19.33 -  val numeral_simp_tac_ss = ZF_ss addsimps add_0s@tc_rules@natifys
   19.34 -  val numeral_simp_tac  = ALLGOALS (asm_simp_tac numeral_simp_tac_ss)
   19.35 +  val norm_tac_ss1      = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac
   19.36 +  val norm_tac_ss2      = ZF_ss addsimps add_0s @ mult_1s @ add_ac @ mult_ac @ tc_rules @ natifys
   19.37 +  fun norm_tac ss =
   19.38 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
   19.39 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
   19.40 +  val numeral_simp_tac_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys
   19.41 +  fun numeral_simp_tac ss =
   19.42 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss numeral_simp_tac_ss))
   19.43    val simplify_meta_eq  = simplify_meta_eq final_rules
   19.44    end;
   19.45  
   19.46 @@ -164,7 +165,7 @@
   19.47    val dest_bal = FOLogic.dest_eq
   19.48    val bal_add1 = eq_add_iff RS iff_trans
   19.49    val bal_add2 = eq_add_iff RS iff_trans
   19.50 -  val trans_tac = gen_trans_tac iff_trans
   19.51 +  fun trans_tac _ = gen_trans_tac iff_trans
   19.52    end;
   19.53  
   19.54  structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
   19.55 @@ -177,7 +178,7 @@
   19.56    val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
   19.57    val bal_add1 = less_add_iff RS iff_trans
   19.58    val bal_add2 = less_add_iff RS iff_trans
   19.59 -  val trans_tac = gen_trans_tac iff_trans
   19.60 +  fun trans_tac _ = gen_trans_tac iff_trans
   19.61    end;
   19.62  
   19.63  structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
   19.64 @@ -190,7 +191,7 @@
   19.65    val dest_bal = FOLogic.dest_bin "Arith.diff" iT
   19.66    val bal_add1 = diff_add_eq RS trans
   19.67    val bal_add2 = diff_add_eq RS trans
   19.68 -  val trans_tac = gen_trans_tac trans
   19.69 +  fun trans_tac _ = gen_trans_tac trans
   19.70    end;
   19.71  
   19.72  structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);