435 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0" |
435 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0" |
436 by (simp add: algebra_simps) |
436 by (simp add: algebra_simps) |
437 |
437 |
438 (* FIXME: duplicates right_minus_eq from class group_add *) |
438 (* FIXME: duplicates right_minus_eq from class group_add *) |
439 (* but only this one is declared as a simp rule. *) |
439 (* but only this one is declared as a simp rule. *) |
440 lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b" |
440 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b" |
441 by (simp add: algebra_simps) |
441 by (simp add: algebra_simps) |
442 |
442 |
443 end |
443 end |
444 |
444 |
445 subsection {* (Partially) Ordered Groups *} |
445 subsection {* (Partially) Ordered Groups *} |
770 |
770 |
771 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0" |
771 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0" |
772 by (simp add: algebra_simps) |
772 by (simp add: algebra_simps) |
773 |
773 |
774 text{*Legacy - use @{text algebra_simps} *} |
774 text{*Legacy - use @{text algebra_simps} *} |
775 lemmas group_simps[noatp] = algebra_simps |
775 lemmas group_simps[no_atp] = algebra_simps |
776 |
776 |
777 end |
777 end |
778 |
778 |
779 text{*Legacy - use @{text algebra_simps} *} |
779 text{*Legacy - use @{text algebra_simps} *} |
780 lemmas group_simps[noatp] = algebra_simps |
780 lemmas group_simps[no_atp] = algebra_simps |
781 |
781 |
782 class linordered_ab_semigroup_add = |
782 class linordered_ab_semigroup_add = |
783 linorder + ordered_ab_semigroup_add |
783 linorder + ordered_ab_semigroup_add |
784 |
784 |
785 class linordered_cancel_ab_semigroup_add = |
785 class linordered_cancel_ab_semigroup_add = |
1199 done |
1199 done |
1200 |
1200 |
1201 |
1201 |
1202 subsection {* Tools setup *} |
1202 subsection {* Tools setup *} |
1203 |
1203 |
1204 lemma add_mono_thms_linordered_semiring [noatp]: |
1204 lemma add_mono_thms_linordered_semiring [no_atp]: |
1205 fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add" |
1205 fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add" |
1206 shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" |
1206 shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" |
1207 and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" |
1207 and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" |
1208 and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l" |
1208 and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l" |
1209 and "i = j \<and> k = l \<Longrightarrow> i + k = j + l" |
1209 and "i = j \<and> k = l \<Longrightarrow> i + k = j + l" |
1210 by (rule add_mono, clarify+)+ |
1210 by (rule add_mono, clarify+)+ |
1211 |
1211 |
1212 lemma add_mono_thms_linordered_field [noatp]: |
1212 lemma add_mono_thms_linordered_field [no_atp]: |
1213 fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add" |
1213 fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add" |
1214 shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l" |
1214 shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l" |
1215 and "i = j \<and> k < l \<Longrightarrow> i + k < j + l" |
1215 and "i = j \<and> k < l \<Longrightarrow> i + k < j + l" |
1216 and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l" |
1216 and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l" |
1217 and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l" |
1217 and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l" |
1218 and "i < j \<and> k < l \<Longrightarrow> i + k < j + l" |
1218 and "i < j \<and> k < l \<Longrightarrow> i + k < j + l" |
1219 by (auto intro: add_strict_right_mono add_strict_left_mono |
1219 by (auto intro: add_strict_right_mono add_strict_left_mono |
1220 add_less_le_mono add_le_less_mono add_strict_mono) |
1220 add_less_le_mono add_le_less_mono add_strict_mono) |
1221 |
1221 |
1222 text{*Simplification of @{term "x-y < 0"}, etc.*} |
1222 text{*Simplification of @{term "x-y < 0"}, etc.*} |
1223 lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric] |
1223 lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric] |
1224 lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric] |
1224 lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric] |
1225 |
1225 |
1226 ML {* |
1226 ML {* |
1227 structure ab_group_add_cancel = Abel_Cancel |
1227 structure ab_group_add_cancel = Abel_Cancel |
1228 ( |
1228 ( |
1229 |
1229 |