src/HOL/Tools/int_arith.ML
 changeset 29269 5c25a2012975 parent 28952 15a4b2cf8c34 child 30496 7cdcc9dd95cb
equal inserted replaced
29268:6aefc5ff8e63 29269:5c25a2012975
`     1 (*  Title:      HOL/int_arith1.ML`
`     1 (*  Title:      HOL/Tools/int_arith1.ML`
`     2     ID:         \$Id\$`
`       `
`     3     Authors:    Larry Paulson and Tobias Nipkow`
`     2     Authors:    Larry Paulson and Tobias Nipkow`
`     4 `
`     3 `
`     5 Simprocs and decision procedure for linear arithmetic.`
`     4 Simprocs and decision procedure for linear arithmetic.`
`     6 *)`
`     5 *)`
`     7 `
`     6 `
`    64 fun num_ord (i,j) =`
`    63 fun num_ord (i,j) =`
`    65   (case int_ord (abs i, abs j) of`
`    64   (case int_ord (abs i, abs j) of`
`    66     EQUAL => int_ord (Int.sign i, Int.sign j) `
`    65     EQUAL => int_ord (Int.sign i, Int.sign j) `
`    67   | ord => ord);`
`    66   | ord => ord);`
`    68 `
`    67 `
`    69 (*This resembles Term.term_ord, but it puts binary numerals before other`
`    68 (*This resembles TermOrd.term_ord, but it puts binary numerals before other`
`    70   non-atomic terms.*)`
`    69   non-atomic terms.*)`
`    71 local open Term `
`    70 local open Term `
`    72 in `
`    71 in `
`    73 fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =`
`    72 fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =`
`    74       (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)`
`    73       (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)`
`    75   | numterm_ord`
`    74   | numterm_ord`
`    76      (Const(@{const_name Int.number_of}, _) \$ v, Const(@{const_name Int.number_of}, _) \$ w) =`
`    75      (Const(@{const_name Int.number_of}, _) \$ v, Const(@{const_name Int.number_of}, _) \$ w) =`
`    77      num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)`
`    76      num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)`
`    78   | numterm_ord (Const(@{const_name Int.number_of}, _) \$ _, _) = LESS`
`    77   | numterm_ord (Const(@{const_name Int.number_of}, _) \$ _, _) = LESS`
`    79   | numterm_ord (_, Const(@{const_name Int.number_of}, _) \$ _) = GREATER`
`    78   | numterm_ord (_, Const(@{const_name Int.number_of}, _) \$ _) = GREATER`
`    80   | numterm_ord (t, u) =`
`    79   | numterm_ord (t, u) =`
`    81       (case int_ord (size_of_term t, size_of_term u) of`
`    80       (case int_ord (size_of_term t, size_of_term u) of`
`    82         EQUAL =>`
`    81         EQUAL =>`
`    83           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in`
`    82           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in`
`    84             (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)`
`    83             (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)`
`    85           end`
`    84           end`
`    86       | ord => ord)`
`    85       | ord => ord)`
`    87 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)`
`    86 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)`
`    88 end;`
`    87 end;`
`    89 `
`    88 `
`   162 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);`
`   161 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);`
`   163 `
`   162 `
`   164 (*Express t as a product of (possibly) a numeral with other sorted terms*)`
`   163 (*Express t as a product of (possibly) a numeral with other sorted terms*)`
`   165 fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) \$ t) = dest_coeff (~sign) t`
`   164 fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) \$ t) = dest_coeff (~sign) t`
`   166   | dest_coeff sign t =`
`   165   | dest_coeff sign t =`
`   167     let val ts = sort Term.term_ord (dest_prod t)`
`   166     let val ts = sort TermOrd.term_ord (dest_prod t)`
`   168         val (n, ts') = find_first_numeral [] ts`
`   167         val (n, ts') = find_first_numeral [] ts`
`   169                           handle TERM _ => (1, ts)`
`   168                           handle TERM _ => (1, ts)`
`   170     in (sign*n, mk_prod (Term.fastype_of t) ts') end;`
`   169     in (sign*n, mk_prod (Term.fastype_of t) ts') end;`
`   171 `
`   170 `
`   172 (*Find first coefficient-term THAT MATCHES u*)`
`   171 (*Find first coefficient-term THAT MATCHES u*)`