src/HOL/Decision_Procs/cooper_tac.ML
changeset 45620 f2a587696afb
parent 44121 44adaa6db327
child 45654 cf10bde35973
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Nov 23 22:07:55 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Nov 23 22:59:39 2011 +0100
     1.3 @@ -86,19 +86,21 @@
     1.4      val simpset0 = HOL_basic_ss
     1.5        addsimps [mod_div_equality', Suc_eq_plus1]
     1.6        addsimps comp_arith
     1.7 -      addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
     1.8 +      |> fold Splitter.add_split
     1.9 +          [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
    1.10      (* Simp rules for changing (n::int) to int n *)
    1.11      val simpset1 = HOL_basic_ss
    1.12        addsimps [@{thm nat_number_of_def}, zdvd_int] @ map (fn r => r RS sym)
    1.13          [@{thm int_int_eq}, @{thm zle_int}, @{thm zless_int}, @{thm zadd_int}, @{thm zmult_int}]
    1.14 -      addsplits [zdiff_int_split]
    1.15 +      |> Splitter.add_split zdiff_int_split
    1.16      (*simp rules for elimination of int n*)
    1.17  
    1.18      val simpset2 = HOL_basic_ss
    1.19 -      addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}]
    1.20 -      addcongs [@{thm conj_le_cong}, @{thm imp_le_cong}]
    1.21 +      addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat},
    1.22 +        @{thm number_of1}, @{thm number_of2}, @{thm int_0}, @{thm int_1}]
    1.23 +      |> fold Simplifier.add_cong [@{thm conj_le_cong}, @{thm imp_le_cong}]
    1.24      (* simp rules for elimination of abs *)
    1.25 -    val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}]
    1.26 +    val simpset3 = HOL_basic_ss |> Splitter.add_split @{thm abs_split}
    1.27      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    1.28      (* Theorem for the nat --> int transformation *)
    1.29      val pre_thm = Seq.hd (EVERY