src/HOL/Library/Word.thy
changeset 72954 eb1e5c4f70cd
parent 72830 ec0d3a62bb3b
child 73535 0f33c7031ec9
equal deleted inserted replaced
72953:90ada01470cb 72954:eb1e5c4f70cd
  3225   unat_sub_if' unat_plus_if' unat_div unat_mod
  3225   unat_sub_if' unat_plus_if' unat_div unat_mod
  3226 
  3226 
  3227 \<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
  3227 \<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
  3228 ML \<open>
  3228 ML \<open>
  3229 val unat_arith_simpset =
  3229 val unat_arith_simpset =
  3230   @{context}
  3230   @{context} (* TODO: completely explicitly determined simpset *)
       
  3231   |> fold Simplifier.del_simp @{thms unsigned_of_nat unsigned_of_int}
  3231   |> fold Simplifier.add_simp @{thms unat_arith_simps}
  3232   |> fold Simplifier.add_simp @{thms unat_arith_simps}
  3232   |> fold Splitter.add_split @{thms if_split_asm}
  3233   |> fold Splitter.add_split @{thms if_split_asm}
  3233   |> fold Simplifier.add_cong @{thms power_False_cong}
  3234   |> fold Simplifier.add_cong @{thms power_False_cong}
  3234   |> simpset_of
  3235   |> simpset_of
  3235 
  3236