src/HOL/Multivariate_Analysis/normarith.ML
changeset 39032 548e933b90ad
parent 37744 3daaf23b9ab4
child 40718 4d7211968607
equal deleted inserted replaced
39031:b27d6643591c 39032:548e933b90ad
    30             if not (is_ratconst (Thm.dest_arg1 t)) then acc else
    30             if not (is_ratconst (Thm.dest_arg1 t)) then acc else
    31             augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
    31             augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
    32                       (Thm.dest_arg t) acc
    32                       (Thm.dest_arg t) acc
    33       | _ => augment_norm true t acc
    33       | _ => augment_norm true t acc
    34 
    34 
    35  val cterm_lincomb_neg = FuncUtil.Ctermfunc.map Rat.neg
    35  val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
    36  fun cterm_lincomb_cmul c t =
    36  fun cterm_lincomb_cmul c t =
    37     if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn x => x */ c) t
    37     if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x */ c) t
    38  fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
    38  fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
    39  fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
    39  fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
    40  fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
    40  fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
    41 
    41 
    42  val int_lincomb_neg = FuncUtil.Intfunc.map Rat.neg
    42  val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
    43  fun int_lincomb_cmul c t =
    43  fun int_lincomb_cmul c t =
    44     if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn x => x */ c) t
    44     if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t
    45  fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
    45  fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
    46  fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
    46  fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
    47  fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
    47  fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
    48 
    48 
    49 fun vector_lincomb t = case term_of t of
    49 fun vector_lincomb t = case term_of t of