--- a/src/HOL/Groups.thy Sun Mar 13 09:06:50 2016 +0100
+++ b/src/HOL/Groups.thy Sun Mar 13 10:22:46 2016 +0100
@@ -310,6 +310,27 @@
then show "c = a - b" by simp
qed
+lemma add_cancel_right_right [simp]:
+ "a = a + b \<longleftrightarrow> b = 0" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?Q then show ?P by simp
+next
+ assume ?P then have "a - a = a + b - a" by simp
+ then show ?Q by simp
+qed
+
+lemma add_cancel_right_left [simp]:
+ "a = b + a \<longleftrightarrow> b = 0"
+ using add_cancel_right_right [of a b] by (simp add: ac_simps)
+
+lemma add_cancel_left_right [simp]:
+ "a + b = a \<longleftrightarrow> b = 0"
+ by (auto dest: sym)
+
+lemma add_cancel_left_left [simp]:
+ "b + a = a \<longleftrightarrow> b = 0"
+ by (auto dest: sym)
+
end
class comm_monoid_diff = cancel_comm_monoid_add +
--- a/src/HOL/Nat.thy Sun Mar 13 09:06:50 2016 +0100
+++ b/src/HOL/Nat.thy Sun Mar 13 10:22:46 2016 +0100
@@ -1025,10 +1025,10 @@
by (rule add_mono)
lemma le_add2: "n \<le> ((m + n)::nat)"
-by (insert add_right_mono [of 0 m n], simp)
+ by simp
lemma le_add1: "n \<le> ((n + m)::nat)"
-by (simp add: add.commute, rule le_add2)
+ by simp
lemma less_add_Suc1: "i < Suc (i + m)"
by (rule le_less_trans, rule le_add1, rule lessI)
--- a/src/HOL/Random.thy Sun Mar 13 09:06:50 2016 +0100
+++ b/src/HOL/Random.thy Sun Mar 13 10:22:46 2016 +0100
@@ -1,4 +1,3 @@
-
(* Author: Florian Haftmann, TU Muenchen *)
section \<open>A HOL random engine\<close>
@@ -118,7 +117,7 @@
"select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
proof -
have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
- by (induct xs) (auto simp add: less_natural_def, simp add: plus_natural_def)
+ by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
then show ?thesis by (simp only: select_weight_def pick_drop_zero)
qed
--- a/src/HOL/Rings.thy Sun Mar 13 09:06:50 2016 +0100
+++ b/src/HOL/Rings.thy Sun Mar 13 10:22:46 2016 +0100
@@ -1349,6 +1349,38 @@
"a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
by (force simp add: mult_right_mono not_le [symmetric])
+lemma less_eq_add_cancel_left_greater_eq_zero [simp]:
+ "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
+ using add_le_cancel_left [of a 0 b] by simp
+
+lemma less_eq_add_cancel_left_less_eq_zero [simp]:
+ "a + b \<le> a \<longleftrightarrow> b \<le> 0"
+ using add_le_cancel_left [of a b 0] by simp
+
+lemma less_eq_add_cancel_right_greater_eq_zero [simp]:
+ "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
+ using add_le_cancel_right [of 0 a b] by simp
+
+lemma less_eq_add_cancel_right_less_eq_zero [simp]:
+ "b + a \<le> a \<longleftrightarrow> b \<le> 0"
+ using add_le_cancel_right [of b a 0] by simp
+
+lemma less_add_cancel_left_greater_zero [simp]:
+ "a < a + b \<longleftrightarrow> 0 < b"
+ using add_less_cancel_left [of a 0 b] by simp
+
+lemma less_add_cancel_left_less_zero [simp]:
+ "a + b < a \<longleftrightarrow> b < 0"
+ using add_less_cancel_left [of a b 0] by simp
+
+lemma less_add_cancel_right_greater_zero [simp]:
+ "a < b + a \<longleftrightarrow> 0 < b"
+ using add_less_cancel_right [of 0 a b] by simp
+
+lemma less_add_cancel_right_less_zero [simp]:
+ "b + a < a \<longleftrightarrow> b < 0"
+ using add_less_cancel_right [of b a 0] by simp
+
end
class linordered_semiring_1 = linordered_semiring + semiring_1
--- a/src/HOL/UNITY/Comp/AllocBase.thy Sun Mar 13 09:06:50 2016 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Sun Mar 13 10:22:46 2016 +0100
@@ -12,38 +12,32 @@
axiomatization NbT :: nat (*Number of tokens in system*)
where NbT_pos: "0 < NbT"
-(*This function merely sums the elements of a list*)
-primrec tokens :: "nat list => nat" where
- "tokens [] = 0"
-| "tokens (x#xs) = x + tokens xs"
+abbreviation (input) tokens :: "nat list \<Rightarrow> nat"
+where
+ "tokens \<equiv> listsum"
-abbreviation (input) "bag_of \<equiv> mset"
+abbreviation (input)
+ "bag_of \<equiv> mset"
-lemma setsum_fun_mono [rule_format]:
- "!!f :: nat=>nat.
- (ALL i. i<n --> f i <= g i) -->
- setsum f (lessThan n) <= setsum g (lessThan n)"
-apply (induct_tac "n")
-apply (auto simp add: lessThan_Suc)
-done
+lemma setsum_fun_mono:
+ fixes f :: "nat \<Rightarrow> nat"
+ shows "(\<And>i. i < n \<Longrightarrow> f i \<le> g i) \<Longrightarrow> setsum f {..<n} \<le> setsum g {..<n}"
+ by (induct n) (auto simp add: lessThan_Suc add_le_mono)
-lemma tokens_mono_prefix: "xs <= ys ==> tokens xs <= tokens ys"
+lemma tokens_mono_prefix: "xs \<le> ys \<Longrightarrow> tokens xs \<le> tokens ys"
by (induct ys arbitrary: xs) (auto simp add: prefix_Cons)
lemma mono_tokens: "mono tokens"
-apply (unfold mono_def)
-apply (blast intro: tokens_mono_prefix)
-done
+ using tokens_mono_prefix by (rule monoI)
(** bag_of **)
lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
- by (induct l) (simp_all add: ac_simps)
+ by (fact mset_append)
lemma subseteq_le_multiset: "A #\<subseteq># A + B"
unfolding le_multiset_def apply (cases B; simp)
-apply (rule HOL.disjI1)
apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
apply (simp add: less_multiset\<^sub>H\<^sub>O)
done
@@ -92,9 +86,10 @@
"[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]
==> bag_of (sublist l (UNION I A)) =
(\<Sum>i\<in>I. bag_of (sublist l (A i)))"
-apply (simp del: UN_simps
- add: UN_simps [symmetric] add: bag_of_sublist)
-apply (subst setsum.UNION_disjoint, auto)
+apply (auto simp add: bag_of_sublist)
+unfolding UN_simps [symmetric]
+apply (subst setsum.UNION_disjoint)
+apply auto
done
end