src/HOL/Tools/SMT/smt_normalize.ML
changeset 47108 2a1953f0d20d
parent 46497 89ccf66aa73d
child 47155 ade3fc826af3
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -451,7 +451,7 @@
     1.4  
     1.5    val nat_ops = simple_nat_ops @ mult_nat_ops
     1.6  
     1.7 -  val nat_consts = nat_ops @ [@{const number_of (nat)},
     1.8 +  val nat_consts = nat_ops @ [@{const numeral (nat)},
     1.9      @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
    1.10  
    1.11    val nat_int_coercions = [@{const of_nat (int)}, @{const nat}]
    1.12 @@ -466,7 +466,7 @@
    1.13    val expands = map mk_meta_eq @{lemma
    1.14      "0 = nat 0"
    1.15      "1 = nat 1"
    1.16 -    "(number_of :: int => nat) = (%i. nat (number_of i))"
    1.17 +    "(numeral :: num => nat) = (%i. nat (numeral i))"
    1.18      "op < = (%a b. int a < int b)"
    1.19      "op <= = (%a b. int a <= int b)"
    1.20      "Suc = (%a. nat (int a + 1))"
    1.21 @@ -493,8 +493,7 @@
    1.22      let
    1.23        val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
    1.24        val ss = HOL_ss
    1.25 -        addsimps [@{thm Nat_Numeral.int_nat_number_of}]
    1.26 -        addsimps @{thms neg_simps}
    1.27 +        addsimps [@{thm Nat_Numeral.int_numeral}]
    1.28        fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1       
    1.29      in Goal.norm_result (Goal.prove_internal [] eq tac) end
    1.30  
    1.31 @@ -507,7 +506,7 @@
    1.32  
    1.33    fun int_conv ctxt ct =
    1.34      (case Thm.term_of ct of
    1.35 -      @{const of_nat (int)} $ (n as (@{const number_of (nat)} $ _)) =>
    1.36 +      @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) =>
    1.37          Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
    1.38      | @{const of_nat (int)} $ _ =>
    1.39          (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
    1.40 @@ -549,23 +548,15 @@
    1.41      rewrite Numeral1 into 1
    1.42    *)
    1.43  
    1.44 -  fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) $ _) =
    1.45 +  fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) =
    1.46          (case try HOLogic.dest_number t of
    1.47            SOME (_, i) => SMT_Builtin.is_builtin_num ctxt t andalso i < 2
    1.48          | NONE => false)
    1.49      | is_strange_number _ _ = false
    1.50  
    1.51    val pos_num_ss = HOL_ss
    1.52 -    addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}]
    1.53 -    addsimps [@{thm Int.number_of_Pls}, @{thm Int.numeral_1_eq_1}]
    1.54 -    addsimps @{thms Int.pred_bin_simps}
    1.55 -    addsimps @{thms Int.normalize_bin_simps}
    1.56 -    addsimps @{lemma
    1.57 -      "Int.Min = - Int.Bit1 Int.Pls"
    1.58 -      "Int.Bit0 (- Int.Pls) = - Int.Pls"
    1.59 -      "Int.Bit0 (- k) = - Int.Bit0 k"
    1.60 -      "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
    1.61 -      by simp_all (simp add: pred_def)}
    1.62 +    addsimps [@{thm Num.numeral_One}]
    1.63 +    addsimps [@{thm Num.neg_numeral_def}]
    1.64  
    1.65    fun norm_num_conv ctxt =
    1.66      SMT_Utils.if_conv (is_strange_number ctxt)