modernized some old-style infix operations, which were left over from the time of ML proof scripts;
--- 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)
--- 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});
--- 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 ***)
--- 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"}
--- 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
--- 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 *)
--- 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. *}
--- 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})
*}
--- 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);
--- 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
--- 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
--- 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
--- 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))
--- 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)
--- 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;
--- 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};
--- 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
--- 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;
--- 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;
--- 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 *)
--- 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)
--- 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
--- 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 *)
--- 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;
--- 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;
--- 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 *)
--- 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};
--- 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;
--- 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}];
--- 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} *}
--- 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