# HG changeset patch
# User haftmann
# Date 1457860966 -3600
# Node ID 19f87fa0cfcbad15388c766e69b1ae878af84da8
# Parent  43d282be735051ac7250db76c09085492082eea9
more theorems on orderings

diff -r 43d282be7350 -r 19f87fa0cfcb src/HOL/Groups.thy
--- 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 +
diff -r 43d282be7350 -r 19f87fa0cfcb src/HOL/Nat.thy
--- 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)
diff -r 43d282be7350 -r 19f87fa0cfcb src/HOL/Random.thy
--- 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
 
diff -r 43d282be7350 -r 19f87fa0cfcb src/HOL/Rings.thy
--- 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
diff -r 43d282be7350 -r 19f87fa0cfcb src/HOL/UNITY/Comp/AllocBase.thy
--- 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