src/HOL/Word/Word.thy
changeset 51717 9e7d1c139569
parent 51375 d9e62d9c98de
child 53062 3af1a6020014
     1.1 --- a/src/HOL/Word/Word.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -1447,8 +1447,8 @@
     1.4  
     1.5  (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
     1.6  ML {*
     1.7 -fun uint_arith_ss_of ss = 
     1.8 -  ss addsimps @{thms uint_arith_simps}
     1.9 +fun uint_arith_simpset ctxt = 
    1.10 +  ctxt addsimps @{thms uint_arith_simps}
    1.11       delsimps @{thms word_uint.Rep_inject}
    1.12       |> fold Splitter.add_split @{thms split_if_asm}
    1.13       |> fold Simplifier.add_cong @{thms power_False_cong}
    1.14 @@ -1460,9 +1460,11 @@
    1.15          handle Cooper.COOPER _ => Seq.empty;
    1.16    in 
    1.17      [ clarify_tac ctxt 1,
    1.18 -      full_simp_tac (uint_arith_ss_of (simpset_of ctxt)) 1,
    1.19 -      ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms uint_splits}
    1.20 -                                      |> fold Simplifier.add_cong @{thms power_False_cong})),
    1.21 +      full_simp_tac (uint_arith_simpset ctxt) 1,
    1.22 +      ALLGOALS (full_simp_tac
    1.23 +        (put_simpset HOL_ss ctxt
    1.24 +          |> fold Splitter.add_split @{thms uint_splits}
    1.25 +          |> fold Simplifier.add_cong @{thms power_False_cong})),
    1.26        rewrite_goals_tac @{thms word_size}, 
    1.27        ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
    1.28                           REPEAT (etac conjE n) THEN
    1.29 @@ -1946,8 +1948,8 @@
    1.30  (* unat_arith_tac: tactic to reduce word arithmetic to nat, 
    1.31     try to solve via arith *)
    1.32  ML {*
    1.33 -fun unat_arith_ss_of ss = 
    1.34 -  ss addsimps @{thms unat_arith_simps}
    1.35 +fun unat_arith_simpset ctxt = 
    1.36 +  ctxt addsimps @{thms unat_arith_simps}
    1.37       delsimps @{thms word_unat.Rep_inject}
    1.38       |> fold Splitter.add_split @{thms split_if_asm}
    1.39       |> fold Simplifier.add_cong @{thms power_False_cong}
    1.40 @@ -1959,9 +1961,11 @@
    1.41          handle Cooper.COOPER _ => Seq.empty;
    1.42    in 
    1.43      [ clarify_tac ctxt 1,
    1.44 -      full_simp_tac (unat_arith_ss_of (simpset_of ctxt)) 1,
    1.45 -      ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms unat_splits}
    1.46 -                                      |> fold Simplifier.add_cong @{thms power_False_cong})),
    1.47 +      full_simp_tac (unat_arith_simpset ctxt) 1,
    1.48 +      ALLGOALS (full_simp_tac
    1.49 +        (put_simpset HOL_ss ctxt
    1.50 +          |> fold Splitter.add_split @{thms unat_splits}
    1.51 +          |> fold Simplifier.add_cong @{thms power_False_cong})),
    1.52        rewrite_goals_tac @{thms word_size}, 
    1.53        ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
    1.54                           REPEAT (etac conjE n) THEN