src/HOL/Tools/SMT/smt_normalize.ML
changeset 41280 a7de9d36f4f2
parent 41224 8a104c2a186f
child 41300 528f5d00b542
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sun Dec 19 00:13:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sun Dec 19 17:55:56 2010 +0100
     1.3 @@ -431,20 +431,27 @@
     1.4      "ALL i. i < 0 --> int (nat i) = 0"
     1.5      by simp_all}
     1.6  
     1.7 -  val nat_ops = [
     1.8 +  val simple_nat_ops = [
     1.9      @{const less (nat)}, @{const less_eq (nat)},
    1.10 -    @{const Suc}, @{const plus (nat)}, @{const minus (nat)},
    1.11 -    @{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
    1.12 +    @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
    1.13 +
    1.14 +  val mult_nat_ops =
    1.15 +    [@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
    1.16 +
    1.17 +  val nat_ops = simple_nat_ops @ mult_nat_ops
    1.18  
    1.19    val nat_consts = nat_ops @ [@{const number_of (nat)},
    1.20      @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
    1.21  
    1.22    val nat_int_coercions = [@{const of_nat (int)}, @{const nat}]
    1.23  
    1.24 -  val nat_ops' = nat_int_coercions @ nat_ops
    1.25 +  val builtin_nat_ops = nat_int_coercions @ simple_nat_ops
    1.26  
    1.27    val is_nat_const = member (op aconv) nat_consts
    1.28  
    1.29 +  fun is_nat_const' @{const of_nat (int)} = true
    1.30 +    | is_nat_const' t = is_nat_const t
    1.31 +
    1.32    val expands = map mk_meta_eq @{lemma
    1.33      "0 = nat 0"
    1.34      "1 = nat 1"
    1.35 @@ -494,16 +501,17 @@
    1.36          Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
    1.37      | @{const of_nat (int)} $ _ =>
    1.38          (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
    1.39 -        Conv.top_sweep_conv nat_conv ctxt        
    1.40 +        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt        
    1.41      | _ => Conv.no_conv) ct
    1.42  
    1.43    and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
    1.44  
    1.45    and expand_conv ctxt =
    1.46 -    U.if_conv (not o is_nat_const o Term.head_of) Conv.no_conv
    1.47 +    U.if_conv (is_nat_const o Term.head_of)
    1.48        (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
    1.49 +      (int_conv ctxt)
    1.50  
    1.51 -  and nat_conv ctxt = U.if_exists_conv is_nat_const
    1.52 +  and nat_conv ctxt = U.if_exists_conv is_nat_const'
    1.53      (Conv.top_sweep_conv expand_conv ctxt)
    1.54  
    1.55    val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
    1.56 @@ -517,7 +525,7 @@
    1.57  
    1.58  val setup_nat_as_int =
    1.59    B.add_builtin_typ_ext (@{typ nat}, K true) #>
    1.60 -  fold (B.add_builtin_fun_ext' o Term.dest_Const) nat_ops'
    1.61 +  fold (B.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
    1.62  
    1.63  end
    1.64