author haftmann Sun, 13 Mar 2016 10:22:46 +0100 changeset 62608 19f87fa0cfcb parent 62607 43d282be7350 child 62609 656e9412667c
more theorems on orderings
 src/HOL/Groups.thy file | annotate | diff | comparison | revisions src/HOL/Nat.thy file | annotate | diff | comparison | revisions src/HOL/Random.thy file | annotate | diff | comparison | revisions src/HOL/Rings.thy file | annotate | diff | comparison | revisions src/HOL/UNITY/Comp/AllocBase.thy file | annotate | diff | comparison | revisions
```--- 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

+  "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
+
+  "a = b + a \<longleftrightarrow> b = 0"
+
+  "a + b = a \<longleftrightarrow> b = 0"
+  by (auto dest: sym)
+
+  "b + a = a \<longleftrightarrow> b = 0"
+  by (auto dest: sym)
+
end

```--- 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 @@

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

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 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])

+  "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
+  using add_le_cancel_left [of a 0 b] by simp
+
+  "a + b \<le> a \<longleftrightarrow> b \<le> 0"
+  using add_le_cancel_left [of a b 0] by simp
+
+  "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
+  using add_le_cancel_right [of 0 a b] by simp
+
+  "b + a \<le> a \<longleftrightarrow> b \<le> 0"
+  using add_le_cancel_right [of b a 0] by simp
+
+  "a < a + b \<longleftrightarrow> 0 < b"
+  using add_less_cancel_left [of a 0 b] by simp
+
+  "a + b < a \<longleftrightarrow> b < 0"
+  using add_less_cancel_left [of a b 0] by simp
+
+  "a < b + a \<longleftrightarrow> 0 < b"
+  using add_less_cancel_right [of 0 a b] by 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")
-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}"

-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])
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