equal
deleted
inserted
replaced
1024 |
1024 |
1025 lemma poly_mono: "abs(x) \<le> k ==> abs(poly p x) \<le> poly (map abs p) k" |
1025 lemma poly_mono: "abs(x) \<le> k ==> abs(poly p x) \<le> poly (map abs p) k" |
1026 apply (induct "p", auto) |
1026 apply (induct "p", auto) |
1027 apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans) |
1027 apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans) |
1028 apply (rule abs_triangle_ineq) |
1028 apply (rule abs_triangle_ineq) |
1029 apply (auto intro!: mult_mono, arith) |
1029 apply (auto intro!: mult_mono simp add: abs_mult, arith) |
1030 done |
1030 done |
1031 |
1031 |
1032 ML |
1032 ML |
1033 {* |
1033 {* |
1034 val padd_Nil2 = thm "padd_Nil2"; |
1034 val padd_Nil2 = thm "padd_Nil2"; |