# HG changeset patch # User wenzelm # Date 1322085579 -3600 # Node ID f2a587696afbc7b1254696d6dbbe60605df052b0 # Parent 76c5f277b23466f7ad7ad1cc5c8d1d82621cfd14 modernized some old-style infix operations, which were left over from the time of ML proof scripts; diff -r 76c5f277b234 -r f2a587696afb NEWS --- a/NEWS Wed Nov 23 22:07:55 2011 +0100 +++ b/NEWS Wed Nov 23 22:59:39 2011 +0100 @@ -167,6 +167,15 @@ change of semantics: update is applied to auxiliary local theory context as well. +* Modernized some old-style infix operations: + + addeqcongs ~> Simplifier.add_eqcong + deleqcongs ~> Simplifier.del_eqcong + addcongs ~> Simplifier.add_cong + delcongs ~> Simplifier.del_cong + addsplits ~> Splitter.add_split + delsplits ~> Splitter.del_split + New in Isabelle2011-1 (October 2011) diff -r 76c5f277b234 -r f2a587696afb src/FOL/FOL.thy --- a/src/FOL/FOL.thy Wed Nov 23 22:07:55 2011 +0100 +++ b/src/FOL/FOL.thy Wed Nov 23 22:59:39 2011 +0100 @@ -339,7 +339,7 @@ FOL_basic_ss addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps}) addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}] - addcongs [@{thm imp_cong}]; + |> Simplifier.add_cong @{thm imp_cong}; (*classical simprules too*) val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps}); diff -r 76c5f277b234 -r f2a587696afb src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/FOL/simpdata.ML Wed Nov 23 22:59:39 2011 +0100 @@ -100,8 +100,6 @@ val split_tac = Splitter.split_tac; val split_inside_tac = Splitter.split_inside_tac; val split_asm_tac = Splitter.split_asm_tac; -val op addsplits = Splitter.addsplits; -val op delsplits = Splitter.delsplits; (*** Standard simpsets ***) diff -r 76c5f277b234 -r f2a587696afb src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Nov 23 22:59:39 2011 +0100 @@ -865,7 +865,7 @@ in h end; fun class_field_ss phi = HOL_basic_ss addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}]) - addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}] + |> fold Splitter.add_split [@{thm "abs_split"}, @{thm "split_max"}, @{thm "split_min"}] in Ferrante_Rackoff_Data.funs @{thm "class_dense_linordered_field.ferrack_axiom"} diff -r 76c5f277b234 -r f2a587696afb src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Nov 23 22:59:39 2011 +0100 @@ -86,19 +86,21 @@ val simpset0 = HOL_basic_ss addsimps [mod_div_equality', Suc_eq_plus1] addsimps comp_arith - addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}] + |> fold Splitter.add_split + [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}] (* Simp rules for changing (n::int) to int n *) val simpset1 = HOL_basic_ss addsimps [@{thm nat_number_of_def}, zdvd_int] @ map (fn r => r RS sym) [@{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}] - addsplits [zdiff_int_split] + |> Splitter.add_split zdiff_int_split (*simp rules for elimination of int n*) val simpset2 = HOL_basic_ss - addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}] - addcongs [@{thm conj_le_cong}, @{thm imp_le_cong}] + addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, + @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}] + |> fold Simplifier.add_cong [@{thm conj_le_cong}, @{thm imp_le_cong}] (* simp rules for elimination of abs *) - val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}] + val simpset3 = HOL_basic_ss |> Splitter.add_split @{thm abs_split} val ct = cterm_of thy (HOLogic.mk_Trueprop t) (* Theorem for the nat --> int transformation *) val pre_thm = Seq.hd (EVERY diff -r 76c5f277b234 -r f2a587696afb src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Nov 23 22:59:39 2011 +0100 @@ -108,19 +108,21 @@ val simpset0 = HOL_basic_ss addsimps [mod_div_equality', @{thm Suc_eq_plus1}] addsimps comp_ths - addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}] + |> fold Splitter.add_split + [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, + @{thm "split_min"}, @{thm "split_max"}] (* Simp rules for changing (n::int) to int n *) val simpset1 = HOL_basic_ss addsimps [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, @{thm "zmult_int"}] - addsplits [@{thm "zdiff_int_split"}] + |> Splitter.add_split @{thm "zdiff_int_split"} (*simp rules for elimination of int n*) val simpset2 = HOL_basic_ss addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}] - addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] + |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] (* simp rules for elimination of abs *) val ct = cterm_of thy (HOLogic.mk_Trueprop t) (* Theorem for the nat --> int transformation *) diff -r 76c5f277b234 -r f2a587696afb src/HOL/HOLCF/IOA/ABP/Correctness.thy --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Nov 23 22:59:39 2011 +0100 @@ -84,8 +84,9 @@ "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))" apply simp apply (tactic {* auto_tac (map_simpset (fn _ => - HOL_ss addsplits [@{thm list.split}] - addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *}) + HOL_ss + addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}]) + |> Splitter.add_split @{thm list.split}) @{context}) *}) done text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *} diff -r 76c5f277b234 -r f2a587696afb src/HOL/HOLCF/IOA/NTP/Impl.thy --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Wed Nov 23 22:59:39 2011 +0100 @@ -105,8 +105,10 @@ val ss = @{simpset} addsimps @{thms "transitions"}; val rename_ss = ss addsimps @{thms unfold_renaming}; -val tac = asm_simp_tac (ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}]) -val tac_ren = asm_simp_tac (rename_ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}]) +val tac = + asm_simp_tac (ss |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if}) +val tac_ren = + asm_simp_tac (rename_ss |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if}) *} diff -r 76c5f277b234 -r f2a587696afb src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Wed Nov 23 22:59:39 2011 +0100 @@ -145,9 +145,9 @@ let val ss' = Simplifier.global_context (theory_of_thm st) ss addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms) - delcongs weak_congs - addcongs strong_congs addsimprocs [perm_simproc_fun, perm_simproc_app] + |> fold Simplifier.del_cong weak_congs + |> fold Simplifier.add_cong strong_congs in stac ss' i st end); diff -r 76c5f277b234 -r f2a587696afb src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Statespace/state_fun.ML Wed Nov 23 22:59:39 2011 +0100 @@ -78,7 +78,7 @@ addsimps (@{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms}) addsimprocs [lazy_conj_simproc] - addcongs [@{thm block_conj_cong}]); + |> Simplifier.add_cong @{thm block_conj_cong}); end; @@ -88,8 +88,8 @@ @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel}, @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}]) addsimprocs [lazy_conj_simproc] - addcongs @{thms block_conj_cong} - addSolver StateSpace.distinctNameSolver); + addSolver StateSpace.distinctNameSolver + |> fold Simplifier.add_cong @{thms block_conj_cong}); val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id}; @@ -160,7 +160,7 @@ (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct} @ @{thms char.distinct}) addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc] - addcongs @{thms block_conj_cong}); + |> fold Simplifier.add_cong @{thms block_conj_cong}); in diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 23 22:59:39 2011 +0100 @@ -355,7 +355,7 @@ ((Binding.empty, flat inject), [iff_add]), ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]), - ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]), + ((Binding.empty, weak_case_congs), [Simplifier.cong_add]), ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @ named_rules @ unnamed_rules) |> snd diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Nov 23 22:59:39 2011 +0100 @@ -784,17 +784,17 @@ local val ss1 = comp_ss - addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] - @ map (fn r => r RS sym) + addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] + @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, @{thm "zmult_int"}] - addsplits [@{thm "zdiff_int_split"}] + |> Splitter.add_split @{thm "zdiff_int_split"} val ss2 = HOL_basic_ss addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}] - addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] + |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms} @ map (Thm.symmetric o mk_meta_eq) [@{thm "dvd_eq_mod_eq_0"}, @@ -807,9 +807,11 @@ @{thm "mod_1"}, @{thm "Suc_eq_plus1"}] @ @{thms add_ac} addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}] - val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits - [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, - @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] +val splits_ss = + comp_ss addsimps [@{thm "mod_div_equality'"}] + |> fold Splitter.add_split + [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, + @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] in fun nat_to_int_tac ctxt = simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Wed Nov 23 22:59:39 2011 +0100 @@ -781,8 +781,9 @@ end val ctm = cprop_of th val names = Misc_Legacy.add_term_names (term_of ctm, []) - val th1 = Raw_Simplifier.rewrite_cterm (false,true,false) - (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm + val th1 = + Raw_Simplifier.rewrite_cterm (false, true, false) + (prover names) (ss0 addsimps [cut_lemma'] |> fold Simplifier.add_eqcong congs) ctm val th2 = Thm.equal_elim th1 th in (th2, filter_out restricted (!tc_list)) diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Nov 23 22:59:39 2011 +0100 @@ -431,9 +431,11 @@ (*case_ss causes minimal simplification: bodies of case expressions are not simplified. Otherwise large examples (Red-Black trees) are too slow.*) - val case_ss = Simplifier.global_context theory - (HOL_basic_ss addcongs - (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites) + val case_ss = + Simplifier.global_context theory + (HOL_basic_ss addsimps case_rewrites + |> fold (Simplifier.add_cong o #weak_case_cong o snd) + (Symtab.dest (Datatype.get_all theory))) val corollaries' = map (Simplifier.simplify case_ss) corollaries val extract = Rules.CONTEXT_REWRITE_RULE (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs) diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/arith_data.ML Wed Nov 23 22:59:39 2011 +0100 @@ -114,7 +114,7 @@ in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end; fun simplify_meta_eq rules = - let val ss0 = HOL_basic_ss addeqcongs [@{thm eq_cong2}] addsimps rules + let val ss0 = HOL_basic_ss addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2} in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end end; diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/lin_arith.ML Wed Nov 23 22:59:39 2011 +0100 @@ -807,7 +807,7 @@ addsimprocs [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}] (*abel_cancel helps it work in abstract algebraic domains*) addsimprocs Nat_Arith.nat_cancel_sums_add - addcongs [@{thm if_weak_cong}], + |> Simplifier.add_cong @{thm if_weak_cong}, number_of = number_of}) #> add_discrete_type @{type_name nat}; diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/numeral_simprocs.ML Wed Nov 23 22:59:39 2011 +0100 @@ -687,15 +687,16 @@ in -val field_comp_conv = (Simplifier.rewrite -(HOL_basic_ss addsimps @{thms "semiring_norm"} - addsimps ths addsimps @{thms simp_thms} - addsimprocs field_cancel_numeral_factors - addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, - ord_frac_simproc] - addcongs [@{thm "if_weak_cong"}])) -then_conv (Simplifier.rewrite (HOL_basic_ss addsimps - [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})) +val field_comp_conv = + Simplifier.rewrite + (HOL_basic_ss addsimps @{thms "semiring_norm"} + addsimps ths addsimps @{thms simp_thms} + addsimprocs field_cancel_numeral_factors + addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] + |> Simplifier.add_cong @{thm "if_weak_cong"}) + then_conv + Simplifier.rewrite (HOL_basic_ss addsimps + [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}) end diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/recdef.ML Wed Nov 23 22:59:39 2011 +0100 @@ -167,7 +167,7 @@ | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0)); val {simps, congs, wfs} = get_hints ctxt; val ctxt' = ctxt - |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]); + |> Simplifier.map_simpset (fn ss => ss addsimps simps |> Simplifier.del_cong imp_cong); in (ctxt', rev (map snd congs), wfs) end; fun prepare_hints_i thy () = @@ -175,7 +175,7 @@ val ctxt = Proof_Context.init_global thy; val {simps, congs, wfs} = get_global_hints thy; val ctxt' = ctxt - |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]); + |> Simplifier.map_simpset (fn ss => ss addsimps simps |> Simplifier.del_cong imp_cong); in (ctxt', rev (map snd congs), wfs) end; diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/record.ML Wed Nov 23 22:59:39 2011 +0100 @@ -515,8 +515,8 @@ updates = fold Symtab.update_new upds updates, simpset = Simplifier.addsimps (simpset, simps), defset = Simplifier.addsimps (defset, defs), - foldcong = foldcong addcongs folds, - unfoldcong = unfoldcong addcongs unfolds} + foldcong = foldcong |> fold Simplifier.add_cong folds, + unfoldcong = unfoldcong |> fold Simplifier.add_cong unfolds} equalities extinjects extsplit splits extfields fieldext; in Data.put data thy end; diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/simpdata.ML Wed Nov 23 22:59:39 2011 +0100 @@ -145,9 +145,6 @@ val split_tac = Splitter.split_tac; val split_inside_tac = Splitter.split_inside_tac; -val op addsplits = Splitter.addsplits; -val op delsplits = Splitter.delsplits; - (* integration of simplifier with classical reasoner *) diff -r 76c5f277b234 -r f2a587696afb src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/transfer.ML Wed Nov 23 22:59:39 2011 +0100 @@ -129,8 +129,9 @@ (* transfer *) val (hyps, ctxt5) = ctxt4 |> Assumption.add_assumes (map transform c_vars'); - val simpset = Simplifier.context ctxt5 HOL_ss - addsimps (inj @ embed @ return) addcongs cong; + val simpset = + Simplifier.context ctxt5 HOL_ss addsimps (inj @ embed @ return) + |> fold Simplifier.add_cong cong; val thm' = thm |> Drule.cterm_instantiate (c_vars ~~ c_exprs') |> fold_rev Thm.implies_intr (map cprop_of hyps) diff -r 76c5f277b234 -r f2a587696afb src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Word/Word.thy Wed Nov 23 22:59:39 2011 +0100 @@ -1419,8 +1419,8 @@ fun uint_arith_ss_of ss = ss addsimps @{thms uint_arith_simps} delsimps @{thms word_uint.Rep_inject} - addsplits @{thms split_if_asm} - addcongs @{thms power_False_cong} + |> fold Splitter.add_split @{thms split_if_asm} + |> fold Simplifier.add_cong @{thms power_False_cong} fun uint_arith_tacs ctxt = let @@ -1430,8 +1430,8 @@ in [ clarify_tac ctxt 1, full_simp_tac (uint_arith_ss_of (simpset_of ctxt)) 1, - ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits} - addcongs @{thms power_False_cong})), + ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms uint_splits} + |> fold Simplifier.add_cong @{thms power_False_cong})), rewrite_goals_tac @{thms word_size}, ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN REPEAT (etac conjE n) THEN @@ -1924,8 +1924,8 @@ fun unat_arith_ss_of ss = ss addsimps @{thms unat_arith_simps} delsimps @{thms word_unat.Rep_inject} - addsplits @{thms split_if_asm} - addcongs @{thms power_False_cong} + |> fold Splitter.add_split @{thms split_if_asm} + |> fold Simplifier.add_cong @{thms power_False_cong} fun unat_arith_tacs ctxt = let @@ -1935,8 +1935,8 @@ in [ clarify_tac ctxt 1, full_simp_tac (unat_arith_ss_of (simpset_of ctxt)) 1, - ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits} - addcongs @{thms power_False_cong})), + ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms unat_splits} + |> fold Simplifier.add_cong @{thms power_False_cong})), rewrite_goals_tac @{thms word_size}, ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN REPEAT (etac conjE n) THEN diff -r 76c5f277b234 -r f2a587696afb src/Provers/splitter.ML --- a/src/Provers/splitter.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/Provers/splitter.ML Wed Nov 23 22:59:39 2011 +0100 @@ -7,8 +7,6 @@ where "f args" must be a first-order term without duplicate variables. *) -infix 4 addsplits delsplits; - signature SPLITTER_DATA = sig val thy : theory @@ -34,8 +32,8 @@ val split_tac : thm list -> int -> tactic val split_inside_tac: thm list -> int -> tactic val split_asm_tac : thm list -> int -> tactic - val addsplits : simpset * thm list -> simpset - val delsplits : simpset * thm list -> simpset + val add_split: thm -> simpset -> simpset + val del_split: thm -> simpset -> simpset val split_add: attribute val split_del: attribute val split_modifiers : Method.modifier parser list @@ -419,7 +417,7 @@ (** declare split rules **) -(* addsplits / delsplits *) +(* add_split / del_split *) fun string_of_typ (Type (s, Ts)) = (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s @@ -428,29 +426,23 @@ fun split_name (name, T) asm = "split " ^ (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T; -fun ss addsplits splits = +fun add_split split ss = let - fun addsplit split ss = - let - val (name, asm) = split_thm_info split - val tac = (if asm then split_asm_tac else split_tac) [split] - in Simplifier.addloop (ss, (split_name name asm, tac)) end - in fold addsplit splits ss end; + val (name, asm) = split_thm_info split + val tac = (if asm then split_asm_tac else split_tac) [split] + in Simplifier.addloop (ss, (split_name name asm, tac)) end; -fun ss delsplits splits = - let - fun delsplit split ss = - let val (name, asm) = split_thm_info split - in Simplifier.delloop (ss, split_name name asm) end - in fold delsplit splits ss end; +fun del_split split ss = + let val (name, asm) = split_thm_info split + in Simplifier.delloop (ss, split_name name asm) end; (* attributes *) val splitN = "split"; -val split_add = Simplifier.attrib (op addsplits); -val split_del = Simplifier.attrib (op delsplits); +val split_add = Simplifier.attrib add_split; +val split_del = Simplifier.attrib del_split; (* methods *) diff -r 76c5f277b234 -r f2a587696afb src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/Pure/Isar/local_defs.ML Wed Nov 23 22:59:39 2011 +0100 @@ -217,8 +217,8 @@ fun meta_rewrite_conv ctxt = Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE)) (Raw_Simplifier.context ctxt empty_ss - addeqcongs [Drule.equals_cong] (*protect meta-level equality*) - addsimps (Rules.get (Context.Proof ctxt))); + addsimps (Rules.get (Context.Proof ctxt)) + |> Raw_Simplifier.add_eqcong Drule.equals_cong); (*protect meta-level equality*) val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv; diff -r 76c5f277b234 -r f2a587696afb src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/Pure/raw_simplifier.ML Wed Nov 23 22:59:39 2011 +0100 @@ -5,7 +5,7 @@ *) infix 4 - addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs + addsimps delsimps addsimprocs delsimprocs setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver; @@ -39,10 +39,6 @@ val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc val addsimps: simpset * thm list -> simpset val delsimps: simpset * thm list -> simpset - val addeqcongs: simpset * thm list -> simpset - val deleqcongs: simpset * thm list -> simpset - val addcongs: simpset * thm list -> simpset - val delcongs: simpset * thm list -> simpset val addsimprocs: simpset * simproc list -> simpset val delsimprocs: simpset * simproc list -> simpset val mksimps: simpset -> thm -> thm list @@ -99,6 +95,10 @@ val prems_of: simpset -> thm list val add_simp: thm -> simpset -> simpset val del_simp: thm -> simpset -> simpset + val add_eqcong: thm -> simpset -> simpset + val del_eqcong: thm -> simpset -> simpset + val add_cong: thm -> simpset -> simpset + val del_cong: thm -> simpset -> simpset val solver: simpset -> solver -> int -> tactic val simp_depth_limit_raw: Config.raw val clear_ss: simpset -> simpset @@ -569,7 +569,11 @@ is_full_cong_prems prems (xs ~~ ys) end; -fun add_cong (ss, thm) = ss |> +fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss; + +in + +fun add_eqcong thm ss = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => let val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm)) @@ -586,7 +590,7 @@ val weak' = if is_full_cong thm then weak else a :: weak; in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); -fun del_cong (ss, thm) = ss |> +fun del_eqcong thm ss = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => let val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ => @@ -600,15 +604,8 @@ if is_full_cong thm then NONE else SOME a); in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); -fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss; - -in - -val (op addeqcongs) = Library.foldl add_cong; -val (op deleqcongs) = Library.foldl del_cong; - -fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs; -fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs; +fun add_cong thm ss = add_eqcong (mk_cong ss thm) ss; +fun del_cong thm ss = del_eqcong (mk_cong ss thm) ss; end; @@ -1366,7 +1363,7 @@ in val norm_hhf = gen_norm_hhf hhf_ss; -val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]); +val norm_hhf_protect = gen_norm_hhf (hhf_ss |> add_eqcong Drule.protect_cong); end; diff -r 76c5f277b234 -r f2a587696afb src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/Pure/simplifier.ML Wed Nov 23 22:59:39 2011 +0100 @@ -37,6 +37,10 @@ val prems_of: simpset -> thm list val add_simp: thm -> simpset -> simpset val del_simp: thm -> simpset -> simpset + val add_eqcong: thm -> simpset -> simpset + val del_eqcong: thm -> simpset -> simpset + val add_cong: thm -> simpset -> simpset + val del_cong: thm -> simpset -> simpset val add_prems: thm list -> simpset -> simpset val inherit_context: simpset -> simpset -> simpset val the_context: simpset -> Proof.context @@ -54,7 +58,7 @@ val asm_full_rewrite: simpset -> conv val get_ss: Context.generic -> simpset val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic - val attrib: (simpset * thm list -> simpset) -> attribute + val attrib: (thm -> simpset -> simpset) -> attribute val simp_add: attribute val simp_del: attribute val cong_add: attribute @@ -127,12 +131,12 @@ (* attributes *) -fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th]))); +fun attrib f = Thm.declaration_attribute (map_ss o f); -val simp_add = attrib (op addsimps); -val simp_del = attrib (op delsimps); -val cong_add = attrib (op addcongs); -val cong_del = attrib (op delcongs); +val simp_add = attrib add_simp; +val simp_del = attrib del_simp; +val cong_add = attrib add_cong; +val cong_del = attrib del_cong; (* local simpset *) diff -r 76c5f277b234 -r f2a587696afb src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/Sequents/simpdata.ML Wed Nov 23 22:59:39 2011 +0100 @@ -85,6 +85,6 @@ val LK_ss = LK_basic_ss addsimps LK_simps - addeqcongs [@{thm left_cong}] - addcongs [@{thm imp_cong}]; + |> Simplifier.add_eqcong @{thm left_cong} + |> Simplifier.add_cong @{thm imp_cong}; diff -r 76c5f277b234 -r f2a587696afb src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/Tools/Code/code_simp.ML Wed Nov 23 22:59:39 2011 +0100 @@ -36,7 +36,8 @@ (* build simpset and conversion from program *) fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss = - ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong) + ss addsimps (map_filter (fst o snd)) eqs + |> fold Simplifier.add_cong (the_list some_cong) | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss = ss addsimps (map (fst o snd) classparam_instances) | add_stmt _ ss = ss; diff -r 76c5f277b234 -r f2a587696afb src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/ZF/arith_data.ML Wed Nov 23 22:59:39 2011 +0100 @@ -127,9 +127,10 @@ (*Final simplification: cancel + and **) fun simplify_meta_eq rules = let val ss0 = - FOL_ss addeqcongs [@{thm eq_cong2}, @{thm iff_cong2}] + FOL_ss delsimps @{thms iff_simps} (*these could erase the whole rule!*) addsimps rules + |> fold Simplifier.add_eqcong [@{thm eq_cong2}, @{thm iff_cong2}] in fn ss => mk_meta_eq o simplify (Simplifier.inherit_context ss ss0) end; val final_rules = add_0s @ mult_1s @ [@{thm mult_0}, @{thm mult_0_right}]; diff -r 76c5f277b234 -r f2a587696afb src/ZF/pair.thy --- a/src/ZF/pair.thy Wed Nov 23 22:07:55 2011 +0100 +++ b/src/ZF/pair.thy Wed Nov 23 22:59:39 2011 +0100 @@ -12,7 +12,7 @@ setup {* Simplifier.map_simpset_global (fn ss => ss setmksimps (K (map mk_eq o ZF_atomize o gen_all)) - addcongs [@{thm if_weak_cong}]) + |> Simplifier.add_cong @{thm if_weak_cong}) *} ML {* val ZF_ss = @{simpset} *} diff -r 76c5f277b234 -r f2a587696afb src/ZF/upair.thy --- a/src/ZF/upair.thy Wed Nov 23 22:07:55 2011 +0100 +++ b/src/ZF/upair.thy Wed Nov 23 22:59:39 2011 +0100 @@ -224,8 +224,7 @@ "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))" by (case_tac Q, simp_all) -(** Rewrite rules for boolean case-splitting: faster than - addsplits[split_if] +(** Rewrite rules for boolean case-splitting: faster than split_if [split] **) lemmas split_if_eq1 = split_if [of "%x. x = b"] for b