equal
deleted
inserted
replaced
1455 assumes "abs (x - y) < e / 2" |
1455 assumes "abs (x - y) < e / 2" |
1456 and "abs (x' - y) < e / 2" |
1456 and "abs (x' - y) < e / 2" |
1457 shows "abs (x - x') < e" |
1457 shows "abs (x - x') < e" |
1458 using assms by linarith |
1458 using assms by linarith |
1459 |
1459 |
1460 lemma eps_leI: |
|
1461 assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y" |
|
1462 by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl) |
|
1463 |
|
1464 lemma sum_clauses: |
1460 lemma sum_clauses: |
1465 shows "sum f {} = 0" |
1461 shows "sum f {} = 0" |
1466 and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)" |
1462 and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)" |
1467 by (auto simp add: insert_absorb) |
1463 by (auto simp add: insert_absorb) |
1468 |
1464 |