src/integer/CooperMath.sml

75 fun sum_var_coeffs var tm = let
79     sum_var_coeffs var (rand (rator tm)) + sum_var_coeffs var (rand tm)
83     if r = var then int_of_term l else zero
147 fun collect_in_sum var tm = let
148   (* all terms involving var in tm are collected together such that the
149      form of the tm becomes c * var + e *)
152   case partition (free_in var) summands of
544     (* turn ~ var into ~1 * var *)
569       val (var, rest) = Lib.pluck is_var mcands
572                 (mk_eq(tm, mk_mult(list_mk_mult rest, var))))
644   fun normalise_eqs var tm =
645     if is_eq tm andalso free_in var (rhs tm) then
650   fun phase2_CONV var tm = let
670       BINOP_CONV (phase2_CONV var) tm
672       RAND_CONV (phase2_CONV var) tm
673     else if free_in var tm then let
676       val var_onL = sum_var_coeffs var l
677       val var_onR = sum_var_coeffs var r
682         move_terms_from tt dir1 (free_in var) THENC
683         move_terms_from tt dir2 (not o free_in var)
751        normalise_eqs var) tm
755          RAND_CONV (collect_in_sum var) THENC
780 fun find_coeff_binop var term = let
785   if is_mult arg1 andalso rand arg1 = var then
787   else if is_mult arg2 andalso rand arg2 = var then
793 fun find_coeff_divides var term = let
799     else if is_mult t andalso rand t = var then
807 fun find_coeffs var term = let
809      the var x:
822     case find_coeff_binop var tm of
833       case find_coeff_divides var tm of
842 fun find_coeff var term =  (* works over un-negated leaves *)
843   if is_divides term then find_coeff_divides var term
844   else if is_less term orelse is_eq term then find_coeff_binop var term
889     val (var, body) = Psyntax.dest_exists term
891     val coeffs = find_coeffs var body
894      var to be the same lcm *)
909         case (find_coeff var term) of
924       val arg = mk_mult(term_of_int lcm, var)
925       val body = Term.subst[(arg |-> var)] tm
927       SYM (BETA_CONV (mk_comb(mk_abs(var, body), arg)))
933                                             (SPEC var INT_DIVIDES_1)))) THENC
940      RENAME_VARS_CONV [fst (dest_var var)] THENC
963   val (var, body) = dest_exists tm
1042     if List.exists (simple_divides var) body_conjuncts then
1045       BINDER_CONV (find_sdivides var elim_sdivides) THENC
1054     else if List.all (not o mem var o free_vars) body_conjuncts then
1070   (BINDER_CONV ((*Profile.profile "simpcst.quick"*) (find_cst var quick_cst_elim)) THENC