src/HOL/Tools/SMT/smt_normalize.ML
changeset 54489 03ff4d1e6784
parent 54293 cd896760fa0f
child 54883 dd04a8b654fc
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -526,23 +526,26 @@
     1.4  
     1.5  local
     1.6    (*
     1.7 -    rewrite negative numerals into positive numerals,
     1.8 -    rewrite Numeral0 into 0
     1.9      rewrite Numeral1 into 1
    1.10 +    rewrite - 0 into 0
    1.11    *)
    1.12  
    1.13 -  fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) =
    1.14 -        SMT_Builtin.is_builtin_num ctxt t
    1.15 -    | is_strange_number _ _ = false
    1.16 +  fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) =
    1.17 +        true
    1.18 +    | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) =
    1.19 +        true
    1.20 +    | is_irregular_number _ =
    1.21 +        false;
    1.22  
    1.23 -  val pos_num_ss =
    1.24 +  fun is_strange_number ctxt t = is_irregular_number t andalso SMT_Builtin.is_builtin_num ctxt t;
    1.25 +
    1.26 +  val proper_num_ss =
    1.27      simpset_of (put_simpset HOL_ss @{context}
    1.28 -      addsimps [@{thm Num.numeral_One}]
    1.29 -      addsimps [@{thm Num.neg_numeral_def}])
    1.30 +      addsimps @{thms Num.numeral_One minus_zero})
    1.31  
    1.32    fun norm_num_conv ctxt =
    1.33      SMT_Utils.if_conv (is_strange_number ctxt)
    1.34 -      (Simplifier.rewrite (put_simpset pos_num_ss ctxt)) Conv.no_conv
    1.35 +      (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv
    1.36  in
    1.37  
    1.38  fun normalize_numerals_conv ctxt =