src/HOL/Tools/SMT/smt_normalize.ML
changeset 40579 98ebd2300823
parent 40424 7550b2cba1cb
child 40663 e080c9e68752
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 17 08:14:55 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 17 08:14:56 2010 +0100
     1.3 @@ -162,10 +162,12 @@
     1.4      addsimps [@{thm Nat_Numeral.int_nat_number_of}]
     1.5      addsimps @{thms neg_simps}
     1.6  
     1.7 +  val int_eq = Thm.cterm_of @{theory} @{const "==" (int)}
     1.8 +
     1.9    fun cancel_int_nat_simproc _ ss ct = 
    1.10      let
    1.11        val num = Thm.dest_arg (Thm.dest_arg ct)
    1.12 -      val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num
    1.13 +      val goal = Thm.mk_binop int_eq ct num
    1.14        val simpset = Simplifier.inherit_context ss cancel_int_nat_ss
    1.15        fun tac _ = Simplifier.simp_tac simpset 1
    1.16      in on_positive num (Goal.prove_internal [] goal) tac end
    1.17 @@ -180,8 +182,8 @@
    1.18    fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
    1.19  
    1.20    val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
    1.21 -  val uses_nat_int =
    1.22 -    Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
    1.23 +  val uses_nat_int = Term.exists_subterm (member (op aconv)
    1.24 +    [@{const of_nat (int)}, @{const nat}])
    1.25  in
    1.26  fun nat_as_int ctxt =
    1.27    map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
    1.28 @@ -285,7 +287,7 @@
    1.29  
    1.30  fun norm_def ctxt thm =
    1.31    (case Thm.prop_of thm of
    1.32 -    @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    1.33 +    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    1.34        norm_def ctxt (thm RS @{thm fun_cong})
    1.35    | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
    1.36        norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
    1.37 @@ -293,7 +295,7 @@
    1.38  
    1.39  fun atomize_conv ctxt ct =
    1.40    (case Thm.term_of ct of
    1.41 -    @{term "op ==>"} $ _ $ _ =>
    1.42 +    @{const "==>"} $ _ $ _ =>
    1.43        Conv.binop_conv (atomize_conv ctxt) then_conv
    1.44        Conv.rewr_conv @{thm atomize_imp}
    1.45    | Const (@{const_name "=="}, _) $ _ $ _ =>