parameterize assoc_fold with is_numeral predicate
authorhuffman
Thu Mar 26 11:33:50 2009 -0700 (2009-03-26)
changeset 30732afca5be252d6
parent 30731 da8598ec4e98
child 30733 8fe5bf6169e9
parameterize assoc_fold with is_numeral predicate
src/HOL/Tools/int_arith.ML
src/Provers/Arith/assoc_fold.ML
     1.1 --- a/src/HOL/Tools/int_arith.ML	Thu Mar 26 14:30:20 2009 +0000
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Thu Mar 26 11:33:50 2009 -0700
     1.3 @@ -377,6 +377,8 @@
     1.4  struct
     1.5    val assoc_ss = HOL_ss addsimps @{thms mult_ac}
     1.6    val eq_reflection = eq_reflection
     1.7 +  fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
     1.8 +    | is_numeral _ = false;
     1.9  end;
    1.10  
    1.11  structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
     2.1 --- a/src/Provers/Arith/assoc_fold.ML	Thu Mar 26 14:30:20 2009 +0000
     2.2 +++ b/src/Provers/Arith/assoc_fold.ML	Thu Mar 26 11:33:50 2009 -0700
     2.3 @@ -12,6 +12,7 @@
     2.4  sig
     2.5    val assoc_ss: simpset
     2.6    val eq_reflection: thm
     2.7 +  val is_numeral: term -> bool
     2.8  end;
     2.9  
    2.10  signature ASSOC_FOLD =
    2.11 @@ -29,10 +30,9 @@
    2.12  
    2.13  (*Separate the literals from the other terms being combined*)
    2.14  fun sift_terms plus (t, (lits,others)) =
    2.15 +  if Data.is_numeral t then (t::lits, others) (*new literal*) else
    2.16    (case t of
    2.17 -    Const (@{const_name Int.number_of}, _) $ _ =>       (* FIXME logic dependent *)
    2.18 -      (t::lits, others)         (*new literal*)
    2.19 -  | (f as Const _) $ x $ y =>
    2.20 +    (f as Const _) $ x $ y =>
    2.21        if f = plus
    2.22        then sift_terms plus (x, sift_terms plus (y, (lits,others)))
    2.23        else (lits, t::others)    (*arbitrary summand*)