modernized some old-style infix operations, which were left over from the time of ML proof scripts;
authorwenzelm
Wed Nov 23 22:59:39 2011 +0100 (2011-11-23)
changeset 45620f2a587696afb
parent 45619 76c5f277b234
child 45621 5296df35b656
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
NEWS
src/FOL/FOL.thy
src/FOL/simpdata.ML
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOLCF/IOA/ABP/Correctness.thy
src/HOL/HOLCF/IOA/NTP/Impl.thy
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/record.ML
src/HOL/Tools/simpdata.ML
src/HOL/Tools/transfer.ML
src/HOL/Word/Word.thy
src/Provers/splitter.ML
src/Pure/Isar/local_defs.ML
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
src/Sequents/simpdata.ML
src/Tools/Code/code_simp.ML
src/ZF/arith_data.ML
src/ZF/pair.thy
src/ZF/upair.thy
     1.1 --- a/NEWS	Wed Nov 23 22:07:55 2011 +0100
     1.2 +++ b/NEWS	Wed Nov 23 22:59:39 2011 +0100
     1.3 @@ -167,6 +167,15 @@
     1.4  change of semantics: update is applied to auxiliary local theory
     1.5  context as well.
     1.6  
     1.7 +* Modernized some old-style infix operations:
     1.8 +
     1.9 +  addeqcongs    ~> Simplifier.add_eqcong
    1.10 +  deleqcongs    ~> Simplifier.del_eqcong
    1.11 +  addcongs      ~> Simplifier.add_cong
    1.12 +  delcongs      ~> Simplifier.del_cong
    1.13 +  addsplits     ~> Splitter.add_split
    1.14 +  delsplits     ~> Splitter.del_split
    1.15 +
    1.16  
    1.17  
    1.18  New in Isabelle2011-1 (October 2011)
     2.1 --- a/src/FOL/FOL.thy	Wed Nov 23 22:07:55 2011 +0100
     2.2 +++ b/src/FOL/FOL.thy	Wed Nov 23 22:59:39 2011 +0100
     2.3 @@ -339,7 +339,7 @@
     2.4    FOL_basic_ss
     2.5    addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
     2.6    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
     2.7 -  addcongs [@{thm imp_cong}];
     2.8 +  |> Simplifier.add_cong @{thm imp_cong};
     2.9  
    2.10  (*classical simprules too*)
    2.11  val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
     3.1 --- a/src/FOL/simpdata.ML	Wed Nov 23 22:07:55 2011 +0100
     3.2 +++ b/src/FOL/simpdata.ML	Wed Nov 23 22:59:39 2011 +0100
     3.3 @@ -100,8 +100,6 @@
     3.4  val split_tac = Splitter.split_tac;
     3.5  val split_inside_tac = Splitter.split_inside_tac;
     3.6  val split_asm_tac = Splitter.split_asm_tac;
     3.7 -val op addsplits = Splitter.addsplits;
     3.8 -val op delsplits = Splitter.delsplits;
     3.9  
    3.10  
    3.11  (*** Standard simpsets ***)
     4.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Nov 23 22:07:55 2011 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Nov 23 22:59:39 2011 +0100
     4.3 @@ -865,7 +865,7 @@
     4.4   in h end;
     4.5  fun class_field_ss phi =
     4.6     HOL_basic_ss addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}])
     4.7 -   addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}]
     4.8 +   |> fold Splitter.add_split [@{thm "abs_split"}, @{thm "split_max"}, @{thm "split_min"}]
     4.9  
    4.10  in
    4.11  Ferrante_Rackoff_Data.funs @{thm "class_dense_linordered_field.ferrack_axiom"}
     5.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Nov 23 22:07:55 2011 +0100
     5.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Nov 23 22:59:39 2011 +0100
     5.3 @@ -86,19 +86,21 @@
     5.4      val simpset0 = HOL_basic_ss
     5.5        addsimps [mod_div_equality', Suc_eq_plus1]
     5.6        addsimps comp_arith
     5.7 -      addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
     5.8 +      |> fold Splitter.add_split
     5.9 +          [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
    5.10      (* Simp rules for changing (n::int) to int n *)
    5.11      val simpset1 = HOL_basic_ss
    5.12        addsimps [@{thm nat_number_of_def}, zdvd_int] @ map (fn r => r RS sym)
    5.13          [@{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}]
    5.14 -      addsplits [zdiff_int_split]
    5.15 +      |> Splitter.add_split zdiff_int_split
    5.16      (*simp rules for elimination of int n*)
    5.17  
    5.18      val simpset2 = HOL_basic_ss
    5.19 -      addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}]
    5.20 -      addcongs [@{thm conj_le_cong}, @{thm imp_le_cong}]
    5.21 +      addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat},
    5.22 +        @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}]
    5.23 +      |> fold Simplifier.add_cong [@{thm conj_le_cong}, @{thm imp_le_cong}]
    5.24      (* simp rules for elimination of abs *)
    5.25 -    val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}]
    5.26 +    val simpset3 = HOL_basic_ss |> Splitter.add_split @{thm abs_split}
    5.27      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    5.28      (* Theorem for the nat --> int transformation *)
    5.29      val pre_thm = Seq.hd (EVERY
     6.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Wed Nov 23 22:07:55 2011 +0100
     6.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Nov 23 22:59:39 2011 +0100
     6.3 @@ -108,19 +108,21 @@
     6.4      val simpset0 = HOL_basic_ss
     6.5        addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
     6.6        addsimps comp_ths
     6.7 -      addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}]
     6.8 +      |> fold Splitter.add_split
     6.9 +          [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
    6.10 +            @{thm "split_min"}, @{thm "split_max"}]
    6.11      (* Simp rules for changing (n::int) to int n *)
    6.12      val simpset1 = HOL_basic_ss
    6.13        addsimps [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] @ map (fn r => r RS sym)
    6.14          [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
    6.15           @{thm "zmult_int"}]
    6.16 -      addsplits [@{thm "zdiff_int_split"}]
    6.17 +      |> Splitter.add_split @{thm "zdiff_int_split"}
    6.18      (*simp rules for elimination of int n*)
    6.19  
    6.20      val simpset2 = HOL_basic_ss
    6.21        addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
    6.22                  @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}]
    6.23 -      addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    6.24 +      |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    6.25      (* simp rules for elimination of abs *)
    6.26      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    6.27      (* Theorem for the nat --> int transformation *)
     7.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Nov 23 22:07:55 2011 +0100
     7.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Nov 23 22:59:39 2011 +0100
     7.3 @@ -84,8 +84,9 @@
     7.4      "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
     7.5    apply simp
     7.6    apply (tactic {* auto_tac (map_simpset (fn _ =>
     7.7 -    HOL_ss addsplits [@{thm list.split}]
     7.8 -    addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
     7.9 +    HOL_ss
    7.10 +    addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])
    7.11 +    |> Splitter.add_split @{thm list.split}) @{context}) *})
    7.12    done
    7.13  
    7.14  text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}
     8.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Nov 23 22:07:55 2011 +0100
     8.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Nov 23 22:59:39 2011 +0100
     8.3 @@ -105,8 +105,10 @@
     8.4  val ss = @{simpset} addsimps @{thms "transitions"};
     8.5  val rename_ss = ss addsimps @{thms unfold_renaming};
     8.6  
     8.7 -val tac     = asm_simp_tac (ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
     8.8 -val tac_ren = asm_simp_tac (rename_ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
     8.9 +val tac =
    8.10 +  asm_simp_tac (ss |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
    8.11 +val tac_ren =
    8.12 +  asm_simp_tac (rename_ss |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
    8.13  *}
    8.14  
    8.15  
     9.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Nov 23 22:07:55 2011 +0100
     9.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Nov 23 22:59:39 2011 +0100
     9.3 @@ -145,9 +145,9 @@
     9.4      let
     9.5         val ss' = Simplifier.global_context (theory_of_thm st) ss
     9.6           addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
     9.7 -         delcongs weak_congs
     9.8 -         addcongs strong_congs
     9.9           addsimprocs [perm_simproc_fun, perm_simproc_app]
    9.10 +         |> fold Simplifier.del_cong weak_congs
    9.11 +         |> fold Simplifier.add_cong strong_congs
    9.12      in
    9.13        stac ss' i st
    9.14      end);
    10.1 --- a/src/HOL/Statespace/state_fun.ML	Wed Nov 23 22:07:55 2011 +0100
    10.2 +++ b/src/HOL/Statespace/state_fun.ML	Wed Nov 23 22:59:39 2011 +0100
    10.3 @@ -78,7 +78,7 @@
    10.4    addsimps (@{thms list.inject} @ @{thms char.inject}
    10.5      @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms})
    10.6    addsimprocs [lazy_conj_simproc]
    10.7 -  addcongs [@{thm block_conj_cong}]);
    10.8 +  |> Simplifier.add_cong @{thm block_conj_cong});
    10.9  
   10.10  end;
   10.11  
   10.12 @@ -88,8 +88,8 @@
   10.13      @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
   10.14        @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
   10.15    addsimprocs [lazy_conj_simproc]
   10.16 -  addcongs @{thms block_conj_cong}
   10.17 -  addSolver StateSpace.distinctNameSolver);
   10.18 +  addSolver StateSpace.distinctNameSolver
   10.19 +  |> fold Simplifier.add_cong @{thms block_conj_cong});
   10.20  
   10.21  val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id};
   10.22  
   10.23 @@ -160,7 +160,7 @@
   10.24    (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
   10.25      @ @{thms list.distinct} @ @{thms char.distinct})
   10.26    addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
   10.27 -  addcongs @{thms block_conj_cong});
   10.28 +  |> fold Simplifier.add_cong @{thms block_conj_cong});
   10.29  
   10.30  in
   10.31  
    11.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Nov 23 22:07:55 2011 +0100
    11.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Nov 23 22:59:39 2011 +0100
    11.3 @@ -355,7 +355,7 @@
    11.4          ((Binding.empty, flat inject), [iff_add]),
    11.5          ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
    11.6            [Classical.safe_elim NONE]),
    11.7 -        ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]),
    11.8 +        ((Binding.empty, weak_case_congs), [Simplifier.cong_add]),
    11.9          ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
   11.10            named_rules @ unnamed_rules)
   11.11      |> snd
    12.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Nov 23 22:07:55 2011 +0100
    12.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Nov 23 22:59:39 2011 +0100
    12.3 @@ -784,17 +784,17 @@
    12.4  
    12.5  local
    12.6  val ss1 = comp_ss
    12.7 -  addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
    12.8 -      @ map (fn r => r RS sym) 
    12.9 +  addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}]
   12.10 +      @ map (fn r => r RS sym)
   12.11          [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
   12.12           @{thm "zmult_int"}]
   12.13 -    addsplits [@{thm "zdiff_int_split"}]
   12.14 +  |> Splitter.add_split @{thm "zdiff_int_split"}
   12.15  
   12.16  val ss2 = HOL_basic_ss
   12.17    addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
   12.18              @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
   12.19              @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
   12.20 -  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
   12.21 +  |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
   12.22  val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
   12.23    @ map (Thm.symmetric o mk_meta_eq) 
   12.24      [@{thm "dvd_eq_mod_eq_0"},
   12.25 @@ -807,9 +807,11 @@
   12.26       @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
   12.27    @ @{thms add_ac}
   12.28   addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
   12.29 - val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
   12.30 -     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
   12.31 -      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
   12.32 +val splits_ss =
   12.33 +  comp_ss addsimps [@{thm "mod_div_equality'"}]
   12.34 +  |> fold Splitter.add_split
   12.35 +    [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
   12.36 +     @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
   12.37  in
   12.38  fun nat_to_int_tac ctxt = 
   12.39    simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
    13.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Nov 23 22:07:55 2011 +0100
    13.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Nov 23 22:59:39 2011 +0100
    13.3 @@ -781,8 +781,9 @@
    13.4      end
    13.5      val ctm = cprop_of th
    13.6      val names = Misc_Legacy.add_term_names (term_of ctm, [])
    13.7 -    val th1 = Raw_Simplifier.rewrite_cterm (false,true,false)
    13.8 -      (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
    13.9 +    val th1 =
   13.10 +      Raw_Simplifier.rewrite_cterm (false, true, false)
   13.11 +        (prover names) (ss0 addsimps [cut_lemma'] |> fold Simplifier.add_eqcong congs) ctm
   13.12      val th2 = Thm.equal_elim th1 th
   13.13   in
   13.14   (th2, filter_out restricted (!tc_list))
    14.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Nov 23 22:07:55 2011 +0100
    14.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Nov 23 22:59:39 2011 +0100
    14.3 @@ -431,9 +431,11 @@
    14.4       (*case_ss causes minimal simplification: bodies of case expressions are
    14.5         not simplified. Otherwise large examples (Red-Black trees) are too
    14.6         slow.*)
    14.7 -     val case_ss = Simplifier.global_context theory
    14.8 -       (HOL_basic_ss addcongs
    14.9 -         (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
   14.10 +     val case_ss =
   14.11 +       Simplifier.global_context theory
   14.12 +         (HOL_basic_ss addsimps case_rewrites
   14.13 +          |> fold (Simplifier.add_cong o #weak_case_cong o snd)
   14.14 +              (Symtab.dest (Datatype.get_all theory)))
   14.15       val corollaries' = map (Simplifier.simplify case_ss) corollaries
   14.16       val extract = Rules.CONTEXT_REWRITE_RULE
   14.17                       (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs)
    15.1 --- a/src/HOL/Tools/arith_data.ML	Wed Nov 23 22:07:55 2011 +0100
    15.2 +++ b/src/HOL/Tools/arith_data.ML	Wed Nov 23 22:59:39 2011 +0100
    15.3 @@ -114,7 +114,7 @@
    15.4    in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    15.5  
    15.6  fun simplify_meta_eq rules =
    15.7 -  let val ss0 = HOL_basic_ss addeqcongs [@{thm eq_cong2}] addsimps rules
    15.8 +  let val ss0 = HOL_basic_ss addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2}
    15.9    in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
   15.10  
   15.11  end;
    16.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Nov 23 22:07:55 2011 +0100
    16.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Nov 23 22:59:39 2011 +0100
    16.3 @@ -807,7 +807,7 @@
    16.4        addsimprocs [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}]
    16.5         (*abel_cancel helps it work in abstract algebraic domains*)
    16.6        addsimprocs Nat_Arith.nat_cancel_sums_add
    16.7 -      addcongs [@{thm if_weak_cong}],
    16.8 +      |> Simplifier.add_cong @{thm if_weak_cong},
    16.9      number_of = number_of}) #>
   16.10    add_discrete_type @{type_name nat};
   16.11  
    17.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Nov 23 22:07:55 2011 +0100
    17.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Nov 23 22:59:39 2011 +0100
    17.3 @@ -687,15 +687,16 @@
    17.4  
    17.5  in
    17.6  
    17.7 -val field_comp_conv = (Simplifier.rewrite
    17.8 -(HOL_basic_ss addsimps @{thms "semiring_norm"}
    17.9 -              addsimps ths addsimps @{thms simp_thms}
   17.10 -              addsimprocs field_cancel_numeral_factors
   17.11 -               addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
   17.12 -                            ord_frac_simproc]
   17.13 -                addcongs [@{thm "if_weak_cong"}]))
   17.14 -then_conv (Simplifier.rewrite (HOL_basic_ss addsimps
   17.15 -  [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)}))
   17.16 +val field_comp_conv =
   17.17 +  Simplifier.rewrite
   17.18 +    (HOL_basic_ss addsimps @{thms "semiring_norm"}
   17.19 +      addsimps ths addsimps @{thms simp_thms}
   17.20 +      addsimprocs field_cancel_numeral_factors
   17.21 +      addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc]
   17.22 +      |> Simplifier.add_cong @{thm "if_weak_cong"})
   17.23 +  then_conv
   17.24 +  Simplifier.rewrite (HOL_basic_ss addsimps
   17.25 +    [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})
   17.26  
   17.27  end
   17.28  
    18.1 --- a/src/HOL/Tools/recdef.ML	Wed Nov 23 22:07:55 2011 +0100
    18.2 +++ b/src/HOL/Tools/recdef.ML	Wed Nov 23 22:59:39 2011 +0100
    18.3 @@ -167,7 +167,7 @@
    18.4        | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
    18.5      val {simps, congs, wfs} = get_hints ctxt;
    18.6      val ctxt' = ctxt
    18.7 -      |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
    18.8 +      |> Simplifier.map_simpset (fn ss => ss addsimps simps |> Simplifier.del_cong imp_cong);
    18.9    in (ctxt', rev (map snd congs), wfs) end;
   18.10  
   18.11  fun prepare_hints_i thy () =
   18.12 @@ -175,7 +175,7 @@
   18.13      val ctxt = Proof_Context.init_global thy;
   18.14      val {simps, congs, wfs} = get_global_hints thy;
   18.15      val ctxt' = ctxt
   18.16 -      |> Simplifier.map_simpset (fn ss => ss addsimps simps delcongs [imp_cong]);
   18.17 +      |> Simplifier.map_simpset (fn ss => ss addsimps simps |> Simplifier.del_cong imp_cong);
   18.18    in (ctxt', rev (map snd congs), wfs) end;
   18.19  
   18.20  
    19.1 --- a/src/HOL/Tools/record.ML	Wed Nov 23 22:07:55 2011 +0100
    19.2 +++ b/src/HOL/Tools/record.ML	Wed Nov 23 22:59:39 2011 +0100
    19.3 @@ -515,8 +515,8 @@
    19.4          updates = fold Symtab.update_new upds updates,
    19.5          simpset = Simplifier.addsimps (simpset, simps),
    19.6          defset = Simplifier.addsimps (defset, defs),
    19.7 -        foldcong = foldcong addcongs folds,
    19.8 -        unfoldcong = unfoldcong addcongs unfolds}
    19.9 +        foldcong = foldcong |> fold Simplifier.add_cong folds,
   19.10 +        unfoldcong = unfoldcong |> fold Simplifier.add_cong unfolds}
   19.11         equalities extinjects extsplit splits extfields fieldext;
   19.12    in Data.put data thy end;
   19.13  
    20.1 --- a/src/HOL/Tools/simpdata.ML	Wed Nov 23 22:07:55 2011 +0100
    20.2 +++ b/src/HOL/Tools/simpdata.ML	Wed Nov 23 22:59:39 2011 +0100
    20.3 @@ -145,9 +145,6 @@
    20.4  val split_tac = Splitter.split_tac;
    20.5  val split_inside_tac = Splitter.split_inside_tac;
    20.6  
    20.7 -val op addsplits = Splitter.addsplits;
    20.8 -val op delsplits = Splitter.delsplits;
    20.9 -
   20.10  
   20.11  (* integration of simplifier with classical reasoner *)
   20.12  
    21.1 --- a/src/HOL/Tools/transfer.ML	Wed Nov 23 22:07:55 2011 +0100
    21.2 +++ b/src/HOL/Tools/transfer.ML	Wed Nov 23 22:59:39 2011 +0100
    21.3 @@ -129,8 +129,9 @@
    21.4      (* transfer *)
    21.5      val (hyps, ctxt5) = ctxt4
    21.6        |> Assumption.add_assumes (map transform c_vars');
    21.7 -    val simpset = Simplifier.context ctxt5 HOL_ss
    21.8 -      addsimps (inj @ embed @ return) addcongs cong;
    21.9 +    val simpset =
   21.10 +      Simplifier.context ctxt5 HOL_ss addsimps (inj @ embed @ return)
   21.11 +      |> fold Simplifier.add_cong cong;
   21.12      val thm' = thm
   21.13        |> Drule.cterm_instantiate (c_vars ~~ c_exprs')
   21.14        |> fold_rev Thm.implies_intr (map cprop_of hyps)
    22.1 --- a/src/HOL/Word/Word.thy	Wed Nov 23 22:07:55 2011 +0100
    22.2 +++ b/src/HOL/Word/Word.thy	Wed Nov 23 22:59:39 2011 +0100
    22.3 @@ -1419,8 +1419,8 @@
    22.4  fun uint_arith_ss_of ss = 
    22.5    ss addsimps @{thms uint_arith_simps}
    22.6       delsimps @{thms word_uint.Rep_inject}
    22.7 -     addsplits @{thms split_if_asm} 
    22.8 -     addcongs @{thms power_False_cong}
    22.9 +     |> fold Splitter.add_split @{thms split_if_asm}
   22.10 +     |> fold Simplifier.add_cong @{thms power_False_cong}
   22.11  
   22.12  fun uint_arith_tacs ctxt = 
   22.13    let
   22.14 @@ -1430,8 +1430,8 @@
   22.15    in 
   22.16      [ clarify_tac ctxt 1,
   22.17        full_simp_tac (uint_arith_ss_of (simpset_of ctxt)) 1,
   22.18 -      ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits} 
   22.19 -                                      addcongs @{thms power_False_cong})),
   22.20 +      ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms uint_splits}
   22.21 +                                      |> fold Simplifier.add_cong @{thms power_False_cong})),
   22.22        rewrite_goals_tac @{thms word_size}, 
   22.23        ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
   22.24                           REPEAT (etac conjE n) THEN
   22.25 @@ -1924,8 +1924,8 @@
   22.26  fun unat_arith_ss_of ss = 
   22.27    ss addsimps @{thms unat_arith_simps}
   22.28       delsimps @{thms word_unat.Rep_inject}
   22.29 -     addsplits @{thms split_if_asm}
   22.30 -     addcongs @{thms power_False_cong}
   22.31 +     |> fold Splitter.add_split @{thms split_if_asm}
   22.32 +     |> fold Simplifier.add_cong @{thms power_False_cong}
   22.33  
   22.34  fun unat_arith_tacs ctxt =   
   22.35    let
   22.36 @@ -1935,8 +1935,8 @@
   22.37    in 
   22.38      [ clarify_tac ctxt 1,
   22.39        full_simp_tac (unat_arith_ss_of (simpset_of ctxt)) 1,
   22.40 -      ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits} 
   22.41 -                                       addcongs @{thms power_False_cong})),
   22.42 +      ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms unat_splits}
   22.43 +                                      |> fold Simplifier.add_cong @{thms power_False_cong})),
   22.44        rewrite_goals_tac @{thms word_size}, 
   22.45        ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
   22.46                           REPEAT (etac conjE n) THEN
    23.1 --- a/src/Provers/splitter.ML	Wed Nov 23 22:07:55 2011 +0100
    23.2 +++ b/src/Provers/splitter.ML	Wed Nov 23 22:59:39 2011 +0100
    23.3 @@ -7,8 +7,6 @@
    23.4  where "f args" must be a first-order term without duplicate variables.
    23.5  *)
    23.6  
    23.7 -infix 4 addsplits delsplits;
    23.8 -
    23.9  signature SPLITTER_DATA =
   23.10  sig
   23.11    val thy           : theory
   23.12 @@ -34,8 +32,8 @@
   23.13    val split_tac       : thm list -> int -> tactic
   23.14    val split_inside_tac: thm list -> int -> tactic
   23.15    val split_asm_tac   : thm list -> int -> tactic
   23.16 -  val addsplits       : simpset * thm list -> simpset
   23.17 -  val delsplits       : simpset * thm list -> simpset
   23.18 +  val add_split: thm -> simpset -> simpset
   23.19 +  val del_split: thm -> simpset -> simpset
   23.20    val split_add: attribute
   23.21    val split_del: attribute
   23.22    val split_modifiers : Method.modifier parser list
   23.23 @@ -419,7 +417,7 @@
   23.24  
   23.25  (** declare split rules **)
   23.26  
   23.27 -(* addsplits / delsplits *)
   23.28 +(* add_split / del_split *)
   23.29  
   23.30  fun string_of_typ (Type (s, Ts)) =
   23.31        (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s
   23.32 @@ -428,29 +426,23 @@
   23.33  fun split_name (name, T) asm = "split " ^
   23.34    (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
   23.35  
   23.36 -fun ss addsplits splits =
   23.37 +fun add_split split ss =
   23.38    let
   23.39 -    fun addsplit split ss =
   23.40 -      let
   23.41 -        val (name, asm) = split_thm_info split
   23.42 -        val tac = (if asm then split_asm_tac else split_tac) [split]
   23.43 -      in Simplifier.addloop (ss, (split_name name asm, tac)) end
   23.44 -  in fold addsplit splits ss end;
   23.45 +    val (name, asm) = split_thm_info split
   23.46 +    val tac = (if asm then split_asm_tac else split_tac) [split]
   23.47 +  in Simplifier.addloop (ss, (split_name name asm, tac)) end;
   23.48  
   23.49 -fun ss delsplits splits =
   23.50 -  let
   23.51 -    fun delsplit split ss =
   23.52 -      let val (name, asm) = split_thm_info split
   23.53 -      in Simplifier.delloop (ss, split_name name asm) end
   23.54 -  in fold delsplit splits ss end;
   23.55 +fun del_split split ss =
   23.56 +  let val (name, asm) = split_thm_info split
   23.57 +  in Simplifier.delloop (ss, split_name name asm) end;
   23.58  
   23.59  
   23.60  (* attributes *)
   23.61  
   23.62  val splitN = "split";
   23.63  
   23.64 -val split_add = Simplifier.attrib (op addsplits);
   23.65 -val split_del = Simplifier.attrib (op delsplits);
   23.66 +val split_add = Simplifier.attrib add_split;
   23.67 +val split_del = Simplifier.attrib del_split;
   23.68  
   23.69  
   23.70  (* methods *)
    24.1 --- a/src/Pure/Isar/local_defs.ML	Wed Nov 23 22:07:55 2011 +0100
    24.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Nov 23 22:59:39 2011 +0100
    24.3 @@ -217,8 +217,8 @@
    24.4  fun meta_rewrite_conv ctxt =
    24.5    Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
    24.6      (Raw_Simplifier.context ctxt empty_ss
    24.7 -      addeqcongs [Drule.equals_cong]    (*protect meta-level equality*)
    24.8 -      addsimps (Rules.get (Context.Proof ctxt)));
    24.9 +      addsimps (Rules.get (Context.Proof ctxt))
   24.10 +      |> Raw_Simplifier.add_eqcong Drule.equals_cong);    (*protect meta-level equality*)
   24.11  
   24.12  val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;
   24.13  
    25.1 --- a/src/Pure/raw_simplifier.ML	Wed Nov 23 22:07:55 2011 +0100
    25.2 +++ b/src/Pure/raw_simplifier.ML	Wed Nov 23 22:59:39 2011 +0100
    25.3 @@ -5,7 +5,7 @@
    25.4  *)
    25.5  
    25.6  infix 4
    25.7 -  addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
    25.8 +  addsimps delsimps addsimprocs delsimprocs
    25.9    setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
   25.10    setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
   25.11  
   25.12 @@ -39,10 +39,6 @@
   25.13    val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
   25.14    val addsimps: simpset * thm list -> simpset
   25.15    val delsimps: simpset * thm list -> simpset
   25.16 -  val addeqcongs: simpset * thm list -> simpset
   25.17 -  val deleqcongs: simpset * thm list -> simpset
   25.18 -  val addcongs: simpset * thm list -> simpset
   25.19 -  val delcongs: simpset * thm list -> simpset
   25.20    val addsimprocs: simpset * simproc list -> simpset
   25.21    val delsimprocs: simpset * simproc list -> simpset
   25.22    val mksimps: simpset -> thm -> thm list
   25.23 @@ -99,6 +95,10 @@
   25.24    val prems_of: simpset -> thm list
   25.25    val add_simp: thm -> simpset -> simpset
   25.26    val del_simp: thm -> simpset -> simpset
   25.27 +  val add_eqcong: thm -> simpset -> simpset
   25.28 +  val del_eqcong: thm -> simpset -> simpset
   25.29 +  val add_cong: thm -> simpset -> simpset
   25.30 +  val del_cong: thm -> simpset -> simpset
   25.31    val solver: simpset -> solver -> int -> tactic
   25.32    val simp_depth_limit_raw: Config.raw
   25.33    val clear_ss: simpset -> simpset
   25.34 @@ -569,7 +569,11 @@
   25.35      is_full_cong_prems prems (xs ~~ ys)
   25.36    end;
   25.37  
   25.38 -fun add_cong (ss, thm) = ss |>
   25.39 +fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
   25.40 +
   25.41 +in
   25.42 +
   25.43 +fun add_eqcong thm ss = ss |>
   25.44    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   25.45      let
   25.46        val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
   25.47 @@ -586,7 +590,7 @@
   25.48        val weak' = if is_full_cong thm then weak else a :: weak;
   25.49      in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   25.50  
   25.51 -fun del_cong (ss, thm) = ss |>
   25.52 +fun del_eqcong thm ss = ss |>
   25.53    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   25.54      let
   25.55        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
   25.56 @@ -600,15 +604,8 @@
   25.57          if is_full_cong thm then NONE else SOME a);
   25.58      in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   25.59  
   25.60 -fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
   25.61 -
   25.62 -in
   25.63 -
   25.64 -val (op addeqcongs) = Library.foldl add_cong;
   25.65 -val (op deleqcongs) = Library.foldl del_cong;
   25.66 -
   25.67 -fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
   25.68 -fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
   25.69 +fun add_cong thm ss = add_eqcong (mk_cong ss thm) ss;
   25.70 +fun del_cong thm ss = del_eqcong (mk_cong ss thm) ss;
   25.71  
   25.72  end;
   25.73  
   25.74 @@ -1366,7 +1363,7 @@
   25.75  in
   25.76  
   25.77  val norm_hhf = gen_norm_hhf hhf_ss;
   25.78 -val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
   25.79 +val norm_hhf_protect = gen_norm_hhf (hhf_ss |> add_eqcong Drule.protect_cong);
   25.80  
   25.81  end;
   25.82  
    26.1 --- a/src/Pure/simplifier.ML	Wed Nov 23 22:07:55 2011 +0100
    26.2 +++ b/src/Pure/simplifier.ML	Wed Nov 23 22:59:39 2011 +0100
    26.3 @@ -37,6 +37,10 @@
    26.4    val prems_of: simpset -> thm list
    26.5    val add_simp: thm -> simpset -> simpset
    26.6    val del_simp: thm -> simpset -> simpset
    26.7 +  val add_eqcong: thm -> simpset -> simpset
    26.8 +  val del_eqcong: thm -> simpset -> simpset
    26.9 +  val add_cong: thm -> simpset -> simpset
   26.10 +  val del_cong: thm -> simpset -> simpset
   26.11    val add_prems: thm list -> simpset -> simpset
   26.12    val inherit_context: simpset -> simpset -> simpset
   26.13    val the_context: simpset -> Proof.context
   26.14 @@ -54,7 +58,7 @@
   26.15    val asm_full_rewrite: simpset -> conv
   26.16    val get_ss: Context.generic -> simpset
   26.17    val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
   26.18 -  val attrib: (simpset * thm list -> simpset) -> attribute
   26.19 +  val attrib: (thm -> simpset -> simpset) -> attribute
   26.20    val simp_add: attribute
   26.21    val simp_del: attribute
   26.22    val cong_add: attribute
   26.23 @@ -127,12 +131,12 @@
   26.24  
   26.25  (* attributes *)
   26.26  
   26.27 -fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
   26.28 +fun attrib f = Thm.declaration_attribute (map_ss o f);
   26.29  
   26.30 -val simp_add = attrib (op addsimps);
   26.31 -val simp_del = attrib (op delsimps);
   26.32 -val cong_add = attrib (op addcongs);
   26.33 -val cong_del = attrib (op delcongs);
   26.34 +val simp_add = attrib add_simp;
   26.35 +val simp_del = attrib del_simp;
   26.36 +val cong_add = attrib add_cong;
   26.37 +val cong_del = attrib del_cong;
   26.38  
   26.39  
   26.40  (* local simpset *)
    27.1 --- a/src/Sequents/simpdata.ML	Wed Nov 23 22:07:55 2011 +0100
    27.2 +++ b/src/Sequents/simpdata.ML	Wed Nov 23 22:59:39 2011 +0100
    27.3 @@ -85,6 +85,6 @@
    27.4  
    27.5  val LK_ss =
    27.6    LK_basic_ss addsimps LK_simps
    27.7 -  addeqcongs [@{thm left_cong}]
    27.8 -  addcongs [@{thm imp_cong}];
    27.9 +  |> Simplifier.add_eqcong @{thm left_cong}
   27.10 +  |> Simplifier.add_cong @{thm imp_cong};
   27.11  
    28.1 --- a/src/Tools/Code/code_simp.ML	Wed Nov 23 22:07:55 2011 +0100
    28.2 +++ b/src/Tools/Code/code_simp.ML	Wed Nov 23 22:59:39 2011 +0100
    28.3 @@ -36,7 +36,8 @@
    28.4  (* build simpset and conversion from program *)
    28.5  
    28.6  fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
    28.7 -      ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong)
    28.8 +      ss addsimps (map_filter (fst o snd)) eqs
    28.9 +      |> fold Simplifier.add_cong (the_list some_cong)
   28.10    | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
   28.11        ss addsimps (map (fst o snd) classparam_instances)
   28.12    | add_stmt _ ss = ss;
    29.1 --- a/src/ZF/arith_data.ML	Wed Nov 23 22:07:55 2011 +0100
    29.2 +++ b/src/ZF/arith_data.ML	Wed Nov 23 22:59:39 2011 +0100
    29.3 @@ -127,9 +127,10 @@
    29.4  (*Final simplification: cancel + and **)
    29.5  fun simplify_meta_eq rules =
    29.6    let val ss0 =
    29.7 -    FOL_ss addeqcongs [@{thm eq_cong2}, @{thm iff_cong2}]
    29.8 +    FOL_ss
    29.9        delsimps @{thms iff_simps} (*these could erase the whole rule!*)
   29.10        addsimps rules
   29.11 +      |> fold Simplifier.add_eqcong [@{thm eq_cong2}, @{thm iff_cong2}]
   29.12    in fn ss => mk_meta_eq o simplify (Simplifier.inherit_context ss ss0) end;
   29.13  
   29.14  val final_rules = add_0s @ mult_1s @ [@{thm mult_0}, @{thm mult_0_right}];
    30.1 --- a/src/ZF/pair.thy	Wed Nov 23 22:07:55 2011 +0100
    30.2 +++ b/src/ZF/pair.thy	Wed Nov 23 22:59:39 2011 +0100
    30.3 @@ -12,7 +12,7 @@
    30.4  setup {*
    30.5    Simplifier.map_simpset_global (fn ss =>
    30.6      ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    30.7 -    addcongs [@{thm if_weak_cong}])
    30.8 +    |> Simplifier.add_cong @{thm if_weak_cong})
    30.9  *}
   30.10  
   30.11  ML {* val ZF_ss = @{simpset} *}
    31.1 --- a/src/ZF/upair.thy	Wed Nov 23 22:07:55 2011 +0100
    31.2 +++ b/src/ZF/upair.thy	Wed Nov 23 22:59:39 2011 +0100
    31.3 @@ -224,8 +224,7 @@
    31.4       "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
    31.5  by (case_tac Q, simp_all)
    31.6  
    31.7 -(** Rewrite rules for boolean case-splitting: faster than 
    31.8 -        addsplits[split_if]
    31.9 +(** Rewrite rules for boolean case-splitting: faster than split_if [split]
   31.10  **)
   31.11  
   31.12  lemmas split_if_eq1 = split_if [of "%x. x = b"] for b