change_claset/simpset;
authorwenzelm
Mon Oct 17 23:10:10 2005 +0200 (2005-10-17)
changeset 17875d81094515061
parent 17874 8be65cf94d2e
child 17876 b9c92f384109
change_claset/simpset;
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
src/FOL/simpdata.ML
src/HOL/Integ/int_arith1.ML
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/record_package.ML
src/HOL/arith_data.ML
src/HOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Mon Oct 17 19:19:29 2005 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Mon Oct 17 23:10:10 2005 +0200
     1.3 @@ -339,7 +339,7 @@
     1.4  
     1.5  fun unfold_tac ss ths =
     1.6    ALLGOALS (full_simp_tac
     1.7 -    (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
     1.8 +    (Simplifier.inherit_context ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
     1.9  
    1.10  
    1.11  (*intuitionistic simprules only*)
    1.12 @@ -360,7 +360,7 @@
    1.13  (*classical simprules too*)
    1.14  val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
    1.15  
    1.16 -val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)];
    1.17 +val simpsetup = [fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)];
    1.18  
    1.19  
    1.20  (*** integration of simplifier with classical reasoner ***)
     2.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Oct 17 19:19:29 2005 +0200
     2.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon Oct 17 23:10:10 2005 +0200
     2.3 @@ -309,7 +309,7 @@
     2.4    | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
     2.5  
     2.6  fun simplify_meta_eq rules ss =
     2.7 -    simplify (Simplifier.inherit_bounds ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
     2.8 +    simplify (Simplifier.inherit_context ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
     2.9      o mk_meta_eq;
    2.10  
    2.11  structure CancelNumeralsCommon =
    2.12 @@ -321,14 +321,14 @@
    2.13    val find_first_coeff  = find_first_coeff []
    2.14    val trans_tac         = fn _ => trans_tac
    2.15    fun norm_tac ss =
    2.16 -    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    2.17 +    let val num_ss' = Simplifier.inherit_context ss num_ss in
    2.18        ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    2.19                                           diff_simps @ minus_simps @ add_ac))
    2.20        THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
    2.21        THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
    2.22      end
    2.23    fun numeral_simp_tac ss =
    2.24 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    2.25 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    2.26    val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
    2.27    end;
    2.28  
    2.29 @@ -399,14 +399,14 @@
    2.30    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    2.31    val trans_tac         = fn _ => trans_tac
    2.32    fun norm_tac ss =
    2.33 -    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    2.34 +    let val num_ss' = Simplifier.inherit_context ss num_ss in
    2.35        ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    2.36                                            diff_simps @ minus_simps @ add_ac))
    2.37        THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
    2.38        THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
    2.39      end
    2.40    fun numeral_simp_tac ss =
    2.41 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    2.42 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    2.43    val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
    2.44    end;
    2.45  
     3.1 --- a/src/HOL/Product_Type.thy	Mon Oct 17 19:19:29 2005 +0200
     3.2 +++ b/src/HOL/Product_Type.thy	Mon Oct 17 23:10:10 2005 +0200
     3.3 @@ -320,7 +320,7 @@
     3.4     if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
     3.5    end;
     3.6  
     3.7 -claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac);
     3.8 +change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
     3.9  *}
    3.10  
    3.11  lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))"
    3.12 @@ -415,7 +415,7 @@
    3.13    |   split_pat tp i _ = NONE;
    3.14    fun metaeq thy ss lhs rhs = mk_meta_eq (Tactic.prove thy [] []
    3.15          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
    3.16 -        (K (simp_tac (Simplifier.inherit_bounds ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
    3.17 +        (K (simp_tac (Simplifier.inherit_context ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
    3.18  
    3.19    fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
    3.20    |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
    3.21 @@ -529,7 +529,7 @@
    3.22  end;
    3.23  (* This prevents applications of splitE for already splitted arguments leading
    3.24     to quite time-consuming computations (in particular for nested tuples) *)
    3.25 -claset_ref() := claset() addSbefore ("split_conv_tac", split_conv_tac);
    3.26 +change_claset (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac));
    3.27  *}
    3.28  
    3.29  lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
     4.1 --- a/src/HOL/Set.thy	Mon Oct 17 19:19:29 2005 +0200
     4.2 +++ b/src/HOL/Set.thy	Mon Oct 17 23:10:10 2005 +0200
     4.3 @@ -380,7 +380,7 @@
     4.4  *}
     4.5  
     4.6  ML_setup {*
     4.7 -  claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1);
     4.8 +  change_claset (fn cs => cs addbefore ("bspec", datac (thm "bspec") 1));
     4.9  *}
    4.10  
    4.11  lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
    4.12 @@ -431,7 +431,7 @@
    4.13  
    4.14      val simpset = Simplifier.clear_ss HOL_basic_ss;
    4.15      fun unfold_tac ss th =
    4.16 -      ALLGOALS (full_simp_tac (Simplifier.inherit_bounds ss simpset addsimps [th]));
    4.17 +      ALLGOALS (full_simp_tac (Simplifier.inherit_context ss simpset addsimps [th]));
    4.18  
    4.19      fun prove_bex_tac ss =
    4.20        unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac;
    4.21 @@ -977,7 +977,7 @@
    4.22  
    4.23  ML_setup {*
    4.24    val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs;
    4.25 -  simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);
    4.26 +  change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
    4.27  *}
    4.28  
    4.29  declare subset_UNIV [simp] subset_refl [simp]
     5.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Oct 17 19:19:29 2005 +0200
     5.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Oct 17 23:10:10 2005 +0200
     5.3 @@ -352,7 +352,7 @@
     5.4                                      atac 2, resolve_tac thms 1, etac FalseE 1])))
     5.5                                 | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
     5.6                                     (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
     5.7 -                                    full_simp_tac (Simplifier.inherit_bounds ss simpset) 1,
     5.8 +                                    full_simp_tac (Simplifier.inherit_context ss simpset) 1,
     5.9                                      REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    5.10                                      eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    5.11                                      etac FalseE 1]))))
    5.12 @@ -372,7 +372,7 @@
    5.13  
    5.14  val simproc_setup =
    5.15    [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
    5.16 -   fn thy => (simpset_ref_of thy := simpset_of thy addsimprocs [distinct_simproc]; thy)];
    5.17 +   fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy)];
    5.18  
    5.19  
    5.20  (**** translation rules for case ****)
     6.1 --- a/src/HOL/Tools/record_package.ML	Mon Oct 17 19:19:29 2005 +0200
     6.2 +++ b/src/HOL/Tools/record_package.ML	Mon Oct 17 23:10:10 2005 +0200
     6.3 @@ -826,7 +826,7 @@
     6.4                   | NONE => extsplits)
     6.5    in
     6.6      quick_and_dirty_prove true sg [] prop
     6.7 -      (fn _ => simp_tac (Simplifier.inherit_bounds ss simpset addsimps thms) 1)
     6.8 +      (fn _ => simp_tac (Simplifier.inherit_context ss simpset addsimps thms) 1)
     6.9    end;
    6.10  
    6.11  
    6.12 @@ -1069,7 +1069,7 @@
    6.13         let
    6.14           fun prove prop =
    6.15             quick_and_dirty_prove true sg [] prop
    6.16 -             (fn _ => simp_tac (Simplifier.inherit_bounds ss (get_simpset sg)
    6.17 +             (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset sg)
    6.18                 addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
    6.19  
    6.20           fun mkeq (lr,Teq,(sel,Tsel),x) i =
    6.21 @@ -2106,8 +2106,8 @@
    6.22   [RecordsData.init,
    6.23    Theory.add_trfuns ([], parse_translation, [], []),
    6.24    Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),
    6.25 -  Simplifier.change_simpset_of Simplifier.addsimprocs
    6.26 -    [record_simproc, record_upd_simproc, record_eq_simproc]];
    6.27 +  (fn thy => (Simplifier.change_simpset_of thy
    6.28 +    (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy))];
    6.29  
    6.30  (* outer syntax *)
    6.31  
     7.1 --- a/src/HOL/arith_data.ML	Mon Oct 17 19:19:29 2005 +0200
     7.2 +++ b/src/HOL/arith_data.ML	Mon Oct 17 23:10:10 2005 +0200
     7.3 @@ -64,7 +64,7 @@
     7.4  (* rewriting *)
     7.5  
     7.6  fun simp_all_tac rules ss =
     7.7 -  ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rules));
     7.8 +  ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rules));
     7.9  
    7.10  val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
    7.11  val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
    7.12 @@ -394,7 +394,7 @@
    7.13  val add_rules =
    7.14   [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
    7.15    One_nat_def,isolateSuc,
    7.16 -  order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, 
    7.17 +  order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one,
    7.18    zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
    7.19  
    7.20  val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
    7.21 @@ -431,7 +431,7 @@
    7.22      neqE = [linorder_neqE_nat,
    7.23        get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
    7.24      simpset = HOL_basic_ss addsimps add_rules
    7.25 -                   addsimprocs [ab_group_add_cancel.sum_conv, 
    7.26 +                   addsimprocs [ab_group_add_cancel.sum_conv,
    7.27                                  ab_group_add_cancel.rel_conv]
    7.28                     (*abel_cancel helps it work in abstract algebraic domains*)
    7.29                     addsimprocs nat_cancel_sums_add}),
    7.30 @@ -538,15 +538,14 @@
    7.31  (* theory setup *)
    7.32  
    7.33  val arith_setup =
    7.34 - [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
    7.35    init_lin_arith_data @
    7.36 -  [Simplifier.change_simpset_of (op addSolver)
    7.37 -   (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac),
    7.38 -  Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
    7.39 +  [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
    7.40 +    addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
    7.41 +    addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy),
    7.42    Method.add_methods
    7.43 -      [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
    7.44 -	"decide linear arithmethic")],
    7.45 +    [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
    7.46 +      "decide linear arithmethic")],
    7.47    Attrib.add_attributes [("arith_split",
    7.48 -    (Attrib.no_args arith_split_add, 
    7.49 +    (Attrib.no_args arith_split_add,
    7.50       Attrib.no_args Attrib.undef_local_attribute),
    7.51      "declaration of split rules for arithmetic procedure")]];
     8.1 --- a/src/HOL/simpdata.ML	Mon Oct 17 19:19:29 2005 +0200
     8.2 +++ b/src/HOL/simpdata.ML	Mon Oct 17 23:10:10 2005 +0200
     8.3 @@ -350,7 +350,7 @@
     8.4  
     8.5  fun unfold_tac ss ths =
     8.6    ALLGOALS (full_simp_tac
     8.7 -    (Simplifier.inherit_bounds ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
     8.8 +    (Simplifier.inherit_context ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
     8.9  
    8.10  (*In general it seems wrong to add distributive laws by default: they
    8.11    might cause exponential blow-up.  But imp_disjL has been in for a while
    8.12 @@ -424,7 +424,7 @@
    8.13  
    8.14  (* default simpset *)
    8.15  val simpsetup =
    8.16 -  [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
    8.17 +  [fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)];
    8.18  
    8.19  
    8.20  (*** integration of simplifier with classical reasoner ***)